[pulse] Record the trace of the address written to

Reviewed By: skcho

Differential Revision: D17004433

fbshipit-source-id: 937319c27

infer/src/pulse/PulseAbductiveDomain.ml

@@ -168,10 +168,12 @@ module Memory = struct
     if phys_equal new_pre pre then astate else {astate with pre= new_pre}
 
 
-  let add_edge addr access new_addr_trace astate =
+  let add_edge addr access new_addr_trace loc astate =
     map_post_heap astate ~f:(fun heap ->
         BaseMemory.add_edge addr access new_addr_trace heap
-        |> BaseMemory.add_attributes addr (Attributes.singleton WrittenTo) )
+        |> BaseMemory.add_attributes addr
+             (Attributes.singleton
+                (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc}))) )
 
 
   let find_edge_opt address access astate =
@@ -220,10 +222,12 @@ module Memory = struct
 
   let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap
 
-  let set_cell addr cell astate =
+  let set_cell addr cell loc astate =
     map_post_heap astate ~f:(fun heap ->
         BaseMemory.set_cell addr cell heap
-        |> BaseMemory.add_attributes addr (Attributes.singleton WrittenTo) )
+        |> BaseMemory.add_attributes addr
+             (Attributes.singleton
+                (WrittenTo (PulseDomain.InterprocAction.Immediate {imm= (); location= loc}))) )
 
 
   module Edges = BaseMemory.Edges
@@ -582,7 +586,7 @@ module PrePost = struct
                 {action= trace.action; f= Call proc_name; location}
           ; history= trace.history }
     | MustBeValid _
-    | WrittenTo
+    | WrittenTo _
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
     | Closure _
@@ -617,8 +621,23 @@ module PrePost = struct
           (fun _ _ post_cell -> Some post_cell)
           post_edges_minus_pre translated_post_edges
       in
+      let written_to =
+        (let open Option.Monad_infix in
+        PulseDomain.Memory.find_opt addr_caller heap
+        >>= fun (_edges, attrs) ->
+        PulseDomain.Attributes.get_written_to attrs
+        >>| fun callee_action ->
+        PulseDomain.Attribute.WrittenTo
+          (PulseDomain.InterprocAction.ViaCall
+             {action= callee_action; f= Call callee_proc_name; location= call_loc}))
+        |> Option.value
+             ~default:
+               (PulseDomain.Attribute.WrittenTo
+                  (PulseDomain.InterprocAction.Immediate {imm= (); location= call_loc}))
+      in
       PulseDomain.Memory.set_edges addr_caller edges_post_caller heap
-      |> PulseDomain.Memory.add_attributes addr_caller (PulseDomain.Attributes.singleton WrittenTo)
+      |> PulseDomain.Memory.add_attributes addr_caller
+           (PulseDomain.Attributes.singleton written_to)
     in
     let caller_post = Domain.make (call_state.astate.post :> base_domain).stack heap in
     {call_state with subst; astate= {call_state.astate with post= caller_post}}

infer/src/pulse/PulseAbductiveDomain.mli

@@ -45,7 +45,8 @@ module Memory : sig
 
   val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
 
-  val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
+  val add_edge :
+    AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> Location.t -> t -> t
 
   val check_valid :
        unit PulseDomain.InterprocAction.t
@@ -57,7 +58,7 @@ module Memory : sig
 
   val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option
 
-  val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t
+  val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> Location.t -> t -> t
 
   val invalidate :
        AbstractAddress.t * PulseDomain.ValueHistory.t

infer/src/pulse/PulseDomain.ml

@@ -178,6 +178,8 @@ module InterprocAction = struct
     | ViaCall of {action: 'a t; f: call_event; location: Location.t}
   [@@deriving compare]
 
+  let dummy = Immediate {imm= (); location= Location.dummy}
+
   let rec get_immediate = function
     | Immediate {imm; _} ->
         imm
@@ -246,7 +248,7 @@ module Attribute = struct
   type t =
     | Invalid of Invalidation.t Trace.t
     | MustBeValid of unit InterprocAction.t
-    | WrittenTo
+    | WrittenTo of unit InterprocAction.t
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t
     | Closure of Typ.Procname.t
@@ -259,7 +261,7 @@ module Attribute = struct
 
   let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun ""))
 
-  let address_is_written_to_rank = Variants.to_rank WrittenTo
+  let written_to_rank = Variants.to_rank (WrittenTo InterprocAction.dummy)
 
   let address_of_stack_variable_rank =
     let pname = Typ.Procname.from_string_c_fun "" in
@@ -274,9 +276,7 @@ module Attribute = struct
          {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []})
 
 
-  let must_be_valid_rank =
+  let must_be_valid_rank = Variants.to_rank (MustBeValid InterprocAction.dummy)
-    Variants.to_rank (MustBeValid (Immediate {imm= (); location= Location.dummy}))
-
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
@@ -288,8 +288,11 @@ module Attribute = struct
           (InterprocAction.pp (fun _ () -> ()))
           action Location.pp
           (InterprocAction.to_outer_location action)
-    | WrittenTo ->
+    | WrittenTo action ->
-        F.fprintf f "written"
+        F.fprintf f "WrittenTo (written by %a @ %a)"
+          (InterprocAction.pp (fun _ () -> ()))
+          action Location.pp
+          (InterprocAction.to_outer_location action)
     | AddressOfCppTemporary (var, history) ->
         F.fprintf f "t&%a (%a)" Var.pp var ValueHistory.pp history
     | AddressOfStackVariable (var, history, location) ->
@@ -317,6 +320,13 @@ module Attributes = struct
            action )
 
 
+  let get_written_to attrs =
+    Set.find_rank attrs Attribute.written_to_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.WrittenTo action) = attr in
+           action )
+
+
   let get_closure_proc_name attrs =
     Set.find_rank attrs Attribute.closure_rank
     |> Option.map ~f:(fun attr ->
@@ -336,7 +346,7 @@ module Attributes = struct
 
 
   let is_modified attrs =
-    Option.is_some (Set.find_rank attrs Attribute.address_is_written_to_rank)
+    Option.is_some (Set.find_rank attrs Attribute.written_to_rank)
     || Option.is_some (Set.find_rank attrs Attribute.invalid_rank)
 
 

infer/src/pulse/PulseDomain.mli

@@ -83,7 +83,7 @@ module Attribute : sig
   type t =
     | Invalid of Invalidation.t Trace.t
     | MustBeValid of unit InterprocAction.t
-    | WrittenTo
+    | WrittenTo of unit InterprocAction.t
     | AddressOfCppTemporary of Var.t * ValueHistory.t
     | AddressOfStackVariable of Var.t * ValueHistory.t * Location.t
     | Closure of Typ.Procname.t
@@ -96,6 +96,8 @@ module Attributes : sig
 
   val get_must_be_valid : t -> unit InterprocAction.t option
 
+  val get_written_to : t -> unit InterprocAction.t option
+
   val get_address_of_stack_variable : t -> (Var.t * ValueHistory.t * Location.t) option
 
   val is_modified : t -> bool

infer/src/pulse/PulseOperations.ml

@@ -98,7 +98,7 @@ module Closures = struct
     let astate =
       Memory.set_cell closure_addr
         (fake_capture_edges, Attributes.singleton (Closure pname))
-        astate
+        location astate
     in
     (astate, (closure_addr, (* TODO: trace *) []))
 end
@@ -178,7 +178,7 @@ let action_of_address location = InterprocAction.Immediate {imm= (); location}
 let write_access location addr_trace_ref access addr_trace_obj astate =
   let action = action_of_address location in
   check_addr_access action addr_trace_ref astate
-  >>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj
+  >>| Memory.add_edge (fst addr_trace_ref) access addr_trace_obj location
 
 
 let write_deref location ~ref:addr_trace_ref ~obj:addr_trace_obj astate =
@@ -237,7 +237,7 @@ let shallow_copy location addr_hist astate =
         cell
   in
   let copy = AbstractAddress.mk_fresh () in
-  (Memory.set_cell copy cell astate, copy)
+  (Memory.set_cell copy cell location astate, copy)
 
 
 let check_address_escape escape_location proc_desc address history astate =