rustproof_libsmt/theories/
bitvec.rs

1//! Defines basic operations defined under FixedSizeBitVectors theory in SMTLIB2.
2
3use std::fmt;
4
5use backends::backend::SMTNode;
6
7#[macro_export]
8macro_rules! bv_const {
9    ($solver: ident, $i: expr, $n: expr) => { $solver.new_const(bitvec::OpCodes::Const($i, $n)) }
10}
11
12#[derive(Clone, Debug)]
13pub enum OpCodes {
14    Concat,
15    Extract(u64, u64),
16    BvNot,
17    BvAnd,
18    BvOr,
19    BvNeg,
20    BvAdd,
21    BvMul,
22    BvSMulDoesNotOverflow,
23    BvSMulDoesNotUnderflow,
24    BvUMulDoesNotOverflow,
25    BvUDiv,
26    BvURem,
27    BvShl,
28    BvLShr,
29    BvULt,
30    BvNand,
31    BvNor,
32    BvXor,
33    BvXnor,
34    BvComp,
35    BvSub,
36    BvSDiv,
37    BvSRem,
38    BvSMod,
39    BvAShr,
40    // parameterized functions
41    Repeat(u64),
42    ZeroExtend(u64),
43    SignExtend(u64),
44    RotateLeft(u64),
45    RotateRight(u64),
46    // logical functions
47    BvULe,
48    BvUGt,
49    BvUGe,
50    BvSLt,
51    BvSLe,
52    BvSGt,
53    BvSGe,
54    Const(u64, usize),
55    FreeVar(String),
56}
57
58impl fmt::Display for OpCodes {
59    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
60        let s = match *self {
61            OpCodes::Concat => "concat".to_owned(),
62            OpCodes::Extract(i, j) => format!("(_ extract {} {})", i, j),
63            OpCodes::BvNot => "bvnot".to_owned(),
64            OpCodes::BvAnd => "bvand".to_owned(),
65            OpCodes::BvOr => "bvor".to_owned(),
66            OpCodes::BvNeg => "bvneg".to_owned(),
67            OpCodes::BvAdd => "bvadd".to_owned(),
68            OpCodes::BvMul => "bvmul".to_owned(),
69            OpCodes::BvSMulDoesNotOverflow => "bvsmul_noovfl".to_owned(),
70            OpCodes::BvSMulDoesNotUnderflow => "bvsmul_noudfl".to_owned(),
71            OpCodes::BvUMulDoesNotOverflow => "bvumul_noovfl".to_owned(),
72            OpCodes::BvUDiv => "bvudiv".to_owned(),
73            OpCodes::BvURem => "bvurem".to_owned(),
74            OpCodes::BvShl => "bvshl".to_owned(),
75            OpCodes::BvLShr => "bvlshr".to_owned(),
76            OpCodes::BvULt => "bvult".to_owned(),
77            OpCodes::BvNand => "bvnand".to_owned(),
78            OpCodes::BvNor => "bvnor".to_owned(),
79            OpCodes::BvXor => "bvxor".to_owned(),
80            OpCodes::BvXnor => "bvxnor".to_owned(),
81            OpCodes::BvComp => "bvcomp".to_owned(),
82            OpCodes::BvSub => "bvsub".to_owned(),
83            OpCodes::BvSDiv => "bvsdiv".to_owned(),
84            OpCodes::BvSRem => "bvsrem".to_owned(),
85            OpCodes::BvSMod => "bvsmod".to_owned(),
86            OpCodes::BvAShr => "bvashr".to_owned(),
87            OpCodes::Repeat(i) => format!("(_ repeat {})", i),
88            OpCodes::ZeroExtend(i) => format!("(_ zero_extend {})", i),
89            OpCodes::SignExtend(i) => format!("(_ sign_extend {})", i),
90            OpCodes::RotateLeft(i) => format!("(_ rotate_left {})", i),
91            OpCodes::RotateRight(i) => format!("(_ rotate_right {})", i),
92            OpCodes::BvULe => "bvule".to_owned(),
93            OpCodes::BvUGt => "bvugt".to_owned(),
94            OpCodes::BvUGe => "bvuge".to_owned(),
95            OpCodes::BvSLt => "bvslt".to_owned(),
96            OpCodes::BvSLe => "bvsle".to_owned(),
97            OpCodes::BvSGt => "bvsgt".to_owned(),
98            OpCodes::BvSGe => "bvsge".to_owned(),
99            OpCodes::Const(val, n) => format!("(_ bv{} {})", val, n),
100            OpCodes::FreeVar(ref name) => format!("{}", name),
101        };
102        write!(f, "{}", s)
103    }
104}
105
106impl_smt_node!(OpCodes, define vars [OpCodes::FreeVar(_)], define consts [OpCodes::Const(_, _)]);
107
108#[derive(Clone, Debug)]
109pub enum Sorts {
110    BitVector(usize),
111    Bool,
112}
113
114impl fmt::Display for Sorts {
115    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
116        let s = match *self {
117            Sorts::BitVector(ref n) => format!("(_ BitVec {})", n),
118            Sorts::Bool => format!("{}", "bool"),
119        };
120        write!(f, "{}", s)
121    }
122}
rustproof_libsmt/theories/bitvec.rs

rustproof_libsmt/theories/
bitvec.rs
