[pulse] separate traces from their action

Summary:
This simplifies the code overall. It also makes accessing the action of
a "trace" (which is now stored alongside it instead of deep inside it)
constant time instead of linear in the number of nested calls.

Reviewed By: skcho

Differential Revision: D18206460

fbshipit-source-id: 9546ff36f

infer/src/checkers/impurityDomain.ml

@@ -8,7 +8,7 @@
 open! IStd
 module F = Format
 
-type trace = WrittenTo of unit PulseTrace.t | Invalid of PulseInvalidation.t PulseTrace.t
+type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t)
 [@@deriving compare]
 
 module ModifiedVar = struct
@@ -55,14 +55,14 @@ let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog =
     match trace with
     | WrittenTo access_trace ->
         PulseTrace.add_to_errlog ~nesting
-          (fun fmt () ->
+          ~pp_immediate:(fun fmt ->
             F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
           access_trace errlog
-    | Invalid invalidation_trace ->
+    | Invalid (invalidation, invalidation_trace) ->
         PulseTrace.add_to_errlog ~nesting
-          (fun fmt invalid ->
+          ~pp_immediate:(fun fmt ->
             F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
-              PulseInvalidation.describe invalid )
+              PulseInvalidation.describe invalidation )
           invalidation_trace errlog
   in
   let first_trace, rest = trace_list in

infer/src/checkers/impurityDomain.mli

@@ -6,7 +6,7 @@
  *)
 open! IStd
 
-type trace = WrittenTo of unit PulseTrace.t | Invalid of PulseInvalidation.t PulseTrace.t
+type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t)
 
 module ModifiedVar : sig
   type nonempty_action_type = trace * trace list

infer/src/pulse/PulseAbductiveDomain.ml

@@ -172,8 +172,7 @@ module Memory = struct
   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 {imm= (); location; history}))
-    )
+        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {location; history})) )
 
 
   let find_edge_opt address access astate =
@@ -229,8 +228,7 @@ module Memory = struct
   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 {imm= (); location; history}))
-    )
+        |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {location; history})) )
 
 
   module Edges = BaseMemory.Edges
@@ -305,10 +303,9 @@ module PrePost = struct
 
 
   let add_out_of_scope_attribute addr pvar location history heap typ =
-    let attr =
-      Attribute.Invalid (Immediate {imm= GoneOutOfScope (pvar, typ); location; history})
-    in
-    BaseMemory.add_attribute addr attr heap
+    BaseMemory.add_attribute addr
+      (Invalid (GoneOutOfScope (pvar, typ), Immediate {location; history}))
+      heap
 
 
   (** invalidate local variables going out of scope *)
@@ -613,13 +610,11 @@ module PrePost = struct
 
   let add_call_to_attr proc_name call_location caller_history attr =
     match (attr : Attribute.t) with
-    | Invalid invalidation ->
+    | Invalid (invalidation, in_call) ->
         Attribute.Invalid
-          (ViaCall
-             { f= Call proc_name
-             ; location= call_location
-             ; history= caller_history
-             ; in_call= invalidation })
+          ( invalidation
+          , ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call}
+          )
     | AddressOfCppTemporary (_, _)
     | AddressOfStackVariable (_, _, _)
     | Arithmetic _
@@ -668,7 +663,7 @@ module PrePost = struct
         let callee_trace =
           match written_to_callee_opt with
           | None ->
-              Trace.Immediate {imm= (); location= call_loc; history= []}
+              Trace.Immediate {location= call_loc; history= []}
           | Some access_trace ->
               access_trace
         in
@@ -858,10 +853,10 @@ module PrePost = struct
                   ; history= hist_caller }
               in
               Memory.check_valid access_trace addr_caller astate
-              |> Result.map_error ~f:(fun invalidated_by ->
+              |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
                      L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
-                     Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace}
-                 ) ) )
+                     Diagnostic.AccessToInvalidAddress
+                       {invalidation; invalidation_trace; access_trace} ) ) )
       call_state.subst (Ok call_state.astate)
 
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -59,7 +59,7 @@ module Memory : sig
     -> t
     -> t
 
-  val check_valid : unit Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t Trace.t) result
+  val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result
 
   val find_opt : AbstractValue.t -> t -> BaseMemory.cell option
 

infer/src/pulse/PulseAttribute.ml

@@ -31,21 +31,21 @@ module Attribute = struct
     | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
     | Arithmetic of Arithmetic.t
     | Closure of Typ.Procname.t
-    | Invalid of Invalidation.t Trace.t
-    | MustBeValid of unit Trace.t
+    | Invalid of Invalidation.t * Trace.t
+    | MustBeValid of Trace.t
     | StdVectorReserve
-    | WrittenTo of unit Trace.t
+    | WrittenTo of Trace.t
   [@@deriving compare, variants]
 
   let equal = [%compare.equal: t]
 
   let to_rank = Variants.to_rank
 
-  let mk_dummy_trace imm = Trace.Immediate {imm; location= Location.dummy; history= []}
+  let dummy_trace = Trace.Immediate {location= Location.dummy; history= []}
 
   let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun ""))
 
-  let written_to_rank = Variants.to_rank (WrittenTo (mk_dummy_trace ()))
+  let written_to_rank = Variants.to_rank (WrittenTo dummy_trace)
 
   let address_of_stack_variable_rank =
     let pname = Typ.Procname.from_string_c_fun "" in
@@ -54,16 +54,16 @@ module Attribute = struct
     Variants.to_rank (AddressOfStackVariable (var, location, []))
 
 
-  let invalid_rank = Variants.to_rank (Invalid (mk_dummy_trace Invalidation.Nullptr))
+  let invalid_rank = Variants.to_rank (Invalid (Invalidation.Nullptr, dummy_trace))
 
-  let must_be_valid_rank = Variants.to_rank (MustBeValid (mk_dummy_trace ()))
+  let must_be_valid_rank = Variants.to_rank (MustBeValid dummy_trace)
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 
   let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero))
 
   let pp f attribute =
-    let pp_string_if_debug string fmt () =
+    let pp_string_if_debug string fmt =
       if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string
     in
     match attribute with
@@ -75,14 +75,16 @@ module Attribute = struct
         Typ.Procname.pp f pname
     | Arithmetic phi ->
         Arithmetic.pp f phi
-    | Invalid invalidation ->
-        F.fprintf f "Invalid %a" (Trace.pp Invalidation.pp) invalidation
-    | MustBeValid action ->
-        F.fprintf f "MustBeValid %a" (Trace.pp (pp_string_if_debug "access")) action
+    | Invalid (invalidation, trace) ->
+        F.fprintf f "Invalid %a"
+          (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
+          trace
+    | MustBeValid trace ->
+        F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
-    | WrittenTo action ->
-        F.fprintf f "WrittenTo %a" (Trace.pp (pp_string_if_debug "mutation")) action
+    | WrittenTo trace ->
+        F.fprintf f "WrittenTo %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "mutation")) trace
 end
 
 module Attributes = struct
@@ -91,8 +93,8 @@ module Attributes = struct
   let get_invalid attrs =
     Set.find_rank attrs Attribute.invalid_rank
     |> Option.map ~f:(fun attr ->
-           let[@warning "-8"] (Attribute.Invalid invalidation) = attr in
-           invalidation )
+           let[@warning "-8"] (Attribute.Invalid (invalidation, trace)) = attr in
+           (invalidation, trace) )
 
 
   let get_must_be_valid attrs =

infer/src/pulse/PulseAttribute.mli

@@ -16,10 +16,10 @@ type t =
   | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t
   | Arithmetic of Arithmetic.t
   | Closure of Typ.Procname.t
-  | Invalid of Invalidation.t Trace.t
-  | MustBeValid of unit Trace.t
+  | Invalid of Invalidation.t * Trace.t
+  | MustBeValid of Trace.t
   | StdVectorReserve
-  | WrittenTo of unit Trace.t
+  | WrittenTo of Trace.t
 [@@deriving compare]
 
 val pp : F.formatter -> t -> unit
@@ -33,11 +33,11 @@ module Attributes : sig
 
   val get_arithmetic : t -> Arithmetic.t option
 
-  val get_invalid : t -> Invalidation.t Trace.t option
+  val get_invalid : t -> (Invalidation.t * Trace.t) option
 
-  val get_must_be_valid : t -> unit Trace.t option
+  val get_must_be_valid : t -> Trace.t option
 
-  val get_written_to : t -> unit Trace.t option
+  val get_written_to : t -> Trace.t option
 
   val is_modified : t -> bool
 

infer/src/pulse/PulseBaseMemory.ml

@@ -68,9 +68,8 @@ let add_attribute addr attribute memory =
       (fst memory, Graph.add addr new_attrs (snd memory))
 
 
-let invalidate (address, history) invalid location memory =
-  let invalidation = Trace.Immediate {imm= invalid; location; history} in
-  add_attribute address (Attribute.Invalid invalidation) memory
+let invalidate (address, history) invalidation location memory =
+  add_attribute address (Attribute.Invalid (invalidation, Immediate {location; history})) memory
 
 
 let check_valid address memory =

infer/src/pulse/PulseBaseMemory.mli

@@ -56,13 +56,13 @@ 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 check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result
 
 val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
 val get_arithmetic : AbstractValue.t -> t -> Arithmetic.t option
 
-val get_must_be_valid : AbstractValue.t -> t -> unit Trace.t option
+val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
 
 val std_vector_reserve : AbstractValue.t -> t -> t
 

infer/src/pulse/PulseDiagnostic.ml

@@ -13,18 +13,21 @@ module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
 
 type t =
-  | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}
+  | AccessToInvalidAddress of
+      { invalidation: Invalidation.t
+      ; invalidation_trace: Trace.t
+      ; access_trace: Trace.t }
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 let get_location = function
-  | AccessToInvalidAddress {accessed_by} ->
-      Trace.get_outer_location accessed_by
+  | AccessToInvalidAddress {access_trace} ->
+      Trace.get_outer_location access_trace
   | StackVariableAddressEscape {location} ->
       location
 
 
 let get_message = function
-  | AccessToInvalidAddress {accessed_by; invalidated_by} ->
+  | AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} ->
       (* The goal is to get one of the following messages depending on the scenario:
 
          42: delete x; return x->f
@@ -42,30 +45,29 @@ let get_message = function
          Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then
          "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
       *)
-      let pp_access_trace fmt (trace : unit Trace.t) =
+      let pp_access_trace fmt (trace : Trace.t) =
         match trace with
-        | Immediate {imm= (); _} ->
+        | Immediate _ ->
             F.fprintf fmt "accessing memory that "
         | ViaCall {f; _} ->
             F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f
       in
-      let pp_invalidation_trace line fmt (trace : Invalidation.t Trace.t) =
+      let pp_invalidation_trace line invalidation fmt (trace : Trace.t) =
         let pp_line fmt line = F.fprintf fmt " on line %d" line in
         match trace with
-        | ViaCall {f; in_call} ->
-            let invalid = Trace.get_immediate in_call in
-            F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalid
-              pp_line line CallEvent.describe f
-        | Immediate {imm= invalid} ->
-            F.fprintf fmt "%a%a" Invalidation.describe invalid pp_line line
+        | Immediate _ ->
+            F.fprintf fmt "%a%a" Invalidation.describe invalidation pp_line line
+        | ViaCall {f; _} ->
+            F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe
+              invalidation pp_line line CallEvent.describe f
       in
       let invalidation_line =
-        let {Location.line; _} = Trace.get_outer_location invalidated_by in
+        let {Location.line; _} = Trace.get_outer_location invalidation_trace in
         line
       in
-      F.asprintf "%a%a" pp_access_trace accessed_by
-        (pp_invalidation_trace invalidation_line)
-        invalidated_by
+      F.asprintf "%a%a" pp_access_trace access_trace
+        (pp_invalidation_trace invalidation_line invalidation)
+        invalidation_trace
   | StackVariableAddressEscape {variable; _} ->
       let pp_var f var =
         if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary"
@@ -81,19 +83,19 @@ let add_errlog_header ~title location errlog =
 
 
 let get_trace = function
-  | AccessToInvalidAddress {accessed_by; invalidated_by} ->
-      let start_location = Trace.get_start_location invalidated_by in
+  | AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} ->
+      let start_location = Trace.get_start_location invalidation_trace in
       add_errlog_header ~title:"invalidation part of the trace starts here" start_location
       @@ Trace.add_to_errlog ~nesting:1
-           (fun fmt invalid -> F.fprintf fmt "%a" Invalidation.describe invalid)
-           invalidated_by
+           ~pp_immediate:(fun fmt -> F.fprintf fmt "%a" Invalidation.describe invalidation)
+           invalidation_trace
       @@
-      let access_start_location = Trace.get_start_location accessed_by in
+      let access_start_location = Trace.get_start_location access_trace in
       add_errlog_header ~title:"use-after-lifetime part of the trace starts here"
         access_start_location
       @@ Trace.add_to_errlog ~nesting:1
-           (fun fmt () -> F.pp_print_string fmt "invalid access occurs here")
-           accessed_by
+           ~pp_immediate:(fun fmt -> F.pp_print_string fmt "invalid access occurs here")
+           access_trace
       @@ []
   | StackVariableAddressEscape {history; location; _} ->
       ValueHistory.add_to_errlog ~nesting:0 history
@@ -103,7 +105,7 @@ let get_trace = function
 
 
 let get_issue_type = function
-  | AccessToInvalidAddress {invalidated_by} ->
-      Trace.get_immediate invalidated_by |> Invalidation.issue_type_of_cause
+  | AccessToInvalidAddress {invalidation; _} ->
+      Invalidation.issue_type_of_cause invalidation
   | StackVariableAddressEscape _ ->
       IssueType.stack_variable_address_escape

infer/src/pulse/PulseDiagnostic.mli

@@ -12,7 +12,10 @@ module ValueHistory = PulseValueHistory
 
 (** an error to report to the user *)
 type t =
-  | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t}
+  | AccessToInvalidAddress of
+      { invalidation: Invalidation.t
+      ; invalidation_trace: Trace.t
+      ; access_trace: Trace.t }
   | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t}
 
 val get_message : t -> string

infer/src/pulse/PulseOperations.ml

@@ -16,10 +16,10 @@ 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 accessed_by = Trace.Immediate {imm= (); location; history} in
-  Memory.check_valid accessed_by address astate
-  |> Result.map_error ~f:(fun invalidated_by ->
-         Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} )
+  let access_trace = Trace.Immediate {location; history} in
+  Memory.check_valid access_trace address astate
+  |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
+         Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} )
 
 
 module Closures = struct

infer/src/pulse/PulseTrace.ml

@@ -9,46 +9,39 @@ module F = Format
 module CallEvent = PulseCallEvent
 module ValueHistory = PulseValueHistory
 
-type 'a t =
-  | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t}
-  | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: 'a t}
+type t =
+  | Immediate of {location: Location.t; history: ValueHistory.t}
+  | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: t}
 [@@deriving compare]
 
-let rec get_immediate = function
-  | Immediate {imm; _} ->
-      imm
-  | ViaCall {in_call; _} ->
-      get_immediate in_call
-
-
 let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location
 
-let get_history = function Immediate {history; _} | ViaCall {history; _} -> history
+let get_outer_history = function Immediate {history; _} | ViaCall {history; _} -> history
 
 let get_start_location trace =
-  match get_history trace |> List.last with
+  match get_outer_history trace |> List.last with
   | Some event ->
       ValueHistory.location_of_event event
   | None ->
       get_outer_location trace
 
 
-let rec pp pp_immediate fmt = function
-  | Immediate {imm; location= _; history} ->
-      if Config.debug_level_analysis < 3 then pp_immediate fmt imm
-      else F.fprintf fmt "%a::%a" ValueHistory.pp history pp_immediate imm
-  | ViaCall {f; location= _; history; in_call} ->
-      if Config.debug_level_analysis < 3 then pp pp_immediate fmt in_call
-      else
-        F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp pp_immediate) in_call
+let rec pp ~pp_immediate fmt trace =
+  if Config.debug_level_analysis < 3 then pp_immediate fmt
+  else
+    match trace with
+    | Immediate {location= _; history} ->
+        F.fprintf fmt "%a::%t" ValueHistory.pp history pp_immediate
+    | ViaCall {f; location= _; history; in_call} ->
+        F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp ~pp_immediate)
+          in_call
 
 
-let rec add_to_errlog ~nesting pp_immediate trace errlog =
+let rec add_to_errlog ~nesting ~pp_immediate trace errlog =
   match trace with
-  | Immediate {imm; location; history} ->
+  | Immediate {location; history} ->
       ValueHistory.add_to_errlog ~nesting history
-      @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
-         :: errlog
+      @@ (Errlog.make_trace_element nesting location (F.asprintf "%t" pp_immediate) [] :: errlog)
   | ViaCall {f; location; in_call; history} ->
       ValueHistory.add_to_errlog ~nesting history
       @@ (fun errlog ->
@@ -56,5 +49,5 @@ let rec add_to_errlog ~nesting pp_immediate trace errlog =
              (F.asprintf "when calling %a here" CallEvent.pp f)
              []
            :: errlog )
-      @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call
+      @@ add_to_errlog ~nesting:(nesting + 1) ~pp_immediate in_call
       @@ errlog

infer/src/pulse/PulseTrace.mli

@@ -9,29 +9,27 @@ module F = Format
 module CallEvent = PulseCallEvent
 module ValueHistory = PulseValueHistory
 
-type 'a t =
-  | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t}
+type t =
+  | Immediate of {location: Location.t; history: ValueHistory.t}
   | ViaCall of
       { f: CallEvent.t
       ; location: Location.t  (** location of the call event *)
       ; history: ValueHistory.t  (** the call involves a value with this prior history *)
-      ; in_call: 'a t  (** last step of the trace is in a call to [f] made at [location] *) }
+      ; in_call: t  (** last step of the trace is in a call to [f] made at [location] *) }
 [@@deriving compare]
 
-val pp : (F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
+val pp : pp_immediate:(F.formatter -> unit) -> F.formatter -> t -> unit
 
-val get_outer_location : 'a t -> Location.t
+val get_outer_location : t -> Location.t
 (** skip histories and go straight to the where the action is: either the action itself or the
-      call that leads to the action *)
+    call that leads to the action *)
 
-val get_start_location : 'a t -> Location.t
+val get_start_location : t -> Location.t
 (** initial step in the history if not empty, or else same as {!get_outer_location} *)
 
-val get_immediate : 'a t -> 'a
-
 val add_to_errlog :
      nesting:int
-  -> (F.formatter -> 'a -> unit)
-  -> 'a t
+  -> pp_immediate:(F.formatter -> unit)
+  -> t
   -> Errlog.loc_trace_elem list
   -> Errlog.loc_trace_elem list