veri_ir/
annotation_ir.rs

1/// A higher-level annotation IR that does not specify bitvector widths.
2/// This allows annotations to be generic over possible types, which
3/// corresponds to how ISLE rewrites are written.
4use std::fmt;
5/// A bound variable, including the VIR type
6#[derive(Clone, Debug, PartialEq, Eq)]
7pub struct BoundVar {
8    pub name: String,
9    pub ty: Option<Type>,
10}
11
12impl BoundVar {
13    /// Construct a new bound variable
14    pub fn new_with_ty(name: &str, ty: &Type) -> Self {
15        BoundVar {
16            name: name.to_string(),
17            ty: Some(ty.clone()),
18        }
19    }
20
21    /// Construct a new bound variable, cloning from references
22    pub fn new(name: &str) -> Self {
23        BoundVar {
24            name: name.to_string(),
25            ty: None,
26        }
27    }
28
29    /// An expression with the bound variable's name
30    pub fn as_expr(&self) -> Expr {
31        Expr::Var(self.name.clone())
32    }
33}
34
35/// A function signature annotation, including the bound variable names for all
36/// arguments and the return value.
37#[derive(Clone, Debug, PartialEq, Eq)]
38pub struct TermSignature {
39    pub args: Vec<BoundVar>,
40    pub ret: BoundVar,
41}
42
43/// Verification IR annotations for an ISLE term consist of the function
44/// signature and a list of assertions.
45#[derive(Clone, Debug, PartialEq, Eq)]
46pub struct TermAnnotation {
47    pub sig: TermSignature,
48    // Note: extra Box for now for ease of parsing
49    #[allow(clippy::vec_box)]
50    pub assumptions: Vec<Box<Expr>>,
51
52    #[allow(clippy::vec_box)]
53    pub assertions: Vec<Box<Expr>>,
54}
55
56impl TermAnnotation {
57    /// New annotation
58    pub fn new(sig: TermSignature, assumptions: Vec<Expr>, assertions: Vec<Expr>) -> Self {
59        TermAnnotation {
60            sig,
61            assumptions: assumptions.iter().map(|x| Box::new(x.clone())).collect(),
62            assertions: assertions.iter().map(|x| Box::new(x.clone())).collect(),
63        }
64    }
65
66    pub fn sig(&self) -> &TermSignature {
67        &self.sig
68    }
69
70    pub fn assertions(&self) -> Vec<Expr> {
71        self.assumptions.iter().map(|x| *x.clone()).collect()
72    }
73}
74
75/// Higher-level type, not including bitwidths.
76#[derive(Clone, Debug, Hash, PartialEq, Eq)]
77pub enum Type {
78    /// Internal type used solely for type inference
79    Poly(u32),
80
81    /// The expression is a bitvector, currently modeled in the
82    /// logic QF_BV https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt
83    /// This corresponds to Cranelift's Isle type:
84    /// (type Value (primitive Value))
85    BitVector,
86
87    /// Use if the width is known
88    BitVectorWithWidth(usize),
89
90    // Use if the width is unknown after inference, indexed by a
91    // canonical type variable
92    BitVectorUnknown(u32),
93
94    /// The expression is an integer (currently used for ISLE type,
95    /// representing bitwidth)
96    Int,
97
98    /// The expression is a boolean.
99    Bool,
100
101    /// Unit, removed before SMT-Lib
102    Unit,
103}
104
105impl fmt::Display for Type {
106    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
107        match self {
108            Type::Poly(_) => write!(f, "poly"),
109            Type::BitVector => write!(f, "bv"),
110            Type::BitVectorWithWidth(w) => write!(f, "bv{}", *w),
111            Type::BitVectorUnknown(_) => write!(f, "bv"),
112            Type::Int => write!(f, "Int"),
113            Type::Bool => write!(f, "Bool"),
114            Type::Unit => write!(f, "Unit"),
115        }
116    }
117}
118
119impl Type {
120    pub fn is_poly(&self) -> bool {
121        matches!(self, Type::Poly(_))
122    }
123}
124
125/// Type-specified constants
126#[derive(Clone, Debug, PartialEq, Eq)]
127pub struct Const {
128    pub ty: Type,
129    pub value: i128,
130    pub width: usize,
131}
132
133/// Width arguments
134#[derive(Clone, Debug, PartialEq, Eq)]
135pub enum Width {
136    Const(usize),
137    RegWidth,
138}
139
140/// Typed expressions (u32 is the type var)
141#[derive(Clone, Debug, PartialEq, Eq)]
142pub enum Expr {
143    // Terminal nodes
144    Var(String),
145    Const(Const),
146    True,
147    False,
148
149    // Get the width of a bitvector
150    WidthOf(Box<Expr>),
151
152    // Boolean operations
153    Not(Box<Expr>),
154    And(Box<Expr>, Box<Expr>),
155    Or(Box<Expr>, Box<Expr>),
156    Imp(Box<Expr>, Box<Expr>),
157    Eq(Box<Expr>, Box<Expr>),
158    Lte(Box<Expr>, Box<Expr>),
159    Lt(Box<Expr>, Box<Expr>),
160
161    BVSgt(Box<Expr>, Box<Expr>),
162    BVSgte(Box<Expr>, Box<Expr>),
163    BVSlt(Box<Expr>, Box<Expr>),
164    BVSlte(Box<Expr>, Box<Expr>),
165    BVUgt(Box<Expr>, Box<Expr>),
166    BVUgte(Box<Expr>, Box<Expr>),
167    BVUlt(Box<Expr>, Box<Expr>),
168    BVUlte(Box<Expr>, Box<Expr>),
169
170    BVSaddo(Box<Expr>, Box<Expr>),
171
172    // Bitvector operations
173    //      Note: these follow the naming conventions of the SMT theory of bitvectors:
174    //      https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt
175    // Unary operators
176    BVNeg(Box<Expr>),
177    BVNot(Box<Expr>),
178    CLZ(Box<Expr>),
179    CLS(Box<Expr>),
180    Rev(Box<Expr>),
181    BVPopcnt(Box<Expr>),
182
183    // Binary operators
184    BVMul(Box<Expr>, Box<Expr>),
185    BVUDiv(Box<Expr>, Box<Expr>),
186    BVSDiv(Box<Expr>, Box<Expr>),
187    BVAdd(Box<Expr>, Box<Expr>),
188    BVSub(Box<Expr>, Box<Expr>),
189    BVUrem(Box<Expr>, Box<Expr>),
190    BVSrem(Box<Expr>, Box<Expr>),
191    BVAnd(Box<Expr>, Box<Expr>),
192    BVOr(Box<Expr>, Box<Expr>),
193    BVXor(Box<Expr>, Box<Expr>),
194    BVRotl(Box<Expr>, Box<Expr>),
195    BVRotr(Box<Expr>, Box<Expr>),
196    BVShl(Box<Expr>, Box<Expr>),
197    BVShr(Box<Expr>, Box<Expr>),
198    BVAShr(Box<Expr>, Box<Expr>),
199
200    // Includes type
201    BVSubs(Box<Expr>, Box<Expr>, Box<Expr>),
202
203    // Conversions
204    // Zero extend, static and dynamic width
205    BVZeroExtTo(Box<Width>, Box<Expr>),
206    BVZeroExtToVarWidth(Box<Expr>, Box<Expr>),
207
208    // Sign extend, static and dynamic width
209    BVSignExtTo(Box<Width>, Box<Expr>),
210    BVSignExtToVarWidth(Box<Expr>, Box<Expr>),
211
212    // Extract specified bits
213    BVExtract(usize, usize, Box<Expr>),
214
215    // Concat two bitvectors
216    BVConcat(Vec<Expr>),
217
218    // Convert integer to bitvector
219    BVIntToBv(usize, Box<Expr>),
220
221    // Convert bitvector to integer
222    BVToInt(Box<Expr>),
223
224    // Conversion to wider/narrower bits, without an explicit extend
225    // Allow the destination width to be symbolic.
226    BVConvTo(Box<Expr>, Box<Expr>),
227
228    // Conditional if-then-else
229    Conditional(Box<Expr>, Box<Expr>, Box<Expr>),
230
231    // Switch
232    Switch(Box<Expr>, Vec<(Expr, Expr)>),
233
234    LoadEffect(Box<Expr>, Box<Expr>, Box<Expr>),
235
236    StoreEffect(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>),
237}
238
239impl Expr {
240    pub fn var(s: &str) -> Expr {
241        Expr::Var(s.to_string())
242    }
243
244    pub fn unary<F: Fn(Box<Expr>) -> Expr>(f: F, x: Expr) -> Expr {
245        f(Box::new(x))
246    }
247
248    pub fn binary<F: Fn(Box<Expr>, Box<Expr>) -> Expr>(f: F, x: Expr, y: Expr) -> Expr {
249        f(Box::new(x), Box::new(y))
250    }
251}
veri_ir/annotation_ir.rs

veri_ir/
annotation_ir.rs
