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

//! Adversarial-input gates for weir reference oracles.
//!
//! Op id: `weir::tests::df::adversarial`. Soundness: `Exact` over
//! the contract  -  every oracle must return a well-defined output
//! (not panic, not OOB-index) on hostile inputs: empty vectors,
//! single-byte tail with mismatched lengths, max-u32 boundary
//! values, and zero-padded right-extension.

/// Length-mismatch shouldn't OOB-index any oracle.
#[test]
fn bitset_and_oracles_truncate_to_shorter_input() {
    let long = vec![0xFFu32; 10];
    let short = vec![0x0Fu32; 1];
    // Truncates to len 1 in all cases.
    assert_eq!(weir::oracle::bitset::dominators(&long, &short).len(), 1);
    assert_eq!(weir::oracle::bitset::must_init(&long, &short).len(), 1);
    assert_eq!(weir::oracle::bitset::scc_query(&long, &short).len(), 1);
    assert_eq!(weir::oracle::bitset::value_set(&long, &short).len(), 1);
    assert_eq!(weir::oracle::bitset::post_dominates(&long, &short).len(), 1);
    assert_eq!(weir::oracle::bitset::live_at(&long, &short).len(), 1);
    assert_eq!(weir::oracle::bitset::escapes(&long, &short).len(), 1);
}

/// Empty inputs must produce empty outputs without panic.
#[test]
fn bitset_oracles_return_empty_on_empty_input() {
    assert!(weir::oracle::bitset::dominators(&[], &[]).is_empty());
    assert!(weir::oracle::bitset::must_init(&[], &[]).is_empty());
    assert!(weir::oracle::bitset::scc_query(&[], &[]).is_empty());
    assert!(weir::oracle::bitset::value_set(&[], &[]).is_empty());
    assert!(weir::oracle::bitset::post_dominates(&[], &[]).is_empty());
    assert!(weir::oracle::bitset::live_at(&[], &[]).is_empty());
    assert!(weir::oracle::bitset::escapes(&[], &[]).is_empty());
    assert_eq!(weir::oracle::summary::may_alias(&[], &[]), 0);
}

/// max-u32 word should not panic the AND oracles.
#[test]
fn bitset_and_oracles_handle_u32_max_values() {
    let max = vec![u32::MAX; 4];
    let half = vec![0xFFFF_FFFFu32, 0x0000_FFFFu32, 0xFFFF_0000u32, 0u32];
    let out = weir::oracle::bitset::dominators(&max, &half);
    assert_eq!(
        out,
        vec![0xFFFF_FFFFu32, 0x0000_FFFFu32, 0xFFFF_0000u32, 0u32]
    );
}

/// range_check on adversarial u32 boundary values.
#[test]
fn range_check_adversarial_boundary_values() {
    // hi[0] = u32::MAX, bound[0] = u32::MAX → not strictly less → 0.
    // hi[1] = u32::MAX - 1, bound[1] = u32::MAX → strictly less → 1.
    // hi[2] = 0, bound[2] = 0 → not strictly less → 0.
    // hi[3] = 0, bound[3] = 1 → strictly less → 1.
    let hi = vec![u32::MAX, u32::MAX - 1, 0u32, 0u32];
    let bnd = vec![u32::MAX, u32::MAX, 0u32, 1u32];
    let out = weir::oracle::summary::range_check(&hi, &bnd);
    assert_eq!(out, vec![0u32, 1u32, 0u32, 1u32]);
}

/// may_alias on a bitset where the only overlap is in the last bit
/// of the last word.
#[test]
fn may_alias_detects_high_bit_overlap_in_last_word() {
    let a = vec![0u32, 0u32, 0u32, 1u32 << 31];
    let b = vec![0xFFFFu32, 0u32, 0u32, 1u32 << 31];
    assert_eq!(weir::oracle::summary::may_alias(&a, &b), 1);
}

/// may_alias returns 0 when only one input has bits set, even when
/// length matches.
#[test]
fn may_alias_returns_zero_when_one_side_is_zero() {
    let a = vec![0u32, 0u32, 0u32, 0u32];
    let b = vec![0xFFFFu32; 4];
    assert_eq!(weir::oracle::summary::may_alias(&a, &b), 0);
    assert_eq!(weir::oracle::summary::may_alias(&b, &a), 0);
}