Skip to content

Commit

Permalink
Minor cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Aug 28, 2024
1 parent 8364cc2 commit 289836f
Show file tree
Hide file tree
Showing 12 changed files with 66 additions and 63 deletions.
4 changes: 2 additions & 2 deletions avr.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@

DEFAULT_TOP="-"
DEFAULT_BIN="build/bin"
DEFAULT_BACKEND="y2"
DEFAULT_BACKEND="y2bt"
DEFAULT_NAME="test"
DEFAULT_PROP_SELECT="-"
DEFAULT_INIT_FILE="-"
Expand Down Expand Up @@ -65,7 +65,7 @@ def getopts(header):
p.add_argument('-n', '--name', help='<test-name> (default: %s)' % DEFAULT_NAME, type=str, default=DEFAULT_NAME)
p.add_argument('-o', '--out', help='<output-path> (default: %s)' % DEFAULT_OUT, type=str, default=DEFAULT_OUT)
p.add_argument('-b', '--bin', help='binary path (default: %s)' % DEFAULT_BIN, type=str, default=DEFAULT_BIN)
p.add_argument('--backend', help='backend to use: y2, bt, m5 (default: %s)' % DEFAULT_BACKEND, type=str, default=DEFAULT_BACKEND)
p.add_argument('--backend', help='backend to use: y2, bt, y2bt (default: %s)' % DEFAULT_BACKEND, type=str, default=DEFAULT_BACKEND)
p.add_argument('-y', '--yosys', help='path to yosys installation (default: %s)' % DEFAULT_YOSYS, type=str, default=DEFAULT_YOSYS)
p.add_argument('--vmt', help='toggles using vmt frontend (default: %s)' % DEFAULT_EN_VMT, action="count", default=0)
p.add_argument('-j', '--jg', help='toggles using jg frontend (default: %s)' % DEFAULT_EN_JG, action="count", default=0)
Expand Down
2 changes: 1 addition & 1 deletion src/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@ VWN_LOC = vwn
all:
$(MAKE) vw
$(MAKE) da
CONFIG_Y2BT=1 $(MAKE) re
CONFIG_Y2=1 $(MAKE) re
CONFIG_BT=1 $(MAKE) re
CONFIG_M5=1 $(MAKE) re

clean:
$(MAKE) vwc
Expand Down
12 changes: 6 additions & 6 deletions src/reach/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,18 +43,18 @@ ifeq ($(ENABLE_M5), 1)
LINKLIBS += $(MSAT_LIB)
CFLAGS += -D_M5
endif
ifeq ($(CONFIG_M5), 1)
CFLAGS += -DBACKEND_M5
REACH_SUFFIX = m5
endif

ifeq ($(ENABLE_Z3), 1)
Z3_DIR = $(DEPS)/z3
Z3_LIB = $(Z3_DIR)/build/lib/libz3.a
INCLUDE += -I$(Z3_DIR)/build/include
LINKLIBS += $(Z3_LIB)
CFLAGS += -D_Z3 -DBACKEND_Z3
REACH_SUFFIX = z3
CFLAGS += -D_Z3
endif

ifeq ($(CONFIG_Y2BT), 1)
CFLAGS += -DBACKEND_Y2BT
REACH_SUFFIX = y2bt
endif

DEPDIR := .d
Expand Down
2 changes: 1 addition & 1 deletion src/reach/avr_config.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ int Config::g_forward_check = 0;
int Config::g_fineness = 0;
int Config::g_lazy_assume = 0;

bool Config::g_uf_propagate = true;
bool Config::g_uf_propagate = false;
bool Config::g_uf_heavy_only = false;
bool Config::g_uf_no_bitwise = false;
bool Config::g_uf_no_sext = false;
Expand Down
18 changes: 11 additions & 7 deletions src/reach/avr_word_netlist.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1894,7 +1894,9 @@ 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(rhs) && NumInst::as(rhs)->get_num() == 0) {
// divide by 0, do nothing
} else if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
// 0 / rhs = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (lhs == rhs) {
Expand All @@ -1912,11 +1914,13 @@ 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(rhs) && NumInst::as(rhs)->get_num() == 0) {
// modulo by 0, do nothing
} else if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) {
// 0 % rhs = 0
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1) {
// lhs % 1 = 0
} else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1 && get_size() > 1) {
// lhs % 1 = 0 (if not boolean)
t_simple = NumInst::create(0, get_size(), get_sort());
} else if (lhs == rhs) {
// x % x = 0
Expand Down Expand Up @@ -2135,9 +2139,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
39 changes: 27 additions & 12 deletions src/reach/reach_backend.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,30 +27,45 @@
/// Note: Only one of the below flag should be enabled

// #define BACKEND_Y2 // Yices 2 for all queries
// #define BACKEND_BT // Yices 2 for abstract, Boolector for bv queries
// #define BACKEND_M5 // Yices 2 for abstract, MathSAT 5 for bv queries
// #define BACKEND_BT // Boolector for all queries
// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries

// Use Y2 backend for all abstract queries
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE y2_API // Solver for getting unsat core
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core

/// Config: BACKEND_Y2
#ifdef BACKEND_Y2
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE y2_API // Solver for getting unsat core
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core

#define SOLVER_BV y2_API // Solver for concrete / bit-vector queries
#endif

/// Config: BACKEND_BT
#ifdef BACKEND_BT
#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
#define SOLVER_CTI bt_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH bt_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN bt_API // Solver for checking if frame restriction global
#define SOLVER_AB bt_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE bt_API // Solver for getting unsat core
#define SOLVER_MUS bt_API // Solver for getting minimal unsat core

#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
#endif

/// Config: BACKEND_M5
#ifdef BACKEND_M5
#define SOLVER_BV m5_API // Solver for concrete / bit-vector queries
/// Config: BACKEND_Y2BT
#ifdef BACKEND_Y2BT
#define SOLVER_CTI y2_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ]
#define SOLVER_REACH y2_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check
#define SOLVER_CONTAIN y2_API // Solver for checking if frame restriction global
#define SOLVER_AB y2_API // Solver for all other abstract queries: Basis check, Lemma redundancy check
#define SOLVER_CORE y2_API // Solver for getting unsat core
#define SOLVER_MUS y2_API // Solver for getting minimal unsat core

#define SOLVER_BV bt_API // Solver for concrete / bit-vector queries
#endif


Expand Down
8 changes: 0 additions & 8 deletions src/reach/reach_cegar.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3480,10 +3480,6 @@ void Reach::generalize_unsat_query(BR_QUERY& q, InstLL& muses) {
void Reach::generalize_unsat_query(BR_QUERY& q, InstLL& muses) {
bool en_y2_core = true;

#ifdef BACKEND_Z3
en_y2_core = false;
#endif

#ifdef USE_Z3_CORE
en_y2_core = false;
#endif
Expand Down Expand Up @@ -4852,10 +4848,6 @@ int Reach::ccext_block() {
Solver* mus_solver = y_solver.solver_main;
Solver* core_solver = y_solver.solver_main;

#ifdef BACKEND_Z3
core_solver = mus_solver;
#endif

// generalize_unsat_query(brQuery, muses);
generalize_unsat_query(brQuery, muses, core_solver, mus_solver);
res = 1;
Expand Down
16 changes: 4 additions & 12 deletions src/reach/reach_core.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -260,26 +260,18 @@ void Reach::init_solv()

string s = "";

#ifdef BACKEND_HYBRID
s += "y2+bt";
#endif

#ifdef BACKEND_Y2
s += "+y2";
#endif

#ifdef BACKEND_Z3
s += "+z3";
#endif

#ifdef BACKEND_M5
s += "+m5";
#endif

#ifdef BACKEND_BT
s += "+bt";
#endif

#ifdef BACKEND_Y2BT
s += "y2+bt";
#endif

_resFile << s << endl;

#ifdef _Z3
Expand Down
2 changes: 1 addition & 1 deletion src/reach/reach_y2.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7201,7 +7201,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
case OpInst::ReductionXNor: {
assert(y_ch.size() == 1);
unsigned sz = (*(ch->begin()))->get_size();
assert(sz > 1);
// assert(sz > 1);

y2_expr bit = yices_bvextract(a, 0, 0);
y2_expr bit2 = yices_bvextract(a, 1, 1);
Expand Down
20 changes: 10 additions & 10 deletions src/vwn/btor2_frontend.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -508,16 +508,16 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
} break;
case BTOR2_TAG_constd: {
string snum(t.constant);
if (sz == 1 && snum != "1") {
snum = "0";
}
node = NumInst::create(snum, sz, 10, sort);
// {
// string numstr = NumInst::as(node)->get_mpz()->get_str(10);
// if (numstr != snum) {
// btor2_loge("number error: gave " << snum << ", got " << numstr);
// }
// }
std::string binary = std::bitset<8>(strtol(snum.c_str(), NULL, 10)).to_string();
// cout << "snum: " << snum << " binary: " << binary << endl;
string snum2 = binary.substr(0, sz);
node = NumInst::create(snum2, sz, 2, sort);
// {
// string numstr = NumInst::as(node)->get_mpz()->get_str(10);
// if (numstr != snum) {
// btor2_loge("number error: gave " << snum << ", got " << numstr);
// }
// }
constants.insert(node);
done = true;
} break;
Expand Down
2 changes: 1 addition & 1 deletion src/vwn/btor2_utils.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ extern "C"

#include <list>
#include <inttypes.h> /* strtoimax, PRIdMAX, SCNdMAX */

#include <bitset>


#endif /* SRC_VWN_BTOR2_UTILS_H_ */
4 changes: 2 additions & 2 deletions workers.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,5 +12,5 @@ python3 avr.py --abstract sa+heavy --backend bt --split
python3 avr.py --kind --abstract sa --backend bt --split
python3 avr.py --abstract sa8 --split --interpol 1
python3 avr.py --abstract sa16 --split --forward 1 --backend bt
python3 avr.py --abstract sa --interpol 1 --forward 1 --backend bt
python3 avr.py --bmc --abstract sa --split
python3 avr.py --abstract sa32 --backend bt --level 0 --granularity 3
python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1

0 comments on commit 289836f

Please sign in to comment.