From e891d9b9c70241491b3f9dafaf493168678e5eef Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sun, 25 Aug 2024 18:37:23 +0000 Subject: [PATCH 01/19] Stashing temp changes --- .gitignore | 4 +- build/avr => avr | 3 +- avr.py | 26 +++++++---- avr_pr.py | 10 ++-- deps/build_deps.sh | 2 +- src/Makefile | 33 +++++++------ src/dpa/avr_word_netlist.h | 4 ++ src/makefile.include | 13 +----- src/reach/Makefile | 50 ++++++++++++-------- src/reach/avr_word_netlist.cpp | 10 ++-- src/reach/avr_word_netlist.h | 4 ++ src/reach/reach_backend.h | 2 +- src/reach/reach_bt.cpp | 60 +++++++++++++++++++----- src/reach/reach_cegar.cpp | 11 +++-- src/reach/reach_coi.cpp | 10 +++- src/reach/reach_core.cpp | 2 +- src/reach/reach_m5.cpp | 9 +++- src/reach/reach_util.cpp | 85 ++++++++++++++-------------------- src/reach/reach_y2.cpp | 52 +++++++++------------ src/reach/reach_z3.cpp | 15 ------ src/vwn/avr_word_netlist.h | 5 ++ src/vwn/btor2_frontend.cpp | 5 +- src/vwn/ilang_frontend.cpp | 2 +- workers.txt | 30 ++++++------ 24 files changed, 247 insertions(+), 200 deletions(-) rename build/avr => avr (97%) diff --git a/.gitignore b/.gitignore index 1ad555c..9a77152 100644 --- a/.gitignore +++ b/.gitignore @@ -6,11 +6,13 @@ .idea/ build/bin*/dpa -build/bin*/reach +build/bin*/reach* build/bin*/vwn +hwmcc*/ deps/* output/* +xtras/*/ *.a *.o diff --git a/build/avr b/avr similarity index 97% rename from build/avr rename to avr index 2e4de29..7074eb4 100755 --- a/build/avr +++ b/avr @@ -35,6 +35,7 @@ enKind="${32}" bmcKmax="${33}" createAig="${34}" parseOnly="${35}" +backendSuffix="${36}" BM_PATH="$p_dir" OUT_DIR="$p_out" @@ -293,7 +294,7 @@ then exit $avr_exit fi -$p_bin/reach $OUT_PATH $p_bin > $OUT_PATH/data/reach.output 2>> >(tee -a $OUT_PATH/avr.err >&2) & echo $! > $pidFile +$p_bin/reach_${backendSuffix} $OUT_PATH $p_bin > $OUT_PATH/data/reach.output 2>> >(tee -a $OUT_PATH/avr.err >&2) & echo $! > $pidFile wait avr_exit=$? diff --git a/avr.py b/avr.py index 7ccf689..0bf84ef 100755 --- a/avr.py +++ b/avr.py @@ -23,16 +23,17 @@ DEFAULT_TOP="-" DEFAULT_BIN="build/bin" +DEFAULT_BACKEND="y2" DEFAULT_NAME="test" DEFAULT_PROP_SELECT="-" DEFAULT_INIT_FILE="-" DEFAULT_OUT="output" DEFAULT_YOSYS="deps/yosys" DEFAULT_CLK="clk" -DEFAULT_TIMEOUT=3600 -DEFAULT_MEMOUT=64000 +DEFAULT_TIMEOUT=3590 +DEFAULT_MEMOUT=118000 DEFAULT_MEMORY=False -DEFAULT_SPLIT=True +DEFAULT_SPLIT=False DEFAULT_GRANULARITY=2 DEFAULT_RANDOM=False DEFAULT_EFFORT_MININV=0 @@ -64,6 +65,7 @@ def getopts(header): p.add_argument('-n', '--name', help=' (default: %s)' % DEFAULT_NAME, type=str, default=DEFAULT_NAME) p.add_argument('-o', '--out', help=' (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('-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) @@ -123,14 +125,14 @@ def split_path(name): def main(): known, opts = getopts(header) print(short_header) - if not os.path.isfile("build/avr"): + if not os.path.isfile("avr"): raise Exception("avr: main shell script not found") if not os.path.isfile(opts.bin + "/vwn"): - raise Exception("avr: vwn binary not found") + raise Exception(f"avr: vwn binary not found in {opts.bin}") if not os.path.isfile(opts.bin + "/dpa"): - raise Exception("avr: dpa binary not found") - if not os.path.isfile(opts.bin + "/reach"): - raise Exception("avr: reach binary not found") + raise Exception(f"avr: dpa binary not found in {opts.bin}") + if not os.path.isfile(opts.bin + "/reach_" + opts.backend): + raise Exception(f"avr: reach binary not found in {opts.bin}") if not os.path.exists(opts.out): os.makedirs(opts.out) @@ -161,6 +163,8 @@ def main(): en_bt = not DEFAULT_EN_BTOR2 print("\t(output dir: %s/work_%s)" % (opts.out, opts.name)) + print("\t(backend: %s)" % opts.backend) + if (en_jg): print("\t(frontend: jg)") en_vmt = False @@ -185,7 +189,7 @@ def main(): opts.yosys = ys_path print("\t(found yosys in %s)" % opts.yosys) - command = "./build/avr" + command = "./avr" command = command + " " + f command = command + " " + str(opts.top) command = command + " " + path @@ -266,7 +270,9 @@ def main(): if (opts.parse % 2 == 1): parse_only = not DEFAULT_PARSE_ONLY command = command + " " + str(parse_only) - + + command = command + " " + str(opts.backend) + s = subprocess.call("exec " + command, shell=True) if (s != 0): raise Exception("avr ERROR: return code %d" % s) diff --git a/avr_pr.py b/avr_pr.py index 78032d2..f567b4f 100755 --- a/avr_pr.py +++ b/avr_pr.py @@ -16,7 +16,7 @@ start_time = time.time() cmdSuffix = "" -maxWorkers = 8 +maxWorkers = 16 optSuffix = " " commands = [] @@ -30,14 +30,14 @@ DEFAULT_NAME="test" DEFAULT_WORKERS="workers.txt" #DEFAULT_BIN="bin" -DEFAULT_TIMEOUT=3600 -DEFAULT_MEMOUT=16000 +DEFAULT_TIMEOUT=3590 +DEFAULT_MEMOUT=118000 DEFAULT_PRINT_SMT2=False -DEFAULT_PRINT_WITNESS=True +DEFAULT_PRINT_WITNESS=False maxTimeSec = DEFAULT_TIMEOUT maxMemMB = DEFAULT_MEMOUT -maxInitW = 2 +maxInitW = 12 resultW = 0 out_path = DEFAULT_OUT + "/" + DEFAULT_NAME diff --git a/deps/build_deps.sh b/deps/build_deps.sh index c3de164..0fcd513 100755 --- a/deps/build_deps.sh +++ b/deps/build_deps.sh @@ -1,7 +1,7 @@ #!/bin/bash -x set -e -MATHSATVERSION="5.6.10" +MATHSATVERSION="5.6.11" echo "Installing dependencies..." diff --git a/src/Makefile b/src/Makefile index abae79e..0d9a905 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,38 +1,45 @@ +#ENABLE_Y2 := 0 +#ENABLE_M5 := 0 +#ENABLE_BT := 0 +#ENABLE_Z3 := 0 + REA_LOC = reach DPA_LOC = dpa VWN_LOC = vwn all: - $(MAKE) da - $(MAKE) re $(MAKE) vw + $(MAKE) da + ENABLE_Y2=1 $(MAKE) re + ENABLE_BT=1 $(MAKE) re +# ENABLE_M5=1 $(MAKE) re clean: + $(MAKE) vwc $(MAKE) dac $(MAKE) rec - $(MAKE) vwc @echo Cleaning Complete -re: - @cd $(REA_LOC); $(MAKE) +vw: + @cd $(VWN_LOC) ; $(MAKE) @echo - @echo %%% reach: Compilation Complete. + @echo %%% vwn: Compilation Complete. da: @cd $(DPA_LOC); $(MAKE) @echo @echo %%% dpa: Compilation Complete. -vw: - @cd $(VWN_LOC) ; $(MAKE) +re: + @cd $(REA_LOC); $(MAKE) @echo - @echo %%% vwn: Compilation Complete. + @echo %%% reach: Compilation Complete. -rec: - @cd $(REA_LOC); $(MAKE) clean +vwc: + @cd $(VWN_LOC) ; $(MAKE) clean dac: @cd $(DPA_LOC); $(MAKE) clean -vwc: - @cd $(VWN_LOC) ; $(MAKE) clean +rec: + @cd $(REA_LOC); $(MAKE) clean diff --git a/src/dpa/avr_word_netlist.h b/src/dpa/avr_word_netlist.h index feb2098..e3c16da 100644 --- a/src/dpa/avr_word_netlist.h +++ b/src/dpa/avr_word_netlist.h @@ -623,6 +623,8 @@ class NumInst: public Inst { // you can't call! NumInst(unsigned long num, unsigned size, SORT sort) { + if (size == 1) + assert(num == 0 || num == 1); m_sort = sort; m_size = size; m_mpz = mpz_class(num); @@ -632,6 +634,8 @@ class NumInst: public Inst { // m_mpz.set_str(snum, base); // } NumInst(mpz_class mnum, unsigned size, SORT sort) { + if (size == 1) + assert(mnum.get_si() == 0 || mnum.get_si() == 1); m_sort = sort; m_size = size; m_mpz = mnum; diff --git a/src/makefile.include b/src/makefile.include index b64fc52..912c2d6 100644 --- a/src/makefile.include +++ b/src/makefile.include @@ -1,15 +1,5 @@ STATIC_MODE := 0 -### enable/disable solver environments -### by default, z3 environment is disabled -### also choose a BACKEND_* flag in src/reach/reach_backend.h -### to change solver backends for different kinds of SMT queries -### -ENABLE_Y2 := 1 -ENABLE_M5 := 1 -ENABLE_BT := 1 -ENABLE_Z3 := 0 - ENABLE_VMT := 1 ENABLE_BTOR2 := 1 @@ -27,7 +17,6 @@ STATIC_GMP = -lgmp STATIC_GMPXX = -lgmpxx #### reach : reachability computation -REACH_BIN = $(BIN_DIR)/reach REACH_OBJS = avr_word_netlist.o avr_util.o avr_config.o reach_sa.o reach_backend.o reach_z3.o reach_y2.o \ reach_evaluate.o reach_coi.o reach_simulate.o reach_util.o reach_tsim.o reach_solve.o \ reach_cegar.o reach_core.o reach.o reach_cex.o reach_print.o reach_bmc.o reach_bool.o @@ -53,7 +42,7 @@ ifeq ($(ENABLE_BTOR2), 1) VWN_OBJS += btor2_frontend.o btor2_parser.o endif -GPP=g++ -std=c++11 +GPP=g++ -std=c++17 #### flags CFLAG_OPT = -g -O3 diff --git a/src/reach/Makefile b/src/reach/Makefile index 1d12627..0433c90 100644 --- a/src/reach/Makefile +++ b/src/reach/Makefile @@ -10,20 +10,26 @@ else LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl endif +Y2_DIR = $(DEPS)/yices2 +Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a +INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include +LINKLIBS += $(Y2_LIB) +CFLAGS += -D_Y2 ifeq ($(ENABLE_Y2), 1) - Y2_DIR = $(DEPS)/yices2 - Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a - INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include - LINKLIBS += $(Y2_LIB) - CFLAGS += -D_Y2 + CFLAGS += -DBACKEND_Y2 + REACH_SUFFIX = y2 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 +ifeq ($(ENABLE_BT), 1) + BT_DIR = $(DEPS)/boolector + BT_LIB = $(BT_DIR)/build/lib/libboolector.a + BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a + BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a + INCLUDE += -I$(BT_DIR)/src + LINKLIBS += $(BT_LIB) + CFLAGS += -D_BT + CFLAGS += -DBACKEND_BT + REACH_SUFFIX = bt endif ifeq ($(ENABLE_M5), 1) @@ -32,16 +38,17 @@ ifeq ($(ENABLE_M5), 1) INCLUDE += -I$(MSAT_DIR)/include LINKLIBS += $(MSAT_LIB) CFLAGS += -D_M5 + CFLAGS += -DBACKEND_M5 + REACH_SUFFIX = m5 endif -ifeq ($(ENABLE_BT), 1) - BT_DIR = $(DEPS)/boolector - BT_LIB = $(BT_DIR)/build/lib/libboolector.a - BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a - BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a - INCLUDE += -I$(BT_DIR)/src - LINKLIBS += $(BT_LIB) - CFLAGS += -D_BT +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 endif DEPDIR := .d @@ -51,7 +58,10 @@ DEPFLAGS = -MT $@ -MMD -MP -MF $(DEPDIR)/$*.Td COMPILE.cc = $(CXX) $(DEPFLAGS) $(CFLAGS) $(INCLUDE) POSTCOMPILE = mv -f $(DEPDIR)/$*.Td $(DEPDIR)/$*.d +REACH_BIN = $(BIN_DIR)/reach_$(REACH_SUFFIX) + all: + rm -f *.o $(MAKE) $(REACH_BIN) $(REACH_BIN):$(REACH_OBJS) @@ -65,7 +75,7 @@ $(REACH_BIN):$(REACH_OBJS) clean: rm -f *.o - rm -f $(REACH_BIN) + rm -f $(BIN_DIR)/reach* rm -rf .d/ $(DEPDIR)/%.d: ; diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index f3573c9..04c9586 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -5427,16 +5427,16 @@ void OpInst::calc_size() { assert((*cit)->get_type() == Num); unsigned width = NumInst::as(*cit)->get_num(); cit++; + unsigned sz = NumInst::as(*cit)->get_num(); + cit++; assert((*cit)->get_type() == Num); - m_size = (*cit)->get_size(); + m_size = sz; m_sort.sz = m_size; - unsigned range = m_size; - assert(range > 0); m_sort.type = arraytype; m_sort.args.clear(); m_sort.args.push_back(SORT(width)); - m_sort.args.push_back(SORT(range)); + m_sort.args.push_back(SORT(m_size)); assert(m_size > 0); assert(m_sort.sz > 0); } @@ -5643,7 +5643,7 @@ unsigned find_size(OpInst::OpType op, InstL& exps) second++; assert((*first)->get_type() == Num); assert((*second)->get_type() == Num); - size = (*second)->get_size(); + size = NumInst::as(*second)->get_num(); assert (size > 0); } break; diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h index 812e51c..ac0f07c 100644 --- a/src/reach/avr_word_netlist.h +++ b/src/reach/avr_word_netlist.h @@ -2155,6 +2155,8 @@ class NumInst: public Inst { // you can't call! NumInst(unsigned long num, unsigned size, bool fromSystem, SORT sort) { + if (size == 1) + assert(num == 0 || num == 1); m_sort = sort; m_size = size; m_mpz = mpz_class(num); @@ -2188,6 +2190,8 @@ class NumInst: public Inst { // m_mpz.set_str(snum, base); // } NumInst(mpz_class mnum, unsigned size, bool fromSystem, SORT sort) { + if (size == 1) + assert(mnum.get_si() == 0 || mnum.get_si() == 1); m_sort = sort; m_size = size; m_mpz = mnum; diff --git a/src/reach/reach_backend.h b/src/reach/reach_backend.h index b0dd9de..88a7ec7 100644 --- a/src/reach/reach_backend.h +++ b/src/reach/reach_backend.h @@ -26,7 +26,7 @@ /// Configurations /// Note: Only one of the below flag should be enabled -#define BACKEND_Y2 // Yices 2 for all queries +// #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 diff --git a/src/reach/reach_bt.cpp b/src/reach/reach_bt.cpp index f54c2e6..df98c5c 100644 --- a/src/reach/reach_bt.cpp +++ b/src/reach/reach_bt.cpp @@ -1893,7 +1893,14 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { int maxaddress = pow(2, width) - 1; bool initialized = false; for (int i = 0; i <= maxaddress; i++) { - string v = value.substr(i*size, size); + string v; + if (value.size() <= size) { + v = value; + } else if (value.size() > (i*size)) { + v = value.substr(i*size, size); + } else { + v = "0"; + } Inst* address = NumInst::create(maxaddress - i, width, SORT()); Inst* data = NumInst::create(v, size, 2, SORT()); bt_expr_ptr b = create_bt_number(NumInst::as(data)); @@ -2180,6 +2187,10 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { case OpInst::AShiftR: case OpInst::Sext: case OpInst::Zext: + case OpInst::RotateL: + case OpInst::RotateR: + case OpInst::VRotateL: + case OpInst::VRotateR: case OpInst::IntAdd: case OpInst::IntSub: case OpInst::IntMult: @@ -2306,6 +2317,43 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { res = boolector_uext(g_ctx, a2, amount); } break; + case OpInst::RotateL: + case OpInst::RotateR: { + assert(y_ch.size() == 2); + InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); + ve_it2++; + NumInst* num = NumInst::as(*ve_it2); + cout << "Rotate: " << *e << endl; + if (num != 0) + { + int rotate_amount = num->get_mpz()->get_si() % e->get_size(); + cout << "rotate_amount: " << rotate_amount << endl; + if (rotate_amount != 0) { + if (o == OpInst::RotateL) + { + res = boolector_roli(g_ctx, a, rotate_amount); + } else { + res = boolector_rori(g_ctx, a, rotate_amount); + } + } else { + res = a; + } + } else { + cout << "Expected second operand as number in " << *e << endl; + assert(0); + } + } + break; + case OpInst::VRotateL:{ + assert(y_ch.size() == 2); + res = boolector_rol(g_ctx, a, b); + } + break; + case OpInst::VRotateR:{ + assert(y_ch.size() == 2); + res = boolector_ror(g_ctx, a, b); + } + break; case OpInst::IntAdd: { bt_loge("unsupported"); } @@ -2335,7 +2383,6 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { } } break; - case OpInst::AddC: case OpInst::AShiftL: assert(0); // for now. @@ -2364,15 +2411,6 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { res = boolector_not(g_ctx, res); } break; - case OpInst::RotateR: - case OpInst::VRotateR:{ - bt_loge("TODO"); - } - break; - case OpInst::RotateL: - case OpInst::VRotateL:{ - bt_loge("TODO"); - } break; case OpInst::VShiftL: case OpInst::VShiftR: diff --git a/src/reach/reach_cegar.cpp b/src/reach/reach_cegar.cpp index ba29ba4..8ca0ae4 100644 --- a/src/reach/reach_cegar.cpp +++ b/src/reach/reach_cegar.cpp @@ -4517,7 +4517,9 @@ int Reach::ccext_block() { s_check_result = y_solver.solver_main->s_check(AB_QUERY_TIMEOUT, false); if (s_check_result == AVR_QUSAT) { assumptions.clear(); - cube = conjunct_cube.front(); + if (!conjunct_cube.empty()) { + cube = conjunct_cube.front(); + } // possible in relational inputs (like vmt - gulwani_cegar1) AVR_LOG(15, 0, "\t(warning: F[" << frameIdx << "] has become UNSAT)" << endl); @@ -4966,10 +4968,9 @@ int Reach::ccext_block() { #ifdef AVR_ADD_INITS_ENABLE Inst *ve_gcube_before = ve_gcube; AVR_LOG(6, 1, "## call add_inits_to_gcube in ccext_block !" << endl); -// cout << "Cube: " << *cube << endl; -// cout << "Gcube: " << *ve_gcube << endl; -// cout << "Gcubes: " << gcubes << endl; -// cout << "Gcubes$: " << gcubes_next << endl; + // cout << "Cube: " << *cube << endl; + // cout << "Gcube: " << *ve_gcube << endl; + // cout << "Gcubes: " << gcubes << endl; InstL conjunct_ve_gcube; collect_cubes(ve_gcube, true); diff --git a/src/reach/reach_coi.cpp b/src/reach/reach_coi.cpp index 32eeb9e..bc1d72e 100644 --- a/src/reach/reach_coi.cpp +++ b/src/reach/reach_coi.cpp @@ -896,7 +896,13 @@ bool Reach::find_from_minset2(Solver* solver, Inst*e, InstS& relSig, InstS& relC find_from_minset2(solver, child, relSig, relConst, relUFtype); e->coi.update(child->coi); } - else if (opT == OpInst::LogAnd || opT == OpInst::LogOr) { + else if (opT == OpInst::LogAnd + || opT == OpInst::LogNand + || opT == OpInst::LogOr + || opT == OpInst::LogNor + || opT == OpInst::LogXor + || opT == OpInst::LogXNor + ) { int eVal = get_bval(solver, e); // AVR_LOG(9, 1, "[COI]: (sval) e: " << *e << "\t" << eVal << endl); if (eVal == INVALID_SVAL) { @@ -939,7 +945,7 @@ bool Reach::find_from_minset2(Solver* solver, Inst*e, InstS& relSig, InstS& relC else { string ufType = op->get_euf_func_name(); if (ufType == "0") - cout << "\t(error: unexpected uf type)\t" << *e << endl; + cout << "\t(error: unexpected uf type)\t" << *e << "\t" << op->get_op() << endl; assert (ufType != "0"); // if (_s_uf.find(e) != _s_uf.end()) { diff --git a/src/reach/reach_core.cpp b/src/reach/reach_core.cpp index bde30cc..94b99b7 100644 --- a/src/reach/reach_core.cpp +++ b/src/reach/reach_core.cpp @@ -273,7 +273,7 @@ void Reach::init_solv() #endif #ifdef BACKEND_M5 - s += "+y2"; + s += "+m5"; #endif #ifdef BACKEND_BT diff --git a/src/reach/reach_m5.cpp b/src/reach/reach_m5.cpp index b9ee356..42089f0 100644 --- a/src/reach/reach_m5.cpp +++ b/src/reach/reach_m5.cpp @@ -2632,7 +2632,14 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) { Inst* defval; for (int i = 0; i <= maxaddress; i++) { - string v = value.substr(i*size, size); + string v; + if (value.size() <= size) { + v = value; + } else if (value.size() > (i*size)) { + v = value.substr(i*size, size); + } else { + v = "0"; + } Inst* data = NumInst::create(v, size, 2, SORT()); if (i == 0) { defval = data; diff --git a/src/reach/reach_util.cpp b/src/reach/reach_util.cpp index 0328306..cdd72dd 100644 --- a/src/reach/reach_util.cpp +++ b/src/reach/reach_util.cpp @@ -401,17 +401,17 @@ Inst* Reach::replace_constant_with_value(Inst *top) { Inst* num; if (c->get_sort_type() == arraytype) { if (c->get_sort_domain()->type == bvtype && c->get_sort_range()->type == bvtype) { - string value = top->get_ival()->get_str(2); - while (value.length() < c->get_size()) - value = "0" + value; + int width = c->get_sort_domain()->sz; + int size = c->get_size(); + assert(size == c->get_sort_range()->sz); - int width = c->get_sort_domain()->sz; - int size = c->get_size(); - assert(size == c->get_sort_range()->sz); + string value = top->get_ival()->get_str(2); + while (value.length() < (c->get_size() * 2)) + value = "0" + value; Inst* wI = NumInst::create(width, 32, SORT()); Inst* sI = NumInst::create(size, 32, SORT()); - Inst* dI = NumInst::create(value, size, 2, SORT()); + Inst* dI = NumInst::create(value, value.length(), 2, SORT()); num = OpInst::create(OpInst::ArrayConst, wI, sI, dI); } else { @@ -5746,52 +5746,37 @@ void Reach::check_correctness() ve_reach = OpInst::create(OpInst::LogAnd, conjunct_reach); res = int_solver->check_sat(ve_reach, 0, false); - if(res == false) - { - AVR_LOG(8, 0, "There is a wrong (UNSAT) reachability lemma!!!" << endl); - - SOLVER_MUS tmpSolver(_abstract_mapper, AVR_EXTRA_IDX, true, regular); - tmpSolver.disable_fallback(); - tmpSolver.assert_all_wire_constraints(); - InstLL muses; - tmpSolver.get_muses_2(0, conjunct_reach, muses, num_scalls_sat_correctness, num_scalls_unsat_correctness, &tmpSolver); - cout << "mus: " << muses.front() << endl; - assert(0); - } - else - { - AVR_LOG(8, 0, "reachability-lemmas-check successful!" << endl); - } delete static_cast(int_solver); /// END - /// Checking Refinements [SAT is correct] - if(_numRefinements > 0) - { - int_solver = new SOLVER_AB(_abstract_mapper, AVR_EXTRA_IDX, false, regular); - int_solver->assert_all_wire_constraints(); - conjunct_reach.clear(); - for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3) - conjunct_reach.push_back(*it3); - - ve_reach = OpInst::create(OpInst::LogAnd, conjunct_reach); - AVR_LOG(8, 6, "Checking Q:" << conjunct_reach); - bool res = int_solver->check_sat(ve_reach, 0, false); - - if(res == false) - { - AVR_LOG(8, 0, "There is a wrong (UNSAT) datapath lemma!!!" << endl); - AVR_LOG(8, 0, "Possible errors include: incorrect assumptions" << endl); - int_solver->print_query(0, ERROR, "error"); - assert(0); - } - else - { - AVR_LOG(8, 0, "DP-lemmas-check successful!" << endl); - } - delete static_cast(int_solver); - } - /// END +// /// Checking Refinements [SAT is correct] +// if(_numRefinements > 0) +// { +// int_solver = new SOLVER_AB(_abstract_mapper, AVR_EXTRA_IDX, false, regular); +// int_solver->assert_all_wire_constraints(); +// conjunct_reach.clear(); +// for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3) +// conjunct_reach.push_back(*it3); +// +// ve_reach = OpInst::create(OpInst::LogAnd, conjunct_reach); +// AVR_LOG(8, 6, "Checking Q:" << conjunct_reach); +// bool res = int_solver->check_sat(ve_reach, 0, false); +// +// if(res == false) +// { +// AVR_LOG(8, 0, "There is a wrong (UNSAT) datapath lemma!!!" << endl); +// AVR_LOG(8, 0, "Possible errors include: incorrect assumptions" << endl); +// int_solver->print_query(0, ERROR, "error"); +// AVR_LOG(8, 0, "Checking Q:" << conjunct_reach); +// // assert(0); +// } +// else +// { +// AVR_LOG(8, 0, "DP-lemmas-check successful!" << endl); +// } +// delete static_cast(int_solver); +// } +// /// END /// (I & Refinements -> F[converged]) int_solver = new SOLVER_AB(_abstract_mapper, AVR_EXTRA_IDX, false, regular); diff --git a/src/reach/reach_y2.cpp b/src/reach/reach_y2.cpp index c0e0ec3..6d15df5 100644 --- a/src/reach/reach_y2.cpp +++ b/src/reach/reach_y2.cpp @@ -5367,7 +5367,7 @@ bool y2_API::get_relation(Inst* lhs, Inst* rhs, bool expected) bool y2_API::get_assignment(Inst* e, int& val) { - assert(e->get_sort_type() == bvtype); + assert(e->get_sort_type() == bvtype || e->get_sort_type() == arraytype); assert(m_model != NULL); y2_expr decl = e->y2_node.solv_var(get_vIdx()); @@ -6004,6 +6004,9 @@ y2_expr_ptr y2_API::create_y2_number(NumInst* num) { if (num->get_num() == 1) return m_b1; else { + if (num->get_num() != 0) { + cout << "num: " << *num << endl; + } assert (num->get_num() == 0); return m_b0; } @@ -6620,7 +6623,14 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) value = "0" + value; int maxaddress = pow(2, width) - 1; for (int i = 0; i <= maxaddress; i++) { - string v = value.substr(i*size, size); + string v; + if (value.size() <= size) { + v = value; + } else if (value.size() > (i*size)) { + v = value.substr(i*size, size); + } else { + v = "0"; + } Inst* address = NumInst::create(maxaddress - i, width, SORT()); Inst* data = NumInst::create(v, size, 2, SORT()); y2_expr_ptr a = create_y2_number(NumInst::as(address)); @@ -7085,25 +7095,12 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) assert(y_ch.size() == 2); InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); ve_it2++; - NumInst* num = NumInst::as(*ve_it2); - if (num != 0) - { - if (o == OpInst::ShiftL) - { - res = yices_shift_left0(a, num->get_mpz()->get_si()); - } else { - res = yices_shift_right0(a, num->get_mpz()->get_si()); - } - } + if (o == OpInst::ShiftR) + res = yices_bvlshr(a, b); + else if (o == OpInst::ShiftL) + res = yices_bvshl(a, b); else - { - if (o == OpInst::ShiftR) - res = yices_bvlshr(a, b); - else if (o == OpInst::ShiftL) - res = yices_bvshl(a, b); - else - assert(0); - } + assert(0); assert(res != -1); } break; @@ -7111,16 +7108,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) assert(y_ch.size() == 2); InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); ve_it2++; - NumInst* num = NumInst::as(*ve_it2); - if (num != 0) - { - res = yices_ashift_right(a, num->get_mpz()->get_si()); - assert(res != -1); - } - else - { - res = yices_bvashr(a, b); - } + res = yices_bvashr(a, b); assert(res != -1); } break; @@ -7240,6 +7228,10 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) cout << "Expected second operand as number in " << *e << endl; assert(0); } + if (res == -1) { + cout << "e: " << *e << endl; + cout << yices_error_string() << endl; + } assert(res != -1); } break; diff --git a/src/reach/reach_z3.cpp b/src/reach/reach_z3.cpp index 609756a..50e5293 100644 --- a/src/reach/reach_z3.cpp +++ b/src/reach/reach_z3.cpp @@ -5372,22 +5372,7 @@ void z3_API::inst2yices(Inst*e, bool bvAllConstraints) assert(y_ch.size() == 2); InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); ve_it2++; - NumInst* num = NumInst::as(*ve_it2); - if (num != 0) { - if (o == OpInst::ShiftL) - { - z3_expr_ptr sExpr = new z3_expr(*g_ctx); - *sExpr = shl(term(a), num->get_mpz()->get_si()); - res = sExpr; - } - else { - z3_expr_ptr sExpr = new z3_expr(*g_ctx); - *sExpr = lshr(term(a), num->get_mpz()->get_si()); - res = sExpr; - } - } - else { if (o == OpInst::ShiftR) { z3_expr_ptr sExpr = new z3_expr(*g_ctx); diff --git a/src/vwn/avr_word_netlist.h b/src/vwn/avr_word_netlist.h index 1cd05d2..3026759 100644 --- a/src/vwn/avr_word_netlist.h +++ b/src/vwn/avr_word_netlist.h @@ -660,6 +660,8 @@ class NumInst: public Inst { // you can't call! NumInst(unsigned long num, unsigned size, SORT sort) { + if (size == 1) + assert(num == 0 || num == 1); m_sort = sort; m_size = size; m_mpz = mpz_class(num); @@ -673,6 +675,9 @@ class NumInst: public Inst { // m_mpz.set_str(snum, base); // } NumInst(mpz_class mnum, unsigned size, SORT sort) { + if (size == 1) { + assert(mnum.get_si() == 0 || mnum.get_si() == 1); + } m_sort = sort; m_size = size; m_mpz = mnum; diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp index e13c962..4ba3531 100644 --- a/src/vwn/btor2_frontend.cpp +++ b/src/vwn/btor2_frontend.cpp @@ -306,7 +306,7 @@ Inst* Btor2Frontend::get_init(Btor2Line& t, int sz, SORT sort, InstL& args) { InstL args; args.push_back(NumInst::create(width, 32)); args.push_back(NumInst::create(sz, 32)); - args.push_back(NumInst::create(*value, sz)); + args.push_back(NumInst::create(*value, init_val->get_size())); rhs = OpInst::create(OpInst::ArrayConst, args); done = true; } @@ -508,6 +508,9 @@ 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); diff --git a/src/vwn/ilang_frontend.cpp b/src/vwn/ilang_frontend.cpp index 2958418..5170e61 100644 --- a/src/vwn/ilang_frontend.cpp +++ b/src/vwn/ilang_frontend.cpp @@ -1586,7 +1586,7 @@ void IlangFrontend::process_memory(Cell& c) { args.push_back(NumInst::create(width, 32)); args.push_back(NumInst::create(size, 32)); - args.push_back(NumInst::create(*value, size)); + args.push_back(NumInst::create(*value, init_val->get_size())); Inst* rhs = OpInst::create(OpInst::ArrayConst, args); initials.push_back(OpInst::create(OpInst::Eq, pre, rhs)); map_init[pre] = rhs; diff --git a/workers.txt b/workers.txt index 3e2bfa6..8410bcd 100755 --- a/workers.txt +++ b/workers.txt @@ -1,14 +1,16 @@ -python3 avr.py --bin build/bin -python3 avr.py --bin build/bin --abstract sa -python3 avr.py --bin build/bin --abstract sa --kind -python3 avr.py --bin build/bin --abstract sa --bmc -python3 avr.py --bin build/bin --split -# python3 avr.py --bin build/bin_bt_cad -# python3 avr.py --bin build/bin_bt_cad --abstract sa -python3 avr.py --bin build/bin --abstract sa8 -python3 avr.py --bin build/bin --abstract sa16 -python3 avr.py --bin build/bin --abstract sa32 -python3 avr.py --bin build/bin --level 0 -python3 avr.py --bin build/bin --level 5 -python3 avr.py --bin build/bin --interpol 1 -python3 avr.py --bin build/bin --forward 1 +python3 avr.py --split +python3 avr.py +python3 avr.py --abstract sa +python3 avr.py --kind --backend bt +python3 avr.py --abstract sa4 --split --interpol 1 --forward 1 +python3 avr.py --bmc --abstract sa --split --backend bt +python3 avr.py --kind --split +python3 avr.py --abstract sa8 --split --interpol 1 +python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1 +python3 avr.py --split --backend bt +python3 avr.py --kind --split +python3 avr.py --split --level 0 +python3 avr.py --abstract sa --interpol 1 --forward 1 --backend bt +python3 avr.py --bmc --split +python3 avr.py --abstract sa32 --granularity 3 --level 0 --backend bt +python3 avr.py --abstract sa16 --split --forward 1 --backend bt \ No newline at end of file From 93651cf27e51059dc449e1dd2d74a01ef05d8e32 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sun, 25 Aug 2024 19:28:01 +0000 Subject: [PATCH 02/19] Temp changes --- src/reach/avr_config.cpp | 14 +++++++------- src/reach/avr_config.h | 4 ++-- src/reach/avr_word_netlist.cpp | 20 ++++++++++++++++++++ src/reach/avr_word_netlist.h | 1 + src/reach/reach_bt.cpp | 8 ++++---- src/reach/reach_cegar.cpp | 4 ++-- src/reach/reach_core.h | 6 +++--- src/reach/reach_m5.cpp | 4 ++-- src/reach/reach_y2.cpp | 4 ++-- 9 files changed, 43 insertions(+), 22 deletions(-) diff --git a/src/reach/avr_config.cpp b/src/reach/avr_config.cpp index 53390b7..7823a0b 100644 --- a/src/reach/avr_config.cpp +++ b/src/reach/avr_config.cpp @@ -27,7 +27,7 @@ int Config::g_fineness = 0; int Config::g_lazy_assume = 0; bool Config::g_uf_unordered = false; -bool Config::g_uf_mult_only = false; +bool Config::g_uf_heavy_only = false; bool Config::g_uf_no_bitwise = false; bool Config::g_uf_no_sext = false; bool Config::g_uf_no_shift = false; @@ -249,8 +249,8 @@ void Config::set_abstraction(string& name) { { if (name.find(NAME_UF_UNORDERED) != string::npos) g_uf_unordered = !g_uf_unordered; - if (name.find(NAME_UF_MULT_ONLY) != string::npos) - g_uf_mult_only = !g_uf_mult_only; + if (name.find(NAME_UF_HEAVY_ONLY) != string::npos) + g_uf_heavy_only = !g_uf_heavy_only; if (name.find(NAME_UF_NO_BITWISE) != string::npos) g_uf_no_bitwise = !g_uf_no_bitwise; if (name.find(NAME_UF_NO_SEXT) != string::npos) @@ -287,11 +287,11 @@ void Config::set_abstraction(string& name) { } } - if (g_uf_mult_only) { + if (g_uf_heavy_only) { g_ab_interpret = true; g_ab_interpret_limit = 0; - g_ab_interpret_excc = LEVEL_EXCC_ALL; - g_uf_unordered = true; + // g_ab_interpret_excc = LEVEL_EXCC_NONE; + // g_uf_unordered = false; } cerr << "\t(abstraction: " << (g_ab_interpret?"sa":"sa+uf") @@ -299,7 +299,7 @@ void Config::set_abstraction(string& name) { << ((g_ab_interpret_excc != LEVEL_EXCC_DEFAULT)?"+ec"+to_string(g_ab_interpret_excc):"") << (g_fineness != FINENESS_DEFAULT?"+l"+to_string(g_fineness):"") << (g_uf_unordered?"+unordered":"") - << (g_uf_mult_only?"+mult":"") + << (g_uf_heavy_only?"+heavy":"") << (g_uf_no_bitwise?"+nobitwise":"") << (g_uf_no_sext?"+nosignex":"") << (g_uf_no_shift?"+noshift":"") diff --git a/src/reach/avr_config.h b/src/reach/avr_config.h index 9bb4bae..270ab87 100644 --- a/src/reach/avr_config.h +++ b/src/reach/avr_config.h @@ -176,7 +176,7 @@ #define NAME_EXCC "ec" #define NAME_UF_UNORDERED "+unordered" -#define NAME_UF_MULT_ONLY "+mult" +#define NAME_UF_HEAVY_ONLY "+heavy" #define NAME_UF_NO_BITWISE "+nobitwise" #define NAME_UF_NO_SEXT "+nosignex" #define NAME_UF_NO_SHIFT "+noshift" @@ -264,7 +264,7 @@ class Config { static int g_fineness; static int g_lazy_assume; static bool g_uf_unordered; - static bool g_uf_mult_only; + static bool g_uf_heavy_only; static bool g_uf_no_bitwise; static bool g_uf_no_sext; static bool g_uf_no_shift; diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 04c9586..49af034 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -1882,6 +1882,26 @@ bool OpInst::is_unordered_uf() { } #endif +bool OpInst::is_heavy_uf() { + bool result = false; + switch (m_op) { + case Mult: + case Div: + case SDiv: + case Rem: + case SRem: + case SMod: + // case ArrayConst: + // case ArraySelect: + case ArrayStore: + result = (get_size() > 4); + break; + default: + ; + } + return result; +} + Inst* OpInst::create(OpType op, Inst* exp1, Inst* exp2, Inst* exp3, int o_size, bool to_simplify, Inst* wire, SORT sort) { if (op == OpInst::LogNot) { OpInst* opt = OpInst::as(exp1); diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h index ac0f07c..0635596 100644 --- a/src/reach/avr_word_netlist.h +++ b/src/reach/avr_word_netlist.h @@ -2560,6 +2560,7 @@ class OpInst: public Inst { int get_simple_version(); bool is_unordered_uf(); #endif +bool is_heavy_uf(); protected: OpType m_op; diff --git a/src/reach/reach_bt.cpp b/src/reach/reach_bt.cpp index df98c5c..5220fb9 100644 --- a/src/reach/reach_bt.cpp +++ b/src/reach/reach_bt.cpp @@ -1691,7 +1691,7 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { - if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (OpInst::as(e) && e != simplified) { @@ -2323,11 +2323,11 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); ve_it2++; NumInst* num = NumInst::as(*ve_it2); - cout << "Rotate: " << *e << endl; + // cout << "Rotate: " << *e << endl; if (num != 0) { int rotate_amount = num->get_mpz()->get_si() % e->get_size(); - cout << "rotate_amount: " << rotate_amount << endl; + // cout << "rotate_amount: " << rotate_amount << endl; if (rotate_amount != 0) { if (o == OpInst::RotateL) { @@ -2682,7 +2682,7 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) { #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { - if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (e != simplified) { diff --git a/src/reach/reach_cegar.cpp b/src/reach/reach_cegar.cpp index 8ca0ae4..eb2d0fa 100644 --- a/src/reach/reach_cegar.cpp +++ b/src/reach/reach_cegar.cpp @@ -94,7 +94,7 @@ void Reach::retrieve_ab_sol(Solver* solver, Inst* e, InstS& relSig, InstS& relCo #ifdef INTERPRET_EX_CC if (solver->m_allow_ex_cc) { - if (Config::g_uf_mult_only || (_abstract_mapper->fetch_op(e) == Solver::TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (_abstract_mapper->fetch_op(e) == Solver::TheoryMapper::EUF_OP) || (_abstract_mapper->fetch_op(e->t_simple) == Solver::TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (e != simplified) @@ -170,7 +170,7 @@ void Reach::retrieve_cex_val(Inst* e, Solver*solver, bool abstract, bool init_vi e->set_visit(); #ifdef INTERPRET_EX_CC - if (Config::g_uf_mult_only || solver->m_allow_ex_cc && abstract && evalSimple) + if (Config::g_uf_heavy_only || solver->m_allow_ex_cc && abstract && evalSimple) { if ((_abstract_mapper->fetch_op(e) == Solver::TheoryMapper::EUF_OP) || (_abstract_mapper->fetch_op(e->t_simple) == Solver::TheoryMapper::EUF_OP)) { diff --git a/src/reach/reach_core.h b/src/reach/reach_core.h index c3c398a..26462dc 100644 --- a/src/reach/reach_core.h +++ b/src/reach/reach_core.h @@ -683,10 +683,10 @@ class UFBV_Mapper: public Solver::TheoryMapper { if (e) { e = e->get_port(); - if (Config::g_uf_mult_only) { + if (Config::g_uf_heavy_only) { if (e->get_type() == Op) { OpInst* op = OpInst::as(e); - if (op->get_op() == OpInst::Mult) + if (op->is_heavy_uf()) return Solver::TheoryMapper::EUF_OP; } return Solver::TheoryMapper::BV_OP; @@ -709,7 +709,7 @@ class UFBV_Mapper: public Solver::TheoryMapper { return Solver::TheoryMapper::EUF_OP; } virtual Solver::TheoryMapper::VarType fetch_var(Inst*e) { - if (Config::g_uf_mult_only) + if (Config::g_uf_heavy_only) return Solver::TheoryMapper::BV_VAR; else if (Config::g_ab_interpret_excc >= LEVEL_EXCC_ALL) return Solver::TheoryMapper::BV_VAR; diff --git a/src/reach/reach_m5.cpp b/src/reach/reach_m5.cpp index 42089f0..93054ba 100644 --- a/src/reach/reach_m5.cpp +++ b/src/reach/reach_m5.cpp @@ -2416,7 +2416,7 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) { #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { - if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (OpInst::as(e) && e != simplified) { @@ -3508,7 +3508,7 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) { #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { - if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (e != simplified) { diff --git a/src/reach/reach_y2.cpp b/src/reach/reach_y2.cpp index 6d15df5..7d20406 100644 --- a/src/reach/reach_y2.cpp +++ b/src/reach/reach_y2.cpp @@ -6191,7 +6191,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { - if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (OpInst::as(e) && e != simplified) @@ -7820,7 +7820,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { - if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || + if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (e != simplified) From fac9c3be139b3bb8895f78d5815684487fb007de Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sun, 25 Aug 2024 20:20:53 +0000 Subject: [PATCH 03/19] Fix compiling multiple backend --- src/Makefile | 11 +++-------- src/makefile.include | 5 +++++ src/reach/Makefile | 40 +++++++++++++++++++++++----------------- 3 files changed, 31 insertions(+), 25 deletions(-) diff --git a/src/Makefile b/src/Makefile index 0d9a905..c6847e3 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,8 +1,3 @@ -#ENABLE_Y2 := 0 -#ENABLE_M5 := 0 -#ENABLE_BT := 0 -#ENABLE_Z3 := 0 - REA_LOC = reach DPA_LOC = dpa VWN_LOC = vwn @@ -10,9 +5,9 @@ VWN_LOC = vwn all: $(MAKE) vw $(MAKE) da - ENABLE_Y2=1 $(MAKE) re - ENABLE_BT=1 $(MAKE) re -# ENABLE_M5=1 $(MAKE) re + CONFIG_Y2=1 $(MAKE) re + CONFIG_BT=1 $(MAKE) re + CONFIG_M5=1 $(MAKE) re clean: $(MAKE) vwc diff --git a/src/makefile.include b/src/makefile.include index 912c2d6..edd40be 100644 --- a/src/makefile.include +++ b/src/makefile.include @@ -3,6 +3,11 @@ STATIC_MODE := 0 ENABLE_VMT := 1 ENABLE_BTOR2 := 1 +ENABLE_Y2 := 1 +ENABLE_BT := 1 +ENABLE_M5 := 1 +ENABLE_Z3 := 0 + CURR_DIR = $(shell pwd) BIN_DIR = $(CURR_DIR)/../../build/bin DEPS = $(CURR_DIR)/../../deps diff --git a/src/reach/Makefile b/src/reach/Makefile index 0433c90..b3dcca2 100644 --- a/src/reach/Makefile +++ b/src/reach/Makefile @@ -10,34 +10,40 @@ else LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl endif -Y2_DIR = $(DEPS)/yices2 -Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a -INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include -LINKLIBS += $(Y2_LIB) -CFLAGS += -D_Y2 ifeq ($(ENABLE_Y2), 1) + Y2_DIR = $(DEPS)/yices2 + Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a + INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include + LINKLIBS += $(Y2_LIB) + CFLAGS += -D_Y2 +endif +ifeq ($(CONFIG_Y2), 1) CFLAGS += -DBACKEND_Y2 REACH_SUFFIX = y2 endif ifeq ($(ENABLE_BT), 1) - BT_DIR = $(DEPS)/boolector - BT_LIB = $(BT_DIR)/build/lib/libboolector.a - BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a - BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a - INCLUDE += -I$(BT_DIR)/src - LINKLIBS += $(BT_LIB) - CFLAGS += -D_BT + BT_DIR = $(DEPS)/boolector + BT_LIB = $(BT_DIR)/build/lib/libboolector.a + BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a + BT_LIB += $(BT_DIR)/deps/cadical/build/libcadical.a + INCLUDE += -I$(BT_DIR)/src + LINKLIBS += $(BT_LIB) + CFLAGS += -D_BT +endif +ifeq ($(CONFIG_BT), 1) CFLAGS += -DBACKEND_BT REACH_SUFFIX = bt endif ifeq ($(ENABLE_M5), 1) - MSAT_DIR = $(DEPS)/mathsat - MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a $(STATIC_GMPXX) $(STATIC_GMP) - INCLUDE += -I$(MSAT_DIR)/include - LINKLIBS += $(MSAT_LIB) - CFLAGS += -D_M5 + MSAT_DIR = $(DEPS)/mathsat + MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a # $(STATIC_GMPXX) $(STATIC_GMP) + INCLUDE += -I$(MSAT_DIR)/include + LINKLIBS += $(MSAT_LIB) + CFLAGS += -D_M5 +endif +ifeq ($(CONFIG_M5), 1) CFLAGS += -DBACKEND_M5 REACH_SUFFIX = m5 endif From 48518dcd228571704ef8bd2b1d78e74f56da2c66 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 26 Aug 2024 23:03:45 +0000 Subject: [PATCH 04/19] Stash temp changes --- src/reach/avr_config.cpp | 8 +- src/reach/avr_config.h | 4 +- src/reach/avr_word_netlist.cpp | 384 ++++- src/reach/avr_word_netlist.h | 2 +- src/reach/reach_y2.cpp | 2709 ++++++++++++++++---------------- workers.txt | 24 +- 6 files changed, 1689 insertions(+), 1442 deletions(-) diff --git a/src/reach/avr_config.cpp b/src/reach/avr_config.cpp index 7823a0b..62ac4a2 100644 --- a/src/reach/avr_config.cpp +++ b/src/reach/avr_config.cpp @@ -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_unordered = false; +bool Config::g_uf_propagate = true; bool Config::g_uf_heavy_only = false; bool Config::g_uf_no_bitwise = false; bool Config::g_uf_no_sext = false; @@ -247,8 +247,8 @@ void Config::set_abstraction(string& name) { g_ab_interpret_excc = LEVEL_EXCC_DEFAULT; { - if (name.find(NAME_UF_UNORDERED) != string::npos) - g_uf_unordered = !g_uf_unordered; + if (name.find(NAME_UF_PROPAGATE) != string::npos) + g_uf_propagate = !g_uf_propagate; if (name.find(NAME_UF_HEAVY_ONLY) != string::npos) g_uf_heavy_only = !g_uf_heavy_only; if (name.find(NAME_UF_NO_BITWISE) != string::npos) @@ -298,7 +298,7 @@ void Config::set_abstraction(string& name) { << (g_ab_interpret_limit == 0?"":to_string(g_ab_interpret_limit)) << ((g_ab_interpret_excc != LEVEL_EXCC_DEFAULT)?"+ec"+to_string(g_ab_interpret_excc):"") << (g_fineness != FINENESS_DEFAULT?"+l"+to_string(g_fineness):"") - << (g_uf_unordered?"+unordered":"") + << (g_uf_propagate?"+propagate":"") << (g_uf_heavy_only?"+heavy":"") << (g_uf_no_bitwise?"+nobitwise":"") << (g_uf_no_sext?"+nosignex":"") diff --git a/src/reach/avr_config.h b/src/reach/avr_config.h index 270ab87..3c04a22 100644 --- a/src/reach/avr_config.h +++ b/src/reach/avr_config.h @@ -175,7 +175,7 @@ #define NAME_SABV "sa" #define NAME_EXCC "ec" -#define NAME_UF_UNORDERED "+unordered" +#define NAME_UF_PROPAGATE "+propagate" #define NAME_UF_HEAVY_ONLY "+heavy" #define NAME_UF_NO_BITWISE "+nobitwise" #define NAME_UF_NO_SEXT "+nosignex" @@ -263,7 +263,7 @@ class Config { static int g_forward_check; static int g_fineness; static int g_lazy_assume; - static bool g_uf_unordered; + static bool g_uf_propagate; static bool g_uf_heavy_only; static bool g_uf_no_bitwise; static bool g_uf_no_sext; diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 49af034..cf8c60b 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -1818,69 +1818,327 @@ int OpInst::get_simple_version() { } return version; } +#endif -bool OpInst::is_unordered_uf() { - bool result = false; +void OpInst::propagate_uf() { switch (m_op) { - case BitWiseAnd: - case BitWiseOr: - case BitWiseXor: - case BitWiseXNor: + case Add: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) { + // 0 + rhs = rhs + t_simple = rhs; + } else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) { + // lhs + 0 = lhs + t_simple = lhs; + } else { + // InstL newCh; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) + // newCh.push_front(*cit); + // t_simple = OpInst::create(m_op, newCh, get_size(), false); + } + } + } break; + case Sub: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) { + // lhs - 0 = lhs + t_simple = lhs; + } else if (lhs == rhs) { + // x - x = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } + } + } break; + case Mult: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + 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() == 0) { + // lhs * 0 = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } else if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 1) { + // 1 * rhs = rhs + t_simple = rhs; + } else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1) { + // lhs * 1 = lhs + t_simple = lhs; + } else { + // InstL newCh; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) + // newCh.push_front(*cit); + // t_simple = OpInst::create(m_op, newCh, get_size(), false); + } + } + } break; + case Div: + case SDiv: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + 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) { + // x / x = 1 + t_simple = NumInst::create(1, get_size(), get_sort()); + } + } + } break; + case Rem: + case SRem: + case SMod: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + 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(lhs)->get_num() == 1) { + // lhs % 1 = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } else if (lhs == rhs) { + // x % x = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } + } + } break; + case Gr: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) { + // 0 > x = false + t_simple = NumInst::create(0, 1, SORT()); + } else if (lhs == rhs) { + // x > x = false + t_simple = NumInst::create(0, 1, SORT()); + } + } break; + case SGr: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (lhs == rhs) { + // x >s x = false + t_simple = NumInst::create(0, 1, SORT()); + } + } break; + case Le: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) { + // x < 0 = false + t_simple = NumInst::create(0, 1, SORT()); + } else if (lhs == rhs) { + // x < x = false + t_simple = NumInst::create(0, 1, SORT()); + } + } break; + case SLe: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (lhs == rhs) { + // x size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) { + // x >= 0 = true + t_simple = NumInst::create(1, 1, SORT()); + } else if (lhs == rhs) { + // x >= x = true + t_simple = NumInst::create(1, 1, SORT()); + } + } break; + case SGrEq: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (lhs == rhs) { + // x >=s x = true + t_simple = NumInst::create(1, 1, SORT()); + } + } break; + case LeEq: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) { + // 0 <= x = true + t_simple = NumInst::create(1, 1, SORT()); + } else if (lhs == rhs) { + // x <= x = true + t_simple = NumInst::create(1, 1, SORT()); + } + } break; + case SLeEq: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (lhs == rhs) { + // x <=s x = true + t_simple = NumInst::create(1, 1, SORT()); + } + } break; + case BitWiseAnd: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + 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() == 0) { + // lhs & 0 = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } else if (lhs == rhs) { + // x & x = x + t_simple = lhs; + } else { + // InstL newCh; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) + // newCh.push_front(*cit); + // t_simple = OpInst::create(m_op, newCh, get_size(), false); + } + } + } break; + case BitWiseOr: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) { + // 0 | rhs = rhs + t_simple = rhs; + } else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) { + // lhs | 0 = lhs + t_simple = lhs; + } else if (lhs == rhs) { + // x & x = x + t_simple = lhs; + } else { + // InstL newCh; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) + // newCh.push_front(*cit); + // t_simple = OpInst::create(m_op, newCh, get_size(), false); + } + } + } break; + case BitWiseXor: { + const InstL* ch = get_children(); + if (ch->size() == 2) { + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (lhs == rhs) { + // x xor x = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } else { + // InstL newCh; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) + // newCh.push_front(*cit); + // t_simple = OpInst::create(m_op, newCh, get_size(), false); + } + } + } break; + case BitWiseXNor: case BitWiseNor: - case BitWiseNand: - case Add: - case Mult: - result = true; - break; -// case Sub: -// case AddC: -// case Div: -// case Mod: -// case Minus: -// case VShiftL: -// case VShiftR: -// case VAShiftL: -// case VAShiftR: -// case VRotateL: -// case VRotateR: -// case VEx: -// case RotateL: -// case RotateR: -// case Unknown: -// case Future: -// case ShiftL: -// case AShiftL: -// case ShiftR: -// case AShiftR: -// case Extract: -// case Concat: -// case Eq: -// case NotEq: -// case Ternary: -// case Gr: -// case Le: -// case GrEq: -// case LeEq: -// case ReductionAnd: -// case ReductionOr: -// case ReductionXor: -// case ReductionXNor: -// case ReductionNand: -// case ReductionNor: -// case LogNot: -// case LogNand: -// case LogNor: -// case LogAnd: -// case LogXor: -// case LogXNor: -// case LogOr: -// break; - default: + case BitWiseNand: { + // const InstL* ch = get_children(); + // assert(ch); + // + // InstL newCh; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) + // newCh.push_front(*cit); + // t_simple = OpInst::create(m_op, newCh, get_size(), false); + } break; + case ShiftL: + case ShiftR: + case AShiftL: + case AShiftR: + case VShiftL: + case VShiftR: + case VAShiftL: + case VAShiftR: { + const InstL* ch = get_children(); + assert (ch->size() == 2); + InstL::const_iterator cit = ch->begin(); + Inst* lhs = (*cit)->get_simple(); + cit++; + Inst* rhs = (*cit)->get_simple(); + if (NumInst::as(lhs) && NumInst::as(lhs)->get_num() == 0) { + // 0 shift rhs = 0 + t_simple = NumInst::create(0, get_size(), get_sort()); + } else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 0) { + // lhs shift 0 = lhs + t_simple = lhs; + } + } break; + default: ; } - return result; + + if (this != this->get_simple()) { + cout << "uf_prop: " << *this << " -> " << *(this->t_simple) << endl; + } } -#endif bool OpInst::is_heavy_uf() { bool result = false; @@ -3418,16 +3676,8 @@ Inst* OpInst::create(OpInst::OpType op, InstL exps, int o_size, bool to_simplify // return e->t_simple; // do nothing, done } - else if (Config::g_uf_unordered) { - if (e->is_unordered_uf()) { - const InstL* ch = e->get_children(); - assert(ch); - - InstL newCh; - for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); cit++) - newCh.push_front(*cit); - e->t_simple = OpInst::create(op, newCh, e->get_size(), false); - } + else if (Config::g_uf_propagate) { + e->propagate_uf(); } } } diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h index 0635596..057dd0b 100644 --- a/src/reach/avr_word_netlist.h +++ b/src/reach/avr_word_netlist.h @@ -2558,8 +2558,8 @@ class OpInst: public Inst { #ifdef INTERPRET_EX_UF int get_simple_version(); - bool is_unordered_uf(); #endif +void propagate_uf(); bool is_heavy_uf(); protected: diff --git a/src/reach/reach_y2.cpp b/src/reach/reach_y2.cpp index 7d20406..3f6c2a8 100644 --- a/src/reach/reach_y2.cpp +++ b/src/reach/reach_y2.cpp @@ -6060,16 +6060,28 @@ y2_expr_ptr y2_API::create_y2_number(NumInst* num) { } } +void y2_API::increase_cond_activity() { +// for (auto& cond: conds) { +// double act1 = -1; +// y2_get_activity(m_ctx, cond, &act1); +// y2_increase_activity(m_ctx, cond); +// double act2 = -1; +// y2_get_activity(m_ctx, cond, &act2); +//// cout << print_term(cond) << " : " << act1 << " -> " << act2 << endl; +//// assert(0); +// } +} + void y2_API::inst2yices(Inst*e, bool bvAllConstraints) { -// cout<< endl << "--en--> " << *e << endl; + // cout<< endl << "--en--> " << *e << endl; assert(e != 0); assert(m_mapper); -// cout << "m_ba_idx: " << m_ba_idx << " e->yvar_sz: " << e->yvar.size() << endl; + // cout << "m_ba_idx: " << m_ba_idx << " e->yvar_sz: " << e->yvar.size() << endl; if (e->get_visit()) { -// cout<< endl << "--gex--> " << *e << "\t" << print_term(e->yvar[m_ba_idx]) << endl; + // cout<< endl << "--gex--> " << *e << "\t" << print_term(e->yvar[m_ba_idx]) << endl; assert (e->y2_node.get_y2_key() == Y2_INFO::st_y2_key); return; @@ -6099,11 +6111,11 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) reuseAllowed = false; if (!allow_all) { -// if (w->get_name().length() > 5 && w->get_name().substr(w->get_name().length() - 5) == "$next") -// { -// ch = 0; -// } -// else + // if (w->get_name().length() > 5 && w->get_name().substr(w->get_name().length() - 5) == "$next") + // { + // ch = 0; + // } + // else { if (w->is_connected(WireInst::get_connect_key())) { @@ -6112,46 +6124,46 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) else { ch = 0; -// cout << "(ignoring wire: " << *w << ")" << endl; + // cout << "(ignoring wire: " << *w << ")" << endl; } } } #endif -// WireInst* w = WireInst::as(e); -// if (w) -// { -// if (w->is_connected(WireInst::get_connect_key())) -// { -// ch = 0; -// reuseAllowed = false; -// -// Inst* rhs = w->get_connection(); -// inst2yices(rhs); -// y_ch.push_back(rhs->y_var[yIdx]); -// s_sz.push_back(rhs->get_size()); -// assert(y_ch.back()); -// } -// } + // WireInst* w = WireInst::as(e); + // if (w) + // { + // if (w->is_connected(WireInst::get_connect_key())) + // { + // ch = 0; + // reuseAllowed = false; + // + // Inst* rhs = w->get_connection(); + // inst2yices(rhs); + // y_ch.push_back(rhs->y_var[yIdx]); + // s_sz.push_back(rhs->get_size()); + // assert(y_ch.back()); + // } + // } } } -// if (ch) -// { -// for (auto& v: *ch) -// { -// inst2yices(v); -// y_ch.push_back(v->y2_node.solv_var(yIdx)); -// s_sz.push_back(v->get_size()); -// assert(y_ch.back()); -// assert(v->y2_node.solv_vset(yIdx)); -// } -// } + // if (ch) + // { + // for (auto& v: *ch) + // { + // inst2yices(v); + // y_ch.push_back(v->y2_node.solv_var(yIdx)); + // s_sz.push_back(v->get_size()); + // assert(y_ch.back()); + // assert(v->y2_node.solv_vset(yIdx)); + // } + // } // first, collect data if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { -// assert(!m_abstract); + // assert(!m_abstract); } else if (m_mapper->fetch_var(e) == TheoryMapper::EUF_VAR) { @@ -6192,7 +6204,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) if (m_allow_ex_cc) { if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || - (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { + (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (OpInst::as(e) && e != simplified) { @@ -6203,47 +6215,47 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) } } -//#ifdef INTERPRET_UF_EXCC -// { -// OpInst* op = OpInst::as(e); -// if (op && op->get_op() == OpInst::Concat) { -// if (e->get_size() != 1) { -// -// const InstL* ch = op->get_children(); -// assert(ch); -// unsigned s_loc = 0, e_loc = 0; -//// cout << "Asserting for " << *e << endl; -// for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); ++cit) -// { -// Inst *tve = *cit; -// unsigned size = tve->get_size(); -// s_loc = e_loc; -// e_loc += size; -// unsigned ns = s_loc; -// unsigned ne = size - 1 + s_loc; -// -// { -// Inst* Ki = ExInst::create(e, ne, ns); -// Inst* eqInst = OpInst::create(OpInst::Eq, tve, Ki); -// inst2yices(eqInst); -// force(eqInst); -// } -// -// int c = 0; -// for (int i = ns; i<= ne; i++, c++) { -// Inst* lhs = ExInst::create(e, i, i); -// Inst* rhs = ExInst::create(tve, c, c); -// Inst* eqInst = OpInst::create(OpInst::Eq, lhs, rhs); -// inst2yices(eqInst); -// force(eqInst); -// } -// -//// cout << "\t" << *eqInst << endl; -// } -// } -// } -// } -//#endif + //#ifdef INTERPRET_UF_EXCC + // { + // OpInst* op = OpInst::as(e); + // if (op && op->get_op() == OpInst::Concat) { + // if (e->get_size() != 1) { + // + // const InstL* ch = op->get_children(); + // assert(ch); + // unsigned s_loc = 0, e_loc = 0; + //// cout << "Asserting for " << *e << endl; + // for (InstL::const_iterator cit = ch->begin(); cit != ch->end(); ++cit) + // { + // Inst *tve = *cit; + // unsigned size = tve->get_size(); + // s_loc = e_loc; + // e_loc += size; + // unsigned ns = s_loc; + // unsigned ne = size - 1 + s_loc; + // + // { + // Inst* Ki = ExInst::create(e, ne, ns); + // Inst* eqInst = OpInst::create(OpInst::Eq, tve, Ki); + // inst2yices(eqInst); + // force(eqInst); + // } + // + // int c = 0; + // for (int i = ns; i<= ne; i++, c++) { + // Inst* lhs = ExInst::create(e, i, i); + // Inst* rhs = ExInst::create(tve, c, c); + // Inst* eqInst = OpInst::create(OpInst::Eq, lhs, rhs); + // inst2yices(eqInst); + // force(eqInst); + // } + // + //// cout << "\t" << *eqInst << endl; + // } + // } + // } + // } + //#endif #endif @@ -6264,7 +6276,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) if (e->y2_node.solv_cset(cIdx)) { /// Constraints already set, use stored constraints. - // cout << "reusing stored constraints " << *e << " nC: " << e->y_constraints[yIdx].size() << endl; + // cout << "reusing stored constraints " << *e << " nC: " << e->y_constraints[yIdx].size() << endl; for (auto& c : e->y2_node.solv_constraints(cIdx)) { @@ -6288,7 +6300,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) e->y2_node.y2_cset[cIdx] = true; -// cout << " e: " << *e << " of type " << e->get_sort().sort2str() << endl; + // cout << " e: " << *e << " of type " << e->get_sort().sort2str() << endl; // assert(name == print_term(yvar)); // now link this node with the children's yices expressions @@ -6353,25 +6365,25 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) switch (e->get_type()) { - case Num: { - NumInst* num = NumInst::as(e); - assert(num != 0); + case Num: { + NumInst* num = NumInst::as(e); + assert(num != 0); - if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - y2_expr_ptr c = create_y2_number(num); - add_gate_constraint(yvar, c, "constant link", e, false, false); + if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + y2_expr_ptr c = create_y2_number(num); + add_gate_constraint(yvar, c, "constant link", e, false, false); - // required to remain in QF_LIA - if (e->get_sort_type() == inttype) - yvar = c; - } - else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { - yvar = ((*(num->get_mpz()) == 0) ? m_b0 : m_b1); + // required to remain in QF_LIA + if (e->get_sort_type() == inttype) + yvar = c; + } + else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { + yvar = ((*(num->get_mpz()) == 0) ? m_b0 : m_b1); -// add_constraint(yices_eq((*(num->get_mpz()) == 0) ? m_b0 : m_b1, yvar), "num to boolean conversion", e); - } - else { - add_variable(yvar, e); + // add_constraint(yices_eq((*(num->get_mpz()) == 0) ? m_b0 : m_b1, yvar), "num to boolean conversion", e); + } + else { + add_variable(yvar, e); #ifdef Y2_CREATE_UCONSTANTS y2_expr_ptr c = create_const_var(num->get_mpz(), num->get_size()); add_constraint(yices_eq(yvar, c), "num constraint", e); @@ -6392,586 +6404,508 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) #endif + } } - } break; - case Sig: { - add_variable(yvar, e); - // nothing! - } + case Sig: { + add_variable(yvar, e); + // nothing! + } break; - case Wire: { - if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { - if (y_ch.size() == 0) { - add_variable(yvar, e); - } - else { - assert(y_ch.size() == 1); - y2_expr_ptr res = y_ch.front(); + case Wire: { + if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { + if (y_ch.size() == 0) { + add_variable(yvar, e); + } + else { + assert(y_ch.size() == 1); + y2_expr_ptr res = y_ch.front(); - add_gate_constraint(yvar, res, "port connection", e, !m_abstract, false); - } - } - else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { - assert(y_ch.size() == 1); - y2_expr_ptr res = y_ch.front(); + add_gate_constraint(yvar, res, "port connection", e, !m_abstract, false); + } + } + else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { + assert(y_ch.size() == 1); + y2_expr_ptr res = y_ch.front(); - add_gate_constraint(yvar, res, "port connection", e, false, false); - } - else { - assert(0); + add_gate_constraint(yvar, res, "port connection", e, false, false); + } + else { + assert(0); + } } - } break; - case Const: { - add_variable(yvar, e); - // nothing! - } + case Const: { + add_variable(yvar, e); + // nothing! + } break; - case Op: { - OpInst* op = OpInst::as(e); - assert(op != 0); - y2_expr res = 0; - string opstr = ""; - bool interpreted = false; - - y2_expr_list::iterator it = y_ch.begin(), it2 = y_ch.begin(), end_it = y_ch.end(); - it2++; + case Op: { + OpInst* op = OpInst::as(e); + assert(op != 0); + y2_expr res = 0; + string opstr = ""; + bool interpreted = false; - OpInst::OpType o = op->get_op(); + y2_expr_list::iterator it = y_ch.begin(), it2 = y_ch.begin(), end_it = y_ch.end(); + it2++; - if (o == OpInst::BitWiseXor && op->get_size() == 1 && (m_mapper->fetch_op(e) != TheoryMapper::BV_OP)) { - o = OpInst::LogXor; - } - if (o == OpInst::BitWiseXNor && op->get_size() == 1 && (m_mapper->fetch_op(e) != TheoryMapper::BV_OP)) { - o = OpInst::LogXNor; - } + OpInst::OpType o = op->get_op(); - switch (o) { - case OpInst::Extract: - case OpInst::Unknown: - case OpInst::Future: - cout << *op << endl; - assert(0); - break; + if (o == OpInst::BitWiseXor && op->get_size() == 1 && (m_mapper->fetch_op(e) != TheoryMapper::BV_OP)) { + o = OpInst::LogXor; + } + if (o == OpInst::BitWiseXNor && op->get_size() == 1 && (m_mapper->fetch_op(e) != TheoryMapper::BV_OP)) { + o = OpInst::LogXNor; + } - // "control" operators! - case OpInst::LogNot: - case OpInst::LogNand: - case OpInst::LogNor: - case OpInst::LogAnd: - case OpInst::LogXor: - case OpInst::LogXNor: - case OpInst::LogOr: - case OpInst::Eq: - case OpInst::NotEq: - case OpInst::ArrayConst: - case OpInst::ArraySelect: - case OpInst::ArrayStore: - case OpInst::Gr: - case OpInst::SGr: - case OpInst::Le: - case OpInst::SLe: - case OpInst::GrEq: - case OpInst::SGrEq: - case OpInst::LeEq: - case OpInst::SLeEq: - case OpInst::IntLe: - case OpInst::IntLeEq: - case OpInst::IntGr: - case OpInst::IntGrEq: - { - y2_expr log = 0; switch (o) { - - case OpInst::LogNot: { - if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - log = yices_not(*it); - } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { - log = yices_not(*it); - } else { + case OpInst::Extract: + case OpInst::Unknown: + case OpInst::Future: + cout << *op << endl; assert(0); - } - assert(log != Y2_INVALID_EXPR); - interpreted = true; - } - break; - case OpInst::LogNand: - case OpInst::LogNor: - case OpInst::LogAnd: - case OpInst::LogOr: { - y2_expr arguments[y_ch.size()]; - for (unsigned j = 0; j < y_ch.size(); j++, ++it) { - arguments[j] = *it; - } + break; - if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - log = ((o == OpInst::LogAnd) || (o == OpInst::LogNand)) ? yices_and(y_ch.size(), arguments) : yices_or(y_ch.size(), arguments); - if((o == OpInst::LogNor) || (o == OpInst::LogNand)){ - log = yices_not(log); - } - } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { - log = ((o == OpInst::LogAnd) || (o == OpInst::LogNand)) ? yices_and(y_ch.size(), arguments) : yices_or(y_ch.size(), arguments); - if((o == OpInst::LogNor) || (o == OpInst::LogNand)){ - log = yices_not(log); - } - } else { - assert(0); - } - interpreted = true; - } - break; - case OpInst::LogXNor: - case OpInst::LogXor: { - y2_expr arguments[y_ch.size()]; - for (unsigned j = 0; j < y_ch.size(); j++, ++it) { - arguments[j] = *it; - } + // "control" operators! + case OpInst::LogNot: + case OpInst::LogNand: + case OpInst::LogNor: + case OpInst::LogAnd: + case OpInst::LogXor: + case OpInst::LogXNor: + case OpInst::LogOr: + case OpInst::Eq: + case OpInst::NotEq: + case OpInst::ArrayConst: + case OpInst::ArraySelect: + case OpInst::ArrayStore: + case OpInst::Gr: + case OpInst::SGr: + case OpInst::Le: + case OpInst::SLe: + case OpInst::GrEq: + case OpInst::SGrEq: + case OpInst::LeEq: + case OpInst::SLeEq: + case OpInst::IntLe: + case OpInst::IntLeEq: + case OpInst::IntGr: + case OpInst::IntGrEq: + { + y2_expr log = 0; + switch (o) { - if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - log = yices_xor(y_ch.size(), arguments); - if(o == OpInst::LogXNor){ - log = yices_not(log); - } - } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { - log = yices_xor(y_ch.size(), arguments); - if(o == OpInst::LogXNor){ - log = yices_not(log); - } - } else { - assert(0); - } - interpreted = true; - } - break; - case OpInst::Eq:{ - assert(y_ch.size() == 2); - if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - log = yices_eq(*it, *it2); - } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { - log = yices_eq(*it, *it2); + case OpInst::LogNot: { + if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + log = yices_not(*it); + } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { + log = yices_not(*it); + } else { + assert(0); + } + assert(log != Y2_INVALID_EXPR); + interpreted = true; + } + break; + case OpInst::LogNand: + case OpInst::LogNor: + case OpInst::LogAnd: + case OpInst::LogOr: { + y2_expr arguments[y_ch.size()]; + for (unsigned j = 0; j < y_ch.size(); j++, ++it) { + arguments[j] = *it; + } - assert(log); + if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + log = ((o == OpInst::LogAnd) || (o == OpInst::LogNand)) ? yices_and(y_ch.size(), arguments) : yices_or(y_ch.size(), arguments); + if((o == OpInst::LogNor) || (o == OpInst::LogNand)){ + log = yices_not(log); + } + } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { + log = ((o == OpInst::LogAnd) || (o == OpInst::LogNand)) ? yices_and(y_ch.size(), arguments) : yices_or(y_ch.size(), arguments); + if((o == OpInst::LogNor) || (o == OpInst::LogNand)){ + log = yices_not(log); + } + } else { + assert(0); + } + interpreted = true; + } + break; + case OpInst::LogXNor: + case OpInst::LogXor: { + y2_expr arguments[y_ch.size()]; + for (unsigned j = 0; j < y_ch.size(); j++, ++it) { + arguments[j] = *it; + } -//#ifdef INTERPRET_EX_CC -// if (m_allow_ex_cc) -// { -// OpInst* op_t = OpInst::as(e); -// assert(op_t); -// -// Inst* simplified = op_t->t_simple; -// if (e != simplified) -// { -// y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); -// add_constraint(yices_eq(log, a), "partial interpretation of == with Ex/Cc", e); -//// cout << "Asserting " << *e << " == " << *simplified << endl; -// } -// } -//#endif - } else { - assert(0); - } - interpreted = true; - } - break; - case OpInst::NotEq: { - assert(y_ch.size() == 2); - if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - log = yices_neq(*it, *it2); - } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { - log = yices_neq(*it, *it2); - -//#ifdef INTERPRET_EX_CC -// if (m_allow_ex_cc) -// { -// OpInst* op_t = OpInst::as(e); -// assert(op_t); -// -// Inst* simplified = op_t->t_simple; -// if (e != simplified) -// { -// y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); -// add_constraint(yices_eq(log, a), "partial interpretation of != with Ex/Cc", e); -//// cout << "Asserting " << *e << " == " << *simplified << endl; -// } -// } -//#endif - } else { - assert(0); - } - interpreted = true; - } - break; - case OpInst::ArrayConst: { - if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { - y2_type functt = create_bv_sort(make_pair(e->get_size(), e->get_sort())); - y2_expr funct = yices_new_uninterpreted_term(functt); - log = funct; -// cout << "constarray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; - - SORT* d = e->get_sort_domain(); - SORT* r = e->get_sort_range(); - assert(d->type == bvtype); - assert(r->type == bvtype); - int width = d->sz; - int size = r->sz; - - Inst* init_val = e->get_children()->back(); - assert(init_val->get_type() == Num); - string value = NumInst::as(init_val)->get_mpz()->get_str(2); - while (value.length() < e->get_size()) - value = "0" + value; - int maxaddress = pow(2, width) - 1; - for (int i = 0; i <= maxaddress; i++) { - string v; - if (value.size() <= size) { - v = value; - } else if (value.size() > (i*size)) { - v = value.substr(i*size, size); - } else { - v = "0"; + if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + log = yices_xor(y_ch.size(), arguments); + if(o == OpInst::LogXNor){ + log = yices_not(log); + } + } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { + log = yices_xor(y_ch.size(), arguments); + if(o == OpInst::LogXNor){ + log = yices_not(log); + } + } else { + assert(0); + } + interpreted = true; + } + break; + case OpInst::Eq:{ + assert(y_ch.size() == 2); + if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + log = yices_eq(*it, *it2); + } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { + log = yices_eq(*it, *it2); + + assert(log); + + //#ifdef INTERPRET_EX_CC + // if (m_allow_ex_cc) + // { + // OpInst* op_t = OpInst::as(e); + // assert(op_t); + // + // Inst* simplified = op_t->t_simple; + // if (e != simplified) + // { + // y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); + // add_constraint(yices_eq(log, a), "partial interpretation of == with Ex/Cc", e); + //// cout << "Asserting " << *e << " == " << *simplified << endl; + // } + // } + //#endif + } else { + assert(0); + } + interpreted = true; + } + break; + case OpInst::NotEq: { + assert(y_ch.size() == 2); + if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + log = yices_neq(*it, *it2); + } else if (m_mapper->fetch_var(e) == TheoryMapper::BOOL_VAR) { + log = yices_neq(*it, *it2); + + //#ifdef INTERPRET_EX_CC + // if (m_allow_ex_cc) + // { + // OpInst* op_t = OpInst::as(e); + // assert(op_t); + // + // Inst* simplified = op_t->t_simple; + // if (e != simplified) + // { + // y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); + // add_constraint(yices_eq(log, a), "partial interpretation of != with Ex/Cc", e); + //// cout << "Asserting " << *e << " == " << *simplified << endl; + // } + // } + //#endif + } else { + assert(0); + } + interpreted = true; } - Inst* address = NumInst::create(maxaddress - i, width, SORT()); - Inst* data = NumInst::create(v, size, 2, SORT()); - y2_expr_ptr a = create_y2_number(NumInst::as(address)); - y2_expr_ptr b = create_y2_number(NumInst::as(data)); + break; + case OpInst::ArrayConst: { + if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { + y2_type functt = create_bv_sort(make_pair(e->get_size(), e->get_sort())); + y2_expr funct = yices_new_uninterpreted_term(functt); + log = funct; + // cout << "constarray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; + + SORT* d = e->get_sort_domain(); + SORT* r = e->get_sort_range(); + assert(d->type == bvtype); + assert(r->type == bvtype); + int width = d->sz; + int size = r->sz; + + Inst* init_val = e->get_children()->back(); + assert(init_val->get_type() == Num); + string value = NumInst::as(init_val)->get_mpz()->get_str(2); + while (value.length() < e->get_size()) + value = "0" + value; + int maxaddress = pow(2, width) - 1; + for (int i = 0; i <= maxaddress; i++) { + string v; + if (value.size() <= size) { + v = value; + } else if (value.size() > (i*size)) { + v = value.substr(i*size, size); + } else { + v = "0"; + } + Inst* address = NumInst::create(maxaddress - i, width, SORT()); + Inst* data = NumInst::create(v, size, 2, SORT()); + y2_expr_ptr a = create_y2_number(NumInst::as(address)); + y2_expr_ptr b = create_y2_number(NumInst::as(data)); #ifndef Y2_ARRAY_ALLOW_BOOL if (yices_term_is_bool(a)) a = yices_ite(a, m_v1, m_v0); if (yices_term_is_bool(b)) b = yices_ite(b, m_v1, m_v0); #endif - log = yices_update1(log, a, b); - } -// cout << "updatearray: " << print_term(log) << endl; - } else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { - SORT* d = e->get_sort_domain(); - SORT* r = e->get_sort_range(); - assert(d->type == bvtype); - assert(r->type == bvtype); - int width = d->sz; - int size = r->sz; - - y2_type functt; - if (m_mapper->fetch_logic() == TheoryMapper::QF_UFBV && m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - // operation is EUF but output is BV, i.e. input is EUF type, output is BV type - functt = create_int_sort(make_pair(e->get_size(), e->get_sort()), false, true); - } - else if (m_mapper->fetch_logic() == TheoryMapper::QF_UFBV && e->ab_interpret.input_concrete()) { - functt = create_int_sort(make_pair(e->get_size(), e->get_sort()), true, false); - } - else { - functt = create_int_sort(make_pair(e->get_size(), e->get_sort())); - } + log = yices_update1(log, a, b); + } + // cout << "updatearray: " << print_term(log) << endl; + } else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { + SORT* d = e->get_sort_domain(); + SORT* r = e->get_sort_range(); + assert(d->type == bvtype); + assert(r->type == bvtype); + int width = d->sz; + int size = r->sz; + + y2_type functt; + if (m_mapper->fetch_logic() == TheoryMapper::QF_UFBV && m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + // operation is EUF but output is BV, i.e. input is EUF type, output is BV type + functt = create_int_sort(make_pair(e->get_size(), e->get_sort()), false, true); + } + else if (m_mapper->fetch_logic() == TheoryMapper::QF_UFBV && e->ab_interpret.input_concrete()) { + functt = create_int_sort(make_pair(e->get_size(), e->get_sort()), true, false); + } + else { + functt = create_int_sort(make_pair(e->get_size(), e->get_sort())); + } - y2_expr funct = yices_new_uninterpreted_term(functt); - log = funct; -// cout << "constarray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; - -// int width = e->get_sort_width(); -// Inst* init_val = e->get_children()->back(); -// assert(init_val->get_type() == Num); -// string value = NumInst::as(init_val)->get_mpz()->get_str(2); -// while (value.length() < e->get_size()) -// value = "0" + value; -// int size = e->get_sort_size(); -// int maxaddress = pow(2, width) - 1; -// for (int i = 0; i <= maxaddress; i++) { -// string v = value.substr(i*size, size); -// Inst* address = NumInst::create(maxaddress - i, width); -// Inst* data = NumInst::create(v, size, 2); -// inst2yices(address); -// inst2yices(data); -// y2_expr_ptr a = address->y2_node.solv_var(yIdx); -// y2_expr_ptr b = data->y2_node.solv_var(yIdx); -// log = yices_update1(log, a, b); -// } - } else { - assert(0); - } - assert(log); - interpreted = true; - } - break; - case OpInst::ArraySelect: { - y2_expr a = *it; - y2_expr b = *it2; + y2_expr funct = yices_new_uninterpreted_term(functt); + log = funct; + // cout << "constarray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; + + // int width = e->get_sort_width(); + // Inst* init_val = e->get_children()->back(); + // assert(init_val->get_type() == Num); + // string value = NumInst::as(init_val)->get_mpz()->get_str(2); + // while (value.length() < e->get_size()) + // value = "0" + value; + // int size = e->get_sort_size(); + // int maxaddress = pow(2, width) - 1; + // for (int i = 0; i <= maxaddress; i++) { + // string v = value.substr(i*size, size); + // Inst* address = NumInst::create(maxaddress - i, width); + // Inst* data = NumInst::create(v, size, 2); + // inst2yices(address); + // inst2yices(data); + // y2_expr_ptr a = address->y2_node.solv_var(yIdx); + // y2_expr_ptr b = data->y2_node.solv_var(yIdx); + // log = yices_update1(log, a, b); + // } + } else { + assert(0); + } + assert(log); + interpreted = true; + } + break; + case OpInst::ArraySelect: { + y2_expr a = *it; + y2_expr b = *it2; #ifndef Y2_ARRAY_ALLOW_BOOL if (yices_term_is_bool(b)) b = yices_ite(b, m_v1, m_v0); #endif - log = yices_application1(a, b); - if (log == Y2_INVALID_EXPR) { - cout << "e: " << *e << endl; - cout << "a: " << print_term(a) << " of type " << print_type(yices_type_of_term(a)) << endl; - cout << "b: " << print_term(b) << " of type " << print_type(yices_type_of_term(b)) << endl; - - yices_print_error(stdout); - assert(0); - } -// cout << "selectarray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; - assert(log); - assert(log != Y2_INVALID_EXPR); - interpreted = true; - } - break; - case OpInst::ArrayStore: { - y2_expr a = *it; - y2_expr b = *it2; - it2++; - y2_expr c = *it2; + log = yices_application1(a, b); + if (log == Y2_INVALID_EXPR) { + cout << "e: " << *e << endl; + cout << "a: " << print_term(a) << " of type " << print_type(yices_type_of_term(a)) << endl; + cout << "b: " << print_term(b) << " of type " << print_type(yices_type_of_term(b)) << endl; + + yices_print_error(stdout); + assert(0); + } + // cout << "selectarray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; + assert(log); + assert(log != Y2_INVALID_EXPR); + interpreted = true; + } + break; + case OpInst::ArrayStore: { + y2_expr a = *it; + y2_expr b = *it2; + it2++; + y2_expr c = *it2; #ifndef Y2_ARRAY_ALLOW_BOOL if (yices_term_is_bool(b)) b = yices_ite(b, m_v1, m_v0); if (yices_term_is_bool(c)) c = yices_ite(c, m_v1, m_v0); #endif - log = yices_update1(a, b, c); -// cout << "storearray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; - assert(log); - interpreted = true; - } - break; - case OpInst::Gr: - case OpInst::SGr: - case OpInst::Le: - case OpInst::SLe: - case OpInst::GrEq: - case OpInst::SGrEq: - case OpInst::LeEq: - case OpInst::SLeEq: - case OpInst::IntLe: - case OpInst::IntLeEq: - case OpInst::IntGr: - case OpInst::IntGrEq: - { - if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { - switch (o) { - case OpInst::Gr: - opstr = "Gr"; - break; - case OpInst::SGr: - opstr = "SGr"; - break; - case OpInst::Le: - opstr = "Le"; - break; - case OpInst::SLe: - opstr = "SLe"; - break; - case OpInst::GrEq: - opstr = "GrEq"; - break; - case OpInst::SGrEq: - opstr = "SGrEq"; - break; - case OpInst::LeEq: - opstr = "LeEq"; - break; - case OpInst::SLeEq: - opstr = "SLeEq"; - break; - case OpInst::IntLe: - opstr = "IntLe"; - break; - case OpInst::IntLeEq: - opstr = "IntLeEq"; - break; - case OpInst::IntGr: - opstr = "IntGr"; + log = yices_update1(a, b, c); + // cout << "storearray: " << print_term(log) << " of type " << print_type(yices_type_of_term(log)) << endl; + assert(log); + interpreted = true; + } break; - case OpInst::IntGrEq: - opstr = "IntGrEq"; + case OpInst::Gr: + case OpInst::SGr: + case OpInst::Le: + case OpInst::SLe: + case OpInst::GrEq: + case OpInst::SGrEq: + case OpInst::LeEq: + case OpInst::SLeEq: + case OpInst::IntLe: + case OpInst::IntLeEq: + case OpInst::IntGr: + case OpInst::IntGrEq: + { + if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { + switch (o) { + case OpInst::Gr: + opstr = "Gr"; + break; + case OpInst::SGr: + opstr = "SGr"; + break; + case OpInst::Le: + opstr = "Le"; + break; + case OpInst::SLe: + opstr = "SLe"; + break; + case OpInst::GrEq: + opstr = "GrEq"; + break; + case OpInst::SGrEq: + opstr = "SGrEq"; + break; + case OpInst::LeEq: + opstr = "LeEq"; + break; + case OpInst::SLeEq: + opstr = "SLeEq"; + break; + case OpInst::IntLe: + opstr = "IntLe"; + break; + case OpInst::IntLeEq: + opstr = "IntLeEq"; + break; + case OpInst::IntGr: + opstr = "IntGr"; + break; + case OpInst::IntGrEq: + opstr = "IntGrEq"; + break; + default: + assert(0); + } + } else if (m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { + assert(0); + } else if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { + + y2_expr_ptr y1 = *it; + y2_expr_ptr y2 = *it2; + Inst* c1 = e->get_children()->front(); + Inst* c2 = e->get_children()->back(); + int c1Sz = c1->get_size(); + int c2Sz = c2->get_size(); + + if (yices_term_is_bool(y1)) + y1 = yices_ite(y1, m_v1, m_v0); + if (yices_term_is_bool(y2)) + y2 = yices_ite(y2, m_v1, m_v0); + + if (c1Sz < c2Sz) + y1 = yices_zero_extend(y1, (c2Sz - c1Sz)); + if (c2Sz < c1Sz) + y2 = yices_zero_extend(y2, (c1Sz - c2Sz)); + + switch (o) { + case OpInst::Gr: + log = yices_bvgt_atom(y1, y2); + break; + case OpInst::SGr: + log = yices_bvsgt_atom(y1, y2); + break; + case OpInst::Le: + log = yices_bvlt_atom(y1, y2); + break; + case OpInst::SLe: + log = yices_bvslt_atom(y1, y2); + break; + case OpInst::GrEq: + log = yices_bvge_atom(y1, y2); + break; + case OpInst::SGrEq: + log = yices_bvsge_atom(y1, y2); + break; + case OpInst::LeEq: + log = yices_bvle_atom(y1, y2); + break; + case OpInst::SLeEq: + log = yices_bvsle_atom(y1, y2); + break; + case OpInst::IntLe: + log = yices_arith_lt_atom(y1, y2); + break; + case OpInst::IntLeEq: + log = yices_arith_leq_atom(y1, y2); + break; + case OpInst::IntGr: + log = yices_arith_gt_atom(y1, y2); + break; + case OpInst::IntGrEq: + log = yices_arith_geq_atom(y1, y2); + break; + default: + assert(0); + } + interpreted = true; + } + } break; - default: - assert(0); + default: + assert(0); } - } else if (m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { - assert(0); - } else if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { - - y2_expr_ptr y1 = *it; - y2_expr_ptr y2 = *it2; - Inst* c1 = e->get_children()->front(); - Inst* c2 = e->get_children()->back(); - int c1Sz = c1->get_size(); - int c2Sz = c2->get_size(); - - if (yices_term_is_bool(y1)) - y1 = yices_ite(y1, m_v1, m_v0); - if (yices_term_is_bool(y2)) - y2 = yices_ite(y2, m_v1, m_v0); - - if (c1Sz < c2Sz) - y1 = yices_zero_extend(y1, (c2Sz - c1Sz)); - if (c2Sz < c1Sz) - y2 = yices_zero_extend(y2, (c1Sz - c2Sz)); - - switch (o) { - case OpInst::Gr: - log = yices_bvgt_atom(y1, y2); - break; - case OpInst::SGr: - log = yices_bvsgt_atom(y1, y2); - break; - case OpInst::Le: - log = yices_bvlt_atom(y1, y2); - break; - case OpInst::SLe: - log = yices_bvslt_atom(y1, y2); - break; - case OpInst::GrEq: - log = yices_bvge_atom(y1, y2); - break; - case OpInst::SGrEq: - log = yices_bvsge_atom(y1, y2); - break; - case OpInst::LeEq: - log = yices_bvle_atom(y1, y2); - break; - case OpInst::SLeEq: - log = yices_bvsle_atom(y1, y2); - break; - case OpInst::IntLe: - log = yices_arith_lt_atom(y1, y2); - break; - case OpInst::IntLeEq: - log = yices_arith_leq_atom(y1, y2); - break; - case OpInst::IntGr: - log = yices_arith_gt_atom(y1, y2); - break; - case OpInst::IntGrEq: - log = yices_arith_geq_atom(y1, y2); - break; - default: + if (opstr != "") { + // add_yices_func(yvar, opstr, e->get_size() == 1, y_ch, s_sz, e, (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) ? e->get_size() : 0); + } else if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { + res = log; + } else if (interpreted) { + res = log; + } else assert(0); - } - interpreted = true; } - } break; - default: - assert(0); - } - if (opstr != "") { -// add_yices_func(yvar, opstr, e->get_size() == 1, y_ch, s_sz, e, (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) ? e->get_size() : 0); - } else if (m_mapper->fetch_var(e) == TheoryMapper::BV_VAR) { - res = log; - } else if (interpreted) { - res = log; - } else - assert(0); - } - break; - case OpInst::Concat: { - if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { -// assert(m_mapper->fetch_var(e) == TheoryMapper::BV_VAR); - if (y_ch.size() == 1) { - res = *it; - } else { - y2_expr arguments[y_ch.size()]; - for (int j = (y_ch.size() - 1); j >= 0; j--, ++it) { - if (yices_term_is_bitvector(*it)) - arguments[j] = *it; - else - { - assert (yices_term_is_bool(*it)); - arguments[j] = yices_ite(*it, m_v1, m_v0); + case OpInst::Concat: { + if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { + // assert(m_mapper->fetch_var(e) == TheoryMapper::BV_VAR); + if (y_ch.size() == 1) { + res = *it; + } else { + y2_expr arguments[y_ch.size()]; + for (int j = (y_ch.size() - 1); j >= 0; j--, ++it) { + if (yices_term_is_bitvector(*it)) + arguments[j] = *it; + else + { + assert (yices_term_is_bool(*it)); + arguments[j] = yices_ite(*it, m_v1, m_v0); + } + } + res = yices_bvconcat(y_ch.size(), arguments); } } - res = yices_bvconcat(y_ch.size(), arguments); + else + { + opstr = "Concat"; + } } - } - else - { - opstr = "Concat"; - } - } - break; - - // "datapath" operators - case OpInst::Minus: - case OpInst::Add: - case OpInst::AddC: - case OpInst::Sub: - case OpInst::Mult: - case OpInst::Div: - case OpInst::SDiv: - case OpInst::Rem: - case OpInst::SRem: - case OpInst::SMod: - case OpInst::BitWiseNot: - case OpInst::BitWiseAnd: - case OpInst::BitWiseNand: - case OpInst::BitWiseOr: - case OpInst::BitWiseNor: - case OpInst::BitWiseXor: - case OpInst::BitWiseXNor: - case OpInst::ReductionAnd: - case OpInst::ReductionOr: - case OpInst::ReductionXor: - case OpInst::ReductionXNor: - case OpInst::ReductionNand: - case OpInst::ReductionNor: - case OpInst::RotateL: - case OpInst::RotateR: - case OpInst::ShiftL: - case OpInst::ShiftR: - case OpInst::AShiftR: - case OpInst::AShiftL: - case OpInst::Sext: - case OpInst::Zext: - case OpInst::VShiftL: - case OpInst::VShiftR: - case OpInst::VAShiftL: - case OpInst::VAShiftR: - case OpInst::VRotateL: - case OpInst::VRotateR: - case OpInst::VEx: - case OpInst::IntAdd: - case OpInst::IntSub: - case OpInst::IntMult: - case OpInst::IntDiv: - case OpInst::IntMod: - case OpInst::IntFloor: - case OpInst::IntMinus: - { - if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { - assert(m_mapper->fetch_var(e) == TheoryMapper::BV_VAR); - - y2_expr_ptr a = (*it); - if (yices_term_is_bool(a)) - a = yices_ite(a, m_v1, m_v0); - Inst* c1 = e->get_children()->front(); - int outSz = e->get_size(); - int c1Sz = c1->get_size(); - if (c1Sz < outSz) - a = yices_zero_extend(a, (outSz - c1Sz)); - - switch (o) { - case OpInst::Minus: { - assert(y_ch.size() == 1); - res = yices_bvneg(a); - } - break; - case OpInst::BitWiseNot: { - assert(y_ch.size() == 1); - res = yices_bvnot(a); - } - break; - case OpInst::IntFloor: { - assert(y_ch.size() == 1); - res = yices_floor(a); - } - break; - case OpInst::IntMinus: { - assert(y_ch.size() == 1); - res = yices_neg(a); - } - break; + break; + // "datapath" operators + case OpInst::Minus: case OpInst::Add: + case OpInst::AddC: case OpInst::Sub: case OpInst::Mult: case OpInst::Div: @@ -6979,451 +6913,529 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) case OpInst::Rem: case OpInst::SRem: case OpInst::SMod: + case OpInst::BitWiseNot: case OpInst::BitWiseAnd: case OpInst::BitWiseNand: case OpInst::BitWiseOr: case OpInst::BitWiseNor: case OpInst::BitWiseXor: case OpInst::BitWiseXNor: + case OpInst::ReductionAnd: + case OpInst::ReductionOr: + case OpInst::ReductionXor: + case OpInst::ReductionXNor: + case OpInst::ReductionNand: + case OpInst::ReductionNor: + case OpInst::RotateL: + case OpInst::RotateR: case OpInst::ShiftL: case OpInst::ShiftR: case OpInst::AShiftR: + case OpInst::AShiftL: case OpInst::Sext: case OpInst::Zext: + case OpInst::VShiftL: + case OpInst::VShiftR: + case OpInst::VAShiftL: + case OpInst::VAShiftR: + case OpInst::VRotateL: + case OpInst::VRotateR: + case OpInst::VEx: case OpInst::IntAdd: case OpInst::IntSub: case OpInst::IntMult: case OpInst::IntDiv: case OpInst::IntMod: + case OpInst::IntFloor: + case OpInst::IntMinus: { - y2_expr_ptr b = (*it2); - if (yices_term_is_bool(b)) - b = yices_ite(b, m_v1, m_v0); - - int outSz = e->get_size(); - int maxSz = outSz; - if (e->get_sort_type() == bvtype) { - Inst* c2 = e->get_children()->back(); - int c2Sz = c2->get_size(); - if (maxSz < c1Sz) - maxSz = c1Sz; - if (maxSz < c2Sz) - maxSz = c2Sz; - - if (outSz < maxSz) - { - a = yices_zero_extend(a, (maxSz - outSz)); - } - if (c2Sz < maxSz) - { - b = yices_zero_extend(b, (maxSz - c2Sz)); - } - } + if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { + assert(m_mapper->fetch_var(e) == TheoryMapper::BV_VAR); - switch (o) { - case OpInst::Add:{ - assert(y_ch.size() == 2); - res = yices_bvadd(a, b); - }break; - case OpInst::Sub: { - assert(y_ch.size() == 2); - res = yices_bvsub(a, b); - } - break; - case OpInst::Mult:{ - assert(y_ch.size() == 2); - res = yices_bvmul(a, b); - } - break; - case OpInst::Div:{ - assert(y_ch.size() == 2); - res = yices_bvdiv(a, b); - } - break; - case OpInst::SDiv:{ - assert(y_ch.size() == 2); - res = yices_bvsdiv(a, b); - } - break; - case OpInst::Rem:{ - assert(y_ch.size() == 2); - res = yices_bvrem(a, b); - } - break; - case OpInst::SRem:{ - assert(y_ch.size() == 2); - res = yices_bvsrem(a, b); - } - break; - case OpInst::SMod:{ - assert(y_ch.size() == 2); - res = yices_bvsmod(a, b); - } - break; - case OpInst::BitWiseAnd: { - assert(y_ch.size() == 2); - res = yices_bvand2(a, b); - } - break; - case OpInst::BitWiseNand: { - assert(y_ch.size() == 2); - res = yices_bvnand(a, b); - } - break; - case OpInst::BitWiseOr: { - assert(y_ch.size() == 2); - res = yices_bvor2(a, b); - } - break; - case OpInst::BitWiseNor: { - assert(y_ch.size() == 2); - res = yices_bvnor(a, b); - } - break; - case OpInst::BitWiseXor: { - assert(y_ch.size() == 2); - res = yices_bvxor2(a, b); - } - break; - case OpInst::BitWiseXNor: { - assert(y_ch.size() == 2); - res = yices_bvxnor(a, b); - } - break; - case OpInst::ShiftL: - case OpInst::ShiftR: { - assert(y_ch.size() == 2); - InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); - ve_it2++; - if (o == OpInst::ShiftR) - res = yices_bvlshr(a, b); - else if (o == OpInst::ShiftL) - res = yices_bvshl(a, b); - else - assert(0); - assert(res != -1); - } - break; - case OpInst::AShiftR: { - assert(y_ch.size() == 2); - InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); - ve_it2++; - res = yices_bvashr(a, b); - assert(res != -1); - } - break; - case OpInst::Sext: - case OpInst::Zext: { - y2_expr_ptr a2 = (*it); - if (yices_term_is_bool(a2)) - a2 = yices_ite(a2, m_v1, m_v0); - assert(y_ch.size() == 2); - InstL::const_iterator ve_it = ch->begin(); - int amount = e->get_size() - (*ve_it)->get_size(); - assert(amount >= 0); - { - if (o == OpInst::Sext) - { - res = yices_sign_extend(a2, amount); - } else { - res = yices_zero_extend(a2, amount); + y2_expr_ptr a = (*it); + if (yices_term_is_bool(a)) + a = yices_ite(a, m_v1, m_v0); + Inst* c1 = e->get_children()->front(); + int outSz = e->get_size(); + int c1Sz = c1->get_size(); + if (c1Sz < outSz) + a = yices_zero_extend(a, (outSz - c1Sz)); + + switch (o) { + case OpInst::Minus: { + assert(y_ch.size() == 1); + res = yices_bvneg(a); } - } - assert(res != -1); - } - break; - case OpInst::IntAdd: { - assert(y_ch.size() == 2); - res = yices_add(a, b); - } - break; - case OpInst::IntSub: { - assert(y_ch.size() == 2); - res = yices_sub(a, b); - } - break; - case OpInst::IntMult: { - assert(y_ch.size() == 2); - res = yices_mul(a, b); - } - break; - case OpInst::IntDiv: { - assert(y_ch.size() == 2); - res = yices_idiv(a, b); - } - break; - case OpInst::IntMod: { - assert(y_ch.size() == 2); - res = yices_imod(a, b); - } - break; - default: - assert(0); - } - if (e->get_sort_type() == bvtype) { - if (outSz < maxSz) - res = yices_bvextract(res, 0, (outSz - 1)); - } - } - break; - - case OpInst::AddC: - case OpInst::AShiftL: - assert(0); // for now. + break; + case OpInst::BitWiseNot: { + assert(y_ch.size() == 1); + res = yices_bvnot(a); + } + break; + case OpInst::IntFloor: { + assert(y_ch.size() == 1); + res = yices_floor(a); + } + break; + case OpInst::IntMinus: { + assert(y_ch.size() == 1); + res = yices_neg(a); + } + break; + + case OpInst::Add: + case OpInst::Sub: + case OpInst::Mult: + case OpInst::Div: + case OpInst::SDiv: + case OpInst::Rem: + case OpInst::SRem: + case OpInst::SMod: + case OpInst::BitWiseAnd: + case OpInst::BitWiseNand: + case OpInst::BitWiseOr: + case OpInst::BitWiseNor: + case OpInst::BitWiseXor: + case OpInst::BitWiseXNor: + case OpInst::ShiftL: + case OpInst::ShiftR: + case OpInst::AShiftR: + case OpInst::Sext: + case OpInst::Zext: + case OpInst::IntAdd: + case OpInst::IntSub: + case OpInst::IntMult: + case OpInst::IntDiv: + case OpInst::IntMod: + { + y2_expr_ptr b = (*it2); + if (yices_term_is_bool(b)) + b = yices_ite(b, m_v1, m_v0); + + int outSz = e->get_size(); + int maxSz = outSz; + if (e->get_sort_type() == bvtype) { + Inst* c2 = e->get_children()->back(); + int c2Sz = c2->get_size(); + if (maxSz < c1Sz) + maxSz = c1Sz; + if (maxSz < c2Sz) + maxSz = c2Sz; + + if (outSz < maxSz) + { + a = yices_zero_extend(a, (maxSz - outSz)); + } + if (c2Sz < maxSz) + { + b = yices_zero_extend(b, (maxSz - c2Sz)); + } + } - case OpInst::ReductionAnd: - case OpInst::ReductionNand: { - assert(y_ch.size() == 1); - res = yices_redand(a); - if (o == OpInst::ReductionNand) res = yices_bvnot(res); - } - break; - case OpInst::ReductionOr: - case OpInst::ReductionNor: { - assert(y_ch.size() == 1); - res = yices_redor(a); - if (o == OpInst::ReductionNor) res = yices_bvnot(res); - } - break; - case OpInst::ReductionXor: - case OpInst::ReductionXNor: { - assert(y_ch.size() == 1); - unsigned sz = (*(ch->begin()))->get_size(); - assert(sz > 1); + switch (o) { + case OpInst::Add:{ + assert(y_ch.size() == 2); + res = yices_bvadd(a, b); + }break; + case OpInst::Sub: { + assert(y_ch.size() == 2); + res = yices_bvsub(a, b); + } + break; + case OpInst::Mult:{ + assert(y_ch.size() == 2); + res = yices_bvmul(a, b); + } + break; + case OpInst::Div:{ + assert(y_ch.size() == 2); + res = yices_bvdiv(a, b); + } + break; + case OpInst::SDiv:{ + assert(y_ch.size() == 2); + res = yices_bvsdiv(a, b); + } + break; + case OpInst::Rem:{ + assert(y_ch.size() == 2); + res = yices_bvrem(a, b); + } + break; + case OpInst::SRem:{ + assert(y_ch.size() == 2); + res = yices_bvsrem(a, b); + } + break; + case OpInst::SMod:{ + assert(y_ch.size() == 2); + res = yices_bvsmod(a, b); + } + break; + case OpInst::BitWiseAnd: { + assert(y_ch.size() == 2); + res = yices_bvand2(a, b); + } + break; + case OpInst::BitWiseNand: { + assert(y_ch.size() == 2); + res = yices_bvnand(a, b); + } + break; + case OpInst::BitWiseOr: { + assert(y_ch.size() == 2); + res = yices_bvor2(a, b); + } + break; + case OpInst::BitWiseNor: { + assert(y_ch.size() == 2); + res = yices_bvnor(a, b); + } + break; + case OpInst::BitWiseXor: { + assert(y_ch.size() == 2); + res = yices_bvxor2(a, b); + } + break; + case OpInst::BitWiseXNor: { + assert(y_ch.size() == 2); + res = yices_bvxnor(a, b); + } + break; + case OpInst::ShiftL: + case OpInst::ShiftR: { + assert(y_ch.size() == 2); + InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); + ve_it2++; + if (o == OpInst::ShiftR) + res = yices_bvlshr(a, b); + else if (o == OpInst::ShiftL) + res = yices_bvshl(a, b); + else + assert(0); + assert(res != -1); + } + break; + case OpInst::AShiftR: { + assert(y_ch.size() == 2); + InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); + ve_it2++; + res = yices_bvashr(a, b); + assert(res != -1); + } + break; + case OpInst::Sext: + case OpInst::Zext: { + y2_expr_ptr a2 = (*it); + if (yices_term_is_bool(a2)) + a2 = yices_ite(a2, m_v1, m_v0); + assert(y_ch.size() == 2); + InstL::const_iterator ve_it = ch->begin(); + int amount = e->get_size() - (*ve_it)->get_size(); + assert(amount >= 0); + { + if (o == OpInst::Sext) + { + res = yices_sign_extend(a2, amount); + } else { + res = yices_zero_extend(a2, amount); + } + } + assert(res != -1); + } + break; + case OpInst::IntAdd: { + assert(y_ch.size() == 2); + res = yices_add(a, b); + } + break; + case OpInst::IntSub: { + assert(y_ch.size() == 2); + res = yices_sub(a, b); + } + break; + case OpInst::IntMult: { + assert(y_ch.size() == 2); + res = yices_mul(a, b); + } + break; + case OpInst::IntDiv: { + assert(y_ch.size() == 2); + res = yices_idiv(a, b); + } + break; + case OpInst::IntMod: { + assert(y_ch.size() == 2); + res = yices_imod(a, b); + } + break; + default: + assert(0); + } + if (e->get_sort_type() == bvtype) { + if (outSz < maxSz) + res = yices_bvextract(res, 0, (outSz - 1)); + } + } + break; - y2_expr bit = yices_bvextract(a, 0, 0); - y2_expr bit2 = yices_bvextract(a, 1, 1); - bit = yices_bvxor2(bit, bit2); - for (unsigned i = 2; i < sz; i++) - { - bit = yices_bvxor2(bit, yices_bvextract(a, i, i)); - } - if (o == OpInst::ReductionXNor) bit = yices_bvnot(bit); - res = bit; - } - break; + case OpInst::AddC: + case OpInst::AShiftL: + assert(0); // for now. - case OpInst::RotateL: - case OpInst::RotateR: { - assert(y_ch.size() == 2); - InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); - ve_it2++; - NumInst* num = NumInst::as(*ve_it2); - // cout << "Rotate: " << *e << endl; - if (num != 0) - { - int rotate_amount = num->get_mpz()->get_si() % e->get_size(); - // cout << "rotate_amount: " << rotate_amount << endl; - if (rotate_amount != 0) { - if (o == OpInst::RotateL) - { - res = yices_rotate_left(a, rotate_amount); - } else { - res = yices_rotate_right(a, rotate_amount); + case OpInst::ReductionAnd: + case OpInst::ReductionNand: { + assert(y_ch.size() == 1); + res = yices_redand(a); + if (o == OpInst::ReductionNand) res = yices_bvnot(res); } - } else { - res = a; - } - } else { - cout << "Expected second operand as number in " << *e << endl; - assert(0); - } - if (res == -1) { - cout << "e: " << *e << endl; - cout << yices_error_string() << endl; - } - assert(res != -1); - } - break; - case OpInst::VRotateR:{ - const InstL* ch = e->get_children(); - InstL::const_iterator ve_it = ch->begin(); - Inst *ve_val = *ve_it; - ++ve_it; - int amt_size = (*ve_it)->get_size(); - int rotate_amount = (1 << amt_size) - 1; - int out_size = e->get_size(); - - bool simp_to_zero = false; - if(ve_val == NumInst::create(0, ve_val->get_size(), SORT())){ - simp_to_zero = true; - }else if((ve_val->get_type() == Op) && (OpInst::as(ve_val)->get_op() == OpInst::Concat)){ - const InstL* chs = ve_val->get_children(); - - if(chs && !chs->empty()){ - for(InstL::const_iterator cit = chs->begin(); cit != chs->end(); ++cit){ - Inst *tve = *cit; - if(tve != NumInst::create(0, tve->get_size(), SORT())){ // TODO check type and value - simp_to_zero = false; - break; + break; + case OpInst::ReductionOr: + case OpInst::ReductionNor: { + assert(y_ch.size() == 1); + res = yices_redor(a); + if (o == OpInst::ReductionNor) res = yices_bvnot(res); + } + break; + case OpInst::ReductionXor: + case OpInst::ReductionXNor: { + assert(y_ch.size() == 1); + unsigned sz = (*(ch->begin()))->get_size(); + assert(sz > 1); + + y2_expr bit = yices_bvextract(a, 0, 0); + y2_expr bit2 = yices_bvextract(a, 1, 1); + bit = yices_bvxor2(bit, bit2); + for (unsigned i = 2; i < sz; i++) + { + bit = yices_bvxor2(bit, yices_bvextract(a, i, i)); } - simp_to_zero = true; + if (o == OpInst::ReductionXNor) bit = yices_bvnot(bit); + res = bit; } - } - } - if(simp_to_zero == true){ - //cout << "(simp_to_zero == true): e: " << *e << endl; - res = yices_bvconst_uint32(out_size, 0); - }else{ - //cout << "(simp_to_zero == false): e: " << *e << endl; - // int rotate_amount = 31; - y2_expr els = yices_bvconcat2(yices_bvextract(*it, 0, rotate_amount-1), yices_bvextract(*it, rotate_amount, out_size-1)); //right 31 - rotate_amount--; - y2_expr thn = yices_bvconcat2(yices_bvextract(*it, 0, rotate_amount-1), yices_bvextract(*it, rotate_amount, out_size-1)); //right 30 - - y2_expr num = yices_bvconst_uint32(amt_size, rotate_amount); - y2_expr cond = yices_eq(*it2, num); - res = yices_ite(cond, thn, els); // (sel == 30) ? rotate_30 : rotate_31 - - for(; rotate_amount > 0; --rotate_amount){ - thn = yices_bvconcat2(yices_bvextract(*it, 0, rotate_amount-1), yices_bvextract(*it, rotate_amount, out_size-1)); - num = yices_bvconst_uint32(amt_size, rotate_amount); - cond = yices_eq(*it2, num); - res = yices_ite(cond, thn, res); - } - num = yices_bvconst_uint32(amt_size, 0); - cond = yices_eq(*it2, num); - res = yices_ite(cond, *it, res); - #ifdef YICES_BV_INPUT_DUMP_DERIVED + break; + + case OpInst::RotateL: + case OpInst::RotateR: { + assert(y_ch.size() == 2); + InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin(); + ve_it2++; + NumInst* num = NumInst::as(*ve_it2); + // cout << "Rotate: " << *e << endl; + if (num != 0) + { + int rotate_amount = num->get_mpz()->get_si() % e->get_size(); + // cout << "rotate_amount: " << rotate_amount << endl; + if (rotate_amount != 0) { + if (o == OpInst::RotateL) + { + res = yices_rotate_left(a, rotate_amount); + } else { + res = yices_rotate_right(a, rotate_amount); + } + } else { + res = a; + } + } else { + cout << "Expected second operand as number in " << *e << endl; + assert(0); + } + if (res == -1) { + cout << "e: " << *e << endl; + cout << yices_error_string() << endl; + } + assert(res != -1); + } + break; + case OpInst::VRotateR:{ + const InstL* ch = e->get_children(); + InstL::const_iterator ve_it = ch->begin(); + Inst *ve_val = *ve_it; + ++ve_it; + int amt_size = (*ve_it)->get_size(); + int rotate_amount = (1 << amt_size) - 1; + int out_size = e->get_size(); + + bool simp_to_zero = false; + if(ve_val == NumInst::create(0, ve_val->get_size(), SORT())){ + simp_to_zero = true; + }else if((ve_val->get_type() == Op) && (OpInst::as(ve_val)->get_op() == OpInst::Concat)){ + const InstL* chs = ve_val->get_children(); + + if(chs && !chs->empty()){ + for(InstL::const_iterator cit = chs->begin(); cit != chs->end(); ++cit){ + Inst *tve = *cit; + if(tve != NumInst::create(0, tve->get_size(), SORT())){ // TODO check type and value + simp_to_zero = false; + break; + } + simp_to_zero = true; + } + } + } + if(simp_to_zero == true){ + //cout << "(simp_to_zero == true): e: " << *e << endl; + res = yices_bvconst_uint32(out_size, 0); + }else{ + //cout << "(simp_to_zero == false): e: " << *e << endl; + // int rotate_amount = 31; + y2_expr els = yices_bvconcat2(yices_bvextract(*it, 0, rotate_amount-1), yices_bvextract(*it, rotate_amount, out_size-1)); //right 31 + rotate_amount--; + y2_expr thn = yices_bvconcat2(yices_bvextract(*it, 0, rotate_amount-1), yices_bvextract(*it, rotate_amount, out_size-1)); //right 30 + + y2_expr num = yices_bvconst_uint32(amt_size, rotate_amount); + y2_expr cond = yices_eq(*it2, num); + res = yices_ite(cond, thn, els); // (sel == 30) ? rotate_30 : rotate_31 + + for(; rotate_amount > 0; --rotate_amount){ + thn = yices_bvconcat2(yices_bvextract(*it, 0, rotate_amount-1), yices_bvextract(*it, rotate_amount, out_size-1)); + num = yices_bvconst_uint32(amt_size, rotate_amount); + cond = yices_eq(*it2, num); + res = yices_ite(cond, thn, res); + } + num = yices_bvconst_uint32(amt_size, 0); + cond = yices_eq(*it2, num); + res = yices_ite(cond, *it, res); +#ifdef YICES_BV_INPUT_DUMP_DERIVED cout << this <<": "; cout << "(derived "; yices_pp_expr(res); cout << endl; - #endif - } - break; - //yices_mk_bv_concat(m_ctx, yices_mk_bv_extract(m_ctx, out_size-1-rotate_amount, 0, *it), yices_mk_bv_extract(m_ctx, out_size-1, out_size-rotate_amount, *it)) //left - } - case OpInst::VRotateL:{ - const InstL* ch = e->get_children(); - InstL::const_iterator ve_it = ch->begin(); - Inst *ve_val = *ve_it; - ++ve_it; - int amt_size = (*ve_it)->get_size(); - int rotate_amount = (1 << amt_size) - 1; - int out_size = e->get_size(); - - bool simp_to_zero = false; - if(ve_val == NumInst::create(0, ve_val->get_size(), SORT())){ - simp_to_zero = true; - }else if((ve_val->get_type() == Op) && (OpInst::as(ve_val)->get_op() == OpInst::Concat)){ - const InstL* chs = ve_val->get_children(); - - if(chs && !chs->empty()){ - for(InstL::const_iterator cit = chs->begin(); cit != chs->end(); ++cit){ - Inst *tve = *cit; - if(tve != NumInst::create(0, tve->get_size(), SORT())){ // TODO check type and value - simp_to_zero = false; - break; +#endif } - simp_to_zero = true; + break; + //yices_mk_bv_concat(m_ctx, yices_mk_bv_extract(m_ctx, out_size-1-rotate_amount, 0, *it), yices_mk_bv_extract(m_ctx, out_size-1, out_size-rotate_amount, *it)) //left } - } - } - if(simp_to_zero == true){ - //cout << "(simp_to_zero == true): e: " << *e << endl; - res = yices_bvconst_uint32(out_size, 0); - }else{ - //cout << "(simp_to_zero == false): e: " << *e << endl; - //int rotate_amount = 31; - - y2_expr els = yices_bvconcat2(yices_bvextract(*it, 0, out_size-rotate_amount-1), yices_bvextract(*it, out_size-rotate_amount, out_size-1)); //right 31 - rotate_amount--; - y2_expr thn = yices_bvconcat2(yices_bvextract(*it, 0, out_size-rotate_amount-1), yices_bvextract(*it, out_size-rotate_amount, out_size-1)); //right 30 - - y2_expr num = yices_bvconst_uint32(amt_size, rotate_amount); - y2_expr cond = yices_eq(*it2, num); - res = yices_ite(cond, thn, els); // (sel == 30) ? rotate_30 : rotate_31 - - for(; rotate_amount > 0; --rotate_amount){ - thn = yices_bvconcat2(yices_bvextract(*it, 0, out_size-rotate_amount-1), yices_bvextract(*it, out_size-rotate_amount, out_size-1)); - num = yices_bvconst_uint32(amt_size, rotate_amount); - cond = yices_eq(*it2, num); - res = yices_ite(cond, thn, res); - } - num = yices_bvconst_uint32(amt_size, 0); - cond = yices_eq(*it2, num); - res = yices_ite(cond, *it, res); - #ifdef YICES_BV_INPUT_DUMP_DERIVED + case OpInst::VRotateL:{ + const InstL* ch = e->get_children(); + InstL::const_iterator ve_it = ch->begin(); + Inst *ve_val = *ve_it; + ++ve_it; + int amt_size = (*ve_it)->get_size(); + int rotate_amount = (1 << amt_size) - 1; + int out_size = e->get_size(); + + bool simp_to_zero = false; + if(ve_val == NumInst::create(0, ve_val->get_size(), SORT())){ + simp_to_zero = true; + }else if((ve_val->get_type() == Op) && (OpInst::as(ve_val)->get_op() == OpInst::Concat)){ + const InstL* chs = ve_val->get_children(); + + if(chs && !chs->empty()){ + for(InstL::const_iterator cit = chs->begin(); cit != chs->end(); ++cit){ + Inst *tve = *cit; + if(tve != NumInst::create(0, tve->get_size(), SORT())){ // TODO check type and value + simp_to_zero = false; + break; + } + simp_to_zero = true; + } + } + } + if(simp_to_zero == true){ + //cout << "(simp_to_zero == true): e: " << *e << endl; + res = yices_bvconst_uint32(out_size, 0); + }else{ + //cout << "(simp_to_zero == false): e: " << *e << endl; + //int rotate_amount = 31; + + y2_expr els = yices_bvconcat2(yices_bvextract(*it, 0, out_size-rotate_amount-1), yices_bvextract(*it, out_size-rotate_amount, out_size-1)); //right 31 + rotate_amount--; + y2_expr thn = yices_bvconcat2(yices_bvextract(*it, 0, out_size-rotate_amount-1), yices_bvextract(*it, out_size-rotate_amount, out_size-1)); //right 30 + + y2_expr num = yices_bvconst_uint32(amt_size, rotate_amount); + y2_expr cond = yices_eq(*it2, num); + res = yices_ite(cond, thn, els); // (sel == 30) ? rotate_30 : rotate_31 + + for(; rotate_amount > 0; --rotate_amount){ + thn = yices_bvconcat2(yices_bvextract(*it, 0, out_size-rotate_amount-1), yices_bvextract(*it, out_size-rotate_amount, out_size-1)); + num = yices_bvconst_uint32(amt_size, rotate_amount); + cond = yices_eq(*it2, num); + res = yices_ite(cond, thn, res); + } + num = yices_bvconst_uint32(amt_size, 0); + cond = yices_eq(*it2, num); + res = yices_ite(cond, *it, res); +#ifdef YICES_BV_INPUT_DUMP_DERIVED cout << this <<": "; cout << "(derived "; yices_pp_expr(res); cout << endl; - #endif - } - break; - } - case OpInst::VShiftL: //TODO - case OpInst::VShiftR: - case OpInst::VAShiftL: - case OpInst::VAShiftR: - case OpInst::VEx:{ - const InstL* ch = e->get_children(); - InstL::const_iterator ve_it = ch->begin(); - int ex_offset = (*ve_it)->get_size()-1; - ++ve_it; - int idx_size = (*ve_it)->get_size(); - -// cout << "ex_offset: " << ex_offset << endl; -// cout << "idx_size: " << idx_size << endl; - - y2_expr els = yices_bvextract(*it, ex_offset, ex_offset); - ex_offset--; - y2_expr thn = yices_bvextract(*it, ex_offset, ex_offset); - - y2_expr num = yices_bvconst_uint32(idx_size, ex_offset); - y2_expr cond = yices_eq(*it2, num); - res = yices_ite(cond, thn, els); // (sel == 30) ? rotate_30 : rotate_31 - - for(; ex_offset >= 0; --ex_offset){ - thn = yices_bvextract(*it, ex_offset, ex_offset); - num = yices_bvconst_uint32(idx_size, ex_offset); - cond = yices_eq(*it2, num); - res = yices_ite(cond, thn, res); - } - #ifdef YICES_BV_INPUT_DUMP_DERIVED +#endif + } + break; + } + case OpInst::VShiftL: //TODO + case OpInst::VShiftR: + case OpInst::VAShiftL: + case OpInst::VAShiftR: + case OpInst::VEx:{ + const InstL* ch = e->get_children(); + InstL::const_iterator ve_it = ch->begin(); + int ex_offset = (*ve_it)->get_size()-1; + ++ve_it; + int idx_size = (*ve_it)->get_size(); + + // cout << "ex_offset: " << ex_offset << endl; + // cout << "idx_size: " << idx_size << endl; + + y2_expr els = yices_bvextract(*it, ex_offset, ex_offset); + ex_offset--; + y2_expr thn = yices_bvextract(*it, ex_offset, ex_offset); + + y2_expr num = yices_bvconst_uint32(idx_size, ex_offset); + y2_expr cond = yices_eq(*it2, num); + res = yices_ite(cond, thn, els); // (sel == 30) ? rotate_30 : rotate_31 + + for(; ex_offset >= 0; --ex_offset){ + thn = yices_bvextract(*it, ex_offset, ex_offset); + num = yices_bvconst_uint32(idx_size, ex_offset); + cond = yices_eq(*it2, num); + res = yices_ite(cond, thn, res); + } +#ifdef YICES_BV_INPUT_DUMP_DERIVED cout << this <<": "; cout << "(derived "; yices_pp_expr(res); cout << endl; - #endif - break; - } - default: - cout << "Error converting expression to yices equivalent: " << *e << endl; - assert(0); - } - } else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { - switch (o) { - case OpInst::VShiftL: //TODO - opstr = "VShiftL"; - break; - case OpInst::VShiftR: - opstr = "VShiftR"; - break; - case OpInst::VAShiftL: - opstr = "VAShiftL"; - break; - case OpInst::VAShiftR: - opstr = "VAShiftR"; - break; - case OpInst::VRotateL: - opstr = "VRotateL"; - break; - case OpInst::VRotateR: - opstr = "VRotateR"; - break; - case OpInst::VEx: - opstr = "VEx"; - break; - case OpInst::Minus: - opstr = "Minus"; - break; - case OpInst::AddC: - opstr = "AddC"; - break; - case OpInst::Add: - if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { +#endif + break; + } + default: + cout << "Error converting expression to yices equivalent: " << *e << endl; + assert(0); + } + } else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { + switch (o) { + case OpInst::VShiftL: //TODO + opstr = "VShiftL"; + break; + case OpInst::VShiftR: + opstr = "VShiftR"; + break; + case OpInst::VAShiftL: + opstr = "VAShiftL"; + break; + case OpInst::VAShiftR: + opstr = "VAShiftR"; + break; + case OpInst::VRotateL: + opstr = "VRotateL"; + break; + case OpInst::VRotateR: + opstr = "VRotateR"; + break; + case OpInst::VEx: + opstr = "VEx"; + break; + case OpInst::Minus: + opstr = "Minus"; + break; + case OpInst::AddC: + opstr = "AddC"; + break; + case OpInst::Add: + if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { #ifdef USE_INTERPRETED_ADD_SUB yices_expr args[2]; args[0] = *it; @@ -7446,44 +7458,44 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) opstr = "Add"; } #else - opstr = "Add"; + opstr = "Add"; #endif - } else if (m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { - //TODO -// if (config->get_arg(UBADD_ARG) == "1") { -// yices_expr arguments[2]; -// arguments[0] = *it; -// arguments[1] = *it2; -// res = yices_mk_sum(m_ctx, arguments, 2); -// interpreted = true; -// } else { -// InstL::const_iterator cit = ch->begin(), cit2; -// cit2 = cit; -// cit2++; -// if ((*cit2)->get_type() == Num) { -// NumInst* num = NumInst::as(*cit2); -// assert(num != 0); -// yices_expr arguments[2]; -// arguments[0] = *it; -// arguments[1] = yices_mk_num(m_ctx, num->get_mpz()); -// res = yices_mk_sum(m_ctx, arguments, 2); -// interpreted = true; -// } else if ((*cit)->get_type() == Num) { -// NumInst* num = NumInst::as(*cit); -// assert(num != 0); -// yices_expr arguments[2]; -// arguments[1] = *it; -// arguments[0] = yices_mk_num(m_ctx, num->get_mpz()); -// res = yices_mk_sum(m_ctx, arguments, 2); -// interpreted = true; -// } else -// opstr = "Add"; -// } - } else - assert(0); - break; - case OpInst::Sub: - if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { + } else if (m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { + //TODO + // if (config->get_arg(UBADD_ARG) == "1") { + // yices_expr arguments[2]; + // arguments[0] = *it; + // arguments[1] = *it2; + // res = yices_mk_sum(m_ctx, arguments, 2); + // interpreted = true; + // } else { + // InstL::const_iterator cit = ch->begin(), cit2; + // cit2 = cit; + // cit2++; + // if ((*cit2)->get_type() == Num) { + // NumInst* num = NumInst::as(*cit2); + // assert(num != 0); + // yices_expr arguments[2]; + // arguments[0] = *it; + // arguments[1] = yices_mk_num(m_ctx, num->get_mpz()); + // res = yices_mk_sum(m_ctx, arguments, 2); + // interpreted = true; + // } else if ((*cit)->get_type() == Num) { + // NumInst* num = NumInst::as(*cit); + // assert(num != 0); + // yices_expr arguments[2]; + // arguments[1] = *it; + // arguments[0] = yices_mk_num(m_ctx, num->get_mpz()); + // res = yices_mk_sum(m_ctx, arguments, 2); + // interpreted = true; + // } else + // opstr = "Add"; + // } + } else + assert(0); + break; + case OpInst::Sub: + if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) { #ifdef USE_INTERPRETED_ADD_SUB yices_expr args[2]; args[0] = *it; @@ -7506,225 +7518,225 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) opstr = "Sub"; } #else - opstr = "Sub"; + opstr = "Sub"; #endif - } else if (m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) - { - assert(0); -// InstL::const_iterator cit2 = ch->begin(); -// cit2++; -// if ((*cit2)->get_type() == Num) { -// NumInst* num = NumInst::as(*cit2); -// assert(num != 0); -// yices_expr arguments[2]; -// arguments[0] = *it; -// arguments[1] = yices_mk_num(m_ctx, num->get_mpz()->get_si()); -// res = yices_mk_sub(m_ctx, arguments, 2); -// interpreted = true; -// } else -// opstr = "Sub"; - } else - assert(0); - break; - case OpInst::Mult: - opstr = "Mult"; - break; - case OpInst::Div: - opstr = "Div"; - break; - case OpInst::SDiv: - opstr = "SDiv"; - break; - case OpInst::Rem: - opstr = "Rem"; - break; - case OpInst::SRem: - opstr = "SRem"; - break; - case OpInst::SMod: - opstr = "SMod"; - break; - case OpInst::BitWiseAnd: - opstr = "BitWiseAnd"; - break; - case OpInst::BitWiseOr: - opstr = "BitWiseOr"; - break; - case OpInst::BitWiseNot: - opstr = "BitWiseNot"; - break; - case OpInst::BitWiseXor: - opstr = "BitWiseXor"; - break; - case OpInst::BitWiseXNor: - opstr = "BitWiseXNor"; - break; - case OpInst::BitWiseNor: - opstr = "BitWiseNor"; - break; - case OpInst::BitWiseNand: - opstr = "BitWiseNand"; - break; - case OpInst::ReductionAnd: - opstr = "ReductionAnd"; - break; - case OpInst::ReductionOr: - opstr = "ReductionOr"; - break; - case OpInst::ReductionXor: - opstr = "ReductionXor"; - break; - case OpInst::ReductionXNor: - opstr = "ReductionXNor"; - break; - case OpInst::ReductionNand: - opstr = "ReductionNand"; - break; - case OpInst::ReductionNor: - opstr = "ReductionNor"; - break; - case OpInst::RotateL: - opstr = "RotateL"; - break; - case OpInst::RotateR: - opstr = "RotateR"; - break; - case OpInst::ShiftL: - opstr = "ShiftL"; - break; - case OpInst::ShiftR: - opstr = "ShiftR"; - break; - case OpInst::AShiftR: - opstr = "AShiftR"; - break; - case OpInst::AShiftL: - opstr = "AShiftL"; - break; - case OpInst::Sext: - opstr = "Sext"; - break; - case OpInst::Zext: - opstr = "Zext"; - break; -// case OpInst::ArrayConst: -// opstr = "ArrayConst"; -// break; -// case OpInst::ArraySelect: -// opstr = "ArraySelect"; -// break; -// case OpInst::ArrayStore: -// opstr = "ArrayStore"; -// break; - case OpInst::IntAdd: - opstr = "IntAdd"; - break; - case OpInst::IntSub: - opstr = "IntSub"; - break; - case OpInst::IntMult: - opstr = "IntMult"; - break; - case OpInst::IntDiv: - opstr = "IntDiv"; - break; - case OpInst::IntMod: - opstr = "IntMod"; - break; - case OpInst::IntFloor: - opstr = "IntFloor"; - break; - case OpInst::IntMinus: - opstr = "IntMinus"; - break; - default: - assert(0); + } else if (m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) + { + assert(0); + // InstL::const_iterator cit2 = ch->begin(); + // cit2++; + // if ((*cit2)->get_type() == Num) { + // NumInst* num = NumInst::as(*cit2); + // assert(num != 0); + // yices_expr arguments[2]; + // arguments[0] = *it; + // arguments[1] = yices_mk_num(m_ctx, num->get_mpz()->get_si()); + // res = yices_mk_sub(m_ctx, arguments, 2); + // interpreted = true; + // } else + // opstr = "Sub"; + } else + assert(0); + break; + case OpInst::Mult: + opstr = "Mult"; + break; + case OpInst::Div: + opstr = "Div"; + break; + case OpInst::SDiv: + opstr = "SDiv"; + break; + case OpInst::Rem: + opstr = "Rem"; + break; + case OpInst::SRem: + opstr = "SRem"; + break; + case OpInst::SMod: + opstr = "SMod"; + break; + case OpInst::BitWiseAnd: + opstr = "BitWiseAnd"; + break; + case OpInst::BitWiseOr: + opstr = "BitWiseOr"; + break; + case OpInst::BitWiseNot: + opstr = "BitWiseNot"; + break; + case OpInst::BitWiseXor: + opstr = "BitWiseXor"; + break; + case OpInst::BitWiseXNor: + opstr = "BitWiseXNor"; + break; + case OpInst::BitWiseNor: + opstr = "BitWiseNor"; + break; + case OpInst::BitWiseNand: + opstr = "BitWiseNand"; + break; + case OpInst::ReductionAnd: + opstr = "ReductionAnd"; + break; + case OpInst::ReductionOr: + opstr = "ReductionOr"; + break; + case OpInst::ReductionXor: + opstr = "ReductionXor"; + break; + case OpInst::ReductionXNor: + opstr = "ReductionXNor"; + break; + case OpInst::ReductionNand: + opstr = "ReductionNand"; + break; + case OpInst::ReductionNor: + opstr = "ReductionNor"; + break; + case OpInst::RotateL: + opstr = "RotateL"; + break; + case OpInst::RotateR: + opstr = "RotateR"; + break; + case OpInst::ShiftL: + opstr = "ShiftL"; + break; + case OpInst::ShiftR: + opstr = "ShiftR"; + break; + case OpInst::AShiftR: + opstr = "AShiftR"; + break; + case OpInst::AShiftL: + opstr = "AShiftL"; + break; + case OpInst::Sext: + opstr = "Sext"; + break; + case OpInst::Zext: + opstr = "Zext"; + break; + // case OpInst::ArrayConst: + // opstr = "ArrayConst"; + // break; + // case OpInst::ArraySelect: + // opstr = "ArraySelect"; + // break; + // case OpInst::ArrayStore: + // opstr = "ArrayStore"; + // break; + case OpInst::IntAdd: + opstr = "IntAdd"; + break; + case OpInst::IntSub: + opstr = "IntSub"; + break; + case OpInst::IntMult: + opstr = "IntMult"; + break; + case OpInst::IntDiv: + opstr = "IntDiv"; + break; + case OpInst::IntMod: + opstr = "IntMod"; + break; + case OpInst::IntFloor: + opstr = "IntFloor"; + break; + case OpInst::IntMinus: + opstr = "IntMinus"; + break; + default: + assert(0); + } + } } - } - } - break; - case OpInst::Ternary: { -// for (auto& c: y_ch) { -// cout << print_term(c) << endl; -// } -// cout << y_ch.size() << endl; - - assert(y_ch.size() == 3); - y2_expr_list::iterator it3 = it2; - it3++; - y2_expr_ptr cond = (*it); - y2_expr_ptr y1 = (*it2); - y2_expr_ptr y2 = (*it3); - - if (yices_term_is_bitvector(cond)) - cond = yices_eq(cond, m_v1); + break; + case OpInst::Ternary: { + // for (auto& c: y_ch) { + // cout << print_term(c) << endl; + // } + // cout << y_ch.size() << endl; - res = yices_ite(cond, y1, y2); -// conds.push_back(cond); + assert(y_ch.size() == 3); + y2_expr_list::iterator it3 = it2; + it3++; + y2_expr_ptr cond = (*it); + y2_expr_ptr y1 = (*it2); + y2_expr_ptr y2 = (*it3); - interpreted = true; + if (yices_term_is_bitvector(cond)) + cond = yices_eq(cond, m_v1); -// cout << *e << " " << print_term(y1) << " of type " << print_type(yices_type_of_term(y1)) << endl; -// cout << *e << " " << print_term(y2) << " of type " << print_type(yices_type_of_term(y2)) << endl; -// cout << *e << " " << print_term(cond) << " of type " << print_type(yices_type_of_term(cond)) << endl; -// cout << *e << " " << print_term(yvar) << " of type " << print_type(yices_type_of_term(yvar)) << endl; + res = yices_ite(cond, y1, y2); + // conds.push_back(cond); - assert(res); + interpreted = true; -//#ifdef INTERPRET_EX_CC -// if (m_allow_ex_cc) -// { -// OpInst* op_t = OpInst::as(e); -// assert(op_t); -// assert(op_t->get_op() == OpInst::Ternary); -// -// Inst* simplified = op_t->t_simple; -// if (e != simplified) -// { -// y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); -// add_constraint(yices_eq(res, a), "partial interpretation of ternary with Ex/Cc", e); -//// cout << "Asserting " << *e << " == " << *simplified << endl; -// } -// } -//#endif - } - break; - default: - AVR_COUT << o << endl; - assert(0); - } - if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { - assert(res); - add_gate_constraint(yvar, res, "result of a bv op", e, false, true); - } - else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { - if (interpreted) { + // cout << *e << " " << print_term(y1) << " of type " << print_type(yices_type_of_term(y1)) << endl; + // cout << *e << " " << print_term(y2) << " of type " << print_type(yices_type_of_term(y2)) << endl; + // cout << *e << " " << print_term(cond) << " of type " << print_type(yices_type_of_term(cond)) << endl; + // cout << *e << " " << print_term(yvar) << " of type " << print_type(yices_type_of_term(yvar)) << endl; + + assert(res); + + //#ifdef INTERPRET_EX_CC + // if (m_allow_ex_cc) + // { + // OpInst* op_t = OpInst::as(e); + // assert(op_t); + // assert(op_t->get_op() == OpInst::Ternary); + // + // Inst* simplified = op_t->t_simple; + // if (e != simplified) + // { + // y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); + // add_constraint(yices_eq(res, a), "partial interpretation of ternary with Ex/Cc", e); + //// cout << "Asserting " << *e << " == " << *simplified << endl; + // } + // } + //#endif + } + break; + default: + AVR_COUT << o << endl; + assert(0); + } + if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { assert(res); - add_gate_constraint(yvar, res, "interpreted operator constraint for EUF", e, false, true); + add_gate_constraint(yvar, res, "result of a bv op", e, false, true); } - else { - if (opstr == "") { - cout << OpInst::op2str(o) << endl; - assert(0); + else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { + if (interpreted) { + assert(res); + add_gate_constraint(yvar, res, "interpreted operator constraint for EUF", e, false, true); } - add_yices_func(yvar, opstr, e->get_size() == 1, y_ch, s_sz, e); - -//#ifdef INTERPRET_EX_CC -// if (m_allow_ex_cc) -// { -// OpInst* op_cc = OpInst::as(e); -// assert(op_cc); -//// if (op_cc->get_op() == OpInst::Concat) -// { -// Inst* simplified = op_cc->t_simple; -// if (e != simplified) -// { -// add_constraint(yices_eq(yvar, simplified->y2_node.solv_var(get_vIdx())), "partial interpretation of Cc", e); -//// cout << "Asserting " << *e << " == " << *simplified << endl; -// } -// -// /// Test -//// const InstL* ch = op_cc->get_children(); + else { + if (opstr == "") { + cout << OpInst::op2str(o) << endl; + assert(0); + } + add_yices_func(yvar, opstr, e->get_size() == 1, y_ch, s_sz, e); + + //#ifdef INTERPRET_EX_CC + // if (m_allow_ex_cc) + // { + // OpInst* op_cc = OpInst::as(e); + // assert(op_cc); + //// if (op_cc->get_op() == OpInst::Concat) + // { + // Inst* simplified = op_cc->t_simple; + // if (e != simplified) + // { + // add_constraint(yices_eq(yvar, simplified->y2_node.solv_var(get_vIdx())), "partial interpretation of Cc", e); + //// cout << "Asserting " << *e << " == " << *simplified << endl; + // } + // + // /// Test + //// const InstL* ch = op_cc->get_children(); //// if (ch) //// { //// unsigned s_loc = 0, e_loc = 0; @@ -7741,62 +7753,62 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) //// add_constraint(yices_eq(tve->y_var[ABSTRACT], ex_tve->y_var[ABSTRACT]), "partial interpretation of Cc", e); //// } //// } -// } -// } -//#endif + // } + // } + //#endif + } + } else { + assert(0); } - } else { - assert(0); } - } break; - case Ex: { - ExInst* ex = ExInst::as(e); - assert(ex != 0); - if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { - - y2_expr_ptr res = yices_bvextract(y_ch.front(), ex->get_lo(), ex->get_hi()); - assert(res); - - add_gate_constraint(yvar, res, "result of a bv EX", e, false, true); - - } else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { - assert(y_ch.size() == 1); - s_sz.clear(); - s_sz.push_back(ex->get_hi()); - s_sz.push_back(ex->get_lo()); - s_sz.push_back((*(ch->begin()))->get_size()); - add_yices_func(yvar, "Extract", e->get_size() == 1, y_ch, s_sz, e); - -//#ifdef INTERPRET_EX_CC -// if (m_allow_ex_cc) -// { -// ExInst* ex = ExInst::as(e); -// Inst* simplified = ex->t_simple; -// if (e != simplified) -// { -// add_constraint(yices_eq(yvar, simplified->y2_node.solv_var(get_vIdx())), "partial interpretation of Ex", e); -// // cout << "Asserting " << *e << " == " << *simplified << endl; -// } -// } -//#endif - } else - assert(0); - } + case Ex: { + ExInst* ex = ExInst::as(e); + assert(ex != 0); + if (m_mapper->fetch_op(e) == TheoryMapper::BV_OP) { + + y2_expr_ptr res = yices_bvextract(y_ch.front(), ex->get_lo(), ex->get_hi()); + assert(res); + + add_gate_constraint(yvar, res, "result of a bv EX", e, false, true); + + } else if (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP || m_mapper->fetch_op(e) == TheoryMapper::CLU_OP) { + assert(y_ch.size() == 1); + s_sz.clear(); + s_sz.push_back(ex->get_hi()); + s_sz.push_back(ex->get_lo()); + s_sz.push_back((*(ch->begin()))->get_size()); + add_yices_func(yvar, "Extract", e->get_size() == 1, y_ch, s_sz, e); + + //#ifdef INTERPRET_EX_CC + // if (m_allow_ex_cc) + // { + // ExInst* ex = ExInst::as(e); + // Inst* simplified = ex->t_simple; + // if (e != simplified) + // { + // add_constraint(yices_eq(yvar, simplified->y2_node.solv_var(get_vIdx())), "partial interpretation of Ex", e); + // // cout << "Asserting " << *e << " == " << *simplified << endl; + // } + // } + //#endif + } else + assert(0); + } break; - case UF: { - UFInst* uf = UFInst::as(e); - assert(uf != 0); - assert(ch != 0); - assert(ch->size() > 0); - // unsigned ch_sz = (*(ch->begin()))->get_size(); + case UF: { + UFInst* uf = UFInst::as(e); + assert(uf != 0); + assert(ch != 0); + assert(ch->size() > 0); + // unsigned ch_sz = (*(ch->begin()))->get_size(); - // cout<<"uf->get_name = "<get_name()<get_name())<get_name = "<get_name()<get_name())<get_name()), e->get_size() == 1, y_ch, s_sz, e); + add_yices_func(yvar, clean_str(uf->get_name()), e->get_size() == 1, y_ch, s_sz, e); - /* if(m_mapper->fetch_op(e)==TheoryMapper::BV_OP){ + /* if(m_mapper->fetch_op(e)==TheoryMapper::BV_OP){ yices_type domains[ch->size()]; for(unsigned i = 0 ; i < ch->size(); i++) domains[i] = yices_mk_bitvector_type(m_ctx,ch_sz); @@ -7809,23 +7821,23 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) s_sz.clear(); add_yices_func(yvar,clean_str(uf->get_name()),e->get_size()==1,y_ch,s_sz,e,(m_mapper->fetch_var(e)==TheoryMapper::BV_VAR)?e->get_size():0); } else assert(0);*/ - } + } break; - case Mem: - default: - AVR_COUT << e->get_type() << endl; - assert(0); + case Mem: + default: + AVR_COUT << e->get_type() << endl; + assert(0); } #ifdef INTERPRET_EX_CC if (m_allow_ex_cc) { if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) || - (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { + (m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) { Inst* simplified = e->t_simple; if (e != simplified) { - #ifdef INTERPRET_UF_NUM +#ifdef INTERPRET_UF_NUM { NumInst* num = NumInst::as(e); if (num) { @@ -7850,9 +7862,9 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) } } } - #endif +#endif - #ifdef INTERPRET_UF_SIG +#ifdef INTERPRET_UF_SIG { SigInst* sig = SigInst::as(e); if (sig) { @@ -7877,7 +7889,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) } } } - #endif +#endif { y2_expr_ptr a = simplified->y2_node.solv_var(get_vIdx()); @@ -7893,23 +7905,8 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints) } assert(yvar != Y2_INVALID_EXPR); -// cout << "[I2Y]\t" << *e << " --> " << print_term(yvar) << endl; -} - -void y2_API::increase_cond_activity() { -// for (auto& cond: conds) { -// double act1 = -1; -// y2_get_activity(m_ctx, cond, &act1); -// y2_increase_activity(m_ctx, cond); -// double act2 = -1; -// y2_get_activity(m_ctx, cond, &act2); -//// cout << print_term(cond) << " : " << act1 << " -> " << act2 << endl; -//// assert(0); -// } + // cout << "[I2Y]\t" << *e << " --> " << print_term(yvar) << endl; } - - - }; #endif diff --git a/workers.txt b/workers.txt index 8410bcd..c17de9a 100755 --- a/workers.txt +++ b/workers.txt @@ -1,16 +1,16 @@ python3 avr.py --split -python3 avr.py +python3 avr.py --kind --abstract sa --backend bt +python3 avr.py --kind --abstract sa --split +python3 avr.py --abstract sa --backend bt python3 avr.py --abstract sa -python3 avr.py --kind --backend bt -python3 avr.py --abstract sa4 --split --interpol 1 --forward 1 -python3 avr.py --bmc --abstract sa --split --backend bt -python3 avr.py --kind --split -python3 avr.py --abstract sa8 --split --interpol 1 +python3 avr.py +python3 avr.py --bmc --abstract sa --backend bt --split +python3 avr.py --bmc --abstract sa+heavy python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1 -python3 avr.py --split --backend bt -python3 avr.py --kind --split -python3 avr.py --split --level 0 +python3 avr.py --abstract sa4 --split --forward 1 --interpol 1 +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 --split -python3 avr.py --abstract sa32 --granularity 3 --level 0 --backend bt -python3 avr.py --abstract sa16 --split --forward 1 --backend bt \ No newline at end of file +python3 avr.py --bmc --abstract sa --split From 8364cc24b681240a8917c07247227dad0bc38fec Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 26 Aug 2024 23:45:43 +0000 Subject: [PATCH 05/19] Minor correction --- src/reach/avr_word_netlist.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index cf8c60b..60077fb 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -1915,7 +1915,7 @@ void OpInst::propagate_uf() { 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(lhs)->get_num() == 1) { + } else if (NumInst::as(rhs) && NumInst::as(rhs)->get_num() == 1) { // lhs % 1 = 0 t_simple = NumInst::create(0, get_size(), get_sort()); } else if (lhs == rhs) { From 289836f21d8c3a119561a6c8d58713822af81f77 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Wed, 28 Aug 2024 21:48:35 +0000 Subject: [PATCH 06/19] Minor cleanup --- avr.py | 4 ++-- src/Makefile | 2 +- src/reach/Makefile | 12 +++++------ src/reach/avr_config.cpp | 2 +- src/reach/avr_word_netlist.cpp | 18 ++++++++++------ src/reach/reach_backend.h | 39 +++++++++++++++++++++++----------- src/reach/reach_cegar.cpp | 8 ------- src/reach/reach_core.cpp | 16 ++++---------- src/reach/reach_y2.cpp | 2 +- src/vwn/btor2_frontend.cpp | 20 ++++++++--------- src/vwn/btor2_utils.h | 2 +- workers.txt | 4 ++-- 12 files changed, 66 insertions(+), 63 deletions(-) diff --git a/avr.py b/avr.py index 0bf84ef..f988576 100755 --- a/avr.py +++ b/avr.py @@ -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="-" @@ -65,7 +65,7 @@ def getopts(header): p.add_argument('-n', '--name', help=' (default: %s)' % DEFAULT_NAME, type=str, default=DEFAULT_NAME) p.add_argument('-o', '--out', help=' (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) diff --git a/src/Makefile b/src/Makefile index c6847e3..18983cc 100644 --- a/src/Makefile +++ b/src/Makefile @@ -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 diff --git a/src/reach/Makefile b/src/reach/Makefile index b3dcca2..3665bae 100644 --- a/src/reach/Makefile +++ b/src/reach/Makefile @@ -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 diff --git a/src/reach/avr_config.cpp b/src/reach/avr_config.cpp index 62ac4a2..3441c54 100644 --- a/src/reach/avr_config.cpp +++ b/src/reach/avr_config.cpp @@ -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; diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 60077fb..829a213 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -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) { @@ -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 @@ -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() { diff --git a/src/reach/reach_backend.h b/src/reach/reach_backend.h index 88a7ec7..b47853c 100644 --- a/src/reach/reach_backend.h +++ b/src/reach/reach_backend.h @@ -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 diff --git a/src/reach/reach_cegar.cpp b/src/reach/reach_cegar.cpp index eb2d0fa..b69c551 100644 --- a/src/reach/reach_cegar.cpp +++ b/src/reach/reach_cegar.cpp @@ -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 @@ -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; diff --git a/src/reach/reach_core.cpp b/src/reach/reach_core.cpp index 94b99b7..d7c82ce 100644 --- a/src/reach/reach_core.cpp +++ b/src/reach/reach_core.cpp @@ -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 diff --git a/src/reach/reach_y2.cpp b/src/reach/reach_y2.cpp index 3f6c2a8..21076ad 100644 --- a/src/reach/reach_y2.cpp +++ b/src/reach/reach_y2.cpp @@ -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); diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp index 4ba3531..8cf103b 100644 --- a/src/vwn/btor2_frontend.cpp +++ b/src/vwn/btor2_frontend.cpp @@ -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; diff --git a/src/vwn/btor2_utils.h b/src/vwn/btor2_utils.h index f62c4f2..de98bbd 100644 --- a/src/vwn/btor2_utils.h +++ b/src/vwn/btor2_utils.h @@ -36,7 +36,7 @@ extern "C" #include #include /* strtoimax, PRIdMAX, SCNdMAX */ - +#include #endif /* SRC_VWN_BTOR2_UTILS_H_ */ diff --git a/workers.txt b/workers.txt index c17de9a..4a72072 100755 --- a/workers.txt +++ b/workers.txt @@ -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 From bea68a0f9ad800ca8903dcf4010993c8c2d60060 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Thu, 29 Aug 2024 02:09:21 +0000 Subject: [PATCH 07/19] Minor fixes --- src/reach/avr_config.cpp | 8 ++++---- src/reach/avr_config.h | 4 ++-- src/reach/avr_word_netlist.cpp | 2 +- src/reach/reach_cegar.cpp | 21 +++++++++++---------- src/reach/reach_core.h | 1 + src/reach/reach_util.cpp | 8 ++++---- 6 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/reach/avr_config.cpp b/src/reach/avr_config.cpp index 3441c54..46f20aa 100644 --- a/src/reach/avr_config.cpp +++ b/src/reach/avr_config.cpp @@ -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 = false; +bool Config::g_uf_no_propagate = false; bool Config::g_uf_heavy_only = false; bool Config::g_uf_no_bitwise = false; bool Config::g_uf_no_sext = false; @@ -247,8 +247,8 @@ void Config::set_abstraction(string& name) { g_ab_interpret_excc = LEVEL_EXCC_DEFAULT; { - if (name.find(NAME_UF_PROPAGATE) != string::npos) - g_uf_propagate = !g_uf_propagate; + if (name.find(NAME_UF_NO_PROPAGATE) != string::npos) + g_uf_no_propagate = !g_uf_no_propagate; if (name.find(NAME_UF_HEAVY_ONLY) != string::npos) g_uf_heavy_only = !g_uf_heavy_only; if (name.find(NAME_UF_NO_BITWISE) != string::npos) @@ -298,7 +298,7 @@ void Config::set_abstraction(string& name) { << (g_ab_interpret_limit == 0?"":to_string(g_ab_interpret_limit)) << ((g_ab_interpret_excc != LEVEL_EXCC_DEFAULT)?"+ec"+to_string(g_ab_interpret_excc):"") << (g_fineness != FINENESS_DEFAULT?"+l"+to_string(g_fineness):"") - << (g_uf_propagate?"+propagate":"") + << (g_uf_no_propagate?"+nopropagate":"") << (g_uf_heavy_only?"+heavy":"") << (g_uf_no_bitwise?"+nobitwise":"") << (g_uf_no_sext?"+nosignex":"") diff --git a/src/reach/avr_config.h b/src/reach/avr_config.h index 3c04a22..8a80880 100644 --- a/src/reach/avr_config.h +++ b/src/reach/avr_config.h @@ -175,7 +175,7 @@ #define NAME_SABV "sa" #define NAME_EXCC "ec" -#define NAME_UF_PROPAGATE "+propagate" +#define NAME_UF_NO_PROPAGATE "+nopropagate" #define NAME_UF_HEAVY_ONLY "+heavy" #define NAME_UF_NO_BITWISE "+nobitwise" #define NAME_UF_NO_SEXT "+nosignex" @@ -263,7 +263,7 @@ class Config { static int g_forward_check; static int g_fineness; static int g_lazy_assume; - static bool g_uf_propagate; + static bool g_uf_no_propagate; static bool g_uf_heavy_only; static bool g_uf_no_bitwise; static bool g_uf_no_sext; diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 829a213..ee9d1cf 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -3680,7 +3680,7 @@ Inst* OpInst::create(OpInst::OpType op, InstL exps, int o_size, bool to_simplify // return e->t_simple; // do nothing, done } - else if (Config::g_uf_propagate) { + else if (!Config::g_uf_no_propagate) { e->propagate_uf(); } } diff --git a/src/reach/reach_cegar.cpp b/src/reach/reach_cegar.cpp index b69c551..8d8374c 100644 --- a/src/reach/reach_cegar.cpp +++ b/src/reach/reach_cegar.cpp @@ -539,11 +539,13 @@ void Reach::refine(InstL& hardConstraints, ABSTRACT_CUBE& abCube, Inst *top_wo_r else hardConstraints.push_back(v.first); } - for (auto& v: _assume_T) { - if (Config::g_lazy_assume > LAZY_ASSUME_NONE) - viol.push_back(v.first); - else - hardConstraints.push_back(v.first); + if (_frame_idx != 0) { + for (auto& v: _assume_T) { + if (Config::g_lazy_assume > LAZY_ASSUME_NONE) + viol.push_back(v.first); + else + hardConstraints.push_back(v.first); + } } if (!hardConstraints.empty()) { viol.push_back(OpInst::create(OpInst::LogAnd, hardConstraints)); @@ -6120,14 +6122,13 @@ int Reach::verify() { conjunct_prop.push_back(_ve_prop_eq_0); conjunct_prop.push_back(_ve_model); InstL conjunct_prop_wo_ref = conjunct_prop; - for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3) + for (InstL::iterator it3 = _negated_refs.begin(); it3 != _negated_refs.end(); ++it3) { + if (*it3 == _ve_assume_T) + continue; conjunct_prop.push_back(*it3); + } if (Config::g_lazy_assume >= LAZY_ASSUME_L2) conjunct_prop.push_back(_ve_assume); - if (Config::g_lazy_assume >= LAZY_ASSUME_L1) { - for (auto& v: _assume_T) - conjunct_prop.push_back(v.first); - } ve_prop = OpInst::create(OpInst::LogAnd, conjunct_prop); AVR_LOG(15, 0, "[Basis Step]:" << endl); diff --git a/src/reach/reach_core.h b/src/reach/reach_core.h index 26462dc..1c2abc7 100644 --- a/src/reach/reach_core.h +++ b/src/reach/reach_core.h @@ -1554,6 +1554,7 @@ class Reach{ InstL _assume_wires; InstS _assume_regNext; InstToBoolM _assume_T; + Inst* _ve_assume_T; InstL _assume_Twires; diff --git a/src/reach/reach_util.cpp b/src/reach/reach_util.cpp index cdd72dd..f060609 100644 --- a/src/reach/reach_util.cpp +++ b/src/reach/reach_util.cpp @@ -7415,8 +7415,8 @@ void Reach::collect_system() { assumeT.push_back(coneT); } if (!assumeT.empty()) { - Inst* tveAssume = OpInst::create(OpInst::LogAnd, assumeT); - add_all_wires(tveAssume, _assume_Twires, true); + _ve_assume_T = OpInst::create(OpInst::LogAnd, assumeT); + add_all_wires(_ve_assume_T, _assume_Twires, true); if (Config::g_lazy_assume >= LAZY_ASSUME_L1) { for (auto& v: assumeT) { _assume_T.insert(make_pair(v, false)); @@ -7424,8 +7424,8 @@ void Reach::collect_system() { } else { numAssumeLemmas++; - _negated_refs.push_back(tveAssume); - _assume_T.insert(make_pair(tveAssume, true)); + _negated_refs.push_back(_ve_assume_T); + _assume_T.insert(make_pair(_ve_assume_T, true)); } } } From 19b239555699a311cc2950fa26af3233620cbe37 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 30 Aug 2024 01:18:14 +0000 Subject: [PATCH 08/19] Correct negative decimal in btor --- src/vwn/btor2_frontend.cpp | 58 +++++++++++++++++++++++--------------- 1 file changed, 36 insertions(+), 22 deletions(-) diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp index 8cf103b..f0feedb 100644 --- a/src/vwn/btor2_frontend.cpp +++ b/src/vwn/btor2_frontend.cpp @@ -492,13 +492,16 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) { } break; case BTOR2_TAG_const: { string snum(t.constant); + if (snum[0] == '-') { + btor2_loge("negative boolean number isn't allowed: found in BTOR2_TAG_const " << snum); + } node = NumInst::create(snum, sz, 2, sort); -// { -// string numstr = NumInst::as(node)->get_mpz()->get_str(2); -// if (numstr != snum) { -// btor2_loge("number error: gave " << snum << ", got " << numstr); -// } -// } + { + string numstr = NumInst::as(node)->get_mpz()->get_str(2); + if (numstr != snum) { + btor2_loge("number error: gave " << snum << ", got " << numstr); + } + } constants.insert(node); done = true; } break; @@ -508,28 +511,39 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) { } break; case BTOR2_TAG_constd: { string snum(t.constant); - 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); - // } - // } + 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); + } + } else { + node = NumInst::create(snum, sz, 10, sort); + } + if (sz != 1) + { + 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; case BTOR2_TAG_consth: { string snum(t.constant); node = NumInst::create(snum, sz, 16, sort); -// { -// string numstr = NumInst::as(node)->get_mpz()->get_str(16); -// if (numstr != snum) { -// btor2_loge("number error: gave " << snum << ", got " << numstr); -// } -// } + { + string numstr = NumInst::as(node)->get_mpz()->get_str(16); + if (numstr != snum) { + btor2_loge("number error: gave " << snum << ", got " << numstr); + } + } constants.insert(node); done = true; } break; From 8caf71acab0e5ecc1db6949fb23be8a239729318 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 30 Aug 2024 01:24:51 +0000 Subject: [PATCH 09/19] Minor --- src/vwn/btor2_frontend.cpp | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp index f0feedb..a4f1885 100644 --- a/src/vwn/btor2_frontend.cpp +++ b/src/vwn/btor2_frontend.cpp @@ -496,12 +496,12 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) { btor2_loge("negative boolean number isn't allowed: found in BTOR2_TAG_const " << snum); } node = NumInst::create(snum, sz, 2, sort); - { - string numstr = NumInst::as(node)->get_mpz()->get_str(2); - if (numstr != snum) { - btor2_loge("number error: gave " << snum << ", got " << numstr); - } - } + // { + // string numstr = NumInst::as(node)->get_mpz()->get_str(2); + // if (numstr != snum) { + // btor2_loge("number error: gave " << snum << ", got " << numstr); + // } + // } constants.insert(node); done = true; } break; @@ -525,25 +525,25 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) { } else { node = NumInst::create(snum, sz, 10, sort); } - if (sz != 1) - { - string numstr = NumInst::as(node)->get_mpz()->get_str(10); - if (numstr != snum) { - btor2_loge("number error: gave " << snum << ", got " << numstr); - } - } + // if (sz != 1) + // { + // 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; case BTOR2_TAG_consth: { string snum(t.constant); node = NumInst::create(snum, sz, 16, sort); - { - string numstr = NumInst::as(node)->get_mpz()->get_str(16); - if (numstr != snum) { - btor2_loge("number error: gave " << snum << ", got " << numstr); - } - } + // { + // string numstr = NumInst::as(node)->get_mpz()->get_str(16); + // if (numstr != snum) { + // btor2_loge("number error: gave " << snum << ", got " << numstr); + // } + // } constants.insert(node); done = true; } break; From 651392879b4244b710875551f6d02a801fc336c6 Mon Sep 17 00:00:00 2001 From: Ubuntu Date: Fri, 30 Aug 2024 19:27:46 +0000 Subject: [PATCH 10/19] Minor --- src/reach/avr_word_netlist.cpp | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index ee9d1cf..6f94118 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -1897,11 +1897,14 @@ void OpInst::propagate_uf() { 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()); + // 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) { + // lhs / 1 = lhs (if not boolean) + t_simple = lhs; } else if (lhs == rhs) { - // x / x = 1 - t_simple = NumInst::create(1, get_size(), get_sort()); + // x / x = ? (since x can be 0) + // t_simple = NumInst::create(1, get_size(), get_sort()); } } } break; @@ -1917,14 +1920,14 @@ void OpInst::propagate_uf() { 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()); + // 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) { // lhs % 1 = 0 (if not boolean) t_simple = NumInst::create(0, get_size(), get_sort()); } else if (lhs == rhs) { - // x % x = 0 - t_simple = NumInst::create(0, get_size(), get_sort()); + // x % x = ? (since x can be 0) + // t_simple = NumInst::create(0, get_size(), get_sort()); } } } break; From a8fe19a614e12e96501dc34bcd86565905327b25 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Fri, 30 Aug 2024 19:31:16 +0000 Subject: [PATCH 11/19] Refactor --- .gitignore | 1 + README.md | 2 +- avr.py | 8 ++------ avr_pr.py | 6 +++--- 4 files changed, 7 insertions(+), 10 deletions(-) diff --git a/.gitignore b/.gitignore index 9a77152..bc2bed6 100644 --- a/.gitignore +++ b/.gitignore @@ -25,6 +25,7 @@ xtras/*/ .settings/* .d/* gmon.out +.*DS_Store # But not these files !.gitignore diff --git a/README.md b/README.md index 67aaecb..7b0d5d6 100755 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ # AVR -- **A**bstractly **V**erifying **R**eachability -

(also known as Averroes v2.0) +

(also known as Averroes v2)

diff --git a/avr.py b/avr.py index f988576..af71f60 100755 --- a/avr.py +++ b/avr.py @@ -9,17 +9,13 @@ # Author: Aman Goel (amangoel@umich.edu), University of Michigan ###################################################################################### -import os, sys +import os import subprocess import argparse -import tempfile -import shutil import ntpath -from distutils import spawn -import re from distutils.spawn import find_executable -version=2.1 +version=2.2 DEFAULT_TOP="-" DEFAULT_BIN="build/bin" diff --git a/avr_pr.py b/avr_pr.py index f567b4f..5eb225b 100755 --- a/avr_pr.py +++ b/avr_pr.py @@ -8,11 +8,11 @@ ###################################################################################### -import os, sys, datetime, time, resource, argparse, shutil, signal -from subprocess import Popen, PIPE, DEVNULL, STDOUT +import os, sys, time, argparse, shutil, signal +from subprocess import Popen, PIPE from enum import Enum -version=2.1 +version=2.2 start_time = time.time() cmdSuffix = "" From bd241b67ec0bde16c24a7bcb5bc075f1fe1fbf83 Mon Sep 17 00:00:00 2001 From: Ubuntu Date: Fri, 30 Aug 2024 20:53:01 +0000 Subject: [PATCH 12/19] Static compile --- src/dpa/Makefile | 2 +- src/makefile.include | 6 ++++-- src/reach/Makefile | 12 ++++++++---- src/reach/reach_backend.h | 34 +++++++++++++++++++++++----------- src/vwn/Makefile | 2 +- workers.txt | 24 ++++++++++++------------ 6 files changed, 49 insertions(+), 31 deletions(-) diff --git a/src/dpa/Makefile b/src/dpa/Makefile index ae529cc..36585ea 100644 --- a/src/dpa/Makefile +++ b/src/dpa/Makefile @@ -2,7 +2,7 @@ include ../makefile.include ifeq ($(STATIC_DPA), 1) CXX += -static-libstdc++ -static-libgcc -static - LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64 +# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64 LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive else LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl diff --git a/src/makefile.include b/src/makefile.include index edd40be..5d0773f 100644 --- a/src/makefile.include +++ b/src/makefile.include @@ -50,7 +50,8 @@ endif GPP=g++ -std=c++17 #### flags -CFLAG_OPT = -g -O3 +#CFLAG_OPT = -g -O3 +CFLAG_OPT = -O3 #### includes INCLUDE_DIRS = @@ -59,7 +60,8 @@ CFLAGS_INC = $(INCLUDE_DIRS) CFLAGS = -c $(CFLAGS_INC) $(CFLAG_OPT) #### optional flags -FLAG_PG = -pg +#FLAG_PG = -pg +FLAG_PG = #### link flags LINK_FLAGS = $(CFLAG_OPT) diff --git a/src/reach/Makefile b/src/reach/Makefile index 3665bae..205677e 100644 --- a/src/reach/Makefile +++ b/src/reach/Makefile @@ -1,10 +1,10 @@ include ../makefile.include -CFLAGS += -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label +CFLAGS += -fPIC -Werror -Wreturn-type -Wunknown-pragmas -Wunused-value -Wunused-label ifeq ($(STATIC_REA), 1) CXX += -static-libstdc++ -static-libgcc -static - LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64 +# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64 LINK_FLAGS += $(STATIC_GMPXX) $(STATIC_GMP) -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive else LINK_FLAGS += -pthread -lgmpxx -lgmp -lrt -ldl @@ -12,7 +12,7 @@ endif ifeq ($(ENABLE_Y2), 1) Y2_DIR = $(DEPS)/yices2 - Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a + Y2_LIB = $(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/lib/libyices.a $(STATIC_GMPXX) $(STATIC_GMP) INCLUDE += -I$(Y2_DIR)/build/x86_64-pc-linux-gnu-release/dist/include LINKLIBS += $(Y2_LIB) CFLAGS += -D_Y2 @@ -38,11 +38,15 @@ endif ifeq ($(ENABLE_M5), 1) MSAT_DIR = $(DEPS)/mathsat - MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a # $(STATIC_GMPXX) $(STATIC_GMP) + MSAT_LIB = $(MSAT_DIR)/lib/libmathsat.a $(STATIC_GMPXX) $(STATIC_GMP) INCLUDE += -I$(MSAT_DIR)/include 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 diff --git a/src/reach/reach_backend.h b/src/reach/reach_backend.h index b47853c..1fedbee 100644 --- a/src/reach/reach_backend.h +++ b/src/reach/reach_backend.h @@ -26,11 +26,23 @@ /// Configurations /// Note: Only one of the below flag should be enabled +// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries // #define BACKEND_Y2 // Yices 2 for all queries // #define BACKEND_BT // Boolector for all queries -// #define BACKEND_Y2BT // Yices 2 for abstract, Boolector for bv queries +// #define BACKEND_MT // MathSAT 5 for all queries + -// Use Y2 backend for all abstract 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 /// Config: BACKEND_Y2 #ifdef BACKEND_Y2 @@ -56,16 +68,16 @@ #define SOLVER_BV bt_API // Solver for concrete / bit-vector queries #endif -/// 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 +/// Config: BACKEND_M5 +#ifdef BACKEND_M5 + #define SOLVER_CTI m5_API // Solver for checking SAT_abstract ? [ F[top] ^ P ^ T ^ !P+ ] + #define SOLVER_REACH m5_API // Solver for checking SAT_abstract ? [ F[k-1] ^ P ^ T ^ C+ ] and for Fast-forward check + #define SOLVER_CONTAIN m5_API // Solver for checking if frame restriction global + #define SOLVER_AB m5_API // Solver for all other abstract queries: Basis check, Lemma redundancy check + #define SOLVER_CORE m5_API // Solver for getting unsat core + #define SOLVER_MUS m5_API // Solver for getting minimal unsat core - #define SOLVER_BV bt_API // Solver for concrete / bit-vector queries + #define SOLVER_BV m5_API // Solver for concrete / bit-vector queries #endif diff --git a/src/vwn/Makefile b/src/vwn/Makefile index 130487c..4b0077a 100644 --- a/src/vwn/Makefile +++ b/src/vwn/Makefile @@ -8,7 +8,7 @@ LINKLIBS = ifeq ($(STATIC_VWN), 1) CXX += -static-libstdc++ -static-libgcc -static - LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64 +# LINK_FLAGS += -L/usr/lib/x86_64-redhat-linux6E/lib64 LINK_FLAGS += -static -pthread -Wl,--whole-archive -lpthread -Wl,--no-whole-archive LINKLIBS += $(STATIC_GMPXX) $(STATIC_GMP) else diff --git a/workers.txt b/workers.txt index 4a72072..b6b78eb 100755 --- a/workers.txt +++ b/workers.txt @@ -1,16 +1,16 @@ -python3 avr.py --split +python3 avr.py --backend y2 --split python3 avr.py --kind --abstract sa --backend bt -python3 avr.py --kind --abstract sa --split -python3 avr.py --abstract sa --backend bt +python3 avr.py --kind --abstract sa --backend y2 --split python3 avr.py --abstract sa -python3 avr.py python3 avr.py --bmc --abstract sa --backend bt --split -python3 avr.py --bmc --abstract sa+heavy -python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1 -python3 avr.py --abstract sa4 --split --forward 1 --interpol 1 -python3 avr.py --abstract sa+heavy --backend bt --split +python3 avr.py +python3 avr.py --abstract sa8 --level 5 --granularity 3 --forward 1 --interpol 1 +python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1 +python3 avr.py --split --level 0 +python3 avr.py --abstract sa8 --backend y2 --split --interpol 1 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 sa32 --backend bt --level 0 --granularity 3 -python3 avr.py --abstract sa8 --level 5 --granularity 3 --interpol 1 --forward 1 +python3 avr.py --bmc --abstract sa --backend y2 +python3 avr.py --abstract sa --backend bt +python3 avr.py --abstract sa+heavy +python3 avr.py --bmc --abstract sa+heavy --backend bt +python3 avr.py --kind --abstract sa+heavy --backend bt From 4225df4f2103ad268d9646b45c67b4ee423d315f Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sat, 31 Aug 2024 09:24:43 +0000 Subject: [PATCH 13/19] 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) { From 2c867dc3b3ccdab493970addb14c24aba50cd5dd Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sat, 31 Aug 2024 09:32:33 +0000 Subject: [PATCH 14/19] Minor --- src/reach/avr_word_netlist.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 49cab3e..0144281 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -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() { From c586805fbf5b09f22b5fbe57cf40689600b1f136 Mon Sep 17 00:00:00 2001 From: Ubuntu Date: Sun, 1 Sep 2024 04:09:16 +0000 Subject: [PATCH 15/19] Stash changes --- avr_pr.py | 2 +- workers.txt | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/avr_pr.py b/avr_pr.py index 5eb225b..f6713df 100755 --- a/avr_pr.py +++ b/avr_pr.py @@ -37,7 +37,7 @@ maxTimeSec = DEFAULT_TIMEOUT maxMemMB = DEFAULT_MEMOUT -maxInitW = 12 +maxInitW = 16 resultW = 0 out_path = DEFAULT_OUT + "/" + DEFAULT_NAME diff --git a/workers.txt b/workers.txt index b6b78eb..ec90209 100755 --- a/workers.txt +++ b/workers.txt @@ -1,16 +1,16 @@ python3 avr.py --backend y2 --split -python3 avr.py --kind --abstract sa --backend bt python3 avr.py --kind --abstract sa --backend y2 --split python3 avr.py --abstract sa +python3 avr.py --kind --abstract sa --backend bt python3 avr.py --bmc --abstract sa --backend bt --split -python3 avr.py python3 avr.py --abstract sa8 --level 5 --granularity 3 --forward 1 --interpol 1 python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1 -python3 avr.py --split --level 0 +python3 avr.py python3 avr.py --abstract sa8 --backend y2 --split --interpol 1 -python3 avr.py --kind --abstract sa --backend bt --split -python3 avr.py --bmc --abstract sa --backend y2 -python3 avr.py --abstract sa --backend bt -python3 avr.py --abstract sa+heavy +python3 avr.py --split --level 0 python3 avr.py --bmc --abstract sa+heavy --backend bt -python3 avr.py --kind --abstract sa+heavy --backend bt +python3 avr.py --bmc --abstract sa --backend y2 +python3 avr.py --kind --abstract sa --backend bt --split +python3 avr.py --abstract sa+heavy --backend y2 --split +python3 avr.py --abstract sa16 --backend y2 --split +python3 avr.py --kind --abstract sa --backend y2 From 43ab77e4ed65a6211a77e7fc20164de81aae51b4 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Mon, 9 Sep 2024 08:12:44 +0000 Subject: [PATCH 16/19] Correct long int overflow in decimal const parsing in btor2 frontend --- src/vwn/btor2_frontend.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp index 967e11c..ea70225 100644 --- a/src/vwn/btor2_frontend.cpp +++ b/src/vwn/btor2_frontend.cpp @@ -514,7 +514,7 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) { mpz_t mpz_mask; mpz_init(mpz_mask); - mpz_set_si(mpz_mask, strtol(snum.c_str(), NULL, 10)); + mpz_set_str(mpz_mask, snum.c_str(), 10); mpz_class t_mpzc(mpz_mask); string str_num = t_mpzc.get_str(2); From d687a1bd283533d0992ae94678adb91ea4b0292d Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Tue, 10 Sep 2024 19:12:21 +0000 Subject: [PATCH 17/19] Correct int overflow in uf partial interpretation --- src/reach/avr_word_netlist.cpp | 54 +++++++++++++++++----------------- src/reach/avr_word_netlist.h | 10 +++++++ 2 files changed, 37 insertions(+), 27 deletions(-) diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 0144281..1b5b72d 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -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; } @@ -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 { @@ -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) { @@ -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 { @@ -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) { @@ -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) { @@ -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) { @@ -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) { @@ -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) { @@ -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) { @@ -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) { @@ -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) { @@ -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; } @@ -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() { diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h index 820431f..8b13c17 100644 --- a/src/reach/avr_word_netlist.h +++ b/src/reach/avr_word_netlist.h @@ -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) { From 170030a507894fbbdd29fc285716bc614ff86e6d Mon Sep 17 00:00:00 2001 From: Ubuntu Date: Tue, 10 Sep 2024 19:38:12 +0000 Subject: [PATCH 18/19] Minor updates --- avr_pr.py | 2 +- src/reach/avr_word_netlist.cpp | 6 +++--- workers.txt | 18 +++++++++--------- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/avr_pr.py b/avr_pr.py index f6713df..853f786 100755 --- a/avr_pr.py +++ b/avr_pr.py @@ -12,7 +12,7 @@ from subprocess import Popen, PIPE from enum import Enum -version=2.2 +version="2.2.3" start_time = time.time() cmdSuffix = "" diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 1b5b72d..e668960 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -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() { diff --git a/workers.txt b/workers.txt index ec90209..f5297d2 100755 --- a/workers.txt +++ b/workers.txt @@ -1,16 +1,16 @@ +python3 avr.py --backend y2 --split --abstract sa+uf+nopropagate python3 avr.py --backend y2 --split python3 avr.py --kind --abstract sa --backend y2 --split +python3 avr.py --kind --abstract sa --backend y2 python3 avr.py --abstract sa -python3 avr.py --kind --abstract sa --backend bt -python3 avr.py --bmc --abstract sa --backend bt --split python3 avr.py --abstract sa8 --level 5 --granularity 3 --forward 1 --interpol 1 -python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1 +python3 avr.py --bmc --abstract sa --backend y2 --split python3 avr.py -python3 avr.py --abstract sa8 --backend y2 --split --interpol 1 -python3 avr.py --split --level 0 -python3 avr.py --bmc --abstract sa+heavy --backend bt -python3 avr.py --bmc --abstract sa --backend y2 -python3 avr.py --kind --abstract sa --backend bt --split +python3 avr.py --bmc --abstract sa --backend bt +python3 avr.py --kind --abstract sa --backend bt +python3 avr.py --abstract sa4 --backend y2 --split --forward 1 --interpol 1 python3 avr.py --abstract sa+heavy --backend y2 --split +python3 avr.py --bmc --abstract sa+heavy --backend bt +python3 avr.py --split --level 0 python3 avr.py --abstract sa16 --backend y2 --split -python3 avr.py --kind --abstract sa --backend y2 +python3 avr.py --abstract sa8 --backend y2 --split --interpol 1 From 60b22cc6d180985b2dfa0aa19d898a9b27e7672f Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Tue, 10 Sep 2024 23:11:29 +0000 Subject: [PATCH 19/19] Minor correction --- avr_pr.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/avr_pr.py b/avr_pr.py index 853f786..b52e909 100755 --- a/avr_pr.py +++ b/avr_pr.py @@ -431,8 +431,11 @@ def terminate_ps(pid_s): valid, pid = is_valid_pid(pid_s) if (valid): if (check_pid(pid)): - os.kill(pid, signal.SIGTERM) - os.kill(pid, signal.SIGKILL) + try: + os.kill(pid, signal.SIGTERM) + os.kill(pid, signal.SIGKILL) + except ProcessLookupError: + pass #else: #assert(0)