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 31832a7bd69..e9a7dc836e4 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 @@ -25,4 +25,8 @@ module CppLangImplConstant implements LangSig { * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). */ predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() } + + predicate includeConstantBounds() { any() } + + predicate includeRelativeBounds() { 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 3b153f001d6..a19baf2eea7 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 @@ -173,11 +173,11 @@ private module ModulusAnalysisInstantiated implements ModulusAnalysisSig { } module ConstantStage = - RangeStage; module RelativeStage = - RangeStage; private newtype TSemReason = 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 4f88f5ca355..3774d47db8b 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 @@ -57,4 +57,8 @@ module CppLangImplRelative implements LangSig { * Holds if `e2 >= e1 + delta` (if `upper = false`) or `e2 <= e1 + delta` (if `upper = true`). */ predicate additionalBoundFlowStep(SemExpr e2, SemExpr e1, float delta, boolean upper) { none() } + + predicate includeConstantBounds() { none() } + + predicate includeRelativeBounds() { any() } } diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index a8801c58404..55c0e3b432e 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -289,6 +289,10 @@ signature module LangSig { predicate ignoreExprBound(Sem::Expr e); default predicate javaCompatibility() { none() } + + default predicate includeConstantBounds() { any() } + + default predicate includeRelativeBounds() { any() } } signature module BoundSig { @@ -983,6 +987,13 @@ module RangeStage< ) } + private predicate includeBound(SemBound b) { + // always include phi bounds + b.(SemSsaBound).getVariable() instanceof Sem::SsaPhiNode + or + if b instanceof SemZeroBound then includeConstantBounds() else includeRelativeBounds() + } + /** * Holds if `e` has an upper (for `upper = true`) or lower * (for `upper = false`) bound of `b`. @@ -1122,13 +1133,15 @@ module RangeStage< (upper = true or upper = false) and fromBackEdge = false and origdelta = delta and - reason = TSemNoReason() + reason = TSemNoReason() and + includeBound(b) or baseBound(e, delta, upper) and b instanceof SemZeroBound and fromBackEdge = false and origdelta = delta and - reason = TSemNoReason() + reason = TSemNoReason() and + includeBound(b) or exists(Sem::SsaVariable v, SsaReadPositionBlock bb | boundedSsa(v, b, delta, bb, upper, fromBackEdge, origdelta, reason) and