Properly distinguish checked and unchecked binary operations

This is important because they have different types and runtime
semantics.

charon/src/expressions.rs

@@ -141,6 +141,14 @@ pub enum BinOp {
     Sub,
     /// Can overflow
     Mul,
+    /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
+    /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
+    /// overflowed.
+    CheckedAdd,
+    /// Like `CheckedAdd`.
+    CheckedSub,
+    /// Like `CheckedAdd`.
+    CheckedMul,
     /// Can fail if the shift is too big
     Shl,
     /// Can fail if the shift is too big

charon/src/expressions_utils.rs

@@ -73,6 +73,9 @@ impl std::fmt::Display for BinOp {
             BinOp::Add => write!(f, "+"),
             BinOp::Sub => write!(f, "-"),
             BinOp::Mul => write!(f, "*"),
+            BinOp::CheckedAdd => write!(f, "checked.+"),
+            BinOp::CheckedSub => write!(f, "checked.-"),
+            BinOp::CheckedMul => write!(f, "checked.*"),
             BinOp::Shl => write!(f, "<<"),
             BinOp::Shr => write!(f, ">>"),
         }

charon/src/transform/remove_dynamic_checks.rs

@@ -87,13 +87,13 @@ fn remove_dynamic_checks(ctx: &mut TransCtx, block: &mut BlockData) {
         }] if lt_op2 == x && cond == has_overflow && *expected == true => rest,
 
         // Overflow checks for addition/subtraction/multiplication. They look like:
-        //   r := x + y;
+        //   r := x checked.+ y;
         //   assert(move r.1 == false);
         // They only happen in constants because we compile with `-C opt-level=3`. They're tricky
         // to remove so we leave them.
         [.., Statement {
             content:
-                RawStatement::Assign(result, Rvalue::BinaryOp(BinOp::Add | BinOp::Sub | BinOp::Mul, ..)),
+                RawStatement::Assign(result, Rvalue::BinaryOp(BinOp::CheckedAdd | BinOp::CheckedSub | BinOp::CheckedMul, ..)),
             ..
         }] if cond.var_id == result.var_id
             && result.projection.is_empty()

charon/src/translate_functions_to_ullbc.rs

@@ -682,16 +682,30 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
                     }
                 }
             }
-            hax::Rvalue::BinaryOp(binop, operands)
-            | hax::Rvalue::CheckedBinaryOp(binop, operands) => {
-                // We merge checked and unchecked binary operations
+            hax::Rvalue::BinaryOp(binop, operands) => {
                 let (left, right) = operands.deref();
                 Ok(Rvalue::BinaryOp(
                     self.t_ctx.translate_binaryop_kind(span, *binop)?,
                     self.translate_operand(span, left)?,
                     self.translate_operand(span, right)?,
                 ))
             }
+            hax::Rvalue::CheckedBinaryOp(binop, operands) => {
+                let binop = match binop {
+                    hax::BinOp::Add => BinOp::CheckedAdd,
+                    hax::BinOp::Sub => BinOp::CheckedSub,
+                    hax::BinOp::Mul => BinOp::CheckedMul,
+                    _ => {
+                        error_or_panic!(self, span, "Only Add, Sub and Mul are supported as checked binary operations, found {binop:?}");
+                    }
+                };
+                let (left, right) = operands.deref();
+                Ok(Rvalue::BinaryOp(
+                    binop,
+                    self.translate_operand(span, left)?,
+                    self.translate_operand(span, right)?,
+                ))
+            }
             hax::Rvalue::NullaryOp(nullop, _ty) => {
                 trace!("NullOp: {:?}", nullop);
                 // Nullary operations are very low-level and shouldn't be necessary

charon/tests/ui/remove-dynamic-checks.out

@@ -375,7 +375,7 @@ global test_crate::CONST0  {
     let @0: usize; // return
     let @1: (usize, bool); // anonymous local
 
-    @1 := const (1 : usize) + const (1 : usize)
+    @1 := const (1 : usize) checked.+ const (1 : usize)
     assert(move ((@1).1) == false)
     @0 := move ((@1).0)
     return
@@ -385,7 +385,7 @@ global test_crate::CONST1  {
     let @0: usize; // return
     let @1: (usize, bool); // anonymous local
 
-    @1 := const (2 : usize) * const (2 : usize)
+    @1 := const (2 : usize) checked.* const (2 : usize)
     assert(move ((@1).1) == false)
     @0 := move ((@1).0)
     return