[infer][PR] Don't join postconditions. Fixes #678.

Summary:
Increases precision a bit. I didn't observe speed problems on what I tested. (But, who knows?)
Closes https://github.com/facebook/infer/pull/799

Reviewed By: jvillard

Differential Revision: D6284206

Pulled By: rgrig

fbshipit-source-id: 6f1e8631f

infer/src/biabduction/interproc.ml

@@ -665,7 +665,7 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma
         let vset = vset_add_pathset vset pathset_diverging in
         compute_visited vset
       in
-      (do_join_post pname tenv pathset, visited)
+      (pathset, visited)
     with Exceptions.Leak _ ->
       L.d_strln "Leak in post collection" ;
       assert false

infer/tests/build_systems/ant/issues.exp

@@ -113,7 +113,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.Nu
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRet():void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()]
-codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
+codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hashmapNPE(...)]

infer/tests/codetoanalyze/c/biabduction/arrays.c

@@ -0,0 +1,32 @@
+/*
+ * 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.
+ */
+#include <stdint.h>
+
+const char* GetVarint64Ptr(const char* p, const char* limit) {
+  for (uint32_t shift = 0; shift <= 63 && p < limit; shift += 7) {
+    uint64_t byte = *p;
+    p++;
+    if (!(byte & 128)) {
+      return p;
+    }
+  }
+  return 0;
+}
+
+char* data_;
+
+void DecodeCurrentValue() {
+  const char* limit = data_ + 1;
+  const char* newp = GetVarint64Ptr(data_, limit);
+  while (!newp) {
+  }
+  newp = GetVarint64Ptr(newp, limit);
+  while (!newp) {
+  }
+  // TODO: ensure this does not trigger assertion failure in Absarray (see
+  // T42274983)
+}

infer/tests/codetoanalyze/c/biabduction/issues.exp

@@ -1,4 +1,5 @@
 codetoanalyze/c/biabduction/abduce.c, FN_set_ptr_param_array_get_null_bad, 3, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure FN_set_ptr_param_array_get_null_bad()]
+codetoanalyze/c/biabduction/arrays.c, DecodeCurrentValue, 5, Assert_failure, no_bucket, ERROR, [start of procedure DecodeCurrentValue(),start of procedure GetVarint64Ptr(),Loop condition is true. Entering loop body,Loop condition is true. Entering loop body,Taking true branch,return from a call to GetVarint64Ptr,Loop condition is false. Leaving loop,start of procedure GetVarint64Ptr(),Loop condition is true. Entering loop body,Loop condition is false. Leaving loop,return from a call to GetVarint64Ptr]
 codetoanalyze/c/biabduction/example.c, bar, 2, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure bar()]
 codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure foo()]
 codetoanalyze/c/biabduction/example.c, global_addr_alias_bad, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure global_addr_alias_bad(),Taking true branch]

infer/tests/codetoanalyze/java/infer/NopFun.java

@@ -0,0 +1,32 @@
+/*
+ * 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.
+ */
+// Command: infer -g --biabduction-only
+class T {
+  static int q;
+
+  static void f() {
+    if (q == 0) {
+      q = 1;
+    } else if (q == 1) {
+      while (true) ;
+    }
+  }
+
+  static void h() {
+    // Important to have 2 branches, and one of them is (q==1).
+    if (q == 1) {
+    } else if (q == 2) {
+    }
+  }
+
+  static void go() {
+    q = 0;
+    f();
+    h(); // warning disappears if the NOP function h() is called here
+    f(); // should warn of PRECONDITION_NOT_MET here
+  }
+}

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

@@ -105,6 +105,7 @@ codetoanalyze/java/infer/JunitAssertion.java, codetoanalyze.java.infer.JunitAsse
 codetoanalyze/java/infer/Lists.java, codetoanalyze.java.infer.Lists.clearCausesEmptinessNPE(java.util.List,int):void, 5, NULL_DEREFERENCE, B1, ERROR, [start of procedure clearCausesEmptinessNPE(...),Taking true branch,Taking true branch]
 codetoanalyze/java/infer/Lists.java, codetoanalyze.java.infer.Lists.getElementNPE(java.util.List):void, 4, NULL_DEREFERENCE, B2, ERROR, [start of procedure getElementNPE(...),Taking false branch,start of procedure getElement(...),Taking true branch,return from a call to Object Lists.getElement(List)]
 codetoanalyze/java/infer/Lists.java, codetoanalyze.java.infer.Lists.removeInvalidatesNonEmptinessNPE(java.util.List,int):void, 5, NULL_DEREFERENCE, B1, ERROR, [start of procedure removeInvalidatesNonEmptinessNPE(...),Taking true branch,Taking true branch]
+codetoanalyze/java/infer/NopFun.java, T.go():void, 4, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure go(),start of procedure f(),Taking true branch,return from a call to void T.f(),start of procedure h(),Taking true branch,return from a call to void T.h()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars():void, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure npeWithDollars()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$E.dereferenceNullableInterfaceFieldBad():void, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceNullableInterfaceFieldBad()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.FP_noNullPointerExceptionAfterSkipFunction():void, 4, NULL_DEREFERENCE, B5, ERROR, [start of procedure FP_noNullPointerExceptionAfterSkipFunction(),Skipping String(...): unknown method,Skipping toString(): unknown method,start of procedure genericMethodSomewhereCheckingForNull(...),Taking true branch,return from a call to void NullPointerExceptions.genericMethodSomewhereCheckingForNull(String)]
@@ -118,7 +119,7 @@ codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.Nu
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefNullableRet(boolean):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure derefNullableRet(...),start of procedure nullableRet(...),Taking true branch,return from a call to Object NullPointerExceptions.nullableRet(boolean)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRet():void, 2, NULL_DEREFERENCE, B1, ERROR, [start of procedure derefUndefNullableRet(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet()]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.derefUndefNullableRetWrapper():void, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure derefUndefNullableRetWrapper(),start of procedure undefNullableWrapper(),Skipping undefNullableRet(): unknown method,Definition of undefNullableRet(),return from a call to Object NullPointerExceptions.undefNullableWrapper()]
-codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
+codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterLoopOnList(codetoanalyze.java.infer.NullPointerExceptions$L):void, 2, NULL_DEREFERENCE, B2, ERROR, [start of procedure dereferenceAfterLoopOnList(...),start of procedure returnsNullAfterLoopOnList(...),Taking true branch,Taking false branch,return from a call to Object NullPointerExceptions.returnsNullAfterLoopOnList(NullPointerExceptions$L)]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock1(java.util.concurrent.locks.Lock):void, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceAfterUnlock1(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.dereferenceAfterUnlock2(java.util.concurrent.locks.Lock):void, 6, NULL_DEREFERENCE, B1, ERROR, [start of procedure dereferenceAfterUnlock2(...),Skipping toString(): unknown method]
 codetoanalyze/java/infer/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.hashmapNPE(java.util.HashMap,java.lang.Object):java.lang.String, 1, NULL_DEREFERENCE, B2, ERROR, [start of procedure hashmapNPE(...)]

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

@@ -1,5 +1,5 @@
 codetoanalyze/java/infer/ArrayOutOfBounds.java, codetoanalyze.java.infer.ArrayOutOfBounds.arrayOutOfBounds():int, 2, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure arrayOutOfBounds(),Taking true branch,exception java.lang.ArrayIndexOutOfBoundsException,return from a call to int ArrayOutOfBounds.arrayOutOfBounds()]
-codetoanalyze/java/infer/ArrayOutOfBounds.java, codetoanalyze.java.infer.ArrayOutOfBounds.switchedArrsOutOfBounds():void, 2, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure switchedArrsOutOfBounds(),start of procedure buggyIter(...),Taking true branch,Taking false branch,return from a call to void ArrayOutOfBounds.buggyIter(int[],int[]),return from a call to void ArrayOutOfBounds.switchedArrsOutOfBounds()]
+codetoanalyze/java/infer/ArrayOutOfBounds.java, codetoanalyze.java.infer.ArrayOutOfBounds.switchedArrsOutOfBounds():void, 2, java.lang.ArrayIndexOutOfBoundsException, no_bucket, ERROR, [start of procedure switchedArrsOutOfBounds(),start of procedure buggyIter(...),Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking true branch,Taking false branch,return from a call to void ArrayOutOfBounds.buggyIter(int[],int[]),return from a call to void ArrayOutOfBounds.switchedArrsOutOfBounds()]
 codetoanalyze/java/infer/ClassCastExceptions.java, codetoanalyze.java.infer.ClassCastExceptions.classCastException():void, 3, java.lang.ClassCastException, no_bucket, ERROR, [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>(),Skipping ClassCastException(): unknown method,exception java.lang.ClassCastException,return from a call to void ClassCastExceptions.classCastException()]
 codetoanalyze/java/infer/ClassCastExceptions.java, codetoanalyze.java.infer.ClassCastExceptions.classCastExceptionImplementsInterface():int, 0, java.lang.ClassCastException, no_bucket, ERROR, [start of procedure classCastExceptionImplementsInterface(),start of procedure AnotherImplementationOfInterface(),return from a call to AnotherImplementationOfInterface.<init>(),start of procedure classCastExceptionImplementsInterfaceCallee(...),Skipping ClassCastException(): unknown method,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/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars():void, 3, java.lang.NullPointerException, no_bucket, ERROR, [start of procedure npeWithDollars(),exception java.lang.NullPointerException,return from a call to void NullPointerExceptions$$$Class$Name$With$Dollars.npeWithDollars()]