various small updates from copilot

Author: ThanhVu (Vu) Nguyen

src/alg.py

@@ -194,7 +194,7 @@ def f(tasks):
         return dinvs
 
     @beartype
-    def cleanup(self, dinvs:DInvs, dtraces:DTraces) -> None:
+    def cleanup(self, dinvs: DInvs, dtraces: DTraces) -> None:
         """
         Save and analyze result
         Clean up tmpdir
@@ -231,7 +231,7 @@ def _infer(self, typ: str, _get_invs: Callable) -> tuple:
         return typ, (dinvs, dtraces),  et
 
     @beartype
-    def _infer_eqts(self, maxdeg:int | None) -> tuple[DInvs, DTraces]:
+    def _infer_eqts(self, maxdeg: int | None) -> tuple[DInvs, DTraces]:
         dinvs, dtraces = infer.eqt.Infer(
             self.symstates, self.prog).gen(self.get_auto_deg(maxdeg))
         return dinvs, dtraces
@@ -325,8 +325,11 @@ def start(self, seed: float, maxdeg: int | None) -> DInvs:
             f"got {self.dtraces.siz} traces over {len(self.dtraces)} locs")
         mlog.debug(f"{self.dtraces}")
 
-        tasks = (self._nested_arrays_tasks() + self._eqts_tasks(maxdeg) + self._ieqs_tasks() +
-                 self._minmax_tasks() + self._congruences_tasks())
+        tasks = (self._nested_arrays_tasks() +
+                 self._eqts_tasks(maxdeg) +
+                 self._ieqs_tasks() +
+                 self._minmax_tasks() +
+                 self._congruences_tasks())
 
         def f(tasks):
             rs = [(loc, _f(loc)) for loc, _f in tasks]
@@ -360,31 +363,35 @@ def _eqts_tasks(self, maxdeg):
         autodeg = self.get_auto_deg(maxdeg)
 
         def _f(l):
-            return infer.eqt.Infer.gen_from_traces(autodeg, self.dtraces[l], self.inv_decls[l])
+            return infer.eqt.Infer.gen_from_traces(
+                autodeg, self.dtraces[l], self.inv_decls[l])
 
         def _g(l):
             return not self.inv_decls[l].array_only
         return self._mk_tasks(settings.DO_EQTS, _g, _f)
 
     def _ieqs_tasks(self):
         def _f(l):
-            return infer.oct.Infer.gen_from_traces(self.dtraces[l], self.inv_decls[l])
+            return infer.oct.Infer.gen_from_traces(
+                self.dtraces[l], self.inv_decls[l])
 
         def _g(l):
             return not self.inv_decls[l].array_only
         return self._mk_tasks(settings.DO_IEQS, _g,  _f)
 
     def _minmax_tasks(self):
         def _f(l):
-            return infer.mp.Infer.gen_from_traces(self.dtraces[l], self.inv_decls[l])
+            return infer.mp.Infer.gen_from_traces(
+                self.dtraces[l], self.inv_decls[l])
 
         def _g(l):
             return not self.inv_decls[l].array_only
         return self._mk_tasks(settings.DO_MINMAXPLUS, _g, _f)
 
     def _congruences_tasks(self):
         def _f(l):
-            return infer.congruence.Infer.gen_from_traces(self.dtraces[l], self.inv_decls[l])
+            return infer.congruence.Infer.gen_from_traces(
+                self.dtraces[l], self.inv_decls[l])
 
         def _g(l):
             return not self.inv_decls[l].array_only

src/c_instrument.py

@@ -21,6 +21,7 @@ def replacer(match):
     )
     return re.sub(pattern, replacer, text)
 
+
 class AddPrintfVisitor(c_ast.NodeVisitor):
     """
     add printf() calls to vtrace definitions
@@ -30,12 +31,12 @@ def __init__(self, vtrace: str) -> None:
         self.vtrace = vtrace
 
     @beartype
-    def visit_FuncDef(self, node:c_ast.Node) -> None:
+    def visit_FuncDef(self, node: c_ast.Node) -> None:
         if node.decl.name.startswith(self.vtrace) and not node.body.block_items:
             self._insert_funccall(node)
 
     @beartype
-    def _insert_funccall(self,node:c_ast.FuncDef)-> None:
+    def _insert_funccall(self, node: c_ast.FuncDef)-> None:
         myvars = [p.name for p in node.decl.type.args.params]
         funcalls  = self._create_new_funs(node.decl.name, myvars)
         node.body.block_items = funcalls
@@ -122,14 +123,14 @@ def visit_FuncDef(self, node:c_ast.Node) -> None:
 
 
 @beartype
-def gen(filename:Path, myast:c_ast.FileAST, includes:list[str]) -> None:
+def gen(filename: Path, myast: c_ast.FileAST, includes: list[str]) -> None:
     generator = c_generator.CGenerator()
     instr = generator.visit(myast)
     instr = '\n'.join(includes + [instr])
     vwrite(filename, instr)
 
 @beartype    
-def instrument(filename:Path, tracefile:Path,  symexefile:Path) -> list[str]:
+def instrument(filename: Path, tracefile: Path,  symexefile: Path) -> list[str]:
     includes = []
     src = []
     text = filename.read_text()
@@ -181,4 +182,4 @@ def instrument(filename:Path, tracefile:Path,  symexefile:Path) -> list[str]:
     symexefile = Path(sys.argv[2])    
     tracefile = Path(sys.argv[3])
     typ_output = instrument(filename, tracefile, symexefile)
-    print('\n'.join(typ_info))
+    print('\n'.join(typ_output))

src/data/symstates.py

@@ -647,10 +647,11 @@ def get_solver_stats(self):
                     self.solver_stats_.append(stat)
                 except Empty:
                     break
-                except:
+                except Exception:
                     mlog.exception(f"get_solver_stats() error")
                     break
 
+
 class SymStatesMaker(metaclass=abc.ABCMeta):
 
     @beartype
@@ -678,8 +679,15 @@ def compute(self) -> defaultdict:
         """
         Run symbolic execution to obtain symbolic states
         """
-        tasks = [depth for depth in
-                    range(self.mindepth, settings.SE_MAXDEPTH + 1)]
+
+        mind = self.mindepth
+        maxd = settings.SE_MAX_DEPTH 
+        if mind >= maxd:
+            mlog.warning("mindepth {mind} >= maxdepth {maxd}, "
+                         "setting mindepth=maxdepth={maxd}")
+            mind = maxd
+            
+        tasks = [depth for depth in range(mind, maxd + 1)]
 
         def f(tasks):
             rs = [(depth, self.get_ss(depth)) for depth in tasks]
@@ -699,8 +707,12 @@ def f(tasks):
 
         def f(tasks):
             rs = [symstates[loc][depth] for loc, depth in tasks]
-            rs = [
-                (loc, depth, Z3.to_smt2_str(pcs.myexpr), Z3.to_smt2_str(pcs.mypc))
+            rs = [(
+                    loc,
+                    depth,
+                    Z3.to_smt2_str(pcs.myexpr),
+                    Z3.to_smt2_str(pcs.mypc)
+                )
                 for pcs, (loc, depth) in zip(rs, tasks)
             ]
             return rs
@@ -856,7 +868,7 @@ def mk(self, depth:int) -> str:
         return settings.Java.JPF_RUN(jpffile=self.mk_JPF_runfile(max_val, depth))
 
     @beartype
-    def mk_JPF_runfile(self, max_int:int, depth:int) -> Path:
+    def mk_JPF_runfile(self, max_int: int, depth: int) -> Path:
         assert max_int >= 0, max_int
 
         symargs = ["sym"] * self.ninps

src/settings.py

@@ -27,7 +27,7 @@
 N_RAND_INPS = 100  # number of random inputs, only used when DO_SS is False
 INP_MAX_V = 300
 SE_DEPTH_NOCHANGES_MAX = 3
-SE_MAXDEPTH = 30
+SE_MAX_DEPTH = 30
 SOLVER_TIMEOUT = 3  # secs
 EQT_RATE = 1.5
 UGLY_FACTOR = 20  # remove equalities that have lots of terms and "large" coefficients
@@ -61,6 +61,7 @@
 JAVAC_CMD = Path("/usr/bin/javac")
 JAVA_CMD = Path("/usr/bin/java")
 
+
 class Java:
     SE_MIN_DEPTH = 7
 
@@ -259,10 +260,10 @@ def setup(settings, args):
 
     if args.se_maxdepth and args.se_maxdepth >= 1:
         if settings:
-            settings.SE_MAXDEPTH = args.se_maxdepth
+            settings.SE_MAX_DEPTH = args.se_maxdepth
         else:
             opts.append(f"-se_maxdepth {args.se_maxdepth}")
-
+            
     if args.tmpdir:
         if settings:
             settings.TMPDIR = Path(args.tmpdir)