Merge pull request #10039 from rdmarsh2/rdmarsh2/cpp/sem-range-analysis-perf

C++: Fix missing bounds and performance issues in semantic range analysis

Author: Robert Marsh

cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticExprSpecific.qll

@@ -119,27 +119,67 @@ module SemanticExprConfig {
     result = block.getDisplayIndex()
   }
 
-  class SsaVariable instanceof IR::Instruction {
-    SsaVariable() { super.hasMemoryResult() }
+  newtype TSsaVariable =
+    TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
+    TSsaOperand(IR::Operand op) { op.isDefinitionInexact() }
 
-    final string toString() { result = super.toString() }
+  class SsaVariable extends TSsaVariable {
+    string toString() { none() }
 
-    final Location getLocation() { result = super.getLocation() }
+    Location getLocation() { none() }
+
+    IR::Instruction asInstruction() { none() }
+
+    IR::Operand asOperand() { none() }
   }
 
-  predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v = sourceExpr }
+  class SsaInstructionVariable extends SsaVariable, TSsaInstruction {
+    IR::Instruction instr;
+
+    SsaInstructionVariable() { this = TSsaInstruction(instr) }
+
+    final override string toString() { result = instr.toString() }
+
+    final override Location getLocation() { result = instr.getLocation() }
 
-  predicate phi(SsaVariable v) { v instanceof IR::PhiInstruction }
+    final override IR::Instruction asInstruction() { result = instr }
+  }
+
+  class SsaOperand extends SsaVariable, TSsaOperand {
+    IR::Operand op;
+
+    SsaOperand() { this = TSsaOperand(op) }
+
+    final override string toString() { result = op.toString() }
+
+    final override Location getLocation() { result = op.getLocation() }
+
+    final override IR::Operand asOperand() { result = op }
+  }
 
-  SsaVariable getAPhiInput(SsaVariable v) { result = v.(IR::PhiInstruction).getAnInput() }
+  predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v.asInstruction() = sourceExpr }
 
-  Expr getAUse(SsaVariable v) { result.(IR::LoadInstruction).getSourceValue() = v }
+  predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }
+
+  SsaVariable getAPhiInput(SsaVariable v) {
+    exists(IR::PhiInstruction instr |
+      result.asInstruction() = instr.getAnInput()
+      or
+      result.asOperand() = instr.getAnInputOperand()
+    )
+  }
+
+  Expr getAUse(SsaVariable v) { result.(IR::LoadInstruction).getSourceValue() = v.asInstruction() }
 
   SemType getSsaVariableType(SsaVariable v) {
-    result = getSemanticType(v.(IR::Instruction).getResultIRType())
+    result = getSemanticType(v.asInstruction().getResultIRType())
   }
 
-  BasicBlock getSsaVariableBasicBlock(SsaVariable v) { result = v.(IR::Instruction).getBlock() }
+  BasicBlock getSsaVariableBasicBlock(SsaVariable v) {
+    result = v.asInstruction().getBlock()
+    or
+    result = v.asOperand().getUse().getBlock()
+  }
 
   private newtype TReadPosition =
     TReadPositionBlock(IR::IRBlock block) or
@@ -169,7 +209,9 @@ module SemanticExprConfig {
 
     final override predicate hasRead(SsaVariable v) {
       exists(IR::Operand operand |
-        operand.getDef() = v and not operand instanceof IR::PhiInputOperand
+        operand.getDef() = v.asInstruction() and
+        not operand instanceof IR::PhiInputOperand and
+        operand.getUse().getBlock() = block
       )
     }
   }
@@ -186,7 +228,7 @@ module SemanticExprConfig {
 
     final override predicate hasRead(SsaVariable v) {
       exists(IR::PhiInputOperand operand |
-        operand.getDef() = v and
+        operand.getDef() = v.asInstruction() and
         operand.getPredecessorBlock() = pred and
         operand.getUse().getBlock() = succ
       )
@@ -205,17 +247,16 @@ module SemanticExprConfig {
     exists(IR::PhiInputOperand operand |
       pos = TReadPositionPhiInputEdge(operand.getPredecessorBlock(), operand.getUse().getBlock())
     |
-      phi = operand.getUse() and input = operand.getDef()
+      phi.asInstruction() = operand.getUse() and
+      (
+        input.asInstruction() = operand.getDef()
+        or
+        input.asOperand() = operand
+      )
     )
   }
 
   class Bound instanceof IRBound::Bound {
-    Bound() {
-      this instanceof IRBound::ZeroBound
-      or
-      this.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction() instanceof SsaVariable
-    }
-
     string toString() { result = super.toString() }
 
     final Location getLocation() { result = super.getLocation() }
@@ -228,21 +269,21 @@ module SemanticExprConfig {
 
     override string toString() {
       result =
-        min(SsaVariable instr |
-          instr = bound.getValueNumber().getAnInstruction()
+        min(SsaVariable v |
+          v.asInstruction() = bound.getValueNumber().getAnInstruction()
         |
-          instr
+          v
           order by
-            instr.(IR::Instruction).getBlock().getDisplayIndex(),
-            instr.(IR::Instruction).getDisplayIndexInBlock()
+            v.asInstruction().getBlock().getDisplayIndex(),
+            v.asInstruction().getDisplayIndexInBlock()
         ).toString()
     }
   }
 
   predicate zeroBound(Bound bound) { bound instanceof IRBound::ZeroBound }
 
   predicate ssaBound(Bound bound, SsaVariable v) {
-    v = bound.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction()
+    v.asInstruction() = bound.(IRBound::ValueNumberBound).getValueNumber().getAnInstruction()
   }
 
   Expr getBoundExpr(Bound bound, int delta) {
@@ -284,9 +325,13 @@ SemBasicBlock getSemanticBasicBlock(IR::IRBlock block) { result = block }
 
 IR::IRBlock getCppBasicBlock(SemBasicBlock block) { block = result }
 
-SemSsaVariable getSemanticSsaVariable(IR::Instruction instr) { result = instr }
+SemSsaVariable getSemanticSsaVariable(IR::Instruction instr) {
+  result.(SemanticExprConfig::SsaVariable).asInstruction() = instr
+}
 
-IR::Instruction getCppSsaVariableInstruction(SemSsaVariable v) { v = result }
+IR::Instruction getCppSsaVariableInstruction(SemSsaVariable var) {
+  var.(SemanticExprConfig::SsaVariable).asInstruction() = result
+}
 
 SemBound getSemanticBound(IRBound::Bound bound) { result = bound }
 

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/ModulusAnalysis.qll

@@ -160,6 +160,7 @@ private predicate phiModulusInit(SemSsaPhiNode phi, SemBound b, int val, int mod
 /**
  * Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
  */
+pragma[nomagic]
 private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int mod, int rix) {
   rix = 0 and
   phiModulusInit(phi, b, val, mod)
@@ -169,7 +170,7 @@ private predicate phiModulusRankStep(SemSsaPhiNode phi, SemBound b, int val, int
     val = remainder(v1, mod)
   |
     exists(int v2, int m2 |
-      rankedPhiInput(phi, inp, edge, rix) and
+      rankedPhiInput(pragma[only_bind_out](phi), inp, edge, rix) and
       phiModulusRankStep(phi, b, v1, m1, rix - 1) and
       ssaModulus(inp, edge, b, v2, m2) and
       mod = m1.gcd(m2).gcd(v1 - v2)

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll

@@ -342,7 +342,10 @@ private class ConvertOrBoxExpr extends SemUnaryExpr {
  * A cast that can be ignored for the purpose of range analysis.
  */
 private class SafeCastExpr extends ConvertOrBoxExpr {
-  SafeCastExpr() { conversionCannotOverflow(getTrackedType(getOperand()), getTrackedType(this)) }
+  SafeCastExpr() {
+    conversionCannotOverflow(getTrackedType(pragma[only_bind_into](getOperand())),
+      getTrackedType(this))
+  }
 }
 
 /**

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SignAnalysisCommon.qll

@@ -189,9 +189,12 @@ private class BinarySignExpr extends FlowSignExpr {
   BinarySignExpr() { binary = this }
 
   override Sign getSignRestriction() {
-    result =
-      semExprSign(binary.getLeftOperand())
-          .applyBinaryOp(semExprSign(binary.getRightOperand()), binary.getOpcode())
+    exists(SemExpr left, SemExpr right |
+      binaryExprOperands(binary, left, right) and
+      result =
+        semExprSign(pragma[only_bind_out](left))
+            .applyBinaryOp(semExprSign(pragma[only_bind_out](right)), binary.getOpcode())
+    )
     or
     exists(SemDivExpr div | div = binary |
       result = semExprSign(div.getLeftOperand()) and
@@ -201,6 +204,10 @@ private class BinarySignExpr extends FlowSignExpr {
   }
 }
 
+private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
+  binary.getLeftOperand() = left and binary.getRightOperand() = right
+}
+
 /**
  * A `Convert`, `Box`, or `Unbox` expression.
  */
@@ -221,7 +228,7 @@ private class UnarySignExpr extends FlowSignExpr {
   UnarySignExpr() { unary = this and not this instanceof SemCastExpr }
 
   override Sign getSignRestriction() {
-    result = semExprSign(unary.getOperand()).applyUnaryOp(unary.getOpcode())
+    result = semExprSign(pragma[only_bind_out](unary.getOperand())).applyUnaryOp(unary.getOpcode())
   }
 }
 

cpp/ql/test/library-tests/ir/range-analysis/RangeAnalysis.ql

@@ -1,6 +1,7 @@
 import cpp
 import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
 import experimental.semmle.code.cpp.semantic.Semantic
+import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
 import semmle.code.cpp.ir.IR as IR
 import TestUtilities.InlineExpectationsTest
 
@@ -37,8 +38,13 @@ private string getBoundString(SemBound b, int delta) {
   b instanceof SemZeroBound and result = delta.toString()
   or
   result =
-    strictconcat(b.(SemSsaBound).getAVariable().(IR::Instruction).getAst().toString(), ":") +
-      getOffsetString(delta)
+    strictconcat(b.(SemSsaBound)
+              .getAVariable()
+              .(SemanticExprConfig::SsaVariable)
+              .asInstruction()
+              .getAst()
+              .toString(), ":"
+      ) + getOffsetString(delta)
 }
 
 private string getARangeString(SemExpr e) {