fix --early-exit #437
fix --early-exit #437
Conversation
|
Things I checked:
Things I still need to check:
|
| @@ -0,0 +1,174 @@ | |||
| import json | |||
There was a problem hiding this comment.
no changes here, just moving build-related functionality out of __main__.py and into its own module
| @@ -0,0 +1,160 @@ | |||
| import io | |||
There was a problem hiding this comment.
no changes here, just moving trace-related functionality out of __main__.py and into its own module
| @@ -0,0 +1,217 @@ | |||
| import concurrent.futures | |||
There was a problem hiding this comment.
new module that provides an executor/futures abstraction layer built on top of subprocess.Popen
src/halmos/solve.py
Outdated
| return SolverOutput.from_result(stdout, stderr, returncode, path_ctx) | ||
|
|
||
|
|
||
| def solve_end_to_end(ctx: PathContext) -> None: |
There was a problem hiding this comment.
used to be gen_model_from_sexpr
| @dataclass(frozen=True) | ||
| class PathContext: | ||
| # id of this path | ||
| path_id: int |
There was a problem hiding this comment.
roughly corresponds to the old iteration idx
|
|
||
| refined_ctx = ctx.refine() | ||
|
|
||
| if refined_ctx.query.smtlib != query.smtlib: |
0xkarmacoma
force-pushed
the
fix/early-exit
branch
from
625d4df to
bfce538
Compare
(hopefully works on windows too)
0xkarmacoma
force-pushed
the
fix/early-exit
branch
from
1e8c6cd to
5068e59
Compare
|
TODO: fix the case where:
ERROR encountered exception during assertion solving: RuntimeError('Cannot submit to a shutdown executor.')
ERROR exception calling callback for <Future at 0x112aee4e0 state=finished raised RuntimeError>
Traceback (most recent call last):
File "/Users/karma/.pyenv/versions/3.12.1/lib/python3.12/concurrent/futures/_base.py", line 340, in _invoke_callbacks
callback(self)
File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 472, in solve_end_to_end_callback
solver_output = future.result()
^^^^^^^^^^^^^^^
File "/Users/karma/.pyenv/versions/3.12.1/lib/python3.12/concurrent/futures/_base.py", line 449, in result
return self.__get_result()
^^^^^^^^^^^^^^^^^^^
File "/Users/karma/.pyenv/versions/3.12.1/lib/python3.12/concurrent/futures/_base.py", line 401, in __get_result
raise self._exception
File "/Users/karma/.pyenv/versions/3.12.1/lib/python3.12/concurrent/futures/thread.py", line 58, in run
result = self.fn(*self.args, **self.kwargs)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/Users/karma/projects/halmos/src/halmos/solve.py", line 438, in solve_end_to_end
solver_output = solve_low_level(ctx)
^^^^^^^^^^^^^^^^^^^^
File "/Users/karma/projects/halmos/src/halmos/solve.py", line 399, in solve_low_level
path_ctx.solving_ctx.executor.submit(future)
File "/Users/karma/projects/halmos/src/halmos/processes.py", line 161, in submit
raise RuntimeError("Cannot submit to a shutdown executor.")
RuntimeError: Cannot submit to a shutdown executor. We need some way to also interrupt path exploration when early exit is triggered. |
✅ in 1fc8649 |
src/halmos/__main__.py
Outdated
| render_trace(setup_ex.context) | ||
|
|
||
| else: | ||
| setup_exs_no_error.append(setup_ex) |
There was a problem hiding this comment.
this refactoring is incorrect. the smt query needs to be generated 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.
alternatively, we could consider modifying path.to_smt2() to not rely on the shared solver. the idea is to create a temporary new solver with a separate z3 context, add all path constraints to the new solver, and generate a smt query from it. this indeeds already happens when --cache-solver is enabled. so this approach would improve the code maintainability avoiding this potential mistake in the future. but, a downside is the additional performance overhead of creating a new solver and translating all constraints to the new context. wdyt?
There was a problem hiding this comment.
good catch, I didn't realize. I agree that managing paths and context is a bit of a minefield, I believe I have restored it to its original meaning in 9a9d3cd and made a comment about the landmine. We can re-evaluate later if a different approach is needed 🙏
src/halmos/__main__.py
Outdated
| path_ctx = PathContext( | ||
| args=args, | ||
| path_id=path_id, | ||
| query=ex.path.to_smt2(args), |
There was a problem hiding this comment.
as mentioned above, calling path.to_smt2() here will generate an incorrect query unless it's the last path.
the ci failure might be related to this:
https://github.com/a16z/halmos/actions/runs/12958246417/job/36148232775#step:9:27
and fix off by one error in num_execs
Co-authored-by: Daejun Park <[email protected]>
10x faster morpho-data-structures testProveNextBucket [PASS] testProveNextBucket(uint256) (paths: 100, time: 123.20s (paths: 123.20s, models: 0.00s), bounds: []) [PASS] testProveNextBucket(uint256) (paths: 100, time: 12.11s (paths: 11.28s, models: 0.83s), bounds: [])
| f"loop condition: {cond}\n" | ||
| f"calldata: {ex.calldata()}\n" | ||
| f"path condition:\n{ex.path}\n" | ||
| ) |
There was a problem hiding this comment.
oh wow. great catch. (curious why it wasn't caught earlier by my performance regression testing.)
There was a problem hiding this comment.
it has a disproportionate effect on the morpho test because it bumps against the loop limit and also has very complex path conditions, not much visible effect on other tests
There was a problem hiding this comment.
looks good to me!
it seems we're still having intermittent failures with the morpho tests. there may be still hidden issues with z3 objects related to threading or garbage collection. but i'm ok with merging this for now and addressing it separately, so we can merge this long running pr. i'll defer to you.
fixes #243
high-level notes:
thread_pool.shutdown(wait=False)was not what we needed it to be)PopenExecutor.shutdown(wait=False), it does terminate/kill every process that has been submitted to that executor and is still runningsolve_end_to_endfunction calls to a thread pool, but that functions submitssolve_low_levelcalls to the executor and blocks on the result.solve_low_levelcan be interrupted if the underlying process returns, times out, gets killed, etc -- this is the key architectural change--solver-commanddefaults toz3) and we need to parse the model values from the smtlib output. This means we no longer printCounterexample: see xyz.smt2Additionally, to make the transition to this model easier I introduced a hierarchy of context objects: