Code

fix --early-exit#437

Code

Merged

0xkarmacoma merged 46 commits intomaina16z/halmos:mainfrom fix/early-exita16z/halmos:fix/early-exitCopy head branch name to clipboardJan 28, 2025

+1,544-857

Commits

Commits on Jan 22, 2025

• add build directory to .gitignore

  0xkarmacoma

  committed
  93c32f6

  Copy full SHA for 93c32f6

• add psutil to dependencies

  0xkarmacoma

  committed
  d419691

  Copy full SHA for d419691

• add PopenFuture and PopenExecutor

  0xkarmacoma

  committed
  57151cf

  Copy full SHA for 57151cf

• WIP: add traces.py

  0xkarmacoma

  committed
  771dea6

  Copy full SHA for 771dea6

• XXX sort data into contract, function and path contexts

  0xkarmacoma

  committed
  076caae

  Copy full SHA for 076caae

• XXX early exit wired actually wired

  0xkarmacoma

  committed
  926e733

  Copy full SHA for 926e733

• add triage for solver models

  0xkarmacoma

  committed
  e72b36d

  Copy full SHA for e72b36d

• add basic smtlib parsing

  0xkarmacoma

  committed
  45d9e67

  Copy full SHA for 45d9e67

• actually parse external solver output using smtlib

  0xkarmacoma

  committed
  1bdafec

  Copy full SHA for 1bdafec

• fix counterexample output

  0xkarmacoma

  committed
  db346c0

  Copy full SHA for db346c0

• make z3 the default --solver-command (so we always dump queries)

  0xkarmacoma

  committed
  bfe126d

  Copy full SHA for bfe126d

• bring back refinement

  0xkarmacoma

  committed
  cdf4e16

  Copy full SHA for cdf4e16

• fix solve invocation in setup

  0xkarmacoma

  committed
  175ede3

  Copy full SHA for 175ede3

• bring back timeouts, clean children after timeout

  0xkarmacoma

  committed
  cf85376

  Copy full SHA for cf85376

• migrate build output parsing function in build.py

  0xkarmacoma

  committed
  ea3d493

  Copy full SHA for ea3d493

• move solving-related functions to solve.py

  0xkarmacoma

  committed
  2239231

  Copy full SHA for 2239231

• fix setup_exs_no_error access pattern

  0xkarmacoma

  committed
  19c772f

  Copy full SHA for 19c772f

• merge smtlib.py into solve.py

  0xkarmacoma

  committed
  5d1a24f

  Copy full SHA for 5d1a24f

• adjust halmos_var_pattern to support p_ prefix

  0xkarmacoma

  committed
  b1ebdc6

  Copy full SHA for b1ebdc6

• speed up early exit

  0xkarmacoma

  committed
  d847464

  Copy full SHA for d847464

• bring back model output in solve_end_to_end

  0xkarmacoma

  committed
  03ed948

  Copy full SHA for 03ed948

• shutdown executors on signal

  0xkarmacoma

  committed
  a6fd067

  Copy full SHA for a6fd067

• disable ExecutorRegistry().shutdown_all() for now

  0xkarmacoma

  committed
  f41a3cb

  Copy full SHA for f41a3cb

• fix bad merge

  0xkarmacoma

  committed
  7b38cdc

  Copy full SHA for 7b38cdc

• fix z3 thread safety issue (--print-failed-states disabled for now)

  0xkarmacoma

  committed
  0125a3d

  Copy full SHA for 0125a3d

• fix setup() with multiple paths

  0xkarmacoma

  committed
  51657ba

  Copy full SHA for 51657ba

• share a SolvingContext between FunctionContext and PathContext

  0xkarmacoma

  committed
  01dcb3b

  Copy full SHA for 01dcb3b

• use tempfile and path to manage smt2 files

  Show description for 85ca04c
  0xkarmacoma

  committed
  85ca04c

  Copy full SHA for 85ca04c

• TemporaryDirectory 3.11 compatibility support

  0xkarmacoma

  committed
  5831899

  Copy full SHA for 5831899

• trying a thing on windows

  0xkarmacoma

  committed
  61834c0

  Copy full SHA for 61834c0

• try specifying full path to z3

  0xkarmacoma

  committed
  d3a63a3

  Copy full SHA for d3a63a3

• warn if z3 is not found

  0xkarmacoma

  committed
  955f410

  Copy full SHA for 955f410

• update uv version

  0xkarmacoma

  committed
  9355d09

  Copy full SHA for 9355d09

• fix bad reference

  0xkarmacoma

  committed
  9859579

  Copy full SHA for 9859579

• XXX print path to see what's up on windows ci

  0xkarmacoma

  committed
  b9f2985

  Copy full SHA for b9f2985

• finish merge

  0xkarmacoma

  committed
  5068e59

  Copy full SHA for 5068e59

• print venv contents

  0xkarmacoma

  committed
  60ef79c

  Copy full SHA for 60ef79c

Commits on Jan 23, 2025

• dynamically locate z3 in the venv

  0xkarmacoma

  committed
  5803051

  Copy full SHA for 5803051

• fix: avoid raising when path exploration > first cex

  0xkarmacoma

  committed
  1fc8649

  Copy full SHA for 1fc8649

Commits on Jan 25, 2025

• cleanup: print trace counterexample in the right place

  Show description for f705954
  0xkarmacoma

  committed
  f705954

  Copy full SHA for f705954

• bring back the executor shutdown in on_exit

  0xkarmacoma

  committed
  3a501ae

  Copy full SHA for 3a501ae

• fix status display condition

  Show description for d7dddf8
  

  0xkarmacoma

  and

  daejunpark

  authored
  d7dddf8

  Copy full SHA for d7dddf8

Commits on Jan 27, 2025

• fix unsafe setup_ex.path.to_smt2() access

  0xkarmacoma

  committed
  9a9d3cd

  Copy full SHA for 9a9d3cd

• simplify PotentialModel

  0xkarmacoma

  committed
  7d5d350

  Copy full SHA for 7d5d350

Commits on Jan 28, 2025

• only render paths to string when debug is active

  Show description for e918408
  0xkarmacoma

  committed
  e918408

  Copy full SHA for e918408

• switch halmos-solady to bitwuzla

  0xkarmacoma

  committed
  0b7dc6e

  Copy full SHA for 0b7dc6e