[java] model `Double` like `Integer`

Summary:
Get rid of false positive as in the test by modelling `Double`. Longer term we
should probably prevent biabduction from blocking the angelic analysis on
`Nullable` fields but that seems harder.

Reviewed By: jeremydubreil

Differential Revision: D14005228

fbshipit-source-id: 59ef2ed66

infer/models/java/src/java/lang/Double.java

@@ -0,0 +1,31 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+package java.lang;
+
+public final class Double {
+
+  protected final double value;
+
+  public Double(double i) {
+    this.value = i;
+  }
+
+  public static Double valueOf(double i) {
+    return new Double(i);
+  }
+
+  public boolean equals(Object anObject) {
+    return anObject != null
+        && anObject instanceof Double
+        && this.value == ((Double) anObject).value;
+  }
+
+  public double doubleValue() {
+    return this.value;
+  }
+}

infer/tests/codetoanalyze/java/infer/DoubleExample.java

@@ -0,0 +1,24 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+package codetoanalyze.java.infer;
+
+import javax.annotation.Nullable;
+
+public class DoubleExample {
+
+  @Nullable Double x;
+
+  private Double testAssignNonNullOk() {
+    x = 1.0;
+    return x + 1.0;
+  }
+
+  private Double testdReadNullableBad() {
+    return x + 1.0;
+  }
+}

infer/tests/codetoanalyze/java/infer/issues.exp

@@ -42,6 +42,7 @@ codetoanalyze/java/infer/CursorNPEs.java, codetoanalyze.java.infer.CursorNPEs.cu
 codetoanalyze/java/infer/DivideByZero.java, codetoanalyze.java.infer.DivideByZero.callDivideByZeroInterProc():int, 1, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure callDivideByZeroInterProc(),start of procedure divideByZeroInterProc(...)]
 codetoanalyze/java/infer/DivideByZero.java, codetoanalyze.java.infer.DivideByZero.divByZeroLocal(java.lang.String):int, 3, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure divByZeroLocal(...)]
 codetoanalyze/java/infer/DivideByZero.java, codetoanalyze.java.infer.DivideByZero.divideByZeroWithStaticField():int, 2, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure divideByZeroWithStaticField(),start of procedure setXToZero(),return from a call to void DivideByZero.setXToZero(),start of procedure divideByZeroInterProc(...)]
+codetoanalyze/java/infer/DoubleExample.java, codetoanalyze.java.infer.DoubleExample.testdReadNullableBad():java.lang.Double, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure testdReadNullableBad()]
 codetoanalyze/java/infer/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldBad():void, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure dispatchOnFieldBad(),start of procedure DynamicDispatch$Subtype(),start of procedure DynamicDispatch$Supertype(),return from a call to DynamicDispatch$Supertype.<init>(),return from a call to DynamicDispatch$Subtype.<init>(),start of procedure DynamicDispatch$WithField(...),return from a call to DynamicDispatch$WithField.<init>(DynamicDispatch$Subtype),start of procedure foo(),return from a call to Object DynamicDispatch$Subtype.foo()]
 codetoanalyze/java/infer/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeBad():void, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure dynamicDispatchCallsWrapperWithSubtypeBad(),start of procedure DynamicDispatch$Subtype(),start of procedure DynamicDispatch$Supertype(),return from a call to DynamicDispatch$Supertype.<init>(),return from a call to DynamicDispatch$Subtype.<init>(),start of procedure dynamicDispatchWrapperFoo(...),start of procedure foo(),return from a call to Object DynamicDispatch$Subtype.foo(),return from a call to Object DynamicDispatch.dynamicDispatchWrapperFoo(DynamicDispatch$Subtype)]
 codetoanalyze/java/infer/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure dynamicDispatchCallsWrapperWithSupertypeBad(),start of procedure DynamicDispatch$Supertype(),return from a call to DynamicDispatch$Supertype.<init>(),start of procedure dynamicDispatchWrapperBar(...),start of procedure bar(),return from a call to Object DynamicDispatch$Supertype.bar(),return from a call to Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)]