diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractTypes.ml | 3 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 12 | ||||
| -rw-r--r-- | compiler/Translate.ml | 5 |
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; |