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

//! Cross-primitive composition gates  -  multi-primitive pipelines
//! that mirror how surgec's rule lowering chains weir ops.
//!
//! Op id: `weir::tests::df::cross_primitive_composition`. Soundness:
//! `Exact`  -  these are pure reference oracle compositions. The test pins
//! the soundness-marker join semantics so a regression that swaps
//! a marker silently widens the composed regime.

use weir::soundness::{Soundness, SoundnessTagged};

#[test]
fn dominators_then_must_init_chain_is_a_subset() {
    // Reaching-def filter pipeline: nodes where some def dominates,
    // then nodes that use the var. Output is subset of both.
    let dom_set = vec![0xFF00_FF00u32];
    let target_set = vec![0xFFFF_FFFFu32];
    let dom_result = weir::oracle::bitset::dominators(&dom_set, &target_set);

    let use_set = vec![0x0FF0_0FF0u32];
    let final_result = weir::oracle::bitset::must_init(&dom_result, &use_set);

    // final_result ⊆ dom_result ⊆ dom_set ∩ target_set, and
    // final_result ⊆ use_set.
    for i in 0..final_result.len() {
        assert_eq!(
            final_result[i] & dom_result[i],
            final_result[i],
            "final ⊄ dom_result at i={i}"
        );
        assert_eq!(
            final_result[i] & use_set[i],
            final_result[i],
            "final ⊄ use_set at i={i}"
        );
    }
}

#[test]
fn may_alias_then_must_init_chain_propagates_soundness() {
    // may_alias is MayOver; must_init is Exact. The composed pipeline
    // is MayOver (the least-precise of the two).
    let composed = weir::may_alias::MayAlias
        .soundness()
        .join(weir::must_init::MustInit.soundness());
    assert_eq!(composed, Soundness::MayOver);
}

#[test]
fn dominators_then_dominators_chain_remains_exact() {
    // Two Exact primitives compose to Exact.
    let composed = weir::dominators::Dominators
        .soundness()
        .join(weir::dominators::Dominators.soundness());
    assert_eq!(composed, Soundness::Exact);
}

#[test]
fn empty_intermediate_propagates_to_zero_final() {
    // First stage produces empty bitset → second stage filters with it
    // → final result is all zero.
    let dom_set = vec![0u32; 4];
    let target_set = vec![0xFFFF_FFFFu32; 4];
    let dom_result = weir::oracle::bitset::dominators(&dom_set, &target_set);
    assert!(dom_result.iter().all(|&w| w == 0));

    let use_set = vec![0xAAAA_AAAAu32; 4];
    let final_result = weir::oracle::bitset::must_init(&dom_result, &use_set);
    assert!(final_result.iter().all(|&w| w == 0));
}

#[test]
fn may_alias_returns_zero_after_dominators_filter_zeroes_pts() {
    // Dominators-filter zeroes out the pts set; may_alias on zero
    // pts must return 0.
    let pts = vec![0xFFFF_FFFFu32; 4];
    let zero_dom = vec![0u32; 4];
    let filtered_pts = weir::oracle::bitset::dominators(&pts, &zero_dom);
    let other_pts = vec![0x5555_5555u32; 4];
    assert_eq!(
        weir::oracle::summary::may_alias(&filtered_pts, &other_pts),
        0
    );
}