veri_engine_lib/solver/encoded_ops/
subs.rs

1use crate::solver::SolverCtx;
2use easy_smt::SExpr;
3
4// Future work: likely remove this when we add rule-chaining
5
6// Build the results of a subtraction with flags. Put the 4 flags in the high bits.
7// Encoding adapted from SAIL ISLA: https://github.com/rems-project/isla
8//
9// N: Set to 1 when the result of the operation is negative
10// Z: Set to 1 when the result of the operation is zero
11// C: Set to 1 when the operation results in a carry, or when a subtraction results in no borrow
12// V: Set to 1 when the operation causes overflow
13//
14//   67  66  65  64  63 ...            0
15//  [ N | Z | C | V |   ... result ...  ]
16pub fn subs(s: &mut SolverCtx, ty: usize, x: SExpr, y: SExpr, id: u32) -> SExpr {
17    let id = format!("{ty}_{id}");
18    let (size, wide_size, x, y, zero, one, w_minus_one) = match ty {
19        32 => (
20            s.smt.numeral(32),
21            s.smt.numeral(32 * 2),
22            s.smt.extract(31, 0, x),
23            s.smt.extract(31, 0, y),
24            s.bv(0, 32),
25            s.bv(1, 32 * 2),
26            s.bv(31, 32),
27        ),
28        64 => (
29            s.smt.numeral(64),
30            s.smt.numeral(64 * 2),
31            s.smt.extract(63, 0, x),
32            s.smt.extract(63, 0, y),
33            s.bv(0, 64),
34            s.bv(1, 64 * 2),
35            s.bv(63, 64),
36        ),
37        _ => unreachable!(),
38    };
39
40    let b0 = s.bv(0, 1);
41    let b1 = s.bv(1, 1);
42
43    // (define-const ynot (bvnot y))
44    let ynot = s.declare(
45        format!("ynot_{id}", id = id),
46        s.smt
47            .list(vec![s.smt.atoms().und, s.smt.atom("BitVec"), size]),
48    );
49    s.assume(s.smt.eq(ynot, s.smt.bvnot(y)));
50
51    // (define-const
52    //   subs_wide
53    //   (bvadd (bvadd ((_ zero_extend 64) x) ((_ zero_extend 64) ynot)) #x00000000000000000000000000000001))
54    let subs_wide = s.declare(
55        format!("subs_wide_{id}", id = id),
56        s.smt
57            .list(vec![s.smt.atoms().und, s.smt.atom("BitVec"), wide_size]),
58    );
59    s.assume(s.smt.eq(
60        subs_wide,
61        s.smt.bvadd(
62            s.smt.bvadd(s.zero_extend(ty, x), s.zero_extend(ty, ynot)),
63            one,
64        ),
65    ));
66
67    // (define-const subs ((_ extract 63 0) subs_wide))
68    let subs = s.declare(
69        format!("subs_{id}", id = id),
70        s.smt
71            .list(vec![s.smt.atoms().und, s.smt.atom("BitVec"), size]),
72    );
73    s.assume(s.smt.eq(
74        subs,
75        s.smt.extract((ty - 1).try_into().unwrap(), 0, subs_wide),
76    ));
77
78    // (define-const flags
79    //  (concat (concat (concat
80    //    ((_ extract 0 0) (bvlshr subs #x000000000000003f))
81    //    (ite (= subs #x0000000000000000) #b1 #b0))
82    //    (ite (= ((_ zero_extend 64) subs) subs_wide) #b0 #b1))
83    //    (ite (= ((_ sign_extend 64) subs) (bvadd (bvadd ((_ sign_extend 64) x) ((_ sign_extend 64) ynot)) #x00000000000000000000000000000001)) #b0 #b1)))
84    let flags = s.declare(
85        format!("flags_{id}", id = id),
86        s.smt.list(vec![
87            s.smt.atoms().und,
88            s.smt.atom("BitVec"),
89            s.smt.numeral(4),
90        ]),
91    );
92
93    // N: Set to 1 when the result of the operation is negative
94    // Z: Set to 1 when the result of the operation is zero
95    // C: Set to 1 when the operation results in a carry, or when a subtraction results in no borrow
96    // V: Set to 1 when the operation causes overflow
97    s.assume(
98        s.smt.eq(
99            flags,
100            s.smt.concat(
101                s.smt.concat(
102                    s.smt.concat(
103                        // N flag: result is negative
104                        s.smt.extract(0, 0, s.smt.bvlshr(subs, w_minus_one)),
105                        // Z flag: result is zero
106                        s.smt.ite(s.smt.eq(subs, zero), b1, b0),
107                    ),
108                    // C flag: result has carry/subtraction has no borrow
109                    s.smt
110                        .ite(s.smt.eq(s.zero_extend(ty, subs), subs_wide), b0, b1),
111                ),
112                // V: operation causes overflow
113                s.smt.ite(
114                    s.smt.eq(
115                        s.sign_extend(ty, subs),
116                        s.smt.bvadd(
117                            s.smt.bvadd(s.sign_extend(ty, x), s.sign_extend(ty, ynot)),
118                            one,
119                        ),
120                    ),
121                    b0,
122                    b1,
123                ),
124            ),
125        ),
126    );
127
128    let ret = s.declare(
129        format!("subs_ret_{id}", id = id),
130        s.smt.list(vec![
131            s.smt.atoms().und,
132            s.smt.atom("BitVec"),
133            s.smt.numeral(68),
134        ]),
135    );
136
137    s.assume(s.smt.eq(
138        ret,
139        match ty {
140            // Pad 32 back to full reg width of 64 before adding flags to the left
141            32 => s.smt.concat(flags, s.zero_extend(ty, subs)),
142            64 => s.smt.concat(flags, subs),
143            _ => unreachable!(),
144        },
145    ));
146    ret
147}
veri_engine_lib/solver/encoded_ops/subs.rs

veri_engine_lib/solver/encoded_ops/
subs.rs
