Stashing temp changes

.gitignore

@@ -6,11 +6,13 @@
 .idea/
 
 build/bin*/dpa
-build/bin*/reach
+build/bin*/reach*
 build/bin*/vwn
 
+hwmcc*/
 deps/*
 output/*
+xtras/*/
 
 *.a
 *.o

build/avr → 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=$?
 

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='<test-name> (default: %s)' % DEFAULT_NAME, type=str, default=DEFAULT_NAME)
 	p.add_argument('-o', '--out',       help='<output-path> (default: %s)' % DEFAULT_OUT, type=str, default=DEFAULT_OUT)
 	p.add_argument('-b', '--bin',       help='binary path (default: %s)' % DEFAULT_BIN, type=str, default=DEFAULT_BIN)
+	p.add_argument('--backend',         help='backend to use: y2, bt, m5 (default: %s)' % DEFAULT_BACKEND, type=str, default=DEFAULT_BACKEND)
 	p.add_argument('-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)

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
 

deps/build_deps.sh

@@ -1,7 +1,7 @@
 #!/bin/bash -x
 set -e
 
-MATHSATVERSION="5.6.10"
+MATHSATVERSION="5.6.11"
 
 echo "Installing dependencies..."
 

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

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;

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

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: ;

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;

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;

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