diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractTypes.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 12 |
2 files changed, 12 insertions, 3 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 *) |