From f6784e3796a74335174ac16ba3bd80f76fd1dc62 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 24 Jun 2015 13:46:57 -0600 Subject: [PATCH] [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 | 7 +++ .../java/src/android/database/Cursor.java | 3 +- .../facebook/infer/models/InferBuiltins.java | 20 +++---- .../java/src/junit/framework/Assert.java | 17 +++--- infer/src/backend/symExec.ml | 5 +- infer/src/java/jTrans.ml | 4 +- infer/tests/Makefile | 3 +- infer/tests/codetoanalyze/java/infer/BUCK | 1 + .../codetoanalyze/java/infer/Builtins.java | 36 +++++++++++++ .../tests/codetoanalyze/java/infer/build.xml | 3 +- .../endtoend/java/infer/BuiltinsTest.java | 53 +++++++++++++++++++ infer/tests/utils/InferRunner.java | 1 + 12 files changed, 123 insertions(+), 30 deletions(-) create mode 100644 infer/lib/java/BUCK create mode 100644 infer/tests/codetoanalyze/java/infer/Builtins.java create mode 100644 infer/tests/endtoend/java/infer/BuiltinsTest.java 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",