Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix --early-exit #437

Merged
merged 46 commits into from
Jan 28, 2025
Merged

fix --early-exit #437

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
93c32f6
add build directory to .gitignore
0xkarmacoma Dec 18, 2024
d419691
add psutil to dependencies
0xkarmacoma Dec 18, 2024
57151cf
add PopenFuture and PopenExecutor
0xkarmacoma Dec 18, 2024
771dea6
WIP: add traces.py
0xkarmacoma Jan 16, 2025
076caae
XXX sort data into contract, function and path contexts
0xkarmacoma Jan 16, 2025
926e733
XXX early exit wired actually wired
0xkarmacoma Jan 16, 2025
e72b36d
add triage for solver models
0xkarmacoma Jan 16, 2025
45d9e67
add basic smtlib parsing
0xkarmacoma Dec 20, 2024
1bdafec
actually parse external solver output using smtlib
0xkarmacoma Dec 21, 2024
db346c0
fix counterexample output
0xkarmacoma Jan 17, 2025
bfe126d
make z3 the default --solver-command (so we always dump queries)
0xkarmacoma Jan 8, 2025
cdf4e16
bring back refinement
0xkarmacoma Jan 17, 2025
175ede3
fix solve invocation in setup
0xkarmacoma Jan 9, 2025
cf85376
bring back timeouts, clean children after timeout
0xkarmacoma Jan 17, 2025
ea3d493
migrate build output parsing function in build.py
0xkarmacoma Jan 9, 2025
2239231
move solving-related functions to solve.py
0xkarmacoma Jan 9, 2025
19c772f
fix setup_exs_no_error access pattern
0xkarmacoma Jan 9, 2025
5d1a24f
merge smtlib.py into solve.py
0xkarmacoma Jan 9, 2025
b1ebdc6
adjust halmos_var_pattern to support p_ prefix
0xkarmacoma Jan 9, 2025
d847464
speed up early exit
0xkarmacoma Jan 9, 2025
03ed948
bring back model output in solve_end_to_end
0xkarmacoma Jan 9, 2025
a6fd067
shutdown executors on signal
0xkarmacoma Jan 10, 2025
f41a3cb
disable ExecutorRegistry().shutdown_all() for now
0xkarmacoma Jan 16, 2025
7b38cdc
fix bad merge
0xkarmacoma Jan 17, 2025
0125a3d
fix z3 thread safety issue (--print-failed-states disabled for now)
0xkarmacoma Jan 17, 2025
51657ba
fix setup() with multiple paths
0xkarmacoma Jan 17, 2025
01dcb3b
share a SolvingContext between FunctionContext and PathContext
0xkarmacoma Jan 17, 2025
85ca04c
use tempfile and path to manage smt2 files
0xkarmacoma Jan 18, 2025
5831899
TemporaryDirectory 3.11 compatibility support
0xkarmacoma Jan 18, 2025
61834c0
trying a thing on windows
0xkarmacoma Jan 18, 2025
d3a63a3
try specifying full path to z3
0xkarmacoma Jan 18, 2025
955f410
warn if z3 is not found
0xkarmacoma Jan 18, 2025
9355d09
update uv version
0xkarmacoma Jan 18, 2025
9859579
fix bad reference
0xkarmacoma Jan 22, 2025
b9f2985
XXX print path to see what's up on windows ci
0xkarmacoma Jan 22, 2025
5068e59
finish merge
0xkarmacoma Jan 22, 2025
60ef79c
print venv contents
0xkarmacoma Jan 22, 2025
5803051
dynamically locate z3 in the venv
0xkarmacoma Jan 23, 2025
1fc8649
fix: avoid raising when path exploration > first cex
0xkarmacoma Jan 23, 2025
f705954
cleanup: print trace counterexample in the right place
0xkarmacoma Jan 25, 2025
3a501ae
bring back the executor shutdown in on_exit
0xkarmacoma Jan 25, 2025
d7dddf8
fix status display condition
0xkarmacoma Jan 25, 2025
9a9d3cd
fix unsafe setup_ex.path.to_smt2() access
0xkarmacoma Jan 27, 2025
7d5d350
simplify PotentialModel
0xkarmacoma Jan 27, 2025
e918408
only render paths to string when debug is active
0xkarmacoma Jan 28, 2025
0b7dc6e
switch halmos-solady to bitwuzla
0xkarmacoma Jan 28, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/test-external.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ jobs:
profile: ""
- repo: "zobront/halmos-solady"
dir: "halmos-solady"
cmd: "--function testCheck --solver-command yices-smt2 --solver-threads 3"
cmd: "--function testCheck --solver-command 'bitwuzla --produce-models' --solver-threads 3"
branch: ""
profile: ""
- repo: "pcaversaccio/snekmate"
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ jobs:
uses: astral-sh/setup-uv@v4
with:
# Install a specific version of uv.
version: "0.5.6"
version: "0.5.21"

- name: Set up python ${{ matrix.python-version }}
run: uv python install ${{ matrix.python-version }}
Expand Down
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,3 +31,6 @@ out/
# - adds friction to CI
# (at the cost of reproducible builds)
uv.lock

# https://docs.astral.sh/uv/concepts/projects/layout/#the-build-directory
build/
3 changes: 2 additions & 1 deletion pyproject.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,8 @@ dependencies = [
"z3-solver==4.12.6.0",
"eth_hash[pysha3]>=0.7.0",
"rich>=13.9.4",
"xxhash>=3.5.0"
"xxhash>=3.5.0",
"psutil>=6.1.0",
]
dynamic = ["version"]

Expand Down
Loading
Loading