C++: Split new range analysis into constant and relative stages

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

@@ -5,6 +5,7 @@
 private import SemanticExpr
 private import SemanticExprSpecific::SemanticExprConfig as Specific
 private import SemanticSSA
+private import SemanticLocation
 
 /**
  * A valid base for an expression bound.
@@ -14,6 +15,8 @@ private import SemanticSSA
 class SemBound instanceof Specific::Bound {
   final string toString() { result = super.toString() }
 
+  final SemLocation getLocation() { result = super.getLocation() }
+
   final SemExpr getExpr(int delta) { result = Specific::getBoundExpr(this, delta) }
 }
 

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

@@ -0,0 +1,23 @@
+private import semmle.code.cpp.Location
+
+class SemLocation instanceof Location {
+  /**
+   * Gets a textual representation of this element.
+   *
+   * The format is "file://filePath:startLine:startColumn:endLine:endColumn".
+   */
+  string toString() { result = super.toString() }
+
+  /**
+   * Holds if this element is at the specified location.
+   * The location spans column `startcolumn` of line `startline` to
+   * column `endcolumn` of line `endline` in file `filepath`.
+   * For more information, see
+   * [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
+   */
+  predicate hasLocationInfo(
+    string filepath, int startline, int startcolumn, int endline, int endcolumn
+  ) {
+    super.hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
+  }
+}

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

@@ -0,0 +1,29 @@
+private import RangeAnalysisStage
+
+module IntDelta implements DeltaSig {
+  class Delta = int;
+
+  bindingset[d]
+  bindingset[result]
+  float toFloat(Delta d) { result = d }
+
+  bindingset[d]
+  bindingset[result]
+  int toInt(Delta d) { result = d }
+
+  bindingset[n]
+  bindingset[result]
+  Delta fromInt(int n) { result = n }
+
+  bindingset[f]
+  Delta fromFloat(float f) {
+    result =
+      min(float diff, float res |
+        diff = (res - f) and res = f.ceil()
+        or
+        diff = (f - res) and res = f.floor()
+      |
+        res order by diff
+      )
+  }
+}

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

@@ -1,24 +1,2 @@
-private import RangeAnalysisStage
-private import RangeAnalysisSpecific
-private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
-private import RangeUtils
-private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
-
-module Bounds implements BoundSig<FloatDelta> {
-  class SemBound instanceof SemanticBound::SemBound {
-    string toString() { result = super.toString() }
-
-    SemExpr getExpr(float delta) { result = super.getExpr(delta) }
-  }
-
-  class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
-
-  class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
-    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
-  }
-}
-
-private module CppRangeAnalysis =
-  RangeStage<FloatDelta, Bounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
-
-import CppRangeAnalysis
+import RangeAnalysisImpl
+import experimental.semmle.code.cpp.semantic.SemanticBound

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

@@ -0,0 +1,107 @@
+private import RangeAnalysisStage
+private import RangeAnalysisSpecific
+private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
+private import RangeUtils
+private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
+private import experimental.semmle.code.cpp.semantic.SemanticLocation
+private import experimental.semmle.code.cpp.semantic.SemanticSSA
+
+module ConstantBounds implements BoundSig<FloatDelta> {
+  class SemBound instanceof SemanticBound::SemBound {
+    SemBound() {
+      this instanceof SemanticBound::SemZeroBound
+      or
+      this.(SemanticBound::SemSsaBound).getAVariable() instanceof SemSsaPhiNode
+    }
+
+    string toString() { result = super.toString() }
+
+    SemLocation getLocation() { result = super.getLocation() }
+
+    SemExpr getExpr(float delta) { result = super.getExpr(delta) }
+  }
+
+  class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
+
+  class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
+    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
+  }
+}
+
+private module RelativeBounds implements BoundSig<FloatDelta> {
+  class SemBound instanceof SemanticBound::SemBound {
+    SemBound() { not this instanceof SemanticBound::SemZeroBound }
+
+    string toString() { result = super.toString() }
+
+    SemLocation getLocation() { result = super.getLocation() }
+
+    SemExpr getExpr(float delta) { result = super.getExpr(delta) }
+  }
+
+  class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { }
+
+  class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound {
+    SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() }
+  }
+}
+
+private module ConstantStage =
+  RangeStage<FloatDelta, ConstantBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
+
+private module RelativeStage =
+  RangeStage<FloatDelta, RelativeBounds, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
+
+private newtype TSemReason =
+  TSemNoReason() or
+  TSemCondReason(SemGuard guard) {
+    guard = any(ConstantStage::SemCondReason reason).getCond()
+    or
+    guard = any(RelativeStage::SemCondReason reason).getCond()
+  }
+
+/**
+ * A reason for an inferred bound. This can either be `CondReason` if the bound
+ * is due to a specific condition, or `NoReason` if the bound is inferred
+ * without going through a bounding condition.
+ */
+abstract class SemReason extends TSemReason {
+  /** Gets a textual representation of this reason. */
+  abstract string toString();
+}
+
+/**
+ * A reason for an inferred bound that indicates that the bound is inferred
+ * without going through a bounding condition.
+ */
+class SemNoReason extends SemReason, TSemNoReason {
+  override string toString() { result = "NoReason" }
+}
+
+/** A reason for an inferred bound pointing to a condition. */
+class SemCondReason extends SemReason, TSemCondReason {
+  /** Gets the condition that is the reason for the bound. */
+  SemGuard getCond() { this = TSemCondReason(result) }
+
+  override string toString() { result = getCond().toString() }
+}
+
+private ConstantStage::SemReason constantReason(SemReason reason) {
+  result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
+  or
+  result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
+}
+
+private RelativeStage::SemReason relativeReason(SemReason reason) {
+  result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
+  or
+  result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
+}
+
+predicate semBounded(
+  SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason
+) {
+  ConstantStage::semBounded(e, b, delta, upper, constantReason(reason))
+  or
+  RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason))
+}

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

@@ -73,6 +73,7 @@ import experimental.semmle.code.cpp.semantic.SemanticCFG
 import experimental.semmle.code.cpp.semantic.SemanticType
 import experimental.semmle.code.cpp.semantic.SemanticOpcode
 private import ConstantAnalysis
+import experimental.semmle.code.cpp.semantic.SemanticLocation
 
 /**
  * Holds if `typ` is a small integral type with the given lower and upper bounds.
@@ -228,6 +229,10 @@ signature module UtilSig<DeltaSig DeltaParam> {
 
 signature module BoundSig<DeltaSig D> {
   class SemBound {
+    string toString();
+
+    SemLocation getLocation();
+
     SemExpr getExpr(D::Delta delta);
   }
 

cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql

@@ -4,12 +4,12 @@ import experimental.semmle.code.cpp.semantic.Semantic
 import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
 import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
 import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
-import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysis
+import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisImpl
 import semmle.code.cpp.ir.IR as IR
 import TestUtilities.InlineExpectationsTest
 
 module ModulusAnalysisInstantiated =
-  ModulusAnalysis<FloatDelta, Bounds, RangeUtil<FloatDelta, CppLangImpl>>;
+  ModulusAnalysis<FloatDelta, ConstantBounds, RangeUtil<FloatDelta, CppLangImpl>>;
 
 class ModulusAnalysisTest extends InlineExpectationsTest {
   ModulusAnalysisTest() { this = "ModulusAnalysisTest" }