From 4ddee12939f32c419a714bb8be6e07723769946e Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Wed, 11 Dec 2024 14:49:34 +0000 Subject: [PATCH] Alternative resource inference scheme Not all predicates are automatically un/packed. Instead, resources with multiple clauses (including recursive predicates) are only packed when instructed by the user. --- backend/cn/lib/check.ml | 8 ++++-- backend/cn/lib/pack.ml | 42 ++++++++++++++++++++++++----- backend/cn/lib/resourceInference.ml | 3 ++- backend/cn/lib/typing.ml | 17 +++++++++++- backend/cn/lib/typing.mli | 4 +++ 5 files changed, 64 insertions(+), 10 deletions(-) diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index 3f0d54d36..fef1aa8d5 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -1845,8 +1845,12 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m = let aux loc stmt = (* copying bits of code from elsewhere in check.ml *) match stmt with - | Cnprog.Pack_unpack (_pack_unpack, _pt) -> - warn loc !^"Explicit pack/unpack unsupported."; + | Cnprog.Pack_unpack (Pack, pt) -> + let@ pt = WellTyped.WReq.welltyped loc (P pt) in + let pt = match pt with P pt -> pt | Q _ -> assert false in + add_packable_resource loc pt + | Cnprog.Pack_unpack (Unpack, _pt) -> + warn loc !^"Explicit unpack unsupported."; return () | To_from_bytes ((To | From), { name = PName _; _ }) -> fail (fun _ -> { loc; msg = Byte_conv_needs_owned }) diff --git a/backend/cn/lib/pack.ml b/backend/cn/lib/pack.ml index aeeb9da63..4f2411056 100644 --- a/backend/cn/lib/pack.ml +++ b/backend/cn/lib/pack.ml @@ -39,7 +39,7 @@ let unfolded_array loc' init (ict, olength) pointer = } -let packing_ft loc global provable ret = +let packing_ft loc global provable packable_resources ret = match ret with | P ret -> (match ret.name with @@ -90,9 +90,39 @@ let packing_ft loc global provable ret = Some at | PName pn -> let def = Sym.Map.find pn global.resource_predicates in - (match Predicate.identify_right_clause provable def ret.pointer ret.iargs with - | None -> None - | Some right_clause -> Some right_clause.packing_ft)) + let packing_permitted = + match def.clauses with + | None -> false + | Some [] -> assert false + | Some [ _single_clause ] -> true + | Some _multiple_clauses -> + let in_packable_list = + let open Request.Predicate in + let loc' = Cerb_location.other __FUNCTION__ in + IT.or_ + (List.filter_map + (fun packable -> + match packable.name with + | PName pn' when Sym.equal pn' pn -> + Some + (IT.and_ + (List.map2 + (fun a b -> IT.eq__ a b loc') + (packable.pointer :: packable.iargs) + (ret.pointer :: ret.iargs)) + loc') + | _ -> None) + packable_resources) + loc' + in + (match provable (LC.T in_packable_list) with `True -> true | `False -> false) + in + if not packing_permitted then + None + else ( + match Predicate.identify_right_clause provable def ret.pointer ret.iargs with + | None -> None + | Some right_clause -> Some right_clause.packing_ft)) | Q _ -> None @@ -134,14 +164,14 @@ let unpack_owned loc global (ct, init) pointer (O o) = Some res -let unpack loc global provable (ret, O o) = +let unpack loc global provable packable_resources (ret, O o) = match ret with | P { name = Owned (ct, init); pointer; iargs = [] } -> (match unpack_owned loc global (ct, init) pointer (O o) with | None -> None | Some re -> Some (`RES re)) | _ -> - (match packing_ft loc global provable ret with + (match packing_ft loc global provable packable_resources ret with | None -> None | Some packing_ft -> Some (`LRT (Definition.Clause.lrt o packing_ft))) diff --git a/backend/cn/lib/resourceInference.ml b/backend/cn/lib/resourceInference.ml index 706182772..0dd72b522 100644 --- a/backend/cn/lib/resourceInference.ml +++ b/backend/cn/lib/resourceInference.ml @@ -227,7 +227,8 @@ module General = struct match needed with | false -> return (Some ((requested, oarg), changed_or_deleted)) | true -> - (match Pack.packing_ft here global provable (P requested) with + let@ packable_resources = get_packable_resources () in + (match Pack.packing_ft here global provable packable_resources (P requested) with | Some packing_ft -> let ft_pp = lazy (LogicalArgumentTypes.pp (fun _ -> Pp.string "resource") packing_ft) diff --git a/backend/cn/lib/typing.ml b/backend/cn/lib/typing.ml index c4f74ef25..fca9d00c7 100644 --- a/backend/cn/lib/typing.ml +++ b/backend/cn/lib/typing.ml @@ -14,6 +14,7 @@ type s = past_models : (Solver.model_with_q * Context.t) list; found_equalities : EqTable.table; movable_indices : (Req.name * IT.t) list; + packable_resources : Request.Predicate.t list; unfold_resources_required : bool; log : Explain.log } @@ -24,6 +25,7 @@ let empty_s (c : Context.t) = sym_eqs = Sym.Map.empty; past_models = []; found_equalities = EqTable.empty; + packable_resources = []; movable_indices = []; unfold_resources_required = false; log = [] @@ -419,6 +421,12 @@ let init_solver () = { s with solver = Some solver }) +let get_packable_resources () = inspect (fun s -> s.packable_resources) + +let set_packable_resources res : unit m = + modify (fun s -> { s with packable_resources = res }) + + let get_movable_indices () = inspect (fun s -> s.movable_indices) let set_movable_indices ixs : unit m = modify (fun s -> { s with movable_indices = ixs }) @@ -452,6 +460,12 @@ let add_r_internal ?(derive_constraints = true) loc (r, Res.O oargs) = iterM (fun x -> add_c_internal (LC.T x)) pointer_facts +let add_packable_resource _loc re = + let@ res = get_packable_resources () in + let@ () = set_packable_resources (re :: res) in + set_unfold_resources () + + let add_movable_index _loc (pred, ix) = let@ ixs = get_movable_indices () in let@ () = set_movable_indices ((pred, ix) :: ixs) in @@ -678,6 +692,7 @@ let map_and_fold_resources_internal loc (f : Res.t -> 'acc -> changed * 'acc) (a let do_unfold_resources loc = let rec aux () = let@ s = get_typing_context () in + let@ packable_resources = get_packable_resources () in let@ movable_indices = get_movable_indices () in let@ _provable_f = provable_internal (Locations.other __FUNCTION__) in let resources, orig_ix = s.resources in @@ -692,7 +707,7 @@ let do_unfold_resources loc = let keep, unpack, extract = List.fold_right (fun (re, i) (keep, unpack, extract) -> - match Pack.unpack loc s.global provable_f2 re with + match Pack.unpack loc s.global provable_f2 packable_resources re with | Some unpackable -> let pname = Req.get_name (fst re) in (keep, (i, pname, unpackable) :: unpack, extract) diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli index b46997b96..2e65b83bd 100644 --- a/backend/cn/lib/typing.mli +++ b/backend/cn/lib/typing.mli @@ -166,12 +166,16 @@ val bind_logical_return val bind_return : Locations.t -> IndexTerms.t list -> ReturnTypes.t -> IndexTerms.t m +val add_packable_resource : Locations.t -> Request.Predicate.t -> unit m + val add_movable_index : Locations.t -> (* verbose:bool -> *) Request.name * IndexTerms.t -> unit m +val get_packable_resources : unit -> Request.Predicate.t list m + val get_movable_indices : unit -> (Request.name * IndexTerms.t) list m val record_action : Explain.action * Locations.t -> unit m