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

//! `weir::may_alias`  -  Program construction + reference oracle parity.
//!
//! Op id: `weir::tests::df::may_alias`. Soundness: `MayOver`  -
//! the may-alias predicate is true when two points-to sets share
//! any node. The reference oracle returns 1 iff the bitwise-AND of the
//! two pts sets has any non-zero word; the GPU Program reduces
//! the same intersection through `bitset_any`. These tests pin
//! the oracle's truth table and the Program's buffer set so a
//! refactor that breaks either direction is caught at compile-test
//! time, before reaching the dispatch path.

use weir::may_alias::may_alias;
use weir::oracle::summary::may_alias as cpu_ref;

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

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

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

#[test]
fn cpu_ref_handles_multi_word_overlap_in_high_word() {
    // word 0 disjoint, word 1 overlaps on bit 17.
    let p = vec![0b0000_0000u32, 1u32 << 17];
    let q = vec![0b1111_0000u32, (1u32 << 17) | (1u32 << 5)];
    assert_eq!(cpu_ref(&p, &q), 1);
}

#[test]
fn may_alias_program_declares_four_buffers() {
    let prog = may_alias(64, "pts_p", "pts_q", "intersect", "out");
    let mut names: Vec<&str> = prog.buffers().iter().map(|b| b.name()).collect();
    names.sort();
    // pts_p and pts_q are inputs; intersect is scratch; out is the
    // 1-element scalar result.
    assert!(names.contains(&"pts_p"), "missing pts_p in {names:?}");
    assert!(names.contains(&"pts_q"), "missing pts_q in {names:?}");
    assert!(
        names.contains(&"intersect"),
        "missing intersect in {names:?}"
    );
    assert!(names.contains(&"out"), "missing out in {names:?}");
    assert!(!prog.entry().is_empty(), "may_alias must emit kernel body");
}

#[test]
fn may_alias_program_node_count_scales() {
    for &n in &[1u32, 32, 33, 64, 128] {
        let prog = may_alias(n, "p", "q", "i", "o");
        assert_eq!(prog.buffers().len(), 4, "node_count={n}: 4 buffers");
        assert!(!prog.entry().is_empty());
    }
}