Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixes and missing operator implementations for btorsim #25

Merged
merged 5 commits into from
Aug 7, 2024
Merged

Fixes and missing operator implementations for btorsim #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4e9d2eb
btorsim: mark iff as implemented
Ferdi265 May 18, 2024
fd3e6f4
btorsim: fix sra not working
Ferdi265 May 20, 2024
37e4beb
btorsim: implement rol and ror
Ferdi265 May 20, 2024
51844c7
btorsim: implement smod
Ferdi265 May 20, 2024
7e1e61f
btorsim: smod: compute add_urem and add_neg_urem inline
Ferdi265 Aug 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 25 additions & 3 deletions src/btorsim/btorsim.cpp
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading