charon_lib/transform/
remove_arithmetic_overflow_checks.rs

1//! # Micro-pass: remove the overflow checks for arithmetic operations we couldn't remove in
2//! [`remove_dynamic_checks`]. See comments there for more details.
3use crate::transform::TransformCtx;
4use crate::ullbc_ast::*;
5
6use super::ctx::UllbcPass;
7
8pub struct Transform;
9
10impl Transform {
11    /// After `remove_dynamic_checks`, the only remaining dynamic checks are overflow checks. We
12    /// couldn't remove them in ullbc because the generated code spans two basic blocks. They are
13    /// inserted only in constants since we otherwise compile in release mode. These assertions
14    /// look like:
15    /// ```text
16    /// r := x checked.+ y;
17    /// assert(move r.1 == false);
18    /// z := move r.0;
19    /// ```
20    /// We replace that with:
21    /// ```text
22    /// z := x + y;
23    /// ```
24    fn update_statements(seq: &mut [Statement]) {
25        if let [Statement {
26            content:
27                RawStatement::Assign(
28                    binop,
29                    Rvalue::BinaryOp(
30                        op @ (BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul),
31                        _,
32                        _,
33                    ),
34                ),
35            ..
36        }, Statement {
37            content:
38                RawStatement::Assert(Assert {
39                    cond: Operand::Move(assert_cond),
40                    expected: false,
41                    ..
42                }),
43            ..
44        }, Statement {
45            content: RawStatement::Assign(final_value, Rvalue::Use(Operand::Move(assigned))),
46            ..
47        }, ..] = seq
48        {
49            // assigned should be: binop.0
50            // assert_cond should be: binop.1
51            if let Some((sub0, ProjectionElem::Field(FieldProjKind::Tuple(..), fid0))) =
52                assigned.as_projection()
53                && fid0.index() == 0
54                && let Some((sub1, ProjectionElem::Field(FieldProjKind::Tuple(..), fid1))) =
55                    assert_cond.as_projection()
56                && fid1.index() == 1
57                && binop.is_local()
58                && *sub0 == *binop
59                && *sub1 == *binop
60            {
61                // Switch to the unchecked operation.
62                *op = match op {
63                    BinOp::CheckedAdd => BinOp::Add,
64                    BinOp::CheckedSub => BinOp::Sub,
65                    BinOp::CheckedMul => BinOp::Mul,
66                    _ => unreachable!(),
67                };
68                // Assign to the correct value in the first statement.
69                std::mem::swap(binop, final_value);
70                // Remove the other two statements.
71                seq[1].content = RawStatement::Nop;
72                seq[2].content = RawStatement::Nop;
73            }
74        }
75    }
76}
77
78impl UllbcPass for Transform {
79    fn transform_body(&self, _ctx: &mut TransformCtx, b: &mut ExprBody) {
80        b.transform_sequences(|_, seq| {
81            Transform::update_statements(seq);
82            Vec::new()
83        })
84    }
85}
charon_lib/transform/remove_arithmetic_overflow_checks.rs

charon_lib/transform/
remove_arithmetic_overflow_checks.rs
