Imported GIT HEAD: 0.8+20190328git32bd0f2

4 files changed, 176 insertions, 22 deletions

diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index dce82f01..92941d4c 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o
 
 ifneq ($(CONFIG),mxe)
 ifneq ($(CONFIG),emcc)
+
+# MSYS targets support yosys-smtbmc, but require a launcher script
+ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
+TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py
+# Needed to find the Python interpreter for yosys-smtbmc scripts.
+# Override if necessary, it is only used for msys2 targets.
+PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
+
+yosys-smtbmc-script.py: backends/smt2/smtbmc.py
+	$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \
+		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+
+yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
+	$(P) gcc -DGUI=0 -O -s -o $@ $<
+# Other targets
+else
 TARGETS += yosys-smtbmc
 
 yosys-smtbmc: backends/smt2/smtbmc.py
 	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
 	$(Q) chmod +x $@.new
 	$(Q) mv $@.new $@
+endif
 
 $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
 endif
 endif
-
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e2777ae0..688535f3 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -416,6 +416,7 @@ struct Smt2Worker
 		for (char ch : expr) {
 			if (ch == 'A') processed_expr += get_bv(sig_a);
 			else if (ch == 'B') processed_expr += get_bv(sig_b);
+			else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
 			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
 			else processed_expr += ch;
@@ -554,7 +555,9 @@ struct Smt2Worker
 
 			if (cell->type.in("$shift", "$shiftx")) {
 				if (cell->getParam("\\B_SIGNED").as_bool()) {
-					/* FIXME */
+					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
+							"(bvlshr A B) (bvlshr A (bvneg B)))",
+							GetSize(cell->getPort("\\B")), 0), 's');
 				} else {
 					return export_bvop(cell, "(bvlshr A B)", 's');
 				}
@@ -885,8 +888,8 @@ struct Smt2Worker
 
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
-				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
-						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+				string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
 
 				if (cell->type == "$cover")
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
@@ -1101,20 +1104,27 @@ struct Smt2Worker
 							break;
 
 						Const initword = init_data.extract(i*width, width, State::Sx);
+						Const initmask = initword;
 						bool gen_init_constr = false;
 
-						for (auto bit : initword.bits)
-							if (bit == State::S0 || bit == State::S1)
+						for (int k = 0; k < GetSize(initword); k++) {
+							if (initword[k] == State::S0 || initword[k] == State::S1) {
 								gen_init_constr = true;
+								initmask[k] = State::S1;
+							} else {
+								initmask[k] = State::S0;
+								initword[k] = State::S0;
+							}
+						}
 
 						if (gen_init_constr)
 						{
 							if (statebv)
 								/* FIXME */;
 							else
-								init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+								init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
 										get_id(module), arrayid, Const(i, abits).as_string().c_str(),
-										initword.as_string().c_str(), get_id(cell), i));
+										initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
 						}
 					}
 				}
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 6af2a5ac..445a42e0 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -32,6 +32,7 @@ cexfile = None
 aimfile = None
 aiwfile = None
 aigheader = True
+btorwitfile = None
 vlogtbfile = None
 vlogtbtop = None
 inconstr = list()
@@ -86,12 +87,15 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
     --aig <aim_filename>:<aiw_filename>
         like above, but for map files and witness files that do not
-        share a filename prefix (or use differen file extensions).
+        share a filename prefix (or use different file extensions).
 
     --aig-noheader
         the AIGER witness file does not include the status and
         properties lines.
 
+    --btorwit <btor_witness_filename>
+        read a BTOR witness.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -99,8 +103,8 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --presat
         check if the design with assumptions but without assertions
         is SAT before checking if assertions are UNSAT. This will
-        detect if there are contradicting assumtions. In some cases
-        this will also help to "warmup" the solver, potentially
+        detect if there are contradicting assumptions. In some cases
+        this will also help to "warm up" the solver, potentially
         yielding a speedup.
 
     --final-only
@@ -145,14 +149,14 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --append <num_steps>
         add <num_steps> time steps at the end of the trace
         when creating a counter example (this additional time
-        steps will still be constrained by assumtions)
+        steps will still be constrained by assumptions)
 """ + so.helpmsg())
     sys.exit(1)
 
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
              "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
              "smtc-init", "smtc-top=", "noinit"])
 except:
@@ -189,6 +193,8 @@ for o, a in opts:
             aiwfile = a + ".aiw"
     elif o == "--aig-noheader":
         aigheader = False
+    elif o == "--btorwit":
+        btorwitfile = a
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -575,6 +581,103 @@ if aimfile is not None:
                 num_steps = max(num_steps, step+1)
             step += 1
 
+if btorwitfile is not None:
+    with open(btorwitfile, "r") as f:
+        step = None
+        suffix = None
+        altsuffix = None
+        header_okay = False
+
+        for line in f:
+            line = line.strip()
+
+            if line == "sat":
+                header_okay = True
+                continue
+
+            if not header_okay:
+                continue
+
+            if line == "" or line[0] == "b" or line[0] == "j":
+                continue
+
+            if line == ".":
+                break
+
+            if line[0] == '#' or line[0] == '@':
+                step = int(line[1:])
+                suffix = line
+                altsuffix = suffix
+                if suffix[0] == "@":
+                    altsuffix = "#" + suffix[1:]
+                else:
+                    altsuffix = "@" + suffix[1:]
+                continue
+
+            line = line.split()
+
+            if len(line) == 0:
+                continue
+
+            if line[-1].endswith(suffix):
+                line[-1] = line[-1][0:len(line[-1]) - len(suffix)]
+
+            if line[-1].endswith(altsuffix):
+                line[-1] = line[-1][0:len(line[-1]) - len(altsuffix)]
+
+            if line[-1][0] == "$":
+                continue
+
+            # BV assignments
+            if len(line) == 3 and line[1][0] != "[":
+                value = line[1]
+                name = line[2]
+
+                path = smt.get_path(topmod, name)
+
+                if not smt.net_exists(topmod, path):
+                    continue
+
+                width = smt.net_width(topmod, path)
+
+                if width == 1:
+                    assert value in ["0", "1"]
+                    value = "true" if value == "1" else "false"
+                else:
+                    value = "#b" + value
+
+                smtexpr = "(= [%s] %s)" % (name, value)
+                constr_assumes[step].append((btorwitfile, smtexpr))
+
+            # Array assignments
+            if len(line) == 4 and line[1][0] == "[":
+                index = line[1]
+                value = line[2]
+                name = line[3]
+
+                path = smt.get_path(topmod, name)
+
+                if not smt.mem_exists(topmod, path):
+                    continue
+
+                meminfo = smt.mem_info(topmod, path)
+
+                if meminfo[1] == 1:
+                    assert value in ["0", "1"]
+                    value = "true" if value == "1" else "false"
+                else:
+                    value = "#b" + value
+
+                assert index[0] == "["
+                assert index[-1] == "]"
+                index = "#b" + index[1:-1]
+
+                smtexpr = "(= (select [%s] %s) %s)" % (name, index, value)
+                constr_assumes[step].append((btorwitfile, smtexpr))
+
+        skip_steps = step
+        num_steps = step+1
+
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)
     print_msg("Writing trace to VCD file: %s" % (filename))
@@ -1259,7 +1362,11 @@ elif covermode:
                     smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
                     smt_assert_consequent(get_constr_expr(constr_assumes, i))
                 print_msg("Re-solving with appended steps..")
-                assert smt_check_sat() == "sat"
+                if smt_check_sat() == "unsat":
+                    print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+                    found_failed_assert = True
+                    retstatus = False
+                    break
 
             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
             assert len(reached_covers) == len(cover_desc)
@@ -1377,7 +1484,11 @@ else:  # not tempind, covermode
                             smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
                             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
-                            assert smt_check_sat() == "sat"
+                        print_msg("Re-solving with appended steps..")
+                        if smt_check_sat() == "unsat":
+                            print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+                            retstatus = False
+                            break
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 3fc823e3..ab20a4af 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -31,11 +31,19 @@ from threading import Thread
 # does not run out of stack frames when parsing large expressions
 if os.name == "posix":
     smtio_reclimit = 64 * 1024
-    smtio_stacksize = 128 * 1024 * 1024
     if sys.getrecursionlimit() < smtio_reclimit:
         sys.setrecursionlimit(smtio_reclimit)
-    if resource.getrlimit(resource.RLIMIT_STACK)[0] < smtio_stacksize:
-        resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, -1))
+
+    current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK)
+    if current_rlimit_stack[0] != resource.RLIM_INFINITY:
+        smtio_stacksize = 128 * 1024 * 1024
+        if os.uname().sysname == "Darwin":
+            # MacOS has rather conservative stack limits
+            smtio_stacksize = 16 * 1024 * 1024
+        if current_rlimit_stack[1] != resource.RLIM_INFINITY:
+            smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
+        if current_rlimit_stack[0] < smtio_stacksize:
+            resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
 
 
 # currently running solvers (so we can kill them)
@@ -158,19 +166,28 @@ class SmtIo:
             self.unroll = False
 
         if self.solver == "yices":
-            self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
+            if self.noincr:
+                self.popen_vargs = ['yices-smt2'] + self.solver_opts
+            else:
+                self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 
         if self.solver == "z3":
             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
 
         if self.solver == "cvc4":
-            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+            if self.noincr:
+                self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
+            else:
+                self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 
         if self.solver == "mathsat":
             self.popen_vargs = ['mathsat'] + self.solver_opts
 
         if self.solver == "boolector":
-            self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
+            if self.noincr:
+                self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
+            else:
+                self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
             self.unroll = True
 
         if self.solver == "abc":
@@ -767,7 +784,7 @@ class SmtIo:
 
     def get_path(self, mod, path):
         assert mod in self.modinfo
-        path = path.split(".")
+        path = path.replace("\\", "/").split(".")
 
         for i in range(len(path)-1):
             first = ".".join(path[0:i+1])