[rust][TreeBorrows] Follow Pulse equalities in the borrow state

infer/src/pulse/PulseTreeBorrows.ml

@@ -300,6 +300,120 @@ module St = struct
           go state visited (List.rev_append children order) (rest @ children)
     in
     go state (AVSet.singleton av) [av] [av]
+
+
+  let perm_severity (p : Perm.t) =
+    match p with
+    | Perm.Reserved ->
+        0
+    | Perm.ReservedConflicted ->
+        1
+    | Perm.Unique ->
+        2
+    | Perm.Frozen ->
+        3
+    | Perm.Disabled ->
+        4
+
+
+  let perm_join a b = if perm_severity a >= perm_severity b then a else b
+
+  let redirect_tag state ~from ~to_ =
+    let sub t = if Tag.equal t from then to_ else t in
+    let parent =
+      Tag.Map.map
+        (function Some p when Tag.equal p from -> Some to_ | other -> other)
+        (Tag.Map.remove from state.parent)
+    in
+    let tags_at =
+      AVMap.map
+        (fun entries ->
+          match Tag.Map.find_opt from entries with
+          | None ->
+              entries
+          | Some p ->
+              let entries = Tag.Map.remove from entries in
+              Tag.Map.update to_
+                (function None -> Some p | Some p0 -> Some (perm_join p0 p))
+                entries )
+        state.tags_at
+    in
+    let pointer_tag = AVMap.map sub state.pointer_tag in
+    let temps = IdentMap.map sub state.temps in
+    let object_root = AVMap.map sub state.object_root in
+    {state with parent; tags_at; pointer_tag; temps; object_root}
+
+
+  let merge_owner_trees state ~survivor ~victim =
+    let ms = tag_info_of state survivor and mv = tag_info_of state victim in
+    let merged =
+      { Tag.Info.protector= ms.Tag.Info.protector || mv.Tag.Info.protector
+      ; borrowed_cell=
+          ( match ms.Tag.Info.borrowed_cell with
+          | Some _ ->
+              ms.Tag.Info.borrowed_cell
+          | None ->
+              mv.Tag.Info.borrowed_cell ) }
+    in
+    let tag_infos = Tag.Map.add survivor merged (Tag.Map.remove victim state.tag_infos) in
+    redirect_tag {state with tag_infos} ~from:victim ~to_:survivor
+
+
+  let canonicalize_owners state ~f =
+    let tags_at =
+      AVMap.fold
+        (fun av entries m ->
+          let av' = f av in
+          match AVMap.find_opt av' m with
+          | None ->
+              AVMap.add av' entries m
+          | Some entries0 ->
+              AVMap.add av' (Tag.Map.union (fun _ p0 p -> Some (perm_join p0 p)) entries0 entries) m )
+        state.tags_at AVMap.empty
+    in
+    let pointer_tag =
+      AVMap.fold
+        (fun av tag m ->
+          let av' = f av in
+          match AVMap.find_opt av' m with
+          | Some tag0 when not (Tag.equal tag0 tag) ->
+              AVMap.remove av' m
+          | _ ->
+              AVMap.add av' tag m )
+        state.pointer_tag AVMap.empty
+    in
+    let tag_infos =
+      Tag.Map.map
+        (fun m -> {m with Tag.Info.borrowed_cell= Option.map m.Tag.Info.borrowed_cell ~f})
+        state.tag_infos
+    in
+    let state = {state with tags_at; pointer_tag; tag_infos} in
+    let object_root, merges =
+      AVMap.fold
+        (fun av tag (m, ms) ->
+          let av' = f av in
+          match AVMap.find_opt av' m with
+          | Some tag0 when not (Tag.equal tag0 tag) ->
+              let s, v = if Tag.compare tag0 tag <= 0 then (tag0, tag) else (tag, tag0) in
+              (AVMap.add av' s m, (s, v) :: ms)
+          | _ ->
+              (AVMap.add av' tag m, ms) )
+        state.object_root (AVMap.empty, [])
+    in
+    let state = {state with object_root} in
+    let resolve redirects t =
+      let rec go t = match Tag.Map.find_opt t redirects with Some t' -> go t' | None -> t in
+      go t
+    in
+    let state, redirects =
+      List.fold merges ~init:(state, Tag.Map.empty) ~f:(fun (st, rd) (s, v) ->
+          let s = resolve rd s and v = resolve rd v in
+          if Tag.equal s v then (st, rd)
+          else
+            let s, v = if Tag.compare s v <= 0 then (s, v) else (v, s) in
+            (merge_owner_trees st ~survivor:s ~victim:v, Tag.Map.add v s rd) )
+    in
+    {state with object_root= AVMap.map (resolve redirects) state.object_root}
 end
 
 type error = {loc: Location.t; description: string} [@@deriving compare, equal]
@@ -308,6 +422,8 @@ type state = {st: St.t; errors: error list} [@@deriving compare, equal]
 
 let start () = {st= St.empty; errors= []}
 
+let canonicalize ~f (state : state) : state = {state with st= St.canonicalize_owners state.st ~f}
+
 let do_reborrow ~(protector : bool) (st : St.t) ~(succs : AbstractValue.t -> AbstractValue.t list)
     ~(bind : AbstractValue.t option) ~(is_mut : bool) ~(src : Operand.t)
     ~(borrowed_cell : AbstractValue.t) : St.t * Tag.t option =

infer/src/pulse/PulseTreeBorrows.mli

@@ -73,4 +73,6 @@ val exec_store :
   -> state
   -> state
 
+val canonicalize : f:(AbstractValue.t -> AbstractValue.t) -> state -> state
+
 val report_errors : Procdesc.t -> Errlog.t -> state -> unit

infer/src/pulse/PulseTreeBorrowsOperations.ml

@@ -12,6 +12,10 @@ module Operand = PulseTreeBorrows.Operand
 
 let get_var_repr astate v = Formula.get_var_repr astate.AbductiveDomain.path_condition v
 
+let canonicalize_tb astate =
+  PulseTreeBorrows.canonicalize ~f:(get_var_repr astate) (AbductiveDomain.get_tree_borrows astate)
+
+
 let succs_of_heap ~get_var_repr heap av =
   match UnsafeMemory.find_opt av heap with
   | None ->
@@ -100,8 +104,7 @@ let operand_of_exp astate exp : Operand.t =
 let exec_load ~id ~e ~typ ~loc (astate : AbductiveDomain.t) =
   let src = operand_of_exp astate e in
   AbductiveDomain.set_tree_borrows
-    (PulseTreeBorrows.exec_load ~id ~typ ~src ~succs:(succs_of astate) ~loc
-       (AbductiveDomain.get_tree_borrows astate) )
+    (PulseTreeBorrows.exec_load ~id ~typ ~src ~succs:(succs_of astate) ~loc (canonicalize_tb astate))
     astate
 
 
@@ -110,7 +113,7 @@ let exec_store ~lhs ~rhs ~typ ~loc (astate : AbductiveDomain.t) =
   let rhs = operand_of_exp astate rhs in
   AbductiveDomain.set_tree_borrows
     (PulseTreeBorrows.exec_store ~lhs ~rhs ~typ ~succs:(succs_of astate) ~loc
-       (AbductiveDomain.get_tree_borrows astate) )
+       (canonicalize_tb astate) )
     astate
 
 
@@ -124,5 +127,5 @@ let exec_retag ~dst_exp ~src_exp ~is_mut ~loc (astate : AbductiveDomain.t) =
   let src = operand_of_exp astate src_exp in
   AbductiveDomain.set_tree_borrows
     (PulseTreeBorrows.exec_retag ~dst ~src ~is_mut ~protected:false ~succs:(succs_of astate) ~loc
-       (AbductiveDomain.get_tree_borrows astate) )
+       (canonicalize_tb astate) )
     astate