Ssa: Extend consistency checks and reduce phi read nodes

java/ql/consistency-queries/SsaConsistency.ql

@@ -0,0 +1,3 @@
+import java
+import semmle.code.java.dataflow.internal.SsaImpl
+import Impl::Consistency

java/ql/lib/semmle/code/java/dataflow/internal/BaseSSA.qll

@@ -168,12 +168,15 @@ private module SsaInput implements SsaImplCommon::InputSig<Location> {
    * Holds if the `i`th of basic block `bb` reads source variable `v`.
    */
   predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
-    exists(VarRead use |
-      v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true
+    hasDominanceInformation(bb) and
+    (
+      exists(VarRead use |
+        v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true
+      )
+      or
+      variableCapture(v, _, bb, i) and
+      certain = false
     )
-    or
-    variableCapture(v, _, bb, i) and
-    certain = false
   }
 }
 

java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll

@@ -204,12 +204,15 @@ private module SsaInput implements SsaImplCommon::InputSig<Location> {
    * This includes implicit reads via calls.
    */
   predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
-    exists(VarRead use |
-      v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true
+    hasDominanceInformation(bb) and
+    (
+      exists(VarRead use |
+        v.getAnAccess() = use and bb.getNode(i) = use.getControlFlowNode() and certain = true
+      )
+      or
+      variableCapture(v, _, bb, i) and
+      certain = false
     )
-    or
-    variableCapture(v, _, bb, i) and
-    certain = false
   }
 }
 

ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.expected

@@ -12,7 +12,6 @@ newStyleBarrierGuards
 | barrier-guards.rb:28:5:28:7 | foo |
 | barrier-guards.rb:37:21:38:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:38:5:38:7 | foo |
-| barrier-guards.rb:43:16:46:5 | [input] SSA phi read(foo) |
 | barrier-guards.rb:45:9:45:11 | foo |
 | barrier-guards.rb:70:22:71:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:71:5:71:7 | foo |
@@ -51,9 +50,7 @@ newStyleBarrierGuards
 | barrier-guards.rb:199:4:199:15 | [input] SSA phi read(foo) |
 | barrier-guards.rb:199:4:199:31 | [input] SSA phi read(foo) |
 | barrier-guards.rb:199:20:199:31 | [input] SSA phi read(foo) |
-| barrier-guards.rb:203:4:203:15 | [input] SSA phi read(foo) |
 | barrier-guards.rb:203:36:203:47 | [input] SSA phi read(foo) |
-| barrier-guards.rb:207:21:207:21 | [input] SSA phi read(foo) |
 | barrier-guards.rb:207:22:208:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:208:5:208:7 | foo |
 | barrier-guards.rb:211:22:212:19 | [input] SSA phi read(foo) |
@@ -64,8 +61,6 @@ newStyleBarrierGuards
 | barrier-guards.rb:219:21:219:32 | [input] SSA phi read(foo) |
 | barrier-guards.rb:219:95:220:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:220:5:220:7 | foo |
-| barrier-guards.rb:227:21:227:21 | [input] SSA phi read(foo) |
-| barrier-guards.rb:227:22:228:7 | [input] SSA phi read(foo) |
 | barrier-guards.rb:232:18:233:19 | [input] SSA phi read(foo) |
 | barrier-guards.rb:233:5:233:7 | foo |
 | barrier-guards.rb:237:19:237:38 | [input] SSA phi read(foo) |

rust/ql/test/query-tests/security/CWE-089/CONSISTENCY/SsaConsistency.expected

@@ -0,0 +1,4 @@
+uselessPhiNode
+| sqlx.rs:155:5:157:5 | phi | 1 |
+phiWithoutTwoPriorRefs
+| sqlx.rs:155:5:157:5 | phi | 1 |

shared/ssa/codeql/ssa/Ssa.qll

@@ -307,6 +307,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
   private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
     exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) |
       ssaDefReachesRead(v, _, readbb, _) and
+      variableRead(readbb, _, v, true) and
       not variableWrite(readbb, _, v, _)
       or
       synthPhiRead(readbb, v) and
@@ -1379,6 +1380,56 @@ module Make<LocationSig Location, InputSig<Location> Input> {
         not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
       )
     }
+
+    /** Holds if the end of a basic block can be reached by multiple definitions. */
+    query predicate nonUniqueDefReachesEndOfBlock(Definition def, SourceVariable v, BasicBlock bb) {
+      ssaDefReachesEndOfBlock(bb, def, v) and
+      not exists(unique(Definition def0 | ssaDefReachesEndOfBlock(bb, def0, v)))
+    }
+
+    /** Holds if a phi node has less than two inputs. */
+    query predicate uselessPhiNode(PhiNode phi, int inputs) {
+      inputs = count(Definition inp | phiHasInputFromBlock(phi, inp, _)) and
+      inputs < 2
+    }
+
+    /** Holds if a certain read does not have a prior reference. */
+    query predicate readWithoutPriorRef(SourceVariable v, BasicBlock bb, int i) {
+      variableRead(bb, i, v, true) and
+      not AdjacentSsaRefs::adjacentRefRead(_, _, bb, i, v)
+    }
+
+    /**
+     * Holds if a certain read has multiple prior references. The introduction
+     * of phi reads should make the prior reference unique.
+     */
+    query predicate readWithMultiplePriorRefs(
+      SourceVariable v, BasicBlock bb1, int i1, BasicBlock bb2, int i2
+    ) {
+      AdjacentSsaRefs::adjacentRefRead(bb1, i1, bb2, i2, v) and
+      2 <=
+        strictcount(BasicBlock bb0, int i0 | AdjacentSsaRefs::adjacentRefRead(bb0, i0, bb1, i1, v))
+    }
+
+    /** Holds if `phi` has less than 2 immediately prior references. */
+    query predicate phiWithoutTwoPriorRefs(PhiNode phi, int inputRefs) {
+      exists(BasicBlock bbPhi, SourceVariable v |
+        phi.definesAt(v, bbPhi, _) and
+        inputRefs =
+          count(BasicBlock bb, int i | AdjacentSsaRefs::adjacentRefPhi(bb, i, _, bbPhi, v)) and
+        inputRefs < 2
+      )
+    }
+
+    /**
+     * Holds if the phi read for `v` at `bb` has less than 2 immediately prior
+     * references.
+     */
+    query predicate phiReadWithoutTwoPriorRefs(BasicBlock bbPhi, SourceVariable v, int inputRefs) {
+      synthPhiRead(bbPhi, v) and
+      inputRefs = count(BasicBlock bb, int i | AdjacentSsaRefs::adjacentRefPhi(bb, i, _, bbPhi, v)) and
+      inputRefs < 2
+    }
   }
 
   /** Provides the input to `DataFlowIntegration`. */