Data-flow evidence semantics

Analyzer artifact boundary

One Gradle run-plan entry starts one stig-code-analyzer process and produces one analysis.json. For each represented sink ASIL there are at most two such artifacts:

• data-and-control-flow, with sources whose ASIL is greater than or equal to the sink ASIL; and

• cascading faults, with sources whose ASIL is lower than the sink ASIL.

The word run is too ambiguous for the scopes inside that process. This page uses these terms:

A solver execution may contain many logical sink symbols, and each logical symbol may resolve to multiple physical sink call instructions. Every reached physical sink is reconstructed separately and becomes one evidence component. The single analysis.json then stores all such components and their exact provenance in the run-global evidence store.

All configured sinks of that ASIL remain in the artifact. The ICFG is shared once in controlFlowGraph; it is not duplicated per sink or solver execution.

Schema v7 contains:

• codeAnalysisConfiguration.configuredSources[] and configuredSinks[]: the exact endpoint universe;

• solverExecutions[]: deterministic source-batch/sink-batch coverage and per-sink PhASAR verdicts;

• controlFlowGraph.nodes[] and edges[]: the shared module-scoped LLVM instruction catalog and ICFG;

• sinks[]: one record per physical configured sink, plus diagnostic unconfigured leaks;

• dataFlowEvidence.facts[]: run-global canonical IDE-XTaint facts;

• dataFlowEvidence.states[]: run-global (instruction, fact) states;

• dataFlowEvidence.segmentPayloads[]: run-global ordered state sequences;

• dataFlowEvidence.successorLists[]: exact outgoing position lists stored as consecutive-index runs;

• dataFlowEvidence.topologyShapes[]: delta-coded positional adjacency, roots, terminals, and one base payload layout;

• dataFlowEvidence.topologyTemplates[]: one shape reference plus sparse payload overrides; and

• dataFlowEvidence.components[]: physical-sink/solver provenance, leak facts, source-generation boundaries, one topology-template reference, and deterministic storage statistics.

Each sinks[] record owns only evidenceComponentIndices[] into that run-global store. Its legacy facts[] and dataFlowDAG fields are empty in v7.

Kotlin also reads archived schema-v5 and schema-v6 artifacts explicitly. V5 keeps flattened segments[] and edges[]; it has no solver manifest, canonical state table, or evidence-component provenance. V6 has per-sink fact/state/payload dictionaries and isolated component-local topology. Both are compatibility inputs, not the current native output format. Schema v3/v4 shapes remain unsupported.

In v5, sinks[].facts[] contains facts reported at the sink, and segments[].factIds[] only records which of those sink-leak facts contributed that visible instruction segment during separate per-fact reconstruction. It does not identify the propagated fact at each instruction, encode an (instruction, fact) state sequence, or establish a cross-solver segment identity. V6 and v7 do not reinterpret that legacy field: they replace the missing semantics with canonical facts, exact states, ordered payloads, and provenance-isolated components.

Solver batches and authoritative verdicts

The analyzer partitions one invocation on two axes:

maxSourcesPerSolver is currently fixed to one for compatibility. analyzerExecution.maxSinksPerSolver is nullable: null means all configured sinks in each solver; a positive value partitions the sinks deterministically.

Consequently, for N source configuration entries, M logical sink symbols, and an effective sink capacity T, the current count is N * ceil(M / T). With the default maxSinksPerSolver = null, T = M, so there are N solver executions and every one contains all logical sinks. Physical sink call-site multiplicity does not start more solvers; it determines how many sink verdict records and positive evidence components a solver may produce.

Every configured source/sink pair belongs to exactly one solver execution. A physical sink's final verdict is:

PhASAR's leak verdict is authoritative. A negative solver cell emits no evidence component and never cancels a positive cell. Every positive cell that reached a physical sink emits an isolated component reconstructed from the exact matching leak facts.

One compact artifact is not one merged tree

"Appending a solver's knowledge" means interning its exact immutable facts, states, ordered payloads, successor lists, and reusable topology structures, then adding a provenance-bearing component reference. It does not mean connecting the roots or edges of different reconstructions. A component retains its solver execution, physical sink, matched leak facts, and source-generation boundaries even when some of its immutable structure is shared with other components.

Thus one analyzer invocation produces one compact JSON for all configured sources and sinks, but that JSON represents a collection of independently reconstructable evidence DAGs. A one-sink projection may select several components from different source solvers, and an all-sinks presentation may display their union, but traversal remains component scoped. There is no authoritative cross-component path and no lossless operation that turns the collection into one unlabelled tree by unioning equal-looking vertices or edges.

Facts, states, payloads, and components

A fact describes what is tainted. Its identity is structural, not its display label. The canonical schema records the stable base LLVM value kind and ID, ordered access-path offsets, lifetime/precision state, zero state, and over-approximation marker. For example, facts over the same %result.i base with offsets {0, 0} and {20, 0} are different facts.

A flow state is an exact pair:

The instruction ID is assigned once for the module and reused across all solver executions in the analyzer invocation. Printed LLVM text, opcode, source text, source location, PhASAR ESG node numbers, and reconstruction-local vertex IDs are not cross-solver identities.

A segment payload is an ordered sequence of flow-state references in data-flow order. Order and facts are semantic. Two payloads are equal only when their complete ordered state sequences are equal.

An evidence component is one positive reconstruction for one physical sink and one solver execution. In schema v7 it references one exact topology template and retains its own sink, leak facts, source-generation boundaries, storage statistics, and solver-execution ID. Segment identity inside the template is positional. Equal payload references at positions 7 and 19 remain two vertices even if their ordered state sequences are identical.

A successor list is the exact ordered outgoing segment-position list for one position. It is shared only by exact index-sequence equality and serialized as consecutive (start, length) runs. Empty terminal lists remain explicit.

A topology shape fixes the segment-position count, exact successor-list reference at every position, roots, and terminals. It also holds the first retained template's payload layout as a compression base. Payload and successor-list reference arrays are delta coded: the first index is absolute and every later integer is the exact signed difference from the previous index.

A topology template references one shape and contains sparse (segmentPosition, payloadIndex) overrides against that shape's base payload layout. Thus topologies with identical positional adjacency but different facts/payloads can share the shape without sharing their labels. Two completely equal labelled topologies share one template. Expanding a template always recreates the complete ordered payload-position list, exact edges, roots, and terminals. Sharing a shape or template does not combine component provenance or boundaries.

A source-generation boundary records the real PhASAR transition sourceInstructionId -> generatedStateId and the root segment it anchors. A call-return source normally generates its first non-zero state at the instruction after the source call. The source call therefore must not be encoded as a non-existent (source call, non-zero fact) state. One exact generation transition may anchor several topology-distinct roots when those roots start with the same generated state and diverge later; each root retains its own boundary record.

Equal facts, states, payloads, and successor lists may be interned across the run. Exact positional shapes and complete equal topology templates may also be shared. Individual vertices or edges from non-equal templates may not be interned, unioned, or squashed. In particular, equal visible instruction sequences in two solver results do not authorize an edge union. Such a quotient can create a source-to-sink route that no solver produced.

The native diagnostics and schema-v7 storageStatistics/compaction objects quantify offered-versus-retained facts, states, payloads, successor lists, shapes, templates, payload overrides, segment occurrences, edges, roots, terminals, and boundaries. Canonical-key byte counters are logical identity-encoding sizes, not retained lookup strings or hypothetical expanded JSON size. Actual serialized bytes are recorded per evidence section; the final serialization log covers the complete compact artifact. Producer hash buckets are only accelerators and every candidate reuse is confirmed by full equality.

Scale and independent size limits

Configured source and sink counts determine the solver manifest, but they do not by themselves predict JSON size. Let C be the number of positive (solver execution, physical sink) cells. Expanded per-component storage grows roughly with the sum of all C reconstructed topologies. Schema v7 instead grows with the unique canonical facts, states, ordered payloads, successor lists, topology shapes, labelled templates and sparse overrides, plus component provenance for those C cells. Two runs with the same source and sink counts can therefore have very different sizes depending on reachability and exact structural sharing.

Use dataFlowEvidence.compaction and storageStatistics, rather than N * M, to quantify a concrete invocation. They report offered and retained counts for every interned layer, logical segment/edge occurrences, retained successor targets, shapes/templates/overrides, component count, and serialized evidence-section bytes. The complete serialization log reports the final analysis.json byte count. A full-capacity artifact is still required before treating a bounded sample's reduction ratio as a production estimate.

The former 65,536 bound was a segment-count rejection, not a 65 MB file limit. It has been removed. Schema v7 has no configured analyzer-JSON byte limit and does not permit truncation; a complete component of any segment count must be serialized and validated or the analyzer invocation fails. Available native memory, Gradle heap, disk space, and task timeouts remain operational resource constraints rather than accepted evidence cutoffs.

diagramOutputs.maxArtifactSizeMiB is a separate, late publication policy. It never limits analysis.json or P7 graph generation. P7 retains complete generated diagram artifacts under build/ so sink metrics, postconditions, and local inspection consume the complete result. The appendix writes Cytoscape as a lossless .cyjson.gz declared task output and evaluates the limit on those compressed bytes; other formats use their stored bytes. Only an oversized publication asset is omitted, with a HIGH problem, while the original build artifact remains intact. Browser decompression does not reduce the heap required by the parsed Cytoscape graph. See Source-code analysis diagrams.

Reconstruction direction and graph direction

IDE-XTaint solves forward from the configured source batch. getAllLeaks() returns reached sink instructions and facts for the active sink batch. For each positive physical sink, fact-aware reconstruction follows predecessor states backward through the completed ESG until it reaches the configured source boundary. The serialized component edges are then oriented from source toward sink. PhASAR builds the state vector inside each segment during the backward walk; the native adapter reverses that vector too, so payload state order and component-edge order agree.

Reconstruction is performed only for positive cells. There is no segment-count or evidence-depth success limit. If the complete component cannot be reconstructed, validated, or serialized, the analyzer invocation fails and P6 publishes no partial analyzer output.

What a renderer may draw

For schema v7, a faithful state-level renderer selects a sink's component indices, expands each template's shape, successor runs, index deltas, and payload overrides, and identifies every state by (instructionId, factIndex). It must preserve ordered state payloads and component provenance and must not collapse states to instruction text alone: one instruction can occur under several different facts.

The current STIG data-flow presentation remains segment based:

• detailed-per-segment diagrams render component-local segment instances and their edges;

• detailed-per-IR diagrams may show instruction membership and component/fact provenance, but do not synthesize instruction-only data-flow arrows;

• summarized diagrams contract source-to-sink reachability over the component topology; and

• control-flow/ICFG diagrams use controlFlowGraph.edges[], never data-flow component edges.

Schema-v5 segments[].instructionIds[] remains membership metadata and does not authorize adjacent IR-to-IR arrows. V6/v7 add exact ordered state payloads, but dropping each state's fact and drawing only instruction-to-instruction edges would still lose the distinction the new schema is designed to preserve.

Component-aware source-to-sink chaining

For one physical configured sink and one evidence component:

1. Each position listed in the referenced template's shape rootSegmentIndices[] is a topology root.

2. Each root has one or more distinct sourceBoundaries[] records; repeated physical calls may generate the same root state and all are retained.

3. Every boundary source instruction belongs to that component's solver source batch.

4. The boundary's generatedStateIndex is the first exact state of that root payload.

5. Each position listed in terminalSegmentIndices[] is a topology terminal.

6. Every terminal payload contains the selected physical sink instruction.

7. The component's matched leak facts exactly equal the facts on those terminal sink states.

8. Every component edge references two segment instances in that same component.

9. The component is acyclic.

The validator also requires every positive component to belong to a solver verdict that reached that physical sink. Conversely, when graph emission is enabled, every positive physical-sink OR verdict has at least one valid component.

Components remain isolated while Vista builds an all-sinks view. Presentation-only structural compaction may let equal payloads share a visible representation, but it retains all raw segment/edge aliases plus evidenceComponentIds[] and solverExecutionIds[]. It is never serialized back as analyzer evidence and must not be used to derive a new safety verdict.

Z3 feasibility

Z3 is an optional refinement after PhASAR has already produced the structural leak verdict. It does not rewrite sink.leaked, select diagram edges, or cancel structural evidence.

Schema v7 associates every feasible-fact record with a solverExecutionId. A feasible path uses ordered paths[].instructionIds[] from a configured source instruction to the selected physical sink instruction. Flattened segmentIds[] paths are forbidden in v6/v7 because component-local segments from different solvers must not be treated as one namespace-free path.

Archived schema v5 uses paths[].segmentIds[]; those IDs must reference the same sink's flattened segment DAG. In both schemas, the safe implication is one-way:

A positive structural leak need not have a demonstrated feasible path when the path is infeasible, unknown, or outside bounded enumeration.

Pruning and projection

Data-flow pruning is evidence projection, not visual cleanup:

1. Select the physical call sites for the requested logical sink before transformation.

2. Select only their evidence components.

3. Within each component, keep segments reachable from a selected source root that can also reach the selected sink terminal.

4. Never construct an adjacency edge between components, even when payloads are equal.

The schema-v7 one-sink projection retains only transitively referenced global tables and remaps their indices. If the native shape's original base template is outside the selected sink, the projection promotes one retained template to the base, rewrites the delta-coded arrays, and recomputes every other retained template's sparse overrides. The expanded labelled topology remains identical. This projection is in-memory presentation input, not a new analyzer artifact: retained counters describe the projected tables, while offered counts and serialized-section bytes remain telemetry for the validated native artifact that produced them.

The pruning sidecar records selected source/sink instruction IDs, source/sink/kept/pruned segment IDs, and pruned sink IDs. The report renders that sidecar so an absent path is distinguishable from a renderer projection.

All-sinks and one-sink presentation

Both presentations come from the same compact analyzer artifact:

• one-sink views select the physical call sites and components of one logical configured sink;

• summarized all-sinks data-flow views contain only configured source/sink endpoints and direct reached source-to-physical-sink relations derived from component ownership; they contain no internal facts, states, segments, or topology; and

• detailed all-sinks views are unsupported because they would reverse schema-v7 compaction in memory. The legacy enableDetailedDiagramsForAllSinks setting must remain unset or false; P7 rejects true explicitly.

The generated appendix embeds the non-empty summarized all-sinks SVG (or the configured available primary format) and links detailed one-sink viewers separately.

Validation boundary

The native producer validates canonical interning, successor runs, shapes, exact materialized templates, component ownership/provenance, exact source-generation boundaries, sink terminals, Cartesian coverage, OR verdicts, compaction counters, and a per-component round-trip oracle before serialization. AnalysisResult.validate() repeats the schema and semantic checks before Vista conversion. P7 reports failures as CRITICAL; it does not repair evidence.

See Analyzer output validation for the complete validator groups and Source-code analysis diagrams for the user-facing projections.