diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 8d20d09c6..c9620004b 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -9,7 +9,6 @@ module F = Format module L = Logging open Result.Monad_infix module AbstractAddress = PulseDomain.AbstractAddress -module ValueHistory = PulseDomain.ValueHistory open PulseBasicInterface include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index d7501263f..e52cbe2a4 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -11,9 +11,9 @@ module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Attributes = PulseDomain.Attributes module Trace = PulseDomain.Trace -module ValueHistory = PulseDomain.ValueHistory module BaseStack = PulseDomain.Stack module BaseMemory = PulseDomain.Memory +open PulseBasicInterface (** signature common to the "normal" [Domain], representing the post at the current program point, and the inverted [InvertedDomain], representing the inferred pre-condition*) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 704ba561e..570277331 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -8,7 +8,6 @@ open! IStd module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Trace = PulseDomain.Trace -module ValueHistory = PulseDomain.ValueHistory 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 ef428ef9b..00defe7ce 100644 --- a/infer/src/pulse/PulseBasicInterface.ml +++ b/infer/src/pulse/PulseBasicInterface.ml @@ -10,3 +10,4 @@ open! IStd module CallEvent = PulseCallEvent module Invalidation = PulseInvalidation +module ValueHistory = PulseValueHistory diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 0bd0df73d..987a0be0d 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -8,7 +8,6 @@ open! IStd module F = Format module Trace = PulseDomain.Trace -module ValueHistory = PulseDomain.ValueHistory open PulseBasicInterface type t = diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index dc262ddf4..43a6493bc 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -7,7 +7,6 @@ open! IStd module Trace = PulseDomain.Trace -module ValueHistory = PulseDomain.ValueHistory open PulseBasicInterface (** an error to report to the user *) diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 6798a727c..d6c62fcc0 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -11,106 +11,6 @@ open PulseBasicInterface (* {2 Abstract domain description } *) -module ValueHistory = struct - type event = - | Assignment of Location.t - | Call of {f: CallEvent.t; location: Location.t; in_call: t} - | Capture of {captured_as: Pvar.t; location: Location.t} - | CppTemporaryCreated of Location.t - | FormalDeclared of Pvar.t * Location.t - | VariableAccessed of Pvar.t * Location.t - | VariableDeclared of Pvar.t * Location.t - - and t = event list [@@deriving compare] - - let pp_event_no_location fmt event = - let pp_pvar fmt pvar = - if Pvar.is_global pvar then - F.fprintf fmt "global variable `%a`" Pvar.pp_value_non_verbose pvar - else F.fprintf fmt "variable `%a`" Pvar.pp_value_non_verbose pvar - in - match event with - | Assignment _ -> - F.pp_print_string fmt "assigned" - | Call {f; location= _} -> - F.fprintf fmt "passed as argument to %a" CallEvent.pp f - | Capture {captured_as; location= _} -> - F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as - | CppTemporaryCreated _ -> - F.pp_print_string fmt "C++ temporary created" - | FormalDeclared (pvar, _) -> - let pp_proc fmt pvar = - Pvar.get_declaring_function pvar - |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Typ.Procname.pp proc_name) - in - F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar - | VariableAccessed (pvar, _) -> - F.fprintf fmt "%a accessed here" pp_pvar pvar - | VariableDeclared (pvar, _) -> - F.fprintf fmt "%a declared here" pp_pvar pvar - - - let location_of_event = function - | Assignment location - | Call {location} - | Capture {location} - | CppTemporaryCreated location - | FormalDeclared (_, location) - | VariableAccessed (_, location) - | VariableDeclared (_, location) -> - location - - - let pp_event fmt event = - F.fprintf fmt "%a at %a" pp_event_no_location event Location.pp_line (location_of_event event) - - - let pp fmt history = - let rec pp_aux fmt = function - | [] -> - () - | (Call {f; in_call} as event) :: tail -> - F.fprintf fmt "%a@;" pp_event event ; - F.fprintf fmt "[%a]@;" pp_aux (List.rev in_call) ; - if not (List.is_empty tail) then F.fprintf fmt "return from call to %a@;" CallEvent.pp f ; - pp_aux fmt tail - | event :: tail -> - F.fprintf fmt "%a@;" pp_event event ; - pp_aux fmt tail - in - F.fprintf fmt "@[%a@]" pp_aux (List.rev history) - - - let add_event_to_errlog ~nesting event errlog = - let location = location_of_event event in - let description = F.asprintf "%a" pp_event_no_location event in - let tags = [] in - Errlog.make_trace_element nesting location description tags :: errlog - - - let add_returned_from_call_to_errlog ~nesting f location errlog = - let description = F.asprintf "return from call to %a" CallEvent.pp f in - let tags = [] in - Errlog.make_trace_element nesting location description tags :: errlog - - - let add_to_errlog ~nesting history errlog = - let rec add_to_errlog_aux ~nesting history errlog = - match history with - | [] -> - errlog - | (Call {f; location; in_call} as event) :: tail -> - add_to_errlog_aux ~nesting tail - @@ add_event_to_errlog ~nesting event - @@ add_to_errlog_aux ~nesting:(nesting + 1) in_call - @@ add_returned_from_call_to_errlog ~nesting f location - @@ errlog - | event :: tail -> - add_to_errlog_aux ~nesting tail @@ add_event_to_errlog ~nesting event @@ errlog - in - add_to_errlog_aux ~nesting history errlog -end - module Trace = struct type 'a t = | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t} diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 70510db2e..4de23f69b 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -9,21 +9,6 @@ open! IStd module F = Format open PulseBasicInterface -module ValueHistory : sig - type event = - | Assignment of Location.t - | Call of {f: CallEvent.t; location: Location.t; in_call: t} - | Capture of {captured_as: Pvar.t; location: Location.t} - | CppTemporaryCreated of Location.t - | FormalDeclared of Pvar.t * Location.t - | VariableAccessed of Pvar.t * Location.t - | VariableDeclared of Pvar.t * Location.t - - and t = event list [@@deriving compare] - - val add_to_errlog : nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list -end - module Trace : sig type 'a t = | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t} diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index dfe7d323a..afe84cbc5 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -21,7 +21,7 @@ type model = exec_fun module Misc = struct let shallow_copy model_desc : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let event = PulseDomain.ValueHistory.Call {f= Model model_desc; location; in_call= []} in + let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in ( match actuals with | [(dest_pointer_hist, _); (src_pointer_hist, _)] -> PulseOperations.eval_access location src_pointer_hist Dereference astate @@ -65,9 +65,7 @@ module Cplusplus = struct let placement_new : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let event = - PulseDomain.ValueHistory.Call {f= Model "()"; location; in_call= []} - in + let event = ValueHistory.Call {f= Model "()"; location; in_call= []} in match List.rev actuals with | ((address, hist), _) :: _ -> Ok [PulseOperations.write_id ret_id (address, event :: hist) astate] @@ -90,9 +88,7 @@ module StdBasicString = struct let data : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> - let event = - PulseDomain.ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} - in + let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in match actuals with | [(this_hist, _)] -> to_internal_string location this_hist astate @@ -107,7 +103,7 @@ module StdBasicString = struct let destructor : model = fun ~caller_summary:_ location ~ret:(ret_id, _) ~actuals astate -> let model = CallEvent.Model "std::basic_string::~basic_string()" in - let call_event = PulseDomain.ValueHistory.Call {f= model; location; in_call= []} in + let call_event = ValueHistory.Call {f= model; location; in_call= []} in match actuals with | [(this_hist, _)] -> to_internal_string location this_hist astate @@ -126,7 +122,7 @@ module StdFunction = struct fun ~caller_summary location ~ret ~actuals astate -> let havoc_ret (ret_id, _) astate = let event = - PulseDomain.ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} + ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] in @@ -179,7 +175,7 @@ module StdVector = struct match actuals with | (vector, _) :: _ -> let crumb = - PulseDomain.ValueHistory.Call + ValueHistory.Call { f= Model (Format.asprintf "%a()" Invalidation.pp_std_vector_function vector_f) ; location ; in_call= [] } @@ -191,9 +187,7 @@ module StdVector = struct let at : model = fun ~caller_summary:_ location ~ret ~actuals astate -> - let event = - PulseDomain.ValueHistory.Call {f= Model "std::vector::at()"; location; in_call= []} - in + let event = ValueHistory.Call {f= Model "std::vector::at()"; location; in_call= []} in match actuals with | [(vector, _); (index, _)] -> element_of_internal_array location vector (fst index) astate @@ -207,9 +201,7 @@ module StdVector = struct fun ~caller_summary:_ location ~ret:_ ~actuals astate -> match actuals with | [(vector, _); _value] -> - let crumb = - PulseDomain.ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} - in + let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in reallocate_internal_array [crumb] vector Reserve location astate >>| PulseAbductiveDomain.Memory.std_vector_reserve (fst vector) >>| List.return @@ -222,7 +214,7 @@ module StdVector = struct match actuals with | [(vector, _); _value] -> let crumb = - PulseDomain.ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []} + ValueHistory.Call {f= Model "std::vector::push_back()"; location; in_call= []} in if PulseAbductiveDomain.Memory.is_std_vector_reserved (fst vector) astate then (* assume that any call to [push_back] is ok after one called [reserve] on the same vector diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 915abb454..854fde93e 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -10,10 +10,10 @@ module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Attributes = PulseDomain.Attributes module Trace = PulseDomain.Trace -module ValueHistory = PulseDomain.ValueHistory module Memory = PulseAbductiveDomain.Memory module Stack = PulseAbductiveDomain.Stack open Result.Monad_infix +open PulseBasicInterface include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) struct diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 16c205145..9c97a7aab 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -45,16 +45,16 @@ val eval_access : (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if so dereferences it according to the access. *) -val havoc_id : Ident.t -> PulseDomain.ValueHistory.t -> t -> t +val havoc_id : Ident.t -> ValueHistory.t -> t -> t val havoc_deref : - Location.t -> PulseDomain.AddrTracePair.t -> PulseDomain.ValueHistory.t -> t -> t access_result + Location.t -> PulseDomain.AddrTracePair.t -> ValueHistory.t -> t -> t access_result val havoc_field : Location.t -> PulseDomain.AddrTracePair.t -> Typ.Fieldname.t - -> PulseDomain.ValueHistory.t + -> ValueHistory.t -> t -> t access_result @@ -86,25 +86,20 @@ val shallow_copy : Location.t -> PulseDomain.AddrTracePair.t -> t - -> (t * (AbstractAddress.t * PulseDomain.ValueHistory.t)) access_result + -> (t * (AbstractAddress.t * ValueHistory.t)) access_result (** returns the address of a new cell with the same edges as the original *) val remove_vars : Var.t list -> Location.t -> t -> t val check_address_escape : - Location.t - -> Procdesc.t - -> AbstractAddress.t - -> PulseDomain.ValueHistory.t - -> t - -> t access_result + Location.t -> Procdesc.t -> AbstractAddress.t -> ValueHistory.t -> t -> t access_result val call : caller_summary:Summary.t -> Location.t -> Typ.Procname.t -> ret:Ident.t * Typ.t - -> actuals:((AbstractAddress.t * PulseDomain.ValueHistory.t) * Typ.t) list + -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list -> t -> t list access_result (** perform an interprocedural call: apply the summary for the call proc name passed as argument if diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml new file mode 100644 index 000000000..9af63bdb2 --- /dev/null +++ b/infer/src/pulse/PulseValueHistory.ml @@ -0,0 +1,106 @@ +(* + * 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 + +type event = + | Assignment of Location.t + | Call of {f: CallEvent.t; location: Location.t; in_call: t} + | Capture of {captured_as: Pvar.t; location: Location.t} + | CppTemporaryCreated of Location.t + | FormalDeclared of Pvar.t * Location.t + | VariableAccessed of Pvar.t * Location.t + | VariableDeclared of Pvar.t * Location.t + +and t = event list [@@deriving compare] + +let pp_event_no_location fmt event = + let pp_pvar fmt pvar = + if Pvar.is_global pvar then F.fprintf fmt "global variable `%a`" Pvar.pp_value_non_verbose pvar + else F.fprintf fmt "variable `%a`" Pvar.pp_value_non_verbose pvar + in + match event with + | Assignment _ -> + F.pp_print_string fmt "assigned" + | Call {f; location= _} -> + F.fprintf fmt "passed as argument to %a" CallEvent.pp f + | Capture {captured_as; location= _} -> + F.fprintf fmt "value captured as `%a`" Pvar.pp_value_non_verbose captured_as + | CppTemporaryCreated _ -> + F.pp_print_string fmt "C++ temporary created" + | FormalDeclared (pvar, _) -> + let pp_proc fmt pvar = + Pvar.get_declaring_function pvar + |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Typ.Procname.pp proc_name) + in + F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar + | VariableAccessed (pvar, _) -> + F.fprintf fmt "%a accessed here" pp_pvar pvar + | VariableDeclared (pvar, _) -> + F.fprintf fmt "%a declared here" pp_pvar pvar + + +let location_of_event = function + | Assignment location + | Call {location} + | Capture {location} + | CppTemporaryCreated location + | FormalDeclared (_, location) + | VariableAccessed (_, location) + | VariableDeclared (_, location) -> + location + + +let pp_event fmt event = + F.fprintf fmt "%a at %a" pp_event_no_location event Location.pp_line (location_of_event event) + + +let pp fmt history = + let rec pp_aux fmt = function + | [] -> + () + | (Call {f; in_call} as event) :: tail -> + F.fprintf fmt "%a@;" pp_event event ; + F.fprintf fmt "[%a]@;" pp_aux (List.rev in_call) ; + if not (List.is_empty tail) then F.fprintf fmt "return from call to %a@;" CallEvent.pp f ; + pp_aux fmt tail + | event :: tail -> + F.fprintf fmt "%a@;" pp_event event ; + pp_aux fmt tail + in + F.fprintf fmt "@[%a@]" pp_aux (List.rev history) + + +let add_event_to_errlog ~nesting event errlog = + let location = location_of_event event in + let description = F.asprintf "%a" pp_event_no_location event in + let tags = [] in + Errlog.make_trace_element nesting location description tags :: errlog + + +let add_returned_from_call_to_errlog ~nesting f location errlog = + let description = F.asprintf "return from call to %a" CallEvent.pp f in + let tags = [] in + Errlog.make_trace_element nesting location description tags :: errlog + + +let add_to_errlog ~nesting history errlog = + let rec add_to_errlog_aux ~nesting history errlog = + match history with + | [] -> + errlog + | (Call {f; location; in_call} as event) :: tail -> + add_to_errlog_aux ~nesting tail + @@ add_event_to_errlog ~nesting event + @@ add_to_errlog_aux ~nesting:(nesting + 1) in_call + @@ add_returned_from_call_to_errlog ~nesting f location + @@ errlog + | event :: tail -> + add_to_errlog_aux ~nesting tail @@ add_event_to_errlog ~nesting event @@ errlog + in + add_to_errlog_aux ~nesting history errlog diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli new file mode 100644 index 000000000..1c02962a2 --- /dev/null +++ b/infer/src/pulse/PulseValueHistory.mli @@ -0,0 +1,26 @@ +(* + * 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 + +type event = + | Assignment of Location.t + | Call of {f: CallEvent.t; location: Location.t; in_call: t} + | Capture of {captured_as: Pvar.t; location: Location.t} + | CppTemporaryCreated of Location.t + | FormalDeclared of Pvar.t * Location.t + | VariableAccessed of Pvar.t * Location.t + | VariableDeclared of Pvar.t * Location.t + +and t = event list [@@deriving compare] + +val pp : F.formatter -> t -> unit + +val location_of_event : event -> Location.t + +val add_to_errlog : nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list