From 629b09307fbd7061eccf34085eb7255195b575c9 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 10 Sep 2015 06:06:06 -0200 Subject: [PATCH] [Models] Add model for System.getProperty for Infer and Eradicate Summary: System.getProperty can return null when the property is not found, and expects a non-null argument. Add models for Infer and Eradicate to reflect that. --- infer/models/java/src/java/lang/System.java | 9 +++++++++ infer/src/checkers/modelTables.ml | 1 + .../codetoanalyze/java/eradicate/NullMethodCall.java | 7 +++++++ .../java/eradicate/ParameterNotNullable.java | 7 +++++++ .../java/infer/NullPointerExceptions.java | 10 ++++++++++ .../endtoend/java/eradicate/NullMethodCallTest.java | 1 + .../java/eradicate/ParameterNotNullableTest.java | 1 + .../endtoend/java/infer/NullPointerExceptionTest.java | 4 +++- 8 files changed, 39 insertions(+), 1 deletion(-) diff --git a/infer/models/java/src/java/lang/System.java b/infer/models/java/src/java/lang/System.java index 69fbd28a9..24b0e7309 100644 --- a/infer/models/java/src/java/lang/System.java +++ b/infer/models/java/src/java/lang/System.java @@ -10,6 +10,7 @@ package java.lang; import com.facebook.infer.models.InferBuiltins; +import com.facebook.infer.models.InferUndefined; import java.io.ByteArrayInputStream; import java.io.ByteArrayOutputStream; @@ -39,4 +40,12 @@ public final class System { InferBuiltins._exit(); } + public static String getProperty(String key) { + int n = key.length(); // key must not be null + if (InferUndefined.boolean_undefined()) { + return null; + } + return InferUndefined.string_undefined(); + } + } diff --git a/infer/src/checkers/modelTables.ml b/infer/src/checkers/modelTables.ml index cfd128210..279e13799 100644 --- a/infer/src/checkers/modelTables.ml +++ b/infer/src/checkers/modelTables.ml @@ -131,6 +131,7 @@ let annotated_list_nullable = n2, "java.lang.RuntimeException.(java.lang.String,java.lang.Throwable)"; n1, "java.lang.String.equals(java.lang.Object):boolean"; n1, "java.lang.StringBuilder.append(java.lang.String):java.lang.StringBuilder"; + (n, [o]), "java.lang.System.getProperty(java.lang.String):java.lang.String"; on, "java.net.URLClassLoader.newInstance(java.net.URL[],java.lang.ClassLoader):java.net.URLClassLoader"; n1, "java.util.AbstractList.equals(java.lang.Object):boolean"; ca, "java.util.ArrayList.add(java.lang.Object):boolean"; (* container add *) diff --git a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java index e2a21069a..9d533953a 100644 --- a/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java +++ b/infer/tests/codetoanalyze/java/eradicate/NullMethodCall.java @@ -11,6 +11,7 @@ package codetoanalyze.java.eradicate; import com.google.common.base.Preconditions; +import java.lang.System; import javax.annotation.Nullable; import com.facebook.infer.annotation.Assertions; @@ -232,5 +233,11 @@ public class NullMethodCall { s.toString().isEmpty(); } } + + public void testSystemGetPropertyReturn() { + String s = System.getProperty(""); + int n = s.length(); + } + } diff --git a/infer/tests/codetoanalyze/java/eradicate/ParameterNotNullable.java b/infer/tests/codetoanalyze/java/eradicate/ParameterNotNullable.java index 9292e0b40..5c5c413c9 100644 --- a/infer/tests/codetoanalyze/java/eradicate/ParameterNotNullable.java +++ b/infer/tests/codetoanalyze/java/eradicate/ParameterNotNullable.java @@ -9,6 +9,7 @@ package codetoanalyze.java.eradicate; +import java.lang.System; import javax.annotation.Nullable; import android.annotation.SuppressLint; @@ -64,4 +65,10 @@ public class ParameterNotNullable { return new ParameterNotNullable(null); } } + + public @Nullable String testSystemGetPropertyArgument() { + String s = System.getProperty(null); + return s; + } + } diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java index 66836ac05..72bb7224d 100644 --- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java +++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java @@ -24,6 +24,7 @@ import java.io.File; import java.io.FileInputStream; import java.io.FileOutputStream; import java.io.IOException; +import java.lang.System; import java.util.HashMap; public class NullPointerExceptions { @@ -393,4 +394,13 @@ public class NullPointerExceptions { o.toString(); } + public @Nullable String testSystemGetPropertyArgument() { + String s = System.getProperty(null); + return s; + } + + public void testSystemGetPropertyReturn() { + String s = System.getProperty(""); + int n = s.length(); + } } diff --git a/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java b/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java index 72c320488..9d6787823 100644 --- a/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java +++ b/infer/tests/endtoend/java/eradicate/NullMethodCallTest.java @@ -45,6 +45,7 @@ public class NullMethodCallTest { "outerPrivateField", "testFieldAssignmentIfThenElse", "testExceptionPerInstruction", + "testSystemGetPropertyReturn", }; assertThat( "Results should contain " + NULL_METHOD_CALL, diff --git a/infer/tests/endtoend/java/eradicate/ParameterNotNullableTest.java b/infer/tests/endtoend/java/eradicate/ParameterNotNullableTest.java index aaedc9264..efc39b155 100644 --- a/infer/tests/endtoend/java/eradicate/ParameterNotNullableTest.java +++ b/infer/tests/endtoend/java/eradicate/ParameterNotNullableTest.java @@ -42,6 +42,7 @@ public class ParameterNotNullableTest { String[] methods = { "callNull", "callNullable", + "testSystemGetPropertyArgument", }; assertThat( "Results should contain " + PARAMETER_NOT_NULLABLE, diff --git a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java index 7d7b95b07..0d44c9b03 100644 --- a/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java +++ b/infer/tests/endtoend/java/infer/NullPointerExceptionTest.java @@ -61,7 +61,9 @@ public class NullPointerExceptionTest { "nullPointerExceptionArrayLength", "npeWithDollars", "someNPEAfterResourceLeak", - "derefNullableGetter" + "derefNullableGetter", + "testSystemGetPropertyArgument", + "testSystemGetPropertyReturn", }; assertThat( "Results should contain " + NULL_DEREFERENCE,