Alternative resource inference scheme

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 })

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)))
 

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)

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)

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