[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

@@ -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();
+    }
+
 }

infer/src/checkers/modelTables.ml

@@ -131,6 +131,7 @@ let annotated_list_nullable =
     n2, "java.lang.RuntimeException.<init>(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 *)

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();
+  }
+
 }
 

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;
+  }
+
 }

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();
+  }
 }

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,

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,

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,