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

@@ -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 =

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, [])
 
 
+

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

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