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}