[pulse] more aggressive join

Summary:
Do the intersection of the heap and stack domains, and the union of the
invalid location sets. This forgets invalid locations that appear only
in one heap, unfortunately. We can start with this and improve later.

Reviewed By: mbouaziz

Differential Revision: D10445825

fbshipit-source-id: cc24460af

infer/src/checkers/PulseDomain.ml

@@ -47,20 +47,40 @@ module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLoca
   let pp = AbstractLocation.pp
 end
 
-module MemoryKey = struct
+module Access = struct
-  type t = AbstractLocation.t * AccessPath.access [@@deriving compare]
+  type t = AccessPath.access [@@deriving compare]
 
-  let pp f k = Pp.pair ~fst:AbstractLocation.pp ~snd:AccessPath.pp_access f k
+  let pp = AccessPath.pp_access
 end
 
-module MemoryDomain = AbstractDomain.Map (MemoryKey) (AbstractLocationDomain)
+module MemoryEdges = AbstractDomain.InvertedMap (Access) (AbstractLocationDomain)
-module AliasingDomain = AbstractDomain.Map (Var) (AbstractLocationDomain)
+
+module MemoryDomain = struct
+  include AbstractDomain.InvertedMap (AbstractLocation) (MemoryEdges)
+
+  let add_edge loc_src access loc_end memory =
+    let edges =
+      match find_opt loc_src memory with Some edges -> edges | None -> MemoryEdges.empty
+    in
+    add loc_src (MemoryEdges.add access loc_end edges) memory
+
+
+  let find_edge_opt loc access memory =
+    let open Option.Monad_infix in
+    find_opt loc memory >>= MemoryEdges.find_opt access
+end
+
+module AliasingDomain = AbstractDomain.InvertedMap (Var) (AbstractLocationDomain)
 module AbstractLocationsDomain = AbstractDomain.FiniteSet (AbstractLocation)
 module InvalidLocationsDomain = AbstractLocationsDomain
 
 type t =
   {heap: MemoryDomain.astate; stack: AliasingDomain.astate; invalids: InvalidLocationsDomain.astate}
 
+let initial =
+  {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty}
+
+
 module Domain : AbstractDomain.S with type astate = t = struct
   type astate = t
 
@@ -107,10 +127,6 @@ end
 
 include Domain
 
-let initial =
-  {heap= MemoryDomain.empty; stack= AliasingDomain.empty; invalids= AbstractLocationsDomain.empty}
-
-
 module Diagnostic = struct
   (* TODO: more structured error type so that we can actually report something informative about
        the variables being accessed along with a trace *)
@@ -140,15 +156,15 @@ let rec walk ~overwrite_last loc path astate =
   | [a], Some new_loc ->
       check_loc_access loc astate
       >>| fun astate ->
-      let heap = MemoryDomain.add (loc, a) new_loc astate.heap in
+      let heap = MemoryDomain.add_edge loc a new_loc astate.heap in
       ({astate with heap}, new_loc)
   | a :: path, _ -> (
       check_loc_access loc astate
       >>= fun astate ->
-      match MemoryDomain.find_opt (loc, a) astate.heap with
+      match MemoryDomain.find_edge_opt loc a astate.heap with
       | None ->
           let loc' = AbstractLocation.mk_fresh () in
-          let heap = MemoryDomain.add (loc, a) loc' astate.heap in
+          let heap = MemoryDomain.add_edge loc a loc' astate.heap in
           let astate = {astate with heap} in
           walk ~overwrite_last loc' path astate
       | Some loc' ->

infer/src/checkers/PulseDomain.mli

@@ -14,8 +14,8 @@ module AbstractLocation : sig
   val pp : F.formatter -> t -> unit
 end
 
-module MemoryKey : sig
+module Access : sig
-  type t = AbstractLocation.t * AccessPath.access [@@deriving compare]
+  type t = AccessPath.access [@@deriving compare]
 
   val pp : F.formatter -> t -> unit
 end
@@ -24,9 +24,11 @@ module AbstractLocationDomain : AbstractDomain.S with type astate = AbstractLoca
 
 module AbstractLocationsDomain : module type of AbstractDomain.FiniteSet (AbstractLocation)
 
-module MemoryDomain : module type of AbstractDomain.Map (MemoryKey) (AbstractLocationDomain)
+module MemoryEdges : module type of AbstractDomain.InvertedMap (Access) (AbstractLocationDomain)
 
-module AliasingDomain : module type of AbstractDomain.Map (Var) (AbstractLocationDomain)
+module MemoryDomain : module type of AbstractDomain.InvertedMap (AbstractLocation) (MemoryEdges)
+
+module AliasingDomain : module type of AbstractDomain.InvertedMap (Var) (AbstractLocationDomain)
 
 module InvalidLocationsDomain : module type of AbstractLocationsDomain
 

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

@@ -1,6 +1,3 @@
-codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []
-codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, []
-codetoanalyze/cpp/ownership/basics.cpp, multiple_invalidations_loop_bad, 8, USE_AFTER_LIFETIME, no_bucket, ERROR, []
 codetoanalyze/cpp/ownership/returns.cpp, returns::return_deleted_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, []
 codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_branch_bad, 5, USE_AFTER_LIFETIME, no_bucket, ERROR, []
 codetoanalyze/cpp/ownership/use_after_delete.cpp, delete_in_loop_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, []