From 4225df4f2103ad268d9646b45c67b4ee423d315f Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sat, 31 Aug 2024 09:24:43 +0000 Subject: [PATCH] Exp changes --- src/reach/avr_word_netlist.cpp | 83 ++++++++++++++++++++++++++++++++-- src/reach/avr_word_netlist.h | 20 ++++++++ src/vwn/btor2_frontend.cpp | 50 +++++++++++++++----- 3 files changed, 138 insertions(+), 15 deletions(-) diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 6f94118..49cab3e 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -1822,6 +1822,17 @@ int OpInst::get_simple_version() { void OpInst::propagate_uf() { switch (m_op) { + case Minus: { + const InstL* ch = get_children(); + 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) { + // -0 = 0 + t_simple = lhs; + } + } + } break; case Add: { const InstL* ch = get_children(); if (ch->size() == 2) { @@ -1944,6 +1955,13 @@ void OpInst::propagate_uf() { } else if (lhs == rhs) { // x > x = false t_simple = NumInst::create(0, 1, SORT()); + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) > 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } } } break; case SGr: { @@ -1956,6 +1974,15 @@ void OpInst::propagate_uf() { if (lhs == rhs) { // x >s x = false t_simple = NumInst::create(0, 1, SORT()); + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (get_size() > 1) { + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) > 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } + } } } break; case Le: { @@ -1971,6 +1998,13 @@ void OpInst::propagate_uf() { } else if (lhs == rhs) { // x < x = false t_simple = NumInst::create(0, 1, SORT()); + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) < 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } } } break; case SLe: { @@ -1983,6 +2017,15 @@ void OpInst::propagate_uf() { if (lhs == rhs) { // x 1) { + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) < 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } + } } } break; case GrEq: { @@ -1998,6 +2041,13 @@ void OpInst::propagate_uf() { } else if (lhs == rhs) { // x >= x = true t_simple = NumInst::create(1, 1, SORT()); + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) >= 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } } } break; case SGrEq: { @@ -2010,6 +2060,15 @@ void OpInst::propagate_uf() { if (lhs == rhs) { // x >=s x = true t_simple = NumInst::create(1, 1, SORT()); + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (get_size() > 1) { + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) >= 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } + } } } break; case LeEq: { @@ -2025,6 +2084,13 @@ void OpInst::propagate_uf() { } else if (lhs == rhs) { // x <= x = true t_simple = NumInst::create(1, 1, SORT()); + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), false) <= 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } } } break; case SLeEq: { @@ -2037,7 +2103,16 @@ void OpInst::propagate_uf() { if (lhs == rhs) { // x <=s x = true t_simple = NumInst::create(1, 1, SORT()); - } + } else if (NumInst::as(lhs) && NumInst::as(rhs)) { + // both are numbers + if (get_size() > 1) { + if (NumInst::as(lhs)->num_cmp(NumInst::as(rhs), true) <= 0) { + t_simple = NumInst::create(1, 1, SORT()); + } else { + t_simple = NumInst::create(0, 1, SORT()); + } + } + } } break; case BitWiseAnd: { const InstL* ch = get_children(); @@ -2142,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() { diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h index 057dd0b..820431f 100644 --- a/src/reach/avr_word_netlist.h +++ b/src/reach/avr_word_netlist.h @@ -2131,6 +2131,26 @@ class NumInst: public Inst { return m_mpz.get_si(); } + int num_cmp(NumInst* rhs, bool sign) { + assert (get_sort_type() == bvtype); + if (!sign) { + return mpz_cmp(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t()); + } else { + assert(get_size() > 1); + string str_lhs = get_mpz()->get_str(2); + string str_rhs = rhs->get_mpz()->get_str(2); + if (str_lhs[0] == '0' && str_rhs[0] == '0') { + return mpz_cmp(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t()); + } else if (str_lhs[0] == '0' && str_rhs[0] == '1') { + return 1; + } else if (str_lhs[0] == '1' && str_rhs[0] == '0') { + return -1; + } else { + return (-1)*mpz_cmpabs(get_mpz()->get_mpz_t(), rhs->get_mpz()->get_mpz_t()); + } + } + } + static Inst *read_bin(); virtual void write_bin(); diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp index a4f1885..967e11c 100644 --- a/src/vwn/btor2_frontend.cpp +++ b/src/vwn/btor2_frontend.cpp @@ -511,21 +511,49 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) { } break; case BTOR2_TAG_constd: { string snum(t.constant); + + mpz_t mpz_mask; + mpz_init(mpz_mask); + mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10)); + mpz_class t_mpzc(mpz_mask); + string str_num = t_mpzc.get_str(2); + + char bv_val[sz]; + string str_bv = ""; if (snum[0] == '-') { - if (sz == 1) { - //boolean negative means 1 (since sign bit has to be 1) - node = NumInst::create(1, sz); - } else { - mpz_t mpz_mask; - mpz_init(mpz_mask); - mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10)); - mpz_class t_mpzc(mpz_mask); - node = NumInst::create(t_mpzc, sz); + assert (str_num[0] == '-'); + + int i = 0; + int j = str_num.length() - 1; + for(; i < int(str_num.length() - 1); ++i, --j){ + bv_val[i] = (str_num[j] == '0') ? '1' : '0'; + } + for(; i < sz; ++i){ + bv_val[i] = '1'; + } + // plus one + for(i=0; i < sz; ++i){ + if(bv_val[i] == '1'){ + bv_val[i] = '0'; + }else{ + bv_val[i] = '1'; + break; + } } } else { - node = NumInst::create(snum, sz, 10, sort); + int i = 0; + int j = str_num.length() - 1; + for(; i < int(str_num.length()); ++i, --j){ + bv_val[i] = str_num[j]; + } + for(; i < sz; ++i){ + bv_val[i] = '0'; + } + } + for(int i=0; i < sz; ++i){ + str_bv = bv_val[i] + str_bv; } - // if (sz != 1) + node = NumInst::create(str_bv, sz, 2, sort); // { // string numstr = NumInst::as(node)->get_mpz()->get_str(10); // if (numstr != snum) {