diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/ExtractTypes.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 6 |
3 files changed, 12 insertions, 3 deletions
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index ca9984be..f61c28e4 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -177,7 +177,9 @@ let extract_binop (extract_expr : bool -> texpression -> unit) | Add -> "+" | Sub -> "-" | Mul -> "*" - | _ -> raise (Failure "Unreachable") + | Shl -> "<<<" + | Shr -> ">>>" + | BitXor | BitAnd | BitOr -> raise (Failure "Unimplemented") in let binop = match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index cc0580be..ac6c9ede 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -580,7 +580,10 @@ let eval_binary_op_symbolic (config : config) (binop : binop) (op1 : operand) | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> assert (int_ty1 = int_ty2); TLiteral (TInteger int_ty1) - | Shl | Shr -> raise Unimplemented + | Shl | Shr -> + (* The number of bits can be of a different integer type + than the operand *) + TLiteral (TInteger int_ty1) | Ne | Eq -> raise (Failure "Unreachable")) | _ -> raise (Failure "Invalid inputs for binop") in diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 4df3ee73..f5b055fd 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1755,7 +1755,11 @@ and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) : | [ arg0; arg1 ] -> let int_ty0 = ty_as_integer arg0.ty in let int_ty1 = ty_as_integer arg1.ty in - assert (int_ty0 = int_ty1); + (match binop with + (* The Rust compiler accepts bitshifts for any integer type combination for ty0, ty1 *) + | E.Shl | E.Shr -> () + | _ -> assert (int_ty0 = int_ty1) + ); let effect_info = { can_fail = ExpressionsUtils.binop_can_fail binop; |