Merge pull request #14588 from aschackmull/shared/rangeanalysis

C++/Java: Share core range analysis
This commit is contained in:
Mathias Vorreiter Pedersen 2023-10-26 16:32:46 +01:00 коммит произвёл GitHub
Родитель 867a39083e 6882504397
Коммит 30ecb4b0c8
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
22 изменённых файлов: 1006 добавлений и 1132 удалений

Просмотреть файл

@ -7,6 +7,7 @@ library: true
upgrades: upgrades
dependencies:
codeql/dataflow: ${workspace}
codeql/rangeanalysis: ${workspace}
codeql/ssa: ${workspace}
codeql/tutorial: ${workspace}
codeql/util: ${workspace}

Просмотреть файл

@ -8,6 +8,18 @@ class SemLocation instanceof Location {
*/
string toString() { result = super.toString() }
/** Gets the 1-based line number (inclusive) where this location starts. */
int getStartLine() { result = super.getStartLine() }
/** Gets the 1-based column number (inclusive) where this location starts. */
int getStartColumn() { result = super.getStartColumn() }
/** Gets the 1-based line number (inclusive) where this location ends. */
int getEndLine() { result = super.getEndLine() }
/** Gets the 1-based column number (inclusive) where this location ends. */
int getEndColumn() { result = super.getEndColumn() }
/**
* Holds if this element is at the specified location.
* The location spans column `startcolumn` of line `startline` to

Просмотреть файл

@ -1,5 +1,7 @@
private import RangeAnalysisStage
private import RangeAnalysisImpl
private import codeql.rangeanalysis.RangeAnalysis
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticExpr
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType
module FloatDelta implements DeltaSig {
class Delta = float;
@ -20,7 +22,7 @@ module FloatDelta implements DeltaSig {
Delta fromFloat(float f) { result = f }
}
module FloatOverflow implements OverflowSig<FloatDelta> {
module FloatOverflow implements OverflowSig<Sem, FloatDelta> {
predicate semExprDoesNotOverflow(boolean positively, SemExpr expr) {
exists(float lb, float ub, float delta |
typeBounds(expr.getSemType(), lb, ub) and

Просмотреть файл

@ -1,29 +0,0 @@
private import RangeAnalysisStage
module IntDelta implements DeltaSig {
class Delta = int;
bindingset[d]
bindingset[result]
float toFloat(Delta d) { result = d }
bindingset[d]
bindingset[result]
int toInt(Delta d) { result = d }
bindingset[n]
bindingset[result]
Delta fromInt(int n) { result = n }
bindingset[f]
Delta fromFloat(float f) {
result =
min(float diff, float res |
diff = (res - f) and res = f.ceil()
or
diff = (f - res) and res = f.floor()
|
res order by diff
)
}
}

Просмотреть файл

@ -12,11 +12,13 @@
private import ModulusAnalysisSpecific::Private
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import ConstantAnalysis
private import RangeUtils
private import RangeAnalysisStage
private import codeql.rangeanalysis.RangeAnalysis
private import RangeAnalysisImpl
module ModulusAnalysis<DeltaSig D, BoundSig<D> Bounds, UtilSig<D> U> {
module ModulusAnalysis<DeltaSig D, BoundSig<SemLocation, Sem, D> Bounds, UtilSig<Sem, D> U> {
pragma[nomagic]
private predicate valueFlowStepSsaEqFlowCond(
SemSsaReadPosition pos, SemSsaVariable v, SemExpr e, int delta

Просмотреть файл

@ -3,10 +3,11 @@
*/
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import RangeAnalysisImpl
private import codeql.rangeanalysis.RangeAnalysis
module CppLangImplConstant implements LangSig<FloatDelta> {
module CppLangImplConstant implements LangSig<Sem, FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*

Просмотреть файл

@ -1,13 +1,104 @@
private import RangeAnalysisStage
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
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticBound as SemanticBound
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticLocation
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticSSA
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.SemanticType as SemanticType
private import SemanticType
private import codeql.rangeanalysis.RangeAnalysis
private import ConstantAnalysis as ConstantAnalysis
module ConstantBounds implements BoundSig<FloatDelta> {
module Sem implements Semantic {
class Expr = SemExpr;
class ConstantIntegerExpr = ConstantAnalysis::SemConstantIntegerExpr;
class BinaryExpr = SemBinaryExpr;
class AddExpr = SemAddExpr;
class SubExpr = SemSubExpr;
class MulExpr = SemMulExpr;
class DivExpr = SemDivExpr;
class RemExpr = SemRemExpr;
class BitAndExpr = SemBitAndExpr;
class BitOrExpr = SemBitOrExpr;
class ShiftLeftExpr = SemShiftLeftExpr;
class ShiftRightExpr = SemShiftRightExpr;
class ShiftRightUnsignedExpr = SemShiftRightUnsignedExpr;
class RelationalExpr = SemRelationalExpr;
class UnaryExpr = SemUnaryExpr;
class ConvertExpr = SemConvertExpr;
class BoxExpr = SemBoxExpr;
class UnboxExpr = SemUnboxExpr;
class NegateExpr = SemNegateExpr;
class AddOneExpr = SemAddOneExpr;
class SubOneExpr = SemSubOneExpr;
class ConditionalExpr = SemConditionalExpr;
class BasicBlock = SemBasicBlock;
class Guard = SemGuard;
predicate implies_v2 = semImplies_v2/4;
predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;
class Type = SemType;
class IntegerType = SemIntegerType;
class FloatingPointType = SemFloatingPointType;
class AddressType = SemAddressType;
class SsaVariable = SemSsaVariable;
class SsaPhiNode = SemSsaPhiNode;
class SsaExplicitUpdate = SemSsaExplicitUpdate;
class SsaReadPosition = SemSsaReadPosition;
class SsaReadPositionPhiInputEdge = SemSsaReadPositionPhiInputEdge;
class SsaReadPositionBlock = SemSsaReadPositionBlock;
predicate backEdge = semBackEdge/3;
predicate conversionCannotOverflow(Type fromType, Type toType) {
SemanticType::conversionCannotOverflow(fromType, toType)
}
}
module SignAnalysis implements SignAnalysisSig<Sem> {
private import SignAnalysisCommon as SA
import SA::SignAnalysis<FloatDelta, Util>
}
module ConstantBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
SemBound() {
this instanceof SemanticBound::SemZeroBound
@ -29,7 +120,7 @@ module ConstantBounds implements BoundSig<FloatDelta> {
}
}
module RelativeBounds implements BoundSig<FloatDelta> {
module RelativeBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
SemBound() { not this instanceof SemanticBound::SemZeroBound }
@ -47,13 +138,38 @@ module RelativeBounds implements BoundSig<FloatDelta> {
}
}
module AllBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
class SemBound instanceof SemanticBound::SemBound {
string toString() { result = super.toString() }
SemLocation getLocation() { result = super.getLocation() }
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 ModulusAnalysisInstantiated implements ModulusAnalysisSig<Sem> {
class ModBound = AllBounds::SemBound;
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.ModulusAnalysis as MA
import MA::ModulusAnalysis<FloatDelta, AllBounds, Util>
}
module Util = RangeUtil<FloatDelta, CppLangImplConstant>;
module ConstantStage =
RangeStage<FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
RangeUtil<FloatDelta, CppLangImplConstant>>;
RangeStage<SemLocation, Sem, FloatDelta, ConstantBounds, FloatOverflow, CppLangImplConstant,
SignAnalysis, ModulusAnalysisInstantiated, Util>;
module RelativeStage =
RangeStage<FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
RangeUtil<FloatDelta, CppLangImplRelative>>;
RangeStage<SemLocation, Sem, FloatDelta, RelativeBounds, FloatOverflow, CppLangImplRelative,
SignAnalysis, ModulusAnalysisInstantiated, Util>;
private newtype TSemReason =
TSemNoReason() or

Просмотреть файл

@ -3,13 +3,12 @@
*/
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisStage
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.FloatDelta
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.IntDelta
private import RangeAnalysisImpl
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
private import codeql.rangeanalysis.RangeAnalysis
module CppLangImplRelative implements LangSig<FloatDelta> {
module CppLangImplRelative implements LangSig<Sem, FloatDelta> {
/**
* Holds if the specified expression should be excluded from the result of `ssaRead()`.
*

Просмотреть файл

@ -4,10 +4,11 @@
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
private import RangeAnalysisRelativeSpecific
private import RangeAnalysisStage as Range
private import codeql.rangeanalysis.RangeAnalysis
private import RangeAnalysisImpl
private import ConstantAnalysis
module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::UtilSig<D> {
module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
/**
* Gets an expression that equals `v - d`.
*/
@ -138,27 +139,33 @@ module RangeUtil<Range::DeltaSig D, Range::LangSig<D> Lang> implements Range::Ut
or
not exists(Lang::getAlternateTypeForSsaVariable(var)) and result = var.getType()
}
import Ranking
}
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}
import Ranking
/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
module Ranking {
/**
* Holds if `rix` is the number of input edges to `phi`.
*/
predicate maxPhiInputRank(SemSsaPhiNode phi, int rix) {
rix = max(int r | rankedPhiInput(phi, _, _, r))
}
/**
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
* in an arbitrary 1-based numbering of the input edges to `phi`.
*/
predicate rankedPhiInput(
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
) {
edge.phiInput(phi, inp) and
edge =
rank[r](SemSsaReadPositionPhiInputEdge e |
e.phiInput(phi, _)
|
e order by e.getOrigBlock().getUniqueId()
)
}
}

Просмотреть файл

@ -6,14 +6,15 @@
* three-valued domain `{negative, zero, positive}`.
*/
private import RangeAnalysisStage
private import codeql.rangeanalysis.RangeAnalysis
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<D> Utils> {
module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
/**
* An SSA definition for which the analysis can compute the sign.
*
@ -507,4 +508,16 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
not semExprSign(e) = TPos() and
not semExprSign(e) = TZero()
}
/**
* Holds if `e` may have positive values. This does not rule out the
* possibility for negative values.
*/
predicate semMayBePositive(SemExpr e) { semExprSign(e) = TPos() }
/**
* Holds if `e` may have negative values. This does not rule out the
* possibility for positive values.
*/
predicate semMayBeNegative(SemExpr e) { semExprSign(e) = TNeg() }
}

Просмотреть файл

@ -56,7 +56,7 @@
while (f3_get(n)) n+=2;
for (int i = 0; i < n; i += 2) {
range(i); // $ range=>=0 SPURIOUS: range="<=Phi: call to f3_get-1" range="<=Phi: call to f3_get-2"
range(i); // $ range=>=0 range="<=Phi: call to f3_get-2"
}
}
@ -117,3 +117,16 @@ void test_sub(int x, int y, int n) {
}
}
}
void test_div(int x) {
if (3 <= x && x <= 7) {
range(x / 2); // $ range=>=1 range=<=3
range(x / 3); // $ range=>=1 range=<=2
range(x >> 2); // $ range=>=0 range=<=1
}
if (2 <= x && x <= 8) {
range(x / 2); // $ range=>=1 range=<=4
range(x / 3); // $ range=>=0 range=<=2
range(x >> 2); // $ range=>=0 range=<=2
}
}

Просмотреть файл

@ -25,16 +25,8 @@ abstract class Bound extends TBound {
/** Gets an expression that equals this bound. */
Expr getExpr() { result = this.getExpr(0) }
/**
* Holds if this element is at the specified location.
* The location spans column `sc` of line `sl` to
* column `ec` of line `el` in file `path`.
* For more information, see
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
*/
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
}
/** Gets the location of this bound. */
abstract Location getLocation();
}
/**
@ -45,6 +37,8 @@ class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
}
/**
@ -58,9 +52,7 @@ class SsaBound extends Bound, TBoundSsa {
override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
this.getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
override Location getLocation() { result = this.getSsa().getLocation() }
}
/**
@ -72,7 +64,5 @@ class ExprBound extends Bound, TBoundExpr {
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
this.getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
override Location getLocation() { result = this.getExpr().getLocation() }
}

Просмотреть файл

@ -12,6 +12,8 @@ class SsaVariable = SU::SsaVariable;
class Expr = CS::ControlFlow::Nodes::ExprNode;
class Location = CS::Location;
class IntegralType = CS::IntegralType;
class ConstantIntegerExpr = CU::ConstantIntegerExpr;

Просмотреть файл

@ -8,6 +8,7 @@ upgrades: upgrades
dependencies:
codeql/dataflow: ${workspace}
codeql/mad: ${workspace}
codeql/rangeanalysis: ${workspace}
codeql/regex: ${workspace}
codeql/tutorial: ${workspace}
codeql/typetracking: ${workspace}

Просмотреть файл

@ -1090,6 +1090,24 @@ class PrimitiveType extends Type, @primitive {
override string getAPrimaryQlClass() { result = "PrimitiveType" }
}
private int getByteSize(PrimitiveType t) {
t.hasName("boolean") and result = 1
or
t.hasName("byte") and result = 1
or
t.hasName("char") and result = 2
or
t.hasName("short") and result = 2
or
t.hasName("int") and result = 4
or
t.hasName("float") and result = 4
or
t.hasName("long") and result = 8
or
t.hasName("double") and result = 8
}
/** The type of the `null` literal. */
class NullType extends Type, @primitive {
NullType() { this.hasName("<nulltype>") }
@ -1282,6 +1300,12 @@ class IntegralType extends Type {
name = ["byte", "char", "short", "int", "long"]
)
}
/** Gets the size in bytes of this numeric type. */
final int getByteSize() {
result = getByteSize(this) or
result = getByteSize(this.(BoxedType).getPrimitiveType())
}
}
/** A boolean type, which may be either a primitive or a boxed type. */

Просмотреть файл

@ -25,16 +25,8 @@ abstract class Bound extends TBound {
/** Gets an expression that equals this bound. */
Expr getExpr() { result = this.getExpr(0) }
/**
* Holds if this element is at the specified location.
* The location spans column `sc` of line `sl` to
* column `ec` of line `el` in file `path`.
* For more information, see
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
*/
predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
}
/** Gets the location of this bound. */
abstract Location getLocation();
}
/**
@ -45,6 +37,8 @@ class ZeroBound extends Bound, TBoundZero {
override string toString() { result = "0" }
override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
override Location getLocation() { result.hasLocationInfo("", 0, 0, 0, 0) }
}
/**
@ -58,9 +52,7 @@ class SsaBound extends Bound, TBoundSsa {
override Expr getExpr(int delta) { result = this.getSsa().getAUse() and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
this.getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
override Location getLocation() { result = this.getSsa().getLocation() }
}
/**
@ -72,7 +64,5 @@ class ExprBound extends Bound, TBoundExpr {
override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
this.getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
}
override Location getLocation() { result = this.getExpr().getLocation() }
}

Разница между файлами не показана из-за своего большого размера Загрузить разницу

Просмотреть файл

@ -145,6 +145,9 @@ class ConstantStringExpr extends Expr {
string getStringValue() { constantStringExpr(this, result) }
}
bindingset[f]
private predicate okInt(float f) { -2.pow(31) <= f and f <= 2.pow(31) - 1 }
/**
* Gets an expression that equals `v - d`.
*/
@ -153,14 +156,16 @@ Expr ssaRead(SsaVariable v, int delta) {
or
exists(int d1, ConstantIntegerExpr c |
result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
delta = d1 - c.getIntValue()
delta = d1 - c.getIntValue() and
okInt(d1.(float) - c.getIntValue().(float))
)
or
exists(SubExpr sub, int d1, ConstantIntegerExpr c |
result = sub and
sub.getLeftOperand() = ssaRead(v, d1) and
sub.getRightOperand() = c and
delta = d1 + c.getIntValue()
delta = d1 + c.getIntValue() and
okInt(d1.(float) + c.getIntValue().(float))
)
or
v.(SsaExplicitUpdate).getDefiningExpr().(PreIncExpr) = result and delta = 0

Просмотреть файл

@ -10,6 +10,8 @@ class SsaVariable = Ssa::SsaVariable;
class Expr = J::Expr;
class Location = J::Location;
class IntegralType = J::IntegralType;
class ConstantIntegerExpr = RU::ConstantIntegerExpr;

Просмотреть файл

@ -0,0 +1,4 @@
---
category: minorAnalysis
---
* Initial release. Moves the range analysis library into its own qlpack.

Просмотреть файл

@ -0,0 +1,7 @@
name: codeql/rangeanalysis
version: 0.0.1-dev
groups: shared
library: true
dependencies:
codeql/util: ${workspace}
warnOnImplicitThis: true