diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll index c881de4c340..3716625656c 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/SimpleRangeAnalysis.qll @@ -10,6 +10,7 @@ private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExprS private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysis private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.RangeAnalysisImpl private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils + /** * Gets the lower bound of the expression. * diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll index d112cac1a75..8767c53aa19 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/FloatDelta.qll @@ -23,8 +23,9 @@ module FloatDelta implements DeltaSig { module FloatOverflow implements OverflowSig { predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) { exists(float lb, float ub, float delta | - typeBounds(expr.getSemType(), lb, ub) and - ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _, _, _) + typeBounds(expr.getSemType(), lb, ub) and + ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _, + _, _) | positively = true and delta < ub or diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysis.qll index 013068393da..1749cef13b2 100644 --- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysis.qll +++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysis.qll @@ -1,3 +1,3 @@ import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound private import RangeAnalysisImpl as Impl -import Impl::Public \ No newline at end of file +import Impl::Public 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 a8613efe7a3..5a32d80cb14 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,4 +1,4 @@ -private import RangeAnalysisStage +private import RangeAnalysisStage private import RangeAnalysisConstantSpecific private import RangeAnalysisRelativeSpecific private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta @@ -61,7 +61,6 @@ private newtype TSemReason = guard = any(RelativeStage::SemCondReason reason).getCond() } - ConstantStage::SemReason constantReason(SemReason reason) { result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason or @@ -73,6 +72,7 @@ RelativeStage::SemReason relativeReason(SemReason reason) { or result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond() } + import Public module Public { 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 20fe2603078..7643c4aadb9 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 @@ -30,33 +30,32 @@ module CppLangImplRelative implements LangSig { typeBounds(e.getSemType(), lb, ub) and ( upper = false and - delta < lb or + delta < lb + or upper = true and delta > ub ) ) } - -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 -} - + 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 + } /** * Ignore any inferred zero lower bound on this expression.