From 7ea74df4b35072dc33b2013148dd070758210ac4 Mon Sep 17 00:00:00 2001 From: Robert Marsh Date: Tue, 17 Jan 2023 09:35:31 -0500 Subject: [PATCH] C++: SimpleRangeAnalysis wrapper uses constant stage --- .../code/cpp/semantic/analysis/FloatDelta.qll | 2 +- .../cpp/semantic/analysis/RangeAnalysis.qll | 3 +- .../semantic/analysis/RangeAnalysisImpl.qll | 72 +++++----- .../analysis/RangeAnalysisSpecific2.qll | 127 ++++++++++++++++++ .../semantic/analysis/SimpleRangeAnalysis.qll | 14 +- 5 files changed, 177 insertions(+), 41 deletions(-) create mode 100644 cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific2.qll diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll index 4c7f6d0a23a..500f7b2cac5 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/FloatDelta.qll @@ -33,7 +33,7 @@ module FloatOverflow implements OverflowSig { predicate semExprDoesntOverflow(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.booleanNot(), _, _, _) + ConstantStage::initialBounded(expr, any(ConstantBounds::SemZeroBound b), delta, positively, _, _, _) | positively = true and delta < ub or diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll index e9b7d9dc2ac..0413aefd5ad 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysis.qll @@ -1,2 +1,3 @@ -import RangeAnalysisImpl import experimental.semmle.code.cpp.semantic.SemanticBound +private import RangeAnalysisImpl as Impl +import Impl::Public \ No newline at end of file diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll index 270b1c4a558..272cc875cc1 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll @@ -28,7 +28,7 @@ module ConstantBounds implements BoundSig { } } -private module RelativeBounds implements BoundSig { +module RelativeBounds implements BoundSig { class SemBound instanceof SemanticBound::SemBound { SemBound() { not this instanceof SemanticBound::SemZeroBound } @@ -60,48 +60,52 @@ private newtype TSemReason = guard = any(RelativeStage::SemCondReason reason).getCond() } -/** - * 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 = getCond().toString() } -} - -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() } -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() } +import Public -predicate semBounded( - SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason -) { - ConstantStage::semBounded(e, b, delta, upper, constantReason(reason)) - or - RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason)) +module Public { + predicate semBounded( + SemExpr e, SemanticBound::SemBound b, float delta, boolean upper, SemReason reason + ) { + ConstantStage::semBounded(e, b, delta, upper, constantReason(reason)) + or + RelativeStage::semBounded(e, b, delta, upper, relativeReason(reason)) + } + + /** + * 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 = getCond().toString() } + } } diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific2.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific2.qll new file mode 100644 index 00000000000..1ea72e355b9 --- /dev/null +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisSpecific2.qll @@ -0,0 +1,127 @@ +/** + * C++-specific implementation of range analysis. + */ + +private import experimental.semmle.code.cpp.semantic.Semantic +private import RangeAnalysisStage +private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta +private import experimental.semmle.code.cpp.semantic.analysis.IntDelta +private import RangeAnalysisImpl +private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils + +module CppLangImpl2 implements LangSig { + /** + * Holds if the specified expression should be excluded from the result of `ssaRead()`. + * + * This predicate is to keep the results identical to the original Java implementation. It should be + * removed once we have the new implementation matching the old results exactly. + */ + predicate ignoreSsaReadCopy(SemExpr e) { none() } + + /** + * Ignore the bound on this expression. + * + * This predicate is to keep the results identical to the original Java implementation. It should be + * removed once we have the new implementation matching the old results exactly. + */ + predicate ignoreExprBound(SemExpr e) { + exists(boolean upper, float delta, ConstantBounds::SemZeroBound b, float lb, float ub | + ConstantStage::semBounded(e, b, delta, upper, _) and + typeBounds(e.getSemType(), lb, ub) and + ( + upper = false and + 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 +} + + + /** + * Ignore any inferred zero lower bound on this expression. + * + * This predicate is to keep the results identical to the original Java implementation. It should be + * removed once we have the new implementation matching the old results exactly. + */ + predicate ignoreZeroLowerBound(SemExpr e) { none() } + + /** + * Holds if the specified expression should be excluded from the result of `ssaRead()`. + * + * This predicate is to keep the results identical to the original Java implementation. It should be + * removed once we have the new implementation matching the old results exactly. + */ + predicate ignoreSsaReadArithmeticExpr(SemExpr e) { none() } + + /** + * Holds if the specified variable should be excluded from the result of `ssaRead()`. + * + * This predicate is to keep the results identical to the original Java implementation. It should be + * removed once we have the new implementation matching the old results exactly. + */ + predicate ignoreSsaReadAssignment(SemSsaVariable v) { none() } + + /** + * Adds additional results to `ssaRead()` that are specific to Java. + * + * This predicate handles propagation of offsets for post-increment and post-decrement expressions + * in exactly the same way as the old Java implementation. Once the new implementation matches the + * old one, we should remove this predicate and propagate deltas for all similar patterns, whether + * or not they come from a post-increment/decrement expression. + */ + SemExpr specificSsaRead(SemSsaVariable v, float delta) { none() } + + /** + * Holds if `e >= bound` (if `upper = false`) or `e <= bound` (if `upper = true`). + */ + predicate hasConstantBound(SemExpr e, float bound, boolean upper) { none() } + + /** + * Holds if `e >= bound + delta` (if `upper = false`) or `e <= bound + delta` (if `upper = true`). + */ + predicate hasBound(SemExpr e, SemExpr bound, float delta, boolean upper) { none() } + + /** + * Holds if the value of `dest` is known to be `src + delta`. + */ + predicate additionalValueFlowStep(SemExpr dest, SemExpr src, float delta) { 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() } +} diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll index e9ebcc5dcfb..e3d80513beb 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll @@ -7,7 +7,7 @@ private import cpp private import semmle.code.cpp.ir.IR private import experimental.semmle.code.cpp.semantic.SemanticBound private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific -private import RangeAnalysis +private import RangeAnalysisImpl private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils /** @@ -23,8 +23,10 @@ private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils * `lowerBound(expr.getFullyConverted())` */ float lowerBound(Expr expr) { - exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound | - semBounded(getSemanticExpr(i), b, result, false, _) + exists(Instruction i, ConstantBounds::SemBound b | + i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound + | + ConstantStage::semBounded(getSemanticExpr(i), b, result, false, _) ) } @@ -41,8 +43,10 @@ float lowerBound(Expr expr) { * `upperBound(expr.getFullyConverted())` */ float upperBound(Expr expr) { - exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound | - semBounded(getSemanticExpr(i), b, result, true, _) + exists(Instruction i, ConstantBounds::SemBound b | + i.getAst() = expr and b instanceof ConstantBounds::SemZeroBound + | + ConstantStage::semBounded(getSemanticExpr(i), b, result, true, _) ) }