Merge pull request #129 from AeneasVerif/dyn-checks-earlier

Rework the removal of dynamic checks

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.1"
+let supported_charon_version = "0.1.2"

charon-ml/src/Expressions.ml

@@ -101,6 +101,9 @@ type binop =
   | Add
   | Sub
   | Mul
+  | CheckedAdd
+  | CheckedSub
+  | CheckedMul
   | Shl
   | Shr
 [@@deriving show, ord]

charon-ml/src/ExpressionsUtils.ml

@@ -5,5 +5,7 @@ let unop_can_fail (unop : unop) : bool =
 
 let binop_can_fail (binop : binop) : bool =
   match binop with
-  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt -> false
+  | BitXor | BitAnd | BitOr | Eq | Lt | Le | Ne | Ge | Gt | CheckedAdd
+  | CheckedSub | CheckedMul ->
+      false
   | Div | Rem | Add | Sub | Mul | Shl | Shr -> true

charon-ml/src/GAstOfJson.ml

@@ -749,6 +749,9 @@ let binop_of_json (js : json) : (binop, string) result =
   | `String "Add" -> Ok Add
   | `String "Sub" -> Ok Sub
   | `String "Mul" -> Ok Mul
+  | `String "CheckedAdd" -> Ok CheckedAdd
+  | `String "CheckedSub" -> Ok CheckedSub
+  | `String "CheckedMul" -> Ok CheckedMul
   | `String "Shl" -> Ok Shl
   | `String "Shr" -> Ok Shr
   | _ -> Error ("binop_of_json failed on:" ^ show js)

charon-ml/src/PrintExpressions.ml

@@ -82,6 +82,9 @@ let binop_to_string (binop : binop) : string =
   | Add -> "+"
   | Sub -> "-"
   | Mul -> "*"
+  | CheckedAdd -> "checked.+"
+  | CheckedSub -> "checked.-"
+  | CheckedMul -> "checked.*"
   | Shl -> "<<"
   | Shr -> ">>"
 

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.1"
+version = "0.1.2"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 

charon/src/ast/expressions.rs

@@ -140,19 +140,27 @@ pub enum BinOp {
     Ne,
     Ge,
     Gt,
-    /// Can fail if the divisor is 0.
+    /// Fails if the divisor is 0, or if the operation is `int::MIN / -1`.
     Div,
-    /// Can fail if the divisor is 0.
+    /// Fails if the divisor is 0, or if the operation is `int::MIN % -1`.
     Rem,
-    /// Can overflow
+    /// Fails on overflow.
     Add,
-    /// Can overflow
+    /// Fails on overflow.
     Sub,
-    /// Can overflow
+    /// Fails on overflow.
     Mul,
-    /// Can fail if the shift is too big
+    /// 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. This operation does not fail.
+    CheckedAdd,
+    /// Like `CheckedAdd`.
+    CheckedSub,
+    /// Like `CheckedAdd`.
+    CheckedMul,
+    /// Fails if the shift is bigger than the bit-size of the type.
     Shl,
-    /// Can fail if the shift is too big
+    /// Fails if the shift is bigger than the bit-size of the type.
     Shr,
     // No Offset binary operation: this is an operation on raw pointers
 }

charon/src/driver.rs

@@ -271,6 +271,15 @@ pub fn translate(
     // we simply apply some micro-passes to make the code cleaner, before
     // serializing the result.
 
+    // # Micro-pass: Remove overflow/div-by-zero/bounds checks since they are already part of the
+    // arithmetic/array operation in the semantics of (U)LLBC.
+    // **WARNING**: this pass uses the fact that the dynamic checks introduced by Rustc use a
+    // special "assert" construct. Because of this, it must happen *before* the
+    // [reconstruct_asserts] pass. See the comments in [crate::remove_dynamic_checks].
+    // **WARNING**: this pass relies on a precise structure of the MIR statements. Because of this,
+    // it must happen before passes that insert statements like [simplify_constants].
+    remove_dynamic_checks::transform(&mut ctx);
+
     // # Micro-pass: desugar the constants to other values/operands as much
     // as possible.
     simplify_constants::transform(&mut ctx);
@@ -304,14 +313,6 @@ pub fn translate(
         // which ignores this first variable. This micro-pass updates this.
         update_closure_signatures::transform(&ctx, &mut llbc_funs);
 
-        // # Micro-pass: remove the dynamic checks for array/slice bounds
-        // and division by zero.
-        // **WARNING**: this pass uses the fact that the dynamic checks
-        // introduced by Rustc use a special "assert" construct. Because of
-        // this, it must happen *before* the [reconstruct_asserts] pass.
-        // See the comments in [crate::remove_dynamic_checks].
-        remove_dynamic_checks::transform(&mut ctx, &mut llbc_funs, &mut llbc_globals);
-
         // # Micro-pass: reconstruct the asserts
         reconstruct_asserts::transform(&mut ctx, &mut llbc_funs, &mut llbc_globals);
 

charon/src/lib.rs

@@ -17,6 +17,7 @@
 #![recursion_limit = "256"]
 #![feature(trait_alias)]
 #![feature(let_chains)]
+#![feature(if_let_guard)]
 #![feature(iterator_try_collect)]
 
 extern crate rustc_ast;

charon/src/pretty/fmt_with_ctx.rs

@@ -1486,6 +1486,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, ">>"),
         }