feat(core): Implement deep exclusions - #303
Open
misonijnik wants to merge 57 commits into
Open
Conversation
misonijnik
force-pushed
the
misonijnik/star-operator
branch
6 times, most recently
from
July 23, 2026 15:02
7590da4 to
f2ab56a
Compare
misonijnik
changed the title
misonijnik
force-pushed
the
misonijnik/star-operator
branch
from
July 23, 2026 15:04
f2ab56a to
5c833f4
Compare
misonijnik
force-pushed
the
misonijnik/star-operator
branch
2 times, most recently
from
July 23, 2026 16:07
e2ebaf3 to
2fd6b53
Compare
Saloed
force-pushed
the
misonijnik/star-operator
branch
from
July 25, 2026 11:24
2fd6b53 to
a712316
Compare
misonijnik
force-pushed
the
misonijnik/star-operator
branch
from
July 29, 2026 15:36
7bc46c5 to
f905a8d
Compare
A starred sanitizer records its must-clean claim as a deep exclusion on the fact it cleaned. Three defects kept that claim from surviving to the call site. `mergeAndIntersectDeep` stored the receiver's deep set in the new `Concrete` while computing the hash from the intersected one, so equal exclusion sets disagreed on `hashCode` and every hash-keyed storage misbehaved. The four lineage-join sites -- the automata, cactus and tree side-effect requirement storages, and the summary side-effect merge -- joined with `union`. `union` composes refinements, and a deep entry is not one, so it now states that invariant as a `check` and the join sites call `mergeAndIntersectDeep`: plain entries union, deep entries intersect, because the join of a cleaned and an uncleaned lineage is uncleaned. `MethodCallSummaryHandler` passed `null` as the initial-fact exclusion when applying a summary edge, leaving the initial fact without the deep entries just attached to the exit fact and breaking the single-exclusion edge invariant. Separately, a trailing any-field modifier in a serialized condition (`arg(0).*`) lowered to a plain `ContainsMarkLiteral` over an `AnyAccessor` query, which matches nothing: an abstract fact reports its read mismatch without an accessor, so the refinement that unfolds the fact never fires. It is now normalised into `ContainsMarkOnAnyField`, which the existing any-field lowering handles. Only a trailing modifier is normalised; `arg(0).*.f` keeps its accessor chain.
`DeepCleanSummaryAnalysisTest` conflates two things: whether a starred cleaner survives a summary, and whether it applies to the right field. The new suite holds the program, source, sink and read depth constant across each pair and varies only the cleaner position, which turns out to decide everything. Three positional pairs -- concrete `arg0`, `arg0.f`, `arg0.f.k` -- are green at every depth, including over an ABSTRACT any-field source, where the refinement splits the fact until the cleaner's path is concrete. A concrete clean is a node deletion, and the tree's branches keep `.raw` and `.val` apart through the summary merge. The starred pairs fail exactly where the answer depends on the star. Depth 1 is green and says nothing: the read is `p.val` itself, which the starred cleaner's base component removes as a concrete node. Depths 2 and 3 are the defect, and both fail in the false-positive direction -- their unsanitized siblings stay green, so no finding is lost. Four non-vacuity controls run each config with the cleaner deleted. They are red in Automata, which reports nothing on the `*CleanedFlow` entry points regardless of the cleaner, so all six of its `is silent` cases pass vacuously and are disabled with that as the reason rather than counted as coverage. The two `DeepCleanSummaryAnalysisTest` sibling cases are the same defect and get the same marking, pointing at the plan instead of at a storage-grouping stopgap that plan removes again. `:test` 700/0/19, `:opentaint-dataflow-core:opentaint-dataflow:test` 126/0/0.
…nnotation Behaviour-preserving first step of the field-sensitive deep exclusion plan (docs/superpowers/plans/2026-07-28-deep-exclusion-field-sensitivity.md, Task 2). An abstract tree node gains an optional AbstractionExclusions: the starred sanitizer's residual claim that a mark is removed from whatever later materializes below the node. Each mark carries the minimal relative depth of the claim -- depth 2 at the cleaned base itself (a direct mark-child is the base action's job, mirroring the flat mechanism's minPruneDepth=2), depth 1 anywhere deeper. The annotation is part of node identity (equals/hash/interning) and of the join: merging two lineages at the same node intersects their claims at the weaker depth, with "not abstract" as the identity. The merge-delta contract carries the JOINED state when it changed, so a consumer merging the delta converges (intersect is idempotent and absorbing). The workhorse create() gained the annotation parameter WITHOUT a default, so every construction site states its decision explicitly: transforms and filters preserve, removeAbstraction and concat drop (the claim dies with the abstraction whose growth it constrained), merges join. Nothing constructs a non-null annotation yet; both suites at baseline (126/0/0, 700/0/19) and :test wall-clock is +2s on 2m20s -- far under the plan's 15% gate. Serialization deliberately still drops the annotation (todo Task 5): none exist until the cleaner starts producing them in Task 3.
The starred sanitizer's clean, expressed structurally (Task 1 + the tree half of Task 3's mechanism; the engine does not call it yet): `FinalFactAp.deepClean(mark)` -- implemented by AccessTree, Unsupported by default so automata/cactus keep the legacy flat channel -- deletes every concrete `![m]` node strictly below the base (a direct mark-child stays: that is the base clean action's territory) and annotates each abstract node with the residual claim, from depth 2 at the base and depth 1 anywhere deeper. Enforcement lands in the one place content can materialize below an abstract node: `concatToLeafAbstractNodes` filters the incoming delta by the attach point's annotation before attaching. A sibling branch never meets the claim, which is the whole point. AbstractNodeExclusionTest pins the laws: deletion vs base-mark exemption, per-mark (not blanket) enforcement, depth-1 vs depth-2 semantics, branch confinement across a prepend, and the lineage join -- cleaned meets uncleaned and the claim dies; two cleaned lineages intersect; symmetric; idempotent. 13 new cases, dataflow unit suite 139/0/0.
…(tree) The engine now uses the structural deep clean (Task 3 of the field-sensitivity plan): on `base.[any]`, the cleaner dispatches to `FinalFactAp.deepClean` -- concrete `![m]` nodes below the base are deleted, abstract nodes carry the residual claim -- with the legacy flat `excludeDeep` channel kept only for representations that do not support it (automata, cactus) until Task 6. Making the claim survive to the caller took three seams the plan had not named, each found by measurement on `cleanOnlyFlow`: - the empty-delta summary application never calls `concat`: it runs through `SummaryExclusionRefinement`, which carried only the exclusion set. The refinement now carries the empty delta, and appliers concat it, so the caller's claim transfers onto the transited summary's exit abstraction -- the structural counterpart of the flat design's exclusion-set preservation. `AbstractionExclusions.union` accumulates the caller's claim with the callee's own (both hold for one lineage; marks union at the stronger depth); - `splitOnMatching` classified ANY abstract exit as an identity edge, and the id-edge storage rebuilds its exit as the initial fact's PLAIN abstraction -- silently dropping the claim. An annotated abstraction no longer matches; such edges keep their real exit tree in the merging storage, whose `mergeAdd` join applies the intersection law; - the tree deep sweeps (`delta()`'s removeAccessors pass, the deep half of `AccessPath.filter`) are deleted: tree exclusion sets no longer carry deep entries, and enforcement lives at the concat attach points. The four red acceptance cases are green and re-enabled: both deep starred reads in CleanerFieldSensitivityAnalysisTest and both sibling cases in DeepCleanSummaryAnalysisTest -- with their unsanitized siblings and all four non-vacuity controls still green, so the claim blocks only what the sanitizer cleaned. Two new law tests pin the transit. `:test` 700/0/15 (the four re-enabled cases account for 19->15), wall-clock unchanged; dataflow unit suite 141/0/0.
Task 4 of the field-sensitivity plan, scoped by its shim clause. The three tree-only exclusion merge sites (side-effect requirement storage, edge set, summary merging storage) switch from `mergeAndIntersectDeep` to `union`: tree exclusion sets are deep-free now that the starred clean is structural, and `union`'s check turns any leak of a flat deep entry into a loud failure instead of a silent semantics change. The operator itself, the deep accessors on ExclusionSet, and the deep lift in MethodCallSummaryHandler stay: automata and cactus still run the legacy flat channel, the two CommonFactSideEffectSummary sites are shared by all modes, and half-migrating those would change behavior this plan scopes to Task 6. Marked as legacy at the definition. Both suites green: unit 141/0/0, `:test` 700/0/15.
…ry store Task 5 of the field-sensitivity plan. The tree access-node serializer writes the abstraction's excluded-mark annotation (mask bit 4, then the two depth sets as accessor ids) and reads it back; a round-trip law test pins the sibling shape -- one annotated branch, one plain -- surviving persistence. Persisted method summaries gain a formatVersion property (2), checked on load. Entities written before the property existed read as null and never match -- rejected by version, not silently misread -- and are recomputed. The store-side write stamps the version on both the new-entity and the update paths. Deviation from the plan under its shim clause: the nine "DeepMarkExclusion must not appear in an access path" checks stay, because the flat channel is still live for automata/cactus until Task 6 and the checks guard exactly it. Unit suite 142/0/0, `:test` 700/0/15.
…e the claim Self-review cleanup of the field-sensitivity change. AbstractionExclusions loses `excludesAtDepth` and `afterOneAccessor` (written for anticipated call sites that never materialized) and narrows `allMarks`/ `fromDepth1`/`fromDepth2` to private -- the public surface is now exactly what the engine uses: `contains`, the two `addMark` builders, `join`, `union`, `create`. The `with(Companion)` wrappers at the annotate site become plain imported extensions, matching how AccessTree already imports its own companion members. Two defaulted parameters are made required. `SummaryExclusionRefinement. emptyDelta = null` as a default let a future construction site silently drop a caller's claim; the six zero/ND sites in MethodAnalyzer now state `emptyDelta = null` explicitly and own that no caller-side delta exists on their path. Same for `EmptyAccessTreeDelta.abstraction`. No behavior change: unit 142/0/0, `:test` 700/0/15.
…attachments Two transit seams lost the abstract-node excluded-mark annotation, both in the same shape: the cleaned fact keeps flowing INSIDE a summarized frame after the claim was established, and the machinery that continues it rebuilds the abstraction without the claim. Concat attachment. filterByAbstraction removed the claimed concrete marks from content attached below an annotated abstract node, but the attachment can itself contain abstract nodes -- there the continuation is not yet known, and the fact can still grow after the attach point's abstraction is consumed. The claim now outlives the attach point on those nodes: the attachment's root inherits the annotation verbatim, everything strictly below it takes each claimed mark from relative depth 1 (collapseToDepth1). Without this, a purely abstract delta -- the demand-refined `arg0.f.*` fact passing through the cleaning callee's summary -- came out unprotected, and the read one statement later re-materialized the cleaned mark: the in-helper clean-then-read false positive. Store partition. propagateAbstractFactWithFieldExcluded rebuilt the surviving abstract remainder of a field write via createAbstractAp(base, exclusions) -- a bare abstract node that drops everything the fact's abstraction carried. The new FinalFactAp.abstractPart() is the dual of removeAbstraction: no concrete children, abstraction kept. Cactus and automata carry the claim on the flat exclusion channel, which both implementations preserve, so their behaviour is unchanged. DeepCleanSummarySample gains the in-helper shapes (clean-then-read, the clean one summary deeper, clean plus a depth-2 constant store on the returned object) with a read-only control; all green on Tree with the control red-less. The two in-helper silent cases and their control are disabled in Automata for the documented intervening-call vacuity, matching CleanerFieldSensitivity.
misonijnik
force-pushed
the
misonijnik/star-operator
branch
from
July 30, 2026 07:34
4c45816 to
5361e30
Compare
Saloed
previously approved these changes
Jul 30, 2026
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
2 participants
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.