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 anifds_gpu::IfdsShapedo not have to manually project toProgramGraphShape.