[pulse] Uninitialized check for struct fields

Reviewed By: jvillard

Differential Revision: D25371929

fbshipit-source-id: 966f333e3

infer/src/IR/Fieldname.ml

@@ -25,6 +25,12 @@ let is_java {class_name} = Typ.Name.Java.is_class class_name
 
 let is_java_synthetic t = is_java t && JConfig.is_synthetic_name (get_field_name t)
 
+let is_internal {field_name} =
+  String.is_prefix field_name ~prefix:"__"
+  || (* NOTE: _M_ is internal field of std::thread::id *)
+  String.is_prefix field_name ~prefix:"_M_"
+
+
 module T = struct
   type nonrec t = t [@@deriving compare]
 end

infer/src/IR/Fieldname.mli

@@ -26,6 +26,9 @@ val is_java : t -> bool
 val is_java_synthetic : t -> bool
 (** Check if the field is autogenerated/synthetic **)
 
+val is_internal : t -> bool
+(** Check if the field has the prefix "__" or "_M_" (internal field of std::thread::id) *)
+
 (** Set for fieldnames *)
 module Set : Caml.Set.S with type elt = t
 

infer/src/pulse/Pulse.ml

@@ -70,14 +70,14 @@ module PulseTransferFunctions = struct
     AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals
 
 
-  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret callee_pname
-      call_exp actuals call_loc astate =
+  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv} ret
+      callee_pname call_exp actuals call_loc astate =
     match callee_pname with
     | Some callee_pname when not Config.pulse_intraprocedural_only ->
         let formals_opt = get_pvar_formals callee_pname in
         let callee_data = analyze_dependency callee_pname in
-        PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret
-          ~actuals ~formals_opt astate
+        PulseOperations.call tenv ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname
+          ~ret ~actuals ~formals_opt astate
     | _ ->
         L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
         let astate =
@@ -86,8 +86,8 @@ module PulseTransferFunctions = struct
         in
         [ Ok
             (ContinueProgram
-               (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals
-                  ~formals_opt:None astate)) ]
+               (PulseOperations.unknown_call tenv call_loc (SkippedUnknownCall call_exp) ~ret
+                  ~actuals ~formals_opt:None astate)) ]
 
 
   (** has an object just gone out of scope? *)
@@ -289,8 +289,9 @@ module PulseTransferFunctions = struct
     (astates, ret_vars)
 
 
-  let exec_instr_aux (astate : Domain.t) ({InterproceduralAnalysis.proc_desc} as analysis_data)
-      _cfg_node (instr : Sil.instr) : Domain.t list =
+  let exec_instr_aux (astate : Domain.t)
+      ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) _cfg_node (instr : Sil.instr) :
+      Domain.t list =
     match astate with
     | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ ->
         (* We can also continue the analysis with the error state here
@@ -423,7 +424,7 @@ module PulseTransferFunctions = struct
             in
             remove_vars vars_to_remove astates
       | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) ->
-          [PulseOperations.realloc_pvar pvar typ location astate |> Domain.continue]
+          [PulseOperations.realloc_pvar tenv pvar typ location astate |> Domain.continue]
       | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip) ->
           [ContinueProgram astate] )
 
@@ -454,9 +455,9 @@ let with_debug_exit_node proc_desc ~f =
     ~f
 
 
-let checker ({InterproceduralAnalysis.proc_desc; err_log} as analysis_data) =
+let checker ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data) =
   AbstractValue.State.reset () ;
-  let initial = [ExecutionDomain.mk_initial proc_desc] in
+  let initial = [ExecutionDomain.mk_initial tenv proc_desc] in
   match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with
   | Some posts ->
       with_debug_exit_node proc_desc ~f:(fun () ->

infer/src/pulse/PulseAbductiveDomain.ml

@@ -13,6 +13,7 @@ module BaseDomain = PulseBaseDomain
 module BaseStack = PulseBaseStack
 module BaseMemory = PulseBaseMemory
 module BaseAddressAttributes = PulseBaseAddressAttributes
+module UninitBlocklist = PulseUninitBlocklist
 
 (** signature common to the "normal" [Domain], representing the post at the current program point,
     and the inverted [PreDomain], representing the inferred pre-condition*)
@@ -220,12 +221,26 @@ module AddressAttributes = struct
 
   (** if [address] is in [pre] then add the attribute [attr] *)
   let abduce_attribute address attribute astate =
-    L.d_printfln "Abducing %a:%a" AbstractValue.pp address Attribute.pp attribute ;
+    let is_must_be_initialized_on_written =
+      match (attribute : Attribute.t) with
+      | MustBeInitialized _ ->
+          BaseAddressAttributes.find_opt address (astate.post :> base_domain).attrs
+          |> Option.exists ~f:(fun attrs -> Attributes.get_written_to attrs |> Option.is_some)
+      | _ ->
+          false
+    in
     let new_pre =
-      if BaseMemory.mem address (astate.pre :> base_domain).heap then
-        PreDomain.update astate.pre
-          ~attrs:(BaseAddressAttributes.add_one address attribute (astate.pre :> base_domain).attrs)
-      else astate.pre
+      if is_must_be_initialized_on_written then (
+        L.d_printfln "No abducing %a:%a, the address has been written" AbstractValue.pp address
+          Attribute.pp attribute ;
+        astate.pre )
+      else (
+        L.d_printfln "Abducing %a:%a" AbstractValue.pp address Attribute.pp attribute ;
+        if BaseMemory.mem address (astate.pre :> base_domain).heap then
+          PreDomain.update astate.pre
+            ~attrs:
+              (BaseAddressAttributes.add_one address attribute (astate.pre :> base_domain).attrs)
+        else astate.pre )
     in
     if phys_equal new_pre astate.pre then astate else {astate with pre= new_pre}
 
@@ -312,7 +327,9 @@ module AddressAttributes = struct
         let astate =
           if Attribute.is_suitable_for_pre attr then abduce_attribute value attr astate else astate
         in
-        let astate = add_one value attr astate in
+        let astate =
+          if Attribute.is_suitable_for_post attr then add_one value attr astate else astate
+        in
         match attr with Attribute.WrittenTo _ -> initialize value astate | _ -> astate )
 
 
@@ -430,28 +447,51 @@ module Memory = struct
   let find_opt address astate = BaseMemory.find_opt address (astate.post :> base_domain).heap
 end
 
-let set_uninitialized_post src typ location (post : PostDomain.t) =
+let add_edge_on_src src location stack =
+  match src with
+  | `LocalDecl (pvar, addr_opt) -> (
+    match addr_opt with
+    | None ->
+        let addr = AbstractValue.mk_fresh () in
+        let history = [ValueHistory.VariableDeclared (pvar, location)] in
+        (BaseStack.add (Var.of_pvar pvar) (addr, history) stack, addr)
+    | Some addr ->
+        (stack, addr) )
+  | `Malloc addr ->
+      (stack, addr)
+
+
+let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) =
   match typ.Typ.desc with
   | Tint _ | Tfloat _ | Tptr _ ->
       let {stack; attrs} = (post :> base_domain) in
-      let stack, addr =
-        match src with
-        | `LocalDecl (pvar, addr_opt) -> (
-          match addr_opt with
-          | None ->
-              let addr = AbstractValue.mk_fresh () in
-              let history = [ValueHistory.VariableDeclared (pvar, location)] in
-              (BaseStack.add (Var.of_pvar pvar) (addr, history) stack, addr)
-          | Some addr ->
-              (stack, addr) )
-        | `Malloc addr ->
-            (stack, addr)
-      in
+      let stack, addr = add_edge_on_src src location stack in
       let attrs = BaseAddressAttributes.add_one addr Uninitialized attrs in
       PostDomain.update ~stack ~attrs post
-  | Tstruct _ ->
-      (* TODO: set uninitialized attributes for fields *)
+  | Tstruct typ_name when UninitBlocklist.is_blocklisted_struct typ_name ->
       post
+  | Tstruct (CUnion _) | Tstruct (CppClass {is_union= true}) ->
+      (* Ignore union fields in the uninitialized checker *)
+      post
+  | Tstruct _ -> (
+    match Typ.name typ |> Option.bind ~f:(Tenv.lookup tenv) with
+    | None | Some {fields= [_]} ->
+        (* Ignore single field structs: see D26146578 *)
+        post
+    | Some {fields} ->
+        List.fold fields ~init:post ~f:(fun (acc : PostDomain.t) (field, field_typ, _) ->
+            if Fieldname.is_internal field then acc
+            else
+              let {stack; heap} = (acc :> base_domain) in
+              let stack, addr = add_edge_on_src src location stack in
+              let field_addr = AbstractValue.mk_fresh () in
+              let history = [ValueHistory.StructFieldAddressCreated (field, location)] in
+              let heap =
+                BaseMemory.add_edge addr (HilExp.Access.FieldAccess field) (field_addr, history)
+                  heap
+              in
+              PostDomain.update ~stack ~heap acc
+              |> set_uninitialized_post tenv (`Malloc field_addr) field_typ location ) )
   | Tarray _ ->
       (* TODO: set uninitialized attributes for elements *)
       post
@@ -460,11 +500,11 @@ let set_uninitialized_post src typ location (post : PostDomain.t) =
       post
 
 
-let set_uninitialized src typ location x =
-  {x with post= set_uninitialized_post src typ location x.post}
+let set_uninitialized tenv src typ location x =
+  {x with post= set_uninitialized_post tenv src typ location x.post}
 
 
-let mk_initial proc_desc =
+let mk_initial tenv proc_desc =
   (* HACK: save the formals in the stacks of the pre and the post to remember which local variables
      correspond to formals *)
   let proc_name = Procdesc.get_proc_name proc_desc in
@@ -524,7 +564,7 @@ let mk_initial proc_desc =
   let locals = Procdesc.get_locals proc_desc in
   let post =
     List.fold locals ~init:post ~f:(fun (acc : PostDomain.t) {ProcAttributes.name; typ} ->
-        set_uninitialized_post (`LocalDecl (Pvar.mk name proc_name, None)) typ location acc )
+        set_uninitialized_post tenv (`LocalDecl (Pvar.mk name proc_name, None)) typ location acc )
   in
   { pre
   ; post

infer/src/pulse/PulseAbductiveDomain.mli

@@ -81,7 +81,7 @@ val pp : Format.formatter -> t -> unit
 
 val set_isl_status : isl_status -> t -> t
 
-val mk_initial : Procdesc.t -> t
+val mk_initial : Tenv.t -> Procdesc.t -> t
 
 val get_pre : t -> BaseDomain.t
 
@@ -212,7 +212,8 @@ val initialize : AbstractValue.t -> t -> t
 (** Remove "Uninitialized" attribute of the given address *)
 
 val set_uninitialized :
-     [ `LocalDecl of Pvar.t * AbstractValue.t option
+     Tenv.t
+  -> [ `LocalDecl of Pvar.t * AbstractValue.t option
        (** the second optional parameter is for the address of the variable *)
      | `Malloc of AbstractValue.t  (** the address parameter is a newly allocated address *) ]
   -> Typ.t

infer/src/pulse/PulseAttribute.ml

@@ -270,6 +270,23 @@ let is_suitable_for_pre = function
       false
 
 
+let is_suitable_for_post = function
+  | MustBeInitialized _ | MustBeValid _ ->
+      false
+  | Invalid _
+  | Allocated _
+  | ISLAbduced _
+  | AddressOfCppTemporary _
+  | AddressOfStackVariable _
+  | Closure _
+  | DynamicType _
+  | EndOfCollection
+  | StdVectorReserve
+  | Uninitialized
+  | WrittenTo _ ->
+      true
+
+
 let map_trace ~f = function
   | Allocated (procname, trace) ->
       Allocated (procname, f trace)

infer/src/pulse/PulseAttribute.mli

@@ -31,6 +31,8 @@ val pp : F.formatter -> t -> unit
 
 val is_suitable_for_pre : t -> bool
 
+val is_suitable_for_post : t -> bool
+
 val map_trace : f:(Trace.t -> Trace.t) -> t -> t
 (** applies [f] to the traces found in attributes, leaving attributes without traces intact *)
 

infer/src/pulse/PulseExecutionDomain.ml

@@ -28,7 +28,7 @@ type t = AbductiveDomain.t base_t
 
 let continue astate = ContinueProgram astate
 
-let mk_initial pdesc = ContinueProgram (AbductiveDomain.mk_initial pdesc)
+let mk_initial tenv pdesc = ContinueProgram (AbductiveDomain.mk_initial tenv pdesc)
 
 let leq ~lhs ~rhs =
   phys_equal lhs rhs

infer/src/pulse/PulseExecutionDomain.mli

@@ -27,7 +27,7 @@ include AbstractDomain.NoJoin with type t := t
 
 val continue : AbductiveDomain.t -> t
 
-val mk_initial : Procdesc.t -> t
+val mk_initial : Tenv.t -> Procdesc.t -> t
 
 val is_unsat_cheap : t -> bool
 (** see {!PulsePathCondition.is_unsat_cheap} *)

infer/src/pulse/PulseModels.ml

@@ -86,7 +86,7 @@ module Misc = struct
       don't have the implementation. This triggers a bunch of heuristics, e.g. to havoc arguments we
       suspect are passed by reference. *)
   let unknown_call skip_reason args : model =
-   fun _ ~callee_procname location ~ret astate ->
+   fun {tenv} ~callee_procname location ~ret astate ->
     let actuals =
       List.map args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= actual; typ} ->
           (actual, typ) )
@@ -95,7 +95,7 @@ module Misc = struct
       AnalysisCallbacks.proc_resolve_attributes callee_procname
       |> Option.map ~f:ProcAttributes.get_pvar_formals
     in
-    PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt astate
+    PulseOperations.unknown_call tenv location (Model skip_reason) ~ret ~actuals ~formals_opt astate
     |> ok_continue
 
 
@@ -139,15 +139,15 @@ end
 module C = struct
   let free deleted_access : model = Misc.free_or_delete `Free deleted_access
 
-  let set_uninitialized size_exp_opt location ret_value astate =
+  let set_uninitialized tenv size_exp_opt location ret_value astate =
     Option.value_map size_exp_opt ~default:astate ~f:(fun size_exp ->
         BufferOverrunModels.get_malloc_info_opt size_exp
         |> Option.value_map ~default:astate ~f:(fun (obj_typ, _, _, _) ->
-               AbductiveDomain.set_uninitialized (`Malloc ret_value) obj_typ location astate ) )
+               AbductiveDomain.set_uninitialized tenv (`Malloc ret_value) obj_typ location astate ) )
 
 
   let malloc_common ~size_exp_opt : model =
-   fun _ ~callee_procname location ~ret:(ret_id, _) astate ->
+   fun {tenv} ~callee_procname location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let ret_value =
       (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}])
@@ -156,7 +156,7 @@ module C = struct
     let astate_alloc =
       PulseArithmetic.and_positive ret_addr astate
       |> PulseOperations.allocate callee_procname location ret_value
-      |> set_uninitialized size_exp_opt location ret_addr
+      |> set_uninitialized tenv size_exp_opt location ret_addr
     in
     let result_null =
       let+ astate_null =
@@ -169,7 +169,7 @@ module C = struct
 
 
   let malloc_not_null_common ~size_exp_opt : model =
-   fun _ ~callee_procname location ~ret:(ret_id, _) astate ->
+   fun {tenv} ~callee_procname location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let ret_value =
       (ret_addr, [ValueHistory.Allocation {f= Model (Procname.to_string callee_procname); location}])
@@ -178,7 +178,7 @@ module C = struct
     let astate =
       PulseOperations.allocate callee_procname location ret_value astate
       |> PulseArithmetic.and_positive ret_addr
-      |> set_uninitialized size_exp_opt location ret_addr
+      |> set_uninitialized tenv size_exp_opt location ret_addr
     in
     ok_continue astate
 
@@ -218,7 +218,7 @@ module ObjC = struct
 
 
   let dispatch_sync args : model =
-   fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; proc_desc; tenv} ~callee_procname:_ location ~ret astate ->
     match List.last args with
     | None ->
         ok_continue astate
@@ -230,7 +230,7 @@ module ObjC = struct
         | None ->
             ok_continue astate
         | Some callee_proc_name ->
-            PulseOperations.call ~caller_proc_desc:proc_desc
+            PulseOperations.call tenv ~caller_proc_desc:proc_desc
               ~callee_data:(analyze_dependency callee_proc_name)
               location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate )
 end
@@ -479,6 +479,11 @@ module StdAtomicInteger = struct
 
   let store_backing_int location this_address new_value astate =
     let* astate, this = PulseOperations.eval_access Read location this_address Dereference astate in
+    let astate =
+      AddressAttributes.add_one (fst this_address)
+        (WrittenTo (Trace.Immediate {location; history= []}))
+        astate
+    in
     let* astate, int_field =
       PulseOperations.eval_access Write location this (FieldAccess internal_int) astate
     in
@@ -551,7 +556,7 @@ end
 module StdFunction = struct
   let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals :
       model =
-   fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; proc_desc; tenv} ~callee_procname:_ location ~ret astate ->
     let havoc_ret (ret_id, _) astate =
       let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in
       [PulseOperations.havoc_id ret_id [event] astate]
@@ -570,7 +575,7 @@ module StdFunction = struct
           :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} ->
                  (arg_payload, typ) )
         in
-        PulseOperations.call ~caller_proc_desc:proc_desc
+        PulseOperations.call tenv ~caller_proc_desc:proc_desc
           ~callee_data:(analyze_dependency callee_proc_name)
           location callee_proc_name ~ret ~actuals ~formals_opt:None astate
 

infer/src/pulse/PulseOperations.ml

@@ -315,12 +315,12 @@ let eval_deref_isl location exp astate =
           Ok (acc_astates @ [astate_addr]) )
 
 
-let realloc_pvar pvar typ location astate =
+let realloc_pvar tenv pvar typ location astate =
   let addr = AbstractValue.mk_fresh () in
   let astate =
     Stack.add (Var.of_pvar pvar) (addr, [ValueHistory.VariableDeclared (pvar, location)]) astate
   in
-  AbductiveDomain.set_uninitialized (`LocalDecl (pvar, Some addr)) typ location astate
+  AbductiveDomain.set_uninitialized tenv (`LocalDecl (pvar, Some addr)) typ location astate
 
 
 let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate
@@ -565,22 +565,36 @@ let is_ptr_to_const formal_typ_opt =
       match formal_typ.desc with Typ.Tptr (t, _) -> Typ.is_const t.quals | _ -> false )
 
 
-let unknown_call call_loc reason ~ret ~actuals ~formals_opt astate =
+let unknown_call tenv call_loc reason ~ret ~actuals ~formals_opt astate =
   let event = ValueHistory.Call {f= reason; location= call_loc; in_call= []} in
   let havoc_ret (ret, _) astate = havoc_id ret [event] astate in
+  let rec havoc_fields ((_, history) as addr) typ astate =
+    match typ.Typ.desc with
+    | Tstruct struct_name -> (
+      match Tenv.lookup tenv struct_name with
+      | Some {fields} ->
+          List.fold fields ~init:astate ~f:(fun acc (field, field_typ, _) ->
+              let fresh_value = AbstractValue.mk_fresh () in
+              Memory.add_edge addr (FieldAccess field) (fresh_value, [event]) call_loc acc
+              |> havoc_fields (fresh_value, history) field_typ )
+      | None ->
+          astate )
+    | _ ->
+        astate
+  in
   let havoc_actual_if_ptr (actual, actual_typ) formal_typ_opt astate =
     (* We should not havoc when the corresponding formal is a
        pointer to const *)
-    if
-      (not (Language.curr_language_is Java))
-      && Typ.is_pointer actual_typ
-      && not (is_ptr_to_const formal_typ_opt)
-    then
-      (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when
-         havoc'ing pointer parameters (which normally causes a [check_valid] call. *)
-      let fresh_value = AbstractValue.mk_fresh () in
-      Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate
-    else astate
+    match actual_typ.Typ.desc with
+    | Tptr (typ, _)
+      when (not (Language.curr_language_is Java)) && not (is_ptr_to_const formal_typ_opt) ->
+        (* HACK: write through the pointer even if it is invalid (except in Java). This is to avoid raising issues when
+           havoc'ing pointer parameters (which normally causes a [check_valid] call. *)
+        let fresh_value = AbstractValue.mk_fresh () in
+        Memory.add_edge actual Dereference (fresh_value, [event]) call_loc astate
+        |> havoc_fields actual typ
+    | _ ->
+        astate
   in
   let add_skipped_proc astate =
     match reason with
@@ -683,7 +697,7 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate)
   AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
 
 
-let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
+let call tenv ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
     callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) =
   let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in
   match callee_data with
@@ -743,6 +757,6 @@ let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option)
       L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ;
       let astate =
         conservatively_initialize_args (get_arg_values ()) astate
-        |> unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt
+        |> unknown_call tenv call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt
       in
       [Ok (ContinueProgram astate)]

infer/src/pulse/PulseOperations.mli

@@ -102,7 +102,7 @@ val havoc_field :
   -> t
   -> t access_result
 
-val realloc_pvar : Pvar.t -> Typ.t -> Location.t -> t -> t
+val realloc_pvar : Tenv.t -> Pvar.t -> Typ.t -> Location.t -> t -> t
 
 val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
@@ -185,7 +185,8 @@ val check_address_escape :
   Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result
 
 val call :
-     caller_proc_desc:Procdesc.t
+     Tenv.t
+  -> caller_proc_desc:Procdesc.t
   -> callee_data:(Procdesc.t * PulseSummary.t) option
   -> Location.t
   -> Procname.t
@@ -198,7 +199,8 @@ val call :
     it exists *)
 
 val unknown_call :
-     Location.t
+     Tenv.t
+  -> Location.t
   -> CallEvent.t
   -> ret:Ident.t * Typ.t
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list

infer/src/pulse/PulseUninitBlocklist.ml

@@ -0,0 +1,21 @@
+(*
+ * 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
+
+let dispatch : (unit, unit, unit) ProcnameDispatcher.TypName.dispatcher =
+  let open ProcnameDispatcher.TypName in
+  make_dispatcher
+    [ -"folly" &:: "Optional" &::.*--> ()
+    ; -"std" &:: "__wrap_iter" &::.*--> ()
+    ; -"std" &:: "atomic" &::.*--> ()
+    ; -"std" &:: "function" &::.*--> ()
+    ; -"std" &:: "optional" &::.*--> ()
+    ; -"std" &:: "vector" &::.*--> () ]
+
+
+let is_blocklisted_struct typ_name = dispatch () typ_name |> Option.is_some

infer/src/pulse/PulseUninitBlocklist.mli

@@ -0,0 +1,11 @@
+(*
+ * 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
+
+val is_blocklisted_struct : Typ.name -> bool
+(** Check if a struct name is in the blocklist for uninit checker. *)

infer/src/pulse/PulseValueHistory.ml

@@ -16,6 +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
   | VariableAccessed of Pvar.t * Location.t
   | VariableDeclared of Pvar.t * Location.t
 
@@ -52,6 +53,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
   | VariableAccessed (pvar, _) ->
       F.fprintf fmt "%a accessed here" pp_pvar pvar
   | VariableDeclared (pvar, _) ->
@@ -66,6 +69,7 @@ let location_of_event = function
   | Conditional {location}
   | CppTemporaryCreated location
   | FormalDeclared (_, location)
+  | StructFieldAddressCreated (_, location)
   | VariableAccessed (_, location)
   | VariableDeclared (_, location) ->
       location

infer/src/pulse/PulseValueHistory.mli

@@ -16,6 +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
   | VariableAccessed of Pvar.t * Location.t
   | VariableDeclared of Pvar.t * Location.t
 

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -12,6 +12,7 @@ codetoanalyze/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALI
 codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `p` declared here,read to uninitialized value occurs here]
 codetoanalyze/c/pulse/uninit.c, interprocedural_nop_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]
 codetoanalyze/c/pulse/uninit.c, interprocedural_read_in_callee_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,when calling `read_int_ref` here,parameter `p` of read_int_ref,read to uninitialized value occurs here]
+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, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [variable `x` declared here,read to uninitialized value occurs here]

infer/tests/codetoanalyze/c/pulse/uninit.c

@@ -86,7 +86,13 @@ void get_field_address_good() {
 
 void init_f1(struct uninit_s* p) { p->f1 = 5; }
 
-void interprocedural_struct_bad_FN() {
+void interprocedural_struct_good() {
+  struct uninit_s s;
+  init_f1(&s);
+  int y = s.f1;
+}
+
+void interprocedural_struct_bad() {
   struct uninit_s s;
   init_f1(&s);
   int y = s.f2;
@@ -99,3 +105,14 @@ void malloc_array_good(int len) {
   }
   free(o);
 }
+
+struct uninit_s unknown_struct();
+
+struct uninit_s unknown_wrapper() {
+  return unknown_struct();
+}
+
+void havoc_calling_unknown_struct_good() {
+  struct uninit_s x = unknown_wrapper();
+  int y = x.f1;
+}

infer/tests/codetoanalyze/cpp/pulse/fbstring.cpp

@@ -32,7 +32,7 @@ struct LikeFBString {
   size_t size_;
   unsigned int* refcount_;
 
-  LikeFBString() {}
+  LikeFBString() { category_ = 0; }
 
   LikeFBString(const LikeFBString& src) {
     category_ = src.category();

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -95,6 +95,7 @@ codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::load_store_possible_npe_ba
 codetoanalyze/cpp/pulse/std_atomics.cpp, atomic_test::pre_increment_decrement_test_bad, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/temporaries.cpp, temporaries::call_mk_UniquePtr_A_deref_bad, 4, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `new` (modelled),return from call to `new` (modelled),passed as argument to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,when calling `temporaries::UniquePtr<temporaries::A>::~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::~UniquePtr,when calling `temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr` here,parameter `this` of temporaries::UniquePtr<temporaries::A>::__infer_inner_destructor_~UniquePtr,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `temporaries::mk_UniquePtr_A`,passed as argument to `new` (modelled),return from call to `new` (modelled),passed as argument to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,parameter `y` of temporaries::UniquePtr<temporaries::A>::UniquePtr,assigned,return from call to `temporaries::UniquePtr<temporaries::A>::UniquePtr`,return from call to `temporaries::mk_UniquePtr_A`,passed as argument to `temporaries::UniquePtr<temporaries::A>::get`,return from call to `temporaries::UniquePtr<temporaries::A>::get`,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/trace.cpp, trace_free_bad, 4, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of trace_free_bad,passed as argument to `make_alias`,parameter `src` of make_alias,assigned,return from call to `make_alias`,when calling `do_free` here,parameter `x` of do_free,assigned,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of trace_free_bad,invalid access occurs here]
+codetoanalyze/cpp/pulse/uninit.cpp, Uninit::call_init_by_store_ok, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `i` created,read to uninitialized value occurs here]
 codetoanalyze/cpp/pulse/unknown_functions.cpp, call_init_with_pointer_value_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/unknown_functions.cpp, const_no_init_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/cpp/pulse/use_after_delete.cpp, delete_in_branch_latent, 5, USE_AFTER_DELETE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,invalid access occurs here]

infer/tests/codetoanalyze/cpp/pulse/uninit.cpp

@@ -0,0 +1,36 @@
+/*
+ * 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.
+ */
+
+#include <atomic>
+#include <functional>
+
+void get_closure(std::function<int()> closure);
+
+class Uninit {
+  void closure_call_ok() {
+    auto closure = [this]() { return 5; };
+    get_closure(closure);
+  }
+
+  class MyClass {
+   public:
+    int i;
+    int j;
+  };
+
+  void init_by_store(MyClass* x) {
+    MyClass y{3, 5};
+    reinterpret_cast<std::atomic<MyClass>*>(x)->store(
+        y, std::memory_order_release);
+  }
+
+  void call_init_by_store_ok() {
+    MyClass x;
+    init_by_store(&x);
+    int y = x.i;
+  }
+};