[pulse] Inter-procedural uninit analysis

Summary:
This diff supports inter-procedural uninit analysis in pulse.

* Added `MustBeInitialized` attribute to pre state when an address is read

* Remove `Uninitialized` attribute when callee has `WrittenTo` for the
  same address

Reviewed By: jvillard

Differential Revision: D25368492

fbshipit-source-id: cbc74d4dc

infer/src/pulse/Pulse.ml

@@ -70,6 +70,10 @@ module PulseTransferFunctions = struct
           ~ret ~actuals ~formals_opt astate
     | _ ->
         L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
+        let astate =
+          let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in
+          PulseOperations.conservatively_initialize_args arg_values astate
+        in
         Ok
           [ Domain.ContinueProgram
               (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals
@@ -138,16 +142,6 @@ 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.proc_desc; tenv} as analysis_data) ret call_exp
       actuals call_loc flags astate =
     (* evaluate all actuals *)
@@ -161,7 +155,6 @@ module PulseTransferFunctions = struct
             :: 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
@@ -177,6 +170,13 @@ module PulseTransferFunctions = struct
       match model with
       | Some (model, callee_procname) ->
           L.d_printfln "Found model for call@\n" ;
+          let astate =
+            let arg_values =
+              List.map func_args ~f:(fun {ProcnameDispatcher.Call.FuncArg.arg_payload= value, _} ->
+                  value )
+            in
+            PulseOperations.conservatively_initialize_args arg_values astate
+          in
           model analysis_data ~callee_procname call_loc ~ret astate
       | None ->
           PerfEvent.(log (fun logger -> log_begin_event logger ~name:"pulse interproc call" ())) ;

infer/src/pulse/PulseAbductiveDomain.ml

@@ -118,6 +118,8 @@ let leq ~lhs ~rhs =
         ~rhs:(rhs.post :> BaseDomain.t)
 
 
+let initialize address astate = {astate with post= PostDomain.initialize address astate.post}
+
 module Stack = struct
   let is_abducible astate var =
     (* HACK: formals are pre-registered in the initial state *)
@@ -202,9 +204,14 @@ module AddressAttributes = struct
     abduce_attribute addr (MustBeValid access_trace) astate
 
 
-  let check_initialized addr astate =
+  let check_initialized access_trace addr astate =
-    let+ () = BaseAddressAttributes.check_initialized addr (astate.post :> base_domain).attrs in
+    let attrs = (astate.post :> base_domain).attrs in
-    ()
+    let+ () = BaseAddressAttributes.check_initialized addr attrs in
+    let is_written_to =
+      Option.exists (BaseAddressAttributes.find_opt addr attrs) ~f:(fun attrs ->
+          Attribute.Attributes.get_written_to attrs |> Option.is_some )
+    in
+    if is_written_to then astate else abduce_attribute addr (MustBeInitialized access_trace) astate
 
 
   (** [astate] with [astate.post.attrs = f astate.post.attrs] *)
@@ -258,7 +265,8 @@ module AddressAttributes = struct
         let astate =
           if Attribute.is_suitable_for_pre attr then abduce_attribute value attr astate else astate
         in
-        add_one value attr astate )
+        let astate = add_one value attr astate in
+        match attr with Attribute.WrittenTo _ -> initialize value astate | _ -> astate )
 
 
   let find_opt address astate =
@@ -577,8 +585,6 @@ 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,7 +126,7 @@ 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 check_initialized : Trace.t -> AbstractValue.t -> t -> (t, Trace.t) result
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 

infer/src/pulse/PulseAttribute.ml

@@ -32,6 +32,7 @@ module Attribute = struct
     | DynamicType of Typ.Name.t
     | EndOfCollection
     | Invalid of Invalidation.t * Trace.t
+    | MustBeInitialized of Trace.t
     | MustBeValid of Trace.t
     | StdVectorReserve
     | Uninitialized of Trace.t
@@ -73,6 +74,8 @@ module Attribute = struct
 
   let uninitialized_rank = Variants.to_rank (Uninitialized dummy_trace)
 
+  let must_be_initialized_rank = Variants.to_rank (MustBeInitialized 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
@@ -97,6 +100,10 @@ module Attribute = struct
         F.fprintf f "Invalid %a"
           (Trace.pp ~pp_immediate:(fun fmt -> Invalidation.pp fmt invalidation))
           trace
+    | MustBeInitialized trace ->
+        F.fprintf f "MustBeInitialized %a"
+          (Trace.pp ~pp_immediate:(pp_string_if_debug "read"))
+          trace
     | MustBeValid trace ->
         F.fprintf f "MustBeValid %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "access")) trace
     | StdVectorReserve ->
@@ -181,13 +188,20 @@ module Attributes = struct
            trace )
 
 
+  let get_must_be_initialized attrs =
+    Set.find_rank attrs Attribute.must_be_initialized_rank
+    |> Option.map ~f:(fun attr ->
+           let[@warning "-8"] (Attribute.MustBeInitialized trace) = attr in
+           trace )
+
+
   include Set
 end
 
 include Attribute
 
 let is_suitable_for_pre = function
-  | MustBeValid _ ->
+  | MustBeValid _ | MustBeInitialized _ ->
       true
   | AddressOfCppTemporary _
   | AddressOfStackVariable _
@@ -213,6 +227,8 @@ let map_trace ~f = function
       Uninitialized (f trace)
   | WrittenTo trace ->
       WrittenTo (f trace)
+  | MustBeInitialized trace ->
+      MustBeInitialized (f trace)
   | ( AddressOfCppTemporary _
     | AddressOfStackVariable _
     | Closure _

infer/src/pulse/PulseAttribute.mli

@@ -19,6 +19,7 @@ type t =
   | DynamicType of Typ.Name.t
   | EndOfCollection
   | Invalid of Invalidation.t * Trace.t
+  | MustBeInitialized of Trace.t
   | MustBeValid of Trace.t
   | StdVectorReserve
   | Uninitialized of Trace.t
@@ -56,4 +57,6 @@ module Attributes : sig
   val is_std_vector_reserved : t -> bool
 
   val get_uninitialized : t -> Trace.t option
+
+  val get_must_be_initialized : t -> Trace.t option
 end

infer/src/pulse/PulseBaseAddressAttributes.ml

@@ -119,6 +119,8 @@ let get_closure_proc_name = get_attribute Attributes.get_closure_proc_name
 
 let get_must_be_valid = get_attribute Attributes.get_must_be_valid
 
+let get_must_be_initialized = get_attribute Attributes.get_must_be_initialized
+
 let std_vector_reserve address memory = add_one address Attribute.StdVectorReserve memory
 
 let is_end_of_collection address attrs =

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -39,6 +39,8 @@ val get_closure_proc_name : AbstractValue.t -> t -> Procname.t option
 
 val get_must_be_valid : AbstractValue.t -> t -> Trace.t option
 
+val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option
+
 val std_vector_reserve : AbstractValue.t -> t -> t
 
 val is_std_vector_reserved : AbstractValue.t -> t -> bool

infer/src/pulse/PulseInterproc.ml

@@ -515,27 +515,42 @@ let apply_post callee_proc_name call_location pre_post ~captured_vars_with_actua
 let check_all_valid callee_proc_name call_location {AbductiveDomain.pre; _} call_state =
   AddressMap.fold
     (fun addr_pre (addr_caller, hist_caller) astate_result ->
-      match astate_result with
+      let mk_access_trace callee_access_trace =
-      | Error _ ->
+        Trace.ViaCall
-          astate_result
+          { in_call= callee_access_trace
-      | Ok astate -> (
+          ; f= Call callee_proc_name
+          ; location= call_location
+          ; history= hist_caller }
+      in
+      let open IResult.Let_syntax in
+      let* astate = astate_result in
+      let* astate =
         match BaseAddressAttributes.get_must_be_valid addr_pre (pre :> BaseDomain.t).attrs with
         | None ->
             astate_result
         | Some callee_access_trace ->
-            let access_trace =
+            let access_trace = mk_access_trace callee_access_trace in
-              Trace.ViaCall
-                { in_call= callee_access_trace
-                ; f= Call callee_proc_name
-                ; location= call_location
-                ; history= hist_caller }
-            in
             AddressAttributes.check_valid access_trace addr_caller astate
             |> Result.map_error ~f:(fun (invalidation, invalidation_trace) ->
                    L.d_printfln "ERROR: caller's %a invalid!" AbstractValue.pp addr_caller ;
                    ( Diagnostic.AccessToInvalidAddress
                        {calling_context= []; invalidation; invalidation_trace; access_trace}
-                   , astate ) ) ) )
+                   , astate ) )
+      in
+      match BaseAddressAttributes.get_must_be_initialized addr_pre (pre :> BaseDomain.t).attrs with
+      | None ->
+          astate_result
+      | Some callee_access_trace ->
+          let access_trace = mk_access_trace callee_access_trace in
+          AddressAttributes.check_initialized access_trace addr_caller astate
+          |> Result.map_error ~f:(fun invalidation_trace ->
+                 L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ;
+                 ( Diagnostic.AccessToInvalidAddress
+                     { calling_context= []
+                     ; invalidation= Uninitialized
+                     ; invalidation_trace
+                     ; access_trace }
+                 , astate ) ) )
     call_state.subst (Ok call_state.astate)
 
 

infer/src/pulse/PulseOperations.ml

@@ -27,8 +27,8 @@ let check_addr_access access_mode location (address, history) astate =
   in
   match access_mode with
   | Read ->
-      let+ () =
+      let+ astate =
-        AddressAttributes.check_initialized address astate
+        AddressAttributes.check_initialized access_trace address astate
         |> Result.map_error ~f:(fun invalidation_trace ->
                ( Diagnostic.AccessToInvalidAddress
                    { calling_context= []
@@ -533,10 +533,24 @@ let get_captured_actuals location ~captured_vars ~actual_closure astate =
   (astate, captured_vars_with_actuals)
 
 
+let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) =
+  let reachable_values = BaseDomain.reachable_addresses_from arg_values (post :> BaseDomain.t) in
+  AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
+
+
 let call ~caller_proc_desc err_log ~(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
   | Some (callee_proc_desc, exec_states) ->
+      let astate =
+        (* NOTE: This conservatively initializes all reachable addresses from captured variables
+           when calling ObjC blocks, because the captured variables with call-by-reference in ObjC
+           are incorrectly translated in the frontend.  See T80743637. *)
+        if Procname.is_objc_block callee_pname then
+          conservatively_initialize_args (get_arg_values ()) astate
+        else astate
+      in
       let formals =
         Procdesc.get_formals callee_proc_desc
         |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
@@ -586,5 +600,6 @@ let call ~caller_proc_desc err_log ~(callee_data : (Procdesc.t * PulseSummary.t)
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ;
+      let astate = conservatively_initialize_args (get_arg_values ()) astate in
       unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate
       |> fun astate -> Ok [ExecutionDomain.ContinueProgram astate]

infer/src/pulse/PulseOperations.mli

@@ -156,3 +156,5 @@ val unknown_call :
   -> t
 (** performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and
     the return value as appropriate *)
+
+val conservatively_initialize_args : AbstractValue.t list -> t -> t

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

@@ -5,5 +5,8 @@ codetoanalyze/c/pulse/nullptr.c, malloc_no_check_bad, 2, NULLPTR_DEREFERENCE, no
 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, interprocedural_nop_in_callee_bad, 3, 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, interprocedural_read_in_callee_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,when calling `read_int_ref` here,parameter `p` of read_int_ref,invalid access occurs here]
+codetoanalyze/c/pulse/uninit.c, interprocedural_uninit_in_callee_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `uninit` here,allocated by call to `malloc` (modelled),was uninitialized,use-after-lifetime part of the trace starts here,passed as argument to `uninit`,return from call to `uninit`,assigned,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

@@ -41,20 +41,36 @@ void malloc_bad() {
 
 void init_int_ref(int* p) { *p = 5; }
 
-void nop(int* p) {}
+void interprocedural_init_in_callee_good() {
-
-void interprocedural_good() {
   int x;
   init_int_ref(&x);
   int y = x;
 }
 
-void interprocedural_bad_FN() {
+void nop(int* p) {}
+
+void interprocedural_nop_in_callee_bad() {
   int x;
   nop(&x);
   int y = x;
 }
 
+void read_int_ref(int* p) { int x = *p; }
+
+void interprocedural_read_in_callee_bad() {
+  int x;
+  read_int_ref(&x);
+}
+
+int* uninit() { return (int*)malloc(sizeof(int)); }
+
+void interprocedural_uninit_in_callee_bad() {
+  int* p = uninit();
+  if (p) {
+    int x = *p;
+  }
+}
+
 struct uninit_s {
   int f1;
   int f2;

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

@@ -11,5 +11,6 @@ codetoanalyze/objc/pulse/NPEBlocks.m, Singleton.dispatch_once_no_npe_good_FP, 6,
 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/uninit.m, Uninit.not_set_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

@@ -40,4 +40,24 @@
   return x;
 }
 
+- (BOOL)not_set_in_closure_bad {
+  __block BOOL x;
+
+  void (^block)() = ^() {
+  };
+
+  block();
+  return x;
+}
+
+- (BOOL)use_in_closure_bad_FN {
+  __block BOOL x;
+
+  void (^block)() = ^() {
+    BOOL y = x;
+  };
+
+  block();
+}
+
 @end