[pulse][nullptr][objc] Add nil summaries for ObjC instance methods

Summary: When a method is called in ObjC on nil, there is no NPE, the method is actually not called and the return value is 0/false/nil. (There is an exception in the case where the return type is non-POD. In that case it's UB. This will be addressed later). To implement this behaviour we add additional summary to ObjC instance methods {self = 0} {return = 0}. We also want to make sure that inferred summary will not be used in we call a method on nil, hence, we add a path condition {self > 0} to get a contradiction when needed.

Reviewed By: jvillard

Differential Revision: D26664187

fbshipit-source-id: cdac2a5bb

infer/src/pulse/Pulse.ml

@@ -428,11 +428,15 @@ let with_debug_exit_node proc_desc ~f =
 
 let checker ({InterproceduralAnalysis.proc_desc; err_log; tenv} as analysis_data) =
   AbstractValue.State.reset () ;
-  let initial = [ExecutionDomain.mk_initial tenv proc_desc] in
+  let initial_astate = ExecutionDomain.mk_initial tenv proc_desc in
+  let initial = [initial_astate] in
   match DisjunctiveAnalyzer.compute_post analysis_data ~initial proc_desc with
   | Some posts ->
       with_debug_exit_node proc_desc ~f:(fun () ->
-          let summary = PulseSummary.of_posts proc_desc posts in
+          let updated_posts =
+            PulseObjectiveCSummary.update_objc_method_posts analysis_data ~initial_astate ~posts
+          in
+          let summary = PulseSummary.of_posts proc_desc updated_posts in
           report_topl_errors proc_desc err_log summary ;
           Some summary )
   | None ->

infer/src/pulse/PulseObjectiveCSummary.ml

@@ -0,0 +1,70 @@
+(*
+ * 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.
+ *)
+
+open! IStd
+open PulseBasicInterface
+open PulseOperations.Import
+
+let mk_objc_self_pvar proc_desc =
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  Pvar.mk Mangled.self proc_name
+
+
+let mk_objc_method_nil_summary_aux proc_desc astate =
+  let location = Procdesc.get_loc proc_desc in
+  let self = mk_objc_self_pvar proc_desc in
+  let* astate, self_value = PulseOperations.eval_deref location (Lvar self) astate in
+  let astate = PulseArithmetic.prune_eq_zero (fst self_value) astate in
+  let ret_var = Procdesc.get_ret_var proc_desc in
+  let ret_addr = AbstractValue.mk_fresh () in
+  let ret_value = (ret_addr, []) in
+  let* astate, ret_var_addr_hist = PulseOperations.eval Write location (Lvar ret_var) astate in
+  let* astate = PulseOperations.write_deref location ~ref:ret_var_addr_hist ~obj:ret_value astate in
+  let astate = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate in
+  let+ astate =
+    PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value astate
+  in
+  [astate]
+
+
+let mk_objc_method_nil_summary ({InterproceduralAnalysis.proc_desc} as analysis_data) initial =
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  match (initial, proc_name) with
+  | ContinueProgram astate, Procname.ObjC_Cpp {kind= ObjCInstanceMethod} ->
+      let result = mk_objc_method_nil_summary_aux proc_desc astate in
+      Some (PulseReport.report_list_result analysis_data result)
+  | ContinueProgram _, _
+  | ExitProgram _, _
+  | AbortProgram _, _
+  | LatentAbortProgram _, _
+  | ISLLatentMemoryError _, _ ->
+      None
+
+
+let append_objc_self_positive ({InterproceduralAnalysis.proc_desc} as analysis_data) astate =
+  let location = Procdesc.get_loc proc_desc in
+  let self = mk_objc_self_pvar proc_desc in
+  match astate with
+  | ContinueProgram astate ->
+      let result =
+        let+ astate, value = PulseOperations.eval_deref location (Lvar self) astate in
+        let astate = PulseArithmetic.prune_positive (fst value) astate in
+        [astate]
+      in
+      PulseReport.report_list_result analysis_data result
+  | ExitProgram _ | AbortProgram _ | LatentAbortProgram _ | ISLLatentMemoryError _ ->
+      [astate]
+
+
+let update_objc_method_posts analysis_data ~initial_astate ~posts =
+  let nil_summary = mk_objc_method_nil_summary analysis_data initial_astate in
+  match nil_summary with
+  | None ->
+      posts
+  | Some nil_summary ->
+      let posts = List.concat_map ~f:(append_objc_self_positive analysis_data) posts in
+      nil_summary @ posts

infer/src/pulse/PulseObjectiveCSummary.mli

@@ -0,0 +1,17 @@
+(*
+ * 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.
+ *)
+
+open! IStd
+open PulseDomainInterface
+
+val update_objc_method_posts :
+     PulseSummary.t InterproceduralAnalysis.t
+  -> 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
+    nil summary. Does nothing to posts for other kinds of methods *)

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

@@ -17,6 +17,8 @@
 
 - (std::shared_ptr<int>)returnsnonPOD;
 
+- (int)add:(int)param1 andParam2:(int)param2;
+
 @end
 
 @implementation SomeObject
@@ -29,6 +31,10 @@
   return std::shared_ptr<int>(new int(_x));
 }
 
+- (int)add:(int)param1 andParam2:(int)param2 {
+  return _x + param1 + param2;
+}
+
 @end
 
 int dereferenceNilBad() {
@@ -36,32 +42,58 @@ int dereferenceNilBad() {
   return *int_ptr;
 }
 
-int FP_testCallMethodReturnsPODOk() {
+int testCallMethodReturnsPODOk() {
   SomeObject* obj = nil;
   return [obj returnsPOD];
 }
 
-std::shared_ptr<int> testCallMethodReturnsnonPODBad() {
+std::shared_ptr<int> FN_testCallMethodReturnsnonPODBad() {
   SomeObject* obj = nil;
   std::shared_ptr<int> d = [obj returnsnonPOD]; // UB
   return d;
 }
 
-int FP_testAccessPropertyAccessorOk() {
+int testAccessPropertyAccessorOk() {
   SomeObject* obj = nil;
   return obj.x; // calls property accessor method
 }
 
-std::shared_ptr<int> testAccessPropertyAccessorBad() {
+std::shared_ptr<int> FN_testAccessPropertyAccessorBad() {
   SomeObject* obj = nil;
   return obj.ptr; // calls property accessor method, but return type is non-POD
 }
 
 int methodReturnsPOD(SomeObject* obj) { return [obj returnsPOD]; };
 
-int FP_methodReturnsPODNilOk() { return methodReturnsPOD(nil); };
+int methodReturnsPODNilOk() { return methodReturnsPOD(nil); };
 
 int methodReturnsPODNotNilOK() {
   SomeObject* o = [SomeObject new];
   return methodReturnsPOD(o);
 }
+
+int testFalsyReturnedValueOk() {
+  int x = testCallMethodReturnsPODOk();
+
+  if (x != 0) {
+    int* int_ptr = nil;
+    return *int_ptr;
+  }
+}
+
+int testParamsRemainTheSameOk() {
+  SomeObject* obj = nil;
+  int x1 = 0;
+  int x2 = 5;
+  int x = [obj add:x1 andParam2:x2];
+
+  if (x1 != 0) {
+    int* int_ptr = nil;
+    return *int_ptr;
+  }
+
+  if (x2 != 5) {
+    int* int_ptr = nil;
+    return *int_ptr;
+  }
+}

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

@@ -1,9 +1,4 @@
 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 call to `ABFDataCreate` (modelled),allocation part of the trace ends here,memory becomes unreachable here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, FP_methodReturnsPODNilOk, 0, 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,when calling `methodReturnsPOD` here,parameter `obj` of methodReturnsPOD,when calling `SomeObject.returnsPOD` here,parameter `self` of SomeObject.returnsPOD,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, FP_testAccessPropertyAccessorOk, 2, 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 `SomeObject.x` here,parameter `self` of SomeObject.x,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, FP_testCallMethodReturnsPODOk, 2, 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 `SomeObject.returnsPOD` here,parameter `self` of SomeObject.returnsPOD,invalid access occurs here]
 codetoanalyze/objcpp/pulse/NPEBasic.mm, dereferenceNilBad, 2, 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/objcpp/pulse/NPEBasic.mm, testAccessPropertyAccessorBad, 2, 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 `SomeObject.ptr` here,parameter `self` of SomeObject.ptr,invalid access occurs here]
-codetoanalyze/objcpp/pulse/NPEBasic.mm, testCallMethodReturnsnonPODBad, 2, 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 `SomeObject.returnsnonPOD` here,parameter `self` of SomeObject.returnsnonPOD,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,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from 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,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,was invalidated by `delete`,use-after-lifetime part of the trace starts here,passed as argument to `new` (modelled),return from call to `new` (modelled),assigned,when calling `Simple::Simple` here,parameter `__param_0` of Simple::Simple,invalid access occurs here]