diff --git a/src/alg.py b/src/alg.py index b2ec1ba0..aa6c8592 100644 --- a/src/alg.py +++ b/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,7 +363,8 @@ 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 @@ -368,7 +372,8 @@ def _g(l): 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 @@ -376,7 +381,8 @@ def _g(l): 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 @@ -384,7 +390,8 @@ def _g(l): 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 diff --git a/src/c_instrument.py b/src/c_instrument.py index a60e7647..28b003b4 100644 --- a/src/c_instrument.py +++ b/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)) diff --git a/src/data/symstates.py b/src/data/symstates.py index d83b1929..e8c149e1 100644 --- a/src/data/symstates.py +++ b/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 diff --git a/src/settings.py b/src/settings.py index de9144e4..e74ec582 100644 --- a/src/settings.py +++ b/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)