[infer][models] Fixing InferAssume

Summary:
@public
Using InferBuiltins.assume previously caused an assertion failure in the analyzer. Fixed this, and fixed the implementation of the assume builtin to block when the assumed condition cannot hold.

Test Plan: Added several new tests.

infer/lib/java/BUCK

@@ -0,0 +1,7 @@
+prebuilt_jar(
+    name = 'models',
+    binary_jar = 'models.jar',
+    visibility = [
+        'PUBLIC'
+    ]
+)

infer/models/java/src/android/database/Cursor.java

@@ -9,6 +9,7 @@ package android.database;
 import java.io.Closeable;
 
 import com.facebook.infer.models.InferUndefined;
+import com.facebook.infer.models.InferBuiltins;
 
 import android.database.sqlite.SQLiteCursor;
 
@@ -27,7 +28,7 @@ public class Cursor implements Closeable {
 
     public int getColumnIndex(String columnName) {
       int index = InferUndefined.int_undefined();
-      while (index < -1) {}
+      InferBuiltins.assume(index < -1);
       return index;
     }
 

infer/models/java/src/com/facebook/infer/models/InferBuiltins.java

@@ -8,24 +8,20 @@ package com.facebook.infer.models;
 
 public class InferBuiltins {
 
-    public static void __set_file_attribute(Object o) {
-    }
+    public native static void __set_file_attribute(Object o);
 
-    public static void __set_mem_attribute(Object o) {
-    }
+    public native static void __set_mem_attribute(Object o);
 
-    public static void __set_lock_attribute(Object o) {
-    }
+    public native static void __set_lock_attribute(Object o);
 
-    public static void _exit() {
-    }
+    public native static void _exit();
+
+    private native static void __infer_assume(boolean condition);
 
     public static void assume(boolean condition) {
-      while (!condition) {}
+      __infer_assume(condition);
     }
 
-    public static String __split_get_nth(String s, String sep, int n) {
-        return null;
-    }
+    public native static String __split_get_nth(String s, String sep, int n);
 
 }

infer/models/java/src/junit/framework/Assert.java

@@ -5,29 +5,24 @@
 
 package junit.framework;
 
-public class Assert {
+import com.facebook.infer.models.InferBuiltins;
 
-    public static void assume(boolean condition) {
-        if (!condition) {
-            while (true) {
-            }
-        }
-    }
+public class Assert {
 
     public static void assertTrue(boolean condition) {
-        assume(condition);
+        InferBuiltins.assume(condition);
     }
 
     public static void assertTrue(String message, boolean condition) {
-        assume(condition);
+        InferBuiltins.assume(condition);
     }
 
     public static void assertFalse(boolean condition) {
-        assume(!condition);
+        InferBuiltins.assume(!condition);
     }
 
     public static void assertFalse(String message, boolean condition) {
-        assume(!condition);
+        InferBuiltins.assume(!condition);
     }
 
 }

infer/src/backend/symExec.ml

@@ -2117,13 +2117,14 @@ module ModelBuiltins = struct
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
   (* forces the expression passed as parameter to be assumed true at the point where this
-  builtin is called *)
+  builtin is called, blocks if this causes an inconsistency *)
   let execute___infer_assume
       cfg pdesc instr tenv prop path ret_ids args callee_pname loc: Builtin.ret_typ =
     match args with
     | [(lexp, typ)] ->
         let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop in
-        [(prop_assume, path)]
+        if Prover.check_inconsistency prop_assume then execute_diverge prop_assume path
+        else [(prop_assume, path)]
     | _ -> raise (Exceptions.Wrong_argument_number (try assert false with Assert_failure x -> x))
 
   (* creates a named error state *)

infer/src/java/jTrans.ml

@@ -632,8 +632,8 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
       init
       expr_list in
   let callee_procname =
-    if JBasics.cn_equal cn JConfig.infer_builtins_cl then
-      Procname.from_string (JBasics.ms_name ms)
+    let proc = Procname.from_string (JBasics.ms_name ms) in
+    if JBasics.cn_equal cn JConfig.infer_builtins_cl && SymExec.function_is_builtin proc then proc
     else Cfg.Procdesc.get_proc_name callee_procdesc in
   let call_idl, call_instrs =
     let callee_fun = Sil.Const (Sil.Cfun callee_procname) in

infer/tests/Makefile

@@ -1,5 +1,6 @@
 
 ANNOTATIONS_JAR = ../annotations/annotations.jar
+MODELS_JAR = ../lib/java/models.jar
 JACKSON_JAR = ../../dependencies/java/jackson/jackson-2.2.3.jar
 ANDROID_JAR = ../lib/java/android/android-19.jar
 GUAVA_JAR = ../../dependencies/java/guava/guava-10.0.1-fork.jar
@@ -16,7 +17,7 @@ TRACING_CMD = $(INFERJ) -o $(TRACING_OUT) -a tracing $(TRACING_JAVAC_CMD)
 INFER_OUT = infer_out
 INFER_REPORT = $(INFER_OUT)/report.csv
 INFER_SOURCES = $(shell find codetoanalyze/java/infer -name "*.java")
-INFER_JAVAC_CMD = javac -cp $(JACKSON_JAR):$(ANDROID_JAR) $(INFER_SOURCES)
+INFER_JAVAC_CMD = javac -cp $(JACKSON_JAR):$(ANDROID_JAR):$(MODELS_JAR) $(INFER_SOURCES)
 INFER_CMD = $(INFERJ) -o $(INFER_OUT) -a infer $(INFER_JAVAC_CMD)
 
 ERADICATE_OUT = eradicate_out

infer/tests/codetoanalyze/java/infer/BUCK

@@ -3,6 +3,7 @@ sources = glob(['**/*.java'])
 dependencies = [
     '//infer/lib/java/android:android',
     '//dependencies/java/jackson:jackson',
+    '//infer/lib/java:models'
 ]
 
 java_library(

infer/tests/codetoanalyze/java/infer/Builtins.java

@@ -0,0 +1,36 @@
+/*
+ * Copyright (c) 2013- Facebook.
+ * All rights reserved.
+ */
+
+package codetoanalyze.java.infer;
+
+import com.facebook.infer.models.InferBuiltins;
+
+public class Builtins {
+
+  void blockError() {
+    Object x = null;
+    InferBuiltins.assume(x != null);
+    x.toString();
+  }
+
+  void doNotBlockError(Object x) {
+    Object y = null;
+    InferBuiltins.assume(x != null);
+    y.toString();
+  }
+
+  void blockErrorIntAssume(Object x) {
+    Object y = null;
+    int i = 0;
+    InferBuiltins.assume(i != 0);
+    y.toString();
+  }
+
+  void causeError(Object x) {
+    InferBuiltins.assume(x == null);
+    x.toString();
+  }
+
+}

infer/tests/codetoanalyze/java/infer/build.xml

@@ -8,7 +8,8 @@
         <mkdir dir="ant_out"/>
         <javac srcdir="." destdir="ant_out" includeantruntime="false">
             <bootclasspath>
-                <pathelement location="../../../../lib/java/android/android-19.jar"/>
+              <pathelement location="../../../../lib/java/android/android-19.jar"/>
+              <pathelement location="../../../../lib/java/models.jar"/>
             </bootclasspath>
             <classpath>
               <pathelement location="../../../dependencies/java/jackson/jackson-2.2.3.jar"/>

infer/tests/endtoend/java/infer/BuiltinsTest.java

@@ -0,0 +1,53 @@
+/*
+ * Copyright (c) 2013- Facebook.
+ * All rights reserved.
+ */
+
+package endtoend.java.infer;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.InferException;
+import utils.InferResults;
+
+public class BuiltinsTest {
+
+  public static final String SOURCE_FILE =
+      "infer/tests/codetoanalyze/java/infer/Builtins.java";
+
+  public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
+
+  private static InferResults inferResults;
+
+  @BeforeClass
+  public static void loadResults() throws InterruptedException, IOException {
+    inferResults = InferResults.loadInferResults(
+        BuiltinsTest.class,
+        SOURCE_FILE);
+  }
+
+  @Test
+  public void matchErrors()
+      throws IOException, InterruptedException, InferException {
+    String[] methods = {
+      "doNotBlockError",
+      "causeError"
+    };
+     assertThat(
+        "Results should contain " + NULL_DEREFERENCE,
+        inferResults,
+        containsExactly(
+            NULL_DEREFERENCE,
+            SOURCE_FILE,
+            methods
+        )
+    );
+  }
+
+}

infer/tests/utils/InferRunner.java

@@ -42,6 +42,7 @@ public class InferRunner {
       "/infer/lib/java/android/android-19.jar";
 
   private static final String[] LIBRARIES = {
+      "/infer/lib/java/models.jar",
       "/infer/annotations/annotations.jar",
       "/dependencies/java/guava/guava-10.0.1-fork.jar",
       "/dependencies/java/jackson/jackson-2.2.3.jar",