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 +++++++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'compiler')

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 *)
-- 
cgit v1.2.3