diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll index 8e7f3c7cfb3..70fec44e817 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll @@ -22,8 +22,6 @@ class SemSsaExplicitUpdate extends SemSsaVariable { SemSsaExplicitUpdate() { Specific::explicitUpdate(this, sourceExpr) } - final SemExpr getSourceExpr() { result = sourceExpr } - final SemExpr getDefiningExpr() { result = sourceExpr } } diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ConstantAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ConstantAnalysis.qll index c01b64e73d6..463817ebfd3 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ConstantAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/ConstantAnalysis.qll @@ -14,7 +14,7 @@ private predicate constantIntegerExpr(SemExpr e, int val) { // Copy of another constant exists(SemSsaExplicitUpdate v, SemExpr src | e = v.getAUse() and - src = v.getSourceExpr() and + src = v.getDefiningExpr() and constantIntegerExpr(src, val) ) or diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll index 48461afc440..31832a7bd69 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisConstantSpecific.qll @@ -22,25 +22,7 @@ module CppLangImplConstant implements LangSig { predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() } /** - * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). + * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). */ - predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } - - /** - * Gets the type that range analysis should use to track the result of the specified expression, - * if a type other than the original type of the expression is to be used. - * - * This predicate is commonly used in languages that support immutable "boxed" types that are - * actually references but whose values can be tracked as the type contained in the box. - */ - SemType getAlternateType(SemExpr e) { none() } - - /** - * Gets the type that range analysis should use to track the result of the specified source - * variable, if a type other than the original type of the expression is to be used. - * - * This predicate is commonly used in languages that support immutable "boxed" types that are - * actually references but whose values can be tracked as the type contained in the box. - */ - SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() } + predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() } } diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll index ca4560a1ff5..3b153f001d6 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll @@ -1,7 +1,6 @@ private import RangeAnalysisConstantSpecific private import RangeAnalysisRelativeSpecific private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta -private import RangeUtils private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticCFG private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticGuard @@ -88,6 +87,10 @@ module Sem implements Semantic { class AddressType = SemAddressType; + SemType getExprType(SemExpr e) { result = e.getSemType() } + + SemType getSsaType(SemSsaVariable var) { result = var.getType() } + class SsaVariable = SemSsaVariable; class SsaPhiNode = SemSsaPhiNode; @@ -103,7 +106,7 @@ module Sem implements Semantic { module SignAnalysis implements SignAnalysisSig { private import SignAnalysisCommon as SA - import SA::SignAnalysis + import SA::SignAnalysis } module ConstantBounds implements BoundSig { @@ -166,18 +169,16 @@ private module ModulusAnalysisInstantiated implements ModulusAnalysisSig { class ModBound = AllBounds::SemBound; private import codeql.rangeanalysis.ModulusAnalysis as MA - import MA::ModulusAnalysis + import MA::ModulusAnalysis } -module Util = RangeUtil; - module ConstantStage = RangeStage; + SignAnalysis, ModulusAnalysisInstantiated>; module RelativeStage = RangeStage; + SignAnalysis, ModulusAnalysisInstantiated>; private newtype TSemReason = TSemNoReason() or diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll index 524bb08e261..4f88f5ca355 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisRelativeSpecific.qll @@ -54,25 +54,7 @@ module CppLangImplRelative implements LangSig { predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() } /** - * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). + * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). */ - predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } - - /** - * Gets the type that range analysis should use to track the result of the specified expression, - * if a type other than the original type of the expression is to be used. - * - * This predicate is commonly used in languages that support immutable "boxed" types that are - * actually references but whose values can be tracked as the type contained in the box. - */ - SemType getAlternateType(SemExpr e) { none() } - - /** - * Gets the type that range analysis should use to track the result of the specified source - * variable, if a type other than the original type of the expression is to be used. - * - * This predicate is commonly used in languages that support immutable "boxed" types that are - * actually references but whose values can be tracked as the type contained in the box. - */ - SemType getAlternateTypeForSsaVariable(SemSsaVariable var) { none() } + predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() } } diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll deleted file mode 100644 index 857f69228da..00000000000 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll +++ /dev/null @@ -1,35 +0,0 @@ -/** - * Provides utility predicates for range analysis. - */ - -private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic -private import RangeAnalysisRelativeSpecific -private import codeql.rangeanalysis.RangeAnalysis -private import RangeAnalysisImpl -private import ConstantAnalysis - -module RangeUtil Lang> implements UtilSig { - /** - * Gets the type used to track the specified expression's range information. - * - * Usually, this just `e.getSemType()`, but the language can override this to track immutable boxed - * primitive types as the underlying primitive type. - */ - SemType getTrackedType(SemExpr e) { - result = Lang::getAlternateType(e) - or - not exists(Lang::getAlternateType(e)) and result = e.getSemType() - } - - /** - * Gets the type used to track the specified source variable's range information. - * - * Usually, this just `e.getType()`, but the language can override this to track immutable boxed - * primitive types as the underlying primitive type. - */ - SemType getTrackedTypeForSsaVariable(SemSsaVariable var) { - result = Lang::getAlternateTypeForSsaVariable(var) - or - not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType() - } -} diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll index f6f0d6302b7..9cd57e5ed62 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/SignAnalysisCommon.qll @@ -11,10 +11,9 @@ private import RangeAnalysisImpl private import SignAnalysisSpecific as Specific private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic private import ConstantAnalysis -private import RangeUtils private import Sign -module SignAnalysis Utils> { +module SignAnalysis { private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils /** @@ -39,7 +38,7 @@ module SignAnalysis Utils> { /** An SSA definition whose sign is determined by the sign of that definitions source expression. */ private class ExplicitSignDef extends FlowSignDef instanceof SemSsaExplicitUpdate { - final override Sign getSign() { result = semExprSign(super.getSourceExpr()) } + final override Sign getSign() { result = semExprSign(super.getDefiningExpr()) } } /** An SSA Phi definition, whose sign is the union of the signs of its inputs. */ @@ -148,7 +147,7 @@ module SignAnalysis Utils> { not this instanceof ConstantSignExpr and ( // Only track numeric types. - Utils::getTrackedType(this) instanceof SemNumericType + Sem::getExprType(this) instanceof SemNumericType or // Unless the language says to track this expression anyway. Specific::trackUnknownNonNumericExpr(this) @@ -203,7 +202,7 @@ module SignAnalysis Utils> { /** An expression of an unsigned type. */ private class UnsignedExpr extends FlowSignExpr { - UnsignedExpr() { Utils::getTrackedType(this) instanceof SemUnsignedIntegerType } + UnsignedExpr() { Sem::getExprType(this) instanceof SemUnsignedIntegerType } override Sign getSignRestriction() { result = TPos() or @@ -276,7 +275,7 @@ module SignAnalysis Utils> { override SemUnboxExpr cast; UnboxSignExpr() { - exists(SemType fromType | fromType = Utils::getTrackedType(cast.getOperand()) | + exists(SemType fromType | fromType = Sem::getExprType(cast.getOperand()) | // Only numeric source types are handled here. fromType instanceof SemNumericType ) @@ -471,7 +470,7 @@ module SignAnalysis Utils> { Sign semExprSign(SemExpr e) { exists(Sign s | s = e.(SignExpr).getSign() | if - Utils::getTrackedType(e) instanceof SemUnsignedIntegerType and + Sem::getExprType(e) instanceof SemUnsignedIntegerType and s = TNeg() and not Specific::ignoreTypeRestrictions(e) then result = TPos() diff --git a/cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql b/cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql index feca7bf680a..229cc240c9e 100644 --- a/cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql +++ b/cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql @@ -2,7 +2,6 @@ import cpp import codeql.rangeanalysis.ModulusAnalysis import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation -import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeUtils import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisRelativeSpecific import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisImpl @@ -10,9 +9,7 @@ import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific import semmle.code.cpp.ir.IR as IR import TestUtilities.InlineExpectationsTest -module ModulusAnalysisInstantiated = - ModulusAnalysis>; +module ModulusAnalysisInstantiated = ModulusAnalysis; module ModulusAnalysisTest implements TestSig { string getARelevantTag() { result = "mod" } diff --git a/cpp/ql/test/library-tests/ir/sign-analysis/SignAnalysis.ql b/cpp/ql/test/library-tests/ir/sign-analysis/SignAnalysis.ql index fcc796577d1..cba373a60a1 100644 --- a/cpp/ql/test/library-tests/ir/sign-analysis/SignAnalysis.ql +++ b/cpp/ql/test/library-tests/ir/sign-analysis/SignAnalysis.ql @@ -1,15 +1,13 @@ import cpp import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.SignAnalysisCommon import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic -import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeUtils import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisRelativeSpecific import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprSpecific import semmle.code.cpp.ir.IR as IR import TestUtilities.InlineExpectationsTest -module SignAnalysisInstantiated = - SignAnalysis>; +module SignAnalysisInstantiated = SignAnalysis; module SignAnalysisTest implements TestSig { string getARelevantTag() { result = "sign" } diff --git a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll index 353d92cadc3..2dd72d78a2e 100644 --- a/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll +++ b/java/ql/lib/semmle/code/java/dataflow/NullGuards.qll @@ -6,7 +6,6 @@ import java import SSA private import semmle.code.java.controlflow.internal.GuardsLogic private import semmle.code.java.frameworks.apache.Collections -private import RangeUtils private import IntegerGuards /** Gets an expression that is always `null`. */ diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll index d0335efacec..e0055d53f08 100644 --- a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll +++ b/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll @@ -241,6 +241,10 @@ module Sem implements Semantic { AddressType() { none() } } + Type getExprType(Expr e) { result = e.getType() } + + Type getSsaType(SsaVariable var) { result = var.getSourceVariable().getType() } + final private class FinalSsaVariable = SSA::SsaVariable; class SsaVariable extends FinalSsaVariable { @@ -281,7 +285,7 @@ module Modulus implements ModulusAnalysisSig { class ModBound = Bound; private import codeql.rangeanalysis.ModulusAnalysis as Mod - import Mod::ModulusAnalysis + import Mod::ModulusAnalysis } module IntDelta implements DeltaSig { @@ -332,7 +336,7 @@ module JavaLangImpl implements LangSig { /** * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). */ - predicate hasBound(Sem::Expr e2, Sem::Expr e1, int delta, boolean upper) { + predicate additionalBoundFlowStep(Sem::Expr e2, Sem::Expr e1, int delta, boolean upper) { exists(RandomDataSource rds | e2 = rds.getOutput() and ( @@ -362,21 +366,9 @@ module JavaLangImpl implements LangSig { predicate ignoreExprBound(Sem::Expr e) { none() } - Sem::Type getAlternateType(Sem::Expr e) { none() } - - Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var) { none() } - predicate javaCompatibility() { any() } } -module Utils implements UtilSig { - Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) { - result = var.getSourceVariable().getType() - } - - Sem::Type getTrackedType(Sem::Expr e) { result = e.getType() } -} - module Bounds implements BoundSig { class SemBound = Bound; @@ -394,7 +386,7 @@ module Overflow implements OverflowSig { } module Range = - RangeStage; + RangeStage; predicate bounded = Range::semBounded/5; diff --git a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll index a94e81a942e..f8b4a94079a 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll @@ -14,8 +14,7 @@ private import codeql.util.Location private import RangeAnalysis module ModulusAnalysis< - LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds, - UtilSig U> + LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds> { private import internal.RangeUtils::MakeUtils @@ -254,8 +253,7 @@ module ModulusAnalysis< or exists(Sem::SsaVariable v, SsaReadPositionBlock bb | ssaModulus(v, bb, b, val, mod) and - e = v.getAUse() and - bb.getBlock() = e.getBasicBlock() + bb.getAnSsaRead(v) = e ) or exists(Sem::Expr mid, int val0, int delta | diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index cc41384b5f3..a8801c58404 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -188,6 +188,12 @@ signature module Semantic { class AddressType extends Type; + /** Gets the type of an SSA variable. */ + Type getSsaType(SsaVariable var); + + /** Gets the type of an expression. */ + Type getExprType(Expr e); + class SsaVariable { Expr getAUse(); @@ -270,9 +276,9 @@ signature module LangSig { predicate hasConstantBound(Sem::Expr e, D::Delta bound, boolean upper); /** - * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). + * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). */ - predicate hasBound(Sem::Expr e, Sem::Expr bound, D::Delta delta, boolean upper); + predicate additionalBoundFlowStep(Sem::Expr e2, Sem::Expr e1, D::Delta delta, boolean upper); /** * Ignore the bound on this expression. @@ -282,45 +288,9 @@ signature module LangSig { */ predicate ignoreExprBound(Sem::Expr e); - /** - * Gets the type that range analysis should use to track the result of the specified expression, - * if a type other than the original type of the expression is to be used. - * - * This predicate is commonly used in languages that support immutable "boxed" types that are - * actually references but whose values can be tracked as the type contained in the box. - */ - Sem::Type getAlternateType(Sem::Expr e); - - /** - * Gets the type that range analysis should use to track the result of the specified source - * variable, if a type other than the original type of the expression is to be used. - * - * This predicate is commonly used in languages that support immutable "boxed" types that are - * actually references but whose values can be tracked as the type contained in the box. - */ - Sem::Type getAlternateTypeForSsaVariable(Sem::SsaVariable var); - default predicate javaCompatibility() { none() } } -signature module UtilSig { - /** - * Gets the type used to track the specified source variable's range information. - * - * Usually, this just `e.getType()`, but the language can override this to track immutable boxed - * primitive types as the underlying primitive type. - */ - Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var); - - /** - * Gets the type used to track the specified expression's range information. - * - * Usually, this just `e.getSemType()`, but the language can override this to track immutable boxed - * primitive types as the underlying primitive type. - */ - Sem::Type getTrackedType(Sem::Expr e); -} - signature module BoundSig { class SemBound { string toString(); @@ -344,11 +314,10 @@ signature module OverflowSig { module RangeStage< LocationSig Location, Semantic Sem, DeltaSig D, BoundSig Bounds, OverflowSig OverflowParam, LangSig LangParam, SignAnalysisSig SignAnalysis, - ModulusAnalysisSig ModulusAnalysisParam, UtilSig UtilParam> + ModulusAnalysisSig ModulusAnalysisParam> { private import Bounds private import LangParam - private import UtilParam private import D private import OverflowParam private import SignAnalysis @@ -393,8 +362,8 @@ module RangeStage< */ private class SafeCastExpr extends ConvertOrBoxExpr { SafeCastExpr() { - Sem::conversionCannotOverflow(getTrackedType(pragma[only_bind_into](this.getOperand())), - pragma[only_bind_out](getTrackedType(this))) + Sem::conversionCannotOverflow(Sem::getExprType(pragma[only_bind_into](this.getOperand())), + pragma[only_bind_out](Sem::getExprType(this))) } } @@ -404,14 +373,14 @@ module RangeStage< private class NarrowingCastExpr extends ConvertOrBoxExpr { NarrowingCastExpr() { not this instanceof SafeCastExpr and - typeBound(getTrackedType(this), _, _) + typeBound(Sem::getExprType(this), _, _) } /** Gets the lower bound of the resulting type. */ - float getLowerBound() { typeBound(getTrackedType(this), result, _) } + float getLowerBound() { typeBound(Sem::getExprType(this), result, _) } /** Gets the upper bound of the resulting type. */ - float getUpperBound() { typeBound(getTrackedType(this), _, result) } + float getUpperBound() { typeBound(Sem::getExprType(this), _, result) } } cached @@ -574,8 +543,8 @@ module RangeStage< ) and ( if - getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType or - getTrackedTypeForSsaVariable(v) instanceof Sem::AddressType + Sem::getSsaType(v) instanceof Sem::IntegerType or + Sem::getSsaType(v) instanceof Sem::AddressType then upper = true and strengthen = -1 or @@ -684,7 +653,7 @@ module RangeStage< private predicate unequalFlowStepIntegralSsa( Sem::SsaVariable v, SsaReadPosition pos, Sem::Expr e, D::Delta delta, SemReason reason ) { - getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and + Sem::getSsaType(v) instanceof Sem::IntegerType and exists(Sem::Guard guard, boolean testIsTrue | pos.hasReadOfVar(v) and guard = eqFlowCond(v, e, delta, false, testIsTrue) and @@ -695,12 +664,12 @@ module RangeStage< /** Holds if `e >= 1` as determined by sign analysis. */ private predicate strictlyPositiveIntegralExpr(Sem::Expr e) { - semStrictlyPositive(e) and getTrackedType(e) instanceof Sem::IntegerType + semStrictlyPositive(e) and Sem::getExprType(e) instanceof Sem::IntegerType } /** Holds if `e <= -1` as determined by sign analysis. */ private predicate strictlyNegativeIntegralExpr(Sem::Expr e) { - semStrictlyNegative(e) and getTrackedType(e) instanceof Sem::IntegerType + semStrictlyNegative(e) and Sem::getExprType(e) instanceof Sem::IntegerType } /** @@ -758,7 +727,7 @@ module RangeStage< delta = D::fromInt(0) and upper = false or - hasBound(e2, e1, delta, upper) + additionalBoundFlowStep(e2, e1, delta, upper) } /** Holds if `e2 = e1 * factor` and `factor > 0`. */ @@ -782,7 +751,7 @@ module RangeStage< * therefore only valid for non-negative numbers. */ private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) { - getTrackedType(e2) instanceof Sem::IntegerType and + Sem::getExprType(e2) instanceof Sem::IntegerType and exists(Sem::ConstantIntegerExpr c, D::Delta k | k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0 | @@ -825,11 +794,9 @@ module RangeStage< ) or exists(D::Delta d, SemReason r1, SemReason r2 | - boundedSsa(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d), - pragma[only_bind_into](pos), upper, fromBackEdge, origdelta, r2) + boundedSsa(v, b, d, pos, upper, fromBackEdge, origdelta, r2) or - boundedPhi(pragma[only_bind_into](v), pragma[only_bind_into](b), pragma[only_bind_into](d), - upper, fromBackEdge, origdelta, r2) + boundedPhi(v, b, d, upper, fromBackEdge, origdelta, r2) | unequalIntegralSsa(v, b, d, pos, r1) and ( @@ -853,32 +820,12 @@ module RangeStage< ) { exists(Sem::Expr e, D::Delta d1, D::Delta d2 | unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and - boundedUpper(e, b, d2) and - boundedLower(e, b, d2) and + bounded(e, b, d2, true, _, _, _) and + bounded(e, b, d2, false, _, _, _) and delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2)) ) } - /** - * Holds if `b + delta` is an upper bound for `e`. - * - * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`. - */ - pragma[nomagic] - private predicate boundedUpper(Sem::Expr e, SemBound b, D::Delta delta) { - bounded(e, b, delta, true, _, _, _) - } - - /** - * Holds if `b + delta` is a lower bound for `e`. - * - * This predicate only exists to prevent a bad standard order in `unequalIntegralSsa`. - */ - pragma[nomagic] - private predicate boundedLower(Sem::Expr e, SemBound b, D::Delta delta) { - bounded(e, b, delta, false, _, _, _) - } - /** Weakens a delta to lie in the range `[-1..1]`. */ bindingset[delta, upper] private D::Delta weakenDelta(boolean upper, D::Delta delta) { @@ -1141,7 +1088,7 @@ module RangeStage< ( expr instanceof Sem::NegateExpr or expr instanceof Sem::PreDecExpr or - getTrackedType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType + Sem::getExprType(expr.(Sem::DivExpr)) instanceof Sem::FloatingPointType ) or positively = true and @@ -1185,8 +1132,7 @@ module RangeStage< or exists(Sem::SsaVariable v, SsaReadPositionBlock bb | boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and - e = v.getAUse() and - bb.getBlock() = e.getBasicBlock() + bb.getAnSsaRead(v) = e ) or exists(Sem::Expr mid, D::Delta d1, D::Delta d2 |