Skip to content

Commit

Permalink
[CN] improve CN performance (#436)
Browse files Browse the repository at this point in the history
CN derives constraints from resource ownership; this fixes (some of
the) duplication in what constraints are derived
  • Loading branch information
cp526 authored Jul 26, 2024
1 parent 74f5b37 commit 31ad5db
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 11 deletions.
24 changes: 14 additions & 10 deletions backend/cn/lib/resources.ml
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,8 @@ let addr_of pointer =


(* assumption: the resource is owned *)
let derived_lc1 = function
let derived_lc1 (resource, _) =
match resource with
| P { name = Owned (ct, _); pointer; iargs = _ } ->
let here = Locations.other (__FUNCTION__ ^ ":" ^ string_of_int __LINE__) in
let addr = addr_of pointer in
Expand All @@ -59,7 +60,7 @@ let derived_lc1 = function

(* assumption: both resources are owned at the same *)
(* todo, depending on how much we need *)
let derived_lc2 resource (resource', _) =
let derived_lc2 (resource, _) (resource', _) =
match (resource, resource') with
| ( P { name = Owned (ct1, _); pointer = p1; iargs = _ },
P { name = Owned (ct2, _); pointer = p2; iargs = _ } ) ->
Expand All @@ -72,11 +73,14 @@ let derived_lc2 resource (resource', _) =
| _ -> []


let pointer_facts =
let rec aux acc = function
| [] -> acc
| (r, _) :: rs ->
let acc = derived_lc1 r @ List.concat_map (derived_lc2 r) rs @ acc in
aux acc rs
in
fun resources -> aux [] resources
(* let pointer_facts = *)
(* let rec aux acc = function *)
(* | [] -> acc *)
(* | (r, _) :: rs -> *)
(* let acc = derived_lc1 r @ List.concat_map (derived_lc2 r) rs @ acc in *)
(* aux acc rs *)
(* in *)
(* fun resources -> aux [] resources *)

let pointer_facts ~new_resource ~old_resources =
derived_lc1 new_resource @ List.concat_map (derived_lc2 new_resource) old_resources
6 changes: 5 additions & 1 deletion backend/cn/lib/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -445,7 +445,11 @@ let add_r_internal loc (r, RE.O oargs) =
let@ simp_ctxt = simp_ctxt () in
let r = Simplify.ResourceTypes.simp simp_ctxt r in
let oargs = Simplify.IndexTerms.simp simp_ctxt oargs in
let pointer_facts = Resources.pointer_facts ((r, RE.O oargs) :: Context.get_rs s) in
let pointer_facts =
Resources.pointer_facts
~new_resource:(r, RE.O oargs)
~old_resources:(Context.get_rs s)
in
let@ () = set_typing_context (Context.add_r loc (r, O oargs) s) in
iterM (fun x -> add_c_internal (LC.T x)) pointer_facts

Expand Down

0 comments on commit 31ad5db

Please sign in to comment.