[pulse] Refactor attributes into domain

Summary: Let's move attributes into Pulse's domain.

Reviewed By: jvillard

Differential Revision: D19533915

fbshipit-source-id: 995fd12da

infer/src/absint/AbstractDomain.ml

@@ -616,6 +616,10 @@ module SafeInvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain
 
   let find_last_opt = M.find_last_opt
 
+  let fold_map = M.fold_map
+
+  let of_seq = M.of_seq
+
   let mapi f m =
     let tops = ref [] in
     let f k v =

infer/src/checkers/impurity.ml

@@ -52,7 +52,6 @@ let add_invalid_and_modified ~check_empty attrs acc =
 let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
   let pre_heap = (AbductiveDomain.extract_pre pre_post).BaseDomain.heap in
   let post = AbductiveDomain.extract_post pre_post in
-  let post_heap = post.BaseDomain.heap in
   let post_stack = post.BaseDomain.stack in
   let add_to_modified var addr acc =
     let rec aux acc ~addr_to_explore ~visited : ImpurityDomain.trace list =
@@ -62,20 +61,20 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
       | addr :: addr_to_explore -> (
           if AbstractValue.Set.mem addr visited then aux acc ~addr_to_explore ~visited
           else
-            let cell_pre_opt = BaseMemory.find_opt addr pre_heap in
-            let cell_post_opt = BaseMemory.find_opt addr post_heap in
+            let edges_pre_opt = BaseMemory.find_opt addr pre_heap in
+            let cell_post_opt = BaseDomain.find_cell_opt addr post in
             let visited = AbstractValue.Set.add addr visited in
-            match (cell_pre_opt, cell_post_opt) with
+            match (edges_pre_opt, cell_post_opt) with
             | None, None ->
                 aux acc ~addr_to_explore ~visited
-            | Some (_, _pre_attrs), None ->
+            | Some _, None ->
                 L.(die InternalError)
                   "It is unexpected to have an address which has a binding in pre but not in post!"
-            | None, Some (_edges_post, attrs_post) ->
+            | None, Some (_, attrs_post) ->
                 aux
                   (add_invalid_and_modified ~check_empty:false attrs_post acc)
                   ~addr_to_explore ~visited
-            | Some (edges_pre, _), Some (edges_post, attrs_post) -> (
+            | Some edges_pre, Some (edges_post, attrs_post) -> (
               match get_matching_dest_addr_opt ~edges_pre ~edges_post with
               | Some addr_list ->
                   aux
@@ -100,7 +99,7 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
            match BaseStack.find_opt var post_stack with
            | Some (addr, _) when Typ.is_pointer typ -> (
              match BaseMemory.find_opt addr pre_heap with
-             | Some (edges_pre, _) ->
+             | Some edges_pre ->
                  BaseMemory.Edges.fold
                    (fun _ (addr, _) acc -> add_to_modified var addr acc)
                    edges_pre acc

infer/src/istd/PrettyPrintable.ml

@@ -114,6 +114,10 @@ module type MonoMap = sig
   val mapi : (key -> value -> value) -> t -> t
 
   val is_singleton_or_more : t -> (key * value) IContainer.singleton_or_more
+
+  val fold_map : t -> init:'a -> f:('a -> value -> 'a * value) -> 'a * t
+
+  val of_seq : (key * value) Seq.t -> t
 end
 
 module type PPMap = sig

infer/src/istd/PrettyPrintable.mli

@@ -116,6 +116,10 @@ module type MonoMap = sig
   val mapi : (key -> value -> value) -> t -> t
 
   val is_singleton_or_more : t -> (key * value) IContainer.singleton_or_more
+
+  val fold_map : t -> init:'a -> f:('a -> value -> 'a * value) -> 'a * t
+
+  val of_seq : (key * value) Seq.t -> t
 end
 
 module type PPMap = sig

infer/src/pulse/PulseAbductiveDomain.ml

@@ -12,6 +12,7 @@ module BaseDomain = PulseBaseDomain
 module BaseStack = PulseBaseStack
 module BaseMemory = PulseBaseMemory
 module BaseSkippedCallsMap = BaseDomain.SkippedCallsMap
+module BaseAddressAttributes = PulseBaseAddressAttributes
 
 (** signature common to the "normal" [Domain], representing the post at the current program point,
     and the inverted [InvertedDomain], representing the inferred pre-condition*)
@@ -22,34 +23,50 @@ module type BaseDomain = sig
 
   val empty : t
 
-  val make : BaseStack.t -> BaseMemory.t -> BaseSkippedCallsMap.t -> t
-
   val update :
-    ?stack:BaseStack.t -> ?heap:BaseMemory.t -> ?skipped_calls_map:BaseSkippedCallsMap.t -> t -> t
+       ?stack:BaseStack.t
+    -> ?heap:BaseMemory.t
+    -> ?skipped_calls_map:BaseSkippedCallsMap.t
+    -> ?attrs:BaseAddressAttributes.t
+    -> t
+    -> t
+
+  val filter_addr : f:(AbstractValue.t -> bool) -> t -> t
+  (**filter both heap and attrs *)
 
   include AbstractDomain.NoJoin with type t := t
 end
 
-(* just to expose the [heap] and [stack] record field names without having to type
+(* just to expose record field names without having to type
    [BaseDomain.heap] *)
 type base_domain = BaseDomain.t =
-  {heap: BaseMemory.t; stack: BaseStack.t; skipped_calls_map: BaseSkippedCallsMap.t}
+  { heap: BaseMemory.t
+  ; stack: BaseStack.t
+  ; skipped_calls_map: BaseSkippedCallsMap.t
+  ; attrs: BaseAddressAttributes.t }
 
 (** operations common to [Domain] and [InvertedDomain], see also the [BaseDomain] signature *)
 module BaseDomainCommon = struct
-  let make stack heap skipped_calls_map = {stack; heap; skipped_calls_map}
-
-  let update ?stack ?heap ?skipped_calls_map foot =
-    let new_stack, new_heap, new_skipped_calls_map =
+  let update ?stack ?heap ?skipped_calls_map ?attrs foot =
+    let new_stack, new_heap, new_skipped_calls_map, new_attrs =
       ( Option.value ~default:foot.stack stack
       , Option.value ~default:foot.heap heap
-      , Option.value ~default:foot.skipped_calls_map skipped_calls_map )
+      , Option.value ~default:foot.skipped_calls_map skipped_calls_map
+      , Option.value ~default:foot.attrs attrs )
     in
     if
       phys_equal new_stack foot.stack && phys_equal new_heap foot.heap
       && phys_equal new_skipped_calls_map foot.skipped_calls_map
+      && phys_equal new_attrs foot.attrs
     then foot
-    else {stack= new_stack; heap= new_heap; skipped_calls_map= new_skipped_calls_map}
+    else
+      {stack= new_stack; heap= new_heap; skipped_calls_map= new_skipped_calls_map; attrs= new_attrs}
+
+
+  let filter_addr ~f foot =
+    let heap' = BaseMemory.filter (fun address _ -> f address) foot.heap in
+    let attrs' = BaseAddressAttributes.filter (fun address _ -> f address) foot.attrs in
+    update ~heap:heap' ~attrs:attrs' foot
 end
 
 (** represents the post abstract state at each program point *)
@@ -120,8 +137,7 @@ module Stack = struct
             (* HACK: do not record the history of values in the pre as they are unused *)
             let foot_stack = BaseStack.add var (addr, []) (astate.pre :> base_domain).stack in
             let foot_heap = BaseMemory.register_address addr (astate.pre :> base_domain).heap in
-            let pre_skipped_calls_map = (astate.pre :> base_domain).skipped_calls_map in
-            InvertedDomain.make foot_stack foot_heap pre_skipped_calls_map
+            InvertedDomain.update ~stack:foot_stack ~heap:foot_heap astate.pre
           else astate.pre
         in
         ({post= Domain.update astate.post ~stack:post_stack; pre}, addr_hist)
@@ -149,39 +165,88 @@ module Stack = struct
   let exists f astate = BaseStack.exists f (astate.post :> base_domain).stack
 end
 
-module Memory = struct
+module AddressAttributes = struct
   open Result.Monad_infix
-  module Access = BaseMemory.Access
-
-  (** [astate] with [astate.post.heap = f astate.post.heap] *)
-  let map_post_heap ~f astate =
-    let new_post = Domain.update astate.post ~heap:(f (astate.post :> base_domain).heap) in
-    if phys_equal new_post astate.post then astate else {astate with post= new_post}
-
 
   (** if [address] is in [pre] then add the attribute [attr] *)
   let abduce_attribute address attribute astate =
     L.d_printfln "Abducing %a:%a" AbstractValue.pp address Attribute.pp attribute ;
     let new_pre =
-      if BaseMemory.mem_edges address (astate.pre :> base_domain).heap then
+      if BaseMemory.mem address (astate.pre :> base_domain).heap then
         InvertedDomain.update astate.pre
-          ~heap:(BaseMemory.add_attribute address attribute (astate.pre :> base_domain).heap)
+          ~attrs:(BaseAddressAttributes.add_one address attribute (astate.pre :> base_domain).attrs)
       else astate.pre
     in
     if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre}
 
 
   let check_valid access_trace addr astate =
-    BaseMemory.check_valid addr (astate.post :> base_domain).heap
+    BaseAddressAttributes.check_valid addr (astate.post :> base_domain).attrs
     >>| fun () ->
     (* if [address] is in [pre] and it should be valid then that fact goes in the precondition *)
     abduce_attribute addr (MustBeValid access_trace) astate
 
 
+  (** [astate] with [astate.post.attrs = f astate.post.attrs] *)
+  let map_post_attrs ~f astate =
+    let new_post = Domain.update astate.post ~attrs:(f (astate.post :> base_domain).attrs) in
+    if phys_equal new_post astate.post then astate else {astate with post= new_post}
+
+
+  let invalidate address invalidation location astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.invalidate address invalidation location)
+
+
+  let add_one address attributes astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.add_one address attributes)
+
+
+  let get_closure_proc_name addr astate =
+    BaseAddressAttributes.get_closure_proc_name addr (astate.post :> base_domain).attrs
+
+
+  let get_arithmetic addr astate =
+    BaseAddressAttributes.get_arithmetic addr (astate.post :> base_domain).attrs
+
+
+  let get_bo_itv addr astate =
+    BaseAddressAttributes.get_bo_itv addr (astate.post :> base_domain).attrs
+
+
+  let std_vector_reserve addr astate =
+    map_post_attrs astate ~f:(BaseAddressAttributes.std_vector_reserve addr)
+
+
+  let is_std_vector_reserved addr astate =
+    BaseAddressAttributes.is_std_vector_reserved addr (astate.post :> base_domain).attrs
+
+
+  let abduce_and_add value attrs astate =
+    Attributes.fold attrs ~init:astate ~f:(fun astate attr ->
+        let astate =
+          if Attribute.is_suitable_for_pre attr then abduce_attribute value attr astate else astate
+        in
+        add_one value attr astate )
+
+
+  let find_opt address astate =
+    BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs
+end
+
+module Memory = struct
+  module Access = BaseMemory.Access
+  module Edges = BaseMemory.Edges
+
+  (** [astate] with [astate.post.heap = f astate.post.heap] *)
+  let map_post_heap ~f astate =
+    let new_post = Domain.update astate.post ~heap:(f (astate.post :> base_domain).heap) in
+    if phys_equal new_post astate.post then astate else {astate with post= new_post}
+
+
   let add_edge (addr, history) access new_addr_hist location astate =
-    map_post_heap astate ~f:(fun heap ->
-        BaseMemory.add_edge addr access new_addr_hist heap
-        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {location; history})) )
+    map_post_heap astate ~f:(BaseMemory.add_edge addr access new_addr_hist)
+    |> AddressAttributes.map_post_attrs
+         ~f:(BaseAddressAttributes.add_one addr (WrittenTo (Trace.Immediate {location; history})))
 
 
   let find_edge_opt address access astate =
@@ -199,7 +264,7 @@ module Memory = struct
           BaseMemory.add_edge addr_src access addr_hist_dst (astate.post :> base_domain).heap
         in
         let foot_heap =
-          if BaseMemory.mem_edges addr_src (astate.pre :> base_domain).heap then
+          if BaseMemory.mem addr_src (astate.pre :> base_domain).heap then
             (* HACK: do not record the history of values in the pre as they are unused *)
             BaseMemory.add_edge addr_src access (addr_dst, []) (astate.pre :> base_domain).heap
             |> BaseMemory.register_address addr_dst
@@ -210,47 +275,7 @@ module Memory = struct
         , addr_hist_dst )
 
 
-  let invalidate address invalidation location astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.invalidate address invalidation location heap)
-
-
-  let add_attribute address attributes astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.add_attribute address attributes heap)
-
-
-  let get_closure_proc_name addr astate =
-    BaseMemory.get_closure_proc_name addr (astate.post :> base_domain).heap
-
-
-  let get_arithmetic addr astate = BaseMemory.get_arithmetic addr (astate.post :> base_domain).heap
-
-  let get_bo_itv addr astate = BaseMemory.get_bo_itv addr (astate.post :> base_domain).heap
-
-  let std_vector_reserve addr astate =
-    map_post_heap astate ~f:(fun heap -> BaseMemory.std_vector_reserve addr heap)
-
-
-  let is_std_vector_reserved addr astate =
-    BaseMemory.is_std_vector_reserved addr (astate.post :> base_domain).heap
-
-
   let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap
-
-  let set_cell (addr, history) cell location astate =
-    map_post_heap astate ~f:(fun heap ->
-        BaseMemory.set_cell addr cell heap
-        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {location; history})) )
-
-
-  let abduce_and_add_attributes value attrs astate =
-    Attributes.fold attrs ~init:astate ~f:(fun astate attr ->
-        let astate =
-          if Attribute.is_suitable_for_pre attr then abduce_attribute value attr astate else astate
-        in
-        add_attribute value attr astate )
-
-
-  module Edges = BaseMemory.Edges
 end
 
 let mk_initial proc_desc =
@@ -274,8 +299,7 @@ let mk_initial proc_desc =
       List.fold formals ~init:(InvertedDomain.empty :> base_domain).heap
         ~f:(fun heap (_, (addr, _)) -> BaseMemory.register_address addr heap)
     in
-    let initial_skipped_map = (InvertedDomain.empty :> BaseDomain.t).skipped_calls_map in
-    InvertedDomain.make initial_stack initial_heap initial_skipped_map
+    InvertedDomain.update ~stack:initial_stack ~heap:initial_heap InvertedDomain.empty
   in
   let post = Domain.update ~stack:initial_stack Domain.empty in
   {pre; post}
@@ -296,23 +320,31 @@ let add_skipped_calls_map pname trace astate =
 
 let discard_unreachable ({pre; post} as astate) =
   let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in
-  let pre_old_heap = (pre :> BaseDomain.t).heap in
-  let pre_new_heap =
-    BaseMemory.filter (fun address -> AbstractValue.Set.mem address pre_addresses) pre_old_heap
+  let pre_new =
+    InvertedDomain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address pre_addresses) pre
   in
   let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
   let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in
-  let post_old_heap = (post :> BaseDomain.t).heap in
-  let post_new_heap =
-    BaseMemory.filter (fun address -> AbstractValue.Set.mem address all_addresses) post_old_heap
+  let post_new =
+    Domain.filter_addr ~f:(fun address -> AbstractValue.Set.mem address all_addresses) post
   in
-  if phys_equal pre_new_heap pre_old_heap && phys_equal post_new_heap post_old_heap then astate
-  else
-    {pre= InvertedDomain.update pre ~heap:pre_new_heap; post= Domain.update post ~heap:post_new_heap}
+  if phys_equal pre_new pre && phys_equal post_new post then astate
+  else {pre= pre_new; post= post_new}
 
 
 let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
 
+(* {3 Helper functions to traverse the two maps at once } *)
+
+let find_post_cell_opt addr {post} = BaseDomain.find_cell_opt addr (post :> BaseDomain.t)
+
+let set_post_cell (addr, history) (edges_map, attr_set) location astate =
+  Memory.map_post_heap astate ~f:(BaseMemory.add addr edges_map)
+  |> AddressAttributes.map_post_attrs ~f:(fun attrs ->
+         BaseAddressAttributes.add_one addr (WrittenTo (Trace.Immediate {location; history})) attrs
+         |> BaseAddressAttributes.add addr attr_set )
+
+
 module PrePost = struct
   type domain_t = t
 
@@ -326,7 +358,7 @@ module PrePost = struct
     in
     (* deregister empty edges *)
     let deregister_empty heap =
-      BaseMemory.filter_heap (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) heap
+      BaseMemory.filter (fun _addr edges -> not (BaseMemory.Edges.is_empty edges)) heap
     in
     let pre_heap = deregister_empty (astate.pre :> base_domain).heap in
     let post_heap = deregister_empty (astate.post :> base_domain).heap in
@@ -335,19 +367,19 @@ module PrePost = struct
 
 
   let add_out_of_scope_attribute addr pvar location history heap typ =
-    BaseMemory.add_attribute addr
+    BaseAddressAttributes.add_one addr
       (Invalid (GoneOutOfScope (pvar, typ), Immediate {location; history}))
       heap
 
 
   (** invalidate local variables going out of scope *)
   let invalidate_locals pdesc astate : t =
-    let heap : BaseMemory.t = (astate.post :> BaseDomain.t).heap in
-    let heap' =
-      BaseMemory.fold_attrs
-        (fun addr attrs heap ->
+    let attrs : BaseAddressAttributes.t = (astate.post :> BaseDomain.t).attrs in
+    let attrs' =
+      BaseAddressAttributes.fold
+        (fun addr attrs acc ->
           Attributes.get_address_of_stack_variable attrs
-          |> Option.value_map ~default:heap ~f:(fun (var, location, history) ->
+          |> Option.value_map ~default:acc ~f:(fun (var, location, history) ->
                  let get_local_typ_opt pvar =
                    Procdesc.get_locals pdesc
                    |> List.find_map ~f:(fun ProcAttributes.{name; typ} ->
@@ -356,14 +388,14 @@ module PrePost = struct
                  match var with
                  | Var.ProgramVar pvar ->
                      get_local_typ_opt pvar
-                     |> Option.value_map ~default:heap
-                          ~f:(add_out_of_scope_attribute addr pvar location history heap)
+                     |> Option.value_map ~default:acc
+                          ~f:(add_out_of_scope_attribute addr pvar location history acc)
                  | _ ->
-                     heap ) )
-        heap heap
+                     acc ) )
+        attrs attrs
     in
-    if phys_equal heap heap' then astate
-    else {pre= astate.pre; post= Domain.update astate.post ~heap:heap'}
+    if phys_equal attrs attrs' then astate
+    else {pre= astate.pre; post= Domain.update astate.post ~attrs:attrs'}
 
 
   let of_post pdesc astate =
@@ -506,7 +538,7 @@ module PrePost = struct
       match BaseMemory.find_opt addr_pre pre.BaseDomain.heap with
       | None ->
           Ok call_state
-      | Some (edges_pre, _attrs_pre) ->
+      | Some edges_pre ->
           Container.fold_result
             ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold)
             ~init:call_state edges_pre ~f:(fun call_state (access, (addr_pre_dest, _)) ->
@@ -533,11 +565,11 @@ module PrePost = struct
     |> function Some result -> result | None -> Ok call_state
 
 
-  let is_cell_read_only ~cell_pre_opt ~cell_post:(edges_post, attrs_post) =
-    match cell_pre_opt with
+  let is_cell_read_only ~edges_pre_opt ~cell_post:(edges_post, attrs_post) =
+    match edges_pre_opt with
     | None ->
         false
-    | Some (edges_pre, _) when not (Attributes.is_modified attrs_post) ->
+    | Some edges_pre when not (Attributes.is_modified attrs_post) ->
         let are_edges_equal =
           BaseMemory.Edges.equal
             (fun (addr_dest_pre, _) (addr_dest_post, _) ->
@@ -585,7 +617,7 @@ module PrePost = struct
     let v = Symb.Symbol.get_pulse_value_exn s in
     match PulseAbstractValue.Map.find_opt v !subst with
     | Some (v', _) ->
-        Itv.ItvPure.get_bound (Memory.get_bo_itv v' astate) bound_end
+        Itv.ItvPure.get_bound (AddressAttributes.get_bo_itv v' astate) bound_end
     | None ->
         let v' = PulseAbstractValue.mk_fresh () in
         subst := PulseAbstractValue.Map.add v (v', []) !subst ;
@@ -595,7 +627,9 @@ module PrePost = struct
   let subst_attribute call_state subst_ref astate ~addr_caller attr ~addr_callee =
     match (attr : Attribute.t) with
     | Arithmetic (arith_callee, hist) -> (
-        let arith_caller_opt = Memory.get_arithmetic addr_caller astate |> Option.map ~f:fst in
+        let arith_caller_opt =
+          AddressAttributes.get_arithmetic addr_caller astate |> Option.map ~f:fst
+        in
         match
           Arithmetic.abduce_binop_is_true ~negated:false Eq arith_caller_opt (Some arith_callee)
         with
@@ -670,17 +704,17 @@ module PrePost = struct
         add_call_to_attributes callee_proc_name call_location ~addr_callee ~addr_caller
           caller_history callee_attrs call_state
       in
-      let astate = Memory.abduce_and_add_attributes addr_caller attrs_caller call_state.astate in
+      let astate = AddressAttributes.abduce_and_add addr_caller attrs_caller call_state.astate in
       if phys_equal subst call_state.subst && phys_equal astate call_state.astate then call_state
       else {call_state with subst; astate}
     in
     (* check all callee addresses that make sense for the caller, i.e. the domain of [call_state.subst] *)
     AddressMap.fold
       (fun addr_callee addr_hist_caller call_state ->
-        match BaseMemory.find_opt addr_callee (pre_post.pre :> BaseDomain.t).heap with
+        match BaseAddressAttributes.find_opt addr_callee (pre_post.pre :> BaseDomain.t).attrs with
         | None ->
             call_state
-        | Some (_edges, callee_attrs) ->
+        | Some callee_attrs ->
             one_address_sat addr_callee callee_attrs addr_hist_caller call_state )
       call_state.subst call_state
 
@@ -721,15 +755,15 @@ module PrePost = struct
     else ({call_state with subst= new_subst}, addr_hist_caller)
 
 
-  let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~cell_pre_opt ~addr_caller call_state =
-    match BaseMemory.find_edges_opt addr_caller (call_state.astate.post :> base_domain).heap with
+  let delete_edges_in_callee_pre_from_caller ~addr_callee:_ ~edges_pre_opt ~addr_caller call_state =
+    match BaseMemory.find_opt addr_caller (call_state.astate.post :> base_domain).heap with
     | None ->
         BaseMemory.Edges.empty
     | Some old_post_edges -> (
-      match cell_pre_opt with
+      match edges_pre_opt with
       | None ->
           old_post_edges
-      | Some (edges_pre, _) ->
+      | Some edges_pre ->
           BaseMemory.Edges.merge
             (fun _access old_opt pre_opt ->
               (* TODO: should apply [call_state.subst] to [_access]! Actually, should rewrite the
@@ -741,10 +775,10 @@ module PrePost = struct
             old_post_edges edges_pre )
 
 
-  let record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
+  let record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt
       ~cell_post:(edges_post, attrs_post) ~addr_hist_caller:(addr_caller, hist_caller) call_state =
     let post_edges_minus_pre =
-      delete_edges_in_callee_pre_from_caller ~addr_callee ~cell_pre_opt ~addr_caller call_state
+      delete_edges_in_callee_pre_from_caller ~addr_callee ~edges_pre_opt ~addr_caller call_state
     in
     let call_state =
       let subst, attrs_post_caller =
@@ -752,11 +786,12 @@ module PrePost = struct
           attrs_post call_state
       in
       let astate =
-        Memory.abduce_and_add_attributes addr_caller attrs_post_caller call_state.astate
+        AddressAttributes.abduce_and_add addr_caller attrs_post_caller call_state.astate
       in
       {call_state with subst; astate}
     in
     let heap = (call_state.astate.post :> base_domain).heap in
+    let attrs = (call_state.astate.post :> base_domain).attrs in
     let subst, translated_post_edges =
       BaseMemory.Edges.fold_map ~init:call_state.subst edges_post
         ~f:(fun subst (addr_callee, trace_post) ->
@@ -774,10 +809,13 @@ module PrePost = struct
           (fun _ _ post_cell -> Some post_cell)
           post_edges_minus_pre translated_post_edges
       in
+      BaseMemory.add addr_caller edges_post_caller heap
+    in
+    let attrs =
       let written_to =
         let open Option.Monad_infix in
-        BaseMemory.find_opt addr_caller heap
-        >>= (fun (_edges, attrs) -> Attributes.get_written_to attrs)
+        BaseAddressAttributes.find_opt addr_caller attrs
+        >>= (fun attrs -> Attributes.get_written_to attrs)
         |> fun written_to_callee_opt ->
         let callee_trace =
           match written_to_callee_opt with
@@ -793,32 +831,30 @@ module PrePost = struct
              ; location= call_loc
              ; history= hist_caller })
       in
-      BaseMemory.set_edges addr_caller edges_post_caller heap
-      |> BaseMemory.add_attribute addr_caller written_to
+      BaseAddressAttributes.add_one addr_caller written_to attrs
     in
-    let call_post = (call_state.astate.post :> base_domain) in
-    let caller_post = Domain.make call_post.stack heap call_post.skipped_calls_map in
+    let caller_post = Domain.update ~heap ~attrs call_state.astate.post in
     {call_state with subst; astate= {call_state.astate with post= caller_post}}
 
 
-  let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee
+  let rec record_post_for_address callee_proc_name call_loc ({pre} as pre_post) ~addr_callee
       ~addr_hist_caller call_state =
     L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ;
     match visit call_state ~addr_callee ~addr_hist_caller with
     | `AlreadyVisited, call_state ->
         call_state
     | `NotAlreadyVisited, call_state -> (
-      match BaseMemory.find_opt addr_callee (post :> BaseDomain.t).BaseDomain.heap with
+      match find_post_cell_opt addr_callee pre_post with
       | None ->
           call_state
       | Some ((edges_post, _attrs_post) as cell_post) ->
-          let cell_pre_opt =
+          let edges_pre_opt =
             BaseMemory.find_opt addr_callee (pre :> BaseDomain.t).BaseDomain.heap
           in
           let call_state_after_post =
-            if is_cell_read_only ~cell_pre_opt ~cell_post then call_state
+            if is_cell_read_only ~edges_pre_opt ~cell_post then call_state
             else
-              record_post_cell callee_proc_name call_loc ~addr_callee ~cell_pre_opt
+              record_post_cell callee_proc_name call_loc ~addr_callee ~edges_pre_opt
                 ~addr_hist_caller ~cell_post call_state
           in
           IContainer.fold_of_pervasives_map_fold ~fold:Memory.Edges.fold ~init:call_state_after_post
@@ -912,7 +948,7 @@ module PrePost = struct
 
 
   let record_post_remaining_attributes callee_proc_name call_loc pre_post call_state =
-    BaseMemory.fold_attrs
+    BaseAddressAttributes.fold
       (fun addr_callee attrs call_state ->
         if AddressSet.mem addr_callee call_state.visited then
           (* already recorded the attributes when we were walking the edges map *)
@@ -926,9 +962,9 @@ module PrePost = struct
                 add_call_to_attributes callee_proc_name call_loc ~addr_callee ~addr_caller history
                   attrs call_state
               in
-              let astate = Memory.abduce_and_add_attributes addr_caller attrs' call_state.astate in
+              let astate = AddressAttributes.abduce_and_add addr_caller attrs' call_state.astate in
               {call_state with subst; astate} )
-      (pre_post.post :> BaseDomain.t).heap call_state
+      (pre_post.post :> BaseDomain.t).attrs call_state
 
 
   let record_skipped_calls callee_proc_name call_loc pre_post call_state =
@@ -969,7 +1005,7 @@ module PrePost = struct
         | Error _ ->
             astate_result
         | Ok astate -> (
-          match BaseMemory.get_must_be_valid addr_pre (pre :> BaseDomain.t).heap with
+          match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with
           | None ->
               astate_result
           | Some callee_access_trace ->
@@ -980,7 +1016,7 @@ module PrePost = struct
                   ; location= call_location
                   ; history= hist_caller }
               in
-              Memory.check_valid access_trace addr_caller astate
+              AddressAttributes.check_valid access_trace addr_caller astate
               |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
                      L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
                      Diagnostic.AccessToInvalidAddress

infer/src/pulse/PulseAbductiveDomain.mli

@@ -45,12 +45,6 @@ module Memory : sig
   module Access = BaseMemory.Access
   module Edges = BaseMemory.Edges
 
-  val abduce_attribute : AbstractValue.t -> Attribute.t -> t -> t
-  (** add the attribute to the pre, if meaningful (does not modify the post) *)
-
-  val add_attribute : AbstractValue.t -> Attribute.t -> t -> t
-  (** add the attribute only to the post *)
-
   val add_edge :
        AbstractValue.t * ValueHistory.t
     -> Access.t
@@ -59,13 +53,26 @@ module Memory : sig
     -> t
     -> t
 
-  val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result
+  val eval_edge :
+    AbstractValue.t * ValueHistory.t -> Access.t -> t -> t * (AbstractValue.t * ValueHistory.t)
+  (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and
+      returns what it points to or creates a fresh value if that edge didn't exist. *)
 
-  val find_opt : AbstractValue.t -> t -> BaseMemory.cell option
+  val find_opt : AbstractValue.t -> t -> BaseMemory.Edges.t option
 
   val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option
+end
 
-  val set_cell : AbstractValue.t * ValueHistory.t -> BaseMemory.cell -> Location.t -> t -> t
+(** attribute operations like {!BaseAddressAttributes} but that also take care of propagating facts
+    to the precondition *)
+module AddressAttributes : sig
+  val abduce_attribute : AbstractValue.t -> Attribute.t -> t -> t
+  (** add the attribute to the pre, if meaningful (does not modify the post) *)
+
+  val add_one : AbstractValue.t -> Attribute.t -> t -> t
+  (** add the attribute only to the post *)
+
+  val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
@@ -75,18 +82,19 @@ module Memory : sig
 
   val std_vector_reserve : AbstractValue.t -> t -> t
 
-  val eval_edge :
-    AbstractValue.t * ValueHistory.t -> Access.t -> t -> t * (AbstractValue.t * ValueHistory.t)
-  (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and
-      returns what it points to or creates a fresh value if that edge didn't exist. *)
-
   val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
 
   val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
+
+  val find_opt : AbstractValue.t -> t -> Attributes.t option
 end
 
 val is_local : Var.t -> t -> bool
 
+val find_post_cell_opt : AbstractValue.t -> t -> BaseDomain.cell option
+
+val set_post_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.cell -> Location.t -> t -> t
+
 module PrePost : sig
   type domain_t = t
 

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -0,0 +1,86 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+module L = Logging
+open PulseBasicInterface
+
+module AttributesNoRank = struct
+  include Attributes
+
+  let pp fmt t : unit = PulseAttribute.Attributes.pp fmt t
+end
+
+module Graph = PrettyPrintable.MakePPMonoMap (AbstractValue) (AttributesNoRank)
+
+type t = Graph.t
+
+let add_one addr attribute attrs =
+  match Graph.find_opt addr attrs with
+  | None ->
+      Graph.add addr (Attributes.singleton attribute) attrs
+  | Some old_attrs ->
+      let new_attrs = Attributes.add old_attrs attribute in
+      Graph.add addr new_attrs attrs
+
+
+let add addr attributes attrs =
+  match Graph.find_opt addr attrs with
+  | None ->
+      Graph.add addr attributes attrs
+  | Some old_attrs ->
+      let new_attrs = Attributes.union_prefer_left old_attrs attributes in
+      Graph.add addr new_attrs attrs
+
+
+let fold = Graph.fold
+
+let find_opt = Graph.find_opt
+
+let empty = Graph.empty
+
+let filter = Graph.filter
+
+let pp = Graph.pp
+
+let invalidate (address, history) invalidation location memory =
+  add_one address (Attribute.Invalid (invalidation, Immediate {location; history})) memory
+
+
+let check_valid address attrs =
+  L.d_printfln "Checking validity of %a" AbstractValue.pp address ;
+  match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_invalid with
+  | None ->
+      Ok ()
+  | Some invalidation ->
+      Error invalidation
+
+
+let get_attribute getter address attrs =
+  let open Option.Monad_infix in
+  Graph.find_opt address attrs >>= getter
+
+
+let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
+
+let get_arithmetic = get_attribute Attributes.get_arithmetic
+
+let get_bo_itv v memory =
+  match get_attribute Attributes.get_bo_itv v memory with
+  | None ->
+      Itv.ItvPure.of_pulse_value v
+  | Some itv ->
+      itv
+
+
+let get_must_be_valid = get_attribute Attributes.get_must_be_valid
+
+let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory
+
+let is_std_vector_reserved address attrs =
+  Graph.find_opt address attrs
+  |> Option.value_map ~default:false ~f:Attributes.is_std_vector_reserved

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -0,0 +1,41 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+open PulseBasicInterface
+
+type t
+
+val empty : t
+
+val filter : (AbstractValue.t -> Attributes.t -> bool) -> t -> t
+
+val find_opt : AbstractValue.t -> t -> Attributes.t option
+
+val add_one : AbstractValue.t -> Attribute.t -> t -> t
+
+val add : AbstractValue.t -> Attributes.t -> t -> t
+
+val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a
+
+val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result
+
+val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
+
+val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
+
+val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
+
+val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
+
+val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
+
+val std_vector_reserve : AbstractValue.t -> t -> t
+
+val is_std_vector_reserved : AbstractValue.t -> t -> bool
+
+val pp : F.formatter -> t -> unit

infer/src/pulse/PulseBaseDomain.ml

@@ -10,6 +10,7 @@ module L = Logging
 open PulseBasicInterface
 module Memory = PulseBaseMemory
 module Stack = PulseBaseStack
+module AddressAttributes = PulseBaseAddressAttributes
 
 module SkippedTrace = struct
   type t = PulseTrace.t [@@deriving compare]
@@ -23,7 +24,8 @@ module SkippedCallsMap = PrettyPrintable.MakePPMonoMap (Procname) (SkippedTrace)
 
 (* {2 Abstract domain description } *)
 
-type t = {heap: Memory.t; stack: Stack.t; skipped_calls_map: SkippedCallsMap.t}
+type t =
+  {heap: Memory.t; stack: Stack.t; skipped_calls_map: SkippedCallsMap.t; attrs: AddressAttributes.t}
 
 let empty =
   { heap=
@@ -31,7 +33,20 @@ let empty =
       (* TODO: we could record that 0 is an invalid address at this point but this makes the
          analysis go a bit overboard with the Nullptr reports. *)
   ; stack= Stack.empty
-  ; skipped_calls_map= SkippedCallsMap.empty }
+  ; skipped_calls_map= SkippedCallsMap.empty
+  ; attrs= AddressAttributes.empty }
+
+
+type cell = Memory.Edges.t * Attributes.t
+
+let find_cell_opt addr {heap; attrs} =
+  match (Memory.find_opt addr heap, AddressAttributes.find_opt addr attrs) with
+  | None, None ->
+      None
+  | edges_opt, attrs_opt ->
+      let edges = Option.value edges_opt ~default:Memory.Edges.empty in
+      let attrs = Option.value attrs_opt ~default:Attributes.empty in
+      Some (edges, attrs)
 
 
 (** comparison between two elements of the domain to determine the [<=] relation
@@ -107,18 +122,15 @@ module GraphComparison = struct
     | `AliasingRHS | `AliasingLHS ->
         NotIsomorphic
     | `NotAlreadyVisited mapping -> (
-        let get_non_empty_cell = function
-          | None ->
-              None
-          | Some (edges, attrs) when Memory.Edges.is_empty edges && Attributes.is_empty attrs ->
-              (* this can happen because of [register_address] or because we don't care to delete empty
-                 edges when removing edges *)
-              None
-          | Some _ as some_cell ->
-              some_cell
+        let get_non_empty_cell addr astate =
+          find_cell_opt addr astate
+          |> Option.filter ~f:(fun (edges, attrs) ->
+                 not (Memory.Edges.is_empty edges && Attributes.is_empty attrs)
+                 (* this can happen because of [register_address] or because we don't care to delete empty
+                    edges when removing edges *) )
         in
-        let lhs_cell_opt = Memory.find_opt addr_lhs lhs.heap |> get_non_empty_cell in
-        let rhs_cell_opt = Memory.find_opt addr_rhs rhs.heap |> get_non_empty_cell in
+        let lhs_cell_opt = get_non_empty_cell addr_lhs lhs in
+        let rhs_cell_opt = get_non_empty_cell addr_rhs rhs in
         match (lhs_cell_opt, rhs_cell_opt) with
         | None, None ->
             IsomorphicUpTo mapping
@@ -183,11 +195,10 @@ let leq ~lhs ~rhs =
   phys_equal lhs rhs || GraphComparison.is_isograph ~lhs ~rhs GraphComparison.empty_mapping
 
 
-let pp fmt {heap; stack; skipped_calls_map} =
+let pp fmt {heap; stack; skipped_calls_map; attrs} =
   F.fprintf fmt
     "{@[<v1> roots=@[<hv>%a@];@;mem  =@[<hv>%a@];@;attrs=@[<hv>%a@];@;skipped_calls=@[<hv>%a@];@]}"
-    Stack.pp stack Memory.pp_heap heap Memory.pp_attributes heap SkippedCallsMap.pp
-    skipped_calls_map
+    Stack.pp stack Memory.pp heap AddressAttributes.pp attrs SkippedCallsMap.pp skipped_calls_map
 
 
 module GraphVisit : sig
@@ -229,7 +240,7 @@ end = struct
         match Memory.find_opt address astate.heap with
         | None ->
             Continue (visited, accum)
-        | Some (edges, _) ->
+        | Some edges ->
             visit_edges orig_var ~f rev_accesses astate ~edges (visited, accum) )
       | Stop fin ->
           Stop (visited, fin) )

infer/src/pulse/PulseBaseDomain.mli

@@ -15,7 +15,13 @@ end
 module SkippedCallsMap :
   PrettyPrintable.PPMonoMap with type key = Procname.t and type value = SkippedTrace.t
 
-type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t; skipped_calls_map: SkippedCallsMap.t}
+type t =
+  { heap: PulseBaseMemory.t
+  ; stack: PulseBaseStack.t
+  ; skipped_calls_map: SkippedCallsMap.t
+  ; attrs: PulseBaseAddressAttributes.t }
+
+type cell = PulseBaseMemory.Edges.t * Attributes.t
 
 val empty : t
 
@@ -36,3 +42,5 @@ type isograph_relation =
 val isograph_map : lhs:t -> rhs:t -> mapping -> isograph_relation
 
 val is_isograph : lhs:t -> rhs:t -> mapping -> bool
+
+val find_cell_opt : AbstractValue.t -> t -> cell option

infer/src/pulse/PulseBaseMemory.ml

@@ -5,8 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 open! IStd
-module F = Format
-module L = Logging
 open PulseBasicInterface
 
 (* {3 Heap domain } *)
@@ -19,130 +17,31 @@ module Access = struct
   let pp = HilExp.Access.pp AbstractValue.pp
 end
 
-module Edges = PrettyPrintable.MakePPMap (Access)
+module AddrTrace = struct
+  type t = AbstractValue.t * ValueHistory.t [@@deriving compare]
 
-type edges = (AbstractValue.t * ValueHistory.t) Edges.t [@@deriving compare]
-
-let pp_edges =
-  Edges.pp ~pp_value:(fun f addr_trace ->
-      if Config.debug_level_analysis >= 3 then
-        Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp f addr_trace
-      else AbstractValue.pp f (fst addr_trace) )
-
-
-type cell = edges * Attributes.t
-
-module Graph = PrettyPrintable.MakePPMap (AbstractValue)
-
-type t = edges Graph.t * Attributes.t Graph.t
-
-let pp_heap fmt (heap, _) = Graph.pp ~pp_value:pp_edges fmt heap
+  let pp fmt addr_trace =
+    if Config.debug_level_analysis >= 3 then
+      Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp fmt addr_trace
+    else AbstractValue.pp fmt (fst addr_trace)
+end
 
-let pp_attributes fmt (_, attrs) = Graph.pp ~pp_value:Attributes.pp fmt attrs
+module Edges = PrettyPrintable.MakePPMonoMap (Access) (AddrTrace)
+module Graph = PrettyPrintable.MakePPMonoMap (AbstractValue) (Edges)
 
 let register_address addr memory =
-  if Graph.mem addr (fst memory) then memory
-  else (Graph.add addr Edges.empty (fst memory), snd memory)
-
+  if Graph.mem addr memory then memory else Graph.add addr Edges.empty memory
 
-(* {3 Helper functions to traverse the two maps at once } *)
 
 let add_edge addr_src access value memory =
-  let old_edges = Graph.find_opt addr_src (fst memory) |> Option.value ~default:Edges.empty in
+  let old_edges = Graph.find_opt addr_src memory |> Option.value ~default:Edges.empty in
   let new_edges = Edges.add access value old_edges in
-  if phys_equal old_edges new_edges then memory
-  else (Graph.add addr_src new_edges (fst memory), snd memory)
+  if phys_equal old_edges new_edges then memory else Graph.add addr_src new_edges memory
 
 
 let find_edge_opt addr access memory =
   let open Option.Monad_infix in
-  Graph.find_opt addr (fst memory) >>= Edges.find_opt access
-
-
-let add_attribute addr attribute memory =
-  match Graph.find_opt addr (snd memory) with
-  | None ->
-      (fst memory, Graph.add addr (Attributes.singleton attribute) (snd memory))
-  | Some old_attrs ->
-      let new_attrs = Attributes.add old_attrs attribute in
-      (fst memory, Graph.add addr new_attrs (snd memory))
-
-
-let invalidate (address, history) invalidation location memory =
-  add_attribute address (Attribute.Invalid (invalidation, Immediate {location; history})) memory
-
-
-let check_valid address memory =
-  L.d_printfln "Checking validity of %a" AbstractValue.pp address ;
-  match Graph.find_opt address (snd memory) |> Option.bind ~f:Attributes.get_invalid with
-  | None ->
-      Ok ()
-  | Some invalidation ->
-      Error invalidation
-
-
-let get_attribute getter address memory =
-  let open Option.Monad_infix in
-  Graph.find_opt address (snd memory) >>= getter
-
-
-let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
-
-let get_arithmetic = get_attribute Attributes.get_arithmetic
-
-let get_bo_itv v memory =
-  match get_attribute Attributes.get_bo_itv v memory with
-  | None ->
-      Itv.ItvPure.of_pulse_value v
-  | Some itv ->
-      itv
-
-
-let get_must_be_valid = get_attribute Attributes.get_must_be_valid
-
-let std_vector_reserve address memory = add_attribute address Attribute.StdVectorReserve memory
-
-let is_std_vector_reserved address memory =
-  Graph.find_opt address (snd memory)
-  |> Option.value_map ~default:false ~f:(fun attributes ->
-         Attributes.is_std_vector_reserved attributes )
-
-
-(* {3 Monomorphic {!PPMap} interface as needed } *)
-
-let empty = (Graph.empty, Graph.empty)
-
-let find_edges_opt addr memory = Graph.find_opt addr (fst memory)
-
-let find_attrs_opt addr memory = Graph.find_opt addr (snd memory)
-
-let find_opt addr memory =
-  match (find_edges_opt addr memory, find_attrs_opt addr memory) with
-  | None, None ->
-      None
-  | edges_opt, attrs_opt ->
-      let edges = Option.value edges_opt ~default:Edges.empty in
-      let attrs = Option.value attrs_opt ~default:Attributes.empty in
-      Some (edges, attrs)
-
-
-let fold_attrs f memory init = Graph.fold f (snd memory) init
-
-let set_edges addr edges memory = (Graph.add addr edges (fst memory), snd memory)
-
-let set_cell addr (edges, attrs) memory =
-  (Graph.add addr edges (fst memory), Graph.add addr attrs (snd memory))
-
-
-let filter f memory =
-  let heap = Graph.filter (fun address _ -> f address) (fst memory) in
-  let attrs = Graph.filter (fun address _ -> f address) (snd memory) in
-  if phys_equal heap (fst memory) && phys_equal attrs (snd memory) then memory else (heap, attrs)
-
-
-let filter_heap f memory =
-  let heap = Graph.filter f (fst memory) in
-  if phys_equal heap (fst memory) then memory else (heap, snd memory)
+  Graph.find_opt addr memory >>= Edges.find_opt access
 
 
-let mem_edges addr memory = Graph.mem addr (fst memory)
+include Graph

infer/src/pulse/PulseBaseMemory.mli

@@ -5,7 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 open! IStd
-module F = Format
 open PulseBasicInterface
 
 module Access : sig
@@ -14,56 +13,16 @@ module Access : sig
   val equal : t -> t -> bool
 end
 
-module Edges : PrettyPrintable.PPMap with type key = Access.t
-
-type edges = (AbstractValue.t * ValueHistory.t) Edges.t
-
-type cell = edges * Attributes.t
-
-type t
-
-val empty : t
-
-val filter : (AbstractValue.t -> bool) -> t -> t
-
-val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t
-
-val find_opt : AbstractValue.t -> t -> cell option
-
-val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
-
-val set_edges : AbstractValue.t -> edges -> t -> t
-
-val set_cell : AbstractValue.t -> cell -> t -> t
-
-val find_edges_opt : AbstractValue.t -> t -> edges option
-
-val mem_edges : AbstractValue.t -> t -> bool
+module AddrTrace : sig
+  type t = AbstractValue.t * ValueHistory.t
+end
 
-val pp_heap : F.formatter -> t -> unit
+module Edges : PrettyPrintable.PPMonoMap with type key = Access.t and type value = AddrTrace.t
 
-val pp_attributes : F.formatter -> t -> unit
+include PrettyPrintable.PPMonoMap with type key = AbstractValue.t and type value = Edges.t
 
 val register_address : AbstractValue.t -> t -> t
 
-val add_edge : AbstractValue.t -> Access.t -> AbstractValue.t * ValueHistory.t -> t -> t
-
-val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option
-
-val add_attribute : AbstractValue.t -> Attribute.t -> t -> t
-
-val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
-
-val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result
-
-val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
-
-val get_arithmetic : AbstractValue.t -> t -> (Arithmetic.t * Trace.t) option
-
-val get_bo_itv : AbstractValue.t -> t -> Itv.ItvPure.t
-
-val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
-
-val std_vector_reserve : AbstractValue.t -> t -> t
+val add_edge : AbstractValue.t -> Access.t -> AddrTrace.t -> t -> t
 
-val is_std_vector_reserved : AbstractValue.t -> t -> bool
+val find_edge_opt : AbstractValue.t -> Access.t -> t -> AddrTrace.t option

infer/src/pulse/PulseDomainInterface.ml

@@ -11,6 +11,7 @@ module AbductiveDomain = PulseAbductiveDomain
 
 module Stack = AbductiveDomain.Stack
 module Memory = AbductiveDomain.Memory
+module AddressAttributes = AbductiveDomain.AddressAttributes
 
 module BaseDomain = PulseBaseDomain
 (** use only if you know what you are doing or you risk break bi-abduction *)

infer/src/pulse/PulseModels.ml

@@ -41,8 +41,8 @@ module Misc = struct
     let ret_addr = AbstractValue.mk_fresh () in
     let astate =
       let i = IntLit.of_int64 i64 in
-      Memory.add_attribute ret_addr (BoItv (Itv.ItvPure.of_int_lit i)) astate
-      |> Memory.add_attribute ret_addr
+      AddressAttributes.add_one ret_addr (BoItv (Itv.ItvPure.of_int_lit i)) astate
+      |> AddressAttributes.add_one ret_addr
            (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []}))
     in
     Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
@@ -52,8 +52,8 @@ module Misc = struct
    fun ~caller_summary:_ location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let astate =
-      Memory.add_attribute ret_addr (BoItv Itv.ItvPure.nat) astate
-      |> Memory.add_attribute ret_addr
+      AddressAttributes.add_one ret_addr (BoItv Itv.ItvPure.nat) astate
+      |> AddressAttributes.add_one ret_addr
            (Arithmetic (Arithmetic.zero_inf, Immediate {location; history= []}))
     in
     Ok [PulseOperations.write_id ret_id (ret_addr, []) astate]
@@ -78,9 +78,9 @@ module C = struct
     (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we
        currently know about the value. This is purely to avoid contributing to path explosion. *)
     let is_known_zero =
-      ( Memory.get_arithmetic (fst deleted_access) astate
+      ( AddressAttributes.get_arithmetic (fst deleted_access) astate
       |> function Some (arith, _) -> Arithmetic.is_equal_to_zero arith | None -> false )
-      || Itv.ItvPure.is_zero (Memory.get_bo_itv (fst deleted_access) astate)
+      || Itv.ItvPure.is_zero (AddressAttributes.get_bo_itv (fst deleted_access) astate)
     in
     if is_known_zero then (* freeing 0 is a no-op *)
       Ok [astate]
@@ -274,7 +274,7 @@ module StdFunction = struct
     >>= fun (astate, (lambda, _)) ->
     PulseOperations.Closures.check_captured_addresses location lambda astate
     >>= fun astate ->
-    match PulseAbductiveDomain.Memory.get_closure_proc_name lambda astate with
+    match AddressAttributes.get_closure_proc_name lambda astate with
     | None ->
         (* we don't know what proc name this lambda resolves to *) Ok (havoc_ret ret astate)
     | Some callee_proc_name ->
@@ -338,14 +338,14 @@ module StdVector = struct
    fun ~caller_summary:_ location ~ret:_ astate ->
     let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in
     reallocate_internal_array [crumb] vector Reserve location astate
-    >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector)
+    >>| AddressAttributes.std_vector_reserve (fst vector)
     >>| List.return
 
 
   let push_back vector : model =
    fun ~caller_summary:_ location ~ret:_ astate ->
     let crumb = ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []} in
-    if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then
+    if AddressAttributes.is_std_vector_reserved (fst vector) astate then
       (* assume that any call to [push_back] is ok after one called [reserve] on the same vector
          (a perfect analysis would also make sure we don't exceed the reserved size) *)
       Ok [astate]

infer/src/pulse/PulseOperations.ml

@@ -17,7 +17,7 @@ type 'a access_result = ('a, Diagnostic.t) result
 (** Check that the [address] is not known to be invalid *)
 let check_addr_access location (address, history) astate =
   let access_trace = Trace.Immediate {location; history} in
-  Memory.check_valid access_trace address astate
+  AddressAttributes.check_valid access_trace address astate
   |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
          Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} )
 
@@ -50,8 +50,8 @@ module Closures = struct
     Memory.Edges.of_seq (Caml.List.to_seq fake_fields)
 
 
-  let check_captured_addresses action lambda_addr astate =
-    match Memory.find_opt lambda_addr astate with
+  let check_captured_addresses action lambda_addr (astate : t) =
+    match AbductiveDomain.find_post_cell_opt lambda_addr astate with
     | None ->
         Ok astate
     | Some (edges, attributes) ->
@@ -82,7 +82,7 @@ module Closures = struct
     let closure_addr_hist = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in
     let fake_capture_edges = mk_capture_edges captured_addresses in
     let astate =
-      Memory.set_cell closure_addr_hist
+      AbductiveDomain.set_post_cell closure_addr_hist
         (fake_capture_edges, Attributes.singleton (Closure pname))
         location astate
     in
@@ -104,7 +104,7 @@ let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
     | LiteralOperand i ->
         Some (Arithmetic.equal_to i)
     | AbstractValueOperand v ->
-        Memory.get_arithmetic v astate |> Option.map ~f:fst
+        AddressAttributes.get_arithmetic v astate |> Option.map ~f:fst
   in
   match
     Option.both (arith_of_op op_lhs astate) (arith_of_op op_rhs astate)
@@ -114,7 +114,9 @@ let eval_arith_operand location binop_addr binop_hist bop op_lhs op_rhs astate =
       astate
   | Some binop_a ->
       let binop_trace = Trace.Immediate {location; history= binop_hist} in
-      let astate = Memory.add_attribute binop_addr (Arithmetic (binop_a, binop_trace)) astate in
+      let astate =
+        AddressAttributes.add_one binop_addr (Arithmetic (binop_a, binop_trace)) astate
+      in
       astate
 
 
@@ -124,12 +126,12 @@ let eval_bo_itv_binop binop_addr bop op_lhs op_rhs astate =
     | LiteralOperand i ->
         Itv.ItvPure.of_int_lit i
     | AbstractValueOperand v ->
-        Memory.get_bo_itv v astate
+        AddressAttributes.get_bo_itv v astate
   in
   let bo_itv =
     Itv.ItvPure.arith_binop bop (bo_itv_of_op op_lhs astate) (bo_itv_of_op op_rhs astate)
   in
-  Memory.add_attribute binop_addr (BoItv bo_itv) astate
+  AddressAttributes.add_one binop_addr (BoItv bo_itv) astate
 
 
 let eval_binop location binop op_lhs op_rhs binop_hist astate =
@@ -143,22 +145,22 @@ let eval_binop location binop op_lhs op_rhs binop_hist astate =
 
 let eval_unop_arith location unop_addr unop operand_addr unop_hist astate =
   match
-    Memory.get_arithmetic operand_addr astate
+    AddressAttributes.get_arithmetic operand_addr astate
     |> Option.bind ~f:(function a, _ -> Arithmetic.unop unop a)
   with
   | None ->
       astate
   | Some unop_a ->
       let unop_trace = Trace.Immediate {location; history= unop_hist} in
-      Memory.add_attribute unop_addr (Arithmetic (unop_a, unop_trace)) astate
+      AddressAttributes.add_one unop_addr (Arithmetic (unop_a, unop_trace)) astate
 
 
 let eval_unop_bo_itv unop_addr unop operand_addr astate =
-  match Itv.ItvPure.arith_unop unop (Memory.get_bo_itv operand_addr astate) with
+  match Itv.ItvPure.arith_unop unop (AddressAttributes.get_bo_itv operand_addr astate) with
   | None ->
       astate
   | Some itv ->
-      Memory.add_attribute unop_addr (BoItv itv) astate
+      AddressAttributes.add_one unop_addr (BoItv itv) astate
 
 
 let eval_unop location unop addr unop_hist astate =
@@ -208,11 +210,11 @@ let eval location exp0 astate =
         (* TODO: make identical const the same address *)
         let addr = AbstractValue.mk_fresh () in
         let astate =
-          Memory.add_attribute addr
+          AddressAttributes.add_one addr
             (Arithmetic (Arithmetic.equal_to i, Immediate {location; history= []}))
             astate
-          |> Memory.add_attribute addr (BoItv (Itv.ItvPure.of_int_lit i))
-          |> Memory.invalidate
+          |> AddressAttributes.add_one addr (BoItv (Itv.ItvPure.of_int_lit i))
+          |> AddressAttributes.invalidate
                (addr, [ValueHistory.Assignment location])
                (ConstantDereference i) location
         in
@@ -248,7 +250,10 @@ let eval_arith location exp astate =
   | exp ->
       eval location exp astate
       >>| fun (astate, (value, _)) ->
-      (astate, Some value, Memory.get_arithmetic value astate, Memory.get_bo_itv value astate)
+      ( astate
+      , Some value
+      , AddressAttributes.get_arithmetic value astate
+      , AddressAttributes.get_bo_itv value astate )
 
 
 let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate =
@@ -264,7 +269,8 @@ let record_abduced event location addr_opt orig_arith_hist_opt arith_opt astate
             Trace.add_event event trace
       in
       let attribute = Attribute.Arithmetic (arith, trace) in
-      Memory.abduce_attribute addr attribute astate |> Memory.add_attribute addr attribute
+      AddressAttributes.abduce_attribute addr attribute astate
+      |> AddressAttributes.add_one addr attribute
 
 
 let prune ~is_then_branch if_kind location ~condition astate =
@@ -281,7 +287,8 @@ let prune ~is_then_branch if_kind location ~condition astate =
     | Some (v, NonBottom arith_pruned) ->
         let attr_arith = Attribute.BoItv arith_pruned in
         let astate =
-          Memory.abduce_attribute v attr_arith astate |> Memory.add_attribute v attr_arith
+          AddressAttributes.abduce_attribute v attr_arith astate
+          |> AddressAttributes.add_one v attr_arith
         in
         (astate, true)
   in
@@ -370,7 +377,8 @@ let havoc_field location addr_trace field trace_obj astate =
 
 
 let invalidate location cause addr_trace astate =
-  check_addr_access location addr_trace astate >>| Memory.invalidate addr_trace cause location
+  check_addr_access location addr_trace astate
+  >>| AddressAttributes.invalidate addr_trace cause location
 
 
 let invalidate_deref location cause ref_addr_hist astate =
@@ -384,12 +392,12 @@ let invalidate_array_elements location cause addr_trace astate =
   match Memory.find_opt (fst addr_trace) astate with
   | None ->
       astate
-  | Some (edges, _) ->
+  | Some edges ->
       Memory.Edges.fold
         (fun access dest_addr_trace astate ->
           match (access : Memory.Access.t) with
           | ArrayAccess _ ->
-              Memory.invalidate dest_addr_trace cause location astate
+              AddressAttributes.invalidate dest_addr_trace cause location astate
           | _ ->
               astate )
         edges astate
@@ -399,14 +407,14 @@ let shallow_copy location addr_hist astate =
   check_addr_access location addr_hist astate
   >>| fun astate ->
   let cell =
-    match Memory.find_opt (fst addr_hist) astate with
+    match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with
     | None ->
         (Memory.Edges.empty, Attributes.empty)
     | Some cell ->
         cell
   in
   let copy = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in
-  (Memory.set_cell copy cell location astate, copy)
+  (AbductiveDomain.set_post_cell copy cell location astate, copy)
 
 
 let check_address_escape escape_location proc_desc address history astate =
@@ -420,8 +428,8 @@ let check_address_escape escape_location proc_desc address history astate =
       astate
   in
   let check_address_of_cpp_temporary () =
-    Memory.find_opt address astate
-    |> Option.fold_result ~init:() ~f:(fun () (_, attrs) ->
+    AddressAttributes.find_opt address astate
+    |> Option.fold_result ~init:() ~f:(fun () attrs ->
            IContainer.iter_result ~fold:Attributes.fold attrs ~f:(fun attr ->
                match attr with
                | Attribute.AddressOfCppTemporary (variable, _)
@@ -454,11 +462,11 @@ let check_address_escape escape_location proc_desc address history astate =
 
 
 let mark_address_of_cpp_temporary history variable address astate =
-  Memory.add_attribute address (AddressOfCppTemporary (variable, history)) astate
+  AddressAttributes.add_one address (AddressOfCppTemporary (variable, history)) astate
 
 
 let mark_address_of_stack_variable history variable location address astate =
-  Memory.add_attribute address (AddressOfStackVariable (variable, location, history)) astate
+  AddressAttributes.add_one address (AddressOfStackVariable (variable, location, history)) astate
 
 
 let remove_vars vars location astate =

infer/tests/codetoanalyze/cpp/impurity/issues.exp

@@ -1,5 +1,7 @@
 ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<A*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<A*>::operator++,parameter `this` of std::__wrap_iter<A*>::operator++,parameter `this` modified here]
 ../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::__wrap_iter<int*>::operator++, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::__wrap_iter<int*>::operator++,parameter `this` of std::__wrap_iter<int*>::operator++,parameter `this` modified here]
+../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=<A_*>, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=<A_*>,parameter `__x` of std::operator!=<A_*>,when calling `std::operator==<A_*,_A_*>` here,parameter `__x` modified here,parameter `__y` of std::operator!=<A_*>,when calling `std::operator==<A_*,_A_*>` here,parameter `__y` modified here]
+../../facebook-clang-plugins/clang/install/include/c++/v1/iterator, std::operator!=<int_*>, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function std::operator!=<int_*>,parameter `__x` of std::operator!=<int_*>,when calling `std::operator==<int_*,_int_*>` here,parameter `__x` modified here,parameter `__y` of std::operator!=<int_*>,when calling `std::operator==<int_*,_int_*>` here,parameter `__y` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, alias_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function alias_mod_impure,parameter `array` of alias_mod_impure,assigned,parameter `array` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, array_mod_both_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_both_impure,parameter `a` of array_mod_both_impure,parameter `a` modified here,parameter `a` of array_mod_both_impure,parameter `a` modified here]
 codetoanalyze/cpp/impurity/array_test.cpp, array_mod_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function array_mod_impure,parameter `b` of array_mod_impure,parameter `b` modified here,parameter `a` of array_mod_impure,parameter `a` modified here]