[pulse] better trace when realising latent invalid accesses

Summary:
"glue" together the trace from the caller with the trace from the callee
to form the access trace when applying LatentInvalidAccess summaries.
This is consistent with what happens in function calls and allows Pulse
to better keep track of the history of the value. The goal is to prevent
bugs from getting filtered out because the access trace doesn't contain
the invalidation event for the value.

Reviewed By: da319

Differential Revision: D29550320

fbshipit-source-id: b600c188d

infer/src/pulse/PulseCallOperations.ml

@@ -138,9 +138,9 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s
   | LatentInvalidAccess {astate} ->
       map_call_result ~is_isl_error_prepost:false
         (astate :> AbductiveDomain.t)
-        ~f:(fun subst astate ->
+        ~f:(fun subst astate_post_call ->
           let* astate_summary_result =
-            ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate
+            ( AbductiveDomain.summary_of_post tenv caller_proc_desc call_loc astate_post_call
               >>| AccessResult.ignore_memory_leaks >>| AccessResult.of_abductive_result
               :> (AbductiveDomain.summary, AbductiveDomain.t AccessResult.error) result SatUnsat.t
               )
@@ -168,17 +168,27 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s
                     Sat (Error (ReportableErrorSummary {diagnostic; astate= astate_summary}))
                 | `ISLDelay astate ->
                     Sat (Error (ISLError astate)) )
-            | LatentInvalidAccess {address= address_callee; must_be_valid; calling_context} -> (
+            | LatentInvalidAccess
+                { address= address_callee
+                ; must_be_valid= callee_access_trace, must_be_valid_reason
+                ; calling_context } -> (
               match AbstractValue.Map.find_opt address_callee subst with
               | None ->
                   (* the address became unreachable so the bug can never be reached; drop it *)
                   Unsat
-              | Some (address, _history) -> (
+              | Some (address, caller_history) -> (
+                  let access_trace =
+                    Trace.ViaCall
+                      { in_call= callee_access_trace
+                      ; f= Call callee_pname
+                      ; location= call_loc
+                      ; history= caller_history }
+                  in
                   let calling_context =
                     (CallEvent.Call callee_pname, call_loc) :: calling_context
                   in
                   match
-                    AbductiveDomain.find_post_cell_opt address (astate_summary :> AbductiveDomain.t)
+                    AbductiveDomain.find_post_cell_opt address astate_post_call
                     |> Option.bind ~f:(fun (_, attrs) -> Attributes.get_invalid attrs)
                   with
                   | None ->
@@ -186,7 +196,10 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s
                       Sat
                         (Ok
                            (LatentInvalidAccess
-                              {astate= astate_summary; address; must_be_valid; calling_context}))
+                              { astate= astate_summary
+                              ; address
+                              ; must_be_valid= (access_trace, must_be_valid_reason)
+                              ; calling_context }))
                   | Some (invalidation, invalidation_trace) ->
                       Sat
                         (Error
@@ -196,8 +209,8 @@ let apply_callee tenv path ~caller_proc_desc callee_pname call_loc callee_exec_s
                                     { calling_context
                                     ; invalidation
                                     ; invalidation_trace
-                                    ; access_trace= fst must_be_valid
+                                    ; access_trace
-                                    ; must_be_valid_reason= snd must_be_valid }
+                                    ; must_be_valid_reason }
                               ; astate= astate_summary })) ) ) ) )
   | ISLLatentMemoryError astate ->
       map_call_result ~is_isl_error_prepost:true

infer/src/pulse/PulseReport.ml

@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module L = Logging
 open PulseBasicInterface
 open PulseDomainInterface
 
@@ -66,8 +67,11 @@ let is_constant_deref_without_invalidation (diagnostic : Diagnostic.t) =
 
 
 let is_suppressed tenv proc_desc diagnostic astate =
-  is_constant_deref_without_invalidation diagnostic
+  if is_constant_deref_without_invalidation diagnostic then (
-  ||
+    L.d_printfln ~color:Red
+      "Dropping error: constant dereference with no invalidation in the access trace" ;
+    true )
+  else
     match Procdesc.get_proc_name proc_desc with
     | Procname.Java jn ->
         is_nullsafe_error tenv diagnostic jn

infer/src/pulse/PulseSummary.ml

@@ -42,6 +42,9 @@ let exec_summary_of_post_common tenv ~continue_program proc_desc err_log locatio
       | None ->
           Some (LatentInvalidAccess {astate; address; must_be_valid; calling_context= []})
       | Some (invalidation, invalidation_trace) ->
+          (* NOTE: this probably leads to the error being dropped as the access trace is unlikely to
+             contain the reason for invalidation and thus we will filter out the report. TODO:
+             figure out if that's a problem. *)
           PulseReport.report_summary_error tenv proc_desc err_log
             (ReportableError
                { diagnostic=