[pulse][5/5] timestamps for MustBeInitialized

Summary: Same as MustBeValid: we want to report the first error on the path.

Reviewed By: skcho

Differential Revision: D28674724

fbshipit-source-id: a2ac04b5b

infer/src/pulse/PulseAbductiveDomain.ml

@@ -244,14 +244,15 @@ module AddressAttributes = struct
       astate
 
 
-  let check_initialized access_trace addr astate =
+  let check_initialized path access_trace addr astate =
     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
+    if is_written_to then astate
+    else abduce_attribute addr (MustBeInitialized (path.PathContext.timestamp, access_trace)) astate
 
 
   (** [astate] with [astate.post.attrs = f astate.post.attrs] *)

infer/src/pulse/PulseAbductiveDomain.mli

@@ -127,7 +127,7 @@ module AddressAttributes : sig
     -> t
     -> (t, Invalidation.t * Trace.t) result
 
-  val check_initialized : Trace.t -> AbstractValue.t -> t -> (t, unit) result
+  val check_initialized : PathContext.t -> Trace.t -> AbstractValue.t -> t -> (t, unit) result
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 

infer/src/pulse/PulseAttribute.ml

@@ -34,7 +34,7 @@ module Attribute = struct
     | EndOfCollection
     | Invalid of Invalidation.t * Trace.t
     | ISLAbduced of Trace.t
-    | MustBeInitialized of Trace.t
+    | MustBeInitialized of PathContext.timestamp * Trace.t
     | MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option
     | StdVectorReserve
     | Uninitialized
@@ -97,7 +97,7 @@ module Attribute = struct
 
   let unreachable_at_rank = Variants.to_rank (UnreachableAt Location.dummy)
 
-  let must_be_initialized_rank = Variants.to_rank (MustBeInitialized dummy_trace)
+  let must_be_initialized_rank = Variants.to_rank (MustBeInitialized (PathContext.t0, dummy_trace))
 
   let pp f attribute =
     let pp_string_if_debug string fmt =
@@ -125,10 +125,11 @@ module Attribute = struct
           trace
     | ISLAbduced trace ->
         F.fprintf f "ISLAbduced %a" (Trace.pp ~pp_immediate:(pp_string_if_debug "ISLAbduced")) trace
-    | MustBeInitialized trace ->
-        F.fprintf f "MustBeInitialized %a"
+    | MustBeInitialized (timestamp, trace) ->
+        F.fprintf f "MustBeInitialized(%a, t=%d)"
           (Trace.pp ~pp_immediate:(pp_string_if_debug "read"))
           trace
+          (timestamp :> int)
     | MustBeValid (timestamp, trace, reason) ->
         F.fprintf f "MustBeValid(%a, %a, t=%d)"
           (Trace.pp ~pp_immediate:(pp_string_if_debug "access"))
@@ -201,8 +202,8 @@ module Attribute = struct
         ISLAbduced (add_call_to_trace trace)
     | MustBeValid (_timestamp, trace, reason) ->
         MustBeValid (path.PathContext.timestamp, add_call_to_trace trace, reason)
-    | MustBeInitialized trace ->
-        MustBeInitialized (add_call_to_trace trace)
+    | MustBeInitialized (_timestamp, trace) ->
+        MustBeInitialized (path.PathContext.timestamp, add_call_to_trace trace)
     | WrittenTo trace ->
         WrittenTo (add_call_to_trace trace)
     | ( AddressOfCppTemporary _
@@ -293,8 +294,8 @@ module Attributes = struct
   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 )
+           let[@warning "-8"] (Attribute.MustBeInitialized (timestamp, trace)) = attr in
+           (timestamp, trace) )
 
 
   let get_unreachable_at attrs =

infer/src/pulse/PulseAttribute.mli

@@ -21,7 +21,7 @@ type t =
   | EndOfCollection
   | Invalid of Invalidation.t * Trace.t
   | ISLAbduced of Trace.t  (** The allocation is abduced so as the analysis could run normally *)
-  | MustBeInitialized of Trace.t
+  | MustBeInitialized of PathContext.timestamp * Trace.t
   | MustBeValid of PathContext.timestamp * Trace.t * Invalidation.must_be_valid_reason option
   | StdVectorReserve
   | Uninitialized
@@ -65,7 +65,7 @@ module Attributes : sig
 
   val is_uninitialized : t -> bool
 
-  val get_must_be_initialized : t -> Trace.t option
+  val get_must_be_initialized : t -> (PathContext.timestamp * Trace.t) option
 
   val get_unreachable_at : t -> Location.t option
 

infer/src/pulse/PulseBaseAddressAttributes.mli

@@ -48,7 +48,7 @@ val get_must_be_valid :
 
 val is_must_be_valid_or_allocated_isl : AbstractValue.t -> t -> bool
 
-val get_must_be_initialized : AbstractValue.t -> t -> Trace.t option
+val get_must_be_initialized : AbstractValue.t -> t -> (PathContext.timestamp * Trace.t) option
 
 val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t
 

infer/src/pulse/PulseInterproc.ml

@@ -636,22 +636,12 @@ let check_all_valid path callee_proc_name call_location {AbductiveDomain.pre; _}
       call_state.subst []
   in
   let timestamp_of_check = function
-    | `MustBeValid (timestamp, _, _) ->
-        Some timestamp
-    | `MustBeInitialized _ ->
-        None
+    | `MustBeValid (timestamp, _, _) | `MustBeInitialized (timestamp, _) ->
+        timestamp
   in
   List.sort addresses_to_check ~compare:(fun (_, check1) (_, check2) ->
-      match (timestamp_of_check check1, timestamp_of_check check2) with
-      | Some t1, Some t2 ->
-          (* smaller timestamp first *) PathContext.compare_timestamp t1 t2
-      (* with a timestamp first (gone soon when MustBeInitialized will get a timestamp too), otherwise dummy comparison *)
-      | None, None ->
-          0
-      | Some _, None ->
-          -1
-      | None, Some _ ->
-          1 )
+      (* smaller timestamp first *)
+      PathContext.compare_timestamp (timestamp_of_check check1) (timestamp_of_check check2) )
   |> List.fold_result ~init:call_state.astate ~f:(fun astate ((addr_caller, hist_caller), check) ->
          let mk_access_trace callee_access_trace =
            Trace.ViaCall
@@ -675,9 +665,9 @@ let check_all_valid path callee_proc_name call_location {AbductiveDomain.pre; _}
                             ; access_trace
                             ; must_be_valid_reason }
                       ; astate } )
-         | `MustBeInitialized callee_access_trace ->
+         | `MustBeInitialized (_timestamp, callee_access_trace) ->
              let access_trace = mk_access_trace callee_access_trace in
-             AddressAttributes.check_initialized access_trace addr_caller astate
+             AddressAttributes.check_initialized path access_trace addr_caller astate
              |> Result.map_error ~f:(fun () ->
                     L.d_printfln "ERROR: caller's %a is uninitialized!" AbstractValue.pp addr_caller ;
                     AccessResult.ReportableError

infer/src/pulse/PulseOperations.ml

@@ -67,7 +67,7 @@ let check_addr_access path ?must_be_valid_reason access_mode location (address,
   in
   match access_mode with
   | Read ->
-      AddressAttributes.check_initialized access_trace address astate
+      AddressAttributes.check_initialized path access_trace address astate
       |> Result.map_error ~f:(fun () ->
              ReportableError
                { diagnostic=
@@ -87,7 +87,7 @@ let check_and_abduce_addr_access_isl path access_mode location (address, history
          let* astate = AccessResult.of_abductive_access_result access_trace access_result in
          match access_mode with
          | Read ->
-             AddressAttributes.check_initialized access_trace address astate
+             AddressAttributes.check_initialized path access_trace address astate
              |> Result.map_error ~f:(fun () ->
                     ReportableError
                       { diagnostic=

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

@@ -13,6 +13,6 @@ codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.assignNilBad, 5, NIL_BLOCK_CALL,
 codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramAssignNilBad:, 3, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/objc/pulse/NPENilBlocks.m, BlockA.paramReassignNilBad:, 6, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,assigned,assigned,invalid access occurs here]
 codetoanalyze/objc/pulse/NPENilBlocks.m, calldoSomethingThenCallbackWithNilBad, 2, NIL_BLOCK_CALL, no_bucket, ERROR, [is the null pointer,when calling `BlockA.doSomethingThenCallback:` here,parameter `my_block` of BlockA.doSomethingThenCallback:,invalid access occurs here]
-codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `y` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value occurs here]
+codetoanalyze/objc/pulse/uninit.m, Uninit.call_setter_c_struct_bad, 3, PULSE_UNINITIALIZED_VALUE, no_bucket, ERROR, [struct field address `x` created,when calling `Uninit.setS:` here,parameter `s` of Uninit.setS:,read to uninitialized value 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]