Shared: Bugfix for unique value implication.

Author: aschackmull

java/ql/test/library-tests/guards/Guards.java

@@ -127,4 +127,20 @@ void t6() {
       chk(); // $ guarded='o != null:false' guarded=g(1):false
     }
   }
+
+  void t7(int[] a) {
+    boolean found = false;
+    for (int i = 0; i < a.length; i++) {
+      boolean answer = a[i] == 42;
+      if (answer) {
+        found = true;
+      }
+      if (found) {
+        chk(); // $ guarded=found:true guarded='i < a.length:true'
+      }
+    }
+    if (found) {
+      chk(); // $ guarded=found:true guarded='i < a.length:false'
+    }
+  }
 }

java/ql/test/library-tests/guards/GuardsInline.expected

@@ -54,3 +54,7 @@
 | Guards.java:125:7:125:11 | chk(...) | 'o != null:true' |
 | Guards.java:127:7:127:11 | chk(...) | 'o != null:false' |
 | Guards.java:127:7:127:11 | chk(...) | g(1):false |
+| Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' |
+| Guards.java:139:9:139:13 | chk(...) | found:true |
+| Guards.java:143:7:143:11 | chk(...) | 'i < a.length:false' |
+| Guards.java:143:7:143:11 | chk(...) | found:true |

shared/controlflow/codeql/controlflow/Guards.qll

@@ -647,6 +647,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
      */
     private predicate uniqueValue(SsaDefinition v, Expr e, GuardValue k) {
       possibleValue(v, false, e, k) and
+      not possibleValue(v, true, e, k) and
       forex(Expr other, GuardValue otherval | possibleValue(v, _, other, otherval) and other != e |
         disjointValues(otherval, k)
       )