weirflow 0.1.0

GPU-first dataflow analysis primitives for Vyre and Santh compiler pipelines.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

use super::OP_ID;
use vyre::ir::Program;
use vyre_primitives::graph::csr_forward_traverse::csr_forward_traverse;
use vyre_primitives::graph::program_graph::ProgramGraphShape;

/// Build one Andersen propagation step. Caller MUST supply the real
/// constraint-graph shape (`node_count`, `edge_count`) so the emitted
/// Program is dispatched at the correct grid size. The current
/// points-to bitset is read from `constraints_in` and the expanded
/// bitset after one subset-edge traversal is written to `pts_out`.
/// Host iterates to fixpoint.
///
/// PHASE6_DATAFLOW HIGH: previous 2-arg entry point hardcoded
/// `ProgramGraphShape::new(1, 1)`  -  useless for any real constraint
/// graph (single-node grid means only invocation 0 executes the
/// kernel and the rest of the constraint graph is silently ignored).
/// The 2-arg entry was never sound; replaced with the explicit-shape
/// signature below.
///
/// Andersen subset-closure is identical in kernel shape to
/// [`csr_forward_traverse`] *iterated to fixpoint*. A single dispatch
/// of this Program is ONE step  -  the caller MUST iterate (e.g. via
/// `bitset_fixpoint`) until no new bits propagate.
#[must_use]
pub fn andersen_points_to(
    shape: ProgramGraphShape,
    constraints_in: &str,
    pts_out: &str,
) -> Program {
    csr_forward_traverse(shape, constraints_in, pts_out, u32::MAX)
}

/// Deprecated alias for back-compat with callers that imported the
/// pre-fix name `andersen_points_to_with_shape`. Same semantics as
/// [`andersen_points_to`].
#[deprecated(
    since = "0.4.1",
    note = "use `andersen_points_to(shape, ...)` directly  -  the name suffix is redundant since the 2-arg entry was removed"
)]
#[must_use]
pub fn andersen_points_to_with_shape(
    shape: ProgramGraphShape,
    constraints_in: &str,
    pts_out: &str,
) -> Program {
    andersen_points_to(shape, constraints_in, pts_out)
}

inventory::submit! {
    vyre_harness::OpEntry::new(
        OP_ID,
        || andersen_points_to(ProgramGraphShape::new(4, 3), "pts_in", "pts_out"),
        Some(|| {
            let to_bytes = crate::dispatch_decode::pack_u32;
            // Linear subset chain: 0 ⊆ 1 ⊆ 2 ⊆ 3. The output starts
            // with the seed so the convergence lens accumulates
            // reachability instead of replacing it each iteration.
            vec![vec![
                to_bytes(&[0, 0, 0, 0]),    // pg_nodes
                to_bytes(&[0, 1, 2, 3, 3]), // pg_edge_offsets
                to_bytes(&[1, 2, 3]),       // pg_edge_targets
                to_bytes(&[1, 1, 1]),       // pg_edge_kind_mask
                to_bytes(&[0, 0, 0, 0]),    // pg_node_tags
                to_bytes(&[0b0001]),        // pts_in seed
                to_bytes(&[0b0001]),        // pts_out accumulator seed
            ]]
        }),
        Some(|| {
            let to_bytes = crate::dispatch_decode::pack_u32;
            // One dispatch advances one subset edge and preserves the
            // accumulator seed. The convergence lens reaches 0b1111.
            vec![vec![to_bytes(&[0b0011])]]
        }),
    )
}

inventory::submit! {
    vyre_harness::ConvergenceContract {
        op_id: OP_ID,
        max_iterations: 4096,
    }
}

/// Marker type for the Andersen points-to dataflow primitive.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct PointsTo;

impl crate::soundness::SoundnessTagged for PointsTo {
    fn soundness(&self) -> crate::soundness::Soundness {
        crate::soundness::Soundness::MayOver
    }
}