[infer][java] Use lazy dynamic dispatch by default

Summary: Use the lazy dynamic dispatch by default in prod for the Java analysis

Reviewed By: sblackshear

Differential Revision: D4356872

fbshipit-source-id: 491e92e

infer/models/java/src/java/util/AbstractList.java

@@ -12,7 +12,7 @@ package java.util;
 import com.facebook.infer.builtins.InferUndefined;
 
 // could make List an abstract class directly instead, but that breaks other models
-public abstract class AbstractList<T> extends AbstractCollection<T> implements List<T> {
+public abstract class AbstractList<T> extends AbstractCollection<T> {
 
   // need three-value state for unknown (-1), false (0), or true (1)
   // the reason we can't use a bool is that we want to return either true or false each time we call
@@ -25,7 +25,6 @@ public abstract class AbstractList<T> extends AbstractCollection<T> implements L
     mIsEmpty = 1;
   }
 
-  @Override
   public boolean isEmpty() {
     if (mIsEmpty < 0) {
       if (InferUndefined.boolean_undefined()) {
@@ -37,18 +36,15 @@ public abstract class AbstractList<T> extends AbstractCollection<T> implements L
     return mIsEmpty == 1;
   }
 
-  @Override
   public void add(int index, T toAdd) {
     mIsEmpty = 0;
   }
 
-  @Override
   public T remove(int index) {
     mIsEmpty = -1;
     return any();
   }
 
-  @Override
   public boolean remove(Object o) {
     boolean result = InferUndefined.boolean_undefined();
     if (result) {
@@ -57,7 +53,6 @@ public abstract class AbstractList<T> extends AbstractCollection<T> implements L
     return result;
   }
 
-  @Override
   public void clear() {
     mIsEmpty = 1;
   }

infer/models/java/src/java/util/ArrayList.java

@@ -14,7 +14,7 @@ import java.io.Serializable;
 // abstract so we don't have to implement every method of List
 public abstract class ArrayList<T>
   extends AbstractList<T>
-  implements List<T>, RandomAccess, Cloneable, Serializable {
+  implements RandomAccess, Cloneable, Serializable {
 
   @Override
   public boolean isEmpty() {

infer/models/java/src/java/util/HashMap.java

@@ -75,8 +75,7 @@ public abstract class HashMap<K,V> extends AbstractMap<K,V>
 
   /* does explicit dynamic dispatch to help Infer out */
   private static boolean areEqual(Object x, Object y) {
-      return x == y
-          || (x instanceof Integer && ((Integer) x).equals(y));
+    return x == y;
   }
 
 }

infer/models/java/src/java/util/LinkedList.java

@@ -13,8 +13,8 @@ import java.io.Serializable;
 
 // abstract so we don't have to implement every method of List
 public abstract class LinkedList<T>
-  extends AbstractSequentialList<T>
-  implements Serializable, Cloneable, Iterable<T>, Collection<T>, Deque<T>, List<T>, Queue<T> {
+  extends AbstractList<T>
+  implements Serializable, Cloneable, Iterable<T>, Collection<T>, Deque<T>, Queue<T> {
 
   @Override
   public boolean isEmpty() {

infer/models/java/src/java/util/List.java

@@ -0,0 +1,44 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package java.util;
+
+import java.io.Serializable;
+
+// abstract so we don't have to implement every method of List
+public abstract class List<T>
+  extends AbstractList<T>
+  implements Collection<T>, Iterable<T> {
+
+  @Override
+  public boolean isEmpty() {
+    return super.isEmpty();
+  }
+
+  @Override
+  public void add(int index, T toAdd) {
+    super.add(index, toAdd);
+  }
+
+  @Override
+  public T remove(int index) {
+    return super.remove(index);
+  }
+
+  @Override
+  public boolean remove(Object o) {
+    return super.remove(o);
+  }
+
+  @Override
+  public void clear() {
+    super.clear();
+  }
+
+}

infer/src/backend/symExec.ml

@@ -646,7 +646,7 @@ let resolve_and_analyze
       (* Create the type sprecialized procedure description and analyze it directly *)
       Option.iter
         ~f:(fun specialized_pdesc ->
-           Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
+            Ondemand.analyze_proc_desc ~propagate_exceptions:true caller_pdesc specialized_pdesc)
         (match Ondemand.get_proc_desc resolved_pname with
          | Some resolved_proc_desc ->
              Some resolved_proc_desc
@@ -654,7 +654,7 @@ let resolve_and_analyze
              begin
                Option.map
                  ~f:(fun callee_proc_desc ->
-                    Cfg.specialize_types callee_proc_desc resolved_pname args)
+                     Cfg.specialize_types callee_proc_desc resolved_pname args)
                  (Ondemand.get_proc_desc callee_proc_name)
              end) in
   let resolved_pname = match callee_proc_name with
@@ -1060,12 +1060,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       | None -> (
           match callee_pname with
           | Java callee_pname_java when Config.dynamic_dispatch = `Lazy ->
-              let norm_prop, norm_args =
-                normalize_params
-                  tenv
-                  current_pname
-                  prop_
-                  (call_constructor_url_update_args callee_pname actual_params) in
+              let norm_prop, norm_args' = normalize_params tenv current_pname prop_ actual_params in
+              let norm_args = call_constructor_url_update_args callee_pname norm_args' in
               let exec_skip_call skipped_pname ret_annots ret_type =
                 skip_call norm_prop path skipped_pname ret_annots loc ret_id
                   (Some ret_type) norm_args in

infer/src/base/Config.ml

@@ -1563,7 +1563,9 @@ let clang_frontend_action_string =
     ((if clang_frontend_do_capture then ["translating"] else [])
      @ (if clang_frontend_do_lint then ["linting"] else []))
 
-let dynamic_dispatch = if analyzer = Tracing then `Lazy else !dynamic_dispatch
+let dynamic_dispatch =
+  if analyzer = Tracing || analyzer = Infer then `Lazy
+  else !dynamic_dispatch
 
 let specs_library =
   match infer_cache with

infer/tests/build_systems/ant/issues.exp

@@ -24,7 +24,7 @@ codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPrefsFromContent
 codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.queryUVMLegacyDbNotClosed(), 4, RESOURCE_LEAK, [start of procedure queryUVMLegacyDbNotClosed(),Taking true branch]
 codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasy(), 3, NULL_DEREFERENCE, [start of procedure dynamicDispatchShouldNotCauseFalseNegativeEasy(),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 foo(),return from a call to Object DynamicDispatch$Subtype.foo()]
 codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasy(), 3, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeEasy(),start of procedure DynamicDispatch$Impl(),return from a call to DynamicDispatch$Impl.<init>(),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()]
-codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Interface), 2, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeHard(...),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()]
+codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Impl), 1, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeHard(...),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()]
 codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.bufferedInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure bufferedInputStreamNotClosedAfterRead(),exception java.io.IOException]
 codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.checkedInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure checkedInputStreamNotClosedAfterRead(),exception java.io.IOException]
 codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.cipherInputStreamNotClosedAfterSkip(), 7, RESOURCE_LEAK, [start of procedure cipherInputStreamNotClosedAfterSkip(),exception java.io.IOException]
@@ -99,7 +99,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.
 codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case]
 codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor(), 6, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFaillingResourceConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case]
 codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionInArrayLengthLoop(java.lang.Object[]), 3, NULL_DEREFERENCE, [start of procedure nullPointerExceptionInArrayLengthLoop(...),Taking true branch]
-codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.<init>(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(Object),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch]
+codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.<init>(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(NullPointerExceptions$A),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch]
 codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullArrayParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullArrayParameter(),start of procedure expectNotNullArrayParameter(...)]
 codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullObjectParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullObjectParameter(),start of procedure expectNotNullObjectParameter(...)]
 codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullableFieldNPE(), 1, NULL_DEREFERENCE, [start of procedure nullableFieldNPE()]

infer/tests/build_systems/buck/issues.exp

@@ -24,7 +24,7 @@ infer/tests/codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.loadPref
 infer/tests/codetoanalyze/java/infer/CursorLeaks.java, void CursorLeaks.queryUVMLegacyDbNotClosed(), 4, RESOURCE_LEAK, [start of procedure queryUVMLegacyDbNotClosed(),Taking true branch]
 infer/tests/codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.dynamicDispatchShouldNotCauseFalseNegativeEasy(), 3, NULL_DEREFERENCE, [start of procedure dynamicDispatchShouldNotCauseFalseNegativeEasy(),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 foo(),return from a call to Object DynamicDispatch$Subtype.foo()]
 infer/tests/codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeEasy(), 3, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeEasy(),start of procedure DynamicDispatch$Impl(),return from a call to DynamicDispatch$Impl.<init>(),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()]
-infer/tests/codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Interface), 2, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeHard(...),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()]
+infer/tests/codetoanalyze/java/infer/DynamicDispatch.java, void DynamicDispatch.interfaceShouldNotCauseFalseNegativeHard(DynamicDispatch$Impl), 1, NULL_DEREFERENCE, [start of procedure interfaceShouldNotCauseFalseNegativeHard(...),start of procedure foo(),return from a call to Object DynamicDispatch$Impl.foo()]
 infer/tests/codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.bufferedInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure bufferedInputStreamNotClosedAfterRead(),exception java.io.IOException]
 infer/tests/codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.checkedInputStreamNotClosedAfterRead(), 7, RESOURCE_LEAK, [start of procedure checkedInputStreamNotClosedAfterRead(),exception java.io.IOException]
 infer/tests/codetoanalyze/java/infer/FilterInputStreamLeaks.java, void FilterInputStreamLeaks.cipherInputStreamNotClosedAfterSkip(), 7, RESOURCE_LEAK, [start of procedure cipherInputStreamNotClosedAfterSkip(),exception java.io.IOException]
@@ -99,7 +99,7 @@ infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointe
 infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFailingFileOutputStreamConstructor(), 7, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFailingFileOutputStreamConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case]
 infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionFromFaillingResourceConstructor(), 6, NULL_DEREFERENCE, [start of procedure nullPointerExceptionFromFaillingResourceConstructor(),exception java.io.FileNotFoundException,Switch condition is true. Entering switch case]
 infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionInArrayLengthLoop(java.lang.Object[]), 3, NULL_DEREFERENCE, [start of procedure nullPointerExceptionInArrayLengthLoop(...),Taking true branch]
-infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.<init>(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(Object),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch]
+infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionUnlessFrameFails(), 4, NULL_DEREFERENCE, [start of procedure nullPointerExceptionUnlessFrameFails(),start of procedure NullPointerExceptions$A(...),return from a call to NullPointerExceptions$A.<init>(NullPointerExceptions),start of procedure frame(...),start of procedure id_generics(...),return from a call to Object NullPointerExceptions.id_generics(NullPointerExceptions$A),return from a call to NullPointerExceptions$A NullPointerExceptions.frame(NullPointerExceptions$A),Taking true branch]
 infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullArrayParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullArrayParameter(),start of procedure expectNotNullArrayParameter(...)]
 infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullPointerExceptionWithNullObjectParameter(), 1, NULL_DEREFERENCE, [start of procedure nullPointerExceptionWithNullObjectParameter(),start of procedure expectNotNullObjectParameter(...)]
 infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java, void NullPointerExceptions.nullableFieldNPE(), 1, NULL_DEREFERENCE, [start of procedure nullableFieldNPE()]

infer/tests/codetoanalyze/java/infer/DynamicDispatch.java

@@ -27,12 +27,14 @@ public class DynamicDispatch {
     i.foo().toString();
   }
 
-  // TODO: this test currently fails, but will pass with handling of dynamic dispatch
   static void interfaceShouldNotCauseFalseNegativeHard(Interface i) {
-    // should be a warning since Impl's implementation of foo returns null
     i.foo().toString();
   }
 
+  static void callWithBadImplementation(Impl impl) {
+    interfaceShouldNotCauseFalseNegativeHard(impl);
+  }
+
   static class Supertype {
     Object foo() {
       return new Object();

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

@@ -1,7 +1,6 @@
 codetoanalyze/java/infer/ArrayOutOfBounds.java, int ArrayOutOfBounds.arrayOutOfBounds(), 2, java.lang.ArrayIndexOutOfBoundsException, [start of procedure arrayOutOfBounds(),Taking true branch,exception java.lang.ArrayIndexOutOfBoundsException,return from a call to int ArrayOutOfBounds.arrayOutOfBounds()]
 codetoanalyze/java/infer/ClassCastExceptions.java, int ClassCastExceptions.classCastExceptionImplementsInterface(), 0, java.lang.ClassCastException, [start of procedure classCastExceptionImplementsInterface(),start of procedure AnotherImplementationOfInterface(),return from a call to AnotherImplementationOfInterface.<init>(),start of procedure classCastExceptionImplementsInterfaceCallee(...),exception java.lang.ClassCastException,return from a call to int ClassCastExceptions.classCastExceptionImplementsInterfaceCallee(AnotherImplementationOfInterface),exception java.lang.ClassCastException,return from a call to int ClassCastExceptions.classCastExceptionImplementsInterface()]
 codetoanalyze/java/infer/ClassCastExceptions.java, void ClassCastExceptions.classCastException(), 3, java.lang.ClassCastException, [start of procedure classCastException(),start of procedure SubClassA(),start of procedure SuperClass(),return from a call to SuperClass.<init>(),return from a call to SubClassA.<init>(),exception java.lang.ClassCastException,return from a call to void ClassCastExceptions.classCastException()]
-codetoanalyze/java/infer/ClassCastExceptions.java, void ClassCastExceptions.openHttpURLConnection(), 4, java.lang.ClassCastException, [start of procedure openHttpURLConnection(),start of procedure getURL(),return from a call to String ClassCastExceptions.getURL(),Taking true branch,exception java.lang.ClassCastException,return from a call to void ClassCastExceptions.openHttpURLConnection()]
 codetoanalyze/java/infer/CloseableAsResourceExample.java, T CloseableAsResourceExample.sourceOfNullWithResourceLeak(), 1, RESOURCE_LEAK, [start of procedure sourceOfNullWithResourceLeak(),start of procedure SomeResource(),return from a call to SomeResource.<init>()]
 codetoanalyze/java/infer/CloseableAsResourceExample.java, void CloseableAsResourceExample.failToCloseWithCloseQuietly(), 5, RESOURCE_LEAK, [start of procedure failToCloseWithCloseQuietly(),start of procedure SomeResource(),return from a call to SomeResource.<init>(),Taking true branch,start of procedure doSomething(),Taking true branch,start of procedure LocalException(),return from a call to LocalException.<init>(),Taking true branch,exception codetoanalyze.java.infer.LocalException,return from a call to void SomeResource.doSomething()]
 codetoanalyze/java/infer/CloseableAsResourceExample.java, void CloseableAsResourceExample.leakFoundWhenIndirectlyImplementingCloseable(), 1, RESOURCE_LEAK, [start of procedure leakFoundWhenIndirectlyImplementingCloseable(),start of procedure CloseableAsResourceExample$MyResource(...),return from a call to CloseableAsResourceExample$MyResource.<init>(CloseableAsResourceExample)]