Predicates as a combinator, the final stretch#391
Open
giltho wants to merge 19 commits into
Open
Conversation
Signed-off-by: Sacha Ayoun <[email protected]>
Signed-off-by: Sacha Ayoun <[email protected]>
Signed-off-by: Sacha Ayoun <[email protected]>
Signed-off-by: Sacha Ayoun <[email protected]>
Signed-off-by: Sacha Ayoun <[email protected]>
Signed-off-by: Sacha Ayoun <[email protected]>
giltho
changed the title
…start Signed-off-by: Sacha Ayoun <[email protected]>
… fixes, of_resolver, single verifier stack Behavior-neutral groundwork for moving predicate/wand reasoning into the Abstraction combinator: - Combinators.Abstraction.err_t becomes a proper variant (MissingUPred/ MissingWand/AsrtFailure/OtherErr/SubError) with can_fix/get_fixes/ get_recovery_tactic/get_failing_constraint mirroring the StateErr behaviour PState/Matcher exhibit today for the same situations. - Fix the split_further stub: SubPred splitting now delegates to the underlying memory (it was silently disabled since the wiring commit, turning off core-pred splitting in wand packaging). - Fix sure_is_nonempty to account for non-pure predicates and wands. - Delayed.of_resolver: inverse of resolve, entry point for direct-style (multi-pc) matching code in memory models. - Drop S_verification_NEEDS_CLEANUP: the symbolic debugger now uses the same Verification stack; V_lifter additionally re-projects memory errors (SubError) onto the tool lifter. - Dormant Config.preds_in_memory transition flag; demote a stray stdout print in Matcher to verbose logging. Validated: dune build @ALL, dune fmt, dune test, wisl quicktests, Amazon C + JS (all specs), act sll.c (15/0/2), C + JS env suites.
Matching_walker holds the representation-generic matching-plan machinery (produce_assertion/produce/produce_posts, match_ins_outs_lists, match_assertion, match_mp, match_ + its fuel-limited recovery loop), polymorphic over the state and error types via an ops record, in direct style (explicit states and result lists). Matcher.Make becomes the state-level instantiation: state operations map to State.*, and the user-predicate/wand arms of produce/consume are passed as transitional hooks carrying the exact legacy Pred_state-based code. The fold/unfold/package machinery stays in Matcher for now and goes through the walker for assertion-level production and matching. match_kind/recovery_tactic move to the walker with manifest re-exports, so all external users (PState, Verifier, match_map, debuggers) are unaffected. This is a pure factoring: no behavior change intended, and none observed. Validated: dune build @ALL, dune fmt, dune test, wisl quicktests, Amazon C (114s, all specs) + JS (all specs), act sll.c (15/0/2), C + JS env suites.
…ombinator Implements the full predicate/wand machinery inside Combinators.Abstraction, in direct style over an explicit matching state (memory + path condition), entering Delayed only at the MonadicSMemory boundary (via Delayed.of_resolver): - the memory-level instantiation of the matching walker (pure/typing ops mirror SState.assume_a/assert_a/assume_t/get_type/simplify_val over the materialized pc; sub-memory consume/produce run under the same per-operation matching-flag policy as SState); - consume with candidate lookup (reusing Preds.consume_pred and Wands.consume_wand with pc-based equality) and auto-folding on miss; - fold/unfold (incl. guards and additional bindings), rec_unfold, unfold_all, the predicate selection strategies, unfold_with_vals, unfold_concrete_preds, try_recovering — ports of the Matcher algorithms over the immutable abs state; - wand packaging with two independent path conditions (lhs vs current); - internalized automation, replacing engine-driven recovery: sub-action failures retry after fold/unfold recovery (mirroring the interpreter loop, fuel 10), consumption failures recover step-locally, and concrete-ins predicates are eagerly unfolded after every boundary operation (verification mode only; UX errors flow up unswallowed for bi-abduction); - the four predicate actions (fold/unfold/gunfold/package) implemented against the SLCmd encoding. The new code paths are cold until Config.preds_in_memory routes predicate traffic below the state: pre-flip, the (live) recovery and unfold-concrete wrappers are no-ops over empty predicate sets. Validated: dune build @ALL, dune fmt, dune test, wisl quicktests, Amazon C + JS (all specs), act sll.c (15/0/2), C + JS env suites.
…n_memory All seams are now in place, off by default (toggle with GILLIAN_PREDS_IN_MEMORY=1): - Matcher's legacy user-pred/wand produce/consume arms fall through to the generic core-predicate path (-> the memory) when the flag is set; - PState.execute_action delegates the four predicate actions to the memory, keeping only the state-level concerns as a shim (argument evaluation through the store, Unfold binding spec-vars, the legacy post-action simplifications); - the Normaliser routes user-pred/wand core predicates through produce_core_asrts instead of building Preds.t/Wands.t directly; - a new reserved action GILLIAN_USER_PRED__recover lets the state-level automation (assume-with-unfold on guarded gotos, the matching retry loop) delegate fold/unfold recovery to the memory: this was needed in practice (WISL pointer arithmetic relies on assume-unfold killing junk-pointer branches, and post-conditions rely on the retry loop for pure facts hidden under folded predicates); - the debugger lifter re-projects the memory's predicates so the predicate pane keeps working. Fixes surfaced by A/B-running the suites both ways: - PState's *-assert/consume forget mechanism dropped the substituted state (correct only under in-place mutation; the immutable memory made the predicate rename vanish) - now binds the substituted state; - the walker's matching retry loop only progressed because try_recovering mutated the state-level predicate set in place; an advance_recovery_base ops field lets immutable-store instantiations progress by recovering from the previously recovered state; - in-memory recovery results are simplified at the state level (collapsing the equality chains an unfold introduces), mirroring the legacy unfold; - is_overlapping_asrt no longer forwards user-pred/wand names to the underlying memory (some memories fail hard on unknown names); - pcs that learn a literal false are pruned at the memory boundaries (the legacy engine dropped such branches at its satisfiability checks); - no recovery/eager-unfolding around plain consume/produce: recovery belongs to the matching retry loop and the action path, like the legacy engine - anything more stacks search on search and blows up on recursive predicates. Status with the flag ON: wisl quicktests (127/127 incl. wand.wisl), dune test, act sll.c (15/0/2), C and JS env suites all pass; Amazon C is at 34/38 procs (4 under investigation), Amazon JS under test. Flag OFF (default): the full validation matrix passes unchanged. Validated (flag off): dune build @ALL, dune fmt, dune test, wisl quicktests, Amazon C + JS (all specs), act sll.c (15/0/2), C + JS env suites.
With GILLIAN_PREDS_IN_MEMORY=1, the complete validation matrix now passes: wisl quicktests (127/127, incl. wand.wisl designed failures), dune test, act sll.c (15/0/2), C and JS env suites, Amazon C (all 38 specs) and Amazon JS (all specs). Final two fixes: - unfoldings must be simplified with ~matching:true before any matching:false reduction sees them: an unfolding can pin a location lvar through a pure fact while the sub-memory produce, unable to see the equality, mints a fresh abstract location for the same lvar; only an aloc-unifying (matching) simplification reconciles the two. The PState action shim now applies it after Unfold and GUnfold, and the memory-level [learn] splits conjunctions (like Pc.extend) so that location resolution sees equalities buried in reduced pair-equalities in the first place. - candidate selection for user predicates and wands is outs-aware again: the walker forwards the outs it already knows through a transitional ambient channel (Consume_hints, same dynamic-scoping idea as MP.get_pred_defs), and the memory uses them for scoring only. Without this, two same-name predicates sharing their ins (e.g. two ListToSet over the same list) are picked arbitrarily where the legacy consume picked by outs, failing the post-hoc outs check. Known follow-up before flipping the default: Amazon JS is functionally correct but ~40x slower flag-on (Amazon C: +20%); the hot suspects are per-call pfs materialization in the memory-level equality checks and the eager concrete-unfold pass on every action.
Behavior-parity + perf groundwork for GILLIAN_PREDS_IN_MEMORY=1; flag off is unchanged. Matrix green both ways (quicktests 127, dune test, act 15/0/2, Amazon C all specs, C/JS env suites). Amazon JS passes flag-on but ~40x slower; investigation notes live in the plan file. - Walker recovery-loop progress now uses an explicit exclusion set instead of relying on Preds mutation (or the interim advance_recovery_base, which made recovery dig through recursive preds): ops.try_recovering takes/returns ~tried candidates and always re-launches from astate_i; Abstraction's consume_pred_with_vs ~exclude filters tried candidates while popping the chosen one from the full pred list. The _recover action carries tried as a 4th encoded arg and returns the chosen candidate in its ret values. - execute_sub_action recovers once per action evaluation instead of once per error branch. - Pc: memoize the materialized pfs/gamma (hot in candidate scoring); invalidated on copy/make/extend/extend_types and Abstraction.learn. - Consume_hints: ambient outs-hint channel so the predicate-carrying memory scores candidates on known outs (selection only; outs are still checked by the walker). Fixes wrong-candidate picks in Amazon C (ListToSetUnion, enc_ctx_deserialize). - Abstraction.learn splits conjunctions (location resolution only scans top-level formulas) and resets the pc memo. - should_unfold is purely syntactic (Expr.to_literal on in-args).
Fixes the ~40x Amazon JS slowdown with GILLIAN_PREDS_IN_MEMORY=1 (391s -> 9.7s, on par with the legacy 9.5s). Abstraction.execute_sub_action recovered internally on fixable sub-memory action failures, which preempted the interpreter's own action-retry loop (the error never reached it). The internal path has no state-level simplify, so the alias chains introduced by each unfold were never canonicalized and every later action on the same structure re-dug through it: readElements fired 440 GetCell recovery chains (CElement unfolded 154x, ArrayBuffer 106x) and ~5x the SMT queries, against 84 recoveries total for the legacy engine. Sub-action failures now flow up unswallowed; the interpreter retries through PState.try_recovering, which flag-on delegates to the reserved recover action and simplifies the recovered states — the exact legacy cadence. (Flag-off this recovery was always a no-op: the combinator's pred list is empty when predicates live outside the memory.) Full matrix green both ways: dune test, wisl quicktests 127/127, Amazon C all specs (123s on / 112s off), Amazon JS all specs (9.7s / 9.5s), act sll.c exactly 15/0/2, C env (output identical modulo lvar numbering) and JS env suites.
User-defined predicates and wands are now handled by the Combinators.Abstraction memory combinator by default; the legacy PState/Matcher path remains selectable with GILLIAN_PREDS_IN_MEMORY=0 until the cleanup phase removes it. Full matrix green with the new default: dune test (transformers + C incremental now exercise the in-memory path), wisl quicktests 127/127 (and 127/127 with =0), Amazon C all specs (123s), Amazon JS all specs (9.5s), act sll.c exactly 15/0/2, C env (fail-lines identical to the validated run) and JS env suites.
Predicates and wands are now handled exclusively by the Combinators.Abstraction memory combinator; the transition flag (Config.preds_in_memory / GILLIAN_PREDS_IN_MEMORY) is gone. - matching_walker: drop the transitional consume/produce hooks; user predicates and wands reach consume_core_pred/produce_core_pred like any core predicate. - Matcher: delete the legacy arms and the moved algorithms (consume_pred, consume_wand, fold, unfold, unfold_with_vals', rec_unfold, unfold_all, fold_guarded_with_vals, select_guarded_predicate_to_fold, Predicate_selection_strategies, consume_pred_with_vs, extend_subst_with_bindings, Wand_packaging, package_wand, unfold_concrete_preds and the legacy try_recovering body). S shrinks to Logging, produce, produce_assertion, produce_posts, try_recovering, match_assertion and match_. simplify_astate stays (recovery simplifies recovered states). - PState: delete eval_pred_slcmd (actions always go through the eval/spec-vars/post-simplify shim), the legacy assume-unfold branch, run_spec_aux's state-level concrete unfolding (the memory's post-pass covers it) and set_preds/set_wands. - Normaliser: separate_assertion returns core/pure/types only; normalise_preds/normalise_wands deleted (predicate facts are learned by the memory when producing). - command_line: the debugger predicate pane always re-projects the memory's predicates. Net -1691 lines. Full matrix green: dune test, wisl quicktests 127/127, Amazon C all specs (123s), Amazon JS all specs (9.5s), act sll.c exactly 15/0/2, C env (fail-lines identical) and JS env suites.
Predicates and wands live in the memory (Combinators.Abstraction), so the
state-level {state; preds; wands} record carried permanently-empty fields.
This deletes Pred_state and makes Matcher.t and PState.t the underlying
SState directly.
To keep the dependency graph acyclic once SState itself instantiates the
matcher (next commit), Matcher.Make's parameter is narrowed from SState.S
to a self-contained MatchableState signature spelling out exactly what the
matching engine needs from a state.
The matching reports' astate payload shrinks accordingly (AstateRec is now
just the state); the debugger's predicate pane is unaffected since it is
re-projected from the memory by the command-line lifter.
Validation: dune test; wisl quicktests 127; Amazon C all specs (122.8s);
Amazon JS all specs (9.46s); act sll.c 15 success / 0 error / 2 bug;
C env suite (designed array_oob failure + pre-existing SMT encode warnings
only); JS env suite clean.
…hing Verification runs directly on SState built over the predicate-carrying memory (Combinators.Abstraction); the PState layer had nothing left to add. SState now implements the State.S members that previously raised in pure symbolic execution — evaluate_slcmd, run_spec/run_par_spec, match_invariant, frame_on, produce/produce_posts/match_assertion, try_recovering — through an internal Matcher.Make instantiation (made possible by the MatchableState narrowing), and gains the pred-action shim on execute_action and the unfold-on-assume automation. The latter is gated on verification or bi-abduction mode so plain wpst memories never receive the reserved recover action; in symbolic mode there are no predicates to unfold anyway. Consumers are rewired to plain SState.S: Verifier takes a single state parameter (and owns the postcondition `matches` check), Normaliser, BiState and Abductor retype their functors, and the transformers bi-abduction runner drops its PState wrappers. Gillian.Symbolic.PState is gone; Verifier.S renames SPState to State (and drops its redundant SState alias). Validation: dune test; wisl quicktests 127; Amazon C all specs (122.3s); Amazon JS all specs (9.49s); act sll.c 15 success / 0 error / 2 bug; C env suite (designed array_oob failure + pre-existing SMT encode warnings only); JS env suite clean.
… move to the interpreter Fold/Unfold/GUnfold/Package are executed by the (Abstraction-wrapped) memory, but three concerns around them need the store, the spec-var set, or state-wide simplification: evaluating the store-dependent sub-expressions, registering Unfold binders as spec-vars, and the post-action simplification. These lived in a predicate-aware shim on SState.execute_action (exec_pred_action_in_memory + a shadowing execute_action that decoded SLCmds via SLCmd.of_action) — making the state aware of predicates, which it should not be. Move all three into the interpreter's SL-command branch, which already decodes the command via SLCmd.to_action. The shim is deleted; SState.execute_action is now purely the core memory action executor and the state is predicate-unaware. No interface changes — State.S already exposes eval_expr/add_spec_vars/simplify. Evaluation is done on the structured SLCmd via SLCmd.map before to_action, so each argument is re-encoded into a fresh EList (never decayed into a literal list that SLCmd.of_action could not decode); Package arguments stay raw and Unfold/GUnfold keep the ~matching:true simplification, exactly as the shim did. Validation matrix all green (identical to baseline): dune test; quicktests 127; Amazon C all specs (124s); Amazon JS all specs (9.7s); act sll.c 15/0/2; C env (designed array_oob failure + pre-existing SMT Set warnings only); JS env clean.
Contributor
Author
|
I honestly don't know how you go at reviewing this |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Based on #390 and #388
Sorry i'm giving up on spliiting into PRs it's taking me too much time. I'm still splitting into adequate commits.
The predicate combinator is still, effectively, in the making, but I've had to do the following refactors so far (in addition to the big refactors in #380 #381 #382 #385 #386 #387 #388 and #390):