From 2b755403b03d4375aab4927d920ce841f11e1a05 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 5 Jul 2023 20:52:19 +0100 Subject: [PATCH] performance optimisation: Usually the unpack rule for a resource type is derived from the corresponding pack rule. In the case of Owned we can do better and describe the resources resulting from the unpack without new logical variables or new constraints. --- backend/cn/check.ml | 32 ++++++++--------- backend/cn/pack.ml | 77 +++++++++++++++++++++++++++++++++-------- backend/cn/typing.ml | 40 ++++++++++----------- backend/cn/typing.mli | 5 +-- backend/cn/wellTyped.ml | 18 +++++----- 5 files changed, 110 insertions(+), 62 deletions(-) diff --git a/backend/cn/check.ml b/backend/cn/check.ml index 67b8fd5ac..544c84bc3 100644 --- a/backend/cn/check.ml +++ b/backend/cn/check.ml @@ -98,13 +98,13 @@ let rec pattern_match (M_Pattern (loc, _, pattern)) it = | M_CaseCtor (constructor, pats) -> match constructor, pats with | M_Cnil item_bt, [] -> - let@ () = add_c (LC.t_ (eq__ it (nil_ ~item_bt))) in + let@ () = add_c loc (LC.t_ (eq__ it (nil_ ~item_bt))) in return [] | M_Ccons, [p1; p2] -> let@ item_bt = infer_pattern p1 in let@ a1 = pattern_match p1 (head_ ~item_bt it) in let@ a2 = pattern_match p2 (tail_ it) in - let@ () = add_c (LC.t_ (ne_ (it, nil_ ~item_bt))) in + let@ () = add_c loc (LC.t_ (ne_ (it, nil_ ~item_bt))) in return (a1 @ a2) | M_Ctuple, pats -> let@ all_as = ListM.mapiM (fun i p -> @@ -393,7 +393,7 @@ let check_single_ct loc expr = let@ provable = provable loc in begin match provable (t_ eq) with | `True -> - let@ () = add_c (t_ eq) in + let@ () = add_c loc (t_ eq) in return ct | `False -> (* TODO: this is the most likely case, give a better error *) @@ -713,7 +713,7 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t) let@ eq_opt = get_eq_in_model loc msg ptr ptr_opts in Pp.debug 5 (lazy (Pp.item "function pointer application: case splitting on" (IT.pp eq_opt))); let aux e cond = - let@ () = add_c (t_ cond) in + let@ () = add_c loc (t_ cond) in Pp.debug 5 (lazy (Pp.item "checking consistency of eq branch" (IT.pp cond))); let@ provable = provable loc in match provable (t_ (bool_ false)) with @@ -764,7 +764,7 @@ let rec check_pexpr (pe : 'bty mu_pexpr) ~(expect:BT.t) | M_PEif (pe, e1, e2) -> check_pexpr ~expect:Bool pe (fun c -> let aux e cond = - let@ () = add_c (t_ cond) in + let@ () = add_c loc (t_ cond) in Pp.debug 5 (lazy (Pp.item "checking consistency of if-branch" (IT.pp cond))); let@ provable = provable loc in match provable (t_ (bool_ false)) with @@ -1023,7 +1023,7 @@ let instantiate loc filter arg = let arg_s = Sym.fresh_make_uniq "instance" in let arg_it = sym_ (arg_s, IT.bt arg) in let@ () = add_l arg_s (IT.bt arg_it) (loc, lazy (Sym.pp arg_s)) in - let@ () = add_c (LC.t_ (eq__ arg_it arg)) in + let@ () = add_c loc (LC.t_ (eq__ arg_it arg)) in let@ constraints = all_constraints () in let extra_assumptions = List.filter_map (fun lc -> @@ -1037,7 +1037,7 @@ let instantiate loc filter arg = in if List.length extra_assumptions == 0 then Pp.warn loc (Pp.string "nothing instantiated") else (); - add_cs extra_assumptions + add_cs loc extra_assumptions @@ -1181,8 +1181,8 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr) IT.fresh Loc in let@ () = add_l ret_s (IT.bt ret) (loc, lazy (Pp.string "allocation")) in - let@ () = add_c (t_ (representable_ (Pointer act.ct, ret))) in - let@ () = add_c (t_ (alignedI_ ~align:arg ~t:ret)) in + let@ () = add_c loc (t_ (representable_ (Pointer act.ct, ret))) in + let@ () = add_c loc (t_ (alignedI_ ~align:arg ~t:ret)) in let@ () = add_r loc (P { name = Owned (act.ct, Uninit); @@ -1315,7 +1315,7 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr) | _, M_Eif (c_pe, e1, e2) -> check_pexpr ~expect:Bool c_pe (fun carg -> let aux lc nm e = - let@ () = add_c (t_ lc) in + let@ () = add_c loc (t_ lc) in let@ provable = provable loc in match provable (t_ (bool_ false)) with | `True -> return () @@ -1427,7 +1427,7 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr) | M_CN_extract (to_extract, it) -> let@ predicate_name = RI.predicate_name_of_to_extract loc to_extract in let@ it = WIT.check loc Integer it in - add_movable_index (predicate_name, it) + add_movable_index loc (predicate_name, it) | M_CN_unfold (f, args) -> let@ def = get_logical_function_def loc f in let has_args, expect_args = List.length args, List.length def.args in @@ -1445,7 +1445,7 @@ let rec check_expr labels ~(typ:BT.t orFalse) (e : 'bty mu_expr) in fail (fun _ -> {loc; msg = Generic msg}) | Some body -> - add_c (LC.t_ (eq_ (pred_ f args def.return_bt, body))) + add_c loc (LC.t_ (eq_ (pred_ f args def.return_bt, body))) end | M_CN_apply (lemma, args) -> let@ (_loc, lemma_typ) = get_lemma loc lemma in @@ -1536,10 +1536,10 @@ let bind_arguments (loc : Loc.t) (full_args : _ mu_arguments) = let rec aux_l resources = function | M_Define ((s, it), info, args) -> let@ () = add_l s (IT.bt it) (fst info, lazy (Sym.pp s)) in - let@ () = add_c (LC.t_ (def_ s it)) in + let@ () = add_c (fst info) (LC.t_ (def_ s it)) in aux_l resources args | M_Constraint (lc, info, args) -> - let@ () = add_c lc in + let@ () = add_c (fst info) lc in aux_l resources args | M_Resource ((s, (re, bt)), info, args) -> let@ () = add_l s bt (fst info, lazy (Sym.pp s)) in @@ -1718,7 +1718,7 @@ let record_globals globs = let bt = Loc in let info = (Loc.unknown, lazy (Pp.item "global" (Sym.pp sym))) in let@ () = add_a sym bt info in - let@ () = add_c (t_ (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt)))) in + let@ () = add_c Loc.unknown (t_ (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt)))) in return () ) globs @@ -1729,7 +1729,7 @@ let wf_check_and_record_functions mu_funs mu_call_sigs = (* let lc1 = t_ (ne_ (null_, sym_ (fsym, Loc))) in *) let lc2 = t_ (representable_ (Pointer Void, sym_ (fsym, Loc))) in let@ () = add_l fsym Loc (loc, lazy (Pp.item "global fun-ptr" (Sym.pp fsym))) in - let@ () = add_cs [(* lc1; *) lc2] in + let@ () = add_cs loc [(* lc1; *) lc2] in add_fun_decl fsym (loc, ft, Pmap.find fsym mu_call_sigs) in let welltyped_ping fsym = diff --git a/backend/cn/pack.ml b/backend/cn/pack.ml index 2538e41fa..3d2ec1409 100644 --- a/backend/cn/pack.ml +++ b/backend/cn/pack.ml @@ -18,6 +18,18 @@ let resource_empty provable resource = | `False -> `NonEmpty (constr, Solver.model ()) +let unfolded_array init (ict, olength) pointer = + let length = Option.get olength in + let q_s, q = IT.fresh_named Integer "i" in + Q { + name = Owned (ict, init); + pointer = pointer; + q = q_s; + step = int_ (Memory.size_of_ctype ict); + iargs = []; + permission = and_ [((int_ 0) %<= q); (q %< (int_ length))] + } + let packing_ft loc global provable ret = match ret with @@ -26,18 +38,7 @@ let packing_ft loc global provable ret = | Owned ((Void | Integer _ | Pointer _ | Function _), _init) -> None | Owned ((Array (ict, olength)) as ct, init) -> - let length = Option.get olength in - let qpred = - let q_s, q = IT.fresh_named Integer "i" in - Q { - name = Owned (ict, init); - pointer = ret.pointer; - q = q_s; - step = int_ (Memory.size_of_ctype ict); - iargs = []; - permission = and_ [((int_ 0) %<= q); (q %< (int_ length))] - } - in + let qpred = unfolded_array init (ict, olength) ret.pointer in let o_s, o = IT.fresh_named (BT.of_sct ct) "value" in let at = LAT.Resource ((o_s, (qpred, IT.bt o)), (loc, None), @@ -86,11 +87,56 @@ let packing_ft loc global provable ret = | Q _ -> None +let unpack_owned global (ct, init) pointer (O o) = + let open Sctypes in + match ct with + | (Void | Integer _ | Pointer _ | Function _) -> + None + | Array (ict, olength) -> + Some [(unfolded_array init (ict, olength) pointer, O o)] + | Struct tag -> + let layout = SymMap.find tag global.Global.struct_decls in + let res = + List.fold_right (fun {offset; size; member_or_padding} res -> + match member_or_padding with + | Some (member, mct) -> + let mresource = + (P { + name = Owned (mct, init); + pointer = memberShift_ (pointer, tag, member); + iargs = []; + }, + O (member_ ~member_bt:(BT.of_sct mct) (tag, o, member))) + in + (mresource :: res) + | None -> + let padding_ct = Sctypes.Array (Integer Char, Some size) in + let mresource = + (P { + name = Owned (padding_ct, Uninit); + pointer = pointer_offset_ (pointer, int_ offset); + iargs = []; + }, O (default_ (BT.of_sct padding_ct))) + in + (mresource :: res) + ) layout [] + in + Some res + + let unpack loc global provable (ret, O o) = - match packing_ft loc global provable ret with - | None -> None - | Some packing_ft -> Some (ResourcePredicates.clause_lrt o packing_ft) + match ret with + | P {name = Owned (ct, init); pointer; iargs = []} -> + begin match unpack_owned global (ct, init) pointer (O o) with + | None -> None + | Some re -> Some (`RES re) + end + | _ -> + begin match packing_ft loc global provable ret with + | None -> None + | Some packing_ft -> Some (`LRT (ResourcePredicates.clause_lrt o packing_ft)) + end @@ -137,3 +183,4 @@ let extractable_multiple loc provable = fun movable_indices re -> aux movable_indices (re, []) + diff --git a/backend/cn/typing.ml b/backend/cn/typing.ml index bfb1b2303..3f1d8dbf2 100644 --- a/backend/cn/typing.ml +++ b/backend/cn/typing.ml @@ -409,7 +409,7 @@ let get_movable_indices () = (* copying and adjusting map_and_fold_resources *) -let unfold_resources () = +let unfold_resources loc = let rec aux () = let@ s = get () in let@ movable_indices = get_movable_indices () in @@ -421,13 +421,13 @@ let unfold_resources () = | `False -> let keep, unpack, extract = List.fold_right (fun (re, i) (keep, unpack, extract) -> - match Pack.unpack Loc.unknown s.global provable_f re with + match Pack.unpack loc s.global provable_f re with | Some unpackable -> let pname = RET.pp_predicate_name (RET.predicate_name (fst re)) in (keep, (i, pname, unpackable) :: unpack, extract) | None -> let re_reduced, extracted = - Pack.extractable_multiple Loc.unknown provable_f movable_indices re in + Pack.extractable_multiple loc provable_f movable_indices re in let keep' = match extracted with | [] -> (re_reduced, i) :: keep | _ -> @@ -439,15 +439,15 @@ let unfold_resources () = ) resources ([], [], []) in let@ () = set {s with resources = (keep, orig_ix)} in - let rec do_unpacks = function - | [] -> return () - | (_i, pname, lrt) :: rest -> - let@ _, members = make_return_record Loc.unknown ("unpack_" ^ Pp.plain pname) (LogicalReturnTypes.binders lrt) in - let@ () = bind_logical_return_internal Loc.unknown members lrt in - do_unpacks rest + let do_unpack = function + | (_i, pname, `LRT lrt) -> + let@ _, members = make_return_record loc ("unpack_" ^ Pp.plain pname) (LogicalReturnTypes.binders lrt) in + bind_logical_return_internal loc members lrt + | (_i, _pname, `RES res) -> + iterM (add_r_internal loc) res in - let@ () = do_unpacks unpack in - let@ () = iterM (add_r_internal Loc.unknown) extract in + let@ () = iterM do_unpack unpack in + let@ () = iterM (add_r_internal loc) extract in match unpack, extract with | [], [] -> return () | _ -> @@ -658,30 +658,30 @@ let add_movable_index_internal e : unit m = Ok ((), {s with movable_indices = e :: s.movable_indices}) -let add_movable_index e = +let add_movable_index loc e = let@ () = add_movable_index_internal e in - unfold_resources () + unfold_resources loc let add_r loc re = let@ () = add_r_internal loc re in - unfold_resources () + unfold_resources loc let add_rs loc rs = let@ () = iterM (add_r_internal loc) rs in - unfold_resources () + unfold_resources loc -let add_c c = +let add_c loc c = let@ () = add_c_internal c in - unfold_resources () + unfold_resources loc -let add_cs cs = +let add_cs loc cs = let@ () = iterM add_c_internal cs in - unfold_resources () + unfold_resources loc let bind_logical_return loc members lrt = let@ () = bind_logical_return_internal loc members lrt in - unfold_resources () + unfold_resources loc (* Same for return types *) let bind_return loc members (rt : ReturnTypes.t) = diff --git a/backend/cn/typing.mli b/backend/cn/typing.mli index 222016de7..59425b816 100644 --- a/backend/cn/typing.mli +++ b/backend/cn/typing.mli @@ -33,8 +33,8 @@ val add_a_value : Sym.t -> IndexTerms.t -> Context.l_info -> unit m val add_l : Sym.t -> BaseTypes.t -> Context.l_info -> (unit) m val add_l_value : Sym.t -> IndexTerms.t -> Context.l_info -> unit m val add_ls : (Sym.t * BaseTypes.t * Context.l_info) list -> (unit) m -val add_c : LogicalConstraints.t -> (unit) m -val add_cs : LogicalConstraints.t list -> (unit) m +val add_c : Locations.t -> LogicalConstraints.t -> (unit) m +val add_cs : Locations.t -> LogicalConstraints.t list -> (unit) m val add_r : Locations.t -> Resources.t -> unit m val add_rs : Locations.t -> Resources.t list -> unit m val get_loc_trace : unit -> (Locations.loc list) m @@ -118,6 +118,7 @@ val bind_return: val add_movable_index: + Locations.t -> (ResourceTypes.predicate_name * IndexTerms.t) -> unit m diff --git a/backend/cn/wellTyped.ml b/backend/cn/wellTyped.ml index cde84fe77..10c84a285 100644 --- a/backend/cn/wellTyped.ml +++ b/backend/cn/wellTyped.ml @@ -585,7 +585,7 @@ module WIT = struct let@ t1 = infer loc t1 in pure begin let@ () = add_l name (IT.bt t1) (loc, lazy (Pp.string "let-var")) in - let@ () = add_c (LC.t_ (IT.def_ name t1)) in + let@ () = add_c loc (LC.t_ (IT.def_ name t1)) in let@ t2 = infer loc t2 in return (IT (Let ((name, t1), t2), IT.bt t2)) end @@ -759,7 +759,7 @@ module WLRT = struct (* let s, lrt = LRT.alpha_rename (s, IT.bt it) lrt in *) let@ it = WIT.infer loc it in let@ () = add_l s (IT.bt it) (loc, lazy (Pp.string "let-var")) in - let@ () = add_c (LC.t_ (IT.def_ s it)) in + let@ () = add_c (fst info) (LC.t_ (IT.def_ s it)) in let@ lrt = aux lrt in return (Define ((s, it), info, lrt)) | Resource ((s, (re, re_oa_spec)), info, lrt) -> @@ -773,7 +773,7 @@ module WLRT = struct return (Resource ((s, (re, re_oa_spec)), info, lrt)) | Constraint (lc, info, lrt) -> let@ lc = WLC.welltyped (fst info) lc in - let@ () = add_c lc in + let@ () = add_c (fst info) lc in let@ lrt = aux lrt in return (Constraint (lc, info, lrt)) | I -> @@ -831,7 +831,7 @@ module WLAT = struct (* let s, at = LAT.alpha_rename i_subst (s, IT.bt it) at in *) let@ it = WIT.infer loc it in let@ () = add_l s (IT.bt it) (loc, lazy (Pp.string "let-var")) in - let@ () = add_c (LC.t_ (IT.def_ s it)) in + let@ () = add_c (fst info) (LC.t_ (IT.def_ s it)) in let@ at = aux at in return (LAT.Define ((s, it), info, at)) | LAT.Resource ((s, (re, re_oa_spec)), info, at) -> @@ -845,7 +845,7 @@ module WLAT = struct return (LAT.Resource ((s, (re, re_oa_spec)), info, at)) | LAT.Constraint (lc, info, at) -> let@ lc = WLC.welltyped (fst info) lc in - let@ () = add_c lc in + let@ () = add_c (fst info) lc in let@ at = aux at in return (LAT.Constraint (lc, info, at)) | LAT.I i -> @@ -929,7 +929,7 @@ module WLArgs = struct (* let s, at = LAT.alpha_rename i_subst (s, IT.bt it) at in *) let@ it = WIT.infer loc it in let@ () = add_l s (IT.bt it) (loc, lazy (Pp.string "let-var")) in - let@ () = add_c (LC.t_ (IT.def_ s it)) in + let@ () = add_c (fst info) (LC.t_ (IT.def_ s it)) in let@ at, typ = aux at in return (Mu.M_Define ((s, it), info, at), LAT.Define ((s, it), info, typ)) @@ -945,7 +945,7 @@ module WLArgs = struct LAT.Resource ((s, (re, re_oa_spec)), info, typ)) | Mu.M_Constraint (lc, info, at) -> let@ lc = WLC.welltyped (fst info) lc in - let@ () = add_c lc in + let@ () = add_c (fst info) lc in let@ at, typ = aux at in return (Mu.M_Constraint (lc, info, at), LAT.Constraint (lc, info, typ)) @@ -1042,8 +1042,8 @@ module WRPD = struct let@ guard = WIT.check loc BT.Bool guard in let negated_guards = List.map (fun clause -> IT.not_ clause.guard) acc in pure begin - let@ () = add_c (LC.t_ guard) in - let@ () = add_c (LC.t_ (IT.and_ negated_guards)) in + let@ () = add_c loc (LC.t_ guard) in + let@ () = add_c loc (LC.t_ (IT.and_ negated_guards)) in let@ packing_ft = WLAT.welltyped IT.subst (fun loc it -> WIT.check loc pd.oarg_bt it) "clause" loc packing_ft