Skip to content

Commit daffae0

Browse files
aschackmullaschackmull
committed
Java/C++: Share eqFlowCond.
1 parent cad003a commit daffae0

File tree

6 files changed

+27
-84
lines changed

6 files changed

+27
-84
lines changed

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll

-50
Original file line numberDiff line numberDiff line change
@@ -9,56 +9,6 @@ private import RangeAnalysisImpl
99
private import ConstantAnalysis
1010

1111
module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
12-
/**
13-
* Gets an expression that equals `v - d`.
14-
*/
15-
private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
16-
// There are various language-specific extension points that can be removed once we no longer
17-
// expect to match the original Java implementation's results exactly.
18-
result = v.getAUse() and delta = D::fromInt(0)
19-
or
20-
exists(D::Delta d1, SemConstantIntegerExpr c |
21-
result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
22-
delta = D::fromFloat(D::toFloat(d1) - c.getIntValue())
23-
)
24-
or
25-
exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c |
26-
result = sub and
27-
sub.getLeftOperand() = semSsaRead(v, d1) and
28-
sub.getRightOperand() = c and
29-
delta = D::fromFloat(D::toFloat(d1) + c.getIntValue())
30-
)
31-
or
32-
result = v.(SemSsaExplicitUpdate).getSourceExpr() and
33-
delta = D::fromFloat(0)
34-
or
35-
result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta)
36-
or
37-
result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
38-
}
39-
40-
/**
41-
* Gets a condition that tests whether `v` equals `e + delta`.
42-
*
43-
* If the condition evaluates to `testIsTrue`:
44-
* - `isEq = true` : `v == e + delta`
45-
* - `isEq = false` : `v != e + delta`
46-
*/
47-
pragma[nomagic]
48-
SemGuard semEqFlowCond(
49-
SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
50-
) {
51-
exists(boolean eqpolarity |
52-
result.isEquality(semSsaRead(v, delta), e, eqpolarity) and
53-
(testIsTrue = true or testIsTrue = false) and
54-
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
55-
)
56-
or
57-
exists(boolean testIsTrue0 |
58-
semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
59-
)
60-
}
61-
6212
/**
6313
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
6414
*/

‎java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

-6
Original file line numberDiff line numberDiff line change
@@ -372,12 +372,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
372372
module Utils implements UtilSig<Sem, IntDelta> {
373373
private import RangeUtils as RU
374374

375-
Sem::Guard semEqFlowCond(
376-
Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
377-
) {
378-
result = RU::eqFlowCond(v, e, delta, isEq, testIsTrue)
379-
}
380-
381375
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) {
382376
RU::ssaUpdateStep(v, e, delta)
383377
}

‎java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll

+2-19
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
1919

2020
predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
2121

22+
predicate eqFlowCond = U::eqFlowCond/5;
23+
2224
/**
2325
* Holds if `v` is an input to `phi` that is not along a back edge, and the
2426
* only other input to `phi` is a `null` value.
@@ -156,25 +158,6 @@ class ConstantStringExpr extends Expr {
156158
string getStringValue() { constantStringExpr(this, result) }
157159
}
158160

159-
/**
160-
* Gets a condition that tests whether `v` equals `e + delta`.
161-
*
162-
* If the condition evaluates to `testIsTrue`:
163-
* - `isEq = true` : `v == e + delta`
164-
* - `isEq = false` : `v != e + delta`
165-
*/
166-
Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
167-
exists(boolean eqpolarity |
168-
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
169-
(testIsTrue = true or testIsTrue = false) and
170-
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
171-
)
172-
or
173-
exists(boolean testIsTrue0 |
174-
implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
175-
)
176-
}
177-
178161
/**
179162
* Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
180163
*/

‎shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

+1-1
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ module ModulusAnalysis<
3434
or
3535
exists(Sem::Guard guard, boolean testIsTrue |
3636
hasReadOfVarInlineLate(pos, v) and
37-
guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
37+
guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
3838
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
3939
)
4040
}

‎shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

+4-8
Original file line numberDiff line numberDiff line change
@@ -304,10 +304,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
304304
}
305305

306306
signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
307-
Sem::Guard semEqFlowCond(
308-
Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
309-
);
310-
311307
predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, DeltaParam::Delta delta);
312308

313309
predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta);
@@ -447,7 +443,7 @@ module RangeStage<
447443
*/
448444
cached
449445
predicate possibleReason(Sem::Guard guard) {
450-
guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
446+
guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)
451447
}
452448
}
453449

@@ -609,7 +605,7 @@ module RangeStage<
609605
testIsTrue0)
610606
)
611607
or
612-
result = semEqFlowCond(v, e, delta, true, testIsTrue) and
608+
result = eqFlowCond(v, e, delta, true, testIsTrue) and
613609
(upper = true or upper = false)
614610
or
615611
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
@@ -630,7 +626,7 @@ module RangeStage<
630626
Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
631627
) {
632628
exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
633-
guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
629+
guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
634630
delta = D::toFloat(d2) - D::toFloat(d1) and
635631
guardEq.directlyControls(result, eqIsTrue)
636632
)
@@ -695,7 +691,7 @@ module RangeStage<
695691
getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
696692
exists(Sem::Guard guard, boolean testIsTrue |
697693
pos.hasReadOfVar(v) and
698-
guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
694+
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
699695
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
700696
reason = TSemCondReason(guard)
701697
)

‎shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

+20
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,26 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
3737
result.(CopyValueExpr).getOperand() = ssaRead(v, delta)
3838
}
3939

40+
/**
41+
* Gets a condition that tests whether `v` equals `e + delta`.
42+
*
43+
* If the condition evaluates to `testIsTrue`:
44+
* - `isEq = true` : `v == e + delta`
45+
* - `isEq = false` : `v != e + delta`
46+
*/
47+
pragma[nomagic]
48+
Guard eqFlowCond(SsaVariable v, Expr e, D::Delta delta, boolean isEq, boolean testIsTrue) {
49+
exists(boolean eqpolarity |
50+
result.isEquality(ssaRead(v, delta), e, eqpolarity) and
51+
(testIsTrue = true or testIsTrue = false) and
52+
eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
53+
)
54+
or
55+
exists(boolean testIsTrue0 |
56+
implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
57+
)
58+
}
59+
4060
private newtype TSsaReadPosition =
4161
TSsaReadPositionBlock(BasicBlock bb) {
4262
exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)

0 commit comments

Comments
 (0)