C++: make SemBound a RangeAnalysis parameter

Author: Robert Marsh

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

@@ -16,7 +16,7 @@ private import ConstantAnalysis
 private import RangeUtils
 private import RangeAnalysisStage
 
-module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
+module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
   /**
    * Holds if `e + delta` equals `v` at `pos`.
    */
@@ -146,7 +146,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
   private predicate phiSelfModulus(
     SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int mod
   ) {
-    exists(SemSsaBound phibound, int v, int m |
+    exists(Bounds::SemSsaBound phibound, int v, int m |
       edge.phiInput(phi, inp) and
       phibound.getAVariable() = phi and
       ssaModulus(inp, edge, phibound, v, m) and
@@ -158,7 +158,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
   /**
    * Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
    */
-  private predicate phiModulusInit(SemSsaPhiNode phi, SemBound b, int val, int mod) {
+  private predicate phiModulusInit(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
     exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
       edge.phiInput(phi, inp) and
       ssaModulus(inp, edge, b, val, mod)
@@ -169,7 +169,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
    * 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) {
+  private predicate phiModulusRankStep(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod, int rix) {
     /*
      * base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence
      * class for the phi node.
@@ -213,7 +213,7 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
   /**
    * Holds if `phi` is equal to `b + val` modulo `mod`.
    */
-  private predicate phiModulus(SemSsaPhiNode phi, SemBound b, int val, int mod) {
+  private predicate phiModulus(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
     exists(int r |
       maxPhiInputRank(phi, r) and
       phiModulusRankStep(phi, b, val, mod, r)
@@ -224,19 +224,19 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
    * Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
    */
   private predicate ssaModulus(
-    SemSsaVariable v, SemSsaReadPosition pos, SemBound b, int val, int mod
+    SemSsaVariable v, SemSsaReadPosition pos, Bounds::SemBound b, int val, int mod
   ) {
     phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
     or
-    b.(SemSsaBound).getAVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
+    b.(Bounds::SemSsaBound).getAVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
     or
     exists(SemExpr e, int val0, int delta |
       semExprModulus(e, b, val0, mod) and
       valueFlowStepSsa(v, pos, e, delta) and
       val = remainder(val0 + delta, mod)
     )
     or
-    moduloGuardedRead(v, pos, val, mod) and b instanceof SemZeroBound
+    moduloGuardedRead(v, pos, val, mod) and b instanceof Bounds::SemZeroBound
   }
 
   /**
@@ -247,14 +247,14 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
    * - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
    */
   cached
-  predicate semExprModulus(SemExpr e, SemBound b, int val, int mod) {
+  predicate semExprModulus(SemExpr e, Bounds::SemBound b, int val, int mod) {
     not ignoreExprModulus(e) and
     (
-      e = b.getExpr(val) and mod = 0
+      e = b.getExpr(D::fromInt(val)) and mod = 0
       or
       evenlyDivisibleExpr(e, mod) and
       val = 0 and
-      b instanceof SemZeroBound
+      b instanceof Bounds::SemZeroBound
       or
       exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
         ssaModulus(v, bb, b, val, mod) and
@@ -277,21 +277,21 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
         val = remainder(v1, mod)
       )
       or
-      exists(SemBound b1, SemBound b2, int v1, int v2, int m1, int m2 |
+      exists(Bounds::SemBound b1, Bounds::SemBound b2, int v1, int v2, int m1, int m2 |
         addModulus(e, true, b1, v1, m1) and
         addModulus(e, false, b2, v2, m2) and
         mod = m1.gcd(m2) and
         mod != 1 and
         val = remainder(v1 + v2, mod)
       |
-        b = b1 and b2 instanceof SemZeroBound
+        b = b1 and b2 instanceof Bounds::SemZeroBound
         or
-        b = b2 and b1 instanceof SemZeroBound
+        b = b2 and b1 instanceof Bounds::SemZeroBound
       )
       or
       exists(int v1, int v2, int m1, int m2 |
         subModulus(e, true, b, v1, m1) and
-        subModulus(e, false, any(SemZeroBound zb), v2, m2) and
+        subModulus(e, false, any(Bounds::SemZeroBound zb), v2, m2) and
         mod = m1.gcd(m2) and
         mod != 1 and
         val = remainder(v1 - v2, mod)
@@ -300,20 +300,20 @@ module ModulusAnalysis<DeltaSig D, UtilSig<D> U> {
   }
 
   private predicate condExprBranchModulus(
-    SemConditionalExpr cond, boolean branch, SemBound b, int val, int mod
+    SemConditionalExpr cond, boolean branch, Bounds::SemBound b, int val, int mod
   ) {
     semExprModulus(cond.getBranchExpr(branch), b, val, mod)
   }
 
-  private predicate addModulus(SemExpr add, boolean isLeft, SemBound b, int val, int mod) {
+  private predicate addModulus(SemExpr add, boolean isLeft, Bounds::SemBound b, int val, int mod) {
     exists(SemExpr larg, SemExpr rarg | nonConstAddition(add, larg, rarg) |
       semExprModulus(larg, b, val, mod) and isLeft = true
       or
       semExprModulus(rarg, b, val, mod) and isLeft = false
     )
   }
 
-  private predicate subModulus(SemExpr sub, boolean isLeft, SemBound b, int val, int mod) {
+  private predicate subModulus(SemExpr sub, boolean isLeft, Bounds::SemBound b, int val, int mod) {
     exists(SemExpr larg, SemExpr rarg | nonConstSubtraction(sub, larg, rarg) |
       semExprModulus(larg, b, val, mod) and isLeft = true
       or

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

@@ -2,6 +2,23 @@ private import RangeAnalysisStage
 private import RangeAnalysisSpecific
 private import FloatDelta
 private import RangeUtils
+private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound
 
-private module CppRangeAnalysis = RangeStage<FloatDelta, CppLangImpl, RangeUtil<FloatDelta, CppLangImpl>>;
-import CppRangeAnalysis
+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

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

@@ -89,4 +89,4 @@ module CppLangImpl implements LangSig<FloatDelta> {
    * actually references but whose values can be tracked as the type contained in the box.
    */
   SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() }
-}
+}

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

@@ -66,7 +66,12 @@
 private import RangeUtils as Utils
 private import SignAnalysisCommon
 private import ModulusAnalysis
-private import experimental.semmle.code.cpp.semantic.Semantic
+import experimental.semmle.code.cpp.semantic.SemanticExpr
+import experimental.semmle.code.cpp.semantic.SemanticSSA
+import experimental.semmle.code.cpp.semantic.SemanticGuard
+import experimental.semmle.code.cpp.semantic.SemanticCFG
+import experimental.semmle.code.cpp.semantic.SemanticType
+import experimental.semmle.code.cpp.semantic.SemanticOpcode
 private import ConstantAnalysis
 
 /**
@@ -222,7 +227,19 @@ signature module UtilSig<DeltaSig DeltaParam> {
   SemType getTrackedType(SemExpr e);
 }
 
-module RangeStage<DeltaSig D, LangSig<D> LangParam, UtilSig<D> UtilParam> {
+signature module BoundSig<DeltaSig D> {
+  class SemBound {
+    SemExpr getExpr(D::Delta delta);
+  }
+  class SemZeroBound extends SemBound;
+  class SemSsaBound extends SemBound {
+    SemSsaVariable getAVariable();
+  }
+}
+
+module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<D> UtilParam> {
+  import Bounds // TODO: remove this import?
+
   /**
    * An expression that does conversion, boxing, or unboxing
    */
@@ -270,7 +287,7 @@ module RangeStage<DeltaSig D, LangSig<D> LangParam, UtilSig<D> UtilParam> {
 
   private import SignAnalysisInstantiated
 
-  private module ModulusAnalysisInstantiated = ModulusAnalysis<D, UtilParam>; // TODO: will this cause reevaluation if it's instantiated with the same DeltaSig and UtilParam multiple times?
+  private module ModulusAnalysisInstantiated = ModulusAnalysis<D, Bounds, UtilParam>; // TODO: will this cause reevaluation if it's instantiated with the same DeltaSig and UtilParam multiple times?
 
   private import ModulusAnalysisInstantiated
 
@@ -906,7 +923,7 @@ module RangeStage<DeltaSig D, LangSig<D> LangParam, UtilSig<D> UtilParam> {
   ) {
     not Specific::ignoreExprBound(e) and
     (
-      e = b.getExpr(delta) and
+      e = b.getExpr(D::fromFloat(delta)) and
       (upper = true or upper = false) and
       fromBackEdge = false and
       origdelta = delta and