From 79128771665c83653d6ecf1baa46f902dd265581 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Tue, 23 Feb 2021 03:26:52 -0800 Subject: [PATCH] [uninit] Revise error message to include access paths Summary: This diff finds a declared variable name or declared field names from trace, then constructs an error message including access paths. Reviewed By: jvillard Differential Revision: D26544275 fbshipit-source-id: 135c90a1b --- infer/src/istd/RevList.mli | 2 +- infer/src/pulse/PulseAbductiveDomain.ml | 9 ++++-- infer/src/pulse/PulseDiagnostic.ml | 34 ++++++++++++++++++-- infer/src/pulse/PulseTrace.ml | 8 +++++ infer/src/pulse/PulseTrace.mli | 3 ++ infer/src/pulse/PulseValueHistory.ml | 11 +++++-- infer/src/pulse/PulseValueHistory.mli | 4 ++- infer/tests/codetoanalyze/c/pulse/issues.exp | 2 +- 8 files changed, 62 insertions(+), 11 deletions(-) diff --git a/infer/src/istd/RevList.mli b/infer/src/istd/RevList.mli index a215eb412..64d98ab87 100644 --- a/infer/src/istd/RevList.mli +++ b/infer/src/istd/RevList.mli @@ -7,7 +7,7 @@ open! IStd -type 'a t +type 'a t [@@deriving compare, equal] val empty : 'a t (** Return empty list *) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index d844fcaa9..3312a1aa1 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -463,7 +463,8 @@ let add_edge_on_src src location stack = (stack, addr) -let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) = +let rec set_uninitialized_post tenv src typ location ?(fields_prefix = RevList.empty) + (post : PostDomain.t) = match typ.Typ.desc with | Tint _ | Tfloat _ | Tptr _ -> let {stack; attrs} = (post :> base_domain) in @@ -492,13 +493,15 @@ let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) = if Fieldname.is_internal field then acc else let field_addr = AbstractValue.mk_fresh () in - let history = [ValueHistory.StructFieldAddressCreated (field, location)] in + let fields = RevList.cons field fields_prefix in + let history = [ValueHistory.StructFieldAddressCreated (fields, location)] in let heap = BaseMemory.add_edge addr (HilExp.Access.FieldAccess field) (field_addr, history) (acc :> base_domain).heap in PostDomain.update ~heap acc - |> set_uninitialized_post tenv (`Malloc field_addr) field_typ location ) ) + |> set_uninitialized_post tenv (`Malloc field_addr) field_typ location + ~fields_prefix:fields ) ) | Tarray _ | Tvoid | Tfun | TVar _ -> (* We ignore tricky types to mark uninitialized addresses. *) post diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index e6467e2c4..b29aba8e6 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -111,7 +111,37 @@ let get_message = function "memory dynamically allocated at line %d %a, is not freed after the last access at %a" allocation_line pp_allocation_trace allocation_trace Location.pp location | ReadUninitializedValue {calling_context; trace} -> - let pp_trace fmt (trace : Trace.t) = + let root_var = + PulseTrace.find_map trace ~f:(function VariableDeclared (pvar, _) -> Some pvar | _ -> None) + |> IOption.if_none_evalopt ~f:(fun () -> + PulseTrace.find_map trace ~f:(function + | FormalDeclared (pvar, _) -> + Some pvar + | _ -> + None ) ) + |> Option.map ~f:(F.asprintf "%a" Pvar.pp_value_non_verbose) + in + let declared_fields = + PulseTrace.find_map trace ~f:(function + | StructFieldAddressCreated (fields, _) -> + Some fields + | _ -> + None ) + |> Option.map ~f:(F.asprintf "%a" ValueHistory.pp_fields) + in + let access_path = + match (root_var, declared_fields) with + | None, None -> + None + | Some root_var, None -> + Some root_var + | None, Some declared_fields -> + Some (F.sprintf "_.%s" declared_fields) + | Some root_var, Some declared_fields -> + Some (F.sprintf "%s.%s" root_var declared_fields) + in + let pp_access_path fmt = Option.iter access_path ~f:(F.fprintf fmt " `%s`") in + let pp_location fmt = let {Location.line} = Trace.get_outer_location trace in match immediate_or_first_call calling_context trace with | `Immediate -> @@ -119,7 +149,7 @@ let get_message = function | `Call f -> F.fprintf fmt "during the call to %a on line %d" CallEvent.describe f line in - F.asprintf "uninitialized value is read %a" pp_trace trace + F.asprintf "uninitialized value%t is read %t" pp_access_path pp_location | StackVariableAddressEscape {variable; _} -> let pp_var f var = if Var.is_cpp_temporary var then F.pp_print_string f "C++ temporary" diff --git a/infer/src/pulse/PulseTrace.ml b/infer/src/pulse/PulseTrace.ml index 2800fdf96..6042fdeeb 100644 --- a/infer/src/pulse/PulseTrace.ml +++ b/infer/src/pulse/PulseTrace.ml @@ -54,3 +54,11 @@ let rec add_to_errlog ?(include_value_history = true) ~nesting ~pp_immediate tra @@ errlog in if include_value_history then ValueHistory.add_to_errlog ~nesting history @@ acc else acc + + +let rec find_map ~f trace = + match trace with + | Immediate {history} -> + List.find_map history ~f + | ViaCall {history; in_call} -> + List.find_map history ~f |> IOption.if_none_evalopt ~f:(fun () -> find_map ~f in_call) diff --git a/infer/src/pulse/PulseTrace.mli b/infer/src/pulse/PulseTrace.mli index ed67b71e7..13f8155be 100644 --- a/infer/src/pulse/PulseTrace.mli +++ b/infer/src/pulse/PulseTrace.mli @@ -34,3 +34,6 @@ val add_to_errlog : -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list + +val find_map : f:(ValueHistory.event -> 'a option) -> t -> 'a option +(** Like [List.find_map], but applies to value histories. *) diff --git a/infer/src/pulse/PulseValueHistory.ml b/infer/src/pulse/PulseValueHistory.ml index 049f526df..55fd9b075 100644 --- a/infer/src/pulse/PulseValueHistory.ml +++ b/infer/src/pulse/PulseValueHistory.ml @@ -16,7 +16,7 @@ type event = | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t - | StructFieldAddressCreated of Fieldname.t * Location.t + | StructFieldAddressCreated of Fieldname.t RevList.t * Location.t | VariableAccessed of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t @@ -26,6 +26,11 @@ let yojson_of_event = [%yojson_of: _] let yojson_of_t = [%yojson_of: _] +let pp_fields = + let pp_sep fmt () = Format.pp_print_char fmt '.' in + fun fmt fields -> Format.pp_print_list ~pp_sep Fieldname.pp fmt (RevList.to_list fields) + + let pp_event_no_location fmt event = let pp_pvar fmt pvar = if Pvar.is_global pvar then F.fprintf fmt "global variable `%a`" Pvar.pp_value_non_verbose pvar @@ -53,8 +58,8 @@ let pp_event_no_location fmt event = |> Option.iter ~f:(fun proc_name -> F.fprintf fmt " of %a" Procname.pp proc_name) in F.fprintf fmt "parameter `%a`%a" Pvar.pp_value_non_verbose pvar pp_proc pvar - | StructFieldAddressCreated (field_name, _) -> - F.fprintf fmt "struct field address `%a` created" Fieldname.pp field_name + | StructFieldAddressCreated (field_names, _) -> + F.fprintf fmt "struct field address `%a` created" pp_fields field_names | VariableAccessed (pvar, _) -> F.fprintf fmt "%a accessed here" pp_pvar pvar | VariableDeclared (pvar, _) -> diff --git a/infer/src/pulse/PulseValueHistory.mli b/infer/src/pulse/PulseValueHistory.mli index 67abe4b22..9210fa1e4 100644 --- a/infer/src/pulse/PulseValueHistory.mli +++ b/infer/src/pulse/PulseValueHistory.mli @@ -16,7 +16,7 @@ type event = | Conditional of {is_then_branch: bool; if_kind: Sil.if_kind; location: Location.t} | CppTemporaryCreated of Location.t | FormalDeclared of Pvar.t * Location.t - | StructFieldAddressCreated of Fieldname.t * Location.t + | StructFieldAddressCreated of Fieldname.t RevList.t * Location.t | VariableAccessed of Pvar.t * Location.t | VariableDeclared of Pvar.t * Location.t @@ -24,6 +24,8 @@ and t = event list [@@deriving compare, equal, yojson_of] val pp : F.formatter -> t -> unit +val pp_fields : F.formatter -> Fieldname.t RevList.t -> unit + val location_of_event : event -> Location.t val add_to_errlog : nesting:int -> t -> Errlog.loc_trace_elem list -> Errlog.loc_trace_elem list diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 3282e724e..df73e3691 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -15,5 +15,5 @@ codetoanalyze/c/pulse/uninit.c, interprocedural_read_in_callee_bad, 2, PULSE_UNI codetoanalyze/c/pulse/uninit.c, interprocedural_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f2` created,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, interprocedural_uninit_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [passed as argument to `uninit`,return from call to `uninit`,assigned,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [allocated by call to `malloc` (modelled),assigned,read to uninitialized value occurs here] -codetoanalyze/c/pulse/uninit.c, nested_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `f1` created,when calling `read_g1_f1` here,parameter `x` of read_g1_f1,read to uninitialized value occurs here] +codetoanalyze/c/pulse/uninit.c, nested_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `g1.f1` created,when calling `read_g1_f1` here,parameter `x` of read_g1_f1,read to uninitialized value occurs here] codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]