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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

//! `may_alias`  -  Andersen-style may-alias query packed as a bitset.
//!
//! Given two pointer expressions `p` and `q`, return 1 iff their
//! points-to sets overlap (`pts(p) ∩ pts(q) ≠ ∅`). Implementation:
//! per-node bitset AND of pts(p) and pts(q), then any-reduce.
//!
//! Soundness: [`MayOver`](super::soundness::Soundness::MayOver).

use std::sync::Arc;

use vyre::ir::model::expr::Ident;
use vyre::ir::{BufferAccess, BufferDecl, DataType, Expr, Node, Program};
use vyre_primitives::graph::csr_forward_traverse::bitset_words;

pub(crate) const OP_ID: &str = "weir::may_alias";

/// Build a may-alias Program. Inputs:
/// - `pts_p`, `pts_q`: per-node points-to bitsets.
/// - `intersect_buf`: scratch.
/// - `out_scalar`: 1 if the points-to sets overlap, else 0.
#[must_use]
pub fn may_alias(
    node_count: u32,
    pts_p: &str,
    pts_q: &str,
    intersect_buf: &str,
    out_scalar: &str,
) -> Program {
    let words = bitset_words(node_count);
    let t = Expr::InvocationId { axis: 0 };
    let body = vec![
        Node::let_bind(
            "intersect",
            Expr::bitand(Expr::load(pts_p, t.clone()), Expr::load(pts_q, t.clone())),
        ),
        Node::store(intersect_buf, t.clone(), Expr::var("intersect")),
        Node::if_then(
            Expr::ne(Expr::var("intersect"), Expr::u32(0)),
            vec![Node::let_bind(
                "_",
                Expr::atomic_or(out_scalar, Expr::u32(0), Expr::u32(1)),
            )],
        ),
    ];
    Program::wrapped(
        vec![
            BufferDecl::storage(pts_p, 0, BufferAccess::ReadOnly, DataType::U32).with_count(words),
            BufferDecl::storage(pts_q, 1, BufferAccess::ReadOnly, DataType::U32).with_count(words),
            BufferDecl::storage(intersect_buf, 2, BufferAccess::ReadWrite, DataType::U32)
                .with_count(words),
            BufferDecl::output(out_scalar, 3, DataType::U32).with_count(1),
        ],
        [256, 1, 1],
        vec![Node::Region {
            generator: Ident::from(OP_ID),
            source_region: None,
            body: Arc::new(vec![Node::if_then(
                Expr::lt(t.clone(), Expr::u32(words)),
                body,
            )]),
        }],
    )
}

inventory::submit! {
    vyre_harness::OpEntry::new(
        OP_ID,
        || may_alias(4, "a", "b", "scratch", "out"),
        Some(|| {
            let u32s = crate::dispatch_decode::pack_u32;
            vec![vec![u32s(&[0b1100]), u32s(&[0b1010]), u32s(&[0])]]
        }),
        Some(|| {
            let u32s = crate::dispatch_decode::pack_u32;
            vec![vec![u32s(&[0b1000]), u32s(&[1])]]
        }),
    )
}

/// reference oracle.
#[must_use]
#[cfg(any(test, feature = "cpu-parity"))]
#[deprecated(
    note = "reference oracle only; production code must dispatch the Weir Program on a concrete GPU backend or use weir::oracle for parity evidence"
)]
pub(crate) fn cpu_ref(pts_p: &[u32], pts_q: &[u32]) -> u32 {
    u32::from(
        pts_p
            .iter()
            .zip(pts_q.iter())
            .any(|(left, right)| left & right != 0),
    )
}

/// Soundness marker for [`may_alias`].
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct MayAlias;
impl super::soundness::SoundnessTagged for MayAlias {
    fn soundness(&self) -> super::soundness::Soundness {
        super::soundness::Soundness::MayOver
    }
}

#[cfg(test)]
#[allow(deprecated)]
mod tests {
    use super::*;

    #[test]
    fn overlapping_pts_alias() {
        assert_eq!(cpu_ref(&[0b1010], &[0b0011]), 1);
    }

    #[test]
    fn disjoint_pts_dont_alias() {
        assert_eq!(cpu_ref(&[0b1010], &[0b0101]), 0);
    }

    #[test]
    fn empty_pts_dont_alias() {
        assert_eq!(cpu_ref(&[0], &[0xFFFF]), 0);
    }

    #[test]
    fn identical_pts_alias() {
        assert_eq!(cpu_ref(&[0xDEAD], &[0xDEAD]), 1);
    }
}