Merge pull request #14711 from aschackmull/shared/rangeutil-share2

Java/C++/RangeAnalysis: Move a couple of utility predicates to shared qlpack

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticCFG.qll

@@ -12,9 +12,6 @@ class SemBasicBlock extends Specific::BasicBlock {
   /** Holds if this block (transitively) dominates `otherblock`. */
   final predicate bbDominates(SemBasicBlock otherBlock) { Specific::bbDominates(this, otherBlock) }
 
-  /** Holds if this block has dominance information. */
-  final predicate hasDominanceInformation() { Specific::hasDominanceInformation(this) }
-
   /** Gets an expression that is evaluated in this basic block. */
   final SemExpr getAnExpr() { result.getBasicBlock() = this }
 

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll

@@ -122,8 +122,6 @@ module SemanticExprConfig {
     dominator.dominates(dominated)
   }
 
-  predicate hasDominanceInformation(BasicBlock block) { any() }
-
   private predicate id(Cpp::Locatable x, Cpp::Locatable y) { x = y }
 
   private predicate idOf(Cpp::Locatable x, int y) = equivalenceRelation(id/2)(x, y)

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticGuard.qll

@@ -35,32 +35,4 @@ predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
   Specific::implies_v2(g1, b1, g2, b2)
 }
 
-/**
- * Holds if `guard` directly controls the position `controlled` with the
- * value `testIsTrue`.
- */
-pragma[nomagic]
-predicate semGuardDirectlyControlsSsaRead(
-  SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue
-) {
-  guard.directlyControls(controlled.(SemSsaReadPositionBlock).getBlock(), testIsTrue)
-  or
-  exists(SemSsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
-    guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
-    guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
-  )
-}
-
-/**
- * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
- */
-predicate semGuardControlsSsaRead(SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue) {
-  semGuardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
-  or
-  exists(SemGuard guard0, boolean testIsTrue0 |
-    semImplies_v2(guard0, testIsTrue0, guard, testIsTrue) and
-    semGuardControlsSsaRead(guard0, controlled, testIsTrue0)
-  )
-}
-
 SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll

@@ -63,36 +63,3 @@ class SemSsaReadPositionBlock extends SemSsaReadPosition {
 
   SemExpr getAnExpr() { result = this.getBlock().getAnExpr() }
 }
-
-/**
- * Holds if `inp` is an input to `phi` along a back edge.
- */
-predicate semBackEdge(SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge) {
-  edge.phiInput(phi, inp) and
-  // Conservatively assume that every edge is a back edge if we don't have dominance information.
-  (
-    phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
-    irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock()) or
-    not edge.getOrigBlock().hasDominanceInformation()
-  )
-}
-
-/**
- * Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
- * graph.
- *
- * An ireducible control flow graph is one where the usual dominance-based back edge detection does
- * not work, because there is a cycle with multiple entry points, meaning there are
- * mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
- * remove all detectable back-edges using the normal condition that the predecessor block is
- * dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
- * edges.
- */
-private predicate irreducibleSccEdge(SemBasicBlock b1, SemBasicBlock b2) {
-  trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
-}
-
-private predicate trimmedEdge(SemBasicBlock pred, SemBasicBlock succ) {
-  pred.getASuccessor() = succ and
-  not succ.bbDominates(pred)
-}

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll

@@ -72,14 +72,12 @@ module Sem implements Semantic {
 
   class BasicBlock = SemBasicBlock;
 
+  BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
+
   class Guard = SemGuard;
 
   predicate implies_v2 = semImplies_v2/4;
 
-  predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;
-
-  predicate guardControlsSsaRead = semGuardControlsSsaRead/3;
-
   class Type = SemType;
 
   class IntegerType = SemIntegerType;
@@ -100,8 +98,6 @@ module Sem implements Semantic {
 
   class SsaReadPositionBlock = SemSsaReadPositionBlock;
 
-  predicate backEdge = semBackEdge/3;
-
   predicate conversionCannotOverflow(Type fromType, Type toType) {
     SemanticType::conversionCannotOverflow(fromType, toType)
   }

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll

@@ -294,7 +294,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   ) {
     exists(boolean testIsTrue, SemRelationalExpr comp |
       pos.hasReadOfVar(v) and
-      semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
+      guardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
       not unknownSign(lowerbound)
     |
       testIsTrue = true and
@@ -318,7 +318,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   ) {
     exists(boolean testIsTrue, SemRelationalExpr comp |
       pos.hasReadOfVar(v) and
-      semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
+      guardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
       not unknownSign(upperbound)
     |
       testIsTrue = true and
@@ -343,7 +343,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
   private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
     exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
       pos.hasReadOfVar(pragma[only_bind_into](v)) and
-      semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
+      guardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
       e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and
       guard.isEquality(eqbound, e, polarity) and
       isEq = polarity.booleanXor(testIsTrue).booleanNot() and

java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

@@ -211,7 +211,11 @@ module Sem implements Semantic {
 
   class BasicBlock = J::BasicBlock;
 
-  class Guard extends GL::Guard {
+  BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getABBSuccessor() }
+
+  final private class FinalGuard = GL::Guard;
+
+  class Guard extends FinalGuard {
     Expr asExpr() { result = this }
   }
 
@@ -219,14 +223,6 @@ module Sem implements Semantic {
     GL::implies_v2(g1, b1, g2, b2)
   }
 
-  predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-    RU::guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
-  }
-
-  predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-    RU::guardControlsSsaRead(guard, controlled, testIsTrue)
-  }
-
   class Type = J::Type;
 
   class IntegerType extends J::IntegralType {
@@ -261,6 +257,10 @@ module Sem implements Semantic {
 
   class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionPhiInputEdge
   {
+    BasicBlock getOrigBlock() { result = super.getOrigBlock() }
+
+    BasicBlock getPhiBlock() { result = super.getPhiBlock() }
+
     predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
   }
 
@@ -268,10 +268,6 @@ module Sem implements Semantic {
     BasicBlock getBlock() { result = super.getBlock() }
   }
 
-  predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
-    RU::backEdge(phi, inp, edge)
-  }
-
   predicate conversionCannotOverflow = safeCast/2;
 }
 

java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll

@@ -7,6 +7,18 @@ private import SSA
 private import semmle.code.java.controlflow.internal.GuardsLogic
 private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
 private import semmle.code.java.Constants
+private import semmle.code.java.dataflow.RangeAnalysis
+private import codeql.rangeanalysis.internal.RangeUtils
+
+private module U = MakeUtils<Sem, IntDelta>;
+
+private predicate backEdge = U::backEdge/3;
+
+predicate ssaRead = U::ssaRead/2;
+
+predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
+
+predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
 
 /**
  * Holds if `v` is an input to `phi` that is not along a back edge, and the
@@ -145,79 +157,6 @@ class ConstantStringExpr extends Expr {
   string getStringValue() { constantStringExpr(this, result) }
 }
 
-bindingset[f]
-private predicate okInt(float f) { -2.pow(31) <= f and f <= 2.pow(31) - 1 }
-
-/**
- * Gets an expression that equals `v - d`.
- */
-Expr ssaRead(SsaVariable v, int delta) {
-  result = v.getAUse() and delta = 0
-  or
-  exists(int d1, ConstantIntegerExpr c |
-    result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
-    delta = d1 - c.getIntValue() and
-    okInt(d1.(float) - c.getIntValue().(float))
-  )
-  or
-  exists(SubExpr sub, int d1, ConstantIntegerExpr c |
-    result = sub and
-    sub.getLeftOperand() = ssaRead(v, d1) and
-    sub.getRightOperand() = c and
-    delta = d1 + c.getIntValue() and
-    okInt(d1.(float) + c.getIntValue().(float))
-  )
-  or
-  v.(SsaExplicitUpdate).getDefiningExpr().(PreIncExpr) = result and delta = 0
-  or
-  v.(SsaExplicitUpdate).getDefiningExpr().(PreDecExpr) = result and delta = 0
-  or
-  v.(SsaExplicitUpdate).getDefiningExpr().(PostIncExpr) = result and delta = 1 // x++ === ++x - 1
-  or
-  v.(SsaExplicitUpdate).getDefiningExpr().(PostDecExpr) = result and delta = -1 // x-- === --x + 1
-  or
-  v.(SsaExplicitUpdate).getDefiningExpr().(Assignment) = result and delta = 0
-  or
-  result.(AssignExpr).getSource() = ssaRead(v, delta)
-}
-
-/**
- * Holds if `inp` is an input to `phi` along a back edge.
- */
-predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
-  edge.phiInput(phi, inp) and
-  // Conservatively assume that every edge is a back edge if we don't have dominance information.
-  (
-    phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
-    not hasDominanceInformation(edge.getOrigBlock())
-  )
-}
-
-/**
- * Holds if `guard` directly controls the position `controlled` with the
- * value `testIsTrue`.
- */
-predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-  guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
-  or
-  exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
-    guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
-    guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
-  )
-}
-
-/**
- * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
- */
-predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-  guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
-  or
-  exists(Guard guard0, boolean testIsTrue0 |
-    implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
-    guardControlsSsaRead(guard0, controlled, testIsTrue0)
-  )
-}
-
 /**
  * Gets a condition that tests whether `v` equals `e + delta`.
  *

shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

@@ -17,6 +17,8 @@ module ModulusAnalysis<
   LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
   UtilSig<Sem, D> U>
 {
+  private import internal.RangeUtils::MakeUtils<Sem, D>
+
   bindingset[pos, v]
   pragma[inline_late]
   private predicate hasReadOfVarInlineLate(Sem::SsaReadPosition pos, Sem::SsaVariable v) {
@@ -35,7 +37,7 @@ module ModulusAnalysis<
     exists(Sem::Guard guard, boolean testIsTrue |
       hasReadOfVarInlineLate(pos, v) and
       guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
-      Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
+      guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
     )
   }
 
@@ -107,7 +109,7 @@ module ModulusAnalysis<
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = moduloCheck(v, val, mod, testIsTrue) and
-      Sem::guardControlsSsaRead(guard, pos, testIsTrue)
+      guardControlsSsaRead(guard, pos, testIsTrue)
     )
   }
 

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

@@ -142,7 +142,13 @@ signature module Semantic {
     Expr getBranchExpr(boolean branch);
   }
 
-  class BasicBlock;
+  class BasicBlock {
+    /** Holds if this block (transitively) dominates `otherblock`. */
+    predicate bbDominates(BasicBlock otherBlock);
+  }
+
+  /** Gets an immediate successor of basic block `bb`, if any. */
+  BasicBlock getABasicBlockSuccessor(BasicBlock bb);
 
   class Guard {
     string toString();
@@ -154,14 +160,12 @@ signature module Semantic {
     predicate directlyControls(BasicBlock controlled, boolean branch);
 
     predicate isEquality(Expr e1, Expr e2, boolean polarity);
+
+    predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
   }
 
   predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2);
 
-  predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue);
-
-  predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue);
-
   class Type;
 
   class IntegerType extends Type {
@@ -176,6 +180,8 @@ signature module Semantic {
 
   class SsaVariable {
     Expr getAUse();
+
+    BasicBlock getBasicBlock();
   }
 
   class SsaPhiNode extends SsaVariable;
@@ -189,6 +195,10 @@ signature module Semantic {
   }
 
   class SsaReadPositionPhiInputEdge extends SsaReadPosition {
+    BasicBlock getOrigBlock();
+
+    BasicBlock getPhiBlock();
+
     predicate phiInput(SsaPhiNode phi, SsaVariable inp);
   }
 
@@ -196,8 +206,6 @@ signature module Semantic {
     BasicBlock getBlock();
   }
 
-  predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge);
-
   predicate conversionCannotOverflow(Type fromType, Type toType);
 }
 
@@ -691,7 +699,7 @@ module RangeStage<
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
-      Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
+      guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )
   }
@@ -704,7 +712,7 @@ module RangeStage<
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
-      Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
+      guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )
   }
@@ -928,7 +936,7 @@ module RangeStage<
       origdelta = D::fromFloat(0) and
       reason = TSemNoReason()
     |
-      if Sem::backEdge(phi, inp, edge)
+      if backEdge(phi, inp, edge)
       then
         fromBackEdge = true and
         (

shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

@@ -34,4 +34,63 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
     or
     result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
   }
+
+  /**
+   * Holds if `guard` directly controls the position `controlled` with the
+   * value `testIsTrue`.
+   */
+  pragma[nomagic]
+  predicate guardDirectlyControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
+    guard.directlyControls(controlled.(Lang::SsaReadPositionBlock).getBlock(), testIsTrue)
+    or
+    exists(Lang::SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
+      guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
+      guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
+    )
+  }
+
+  /**
+   * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
+   */
+  predicate guardControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
+    guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
+    or
+    exists(Lang::Guard guard0, boolean testIsTrue0 |
+      Lang::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
+      guardControlsSsaRead(guard0, controlled, testIsTrue0)
+    )
+  }
+
+  /**
+   * Holds if `inp` is an input to `phi` along a back edge.
+   */
+  predicate backEdge(
+    Lang::SsaPhiNode phi, Lang::SsaVariable inp, Lang::SsaReadPositionPhiInputEdge edge
+  ) {
+    edge.phiInput(phi, inp) and
+    (
+      phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
+      irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock())
+    )
+  }
+
+  /**
+   * Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
+   * graph. Or if the edge is part of a cycle in unreachable code.
+   *
+   * An irreducible control flow graph is one where the usual dominance-based back edge detection does
+   * not work, because there is a cycle with multiple entry points, meaning there are
+   * mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
+   * remove all detectable back-edges using the normal condition that the predecessor block is
+   * dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
+   * edges.
+   */
+  private predicate irreducibleSccEdge(Lang::BasicBlock b1, Lang::BasicBlock b2) {
+    trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
+  }
+
+  private predicate trimmedEdge(Lang::BasicBlock pred, Lang::BasicBlock succ) {
+    Lang::getABasicBlockSuccessor(pred) = succ and
+    not succ.bbDominates(pred)
+  }
 }