Skip to main content

weir/
control_dependence.rs

1//! `control_dependence`  -  does `b` execute on every path through `a`?
2//!
3//! Equivalent: `b` is control-dependent on `a` iff `a` does NOT
4//! post-dominate `b` AND `a` post-dominates SOME successor of `b`.
5//! Encoded as a per-node bitset dataflow consumers can intersect with
6//! sink sets for "guarded vs unguarded" analysis.
7
8use vyre::ir::Program;
9use vyre_primitives::bitset::and_not::bitset_and_not;
10use vyre_primitives::graph::csr_forward_traverse::bitset_words;
11
12pub(crate) const OP_ID: &str = "weir::control_dependence";
13
14/// Build a control-dependence query Program. Inputs:
15/// - `successor_pdom`: per-node bitset where bit `n` is set iff `a`
16///   post-dominates a successor of `n`.
17/// - `pdom_n`:         per-node bitset of nodes `a` post-dominates.
18/// - `out`:            per-node bitset; bit `n` set iff `n` is
19///   control-dependent on `a` (= `successor_pdom`
20///   AND NOT `pdom_n`).
21#[must_use]
22pub fn control_dependence(
23    node_count: u32,
24    successor_pdom: &str,
25    pdom_n: &str,
26    out: &str,
27) -> Program {
28    let words = bitset_words(node_count);
29    vyre_harness::region::tag_program(OP_ID, bitset_and_not(successor_pdom, pdom_n, out, words))
30}
31
32/// reference oracle.
33#[must_use]
34#[cfg(any(test, feature = "cpu-parity"))]
35#[deprecated(
36    note = "reference oracle only; production code must dispatch the Weir Program on a concrete GPU backend or use weir::oracle for parity evidence"
37)]
38pub(crate) fn cpu_ref(successor_pdom: &[u32], pdom_n: &[u32]) -> Vec<u32> {
39    vyre_primitives::bitset::and_not::cpu_ref(successor_pdom, pdom_n)
40}
41
42/// Soundness marker for [`control_dependence`].
43#[derive(Clone, Copy, Debug, PartialEq, Eq)]
44pub struct ControlDependence;
45impl super::soundness::SoundnessTagged for ControlDependence {
46    fn soundness(&self) -> super::soundness::Soundness {
47        super::soundness::Soundness::Exact
48    }
49}
50
51inventory::submit! {
52    vyre_harness::OpEntry::new(
53        OP_ID,
54        || control_dependence(4, "succ_pdom", "pdom", "out"),
55        Some(|| {
56            let u32s = crate::dispatch_decode::pack_u32;
57            vec![vec![u32s(&[0b1111]), u32s(&[0b0001]), u32s(&[0])]]
58        }),
59        Some(|| {
60            let u32s = crate::dispatch_decode::pack_u32;
61            vec![vec![u32s(&[0b1110])]]
62        }),
63    )
64}
65
66#[cfg(test)]
67#[allow(deprecated)]
68mod tests {
69    use super::*;
70
71    #[test]
72    fn classical_control_dep() {
73        // succ_pdom = bits 0-3 (a post-dominates a successor of each),
74        // pdom_n = bit 0 (a post-dominates n=0). Result: bits 1-3.
75        assert_eq!(cpu_ref(&[0b1111], &[0b0001]), vec![0b1110]);
76    }
77
78    #[test]
79    fn full_pdom_means_no_control_dep() {
80        assert_eq!(cpu_ref(&[0xFFFF], &[0xFFFF]), vec![0]);
81    }
82
83    #[test]
84    fn no_pdom_gives_full_control_dep() {
85        assert_eq!(cpu_ref(&[0xFFFF], &[0]), vec![0xFFFF]);
86    }
87
88    #[test]
89    fn empty_succ_pdom_yields_empty() {
90        assert_eq!(cpu_ref(&[0], &[0xFFFF]), vec![0]);
91    }
92}