diff --git a/infer/src/checkers/impurityDomain.ml b/infer/src/checkers/impurityDomain.ml index 1139c5cbb..9ade0601c 100644 --- a/infer/src/checkers/impurityDomain.ml +++ b/infer/src/checkers/impurityDomain.ml @@ -8,7 +8,7 @@ open! IStd module F = Format -type trace = WrittenTo of unit PulseTrace.t | Invalid of PulseInvalidation.t PulseTrace.t +type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t) [@@deriving compare] module ModifiedVar = struct @@ -55,14 +55,14 @@ let add_to_errlog ~nesting param_source ModifiedVar.{var; trace_list} errlog = match trace with | WrittenTo access_trace -> PulseTrace.add_to_errlog ~nesting - (fun fmt () -> + ~pp_immediate:(fun fmt -> F.fprintf fmt "%a `%a` modified here" pp_param_source param_source Var.pp var ) access_trace errlog - | Invalid invalidation_trace -> + | Invalid (invalidation, invalidation_trace) -> PulseTrace.add_to_errlog ~nesting - (fun fmt invalid -> + ~pp_immediate:(fun fmt -> F.fprintf fmt "%a `%a` %a here" pp_param_source param_source Var.pp var - PulseInvalidation.describe invalid ) + PulseInvalidation.describe invalidation ) invalidation_trace errlog in let first_trace, rest = trace_list in diff --git a/infer/src/checkers/impurityDomain.mli b/infer/src/checkers/impurityDomain.mli index 4d9c9ffe8..1cc918ee6 100644 --- a/infer/src/checkers/impurityDomain.mli +++ b/infer/src/checkers/impurityDomain.mli @@ -6,7 +6,7 @@ *) open! IStd -type trace = WrittenTo of unit PulseTrace.t | Invalid of PulseInvalidation.t PulseTrace.t +type trace = WrittenTo of PulseTrace.t | Invalid of (PulseInvalidation.t * PulseTrace.t) module ModifiedVar : sig type nonempty_action_type = trace * trace list diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 1ccf1f480..bfb9f21af 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -172,8 +172,7 @@ module Memory = struct let add_edge (addr, history) access new_addr_hist location astate = map_post_heap astate ~f:(fun heap -> BaseMemory.add_edge addr access new_addr_hist heap - |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history})) - ) + |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {location; history})) ) let find_edge_opt address access astate = @@ -229,8 +228,7 @@ module Memory = struct let set_cell (addr, history) cell location astate = map_post_heap astate ~f:(fun heap -> BaseMemory.set_cell addr cell heap - |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {imm= (); location; history})) - ) + |> BaseMemory.add_attribute addr (WrittenTo (Trace.Immediate {location; history})) ) module Edges = BaseMemory.Edges @@ -305,10 +303,9 @@ module PrePost = struct let add_out_of_scope_attribute addr pvar location history heap typ = - let attr = - Attribute.Invalid (Immediate {imm= GoneOutOfScope (pvar, typ); location; history}) - in - BaseMemory.add_attribute addr attr heap + BaseMemory.add_attribute addr + (Invalid (GoneOutOfScope (pvar, typ), Immediate {location; history})) + heap (** invalidate local variables going out of scope *) @@ -613,13 +610,11 @@ module PrePost = struct let add_call_to_attr proc_name call_location caller_history attr = match (attr : Attribute.t) with - | Invalid invalidation -> + | Invalid (invalidation, in_call) -> Attribute.Invalid - (ViaCall - { f= Call proc_name - ; location= call_location - ; history= caller_history - ; in_call= invalidation }) + ( invalidation + , ViaCall {f= Call proc_name; location= call_location; history= caller_history; in_call} + ) | AddressOfCppTemporary (_, _) | AddressOfStackVariable (_, _, _) | Arithmetic _ @@ -668,7 +663,7 @@ module PrePost = struct let callee_trace = match written_to_callee_opt with | None -> - Trace.Immediate {imm= (); location= call_loc; history= []} + Trace.Immediate {location= call_loc; history= []} | Some access_trace -> access_trace in @@ -858,10 +853,10 @@ module PrePost = struct ; history= hist_caller } in Memory.check_valid access_trace addr_caller astate - |> Result.map_error ~f:(fun invalidated_by -> + |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ; - Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by= access_trace} - ) ) ) + Diagnostic.AccessToInvalidAddress + {invalidation; invalidation_trace; access_trace} ) ) ) call_state.subst (Ok call_state.astate) diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index e79a29722..b6087437d 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -59,7 +59,7 @@ module Memory : sig -> t -> t - val check_valid : unit Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t Trace.t) result + val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result val find_opt : AbstractValue.t -> t -> BaseMemory.cell option diff --git a/infer/src/pulse/PulseAttribute.ml b/infer/src/pulse/PulseAttribute.ml index d29107857..81daeba2f 100644 --- a/infer/src/pulse/PulseAttribute.ml +++ b/infer/src/pulse/PulseAttribute.ml @@ -31,21 +31,21 @@ module Attribute = struct | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Arithmetic of Arithmetic.t | Closure of Typ.Procname.t - | Invalid of Invalidation.t Trace.t - | MustBeValid of unit Trace.t + | Invalid of Invalidation.t * Trace.t + | MustBeValid of Trace.t | StdVectorReserve - | WrittenTo of unit Trace.t + | WrittenTo of Trace.t [@@deriving compare, variants] let equal = [%compare.equal: t] let to_rank = Variants.to_rank - let mk_dummy_trace imm = Trace.Immediate {imm; location= Location.dummy; history= []} + let dummy_trace = Trace.Immediate {location= Location.dummy; history= []} let closure_rank = Variants.to_rank (Closure (Typ.Procname.from_string_c_fun "")) - let written_to_rank = Variants.to_rank (WrittenTo (mk_dummy_trace ())) + let written_to_rank = Variants.to_rank (WrittenTo dummy_trace) let address_of_stack_variable_rank = let pname = Typ.Procname.from_string_c_fun "" in @@ -54,16 +54,16 @@ module Attribute = struct Variants.to_rank (AddressOfStackVariable (var, location, [])) - let invalid_rank = Variants.to_rank (Invalid (mk_dummy_trace Invalidation.Nullptr)) + let invalid_rank = Variants.to_rank (Invalid (Invalidation.Nullptr, dummy_trace)) - let must_be_valid_rank = Variants.to_rank (MustBeValid (mk_dummy_trace ())) + let must_be_valid_rank = Variants.to_rank (MustBeValid dummy_trace) let std_vector_reserve_rank = Variants.to_rank StdVectorReserve let const_rank = Variants.to_rank (Arithmetic (Arithmetic.equal_to IntLit.zero)) let pp f attribute = - let pp_string_if_debug string fmt () = + let pp_string_if_debug string fmt = if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string in match attribute with @@ -75,14 +75,16 @@ module Attribute = struct Typ.Procname.pp f pname | Arithmetic phi -> Arithmetic.pp f phi - | Invalid invalidation -> - F.fprintf f "Invalid %a" (Trace.pp Invalidation.pp) invalidation - | MustBeValid action -> - F.fprintf f "MustBeValid %a" (Trace.pp (pp_string_if_debug "access")) action + | Invalid (invalidation, trace) -> + F.fprintf f "Invalid %a" + (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation)) + trace + | MustBeValid trace -> + F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace | StdVectorReserve -> F.pp_print_string f "std::vector::reserve()" - | WrittenTo action -> - F.fprintf f "WrittenTo %a" (Trace.pp (pp_string_if_debug "mutation")) action + | WrittenTo trace -> + F.fprintf f "WrittenTo %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "mutation")) trace end module Attributes = struct @@ -91,8 +93,8 @@ module Attributes = struct let get_invalid attrs = Set.find_rank attrs Attribute.invalid_rank |> Option.map ~f:(fun attr -> - let[@warning "-8"] (Attribute.Invalid invalidation) = attr in - invalidation ) + let[@warning "-8"] (Attribute.Invalid (invalidation, trace)) = attr in + (invalidation, trace) ) let get_must_be_valid attrs = diff --git a/infer/src/pulse/PulseAttribute.mli b/infer/src/pulse/PulseAttribute.mli index f37f2af3a..bd395f0fd 100644 --- a/infer/src/pulse/PulseAttribute.mli +++ b/infer/src/pulse/PulseAttribute.mli @@ -16,10 +16,10 @@ type t = | AddressOfStackVariable of Var.t * Location.t * ValueHistory.t | Arithmetic of Arithmetic.t | Closure of Typ.Procname.t - | Invalid of Invalidation.t Trace.t - | MustBeValid of unit Trace.t + | Invalid of Invalidation.t * Trace.t + | MustBeValid of Trace.t | StdVectorReserve - | WrittenTo of unit Trace.t + | WrittenTo of Trace.t [@@deriving compare] val pp : F.formatter -> t -> unit @@ -33,11 +33,11 @@ module Attributes : sig val get_arithmetic : t -> Arithmetic.t option - val get_invalid : t -> Invalidation.t Trace.t option + val get_invalid : t -> (Invalidation.t * Trace.t) option - val get_must_be_valid : t -> unit Trace.t option + val get_must_be_valid : t -> Trace.t option - val get_written_to : t -> unit Trace.t option + val get_written_to : t -> Trace.t option val is_modified : t -> bool diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index 3d6741274..980bf1207 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/infer/src/pulse/PulseBaseMemory.ml @@ -68,9 +68,8 @@ let add_attribute addr attribute memory = (fst memory, Graph.add addr new_attrs (snd memory)) -let invalidate (address, history) invalid location memory = - let invalidation = Trace.Immediate {imm= invalid; location; history} in - add_attribute address (Attribute.Invalid invalidation) memory +let invalidate (address, history) invalidation location memory = + add_attribute address (Attribute.Invalid (invalidation, Immediate {location; history})) memory let check_valid address memory = diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index af433c154..03a7e3c21 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/infer/src/pulse/PulseBaseMemory.mli @@ -56,13 +56,13 @@ val add_attribute : AbstractValue.t -> Attribute.t -> t -> t val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t -val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result +val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option val get_arithmetic : AbstractValue.t -> t -> Arithmetic.t option -val get_must_be_valid : AbstractValue.t -> t -> unit Trace.t option +val get_must_be_valid : AbstractValue.t -> t -> Trace.t option val std_vector_reserve : AbstractValue.t -> t -> t diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index c0ec6bf0d..940de1b85 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -13,18 +13,21 @@ module Trace = PulseTrace module ValueHistory = PulseValueHistory type t = - | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t} + | AccessToInvalidAddress of + { invalidation: Invalidation.t + ; invalidation_trace: Trace.t + ; access_trace: Trace.t } | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} let get_location = function - | AccessToInvalidAddress {accessed_by} -> - Trace.get_outer_location accessed_by + | AccessToInvalidAddress {access_trace} -> + Trace.get_outer_location access_trace | StackVariableAddressEscape {location} -> location let get_message = function - | AccessToInvalidAddress {accessed_by; invalidated_by} -> + | AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} -> (* The goal is to get one of the following messages depending on the scenario: 42: delete x; return x->f @@ -42,30 +45,29 @@ 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 fmt (trace : unit Trace.t) = + let pp_access_trace fmt (trace : Trace.t) = match trace with - | Immediate {imm= (); _} -> + | Immediate _ -> F.fprintf fmt "accessing memory that " | ViaCall {f; _} -> F.fprintf fmt "call to %a eventually accesses memory that " CallEvent.describe f in - let pp_invalidation_trace line fmt (trace : Invalidation.t Trace.t) = + let pp_invalidation_trace line invalidation fmt (trace : Trace.t) = let pp_line fmt line = F.fprintf fmt " on line %d" line in match trace with - | ViaCall {f; in_call} -> - let invalid = Trace.get_immediate in_call in - F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe invalid - pp_line line CallEvent.describe f - | Immediate {imm= invalid} -> - F.fprintf fmt "%a%a" Invalidation.describe invalid pp_line line + | Immediate _ -> + F.fprintf fmt "%a%a" Invalidation.describe invalidation pp_line line + | ViaCall {f; _} -> + F.fprintf fmt "%a%a indirectly during the call to %a" Invalidation.describe + invalidation pp_line line CallEvent.describe f in let invalidation_line = - let {Location.line; _} = Trace.get_outer_location invalidated_by in + let {Location.line; _} = Trace.get_outer_location invalidation_trace in line in - F.asprintf "%a%a" pp_access_trace accessed_by - (pp_invalidation_trace invalidation_line) - invalidated_by + F.asprintf "%a%a" pp_access_trace access_trace + (pp_invalidation_trace invalidation_line invalidation) + invalidation_trace | StackVariableAddressEscape {variable; _} -> let pp_var f var = if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary" @@ -81,19 +83,19 @@ let add_errlog_header ~title location errlog = let get_trace = function - | AccessToInvalidAddress {accessed_by; invalidated_by} -> - let start_location = Trace.get_start_location invalidated_by in + | AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} -> + let start_location = Trace.get_start_location invalidation_trace in add_errlog_header ~title:"invalidation part of the trace starts here" start_location @@ Trace.add_to_errlog ~nesting:1 - (fun fmt invalid -> F.fprintf fmt "%a" Invalidation.describe invalid) - invalidated_by + ~pp_immediate:(fun fmt -> F.fprintf fmt "%a" Invalidation.describe invalidation) + invalidation_trace @@ - let access_start_location = Trace.get_start_location accessed_by in + let access_start_location = Trace.get_start_location access_trace in add_errlog_header ~title:"use-after-lifetime part of the trace starts here" access_start_location @@ Trace.add_to_errlog ~nesting:1 - (fun fmt () -> F.pp_print_string fmt "invalid access occurs here") - accessed_by + ~pp_immediate:(fun fmt -> F.pp_print_string fmt "invalid access occurs here") + access_trace @@ [] | StackVariableAddressEscape {history; location; _} -> ValueHistory.add_to_errlog ~nesting:0 history @@ -103,7 +105,7 @@ let get_trace = function let get_issue_type = function - | AccessToInvalidAddress {invalidated_by} -> - Trace.get_immediate invalidated_by |> Invalidation.issue_type_of_cause + | AccessToInvalidAddress {invalidation; _} -> + Invalidation.issue_type_of_cause invalidation | StackVariableAddressEscape _ -> IssueType.stack_variable_address_escape diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index d2944af97..fa69be4fe 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -12,7 +12,10 @@ module ValueHistory = PulseValueHistory (** an error to report to the user *) type t = - | AccessToInvalidAddress of {invalidated_by: Invalidation.t Trace.t; accessed_by: unit Trace.t} + | AccessToInvalidAddress of + { invalidation: Invalidation.t + ; invalidation_trace: Trace.t + ; access_trace: Trace.t } | StackVariableAddressEscape of {variable: Var.t; history: ValueHistory.t; location: Location.t} val get_message : t -> string diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index c0e142362..c711b02be 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -16,10 +16,10 @@ type 'a access_result = ('a, Diagnostic.t) result (** Check that the [address] is not known to be invalid *) let check_addr_access location (address, history) astate = - let accessed_by = Trace.Immediate {imm= (); location; history} in - Memory.check_valid accessed_by address astate - |> Result.map_error ~f:(fun invalidated_by -> - Diagnostic.AccessToInvalidAddress {invalidated_by; accessed_by} ) + let access_trace = Trace.Immediate {location; history} in + Memory.check_valid access_trace address astate + |> Result.map_error ~f:(fun (invalidation, invalidation_trace) -> + Diagnostic.AccessToInvalidAddress {invalidation; invalidation_trace; access_trace} ) module Closures = struct diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index fe6e83bff..c603cca57 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -9,46 +9,39 @@ module F = Format module CallEvent = PulseCallEvent module ValueHistory = PulseValueHistory -type 'a t = - | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t} - | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: 'a t} +type t = + | Immediate of {location: Location.t; history: ValueHistory.t} + | ViaCall of {f: CallEvent.t; location: Location.t; history: ValueHistory.t; in_call: t} [@@deriving compare] -let rec get_immediate = function - | Immediate {imm; _} -> - imm - | ViaCall {in_call; _} -> - get_immediate in_call - - let get_outer_location = function Immediate {location; _} | ViaCall {location; _} -> location -let get_history = function Immediate {history; _} | ViaCall {history; _} -> history +let get_outer_history = function Immediate {history; _} | ViaCall {history; _} -> history let get_start_location trace = - match get_history trace |> List.last with + match get_outer_history trace |> List.last with | Some event -> ValueHistory.location_of_event event | None -> get_outer_location trace -let rec pp pp_immediate fmt = function - | Immediate {imm; location= _; history} -> - if Config.debug_level_analysis < 3 then pp_immediate fmt imm - else F.fprintf fmt "%a::%a" ValueHistory.pp history pp_immediate imm - | ViaCall {f; location= _; history; in_call} -> - if Config.debug_level_analysis < 3 then pp pp_immediate fmt in_call - else - F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp pp_immediate) in_call +let rec pp ~pp_immediate fmt trace = + if Config.debug_level_analysis < 3 then pp_immediate fmt + else + match trace with + | Immediate {location= _; history} -> + F.fprintf fmt "%a::%t" ValueHistory.pp history pp_immediate + | ViaCall {f; location= _; history; in_call} -> + F.fprintf fmt "%a::%a[%a]" ValueHistory.pp history CallEvent.pp f (pp ~pp_immediate) + in_call -let rec add_to_errlog ~nesting pp_immediate trace errlog = +let rec add_to_errlog ~nesting ~pp_immediate trace errlog = match trace with - | Immediate {imm; location; history} -> + | Immediate {location; history} -> ValueHistory.add_to_errlog ~nesting history - @@ Errlog.make_trace_element nesting location (F.asprintf "%a" pp_immediate imm) [] - :: errlog + @@ (Errlog.make_trace_element nesting location (F.asprintf "%t" pp_immediate) [] :: errlog) | ViaCall {f; location; in_call; history} -> ValueHistory.add_to_errlog ~nesting history @@ (fun errlog -> @@ -56,5 +49,5 @@ let rec add_to_errlog ~nesting pp_immediate trace errlog = (F.asprintf "when calling %a here" CallEvent.pp f) [] :: errlog ) - @@ add_to_errlog ~nesting:(nesting + 1) pp_immediate in_call + @@ add_to_errlog ~nesting:(nesting + 1) ~pp_immediate in_call @@ errlog diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index 7d4bde141..414fff4d0 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -9,29 +9,27 @@ module F = Format module CallEvent = PulseCallEvent module ValueHistory = PulseValueHistory -type 'a t = - | Immediate of {imm: 'a; location: Location.t; history: ValueHistory.t} +type t = + | Immediate of {location: Location.t; history: ValueHistory.t} | ViaCall of { f: CallEvent.t ; location: Location.t (** location of the call event *) ; history: ValueHistory.t (** the call involves a value with this prior history *) - ; in_call: 'a t (** last step of the trace is in a call to [f] made at [location] *) } + ; in_call: t (** last step of the trace is in a call to [f] made at [location] *) } [@@deriving compare] -val pp : (F.formatter -> 'a -> unit) -> F.formatter -> 'a t -> unit +val pp : pp_immediate:(F.formatter -> unit) -> F.formatter -> t -> unit -val get_outer_location : 'a t -> Location.t +val get_outer_location : t -> Location.t (** skip histories and go straight to the where the action is: either the action itself or the - call that leads to the action *) + call that leads to the action *) -val get_start_location : 'a t -> Location.t +val get_start_location : t -> Location.t (** initial step in the history if not empty, or else same as {!get_outer_location} *) -val get_immediate : 'a t -> 'a - val add_to_errlog : nesting:int - -> (F.formatter -> 'a -> unit) - -> 'a t + -> pp_immediate:(F.formatter -> unit) + -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list