Revert "Merge pull request #13880 from MathiasVP/type-bounds-preparation"

This reverts commit 3e9d9e72dc, reversing
changes made to 877ee7047d.

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

@@ -3,24 +3,10 @@
  */
 
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
-private import codeql.util.Unit
-private import Reason as Reason
 private import RangeAnalysisStage
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
 
 module CppLangImplConstant implements LangSig<FloatDelta> {
-  private module Param implements Reason::ParamSig {
-    class TypeReasonImpl = Unit;
-  }
-
-  class SemReason = Reason::Make<Param>::SemReason;
-
-  class SemNoReason = Reason::Make<Param>::SemNoReason;
-
-  class SemCondReason = Reason::Make<Param>::SemCondReason;
-
-  class SemTypeReason = Reason::Make<Param>::SemTypeReason;
-
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *

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

@@ -61,23 +61,18 @@ private newtype TSemReason =
     guard = any(ConstantStage::SemCondReason reason).getCond()
     or
     guard = any(RelativeStage::SemCondReason reason).getCond()
-  } or
-  TSemTypeReason()
+  }
 
-private ConstantStage::SemReason constantReason(SemReason reason) {
+ConstantStage::SemReason constantReason(SemReason reason) {
   result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason
   or
   result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
-  or
-  result instanceof ConstantStage::SemTypeReason and reason instanceof SemTypeReason
 }
 
-private RelativeStage::SemReason relativeReason(SemReason reason) {
+RelativeStage::SemReason relativeReason(SemReason reason) {
   result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason
   or
   result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond()
-  or
-  result instanceof RelativeStage::SemTypeReason and reason instanceof SemTypeReason
 }
 
 import Public
@@ -116,12 +111,4 @@ module Public {
 
     override string toString() { result = this.getCond().toString() }
   }
-
-  /**
-   * A reason for an inferred bound that indicates that the bound is inferred
-   * based on type-information.
-   */
-  class SemTypeReason extends SemReason, TSemTypeReason {
-    override string toString() { result = "TypeReason" }
-  }
 }

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

@@ -7,25 +7,9 @@ private import RangeAnalysisStage
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
 private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntDelta
 private import RangeAnalysisImpl
-private import codeql.util.Unit
-private import Reason as Reason
 private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 
 module CppLangImplRelative implements LangSig<FloatDelta> {
-  private module Param implements Reason::ParamSig {
-    class TypeReasonImpl extends Unit {
-      TypeReasonImpl() { none() }
-    }
-  }
-
-  class SemReason = Reason::Make<Param>::SemReason;
-
-  class SemNoReason = Reason::Make<Param>::SemNoReason;
-
-  class SemCondReason = Reason::Make<Param>::SemCondReason;
-
-  class SemTypeReason = Reason::Make<Param>::SemTypeReason;
-
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *

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

@@ -113,37 +113,6 @@ signature module DeltaSig {
 }
 
 signature module LangSig<DeltaSig D> {
-  /** A reason for an inferred bound. */
-  class SemReason {
-    /**
-     * Returns `this` if `reason` is not a `SemTypeReason`. Otherwise,
-     * this predicate returns `SemTypeReason`.
-     *
-     * This predicate ensures that we propagate `SemTypeReason` all the way
-     * to the top-level of a call to `semBounded` if the inferred bound is
-     * based on type-information.
-     */
-    bindingset[this, reason]
-    SemReason combineWith(SemReason reason);
-  }
-
-  /**
-   * A reason for an inferred bound that indicates that the bound is inferred
-   * without going through a bounding condition.
-   */
-  class SemNoReason extends SemReason;
-
-  /** A reason for an inferred bound pointing to a condition. */
-  class SemCondReason extends SemReason {
-    SemGuard getCond();
-  }
-
-  /**
-   * A reason for an inferred bound that indicates that the bound is inferred
-   * based on type-information.
-   */
-  class SemTypeReason extends SemReason;
-
   /**
    * Holds if the specified expression should be excluded from the result of `ssaRead()`.
    *
@@ -280,14 +249,6 @@ module RangeStage<
   DeltaSig D, BoundSig<D> Bounds, OverflowSig<D> OverflowParam, LangSig<D> LangParam,
   UtilSig<D> UtilParam>
 {
-  class SemReason = LangParam::SemReason;
-
-  class SemCondReason = LangParam::SemCondReason;
-
-  class SemNoReason = LangParam::SemNoReason;
-
-  class SemTypeReason = LangParam::SemTypeReason;
-
   private import Bounds
   private import LangParam
   private import UtilParam
@@ -548,6 +509,36 @@ module RangeStage<
     )
   }
 
+  private newtype TSemReason =
+    TSemNoReason() or
+    TSemCondReason(SemGuard guard) { possibleReason(guard) }
+
+  /**
+   * 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 = this.getCond().toString() }
+  }
+
   /**
    * Holds if `e + delta` is a valid bound for `v` at `pos`.
    * - `upper = true`  : `v <= e + delta`
@@ -560,13 +551,13 @@ module RangeStage<
     semSsaUpdateStep(v, e, delta) and
     pos.hasReadOfVar(v) and
     (upper = true or upper = false) and
-    reason instanceof SemNoReason
+    reason = TSemNoReason()
     or
     exists(SemGuard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
       semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
-      reason.(SemCondReason).getCond() = guard
+      reason = TSemCondReason(guard)
     )
   }
 
@@ -579,7 +570,7 @@ module RangeStage<
       pos.hasReadOfVar(v) and
       guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
       semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
-      reason.(SemCondReason).getCond() = guard
+      reason = TSemCondReason(guard)
     )
   }
 
@@ -709,7 +700,7 @@ module RangeStage<
       // upper = true:  v <= mid + d1 <= b + d1 + d2 = b + delta
       // upper = false: v >= mid + d1 >= b + d1 + d2 = b + delta
       delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) and
-      (if r1 instanceof SemNoReason then reason = r2 else reason = r1.combineWith(r2))
+      (if r1 instanceof SemNoReason then reason = r2 else reason = r1)
     )
     or
     exists(D::Delta d, SemReason r1, SemReason r2 |
@@ -723,9 +714,9 @@ module RangeStage<
         upper = false and delta = D::fromFloat(D::toFloat(d) + 1)
       ) and
       (
-        reason = r1.combineWith(r2)
+        reason = r1
         or
-        reason = r2.combineWith(r1) and not r2 instanceof SemNoReason
+        reason = r2 and not r2 instanceof SemNoReason
       )
     )
   }
@@ -795,7 +786,7 @@ module RangeStage<
       (upper = true or upper = false) and
       fromBackEdge0 = false and
       origdelta = D::fromFloat(0) and
-      reason instanceof SemNoReason
+      reason = TSemNoReason()
     |
       if semBackEdge(phi, inp, edge)
       then
@@ -1053,13 +1044,13 @@ module RangeStage<
       (upper = true or upper = false) and
       fromBackEdge = false and
       origdelta = delta and
-      reason instanceof SemNoReason
+      reason = TSemNoReason()
       or
       baseBound(e, delta, upper) and
       b instanceof SemZeroBound and
       fromBackEdge = false and
       origdelta = delta and
-      reason instanceof SemNoReason
+      reason = TSemNoReason()
       or
       exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
         boundedSsa(v, bb, b, delta, upper, fromBackEdge, origdelta, reason) and
@@ -1113,9 +1104,9 @@ module RangeStage<
         boundedConditionalExpr(cond, b, upper, true, d1, fbe1, od1, r1) and
         boundedConditionalExpr(cond, b, upper, false, d2, fbe2, od2, r2) and
         (
-          delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1.combineWith(r2)
+          delta = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
           or
-          delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2.combineWith(r1)
+          delta = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
         )
       |
         upper = true and delta = D::fromFloat(D::toFloat(d1).maximum(D::toFloat(d2)))
@@ -1141,15 +1132,9 @@ module RangeStage<
         delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and
         fromBackEdge = fbeLeft.booleanOr(fbeRight)
       |
-        b = bLeft and
-        origdelta = odLeft and
-        reason = rLeft.combineWith(rRight) and
-        bRight instanceof SemZeroBound
+        b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound
         or
-        b = bRight and
-        origdelta = odRight and
-        reason = rRight.combineWith(rLeft) and
-        bLeft instanceof SemZeroBound
+        b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
       )
       or
       exists(
@@ -1165,9 +1150,9 @@ module RangeStage<
         (
           if D::toFloat(d1).abs() > D::toFloat(d2).abs()
           then (
-            d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1.combineWith(r2)
+            d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
           ) else (
-            d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2.combineWith(r1)
+            d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
           )
         )
       |
@@ -1183,14 +1168,11 @@ module RangeStage<
         boundedMulOperand(e, upper, true, dLeft, fbeLeft, odLeft, rLeft) and
         boundedMulOperand(e, upper, false, dRight, fbeRight, odRight, rRight) and
         delta = D::fromFloat(D::toFloat(dLeft) * D::toFloat(dRight)) and
-        fromBackEdge = fbeLeft.booleanOr(fbeRight) and
-        b instanceof SemZeroBound
+        fromBackEdge = fbeLeft.booleanOr(fbeRight)
       |
-        origdelta = odLeft and
-        reason = rLeft.combineWith(rRight)
+        b instanceof SemZeroBound and origdelta = odLeft and reason = rLeft
         or
-        origdelta = odRight and
-        reason = rRight.combineWith(rLeft)
+        b instanceof SemZeroBound and origdelta = odRight and reason = rRight
       )
     )
   }

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

@@ -1,83 +0,0 @@
-/**
- * Provides a `Make` parameterized module for constructing a `Reason` type that is used
- * when implementing the `LangSig` module.
- */
-
-private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
-
-/** The necessary parameters that must be implemented to instantiate `Make`. */
-signature module ParamSig {
-  class TypeReasonImpl;
-}
-
-/**
- * The module that constructs a `Reason` type when provided with an implementation
- * of `ParamSig`.
- */
-module Make<ParamSig Param> {
-  private import Param
-
-  private newtype TSemReason =
-    TSemNoReason() or
-    TSemCondReason(SemGuard guard) or
-    TSemTypeReason(TypeReasonImpl trc)
-
-  /**
-   * 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();
-
-    bindingset[this, reason]
-    abstract SemReason combineWith(SemReason reason);
-  }
-
-  /**
-   * 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" }
-
-    override SemReason combineWith(SemReason reason) { result = reason }
-  }
-
-  /** 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 = this.getCond().toString() }
-
-    bindingset[this, reason]
-    override SemReason combineWith(SemReason reason) {
-      // Since we end up reporting a `SemReason` for the inferred bound we often pick somewhat
-      // arbitrarily between two `SemReason`s during the analysis. This isn't an issue for most reasons
-      // since they're mainly used for constructing alert messages. However, the `SemTypeReason` is
-      // supposed to be used in query logic to filter out bounds inferred by type-based analysis if
-      // the query author chooses to do so. So we need to ensure that if _any_ of the bounds that
-      // contribute to the final bound depends on type information then the `SemReason` we report must
-      // be a `SemTypeReason`. So when we need to combine this `SemCondReason` with a `SemTypeReason`
-      // the result should always be a `SemTypeReason`.
-      if reason instanceof SemTypeReason then result instanceof SemTypeReason else result = this
-    }
-  }
-
-  /**
-   * A reason for an inferred bound that indicates that the bound is inferred
-   * based on type-information.
-   */
-  class SemTypeReason extends SemReason, TSemTypeReason {
-    TypeReasonImpl impl;
-
-    SemTypeReason() { this = TSemTypeReason(impl) }
-
-    override string toString() { result = "TypeReason" }
-
-    bindingset[this, reason]
-    override SemReason combineWith(SemReason reason) { result = this and exists(reason) }
-  }
-}