Merge pull request #218 from jix/fix_engine_list

Fix engine_list's return value

sbysrc/sby_core.py

@@ -305,7 +305,9 @@ class SbyConfig:
                 if section == "engines":
                     mode = "engines"
 
-                    if args is not None:
+                    if args is None:
+                        engine_mode = None
+                    else:
                         section_args = args.split()
 
                         if len(section_args) > 1:
@@ -314,11 +316,16 @@ class SbyConfig:
                         if section_args[0] not in ("bmc", "prove", "cover", "live"):
                             self.error(f"sby file syntax error: Expected one of 'bmc', 'prove', 'cover', 'live' as '[engines]' argument, got '{section_args[0]}'")
 
-                        if section_args[0] in self.engines:
+                        engine_mode = section_args[0]
-                            self.error(f"Already defined engine block for mode '{section_args[0]}'")
+
+                    if engine_mode in self.engines:
+                        if engine_mode is None:
+                            self.error(f"Already defined engine block")
                         else:
-                            self.engines[section_args[0]] = list()
+                            self.error(f"Already defined engine block for mode '{engine_mode}'")
-                            engine_mode = section_args[0]
+                    else:
+                        self.engines[engine_mode] = list()
+
                     continue
 
                 if section == "setup":
@@ -415,8 +422,6 @@ class SbyConfig:
 
             if mode == "engines":
                 args = line.strip().split()
-                if engine_mode not in self.engines:
-                    self.engines[engine_mode] = list()
                 self.engines[engine_mode].append(args)
                 continue
 
@@ -642,7 +647,8 @@ class SbyTask(SbyConfig):
                     print(line, file=f)
 
     def engine_list(self):
-        return list(enumerate(self.engines.items()))
+        engines = self.engines.get(None, []) + self.engines.get(self.opt_mode, [])
+        return list(enumerate(engines))
 
     def check_timeout(self):
         if self.opt_timeout is not None:

sbysrc/sby_mode_bmc.py

@@ -24,20 +24,8 @@ def run(task):
     task.handle_int_option("append", 0)
     task.handle_str_option("aigsmt", "yices")
 
-    for engine_idx, engine_section in task.engine_list():
+    for engine_idx, engine in task.engine_list():
-        if isinstance(engine_section, list):
+        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
-            engine = engine_section
-            engine_name = None
-        else:
-            assert len(engine_section[1]) > 0
-            engine = engine_section[1][0]
-            engine_name = engine_section[0]
-
-        if engine_name is None:
-            engine_name = engine_idx
-
-
-        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "smtbmc":

sbysrc/sby_mode_cover.py

@@ -23,19 +23,8 @@ def run(task):
     task.handle_int_option("depth", 20)
     task.handle_int_option("append", 0)
 
-    for engine_idx, engine_section in task.engine_list():
+    for engine_idx, engine in task.engine_list():
-        if isinstance(engine_section, list):
+        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
-            engine = engine_section
-            engine_name = None
-        else:
-            assert len(engine_section[1]) > 0
-            engine = engine_section[1][0]
-            engine_name = engine_section[0]
-
-        if engine_name is None:
-            engine_name = engine_idx
-
-        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "smtbmc":

sbysrc/sby_mode_live.py

@@ -24,19 +24,8 @@ def run(task):
 
     task.status = "UNKNOWN"
 
-    for engine_idx, engine_section in task.engine_list():
+    for engine_idx, engine in task.engine_list():
-        if isinstance(engine_section, list):
+        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
-            engine = engine_section
-            engine_name = None
-        else:
-            assert len(engine_section[1]) > 0
-            engine = engine_section[1][0]
-            engine_name = engine_section[0]
-
-        if engine_name is None:
-            engine_name = engine_idx
-
-        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "aiger":

sbysrc/sby_mode_prove.py

@@ -31,19 +31,8 @@ def run(task):
     task.basecase_procs = list()
     task.induction_procs = list()
 
-    for engine_idx, engine_section in task.engine_list():
+    for engine_idx, engine in task.engine_list():
-        if isinstance(engine_section, list):
+        task.log(f"""engine_{engine_idx}: {" ".join(engine)}""")
-            engine = engine_section
-            engine_name = None
-        else:
-            assert len(engine_section[1]) > 0
-            engine = engine_section[1][0]
-            engine_name = engine_section[0]
-
-        if engine_name is None:
-            engine_name = engine_idx
-
-        task.log(f"""engine_{engine_name}: {" ".join(engine)}""")
         task.makedirs(f"{task.workdir}/engine_{engine_idx}")
 
         if engine[0] == "smtbmc":

tests/regression/option_skip.sby

@@ -0,0 +1,33 @@
+[tasks]
+smtbmc_pass: smtbmc pass
+smtbmc_fail: smtbmc fail
+btormc_pass: btormc pass
+btormc_fail: btormc fail
+
+[options]
+mode bmc
+pass: expect pass
+fail: expect fail
+pass: depth 5
+fail: depth 6
+
+skip 2
+
+[engines]
+smtbmc: smtbmc boolector
+[engines bmc]
+btormc: btor btormc
+
+[script]
+read -formal top.sv
+prep -top top
+
+[file top.sv]
+module top(input clk);
+    reg [7:0] counter = 0;
+
+    always @(posedge clk) begin
+        counter <= counter + 1;
+        assert (counter < 4);
+    end
+endmodule