[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

@@ -7,7 +7,7 @@
 
 open! IStd
 
-type 'a t
+type 'a t [@@deriving compare, equal]
 
 val empty : 'a t
 (** Return empty list *)

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

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"

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)

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. *)

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, _) ->

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

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]