mirror of
https://github.com/github/codeql.git
synced 2025-12-17 01:03:14 +01:00
Merge pull request #14659 from aschackmull/shared/modulus-analysis
Java/C++: Share modulus analysis
This commit is contained in:
Anders Schack-Mulligen
@@ -1,328 +0,0 @@
|
||||
/**
|
||||
* Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
|
||||
* an expression, `b` is a `Bound` (typically zero or the value of an SSA
|
||||
* variable), and `v` is an integer in the range `[0 .. m-1]`.
|
||||
*/
|
||||
|
||||
/*
|
||||
* The main recursion has base cases in both `ssaModulus` (for guarded reads) and `semExprModulus`
|
||||
* (for constant values). The most interesting recursive case is `phiModulusRankStep`, which
|
||||
* handles phi inputs.
|
||||
*/
|
||||
|
||||
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 codeql.rangeanalysis.RangeAnalysis
|
||||
private import RangeAnalysisImpl
|
||||
|
||||
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
|
||||
) {
|
||||
exists(SemGuard guard, boolean testIsTrue |
|
||||
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
|
||||
semGuardDirectlyControlsSsaRead(guard, pos, testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e + delta` equals `v` at `pos`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, SemExpr e, int delta) {
|
||||
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
|
||||
or
|
||||
pos.hasReadOfVar(v) and
|
||||
valueFlowStepSsaEqFlowCond(pos, v, e, delta)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
|
||||
* `ConstantIntegerExpr`s.
|
||||
*/
|
||||
private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) {
|
||||
exists(SemAddExpr a | a = add |
|
||||
larg = a.getLeftOperand() and
|
||||
rarg = a.getRightOperand()
|
||||
) and
|
||||
not larg instanceof SemConstantIntegerExpr and
|
||||
not rarg instanceof SemConstantIntegerExpr
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
|
||||
* a `ConstantIntegerExpr`.
|
||||
*/
|
||||
private predicate nonConstSubtraction(SemExpr sub, SemExpr larg, SemExpr rarg) {
|
||||
exists(SemSubExpr s | s = sub |
|
||||
larg = s.getLeftOperand() and
|
||||
rarg = s.getRightOperand()
|
||||
) and
|
||||
not rarg instanceof SemConstantIntegerExpr
|
||||
}
|
||||
|
||||
/** Gets an expression that is the remainder modulo `mod` of `arg`. */
|
||||
private SemExpr modExpr(SemExpr arg, int mod) {
|
||||
exists(SemRemExpr rem |
|
||||
result = rem and
|
||||
arg = rem.getLeftOperand() and
|
||||
rem.getRightOperand().(SemConstantIntegerExpr).getIntValue() = mod and
|
||||
mod >= 2
|
||||
)
|
||||
or
|
||||
exists(SemConstantIntegerExpr c |
|
||||
mod = 2.pow([1 .. 30]) and
|
||||
c.getIntValue() = mod - 1 and
|
||||
result.(SemBitAndExpr).hasOperands(arg, c)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
|
||||
* its `testIsTrue` branch.
|
||||
*/
|
||||
private SemGuard moduloCheck(SemSsaVariable v, int val, int mod, boolean testIsTrue) {
|
||||
exists(SemExpr rem, SemConstantIntegerExpr c, int r, boolean polarity |
|
||||
result.isEquality(rem, c, polarity) and
|
||||
c.getIntValue() = r and
|
||||
rem = modExpr(v.getAUse(), mod) and
|
||||
(
|
||||
testIsTrue = polarity and val = r
|
||||
or
|
||||
testIsTrue = polarity.booleanNot() and
|
||||
mod = 2 and
|
||||
val = 1 - r and
|
||||
(r = 0 or r = 1)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
|
||||
*/
|
||||
private predicate moduloGuardedRead(SemSsaVariable v, SemSsaReadPosition pos, int val, int mod) {
|
||||
exists(SemGuard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = moduloCheck(v, val, mod, testIsTrue) and
|
||||
semGuardControlsSsaRead(guard, pos, testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `factor` is a power of 2 that divides `mask`. */
|
||||
bindingset[mask]
|
||||
private predicate andmaskFactor(int mask, int factor) {
|
||||
mask % factor = 0 and
|
||||
factor = 2.pow([1 .. 30])
|
||||
}
|
||||
|
||||
/** Holds if `e` is evenly divisible by `factor`. */
|
||||
private predicate evenlyDivisibleExpr(SemExpr e, int factor) {
|
||||
exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() |
|
||||
e.(SemMulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
|
||||
or
|
||||
e.(SemShiftLeftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
|
||||
or
|
||||
e.(SemBitAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the remainder of `val` modulo `mod`.
|
||||
*
|
||||
* For `mod = 0` the result equals `val` and for `mod > 1` the result is within
|
||||
* the range `[0 .. mod-1]`.
|
||||
*/
|
||||
bindingset[val, mod]
|
||||
private int remainder(int val, int mod) {
|
||||
mod = 0 and result = val
|
||||
or
|
||||
mod > 1 and result = ((val % mod) + mod) % mod
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
|
||||
*/
|
||||
private predicate phiSelfModulus(
|
||||
SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int mod
|
||||
) {
|
||||
exists(Bounds::SemSsaBound phibound, int v, int m |
|
||||
edge.phiInput(phi, inp) and
|
||||
phibound.getVariable() = phi and
|
||||
ssaModulus(inp, edge, phibound, v, m) and
|
||||
mod = m.gcd(v) and
|
||||
mod != 1
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
|
||||
*/
|
||||
private predicate phiModulusInit(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
|
||||
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge |
|
||||
edge.phiInput(phi, inp) and
|
||||
ssaModulus(inp, edge, b, val, mod)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate phiModulusRankStep(
|
||||
SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod, int rix
|
||||
) {
|
||||
/*
|
||||
* base case. If any phi input is equal to `b + val` modulo `mod`, that's a potential congruence
|
||||
* class for the phi node.
|
||||
*/
|
||||
|
||||
rix = 0 and
|
||||
phiModulusInit(phi, b, val, mod)
|
||||
or
|
||||
exists(SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int v1, int m1 |
|
||||
mod != 1 and
|
||||
val = remainder(v1, mod)
|
||||
|
|
||||
/*
|
||||
* Recursive case. If `inp` = `b + v2` mod `m2`, we combine that with the preceding potential
|
||||
* congruence class `b + v1` mod `m1`. The result will be the congruence class of `v1` modulo
|
||||
* the greatest common denominator of `m1`, `m2`, and `v1 - v2`.
|
||||
*/
|
||||
|
||||
exists(int v2, int m2 |
|
||||
rankedPhiInput(pragma[only_bind_out](phi), inp, edge, rix) and
|
||||
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
|
||||
ssaModulus(inp, edge, b, v2, m2) and
|
||||
mod = m1.gcd(m2).gcd(v1 - v2)
|
||||
)
|
||||
or
|
||||
/*
|
||||
* Recursive case. If `inp` = `phi` mod `m2`, we combine that with the preceding potential
|
||||
* congruence class `b + v1` mod `m1`. The result will be a congruence class modulo the greatest
|
||||
* common denominator of `m1` and `m2`.
|
||||
*/
|
||||
|
||||
exists(int m2 |
|
||||
rankedPhiInput(phi, inp, edge, rix) and
|
||||
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
|
||||
phiSelfModulus(phi, inp, edge, m2) and
|
||||
mod = m1.gcd(m2)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `phi` is equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
private predicate phiModulus(SemSsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
|
||||
exists(int r |
|
||||
maxPhiInputRank(phi, r) and
|
||||
phiModulusRankStep(phi, b, val, mod, r)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
private predicate ssaModulus(
|
||||
SemSsaVariable v, SemSsaReadPosition pos, Bounds::SemBound b, int val, int mod
|
||||
) {
|
||||
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
|
||||
or
|
||||
b.(Bounds::SemSsaBound).getVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
|
||||
or
|
||||
exists(SemExpr e, int val0, int delta |
|
||||
semExprModulus(e, b, val0, mod) and
|
||||
valueFlowStepSsa(v, pos, e, delta) and
|
||||
val = remainder(val0 + delta, mod)
|
||||
)
|
||||
or
|
||||
moduloGuardedRead(v, pos, val, mod) and b instanceof Bounds::SemZeroBound
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e` is equal to `b + val` modulo `mod`.
|
||||
*
|
||||
* There are two cases for the modulus:
|
||||
* - `mod = 0`: The equality `e = b + val` is an ordinary equality.
|
||||
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
|
||||
*/
|
||||
cached
|
||||
predicate semExprModulus(SemExpr e, Bounds::SemBound b, int val, int mod) {
|
||||
not ignoreExprModulus(e) and
|
||||
(
|
||||
e = b.getExpr(D::fromInt(val)) and mod = 0
|
||||
or
|
||||
evenlyDivisibleExpr(e, mod) and
|
||||
val = 0 and
|
||||
b instanceof Bounds::SemZeroBound
|
||||
or
|
||||
exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
|
||||
ssaModulus(v, bb, b, val, mod) and
|
||||
e = v.getAUse() and
|
||||
bb.getAnExpr() = e
|
||||
)
|
||||
or
|
||||
exists(SemExpr mid, int val0, int delta |
|
||||
semExprModulus(mid, b, val0, mod) and
|
||||
U::semValueFlowStep(e, mid, D::fromInt(delta)) and
|
||||
val = remainder(val0 + delta, mod)
|
||||
)
|
||||
or
|
||||
exists(SemConditionalExpr cond, int v1, int v2, int m1, int m2 |
|
||||
cond = e and
|
||||
condExprBranchModulus(cond, true, b, v1, m1) and
|
||||
condExprBranchModulus(cond, false, b, v2, m2) and
|
||||
mod = m1.gcd(m2).gcd(v1 - v2) and
|
||||
mod != 1 and
|
||||
val = remainder(v1, mod)
|
||||
)
|
||||
or
|
||||
exists(Bounds::SemBound b1, Bounds::SemBound b2, int v1, int v2, int m1, int m2 |
|
||||
addModulus(e, true, b1, v1, m1) and
|
||||
addModulus(e, false, b2, v2, m2) and
|
||||
mod = m1.gcd(m2) and
|
||||
mod != 1 and
|
||||
val = remainder(v1 + v2, mod)
|
||||
|
|
||||
b = b1 and b2 instanceof Bounds::SemZeroBound
|
||||
or
|
||||
b = b2 and b1 instanceof Bounds::SemZeroBound
|
||||
)
|
||||
or
|
||||
exists(int v1, int v2, int m1, int m2 |
|
||||
subModulus(e, true, b, v1, m1) and
|
||||
subModulus(e, false, any(Bounds::SemZeroBound zb), v2, m2) and
|
||||
mod = m1.gcd(m2) and
|
||||
mod != 1 and
|
||||
val = remainder(v1 - v2, mod)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate condExprBranchModulus(
|
||||
SemConditionalExpr cond, boolean branch, Bounds::SemBound b, int val, int mod
|
||||
) {
|
||||
semExprModulus(cond.getBranchExpr(branch), b, val, mod)
|
||||
}
|
||||
|
||||
private predicate addModulus(SemExpr add, boolean isLeft, Bounds::SemBound b, int val, int mod) {
|
||||
exists(SemExpr larg, SemExpr rarg | nonConstAddition(add, larg, rarg) |
|
||||
semExprModulus(larg, b, val, mod) and isLeft = true
|
||||
or
|
||||
semExprModulus(rarg, b, val, mod) and isLeft = false
|
||||
)
|
||||
}
|
||||
|
||||
private predicate subModulus(SemExpr sub, boolean isLeft, Bounds::SemBound b, int val, int mod) {
|
||||
exists(SemExpr larg, SemExpr rarg | nonConstSubtraction(sub, larg, rarg) |
|
||||
semExprModulus(larg, b, val, mod) and isLeft = true
|
||||
or
|
||||
semExprModulus(rarg, b, val, mod) and isLeft = false
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -1,8 +0,0 @@
|
||||
/**
|
||||
* C++-specific implementation of modulus analysis.
|
||||
*/
|
||||
module Private {
|
||||
private import semmle.code.cpp.rangeanalysis.new.internal.semantic.Semantic
|
||||
|
||||
predicate ignoreExprModulus(SemExpr e) { none() }
|
||||
}
|
||||
@@ -78,6 +78,8 @@ module Sem implements Semantic {
|
||||
|
||||
predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;
|
||||
|
||||
predicate guardControlsSsaRead = semGuardControlsSsaRead/3;
|
||||
|
||||
class Type = SemType;
|
||||
|
||||
class IntegerType = SemIntegerType;
|
||||
@@ -169,8 +171,8 @@ module AllBounds implements BoundSig<SemLocation, Sem, FloatDelta> {
|
||||
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>
|
||||
private import codeql.rangeanalysis.ModulusAnalysis as MA
|
||||
import MA::ModulusAnalysis<SemLocation, Sem, FloatDelta, AllBounds, Util>
|
||||
}
|
||||
|
||||
module Util = RangeUtil<FloatDelta, CppLangImplConstant>;
|
||||
|
||||
@@ -1,6 +1,7 @@
|
||||
import cpp
|
||||
import semmle.code.cpp.rangeanalysis.new.internal.semantic.analysis.ModulusAnalysis
|
||||
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
|
||||
@@ -10,7 +11,8 @@ import semmle.code.cpp.ir.IR as IR
|
||||
import TestUtilities.InlineExpectationsTest
|
||||
|
||||
module ModulusAnalysisInstantiated =
|
||||
ModulusAnalysis<FloatDelta, ConstantBounds, RangeUtil<FloatDelta, CppLangImplRelative>>;
|
||||
ModulusAnalysis<SemLocation, Sem, FloatDelta, ConstantBounds,
|
||||
RangeUtil<FloatDelta, CppLangImplRelative>>;
|
||||
|
||||
module ModulusAnalysisTest implements TestSig {
|
||||
string getARelevantTag() { result = "mod" }
|
||||
@@ -31,7 +33,7 @@ import MakeTest<ModulusAnalysisTest>
|
||||
|
||||
private string getAModString(SemExpr e) {
|
||||
exists(SemBound b, int delta, int mod |
|
||||
ModulusAnalysisInstantiated::semExprModulus(e, b, delta, mod) and
|
||||
ModulusAnalysisInstantiated::exprModulus(e, b, delta, mod) and
|
||||
result = b.toString() + "," + delta.toString() + "," + mod.toString() and
|
||||
not (delta = 0 and mod = 0)
|
||||
)
|
||||
|
||||
@@ -70,7 +70,6 @@ private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionC
|
||||
private import semmle.code.java.controlflow.internal.GuardsLogic
|
||||
private import semmle.code.java.security.RandomDataSource
|
||||
private import SignAnalysis
|
||||
private import ModulusAnalysis
|
||||
private import semmle.code.java.Reflection
|
||||
private import semmle.code.java.Collections
|
||||
private import semmle.code.java.Maps
|
||||
@@ -224,6 +223,10 @@ module Sem implements Semantic {
|
||||
RU::guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
|
||||
}
|
||||
|
||||
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
RU::guardControlsSsaRead(guard, controlled, testIsTrue)
|
||||
}
|
||||
|
||||
class Type = J::Type;
|
||||
|
||||
class IntegerType extends J::IntegralType {
|
||||
@@ -292,7 +295,8 @@ module SignInp implements SignAnalysisSig<Sem> {
|
||||
module Modulus implements ModulusAnalysisSig<Sem> {
|
||||
class ModBound = Bound;
|
||||
|
||||
predicate semExprModulus = exprModulus/4;
|
||||
private import codeql.rangeanalysis.ModulusAnalysis as Mod
|
||||
import Mod::ModulusAnalysis<Location, Sem, IntDelta, Bounds, Utils>
|
||||
}
|
||||
|
||||
module IntDelta implements DeltaSig {
|
||||
|
||||
318
shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
Normal file
318
shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
Normal file
@@ -0,0 +1,318 @@
|
||||
/**
|
||||
* Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
|
||||
* an expression, `b` is a `Bound` (typically zero or the value of an SSA
|
||||
* variable), and `v` is an integer in the range `[0 .. m-1]`.
|
||||
*/
|
||||
|
||||
/*
|
||||
* The main recursion has base cases in both `ssaModulus` (for guarded reads) and `exprModulus`
|
||||
* (for constant values). The most interesting recursive case is `phiModulusRankStep`, which
|
||||
* handles phi inputs.
|
||||
*/
|
||||
|
||||
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>
|
||||
{
|
||||
bindingset[pos, v]
|
||||
pragma[inline_late]
|
||||
private predicate hasReadOfVarInlineLate(Sem::SsaReadPosition pos, Sem::SsaVariable v) {
|
||||
pos.hasReadOfVar(v)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e + delta` equals `v` at `pos`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate valueFlowStepSsa(
|
||||
Sem::SsaVariable v, Sem::SsaReadPosition pos, Sem::Expr e, int delta
|
||||
) {
|
||||
U::semSsaUpdateStep(v, e, D::fromInt(delta)) and pos.hasReadOfVar(v)
|
||||
or
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
hasReadOfVarInlineLate(pos, v) and
|
||||
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
|
||||
Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `add` is the addition of `larg` and `rarg`, neither of which are
|
||||
* `ConstantIntegerExpr`s.
|
||||
*/
|
||||
private predicate nonConstAddition(Sem::Expr add, Sem::Expr larg, Sem::Expr rarg) {
|
||||
exists(Sem::AddExpr a | a = add |
|
||||
larg = a.getLeftOperand() and
|
||||
rarg = a.getRightOperand()
|
||||
) and
|
||||
not larg instanceof Sem::ConstantIntegerExpr and
|
||||
not rarg instanceof Sem::ConstantIntegerExpr
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
|
||||
* a `ConstantIntegerExpr`.
|
||||
*/
|
||||
private predicate nonConstSubtraction(Sem::Expr sub, Sem::Expr larg, Sem::Expr rarg) {
|
||||
exists(Sem::SubExpr s | s = sub |
|
||||
larg = s.getLeftOperand() and
|
||||
rarg = s.getRightOperand()
|
||||
) and
|
||||
not rarg instanceof Sem::ConstantIntegerExpr
|
||||
}
|
||||
|
||||
/** Gets an expression that is the remainder modulo `mod` of `arg`. */
|
||||
private Sem::Expr modExpr(Sem::Expr arg, int mod) {
|
||||
exists(Sem::RemExpr rem |
|
||||
result = rem and
|
||||
arg = rem.getLeftOperand() and
|
||||
rem.getRightOperand().(Sem::ConstantIntegerExpr).getIntValue() = mod and
|
||||
mod >= 2
|
||||
)
|
||||
or
|
||||
exists(Sem::ConstantIntegerExpr c |
|
||||
mod = 2.pow([1 .. 30]) and
|
||||
c.getIntValue() = mod - 1 and
|
||||
result.(Sem::BitAndExpr).hasOperands(arg, c)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
|
||||
* its `testIsTrue` branch.
|
||||
*/
|
||||
private Sem::Guard moduloCheck(Sem::SsaVariable v, int val, int mod, boolean testIsTrue) {
|
||||
exists(Sem::Expr rem, Sem::ConstantIntegerExpr c, int r, boolean polarity |
|
||||
result.isEquality(rem, c, polarity) and
|
||||
c.getIntValue() = r and
|
||||
rem = modExpr(v.getAUse(), mod) and
|
||||
(
|
||||
testIsTrue = polarity and val = r
|
||||
or
|
||||
testIsTrue = polarity.booleanNot() and
|
||||
mod = 2 and
|
||||
val = 1 - r and
|
||||
(r = 0 or r = 1)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
|
||||
*/
|
||||
private predicate moduloGuardedRead(Sem::SsaVariable v, Sem::SsaReadPosition pos, int val, int mod) {
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = moduloCheck(v, val, mod, testIsTrue) and
|
||||
Sem::guardControlsSsaRead(guard, pos, testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `factor` is a power of 2 that divides `mask`. */
|
||||
bindingset[mask]
|
||||
private predicate andmaskFactor(int mask, int factor) {
|
||||
mask % factor = 0 and
|
||||
factor = 2.pow([1 .. 30])
|
||||
}
|
||||
|
||||
/** Holds if `e` is evenly divisible by `factor`. */
|
||||
private predicate evenlyDivisibleExpr(Sem::Expr e, int factor) {
|
||||
exists(Sem::ConstantIntegerExpr c, int k | k = c.getIntValue() |
|
||||
e.(Sem::MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
|
||||
or
|
||||
e.(Sem::ShiftLeftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
|
||||
or
|
||||
e.(Sem::BitAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the remainder of `val` modulo `mod`.
|
||||
*
|
||||
* For `mod = 0` the result equals `val` and for `mod > 1` the result is within
|
||||
* the range `[0 .. mod-1]`.
|
||||
*/
|
||||
bindingset[val, mod]
|
||||
private int remainder(int val, int mod) {
|
||||
mod = 0 and result = val
|
||||
or
|
||||
mod > 1 and result = ((val % mod) + mod) % mod
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
|
||||
*/
|
||||
private predicate phiSelfModulus(
|
||||
Sem::SsaPhiNode phi, Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int mod
|
||||
) {
|
||||
exists(Bounds::SemSsaBound phibound, int v, int m |
|
||||
edge.phiInput(phi, inp) and
|
||||
phibound.getVariable() = phi and
|
||||
ssaModulus(inp, edge, phibound, v, m) and
|
||||
mod = m.gcd(v) and
|
||||
mod != 1
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
|
||||
*/
|
||||
private predicate phiModulusInit(Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
|
||||
exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge |
|
||||
edge.phiInput(phi, inp) and
|
||||
ssaModulus(inp, edge, b, val, mod)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate phiModulusRankStep(
|
||||
Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod, int rix
|
||||
) {
|
||||
// Base case. If any phi input is equal to `b + val` modulo `mod`, that's a
|
||||
// potential congruence class for the phi node.
|
||||
rix = 0 and
|
||||
phiModulusInit(phi, b, val, mod)
|
||||
or
|
||||
exists(Sem::SsaVariable inp, Sem::SsaReadPositionPhiInputEdge edge, int v1, int m1 |
|
||||
mod != 1 and
|
||||
val = remainder(v1, mod)
|
||||
|
|
||||
// Recursive case. If `inp` = `b + v2` modulo `m2`, we combine that with
|
||||
// the preceding potential congruence class `b + v1` modulo `m1`. In order
|
||||
// to represent the result as a single congruence class `b + v` modulo
|
||||
// `mod`, we must have that `mod` divides both `m1` and `m2` and that `v1`
|
||||
// equals `v2` modulo `mod`. The largest value of `mod` that satisfies
|
||||
// this is the greatest common divisor of `m1`, `m2`, and `v1 - v2`.
|
||||
exists(int v2, int m2 |
|
||||
U::rankedPhiInput(phi, inp, edge, rix) and
|
||||
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
|
||||
ssaModulus(inp, edge, b, v2, m2) and
|
||||
mod = m1.gcd(m2).gcd(v1 - v2)
|
||||
)
|
||||
or
|
||||
// Recursive case. If `inp` = `phi` mod `m2`, we combine that with the
|
||||
// preceding potential congruence class `b + v1` mod `m1`. The result will be
|
||||
// the congruence class modulo the greatest common divisor of `m1` and `m2`.
|
||||
exists(int m2 |
|
||||
U::rankedPhiInput(phi, inp, edge, rix) and
|
||||
phiModulusRankStep(phi, b, v1, m1, rix - 1) and
|
||||
phiSelfModulus(phi, inp, edge, m2) and
|
||||
mod = m1.gcd(m2)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `phi` is equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
private predicate phiModulus(Sem::SsaPhiNode phi, Bounds::SemBound b, int val, int mod) {
|
||||
exists(int r |
|
||||
U::maxPhiInputRank(phi, r) and
|
||||
phiModulusRankStep(phi, b, val, mod, r)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
|
||||
*/
|
||||
private predicate ssaModulus(
|
||||
Sem::SsaVariable v, Sem::SsaReadPosition pos, Bounds::SemBound b, int val, int mod
|
||||
) {
|
||||
phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
|
||||
or
|
||||
b.(Bounds::SemSsaBound).getVariable() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
|
||||
or
|
||||
exists(Sem::Expr e, int val0, int delta |
|
||||
exprModulus(e, b, val0, mod) and
|
||||
valueFlowStepSsa(v, pos, e, delta) and
|
||||
val = remainder(val0 + delta, mod)
|
||||
)
|
||||
or
|
||||
moduloGuardedRead(v, pos, val, mod) and b instanceof Bounds::SemZeroBound
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `e` is equal to `b + val` modulo `mod`.
|
||||
*
|
||||
* There are two cases for the modulus:
|
||||
* - `mod = 0`: The equality `e = b + val` is an ordinary equality.
|
||||
* - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
|
||||
*/
|
||||
cached
|
||||
predicate exprModulus(Sem::Expr e, Bounds::SemBound b, int val, int mod) {
|
||||
e = b.getExpr(D::fromInt(val)) and mod = 0
|
||||
or
|
||||
evenlyDivisibleExpr(e, mod) and
|
||||
val = 0 and
|
||||
b instanceof Bounds::SemZeroBound
|
||||
or
|
||||
exists(Sem::SsaVariable v, Sem::SsaReadPositionBlock bb |
|
||||
ssaModulus(v, bb, b, val, mod) and
|
||||
e = v.getAUse() and
|
||||
bb.getBlock() = e.getBasicBlock()
|
||||
)
|
||||
or
|
||||
exists(Sem::Expr mid, int val0, int delta |
|
||||
exprModulus(mid, b, val0, mod) and
|
||||
U::semValueFlowStep(e, mid, D::fromInt(delta)) and
|
||||
val = remainder(val0 + delta, mod)
|
||||
)
|
||||
or
|
||||
exists(Sem::ConditionalExpr cond, int v1, int v2, int m1, int m2 |
|
||||
cond = e and
|
||||
condExprBranchModulus(cond, true, b, v1, m1) and
|
||||
condExprBranchModulus(cond, false, b, v2, m2) and
|
||||
mod = m1.gcd(m2).gcd(v1 - v2) and
|
||||
mod != 1 and
|
||||
val = remainder(v1, mod)
|
||||
)
|
||||
or
|
||||
exists(Bounds::SemBound b1, Bounds::SemBound b2, int v1, int v2, int m1, int m2 |
|
||||
addModulus(e, true, b1, v1, m1) and
|
||||
addModulus(e, false, b2, v2, m2) and
|
||||
mod = m1.gcd(m2) and
|
||||
mod != 1 and
|
||||
val = remainder(v1 + v2, mod)
|
||||
|
|
||||
b = b1 and b2 instanceof Bounds::SemZeroBound
|
||||
or
|
||||
b = b2 and b1 instanceof Bounds::SemZeroBound
|
||||
)
|
||||
or
|
||||
exists(int v1, int v2, int m1, int m2 |
|
||||
subModulus(e, true, b, v1, m1) and
|
||||
subModulus(e, false, any(Bounds::SemZeroBound zb), v2, m2) and
|
||||
mod = m1.gcd(m2) and
|
||||
mod != 1 and
|
||||
val = remainder(v1 - v2, mod)
|
||||
)
|
||||
}
|
||||
|
||||
private predicate condExprBranchModulus(
|
||||
Sem::ConditionalExpr cond, boolean branch, Bounds::SemBound b, int val, int mod
|
||||
) {
|
||||
exprModulus(cond.getBranchExpr(branch), b, val, mod)
|
||||
}
|
||||
|
||||
private predicate addModulus(Sem::Expr add, boolean isLeft, Bounds::SemBound b, int val, int mod) {
|
||||
exists(Sem::Expr larg, Sem::Expr rarg | nonConstAddition(add, larg, rarg) |
|
||||
exprModulus(larg, b, val, mod) and isLeft = true
|
||||
or
|
||||
exprModulus(rarg, b, val, mod) and isLeft = false
|
||||
)
|
||||
}
|
||||
|
||||
private predicate subModulus(Sem::Expr sub, boolean isLeft, Bounds::SemBound b, int val, int mod) {
|
||||
exists(Sem::Expr larg, Sem::Expr rarg | nonConstSubtraction(sub, larg, rarg) |
|
||||
exprModulus(larg, b, val, mod) and isLeft = true
|
||||
or
|
||||
exprModulus(rarg, b, val, mod) and isLeft = false
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -152,12 +152,16 @@ signature module Semantic {
|
||||
Expr asExpr();
|
||||
|
||||
predicate directlyControls(BasicBlock controlled, boolean branch);
|
||||
|
||||
predicate isEquality(Expr e1, Expr e2, boolean polarity);
|
||||
}
|
||||
|
||||
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2);
|
||||
|
||||
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue);
|
||||
|
||||
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue);
|
||||
|
||||
class Type;
|
||||
|
||||
class IntegerType extends Type {
|
||||
@@ -226,7 +230,7 @@ signature module SignAnalysisSig<Semantic Sem> {
|
||||
signature module ModulusAnalysisSig<Semantic Sem> {
|
||||
class ModBound;
|
||||
|
||||
predicate semExprModulus(Sem::Expr e, ModBound b, int val, int mod);
|
||||
predicate exprModulus(Sem::Expr e, ModBound b, int val, int mod);
|
||||
}
|
||||
|
||||
signature module DeltaSig {
|
||||
@@ -356,7 +360,7 @@ 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> ModulusAnalysis, UtilSig<Sem, D> UtilParam>
|
||||
ModulusAnalysisSig<Sem> ModulusAnalysisParam, UtilSig<Sem, D> UtilParam>
|
||||
{
|
||||
private import Bounds
|
||||
private import LangParam
|
||||
@@ -364,7 +368,7 @@ module RangeStage<
|
||||
private import D
|
||||
private import OverflowParam
|
||||
private import SignAnalysis
|
||||
private import ModulusAnalysis
|
||||
private import ModulusAnalysisParam
|
||||
private import internal.RangeUtils::MakeUtils<Sem, D>
|
||||
|
||||
/**
|
||||
@@ -537,8 +541,8 @@ module RangeStage<
|
||||
// strict then the strengthening amount is instead `k - 1` modulo `mod`:
|
||||
// `x < y` means `0 <= y - x - 1 =(mod) k - 1` so `k - 1 <= y - x - 1` and
|
||||
// thus `k - 1 < y - x` with `0 <= k - 1 < mod`.
|
||||
semExprModulus(comp.getLesserOperand(), b, v1, mod1) and
|
||||
semExprModulus(comp.getGreaterOperand(), b, v2, mod2) and
|
||||
exprModulus(comp.getLesserOperand(), b, v1, mod1) and
|
||||
exprModulus(comp.getGreaterOperand(), b, v2, mod2) and
|
||||
mod = mod1.gcd(mod2) and
|
||||
mod != 1 and
|
||||
(testIsTrue = true or testIsTrue = false) and
|
||||
|
||||
Reference in New Issue
Block a user