[pulse][objc][nil] Add constraint `self > 0` before computing spec for Objective-C instance methods

Summary: Adding constraint `self > 0` after computing specs for Objective-C instance methods were causing false positives of the heuristics not to discard `self=0 /\ self|->-` (added new test testAnotherObjectUseSelfOk was FP). This diff adds constrain `self > 0`  before computing Objective-C specs, discarding unsatisfiable `self > 0 /\ self =0`.

Reviewed By: skcho

Differential Revision: D29462462

fbshipit-source-id: 088ee447e

infer/src/pulse/Pulse.ml

@@ -474,7 +474,10 @@ let with_debug_exit_node proc_desc ~f =
 let checker ({InterproceduralAnalysis.tenv; proc_desc; err_log} as analysis_data) =
   AbstractValue.State.reset () ;
   let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
-  let initial = [(initial_astate, PathContext.initial)] in
+  let initial_self_positive =
+    PulseObjectiveCSummary.append_objc_self_positive analysis_data initial_astate
+  in
+  let initial = List.map ~f:(fun initial -> (initial, PathContext.initial)) initial_self_positive in
   match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with
   | Some posts ->
       (* forget path contexts, we don't propagate them across functions *)

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -88,20 +88,23 @@ let mk_objc_method_nil_summary tenv proc_desc initial =
 let append_objc_self_positive {InterproceduralAnalysis.tenv; proc_desc; err_log} astate =
   let location = Procdesc.get_loc proc_desc in
   let self = mk_objc_self_pvar proc_desc in
-  match astate with
+  let proc_name = Procdesc.get_proc_name proc_desc in
-  | ContinueProgram astate ->
+  match (astate, proc_name) with
+  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod}
+    when Procdesc.is_ret_type_pod proc_desc ->
       let result =
         let* astate, value =
           PulseOperations.eval_deref PathContext.initial location (Lvar self) astate
         in
-        PulseArithmetic.prune_positive (fst value) astate
+        PulseArithmetic.and_positive (fst value) astate
       in
       PulseReport.report_result tenv proc_desc err_log location result
-  | ExitProgram _
+  | ContinueProgram _, _
-  | AbortProgram _
+  | ExitProgram _, _
-  | LatentAbortProgram _
+  | AbortProgram _, _
-  | LatentInvalidAccess _
+  | LatentAbortProgram _, _
-  | ISLLatentMemoryError _ ->
+  | LatentInvalidAccess _, _
+  | ISLLatentMemoryError _, _ ->
       [astate]
 
 
@@ -148,5 +151,4 @@ let update_objc_method_posts ({InterproceduralAnalysis.tenv; proc_desc; err_log}
   | Some result ->
       let location = Procdesc.get_loc proc_desc in
       let nil_summary = PulseReport.report_result tenv proc_desc err_log location result in
-      let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in
       nil_summary @ posts

infer/src/pulse/PulseObjectiveCSummary.mli

@@ -14,8 +14,8 @@ val update_objc_method_posts :
   -> initial_astate:ExecutionDomain.t
   -> posts:ExecutionDomain.t list
   -> ExecutionDomain.t list
-(** For ObjC instance methods: adds path condition `self > 0` to given posts and appends additional
+(** For ObjC instance methods: appends additional nil summary and replaces must be valid reason for
-    nil summary. Does nothing to posts for other kinds of methods *)
+    non-pod return type. Does nothing to posts for other kinds of methods *)
 
 val append_objc_actual_self_positive :
      Procdesc.t
@@ -23,5 +23,10 @@ val append_objc_actual_self_positive :
   -> AbductiveDomain.t
   -> AbductiveDomain.t AccessResult.t
 
+val append_objc_self_positive :
+  PulseSummary.t InterproceduralAnalysis.t -> ExecutionDomain.t -> ExecutionDomain.t list
+(** For ObjC instance methods: adds path condition `self > 0` to a given post. Does nothing to posts
+    for other kinds of methods *)
+
 val mk_objc_method_nil_summary :
   Tenv.t -> Procdesc.t -> ExecutionDomain.t -> AbductiveDomain.t AccessResult.t option

infer/tests/codetoanalyze/objcpp/pulse/NPEBasic.mm

@@ -8,10 +8,21 @@
 #import <Foundation/Foundation.h>
 #include <memory>
 
+@interface AnotherObject : NSObject
+- (int)someMethod:(int)param1;
+@end
+
+@implementation AnotherObject
+- (int)someMethod:(int)param1 {
+  return param1;
+}
+@end
+
 @interface SomeObject : NSObject
 
 @property int x;
 @property std::shared_ptr<int> ptr;
+@property AnotherObject* anotherObject;
 
 - (int)returnsPOD;
 
@@ -28,7 +39,6 @@
 - (SomeObject*)get;
 
 + (NSString*)returnsStringNil;
-
 @end
 
 @implementation SomeObject
@@ -53,6 +63,10 @@
   return nil;
 }
 
+- (int)callAnotherObjectMethod {
+  return [_anotherObject someMethod:[self returnsPOD]];
+}
+
 - (SomeObject*)get {
   SomeObject* o = [SomeObject new];
   return o;
@@ -74,6 +88,10 @@
   return shared;
 }
 
+- (int)methodNilDereferenceBad {
+  int* x = nil;
+  return *x;
+}
 @end
 
 int dereferenceNilBad() {
@@ -470,3 +488,8 @@ std::shared_ptr<int> unknown_call_twice_FP() {
   }
   return [[SomeObject sharedInstance] returnsnonPOD];
 }
+
+int testAnotherObjectUseSelfOk() {
+  auto const obj = [SomeObject returnsNil];
+  return [obj callAnotherObjectMethod];
+}

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

@@ -1,4 +1,5 @@
 codetoanalyze/objcpp/pulse/AllocPatternMemLeak.mm, A.create_no_release_leak_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `ABFDataCreate` here,memory becomes unreachable here]
+codetoanalyze/objcpp/pulse/NPEBasic.mm, SomeObject.methodNilDereferenceBad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInArrayBad, 0, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,in call to `NSMutableArray.addObject:` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilInDictBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,in call to `NSMutableDictionary.setObject:forKey:` (modelled),invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, addNilKeyInDictBracketsBad, 2, NIL_INSERTION_INTO_COLLECTION, no_bucket, ERROR, [is the null pointer,assigned,in call to `mutableDictionary[someKey] = value` (modelled),invalid access occurs here]