charon_lib/transform/resugar/reconstruct_fallible_operations.rs
1//! # Micro-pass: remove the dynamic checks for array/slice bounds, overflow, and division by zero.
2//! Note that from a semantic point of view, an out-of-bound access or a division by zero
3//! must lead to a panic in Rust (which is why those checks are always present, even when
4//! compiling for release). In our case, we take this into account in the semantics of our
5//! array/slice manipulation and arithmetic functions, on the verification side.
6
7use derive_generic_visitor::*;
8
9use crate::ast::*;
10use crate::transform::TransformCtx;
11use crate::ullbc_ast::{ExprBody, Statement, StatementKind};
12
13use crate::transform::ctx::UllbcPass;
14
15/// Whether the value uses the given local in a place.
16fn uses_local<T: BodyVisitable>(x: &T, local: LocalId) -> bool {
17 struct FoundIt;
18 struct UsesLocalVisitor(LocalId);
19
20 impl Visitor for UsesLocalVisitor {
21 type Break = FoundIt;
22 }
23 impl VisitBody for UsesLocalVisitor {
24 fn visit_place(&mut self, x: &Place) -> ::std::ops::ControlFlow<Self::Break> {
25 if let Some(local_id) = x.as_local() {
26 if local_id == self.0 {
27 return ControlFlow::Break(FoundIt);
28 }
29 }
30 self.visit_inner(x)
31 }
32 }
33
34 x.drive_body(&mut UsesLocalVisitor(local)).is_break()
35}
36
37fn make_binop_overflow_panic<T: BodyVisitable>(
38 x: &mut [T],
39 matches: impl Fn(&BinOp, &Operand, &Operand) -> bool,
40) -> bool {
41 let mut found = false;
42 for y in x.iter_mut() {
43 y.dyn_visit_in_body_mut(|rv: &mut Rvalue| {
44 if let Rvalue::BinaryOp(binop, op_l, op_r) = rv
45 && matches(binop, op_l, op_r)
46 {
47 *binop = binop.with_overflow(OverflowMode::Panic);
48 found = true;
49 }
50 });
51 }
52 found
53}
54
55fn make_unop_overflow_panic<T: BodyVisitable>(
56 x: &mut [T],
57 matches: impl Fn(&UnOp, &Operand) -> bool,
58) -> bool {
59 let mut found = false;
60 for y in x.iter_mut() {
61 y.dyn_visit_in_body_mut(|rv: &mut Rvalue| {
62 if let Rvalue::UnaryOp(unop, op) = rv
63 && matches(unop, op)
64 {
65 *unop = unop.with_overflow(OverflowMode::Panic);
66 found = true;
67 }
68 });
69 }
70 found
71}
72
73/// Check if the two operands are equivalent: either they're the same constant, or they represent
74/// the same place (regardless of whether the operand is a move or a copy)
75fn equiv_op(op_l: &Operand, op_r: &Operand) -> bool {
76 match (op_l, op_r) {
77 (Operand::Copy(l) | Operand::Move(l), Operand::Copy(r) | Operand::Move(r)) => l == r,
78 (Operand::Const(l), Operand::Const(r)) => l == r,
79 _ => false,
80 }
81}
82
83/// Rustc inserts dynamic checks during MIR lowering. They all end in an `Assert` statement (and
84/// this is the only use of this statement).
85fn remove_dynamic_checks(
86 _ctx: &mut TransformCtx,
87 locals: &mut Locals,
88 statements: &mut [Statement],
89) {
90 // We return the statements we want to keep, which must be a prefix of `block.statements`.
91 let statements_to_keep = match statements {
92 // Bounds checks for slices. They look like:
93 // l := use(copy a.metadata)
94 // b := copy x < copy l
95 // assert(move b == true)
96 [
97 Statement {
98 kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op))),
99 ..
100 },
101 Statement {
102 kind:
103 StatementKind::Assign(
104 is_in_bounds,
105 Rvalue::BinaryOp(BinOp::Lt, _, Operand::Copy(lt_op2)),
106 ),
107 ..
108 },
109 Statement {
110 kind:
111 StatementKind::Assert(Assert {
112 cond: Operand::Move(cond),
113 expected: true,
114 ..
115 }),
116 ..
117 },
118 rest @ ..,
119 ] if lt_op2 == len
120 && cond == is_in_bounds
121 && let Some((_, ProjectionElem::PtrMetadata)) = len_op.as_projection() =>
122 {
123 rest
124 }
125 // Sometimes that instead looks like:
126 // a := &raw const *z
127 // l := use(copy a.metadata)
128 // b := copy x < copy l
129 // assert(move b == true)
130 [
131 Statement {
132 kind:
133 StatementKind::Assign(
134 reborrow,
135 Rvalue::RawPtr {
136 kind: RefKind::Shared,
137 ..
138 },
139 ),
140 ..
141 },
142 Statement {
143 kind: StatementKind::Assign(len, Rvalue::Use(Operand::Copy(len_op))),
144 ..
145 },
146 Statement {
147 kind:
148 StatementKind::Assign(
149 is_in_bounds,
150 Rvalue::BinaryOp(BinOp::Lt, _, Operand::Copy(lt_op2)),
151 ),
152 ..
153 },
154 Statement {
155 kind:
156 StatementKind::Assert(Assert {
157 cond: Operand::Move(cond),
158 expected: true,
159 ..
160 }),
161 ..
162 },
163 rest @ ..,
164 ] if lt_op2 == len
165 && cond == is_in_bounds
166 && let Some((slice_place, ProjectionElem::PtrMetadata)) = len_op.as_projection()
167 && reborrow == slice_place =>
168 {
169 rest
170 }
171
172 // Zero checks for division and remainder. They look like:
173 // b := copy y == const 0
174 // assert(move b == false)
175 // ...
176 // res := x {/,%} move y;
177 // ... or ...
178 // b := const y == const 0
179 // assert(move b == false)
180 // ...
181 // res := x {/,%} const y;
182 //
183 // This also overlaps with overflow checks for negation, which looks like:
184 // is_min := x == INT::min
185 // assert(move is_min == false)
186 // ...
187 // res := -x;
188 [
189 Statement {
190 kind:
191 StatementKind::Assign(
192 is_zero,
193 Rvalue::BinaryOp(BinOp::Eq, y_op, Operand::Const(_zero)),
194 ),
195 ..
196 },
197 Statement {
198 kind:
199 StatementKind::Assert(Assert {
200 cond: Operand::Move(cond),
201 expected: false,
202 ..
203 }),
204 ..
205 },
206 rest @ ..,
207 ] if cond == is_zero => {
208 let found = make_binop_overflow_panic(rest, |bop, _, r| {
209 matches!(bop, BinOp::Div(_) | BinOp::Rem(_)) && equiv_op(r, y_op)
210 }) || make_unop_overflow_panic(rest, |unop, o| {
211 matches!(unop, UnOp::Neg(_)) && equiv_op(o, y_op)
212 });
213 if found {
214 rest
215 } else {
216 return;
217 }
218 }
219
220 // Overflow checks for signed division and remainder. They look like:
221 // is_neg_1 := y == (-1)
222 // is_min := x == INT::min
223 // has_overflow := move (is_neg_1) & move (is_min)
224 // assert(move has_overflow == false)
225 // Note here we don't need to update the operand to panic, as this was already done
226 // by the previous pass for division by zero.
227 [
228 Statement {
229 kind: StatementKind::Assign(is_neg_1, Rvalue::BinaryOp(BinOp::Eq, _y_op, _minus_1)),
230 ..
231 },
232 Statement {
233 kind: StatementKind::Assign(is_min, Rvalue::BinaryOp(BinOp::Eq, _x_op, _int_min)),
234 ..
235 },
236 Statement {
237 kind:
238 StatementKind::Assign(
239 has_overflow,
240 Rvalue::BinaryOp(
241 BinOp::BitAnd,
242 Operand::Move(and_op1),
243 Operand::Move(and_op2),
244 ),
245 ),
246 ..
247 },
248 Statement {
249 kind:
250 StatementKind::Assert(Assert {
251 cond: Operand::Move(cond),
252 expected: false,
253 ..
254 }),
255 ..
256 },
257 rest @ ..,
258 ] if and_op1 == is_neg_1 && and_op2 == is_min && cond == has_overflow => rest,
259
260 // Overflow checks for right/left shift. They can look like:
261 // a := y as u32; // or another type
262 // b := move a < const 32; // or another constant
263 // assert(move b == true);
264 // ...
265 // res := x {<<,>>} y;
266 [
267 Statement {
268 kind: StatementKind::Assign(cast, Rvalue::UnaryOp(UnOp::Cast(_), y_op)),
269 ..
270 },
271 Statement {
272 kind:
273 StatementKind::Assign(
274 has_overflow,
275 Rvalue::BinaryOp(BinOp::Lt, Operand::Move(lhs), Operand::Const(..)),
276 ),
277 ..
278 },
279 Statement {
280 kind:
281 StatementKind::Assert(Assert {
282 cond: Operand::Move(cond),
283 expected: true,
284 ..
285 }),
286 ..
287 },
288 rest @ ..,
289 ] if cond == has_overflow
290 && lhs == cast
291 && let Some(cast_local) = cast.as_local()
292 && !rest.iter().any(|st| uses_local(st, cast_local)) =>
293 {
294 let found = make_binop_overflow_panic(rest, |bop, _, r| {
295 matches!(bop, BinOp::Shl(_) | BinOp::Shr(_)) && equiv_op(r, y_op)
296 });
297 if found {
298 rest
299 } else {
300 return;
301 }
302 }
303 // or like:
304 // b := y < const 32; // or another constant
305 // assert(move b == true);
306 // ...
307 // res := x {<<,>>} y;
308 //
309 // this also overlaps with out of bounds checks for arrays, so we check for either;
310 // these look like:
311 // b := copy y < const _
312 // assert(move b == true)
313 // ...
314 // res := a[y];
315 [
316 Statement {
317 kind:
318 StatementKind::Assign(
319 has_overflow,
320 Rvalue::BinaryOp(BinOp::Lt, y_op, Operand::Const(..)),
321 ),
322 ..
323 },
324 Statement {
325 kind:
326 StatementKind::Assert(Assert {
327 cond: Operand::Move(cond),
328 expected: true,
329 ..
330 }),
331 ..
332 },
333 rest @ ..,
334 ] if cond == has_overflow => {
335 // look for a shift operation
336 let mut found = make_binop_overflow_panic(rest, |bop, _, r| {
337 matches!(bop, BinOp::Shl(_) | BinOp::Shr(_)) && equiv_op(r, y_op)
338 });
339 if !found {
340 // otherwise, look for an array access
341 for stmt in rest.iter_mut() {
342 stmt.dyn_visit_in_body(|p: &Place| {
343 if let Some((_, ProjectionElem::Index { offset, .. })) = p.as_projection()
344 && equiv_op(offset, y_op)
345 {
346 found = true;
347 }
348 });
349 }
350 }
351
352 if found {
353 rest
354 } else {
355 return;
356 }
357 }
358
359 // Overflow checks for addition/subtraction/multiplication. They look like:
360 // ```text
361 // r := x checked.+ y;
362 // assert(move r.1 == false);
363 // ...
364 // z := move r.0;
365 // ```
366 // We replace that with:
367 // ```text
368 // z := x + y;
369 // ```
370 //
371 // But sometimes, because of constant promotion, we end up with a lone checked operation
372 // without assert. In that case we replace it with its wrapping equivalent.
373 [
374 Statement {
375 kind:
376 StatementKind::Assign(
377 tuple,
378 Rvalue::BinaryOp(
379 binop @ (BinOp::AddChecked | BinOp::SubChecked | BinOp::MulChecked),
380 _,
381 _,
382 ),
383 ),
384 ..
385 },
386 rest @ ..,
387 ] if let Some(tuple_local_id) = tuple.as_local() => {
388 // Check if the result boolean is used in any other way than just getting the integer
389 // result.
390 let mut uses_of_tuple = 0;
391 let mut uses_of_integer = 0;
392 if *tuple == locals.return_place() {
393 uses_of_tuple += 1; // The return place counts as a use.
394 }
395 for stmt in rest.iter_mut() {
396 stmt.dyn_visit_in_body(|p: &Place| {
397 if p == tuple {
398 uses_of_tuple += 1;
399 }
400 if let Some((sub, ProjectionElem::Field(FieldProjKind::Tuple(..), fid))) =
401 p.as_projection()
402 && fid.index() == 0
403 && sub == tuple
404 {
405 uses_of_integer += 1;
406 }
407 });
408 }
409 // Check if the operation is followed by an assert.
410 let followed_by_assert = if let [
411 Statement {
412 kind:
413 StatementKind::Assert(Assert {
414 cond: Operand::Move(assert_cond),
415 expected: false,
416 ..
417 }),
418 ..
419 },
420 ..,
421 ] = rest
422 && let Some((sub, ProjectionElem::Field(FieldProjKind::Tuple(..), fid))) =
423 assert_cond.as_projection()
424 && fid.index() == 1
425 && sub == tuple
426 {
427 true
428 } else {
429 false
430 };
431 if uses_of_tuple != uses_of_integer && !followed_by_assert {
432 // The tuple is used either directly or for the overflow check; we change nothing.
433 return;
434 }
435
436 if followed_by_assert {
437 // We have a compiler-emitted assert. We replace the operation with one that has
438 // panic-on-overflow semantics.
439 *binop = binop.with_overflow(OverflowMode::Panic);
440 // The failure behavior is part of the binop now, so we remove the assert.
441 rest[0].kind = StatementKind::Nop;
442 } else {
443 // The tuple is used exclusively to access the integer result, so we replace the
444 // operation with wrapping semantics.
445 *binop = binop.with_overflow(OverflowMode::Wrap);
446 }
447 // Fixup the local type.
448 let result_local = &mut locals.locals[tuple_local_id];
449 result_local.ty = result_local.ty.as_tuple().unwrap()[0].clone();
450 // Fixup the place type.
451 let new_result_place = locals.place_for_var(tuple_local_id);
452 // Replace uses of `r.0` with `r`.
453 for stmt in rest.iter_mut() {
454 stmt.dyn_visit_in_body_mut(|p: &mut Place| {
455 if let Some((sub, ProjectionElem::Field(FieldProjKind::Tuple(..), fid))) =
456 p.as_projection()
457 && sub == tuple
458 {
459 assert_eq!(fid.index(), 0);
460 *p = new_result_place.clone()
461 }
462 });
463 }
464 *tuple = new_result_place;
465 return;
466 }
467
468 _ => return,
469 };
470
471 // Remove the statements we're not keeping.
472 let keep_len = statements_to_keep.len();
473 for i in 0..statements.len() - keep_len {
474 statements[i].kind = StatementKind::Nop;
475 }
476}
477
478pub struct Transform;
479impl UllbcPass for Transform {
480 fn transform_body(&self, ctx: &mut TransformCtx, b: &mut ExprBody) {
481 b.transform_sequences_fwd(|locals, seq| {
482 remove_dynamic_checks(ctx, locals, seq);
483 Vec::new()
484 });
485 }
486}