[pulse] move [PulseTrace] inside [PulseDomain]

Summary:
Just moving code around.

This is needed later to make some types in `PulseTrace` depend on
a new that I'll have to define in `PulseDomain`.

Also, this gives better names all around I think

Reviewed By: mbouaziz

Differential Revision: D15881281

fbshipit-source-id: e86c1472e
master
Jules Villard 6 years ago committed by Facebook Github Bot
parent b03aeb49c2
commit 695b493b56

@ -9,6 +9,8 @@ module F = Format
module L = Logging module L = Logging
open Result.Monad_infix open Result.Monad_infix
module AbstractAddress = PulseDomain.AbstractAddress module AbstractAddress = PulseDomain.AbstractAddress
module InterprocAction = PulseDomain.InterprocAction
module ValueHistory = PulseDomain.ValueHistory
include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *) include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
struct struct
@ -52,7 +54,7 @@ module PulseTransferFunctions = struct
let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc
astate = astate =
(* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *) (* try to evaluate [rhs_exp] down to an abstract address or generate a fresh one *)
let crumb = PulseTrace.Assignment {lhs= lhs_access; location= loc} in let crumb = ValueHistory.Assignment {lhs= lhs_access; location= loc} in
match rhs_exp with match rhs_exp with
| AccessExpression rhs_access -> ( | AccessExpression rhs_access -> (
PulseOperations.read loc rhs_access astate PulseOperations.read loc rhs_access astate
@ -80,7 +82,7 @@ module PulseTransferFunctions = struct
let read_all args astate = let read_all args astate =
PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate
in in
let crumb = PulseTrace.Call {f= `HilCall call; actuals; location= call_loc} in let crumb = ValueHistory.Call {f= `HilCall call; actuals; location= call_loc} in
match call with match call with
| Direct callee_pname when Typ.Procname.is_constructor callee_pname -> ( | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> (
L.d_printfln "constructor call detected@." ; L.d_printfln "constructor call detected@." ;
@ -152,7 +154,7 @@ module PulseTransferFunctions = struct
(* invalidate both [&x] and [x]: reading either is now forbidden *) (* invalidate both [&x] and [x]: reading either is now forbidden *)
let invalidate pvar typ access astate = let invalidate pvar typ access astate =
PulseOperations.invalidate PulseOperations.invalidate
(PulseTrace.Immediate {imm= GoneOutOfScope (pvar, typ); location= call_loc}) (InterprocAction.Immediate {imm= GoneOutOfScope (pvar, typ); location= call_loc})
call_loc access astate call_loc access astate
in in
let out_of_scope_base = HilExp.AccessExpression.base (Var.of_pvar pvar, typ) in let out_of_scope_base = HilExp.AccessExpression.base (Var.of_pvar pvar, typ) in

@ -356,9 +356,10 @@ module PrePost = struct
[call_state.astate] starting from address [addr_caller]. Report an error if some invalid [call_state.astate] starting from address [addr_caller]. Report an error if some invalid
addresses are traversed in the process. *) addresses are traversed in the process. *)
let rec materialize_pre_from_address callee_proc_name call_location access_expr ~pre ~addr_pre let rec materialize_pre_from_address callee_proc_name call_location access_expr ~pre ~addr_pre
~addr_caller breadcrumbs call_state = ~addr_caller history call_state =
let mk_action action = let mk_action action =
PulseTrace.ViaCall {action; proc_name= callee_proc_name; location= call_location} PulseDomain.InterprocAction.ViaCall
{action; proc_name= callee_proc_name; location= call_location}
in in
match visit call_state ~addr_callee:addr_pre ~addr_caller with match visit call_state ~addr_callee:addr_pre ~addr_caller with
| `AlreadyVisited, call_state -> | `AlreadyVisited, call_state ->
@ -374,7 +375,7 @@ module PrePost = struct
| Error invalidated_by -> | Error invalidated_by ->
Error Error
(PulseDiagnostic.AccessToInvalidAddress (PulseDiagnostic.AccessToInvalidAddress
{access= access_expr; invalidated_by; accessed_by= {action; breadcrumbs}}) {access= access_expr; invalidated_by; accessed_by= {action; history}})
| Ok astate -> | Ok astate ->
let call_state = {call_state with astate} in let call_state = {call_state with astate} in
Container.fold_result Container.fold_result
@ -391,7 +392,7 @@ module PrePost = struct
|> Option.value ~default:access_expr |> Option.value ~default:access_expr
in in
materialize_pre_from_address callee_proc_name call_location access_expr ~pre materialize_pre_from_address callee_proc_name call_location access_expr ~pre
~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest breadcrumbs call_state )) ~addr_pre:addr_pre_dest ~addr_caller:addr_caller_dest history call_state ))
|> function Some result -> result | None -> Ok call_state ) |> function Some result -> result | None -> Ok call_state )
@ -456,7 +457,8 @@ module PrePost = struct
fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state fold_globals_of_stack (pre_post.pre :> PulseDomain.t).stack call_state
~f:(fun var ~stack_value:(addr_pre, loc_opt) ~addr_caller call_state -> ~f:(fun var ~stack_value:(addr_pre, loc_opt) ~addr_caller call_state ->
let trace = let trace =
Option.map loc_opt ~f:(fun loc -> PulseTrace.VariableDeclaration loc) |> Option.to_list Option.map loc_opt ~f:(fun loc -> PulseDomain.ValueHistory.VariableDeclaration loc)
|> Option.to_list
in in
let access_expr = HilExp.AccessExpression.base (var, Typ.void) in let access_expr = HilExp.AccessExpression.base (var, Typ.void) in
materialize_pre_from_address callee_proc_name call_location access_expr materialize_pre_from_address callee_proc_name call_location access_expr
@ -521,8 +523,8 @@ module PrePost = struct
match (attr : PulseDomain.Attribute.t) with match (attr : PulseDomain.Attribute.t) with
| Invalid trace -> | Invalid trace ->
PulseDomain.Attribute.Invalid PulseDomain.Attribute.Invalid
{ action= PulseTrace.ViaCall {action= trace.action; proc_name; location} { action= PulseDomain.InterprocAction.ViaCall {action= trace.action; proc_name; location}
; breadcrumbs= trace.breadcrumbs } ; history= trace.history }
| MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve -> | MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve ->
attr attr
@ -580,7 +582,7 @@ module PrePost = struct
let addr_curr, subst = subst_find_or_new subst addr_callee in let addr_curr, subst = subst_find_or_new subst addr_callee in
( subst ( subst
, ( addr_curr , ( addr_curr
, PulseTrace.Call , PulseDomain.ValueHistory.Call
{f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc} {f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc}
:: trace_post ) ) ) :: trace_post ) ) )
in in

@ -43,18 +43,18 @@ module Memory : sig
val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t
val check_valid : val check_valid :
HilExp.AccessExpression.t PulseTrace.action HilExp.AccessExpression.t PulseDomain.InterprocAction.t
-> AbstractAddress.t -> AbstractAddress.t
-> t -> t
-> (t, PulseDomain.Invalidation.t PulseTrace.t) result -> (t, PulseDomain.Invalidation.t PulseDomain.Trace.t) result
val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option
val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t val set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t
val invalidate : val invalidate :
AbstractAddress.t * PulseTrace.breadcrumbs AbstractAddress.t * PulseDomain.ValueHistory.t
-> PulseDomain.Invalidation.t PulseTrace.action -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-> t -> t
-> t -> t
@ -79,8 +79,9 @@ module PrePost : sig
-> Location.t -> Location.t
-> t -> t
-> formals:Var.t list -> formals:Var.t list
-> ret:AbstractAddress.t * PulseTrace.breadcrumbs -> ret:AbstractAddress.t * PulseDomain.ValueHistory.t
-> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseTrace.breadcrumbs) option list -> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseDomain.ValueHistory.t) option
list
-> domain_t -> domain_t
-> (domain_t, PulseDiagnostic.t) result -> (domain_t, PulseDiagnostic.t) result
end end

@ -11,16 +11,16 @@ module F = Format
type t = type t =
| AccessToInvalidAddress of | AccessToInvalidAddress of
{ access: HilExp.AccessExpression.t { access: HilExp.AccessExpression.t
; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
; accessed_by: HilExp.AccessExpression.t PulseTrace.t } ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t }
| StackVariableAddressEscape of | StackVariableAddressEscape of
{ variable: Var.t { variable: Var.t
; trace: PulseTrace.breadcrumbs ; history: PulseDomain.ValueHistory.t
; location: Location.t } ; location: Location.t }
let get_location = function let get_location = function
| AccessToInvalidAddress {accessed_by} -> | AccessToInvalidAddress {accessed_by} ->
PulseTrace.outer_location_of_action accessed_by.action PulseDomain.InterprocAction.to_outer_location accessed_by.action
| StackVariableAddressEscape {location} -> | StackVariableAddressEscape {location} ->
location location
@ -44,8 +44,8 @@ let get_message = function
Likewise if we don't have "x" in the second part but instead some non-user-visible expression, then 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`" "`x->f` accesses `x`, which was invalidated at line 42 by `delete`"
*) *)
let pp_access_trace invalidated f trace = let pp_access_trace invalidated f (trace : HilExp.AccessExpression.t PulseDomain.Trace.t) =
match trace.PulseTrace.action with match trace.action with
| Immediate {imm= access; _} -> ( | Immediate {imm= access; _} -> (
match HilExp.AccessExpression.to_source_string access with match HilExp.AccessExpression.to_source_string access with
| Some access_s when HilExp.AccessExpression.equal access invalidated -> | Some access_s when HilExp.AccessExpression.equal access invalidated ->
@ -65,7 +65,8 @@ let get_message = function
| ViaCall {action; proc_name; _} -> ( | ViaCall {action; proc_name; _} -> (
let access_and_invalidated_s = let access_and_invalidated_s =
match match
( HilExp.AccessExpression.to_source_string (PulseTrace.immediate_of_action action) ( HilExp.AccessExpression.to_source_string
(PulseDomain.InterprocAction.get_immediate action :> HilExp.AccessExpression.t)
, HilExp.AccessExpression.to_source_string invalidated ) , HilExp.AccessExpression.to_source_string invalidated )
with with
| Some access_s, Some invalidated_s -> | Some access_s, Some invalidated_s ->
@ -84,17 +85,19 @@ let get_message = function
proc_name HilExp.AccessExpression.pp invalidated ) proc_name HilExp.AccessExpression.pp invalidated )
in in
let pp_invalidation_trace line f trace = let pp_invalidation_trace line f trace =
match trace.PulseTrace.action with match trace.PulseDomain.Trace.action with
| Immediate {imm= invalidation; _} -> | Immediate {imm= invalidation; _} ->
F.fprintf f "%a on line %d" PulseDomain.Invalidation.describe invalidation line F.fprintf f "%a on line %d" PulseDomain.Invalidation.describe invalidation line
| ViaCall {action; proc_name; _} -> | ViaCall {action; proc_name; _} ->
F.fprintf f "%a on line %d indirectly during the call to `%a`" F.fprintf f "%a on line %d indirectly during the call to `%a`"
PulseDomain.Invalidation.describe PulseDomain.Invalidation.describe
(PulseTrace.immediate_of_action action) (PulseDomain.InterprocAction.get_immediate action)
line Typ.Procname.describe proc_name line Typ.Procname.describe proc_name
in in
let line_of_trace trace = let line_of_trace trace =
let {Location.line; _} = PulseTrace.outer_location_of_action trace.PulseTrace.action in let {Location.line; _} =
PulseDomain.InterprocAction.to_outer_location trace.PulseDomain.Trace.action
in
line line
in in
let invalidation_line = line_of_trace invalidated_by in let invalidation_line = line_of_trace invalidated_by in
@ -111,16 +114,18 @@ let get_message = function
let get_trace = function let get_trace = function
| AccessToInvalidAddress {accessed_by; invalidated_by} -> | AccessToInvalidAddress {accessed_by; invalidated_by} ->
PulseTrace.add_to_errlog ~header:"invalidation part of the trace starts here" PulseDomain.Trace.add_to_errlog ~header:"invalidation part of the trace starts here"
(fun f invalidation -> (fun f invalidation ->
F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation ) F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation )
invalidated_by invalidated_by
@@ PulseTrace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here" @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here"
(fun f access -> F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp access) (fun f (access : HilExp.AccessExpression.t) ->
F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp
(access :> HilExp.AccessExpression.t) )
accessed_by accessed_by
@@ [] @@ []
| StackVariableAddressEscape {trace; location; _} -> | StackVariableAddressEscape {history; location; _} ->
PulseTrace.add_errlog_of_breadcrumbs ~nesting:0 trace PulseDomain.ValueHistory.add_to_errlog ~nesting:0 history
@@ @@
let nesting = 0 in let nesting = 0 in
[Errlog.make_trace_element nesting location "returned here" []] [Errlog.make_trace_element nesting location "returned here" []]
@ -128,7 +133,7 @@ let get_trace = function
let get_issue_type = function let get_issue_type = function
| AccessToInvalidAddress {invalidated_by} -> | AccessToInvalidAddress {invalidated_by} ->
PulseTrace.immediate_of_action invalidated_by.action PulseDomain.InterprocAction.get_immediate invalidated_by.action
|> PulseDomain.Invalidation.issue_type_of_cause |> PulseDomain.Invalidation.issue_type_of_cause
| StackVariableAddressEscape _ -> | StackVariableAddressEscape _ ->
IssueType.stack_variable_address_escape IssueType.stack_variable_address_escape

@ -11,11 +11,11 @@ open! IStd
type t = type t =
| AccessToInvalidAddress of | AccessToInvalidAddress of
{ access: HilExp.AccessExpression.t { access: HilExp.AccessExpression.t
; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t
; accessed_by: HilExp.AccessExpression.t PulseTrace.t } ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t }
| StackVariableAddressEscape of | StackVariableAddressEscape of
{ variable: Var.t { variable: Var.t
; trace: PulseTrace.breadcrumbs ; history: PulseDomain.ValueHistory.t
; location: Location.t } ; location: Location.t }
val get_message : t -> string val get_message : t -> string

@ -96,12 +96,147 @@ module Invalidation = struct
F.fprintf f "StdVector(%a)" describe invalidation F.fprintf f "StdVector(%a)" describe invalidation
end end
module ValueHistory = struct
type event =
| VariableDeclaration of Location.t
| CppTemporaryCreated of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
| Capture of
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t
; location: Location.t }
| Call of
{ f: [`HilCall of HilInstr.call | `Model of string]
; actuals: HilExp.t list
; location: Location.t }
[@@deriving compare]
let pp_event_no_location fmt = function
| VariableDeclaration _ ->
F.pp_print_string fmt "variable declared"
| CppTemporaryCreated _ ->
F.pp_print_string fmt "C++ temporary created"
| Capture {captured_as; captured; location= _} ->
F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured
AccessPath.pp_base captured_as
| Assignment {lhs; location= _} ->
F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
| Call {f; actuals; location= _} ->
let pp_f fmt = function
| `HilCall call ->
F.fprintf fmt "%a" HilInstr.pp_call call
| `Model model ->
F.pp_print_string fmt model
in
F.fprintf fmt "returned from call to `%a(%a)`" pp_f f (Pp.seq ~sep:"," HilExp.pp) actuals
let location_of_event = function
| VariableDeclaration location
| CppTemporaryCreated location
| Assignment {location}
| Capture {location}
| Call {location} ->
location
let pp_event fmt crumb =
F.fprintf fmt "%a at %a" pp_event_no_location crumb Location.pp_line (location_of_event crumb)
let errlog_trace_elem_of_event ~nesting crumb =
let location = location_of_event crumb in
let description = F.asprintf "%a" pp_event_no_location crumb in
let tags = [] in
Errlog.make_trace_element nesting location description tags
type t = event list [@@deriving compare]
let pp f events = Pp.seq ~print_env:Pp.text_break pp_event f events
let add_to_errlog ~nesting events errlog =
List.rev_map_append ~f:(errlog_trace_elem_of_event ~nesting) events errlog
let get_start_location = function [] -> None | crumb :: _ -> Some (location_of_event crumb)
end
module InterprocAction = struct
type 'a t =
| Immediate of {imm: 'a; location: Location.t}
| ViaCall of {action: 'a t; proc_name: Typ.Procname.t; location: Location.t}
[@@deriving compare]
let rec get_immediate = function
| Immediate {imm; _} ->
imm
| ViaCall {action; _} ->
get_immediate action
let pp pp_immediate fmt = function
| Immediate {imm; _} ->
pp_immediate fmt imm
| ViaCall {proc_name; action; _} ->
F.fprintf fmt "%a in call to `%a`" pp_immediate (get_immediate action)
Typ.Procname.describe proc_name
let add_to_errlog ~nesting pp_immediate action errlog =
let rec aux ~nesting rev_errlog action =
match action with
| Immediate {imm; location} ->
let rev_errlog =
Errlog.make_trace_element nesting location (F.asprintf "%a here" pp_immediate imm) []
:: rev_errlog
in
List.rev_append rev_errlog errlog
| ViaCall {action; proc_name; location} ->
aux ~nesting:(nesting + 1)
( Errlog.make_trace_element nesting location
(F.asprintf "when calling `%a` here" Typ.Procname.describe proc_name)
[]
:: rev_errlog )
action
in
aux ~nesting [] action
let to_outer_location = function Immediate {location} | ViaCall {location} -> location
end
module Trace = struct
type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
let pp pp_immediate f {action; _} = InterprocAction.pp pp_immediate f action
let add_errlog_header ~title location errlog =
let depth = 0 in
let tags = [] in
Errlog.make_trace_element depth location title tags :: errlog
let add_to_errlog ~header pp_immediate trace errlog =
let start_location =
match ValueHistory.get_start_location trace.history with
| Some location ->
location
| None ->
InterprocAction.to_outer_location trace.action
in
add_errlog_header ~title:header start_location
@@ ValueHistory.add_to_errlog ~nesting:1 trace.history
@@ InterprocAction.add_to_errlog ~nesting:1 pp_immediate trace.action
@@ errlog
end
(** Purposefully declared before [AbstractAddress] to avoid attributes depending on (** Purposefully declared before [AbstractAddress] to avoid attributes depending on
addresses. Otherwise they become a pain to handle when comparing memory states. *) addresses. Otherwise they become a pain to handle when comparing memory states. *)
module Attribute = struct module Attribute = struct
type t = type t =
| Invalid of Invalidation.t PulseTrace.t | Invalid of Invalidation.t Trace.t
| MustBeValid of HilExp.AccessExpression.t PulseTrace.action | MustBeValid of HilExp.AccessExpression.t InterprocAction.t
| AddressOfCppTemporary of Var.t * Location.t option | AddressOfCppTemporary of Var.t * Location.t option
| Closure of Typ.Procname.t | Closure of Typ.Procname.t
| StdVectorReserve | StdVectorReserve
@ -114,7 +249,7 @@ module Attribute = struct
let invalid_rank = let invalid_rank =
Variants.to_rank Variants.to_rank
(Invalid (Invalid
{action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; breadcrumbs= []}) {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []})
let must_be_valid_rank = let must_be_valid_rank =
@ -131,12 +266,12 @@ module Attribute = struct
let pp f = function let pp f = function
| Invalid invalidation -> | Invalid invalidation ->
(PulseTrace.pp Invalidation.pp) f invalidation (Trace.pp Invalidation.pp) f invalidation
| MustBeValid action -> | MustBeValid action ->
F.fprintf f "MustBeValid (read by %a @ %a)" F.fprintf f "MustBeValid (read by %a @ %a)"
(PulseTrace.pp_action HilExp.AccessExpression.pp) (InterprocAction.pp HilExp.AccessExpression.pp)
action Location.pp action Location.pp
(PulseTrace.outer_location_of_action action) (InterprocAction.to_outer_location action)
| AddressOfCppTemporary (var, location_opt) -> | AddressOfCppTemporary (var, location_opt) ->
F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt
| Closure pname -> | Closure pname ->
@ -215,11 +350,11 @@ module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress)
(* {3 Heap domain } *) (* {3 Heap domain } *)
module AddrTracePair = struct module AddrTracePair = struct
type t = AbstractAddress.t * PulseTrace.breadcrumbs [@@deriving compare] type t = AbstractAddress.t * ValueHistory.t [@@deriving compare]
let pp f addr_trace = let pp f addr_trace =
if Config.debug_level_analysis >= 3 then if Config.debug_level_analysis >= 3 then
Pp.pair ~fst:AbstractAddress.pp ~snd:PulseTrace.pp_breadcrumbs f addr_trace Pp.pair ~fst:AbstractAddress.pp ~snd:ValueHistory.pp f addr_trace
else AbstractAddress.pp f (fst addr_trace) else AbstractAddress.pp f (fst addr_trace)
end end
@ -262,10 +397,9 @@ module Memory : sig
val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
val invalidate : val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> t -> t
AbstractAddress.t * PulseTrace.breadcrumbs -> Invalidation.t PulseTrace.action -> t -> t
val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t PulseTrace.t) result val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
val std_vector_reserve : AbstractAddress.t -> t -> t val std_vector_reserve : AbstractAddress.t -> t -> t
@ -328,8 +462,8 @@ end = struct
add_attributes address (Attributes.singleton attribute) memory add_attributes address (Attributes.singleton attribute) memory
let invalidate (address, breadcrumbs) invalidation memory = let invalidate (address, history) invalidation memory =
add_attribute address (Attribute.Invalid {action= invalidation; breadcrumbs}) memory add_attribute address (Attribute.Invalid {action= invalidation; history}) memory
let check_valid address memory = let check_valid address memory =

@ -35,10 +35,52 @@ module Invalidation : sig
val describe : Format.formatter -> t -> unit val describe : Format.formatter -> t -> unit
end end
module ValueHistory : sig
type event =
| VariableDeclaration of Location.t
| CppTemporaryCreated of Location.t
| Assignment of {lhs: HilExp.access_expression; location: Location.t}
| Capture of
{ captured_as: AccessPath.base
; captured: HilExp.access_expression
; location: Location.t }
| Call of
{ f: [`HilCall of HilInstr.call | `Model of string]
; actuals: HilExp.t list
; location: Location.t }
type t = event list [@@deriving compare]
val add_to_errlog :
nesting:int -> event list -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list
end
module InterprocAction : sig
type 'a t =
| Immediate of {imm: 'a; location: Location.t}
| ViaCall of {action: 'a t; proc_name: Typ.Procname.t; location: Location.t}
[@@deriving compare]
val get_immediate : 'a t -> 'a
val to_outer_location : 'a t -> Location.t
end
module Trace : sig
type 'a t = {action: 'a InterprocAction.t; history: ValueHistory.t} [@@deriving compare]
val add_to_errlog :
header:string
-> (F.formatter -> 'a -> unit)
-> 'a t
-> Errlog.loc_trace_elem list
-> Errlog.loc_trace_elem list
end
module Attribute : sig module Attribute : sig
type t = type t =
| Invalid of Invalidation.t PulseTrace.t | Invalid of Invalidation.t Trace.t
| MustBeValid of HilExp.AccessExpression.t PulseTrace.action | MustBeValid of HilExp.AccessExpression.t InterprocAction.t
| AddressOfCppTemporary of Var.t * Location.t option | AddressOfCppTemporary of Var.t * Location.t option
| Closure of Typ.Procname.t | Closure of Typ.Procname.t
| StdVectorReserve | StdVectorReserve
@ -48,7 +90,7 @@ end
module Attributes : sig module Attributes : sig
include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t include PrettyPrintable.PPUniqRankSet with type elt = Attribute.t
val get_must_be_valid : t -> HilExp.AccessExpression.t PulseTrace.action option val get_must_be_valid : t -> HilExp.AccessExpression.t InterprocAction.t option
end end
module AbstractAddress : sig module AbstractAddress : sig
@ -85,7 +127,7 @@ module Stack : sig
end end
module AddrTracePair : sig module AddrTracePair : sig
type t = AbstractAddress.t * PulseTrace.breadcrumbs [@@deriving compare] type t = AbstractAddress.t * ValueHistory.t [@@deriving compare]
end end
module Memory : sig module Memory : sig
@ -120,10 +162,9 @@ module Memory : sig
val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t
val invalidate : val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> t -> t
AbstractAddress.t * PulseTrace.breadcrumbs -> Invalidation.t PulseTrace.action -> t -> t
val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t PulseTrace.t) result val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
val std_vector_reserve : AbstractAddress.t -> t -> t val std_vector_reserve : AbstractAddress.t -> t -> t

@ -26,7 +26,8 @@ module C = struct
match actuals with match actuals with
| [AccessExpression deleted_access] -> | [AccessExpression deleted_access] ->
PulseOperations.invalidate PulseOperations.invalidate
(PulseTrace.Immediate {imm= PulseDomain.Invalidation.CFree deleted_access; location}) (PulseDomain.InterprocAction.Immediate
{imm= PulseDomain.Invalidation.CFree deleted_access; location})
location deleted_access astate location deleted_access astate
>>| List.return >>| List.return
| _ -> | _ ->
@ -41,7 +42,8 @@ module Cplusplus = struct
match actuals with match actuals with
| [AccessExpression deleted_access] -> | [AccessExpression deleted_access] ->
PulseOperations.invalidate PulseOperations.invalidate
(PulseTrace.Immediate {imm= PulseDomain.Invalidation.CppDelete deleted_access; location}) (PulseDomain.InterprocAction.Immediate
{imm= PulseDomain.Invalidation.CppDelete deleted_access; location})
location deleted_access astate location deleted_access astate
>>| List.return >>| List.return
| _ -> | _ ->
@ -61,7 +63,7 @@ module Cplusplus = struct
Ok astate ) Ok astate )
>>| fun astate -> >>| fun astate ->
[ PulseOperations.havoc_var [ PulseOperations.havoc_var
[PulseTrace.Call {f= `Model "<lambda>"; actuals; location}] [PulseDomain.ValueHistory.Call {f= `Model "<lambda>"; actuals; location}]
ret_var astate ] ret_var astate ]
@ -70,7 +72,7 @@ module Cplusplus = struct
let read_all args astate = let read_all args astate =
PulseOperations.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate PulseOperations.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate
in in
let crumb = PulseTrace.Call {f= `Model "<placement new>"; actuals; location} in let crumb = PulseDomain.ValueHistory.Call {f= `Model "<placement new>"; actuals; location} in
match List.rev actuals with match List.rev actuals with
| HilExp.AccessExpression expr :: other_actuals -> | HilExp.AccessExpression expr :: other_actuals ->
PulseOperations.read location expr astate PulseOperations.read location expr astate
@ -104,7 +106,8 @@ module StdVector = struct
let array_address = to_internal_array vector in let array_address = to_internal_array vector in
let array = deref_internal_array vector in let array = deref_internal_array vector in
let invalidation = let invalidation =
PulseTrace.Immediate {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location} PulseDomain.InterprocAction.Immediate
{imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location}
in in
PulseOperations.invalidate_array_elements invalidation location array astate PulseOperations.invalidate_array_elements invalidation location array astate
>>= PulseOperations.invalidate invalidation location array >>= PulseOperations.invalidate invalidation location array
@ -116,7 +119,7 @@ module StdVector = struct
match actuals with match actuals with
| AccessExpression vector :: _ -> | AccessExpression vector :: _ ->
let crumb = let crumb =
PulseTrace.Call PulseDomain.ValueHistory.Call
{ f= { f=
`Model `Model
(Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f) (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f)
@ -130,7 +133,7 @@ module StdVector = struct
let at : model = let at : model =
fun location ~ret ~actuals astate -> fun location ~ret ~actuals astate ->
let crumb = PulseTrace.Call {f= `Model "std::vector::at"; actuals; location} in let crumb = PulseDomain.ValueHistory.Call {f= `Model "std::vector::at"; actuals; location} in
match actuals with match actuals with
| [AccessExpression vector_access_expr; index_exp] -> | [AccessExpression vector_access_expr; index_exp] ->
PulseOperations.read location PulseOperations.read location
@ -150,7 +153,9 @@ module StdVector = struct
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
match actuals with match actuals with
| [AccessExpression vector; _value] -> | [AccessExpression vector; _value] ->
let crumb = PulseTrace.Call {f= `Model "std::vector::reserve"; actuals; location} in let crumb =
PulseDomain.ValueHistory.Call {f= `Model "std::vector::reserve"; actuals; location}
in
reallocate_internal_array [crumb] vector Reserve location astate reallocate_internal_array [crumb] vector Reserve location astate
>>= PulseOperations.StdVector.mark_reserved location vector >>= PulseOperations.StdVector.mark_reserved location vector
>>| List.return >>| List.return
@ -162,7 +167,9 @@ module StdVector = struct
fun location ~ret:_ ~actuals astate -> fun location ~ret:_ ~actuals astate ->
match actuals with match actuals with
| [AccessExpression vector; _value] -> | [AccessExpression vector; _value] ->
let crumb = PulseTrace.Call {f= `Model "std::vector::push_back"; actuals; location} in let crumb =
PulseDomain.ValueHistory.Call {f= `Model "std::vector::push_back"; actuals; location}
in
PulseOperations.StdVector.is_reserved location vector astate PulseOperations.StdVector.is_reserved location vector astate
>>= fun (astate, is_reserved) -> >>= fun (astate, is_reserved) ->
if is_reserved then if is_reserved then

@ -9,6 +9,8 @@ module L = Logging
module AbstractAddress = PulseDomain.AbstractAddress module AbstractAddress = PulseDomain.AbstractAddress
module Attribute = PulseDomain.Attribute module Attribute = PulseDomain.Attribute
module Attributes = PulseDomain.Attributes module Attributes = PulseDomain.Attributes
module InterprocAction = PulseDomain.InterprocAction
module ValueHistory = PulseDomain.ValueHistory
module Memory = PulseAbductiveDomain.Memory module Memory = PulseAbductiveDomain.Memory
module Stack = PulseAbductiveDomain.Stack module Stack = PulseAbductiveDomain.Stack
open Result.Monad_infix open Result.Monad_infix
@ -26,11 +28,11 @@ type t = PulseAbductiveDomain.t
type 'a access_result = ('a, PulseDiagnostic.t) result type 'a access_result = ('a, PulseDiagnostic.t) result
(** Check that the address is not known to be invalid *) (** Check that the address is not known to be invalid *)
let check_addr_access access action (address, breadcrumbs) astate = let check_addr_access access action (address, history) astate =
Memory.check_valid action address astate Memory.check_valid action address astate
|> Result.map_error ~f:(fun invalidated_by -> |> Result.map_error ~f:(fun invalidated_by ->
PulseDiagnostic.AccessToInvalidAddress PulseDiagnostic.AccessToInvalidAddress
{access; invalidated_by; accessed_by= {action; breadcrumbs}} ) {access; invalidated_by; accessed_by= {action; history}} )
(** Walk the heap starting from [addr] and following [path]. Stop either at the element before last (** Walk the heap starting from [addr] and following [path]. Stop either at the element before last
@ -127,8 +129,8 @@ and walk_access_expr ~on_last astate access_expr location =
let astate, (addr, init_loc_opt) = Stack.materialize access_var astate in let astate, (addr, init_loc_opt) = Stack.materialize access_var astate in
let trace = let trace =
Option.map init_loc_opt ~f:(fun init_loc -> Option.map init_loc_opt ~f:(fun init_loc ->
if Var.is_cpp_temporary access_var then PulseTrace.CppTemporaryCreated init_loc if Var.is_cpp_temporary access_var then ValueHistory.CppTemporaryCreated init_loc
else PulseTrace.VariableDeclaration init_loc ) else ValueHistory.VariableDeclaration init_loc )
|> Option.to_list |> Option.to_list
in in
(astate, (addr, trace)) (astate, (addr, trace))
@ -137,7 +139,7 @@ and walk_access_expr ~on_last astate access_expr location =
| [HilExp.Access.TakeAddress] -> | [HilExp.Access.TakeAddress] ->
Ok (astate, base_addr_trace) Ok (astate, base_addr_trace)
| _ -> | _ ->
let action = PulseTrace.Immediate {imm= access_expr; location} in let action = InterprocAction.Immediate {imm= access_expr; location} in
walk walk
(HilExp.AccessExpression.base base) (HilExp.AccessExpression.base base)
~dereference_to_ignore action ~on_last base_addr_trace ~dereference_to_ignore action ~on_last base_addr_trace
@ -220,7 +222,7 @@ let invalidate_array_elements cause location access_expr astate =
edges astate edges astate
let check_address_escape escape_location proc_desc address trace astate = let check_address_escape escape_location proc_desc address history astate =
let check_address_of_cpp_temporary () = let check_address_of_cpp_temporary () =
Memory.find_opt address astate Memory.find_opt address astate
|> Option.fold_result ~init:() ~f:(fun () (_, attrs) -> |> Option.fold_result ~init:() ~f:(fun () (_, attrs) ->
@ -229,7 +231,7 @@ let check_address_escape escape_location proc_desc address trace astate =
| Attribute.AddressOfCppTemporary (variable, _) -> | Attribute.AddressOfCppTemporary (variable, _) ->
Error Error
(PulseDiagnostic.StackVariableAddressEscape (PulseDiagnostic.StackVariableAddressEscape
{variable; location= escape_location; trace}) {variable; location= escape_location; history})
| _ -> | _ ->
Ok () ) ) Ok () ) )
in in
@ -246,7 +248,8 @@ let check_address_escape escape_location proc_desc address trace astate =
L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable
AbstractAddress.pp address ; AbstractAddress.pp address ;
Error Error
(PulseDiagnostic.StackVariableAddressEscape {variable; location= escape_location; trace}) ) (PulseDiagnostic.StackVariableAddressEscape
{variable; location= escape_location; history}) )
else Ok () ) else Ok () )
in in
check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate check_address_of_cpp_temporary () >>= check_address_of_stack_variable >>| fun () -> astate
@ -323,7 +326,7 @@ module Closures = struct
let write location access_expr pname captured astate = let write location access_expr pname captured astate =
let closure_addr = AbstractAddress.mk_fresh () in let closure_addr = AbstractAddress.mk_fresh () in
write location access_expr write location access_expr
(closure_addr, [PulseTrace.Assignment {lhs= access_expr; location}]) (closure_addr, [ValueHistory.Assignment {lhs= access_expr; location}])
astate astate
>>| fun astate -> >>| fun astate ->
let fake_capture_edges = mk_capture_edges captured in let fake_capture_edges = mk_capture_edges captured in
@ -338,7 +341,7 @@ module Closures = struct
read location access_expr astate read location access_expr astate
>>= fun (astate, (address, trace)) -> >>= fun (astate, (address, trace)) ->
let new_trace = let new_trace =
PulseTrace.Capture {captured_as; captured= captured_access_expr; location} :: trace ValueHistory.Capture {captured_as; captured= captured_access_expr; location} :: trace
in in
Ok (astate, (address, new_trace) :: captured) Ok (astate, (address, new_trace) :: captured)
| _ -> | _ ->

@ -41,35 +41,35 @@ val read :
Location.t Location.t
-> HilExp.AccessExpression.t -> HilExp.AccessExpression.t
-> t -> t
-> (t * (AbstractAddress.t * PulseTrace.breadcrumbs)) access_result -> (t * (AbstractAddress.t * PulseDomain.ValueHistory.t)) access_result
val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result
val havoc_var : PulseTrace.breadcrumbs -> Var.t -> t -> t val havoc_var : PulseDomain.ValueHistory.t -> Var.t -> t -> t
val havoc : val havoc :
PulseTrace.breadcrumbs -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result PulseDomain.ValueHistory.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result
val realloc_var : Var.t -> Location.t -> t -> t val realloc_var : Var.t -> Location.t -> t -> t
val write_var : Var.t -> AbstractAddress.t * PulseTrace.breadcrumbs -> t -> t val write_var : Var.t -> AbstractAddress.t * PulseDomain.ValueHistory.t -> t -> t
val write : val write :
Location.t Location.t
-> HilExp.AccessExpression.t -> HilExp.AccessExpression.t
-> AbstractAddress.t * PulseTrace.breadcrumbs -> AbstractAddress.t * PulseDomain.ValueHistory.t
-> t -> t
-> t access_result -> t access_result
val invalidate : val invalidate :
PulseDomain.Invalidation.t PulseTrace.action PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-> Location.t -> Location.t
-> HilExp.AccessExpression.t -> HilExp.AccessExpression.t
-> t -> t
-> t access_result -> t access_result
val invalidate_array_elements : val invalidate_array_elements :
PulseDomain.Invalidation.t PulseTrace.action PulseDomain.Invalidation.t PulseDomain.InterprocAction.t
-> Location.t -> Location.t
-> HilExp.AccessExpression.t -> HilExp.AccessExpression.t
-> t -> t
@ -78,7 +78,12 @@ val invalidate_array_elements :
val remove_vars : Var.t list -> t -> t val remove_vars : Var.t list -> t -> t
val check_address_escape : val check_address_escape :
Location.t -> Procdesc.t -> AbstractAddress.t -> PulseTrace.breadcrumbs -> t -> t access_result Location.t
-> Procdesc.t
-> AbstractAddress.t
-> PulseDomain.ValueHistory.t
-> t
-> t access_result
module Interproc : sig module Interproc : sig
val call : val call :

@ -1,143 +0,0 @@
(*
* 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
type breadcrumb =
| VariableDeclaration of Location.t
| CppTemporaryCreated of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
| Capture of
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t
; location: Location.t }
| Call of
{ f: [`HilCall of HilInstr.call | `Model of string]
; actuals: HilExp.t list
; location: Location.t }
[@@deriving compare]
let pp_breadcrumb_no_location fmt = function
| VariableDeclaration _ ->
F.pp_print_string fmt "variable declared"
| CppTemporaryCreated _ ->
F.pp_print_string fmt "C++ temporary created"
| Capture {captured_as; captured; location= _} ->
F.fprintf fmt "`%a` captured as `%a`" HilExp.AccessExpression.pp captured AccessPath.pp_base
captured_as
| Assignment {lhs; location= _} ->
F.fprintf fmt "assigned to `%a`" HilExp.AccessExpression.pp lhs
| Call {f; actuals; location= _} ->
let pp_f fmt = function
| `HilCall call ->
F.fprintf fmt "%a" HilInstr.pp_call call
| `Model model ->
F.pp_print_string fmt model
in
F.fprintf fmt "returned from call to `%a(%a)`" pp_f f (Pp.seq ~sep:"," HilExp.pp) actuals
let location_of_breadcrumb = function
| VariableDeclaration location
| CppTemporaryCreated location
| Assignment {location}
| Capture {location}
| Call {location} ->
location
let pp_breadcrumb fmt crumb =
F.fprintf fmt "%a at %a" pp_breadcrumb_no_location crumb Location.pp_line
(location_of_breadcrumb crumb)
let errlog_trace_elem_of_breadcrumb ~nesting crumb =
let location = location_of_breadcrumb crumb in
let description = F.asprintf "%a" pp_breadcrumb_no_location crumb in
let tags = [] in
Errlog.make_trace_element nesting location description tags
type breadcrumbs = breadcrumb list [@@deriving compare]
let pp_breadcrumbs f breadcrumbs = Pp.seq ~print_env:Pp.text_break pp_breadcrumb f breadcrumbs
let add_errlog_of_breadcrumbs ~nesting breadcrumbs errlog =
List.rev_map_append ~f:(errlog_trace_elem_of_breadcrumb ~nesting) breadcrumbs errlog
let start_location_of_breadcrumbs = function
| [] ->
None
| crumb :: _ ->
Some (location_of_breadcrumb crumb)
type 'a action =
| Immediate of {imm: 'a; location: Location.t}
| ViaCall of {action: 'a action; proc_name: Typ.Procname.t; location: Location.t}
[@@deriving compare]
let rec immediate_of_action = function
| Immediate {imm; _} ->
imm
| ViaCall {action; _} ->
immediate_of_action action
let pp_action pp_immediate fmt = function
| Immediate {imm; _} ->
pp_immediate fmt imm
| ViaCall {proc_name; action; _} ->
F.fprintf fmt "%a in call to `%a`" pp_immediate (immediate_of_action action)
Typ.Procname.describe proc_name
let add_errlog_of_action ~nesting pp_immediate action errlog =
let rec aux ~nesting rev_errlog action =
match action with
| Immediate {imm; location} ->
let rev_errlog =
Errlog.make_trace_element nesting location (F.asprintf "%a here" pp_immediate imm) []
:: rev_errlog
in
List.rev_append rev_errlog errlog
| ViaCall {action; proc_name; location} ->
aux ~nesting:(nesting + 1)
( Errlog.make_trace_element nesting location
(F.asprintf "when calling `%a` here" Typ.Procname.describe proc_name)
[]
:: rev_errlog )
action
in
aux ~nesting [] action
let outer_location_of_action = function Immediate {location} | ViaCall {location} -> location
type 'a t = {action: 'a action; breadcrumbs: breadcrumbs} [@@deriving compare]
let pp pp_immediate f {action; _} = pp_action pp_immediate f action
let add_errlog_header ~title location errlog =
let depth = 0 in
let tags = [] in
Errlog.make_trace_element depth location title tags :: errlog
let add_to_errlog ~header pp_immediate trace errlog =
let start_location =
match start_location_of_breadcrumbs trace.breadcrumbs with
| Some location ->
location
| None ->
outer_location_of_action trace.action
in
add_errlog_header ~title:header start_location
@@ add_errlog_of_breadcrumbs ~nesting:1 trace.breadcrumbs
@@ add_errlog_of_action ~nesting:1 pp_immediate trace.action
@@ errlog

@ -1,51 +0,0 @@
(*
* 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
type breadcrumb =
| VariableDeclaration of Location.t
| CppTemporaryCreated of Location.t
| Assignment of {lhs: HilExp.AccessExpression.t; location: Location.t}
| Capture of
{ captured_as: AccessPath.base
; captured: HilExp.AccessExpression.t
; location: Location.t }
| Call of
{ f: [`HilCall of HilInstr.call | `Model of string]
; actuals: HilExp.t list
; location: Location.t }
type breadcrumbs = breadcrumb list [@@deriving compare]
val pp_breadcrumbs : F.formatter -> breadcrumbs -> unit
val add_errlog_of_breadcrumbs :
nesting:int -> breadcrumbs -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list
type 'a action =
| Immediate of {imm: 'a; location: Location.t}
| ViaCall of {action: 'a action; proc_name: Typ.Procname.t; location: Location.t}
[@@deriving compare]
val pp_action : (F.formatter -> 'a -> unit) -> F.formatter -> 'a action -> unit
val immediate_of_action : 'a action -> 'a
val outer_location_of_action : 'a action -> Location.t
type 'a t = {action: 'a action; breadcrumbs: breadcrumbs} [@@deriving compare]
val pp : (F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit
val add_to_errlog :
header:string
-> (F.formatter -> 'a -> unit)
-> 'a t
-> Errlog.loc_trace_elem list
-> Errlog.loc_trace_elem list
Loading…
Cancel
Save