From 1519c83980540a64cbf63858ebf04bdf01d0fe6e Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Thu, 8 Aug 2024 11:17:22 -0700 Subject: [PATCH] Add support for shift-right on signed numbers. Fixes #464 --- backend/cn/lib/check.ml | 11 ++++---- backend/cn/lib/core_to_mucore.ml | 45 ++++++++++++++++++++------------ backend/cn/lib/mucore.mli | 14 ++++++---- frontend/model/translation.lem | 2 +- 4 files changed, 43 insertions(+), 29 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 37104a17b..ae290b067 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -544,8 +544,9 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m = { loc; msg = Mismatch { has = BT.pp ty; expect = !^"comparable type" } }) in let not_yet x = - Pp.debug 1 (lazy (Pp.item "not yet restored" (Pp_mucore_ast.pp_pexpr orig_pe))); - failwith ("todo: " ^ x) in + Pp.debug 1 (lazy (Pp.item "not yet restored" (Pp_mucore_ast.pp_pexpr orig_pe))); + failwith ("todo: " ^ x) + in (match op with | OpDiv -> let@ () = WellTyped.ensure_base_type loc ~expect (bt_of_pexpr pe1) in @@ -625,8 +626,7 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m = | OpSub -> not_yet "OpSub" | OpMul -> not_yet "OpMul" | OpRem_f -> not_yet "OpRem_f" - | OpExp -> not_yet "OpExp" - ) + | OpExp -> not_yet "OpExp") | M_PEapply_fun (fun_id, args) -> let@ () = match mu_fun_return_type fun_id args with @@ -699,11 +699,10 @@ let rec check_pexpr (pe : BT.t mu_pexpr) (k : IT.t -> unit m) : unit m = (* in integers, perform this op and round. in bitvector types, just perform the op (for all the ops where wrapping is consistent) *) let@ () = WellTyped.WCT.is_ct act.loc act.ct in - (* assert ( match act.ct with | Integer ity when Sctypes.is_unsigned_integer_type ity -> true - | _ -> false); *) + | _ -> false); let@ () = ensure_base_type loc ~expect (Memory.bt_of_sct act.ct) in let@ () = ensure_base_type loc ~expect (bt_of_pexpr pe1) in let@ () = WellTyped.ensure_bits_type loc expect in diff --git a/backend/cn/lib/core_to_mucore.ml b/backend/cn/lib/core_to_mucore.ml index 17a39269f..401097691 100644 --- a/backend/cn/lib/core_to_mucore.ml +++ b/backend/cn/lib/core_to_mucore.ml @@ -341,23 +341,34 @@ let rec n_pexpr ~inherit_loc loc (Pexpr (annots, bty, pe)) : unit Mucore.mu_pexp ^^^ list CF.Pp_core.Basic.pp_pexpr args)) | Sym sym, _ -> assert_error loc (!^"PEcall not inlined:" ^^^ Sym.pp sym) | Impl impl, args -> - (match impl, args with - | CF.Implementation.SHR_signed_negative, [Pexpr (_,_,PEval (Vctype ct)) ;arg1;arg2] -> - let arg1 = n_pexpr loc arg1 in - let arg2 = n_pexpr loc arg2 in - let ity = match Sctypes.is_integer_type (convert_ct loc ct) with - | Some i -> i - | None -> failwith "Non-integer type in shift" in - let act = ity_act loc ity in - let op = CF.Core.IOpShr in - let bound = M_Bound_Except act in - let shift = annotate (M_PEbounded_binop (bound,op,arg1,arg2)) in - annotate (M_PEerror ("Shifting a negative number to the right is implementation-dependant.",shift)) - | _ -> assert_error - loc - (!^"PEcall to impl not inlined:" - ^^^ !^(CF.Implementation.string_of_implementation_constant impl)))) - + (match (impl, args) with + | ( CF.Implementation.SHR_signed_negative, + [ Pexpr (_, _, PEval (Vctype ct)); arg1; arg2 ] ) -> + let arg1 = n_pexpr loc arg1 in + let arg2 = n_pexpr loc arg2 in + let ity = + match Sctypes.is_integer_type (convert_ct loc ct) with + | Some i -> i + | None -> failwith "Non-integer type in shift" + in + let act = ity_act loc ity in + let op = CF.Core.IOpShr in + let bound = M_Bound_Except act in + let shift = annotate (M_PEbounded_binop (bound, op, arg1, arg2)) in + let impl_ok = true (* XXX: parameterize *) in + if impl_ok then + shift + else + annotate + (M_PEerror + ( "Shifting a negative number to the right is implementation-dependant.", + shift )) + (* XXX: Make a type for reporting implementation defined behavior? *) + | _ -> + assert_error + loc + (!^"PEcall to impl not inlined:" + ^^^ !^(CF.Implementation.string_of_implementation_constant impl)))) | PElet (pat, e', e'') -> (match (pat, e') with | Pattern (_annots, CaseBase (Some sym, _)), Pexpr (annots2, _, PEsym sym2) diff --git a/backend/cn/lib/mucore.mli b/backend/cn/lib/mucore.mli index 188809471..d2561e591 100644 --- a/backend/cn/lib/mucore.mli +++ b/backend/cn/lib/mucore.mli @@ -144,10 +144,12 @@ end type symbol = Cerb_frontend.Symbol.sym +(** Annotated C type. The annotations are typically an explanation of + something that might go wrong (e.g., overflow on an integer type). *) type act = - { loc : loc; - annot : Cerb_frontend.Annot.annot list; - ct : T.ct + { loc : loc; (** Source location *) + annot : Cerb_frontend.Annot.annot list; (** Annotations *) + ct : T.ct (** Affected type *) } type 'TY mu_object_value_ = @@ -208,9 +210,11 @@ type bw_unop = | M_BW_CTZ | M_BW_FFS +(** What to do on out of bounds. + The annotated C type is the result type of the operation. *) type bound_kind = - | M_Bound_Wrap of act - | M_Bound_Except of act + | M_Bound_Wrap of act (** Wrap around (used for unsigned types) *) + | M_Bound_Except of act (** Report an exception, for signed types *) val bound_kind_act : bound_kind -> act diff --git a/frontend/model/translation.lem b/frontend/model/translation.lem index a4d98060d..a01c5c314 100644 --- a/frontend/model/translation.lem +++ b/frontend/model/translation.lem @@ -1729,7 +1729,7 @@ else Caux.mk_std_pe "6.5.7#5, sentence 3" begin Caux.mk_if_pe_ [Annot.Anot_explode] (Caux.mk_op_pe C.OpGe promoted1_wrp.E.sym_pe (Caux.mk_integer_pe 0)) begin if Global.backend_name () = "Cn" then - Caux.mk_wrapI_pe result_ity C.IOpShr promoted1_wrp.E.sym_pe promoted2_wrp.E.sym_pe + Caux.mk_catch_exceptional_condition_pe result_ity C.IOpShr promoted1_wrp.E.sym_pe promoted2_wrp.E.sym_pe else expr end