Add "expect" config option

diff --git a/docs/examples/quickstart/memory.sby b/docs/examples/quickstart/memory.sby
index 4b250609bce3538e9763d9e0067715179ea18d3f..055d8daee98d2a037f5c74b1044642c3e63c178e 100644 (file)
--- a/docs/examples/quickstart/memory.sby
+++ b/docs/examples/quickstart/memory.sby
@@ -1,6 +1,7 @@
 [options]
 mode bmc
 depth 10
+expect fail
 
 [engines]
 smtbmc -s boolector

diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index cddcf58527038058cee5b1d77fe0d6a316fac306..14667d685c8f839c4eac6e894da06efaaa7a51dc 100644 (file)
--- a/sbysrc/sby.py
+++ b/sbysrc/sby.py
@@ -84,5 +84,5 @@ if opt_force:
 job = SbyJob(sbyfile, workdir, early_logmsgs)
 job.run()
 
-sys.exit(0 if job.status == "PASS" else 1)
+sys.exit(job.retcode)
 

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 3adc6a9568df05ec4523a29239af1a356693a629..f85125901cfaf138089b741df898416c90540d97 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -128,7 +128,9 @@ class SbyJob:
         self.models = dict()
         self.workdir = workdir
 
-        self.status = None
+        self.status = "UNKNOWN"
+        self.expect = ["PASS"]
+
         self.tasks_running = []
         self.tasks_all = []
 
@@ -327,9 +329,35 @@ class SbyJob:
         for task in self.tasks_running:
             task.terminate()
 
+    def update_status(self, new_status):
+        assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
+
+        if new_status == "UNKNOWN":
+            return
+
+        if self.status == "ERROR":
+            return
+
+        if new_status == "PASS":
+            assert self.status != "FAIL"
+            self.status = "PASS"
+
+        elif new_status == "FAIL":
+            assert self.status != "PASS"
+            self.status = "FAIL"
+
+        elif new_status == "ERROR":
+            self.status = "ERROR"
+
+        else:
+            assert 0
+
     def run(self):
         assert "mode" in self.options
 
+        if "expect" in self.options:
+            self.expect = self.options["expect"].upper().split(",")
+
         self.copy_src()
 
         if self.options["mode"] == "bmc":
@@ -363,8 +391,17 @@ class SbyJob:
             self.log("summary: %s" % line)
 
         self.log("DONE (%s)" % self.status)
+
         assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
 
+        if self.status in self.expect:
+            self.retcode = 0
+        else:
+            if self.status == "PASS": self.retcode = 1
+            if self.status == "FAIL": self.retcode = 2
+            if self.status == "ERROR": self.retcode = 3
+            if self.status == "UNKNOWN": self.retcode = 4
+
         with open("%s/%s" % (self.workdir, self.status), "w") as f:
             for line in self.summary:
                 print(line, file=f)

diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py
index f3b114903ddf446a0bc7053421ca88b4efc40ae0..9aa0d48f0745388692f87c266da406e0294c65fe 100644 (file)
--- a/sbysrc/sby_engine_abc.py
+++ b/sbysrc/sby_engine_abc.py
@@ -75,13 +75,13 @@ def run(mode, job, engine_idx, engine):
         assert retcode == 0
         assert task_status is not None
 
-        job.status = task_status
+        job.update_status(task_status)
         job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
-        job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
+        job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status))
 
         job.terminate()
 
-        if job.status == "FAIL":
+        if task_status == "FAIL":
             task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"),
                     ("cd %s; yosys-smtbmc --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " +
                      "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") %

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index c57bf476e9daac83f3c79a398b1a249f78e585ad..0ac29fc779e0a6ec11e1f36ac468957cee7e467a 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -90,11 +90,11 @@ def run(mode, job, engine_idx, engine):
         assert task_status is not None
 
         if mode == "bmc" or mode == "cover":
-            job.status = task_status
+            job.update_status(task_status)
             job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status))
-            job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), job.status))
+            job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status))
 
-            if job.status == "FAIL" and mode != "cover":
+            if task_status == "FAIL" and mode != "cover":
                 job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
 
             job.terminate()
@@ -111,7 +111,7 @@ def run(mode, job, engine_idx, engine):
                     job.basecase_pass = True
 
                 else:
-                    job.status = task_status
+                    job.update_status(task_status)
                     job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx))
                     job.terminate()
 
@@ -126,7 +126,7 @@ def run(mode, job, engine_idx, engine):
                 assert False
 
             if job.basecase_pass and job.induction_pass:
-                job.status = "PASS"
+                job.update_status("PASS")
                 job.summary.append("successful proof by k-induction.")
                 job.terminate()