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

//! Property-based gates for `weir::oracle::summary::may_alias`.
//!
//! Op id: `weir::tests::df::property::may_alias`. Soundness:
//! `MayOver`. Properties exercised: commutativity, alias-with-self
//! reflexivity, alias-with-empty silence, and idempotent alias
//! detection across 1024 random points-to bitset pairs.

use proptest::prelude::*;
use weir::oracle::summary::may_alias as cpu_ref;

proptest! {
    #![proptest_config(ProptestConfig::with_cases(10_000))]

    /// `may_alias(a, b) == may_alias(b, a)` for any pair.
    #[test]
    fn alias_is_commutative(
        a in proptest::collection::vec(any::<u32>(), 1..16),
        b in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        prop_assert_eq!(cpu_ref(&a, &b), cpu_ref(&b, &a));
    }

    /// `may_alias(a, a) == 1` whenever `a` has any non-zero bit.
    #[test]
    fn alias_with_self_iff_nonempty(
        a in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let any_nonzero = a.iter().any(|w| *w != 0);
        prop_assert_eq!(cpu_ref(&a, &a), u32::from(any_nonzero));
    }

    /// `may_alias(_, ∅) == 0` for any first argument.
    #[test]
    fn alias_with_empty_is_zero(
        a in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let empty = vec![0u32; a.len()];
        prop_assert_eq!(cpu_ref(&a, &empty), 0);
    }

    /// Output is always 0 or 1  -  pure boolean indicator.
    #[test]
    fn output_is_indicator(
        a in proptest::collection::vec(any::<u32>(), 1..16),
        b in proptest::collection::vec(any::<u32>(), 1..16),
    ) {
        let out = cpu_ref(&a, &b);
        prop_assert!(out == 0 || out == 1);
    }
}