feat(analyzer): Add $* star operator - #313
Open
misonijnik wants to merge 66 commits into
Open
Conversation
misonijnik
force-pushed
the
misonijnik/2-star
branch
2 times, most recently
from
July 29, 2026 21:09
bdee182 to
76bd03e
Compare
…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.
…peline Accepts a starred metavar in expression, formal-parameter and declaration positions, and carries the star flag on IsMetavar through the automata pipeline, including across the remapping done by string-concat elimination. Parsing only -- no taint semantics are attached yet.
A starred metavar denotes whole-object taint, so:
- a starred source assigns both the value and the any-field position;
- a starred sanitizer cleans both, keeping the field-clean anchored on the
value base;
- a starred sink is satisfied by a mark on the value OR on any field.
The sink side needs a serialized form of the existing ContainsMarkOnAnyField
condition so a rule can express it, added here along with the `withAnyField`
position helper.
Covered by propagator, pattern-not and end-to-end source/sink/sanitizer
field-taint samples.
…esolution Parses the starred metavar on plain and typed Go metavars, threads it through the Go taint emitter, and implements the any-field mark check on the Go condition builder. Backs the any-field position with a real resolver on the source, pass and clean paths -- memoized, since any-field evaluation sits on a hot path -- and adds the any-accessor variant of the sanitizer clean on the Go side. Also completes the Java surface: the star threads through assignment-LHS and typed declarations, the any-field shadow tree collapses via an AnyFieldLift decorator, an unsupported starred / pattern-not coincidence is diagnosed rather than silently mis-lowered, and the serialized any-field condition gets its own key so it round-trips independently of the depth-1 mark check.
Moves the star from a suffix to a prefix. The suffix form was ambiguous with multiplication -- `$X * y` and `$X*y` are ordinary multiplication -- so the prefix spelling is the one the parser can accept unambiguously. Also fixes three clean-path defects the starred sanitizers expose: concrete nested-field taint left behind underneath an any-field position, the sanitizer cleaning only Result instead of its focus position, and the clean not being applied at call-to-start for resolved calls.
Adds the deep-nesting matrix for Java and Go, crossing interprocedural depth with field depth, plus the state-var mechanism the Go side needs to express it via ClassStatic positions. Replaces the runtime array-element sink reader with an any-field condition, and keeps $X and $*X distinct in the constraint solver. The matrix also pins the remaining whole-object source vs value-sanitizer false positives, so the surviving gaps are characterized rather than silent.
Exercises the DeepMarkExclusion machinery through the querylang surface now that the star syntax can express it: the composition boundary of deep exclusions, mixed deep and plain exclusion sanitizers, a starred clean followed by a constant field store, and field-level overwrite after the clean. Unparks the StarDeepSink depth-5 case and accepts a starred metavar in a typed expression position.
misonijnik
force-pushed
the
misonijnik/2-star
branch
from
July 30, 2026 07:42
76bd03e to
d5139a1
Compare
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.