diff options
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 4 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 117 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 29 |
3 files changed, 140 insertions, 10 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e2777ae04..418f8d766 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -554,7 +554,9 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - /* FIXME */ + return export_bvop(cell, stringf("(ite (bvsge B #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'); } diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 6af2a5ac1..721a395e3 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() @@ -92,6 +93,9 @@ yosys-smtbmc [options] <yosys_smt2_output> 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) @@ -152,7 +156,7 @@ yosys-smtbmc [options] <yosys_smt2_output> 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 3fc823e3e..68783e744 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": |