From e75879992c5a5a5102a4c5f20b90e6a1032b8ec5 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 22 Sep 2023 16:40:31 +0200 Subject: Add support for Shl/Shr typechecking in InterpreterExpressions --- compiler/InterpreterExpressions.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 8b2070c6..469bebec 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -523,7 +523,10 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop) | E.BitOr -> assert (int_ty1 = int_ty2); T.Literal (Integer int_ty1) - | E.Shl | E.Shr -> raise Unimplemented + | E.Shl | E.Shr -> + (* The number of bits can be of a different integer type + than the operand *) + T.Literal (Integer int_ty1) | E.Ne | E.Eq -> raise (Failure "Unreachable")) | _ -> raise (Failure "Invalid inputs for binop") in -- cgit v1.2.3 From a5f87ba02342ae0b96fe0d8ba16f1ec78469d760 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 22 Sep 2023 16:48:37 +0200 Subject: Allow bitshifts with any pair of integer types --- compiler/SymbolicToPure.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 3512270a..08f67592 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1542,7 +1542,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; -- cgit v1.2.3 From f4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Fri, 22 Sep 2023 17:27:54 +0200 Subject: Add Lean extraction of shl/shr --- compiler/Extract.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index c4238d83..61856f0a 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -472,7 +472,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) -> let binop = match binop with | Eq -> "=" @@ -486,6 +486,8 @@ let extract_binop (extract_expr : bool -> texpression -> unit) | Add -> "+" | Sub -> "-" | Mul -> "*" + | Shl -> "<<<" + | Shr -> ">>>" | _ -> raise (Failure "Unreachable") in let binop = -- cgit v1.2.3 From dc4b11689131bdb41a43e5aca76538556a3a120c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 29 Nov 2023 15:45:27 +0100 Subject: Add support for more bitwise operations and update the extraction --- compiler/ExtractBase.ml | 12 +++++------- compiler/ExtractTypes.ml | 14 ++++++++++++-- 2 files changed, 17 insertions(+), 9 deletions(-) (limited to 'compiler') 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 f61c28e4..66418410 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 -> "=" @@ -179,7 +179,9 @@ let extract_binop (extract_expr : bool -> texpression -> unit) | Mul -> "*" | Shl -> "<<<" | Shr -> ">>>" - | BitXor | BitAnd | BitOr -> raise (Failure "Unimplemented") + | BitXor -> "^^^" + | BitOr -> "|||" + | BitAnd -> "&&&" in let binop = match !backend with FStar | Lean | HOL4 -> binop | Coq -> "s" ^ binop @@ -192,6 +194,14 @@ let extract_binop (extract_expr : bool -> texpression -> unit) | _ -> let binop = named_binop_name binop int_ty in F.pp_print_string fmt binop; + (* In the case of F*, 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 !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 (); -- cgit v1.2.3 From 3aa9c531db4e9cde25a4a149a64e3ff730ed798b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 29 Nov 2023 15:47:42 +0100 Subject: Fix a minor issue with the extraction --- compiler/ExtractTypes.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'compiler') diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml index 66418410..3657627b 100644 --- a/compiler/ExtractTypes.ml +++ b/compiler/ExtractTypes.ml @@ -192,12 +192,13 @@ 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*, 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 !backend = FStar && is_const arg1 then ( + (* 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 -- cgit v1.2.3