Model ObjC method isKindOfClass

Summary:public We model it as the builtin __instanceof which models the instanceof construct of Java.
The behaviour is the same.

Reviewed By: jvillard

Differential Revision: D2938969

fb-gh-sync-id: 2258de3
shipit-source-id: 2258de3

infer/src/clang/cFrontend_config.ml

@@ -19,6 +19,8 @@ let object_at_indexed_subscript_m = "objectAtIndexedSubscript:"
 
 let string_with_utf8_m = "stringWithUTF8String:"
 
+let is_kind_of_class = "isKindOfClass:"
+
 let nsstring_cl = "NSString"
 
 let nsobject_cl = "NSObject"

infer/src/clang/cFrontend_config.mli

@@ -65,6 +65,8 @@ val nsautorelease_pool_cl : string
 
 val string_with_utf8_m : string
 
+val is_kind_of_class : string
+
 val alloc : string
 
 val malloc : string

infer/src/clang/cTrans_models.ml

@@ -167,17 +167,23 @@ let get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procna
     mk_procname lang [(CFrontend_config.self, class_type)] Ast_expressions.create_void_type
     [] (Some SymExec.ModelBuiltins.__objc_release_autorelease_pool)
 
+let get_predefined_ms_is_kind_of_class class_name method_name mk_procname lang =
+  let condition = method_name = CFrontend_config.is_kind_of_class in
+  let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in
+  get_predefined_ms_method condition class_name method_name Procname.Instance_objc_method
+    mk_procname lang [(CFrontend_config.self, class_type)] Ast_expressions.create_BOOL_type
+    [] (Some SymExec.ModelBuiltins.__instanceof)
+
 let get_predefined_model_method_signature class_name method_name mk_procname lang =
-  match get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procname lang with
-  | Some ms -> Some ms
-  | None ->
+  let next_predefined f a = function
+    | Some _ as x -> x
+    | None -> f a method_name mk_procname lang in
   let class_type = Ast_expressions.create_class_type (class_name, `OBJC) in
-      match get_predefined_ms_retain_release class_type method_name mk_procname lang with
-      | Some ms -> Some ms
-      | None ->
-          match get_predefined_ms_stringWithUTF8String class_name method_name mk_procname lang with
-          | Some ms -> Some ms
-          | None -> get_predefined_ms_autoreleasepool_init class_name method_name mk_procname lang
+  get_predefined_ms_nsautoreleasepool_release class_name method_name mk_procname lang
+  |> next_predefined get_predefined_ms_retain_release class_type
+  |> next_predefined get_predefined_ms_stringWithUTF8String class_name
+  |> next_predefined get_predefined_ms_autoreleasepool_init class_name
+  |> next_predefined get_predefined_ms_is_kind_of_class class_name
 
 let dispatch_functions = [
   ("_dispatch_once", 1);

infer/tests/codetoanalyze/objc/errors/subtyping/KindOfClassExample.m

@@ -0,0 +1,67 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+#import <Foundation/NSObject.h>
+
+
+@interface Base : NSObject
+
++(int) returnsZero1: (Base*) b;
+
+@end
+
+@implementation Base
+
++(int) returnsZero1: (Base*) b {
+    if ([b isKindOfClass:[self class]]) {
+        return 0;
+    }
+    else {
+        return 1;
+    }
+}
+
+@end
+
+@interface Derived : Base
+
+@end
+
+@implementation Derived
+
+@end
+
+int returnsZero2(Base* b) {
+    if ([b isKindOfClass:[Derived class]]) {
+        return 1;
+    }
+    else {
+        return 0;
+    }
+}
+
+int shouldThrowDivideByZero1() {
+    Base* base = [[Base alloc] init];
+    return 1/[Base returnsZero1:base];
+}
+
+int shouldThrowDivideByZero2() {
+    Base* base = [[Base alloc] init];
+    return 1/returnsZero2(base);
+}
+
+int shouldThrowDivideByZero3() {
+    Base* b = [[Derived alloc] init];
+    if ([b isKindOfClass:[Derived class]]) {
+        return 1/0;
+    }
+    else {
+        return 0;
+    }
+}

infer/tests/endtoend/objc/KindOfClassTest.java

@@ -0,0 +1,66 @@
+/*
+ * Copyright (c) 2013 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package endtoend.objc;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsErrorInMethod.contains;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+import static utils.matchers.ResultContainsNoErrorInMethod.doesNotContain;
+
+
+import com.google.common.collect.ImmutableList;
+
+import org.junit.BeforeClass;
+import org.junit.ClassRule;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.DebuggableTemporaryFolder;
+import utils.InferException;
+import utils.InferResults;
+import utils.InferRunner;
+
+public class KindOfClassTest {
+
+  public static final String FILE =
+      "infer/tests/codetoanalyze/objc/errors/subtyping/KindOfClassExample.m";
+
+  public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
+
+  private static ImmutableList<String> inferCmd;
+
+  @ClassRule
+  public static DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
+
+  @BeforeClass
+  public static void runInfer() throws InterruptedException, IOException {
+    inferCmd = InferRunner.createiOSInferCommandWithMLBuckets(folder, FILE, "cf", true);
+  }
+
+  @Test
+  public void nullDereferenceTest() throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferC(inferCmd);
+    String[] procedures = {
+        "shouldThrowDivideByZero1",
+        "shouldThrowDivideByZero2",
+        "shouldThrowDivideByZero3"
+    };
+    assertThat(
+        "Results should contain divide by zero",
+        inferResults,
+        containsExactly(
+            DIVIDE_BY_ZERO,
+            FILE,
+            procedures
+        )
+    );
+  }
+}