From 37395f634d42c5c3cf471c4e433870ef7d290fd6 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Thu, 26 Mar 2026 17:45:44 +1300 Subject: [PATCH 1/5] Add promotable to Globals --- lib/check.ml | 20 +++++++++++--------- lib/core_to_mucore.ml | 4 ++-- lib/fulminate/extract.ml | 2 +- lib/global.ml | 7 ++++--- lib/mucore.ml | 3 ++- lib/mucore.mli | 3 ++- lib/pp_mucore_coq.ml | 4 ++-- lib/typing.mli | 8 +++++--- 8 files changed, 29 insertions(+), 22 deletions(-) diff --git a/lib/check.ml b/lib/check.ml index d8187ddb0..746ea78ce 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -118,7 +118,7 @@ let check_ptrval (loc : Locations.t) ~(expect : BT.t) (ptrval : pointer_value) : unsupported loc !^"invalid function pointer" | Some sym -> (* just to make sure it exists *) - let@ _fun_loc, _, _ = Global.get_fun_decl loc sym in + let@ _fun_loc, _, _, _promotable = Global.get_fun_decl loc sym in (* the symbol of a function is the same as the symbol of its address *) let here = Locations.other __LOC__ in return (sym_ (sym, BT.(Loc ()), here))) @@ -370,7 +370,7 @@ let known_function_pointer loc p = let@ global_funs = Global.get_fun_decls () in let function_addrs = List.map - (fun (sym, (loc, _, _)) -> + (fun (sym, (loc, _, _, _)) -> let t = IT.sym_ (sym, BT.(Loc ()), loc) in (sym, t)) global_funs @@ -931,7 +931,7 @@ let rec check_pexpr path_cs (pe : BT.t Mu.pexpr) : IT.t m = | `Inconsistent_context -> assert false | `Known sym -> (* need to conjure up the characterising 4-tuple *) - let@ _, _, c_sig = Global.get_fun_decl loc sym in + let@ _, _, c_sig, _ = Global.get_fun_decl loc sym in (match IT.const_of_c_sig c_sig loc with | Some it -> return it | None -> @@ -1948,7 +1948,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = match known with | `Inconsistent_context -> return () | `Known fsym -> - let@ _loc, opt_ft, _ = Global.get_fun_decl loc fsym in + let@ _loc, opt_ft, _, _ = Global.get_fun_decl loc fsym in let@ ft = match opt_ft with | Some ft -> return ft @@ -2621,13 +2621,15 @@ let wf_check_and_record_functions funs call_sigs = (fun i fsym def (trusted, checked) -> add_cts fsym; match def with - | Mu.Proc { loc; args_and_body; trusted = tr; _ } -> + | Mu.Proc { loc; args_and_body; trusted = tr; promotable } -> welltyped_ping i fsym; let@ args_and_body = WellTyped.procedure loc args_and_body in let ft = WellTyped.to_argument_type args_and_body in debug 6 (lazy (!^"function type" ^^^ Sym.pp fsym)); debug 6 (lazy (CF.Pp_ast.pp_doc_tree (AT.dtree RT.dtree ft))); - let@ () = Global.add_fun_decl fsym (loc, Some ft, Pmap.find fsym call_sigs) in + let@ () = + Global.add_fun_decl fsym (loc, Some ft, Pmap.find fsym call_sigs, promotable) + in (match tr with | Trusted _ -> return ((fsym, (loc, ft)) :: trusted, checked) | Checked -> return (trusted, (fsym, (loc, args_and_body)) :: checked)) @@ -2640,7 +2642,7 @@ let wf_check_and_record_functions funs call_sigs = let@ ft = WellTyped.function_type "function" loc ft in return (Some ft) in - let@ () = Global.add_fun_decl fsym (loc, oft, Pmap.find fsym call_sigs) in + let@ () = Global.add_fun_decl fsym (loc, oft, Pmap.find fsym call_sigs, []) in return (trusted, checked)) funs ([], []) @@ -2881,7 +2883,7 @@ let add_stdlib_spec = Pp.debug 2 (lazy (Pp.headline ("adding builtin spec for procedure " ^ Sym.pp_string fsym))); - Global.add_fun_decl fsym (Locations.other __LOC__, Some ft, ct) + Global.add_fun_decl fsym (Locations.other __LOC__, Some ft, ct, []) in fun call_sigs fsym -> match @@ -2981,7 +2983,7 @@ let time_check_c_functions in let@ () = Sym.Map.fold - (fun _ (loc, def, _) acc -> + (fun _ (loc, def, _, _) acc -> match def with | None -> acc | Some def -> diff --git a/lib/core_to_mucore.ml b/lib/core_to_mucore.ml index b20c5f095..8dc90756e 100644 --- a/lib/core_to_mucore.ml +++ b/lib/core_to_mucore.ml @@ -1189,7 +1189,7 @@ let normalise_fun_map_decl let@ () = if variadic then unsupported loc !^"variadic functions" else return () in (match decl with | CF.Milicore.Mi_Fun (_bt, _args, _pe) -> assert false - | Mi_Proc (loc, _mrk, _ret_bt, args, body, labels) -> + | Mi_Proc (loc, _mrk, _ret_bt, args, body, labels, promotable) -> debug 2 (lazy (item "normalising procedure" (Sym.pp fname))); let@ parsed_defn_specs = Parse.function_spec attrs in let parsed_decl_spec = @@ -1263,7 +1263,7 @@ let normalise_fun_map_decl ghost_params requires in - return (Some (Mu.Proc { loc; args_and_body; trusted }, functions)) + return (Some (Mu.Proc { loc; args_and_body; trusted; promotable }, functions)) | Mi_ProcDecl (loc, ret_bt, _bts) -> (match Sym.Map.find_opt fname fun_specs with | Some parsed_decl_spec -> diff --git a/lib/fulminate/extract.ml b/lib/fulminate/extract.ml index 9ee5c18df..7ad41c636 100644 --- a/lib/fulminate/extract.ml +++ b/lib/fulminate/extract.ml @@ -101,7 +101,7 @@ let from_fn cabs_tunit (fn, decl) = match decl with | ProcDecl (fn_loc, _fn) -> { fn; fn_loc; internal = None; trusted = false; is_static = false } - | Proc { loc = fn_loc; args_and_body; trusted } -> + | Proc { loc = fn_loc; args_and_body; trusted; promotable = _ } -> let args_and_body = Core_to_mucore.at_of_arguments Fun.id args_and_body in let internal = ArgumentTypes.map diff --git a/lib/global.ml b/lib/global.ml index 848207307..db46664e0 100644 --- a/lib/global.ml +++ b/lib/global.ml @@ -8,7 +8,8 @@ type t = datatypes : BaseTypes.dt_info Sym.Map.t; datatype_constrs : BaseTypes.constr_info Sym.Map.t; datatype_order : Sym.t list list option; - fun_decls : (Locations.t * AT.ft option * Sctypes.c_concrete_sig) Sym.Map.t; + fun_decls : + (Locations.t * AT.ft option * Sctypes.c_concrete_sig * Sym.t list) Sym.Map.t; resource_predicates : Definition.Predicate.t Sym.Map.t; resource_predicate_order : Sym.t list list option; logical_functions : Definition.Function.t Sym.Map.t; @@ -88,7 +89,7 @@ module type Lifted = sig val get_fun_decl : Locations.t -> Sym.t -> - (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) t + (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig * Sym.t list) t val get_lemma : Locations.t -> Sym.t -> (Cerb_location.t * AT.lemmat) t @@ -163,7 +164,7 @@ let pp_struct_layout (tag, layout) = let pp_struct_decls decls = Pp.list pp_struct_layout (Sym.Map.bindings decls) -let pp_fun_decl (sym, (_, t, _)) = +let pp_fun_decl (sym, (_, t, _, _promotable)) = item (plain (Sym.pp sym)) (Pp.option (AT.pp RT.pp) "(no spec)" t) diff --git a/lib/mucore.ml b/lib/mucore.ml index 9afec265b..336646bdc 100644 --- a/lib/mucore.ml +++ b/lib/mucore.ml @@ -274,7 +274,8 @@ type 'TY fun_map_decl = | Proc of { loc : Locations.t; args_and_body : 'TY args_and_body; - trusted : trusted + trusted : trusted; + promotable : Sym.t list } | ProcDecl of Locations.t * ArgumentTypes.ft option diff --git a/lib/mucore.mli b/lib/mucore.mli index 3030edd89..6da18db56 100644 --- a/lib/mucore.mli +++ b/lib/mucore.mli @@ -244,7 +244,8 @@ type 'TY fun_map_decl = | Proc of { loc : Locations.t; args_and_body : 'TY args_and_body; - trusted : trusted + trusted : trusted; + promotable : Sym.t list } | ProcDecl of Locations.t * ArgumentTypes.ft option diff --git a/lib/pp_mucore_coq.ml b/lib/pp_mucore_coq.ml index a5182a1d5..b5af84fd5 100644 --- a/lib/pp_mucore_coq.ml +++ b/lib/pp_mucore_coq.ml @@ -2028,7 +2028,7 @@ let pp_file pp_type pp_type_name file = pp_location loc; pp_option (pp_argument_types pp_return_type) ft ]) - | Proc { loc; args_and_body; trusted } -> + | Proc { loc; args_and_body; trusted; promotable = _ } -> coq_def (Sym.pp_string_no_nums sym) P.empty @@ -2203,7 +2203,7 @@ let pp_global (g : Global.t) = ("Global.datatype_order", pp_option (pp_list (pp_list pp_symbol)) g.datatype_order); ( "Global.fun_decls", pp_sym_map - (fun (l, a, s) -> + (fun (l, a, s, _p) -> pp_tuple [ pp_location l; pp_option pp_argument_types_ft a; pp_c_concrete_sig s ]) g.fun_decls ); diff --git a/lib/typing.mli b/lib/typing.mli index f2b1cf705..6e3cf5495 100644 --- a/lib/typing.mli +++ b/lib/typing.mli @@ -107,7 +107,7 @@ module Global : sig val get_fun_decl : Locations.t -> Sym.t -> - (Locations.t * Global.AT.ft option * Sctypes.c_concrete_sig) m + (Locations.t * Global.AT.ft option * Sctypes.c_concrete_sig * Sym.t list) m val add_lemma : Sym.t -> Locations.t * ArgumentTypes.lemmat -> unit m @@ -121,7 +121,7 @@ module Global : sig val add_fun_decl : Sym.t -> - Locations.t * ArgumentTypes.ft option * Sctypes.c_concrete_sig -> + Locations.t * ArgumentTypes.ft option * Sctypes.c_concrete_sig * Sym.t list -> unit m val set_datatype_order : Sym.t list list option -> unit m @@ -148,7 +148,9 @@ module Global : sig val get_fun_decls : unit -> - (Sym.t * (Locations.t * Global.AT.ft option * Sctypes.c_concrete_sig)) list m + (Sym.t * (Locations.t * Global.AT.ft option * Sctypes.c_concrete_sig * Sym.t list)) + list + m end (* val set_statement_locs : Locations.loc CStatements.LocMap.t -> (unit) m *) From f64557eb19fce3c3572542ccaeae0a9fa327a1d6 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Thu, 26 Mar 2026 22:11:59 +1300 Subject: [PATCH 2/5] Use promotable vars in actions --- bin/common.ml | 2 +- lib/check.ml | 106 ++++++++++++++++++++++++++++++++++++------------ lib/context.ml | 2 + lib/context.mli | 1 + lib/typing.ml | 40 ++++++++++++++++++ lib/typing.mli | 10 +++++ 6 files changed, 134 insertions(+), 27 deletions(-) diff --git a/bin/common.ml b/bin/common.ml index 164f654a9..c91ea5a65 100644 --- a/bin/common.ml +++ b/bin/common.ml @@ -50,7 +50,7 @@ let frontend ~ignore_bitfields:false; CF.Ocaml_implementation.set CF.Ocaml_implementation.HafniumImpl.impl; CF.Switches.set - ([ "inner_arg_temps"; "at_magic_comments" ] + ([ "inner_arg_temps"; "at_magic_comments"; "copy_prop"; "mem2reg" ] (* TODO (DCM, VIP) figure out how to support liveness checks for read-only resources and then switch on "strict_pointer_arith" to elaborate array shift to the effectful version. "strict_pointer_relationals" is also diff --git a/lib/check.ml b/lib/check.ml index 746ea78ce..63aad6b9f 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1249,7 +1249,17 @@ let all_empty loc _original_resources = { loc; msg = Unused_resource { resource; ctxt; model } }) -let load loc pointer ct = +let is_promotable_create = function + | Mu.Esseq + ( Mu.Pattern (_, _, _, CaseBase (Some sym, _)), + Expr (_, _, _, Eaction (Paction (_, Action (_, Create _)))), + _ ) -> + let@ promoted = is_promoted sym in + return promoted + | _ -> return false + + +let load_r loc pointer ct = let@ point, O value = RI.Special.predicate_request loc @@ -1261,6 +1271,63 @@ let load loc pointer ct = return value +let load loc pointer ct = + let sym_opt = is_sym pointer in + match sym_opt with + | None -> load_r loc pointer ct + | Some (sym, _bt) -> + let@ fast = fast_load sym in + (match fast with + | None -> load_r loc pointer ct + | Some None -> assert false + | Some (Some t) -> return t) + + +let store_r loc parg ct varg = + let@ _ = + RI.Special.predicate_request + loc + (Access Store) + ({ name = Owned (ct, Uninit); pointer = parg; iargs = [] }, None) + in + add_r loc (P { name = Owned (ct, Init); pointer = parg; iargs = [] }, O varg) + + +let store loc parg ct varg = + let sym_opt = is_sym parg in + match sym_opt with + | None -> store_r loc parg ct varg + | Some (sym, _bt) -> + let@ did = fast_store sym varg in + if did then + return () + else + store_r loc parg ct varg + + +let kill_r loc arg ct = + let@ _ = + RI.Special.predicate_request + loc + (Access Kill) + ({ name = Owned (ct, Uninit); pointer = arg; iargs = [] }, None) + in + let@ _ = RI.Special.predicate_request loc (Access Kill) (Req.make_alloc arg, None) in + return () + + +let kill loc arg ct = + let sym_opt = is_sym arg in + match sym_opt with + | None -> kill_r loc arg ct + | Some (sym, _bt) -> + let@ did = fast_kill sym in + if did then + return () + else + kill_r loc arg ct + + let instantiate loc filter arg = let arg_s = Sym.fresh_make_uniq "instance" in let arg_it = sym_ (arg_s, IT.get_bt arg, loc) in @@ -1833,15 +1900,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let@ () = WellTyped.ensure_base_type loc ~expect Unit in let@ () = WellTyped.ensure_base_type loc ~expect:(Loc ()) (Mu.bt_of_pexpr pe) in check_pexpr pe (fun arg -> - let@ _ = - RI.Special.predicate_request - loc - (Access Kill) - ({ name = Owned (ct, Uninit); pointer = arg; iargs = [] }, None) - in - let@ _ = - RI.Special.predicate_request loc (Access Kill) (Req.make_alloc arg, None) - in + let@ () = kill loc arg ct in let@ () = record_action (Kill arg, loc) in k (unit_ loc)) | Store (_is_locking, act, p_pe, v_pe, _mo) -> @@ -1876,17 +1935,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in { loc; msg }) in - let@ _ = - RI.Special.predicate_request - loc - (Access Store) - ({ name = Owned (act.ct, Uninit); pointer = parg; iargs = [] }, None) - in - let@ () = - add_r - loc - (P { name = Owned (act.ct, Init); pointer = parg; iargs = [] }, O varg) - in + let@ () = store_r loc parg act.ct varg in let@ () = record_action (Write (parg, varg), loc) in k (unit_ loc))) | Load (act, p_pe, _mo) -> @@ -2293,11 +2342,15 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = ~expect:(Mu.bt_of_expr e1) (Mu.bt_of_pattern p) in - check_expr labels e1 (fun it -> - let@ bound_a, _path_cs = check_and_match_pattern p it in - check_expr labels e2 (fun it2 -> - let@ () = remove_as bound_a in - k it2)) + let@ promoted_create = is_promotable_create e_ in + if promoted_create then + check_expr labels e2 (fun it2 -> k it2) + else + check_expr labels e1 (fun it -> + let@ bound_a, _path_cs = check_and_match_pattern p it in + check_expr labels e2 (fun it2 -> + let@ () = remove_as bound_a in + k it2)) | Erun (label_sym, pes) -> let@ () = WellTyped.ensure_base_type loc ~expect Unit in let@ lt, lkind = @@ -2396,6 +2449,7 @@ let check_procedure (let@ () = add_rs loc initial_resources in let@ pre_state = get_typing_context () in let@ () = modify_where (Where.set_section Body) in + let@ () = init_promoted fsym in let@ () = check_expr_top loc label_context rt body in return ((), pre_state)) in diff --git a/lib/context.ml b/lib/context.ml index 9fe8530f8..3a1db8368 100644 --- a/lib/context.ml +++ b/lib/context.ml @@ -22,6 +22,7 @@ type t = { computational : (basetype_or_value * l_info) Sym.Map.t; logical : (basetype_or_value * l_info) Sym.Map.t; resources : Res.t list; + promoted : IndexTerms.t option Sym.Map.t; constraints : LC.Set.t; global : Global.t; where : Where.t @@ -36,6 +37,7 @@ let empty = { computational = Sym.Map.empty; logical; resources = []; + promoted = Sym.Map.empty; constraints = LC.Set.empty; global = Global.empty; where = Where.empty diff --git a/lib/context.mli b/lib/context.mli index c102e7395..e0ff9fc4a 100644 --- a/lib/context.mli +++ b/lib/context.mli @@ -14,6 +14,7 @@ type t = { computational : (basetype_or_value * l_info) Sym.Map.t; logical : (basetype_or_value * l_info) Sym.Map.t; resources : Resource.t list; + promoted : IndexTerms.t option Sym.Map.t; constraints : LogicalConstraints.Set.t; global : Global.t; where : Where.t diff --git a/lib/typing.ml b/lib/typing.ml index 9a9b86f7c..38c0be732 100644 --- a/lib/typing.ml +++ b/lib/typing.ml @@ -306,6 +306,46 @@ end module WellTyped = WellTyped.Lift (ErrorReader) +let fast_load sym = + let@ ctxt = get_typing_context () in + return (Sym.Map.find_opt sym ctxt.promoted) + + +let is_promoted sym = + let@ ctxt = get_typing_context () in + return (Sym.Map.mem sym ctxt.promoted) + + +let init_promoted f_sym = + let@ ctxt = get_typing_context () in + let here = Locations.other __LOC__ in + let@ _, _, _, promotable = Global.get_fun_decl here f_sym in + let promoted = + List.fold_left (fun map sym -> Sym.Map.add sym None map) Sym.Map.empty promotable + in + set_typing_context { ctxt with promoted } + + +let fast_store sym varg = + let@ ctxt = get_typing_context () in + if Sym.Map.mem sym ctxt.promoted then ( + let promoted = Sym.Map.update sym (fun _ -> Some (Some varg)) ctxt.promoted in + let@ () = set_typing_context { ctxt with promoted } in + return true) + else + return false + + +let fast_kill sym = + let@ ctxt = get_typing_context () in + if Sym.Map.mem sym ctxt.promoted then ( + let promoted = Sym.Map.remove sym ctxt.promoted in + let@ () = set_typing_context { ctxt with promoted } in + return true) + else + return false + + let add_sym_eqs sym_eqs = modify (fun s -> let sym_eqs = diff --git a/lib/typing.mli b/lib/typing.mli index 6e3cf5495..1ccceb8a1 100644 --- a/lib/typing.mli +++ b/lib/typing.mli @@ -194,3 +194,13 @@ val modify_where : (Where.t -> Where.t) -> unit m val init_solver : unit -> unit m module WellTyped : WellTyped_intf.S with type 'a t := 'a t + +val init_promoted : Sym.t -> unit m + +val is_promoted : Sym.t -> bool m + +val fast_load : Sym.t -> IndexTerms.t option option m + +val fast_store : Sym.t -> IndexTerms.t -> bool m + +val fast_kill : Sym.t -> bool m From a439ddf16087ac11261edcae57d562ca5e693080 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Thu, 26 Mar 2026 22:26:40 +1300 Subject: [PATCH 3/5] Use my custom Cerberus --- cn.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cn.opam b/cn.opam index b199e3241..cc0e55fee 100644 --- a/cn.opam +++ b/cn.opam @@ -27,7 +27,7 @@ depends: [ "qcheck-ounit" {with-test} ] pin-depends: [ - ["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#e88d46c"] + ["cerberus-lib.dev" "git+https://github.com/dc-mak/cerberus.git#63e182c"] ] build: [ ["dune" "subst"] {pinned} From a61bd29bc26eba9f257cf95fee26d137197f71b4 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Fri, 27 Mar 2026 16:57:56 +1300 Subject: [PATCH 4/5] Properly add support for copy-prop Switches didn't seem to actually make the pass fire, so I've hardcoded it. A couple of tests show different (and worse) location info for errors, this is pending investigation. The copy-prop pass had a few bugs in it, so the commit also bumps the Cerberus commit version to the one where these are fixed. --- bin/common.ml | 7 +++++-- cn.opam | 2 +- lib/check.ml | 17 ++++++++++++----- lib/wellTyped.ml | 1 + 4 files changed, 19 insertions(+), 8 deletions(-) diff --git a/bin/common.ml b/bin/common.ml index c91ea5a65..730b3d4a6 100644 --- a/bin/common.ml +++ b/bin/common.ml @@ -50,7 +50,7 @@ let frontend ~ignore_bitfields:false; CF.Ocaml_implementation.set CF.Ocaml_implementation.HafniumImpl.impl; CF.Switches.set - ([ "inner_arg_temps"; "at_magic_comments"; "copy_prop"; "mem2reg" ] + ([ "inner_arg_temps"; "at_magic_comments" ] (* TODO (DCM, VIP) figure out how to support liveness checks for read-only resources and then switch on "strict_pointer_arith" to elaborate array shift to the effectful version. "strict_pointer_relationals" is also @@ -83,7 +83,10 @@ let frontend let cabs_tunit = Option.get cabs_tunit_opt in let markers_env, ail_prog = Option.get ail_prog_opt in CF.Tags.set_tagDefs prog0.CF.Core.tagDefs; - let prog1 = CF.Remove_unspecs.rewrite_file prog0 in + let prog1 = + prog0 |> CF.Remove_unspecs.rewrite_file |> CF.Copy_propagation.transform_file + (* |> CF.Core_mem2reg.transform_file *) + in let prog2 = CF.Milicore.core_to_micore__file Locations.update prog1 in let prog3 = if skip_label_inlining then diff --git a/cn.opam b/cn.opam index cc0e55fee..12a80f41e 100644 --- a/cn.opam +++ b/cn.opam @@ -27,7 +27,7 @@ depends: [ "qcheck-ounit" {with-test} ] pin-depends: [ - ["cerberus-lib.dev" "git+https://github.com/dc-mak/cerberus.git#63e182c"] + ["cerberus-lib.dev" "git+https://github.com/dc-mak/cerberus.git#42a3c164"] ] build: [ ["dune" "subst"] {pinned} diff --git a/lib/check.ml b/lib/check.ml index 63aad6b9f..046196810 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1255,8 +1255,11 @@ let is_promotable_create = function Expr (_, _, _, Eaction (Paction (_, Action (_, Create _)))), _ ) -> let@ promoted = is_promoted sym in - return promoted - | _ -> return false + if promoted then + return (Some sym) + else + return None + | _ -> return None let load_r loc pointer ct = @@ -1935,7 +1938,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in { loc; msg }) in - let@ () = store_r loc parg act.ct varg in + let@ () = store loc parg act.ct varg in let@ () = record_action (Write (parg, varg), loc) in k (unit_ loc))) | Load (act, p_pe, _mo) -> @@ -2343,8 +2346,12 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = (Mu.bt_of_pattern p) in let@ promoted_create = is_promotable_create e_ in - if promoted_create then - check_expr labels e2 (fun it2 -> k it2) + if Option.is_some promoted_create then ( + let sym = Option.get promoted_create in + let@ () = add_a sym (BT.Loc ()) (loc, lazy (Sym.pp sym)) in + check_expr labels e2 (fun it2 -> + let@ () = remove_as [ sym ] in + k it2)) else check_expr labels e1 (fun it -> let@ bound_a, _path_cs = check_and_match_pattern p it in diff --git a/lib/wellTyped.ml b/lib/wellTyped.ml index da90e006a..f92b1ca2b 100644 --- a/lib/wellTyped.ml +++ b/lib/wellTyped.ml @@ -1597,6 +1597,7 @@ module BaseTyping = struct with | [] -> None | [ ity ] -> Some ity + (* see https://github.com/rems-project/cerberus/issues/1000 if this assert false is triggered *) | _ -> assert false From 616aad2c7516fdcd33ec5eff90820f0cbb4e377c Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Mon, 30 Mar 2026 16:09:09 +1300 Subject: [PATCH 5/5] Quick support for mem2reg --- bin/common.ml | 6 +- lib/check.ml | 135 +++++++++++++++--- lib/compile.ml | 19 ++- lib/compile.mli | 2 + lib/core_to_mucore.ml | 1 + lib/typing.ml | 8 ++ tests/cn/alloc_create.c | 4 +- tests/cn/copy_alloc_id2.error.c.verify | 1 - tests/cn/disj_nonnull.c | 5 +- tests/cn/fun_addrs_cn_stmt.c | 1 + tests/cn/ptr_diff.error.c | 2 +- tests/cn/ptr_diff.error.c.verify | 1 - tests/cn/ptr_relop.error.c.verify | 1 - .../pointer_from_integer_1i.annot.c | 2 +- 14 files changed, 151 insertions(+), 37 deletions(-) diff --git a/bin/common.ml b/bin/common.ml index 730b3d4a6..c05bdcdd7 100644 --- a/bin/common.ml +++ b/bin/common.ml @@ -84,8 +84,10 @@ let frontend let markers_env, ail_prog = Option.get ail_prog_opt in CF.Tags.set_tagDefs prog0.CF.Core.tagDefs; let prog1 = - prog0 |> CF.Remove_unspecs.rewrite_file |> CF.Copy_propagation.transform_file - (* |> CF.Core_mem2reg.transform_file *) + prog0 + |> CF.Remove_unspecs.rewrite_file + |> CF.Copy_propagation.transform_file + |> CF.Core_mem2reg.transform_file in let prog2 = CF.Milicore.core_to_micore__file Locations.update prog1 in let prog3 = diff --git a/lib/check.ml b/lib/check.ml index 046196810..3f47b2c06 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -1119,6 +1119,58 @@ module Spine : sig val subtype : Locations.t -> LRT.t -> (unit -> unit m) -> unit m end = struct + let rec filter_promoted ftyp = + match ftyp with + | LAT.I _ -> return ftyp + | Define ((sym, it), loc, args) -> + let@ args = filter_promoted args in + return (LAT.Define ((sym, it), loc, args)) + | Constraint (lc, loc, args) -> + let@ args = filter_promoted args in + (match lc with + | LC.T (IT (Good (_, pointer), _, _)) -> + let@ promoted = + let sym_opt = is_sym pointer in + match sym_opt with None -> return None | Some (sym, _bt) -> fast_load sym + in + (match promoted with + | None -> return (LAT.Constraint (lc, loc, args)) + | Some _ -> return args) + | _ -> return (LAT.Constraint (lc, loc, args))) + | Resource ((s, (re, bt)), info, args) -> + (match re with + | P { name = Owned _; pointer; iargs = [] } -> + let sym_opt = is_sym pointer in + let@ promoted = + match sym_opt with None -> return None | Some (sym, _bt) -> fast_load sym + in + (match promoted with + | None | Some None (* not the best error msg, but consistent *) -> + let@ args = filter_promoted args in + return (LAT.Resource ((s, (re, bt)), info, args)) + | Some (Some it) -> return (LAT.Define ((s, it), info, args))) + | P { name = PName maybe_alloc; pointer; iargs = [] } -> + if not (Sym.equal maybe_alloc Alloc.Predicate.sym) then + let@ args = filter_promoted args in + return (LAT.Resource ((s, (re, bt)), info, args)) + else ( + let sym_opt = is_sym pointer in + match sym_opt with + | None -> + let@ args = filter_promoted args in + return (LAT.Resource ((s, (re, bt)), info, args)) + | Some (sym, _bt) -> + let@ fast = fast_load sym in + (match fast with + | None -> + let@ args = filter_promoted args in + return (LAT.Resource ((s, (re, bt)), info, args)) + | Some _ -> filter_promoted args)) + | _ -> + let@ args = filter_promoted args in + return (LAT.Resource ((s, (re, bt)), info, args))) + + let spine_l rt_subst rt_pp loc (situation : call_situation) ftyp k = let start_spine = time_start () in let@ original_resources = all_resources loc in @@ -1130,6 +1182,7 @@ end = struct debug 6 (lazy (item "spec" (LAT.pp rt_pp ftyp)))) in let uiinfo = ((Call situation : situation), []) in + let@ ftyp = filter_promoted ftyp in let@ ftyp = RI.General.ftyp_args_request_step rt_subst loc uiinfo original_resources ftyp in @@ -1252,11 +1305,11 @@ let all_empty loc _original_resources = let is_promotable_create = function | Mu.Esseq ( Mu.Pattern (_, _, _, CaseBase (Some sym, _)), - Expr (_, _, _, Eaction (Paction (_, Action (_, Create _)))), + Expr (loc, _, _, Eaction (Paction (_, Action (_, Create _)))), _ ) -> let@ promoted = is_promoted sym in if promoted then - return (Some sym) + return (Some (sym, loc)) else return None | _ -> return None @@ -1302,8 +1355,9 @@ let store loc parg ct varg = | None -> store_r loc parg ct varg | Some (sym, _bt) -> let@ did = fast_store sym varg in - if did then - return () + if did then ( + debug 6 (lazy !^"did fast store"); + return ()) else store_r loc parg ct varg @@ -1326,6 +1380,9 @@ let kill loc arg ct = | Some (sym, _bt) -> let@ did = fast_kill sym in if did then + (* let@ _ = *) + (* RI.Special.predicate_request loc (Access Kill) (Req.make_alloc arg, None) *) + (* in *) return () else kill_r loc arg ct @@ -1573,6 +1630,24 @@ let bytes_constraints return (and_ [ all_some; bytes_prov_eq; eq_ (value_addr, bytes_addr) here ] here)) +let add_alloc loc ret ct = + let here = Locations.other __LOC__ in + let lookup = Alloc.History.lookup_ptr ret here in + let value = + let size = Memory.size_of_ctype ct in + Alloc.History.make_value ~base:(addr_ ret here) ~size here + in + let@ () = + if !use_vip then + (* This is not backwards compatible because in the solver + * Alloc_id maps to unit if not (!use_vip) *) + add_c loc (LC.T (eq_ (lookup, value) here)) + else + return () + in + add_r loc (P (Req.make_alloc ret), O lookup) + + let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let (Expr (loc, annots, expect, e_)) = e in let@ () = add_trace_information labels annots in @@ -1854,7 +1929,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = check_pexpr pe (fun arg -> let ret_s, ret = match prefix with - | PrefSource (_loc, syms) -> + | CF.Symbol.PrefSource (_loc, syms) -> let syms = List.rev syms in (match syms with | Symbol (_, _, SD_ObjectAddress str) :: _ -> @@ -1874,20 +1949,7 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = ( P { name = Owned (act.ct, Uninit); pointer = ret; iargs = [] }, O (default_ (Memory.bt_of_sct act.ct) loc) ) in - let lookup = Alloc.History.lookup_ptr ret here in - let value = - let size = Memory.size_of_ctype act.ct in - Alloc.History.make_value ~base:(addr_ ret here) ~size here - in - let@ () = - if !use_vip then - (* This is not backwards compatible because in the solver - * Alloc_id maps to unit if not (!use_vip) *) - add_c loc (LC.T (eq_ (lookup, value) here)) - else - return () - in - let@ () = add_r loc (P (Req.make_alloc ret), O lookup) in + let@ () = add_alloc loc ret act.ct in let@ () = record_action (Create ret, loc) in k ret) | CreateReadOnly (_sym1, _ct, _sym2, _prefix) -> @@ -2347,8 +2409,9 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = in let@ promoted_create = is_promotable_create e_ in if Option.is_some promoted_create then ( - let sym = Option.get promoted_create in - let@ () = add_a sym (BT.Loc ()) (loc, lazy (Sym.pp sym)) in + let sym, create_loc = Option.get promoted_create in + let ret = IT.sym_ (sym, BT.Loc (), create_loc) in + let@ () = add_a sym (IT.get_bt ret) (loc, lazy (Pp.string "allocation")) in check_expr labels e2 (fun it2 -> let@ () = remove_as [ sym ] in k it2)) @@ -2411,8 +2474,35 @@ let bind_arguments (_loc : Locations.t) (full_args : _ Mu.arguments) = let@ () = add_c (fst info) lc in aux_l resources args | Resource ((s, (re, bt)), ((loc, _) as info), args) -> + let@ promoted = + match re with + | P { name = Owned _; pointer; iargs = [] } -> + let sym_opt = is_sym pointer in + (match sym_opt with + | None -> return false + | Some (sym, _bt) -> + let@ fast = fast_load sym in + (match fast with None -> return false | Some _ -> return true)) + | P { name = PName maybe_alloc; pointer; iargs = [] } -> + if not (Sym.equal maybe_alloc Alloc.Predicate.sym) then + return false + else ( + let sym_opt = is_sym pointer in + match sym_opt with + | None -> return false + | Some (sym, _bt) -> + let@ fast = fast_load sym in + (match fast with None -> return false | Some _ -> return true)) + | _ -> return false + in let@ () = add_l s bt (fst info, lazy (Sym.pp s)) in - aux_l (resources @ [ (re, Resource.O (sym_ (s, bt, loc))) ]) args + let resources = + if promoted then + resources + else + resources @ [ (re, Resource.O (sym_ (s, bt, loc))) ] + in + aux_l resources args | I i -> return (i, resources) in let rec aux_a = function @@ -2688,6 +2778,7 @@ let wf_check_and_record_functions funs call_sigs = let ft = WellTyped.to_argument_type args_and_body in debug 6 (lazy (!^"function type" ^^^ Sym.pp fsym)); debug 6 (lazy (CF.Pp_ast.pp_doc_tree (AT.dtree RT.dtree ft))); + debug 6 (lazy (!^"promotable" ^^^ Sym.pp fsym ^^^ Pp.list Sym.pp promotable)); let@ () = Global.add_fun_decl fsym (loc, Some ft, Pmap.find fsym call_sigs, promotable) in diff --git a/lib/compile.ml b/lib/compile.ml index 6e6d22820..8bb95a8d0 100644 --- a/lib/compile.ml +++ b/lib/compile.ml @@ -38,7 +38,8 @@ type env = tagDefs : (Cerb_frontend.Symbol.sym, Mu.tag_definition) Pmap.map; fetch_enum_expr : Locations.t -> Sym.t -> unit CF.AilSyntax.expression cerb_frontend_result; - fetch_typedef : Locations.t -> Sym.t -> CF.Ctype.ctype cerb_frontend_result + fetch_typedef : Locations.t -> Sym.t -> CF.Ctype.ctype cerb_frontend_result; + promoted : Sym.t list } let init tagDefs fetch_enum_expr fetch_typedef = @@ -59,7 +60,8 @@ let init tagDefs fetch_enum_expr fetch_typedef = datatype_constrs = Sym.Map.empty; tagDefs; fetch_enum_expr; - fetch_typedef + fetch_typedef; + promoted = [] } @@ -90,6 +92,8 @@ let add_predicate sym pred_sig env = { env with predicates = Sym.Map.add sym pred_sig env.predicates } +let set_promoted env promoted = { env with promoted } + let lookup_computational_or_logical sym env = match Sym.Map.find_opt sym env.logicals with | Some bt -> Some (bt, None) @@ -875,7 +879,16 @@ module C_vars = struct WellTyped (Illtyped_it { it = Terms.pp e; has = SBT.pp has; expected; reason }) }) - | CNExpr_addr nm -> return (sym_ (nm, BT.Loc None, loc)) + | CNExpr_addr nm -> + if List.mem Sym.equal nm env.promoted then + fail + { loc; + msg = + Generic !^"Cannot take address of promoted variable" + [@alert "-deprecated"] + } + else (* error here if symbol is promoted! *) + return (sym_ (nm, BT.Loc None, loc)) | CNExpr_cast (bt, expr) -> let@ expr = self expr in let bt = base_type env bt in diff --git a/lib/compile.mli b/lib/compile.mli index 8390788c2..a8c46f75d 100644 --- a/lib/compile.mli +++ b/lib/compile.mli @@ -24,6 +24,8 @@ val add_predicates (Sym.t, Cerb_frontend.Ctype.ctype) Cerb_frontend.Cn.cn_predicate list -> env +val set_promoted : env -> Sym.t list -> env + type message = | Builtins of Builtins.message | Global of Global.message diff --git a/lib/core_to_mucore.ml b/lib/core_to_mucore.ml index 8dc90756e..db48dd7e7 100644 --- a/lib/core_to_mucore.ml +++ b/lib/core_to_mucore.ml @@ -1202,6 +1202,7 @@ let normalise_fun_map_decl let _, defn_marker, _, ail_args, _ = List.assoc Sym.equal fname ail_prog.CF.AilSyntax.function_definitions in + let env = Compile.set_promoted env promotable in let@ env, d_st = Spec.setup_env_desugaring_state loc diff --git a/lib/typing.ml b/lib/typing.ml index 38c0be732..69542a026 100644 --- a/lib/typing.ml +++ b/lib/typing.ml @@ -327,7 +327,15 @@ let init_promoted f_sym = let fast_store sym varg = + Pp.(debug 6 (lazy (!^"fast store of" ^^^ Sym.pp sym))); + let@ simp_ctxt = simp_ctxt () in + let varg = Simplify.IndexTerms.simp simp_ctxt varg in let@ ctxt = get_typing_context () in + Pp.( + debug + 6 + (lazy + (!^"fast store" ^^^ Pp.list Sym.pp (List.map fst (Sym.Map.bindings ctxt.promoted))))); if Sym.Map.mem sym ctxt.promoted then ( let promoted = Sym.Map.update sym (fun _ -> Some (Some varg)) ctxt.promoted in let@ () = set_typing_context { ctxt with promoted } in diff --git a/tests/cn/alloc_create.c b/tests/cn/alloc_create.c index dfdd7dc63..84050b82f 100644 --- a/tests/cn/alloc_create.c +++ b/tests/cn/alloc_create.c @@ -10,8 +10,8 @@ ensures int main() { - int x = 0; + int x = 0; void *p = &x; /*@ apply check_alloc(&x); @*/ - int y = 1; + int y = 1; p = &y; /*@ apply check_alloc(&y); @*/ } diff --git a/tests/cn/copy_alloc_id2.error.c.verify b/tests/cn/copy_alloc_id2.error.c.verify index d396bef31..8f84671e5 100644 --- a/tests/cn/copy_alloc_id2.error.c.verify +++ b/tests/cn/copy_alloc_id2.error.c.verify @@ -5,4 +5,3 @@ tests/cn/copy_alloc_id2.error.c:10:12: error: Pointer `p` needs to be live for c int* q = __cerbvar_copy_alloc_id(p_int + 0ULL, p); ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Need an Alloc or RW in context with same allocation id -State file: file:///tmp/state__copy_alloc_id2.error.c__f.html diff --git a/tests/cn/disj_nonnull.c b/tests/cn/disj_nonnull.c index 4b74a648c..da54256dc 100644 --- a/tests/cn/disj_nonnull.c +++ b/tests/cn/disj_nonnull.c @@ -20,9 +20,8 @@ void globals() int main() { - int p = 1; - int q = 2; - + int p = 1; void *ptr = &p; + int q = 2; ptr = &q; /*@ assert((u64) &p != (u64) &q); @*/ /*@ assert((u64)&p < (u64)&p + 4u64); @*/ diff --git a/tests/cn/fun_addrs_cn_stmt.c b/tests/cn/fun_addrs_cn_stmt.c index 938baee5d..3fe3e49cf 100644 --- a/tests/cn/fun_addrs_cn_stmt.c +++ b/tests/cn/fun_addrs_cn_stmt.c @@ -19,6 +19,7 @@ int f (int x) /*@ accesses global_x; @*/ { + void *p = &x; /* resolution of the 'g' & 'extern_f' addrs triggered a bug at one point */ /*@ assert (((u32) (&x)) == ((u32) (&x))); @*/; /*@ assert (((u32) (&global_x)) == ((u32) (&global_x))); @*/; diff --git a/tests/cn/ptr_diff.error.c b/tests/cn/ptr_diff.error.c index 837a9c611..abcb3ba1f 100644 --- a/tests/cn/ptr_diff.error.c +++ b/tests/cn/ptr_diff.error.c @@ -1,6 +1,6 @@ int live_RW_footprint(char *p, char *q) /*@ - requires +requires take P = RW(array_shift(p, -2i64)); ptr_eq(q, array_shift(p, 12i64)); ensures diff --git a/tests/cn/ptr_diff.error.c.verify b/tests/cn/ptr_diff.error.c.verify index 4fd1d292d..c7960685e 100644 --- a/tests/cn/ptr_diff.error.c.verify +++ b/tests/cn/ptr_diff.error.c.verify @@ -11,4 +11,3 @@ tests/cn/ptr_diff.error.c:13:10: error: Pointer `q` needs to be live for pointer return q - p; ~~^~~ Need an Alloc or RW in context with same allocation id -State file: file:///tmp/state__ptr_diff.error.c__live_RW_footprint.html diff --git a/tests/cn/ptr_relop.error.c.verify b/tests/cn/ptr_relop.error.c.verify index 061417a58..4f66a72c8 100644 --- a/tests/cn/ptr_relop.error.c.verify +++ b/tests/cn/ptr_relop.error.c.verify @@ -11,4 +11,3 @@ tests/cn/ptr_relop.error.c:13:10: error: Pointer `q` needs to be live for pointe return q > p; ~~^~~ Need an Alloc or RW in context with same allocation id -State file: file:///tmp/state__ptr_relop.error.c__live_owned_footprint.html diff --git a/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c b/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c index 88e1fb1c8..b227430da 100644 --- a/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c +++ b/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c @@ -5,7 +5,7 @@ #include "charon_address_guesses.h" #include "cn_lemmas.h" void f(uintptr_t i) { - int j=5; + int j=5; void *ptr = &j; /*CN_VIP*//*@ apply assert_equal(i, (u64)&j); @*/ #if defined(ANNOT) int *p = copy_alloc_id(i, &j);