From 87da55498b0ba19c74854f3e8218fab857c624e3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 6 May 2024 15:42:48 +0200
Subject: Update charon

---
 compiler/ExtractTypes.ml           |  3 +++
 compiler/InterpreterExpressions.ml | 12 +++++++++---
 flake.lock                         |  6 +++---
 3 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index c2eb8da0..947eceff 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -212,6 +212,9 @@ let extract_binop (meta : Meta.meta)
         | Add -> "+"
         | Sub -> "-"
         | Mul -> "*"
+        | CheckedAdd | CheckedSub | CheckedMul ->
+            craise __FILE__ __LINE__ meta
+              "Checked operations are not implemented"
         | Shl -> "<<<"
         | Shr -> ">>>"
         | BitXor -> "^^^"
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 5f849230..5a4fe7da 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -551,7 +551,7 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
               | Ge -> Z.geq sv1.value sv2.value
               | Gt -> Z.gt sv1.value sv2.value
               | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl
-              | Shr | Ne | Eq ->
+              | Shr | Ne | Eq | CheckedAdd | CheckedSub | CheckedMul ->
                   craise __FILE__ __LINE__ meta "Unreachable"
             in
             Ok
@@ -575,7 +575,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
               | BitXor -> raise Unimplemented
               | BitAnd -> raise Unimplemented
               | BitOr -> raise Unimplemented
-              | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq ->
+              | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq | CheckedAdd
+              | CheckedSub | CheckedMul ->
                   craise __FILE__ __LINE__ meta "Unreachable"
             in
             match res with
@@ -586,7 +587,8 @@ let eval_binary_op_concrete_compute (meta : Meta.meta) (binop : binop)
                     value = VLiteral (VScalar sv);
                     ty = TLiteral (TInteger sv1.int_ty);
                   })
-        | Shl | Shr -> raise Unimplemented
+        | Shl | Shr | CheckedAdd | CheckedSub | CheckedMul ->
+            craise __FILE__ __LINE__ meta "Unimplemented binary operation"
         | Ne | Eq -> craise __FILE__ __LINE__ meta "Unreachable")
     | _ -> craise __FILE__ __LINE__ meta "Invalid inputs for binop"
 
@@ -633,6 +635,10 @@ let eval_binary_op_symbolic (config : config) (meta : Meta.meta) (binop : binop)
             | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr ->
                 sanity_check __FILE__ __LINE__ (int_ty1 = int_ty2) meta;
                 TLiteral (TInteger int_ty1)
+            (* These return `(int, bool)` which isn't a literal type *)
+            | CheckedAdd | CheckedSub | CheckedMul ->
+                craise __FILE__ __LINE__ meta
+                  "Checked operations are not implemented"
             | Shl | Shr ->
                 (* The number of bits can be of a different integer type
                    than the operand *)
diff --git a/flake.lock b/flake.lock
index b9178971..14ee3c05 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1715000450,
-        "narHash": "sha256-N7VGgAwoMeSEYblcKzo7TZWv6upuJdknrnZO1ZSwJWQ=",
+        "lastModified": 1715003183,
+        "narHash": "sha256-/bnkg8txVHgM5X4t2j6TQmDQ22Rb3SCgCMV9pAQGjp8=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "f8fab8d2f4f279f973057d0f7f58c2fd59146e30",
+        "rev": "1a205c55b02f3dff1ae238dfdac5a58d58de6006",
         "type": "github"
       },
       "original": {
-- 
cgit v1.2.3