weir/ifds/tag.rs
1use super::{ifds_reach_step, OP_ID};
2use vyre_primitives::graph::program_graph::ProgramGraphShape;
3
4inventory::submit! {
5 vyre_harness::OpEntry::new(
6 OP_ID,
7 || ifds_reach_step(ProgramGraphShape::new(4, 3), "fin", "fout"),
8 Some(|| {
9 let to_bytes = crate::dispatch_decode::pack_u32;
10 // Tiny supergraph: 0 is a source, 3 is a sink, edges
11 // 0→1→2→3. One step propagates the frontier from 0 to 1.
12 vec![vec![
13 to_bytes(&[0, 0, 0, 0]), // pg_nodes
14 to_bytes(&[0, 1, 2, 3, 3]), // pg_edge_offsets
15 to_bytes(&[1, 2, 3]), // pg_edge_targets
16 to_bytes(&[1, 1, 1]), // pg_edge_kind_mask
17 to_bytes(&[0, 0, 0, 0]), // pg_node_tags
18 to_bytes(&[0b0001]), // fin = {source at 0}
19 to_bytes(&[0b0001]), // fout accumulator seed
20 ]]
21 }),
22 Some(|| {
23 let to_bytes = crate::dispatch_decode::pack_u32;
24 vec![vec![to_bytes(&[0b0011])]]
25 }),
26 )
27}
28
29inventory::submit! {
30 vyre_harness::ConvergenceContract {
31 op_id: OP_ID,
32 max_iterations: 128,
33 }
34}
35
36/// Marker type for the IFDS interprocedural dataflow primitive.
37#[derive(Clone, Copy, Debug, PartialEq, Eq)]
38pub struct Ifds;
39
40impl crate::soundness::SoundnessTagged for Ifds {
41 /// PHASE6_DATAFLOW CRITICAL: corrected from `Exact` to `MayOver`.
42 /// The current implementation is a single forward-reach step over
43 /// a caller-provided supergraph - it is sound (over-approximates)
44 /// only when (a) the supergraph encodes call/return matching and
45 /// (b) the host iterates to fixpoint with sanitizer gating after
46 /// every step. Without those, this is reachability and may report
47 /// non-realizable paths.
48 fn soundness(&self) -> crate::soundness::Soundness {
49 crate::soundness::Soundness::MayOver
50 }
51}