[pulse] Uninitialized value check in pulse

Summary:
This diff adds uninitialized value check in pulse.  For now, it supports only simple cases,

- declared variables with a type of integer, float, void, and pointer
- malloced pointer variables that points to integer, float, void, and pointer

TODOs: I will add more cases in the following diffs.

- declared/malloced array
- declared/malloced struct
- inter-procedural checking

Reviewed By: jvillard

Differential Revision: D25269073

fbshipit-source-id: 317df9a85

infer/man/man1/infer-full.txt

@@ -502,6 +502,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_UNINITIALIZED_VALUE (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              RESOURCE_LEAK (enabled by default),

infer/man/man1/infer-report.txt

@@ -210,6 +210,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_UNINITIALIZED_VALUE (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              RESOURCE_LEAK (enabled by default),

infer/man/man1/infer.txt

@@ -502,6 +502,7 @@ OPTIONS
              PRECONDITION_NOT_FOUND (enabled by default),
              PRECONDITION_NOT_MET (enabled by default),
              PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
+             PULSE_UNINITIALIZED_VALUE (disabled by default),
              PURE_FUNCTION (enabled by default),
              QUANDARY_TAINT_ERROR (enabled by default),
              RESOURCE_LEAK (enabled by default),

infer/src/base/IssueType.ml

@@ -900,6 +900,11 @@ let uninitialized_value =
     ~user_documentation:[%blob "../../documentation/issues/UNINITIALIZED_VALUE.md"]
 
 
+let uninitialized_value_pulse =
+  register ~enabled:false ~id:"PULSE_UNINITIALIZED_VALUE" Error Pulse ~hum:"Unitialized Value"
+    ~user_documentation:"See [UNITIALIZED_VALUE](#uninitialized_value). Re-implemented using Pulse."
+
+
 let unreachable_code_after =
   register ~id:"UNREACHABLE_CODE" Error BufferOverrunChecker
     ~user_documentation:"A program point is unreachable."

infer/src/base/IssueType.mli

@@ -320,6 +320,8 @@ val topl_pulse_error : t
 
 val uninitialized_value : t
 
+val uninitialized_value_pulse : t
+
 val unreachable_code_after : t
 
 val use_after_delete : t

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -58,22 +58,23 @@ let eval_binop ~f e1 e2 =
   {exec; check= no_check}
 
 
-(* It returns a tuple of:
-     - type of array element
-     - stride of the type
-     - array size
-     - flexible array size *)
-let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option = function
+let get_malloc_info_opt = function
   | Exp.BinOp (Binop.Mult _, Exp.Sizeof {typ; nbytes}, length)
   | Exp.BinOp (Binop.Mult _, length, Exp.Sizeof {typ; nbytes}) ->
-      (typ, nbytes, length, None)
+      Some (typ, nbytes, length, None)
   (* In Java all arrays are dynamically allocated *)
   | Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java ->
-      (typ, nbytes, arr_length, Some arr_length)
+      Some (typ, nbytes, arr_length, Some arr_length)
   | Exp.Sizeof {typ; nbytes; dynamic_length} ->
-      (typ, nbytes, Exp.one, dynamic_length)
-  | x ->
-      (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None)
+      Some (typ, nbytes, Exp.one, dynamic_length)
+  | _ ->
+      None
+
+
+let get_malloc_info : Exp.t -> Typ.t * Int.t option * Exp.t * Exp.t option =
+ fun x ->
+  get_malloc_info_opt x
+  |> IOption.if_none_eval ~f:(fun () -> (Typ.mk (Typ.Tint Typ.IChar), Some 1, x, None))
 
 
 let check_alloc_size ~can_be_zero size_exp {location; integer_type_widths} mem cond_set =

infer/src/bufferoverrun/bufferOverrunModels.mli

@@ -70,3 +70,11 @@ end
 module Call : sig
   val dispatch : (Tenv.t, model, unit) ProcnameDispatcher.Call.dispatcher
 end
+
+val get_malloc_info_opt : Exp.t -> (Typ.t * Int.t option * Exp.t * Exp.t option) option
+(** Return a tuple of malloc information with heuristics:
+
+    - type of array element
+    - stride of the type
+    - array size
+    - flexible array size *)

infer/src/pulse/Pulse.ml

@@ -94,7 +94,9 @@ module PulseTransferFunctions = struct
     match (exec_state : ExecutionDomain.t) with
     | ContinueProgram astate ->
         let gone_out_of_scope = Invalidation.GoneOutOfScope (pvar, typ) in
-        let* astate, out_of_scope_base = PulseOperations.eval call_loc (Exp.Lvar pvar) astate in
+        let* astate, out_of_scope_base =
+          PulseOperations.eval NoAccess call_loc (Exp.Lvar pvar) astate
+        in
         (* invalidate [&x] *)
         PulseOperations.invalidate call_loc gone_out_of_scope out_of_scope_base astate
         >>| ExecutionDomain.continue
@@ -126,8 +128,8 @@ module PulseTransferFunctions = struct
     match (lhs : Exp.t) with
     | Lindex (arr, index) ->
         (let open IResult.Let_syntax in
-        let* _astate, (aw_array, _history) = PulseOperations.eval loc arr astate in
-        let+ _astate, (aw_index, _history) = PulseOperations.eval loc index astate in
+        let* _astate, (aw_array, _history) = PulseOperations.eval Read loc arr astate in
+        let+ _astate, (aw_index, _history) = PulseOperations.eval Read loc index astate in
         let topl_event = PulseTopl.ArrayWrite {aw_array; aw_index} in
         AbductiveDomain.Topl.small_step loc topl_event astate)
         |> Result.ok (* don't emit Topl event if evals fail *) |> Option.value ~default:astate
@@ -135,19 +137,30 @@ module PulseTransferFunctions = struct
         astate
 
 
+  (* NOTE: At the moment, it conservatively assumes that all reachable addresses from function
+     arguments are initialized by callee. *)
+  let conservatively_initialize_args func_args ({AbductiveDomain.post} as astate) =
+    let arg_values =
+      List.map func_args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= value, _} -> value)
+    in
+    let reachable_values = BaseDomain.reachable_addresses_from arg_values (post :> BaseDomain.t) in
+    AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
+
+
   let dispatch_call ({InterproceduralAnalysis.tenv} as analysis_data) ret call_exp actuals call_loc
       flags astate =
     (* evaluate all actuals *)
     let* astate, rev_func_args =
       List.fold_result actuals ~init:(astate, [])
         ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) ->
-          let+ astate, actual_evaled = PulseOperations.eval call_loc actual_exp astate in
+          let+ astate, actual_evaled = PulseOperations.eval Read call_loc actual_exp astate in
           ( astate
           , ProcnameDispatcher.Call.FuncArg.
               {exp= actual_exp; arg_payload= actual_evaled; typ= actual_typ}
             :: rev_func_args ) )
     in
     let func_args = List.rev rev_func_args in
+    let astate = conservatively_initialize_args func_args astate in
     let callee_pname = proc_name_of_call call_exp in
     let model =
       match callee_pname with
@@ -278,8 +291,10 @@ module PulseTransferFunctions = struct
           (* [*lhs_exp := rhs_exp] *)
           let event = ValueHistory.Assignment loc in
           let result =
-            let* astate, (rhs_addr, rhs_history) = PulseOperations.eval loc rhs_exp astate in
-            let* astate, lhs_addr_hist = PulseOperations.eval loc lhs_exp astate in
+            let* astate, (rhs_addr, rhs_history) =
+              PulseOperations.eval NoAccess loc rhs_exp astate
+            in
+            let* astate, lhs_addr_hist = PulseOperations.eval Write loc lhs_exp astate in
             let* astate =
               PulseOperations.write_deref loc ~ref:lhs_addr_hist
                 ~obj:(rhs_addr, event :: rhs_history)
@@ -339,8 +354,8 @@ module PulseTransferFunctions = struct
               if List.is_empty ret_vars then vars else List.rev_append vars ret_vars
             in
             remove_vars vars_to_remove astates
-      | Metadata (VariableLifetimeBegins (pvar, _, location)) when not (Pvar.is_global pvar) ->
-          [PulseOperations.realloc_pvar pvar location astate |> Domain.continue]
+      | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) ->
+          [PulseOperations.realloc_pvar pvar typ location astate |> Domain.continue]
       | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip) ->
           [Domain.ContinueProgram astate] )
 

infer/src/pulse/PulseAbductiveDomain.ml

@@ -42,7 +42,11 @@ type base_domain = BaseDomain.t =
   {heap: BaseMemory.t; stack: BaseStack.t; attrs: BaseAddressAttributes.t}
 
 (** represents the post abstract state at each program point *)
-module PostDomain : BaseDomainSig = struct
+module PostDomain : sig
+  include BaseDomainSig
+
+  val initialize : AbstractValue.t -> t -> t
+end = struct
   include BaseDomain
 
   let update ?stack ?heap ?attrs foot =
@@ -70,6 +74,11 @@ module PostDomain : BaseDomainSig = struct
       BaseAddressAttributes.filter_with_discarded_addrs (fun address _ -> f address) foot.attrs
     in
     (update ~heap:heap' ~attrs:attrs' foot, discarded_addresses)
+
+
+  let initialize address x =
+    let attrs = BaseAddressAttributes.initialize address x.attrs in
+    update ~attrs x
 end
 
 (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *)
@@ -193,6 +202,11 @@ module AddressAttributes = struct
     abduce_attribute addr (MustBeValid access_trace) astate
 
 
+  let check_initialized addr astate =
+    let+ () = BaseAddressAttributes.check_initialized addr (astate.post :> base_domain).attrs in
+    ()
+
+
   (** [astate] with [astate.post.attrs = f astate.post.attrs] *)
   let map_post_attrs ~f astate =
     let new_post = PostDomain.update astate.post ~attrs:(f (astate.post :> base_domain).attrs) in
@@ -299,12 +313,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) =
+  match typ.Typ.desc with
+  | Tint _ | Tfloat _ | Tptr _ ->
+      let {stack; attrs} = (post :> base_domain) in
+      let stack, addr, history =
+        match src with
+        | `LocalDecl (pvar, addr_opt) ->
+            let history = [ValueHistory.VariableDeclared (pvar, location)] in
+            let stack, addr =
+              match addr_opt with
+              | None ->
+                  let addr = AbstractValue.mk_fresh () in
+                  (BaseStack.add (Var.of_pvar pvar) (addr, history) stack, addr)
+              | Some addr ->
+                  (stack, addr)
+            in
+            (stack, addr, history)
+        | `Malloc (addr, history) ->
+            (stack, addr, history)
+      in
+      let attrs =
+        BaseAddressAttributes.add_one addr (Uninitialized (Immediate {location; history})) attrs
+      in
+      PostDomain.update ~stack ~attrs post
+  | Tstruct _ ->
+      (* TODO: set uninitialized attributes for fields *)
+      post
+  | Tarray _ ->
+      (* TODO: set uninitialized attributes for elements *)
+      post
+  | Tvoid | Tfun | TVar _ ->
+      (* We ignore tricky types to mark uninitialized addresses. *)
+      post
+
+
+let set_uninitialized src typ location x =
+  {x with post= set_uninitialized_post src typ location x.post}
+
+
 let mk_initial 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
+  let location = Procdesc.get_loc proc_desc in
   let formals_and_captured =
-    let proc_name = Procdesc.get_proc_name proc_desc in
-    let location = Procdesc.get_loc proc_desc in
     let init_var mangled =
       let pvar = Pvar.mk mangled proc_name in
       (Var.of_pvar pvar, (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]))
@@ -328,7 +381,12 @@ let mk_initial proc_desc =
     in
     PreDomain.update ~stack:initial_stack ~heap:initial_heap PreDomain.empty
   in
+  let locals = Procdesc.get_locals proc_desc in
   let post = PostDomain.update ~stack:initial_stack PostDomain.empty 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 )
+  in
   { pre
   ; post
   ; topl= PulseTopl.start ()
@@ -519,6 +577,8 @@ let get_pre {pre} = (pre :> BaseDomain.t)
 
 let get_post {post} = (post :> BaseDomain.t)
 
+let initialize address x = {x with post= PostDomain.initialize address x.post}
+
 (* re-exported for mli *)
 let incorporate_new_eqs astate (phi, new_eqs) =
   if PathCondition.is_unsat_cheap phi then phi

infer/src/pulse/PulseAbductiveDomain.mli

@@ -126,6 +126,8 @@ module AddressAttributes : sig
 
   val check_valid : Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t * Trace.t) result
 
+  val check_initialized : AbstractValue.t -> t -> (unit, Trace.t) result
+
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
   val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
@@ -180,6 +182,20 @@ val incorporate_new_eqs : t -> PathCondition.t * PathCondition.new_eqs -> PathCo
     and [y] being allocated separately. In those cases, the resulting path condition is
     {!PathCondition.false_}. *)
 
+val initialize : AbstractValue.t -> t -> t
+(** Remove "Uninitialized" attribute of the given address *)
+
+val set_uninitialized :
+     [ `LocalDecl of Pvar.t * AbstractValue.t option
+       (** the second optional parameter is for the address of the variable *)
+     | `Malloc of AbstractValue.t * ValueHistory.t
+       (** the address parameter is a newly allocated address *) ]
+  -> Typ.t
+  -> Location.t
+  -> t
+  -> t
+(** Add "Uninitialized" attributes when a variable is declared or a memory is allocated by malloc. *)
+
 module Topl : sig
   val small_step : Location.t -> PulseTopl.event -> t -> t
 

infer/src/pulse/PulseAttribute.ml

@@ -34,6 +34,7 @@ module Attribute = struct
     | Invalid of Invalidation.t * Trace.t
     | MustBeValid of Trace.t
     | StdVectorReserve
+    | Uninitialized of Trace.t
     | WrittenTo of Trace.t
   [@@deriving compare, variants]
 
@@ -70,6 +71,8 @@ module Attribute = struct
 
   let end_of_collection_rank = Variants.to_rank EndOfCollection
 
+  let uninitialized_rank = Variants.to_rank (Uninitialized dummy_trace)
+
   let pp f attribute =
     let pp_string_if_debug string fmt =
       if Config.debug_level_analysis >= 3 then F.pp_print_string fmt string
@@ -98,6 +101,10 @@ module Attribute = struct
         F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace
     | StdVectorReserve ->
         F.pp_print_string f "std::vector::reserve()"
+    | Uninitialized trace ->
+        F.fprintf f "Uninitialized %a"
+          (Trace.pp ~pp_immediate:(pp_string_if_debug "declaration"))
+          trace
     | WrittenTo trace ->
         F.fprintf f "WrittenTo %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "mutation")) trace
 end
@@ -167,6 +174,13 @@ module Attributes = struct
            typ )
 
 
+  let get_uninitialized attrs =
+    Set.find_rank attrs Attribute.uninitialized_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.Uninitialized trace) = attr in
+           trace )
+
+
   include Set
 end
 
@@ -183,6 +197,7 @@ let is_suitable_for_pre = function
   | EndOfCollection
   | Invalid _
   | StdVectorReserve
+  | Uninitialized _
   | WrittenTo _ ->
       false
 
@@ -194,6 +209,8 @@ let map_trace ~f = function
       Invalid (invalidation, f trace)
   | MustBeValid trace ->
       MustBeValid (f trace)
+  | Uninitialized trace ->
+      Uninitialized (f trace)
   | WrittenTo trace ->
       WrittenTo (f trace)
   | ( AddressOfCppTemporary _

infer/src/pulse/PulseAttribute.mli

@@ -21,6 +21,7 @@ type t =
   | Invalid of Invalidation.t * Trace.t
   | MustBeValid of Trace.t
   | StdVectorReserve
+  | Uninitialized of Trace.t
   | WrittenTo of Trace.t
 [@@deriving compare]
 
@@ -53,4 +54,6 @@ module Attributes : sig
   val is_modified : t -> bool
 
   val is_std_vector_reserved : t -> bool
+
+  val get_uninitialized : t -> Trace.t option
 end

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -85,6 +85,15 @@ let check_valid address attrs =
       Error invalidation
 
 
+let check_initialized address attrs =
+  L.d_printfln "Checking if %a is initialized" AbstractValue.pp address ;
+  match Graph.find_opt address attrs |> Option.bind ~f:Attributes.get_uninitialized with
+  | Some trace ->
+      Error trace
+  | None ->
+      Ok ()
+
+
 let get_attribute getter address attrs =
   let open Option.Monad_infix in
   Graph.find_opt address attrs >>= getter
@@ -98,6 +107,14 @@ let remove_allocation_attr address memory =
       memory
 
 
+let initialize address attrs =
+  match get_attribute Attributes.get_uninitialized address attrs with
+  | Some trace ->
+      remove_one address (Attribute.Uninitialized trace) attrs
+  | None ->
+      attrs
+
+
 let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
 
 let get_must_be_valid = get_attribute Attributes.get_must_be_valid

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -31,6 +31,8 @@ val fold : (AbstractValue.t -> Attributes.t -> 'a -> 'a) -> t -> 'a -> 'a
 
 val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t * Trace.t) result
 
+val check_initialized : AbstractValue.t -> t -> (unit, Trace.t) result
+
 val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
 val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
@@ -48,3 +50,5 @@ val is_end_of_collection : AbstractValue.t -> t -> bool
 val pp : F.formatter -> t -> unit
 
 val remove_allocation_attr : AbstractValue.t -> t -> t
+
+val initialize : AbstractValue.t -> t -> t

infer/src/pulse/PulseBaseDomain.ml

@@ -190,9 +190,9 @@ module GraphVisit : sig
     -> t
     -> init:'accum
     -> f:
-         (   'accum
+         (   Var.t
+          -> 'accum
           -> AbstractValue.t
-          -> Var.t
           -> Memory.Access.t list
           -> ('accum, 'final) Base.Continue_or_stop.t)
     -> finish:('accum -> 'final)
@@ -202,6 +202,19 @@ module GraphVisit : sig
       set of addresses that have been visited before [f] returned [Stop] or all reachable addresses
       were seen. [f] is passed each address together with the variable from which the address was
       reached and the access path from that variable to the address. *)
+
+  val fold_from_addresses :
+       AbstractValue.t list
+    -> t
+    -> init:'accum
+    -> f:
+         (   'accum
+          -> AbstractValue.t
+          -> Memory.Access.t list
+          -> ('accum, 'final) Base.Continue_or_stop.t)
+    -> finish:('accum -> 'final)
+    -> AbstractValue.Set.t * 'final
+  (** Similar to [fold], but start from given addresses, instead of stack variables. *)
 end = struct
   open Base.Continue_or_stop
 
@@ -212,41 +225,53 @@ end = struct
       `NotAlreadyVisited visited
 
 
-  let rec visit_address orig_var ~f rev_accesses astate address ((visited, accum) as visited_accum)
-      =
+  let rec visit_address address ~f rev_accesses astate ((visited, accum) as visited_accum) =
     match visit address visited with
     | `AlreadyVisited ->
         Continue visited_accum
     | `NotAlreadyVisited visited -> (
-      match f accum address orig_var rev_accesses with
+      match f accum address rev_accesses with
       | Continue accum -> (
         match Memory.find_opt address astate.heap with
         | None ->
             Continue (visited, accum)
         | Some edges ->
-            visit_edges orig_var ~f rev_accesses astate ~edges (visited, accum) )
+            visit_edges edges ~f rev_accesses astate (visited, accum) )
       | Stop fin ->
           Stop (visited, fin) )
 
 
-  and visit_edges orig_var ~f rev_accesses ~edges astate visited_accum =
+  and visit_edges edges ~f rev_accesses astate visited_accum =
     let finish visited_accum = Continue visited_accum in
     Container.fold_until edges ~fold:Memory.Edges.fold ~finish ~init:visited_accum
       ~f:(fun visited_accum (access, (address, _trace)) ->
-        match visit_address orig_var ~f (access :: rev_accesses) astate address visited_accum with
+        match visit_address address ~f (access :: rev_accesses) astate visited_accum with
         | Continue _ as cont ->
             cont
         | Stop fin ->
             Stop (Stop fin) )
 
 
-  let fold ~var_filter astate ~init ~f ~finish =
+  let visit_address_from_var (orig_var, (address, _loc)) ~f rev_accesses astate visited_accum =
+    visit_address address ~f:(f orig_var) rev_accesses astate visited_accum
+
+
+  let fold_common x astate ~fold ~filter ~visit ~init ~f ~finish =
     let finish (visited, accum) = (visited, finish accum) in
     let init = (AbstractValue.Set.empty, init) in
-    Container.fold_until astate.stack ~fold:(IContainer.fold_of_pervasives_map_fold Stack.fold)
-      ~init ~finish ~f:(fun visited_accum (var, (address, _loc)) ->
-        if var_filter var then visit_address var ~f [] astate address visited_accum
-        else Continue visited_accum )
+    Container.fold_until x ~fold ~init ~finish ~f:(fun visited_accum elem ->
+        if filter elem then visit elem ~f [] astate visited_accum else Continue visited_accum )
+
+
+  let fold ~var_filter astate =
+    fold_common astate.stack astate
+      ~fold:(IContainer.fold_of_pervasives_map_fold Stack.fold)
+      ~filter:(fun (var, _) -> var_filter var)
+      ~visit:visit_address_from_var
+
+
+  let fold_from_addresses from astate =
+    fold_common from astate ~fold:List.fold ~filter:(fun _ -> true) ~visit:visit_address
 end
 
 include GraphComparison
@@ -255,5 +280,11 @@ let reachable_addresses astate =
   GraphVisit.fold astate
     ~var_filter:(fun _ -> true)
     ~init:() ~finish:Fn.id
-    ~f:(fun () _ _ _ -> Continue ())
+    ~f:(fun _ () _ _ -> Continue ())
+  |> fst
+
+
+let reachable_addresses_from addresses astate =
+  GraphVisit.fold_from_addresses addresses astate ~init:() ~finish:Fn.id ~f:(fun () _ _ ->
+      Continue () )
   |> fst

infer/src/pulse/PulseBaseDomain.mli

@@ -20,6 +20,9 @@ val reachable_addresses : t -> AbstractValue.Set.t
 (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable from
     the stack variables *)
 
+val reachable_addresses_from : AbstractValue.t list -> t -> AbstractValue.Set.t
+(** compute the set of abstract addresses that are reachable from given abstract addresses *)
+
 type mapping
 
 val empty_mapping : mapping

infer/src/pulse/PulseInvalidation.ml

@@ -50,6 +50,7 @@ type t =
   | OptionalEmpty
   | StdVector of std_vector_function
   | JavaIterator of java_iterator_function
+  | Uninitialized
 [@@deriving compare, equal]
 
 let issue_type_of_cause = function
@@ -69,6 +70,8 @@ let issue_type_of_cause = function
       IssueType.optional_empty_access
   | JavaIterator _ | StdVector _ ->
       IssueType.vector_invalidation
+  | Uninitialized ->
+      IssueType.uninitialized_value_pulse
 
 
 let describe f cause =
@@ -96,6 +99,8 @@ let describe f cause =
       F.fprintf f "was potentially invalidated by `%a()`" pp_std_vector_function std_vector_f
   | JavaIterator java_iterator_f ->
       F.fprintf f "was potentially invalidated by `%a()`" pp_java_iterator_function java_iterator_f
+  | Uninitialized ->
+      F.pp_print_string f "was uninitialized"
 
 
 let pp f invalidation =
@@ -112,3 +117,5 @@ let pp f invalidation =
       F.fprintf f "StdVector(%a)" describe invalidation
   | JavaIterator _ ->
       F.fprintf f "JavaIterator(%a)" describe invalidation
+  | Uninitialized ->
+      F.pp_print_string f "Uninitialized"

infer/src/pulse/PulseInvalidation.mli

@@ -31,6 +31,7 @@ type t =
   | OptionalEmpty
   | StdVector of std_vector_function
   | JavaIterator of java_iterator_function
+  | Uninitialized
 [@@deriving compare, equal]
 
 val pp : F.formatter -> t -> unit

infer/src/pulse/PulseModels.ml

@@ -36,7 +36,9 @@ module Misc = struct
 
 
   let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate =
-    let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
+    let* astate, obj =
+      PulseOperations.eval_access Read location src_pointer_hist Dereference astate
+    in
     shallow_copy_value location event ret_id dest_pointer_hist obj astate
 
 
@@ -133,7 +135,14 @@ end
 module C = struct
   let free deleted_access : model = Misc.free_or_delete `Free deleted_access
 
-  let malloc _ : model =
+  let set_uninitialized 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 ) )
+
+
+  let malloc_common ~size_exp_opt : model =
    fun _ ~callee_procname location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let ret_value =
@@ -143,6 +152,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_value
     in
     let+ astate_null =
       PulseArithmetic.and_eq_int ret_addr IntLit.zero astate
@@ -151,16 +161,28 @@ module C = struct
     [ExecutionDomain.ContinueProgram astate_alloc; ExecutionDomain.ContinueProgram astate_null]
 
 
-  let malloc_not_null _ : model =
+  let malloc_not_null_common ~size_exp_opt : model =
    fun _ ~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}])
     in
     let astate = PulseOperations.write_id ret_id ret_value astate in
-    PulseOperations.allocate callee_procname location ret_value astate
-    |> PulseArithmetic.and_positive ret_addr
-    |> ok_continue
+    let astate =
+      PulseOperations.allocate callee_procname location ret_value astate
+      |> PulseArithmetic.and_positive ret_addr
+      |> set_uninitialized size_exp_opt location ret_value
+    in
+    ok_continue astate
+
+
+  let malloc size_exp = malloc_common ~size_exp_opt:(Some size_exp)
+
+  let malloc_no_param = malloc_common ~size_exp_opt:None
+
+  let malloc_not_null size_exp = malloc_not_null_common ~size_exp_opt:(Some size_exp)
+
+  let malloc_not_null_no_param = malloc_not_null_common ~size_exp_opt:None
 end
 
 module ObjCCoreFoundation = struct
@@ -193,18 +215,18 @@ module Optional = struct
 
   let internal_value_access = HilExp.Access.FieldAccess internal_value
 
-  let to_internal_value location optional astate =
-    PulseOperations.eval_access location optional internal_value_access astate
+  let to_internal_value mode location optional astate =
+    PulseOperations.eval_access mode location optional internal_value_access astate
 
 
-  let to_internal_value_deref location optional astate =
-    let* astate, pointer = to_internal_value location optional astate in
-    PulseOperations.eval_access location pointer Dereference astate
+  let to_internal_value_deref mode location optional astate =
+    let* astate, pointer = to_internal_value Read location optional astate in
+    PulseOperations.eval_access mode location pointer Dereference astate
 
 
   let write_value location this ~value ~desc astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, value_field = to_internal_value location this astate in
+    let* astate, value_field = to_internal_value Read location this astate in
     let value_hist = (fst value, event :: snd value) in
     let+ astate = PulseOperations.write_deref location ~ref:value_field ~obj:value_hist astate in
     (astate, value_hist)
@@ -232,7 +254,7 @@ module Optional = struct
 
   let assign_optional_value this init ~desc : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let* astate, value = to_internal_value_deref location init astate in
+    let* astate, value = to_internal_value_deref Read location init astate in
     let+ astate, _ = write_value location this ~value ~desc astate in
     [ExecutionDomain.ContinueProgram astate]
 
@@ -247,10 +269,10 @@ module Optional = struct
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let* astate, ((value_addr, value_hist) as value) =
-      to_internal_value_deref location optional astate
+      to_internal_value_deref Write location optional astate
     in
     (* Check dereference to show an error at the callsite of `value()` *)
-    let* astate, _ = PulseOperations.eval_access location value Dereference astate in
+    let* astate, _ = PulseOperations.eval_access Write location value Dereference astate in
     PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate |> ok_continue
 
 
@@ -258,7 +280,7 @@ module Optional = struct
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in
-    let+ astate, (value_addr, _) = to_internal_value_deref location optional astate in
+    let+ astate, (value_addr, _) = to_internal_value_deref Read location optional astate in
     let astate = PulseOperations.write_id ret_id ret_value astate in
     let astate_non_empty = PulseArithmetic.and_positive value_addr astate in
     let astate_true = PulseArithmetic.and_positive ret_addr astate_non_empty in
@@ -270,7 +292,7 @@ module Optional = struct
   let get_pointer optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, value_addr = to_internal_value_deref location optional astate in
+    let* astate, value_addr = to_internal_value_deref Read location optional astate in
     let value_update_hist = (fst value_addr, event :: snd value_addr) in
     let astate_value_addr =
       PulseOperations.write_id ret_id value_update_hist astate
@@ -289,15 +311,15 @@ module Optional = struct
   let value_or optional default ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, value_addr = to_internal_value_deref location optional astate in
+    let* astate, value_addr = to_internal_value_deref Read location optional astate in
     let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in
     let* astate_non_empty, value =
-      PulseOperations.eval_access location value_addr Dereference astate_non_empty
+      PulseOperations.eval_access Read location value_addr Dereference astate_non_empty
     in
     let value_update_hist = (fst value, event :: snd value) in
     let astate_value = PulseOperations.write_id ret_id value_update_hist astate_non_empty in
     let+ astate, (default_val, default_hist) =
-      PulseOperations.eval_access location default Dereference astate
+      PulseOperations.eval_access Read location default Dereference astate
     in
     let default_value_hist = (default_val, event :: default_hist) in
     let astate_empty = PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero astate in
@@ -327,11 +349,11 @@ module StdAtomicInteger = struct
 
 
   let load_backing_int location this astate =
-    let* astate, obj = PulseOperations.eval_access location this Dereference astate in
+    let* astate, obj = PulseOperations.eval_access Read location this Dereference astate in
     let* astate, int_addr =
-      PulseOperations.eval_access location obj (FieldAccess internal_int) astate
+      PulseOperations.eval_access Read location obj (FieldAccess internal_int) astate
     in
-    let+ astate, int_val = PulseOperations.eval_access location int_addr Dereference astate in
+    let+ astate, int_val = PulseOperations.eval_access Read location int_addr Dereference astate in
     (astate, int_addr, int_val)
 
 
@@ -340,7 +362,7 @@ module StdAtomicInteger = struct
     let event = ValueHistory.Call {f= Model "std::atomic::atomic()"; location; in_call= []} in
     let this = (AbstractValue.mk_fresh (), [event]) in
     let* astate, int_field =
-      PulseOperations.eval_access location this (FieldAccess internal_int) astate
+      PulseOperations.eval_access Write location this (FieldAccess internal_int) astate
     in
     let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in
     let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in
@@ -433,9 +455,9 @@ module StdAtomicInteger = struct
   let operator_t = load_instr "std::atomic<T>::operator_T()"
 
   let store_backing_int location this_address new_value astate =
-    let* astate, this = PulseOperations.eval_access location this_address Dereference astate in
+    let* astate, this = PulseOperations.eval_access Read location this_address Dereference astate in
     let* astate, int_field =
-      PulseOperations.eval_access location this (FieldAccess internal_int) astate
+      PulseOperations.eval_access Write location this (FieldAccess internal_int) astate
     in
     PulseOperations.write_deref location ~ref:int_field ~obj:new_value astate
 
@@ -461,7 +483,9 @@ module JavaObject = struct
   let clone src_pointer_hist : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in
-    let* astate, obj = PulseOperations.eval_access location src_pointer_hist Dereference astate in
+    let* astate, obj =
+      PulseOperations.eval_access Read location src_pointer_hist Dereference astate
+    in
     let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in
     let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in
     [ExecutionDomain.ContinueProgram astate]
@@ -477,7 +501,7 @@ module StdBasicString = struct
   let internal_string_access = HilExp.Access.FieldAccess internal_string
 
   let to_internal_string location bstring astate =
-    PulseOperations.eval_access location bstring internal_string_access astate
+    PulseOperations.eval_access Read location bstring internal_string_access astate
 
 
   let data this_hist : model =
@@ -485,7 +509,7 @@ module StdBasicString = struct
     let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in
     let* astate, string_addr_hist = to_internal_string location this_hist astate in
     let+ astate, (string, hist) =
-      PulseOperations.eval_access location string_addr_hist Dereference astate
+      PulseOperations.eval_access Read location string_addr_hist Dereference astate
     in
     let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in
     [ExecutionDomain.ContinueProgram astate]
@@ -513,7 +537,7 @@ module StdFunction = struct
       [PulseOperations.havoc_id ret_id [event] astate]
     in
     let* astate, (lambda, _) =
-      PulseOperations.eval_access location lambda_ptr_hist Dereference astate
+      PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate
     in
     let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in
     match AddressAttributes.get_closure_proc_name lambda astate with
@@ -560,22 +584,24 @@ module GenericArrayBackedCollection = struct
 
   let access = HilExp.Access.FieldAccess field
 
-  let eval location collection astate =
-    PulseOperations.eval_access location collection access astate
+  let eval mode location collection astate =
+    PulseOperations.eval_access mode location collection access astate
 
 
   let eval_element location internal_array index astate =
-    PulseOperations.eval_access location internal_array (ArrayAccess (StdTyp.void, index)) astate
+    PulseOperations.eval_access Read location internal_array
+      (ArrayAccess (StdTyp.void, index))
+      astate
 
 
   let element location collection index astate =
-    let* astate, internal_array = eval location collection astate in
+    let* astate, internal_array = eval Read location collection astate in
     eval_element location internal_array index astate
 
 
   let eval_pointer_to_last_element location collection astate =
     let+ astate, pointer =
-      PulseOperations.eval_access location collection (FieldAccess last_field) astate
+      PulseOperations.eval_access Write location collection (FieldAccess last_field) astate
     in
     let astate = AddressAttributes.mark_as_end_of_collection (fst pointer) astate in
     (astate, pointer)
@@ -586,19 +612,19 @@ module GenericArrayBackedCollectionIterator = struct
 
   let internal_pointer_access = HilExp.Access.FieldAccess internal_pointer
 
-  let to_internal_pointer location iterator astate =
-    PulseOperations.eval_access location iterator internal_pointer_access astate
+  let to_internal_pointer mode location iterator astate =
+    PulseOperations.eval_access mode location iterator internal_pointer_access astate
 
 
-  let to_internal_pointer_deref location iterator astate =
-    let* astate, pointer = to_internal_pointer location iterator astate in
-    let+ astate, index = PulseOperations.eval_access location pointer Dereference astate in
+  let to_internal_pointer_deref mode location iterator astate =
+    let* astate, pointer = to_internal_pointer Read location iterator astate in
+    let+ astate, index = PulseOperations.eval_access mode location pointer Dereference astate in
     (astate, pointer, index)
 
 
-  let to_elem_pointed_by_iterator ?(step = None) location iterator astate =
-    let* astate, pointer = to_internal_pointer location iterator astate in
-    let* astate, index = PulseOperations.eval_access location pointer Dereference astate in
+  let to_elem_pointed_by_iterator mode ?(step = None) location iterator astate =
+    let* astate, pointer = to_internal_pointer Read location iterator astate in
+    let* astate, index = PulseOperations.eval_access mode location pointer Dereference astate in
     (* Check if not end iterator *)
     let is_minus_minus = match step with Some `MinusMinus -> true | _ -> false in
     let* astate =
@@ -612,19 +638,21 @@ module GenericArrayBackedCollectionIterator = struct
       else Ok astate
     in
     (* We do not want to create internal array if iterator pointer has an invalid value *)
-    let* astate = PulseOperations.check_addr_access location index astate in
+    let* astate = PulseOperations.check_addr_access Read location index astate in
     let+ astate, elem = GenericArrayBackedCollection.element location iterator (fst index) astate in
     (astate, pointer, elem)
 
 
   let construct location event ~init ~ref astate =
-    let* astate, (arr_addr, arr_hist) = GenericArrayBackedCollection.eval location init astate in
+    let* astate, (arr_addr, arr_hist) =
+      GenericArrayBackedCollection.eval Read location init astate
+    in
     let* astate =
       PulseOperations.write_field location ~ref GenericArrayBackedCollection.field
         ~obj:(arr_addr, event :: arr_hist)
         astate
     in
-    let* astate, (p_addr, p_hist) = to_internal_pointer location init astate in
+    let* astate, (p_addr, p_hist) = to_internal_pointer Read location init astate in
     PulseOperations.write_field location ~ref internal_pointer ~obj:(p_addr, event :: p_hist) astate
 
 
@@ -637,8 +665,8 @@ module GenericArrayBackedCollectionIterator = struct
   let operator_compare comparison ~desc iter_lhs iter_rhs _ ~callee_procname:_ location
       ~ret:(ret_id, _) astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, _, (index_lhs, _) = to_internal_pointer_deref location iter_lhs astate in
-    let+ astate, _, (index_rhs, _) = to_internal_pointer_deref location iter_rhs astate in
+    let* astate, _, (index_lhs, _) = to_internal_pointer_deref Read location iter_lhs astate in
+    let+ astate, _, (index_rhs, _) = to_internal_pointer_deref Read location iter_rhs astate in
     let ret_val = AbstractValue.mk_fresh () in
     let astate = PulseOperations.write_id ret_id (ret_val, [event]) astate in
     let ret_val_equal, ret_val_notequal =
@@ -663,7 +691,7 @@ module GenericArrayBackedCollectionIterator = struct
 
   let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let+ astate, pointer, (elem, _) = to_elem_pointed_by_iterator location iter astate in
+    let+ astate, pointer, (elem, _) = to_elem_pointed_by_iterator Read location iter astate in
     let astate = PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate in
     [ExecutionDomain.ContinueProgram astate]
 
@@ -671,7 +699,9 @@ module GenericArrayBackedCollectionIterator = struct
   let operator_step step ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let index_new = AbstractValue.mk_fresh () in
-    let* astate, pointer, _ = to_elem_pointed_by_iterator ~step:(Some step) location iter astate in
+    let* astate, pointer, _ =
+      to_elem_pointed_by_iterator Read ~step:(Some step) location iter astate
+    in
     PulseOperations.write_deref location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate
     >>| ExecutionDomain.continue >>| List.return
 end
@@ -691,7 +721,7 @@ module JavaIterator = struct
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let new_index = AbstractValue.mk_fresh () in
     let* astate, (curr_index, curr_index_hist) =
-      GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate
+      GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate
     in
     let* astate, (curr_elem_val, curr_elem_hist) =
       GenericArrayBackedCollection.element location iter curr_index astate
@@ -713,7 +743,7 @@ module JavaIterator = struct
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let new_index = AbstractValue.mk_fresh () in
     let* astate, (curr_index, curr_index_hist) =
-      GenericArrayBackedCollectionIterator.to_internal_pointer location iter astate
+      GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate
     in
     let* astate =
       PulseOperations.write_field location ~ref:iter
@@ -722,7 +752,7 @@ module JavaIterator = struct
         astate
     in
     let new_elem = AbstractValue.mk_fresh () in
-    let* astate, arr = GenericArrayBackedCollection.eval location iter astate in
+    let* astate, arr = GenericArrayBackedCollection.eval Read location iter astate in
     let+ astate =
       PulseOperations.write_arr_index location ~ref:arr ~index:curr_index
         ~obj:(new_elem, event :: curr_index_hist)
@@ -733,7 +763,9 @@ end
 
 module StdVector = struct
   let reallocate_internal_array trace vector vector_f location astate =
-    let* astate, array_address = GenericArrayBackedCollection.eval location vector astate in
+    let* astate, array_address =
+      GenericArrayBackedCollection.eval NoAccess location vector astate
+    in
     PulseOperations.invalidate_array_elements location (StdVector vector_f) array_address astate
     >>= PulseOperations.invalidate_access location (StdVector vector_f) vector
           GenericArrayBackedCollection.access
@@ -781,7 +813,7 @@ module StdVector = struct
     let index_zero = AbstractValue.mk_fresh () in
     let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in
     let* astate, ((arr_addr, _) as arr) =
-      GenericArrayBackedCollection.eval location vector astate
+      GenericArrayBackedCollection.eval Read location vector astate
     in
     let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in
     PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
@@ -795,7 +827,7 @@ module StdVector = struct
   let vector_end vector iter : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::vector::end()"; location; in_call= []} in
-    let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval location vector astate in
+    let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval Read location vector astate in
     let* astate, (pointer_addr, _) =
       GenericArrayBackedCollection.eval_pointer_to_last_element location vector astate
     in
@@ -838,7 +870,7 @@ module JavaCollection = struct
   let set coll (index, _) (new_elem, new_elem_hist) : model =
    fun _ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in
-    let* astate, arr = GenericArrayBackedCollection.eval location coll astate in
+    let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
     let* astate, (old_addr, old_hist) =
       GenericArrayBackedCollection.element location coll index astate
     in
@@ -855,7 +887,7 @@ module JavaCollection = struct
   let add_at coll (index, _) (new_elem, new_elem_hist) : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in
-    let* astate, arr = GenericArrayBackedCollection.eval location coll astate in
+    let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
     let+ astate =
       PulseOperations.write_arr_index location ~ref:arr ~index
         ~obj:(new_elem, event :: new_elem_hist)
@@ -874,7 +906,7 @@ module JavaCollection = struct
   let remove_at coll (index, _) : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in
-    let* astate, arr = GenericArrayBackedCollection.eval location coll astate in
+    let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
     let fresh_elem = AbstractValue.mk_fresh () in
     let+ astate =
       PulseOperations.write_arr_index location ~ref:arr ~index
@@ -943,7 +975,7 @@ module ProcNameDispatcher = struct
     make_dispatcher
       ( transfer_ownership_matchers @ abort_matchers @ return_nonnull_matchers
       @ [ +match_builtin BuiltinDecl.free <>$ capt_arg_payload $--> C.free
-        ; +match_builtin BuiltinDecl.malloc <>$ capt_arg_payload $--> C.malloc
+        ; +match_builtin BuiltinDecl.malloc <>$ capt_exp $--> C.malloc
         ; +match_builtin BuiltinDecl.__delete <>$ capt_arg_payload $--> Cplusplus.delete
         ; +match_builtin BuiltinDecl.__new &--> Misc.return_positive ~desc:"new"
         ; +match_builtin BuiltinDecl.__placement_new &++> Cplusplus.placement_new
@@ -1199,10 +1231,13 @@ module ProcNameDispatcher = struct
           &:: "nextElement" <>$ capt_arg_payload
           $!--> fun x ->
           StdVector.at ~desc:"Enumeration.nextElement" x (AbstractValue.mk_fresh (), []) )
-        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy &++> C.malloc
-        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_foundation_create_or_copy &++> C.malloc
-        ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_arg_payload $--> C.malloc_not_null
-        ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_alloc &++> C.malloc_not_null
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_create_or_copy
+          &--> C.malloc_no_param
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_core_foundation_create_or_copy
+          &--> C.malloc_no_param
+        ; +match_builtin BuiltinDecl.malloc_no_fail <>$ capt_exp $--> C.malloc_not_null
+        ; +map_context_tenv PatternMatch.ObjectiveC.is_modelled_as_alloc
+          &--> C.malloc_not_null_no_param
         ; +map_context_tenv PatternMatch.ObjectiveC.is_core_graphics_release
           <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release
         ; -"CFRelease" <>$ capt_arg_payload $--> ObjCCoreFoundation.cf_bridging_release

infer/src/pulse/PulseOperations.ml

@@ -14,13 +14,34 @@ type t = AbductiveDomain.t
 
 type 'a access_result = 'a PulseReport.access_result
 
-let check_addr_access location (address, history) astate =
+type access_mode = Read | Write | NoAccess
+
+let check_addr_access access_mode location (address, history) astate =
   let access_trace = Trace.Immediate {location; history} in
-  AddressAttributes.check_valid access_trace address astate
-  |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
-         ( Diagnostic.AccessToInvalidAddress
-             {calling_context= []; invalidation; invalidation_trace; access_trace}
-         , astate ) )
+  let* astate =
+    AddressAttributes.check_valid access_trace address astate
+    |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
+           ( Diagnostic.AccessToInvalidAddress
+               {calling_context= []; invalidation; invalidation_trace; access_trace}
+           , astate ) )
+  in
+  match access_mode with
+  | Read ->
+      let+ () =
+        AddressAttributes.check_initialized address astate
+        |> Result.map_error ~f:(fun invalidation_trace ->
+               ( Diagnostic.AccessToInvalidAddress
+                   { calling_context= []
+                   ; invalidation= Uninitialized
+                   ; invalidation_trace
+                   ; access_trace }
+               , astate ) )
+      in
+      astate
+  | Write ->
+      Ok (AbductiveDomain.initialize address astate)
+  | NoAccess ->
+      Ok astate
 
 
 module Closures = struct
@@ -70,7 +91,7 @@ module Closures = struct
             | Attribute.Closure _ ->
                 IContainer.iter_result ~fold:Memory.Edges.fold edges ~f:(fun (access, addr_trace) ->
                     if is_captured_by_ref_fake_access access then
-                      let+ _ = check_addr_access action addr_trace astate in
+                      let+ _ = check_addr_access Read action addr_trace astate in
                       ()
                     else Ok () )
             | _ ->
@@ -97,35 +118,35 @@ end
 
 let eval_var var astate = Stack.eval var astate
 
-let eval_access location addr_hist access astate =
-  let+ astate = check_addr_access location addr_hist astate in
+let eval_access mode location addr_hist access astate =
+  let+ astate = check_addr_access mode location addr_hist astate in
   Memory.eval_edge addr_hist access astate
 
 
-let eval location exp0 astate =
-  let rec eval exp astate =
+let eval mode location exp0 astate =
+  let rec eval mode exp astate =
     match (exp : Exp.t) with
     | Var id ->
         Ok (eval_var (* error in case of missing history? *) [] (Var.of_id id) astate)
     | Lvar pvar ->
         Ok (eval_var [ValueHistory.VariableAccessed (pvar, location)] (Var.of_pvar pvar) astate)
     | Lfield (exp', field, _) ->
-        let* astate, addr_hist = eval exp' astate in
-        eval_access location addr_hist (FieldAccess field) astate
+        let* astate, addr_hist = eval Read exp' astate in
+        eval_access mode location addr_hist (FieldAccess field) astate
     | Lindex (exp', exp_index) ->
-        let* astate, addr_hist_index = eval exp_index astate in
-        let* astate, addr_hist = eval exp' astate in
-        eval_access location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate
+        let* astate, addr_hist_index = eval Read exp_index astate in
+        let* astate, addr_hist = eval Read exp' astate in
+        eval_access mode location addr_hist (ArrayAccess (StdTyp.void, fst addr_hist_index)) astate
     | Closure {name; captured_vars} ->
         let+ astate, rev_captured =
           List.fold_result captured_vars ~init:(astate, [])
             ~f:(fun (astate, rev_captured) (capt_exp, captured_as, _, mode) ->
-              let+ astate, addr_trace = eval capt_exp astate in
+              let+ astate, addr_trace = eval Read capt_exp astate in
               (astate, (captured_as, addr_trace, mode) :: rev_captured) )
         in
         Closures.record location name (List.rev rev_captured) astate
     | Cast (_, exp') ->
-        eval exp' astate
+        eval mode exp' astate
     | Const (Cint i) ->
         let v = AbstractValue.Constants.get_int i in
         let astate =
@@ -136,13 +157,13 @@ let eval location exp0 astate =
         in
         Ok (astate, (v, []))
     | UnOp (unop, exp, _typ) ->
-        let+ astate, (addr, hist) = eval exp astate in
+        let+ astate, (addr, hist) = eval Read exp astate in
         let unop_addr = AbstractValue.mk_fresh () in
         (PulseArithmetic.eval_unop unop_addr unop addr astate, (unop_addr, hist))
     | BinOp (bop, e_lhs, e_rhs) ->
-        let* astate, (addr_lhs, hist_lhs) = eval e_lhs astate in
+        let* astate, (addr_lhs, hist_lhs) = eval Read e_lhs astate in
         (* NOTE: keeping track of only [hist_lhs] into the binop is not the best *)
-        let+ astate, (addr_rhs, _hist_rhs) = eval e_rhs astate in
+        let+ astate, (addr_rhs, _hist_rhs) = eval Read e_rhs astate in
         let binop_addr = AbstractValue.mk_fresh () in
         ( PulseArithmetic.eval_binop binop_addr bop (AbstractValueOperand addr_lhs)
             (AbstractValueOperand addr_rhs) astate
@@ -150,15 +171,15 @@ let eval location exp0 astate =
     | Const _ | Sizeof _ | Exn _ ->
         Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
-  eval exp0 astate
+  eval mode exp0 astate
 
 
-let eval_to_operand location exp astate =
+let eval_to_operand mode location exp astate =
   match (exp : Exp.t) with
   | Const (Cint i) ->
       Ok (astate, PulseArithmetic.LiteralOperand i)
   | exp ->
-      let+ astate, (value, _) = eval location exp astate in
+      let+ astate, (value, _) = eval mode location exp astate in
       (astate, PulseArithmetic.AbstractValueOperand value)
 
 
@@ -166,8 +187,8 @@ let prune location ~condition astate =
   let rec prune_aux ~negated exp astate =
     match (exp : Exp.t) with
     | BinOp (bop, exp_lhs, exp_rhs) ->
-        let* astate, lhs_op = eval_to_operand location exp_lhs astate in
-        let+ astate, rhs_op = eval_to_operand location exp_rhs astate in
+        let* astate, lhs_op = eval_to_operand Read location exp_lhs astate in
+        let+ astate, rhs_op = eval_to_operand Read location exp_rhs astate in
         PulseArithmetic.prune_binop ~negated bop lhs_op rhs_op astate
     | UnOp (LNot, exp', _) ->
         prune_aux ~negated:(not negated) exp' astate
@@ -178,15 +199,17 @@ let prune location ~condition astate =
 
 
 let eval_deref location exp astate =
-  let* astate, addr_hist = eval location exp astate in
-  let+ astate = check_addr_access location addr_hist astate in
+  let* astate, addr_hist = eval Read location exp astate in
+  let+ astate = check_addr_access Read location addr_hist astate in
   Memory.eval_edge addr_hist Dereference astate
 
 
-let realloc_pvar pvar location astate =
-  Stack.add (Var.of_pvar pvar)
-    (AbstractValue.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)])
-    astate
+let realloc_pvar 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
 
 
 let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate
@@ -199,7 +222,7 @@ let havoc_id id loc_opt astate =
 
 
 let write_access location addr_trace_ref access addr_trace_obj astate =
-  check_addr_access location addr_trace_ref astate
+  check_addr_access Write location addr_trace_ref astate
   >>| Memory.add_edge addr_trace_ref access addr_trace_obj location
 
 
@@ -228,7 +251,7 @@ let add_dynamic_type typ address astate = AddressAttributes.add_dynamic_type typ
 let remove_allocation_attr address astate = AddressAttributes.remove_allocation_attr address astate
 
 let invalidate location cause addr_trace astate =
-  check_addr_access location addr_trace astate
+  check_addr_access NoAccess location addr_trace astate
   >>| AddressAttributes.invalidate addr_trace cause location
 
 
@@ -238,7 +261,7 @@ let invalidate_access location cause ref_addr_hist access astate =
 
 
 let invalidate_array_elements location cause addr_trace astate =
-  let+ astate = check_addr_access location addr_trace astate in
+  let+ astate = check_addr_access NoAccess location addr_trace astate in
   match Memory.find_opt (fst addr_trace) astate with
   | None ->
       astate
@@ -252,7 +275,7 @@ let invalidate_array_elements location cause addr_trace astate =
 
 
 let shallow_copy location addr_hist astate =
-  let+ astate = check_addr_access location addr_hist astate in
+  let+ astate = check_addr_access Read location addr_hist astate in
   let cell =
     match AbductiveDomain.find_post_cell_opt (fst addr_hist) astate with
     | None ->
@@ -496,12 +519,12 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret
 
 
 let get_captured_actuals location ~captured_vars ~actual_closure astate =
-  let* astate, this_value_addr = eval_access location actual_closure Dereference astate in
+  let* astate, this_value_addr = eval_access Read location actual_closure Dereference astate in
   let+ _, astate, captured_vars_with_actuals =
     List.fold_result captured_vars ~init:(0, astate, [])
       ~f:(fun (id, astate, captured) (var, mode) ->
         let+ astate, captured_actual =
-          eval_access location this_value_addr
+          eval_access Read location this_value_addr
             (FieldAccess (Closures.mk_fake_field ~id mode))
             astate
         in

infer/src/pulse/PulseOperations.mli

@@ -13,7 +13,16 @@ type t = AbductiveDomain.t
 
 type 'a access_result = 'a PulseReport.access_result
 
-val check_addr_access : Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
+type access_mode =
+  | Read
+  | Write
+  | NoAccess
+      (** The initialized-ness of the address is not checked when it evaluates a heap address
+          without actual memory access, for example, when evaluating [&x.f] we need to check
+          initialized-ness of [x], not that of [x.f]. *)
+
+val check_addr_access :
+  access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
 (** Check that the [address] is not known to be invalid *)
 
 module Closures : sig
@@ -21,7 +30,8 @@ module Closures : sig
   (** assert the validity of the addresses captured by the lambda *)
 end
 
-val eval : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
+val eval :
+  access_mode -> Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** Use the stack and heap to evaluate the given expression down to an abstract address representing
     its value.
 
@@ -34,7 +44,8 @@ val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistor
 (** Like [eval] but evaluates [*exp]. *)
 
 val eval_access :
-     Location.t
+     access_mode
+  -> Location.t
   -> AbstractValue.t * ValueHistory.t
   -> BaseMemory.Access.t
   -> t
@@ -52,7 +63,7 @@ val havoc_field :
   -> t
   -> t access_result
 
-val realloc_pvar : Pvar.t -> Location.t -> t -> t
+val realloc_pvar : Pvar.t -> Typ.t -> Location.t -> t -> t
 
 val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t
 

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

@@ -3,3 +3,7 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LE
 codetoanalyze/c/pulse/memory_leak.c, malloc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),is the null pointer,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, 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/c/pulse/uninit.c, call_to_use_and_mayinit_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `x` declared here,invalid access occurs here]
+codetoanalyze/c/pulse/uninit.c, dereference_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `p` declared here,invalid access occurs here]
+codetoanalyze/c/pulse/uninit.c, malloc_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `malloc` (modelled),was uninitialized,use-after-lifetime part of the trace starts here,allocated by call to `malloc` (modelled),assigned,invalid access occurs here]
+codetoanalyze/c/pulse/uninit.c, self_assign_bad, 2, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `x` declared here,invalid access occurs here]

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

@@ -0,0 +1,85 @@
+/*
+ * 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.
+ */
+
+int dereference_bad() {
+  int* p;
+  return *p;
+}
+
+void self_assign_bad() {
+  int x;
+  x = x;
+}
+
+void use_and_mayinit(int, int*);
+
+void call_to_use_and_mayinit_bad() {
+  int x;
+  use_and_mayinit(x, &x);
+}
+
+void malloc_good() {
+  int* p = (int*)malloc(sizeof(int));
+  if (p) {
+    *p = 5;
+    int x = *p;
+  }
+  free(p);
+}
+
+void malloc_bad() {
+  int* p = (int*)malloc(sizeof(int));
+  if (p) {
+    int x = *p;
+  }
+  free(p);
+}
+
+void init_int_ref(int* p) { *p = 5; }
+
+void nop(int* p) {}
+
+void interprocedural_good() {
+  int x;
+  init_int_ref(&x);
+  int y = x;
+}
+
+void interprocedural_bad_FN() {
+  int x;
+  nop(&x);
+  int y = x;
+}
+
+struct uninit_s {
+  int f1;
+  int f2;
+};
+
+void get_field_address_good() {
+  struct uninit_s* s = (struct uninit_s*)malloc(2 * sizeof(int));
+  if (s) {
+    int* p = &s->f1;
+  }
+  free(s);
+}
+
+void init_f1(struct uninit_s* p) { p->f1 = 5; }
+
+void interprocedural_struct_bad_FN() {
+  struct uninit_s s;
+  init_f1(&s);
+  int y = s.f2;
+}
+
+void malloc_array_good(int len) {
+  char* o = (char*)malloc(len);
+  if (o) {
+    o[0] = 'a';
+  }
+  free(o);
+}

infer/tests/codetoanalyze/cpp/pulse/basics.cpp

@@ -93,7 +93,7 @@ struct A {
 A getA();
 
 int struct_inside_loop_ok(std::vector<int> numbers) {
-  int sum;
+  int sum = 0;
   for (auto number : numbers) {
     A a = getA();
     sum += a.f(number);
@@ -102,7 +102,7 @@ int struct_inside_loop_ok(std::vector<int> numbers) {
 }
 
 int struct_inside_loop_break_ok(std::vector<int> numbers) {
-  int sum;
+  int sum = 0;
   for (auto number : numbers) {
     A a = getA();
     if (number < 0) {
@@ -114,7 +114,7 @@ int struct_inside_loop_break_ok(std::vector<int> numbers) {
 }
 
 int struct_inside_loop_continue_ok(std::vector<int> numbers) {
-  int sum;
+  int sum = 0;
   for (auto number : numbers) {
     A a = getA();
     if (number < 0) {

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

@@ -10,5 +10,6 @@ codetoanalyze/objc/pulse/MemoryLeaksInBlocks.m, block_captured_var_leak_bad, 6,
 codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 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/objc/pulse/NPEBlocks.m, captured_npe_bad, 5, 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,when calling `objc_blockcaptured_npe_bad_3` here,parameter `x` of objc_blockcaptured_npe_bad_3,invalid access occurs here]
 codetoanalyze/objc/pulse/NPEBlocks.m, captured_npe_ok_FP, 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/objc/pulse/uninit.m, Uninit.capture_in_closure_bad, 7, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,variable `x` declared here,was uninitialized,use-after-lifetime part of the trace starts here,variable `x` declared here,invalid access occurs here]
 codetoanalyze/objc/pulse/use_after_free.m, PulseTest.use_after_free_simple_in_objc_method_bad:, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of PulseTest.use_after_free_simple_in_objc_method_bad:,invalid access occurs here]
 codetoanalyze/objc/pulse/use_after_free.m, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here]

infer/tests/codetoanalyze/objc/pulse/uninit.m

@@ -0,0 +1,43 @@
+/*
+ * 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.
+ */
+#import <Foundation/NSObject.h>
+
+@interface Uninit : NSObject
+@end
+
+@implementation Uninit
+
+- (void)capture_in_closure_ok {
+  __block BOOL x;
+
+  void (^block)() = ^() {
+    x = true;
+  };
+}
+
+- (BOOL)capture_in_closure_bad {
+  __block BOOL x;
+
+  void (^block)() = ^() {
+    x = true;
+  };
+
+  return x;
+}
+
+- (BOOL)set_in_closure_ok {
+  __block BOOL x;
+
+  void (^block)() = ^() {
+    x = true;
+  };
+
+  block();
+  return x;
+}
+
+@end