Skip to main content

Module ifds

Module ifds 

Source
Expand description

IFDS/IDE interprocedural dataflow framework (DF-4).

Build one reachability step over the exploded supergraph:

use weir::ifds::ifds_reach_step;
use vyre_primitives::graph::program_graph::ProgramGraphShape;

let shape = ProgramGraphShape::new(4, 4);
let step = ifds_reach_step(shape, "fin", "fout");

DF-4 - IFDS/IDE interprocedural dataflow framework.

Reps & Horwitz & Sagiv (1995): distributive dataflow problems over a finite domain D reduce to graph reachability on the exploded super-graph. Nodes are (statement × fact) pairs; edges encode flow + call-return summary edges. Reaching a sink fact from a source fact = the source taint flows to the sink along some interprocedural path that respects matched call/return.

Following the vyre-libs::security::flows_to idiom, this module ships ONE dispatch step of forward reachability over the super- graph. The caller-side fixpoint driver iterates it until the reach frontier converges, and the surge stdlib composes the source/sink/sanitizer triple on top.

§Soundness

PHASE6_DATAFLOW CRITICAL: previous docstring claimed Soundness::Exact. That was a lie - the body is generic forward reachability with 0xFFFF_FFFF mask, NO call/return matching, NO summary edges, NO sanitizer gating, and NO exploded super-graph construction. Real Reps-Horwitz-Sagiv requires building the exploded super-graph (handled by [super::ifds_gpu]) and then running the step kernel over it.

This module’s [ifds_reach_step] is now correctly tagged MayOver and delegates to [super::ifds_gpu::ifds_gpu_step] when the caller passes a real [super::ifds_gpu::IfdsShape]. The Tier-3 ProgramGraphShape entry remains for back-compat callers that pre-built the CSR by hand - those callers MUST still iterate to fixpoint and gate sanitizer facts themselves.

Rules requiring zero-FP MUST compose this primitive with an explicit sanitizer mask after each step - see surge stdlib flows_to_with_sanitizer.

Underpins C01, C08, C09, C13, C15, C16, C18.

Structs§

Ifds
Marker type for the IFDS interprocedural dataflow primitive.

Functions§

ifds_reach_closure_borrowed_into_result_with_scratch_via
GPU IFDS reachability closure using borrowed dispatch inputs, caller-owned fixed-point scratch, and caller-owned result storage.
ifds_reach_closure_borrowed_into_via
GPU IFDS reachability closure using borrowed dispatch inputs and caller-owned output storage.
ifds_reach_closure_borrowed_into_with_scratch_via
GPU IFDS reachability closure using borrowed dispatch inputs and caller-owned fixed-point scratch.
ifds_reach_closure_borrowed_via
GPU IFDS reachability closure using borrowed dispatch inputs.
ifds_reach_closure_via
ifds_reach_step
Build one IFDS forward-reachability step over an exploded super-graph laid out as a ProgramGraph.
ifds_reach_step_exploded
PHASE6_DATAFLOW CRITICAL: bridge from the high-level IFDS surface to the GPU-native exploded-supergraph step. Pre-fix this module did not import [super::ifds_gpu] at all - the G3 implementation was orphaned. This entry point composes the exploded-supergraph shape with the GPU step kernel so callers that already hold an ifds_gpu::IfdsShape do not have to manually project to ProgramGraphShape.