charon_lib/transform/
remove_dynamic_checks.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, RawStatement, Statement};
12
13use super::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
37/// Rustc inserts dybnamic checks during MIR lowering. They all end in an `Assert` statement (and
38/// this is the only use of this statement).
39fn remove_dynamic_checks(
40    _ctx: &mut TransformCtx,
41    locals: &mut Locals,
42    statements: &mut [Statement],
43) {
44    // We return the statements we want to keep, which must be a prefix of `block.statements`.
45    let statements_to_keep = match statements {
46        // Bounds checks for slices. They look like:
47        //   l := ptr_metadata(copy a)
48        //   b := copy x < copy l
49        //   assert(move b == true)
50        [Statement {
51            content:
52                RawStatement::Assign(len, Rvalue::UnaryOp(UnOp::PtrMetadata, Operand::Copy(len_op))),
53            ..
54        }, Statement {
55            content:
56                RawStatement::Assign(
57                    is_in_bounds,
58                    Rvalue::BinaryOp(BinOp::Lt, _, Operand::Copy(lt_op2)),
59                ),
60            ..
61        }, Statement {
62            content:
63                RawStatement::Assert(Assert {
64                    cond: Operand::Move(cond),
65                    expected: true,
66                    ..
67                }),
68            ..
69        }, rest @ ..]
70            if lt_op2 == len && cond == is_in_bounds && len_op.ty().is_ref() =>
71        {
72            rest
73        }
74        // Sometimes that instead looks like:
75        //   a := &raw const *z
76        //   l := ptr_metadata(move a)
77        //   b := copy x < copy l
78        //   assert(move b == true)
79        [Statement {
80            content: RawStatement::Assign(reborrow, Rvalue::RawPtr(_, RefKind::Shared)),
81            ..
82        }, Statement {
83            content:
84                RawStatement::Assign(len, Rvalue::UnaryOp(UnOp::PtrMetadata, Operand::Move(len_op))),
85            ..
86        }, Statement {
87            content:
88                RawStatement::Assign(
89                    is_in_bounds,
90                    Rvalue::BinaryOp(BinOp::Lt, _, Operand::Copy(lt_op2)),
91                ),
92            ..
93        }, Statement {
94            content:
95                RawStatement::Assert(Assert {
96                    cond: Operand::Move(cond),
97                    expected: true,
98                    ..
99                }),
100            ..
101        }, rest @ ..]
102            if reborrow == len_op && lt_op2 == len && cond == is_in_bounds =>
103        {
104            rest
105        }
106
107        // Bounds checks for arrays. They look like:
108        //   b := copy x < const _
109        //   assert(move b == true)
110        [Statement {
111            content:
112                RawStatement::Assign(is_in_bounds, Rvalue::BinaryOp(BinOp::Lt, _, Operand::Const(_))),
113            ..
114        }, Statement {
115            content:
116                RawStatement::Assert(Assert {
117                    cond: Operand::Move(cond),
118                    expected: true,
119                    ..
120                }),
121            ..
122        }, rest @ ..]
123            if cond == is_in_bounds =>
124        {
125            rest
126        }
127
128        // Zero checks for division and remainder. They look like:
129        //   b := copy x == const 0
130        //   assert(move b == false)
131        [Statement {
132            content:
133                RawStatement::Assign(is_zero, Rvalue::BinaryOp(BinOp::Eq, _, Operand::Const(_zero))),
134            ..
135        }, Statement {
136            content:
137                RawStatement::Assert(Assert {
138                    cond: Operand::Move(cond),
139                    expected: false,
140                    ..
141                }),
142            ..
143        }, rest @ ..]
144            if cond == is_zero =>
145        {
146            rest
147        }
148
149        // Overflow checks for signed division and remainder. They look like:
150        //   is_neg_1 := y == (-1)
151        //   is_min := x == INT::min
152        //   has_overflow := move (is_neg_1) & move (is_min)
153        //   assert(move has_overflow == false)
154        [Statement {
155            content: RawStatement::Assign(is_neg_1, Rvalue::BinaryOp(BinOp::Eq, _y_op, _minus_1)),
156            ..
157        }, Statement {
158            content: RawStatement::Assign(is_min, Rvalue::BinaryOp(BinOp::Eq, _x_op, _int_min)),
159            ..
160        }, Statement {
161            content:
162                RawStatement::Assign(
163                    has_overflow,
164                    Rvalue::BinaryOp(BinOp::BitAnd, Operand::Move(and_op1), Operand::Move(and_op2)),
165                ),
166            ..
167        }, Statement {
168            content:
169                RawStatement::Assert(Assert {
170                    cond: Operand::Move(cond),
171                    expected: false,
172                    ..
173                }),
174            ..
175        }, rest @ ..]
176            if and_op1 == is_neg_1 && and_op2 == is_min && cond == has_overflow =>
177        {
178            rest
179        }
180
181        // Overflow checks for right/left shift. They can look like:
182        //   a := _ as u32; // or another type
183        //   b := move a < const 32; // or another constant
184        //   assert(move b == true);
185        [Statement {
186            content: RawStatement::Assign(cast, Rvalue::UnaryOp(UnOp::Cast(_), _)),
187            ..
188        }, Statement {
189            content:
190                RawStatement::Assign(
191                    has_overflow,
192                    Rvalue::BinaryOp(BinOp::Lt, Operand::Move(lhs), Operand::Const(..)),
193                ),
194            ..
195        }, Statement {
196            content:
197                RawStatement::Assert(Assert {
198                    cond: Operand::Move(cond),
199                    expected: true,
200                    ..
201                }),
202            ..
203        }, rest @ ..]
204            if cond == has_overflow
205                && lhs == cast
206                && let Some(cast_local) = cast.as_local()
207                && !rest.iter().any(|st| uses_local(st, cast_local)) =>
208        {
209            rest
210        }
211        // or like:
212        //   b := _ < const 32; // or another constant
213        //   assert(move b == true);
214        [Statement {
215            content:
216                RawStatement::Assign(has_overflow, Rvalue::BinaryOp(BinOp::Lt, _, Operand::Const(..))),
217            ..
218        }, Statement {
219            content:
220                RawStatement::Assert(Assert {
221                    cond: Operand::Move(cond),
222                    expected: true,
223                    ..
224                }),
225            ..
226        }, rest @ ..]
227            if cond == has_overflow =>
228        {
229            rest
230        }
231
232        // Overflow checks for addition/subtraction/multiplication. They look like:
233        // ```text
234        //   r := x checked.+ y;
235        //   assert(move r.1 == false);
236        //   ...
237        //   z := move r.0;
238        // ```
239        // We replace that with:
240        // ```text
241        // z := x + y;
242        // ```
243        //
244        // But sometimes, because of constant promotion, we end up with a lone checked operation
245        // without assert. In that case we replace it with its wrapping equivalent.
246        [Statement {
247            content:
248                RawStatement::Assign(
249                    result,
250                    rval_op @ Rvalue::BinaryOp(
251                        BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul,
252                        _,
253                        _,
254                    ),
255                ),
256            ..
257        }, rest @ ..]
258            if let Some(result_local_id) = result.as_local() =>
259        {
260            // Look for uses of the overflow boolean.
261            let mut overflow_is_used = false;
262            for stmt in rest.iter_mut() {
263                stmt.dyn_visit_in_body(|p: &Place| {
264                    if let Some((sub, ProjectionElem::Field(FieldProjKind::Tuple(..), fid))) =
265                        p.as_projection()
266                        && fid.index() == 1
267                        && sub == result
268                    {
269                        overflow_is_used = true;
270                    }
271                });
272            }
273            // Check if the operation is followed by an assert.
274            let followed_by_assert = if let [Statement {
275                content:
276                    RawStatement::Assert(Assert {
277                        cond: Operand::Move(assert_cond),
278                        expected: false,
279                        ..
280                    }),
281                ..
282            }, ..] = rest
283                && let Some((sub, ProjectionElem::Field(FieldProjKind::Tuple(..), fid))) =
284                    assert_cond.as_projection()
285                && fid.index() == 1
286                && sub == result
287            {
288                true
289            } else {
290                false
291            };
292            if overflow_is_used && !followed_by_assert {
293                // The overflow boolean is used in a way that isn't a builtin overflow check; we
294                // change nothing.
295                return;
296            }
297            let Rvalue::BinaryOp(binop, ..) = rval_op else {
298                unreachable!()
299            };
300            if followed_by_assert {
301                // We have a compiler-emitted assert. We replace the operation with one that has
302                // panic-on-overflow semantics.
303                *binop = match binop {
304                    BinOp::CheckedAdd => BinOp::Add,
305                    BinOp::CheckedSub => BinOp::Sub,
306                    BinOp::CheckedMul => BinOp::Mul,
307                    _ => unreachable!(),
308                };
309                // The failure behavior is part of the binop now, so we remove the assert.
310                rest[0].content = RawStatement::Nop;
311            } else {
312                // The overflow boolean is not used, we replace the operations with wrapping
313                // semantics.
314                *binop = match binop {
315                    BinOp::CheckedAdd => BinOp::WrappingAdd,
316                    BinOp::CheckedSub => BinOp::WrappingSub,
317                    BinOp::CheckedMul => BinOp::WrappingMul,
318                    _ => unreachable!(),
319                };
320            }
321            // Fixup the local type.
322            let result_local = &mut locals.locals[result_local_id];
323            result_local.ty = result_local.ty.as_tuple().unwrap()[0].clone();
324            // Fixup the place type.
325            let new_result_place = locals.place_for_var(result_local_id);
326            // Replace uses of `r.0` with `r`.
327            for stmt in rest.iter_mut() {
328                stmt.dyn_visit_in_body_mut(|p: &mut Place| {
329                    if let Some((sub, ProjectionElem::Field(FieldProjKind::Tuple(..), fid))) =
330                        p.as_projection()
331                        && sub == result
332                    {
333                        assert_eq!(fid.index(), 0);
334                        *p = new_result_place.clone()
335                    }
336                });
337            }
338            *result = new_result_place;
339            return;
340        }
341
342        _ => return,
343    };
344
345    // Remove the statements we're not keeping.
346    let keep_len = statements_to_keep.len();
347    for i in 0..statements.len() - keep_len {
348        statements[i].content = RawStatement::Nop;
349    }
350}
351
352pub struct Transform;
353impl UllbcPass for Transform {
354    fn transform_body(&self, ctx: &mut TransformCtx, b: &mut ExprBody) {
355        b.transform_sequences_fwd(|locals, seq| {
356            remove_dynamic_checks(ctx, locals, seq);
357            Vec::new()
358        });
359    }
360}