From 9a9d3cd719dd8ba48a46335928f51f706545df02 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Mon, 27 Jan 2025 14:47:15 -0800 Subject: [PATCH] fix unsafe setup_ex.path.to_smt2() access --- src/halmos/__main__.py | 13 +++++++------ src/halmos/solve.py | 6 ++++-- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index 3cca1ebb..16d33c10 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -318,7 +318,7 @@ def setup(ctx: FunctionContext) -> Exec: ) setup_exs_all = sevm.run(setup_ex) - setup_exs_no_error: list[Exec] = [] + setup_exs_no_error: list[tuple[Exec, SMTQuery]] = [] for path_id, setup_ex in enumerate(setup_exs_all): if args.verbose >= VERBOSITY_TRACE_SETUP: @@ -339,24 +339,25 @@ def setup(ctx: FunctionContext) -> Exec: render_trace(setup_ex.context) else: - setup_exs_no_error.append(setup_ex) + # note: ex.path.to_smt2() needs to be called at this point. The solver object is shared across paths, + # and solver.to_smt2() will return a different query if it is called after a different path is explored. + setup_exs_no_error.append((setup_ex, setup_ex.path.to_smt2(args))) setup_exs: list[Exec] = [] match setup_exs_no_error: case []: pass - case [ex]: + case [(ex, _)]: setup_exs.append(ex) case _: - for path_id, ex in enumerate(setup_exs_no_error): + for path_id, (ex, query) in enumerate(setup_exs_no_error): path_ctx = PathContext( args=args, path_id=path_id, - query=ex.path.to_smt2(args), + query=query, solving_ctx=ctx.solving_ctx, ) - solver_output = solve_low_level(path_ctx) if solver_output.result != unsat: setup_exs.append(ex) diff --git a/src/halmos/solve.py b/src/halmos/solve.py index 7518c238..6374e25c 100644 --- a/src/halmos/solve.py +++ b/src/halmos/solve.py @@ -445,8 +445,10 @@ def solve_end_to_end(ctx: PathContext) -> SolverOutput: refined_ctx = ctx.refine() if refined_ctx.query.smtlib != query.smtlib: - # recurse with the refined query - return solve_end_to_end(refined_ctx) + # note that check_unsat_cores cannot return true for the refined query, because it relies on only + # constraint ids, which don't change after refinement + # therefore we can skip the unsat core check in solve_end_to_end and go directly to solve_low_level + return solve_low_level(refined_ctx) else: verbose(" Refinement did not change the query, no need to solve again")