Rangeanalysis: Simplify api.

This commit is contained in:
Anders Schack-Mulligen
2023-11-10 15:35:38 +01:00
parent 30aefabb2a
commit bf6cfd3bef
8 changed files with 41 additions and 91 deletions

View File

@@ -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<Sem> {
private import SignAnalysisCommon as SA
import SA::SignAnalysis<FloatDelta, Util>
import SA::SignAnalysis<FloatDelta>
}
module ConstantBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
@@ -166,18 +169,16 @@ private module ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
class ModBound = AllBounds::SemBound;
private import codeql.rangeanalysis.ModulusAnalysis as MA
import MA::ModulusAnalysis<SemLocation, Sem, FloatDelta, AllBounds, Util>
import MA::ModulusAnalysis<SemLocation, Sem, FloatDelta, AllBounds>
}
module Util = RangeUtil<FloatDelta, CppLangImplConstant>;
module ConstantStage =
RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
SignAnalysis, ModulusAnalysisInstantiated, Util>;
SignAnalysis, ModulusAnalysisInstantiated>;
module RelativeStage =
RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
SignAnalysis, ModulusAnalysisInstantiated, Util>;
SignAnalysis, ModulusAnalysisInstantiated>;
private newtype TSemReason =
TSemNoReason() or

View File

@@ -1,27 +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<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
/**
* 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 = 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 = var.getType() }
}

View File

@@ -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<DeltaSig D, UtilSig<Sem, D> Utils> {
module SignAnalysis<DeltaSig D> {
private import codeql.rangeanalysis.internal.RangeUtils::MakeUtils<Sem, D>
/**
@@ -148,7 +147,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> 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<DeltaSig D, UtilSig<Sem, D> 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<DeltaSig D, UtilSig<Sem, D> 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<DeltaSig D, UtilSig<Sem, D> 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()

View File

@@ -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<SemLocation, Sem, FloatDelta, ConstantBounds,
RangeUtil<FloatDelta, CppLangImplRelative>>;
module ModulusAnalysisInstantiated = ModulusAnalysis<SemLocation, Sem, FloatDelta, ConstantBounds>;
module ModulusAnalysisTest implements TestSig {
string getARelevantTag() { result = "mod" }

View File

@@ -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<FloatDelta, RangeUtil<FloatDelta, CppLangImplRelative>>;
module SignAnalysisInstantiated = SignAnalysis<FloatDelta>;
module SignAnalysisTest implements TestSig {
string getARelevantTag() { result = "sign" }

View File

@@ -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<Sem> {
class ModBound = Bound;
private import codeql.rangeanalysis.ModulusAnalysis as Mod
import Mod::ModulusAnalysis<Location, Sem, IntDelta, Bounds, Utils>
import Mod::ModulusAnalysis<Location, Sem, IntDelta, Bounds>
}
module IntDelta implements DeltaSig {
@@ -365,14 +369,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
predicate javaCompatibility() { any() }
}
module Utils implements UtilSig<Sem, IntDelta> {
Sem::Type getTrackedTypeForSsaVariable(Sem::SsaVariable var) {
result = var.getSourceVariable().getType()
}
Sem::Type getTrackedType(Sem::Expr e) { result = e.getType() }
}
module Bounds implements BoundSig<Location, Sem, IntDelta> {
class SemBound = Bound;
@@ -390,7 +386,7 @@ module Overflow implements OverflowSig<Sem, IntDelta> {
}
module Range =
RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus, Utils>;
RangeStage<Location, Sem, IntDelta, Bounds, Overflow, JavaLangImpl, SignInp, Modulus>;
predicate bounded = Range::semBounded/5;

View File

@@ -14,8 +14,7 @@ private import codeql.util.Location
private import RangeAnalysis
module ModulusAnalysis<
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
UtilSig<Sem, D> U>
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds>
{
private import internal.RangeUtils::MakeUtils<Sem, D>

View File

@@ -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();
@@ -285,24 +291,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
default predicate javaCompatibility() { none() }
}
signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
/**
* 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<LocationSig Location, Semantic Sem, DeltaSig D> {
class SemBound {
string toString();
@@ -326,11 +314,10 @@ signature module OverflowSig<Semantic Sem, DeltaSig D> {
module RangeStage<
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
OverflowSig<Sem, D> OverflowParam, LangSig<Sem, D> LangParam, SignAnalysisSig<Sem> SignAnalysis,
ModulusAnalysisSig<Sem> ModulusAnalysisParam, UtilSig<Sem, D> UtilParam>
ModulusAnalysisSig<Sem> ModulusAnalysisParam>
{
private import Bounds
private import LangParam
private import UtilParam
private import D
private import OverflowParam
private import SignAnalysis
@@ -375,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)))
}
}
@@ -386,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
@@ -556,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
@@ -666,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
@@ -677,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
}
/**
@@ -764,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
|
@@ -1101,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