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 56e7fafab50..e9b7d9dc2ac 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,100 +1,2 @@ -private import RangeAnalysisStage -private import RangeAnalysisSpecific -private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta -private import RangeUtils -private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound -private import semmle.code.cpp.ir.IR as IR - -private module ConstantBounds implements BoundSig { - class SemBound instanceof SemanticBound::SemBound { - SemBound() { - this instanceof SemanticBound::SemZeroBound - or - this.(SemanticBound::SemSsaBound).getExpr(0) instanceof IR::PhiInstruction - } - - string toString() { result = super.toString() } - - SemExpr getExpr(float delta) { result = super.getExpr(delta) } - } - - class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } - - class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { - SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } - } -} - -private module RelativeBounds implements BoundSig { - class SemBound instanceof SemanticBound::SemSsaBound { - string toString() { result = super.toString() } - - SemExpr getExpr(float delta) { result = super.getExpr(delta) } - } - - class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } - - class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { - SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } - } -} - -private module ConstantStage = - RangeStage>; - -private module RelativeStage = - RangeStage>; - -private newtype TSemReason = - TSemNoReason() or - TSemCondReason(SemGuard guard) { - guard = any(ConstantStage::SemCondReason reason).getCond() - or - 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) { - result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason - or - result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond() -} - -private RelativeStage::SemReason relativeReason(SemReason reason) { - result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason - or - result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond() -} - -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)) -} +import RangeAnalysisImpl +import experimental.semmle.code.cpp.semantic.SemanticBound 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 new file mode 100644 index 00000000000..56e7fafab50 --- /dev/null +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisImpl.qll @@ -0,0 +1,100 @@ +private import RangeAnalysisStage +private import RangeAnalysisSpecific +private import experimental.semmle.code.cpp.semantic.analysis.FloatDelta +private import RangeUtils +private import experimental.semmle.code.cpp.semantic.SemanticBound as SemanticBound +private import semmle.code.cpp.ir.IR as IR + +private module ConstantBounds implements BoundSig { + class SemBound instanceof SemanticBound::SemBound { + SemBound() { + this instanceof SemanticBound::SemZeroBound + or + this.(SemanticBound::SemSsaBound).getExpr(0) instanceof IR::PhiInstruction + } + + string toString() { result = super.toString() } + + SemExpr getExpr(float delta) { result = super.getExpr(delta) } + } + + class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } + + class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { + SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } + } +} + +private module RelativeBounds implements BoundSig { + class SemBound instanceof SemanticBound::SemSsaBound { + string toString() { result = super.toString() } + + SemExpr getExpr(float delta) { result = super.getExpr(delta) } + } + + class SemZeroBound extends SemBound instanceof SemanticBound::SemZeroBound { } + + class SemSsaBound extends SemBound instanceof SemanticBound::SemSsaBound { + SemSsaVariable getAVariable() { result = this.(SemanticBound::SemSsaBound).getAVariable() } + } +} + +private module ConstantStage = + RangeStage>; + +private module RelativeStage = + RangeStage>; + +private newtype TSemReason = + TSemNoReason() or + TSemCondReason(SemGuard guard) { + guard = any(ConstantStage::SemCondReason reason).getCond() + or + 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) { + result instanceof ConstantStage::SemNoReason and reason instanceof SemNoReason + or + result.(ConstantStage::SemCondReason).getCond() = reason.(SemCondReason).getCond() +} + +private RelativeStage::SemReason relativeReason(SemReason reason) { + result instanceof RelativeStage::SemNoReason and reason instanceof SemNoReason + or + result.(RelativeStage::SemCondReason).getCond() = reason.(SemCondReason).getCond() +} + +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)) +}