diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index a6f972cde..58a3f5d6b 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -9,6 +9,8 @@ module F = Format module L = Logging open Result.Monad_infix 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 *) struct @@ -52,7 +54,7 @@ module PulseTransferFunctions = struct let rec exec_assign summary (lhs_access : HilExp.AccessExpression.t) (rhs_exp : HilExp.t) loc astate = (* 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 | AccessExpression rhs_access -> ( PulseOperations.read loc rhs_access astate @@ -80,7 +82,7 @@ module PulseTransferFunctions = struct let read_all args astate = PulseOperations.read_all call_loc (List.concat_map args ~f:HilExp.get_access_exprs) astate 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 | Direct callee_pname when Typ.Procname.is_constructor callee_pname -> ( L.d_printfln "constructor call detected@." ; @@ -152,7 +154,7 @@ module PulseTransferFunctions = struct (* invalidate both [&x] and [x]: reading either is now forbidden *) let invalidate pvar typ access astate = PulseOperations.invalidate - (PulseTrace.Immediate {imm= GoneOutOfScope (pvar, typ); location= call_loc}) + (InterprocAction.Immediate {imm= GoneOutOfScope (pvar, typ); location= call_loc}) call_loc access astate in let out_of_scope_base = HilExp.AccessExpression.base (Var.of_pvar pvar, typ) in diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index ec3268efe..aa4f03599 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -356,9 +356,10 @@ module PrePost = struct [call_state.astate] starting from address [addr_caller]. Report an error if some invalid addresses are traversed in the process. *) 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 = - PulseTrace.ViaCall {action; proc_name= callee_proc_name; location= call_location} + PulseDomain.InterprocAction.ViaCall + {action; proc_name= callee_proc_name; location= call_location} in match visit call_state ~addr_callee:addr_pre ~addr_caller with | `AlreadyVisited, call_state -> @@ -374,7 +375,7 @@ module PrePost = struct | Error invalidated_by -> Error (PulseDiagnostic.AccessToInvalidAddress - {access= access_expr; invalidated_by; accessed_by= {action; breadcrumbs}}) + {access= access_expr; invalidated_by; accessed_by= {action; history}}) | Ok astate -> let call_state = {call_state with astate} in Container.fold_result @@ -391,7 +392,7 @@ module PrePost = struct |> Option.value ~default:access_expr in 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 ) @@ -456,7 +457,8 @@ module PrePost = struct 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 -> 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 let access_expr = HilExp.AccessExpression.base (var, Typ.void) in materialize_pre_from_address callee_proc_name call_location access_expr @@ -521,8 +523,8 @@ module PrePost = struct match (attr : PulseDomain.Attribute.t) with | Invalid trace -> PulseDomain.Attribute.Invalid - { action= PulseTrace.ViaCall {action= trace.action; proc_name; location} - ; breadcrumbs= trace.breadcrumbs } + { action= PulseDomain.InterprocAction.ViaCall {action= trace.action; proc_name; location} + ; history= trace.history } | MustBeValid _ | AddressOfCppTemporary (_, _) | Closure _ | StdVectorReserve -> attr @@ -580,7 +582,7 @@ module PrePost = struct let addr_curr, subst = subst_find_or_new subst addr_callee in ( subst , ( addr_curr - , PulseTrace.Call + , PulseDomain.ValueHistory.Call {f= `HilCall (Direct callee_proc_name); actuals= [ (* TODO *) ]; location= call_loc} :: trace_post ) ) ) in diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 30312e980..b19dc7e7d 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -43,18 +43,18 @@ module Memory : sig val add_edge : AbstractAddress.t -> Access.t -> PulseDomain.AddrTracePair.t -> t -> t val check_valid : - HilExp.AccessExpression.t PulseTrace.action + HilExp.AccessExpression.t PulseDomain.InterprocAction.t -> AbstractAddress.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 set_cell : AbstractAddress.t -> PulseDomain.Memory.cell -> t -> t val invalidate : - AbstractAddress.t * PulseTrace.breadcrumbs - -> PulseDomain.Invalidation.t PulseTrace.action + AbstractAddress.t * PulseDomain.ValueHistory.t + -> PulseDomain.Invalidation.t PulseDomain.InterprocAction.t -> t -> t @@ -79,8 +79,9 @@ module PrePost : sig -> Location.t -> t -> formals:Var.t list - -> ret:AbstractAddress.t * PulseTrace.breadcrumbs - -> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseTrace.breadcrumbs) option list + -> ret:AbstractAddress.t * PulseDomain.ValueHistory.t + -> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseDomain.ValueHistory.t) option + list -> domain_t -> (domain_t, PulseDiagnostic.t) result end diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 85e45cc6d..15b11d670 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -11,16 +11,16 @@ module F = Format type t = | AccessToInvalidAddress of { access: HilExp.AccessExpression.t - ; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t - ; accessed_by: HilExp.AccessExpression.t PulseTrace.t } + ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t + ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t } | StackVariableAddressEscape of { variable: Var.t - ; trace: PulseTrace.breadcrumbs + ; history: PulseDomain.ValueHistory.t ; location: Location.t } let get_location = function | AccessToInvalidAddress {accessed_by} -> - PulseTrace.outer_location_of_action accessed_by.action + PulseDomain.InterprocAction.to_outer_location accessed_by.action | StackVariableAddressEscape {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 "`x->f` accesses `x`, which was invalidated at line 42 by `delete`" *) - let pp_access_trace invalidated f trace = - match trace.PulseTrace.action with + let pp_access_trace invalidated f (trace : HilExp.AccessExpression.t PulseDomain.Trace.t) = + match trace.action with | Immediate {imm= access; _} -> ( match HilExp.AccessExpression.to_source_string access with | Some access_s when HilExp.AccessExpression.equal access invalidated -> @@ -65,7 +65,8 @@ let get_message = function | ViaCall {action; proc_name; _} -> ( let access_and_invalidated_s = 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 ) with | Some access_s, Some invalidated_s -> @@ -84,17 +85,19 @@ let get_message = function proc_name HilExp.AccessExpression.pp invalidated ) in let pp_invalidation_trace line f trace = - match trace.PulseTrace.action with + match trace.PulseDomain.Trace.action with | Immediate {imm= invalidation; _} -> F.fprintf f "%a on line %d" PulseDomain.Invalidation.describe invalidation line | ViaCall {action; proc_name; _} -> F.fprintf f "%a on line %d indirectly during the call to `%a`" PulseDomain.Invalidation.describe - (PulseTrace.immediate_of_action action) + (PulseDomain.InterprocAction.get_immediate action) line Typ.Procname.describe proc_name in 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 in let invalidation_line = line_of_trace invalidated_by in @@ -111,16 +114,18 @@ let get_message = function let get_trace = function | 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 -> F.fprintf f "memory %a" PulseDomain.Invalidation.describe invalidation ) invalidated_by - @@ PulseTrace.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) + @@ PulseDomain.Trace.add_to_errlog ~header:"use-after-lifetime part of the trace starts here" + (fun f (access : HilExp.AccessExpression.t) -> + F.fprintf f "invalid access to `%a`" HilExp.AccessExpression.pp + (access :> HilExp.AccessExpression.t) ) accessed_by @@ [] - | StackVariableAddressEscape {trace; location; _} -> - PulseTrace.add_errlog_of_breadcrumbs ~nesting:0 trace + | StackVariableAddressEscape {history; location; _} -> + PulseDomain.ValueHistory.add_to_errlog ~nesting:0 history @@ let nesting = 0 in [Errlog.make_trace_element nesting location "returned here" []] @@ -128,7 +133,7 @@ let get_trace = function let get_issue_type = function | AccessToInvalidAddress {invalidated_by} -> - PulseTrace.immediate_of_action invalidated_by.action + PulseDomain.InterprocAction.get_immediate invalidated_by.action |> PulseDomain.Invalidation.issue_type_of_cause | StackVariableAddressEscape _ -> IssueType.stack_variable_address_escape diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 8b043868d..dc9343a4d 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -11,11 +11,11 @@ open! IStd type t = | AccessToInvalidAddress of { access: HilExp.AccessExpression.t - ; invalidated_by: PulseDomain.Invalidation.t PulseTrace.t - ; accessed_by: HilExp.AccessExpression.t PulseTrace.t } + ; invalidated_by: PulseDomain.Invalidation.t PulseDomain.Trace.t + ; accessed_by: HilExp.AccessExpression.t PulseDomain.Trace.t } | StackVariableAddressEscape of { variable: Var.t - ; trace: PulseTrace.breadcrumbs + ; history: PulseDomain.ValueHistory.t ; location: Location.t } val get_message : t -> string diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index 8548b2110..c28d8e44c 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -96,12 +96,147 @@ module Invalidation = struct F.fprintf f "StdVector(%a)" describe invalidation 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 addresses. Otherwise they become a pain to handle when comparing memory states. *) module Attribute = struct type t = - | Invalid of Invalidation.t PulseTrace.t - | MustBeValid of HilExp.AccessExpression.t PulseTrace.action + | Invalid of Invalidation.t Trace.t + | MustBeValid of HilExp.AccessExpression.t InterprocAction.t | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t | StdVectorReserve @@ -114,7 +249,7 @@ module Attribute = struct let invalid_rank = Variants.to_rank (Invalid - {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; breadcrumbs= []}) + {action= Immediate {imm= Invalidation.Nullptr; location= Location.dummy}; history= []}) let must_be_valid_rank = @@ -131,12 +266,12 @@ module Attribute = struct let pp f = function | Invalid invalidation -> - (PulseTrace.pp Invalidation.pp) f invalidation + (Trace.pp Invalidation.pp) f invalidation | MustBeValid action -> F.fprintf f "MustBeValid (read by %a @ %a)" - (PulseTrace.pp_action HilExp.AccessExpression.pp) + (InterprocAction.pp HilExp.AccessExpression.pp) action Location.pp - (PulseTrace.outer_location_of_action action) + (InterprocAction.to_outer_location action) | AddressOfCppTemporary (var, location_opt) -> F.fprintf f "&%a (%a)" Var.pp var (Pp.option Location.pp) location_opt | Closure pname -> @@ -215,11 +350,11 @@ module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress) (* {3 Heap domain } *) module AddrTracePair = struct - type t = AbstractAddress.t * PulseTrace.breadcrumbs [@@deriving compare] + type t = AbstractAddress.t * ValueHistory.t [@@deriving compare] let pp f addr_trace = 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) end @@ -262,10 +397,9 @@ module Memory : sig val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t - val invalidate : - AbstractAddress.t * PulseTrace.breadcrumbs -> Invalidation.t PulseTrace.action -> t -> t + val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> 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 @@ -328,8 +462,8 @@ end = struct add_attributes address (Attributes.singleton attribute) memory - let invalidate (address, breadcrumbs) invalidation memory = - add_attribute address (Attribute.Invalid {action= invalidation; breadcrumbs}) memory + let invalidate (address, history) invalidation memory = + add_attribute address (Attribute.Invalid {action= invalidation; history}) memory let check_valid address memory = diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index 229267b35..89bacd5a2 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -35,10 +35,52 @@ module Invalidation : sig val describe : Format.formatter -> t -> unit 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 type t = - | Invalid of Invalidation.t PulseTrace.t - | MustBeValid of HilExp.AccessExpression.t PulseTrace.action + | Invalid of Invalidation.t Trace.t + | MustBeValid of HilExp.AccessExpression.t InterprocAction.t | AddressOfCppTemporary of Var.t * Location.t option | Closure of Typ.Procname.t | StdVectorReserve @@ -48,7 +90,7 @@ end module Attributes : sig 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 module AbstractAddress : sig @@ -85,7 +127,7 @@ module Stack : sig end module AddrTracePair : sig - type t = AbstractAddress.t * PulseTrace.breadcrumbs [@@deriving compare] + type t = AbstractAddress.t * ValueHistory.t [@@deriving compare] end module Memory : sig @@ -120,10 +162,9 @@ module Memory : sig val add_attributes : AbstractAddress.t -> Attributes.t -> t -> t - val invalidate : - AbstractAddress.t * PulseTrace.breadcrumbs -> Invalidation.t PulseTrace.action -> t -> t + val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t InterprocAction.t -> 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 diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 09bac586e..30ce94ea2 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -26,7 +26,8 @@ module C = struct match actuals with | [AccessExpression deleted_access] -> 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 >>| List.return | _ -> @@ -41,7 +42,8 @@ module Cplusplus = struct match actuals with | [AccessExpression deleted_access] -> 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 >>| List.return | _ -> @@ -61,7 +63,7 @@ module Cplusplus = struct Ok astate ) >>| fun astate -> [ PulseOperations.havoc_var - [PulseTrace.Call {f= `Model ""; actuals; location}] + [PulseDomain.ValueHistory.Call {f= `Model ""; actuals; location}] ret_var astate ] @@ -70,7 +72,7 @@ module Cplusplus = struct let read_all args astate = PulseOperations.read_all location (List.concat_map args ~f:HilExp.get_access_exprs) astate in - let crumb = PulseTrace.Call {f= `Model ""; actuals; location} in + let crumb = PulseDomain.ValueHistory.Call {f= `Model ""; actuals; location} in match List.rev actuals with | HilExp.AccessExpression expr :: other_actuals -> PulseOperations.read location expr astate @@ -104,7 +106,8 @@ module StdVector = struct let array_address = to_internal_array vector in let array = deref_internal_array vector in let invalidation = - PulseTrace.Immediate {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location} + PulseDomain.InterprocAction.Immediate + {imm= PulseDomain.Invalidation.StdVector (vector_f, vector); location} in PulseOperations.invalidate_array_elements invalidation location array astate >>= PulseOperations.invalidate invalidation location array @@ -116,7 +119,7 @@ module StdVector = struct match actuals with | AccessExpression vector :: _ -> let crumb = - PulseTrace.Call + PulseDomain.ValueHistory.Call { f= `Model (Format.asprintf "%a" PulseDomain.Invalidation.pp_std_vector_function vector_f) @@ -130,7 +133,7 @@ module StdVector = struct let at : model = 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 | [AccessExpression vector_access_expr; index_exp] -> PulseOperations.read location @@ -150,7 +153,9 @@ module StdVector = struct fun location ~ret:_ ~actuals astate -> match actuals with | [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 >>= PulseOperations.StdVector.mark_reserved location vector >>| List.return @@ -162,7 +167,9 @@ module StdVector = struct fun location ~ret:_ ~actuals astate -> match actuals with | [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 >>= fun (astate, is_reserved) -> if is_reserved then diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index 44ac155fe..e9e668091 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -9,6 +9,8 @@ module L = Logging module AbstractAddress = PulseDomain.AbstractAddress module Attribute = PulseDomain.Attribute module Attributes = PulseDomain.Attributes +module InterprocAction = PulseDomain.InterprocAction +module ValueHistory = PulseDomain.ValueHistory module Memory = PulseAbductiveDomain.Memory module Stack = PulseAbductiveDomain.Stack open Result.Monad_infix @@ -26,11 +28,11 @@ type t = PulseAbductiveDomain.t type 'a access_result = ('a, PulseDiagnostic.t) result (** 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 |> Result.map_error ~f:(fun invalidated_by -> 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 @@ -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 trace = Option.map init_loc_opt ~f:(fun init_loc -> - if Var.is_cpp_temporary access_var then PulseTrace.CppTemporaryCreated init_loc - else PulseTrace.VariableDeclaration init_loc ) + if Var.is_cpp_temporary access_var then ValueHistory.CppTemporaryCreated init_loc + else ValueHistory.VariableDeclaration init_loc ) |> Option.to_list in (astate, (addr, trace)) @@ -137,7 +139,7 @@ and walk_access_expr ~on_last astate access_expr location = | [HilExp.Access.TakeAddress] -> Ok (astate, base_addr_trace) | _ -> - let action = PulseTrace.Immediate {imm= access_expr; location} in + let action = InterprocAction.Immediate {imm= access_expr; location} in walk (HilExp.AccessExpression.base base) ~dereference_to_ignore action ~on_last base_addr_trace @@ -220,7 +222,7 @@ let invalidate_array_elements cause location access_expr 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 () = Memory.find_opt address astate |> 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, _) -> Error (PulseDiagnostic.StackVariableAddressEscape - {variable; location= escape_location; trace}) + {variable; location= escape_location; history}) | _ -> Ok () ) ) 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 AbstractAddress.pp address ; Error - (PulseDiagnostic.StackVariableAddressEscape {variable; location= escape_location; trace}) ) + (PulseDiagnostic.StackVariableAddressEscape + {variable; location= escape_location; history}) ) else Ok () ) in 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 closure_addr = AbstractAddress.mk_fresh () in write location access_expr - (closure_addr, [PulseTrace.Assignment {lhs= access_expr; location}]) + (closure_addr, [ValueHistory.Assignment {lhs= access_expr; location}]) astate >>| fun astate -> let fake_capture_edges = mk_capture_edges captured in @@ -338,7 +341,7 @@ module Closures = struct read location access_expr astate >>= fun (astate, (address, 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 Ok (astate, (address, new_trace) :: captured) | _ -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 5b1a8c9be..8084416ab 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -41,35 +41,35 @@ val read : Location.t -> HilExp.AccessExpression.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 havoc_var : PulseTrace.breadcrumbs -> Var.t -> t -> t +val havoc_var : PulseDomain.ValueHistory.t -> Var.t -> t -> t 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 write_var : Var.t -> AbstractAddress.t * PulseTrace.breadcrumbs -> t -> t +val write_var : Var.t -> AbstractAddress.t * PulseDomain.ValueHistory.t -> t -> t val write : Location.t -> HilExp.AccessExpression.t - -> AbstractAddress.t * PulseTrace.breadcrumbs + -> AbstractAddress.t * PulseDomain.ValueHistory.t -> t -> t access_result val invalidate : - PulseDomain.Invalidation.t PulseTrace.action + PulseDomain.Invalidation.t PulseDomain.InterprocAction.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result val invalidate_array_elements : - PulseDomain.Invalidation.t PulseTrace.action + PulseDomain.Invalidation.t PulseDomain.InterprocAction.t -> Location.t -> HilExp.AccessExpression.t -> t @@ -78,7 +78,12 @@ val invalidate_array_elements : val remove_vars : Var.t list -> t -> t 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 val call : diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml deleted file mode 100644 index 23ff30598..000000000 --- a/infer/src/pulse/PulseTrace.ml +++ /dev/null @@ -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 diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli deleted file mode 100644 index e2e03f8f6..000000000 --- a/infer/src/pulse/PulseTrace.mli +++ /dev/null @@ -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