Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

C++/Java: Share core range analysis #14588

Merged
merged 14 commits into from
Oct 26, 2023
Merged
Show file tree
Hide file tree
Changes from 11 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions cpp/ql/lib/qlpack.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ library: true
upgrades: upgrades
dependencies:
codeql/dataflow: ${workspace}
codeql/rangeanalysis: ${workspace}
codeql/ssa: ${workspace}
codeql/tutorial: ${workspace}
codeql/util: ${workspace}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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
Expand Down

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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()`.
*
Expand Down
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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 }

Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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()`.
*
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
*/
Expand Down Expand Up @@ -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()
}
}

/**
* 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()
)
import Ranking

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()
)
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -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.
*
Expand Down Expand Up @@ -507,4 +508,16 @@
not semExprSign(e) = TPos() and
not semExprSign(e) = TZero()
}

/**
* Holds if `e` may have positive values. This does not rule out the
* possibilty for negative values.
*/
Fixed Show fixed Hide fixed
predicate semMayBePositive(SemExpr e) { semExprSign(e) = TPos() }

/**
* Holds if `e` may have negative values. This does not rule out the
* possibilty for positive values.
*/
Fixed Show fixed Hide fixed
predicate semMayBeNegative(SemExpr e) { semExprSign(e) = TNeg() }
}
Loading
Loading