Repository navigation
fix(core, analyzer): Handle sequent instructions via summaries - #406
Merged
Merged
Conversation
Contributor
Author
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ummaries Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ly edges Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Adds InitialFactAp.concat(typeChecker, FinalFactAp.Delta): FinalFactAp?, grafting a per-statement summary delta under an initial access path (spec core/docs/sequent-statement-summaries.md §5). Tree builds an abstract-leaf node from the initial path and delegates to AccessTree.concat; automata wraps the initial graph as an AccessGraphFinalFactAp and delegates to its existing concat; cactus is a stub that errors (its initial fact does not support this yet). The automata "node delta is grafted under the initial path" case compares by structural equals rather than toString: AccessGraph's merge-based concat path allocates node ids differently from a sequential prependAccessor chain, so two structurally identical graphs can render with different (but valid) internal numbering. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Introduce JIRStatementSummary, translating each JVM statement once into edges InitialFactAp -> InitialFactAp? (null = kill edge that keeps the refinement of `from`) plus per-base declared-type filters, per spec §3 in core/docs/sequent-statement-summaries.md. Adds the forEachAliasPathAtStatement alias-path helper it consumes. Not yet wired into JIRMethodSequentFlowFunction (next task). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
A field read x = y.f no longer maps y to alias paths based on the written local x, which the statement overwrites. The b-strict-prefix-of-c composition case is removed: the second transfer is always a move from an accessor-less temporary, so it never arises. The sequent flow function cache reference is volatile. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… the path AccessPath.concat with a node delta now prepends the initial path accessors onto the delta node with the AccessTree prepend operation instead of concatenating the delta onto an abstract path tree. An empty delta still yields the abstract path node annotated with the delta deep exclusion. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ition
The self-read case (x = x.f) has a fixed edge shape, x/{f} -> kill and
x.f -> x plus aliases of the rest, so the pattern/transfer composition
machinery is replaced by direct edge construction on InitialFactAp.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…aviour Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Saloed
force-pushed
the
saloed/sequent-summaries
branch
from
September 30, 2026 11:14
a34edcf to
2ec3f3b
Compare
…aries - The sequent flow function emits every fact through one propagateFact callback; propagate and propagateExitFact extend the result set, so the unchanged, side-effect and refinement-specific callbacks are gone. - A fact-to-fact edge takes its initial exclusions from the emitted fact, so initial and final exclusions always match; a Universe fact is emitted as zero-to-fact. - JIRStatementSummary stores one BaseTransfer (edges + type filters, as arrays) per touched base, found by linear scan, instead of maps. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
JIRMethodSequentPrecondition no longer re-implements moves, field reads, field writes and alias un-application: JIRStatementSummary.buildReversed swaps the forward edges (exclusions move to the matched side, kill edges are dropped, alias-only bases keep an identity edge) and a precondition is to.concat(fact.delta(from)) with the fact's exclusions. InitialFactAp gets a delta operation against another initial fact (tree and automata). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Alias targets get an identity edge in the forward summary, so every edge target is a touched base and reversed() only swaps edges (no ApManager, no synthetic identity). buildReversed is removed; the precondition uses build(...).reversed(). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
For y.f = x with an alias path a.p of y, the summary splits a along a.p.f
(a/{p1} -> a, ..., a.p/{f} -> a.p), keeps the written field weak
(a.p.f -> a.p.f, may-alias) and adds x -> a.p.f, instead of a blanket a -> a
identity plus y/{f} -> a.p. Reversal stays a pure swap. Pinned by an
AliasSampleTest case with real alias analysis.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ersed The builder records the survival of alias targets (A -> A at a read; the split along the alias path and the weak written field at a write) as backward-only edges. build omits them, since an untouched alias base passes forward as Unchanged; buildReversed includes them, so the reversed summary has no spurious kills. With different edge sets reversing is no longer an involution, so the reversed() operation is replaced by buildReversed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ses at reads The statement summary builder takes keepAliasPropagationEdges and produces or skips the survival edges of the aliased location at a field write while generating: build omits them, buildReversed keeps them and swaps all edges. Field reads change no memory, so they no longer emit alias edges. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…edges Forward edges are unique and the swap is injective, so reversed edges cannot repeat. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
StatementSummary (edges, forward transfer, backward preconditions) and StatementSummaryBuilder (move/read/write primitives, alias propagation edges, build/buildReversed) now live in org.opentaint.dataflow.ap.ifds.summary so other languages can reuse them. JIRStatementSummary is reduced to the JVM statement translation onto the builder; the sequent flow function and precondition delegate to StatementSummary.transfer / preconditions. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…summaries GoStatementSummary translates Go statements into StatementSummaryBuilder primitives (move/read/write with alias paths). The Go sequent flow function applies the summary per fact with the JVM emission rules and is cached per statement in GoMethodAnalysisContext; the precondition uses the reversed summary instead of per-statement precondition code and the alias loop. A fact whose base only the reversed summary touches (alias propagation edges) is answered with Unchanged plus the preconditions on other bases, matching the forward Unchanged: otherwise the trace edge search stops at a statement where no edge is stored for the fact (structCopy003T). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The reversed statement summary keeps the alias propagation edges, so a base that the forward summary does not touch (an alias base of a field write) got an explicit precondition naming its own survival. Forward that fact is Unchanged, and MethodAnalyzer does not store an edge propagated as Unchanged, while the trace resolver requires a stored edge for the fact after the statement before it follows an explicit precondition. The finding was then dropped as having no trace, on the JVM (may-alias through a conditional) as well as on Go (structCopy003T). The summary builder now records the bases the forward summary touches and marks the other bases of the reversed summary as unchanged forward. StatementSummary.sequentPreconditions answers such a base with Unchanged plus the preconditions on other bases; the JVM and Go sequent preconditions both use it, replacing the Go-only rule built from a second forward summary. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…lias propagation edges Pins that the reversed summary of an aliased field write drives backward abstraction refinement: a.* refines on box, a.box.* on value, and a.box.value.* reaches the written value, while the forward summary leaves the alias base untouched. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
… unchangedForward MethodSequentFlowFunction.transfer applies a statement summary forward and MethodSequentPrecondition.sequentPreconditions maps the reversed application to sequent preconditions; StatementSummary keeps only the data, find and the raw preconditionFacts. A base the forward summary does not touch answers Unchanged plus other-base preconditions, decided from the forward summary itself, so BaseTransfer#unchangedForward and the builder's forward-base tracking are removed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
StatementSummary is plain summary storage with find only; applying reversed edges to a fact (preconditionFacts) moves to MethodSequentPrecondition next to sequentPreconditions. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…Unchanged The engine stores no edge for a fact the forward flow function answers Unchanged, and the trace resolver follows an explicit precondition only through a stored edge. Pin, at a field read and at a field write through an alias (JVM writeThroughFieldAlias, Go a.box pointer alias), a table of (forward Unchanged, precondition Unchanged) per fact, and check that forward Unchanged implies precondition Unchanged without an explicit precondition naming the fact itself. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… test Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Saloed
marked this pull request as ready for review
September 30, 2026 19:49
Contributor
Author
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.