diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 12 | ||||
| -rw-r--r-- | compiler/ExtractTypes.ml | 17 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 6 |
4 files changed, 29 insertions, 11 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 85ab1112..73ccac44 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -786,7 +786,7 @@ let unop_name (unop : unop) : string = like [<]). *) let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = - let binop = + let binop_s = match binop with | Div -> "div" | Rem -> "rem" @@ -800,16 +800,14 @@ let named_binop_name (binop : E.binop) (int_ty : integer_type) : string = | BitXor -> "xor" | BitAnd -> "and" | BitOr -> "or" - | Shl -> "lsl" - | Shr -> - "asr" - (* NOTE: make sure arithmetic shift right is implemented, i.e. OCaml's asr operator, not lsr *) + | Shl -> "shl" + | Shr -> "shr" | _ -> raise (Failure "Unreachable") in (* Remark: the Lean case is actually not used *) match !backend with - | Lean -> int_name int_ty ^ "." ^ binop - | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop + | Lean -> int_name int_ty ^ "." ^ binop_s + | FStar | Coq | HOL4 -> int_name int_ty ^ "_" ^ binop_s (** A list of keywords/identifiers used by the backend and with which we want to check collision. diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index ca9984be..3657627b 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -163,7 +163,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit) (match (!backend, binop) with | HOL4, (Eq | Ne) | (FStar | Coq | Lean), (Eq | Lt | Le | Ne | Ge | Gt) - | Lean, (Div | Rem | Add | Sub | Mul) -> + | Lean, (Div | Rem | Add | Sub | Mul | Shl | Shr | BitXor | BitOr | BitAnd) -> let binop = match binop with | Eq -> "=" @@ -177,7 +177,11 @@ let extract_binop (extract_expr : bool -> texpression -> unit) | Add -> "+" | Sub -> "-" | Mul -> "*" - | _ -> raise (Failure "Unreachable") + | Shl -> "<<<" + | Shr -> ">>>" + | BitXor -> "^^^" + | BitOr -> "|||" + | BitAnd -> "&&&" in let binop = match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop @@ -188,8 +192,17 @@ let extract_binop (extract_expr : bool -> texpression -> unit) F.pp_print_space fmt (); extract_expr false arg1 | _ -> + let binop_is_shift = match binop with Shl | Shr -> true | _ -> false in let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; + (* In the case of F*, for shift operations, because machine integers + are simply integers with a refinement, if the second argument is a + constant we need to provide the second implicit type argument *) + if binop_is_shift && !backend = FStar && is_const arg1 then ( + F.pp_print_space fmt (); + let ty = ty_as_integer arg1.ty in + F.pp_print_string fmt + ("#" ^ StringUtils.capitalize_first_letter (int_name ty))); F.pp_print_space fmt (); extract_expr true arg0; F.pp_print_space fmt (); 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; |