weir/points_to/
program.rs

1use super::OP_ID;
2use vyre::ir::Program;
3use vyre_primitives::graph::csr_forward_traverse::csr_forward_traverse;
4use vyre_primitives::graph::program_graph::ProgramGraphShape;
5
6/// Build one Andersen propagation step. Caller MUST supply the real
7/// constraint-graph shape (`node_count`, `edge_count`) so the emitted
8/// Program is dispatched at the correct grid size. The current
9/// points-to bitset is read from `constraints_in` and the expanded
10/// bitset after one subset-edge traversal is written to `pts_out`.
11/// Host iterates to fixpoint.
12///
13/// PHASE6_DATAFLOW HIGH: previous 2-arg entry point hardcoded
14/// `ProgramGraphShape::new(1, 1)`  -  useless for any real constraint
15/// graph (single-node grid means only invocation 0 executes the
16/// kernel and the rest of the constraint graph is silently ignored).
17/// The 2-arg entry was never sound; replaced with the explicit-shape
18/// signature below.
19///
20/// Andersen subset-closure is identical in kernel shape to
21/// [`csr_forward_traverse`] *iterated to fixpoint*. A single dispatch
22/// of this Program is ONE step  -  the caller MUST iterate (e.g. via
23/// `bitset_fixpoint`) until no new bits propagate.
24#[must_use]
25pub fn andersen_points_to(
26    shape: ProgramGraphShape,
27    constraints_in: &str,
28    pts_out: &str,
29) -> Program {
30    csr_forward_traverse(shape, constraints_in, pts_out, u32::MAX)
31}
32
33/// Deprecated alias for back-compat with callers that imported the
34/// pre-fix name `andersen_points_to_with_shape`. Same semantics as
35/// [`andersen_points_to`].
36#[deprecated(
37    since = "0.4.1",
38    note = "use `andersen_points_to(shape, ...)` directly  -  the name suffix is redundant since the 2-arg entry was removed"
39)]
40#[must_use]
41pub fn andersen_points_to_with_shape(
42    shape: ProgramGraphShape,
43    constraints_in: &str,
44    pts_out: &str,
45) -> Program {
46    andersen_points_to(shape, constraints_in, pts_out)
47}
48
49inventory::submit! {
50    vyre_harness::OpEntry::new(
51        OP_ID,
52        || andersen_points_to(ProgramGraphShape::new(4, 3), "pts_in", "pts_out"),
53        Some(|| {
54            let to_bytes = crate::dispatch_decode::pack_u32;
55            // Linear subset chain: 0 ⊆ 1 ⊆ 2 ⊆ 3. The output starts
56            // with the seed so the convergence lens accumulates
57            // reachability instead of replacing it each iteration.
58            vec![vec![
59                to_bytes(&[0, 0, 0, 0]),    // pg_nodes
60                to_bytes(&[0, 1, 2, 3, 3]), // pg_edge_offsets
61                to_bytes(&[1, 2, 3]),       // pg_edge_targets
62                to_bytes(&[1, 1, 1]),       // pg_edge_kind_mask
63                to_bytes(&[0, 0, 0, 0]),    // pg_node_tags
64                to_bytes(&[0b0001]),        // pts_in seed
65                to_bytes(&[0b0001]),        // pts_out accumulator seed
66            ]]
67        }),
68        Some(|| {
69            let to_bytes = crate::dispatch_decode::pack_u32;
70            // One dispatch advances one subset edge and preserves the
71            // accumulator seed. The convergence lens reaches 0b1111.
72            vec![vec![to_bytes(&[0b0011])]]
73        }),
74    )
75}
76
77inventory::submit! {
78    vyre_harness::ConvergenceContract {
79        op_id: OP_ID,
80        max_iterations: 4096,
81    }
82}
83
84/// Marker type for the Andersen points-to dataflow primitive.
85#[derive(Clone, Copy, Debug, PartialEq, Eq)]
86pub struct PointsTo;
87
88impl crate::soundness::SoundnessTagged for PointsTo {
89    fn soundness(&self) -> crate::soundness::Soundness {
90        crate::soundness::Soundness::MayOver
91    }
92}
weir/points_to/program.rs

weir/points_to/
program.rs
