Fix/heap design#36
Draft
nils-loose wants to merge 33 commits into
Draft
Conversation
A reusable, multi-level test architecture for the symbolic-executor, with the
shadow-heap redesign as its first consumer. Levels are chosen at the lowest
faithful altitude per behavioral case.
Design:
- docs/test-architecture.md — 4-level architecture, oracle rules, @PendingFeature
red-first convention, seams, build order, per-case map.
- docs/heap-redesign-{plan,tests,testing-setup}.md — the behavioral case matrix.
Production seams (durable; the Phase-1 registry reimplements the same views):
- SymbolicTraceHandler.isSymbolicContextLoss()/isReferenceSemanticChange()
- JVMHeap.size()/values() + ShadowContext.heapSize()/heapLookup()/heapEntries()
L0 (value/structure unit): BaseValueSpec (prover SAT/UNSAT oracles) + ObjectIdentitySpec (O-4).
L1 (processor): executeBoundaryRecovery() fixture + HeapRecoveryV1Spec (V-1).
L2 (forked agent, solver.mode=PRINT): AgentRun + TraceObservation +
HeapRecoveryV1AgentSpec + ToLowerCaseTarget; opt-in `agentTest` Gradle task
(excluded from `test`).
Expected-red cases use @PendingFeature so the suite stays green and each red
flips to a build failure once its fix lands.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Adds the next behavioral cases against the harness: - O-5 (L0): colliding identity hashes — refs unequal (green) + heap must not merge distinct colliding objects (pending, G1). - V-2 (L1): new-object transform return does not alias the receiver (green); paired with V-1 in ValueRecoverySpec (renamed from HeapRecoveryV1Spec). - V-5/V-6/V-9 (L0, ValueSemanticsSpec): copy-ctor keeps phi, interned-literal reuse, concrete grounding (all green). - F-1/F-2 (L1, FlagPolicySpec): context-loss flag fires iff symbolic data flows into the unmodeled call (green). Stats: 33 tests, 29 passed, 4 pending (@PendingFeature: O-4, O-5, V-1 L1, V-1 L2), 0 failed. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Self-contained brief for the agent implementing G1/G2/etc.: the test contract (@PendingFeature reds as acceptance criteria), the red→goal mapping, bug locations, the invariants the harness depends on, run commands, and gotchas. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Re-key the shadow heap from System.identityHashCode (int) to the concrete object reference, via a Guava MapMaker().weakKeys() identity map. Reference identity is collision-free and gives one canonical shadow per concrete object, fixing the duplicate-wrapper / hash-collision / unregistered-object bugs and making ObjectValue.IF_ACMPEQ (this==o2) correct. - JVMHeap/ShadowContext: Object-keyed put/get/heapLookup; weak identity map. - visitGETVALUE_Object: heap calls keyed by inst.val (concrete ref); the int address retained only for NULL/de-intern/delegation/debug. - LDC_Object: thread the concrete constant and key recovery on it. - Declare Guava explicitly (was a transitive leak). - L1 fixture redesigned: this-return vs new-object via the concrete result object, not a fabricated int address. Acceptance: O-4/O-5 green (L0); V-2/F-1/F-2/V-5/V-6/V-9 green; V-1 stays pending (that is G2); L2 anchor green through the real agent. Reviewed by three independent agents (style/refactoring/correctness). Known residual: String keys self-pin (StringValue holds its key), so they do not evict - documented, no worse than the previous never-evicting map. Design + review: docs/heap-redesign-g1-design.md Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…y recovery) After G1 the heap is reference-keyed, but an unmodeled value-returning method whose result IS the receiver (e.g. String.toLowerCase() returning `this`) still re-binds the result to the receiver's symbolic formula via getFromHeap. Fix: at the unmodeled-invoke boundary, stop identity-recovering value types. - PlaceHolder: new ValueOrigin.UNMODELED_RETURN. - InvocationHandler: tag every unmodeled placeholder return with it, strictly after the context-loss recording (PlaceHolder uses identity equality). - Util.isValueType(Object): String + all 8 boxed wrappers. - visitGETVALUE_Object: for an UNMODELED_RETURN placeholder whose concrete result is a value type, concretize via createObjectValue (constant formula, no variables) and skip the heap entirely; non-value results fall through to G1 recovery. Not overwriting the heap preserves V-3 (a genuine symbolic-string round-trip still recovers its formula). Acceptance: V-1 green at L1 (ValueRecoverySpec) and L2 (HeapRecoveryV1AgentSpec, real agent); V-2/F-1/F-2/V-5/V-6/V-9/O-4/O-5 stay green; 0 pending. Converged after 1 design review + 3 independent post-impl reviews (style/refactoring/ correctness). Residual: result-round-trip re-aliasing is deferred to G3 (only identity-splitting closes it); it cannot cause a wrong verdict (VIOLATION is replay-witnessed; SAFE is downgraded by context loss). Design + review: docs/heap-redesign-g2-design.md Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ALUE When a tracked object is mutated inside unmodeled code, the shadow's concrete diverges from the real value at the next GETVALUE sync. Today the primitive divergence path hard-fails (SWATAssert.check(false, ...)) in every assertion- enabled mode - an out-of-band change crashes rather than being a recoverable soundness signal. Make the response configurable. - New ShadowDivergence policy (config `shadow.divergence`): CRASH (default; the original hard assert, for dev/CI bug catching) | FLAG (graceful: record symbolic_context_loss -> SAFE downgraded to UNKNOWN, adopt the observed concrete, continue; sound, recommended for production). - visitGETVALUE_primitive: gate the divergence assert on the policy; the adopt-observed recovery (previously dead after the always-failing assert) is now shared and reachable. Default CRASH = byte-for-byte prior behavior. - Reuses the existing symbolic_context_loss flag (already SAFE-downgrading) rather than a new flag. Scope: primitive GETVALUE path only. Deferred to G4a: the escape-aware DIFFERENTIATED policy (crash only on genuine executor desync, flag legitimate out-of-band) + the escape bit, so the escape set is built once with the purity whitelist; plus StringBuilder/object-ref/array divergence detectors. Acceptance: GoobDetectionSpec E-1 (FLAG detects: flag + re-ground, no crash) and E-2 (no false positive) green; heap+processor+agentTest all green; 0 pending. Converged after 1 design-review round + 3 independent post-impl reviews (style/refactoring/correctness). Design + review: docs/heap-redesign-goob-design.md Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…urns + SAFE-preserving exemption After G2, an unmodeled value-returning pure method's result is concretized, dropping the symbolic relationship to its inputs and downgrading SAFE. G4-full models such a method as a generic, axiom-free uninterpreted function over its inputs and makes that precision-preserving, so SAFE is preserved through the call. Mechanism (executor): - Whitelist of pure, deterministic, UNMODELED JDK methods (UFs/PureMethods; v1 starter: String.trim/strip) + descriptive UF naming pure_<Class>_<method>. - UFs/PureFunctionUF: per-context registry declaring one generic UF per signature (arg sorts from the input formulas), cached. - InvocationHandler.buildPureUF builds pure_<sig>(inputs) for a whitelisted call with a symbolic, value-typed input; carried on the UNMODELED_RETURN placeholder (PlaceHolder.recoveredFormula) and materialized at visitGETVALUE_Object as a StringValue(concrete=observed, formula=UF). v1: String returns only. SAFE preservation (both downgrades avoided for a modeled pure call): - precision_loss: DTOBuilder.isPrecisionLoss extracted to a testable predicate using a FormulaVisitor (visitRecursively + FunctionDeclarationKind.UF) that exempts pure_ UFs while keeping bespoke/axiomatized UFs and non-input vars lossy. Input detection uses exact JavaSMT term identity against the designated inputs (symbolicTrace.getInputs()), fixing String/array inputs that the [A-Z].*_[0-9].* regex rejected (a pre-existing limitation); the regex is kept as an additive backstop for recovery-created (non-designated) symbolic vars. - context_loss: a successfully UF-modeled whitelisted pure call no longer records context loss (sound: whitelist => pure/side-effect-free, return captured by the UF). Non-whitelisted calls (e.g. toLowerCase) still flag it. Trace prep for a future explorer-side decision: BranchDTO carries a per-branch precisionLoss flag (parsed by the explorer, not yet consumed); the aggregate (OR) still drives the current verdict, so the executor remains authoritative for now. Tests: PrecisionLossExemptionSpec (5 exemption controls, realistic java/lang/String_0 inputs), PureFunctionUFSpec U-4/U-5/U-6/U-soundness. 42 heap+processor + 2 L2 green; L2 anchor still flags non-whitelisted toLowerCase. Converged after 1 design-review round (2 iterations) + 3 post-impl reviews + a re-review of the two blocker fixes. Follow-up (noted): an L2 trim-to-branch anchor for end-to-end SAFE preservation. Design + review history: docs/heap-redesign-g4-design.md Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…isted pure trim Closes the noted L2 gap for G4 step 1. The real agent runs a @symbolic program that calls the whitelisted pure unmodeled String.trim() and branches on its result (TrimTarget). The emitted trace shows the relationship preserved (the branch references the input through pure_String_trim) and NEITHER soundness flag set (context-loss skipped because modeled; precision-loss exempt for the pure_ UF over a real input) - i.e. SAFE is genuinely preserved through the call, verified with real instrumentation, contrasting with the non-whitelisted toLowerCase anchor that still flags context loss. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…airs; explorer side documented Step 2 gives the generic UF teeth by accumulating observed ground facts across a testcase's runs. Per the user decision, the EXECUTOR side is implemented now and the explorer side (which touches the solve path + verdict logic, overlapping the upcoming explorer rework) is documented for that rework. Executor (this commit): for a whitelisted pure call, in addition to the result UF pure_<sig>(symbolic inputs), build the same (cached) UF over the CONSTANT observed inputs and carry it on the placeholder (PlaceHolder.observedApplication); at GETVALUE emit `addConstraint(pure_<sig>(const inputs) == observed output)` - a ground fact that only tightens the axiom-free UF (sound; one pair per run cannot self-contradict). It rides the existing UF channel (SymbolicTrace.getConstraints -> UFDTO -> Tree.ufs). v1: String inputs/returns. Explorer (documented, deferred): docs/heap-redesign-g4-step2-explorer-handoff.md specifies the 4 remaining items found by the 2-round design review - (1) inject the accumulated Tree.ufs at solve time (it is currently dead; Node.ufs is frozen per-node, so cross-run accumulation does not reach the solver), threaded through select_branch; (2) a structural contradiction guard in record_ufs; (3) a solve-time UNSAT->UNKNOWN backstop (verdict soundness); (4) an L3 test. Items 1-3 MUST land together (cross-run injection is what enables a contradictory set -> false SAFE), and raise the whitelist's purity bar to a soundness requirement. Tests: PureFunctionUFSpec U-7 (observed pair emitted + ground); 43 heap+processor + 3 L2 green (incl. the trim SAFE-preservation anchor). Design + review: heap-redesign-g4-design.md. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…g survey Audited java.lang for pure/deterministic/side-effect-free, String-returning, UNMODELED methods (5 parallel survey agents; whitelist is soundness-load-bearing so the bar is strict). Added the verified String-class entries to PureMethods.WHITELIST: stripLeading, stripTrailing (no-arg), substring(I), substring(II), repeat(I), replace(CC), indent(I) (arg-taking -> mixed-sort UFs). All confirmed unmodeled stubs in StringValue. Deliberately NOT added (documented): the boxed integral/boolean toString-family is already modeled (IntegerInvocation/etc.) so a UF would never fire (inert); cross-class static String returns (Float/Double/Character.toString, verified unmodeled + pure) are a backlog item pending static-invoke test support; Math/StrictMath have no String returns. Soundness traps catalogued (locale-dependent toLowerCase(), getInteger/ getBoolean property readers, Math.random, raw-bit/NaN, intern, arg-mutating, etc.). Full audited classification + backlog: docs/heap-redesign-g4-whitelist-survey.md. Tests: L2 SubstringTarget (arg-taking, mixed-sort UF -> branch references input via UF, both soundness flags clear, end-to-end SAFE preservation). 43 heap+processor + 4 L2 green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… register-only-non-constant G3 closes the value-type heap-key unsoundness at its source: a value returned from un-instrumented code can be interned/shared (a literal, a constant, a this-return), so the reference-keyed heap (G1) can collide two logically distinct values onto one cell. De-interning at the output boundary gives every produced value a fresh identity, making the reference key sound for value types and letting their shadow (a G4 UF for a whitelisted pure method) round-trip through untracked space. A1 = the String slice (boxed types are A2; the equality-handling review is B): - Part 1 (NoCacheMethodAdapter): wrap a String return `new String(result)` (null-guarded) iff the callee is NOT instrumented (!Util.shouldInstrument(owner)) - the boundary - minus an explicit literal skip-set for the symbolic-input/witness intrinsics (de/uzl/its/swat/** and org/sosy_lab/sv_benchmarks/Verifier; this is load-bearing, not delegated to shouldInstrument). Gated on the existing useStringInterning switch. - Part 2 (visitGETVALUE_Object, String sub-branch only): register the recovered shadow in the heap only when it is NON-CONSTANT (!extractVariablesAndUFs(formula).isEmpty()) - a constant is reconstructible from the observed concrete on round-trip, so registering it would only grow the self-pinning heap leak (a String is its own weak key); symbolic/ UF shadows must be registered to round-trip. Dropped the always-constant formula==null registration. Sound (verified): only object identity changes; `==`/refEquals is value-equality by class (independent of de-interning); VIOLATION is replay-witnessed; the only flag effect is Objects.equals(deInterned) -> VIOLATION->UNKNOWN (conservative). Converged after 2 rounds of 3 independent design auditors + 3 post-impl reviews. Tests: OutputDeInternSpec (L1) pins register-only-non-constant (symbolic->registered, constant->not). 45 heap+processor + 4 L2 green; the L2 trim/substring agent runs now exercise the de-intern wrap (loads, runs, UF survives, flags clear). The wrap is verified at instrument time by NoCacheTransformer's inline CheckClassAdapter. Tracked pre-merge gate (bounded, ~0 expected): measure the reference_semantic_change VIOLATION->UNKNOWN delta on the SV-COMP suite (no String Objects.equals in the suite). Design + full audit history: docs/heap-redesign-g3-design.md. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…wrapper types A1 de-interned un-instrumented String returns so the reference-keyed heap stays sound for that value type. A2 completes the value-type set: the six CACHED boxed wrappers in Util.deInternedClasses (Integer/Long/Short/Byte/Character/Boolean). Float/Double are deliberately excluded - uncached (no shared identity to break) and reference-equality, so de-interning them would be unsound. Part 1 (NoCacheMethodAdapter): A1's inline String wrap is refactored into deInternReturn(Type). Boxed wrappers have no copy constructor, so a boxed return is unbox+reboxed (new Integer(result.intValue()), etc.), null-guarded, via a per-type `Boxed` table. A local holds the unboxed primitive across the NEW - required for the category-2 long (DUP_X1/SWAP cannot reorder a wide value) and uniform across types via Type.getOpcode(ISTORE/ILOAD). Mirrors the existing valueOf(primitive) rewrites; those handle the (prim) overloads and return first, so there is no double-processing. Part 2 (visitGETVALUE_Object non-String branch): register-only-non-constant, scoped via Util.isDeInternedClass(inst.val) so it applies ONLY to the de-interned boxed types - mutable objects and Float/Double keep unconditional registration (sound identity key). A boxed wrapper carries its formula in the inner BoxedValue.getVal(), not the wrapper's own field, so the non-constant predicate reads the right source. Sound (reviewed): de-intern changes only identity; == on boxed is already value-equality via Util.shouldUseValueEquality (independent of A2); a constant boxed is reconstructible from inst.val on round-trip (ValueFactory.createObjectValue), so skipping its registration loses nothing. The boxed UF round-trip win is not yet active (whitelist "Future tier"); the soundness win (fresh identity -> no aliasing collision) holds regardless and the policy is forward-ready. Tests: OutputDeInternSpec (L1) - symbolic boxed registered, constant boxed not, and a mutable object ALWAYS registered (shared-path regression guard); BoxedDeInternAgentSpec (L2) - Integer (cat-1) + Long (cat-2 wide) returns load, verify, and run under the real agent. The category-2 long wrap (LSTORE/LLOAD, 2 slots) was verified valid via javap + CheckClassAdapter and executed. 48 heap+processor + 5 L2 green. 3 post-impl reviews (correctness/refactoring/style). Follow-up (out of scope): the pre-existing six valueOf(prim) rewrite blocks hard-code the same per-type data the `Boxed` table now holds; they could be driven from it so the two don't drift. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…quals -> root) De-interning (G3-A) gives value types fresh identities so the reference-keyed heap stays sound - but that fresh identity diverges from real JVM identity, so the prior mitigation modeled `==` by VALUE-equality (refEquals -> Objects.equals for de-interned classes) plus a conservative reference_semantic_change flag. That over-fired: a de-interned `==` (e.g. `s == "literal"`) was concretized AND flagged via BOTH symbolic-context-loss and reference-semantic-change -> spurious UNKNOWN, losing real SAFEs. G3-B models `==` by ORIGINAL identity instead, exactly: - Provenance (new): identity-keyed weak-key map de-interned-copy -> root(genuine canonical), collapsed at insert. Strong values keep a copy's canonical stable for the copy's lifetime (a fresh return's canonical is not independently reachable, so weak values could strand a live alias and flip a genuine `==` -> a GC-timing VIOLATION->SAFE). - UtilInstrumented.refEquals -> `shouldUseValueEquality(a,b) ? root(a)==root(b) : a==b` (reference on the originals, not Objects.equals). Two de-interned copies of the same interned literal / cached box / returned object share one canonical -> `==` matches the un-transformed program, exactly. - NoCacheMethodAdapter records provenance at every de-intern site: LDC (re-LDC the interned canonical after <init>), the six valueOf blocks (call the REAL valueOf via the raw delegate - NOT recursively rewritten - for the cached canonical; else valueOf(100)==valueOf(100) regresses true->false), and deInternReturn (restructured to keep the original in a local). - InvocationHandler IGNORED_INVOCATIONS += Util.shouldUseValueEquality + Provenance, so the stepped refEquals body fires no spurious context loss. Why empirically uniform (de-intern ALL, incl. literals): a String LITERAL can be the designated @symbolic input (confirmed: `test("seed")` -> the literal is symbolic), so it must be de-interned (distinct identity, registered, recoverable; no collision with a same-value plain literal). Sound: root carries real JVM identity (`root(a)==root(b)` is exact reference-`==`); concretizing is sound (reference `==` is per-path-concrete + VIOLATION is concretely witnessed). Scope: `==`/`!=` exact; identityHashCode/IdentityHashMap on de-interned values in un-instrumented code is an accepted, documented residual. Converged after 2 design-audit rounds + a uniform-model final pass (3 auditors each) + 3 post-impl reviews. Tests: ProvenanceRefEqualsSpec (L0, refEquals+root incl. boxed-cache + collapse-at-insert), StringRefEqAgentSpec (L2: de-interned `==` fires NEITHER flag - the over-firing fix, end to end). 53 L0/L1 + 6 L2 green. Follow-up (G3-B2, separable cleanup; the core already fixes the `==` over-firing because refEquals no longer reaches Objects.equals): delete the now-spurious reference_semantic_change flag + userDeInterned + the ObjectsInvocation block, across Java + explorer (SVCompDriver) + Groovy tests. And (out of scope) table-drive the six valueOf blocks off the `Boxed` enum. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ge flag + userDeInterned The G3-B core (59ed40d) made `==` exact via provenance and routed refEquals through root() instead of Objects.equals, so the `==` path no longer reaches the reference_semantic_change flag. Its only remaining firing site was explicit Objects.equals(deInterned,...) - which is value-equality and de-intern-invariant, so the flag there was spurious (only ever downgraded VIOLATION->UNKNOWN unnecessarily). This removes the dead conservatism across all three languages. Java: drop the ObjectsInvocation `instanceof StringValue` block (+ its now-unused imports), StringValue.userDeInterned (field + invokeInit assignment), SymbolicTraceHandler.record/ isReferenceSemanticChange, the SymbolicTrace field (lombok accessors go with it), and the TraceDTO field/ctor-param/assignment + the DTOBuilder ctor arg. symbolicContextLoss and symbolicPrecisionLoss are preserved (context-loss is still the load-bearing soundness flag). Explorer: delete the full chain - DataTransferObjects DTO field, ConstraintController parse + kwarg, ConstraintService param/docstring/add_trace arg, Database param + record call, Tree field + record_reference_semantic_change, and the SVCompDriver VIOLATION->UNKNOWN downgrade. pydantic v2 default extra='ignore' makes the DTO drop order-independent vs the Java side. Also targets/.../analysis/failures.py - the now-dead 'Found reference semantic change' log-grep stat category. Tests: TraceObservation field+parse, the executeBoundaryRecovery result-map key, and StringRefEqAgentSpec drops its !referenceSemanticChange assertion (flag gone) while keeping !symbolicContextLoss - which still validates the round-2 mechanism (the stepped refEquals body's IGNORED Provenance.root/shouldUseValueEquality suppress context loss). Sound: removing a VIOLATION->UNKNOWN downgrade can only reduce conservatism, never create a wrong verdict; the `==` path is now exact and the explicit-Objects.equals path never diverged. Converged via a 3-auditor proposal review (soundness / explorer-chain / test-impact+completeness; the completeness sweep added the failures.py + unused-import items). 53 L0/L1 + 6 L2 green; explorer verified by py_compile + chain-arity trace (no runnable explorer test in this env). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The class-name guard behind Util.formatClassName carried a
`&& !className.startsWith("L")` clause intended to catch object type
descriptors (Lxxx;). But object descriptors always end in ';', which the
existing ';' clause already rejects, so the term was redundant. Because it
keys on the first character it spuriously rejected every legitimate class
name beginning with 'L' (default-package targets/benchmarks such as
LitSymTarget), tripping SWATAssert and crashing instrumentation.
Drop the term and clarify the message. The guard still rejects every real
descriptor: object (';'), method ('('/')'); arrays are skipped via the
existing '[' early-return. Add UtilClassNameSpec (L0) pinning both halves
of the contract.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… enum The six near-identical valueOf-rewrite blocks in visitMethodInsn each hardcoded owner, the valueOf/ctor descriptors, the load/store opcodes and the primitive Type - all of which the Boxed enum already carried for deInternReturn. Two parallel tables to keep in sync by hand (drift risk). Make Boxed the single source of truth: store one primDescriptor per wrapper and derive boxedDescriptor/valueOfDescriptor/ctorDescriptor/ unboxDescriptor from it (primType stays explicit so short/byte/char keep their int-category stack slot). The six blocks collapse to one enum-driven path (forValueOf -> rewriteValueOf), and the rebox sequence shared with deInternReturn's boxed branch is extracted into reboxFreshFromPrimitive. Behavior-preserving: emitted bytecode is instruction- and descriptor-identical (independently reviewed); adding a 7th wrapper is now a one-line enum row. Broaden BoxedReturnTarget/BoxedDeInternAgentSpec (L2) to drive the valueOf rewrite for all six wrappers through the JVM verifier (previously only Integer+Long were exercised), closing the coverage gap on the derived short/byte/char descriptors. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
scripts/jmethod.py extracts method/class source from the active JDK's lib/src.zip (version-exact, offline): a method/ctor signature index, the brace-matched full source of any method's overloads, its callees, or a field declaration. SKILL.md documents it plus the six-point purity rubric for deciding PureMethods.WHITELIST (G4) eligibility - the tooling for the broad whitelist audit. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The G4 purity whitelist modeled a pure unmodeled method's result as a generic axiom-free UF (pure_<sig>(inputs)) only for String returns. Extend it to all primitive returns so numeric/boolean/char pure methods (Math.*, Character predicates/conversions, etc.) preserve precision instead of losing symbolic context. - InvocationHandler.buildPureUF: drop the String-only gate; pureUFReturnType maps the return descriptor to the exact shadow sort (bool->Boolean, byte/short/char/int/long->bitvector 8/16/16/32/64, float/double->FP single/double, String->String) and declares the UF with it. The step-2 observed pair stays gated to String returns (the only path with a recovery-side consumer); String behavior is unchanged. - ValueFactory: createNumericalValue(type, concrete, formula) overload constructs each primitive value carrying a symbolic formula. - visitGETVALUE_primitive: an UNMODELED_RETURN placeholder carrying a UF result installs it as the value's formula (concrete = observed), mirroring the String path; no MAKE_SYMBOLIC (the UF already carries the inputs). - PureMethods: hand-audited primitive starter set (Math.floorDiv/floorMod/ cbrt, Float.intBitsToFloat, Character.toLowerCase/isDigit) - each verified unmodeled + side-effect-free; covers int/long/double/float/char/boolean. Soundness reviewed (axiom-free UF over-approximates any deterministic function; FP congruence is structural over arg terms, the safe direction). Tests: PureUFPrimitiveRecoverySpec (L0, all 8 sorts incl. short/byte) and PureFunctionPrimitiveAgentSpec (L2, 6 sorts end-to-end, UFs ride branches, no context/precision loss). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…g audit Scale PureMethods.WHITELIST from the starter set to 240 entries using the agent-driven purity audit (jdk-source skill rubric, one agent per class). Non-String (214): pure, deterministic, side-effect-free, UNMODELED methods from Math/StrictMath (transcendentals, exact arithmetic, floorDiv/Mod, fma, bit ops), Character (predicates/conversions), Double/Float (bits, parse, toString, max/min/sum where unmodeled), Byte/Integer (hashCode/bitCount), and Objects (checkIndex/checkFromToIndex/checkFromIndexSize). The audit correctly rejected the only genuinely-impure candidates (Math.random; Character.getName/codePointOf, which do uniName.dat I/O). StrictMath routes to MathInvocation, so its modeled names (sin/cos/sqrt/round/abs/max/min) are excluded as inert. String (26): the StringValue stubs (invokeX returning PlaceHolder) that are genuinely unmodeled, determined empirically since the StringValue model is method-by-method (invokeTrim is a stub, invokeSubstring is a real model). Soundness-filtered to drop locale-dependent (no-arg toLowerCase/toUpperCase), identity (intern), and toString. Drops 3 inert prior entries (substring x2, replace) that are actually modeled - behaviour-neutral. All entries are sound as axiom-free UFs (per the primitive-return soundness review). Verified across every owner + return sort + the String->float parse bridge; WhitelistAuditAgentSpec + StringWhitelistAgentSpec (L2). 9 L2 + 71 L0/L1 green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
ShadowContext.heapLookup/heapEntries and JVMHeap.values() had no callers; only heapSize() is used (by the identity-registry tests). Drop them and the now-unused Collection import. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Strip all @see annotations and the spock.lang.See imports from the heap specs. Linking tests to design docs is worthwhile but needs a considered scheme; removing the ad-hoc links for now. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add docs/heap-tracking.md: a plain-language, present-tense reference for how the executor tracks values and objects (registry, boundary recovery, out-of-band detection, de-interning and reference equality, pure-function UFs, soundness flags) with code pointers and the two not-yet-implemented mechanisms. Delete the point-in-time process docs it supersedes. Fix stale references to the removed reference-semantic-change flag and heap accessors in test-architecture.md, the swat-test skill, and the sv-comp failure analyzer. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Remove development-phase labels (G1-G4, step 2, v1), design-doc references, and coined internal terms from comments and Javadoc across the heap/value-tracking sources. Comments now describe present behavior; no logic changes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Rewrite Spock feature-method names and comments to plain-English behavior descriptions, dropping internal case identifiers (O-/V-/F-/E-/D-/U-) and phase labels. Rename GoobDetectionSpec -> OutOfBandDetectionSpec and HeapRecoveryV1AgentSpec -> HeapRecoveryAgentSpec. No assertion or logic changes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Delete the point-in-time per-phase design docs now consolidated into docs/heap-tracking.md. Rewrite test-architecture.md and the swat-test/jdk-source skills to drop case IDs, phase labels, and @see conventions, and repoint doc links at heap-tracking.md. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
refEquals routes through value equality when EITHER operand is de-interned (not both), and a user-constructed new String/new Integer is never rooted, so it compares unequal to any other instance (matching the real JVM). Replaces the stale residual note that described the earlier value-equality implementation. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ainers When an unmodeled instance method returns a distinct, already-tracked immutable value (e.g. a String or boxed primitive retrieved from a Map/List), recover its registered shadow instead of concretizing, so the value keeps its symbolic formula and the solver can still reason about it. Restricted to the closed set of immutable value types (String + the eight boxed wrappers) since a mutable Number could have drifted, and gated on the return being distinct from the receiver's own shadow so a method returning `this` (e.g. toLowerCase) still concretizes. The receiver is carried on the UNMODELED_RETURN placeholder for the distinctness check; a defensive concrete-equality check falls back to concretize on mismatch. Recovery fires only for values already registered in the heap. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Update the boundary-recovery section to reflect that a distinct, already-tracked immutable value returned from an unmodeled method (e.g. from a Map/List) is now recovered rather than blanket-concretized, while a this-return still concretizes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…verified A branch solved via an uninterpreted pure_ UF can diverge on concrete replay: the predicted branch is never taken because the solver cannot drive the UF to the required value. The divergence was detected but ignored, and the driver concluded SAFE - an unsound false SAFE (autostub compareToIgnoreCase scored -32). Track diverged/unverified branches and, before concluding SAFE, downgrade to UNKNOWN if any remain. compareToIgnoreCase: -32 -> 0 (UNKNOWN); Boolean.compare violation and toLowerCase UNKNOWN unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Re-open a branch that diverged on concrete replay (drop its stored solution so the search returns it again) and retry up to MAX_BRANCH_ATTEMPTS, preferring less-tried branches so a repeatedly-diverging one does not starve the rest; after the cap it is abandoned as unverified, forcing UNKNOWN (piece-1 backstop). Key the unverified/attempt bookkeeping on node gid (not the bytecode iid, which is not unique per node). Bounded and terminating; the divergence is now a handled warning, not a spurious SWAT-assertion error. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…d inject them Emit the ground pair pure_<sig>(constant inputs) == observed output for every whitelisted pure return, not just String: buildPureUF builds constant inputs for all value-type sorts and the observed application for any return sort; visitGETVALUE_primitive asserts it via PureFunctionUF.equalConstant (bitvector/boolean/FP/string). The explorer injects the accumulated per-testcase pairs (Tree.ufs) at solve time, so re-solving a diverged branch is forced to pick a different input. Pairs are true observed facts (sound). autostub compareToIgnoreCase: each retry now explores a distinct input before abandoning -> UNKNOWN; whitelist L2 tests + Boolean.compare/toLowerCase unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Operational recipe for parallel scoring and single/debug runs, the debug workflow, result interpretation, the per-testcase wall-clock cap, and key files. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Bound local scoring runs so a diverging/hanging testcase cannot stall the batch; the process group is SIGKILLed on expiry (outside the SWAT run) and the testcase scores 0 (TIMEOUT). The competition-infra wrapper (run_swat.py) is unaffected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
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.
No description provided.