Skip to content

Commit

Permalink
Correct int overflow in uf partial interpretation
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Sep 10, 2024
1 parent 43ab77e commit d687a1b
Show file tree
Hide file tree
Showing 2 changed files with 37 additions and 27 deletions.
54 changes: 27 additions & 27 deletions src/reach/avr_word_netlist.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1827,7 +1827,7 @@ void OpInst::propagate_uf() {
if (ch->size() == 1) {
InstL::const_iterator cit = ch->begin();
Inst* lhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// -0 = 0
t_simple = lhs;
}
Expand All @@ -1840,10 +1840,10 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 + rhs = rhs
t_simple = rhs;
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
} else if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// lhs + 0 = lhs
t_simple = lhs;
} else {
Expand All @@ -1861,7 +1861,7 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// lhs - 0 = lhs
t_simple = lhs;
} else if (lhs == rhs) {
Expand All @@ -1877,16 +1877,16 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 * rhs = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
} else if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// lhs * 0 = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 1) {
} else if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_one()) {
// 1 * rhs = rhs
t_simple = rhs;
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1) {
} else if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_one()) {
// lhs * 1 = lhs
t_simple = lhs;
} else {
Expand All @@ -1905,12 +1905,12 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// divide by 0, do nothing
} else if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
} else if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 / rhs = ? (since rhs can be 0)
// t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1 && get_size() > 1) {
} else if (get_size() > 1 && NumInst::as(rhs) && NumInst::as(rhs)->num_is_one()) {
// lhs / 1 = lhs (if not boolean)
t_simple = lhs;
} else if (lhs == rhs) {
Expand All @@ -1928,12 +1928,12 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// modulo by 0, do nothing
} else if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
} else if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 % rhs = ? (since rhs can be 0)
// t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1 && get_size() > 1) {
} else if (get_size() > 1 && NumInst::as(rhs) && NumInst::as(rhs)->num_is_one()) {
// lhs % 1 = 0 (if not boolean)
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (lhs == rhs) {
Expand All @@ -1949,7 +1949,7 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 > x = false
t_simple = NumInst::create(0, 1, SORT());
} else if (lhs == rhs) {
Expand Down Expand Up @@ -1992,7 +1992,7 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// x < 0 = false
t_simple = NumInst::create(0, 1, SORT());
} else if (lhs == rhs) {
Expand Down Expand Up @@ -2035,7 +2035,7 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// x >= 0 = true
t_simple = NumInst::create(1, 1, SORT());
} else if (lhs == rhs) {
Expand Down Expand Up @@ -2078,7 +2078,7 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 <= x = true
t_simple = NumInst::create(1, 1, SORT());
} else if (lhs == rhs) {
Expand Down Expand Up @@ -2121,10 +2121,10 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 & rhs = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
} else if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// lhs & 0 = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (lhs == rhs) {
Expand All @@ -2145,10 +2145,10 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 | rhs = rhs
t_simple = rhs;
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
} else if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// lhs | 0 = lhs
t_simple = lhs;
} else if (lhs == rhs) {
Expand Down Expand Up @@ -2205,10 +2205,10 @@ void OpInst::propagate_uf() {
Inst* lhs = (*cit)->get_simple();
cit++;
Inst* rhs = (*cit)->get_simple();
if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
if (NumInst::as(lhs) && NumInst::as(lhs)->num_is_zero()) {
// 0 shift rhs = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) {
} else if (NumInst::as(rhs) && NumInst::as(rhs)->num_is_zero()) {
// lhs shift 0 = lhs
t_simple = lhs;
}
Expand All @@ -2217,9 +2217,9 @@ void OpInst::propagate_uf() {
;
}

// if (this != this->get_simple()) {
// cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl;
// }
if (this != this->get_simple()) {
cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl;
}
}

bool OpInst::is_heavy_uf() {
Expand Down
10 changes: 10 additions & 0 deletions src/reach/avr_word_netlist.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2131,6 +2131,16 @@ class NumInst: public Inst {
return m_mpz.get_si();
}

bool num_is_zero() {
assert (get_sort_type() == bvtype);
return mpz_sgn(get_mpz()->get_mpz_t()) == 0;
}

bool num_is_one() {
assert (get_sort_type() == bvtype);
return mpz_cmp_ui(get_mpz()->get_mpz_t(), 1) == 0;
}

int num_cmp(NumInst* rhs, bool sign) {
assert (get_sort_type() == bvtype);
if (!sign) {
Expand Down

0 comments on commit d687a1b

Please sign in to comment.