diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 5a3890368..1139c5cbb 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/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 ) diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 0a82b5b09..4d9c9ffe8 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index e52cbe2a4..7aba3107f 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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 diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 570277331..e4e7adc1c 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseBasicInterface.ml b/infer/src/pulse/PulseBasicInterface.ml index 00defe7ce..c32af64aa 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -10,4 +10,5 @@ open! IStd module CallEvent = PulseCallEvent module Invalidation = PulseInvalidation +module Trace = PulseTrace module ValueHistory = PulseValueHistory diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 987a0be0d..2ef3548cf 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -7,7 +7,6 @@ open! IStd module F = Format -module Trace = PulseDomain.Trace open PulseBasicInterface type t = diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 43a6493bc..1b667e644 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -6,7 +6,6 @@ *) open! IStd -module Trace = PulseDomain.Trace open PulseBasicInterface (** an error to report to the user *) diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index d6c62fcc0..600828cfe 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/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 diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 4de23f69b..8e14f062a 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/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 diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 854fde93e..8e5ed45d4 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/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 diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml new file mode 100644 index 000000000..fe6e83bff --- /dev/null +++ b/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 diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli new file mode 100644 index 000000000..7d4bde141 --- /dev/null +++ b/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