Skip to content

Commit a519eab

Browse files
aschackmullaschackmull
authored
Merge pull request #19571 from aschackmull/rangeanalysis/guards
Rangeanalysis: Simplify Guards integration.
2 parents fcfe0a2 + 5b21188 commit a519eab

File tree

14 files changed

+78
-136
lines changed

14 files changed

+78
-136
lines changed

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

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -264,10 +264,6 @@ module SemanticExprConfig {
264264

265265
Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }
266266

267-
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
268-
none() // TODO
269-
}
270-
271267
/** Gets the expression associated with `instr`. */
272268
SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
273269
}

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

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,11 @@ class SemGuard instanceof Specific::Guard {
1818
Specific::equalityGuard(this, e1, e2, polarity)
1919
}
2020

21-
final predicate directlyControls(SemBasicBlock controlled, boolean branch) {
21+
final predicate controls(SemBasicBlock controlled, boolean branch) {
2222
Specific::guardDirectlyControlsBlock(this, controlled, branch)
2323
}
2424

25-
final predicate hasBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {
25+
final predicate controlsBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {
2626
Specific::guardHasBranchEdge(this, bb1, bb2, branch)
2727
}
2828

@@ -31,8 +31,4 @@ class SemGuard instanceof Specific::Guard {
3131
final SemExpr asExpr() { result = Specific::getGuardAsExpr(this) }
3232
}
3333

34-
predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
35-
Specific::implies_v2(g1, b1, g2, b2)
36-
}
37-
3834
SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,6 @@ module Sem implements Semantic<SemLocation> {
7777

7878
class Guard = SemGuard;
7979

80-
predicate implies_v2 = semImplies_v2/4;
81-
8280
class Type = SemType;
8381

8482
class IntegerType = SemIntegerType;

‎csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
1717
exists(Guard guard, boolean testIsTrue |
1818
pos.hasReadOfVar(v) and
1919
guard = eqFlowCond(v, e, delta, true, testIsTrue) and
20-
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
20+
guardControlsSsaRead(guard, pos, testIsTrue)
2121
)
2222
}
2323

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -32,8 +32,6 @@ module Private {
3232

3333
class LeftShiftExpr = RU::ExprNode::LeftShiftExpr;
3434

35-
predicate guardDirectlyControlsSsaRead = RU::guardControlsSsaRead/3;
36-
3735
predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
3836

3937
predicate valueFlowStep = RU::valueFlowStep/3;

‎java/ql/lib/semmle/code/java/controlflow/Guards.qll

Lines changed: 34 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
145145
* Evaluating a switch case to true corresponds to taking that switch case, and
146146
* evaluating it to false corresponds to taking some other branch.
147147
*/
148-
class Guard extends ExprParent {
148+
final class Guard extends ExprParent {
149149
Guard() {
150150
this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
151151
or
@@ -360,6 +360,18 @@ private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean b
360360
)
361361
}
362362

363+
pragma[nomagic]
364+
private predicate guardControlsBranchEdge_v2(
365+
Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
366+
) {
367+
guard.hasBranchEdge(bb1, bb2, branch)
368+
or
369+
exists(Guard g, boolean b |
370+
guardControlsBranchEdge_v2(g, bb1, bb2, b) and
371+
implies_v2(g, b, guard, branch)
372+
)
373+
}
374+
363375
pragma[nomagic]
364376
private predicate guardControlsBranchEdge_v3(
365377
Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
@@ -372,6 +384,27 @@ private predicate guardControlsBranchEdge_v3(
372384
)
373385
}
374386

387+
/** INTERNAL: Use `Guard` instead. */
388+
final class Guard_v2 extends Guard {
389+
/**
390+
* Holds if this guard evaluating to `branch` controls the control-flow
391+
* branch edge from `bb1` to `bb2`. That is, following the edge from
392+
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
393+
*/
394+
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
395+
guardControlsBranchEdge_v2(this, bb1, bb2, branch)
396+
}
397+
398+
/**
399+
* Holds if this guard evaluating to `branch` directly or indirectly controls
400+
* the block `controlled`. That is, the evaluation of `controlled` is
401+
* dominated by this guard evaluating to `branch`.
402+
*/
403+
predicate controls(BasicBlock controlled, boolean branch) {
404+
guardControls_v2(this, controlled, branch)
405+
}
406+
}
407+
375408
private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
376409
exists(EqualityTest eqtest |
377410
eqtest = g and

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
1717
exists(Guard guard, boolean testIsTrue |
1818
pos.hasReadOfVar(v) and
1919
guard = eqFlowCond(v, e, delta, true, testIsTrue) and
20-
guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
20+
guardControlsSsaRead(guard, pos, testIsTrue)
2121
)
2222
}
2323

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

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -219,16 +219,10 @@ module Sem implements Semantic<Location> {
219219

220220
int getBlockId1(BasicBlock bb) { idOf(bb, result) }
221221

222-
final private class FinalGuard = GL::Guard;
223-
224-
class Guard extends FinalGuard {
222+
class Guard extends GL::Guard_v2 {
225223
Expr asExpr() { result = this }
226224
}
227225

228-
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
229-
GL::implies_v2(g1, b1, g2, b2)
230-
}
231-
232226
class Type = J::Type;
233227

234228
class IntegerType extends J::IntegralType {

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,6 @@ predicate ssaUpdateStep = U::ssaUpdateStep/3;
1919

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

22-
predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
23-
2422
predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
2523

2624
predicate eqFlowCond = U::eqFlowCond/5;

‎java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll

Lines changed: 7 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ module Private {
44
private import semmle.code.java.dataflow.RangeUtils as RU
55
private import semmle.code.java.controlflow.Guards as G
66
private import semmle.code.java.controlflow.BasicBlocks as BB
7-
private import semmle.code.java.controlflow.internal.GuardsLogic as GL
87
private import SsaReadPositionCommon
98

109
class BasicBlock = BB::BasicBlock;
@@ -15,7 +14,7 @@ module Private {
1514

1615
class Expr = J::Expr;
1716

18-
class Guard = G::Guard;
17+
class Guard = G::Guard_v2;
1918

2019
class ConstantIntegerExpr = RU::ConstantIntegerExpr;
2120

@@ -101,29 +100,17 @@ module Private {
101100
}
102101
}
103102

104-
/**
105-
* Holds if `guard` directly controls the position `controlled` with the
106-
* value `testIsTrue`.
107-
*/
108-
pragma[nomagic]
109-
predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
110-
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
111-
or
112-
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
113-
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
114-
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
115-
)
116-
}
117-
118103
/**
119104
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
120105
*/
121106
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
122-
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
107+
guard.controls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
123108
or
124-
exists(Guard guard0, boolean testIsTrue0 |
125-
GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
126-
guardControlsSsaRead(guard0, controlled, testIsTrue0)
109+
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
110+
guard.controls(controlledEdge.getOrigBlock(), testIsTrue) or
111+
guard
112+
.controlsBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(),
113+
testIsTrue)
127114
)
128115
}
129116

‎java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

Lines changed: 7 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,12 @@ module Private {
77
private import semmle.code.java.dataflow.SSA as Ssa
88
private import semmle.code.java.controlflow.Guards as G
99
private import SsaReadPositionCommon
10-
private import semmle.code.java.controlflow.internal.GuardsLogic as GL
1110
private import Sign
1211
import Impl
1312

1413
class ConstantIntegerExpr = RU::ConstantIntegerExpr;
1514

16-
class Guard = G::Guard;
15+
class Guard = G::Guard_v2;
1716

1817
class SsaVariable = Ssa::SsaVariable;
1918

@@ -170,31 +169,17 @@ module Private {
170169

171170
predicate ssaRead = RU::ssaRead/2;
172171

173-
/**
174-
* Holds if `guard` directly controls the position `controlled` with the
175-
* value `testIsTrue`.
176-
*/
177-
pragma[nomagic]
178-
private predicate guardDirectlyControlsSsaRead(
179-
Guard guard, SsaReadPosition controlled, boolean testIsTrue
180-
) {
181-
guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
182-
or
183-
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
184-
guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
185-
guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
186-
)
187-
}
188-
189172
/**
190173
* Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
191174
*/
192175
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
193-
guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
176+
guard.controls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
194177
or
195-
exists(Guard guard0, boolean testIsTrue0 |
196-
GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
197-
guardControlsSsaRead(guard0, controlled, testIsTrue0)
178+
exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
179+
guard.controls(controlledEdge.getOrigBlock(), testIsTrue) or
180+
guard
181+
.controlsBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(),
182+
testIsTrue)
198183
)
199184
}
200185
}

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

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

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

Lines changed: 18 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -181,21 +181,6 @@ signature module Semantic<LocationSig Location> {
181181
*/
182182
Expr asExpr();
183183

184-
/**
185-
* Holds if the guard directly controls a given basic block. For example in
186-
* the following code, the guard `(x > y)` directly controls the block
187-
* beneath it:
188-
* ```
189-
* if (x > y)
190-
* {
191-
* Console.WriteLine("x is greater than y");
192-
* }
193-
* ```
194-
* `branch` indicates whether the basic block is entered when the guard
195-
* evaluates to `true` or when it evaluates to `false`.
196-
*/
197-
predicate directlyControls(BasicBlock controlled, boolean branch);
198-
199184
/**
200185
* Holds if this guard is an equality test between `e1` and `e2`. If the
201186
* test is negated, that is `!=`, then `polarity` is false, otherwise
@@ -204,24 +189,19 @@ signature module Semantic<LocationSig Location> {
204189
predicate isEquality(Expr e1, Expr e2, boolean polarity);
205190

206191
/**
207-
* Holds if there is a branch edge between two basic blocks. For example
208-
* in the following C code, there are two branch edges from the basic block
209-
* containing the condition `(x > y)` to the beginnings of the true and
210-
* false blocks that follow:
211-
* ```
212-
* if (x > y) {
213-
* printf("x is greater than y\n");
214-
* } else {
215-
* printf("x is not greater than y\n");
216-
* }
217-
* ```
218-
* `branch` indicates whether the second basic block is the one entered
219-
* when the guard evaluates to `true` or when it evaluates to `false`.
192+
* Holds if this guard evaluating to `branch` controls the control-flow
193+
* branch edge from `bb1` to `bb2`. That is, following the edge from
194+
* `bb1` to `bb2` implies that this guard evaluated to `branch`.
220195
*/
221-
predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
222-
}
196+
predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
223197

224-
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2);
198+
/**
199+
* Holds if this guard evaluating to `branch` directly or indirectly controls
200+
* the block `controlled`. That is, the evaluation of `controlled` is
201+
* dominated by this guard evaluating to `branch`.
202+
*/
203+
predicate controls(BasicBlock controlled, boolean branch);
204+
}
225205

226206
class Type;
227207

@@ -670,19 +650,14 @@ module RangeStage<
670650
delta = D::fromFloat(D::toFloat(d1) + d2 + d3)
671651
)
672652
or
673-
exists(boolean testIsTrue0 |
674-
Sem::implies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0),
675-
testIsTrue0)
676-
)
677-
or
678653
result = eqFlowCond(v, e, delta, true, testIsTrue) and
679654
(upper = true or upper = false)
680655
or
681-
// guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
682-
// exists a guard `guardEq` such that `v = v2 - d1 + d2`.
656+
// guard that tests whether `v2` is bounded by `e + delta - d` and
657+
// exists a guard `guardEq` such that `v = v2 + d`.
683658
exists(Sem::SsaVariable v2, D::Delta oldDelta, float d |
684659
// equality needs to control guard
685-
result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
660+
result.getBasicBlock() = eqSsaCondControls(v, v2, d) and
686661
result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
687662
delta = D::fromFloat(D::toFloat(oldDelta) + d)
688663
)
@@ -692,13 +667,11 @@ module RangeStage<
692667
* Gets a basic block in which `v1` equals `v2 + delta`.
693668
*/
694669
pragma[nomagic]
695-
private Sem::BasicBlock eqSsaCondDirectlyControls(
696-
Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
697-
) {
670+
private Sem::BasicBlock eqSsaCondControls(Sem::SsaVariable v1, Sem::SsaVariable v2, float delta) {
698671
exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
699672
guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
700673
delta = D::toFloat(d2) - D::toFloat(d1) and
701-
guardEq.directlyControls(result, eqIsTrue)
674+
guardEq.controls(result, eqIsTrue)
702675
)
703676
}
704677

@@ -749,7 +722,7 @@ module RangeStage<
749722
exists(Sem::Guard guard, boolean testIsTrue |
750723
pos.hasReadOfVar(v) and
751724
guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
752-
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
725+
guardControlsSsaRead(guard, pos, testIsTrue) and
753726
reason = TSemCondReason(guard)
754727
)
755728
}
@@ -762,7 +735,7 @@ module RangeStage<
762735
exists(Sem::Guard guard, boolean testIsTrue |
763736
pos.hasReadOfVar(v) and
764737
guard = eqFlowCond(v, e, delta, false, testIsTrue) and
765-
guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
738+
guardControlsSsaRead(guard, pos, testIsTrue) and
766739
reason = TSemCondReason(guard)
767740
)
768741
}

0 commit comments

Comments
 (0)