diff options
| author | Guillaume Boisseau | 2024-05-06 14:00:40 +0000 |
|---|---|---|
| committer | GitHub | 2024-05-06 14:00:40 +0000 |
| commit | 5c758f8b9b70288f3ef428c53122c75677255520 (patch) | |
| tree | 2101e01f490e9f9821d7b0105bab2568a4d572c9 | |
| parent | a935064196f7fcc65355726a523508f4317d16ee (diff) | |
| parent | 87da55498b0ba19c74854f3e8218fab857c624e3 (diff) | |
Merge pull request #174 from AeneasVerif/bump-charon
Update charon
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractTypes.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 12 | ||||
| -rw-r--r-- | 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 *) @@ -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": { |