[pulse] generate latent abort for non-POD nil messaging summary

Summary:
This way we don't rely on existing summaries already having a
MustBeValid for self and on them having possibly other conditions that
might prevent a report.

Reviewed By: skcho

Differential Revision: D29550321

fbshipit-source-id: b9822fcd4

infer/src/pulse/PulseAbductiveDomain.ml

@@ -326,15 +326,6 @@ module AddressAttributes = struct
     map_post_attrs astate ~f:(BaseAddressAttributes.add_unreachable_at addr location)
 
 
-  let replace_must_be_valid_reason path reason addr astate =
-    match BaseAddressAttributes.get_must_be_valid addr (astate.pre :> base_domain).attrs with
-    | Some (_timestamp, trace, _reason) ->
-        remove_must_be_valid_attr addr astate
-        |> abduce_attribute addr (MustBeValid (path.PathContext.timestamp, trace, Some reason))
-    | None ->
-        astate
-
-
   let is_end_of_collection addr astate =
     BaseAddressAttributes.is_end_of_collection addr (astate.post :> base_domain).attrs
 

infer/src/pulse/PulseAbductiveDomain.mli

@@ -131,9 +131,6 @@ module AddressAttributes : sig
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
-  val replace_must_be_valid_reason :
-    PathContext.t -> Invalidation.must_be_valid_reason -> AbstractValue.t -> t -> t
-
   val allocate : Procname.t -> AbstractValue.t * ValueHistory.t -> Location.t -> t -> t
 
   val add_dynamic_type : Typ.t -> AbstractValue.t -> t -> t

infer/src/pulse/PulseCallOperations.ml

@@ -288,10 +288,8 @@ let call tenv path ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.
       PulseObjectiveCSummary.mk_objc_method_nil_summary tenv procdesc
         (ExecutionDomain.mk_initial tenv procdesc)
       |> Option.value_map ~default:[] ~f:(fun nil_summary ->
-             let<*> nil_astate = nil_summary in
              call_aux tenv path caller_proc_desc call_loc callee_pname ret actuals procdesc
-               ([ContinueProgram nil_astate] :> ExecutionDomain.t list)
-               astate )
+               [nil_summary] astate )
     in
     result_unknown @ result_unknown_nil
   in

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -36,46 +36,79 @@ let init_fields_zero tenv path location ~zero addr typ astate =
   init_fields_zero_helper addr typ astate
 
 
+(** Constructs summary [{self = 0} {return = self}] when [proc_desc] returns a POD type. This allows
+    us to connect invalidation with invalid access in the trace *)
 let mk_objc_method_nil_summary_aux tenv proc_desc astate =
-  (* Constructs summary {self = 0} {return = self}.
-     This allows us to connect invalidation with invalid access in the trace *)
   let path = PathContext.initial in
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
-  let* astate, (self_value, self_history) =
-    PulseOperations.eval_deref path location (Lvar self) astate
+  (* HACK: we are operating on an "empty" initial state and do not expect to create any alarms
+     (nothing is Invalid in the initial state) or unsatisfiability (we won't create arithmetic
+     contradictions) *)
+  let assert_ok = function Ok x -> x | Error _ -> assert false in
+  let astate, (self_value, self_history) =
+    PulseOperations.eval_deref path location (Lvar self) astate |> assert_ok
   in
-  let* astate = PulseArithmetic.prune_eq_zero self_value astate in
+  let astate = PulseArithmetic.prune_eq_zero self_value astate |> assert_ok in
   let event = ValueHistory.NilMessaging location in
   let updated_self_value_hist = (self_value, event :: self_history) in
   match List.last (Procdesc.get_formals proc_desc) with
   | Some (last_formal, {desc= Tptr (typ, _)}) when Mangled.is_return_param last_formal ->
       let ret_param_var = Procdesc.get_ret_param_var proc_desc in
-      let* astate, ret_param_var_addr_hist =
-        PulseOperations.eval_deref path location (Lvar ret_param_var) astate
+      let astate, ret_param_var_addr_hist =
+        PulseOperations.eval_deref path location (Lvar ret_param_var) astate |> assert_ok
       in
       init_fields_zero tenv path location ~zero:updated_self_value_hist ret_param_var_addr_hist typ
         astate
+      |> assert_ok
   | _ ->
       let ret_var = Procdesc.get_ret_var proc_desc in
-      let* astate, ret_var_addr_hist =
-        PulseOperations.eval path Write location (Lvar ret_var) astate
+      let astate, ret_var_addr_hist =
+        PulseOperations.eval path Write location (Lvar ret_var) astate |> assert_ok
       in
       PulseOperations.write_deref path location ~ref:ret_var_addr_hist ~obj:updated_self_value_hist
         astate
+      |> assert_ok
+
+
+let mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate =
+  (* same HACK as above *)
+  let assert_ok = function Ok x -> x | Error _ -> assert false in
+  let path = PathContext.initial in
+  let location = Procdesc.get_loc proc_desc in
+  let self = mk_objc_self_pvar proc_desc in
+  let astate, (self_value, _self_history) =
+    PulseOperations.eval_deref path location (Lvar self) astate |> assert_ok
+  in
+  let trace = Trace.Immediate {location; history= []} in
+  let astate = PulseArithmetic.prune_eq_zero self_value astate |> assert_ok in
+  match AbductiveDomain.summary_of_post tenv proc_desc location astate with
+  | Unsat | Sat (Error _) ->
+      assert false
+  | Sat (Ok astate) ->
+      ExecutionDomain.LatentInvalidAccess
+        { astate
+        ; address= self_value
+        ; must_be_valid=
+            (trace, Some (SelfOfNonPODReturnMethod (Procdesc.get_ret_type_from_signature proc_desc)))
+        ; calling_context= [] }
 
 
 let mk_objc_method_nil_summary tenv proc_desc initial =
   let proc_name = Procdesc.get_proc_name proc_desc in
   match (initial, proc_name) with
-  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
-    when Procdesc.is_ret_type_pod proc_desc ->
-      (* In ObjC, when a method is called on nil, there is no NPE,
-         the method is actually not called and the return value is 0/false/nil.
-         We create a nil summary to avoid reporting NPE in this case.
-         However, there is an exception in the case where the return type is non-POD.
-         In that case it's UB and we want to report an error. *)
-      Some (mk_objc_method_nil_summary_aux tenv proc_desc astate)
+  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
+      if Procdesc.is_ret_type_pod proc_desc then
+        (* In ObjC, when a method is called on nil, there is no NPE,
+           the method is actually not called and the return value is 0/false/nil.
+           We create a nil summary to avoid reporting NPE in this case.
+           However, there is an exception in the case where the return type is non-POD.
+           In that case it's UB and we want to report an error. *)
+        let astate = mk_objc_method_nil_summary_aux tenv proc_desc astate in
+        Some (ContinueProgram astate)
+      else
+        let summary = mk_objc_latent_non_POD_nil_messaging tenv proc_desc astate in
+        Some summary
   | ContinueProgram _, _
   | ExitProgram _, _
   | AbortProgram _, _
@@ -90,8 +123,7 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
   let self = mk_objc_self_pvar proc_desc in
   let proc_name = Procdesc.get_proc_name proc_desc in
   match (astate, proc_name) with
-  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
-    when Procdesc.is_ret_type_pod proc_desc ->
+  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
       let result =
         let* astate, value =
           PulseOperations.eval_deref PathContext.initial location (Lvar self) astate
@@ -111,44 +143,16 @@ let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log}
 let append_objc_actual_self_positive procdesc self_actual astate =
   let procname = Procdesc.get_proc_name procdesc in
   match procname with
-  | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} when Procdesc.is_ret_type_pod procdesc ->
+  | Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
       Option.value_map self_actual ~default:(Ok astate) ~f:(fun ((self, _), _) ->
           PulseArithmetic.prune_positive self astate )
   | _ ->
       Ok astate
 
 
-let update_must_be_valid_reason {InterproceduralAnalysis.tenv; proc_desc; err_log} astate =
-  let path = PathContext.initial in
-  let location = Procdesc.get_loc proc_desc in
-  let self = mk_objc_self_pvar proc_desc in
-  let proc_name = Procdesc.get_proc_name proc_desc in
-  match (astate, proc_name) with
-  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
-    when not (Procdesc.is_ret_type_pod proc_desc) ->
-      let result =
-        (* add reason for must be valid to be because the return type is non pod *)
-        let+ astate, value = PulseOperations.eval_deref path location (Lvar self) astate in
-        AddressAttributes.replace_must_be_valid_reason path
-          (SelfOfNonPODReturnMethod (Procdesc.get_ret_type_from_signature proc_desc))
-          (fst value) astate
-      in
-      PulseReport.report_result tenv proc_desc err_log location result
-  | ContinueProgram _, _
-  | ExitProgram _, _
-  | AbortProgram _, _
-  | LatentAbortProgram _, _
-  | LatentInvalidAccess _, _
-  | ISLLatentMemoryError _, _ ->
-      [astate]
-
-
-let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data)
-    ~initial_astate ~posts =
+let update_objc_method_posts {InterproceduralAnalysis.tenv; proc_desc} ~initial_astate ~posts =
   match mk_objc_method_nil_summary tenv proc_desc initial_astate with
   | None ->
-      List.concat_map ~f:(update_must_be_valid_reason analysis_data) posts
-  | Some result ->
-      let location = Procdesc.get_loc proc_desc in
-      let nil_summary = PulseReport.report_result tenv proc_desc err_log location result in
-      nil_summary @ posts
+      posts
+  | Some nil_summary ->
+      nil_summary :: posts

infer/src/pulse/PulseObjectiveCSummary.mli

@@ -29,4 +29,4 @@ val append_objc_self_positive :
     for other kinds of methods *)
 
 val mk_objc_method_nil_summary :
-  Tenv.t -> Procdesc.t -> ExecutionDomain.t -> AbductiveDomain.t AccessResult.t option
+  Tenv.t -> Procdesc.t -> ExecutionDomain.t -> ExecutionDomain.t option

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

@@ -23,14 +23,14 @@ codetoanalyze/objcpp/pulse/NPEBasic.mm, replaceObjectsAtIndexesWithNilObjectsInA
 codetoanalyze/objcpp/pulse/NPEBasic.mm, replaceObjectsAtNilIndexesWithObjectsInArrayBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `replaceObjectsAtIndexesWithObjectsInArray` here,parameter `indexset` of replaceObjectsAtIndexesWithObjectsInArray,in call to `NSMutableArray.replaceObjectsAtIndexes:withObjects:` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, setByAddingObjectBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `setByAddingObject` here,parameter `object` of setByAddingObject,in call to `NSSet.setByAddingObject` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, setWithObjectBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `setWithObject` here,parameter `object` of setWithObject,in call to `NSSet.setWithObject` (modelled),invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is the null pointer,assigned,when calling `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [*** LATENT ***,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.ptr`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.ptr` here,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatent, 7, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [*** LATENT ***,calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODLatentBad, 1, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `testCallMethodReturnsnonPODLatent`,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,is the null pointer,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNilNilOK_FP, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testNilMessagingForModelNotNilDictBad, 1, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,when calling `addObjectInDict` here,parameter `value` of addObjectInDict,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `SomeObject.returnsNil`,is the null pointer,returned,return from call to `SomeObject.returnsNil`,in call to `SomeObject.get`,parameter `self` of SomeObject.get,a message sent to nil returns nil,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, testNonPODTraceBad, 2, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,in call to `SomeObject.returnsNil`,is the null pointer,returned,return from call to `SomeObject.returnsNil`,in call to `SomeObject.get`,parameter `self` of SomeObject.get,a message sent to nil returns nil,return from call to `SomeObject.get`,assigned,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, testTraceBad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,in call to `SomeObject.getXPtr`,parameter `self` of SomeObject.getXPtr,a message sent to nil returns nil,return from call to `SomeObject.getXPtr`,assigned,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, unknown_call_twice_FP, 4, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [in call to `SomeObject.sharedInstance`,is the null pointer,assigned,returned,return from call to `SomeObject.sharedInstance`,when calling `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,invalid access occurs here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, unknown_call_twice_FP, 4, NIL_MESSAGING_TO_NON_POD, no_bucket, ERROR, [calling context starts here,in call to `SomeObject.returnsnonPOD`,null pointer dereference part of the trace starts here,in call to `SomeObject.sharedInstance`,is the null pointer,assigned,returned,return from call to `SomeObject.sharedInstance`,when calling `SomeObject.returnsnonPOD` here,invalid access occurs here]
 codetoanalyze/objcpp/pulse/use_after_delete.mm, PulseTest.deref_deleted_in_objc_method_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]
 codetoanalyze/objcpp/pulse/use_after_delete.mm, deref_deleted_bad, 3, USE_AFTER_DELETE, no_bucket, ERROR, [invalidation part of the trace starts here,allocated by call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,allocated by call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]