Merge pull request #13931 from MathiasVP/revert-constant-bounds-and-prep

C++: Revert constant bounds for new range analysis

Author: jketema

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

@@ -307,8 +307,3 @@ class SemConditionalExpr extends SemKnownExpr {
     branch = false and result = falseResult
   }
 }
-
-/** Holds if `upper = true` and `e <= bound` or `upper = false` and `e >= bound`. */
-predicate semHasConstantBoundConstantSpecific(SemExpr e, float bound, boolean upper) {
-  Specific::hasConstantBoundConstantSpecific(e, bound, upper)
-}

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

@@ -434,50 +434,6 @@ module SemanticExprConfig {
 
   /** Gets the expression associated with `instr`. */
   SemExpr getSemanticExpr(IR::Instruction instr) { result = Equiv::getEquivalenceClass(instr) }
-
-  private predicate typeBounds(SemType t, float lb, float ub) {
-    exists(SemIntegerType integralType, float limit |
-      integralType = t and limit = 2.pow(8 * integralType.getByteSize())
-    |
-      if integralType instanceof SemBooleanType
-      then lb = 0 and ub = 1
-      else
-        if integralType.isSigned()
-        then (
-          lb = -(limit / 2) and ub = (limit / 2) - 1
-        ) else (
-          lb = 0 and ub = limit - 1
-        )
-    )
-    or
-    // This covers all floating point types. The range is (-Inf, +Inf).
-    t instanceof SemFloatingPointType and lb = -(1.0 / 0.0) and ub = 1.0 / 0.0
-  }
-
-  /**
-   * Holds if `upper = true` and `e <= bound` or `upper = false` and `e >= bound` based
-   * only on type information.
-   */
-  predicate hasConstantBoundConstantSpecific(Expr e, float bound, boolean upper) {
-    exists(
-      SemType converted, SemType unconverted, float unconvertedLb, float convertedLb,
-      float unconvertedUb, float convertedUb
-    |
-      unconverted = getSemanticType(e.getUnconverted().getResultIRType()) and
-      converted = getSemanticType(e.getConverted().getResultIRType()) and
-      typeBounds(unconverted, unconvertedLb, unconvertedUb) and
-      typeBounds(converted, convertedLb, convertedUb) and
-      (
-        upper = true and
-        unconvertedUb < convertedUb and
-        bound = unconvertedUb
-        or
-        upper = false and
-        unconvertedLb > convertedLb and
-        bound = unconvertedLb
-      )
-    )
-  }
 }
 
 predicate getSemanticExpr = SemanticExprConfig::getSemanticExpr/1;
@@ -501,5 +457,3 @@ IRBound::Bound getCppBound(SemBound bound) { bound = result }
 SemGuard getSemanticGuard(IRGuards::IRGuardCondition guard) { result = guard }
 
 IRGuards::IRGuardCondition getCppGuard(SemGuard guard) { guard = result }
-
-predicate hasConstantBoundConstantSpecific = SemanticExprConfig::hasConstantBoundConstantSpecific/3;

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()`.
    *
@@ -74,10 +60,7 @@ module CppLangImplConstant implements LangSig<FloatDelta> {
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
-  predicate hasConstantBound(SemExpr e, float bound, boolean upper, SemReason reason) {
-    semHasConstantBoundConstantSpecific(e, bound, upper) and
-    reason instanceof SemTypeReason
-  }
+  predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
 
   /**
    * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).

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()`.
    *
@@ -110,7 +94,7 @@ module CppLangImplRelative implements LangSig<FloatDelta> {
   /**
    * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`).
    */
-  predicate hasConstantBound(SemExpr e, float bound, boolean upper, SemReason reason) { none() }
+  predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() }
 
   /**
    * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`).