[pulse][4/9] add PulseTrace to PulseBasicInterface

Summary: See explanations in D17955104

Reviewed By: ezgicicek

Differential Revision: D17955282

fbshipit-source-id: a9d75e8a1

infer/src/checkers/impurityDomain.ml

@@ -8,9 +8,7 @@
 open! IStd
 module F = Format
 
-type trace =
-  | WrittenTo of unit PulseDomain.Trace.t
-  | Invalid of PulseInvalidation.t PulseDomain.Trace.t
+type trace = WrittenTo of unit PulseTrace.t | Invalid of PulseInvalidation.t PulseTrace.t
 [@@deriving compare]
 
 module ModifiedVar = struct
@@ -56,12 +54,12 @@ let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog =
   let aux ~nesting errlog trace =
     match trace with
     | WrittenTo access_trace ->
-        PulseDomain.Trace.add_to_errlog ~nesting
+        PulseTrace.add_to_errlog ~nesting
           (fun fmt () ->
             F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var )
           access_trace errlog
     | Invalid invalidation_trace ->
-        PulseDomain.Trace.add_to_errlog ~nesting
+        PulseTrace.add_to_errlog ~nesting
           (fun fmt invalid ->
             F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var
               PulseInvalidation.describe invalid )

infer/src/checkers/impurityDomain.mli

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

infer/src/pulse/PulseAbductiveDomain.ml

@@ -10,7 +10,6 @@ module L = Logging
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
 module Attributes = PulseDomain.Attributes
-module Trace = PulseDomain.Trace
 module BaseStack = PulseDomain.Stack
 module BaseMemory = PulseDomain.Memory
 open PulseBasicInterface

infer/src/pulse/PulseAbductiveDomain.mli

@@ -7,7 +7,6 @@
 open! IStd
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
-module Trace = PulseDomain.Trace
 open PulseBasicInterface
 
 (* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition

infer/src/pulse/PulseBasicInterface.ml

@@ -10,4 +10,5 @@ open! IStd
 
 module CallEvent = PulseCallEvent
 module Invalidation = PulseInvalidation
+module Trace = PulseTrace
 module ValueHistory = PulseValueHistory

infer/src/pulse/PulseDiagnostic.ml

@@ -7,7 +7,6 @@
 
 open! IStd
 module F = Format
-module Trace = PulseDomain.Trace
 open PulseBasicInterface
 
 type t =

infer/src/pulse/PulseDiagnostic.mli

@@ -6,7 +6,6 @@
  *)
 
 open! IStd
-module Trace = PulseDomain.Trace
 open PulseBasicInterface
 
 (** an error to report to the user *)

infer/src/pulse/PulseDomain.ml

@@ -11,62 +11,6 @@ open PulseBasicInterface
 
 (* {2 Abstract domain description } *)
 
-module Trace = struct
-  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}
-  [@@deriving compare]
-
-  (** only for use in the attributes' [*_rank] functions *)
-  let mk_dummy imm = Immediate {imm; location= Location.dummy; history= []}
-
-  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_start_location trace =
-    match get_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 add_to_errlog ~nesting pp_immediate trace errlog =
-    match trace with
-    | Immediate {imm; location; history} ->
-        ValueHistory.add_to_errlog ~nesting history
-        @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
-           :: errlog
-    | ViaCall {f; location; in_call; history} ->
-        ValueHistory.add_to_errlog ~nesting history
-        @@ (fun errlog ->
-             Errlog.make_trace_element nesting location
-               (F.asprintf "when calling %a here" CallEvent.pp f)
-               []
-             :: errlog )
-        @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call
-        @@ errlog
-end
-
 module Attribute = struct
   (** Make sure we don't depend on [AbstractAddress] to avoid attributes depending on
       addresses. Otherwise they become a pain to handle when comparing memory states. *)
@@ -91,9 +35,11 @@ module Attribute = struct
 
   let to_rank = Variants.to_rank
 
+  let mk_dummy_trace imm = Trace.Immediate {imm; 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 (Trace.mk_dummy ()))
+  let written_to_rank = Variants.to_rank (WrittenTo (mk_dummy_trace ()))
 
   let address_of_stack_variable_rank =
     let pname = Typ.Procname.from_string_c_fun "" in
@@ -102,9 +48,9 @@ module Attribute = struct
     Variants.to_rank (AddressOfStackVariable (var, location, []))
 
 
-  let invalid_rank = Variants.to_rank (Invalid (Trace.mk_dummy Invalidation.Nullptr))
+  let invalid_rank = Variants.to_rank (Invalid (mk_dummy_trace Invalidation.Nullptr))
 
-  let must_be_valid_rank = Variants.to_rank (MustBeValid (Trace.mk_dummy ()))
+  let must_be_valid_rank = Variants.to_rank (MustBeValid (mk_dummy_trace ()))
 
   let std_vector_reserve_rank = Variants.to_rank StdVectorReserve
 

infer/src/pulse/PulseDomain.mli

@@ -9,33 +9,6 @@ open! IStd
 module F = Format
 open PulseBasicInterface
 
-module Trace : sig
-  type 'a t =
-    | Immediate of {imm: 'a; 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] *) }
-  [@@deriving compare]
-
-  val get_outer_location : 'a 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 *)
-
-  val get_start_location : 'a 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
-    -> Errlog.loc_trace_elem list
-    -> Errlog.loc_trace_elem list
-end
-
 module Attribute : sig
   type t =
     | AddressOfCppTemporary of Var.t * ValueHistory.t

infer/src/pulse/PulseOperations.ml

@@ -9,7 +9,6 @@ module L = Logging
 module AbstractAddress = PulseDomain.AbstractAddress
 module Attribute = PulseDomain.Attribute
 module Attributes = PulseDomain.Attributes
-module Trace = PulseDomain.Trace
 module Memory = PulseAbductiveDomain.Memory
 module Stack = PulseAbductiveDomain.Stack
 open Result.Monad_infix

infer/src/pulse/PulseTrace.ml

@@ -0,0 +1,60 @@
+(*
+ * 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 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}
+[@@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_start_location trace =
+  match get_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 add_to_errlog ~nesting pp_immediate trace errlog =
+  match trace with
+  | Immediate {imm; location; history} ->
+      ValueHistory.add_to_errlog ~nesting history
+      @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) []
+         :: errlog
+  | ViaCall {f; location; in_call; history} ->
+      ValueHistory.add_to_errlog ~nesting history
+      @@ (fun errlog ->
+           Errlog.make_trace_element nesting location
+             (F.asprintf "when calling %a here" CallEvent.pp f)
+             []
+           :: errlog )
+      @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call
+      @@ errlog

infer/src/pulse/PulseTrace.mli

@@ -0,0 +1,37 @@
+(*
+ * 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 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  (** 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] *) }
+[@@deriving compare]
+
+val pp : (F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
+
+val get_outer_location : 'a 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 *)
+
+val get_start_location : 'a 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
+  -> Errlog.loc_trace_elem list
+  -> Errlog.loc_trace_elem list