Repository navigation
Conversation
JIRMethodAnalysisContext only needs the analysis phase and the manager params from its manager. Introduce the JIRAnalysisManagerBase interface exposing exactly those, implement it in JIRAnalysisManager, and make the context open with an overridable methodCallFactMapper so a second (backward) manager can reuse the context. Forward behaviour is unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit c802d1143d5cc49a2c981ecae301cb2525e8a038)
Add package org.opentaint.dataflow.jvm.ap.ifds.backward: a second TaintAnalysisManager that runs the unchanged IFDS engine over the reversed application graph, where facts are sink demands. - JIRBackwardAnalysisManager mirrors JIRAnalysisManager (params, phase selection via SelectedTaintRulesProvider, relevant rule ids, context reset) and reaches forward-only components (alias analysis, variable reachability, JApplicationGraph downcast) through graph.reversed. Alias analysis is seeded with the forward method entry. isReachable is always true; valid exit facts are Argument/This/ClassStatic only. - JIRBackwardMethodCallFactMapper: call->start maps the result variable to Return only, otherwise forward mapping; exit->return maps callee Argument/This back to the caller arguments/receiver. - Entry-point resolver drops the exceptional exit; start FF, summary handler, side-effect handler and trivial precondition objects. - JIRBackwardTaintRules: sink rules -> demand seeds from the positive mark literals of the rewritten condition, and demand -> source matches (call, method exit, method entry, static field), shared by the call and sequent flow functions. - JIRBackwardFindingTracker: thread-safe source findings, unconditional sinks and demand seeds, exposed by the manager. - Sequent and call flow functions are Phase 1 stubs: correct for the zero fact (zero propagation, sink seeds, unconditional sinks), Unchanged for facts. TaintSourceActionPreconditionEvaluator now takes the FactReader interface so a FinalFactReader demand can be matched and its abstraction refinement recorded; the trace preconditions keep passing InitialFactReader, so their behaviour is unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 3a8f98356d6dda3894508203fbefb2eb88a47770)
BackwardAnalysisTest builds the single-exit JIR graph, reverses it and drives JIRBackwardAnalysisManager through TaintAnalysisUnitRunnerManager directly (FullScan, reset ApManager, run), returning the tracker records, analysed methods and per-statement facts. It provides assertSourceReached and assertNoSourceReached. AnalysisTest exposes findEntryPoint, createRulesProvider, createAnalysisGraph and SingleLocationUnit to subclasses instead of keeping them inline in runAnalysis; forward runs are unchanged. BackwardSmokeTest on SimpleDataFlowSample checks that the sink call seeds one demand on the caller local and that every callee is entered from its exit, and that a method-entry sink seeded at JMethodEnterInst is mapped back to the caller argument through the summary. The source-reach assertion is disabled until the phase 2 flow functions land. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 38aeff474440a3cd751c43fb52f67a367077338b)
Add the observed reversed-graph behaviour, manager and context details, mapper type checks, corrections found against the code (resolution failure has no start base in propagateUnresolvedCallFact, source evaluator generalised to FactReader, pass-through precondition evaluator cannot read FinalFactAp demands), the JIRBackwardTaintRules helper API, tracker API, new known limitations and the phase 1 status/test harness. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 7cf71a8e1dc4ebe4d5f8c61535609727f6054563)
TaintPassActionInverseEvaluator is a FinalFactAp sibling of TaintPassActionEvaluator: a demand on a pass rule's 'to' position becomes a demand on its 'from' position (CopyAllMarks rebuilds the delta after 'to' at 'from', CopyMark maps to·M·$ to from·M·$). Reads go through FinalFactReader, so abstract demands are refined exactly like forward facts. The trace-side TaintPassActionPreconditionEvaluator is unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit e625803e212ebfd7d6b26ea7f69f96e3ad386aa9)
Replaces the Phase 1 stub for facts: - relevance check and call-to-start through the backward fact mapper with the real result variable; - source matches recorded as findings, conditional sources emit their positive mark literals as new demands; - cleaners are inverted by running the forward cleaner on the demand itself: removed alternatives are dropped, surviving demands continue; - constructors keep the demand call-to-return, as forward; - resolution failure overrides the three hooks to know the start base: non Return demands are kept, pass rules (plus defaultGetModel) are inverted with TaintPassActionInverseEvaluator, the generated demands are filtered by the call's cleaners and mapped callee to caller; - every reader refinement is merged into the emitted edges and reported via addSideEffectRequirement, like forward. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 2416b6ea38483e63e3b5fc7690dc59382c1e7d92)
BackwardCallSample holds call-only flows (no sequent FF needed): direct sink(source()), library pass-through with default and user CopyMark rules, a demand through a callee argument heap effect, argument/result/receiver cleaners, a conditional source and negative cases. The callee return-value flow needs the sequent FF and is disabled. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 6425cac27cc8c22888b51c0a0e8fa097965d5a23)
Records cleaner inversion (forward cleaner applied to the demand), pass inversion (TaintPassActionInverseEvaluator, mark conditions treated as satisfied), refinement plumbing, resolution-failure overrides, documented omissions and the Phase 2a test coverage. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 04f8ca713277779180b020b68e40f6cdb470b2fb)
Replace the Phase 1 fact-level stub with the full statement semantics of spec section 4: assignments (copy/cast with forward type filters, field, static and array reads by prepending, binary operands, kill on const/new/ other), strong field and two-level static writes with forward-identical abstraction splitting, weak array writes, return/throw rebasing, and may-alias weak moves for field and array writes using the alias state before the statement. Rules: exit sources are matched at return before Return is rebased, static-field sources at x = C.f, entry sources at JMethodEnterInst; reader refinements from abstract demands are propagated into the emitted edges. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 8d00202797cb9ff31b6b26c5710ee4ddf1fb7047)
BackwardSequentFlowTest runs the backward engine end to end with an entry-point source and a call sink, so the demand only crosses sequent statements: copies, casts, fields, arrays, statics, binary ops, self-referential forms, aliases through a heap indirection, branches, loops and a method-exit sink, each with negative counterparts. BackwardSequentFlowFunctionTest checks the exact Sequent sets for abstract FactToFact demands (refinement on field, element and static accessors), concrete ZeroToFact demands and exit-source matching at return. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 1262dbaface5061e4716aaa423e5a5c34bec098b)
Add section 4.1 (callback structure, type filters, constants, write procedures, alias direction and translation, observed JIR shapes) and 4.2 (status and test inventory) to the backward analysis spec. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 566119fa4ab8dbd881e5b28063c2db4c6f28f112)
The callee-return and smoke source-reach cases now pass with the sequent and call flow functions merged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit bfac792fa2002fdf6d7a8e5907e018c425a1be1c)
ContainsMarkOnAnyField (a ContainsMark on a position with the AnyField modifier) produced no demand, so every AnyField sink was silent unless it also had a BaseOnly alternative whose mark sat at the root. Forward matches such a literal when the fact carries the mark at any path below the position, including the position itself. The demand is now seeded as position.M and position.[any].M, which the flow functions move and match like any other demand. Source condition demands use the same expansion. Found by the backward/forward differential test (CleanerDslControlFlow sequentialMarks, cleanThenRetain; CleanerDsl helper controls and recursive any-only source). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit b26cbd4845e10fb45f43311370066435a6f8f6cb)
Forward aliases the facts a call creates (source results, pass-through results, summary facts with a memory effect) through forEachAliasAfterCallStatement: a fact on a call local b is copied to every alias z.g1..gn of b that persists through the call. Backward ignored this, so a demand on z after the call never reached the call's effect on b. For StringBuilder chains (sb.append(x).append(b)) the demand on sb never became a demand on the intermediate receiver. The call flow function now also processes, for every call local b (receiver, arguments, result) and every alias of b persisting through the call whose base is the demand's base, the demand read through the alias accessors and rebased to b. The derived demand goes through the same source matching, cleaners and call-to-start as the original one, as JIRMethodCallPrecondition does for aliased trace facts. Reading through an abstract demand refines it via the fact reader. A demand irrelevant to the call is still kept unchanged. Found by the backward/forward differential test (JavaDataFlowReachabilityTest chainedAppend, namedReturn). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 05bdbd0e6012ab997ce0e15c5dae03abeea5e3c4)
BackwardForwardDifferentialTest replays every case of JavaDataFlowReachabilityTest, KotlinDataFlowReachabilityTest, MultiReturnDataFlowTest, CleanerDslAnalysisTest, CleanerDslControlFlowAnalysisTest and CleanerFieldSensitivityAnalysisTest (re-declared in ForwardSuiteCases, with the same useDefaultConfig and unroll settings as the forward suite). Forward runs once per case on the full config. Backward findings name a mark, not a sink, so each case's sinks are split into groups whose demanded marks are pairwise distinct and backward runs once per group: the marks it reports must equal the marks of the group's sinks that forward reached. Tree mode additionally checks forward against the forward suite's expectation. Accepted divergences carry their mechanism in the table: lambdaCaptureFlow (lambda resolution is forward-only) and the star-path/Exact-cleaner interaction, evidenced both ways by CleanerStarDualSample. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit a842d1cf4eb68008d54f7cd1fffb5d718205968c)
Forward reports at most one vulnerability per sink statement across the rules of a config, so a group of sinks sharing a call (the cleaner DSL checkpoints) under-reports in the modes where several rules fire there. The forward reference is now one isolated forward run per sink rule, as for the route-oracle benchmark. Automata, BaseOnly and BaseOnlyField subclasses compare backward with forward in the same mode; a rule also agrees when backward matches the forward suite's Tree-verified expectation, since forward in these modes has its own mode-specific results (Automata drops the flatMap and recursive any-only flows its IFDS facts reach; BaseOnlyField forward over-reports 300 matrix groups). Tree stays strict. Divergences now pin the backward value and are checked to still differ from the reference, so a stale entry fails. New entries: Automata keeps the star demand through an Exact cleaner (root-level mark FP), BaseOnlyField seeds root demands with an open field tail (cleaner/field-write FP), and the forward-suite flatMap known false negative that backward reports. Cactus is not run: forward cannot execute there (AccessCactus.equalTo is not implemented). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 990739bea0821027c0580f19456099428a8bfe51)
New section 11: the replay harness (sink groups, per-rule forward runs, mode references, self-checking divergence pins, the star/cleaner evidence sample), the Tree results (609 agree, 11 fixed, 8 accepted groups), the two fixes, the star path vs Exact cleaner mechanism, the access-path mode matrix for the existing backward suite and the differential (Automata, BaseOnly, BaseOnlyField, plus a Cactus record against the suite expectation), and forward observations made on the way. Sections 5, 6a and 9 are updated for the call-site aliases and the any-field seeds. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 8414c2cf2d60c18f7a5b377d84ebd86a9e2e03c5)
The backward entry-point resolver dropped JMethodExitExceptionalInst, and the single-exit graph links throws only to it, so statements that lead only to a throw (a branch ending in a throw, a rethrowing catch handler, a callee that always throws) were never analysed. Forward analyses them and reports sinks there; it only ignores summaries at the exceptional exit. Keep every reversed entry point. An exceptional entry point starts only the Zero fact: the start flow function drops caller demands there, since forward never returns a callee fact to its caller along an exception. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit b20cc7ae30e28b708132a41186c00230e3ba90e5)
callSiteAliasDemands required the demand base to be a local variable, so a demand rooted at an argument, `this` or a static field never reached the call local aliasing it (`b = h.sb; b.append(p); sink(h.sb...)` with `h` a parameter). Forward's forEachAliasAfterCallStatement only needs the call local to be a local; the alias base may be a local, an argument, `this` or ClassStatic, and only constant alias bases are skipped, which a demand never has. Drop the restriction. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 79a816b875df3564f23805e637d2b8473312181f)
…emands Forward applies entry-point sources on the zero fact of every analysed method and, at the exit, dropArgumentsLocalTaintMarks removes the marks assigned on method enter from zero-to-fact facts rooted at an argument or `this`. Only a mark directly at the root is removed (TaintMarkRemover accepts any path below a field), so `arg1.sb.M` still reaches the caller while `arg0.M` does not. Backward matched entry sources on every demand at JMethodEnterInst, including a caller's demand on the argument itself, and so reported `entryHandler(s); sink(s)` with the entry rule on entryHandler, which forward does not. Record an entry-source finding unless the edge's initial fact (the caller demand at the exit) is rooted at an argument or `this` and starts with a mark assigned by an entry rule of the method. Zero-to-fact edges and initial Return / ClassStatic bases always record. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit a399b3107a09f4bee208905cfeca6fa926472f04)
A source match on an abstract demand only refines it (the reader records the exclusion, the concrete initial fact is created by the engine later). The refinement travelled on the emitted demands, so when nothing was emitted after the match, e.g. an exit source on `return "c"` or a void return, it was lost and the concrete edge that records the finding never existed. Report it as a SideEffectRequirement on fact-to-fact edges, as the call flow function already does; zero and ND edges keep the can't-refine check. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit f2b6543e97cf5d1bbd28fbbf7da8b72a84b7e368)
JIRTaintAnalysisContext.handlePhase records the id of every rule queried in Prescan into relevantRuleIds, which later phases pass to TaintRulesProvider.selectRules. Forward queries sinks and sources on the zero fact, but backward matches sources only on demands, and Prescan has none, so no source id was recorded and a semgrep-backed provider (SemgrepRuleProvider.reduceTaint) would drop the taint rule in FullScan. On the zero fact in Prescan, query the call, method-exit, method-entry and static-field source rules, as forward does. Cleaners and pass rules are queried only on facts in both directions. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit bc4d5ee241bb68d4c4637a4901b0cde1aebd0ce3)
The backward summary handler used the default handleSummary, which never calls createSideEffectRequirement. Forward's JIRMethodCallSummaryHandler emits one whenever applying a summary refines the caller's initial fact, which is how the refinement reaches the caller's own callers. Mirror that override. Call aliases are left out: backward inverts call-site aliases on the demand in the call flow function before it enters the callee. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit db2bf2955fd8e5a8b951ae1afa2e0e5e72d8dfab)
…llFact MethodCallFlowFunction.Default.propagateUnresolvedCallFact had no startFactBase, so the backward call flow function re-implemented the three resolution-failure adapters of Default and kept an unreachable override that threw. Default now passes the start base through; the forward JIR and Go implementations ignore it. The backward flow function implements propagateUnresolvedCallFact directly and inherits the adapters. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 4c212023a5a221b9d79e7a48b066ed9314d4bfe6)
JIRBackwardMethodCallFactMapper copied the forward mapping. Delegate to JIRMethodCallFactMapper and override only the differences: exit to return answers nothing for Return, call to start maps a demand on the result variable to Return, and valid exit facts are Argument, This and ClassStatic. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 9c0641ba85b8a719a622b932e3beb0b3fd984bb0)
BackwardDemandSeed is a debugging and test aid, yet one was kept for every sink seed, with its fact, for the whole run. Record seeds only when the manager is created with recordDemandSeeds = true; the test harness enables it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 93cfb41a76a49f14ef5ad5f67459f014b13d445c)
…ionMatcher ForwardSuiteCases.sinkMarks counted marks under Not, which the backward analysis never demands, so such a sink would need an impossible finding. Track the polarity and keep positive marks only. Reuse AnalysisTest's functionMatcher (now a companion function) instead of a copy. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit c705c050ed31796b0efdcb275f788be31b09be55)
BackwardRegressionTest (sample BackwardRegressionSample) checks each case against the expected result in both directions: sinks on paths that end in a throw, the heap effect of an always-throwing callee, a loop without exit, call-site aliases rooted at an argument, `this`, a local and a static field, entry sources of a callee reaching the caller through the argument root (no), an argument field, the return value and a static field (yes), and an exit source on a method returning a constant. With stagedRuleSelection the harness wraps the provider in RuleIdSelectingProvider, which honours selectRules like the semgrep provider, and runs Prescan before FullScan; the prescan cases check that call, entry, exit and static-field source rules survive the selection. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit 4f214d60661d1478360d5c8f1d17bb9cea8c56fa)
Section 1: the exceptional exit is a Zero-only entry point; the earlier "exceptional flow ignored, as in forward" rationale was wrong, forward analyses statements before a throw and only ignores summaries at the exceptional exit. Section 3: the fact mapper delegates to forward. Section 4: entry-source findings versus forward's dropArgumentsLocalTaintMarks, and the refinement kept when a matched demand dies. Section 5: call-site aliases of any base and the start fact base passed to propagateUnresolvedCallFact. Section 6: side-effect requirements on summary application. Section 6a: prescan source registration and why it is needed. Sections 8 and 9: gated demand seeds, exceptional flow and rule selection. Section 10: rewritten for the current tests and harness. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> (cherry picked from commit fc59485794af3e308aae6f0961bac316740d84a3)
Main has no shallow-scan phase, no actionable-rule selection and no BaseOnly access-path modes. Select rules the way JIRAnalysisManager does on main, and drop the BaseOnly differential runs and divergence entries. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Since the flow functions subclass the forward ones, the backward inversion of `C.f = x` reused the forward static write, which clears nothing: it tests the field accessor against a fact that starts with the class-static accessor. The demand on ClassStatic.<C>.f therefore survived an overwrite with a constant (forward has the same weak flow step but drops the finding in trace resolution). The backward write now clears <C> from ClassStatic and f from the <C> subtree with two forward RefAccess writes and restores the rest under <C>; the demand still moves to x through the forward static read. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Backward starts a method at its forward exits, and the single-exit graph connects only returns and throws to them, so a region that never exits (an infinite loop after a sink) was never visited and its sinks were never seeded. JIRBackwardNonExitingStarts computes, in the forward method graph, the statements reachable from the entry that reach no exit and returns one representative of every bottom strongly connected component of that region; every statement of the region is backward-reachable from one of them. The backward entry-point resolver adds them to the reversed graph's entry points, and the start flow function treats them like the exceptional exit: Zero only, no caller demands and no end demands. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Drop BackwardSinkOccurrence and BackwardRunResult from the generic layer. BackwardTaintAnalysisManager now only creates the backward manager and prepares the next run (prepareNextBackwardRun returns the run's timeout or null when done); TaintAnalyzer loops over it and reads the engine's vulnerabilities. The JVM backward manager wraps its rules in JIRBackwardSinkSelection, which returns sink rules only for the selected (statement, rule) pairs of a restricted run, so seeding no longer checks restrictions. JIRBackwardSinkAttribution holds the discovery / disjoint-mark group / isolated-run planning, the time-budget fallbacks and reports the confirmed occurrences to the engine's TaintSinkTracker. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… rule provider One backward run replaces the discovery/group/isolation protocol. JIRBackwardTaintRulesProvider swaps the rules: unconditional sources become sinks at the same method and position, sinks become sources that seed their condition demands, conditional sources turn a demand on their product into demands on their condition. The forward rule code (JIRMethodCallTaintUtil, JIRSequentTaintUtil, applyTaintRules, the exit rule steps) applies them, so a finding is an ordinary sink report at the source statement. Exit-sink demands carry zero-edge marks that do not leave the method through its entry, keeping forward's zero-edge-only exit sinks. End-fact requirements become an extra condition on the derived rule, triggered by the end demands. Derived sinks take their id and meta from TaintRulesProvider.sinkMetaForSource (the semgrep automaton of the source). Sink attribution, sink selection, the finding tracker, the end-requirement helper and prepareNextBackwardRun are removed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
In backward mode findings sit at source statements with derived rule ids, so assertReachable checks only that a finding exists and exact finding sets are compared as empty vs non-empty (assertFindings). Forward assertions are unchanged. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Backward behaves as if no sink had trackFactsReachAnalysisEnd: derived rules no longer carry the requirement literal, no end demands are seeded at method exits, and the prescan requirement collection and the analysisEndMethods plumbing are removed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The mark-free cubes of a method-exit sink stay a sink of the backward provider, reported when Zero reaches a return or throw, like the unconditional call and entry sinks. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Negative samples are not checked in backward mode; tests whose negatives report in backward are marked with the cause. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…conditional When every action of a resolved cleaner is an Exact RemoveMark(M, P) and the resolved condition is exactly the disjunction of the ContainsMark(M, P) checks derived from those actions (P, plus P.[e] for array and Object positions), the condition becomes True. Removing an absent mark is a no-op, so forward removes the same marks. Any-field positions, String positions (the removal also clears <string-bytes>), RemoveAllMarks and ExactAndAnyField reach are left conditional. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…lling The backward rule provider keeps a cleaner only with the mark-free cubes of its condition and drops it when every cube needs a mark, so the call flow function runs the forward cleaner step unchanged. JIRBackwardStarUnroller and its wiring are removed. An Exact cleaner of a value again removes a whole any-field star demand on it: CleanerDslAnalysisTest matrix AnyField-Plain-* and field-store-any, and CleanerDslControlFlowAnalysisTest sequenceNestedAfterPlainSink-m1, are not reported in backward mode. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
RemoveMark cannot remove [any] unless its own position has [any]. The forward cleaner step treats the [any] at the cleaned position as possibly empty, so an Exact RemoveMark(M, x) deleted a whole star demand x.[any]M although forward keeps x.fM. JIRBackwardTaintCleanActionEvaluator runs the forward step and, for an Exact RemoveMark whose position has no [any], adds the demand's P.[any] subtree back unchanged. ExactAndAnyField, [any] positions and RemoveAllMarks keep the forward behaviour. Recovers the backward any-field-sink false negatives (CleanerDslAnalysisTest AnyField-Plain matrix and field-store-any, CleanerDslControlFlowAnalysisTest sequenceNestedAfterPlainSink-m1). The kept star over-approximates when the mark sits on the cleaned value itself: the matrix with a plain source now reports Plain-Plain-AnyField-field-depth0 in backward. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…eir actions Replace the exact-disjunction check with a condition rewriter. Every RemoveMark(M, P) checks ContainsMark(P, M) on the fact before removing, so it is a no-op when that literal is false and the literal can be assumed. The condition is put in NNF, assumed literals become True and their negations False, and the result is folded (constants, flattening, duplicates). Since a literal is implied only for its own action, the rewrite is kept only when assuming each action's literal alone yields the same condition. Cleaners with an action that implies no literal keep their condition: RemoveAllMarks, any-field positions and String positions (the removal also clears <string-bytes>). ExactAndAnyField reach performs the same presence check and is now rewritten. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Replace JIRBackwardNonExitingStarts (extra Zero-only entry points at one representative of every bottom SCC of the non-exiting region) with JIRBackwardExitWiringGraph, a wrapper of the forward application graph. On every methodGraph request (no caching) it marks, in a BitSet over instruction indices, the statements from which an exit is reachable by walking predecessors from the exit points, and gives every other statement an extra forward edge to JMethodExitNormalInst (successors += normal exit, predecessors(normal exit) += those statements). The backward manager builds its method inst graph from JIRBackwardExitWiringGraph(graph.reversed).reversed, so that code is backward-reachable from the normal exit. The special entry points and the zero-only start for them are gone; zero-only stays for the exceptional exit. The generic engine and TaintAnalyzer are unchanged. Consequence: a caller demand entering at the normal exit also flows into code that never returns. This only over-approximates and cannot lose a finding. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…onditions A condition literal is implied only by its own RemoveMark action, so a cleaner with several actions is resolved as one cleaner per action, each condition is simplified against that action alone, and cleaners with equal simplified conditions are joined again. resolveMethodRule now returns a list of rules. The split is equivalent: applyCleaner evaluates every applicable cleaner's condition on the same fact before applying actions. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…itions Resolve rules with flatMap. RemoveMark on a String position now assumes its ContainsMark literal like any other position. An any-field removal assumes both ContainsMarkOnAnyField on the base (the form an any-field condition resolves to) and ContainsMark on the position. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… exit The exceptional exit is a zero-only start, so sinks in code that never returns are still seeded, while caller demands entering at the normal exit no longer flow into it. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…marks A rule condition is put in NNF; its positive mark literals form one set regardless of And/Or structure, negated mark literals count as True, and the rest of the condition is folded with every mark literal replaced by True. Every rule kind is swapped uniformly: mark-free sources become sinks, sources with marks become conditional sources, sinks with marks become seeding sources, mark-free sinks stay sinks, cleaners with marks are dropped. Entry-point and static-field sources and method-entry sinks with marks are now derived too and applied by the backward sequent flow function at JMethodEnterInst and at static reads. The $zero-edge shadow marks and their stripping at JMethodEnterInst are removed; exit-sink demands reach callers like any other demand. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
… context Replace JIRBackwardTaintRulesProvider with JIRBackwardTaintAnalysisContext, which extends the forward JIRTaintAnalysisContext and derives the backward rules from the forward rules prepared at the same statement. A prepared condition that is True (or has no positive mark literal) gives the unconditional role, an expression with positive mark literals gives the conditional role with all of them as demanded marks, so mixed conditions such as `A or M@P` keep their mark-free branch. Static-field rules are served by the context, so the sequent flow function no longer builds them. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ent roles Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…bclasses No forward class is open for backward any more and no backward class extends a forward class. The backward components implement the engine interfaces and hold forward instances: the manager delegates to its own JIRAnalysisManager, the taint context wraps a forward JIRTaintAnalysisContext through the extracted JIRTaintRuleContext interface, the method context is a plain JIRMethodAnalysisContext with the backward taint context and fact mapper, and the flow functions and summary handler delegate to forward instances. Forward variation points are parameters with the forward default: the sequent FF's transfer (JIRSequentTransfer), the call FF's clean-action evaluator argument, the clean evaluator's removeFinalFact, the summary handler's withCallAliases, the context's methodCallFactMapper and the manager's relevantRuleIds. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
The forward sequent flow function had to become internal only because an internal interface cannot declare its members internal. Public members keep the forward class as it is on main. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…orward steps The backward sequent flow function is a standalone MethodSequentFlowFunction that calls the forward steps directly with roles swapped: a read x = y.f moves the demand on x through moveIntoField, a write y.f = x applies clearWrittenField and then fieldRead of y.f into x, and a base move kills the demand on the target and rebases it to the source. The rule hooks at return, static reads and method entry are unchanged. JIRSequentTransfer is removed. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…position Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d sequent flow function
The backward sequent flow function now applies
JIRStatementSummary.buildReversed through the core transfer, like the
forward one applies build. Return and throw are plain reversed moves; the
exit rules run at JMethodExitNormalInst / JMethodExitExceptionalInst via the
forward exit rule hooks, as in forward. Entry and static-field rule hooks
are unchanged. The backward flow function is cached per statement.
- buildReversed keeps the per-base type filters.
- In the reversed build a weak (element) write keeps its written path
refinable (a/{[e]} -> a, a.[e] -> a.[e]) instead of the plain identity,
so an abstract demand on the array is refined down to the element and
reaches the stored value (BackwardEdgeCaseTest arrayFilledInCallee).
- Constants carry no facts in JIRStatementSummary.
- The forward exit rule hooks and FactRefiner are public; the sequent FF
cache holds any MethodSequentFlowFunction.
Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Saloed
force-pushed
the
saloed/backward-main
branch
from
October 1, 2026 07:42
09aa1dd to
b253972
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
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.