xqvm 0.2.0

X-Quadratic Virtual Machine — bytecode interpreter for the XQuad Toolchain
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97

// Copyright (C) 2026 Postquant Labs Incorporated
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU Affero General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Affero General Public License for more details.
//
// You should have received a copy of the GNU Affero General Public License
// along with this program.  If not, see <https://www.gnu.org/licenses/>.
//
// SPDX-License-Identifier: AGPL-3.0-or-later

use core::hash::Hash;

use crate::dataflow::direction::Direction;
use crate::dataflow::lattice::Lattice;

/// Template for a data-flow analysis.
///
/// Implement this trait to define a new analysis.  The worklist solver in
/// [`crate::dataflow::solve`] drives the fixed-point computation; you supply
/// only the domain-specific parts:
///
/// - **`type Value`** -- the lattice element representing facts at a point.
/// - **`type Node`** -- the unit of analysis (typically a basic block index or
///   byte offset).
/// - **`type Dir`** -- [`Forward`](crate::dataflow::Forward) or
///   [`Backward`](crate::dataflow::Backward).
/// - **`boundary_value`** -- the seed value injected at the boundary node
///   (CFG entry for forward, CFG exit for backward).
/// - **`transfer`** -- apply one node's effect to an incoming value, producing
///   the outgoing value.
///
/// # Examples
///
/// A forward constant-zero check (toy example):
///
/// ```rust
/// use xqvm::dataflow::{Analysis, Forward, Lattice};
///
/// #[derive(Clone, PartialEq, Eq)]
/// enum Zeroness { MaybeNonZero, DefinitelyZero }
///
/// impl Lattice for Zeroness {
///     fn top() -> Self { Self::MaybeNonZero }
///     fn meet(&self, other: &Self) -> Self {
///         match (self, other) {
///             (Self::DefinitelyZero, Self::DefinitelyZero) => Self::DefinitelyZero,
///             _ => Self::MaybeNonZero,
///         }
///     }
/// }
///
/// struct ZeronessAnalysis;
///
/// impl Analysis for ZeronessAnalysis {
///     type Value = Zeroness;
///     type Node  = u32;
///     type Dir   = Forward;
///
///     fn boundary_value(&self) -> Zeroness { Zeroness::DefinitelyZero }
///
///     fn transfer(&self, _node: &u32, input: &Zeroness) -> Zeroness {
///         input.clone()
///     }
/// }
/// ```
pub trait Analysis {
    /// The lattice element used as the data-flow value.
    type Value: Lattice;

    /// The type identifying a node (basic block) in the CFG.
    type Node: Eq + Hash + Clone;

    /// The flow direction: [`Forward`](crate::dataflow::Forward) or
    /// [`Backward`](crate::dataflow::Backward).
    type Dir: Direction;

    /// The value injected at the boundary node before the fixed-point iteration.
    ///
    /// For forward analyses this seeds the CFG entry; for backward analyses the
    /// CFG exit.
    fn boundary_value(&self) -> Self::Value;

    /// Apply the effect of `node` to `input`, producing the outgoing value.
    ///
    /// `input` is the meet of all values arriving at `node` from its
    /// predecessors (forward) or successors (backward).  The transfer function
    /// must be monotone: if `a <= b` in the lattice then
    /// `transfer(node, a) <= transfer(node, b)`.
    fn transfer(&self, node: &Self::Node, input: &Self::Value) -> Self::Value;
}