veri_ir/
lib.rs

1//! Verification Intermediate Representation for relevant types, eventually to
2//! be lowered to SMT. The goal is to leave some freedom to change term
3//! encodings or the specific solver backend.
4//!
5//! Note: annotations use the higher-level IR in annotation_ir.rs.
6pub mod annotation_ir;
7use core::fmt;
8use std::collections::HashMap;
9
10#[derive(Clone, Debug, PartialEq, Eq)]
11pub struct TypeContext {
12    pub tyvars: HashMap<Expr, u32>,
13    pub tymap: HashMap<u32, Type>,
14    pub tyvals: HashMap<u32, i128>,
15    // map of type var to set index
16    pub bv_unknown_width_sets: HashMap<u32, u32>,
17}
18
19// Used for providing concrete inputs to test rule semantics
20#[derive(Clone, Debug, PartialEq, Eq)]
21pub struct ConcreteInput {
22    // SMT-LIB-formatted bitvector literal
23    pub literal: String,
24    pub ty: Type,
25}
26#[derive(Clone, Debug, PartialEq, Eq)]
27pub struct ConcreteTest {
28    pub termname: String,
29    // List of name, bitvector literal, widths
30    pub args: Vec<ConcreteInput>,
31    pub output: ConcreteInput,
32}
33
34/// A bound variable, including the VIR type
35#[derive(Clone, Debug, PartialEq, Eq, Hash)]
36pub struct BoundVar {
37    pub name: String,
38    pub tyvar: u32,
39}
40
41/// Verification type
42#[derive(Clone, Debug, PartialEq, Eq, Hash, Copy)]
43pub enum Type {
44    /// The expression is a bitvector, currently modeled in the
45    /// logic QF_BV https://SMT-LIB.cs.uiowa.edu/version1/logics/QF_BV.smt
46    /// This corresponds to Cranelift's Isle type:
47    /// (type Value (primitive Value))
48    BitVector(Option<usize>),
49
50    /// The expression is a boolean. This does not directly correspond
51    /// to a specific Cranelift Isle type, rather, we use it for the
52    /// language of assertions.
53    Bool,
54
55    /// The expression is an Isle type. This is separate from BitVector
56    /// because it allows us to use a different solver type (e.h., Int)
57    //. for assertions (e.g., fits_in_64).
58    /// This corresponds to Cranelift's Isle type:
59    /// (type Type (primitive Type))
60    Int,
61
62    Unit,
63}
64
65impl fmt::Display for Type {
66    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
67        match self {
68            Type::BitVector(None) => write!(f, "bv"),
69            Type::BitVector(Some(s)) => write!(f, "(bv {})", *s),
70            Type::Bool => write!(f, "Bool"),
71            Type::Int => write!(f, "Int"),
72            Type::Unit => write!(f, "Unit"),
73        }
74    }
75}
76
77#[derive(Clone, Debug, PartialEq, Eq, Hash)]
78pub struct TermSignature {
79    pub args: Vec<Type>,
80    pub ret: Type,
81
82    // Which type varies for different bitwidth Values, that is, the type that
83    // is used as a key for testing for that type.
84    pub canonical_type: Option<Type>,
85}
86
87impl fmt::Display for TermSignature {
88    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
89        let args = self
90            .args
91            .iter()
92            .map(|a| a.to_string())
93            .collect::<Vec<_>>()
94            .join(" ");
95        let canon = self
96            .canonical_type
97            .map(|c| format!("(canon {})", c))
98            .unwrap_or_default();
99        write!(f, "((args {}) (ret {}) {})", args, self.ret, canon)
100    }
101}
102
103#[derive(Clone, Debug, PartialEq, Eq, Hash)]
104pub enum Terminal {
105    Var(String),
106
107    // Literal SMT value, for testing (plus type variable)
108    Literal(String, u32),
109
110    // Value, type variable
111    Const(i128, u32),
112    True,
113    False,
114    Wildcard(u32),
115}
116
117#[derive(Clone, Debug, PartialEq, Eq, Hash)]
118pub enum UnaryOp {
119    // Boolean operations
120    Not,
121
122    // Bitvector operations
123    BVNeg,
124    BVNot,
125}
126
127#[derive(Clone, Debug, PartialEq, Eq, Hash)]
128pub enum BinaryOp {
129    // Boolean operations
130    And,
131    Or,
132    Imp,
133    Eq,
134    Lte,
135    Lt,
136
137    // Bitvector operations
138    BVSgt,
139    BVSgte,
140    BVSlt,
141    BVSlte,
142    BVUgt,
143    BVUgte,
144    BVUlt,
145    BVUlte,
146
147    BVMul,
148    BVUDiv,
149    BVSDiv,
150    BVAdd,
151    BVSub,
152    BVUrem,
153    BVSrem,
154    BVAnd,
155    BVOr,
156    BVXor,
157    BVRotl,
158    BVRotr,
159    BVShl,
160    BVShr,
161    BVAShr,
162
163    BVSaddo,
164}
165
166/// Expressions (combined across all types).
167#[derive(Clone, Debug, PartialEq, Eq, Hash)]
168pub enum Expr {
169    // Terminal nodes
170    Terminal(Terminal),
171
172    // Opcode nodes
173    Unary(UnaryOp, Box<Expr>),
174    Binary(BinaryOp, Box<Expr>, Box<Expr>),
175
176    // Count leading zeros
177    CLZ(Box<Expr>),
178    CLS(Box<Expr>),
179    Rev(Box<Expr>),
180
181    BVPopcnt(Box<Expr>),
182
183    BVSubs(Box<Expr>, Box<Expr>, Box<Expr>),
184
185    // ITE
186    Conditional(Box<Expr>, Box<Expr>, Box<Expr>),
187
188    // Switch
189    Switch(Box<Expr>, Vec<(Expr, Expr)>),
190
191    // Conversions
192    // Extract specified bits
193    BVExtract(usize, usize, Box<Expr>),
194
195    // Concat bitvectors
196    BVConcat(Vec<Expr>),
197
198    // Convert integer to bitvector with that value
199    BVIntToBV(usize, Box<Expr>),
200
201    // Convert bitvector to integer with that value
202    BVToInt(Box<Expr>),
203
204    // Zero extend, with static or dynamic width
205    BVZeroExtTo(usize, Box<Expr>),
206    BVZeroExtToVarWidth(Box<Expr>, Box<Expr>),
207
208    // Sign extend, with static or dynamic width
209    BVSignExtTo(usize, Box<Expr>),
210    BVSignExtToVarWidth(Box<Expr>, Box<Expr>),
211
212    // Conversion to wider/narrower bits, without an explicit extend
213    BVConvTo(Box<Expr>, Box<Expr>),
214
215    WidthOf(Box<Expr>),
216
217    LoadEffect(Box<Expr>, Box<Expr>, Box<Expr>),
218    StoreEffect(Box<Expr>, Box<Expr>, Box<Expr>, Box<Expr>),
219}
220
221impl fmt::Display for Expr {
222    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
223        match self {
224            Expr::Terminal(t) => match t {
225                Terminal::Var(v) => write!(f, "{}", v),
226                Terminal::Literal(v, _) => write!(f, "{}", v),
227                Terminal::Const(c, _) => write!(f, "{}", c),
228                Terminal::True => write!(f, "true"),
229                Terminal::False => write!(f, "false"),
230                Terminal::Wildcard(_) => write!(f, "_"),
231            },
232            Expr::Unary(o, e) => {
233                let op = match o {
234                    UnaryOp::Not => "not",
235                    UnaryOp::BVNeg => "bvneg",
236                    UnaryOp::BVNot => "bvnot",
237                };
238                write!(f, "({} {})", op, e)
239            }
240            Expr::Binary(o, x, y) => {
241                let op = match o {
242                    BinaryOp::And => "and",
243                    BinaryOp::Or => "or",
244                    BinaryOp::Imp => "=>",
245                    BinaryOp::Eq => "=",
246                    BinaryOp::Lte => "<=",
247                    BinaryOp::Lt => "<",
248                    BinaryOp::BVSgt => "bvsgt",
249                    BinaryOp::BVSgte => "bvsgte",
250                    BinaryOp::BVSlt => "bvslt",
251                    BinaryOp::BVSlte => "bvslte",
252                    BinaryOp::BVUgt => "bvugt",
253                    BinaryOp::BVUgte => "bvugte",
254                    BinaryOp::BVUlt => "bvult",
255                    BinaryOp::BVUlte => "bvulte",
256                    BinaryOp::BVMul => "bvmul",
257                    BinaryOp::BVUDiv => "bvudiv",
258                    BinaryOp::BVSDiv => "bvsdiv",
259                    BinaryOp::BVAdd => "bvadd",
260                    BinaryOp::BVSub => "bvsub",
261                    BinaryOp::BVUrem => "bvurem",
262                    BinaryOp::BVSrem => "bvsrem",
263                    BinaryOp::BVAnd => "bvand",
264                    BinaryOp::BVOr => "bvor",
265                    BinaryOp::BVXor => "bvxor",
266                    BinaryOp::BVRotl => "rotl",
267                    BinaryOp::BVRotr => "rotr",
268                    BinaryOp::BVShl => "bvshl",
269                    BinaryOp::BVShr => "bvshr",
270                    BinaryOp::BVAShr => "bvashr",
271                    BinaryOp::BVSaddo => "bvsaddo",
272                };
273                write!(f, "({} {} {})", op, x, y)
274            }
275            Expr::CLZ(e) => write!(f, "(clz {})", e),
276            Expr::CLS(e) => write!(f, "(cls {})", e),
277            Expr::Rev(e) => write!(f, "(rev {})", e),
278            Expr::BVPopcnt(e) => write!(f, "(popcnt {})", e),
279            Expr::BVSubs(t, x, y) => write!(f, "(subs {} {} {})", t, x, y),
280            Expr::Conditional(c, t, e) => write!(f, "(if {} {} {})", c, t, e),
281            Expr::Switch(m, cs) => {
282                let cases: Vec<String> = cs.iter().map(|(c, m)| format!("({} {})", c, m)).collect();
283                write!(f, "(switch {} {})", m, cases.join(""))
284            }
285            Expr::BVExtract(h, l, e) => write!(f, "(extract {} {} {})", *h, *l, e),
286            Expr::BVConcat(es) => {
287                let vs: Vec<String> = es.iter().map(|v| format!("{}", v)).collect();
288                write!(f, "(concat {})", vs.join(""))
289            }
290            Expr::BVIntToBV(t, e) => write!(f, "(int2bv {} {})", t, e),
291            Expr::BVToInt(b) => write!(f, "(bv2int {})", b),
292            Expr::BVZeroExtTo(d, e) => write!(f, "(zero_ext {} {})", *d, e),
293            Expr::BVZeroExtToVarWidth(d, e) => write!(f, "(zero_ext {} {})", d, e),
294            Expr::BVSignExtTo(d, e) => write!(f, "(sign_ext {} {})", *d, e),
295            Expr::BVSignExtToVarWidth(d, e) => write!(f, "(sign_ext {} {})", *d, e),
296            Expr::BVConvTo(x, y) => write!(f, "(conv_to {} {})", x, y),
297            Expr::WidthOf(e) => write!(f, "(widthof {})", e),
298            Expr::LoadEffect(x, y, z) => write!(f, "(load_effect {} {} {})", x, y, z),
299            Expr::StoreEffect(w, x, y, z) => write!(f, "(store_effect {} {} {} {})", w, x, y, z),
300        }
301    }
302}
303
304/// To-be-flushed-out verification counterexample for failures
305#[derive(Clone, Debug, PartialEq, Eq)]
306pub struct Counterexample {}
307
308/// To-be-flushed-out verification result
309#[derive(Clone, Debug, PartialEq, Eq)]
310pub enum VerificationResult {
311    InapplicableRule,
312    Success,
313    Failure(Counterexample),
314    Unknown,
315    // Optional: heuristic that a rule is bad if there is only
316    // a single model with distinct bitvector inputs
317    NoDistinctModels,
318}
veri_ir/lib.rs

veri_ir/
lib.rs
