Skip to content

Commit da82ea7

Browse files
committed
fix bitvector rotation for arg > width
1 parent 4dae1e3 commit da82ea7

File tree

2 files changed

+7
-5
lines changed

2 files changed

+7
-5
lines changed

VERSION

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
1.0.1
1+
1.0.2

src/btorsim/btorsimbv.c

+6-4
Original file line numberDiff line numberDiff line change
@@ -1756,9 +1756,10 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b)
17561756
BtorSimBitVector *
17571757
btorsim_bv_rol (const BtorSimBitVector *a, const BtorSimBitVector *b) {
17581758
BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width);
1759-
BtorSimBitVector *rev = btorsim_bv_sub(width, b);
1759+
BtorSimBitVector *rem = btorsim_bv_urem(b, width);
1760+
BtorSimBitVector *rev = btorsim_bv_sub(width, rem);
17601761

1761-
BtorSimBitVector *sll_part = btorsim_bv_sll(a, b);
1762+
BtorSimBitVector *sll_part = btorsim_bv_sll(a, rem);
17621763
BtorSimBitVector *srl_part = btorsim_bv_srl(a, rev);
17631764
BtorSimBitVector *res = btorsim_bv_or(sll_part, srl_part);
17641765

@@ -1772,9 +1773,10 @@ btorsim_bv_rol (const BtorSimBitVector *a, const BtorSimBitVector *b) {
17721773
BtorSimBitVector *
17731774
btorsim_bv_ror (const BtorSimBitVector *a, const BtorSimBitVector *b) {
17741775
BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width);
1775-
BtorSimBitVector *rev = btorsim_bv_sub(width, b);
1776+
BtorSimBitVector *rem = btorsim_bv_urem(b, width);
1777+
BtorSimBitVector *rev = btorsim_bv_sub(width, rem);
17761778

1777-
BtorSimBitVector *srl_part = btorsim_bv_srl(a, b);
1779+
BtorSimBitVector *srl_part = btorsim_bv_srl(a, rem);
17781780
BtorSimBitVector *sll_part = btorsim_bv_sll(a, rev);
17791781
BtorSimBitVector *res = btorsim_bv_or(srl_part, sll_part);
17801782

0 commit comments

Comments
 (0)