summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/ExtractTypes.ml3
-rw-r--r--compiler/InterpreterExpressions.ml12
-rw-r--r--compiler/Translate.ml5
3 files changed, 16 insertions, 4 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/compiler/Translate.ml b/compiler/Translate.ml
index 222b3c57..72a98c3d 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -798,7 +798,10 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
(* Translate *)
export_functions_group pure_funs
| GlobalGroup id -> export_global id
- | TraitDeclGroup id ->
+ | TraitDeclGroup (RecGroup _ids) ->
+ craise_opt_meta __FILE__ __LINE__ None
+ "Mutually recursive trait declarations are not supported"
+ | TraitDeclGroup (NonRecGroup id) ->
(* TODO: update to extract groups *)
if config.extract_trait_decls && config.extract_transparent then (
export_trait_decl_group id;