weir/
may_alias.rs

1//! `may_alias`  -  Andersen-style may-alias query packed as a bitset.
2//!
3//! Given two pointer expressions `p` and `q`, return 1 iff their
4//! points-to sets overlap (`pts(p) ∩ pts(q) ≠ ∅`). Implementation:
5//! per-node bitset AND of pts(p) and pts(q), then any-reduce.
6//!
7//! Soundness: [`MayOver`](super::soundness::Soundness::MayOver).
8
9use std::sync::Arc;
10
11use vyre::ir::model::expr::Ident;
12use vyre::ir::{BufferAccess, BufferDecl, DataType, Expr, Node, Program};
13use vyre_primitives::graph::csr_forward_traverse::bitset_words;
14
15pub(crate) const OP_ID: &str = "weir::may_alias";
16
17/// Build a may-alias Program. Inputs:
18/// - `pts_p`, `pts_q`: per-node points-to bitsets.
19/// - `intersect_buf`: scratch.
20/// - `out_scalar`: 1 if the points-to sets overlap, else 0.
21#[must_use]
22pub fn may_alias(
23    node_count: u32,
24    pts_p: &str,
25    pts_q: &str,
26    intersect_buf: &str,
27    out_scalar: &str,
28) -> Program {
29    let words = bitset_words(node_count);
30    let t = Expr::InvocationId { axis: 0 };
31    let body = vec![
32        Node::let_bind(
33            "intersect",
34            Expr::bitand(Expr::load(pts_p, t.clone()), Expr::load(pts_q, t.clone())),
35        ),
36        Node::store(intersect_buf, t.clone(), Expr::var("intersect")),
37        Node::if_then(
38            Expr::ne(Expr::var("intersect"), Expr::u32(0)),
39            vec![Node::let_bind(
40                "_",
41                Expr::atomic_or(out_scalar, Expr::u32(0), Expr::u32(1)),
42            )],
43        ),
44    ];
45    Program::wrapped(
46        vec![
47            BufferDecl::storage(pts_p, 0, BufferAccess::ReadOnly, DataType::U32).with_count(words),
48            BufferDecl::storage(pts_q, 1, BufferAccess::ReadOnly, DataType::U32).with_count(words),
49            BufferDecl::storage(intersect_buf, 2, BufferAccess::ReadWrite, DataType::U32)
50                .with_count(words),
51            BufferDecl::output(out_scalar, 3, DataType::U32).with_count(1),
52        ],
53        [256, 1, 1],
54        vec![Node::Region {
55            generator: Ident::from(OP_ID),
56            source_region: None,
57            body: Arc::new(vec![Node::if_then(
58                Expr::lt(t.clone(), Expr::u32(words)),
59                body,
60            )]),
61        }],
62    )
63}
64
65inventory::submit! {
66    vyre_harness::OpEntry::new(
67        OP_ID,
68        || may_alias(4, "a", "b", "scratch", "out"),
69        Some(|| {
70            let u32s = crate::dispatch_decode::pack_u32;
71            vec![vec![u32s(&[0b1100]), u32s(&[0b1010]), u32s(&[0])]]
72        }),
73        Some(|| {
74            let u32s = crate::dispatch_decode::pack_u32;
75            vec![vec![u32s(&[0b1000]), u32s(&[1])]]
76        }),
77    )
78}
79
80/// reference oracle.
81#[must_use]
82#[cfg(any(test, feature = "cpu-parity"))]
83#[deprecated(
84    note = "reference oracle only; production code must dispatch the Weir Program on a concrete GPU backend or use weir::oracle for parity evidence"
85)]
86pub(crate) fn cpu_ref(pts_p: &[u32], pts_q: &[u32]) -> u32 {
87    u32::from(
88        pts_p
89            .iter()
90            .zip(pts_q.iter())
91            .any(|(left, right)| left & right != 0),
92    )
93}
94
95/// Soundness marker for [`may_alias`].
96#[derive(Clone, Copy, Debug, PartialEq, Eq)]
97pub struct MayAlias;
98impl super::soundness::SoundnessTagged for MayAlias {
99    fn soundness(&self) -> super::soundness::Soundness {
100        super::soundness::Soundness::MayOver
101    }
102}
103
104#[cfg(test)]
105#[allow(deprecated)]
106mod tests {
107    use super::*;
108
109    #[test]
110    fn overlapping_pts_alias() {
111        assert_eq!(cpu_ref(&[0b1010], &[0b0011]), 1);
112    }
113
114    #[test]
115    fn disjoint_pts_dont_alias() {
116        assert_eq!(cpu_ref(&[0b1010], &[0b0101]), 0);
117    }
118
119    #[test]
120    fn empty_pts_dont_alias() {
121        assert_eq!(cpu_ref(&[0], &[0xFFFF]), 0);
122    }
123
124    #[test]
125    fn identical_pts_alias() {
126        assert_eq!(cpu_ref(&[0xDEAD], &[0xDEAD]), 1);
127    }
128}
weir/may_alias.rs

weir/
may_alias.rs
