mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Java/C++: Move range util guard-controls predicates to shared pack.
This commit is contained in:
@@ -35,32 +35,4 @@ predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
|
||||
Specific::implies_v2(g1, b1, g2, b2)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` directly controls the position `controlled` with the
|
||||
* value `testIsTrue`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate semGuardDirectlyControlsSsaRead(
|
||||
SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue
|
||||
) {
|
||||
guard.directlyControls(controlled.(SemSsaReadPositionBlock).getBlock(), testIsTrue)
|
||||
or
|
||||
exists(SemSsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
|
||||
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
|
||||
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
|
||||
*/
|
||||
predicate semGuardControlsSsaRead(SemGuard guard, SemSsaReadPosition controlled, boolean testIsTrue) {
|
||||
semGuardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
|
||||
or
|
||||
exists(SemGuard guard0, boolean testIsTrue0 |
|
||||
semImplies_v2(guard0, testIsTrue0, guard, testIsTrue) and
|
||||
semGuardControlsSsaRead(guard0, controlled, testIsTrue0)
|
||||
)
|
||||
}
|
||||
|
||||
SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }
|
||||
|
||||
@@ -78,10 +78,6 @@ module Sem implements Semantic {
|
||||
|
||||
predicate implies_v2 = semImplies_v2/4;
|
||||
|
||||
predicate guardDirectlyControlsSsaRead = semGuardDirectlyControlsSsaRead/3;
|
||||
|
||||
predicate guardControlsSsaRead = semGuardControlsSsaRead/3;
|
||||
|
||||
class Type = SemType;
|
||||
|
||||
class IntegerType = SemIntegerType;
|
||||
|
||||
@@ -294,7 +294,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
) {
|
||||
exists(boolean testIsTrue, SemRelationalExpr comp |
|
||||
pos.hasReadOfVar(v) and
|
||||
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
|
||||
guardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
|
||||
not unknownSign(lowerbound)
|
||||
|
|
||||
testIsTrue = true and
|
||||
@@ -318,7 +318,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
) {
|
||||
exists(boolean testIsTrue, SemRelationalExpr comp |
|
||||
pos.hasReadOfVar(v) and
|
||||
semGuardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
|
||||
guardControlsSsaRead(semGetComparisonGuard(comp), pos, testIsTrue) and
|
||||
not unknownSign(upperbound)
|
||||
|
|
||||
testIsTrue = true and
|
||||
@@ -343,7 +343,7 @@ module SignAnalysis<DeltaSig D, UtilSig<Sem, D> Utils> {
|
||||
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
|
||||
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
|
||||
pos.hasReadOfVar(pragma[only_bind_into](v)) and
|
||||
semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
|
||||
guardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
|
||||
e = ssaRead(pragma[only_bind_into](v), D::fromInt(0)) and
|
||||
guard.isEquality(eqbound, e, polarity) and
|
||||
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
|
||||
|
||||
@@ -223,14 +223,6 @@ module Sem implements Semantic {
|
||||
GL::implies_v2(g1, b1, g2, b2)
|
||||
}
|
||||
|
||||
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
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 {
|
||||
@@ -267,6 +259,8 @@ module Sem implements Semantic {
|
||||
{
|
||||
BasicBlock getOrigBlock() { result = super.getOrigBlock() }
|
||||
|
||||
BasicBlock getPhiBlock() { result = super.getPhiBlock() }
|
||||
|
||||
predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
|
||||
}
|
||||
|
||||
|
||||
@@ -10,7 +10,15 @@ private import semmle.code.java.Constants
|
||||
private import semmle.code.java.dataflow.RangeAnalysis
|
||||
private import codeql.rangeanalysis.internal.RangeUtils
|
||||
|
||||
private predicate backEdge = MakeUtils<Sem, IntDelta>::backEdge/3;
|
||||
private module U = MakeUtils<Sem, IntDelta>;
|
||||
|
||||
private predicate backEdge = U::backEdge/3;
|
||||
|
||||
predicate ssaRead = U::ssaRead/2;
|
||||
|
||||
predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
|
||||
|
||||
predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
|
||||
|
||||
/**
|
||||
* Holds if `v` is an input to `phi` that is not along a back edge, and the
|
||||
@@ -149,67 +157,6 @@ 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`.
|
||||
*/
|
||||
Expr ssaRead(SsaVariable v, int delta) {
|
||||
result = v.getAUse() and delta = 0
|
||||
or
|
||||
exists(int d1, ConstantIntegerExpr c |
|
||||
result.(AddExpr).hasOperands(ssaRead(v, d1), c) and
|
||||
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() and
|
||||
okInt(d1.(float) + c.getIntValue().(float))
|
||||
)
|
||||
or
|
||||
v.(SsaExplicitUpdate).getDefiningExpr().(PreIncExpr) = result and delta = 0
|
||||
or
|
||||
v.(SsaExplicitUpdate).getDefiningExpr().(PreDecExpr) = result and delta = 0
|
||||
or
|
||||
v.(SsaExplicitUpdate).getDefiningExpr().(PostIncExpr) = result and delta = 1 // x++ === ++x - 1
|
||||
or
|
||||
v.(SsaExplicitUpdate).getDefiningExpr().(PostDecExpr) = result and delta = -1 // x-- === --x + 1
|
||||
or
|
||||
v.(SsaExplicitUpdate).getDefiningExpr().(Assignment) = result and delta = 0
|
||||
or
|
||||
result.(AssignExpr).getSource() = ssaRead(v, delta)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` directly controls the position `controlled` with the
|
||||
* value `testIsTrue`.
|
||||
*/
|
||||
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
|
||||
or
|
||||
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
|
||||
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
|
||||
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
|
||||
*/
|
||||
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
|
||||
or
|
||||
exists(Guard guard0, boolean testIsTrue0 |
|
||||
implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
|
||||
guardControlsSsaRead(guard0, controlled, testIsTrue0)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a condition that tests whether `v` equals `e + delta`.
|
||||
*
|
||||
|
||||
@@ -17,6 +17,8 @@ module ModulusAnalysis<
|
||||
LocationSig Location, Semantic Sem, DeltaSig D, BoundSig<Location, Sem, D> Bounds,
|
||||
UtilSig<Sem, D> U>
|
||||
{
|
||||
private import internal.RangeUtils::MakeUtils<Sem, D>
|
||||
|
||||
bindingset[pos, v]
|
||||
pragma[inline_late]
|
||||
private predicate hasReadOfVarInlineLate(Sem::SsaReadPosition pos, Sem::SsaVariable v) {
|
||||
@@ -35,7 +37,7 @@ module ModulusAnalysis<
|
||||
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)
|
||||
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -107,7 +109,7 @@ module ModulusAnalysis<
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = moduloCheck(v, val, mod, testIsTrue) and
|
||||
Sem::guardControlsSsaRead(guard, pos, testIsTrue)
|
||||
guardControlsSsaRead(guard, pos, testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
@@ -160,14 +160,12 @@ signature module Semantic {
|
||||
predicate directlyControls(BasicBlock controlled, boolean branch);
|
||||
|
||||
predicate isEquality(Expr e1, Expr e2, boolean polarity);
|
||||
|
||||
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
|
||||
}
|
||||
|
||||
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 {
|
||||
@@ -199,6 +197,8 @@ signature module Semantic {
|
||||
class SsaReadPositionPhiInputEdge extends SsaReadPosition {
|
||||
BasicBlock getOrigBlock();
|
||||
|
||||
BasicBlock getPhiBlock();
|
||||
|
||||
predicate phiInput(SsaPhiNode phi, SsaVariable inp);
|
||||
}
|
||||
|
||||
@@ -699,7 +699,7 @@ module RangeStage<
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
|
||||
Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TSemCondReason(guard)
|
||||
)
|
||||
}
|
||||
@@ -712,7 +712,7 @@ module RangeStage<
|
||||
exists(Sem::Guard guard, boolean testIsTrue |
|
||||
pos.hasReadOfVar(v) and
|
||||
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
|
||||
Sem::guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
|
||||
reason = TSemCondReason(guard)
|
||||
)
|
||||
}
|
||||
|
||||
@@ -35,6 +35,32 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
|
||||
result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` directly controls the position `controlled` with the
|
||||
* value `testIsTrue`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate guardDirectlyControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guard.directlyControls(controlled.(Lang::SsaReadPositionBlock).getBlock(), testIsTrue)
|
||||
or
|
||||
exists(Lang::SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
|
||||
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
|
||||
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
|
||||
*/
|
||||
predicate guardControlsSsaRead(Lang::Guard guard, Lang::SsaReadPosition controlled, boolean testIsTrue) {
|
||||
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
|
||||
or
|
||||
exists(Lang::Guard guard0, boolean testIsTrue0 |
|
||||
Lang::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
|
||||
guardControlsSsaRead(guard0, controlled, testIsTrue0)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `inp` is an input to `phi` along a back edge.
|
||||
*/
|
||||
|
||||
Reference in New Issue
Block a user