[pulse][3/9] add PulseValueHistory to PulseBasicInterface

Summary: See explanations in D17955104

Reviewed By: ezgicicek

Differential Revision: D17955285

fbshipit-source-id: 4e93a86df
master
Jules Villard 5 years ago committed by Facebook Github Bot
parent 168237a605
commit 8251e2dea8

@ -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 *)

@ -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*)

@ -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

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

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

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

@ -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}

@ -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}

@ -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 "<placement new>()"; location; in_call= []}
in
let event = ValueHistory.Call {f= Model "<placement new>()"; 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

@ -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

@ -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

@ -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

@ -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
Loading…
Cancel
Save