diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 56b71ff64..5c013c2cd 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -75,8 +75,8 @@ module PrePost : sig -> Location.t -> t -> formals:Var.t list - -> ret:AbstractAddress.t * PulseTrace.t - -> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseTrace.t) option list + -> ret:AbstractAddress.t * PulseTrace.breadcrumbs + -> actuals:(AbstractAddress.t * HilExp.AccessExpression.t * PulseTrace.breadcrumbs) 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 1959c8f7e..824d1e73b 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -13,8 +13,11 @@ type t = { access: HilExp.AccessExpression.t ; invalidated_by: PulseInvalidation.t PulseTrace.action ; accessed_by: HilExp.AccessExpression.t PulseTrace.action - ; trace: PulseTrace.t } - | StackVariableAddressEscape of {variable: Var.t; trace: PulseTrace.t; location: Location.t} + ; trace: PulseTrace.breadcrumbs } + | StackVariableAddressEscape of + { variable: Var.t + ; trace: PulseTrace.breadcrumbs + ; location: Location.t } let describe_access = PulseTrace.pp_action (Pp.in_backticks HilExp.AccessExpression.pp) @@ -78,11 +81,11 @@ let get_trace = function (PulseTrace.outer_location_of_action accessed_by) @@ PulseTrace.add_errlog_of_action ~nesting:1 pp_invalid_access accessed_by @@ add_header_if_some ~title:"trace of how the access expression was constructed starts here" - (PulseTrace.get_start_location trace) - @@ PulseTrace.add_errlog_of_trace ~nesting:1 trace + (PulseTrace.start_location_of_breadcrumbs trace) + @@ PulseTrace.add_errlog_of_breadcrumbs ~nesting:1 trace @@ [] | StackVariableAddressEscape {trace; location; _} -> - PulseTrace.add_errlog_of_trace ~nesting:0 trace + PulseTrace.add_errlog_of_breadcrumbs ~nesting:0 trace @@ let nesting = 0 in [Errlog.make_trace_element nesting location "returned here" []] diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index a324e8289..49783a828 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -13,8 +13,11 @@ type t = { access: HilExp.AccessExpression.t ; invalidated_by: PulseInvalidation.t PulseTrace.action ; accessed_by: HilExp.AccessExpression.t PulseTrace.action - ; trace: PulseTrace.t } - | StackVariableAddressEscape of {variable: Var.t; trace: PulseTrace.t; location: Location.t} + ; trace: PulseTrace.breadcrumbs } + | StackVariableAddressEscape of + { variable: Var.t + ; trace: PulseTrace.breadcrumbs + ; location: Location.t } val get_message : t -> string diff --git a/infer/src/pulse/PulseDomain.ml b/infer/src/pulse/PulseDomain.ml index fe4e8f6b5..60743a3d6 100644 --- a/infer/src/pulse/PulseDomain.ml +++ b/infer/src/pulse/PulseDomain.ml @@ -128,11 +128,11 @@ module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress) (* {3 Heap domain } *) module AddrTracePair = struct - type t = AbstractAddress.t * PulseTrace.t [@@deriving compare] + type t = AbstractAddress.t * PulseTrace.breadcrumbs [@@deriving compare] let pp f addr_trace = if Config.debug_level_analysis >= 3 then - Pp.pair ~fst:AbstractAddress.pp ~snd:PulseTrace.pp f addr_trace + Pp.pair ~fst:AbstractAddress.pp ~snd:PulseTrace.pp_breadcrumbs f addr_trace else AbstractAddress.pp f (fst addr_trace) end diff --git a/infer/src/pulse/PulseDomain.mli b/infer/src/pulse/PulseDomain.mli index b8d7e75a0..59c1e3e0b 100644 --- a/infer/src/pulse/PulseDomain.mli +++ b/infer/src/pulse/PulseDomain.mli @@ -58,7 +58,7 @@ module Stack : sig end module AddrTracePair : sig - type t = AbstractAddress.t * PulseTrace.t [@@deriving compare] + type t = AbstractAddress.t * PulseTrace.breadcrumbs [@@deriving compare] end module Memory : sig diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index 245512e2d..b006825ef 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -41,22 +41,23 @@ val read : Location.t -> HilExp.AccessExpression.t -> t - -> (t * (AbstractAddress.t * PulseTrace.t)) access_result + -> (t * (AbstractAddress.t * PulseTrace.breadcrumbs)) access_result val read_all : Location.t -> HilExp.AccessExpression.t list -> t -> t access_result -val havoc_var : PulseTrace.t -> Var.t -> t -> t +val havoc_var : PulseTrace.breadcrumbs -> Var.t -> t -> t -val havoc : PulseTrace.t -> Location.t -> HilExp.AccessExpression.t -> t -> t access_result +val havoc : + PulseTrace.breadcrumbs -> 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.t -> t -> t +val write_var : Var.t -> AbstractAddress.t * PulseTrace.breadcrumbs -> t -> t val write : Location.t -> HilExp.AccessExpression.t - -> AbstractAddress.t * PulseTrace.t + -> AbstractAddress.t * PulseTrace.breadcrumbs -> t -> t access_result @@ -77,7 +78,7 @@ val invalidate_array_elements : val remove_vars : Var.t list -> t -> t val check_address_escape : - Location.t -> Procdesc.t -> AbstractAddress.t -> PulseTrace.t -> t -> t access_result + Location.t -> Procdesc.t -> AbstractAddress.t -> PulseTrace.breadcrumbs -> t -> t access_result module Interproc : sig val call : diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index 25ec9e987..b83bf9564 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -62,15 +62,20 @@ let errlog_trace_elem_of_breadcrumb ~nesting crumb = Errlog.make_trace_element nesting location description tags -type t = breadcrumb list [@@deriving compare] +type breadcrumbs = breadcrumb list [@@deriving compare] -let pp f trace = Pp.seq ~print_env:Pp.text_break pp_breadcrumb f trace +let pp_breadcrumbs f breadcrumbs = Pp.seq ~print_env:Pp.text_break pp_breadcrumb f breadcrumbs -let add_errlog_of_trace ~nesting trace errlog = - List.rev_map_append ~f:(errlog_trace_elem_of_breadcrumb ~nesting) trace errlog +let add_errlog_of_breadcrumbs ~nesting breadcrumbs errlog = + List.rev_map_append ~f:(errlog_trace_elem_of_breadcrumb ~nesting) breadcrumbs errlog -let get_start_location = function [] -> None | crumb :: _ -> Some (location_of_breadcrumb crumb) +let start_location_of_breadcrumbs = function + | [] -> + None + | crumb :: _ -> + Some (location_of_breadcrumb crumb) + type 'a action = | Immediate of {imm: 'a; location: Location.t} @@ -112,3 +117,4 @@ let add_errlog_of_action ~nesting pp_immediate action errlog = let outer_location_of_action = function Immediate {location} | ViaCall {location} -> location + diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index 6b42482ff..38d1ca13e 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -21,14 +21,14 @@ type breadcrumb = ; actuals: HilExp.t list ; location: Location.t } -type t = breadcrumb list [@@deriving compare] +type breadcrumbs = breadcrumb list [@@deriving compare] -val pp : F.formatter -> t -> unit +val pp_breadcrumbs : F.formatter -> breadcrumbs -> unit -val add_errlog_of_trace : - nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list +val add_errlog_of_breadcrumbs : + nesting:int -> breadcrumbs -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list -val get_start_location : t -> Location.t option +val start_location_of_breadcrumbs : breadcrumbs -> Location.t option type 'a action = | Immediate of {imm: 'a; location: Location.t}