diff --git a/infer/lib/java/BUCK b/infer/lib/java/BUCK new file mode 100644 index 000000000..1584fade7 --- /dev/null +++ b/infer/lib/java/BUCK @@ -0,0 +1,7 @@ +prebuilt_jar( + name = 'models', + binary_jar = 'models.jar', + visibility = [ + 'PUBLIC' + ] +) diff --git a/infer/models/java/src/android/database/Cursor.java b/infer/models/java/src/android/database/Cursor.java index 4a0ac5272..2f364421f 100644 --- a/infer/models/java/src/android/database/Cursor.java +++ b/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; } diff --git a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java b/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java index be26d6445..165486774 100644 --- a/infer/models/java/src/com/facebook/infer/models/InferBuiltins.java +++ b/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); } diff --git a/infer/models/java/src/junit/framework/Assert.java b/infer/models/java/src/junit/framework/Assert.java index 648cdb801..1bf1b5510 100644 --- a/infer/models/java/src/junit/framework/Assert.java +++ b/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); } } diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 006847e68..a078bc68a 100644 --- a/infer/src/backend/symExec.ml +++ b/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 *) diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index d0da27735..f978b0c74 100644 --- a/infer/src/java/jTrans.ml +++ b/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 diff --git a/infer/tests/Makefile b/infer/tests/Makefile index 5f3af6447..b6d9fe536 100644 --- a/infer/tests/Makefile +++ b/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 diff --git a/infer/tests/codetoanalyze/java/infer/BUCK b/infer/tests/codetoanalyze/java/infer/BUCK index 4dd3957ff..e3eb9f763 100644 --- a/infer/tests/codetoanalyze/java/infer/BUCK +++ b/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( diff --git a/infer/tests/codetoanalyze/java/infer/Builtins.java b/infer/tests/codetoanalyze/java/infer/Builtins.java new file mode 100644 index 000000000..e2e78ebbb --- /dev/null +++ b/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(); + } + +} diff --git a/infer/tests/codetoanalyze/java/infer/build.xml b/infer/tests/codetoanalyze/java/infer/build.xml index 97c950a5c..5b85f32dd 100644 --- a/infer/tests/codetoanalyze/java/infer/build.xml +++ b/infer/tests/codetoanalyze/java/infer/build.xml @@ -8,7 +8,8 @@ - + + diff --git a/infer/tests/endtoend/java/infer/BuiltinsTest.java b/infer/tests/endtoend/java/infer/BuiltinsTest.java new file mode 100644 index 000000000..e7f07a619 --- /dev/null +++ b/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 + ) + ); + } + +} diff --git a/infer/tests/utils/InferRunner.java b/infer/tests/utils/InferRunner.java index 8b3018c54..8cd92dac1 100644 --- a/infer/tests/utils/InferRunner.java +++ b/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",