veri_engine_lib/solver/encoded_ops/
rev.rs

1use crate::solver::SolverCtx;
2use easy_smt::SExpr;
3
4// Future work: possibly move these into the annotation language or an SMTLIB prelude
5
6pub fn rev64(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
7    // Generated code.
8    let x1 = solver.declare(
9        format!("x1_{id}", id = id),
10        solver.smt.list(vec![
11            solver.smt.atoms().und,
12            solver.smt.atom("BitVec"),
13            solver.smt.numeral(64),
14        ]),
15    );
16    solver.assume(solver.smt.eq(
17        x1,
18        solver.smt.bvor(
19            solver.smt.bvlshr(x, solver.smt.atom("#x0000000000000020")),
20            solver.smt.bvshl(x, solver.smt.atom("#x0000000000000020")),
21        ),
22    ));
23    let x2 = solver.declare(
24        format!("x2_{id}", id = id),
25        solver.smt.list(vec![
26            solver.smt.atoms().und,
27            solver.smt.atom("BitVec"),
28            solver.smt.numeral(64),
29        ]),
30    );
31    solver.assume(solver.smt.eq(
32        x2,
33        solver.smt.bvor(
34            solver.smt.bvlshr(
35                solver.smt.bvand(x1, solver.smt.atom("#xffff0000ffff0000")),
36                solver.smt.atom("#x0000000000000010"),
37            ),
38            solver.smt.bvshl(
39                solver.smt.bvand(x1, solver.smt.atom("#x0000ffff0000ffff")),
40                solver.smt.atom("#x0000000000000010"),
41            ),
42        ),
43    ));
44    let x3 = solver.declare(
45        format!("x3_{id}", id = id),
46        solver.smt.list(vec![
47            solver.smt.atoms().und,
48            solver.smt.atom("BitVec"),
49            solver.smt.numeral(64),
50        ]),
51    );
52    solver.assume(solver.smt.eq(
53        x3,
54        solver.smt.bvor(
55            solver.smt.bvlshr(
56                solver.smt.bvand(x2, solver.smt.atom("#xff00ff00ff00ff00")),
57                solver.smt.atom("#x0000000000000008"),
58            ),
59            solver.smt.bvshl(
60                solver.smt.bvand(x2, solver.smt.atom("#x00ff00ff00ff00ff")),
61                solver.smt.atom("#x0000000000000008"),
62            ),
63        ),
64    ));
65    let x4 = solver.declare(
66        format!("x4_{id}", id = id),
67        solver.smt.list(vec![
68            solver.smt.atoms().und,
69            solver.smt.atom("BitVec"),
70            solver.smt.numeral(64),
71        ]),
72    );
73    solver.assume(solver.smt.eq(
74        x4,
75        solver.smt.bvor(
76            solver.smt.bvlshr(
77                solver.smt.bvand(x3, solver.smt.atom("#xf0f0f0f0f0f0f0f0")),
78                solver.smt.atom("#x0000000000000004"),
79            ),
80            solver.smt.bvshl(
81                solver.smt.bvand(x3, solver.smt.atom("#x0f0f0f0f0f0f0f0f")),
82                solver.smt.atom("#x0000000000000004"),
83            ),
84        ),
85    ));
86    let x5 = solver.declare(
87        format!("x5_{id}", id = id),
88        solver.smt.list(vec![
89            solver.smt.atoms().und,
90            solver.smt.atom("BitVec"),
91            solver.smt.numeral(64),
92        ]),
93    );
94    solver.assume(solver.smt.eq(
95        x5,
96        solver.smt.bvor(
97            solver.smt.bvlshr(
98                solver.smt.bvand(x4, solver.smt.atom("#xcccccccccccccccc")),
99                solver.smt.atom("#x0000000000000002"),
100            ),
101            solver.smt.bvshl(
102                solver.smt.bvand(x4, solver.smt.atom("#x3333333333333333")),
103                solver.smt.atom("#x0000000000000002"),
104            ),
105        ),
106    ));
107    let rev64ret = solver.declare(
108        format!("rev64ret_{id}", id = id),
109        solver.smt.list(vec![
110            solver.smt.atoms().und,
111            solver.smt.atom("BitVec"),
112            solver.smt.numeral(64),
113        ]),
114    );
115    solver.assume(solver.smt.eq(
116        rev64ret,
117        solver.smt.bvor(
118            solver.smt.bvlshr(
119                solver.smt.bvand(x5, solver.smt.atom("#xaaaaaaaaaaaaaaaa")),
120                solver.smt.atom("#x0000000000000001"),
121            ),
122            solver.smt.bvshl(
123                solver.smt.bvand(x5, solver.smt.atom("#x5555555555555555")),
124                solver.smt.atom("#x0000000000000001"),
125            ),
126        ),
127    ));
128
129    rev64ret
130}
131
132pub fn rev32(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
133    let x = solver.smt.extract(31, 0, x);
134
135    // Generated code.
136    let x1 = solver.declare(
137        format!("x1_{id}", id = id),
138        solver.smt.list(vec![
139            solver.smt.atoms().und,
140            solver.smt.atom("BitVec"),
141            solver.smt.numeral(32),
142        ]),
143    );
144    solver.assume(solver.smt.eq(
145        x1,
146        solver.smt.bvor(
147            solver.smt.bvlshr(x, solver.smt.atom("#x00000010")),
148            solver.smt.bvshl(x, solver.smt.atom("#x00000010")),
149        ),
150    ));
151    let x2 = solver.declare(
152        format!("x2_{id}", id = id),
153        solver.smt.list(vec![
154            solver.smt.atoms().und,
155            solver.smt.atom("BitVec"),
156            solver.smt.numeral(32),
157        ]),
158    );
159    solver.assume(solver.smt.eq(
160        x2,
161        solver.smt.bvor(
162            solver.smt.bvlshr(
163                solver.smt.bvand(x1, solver.smt.atom("#xff00ff00")),
164                solver.smt.atom("#x00000008"),
165            ),
166            solver.smt.bvshl(
167                solver.smt.bvand(x1, solver.smt.atom("#x00ff00ff")),
168                solver.smt.atom("#x00000008"),
169            ),
170        ),
171    ));
172    let x3 = solver.declare(
173        format!("x3_{id}", id = id),
174        solver.smt.list(vec![
175            solver.smt.atoms().und,
176            solver.smt.atom("BitVec"),
177            solver.smt.numeral(32),
178        ]),
179    );
180    solver.assume(solver.smt.eq(
181        x3,
182        solver.smt.bvor(
183            solver.smt.bvlshr(
184                solver.smt.bvand(x2, solver.smt.atom("#xf0f0f0f0")),
185                solver.smt.atom("#x00000004"),
186            ),
187            solver.smt.bvshl(
188                solver.smt.bvand(x2, solver.smt.atom("#x0f0f0f0f")),
189                solver.smt.atom("#x00000004"),
190            ),
191        ),
192    ));
193    let x4 = solver.declare(
194        format!("x4_{id}", id = id),
195        solver.smt.list(vec![
196            solver.smt.atoms().und,
197            solver.smt.atom("BitVec"),
198            solver.smt.numeral(32),
199        ]),
200    );
201    solver.assume(solver.smt.eq(
202        x4,
203        solver.smt.bvor(
204            solver.smt.bvlshr(
205                solver.smt.bvand(x3, solver.smt.atom("#xcccccccc")),
206                solver.smt.atom("#x00000002"),
207            ),
208            solver.smt.bvshl(
209                solver.smt.bvand(x3, solver.smt.atom("#x33333333")),
210                solver.smt.atom("#x00000002"),
211            ),
212        ),
213    ));
214    let rev32ret = solver.declare(
215        format!("rev32ret_{id}", id = id),
216        solver.smt.list(vec![
217            solver.smt.atoms().und,
218            solver.smt.atom("BitVec"),
219            solver.smt.numeral(32),
220        ]),
221    );
222    solver.assume(solver.smt.eq(
223        rev32ret,
224        solver.smt.bvor(
225            solver.smt.bvlshr(
226                solver.smt.bvand(x4, solver.smt.atom("#xaaaaaaaa")),
227                solver.smt.atom("#x00000001"),
228            ),
229            solver.smt.bvshl(
230                solver.smt.bvand(x4, solver.smt.atom("#x55555555")),
231                solver.smt.atom("#x00000001"),
232            ),
233        ),
234    ));
235
236    rev32ret
237}
238
239pub fn rev16(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
240    let x = solver.smt.extract(15, 0, x);
241
242    // Generated code.
243    let x1 = solver.declare(
244        format!("x1_{id}", id = id),
245        solver.smt.list(vec![
246            solver.smt.atoms().und,
247            solver.smt.atom("BitVec"),
248            solver.smt.numeral(16),
249        ]),
250    );
251    solver.assume(solver.smt.eq(
252        x1,
253        solver.smt.bvor(
254            solver.smt.bvlshr(x, solver.smt.atom("#x0008")),
255            solver.smt.bvshl(x, solver.smt.atom("#x0008")),
256        ),
257    ));
258    let x2 = solver.declare(
259        format!("x2_{id}", id = id),
260        solver.smt.list(vec![
261            solver.smt.atoms().und,
262            solver.smt.atom("BitVec"),
263            solver.smt.numeral(16),
264        ]),
265    );
266    solver.assume(solver.smt.eq(
267        x2,
268        solver.smt.bvor(
269            solver.smt.bvlshr(
270                solver.smt.bvand(x1, solver.smt.atom("#xf0f0")),
271                solver.smt.atom("#x0004"),
272            ),
273            solver.smt.bvshl(
274                solver.smt.bvand(x1, solver.smt.atom("#x0f0f")),
275                solver.smt.atom("#x0004"),
276            ),
277        ),
278    ));
279    let x3 = solver.declare(
280        format!("x3_{id}", id = id),
281        solver.smt.list(vec![
282            solver.smt.atoms().und,
283            solver.smt.atom("BitVec"),
284            solver.smt.numeral(16),
285        ]),
286    );
287    solver.assume(solver.smt.eq(
288        x3,
289        solver.smt.bvor(
290            solver.smt.bvlshr(
291                solver.smt.bvand(x2, solver.smt.atom("#xcccc")),
292                solver.smt.atom("#x0002"),
293            ),
294            solver.smt.bvshl(
295                solver.smt.bvand(x2, solver.smt.atom("#x3333")),
296                solver.smt.atom("#x0002"),
297            ),
298        ),
299    ));
300    let rev16ret = solver.declare(
301        format!("rev16ret_{id}", id = id),
302        solver.smt.list(vec![
303            solver.smt.atoms().und,
304            solver.smt.atom("BitVec"),
305            solver.smt.numeral(16),
306        ]),
307    );
308    solver.assume(solver.smt.eq(
309        rev16ret,
310        solver.smt.bvor(
311            solver.smt.bvlshr(
312                solver.smt.bvand(x3, solver.smt.atom("#xaaaa")),
313                solver.smt.atom("#x0001"),
314            ),
315            solver.smt.bvshl(
316                solver.smt.bvand(x3, solver.smt.atom("#x5555")),
317                solver.smt.atom("#x0001"),
318            ),
319        ),
320    ));
321
322    let padding = solver.new_fresh_bits(solver.bitwidth - 16);
323    solver.smt.concat(padding, rev16ret)
324}
325
326pub fn rev8(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
327    let x = solver.smt.extract(7, 0, x);
328
329    // Generated code.
330    let x1 = solver.declare(
331        format!("x1_{id}", id = id),
332        solver.smt.list(vec![
333            solver.smt.atoms().und,
334            solver.smt.atom("BitVec"),
335            solver.smt.numeral(8),
336        ]),
337    );
338    solver.assume(solver.smt.eq(
339        x1,
340        solver.smt.bvor(
341            solver.smt.bvlshr(x, solver.smt.atom("#x04")),
342            solver.smt.bvshl(x, solver.smt.atom("#x04")),
343        ),
344    ));
345    let x2 = solver.declare(
346        format!("x2_{id}", id = id),
347        solver.smt.list(vec![
348            solver.smt.atoms().und,
349            solver.smt.atom("BitVec"),
350            solver.smt.numeral(8),
351        ]),
352    );
353    solver.assume(solver.smt.eq(
354        x2,
355        solver.smt.bvor(
356            solver.smt.bvlshr(
357                solver.smt.bvand(x1, solver.smt.atom("#xcc")),
358                solver.smt.atom("#x02"),
359            ),
360            solver.smt.bvshl(
361                solver.smt.bvand(x1, solver.smt.atom("#x33")),
362                solver.smt.atom("#x02"),
363            ),
364        ),
365    ));
366    let rev8ret = solver.declare(
367        format!("rev8ret_{id}", id = id),
368        solver.smt.list(vec![
369            solver.smt.atoms().und,
370            solver.smt.atom("BitVec"),
371            solver.smt.numeral(8),
372        ]),
373    );
374    solver.assume(solver.smt.eq(
375        rev8ret,
376        solver.smt.bvor(
377            solver.smt.bvlshr(
378                solver.smt.bvand(x2, solver.smt.atom("#xaa")),
379                solver.smt.atom("#x01"),
380            ),
381            solver.smt.bvshl(
382                solver.smt.bvand(x2, solver.smt.atom("#x55")),
383                solver.smt.atom("#x01"),
384            ),
385        ),
386    ));
387
388    let padding = solver.new_fresh_bits(solver.bitwidth - 8);
389    solver.smt.concat(padding, rev8ret)
390}
391
392pub fn rev1(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
393    let x = solver.smt.extract(0, 0, x);
394
395    // Generated code.
396    let rev1ret = solver.declare(
397        format!("rev1ret_{id}", id = id),
398        solver.smt.list(vec![
399            solver.smt.atoms().und,
400            solver.smt.atom("BitVec"),
401            solver.smt.numeral(1),
402        ]),
403    );
404    solver.assume(solver.smt.eq(rev1ret, x));
405
406    let padding = solver.new_fresh_bits(solver.bitwidth - 1);
407    solver.smt.concat(padding, rev1ret)
408}
veri_engine_lib/solver/encoded_ops/rev.rs

veri_engine_lib/solver/encoded_ops/
rev.rs
