Skip to content

Commit

Permalink
Fixes and missing operator implementations for btorsim (#25)
Browse files Browse the repository at this point in the history 
* btorsim: mark iff as implemented

Btorsim already has an implementation for iff, but it wasn't marked as
implemented.

* btorsim: fix sra not working

The previous sra implementation wasn't working for negative inputs.
The implementation was extracting the wrong sign bit (from b instead of
a) and also accidently forgot to use it in the conditional, and used
not_a instead.

* btorsim: implement rol and ror

This is a simple implementation delegating to sll and srl and or-ing the
results together

* btorsim: implement smod

Smod implementation taken from boolector (src/btorexp.c:1528)

---------

Signed-off-by: Ferdinand Bachmann <[email protected]>
  • Loading branch information
@Ferdi265
Ferdi265 authored Aug 7, 2024
1 parent ff44a21 commit 44bcadb
Show file tree
Hide file tree
Showing 3 changed files with 130 additions and 7 deletions.
28 changes: 25 additions & 3 deletions src/btorsim/btorsim.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,7 @@ parse_model_line (Btor2Line *l)
case BTOR2_TAG_implies:
case BTOR2_TAG_inc:
case BTOR2_TAG_ite:
case BTOR2_TAG_iff:
case BTOR2_TAG_mul:
case BTOR2_TAG_nand:
case BTOR2_TAG_neg:
Expand All @@ -256,6 +257,8 @@ parse_model_line (Btor2Line *l)
case BTOR2_TAG_redand:
case BTOR2_TAG_redor:
case BTOR2_TAG_redxor:
case BTOR2_TAG_rol:
case BTOR2_TAG_ror:
case BTOR2_TAG_sdiv:
case BTOR2_TAG_sext:
case BTOR2_TAG_sgt:
Expand All @@ -264,6 +267,7 @@ parse_model_line (Btor2Line *l)
case BTOR2_TAG_sll:
case BTOR2_TAG_slt:
case BTOR2_TAG_slte:
case BTOR2_TAG_smod:
case BTOR2_TAG_sra:
case BTOR2_TAG_srem:
case BTOR2_TAG_srl:
Expand All @@ -283,11 +287,8 @@ parse_model_line (Btor2Line *l)

case BTOR2_TAG_fair:
case BTOR2_TAG_justice:
case BTOR2_TAG_rol:
case BTOR2_TAG_ror:
case BTOR2_TAG_saddo:
case BTOR2_TAG_sdivo:
case BTOR2_TAG_smod:
case BTOR2_TAG_smulo:
case BTOR2_TAG_ssubo:
case BTOR2_TAG_uaddo:
Expand Down Expand Up @@ -546,6 +547,20 @@ simulate (int64_t id)
assert (args[0].type == BtorSimState::Type::BITVEC);
res.bv_state = btorsim_bv_redxor (args[0].bv_state);
break;
case BTOR2_TAG_rol:
assert (l->nargs == 2);
assert (res.type == BtorSimState::Type::BITVEC);
assert (args[0].type == BtorSimState::Type::BITVEC);
assert (args[1].type == BtorSimState::Type::BITVEC);
res.bv_state = btorsim_bv_rol (args[0].bv_state, args[1].bv_state);
break;
case BTOR2_TAG_ror:
assert (l->nargs == 2);
assert (res.type == BtorSimState::Type::BITVEC);
assert (args[0].type == BtorSimState::Type::BITVEC);
assert (args[1].type == BtorSimState::Type::BITVEC);
res.bv_state = btorsim_bv_ror (args[0].bv_state, args[1].bv_state);
break;
case BTOR2_TAG_slice:
assert (l->nargs == 1);
assert (res.type == BtorSimState::Type::BITVEC);
Expand Down Expand Up @@ -609,6 +624,13 @@ simulate (int64_t id)
assert (args[1].type == BtorSimState::Type::BITVEC);
res.bv_state = btorsim_bv_sll (args[0].bv_state, args[1].bv_state);
break;
case BTOR2_TAG_smod:
assert (l->nargs == 2);
assert (res.type == BtorSimState::Type::BITVEC);
assert (args[0].type == BtorSimState::Type::BITVEC);
assert (args[1].type == BtorSimState::Type::BITVEC);
res.bv_state = btorsim_bv_smod (args[0].bv_state, args[1].bv_state);
break;
case BTOR2_TAG_srl:
assert (l->nargs == 2);
assert (res.type == BtorSimState::Type::BITVEC);
Expand Down
100 changes: 96 additions & 4 deletions src/btorsim/btorsimbv.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1736,15 +1736,15 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b)
assert (a->len == b->len);
assert (a->width == b->width);

BtorSimBitVector *res, *sign_b, *srl1, *srl2, *not_a;
BtorSimBitVector *res, *sign_a, *srl1, *srl2, *not_a;

sign_b = btorsim_bv_slice (b, b->width - 1, b->width - 1);
sign_a = btorsim_bv_slice (a, a->width - 1, a->width - 1);
srl1 = btorsim_bv_srl (a, b);
not_a = btorsim_bv_not (a);
srl2 = btorsim_bv_srl (not_a, b);
res = btorsim_bv_is_true (not_a) ? btorsim_bv_not (srl2)
res = btorsim_bv_is_true (sign_a) ? btorsim_bv_not (srl2)
: btorsim_bv_copy (srl1);
btorsim_bv_free (sign_b);
btorsim_bv_free (sign_a);
btorsim_bv_free (srl1);
btorsim_bv_free (srl2);
btorsim_bv_free (not_a);
Expand All @@ -1753,6 +1753,38 @@ btorsim_bv_sra (const BtorSimBitVector *a, const BtorSimBitVector *b)
return res;
}

BtorSimBitVector *
btorsim_bv_rol (const BtorSimBitVector *a, const BtorSimBitVector *b) {
BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width);
BtorSimBitVector *rev = btorsim_bv_sub(width, b);

BtorSimBitVector *sll_part = btorsim_bv_sll(a, b);
BtorSimBitVector *srl_part = btorsim_bv_srl(a, rev);
BtorSimBitVector *res = btorsim_bv_or(sll_part, srl_part);

btorsim_bv_free(width);
btorsim_bv_free(rev);
btorsim_bv_free(sll_part);
btorsim_bv_free(srl_part);
return res;
}

BtorSimBitVector *
btorsim_bv_ror (const BtorSimBitVector *a, const BtorSimBitVector *b) {
BtorSimBitVector *width = btorsim_bv_uint64_to_bv(a->width, a->width);
BtorSimBitVector *rev = btorsim_bv_sub(width, b);

BtorSimBitVector *srl_part = btorsim_bv_srl(a, b);
BtorSimBitVector *sll_part = btorsim_bv_sll(a, rev);
BtorSimBitVector *res = btorsim_bv_or(srl_part, sll_part);

btorsim_bv_free(width);
btorsim_bv_free(rev);
btorsim_bv_free(srl_part);
btorsim_bv_free(sll_part);
return res;
}

BtorSimBitVector *
btorsim_bv_mul (const BtorSimBitVector *a, const BtorSimBitVector *b)
{
Expand Down Expand Up @@ -2001,6 +2033,66 @@ btorsim_bv_srem (const BtorSimBitVector *a, const BtorSimBitVector *b)
return res;
}

BtorSimBitVector *
btorsim_bv_smod (const BtorSimBitVector *a, const BtorSimBitVector *b)
{
assert (a);
assert (b);
assert (a->len == b->len);
assert (a->width == b->width);

BtorSimBitVector *res = 0, *not_b, *sign_a, *sign_b, *neg_a, *neg_b, *add;
BtorSimBitVector *cond_a, *cond_b, *urem, *neg_urem;
bool a_positive, b_positive;

if (a->width == 1)
{
not_b = btorsim_bv_not (b);
res = btorsim_bv_and (a, not_b);
btorsim_bv_free (not_b);
}
else
{
sign_a = btorsim_bv_slice (a, a->width - 1, a->width - 1);
sign_b = btorsim_bv_slice (b, b->width - 1, b->width - 1);
a_positive = !btorsim_bv_is_true (sign_a);
b_positive = !btorsim_bv_is_true (sign_b);

neg_a = btorsim_bv_neg (a);
neg_b = btorsim_bv_neg (b);
cond_a = a_positive ? btorsim_bv_copy (a)
: btorsim_bv_copy (neg_a);
cond_b = b_positive ? btorsim_bv_copy (b)
: btorsim_bv_copy (neg_b);


urem = btorsim_bv_urem (cond_a, cond_b);
add = btorsim_bv_is_zero(urem) ? btorsim_bv_zero(b->width)
: btorsim_bv_copy(b);

neg_urem = btorsim_bv_neg (urem);

res = a_positive && b_positive ? btorsim_bv_copy(urem)
: !a_positive && b_positive ? btorsim_bv_add(neg_urem, add)
: a_positive && !b_positive ? btorsim_bv_add(urem, add)
: btorsim_bv_copy(neg_urem);

btorsim_bv_free (sign_a);
btorsim_bv_free (sign_b);
btorsim_bv_free (neg_a);
btorsim_bv_free (neg_b);
btorsim_bv_free (cond_a);
btorsim_bv_free (cond_b);
btorsim_bv_free (urem);
btorsim_bv_free (add);
btorsim_bv_free (neg_urem);
}

assert (res);
assert (rem_bits_zero_dbg (res));
return res;
}

BtorSimBitVector *
btorsim_bv_concat (const BtorSimBitVector *a, const BtorSimBitVector *b)
{
Expand Down
9 changes: 9 additions & 0 deletions src/btorsim/btorsimbv.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,12 @@ BtorSimBitVector *btorsim_bv_srl (const BtorSimBitVector *a,
BtorSimBitVector *btorsim_bv_sra (const BtorSimBitVector *a,
const BtorSimBitVector *b);

BtorSimBitVector *btorsim_bv_rol (const BtorSimBitVector *a,
const BtorSimBitVector *b);

BtorSimBitVector *btorsim_bv_ror (const BtorSimBitVector *a,
const BtorSimBitVector *b);

BtorSimBitVector *btorsim_bv_mul (const BtorSimBitVector *a,
const BtorSimBitVector *b);

Expand All @@ -206,6 +212,9 @@ BtorSimBitVector *btorsim_bv_urem (const BtorSimBitVector *a,
BtorSimBitVector *btorsim_bv_srem (const BtorSimBitVector *a,
const BtorSimBitVector *b);

BtorSimBitVector *btorsim_bv_smod (const BtorSimBitVector *a,
const BtorSimBitVector *b);

BtorSimBitVector *btorsim_bv_ite (const BtorSimBitVector *c,
const BtorSimBitVector *t,
const BtorSimBitVector *e);
Expand Down

0 comments on commit 44bcadb

Please sign in to comment.