@@ -20,6 +20,44 @@ private predicate isUnreachedBlock(IRBlock block) {
20
20
block .getFirstInstruction ( ) instanceof UnreachedInstruction
21
21
}
22
22
23
+ private newtype TAbstractValue =
24
+ TBooleanValue ( boolean b ) { b = true or b = false } or
25
+ TMatchValue ( CaseEdge c )
26
+
27
+ /**
28
+ * An abstract value. This is either a boolean value, or a `switch` case.
29
+ */
30
+ abstract class AbstractValue extends TAbstractValue {
31
+ /** Gets an abstract value that represents the dual of this value, if any. */
32
+ abstract AbstractValue getDualValue ( ) ;
33
+
34
+ /** Gets a textual representation of this abstract value. */
35
+ abstract string toString ( ) ;
36
+ }
37
+
38
+ /** A Boolean value. */
39
+ class BooleanValue extends AbstractValue , TBooleanValue {
40
+ /** Gets the underlying Boolean value. */
41
+ boolean getValue ( ) { this = TBooleanValue ( result ) }
42
+
43
+ override BooleanValue getDualValue ( ) { result .getValue ( ) = this .getValue ( ) .booleanNot ( ) }
44
+
45
+ override string toString ( ) { result = this .getValue ( ) .toString ( ) }
46
+ }
47
+
48
+ /** A value that represents a match against a specific `switch` case. */
49
+ class MatchValue extends AbstractValue , TMatchValue {
50
+ /** Gets the case. */
51
+ CaseEdge getCase ( ) { this = TMatchValue ( result ) }
52
+
53
+ override MatchValue getDualValue ( ) {
54
+ // A `MatchValue` has no dual.
55
+ none ( )
56
+ }
57
+
58
+ override string toString ( ) { result = this .getCase ( ) .toString ( ) }
59
+ }
60
+
23
61
/**
24
62
* A Boolean condition in the AST that guards one or more basic blocks. This includes
25
63
* operands of logical operators but not switch statements.
@@ -34,6 +72,15 @@ class GuardCondition extends Expr {
34
72
this .( BinaryLogicalOperation ) .getAnOperand ( ) instanceof GuardCondition
35
73
}
36
74
75
+ /**
76
+ * Holds if this condition controls `controlled`, meaning that `controlled` is only
77
+ * entered if the value of this condition is `v`.
78
+ *
79
+ * For details on what "controls" mean, see the QLDoc for `controls`.
80
+ */
81
+ cached
82
+ predicate valueControls ( BasicBlock controlled , AbstractValue v ) { none ( ) }
83
+
37
84
/**
38
85
* Holds if this condition controls `controlled`, meaning that `controlled` is only
39
86
* entered if the value of this condition is `testIsTrue`.
@@ -61,7 +108,9 @@ class GuardCondition extends Expr {
61
108
* true (for `&&`) or false (for `||`) branch.
62
109
*/
63
110
cached
64
- predicate controls ( BasicBlock controlled , boolean testIsTrue ) { none ( ) }
111
+ final predicate controls ( BasicBlock controlled , boolean testIsTrue ) {
112
+ this .valueControls ( controlled , any ( BooleanValue bv | bv .getValue ( ) = testIsTrue ) )
113
+ }
65
114
66
115
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
67
116
cached
@@ -98,13 +147,13 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
98
147
this .( BinaryLogicalOperation ) .getAnOperand ( ) instanceof GuardCondition
99
148
}
100
149
101
- override predicate controls ( BasicBlock controlled , boolean testIsTrue ) {
150
+ override predicate valueControls ( BasicBlock controlled , AbstractValue v ) {
102
151
exists ( BinaryLogicalOperation binop , GuardCondition lhs , GuardCondition rhs |
103
152
this = binop and
104
153
lhs = binop .getLeftOperand ( ) and
105
154
rhs = binop .getRightOperand ( ) and
106
- lhs .controls ( controlled , testIsTrue ) and
107
- rhs .controls ( controlled , testIsTrue )
155
+ lhs .valueControls ( controlled , v ) and
156
+ rhs .valueControls ( controlled , v )
108
157
)
109
158
}
110
159
@@ -146,10 +195,10 @@ private class GuardConditionFromIR extends GuardCondition {
146
195
147
196
GuardConditionFromIR ( ) { this = ir .getUnconvertedResultExpression ( ) }
148
197
149
- override predicate controls ( BasicBlock controlled , boolean testIsTrue ) {
198
+ override predicate valueControls ( BasicBlock controlled , AbstractValue v ) {
150
199
// This condition must determine the flow of control; that is, this
151
200
// node must be a top-level condition.
152
- this .controlsBlock ( controlled , testIsTrue )
201
+ this .controlsBlock ( controlled , v )
153
202
}
154
203
155
204
/** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
@@ -198,13 +247,13 @@ private class GuardConditionFromIR extends GuardCondition {
198
247
199
248
/**
200
249
* Holds if this condition controls `block`, meaning that `block` is only
201
- * entered if the value of this condition is `testIsTrue `. This helper
250
+ * entered if the value of this condition is `v `. This helper
202
251
* predicate does not necessarily hold for binary logical operations like
203
252
* `&&` and `||`. See the detailed explanation on predicate `controls`.
204
253
*/
205
- private predicate controlsBlock ( BasicBlock controlled , boolean testIsTrue ) {
254
+ private predicate controlsBlock ( BasicBlock controlled , AbstractValue v ) {
206
255
exists ( IRBlock irb |
207
- ir .controls ( irb , testIsTrue ) and
256
+ ir .valueControls ( irb , v ) and
208
257
nonExcludedIRAndBasicBlock ( irb , controlled ) and
209
258
not isUnreachedBlock ( irb )
210
259
)
@@ -249,10 +298,28 @@ private predicate nonExcludedIRAndBasicBlock(IRBlock irb, BasicBlock controlled)
249
298
*/
250
299
cached
251
300
class IRGuardCondition extends Instruction {
252
- ConditionalBranchInstruction branch ;
301
+ Instruction branch ;
253
302
254
303
cached
255
- IRGuardCondition ( ) { branch = get_branch_for_condition ( this ) }
304
+ IRGuardCondition ( ) { branch = getBranchForCondition ( this ) }
305
+
306
+ /**
307
+ * Holds if this condition controls `controlled`, meaning that `controlled` is only
308
+ * entered if the value of this condition is `v`.
309
+ *
310
+ * For details on what "controls" mean, see the QLDoc for `controls`.
311
+ */
312
+ cached
313
+ predicate valueControls ( IRBlock controlled , AbstractValue v ) {
314
+ // This condition must determine the flow of control; that is, this
315
+ // node must be a top-level condition.
316
+ this .controlsBlock ( controlled , v )
317
+ or
318
+ exists ( IRGuardCondition ne |
319
+ this = ne .( LogicalNotInstruction ) .getUnary ( ) and
320
+ ne .valueControls ( controlled , v .getDualValue ( ) )
321
+ )
322
+ }
256
323
257
324
/**
258
325
* Holds if this condition controls `controlled`, meaning that `controlled` is only
@@ -282,13 +349,25 @@ class IRGuardCondition extends Instruction {
282
349
*/
283
350
cached
284
351
predicate controls ( IRBlock controlled , boolean testIsTrue ) {
285
- // This condition must determine the flow of control; that is, this
286
- // node must be a top-level condition.
287
- this .controlsBlock ( controlled , testIsTrue )
352
+ this .valueControls ( controlled , any ( BooleanValue bv | bv .getValue ( ) = testIsTrue ) )
353
+ }
354
+
355
+ /**
356
+ * Holds if the control-flow edge `(pred, succ)` may be taken only if
357
+ * the value of this condition is `v`.
358
+ */
359
+ cached
360
+ predicate valueControlsEdge ( IRBlock pred , IRBlock succ , AbstractValue v ) {
361
+ pred .getASuccessor ( ) = succ and
362
+ this .valueControls ( pred , v )
288
363
or
289
- exists ( IRGuardCondition ne |
290
- this = ne .( LogicalNotInstruction ) .getUnary ( ) and
291
- ne .controls ( controlled , testIsTrue .booleanNot ( ) )
364
+ succ = this .getBranchSuccessor ( v ) and
365
+ (
366
+ branch .( ConditionalBranchInstruction ) .getCondition ( ) = this and
367
+ branch .getBlock ( ) = pred
368
+ or
369
+ branch .( SwitchInstruction ) .getExpression ( ) = this and
370
+ branch .getBlock ( ) = pred
292
371
)
293
372
}
294
373
@@ -297,17 +376,12 @@ class IRGuardCondition extends Instruction {
297
376
* the value of this condition is `testIsTrue`.
298
377
*/
299
378
cached
300
- predicate controlsEdge ( IRBlock pred , IRBlock succ , boolean testIsTrue ) {
301
- pred .getASuccessor ( ) = succ and
302
- this .controls ( pred , testIsTrue )
303
- or
304
- succ = this .getBranchSuccessor ( testIsTrue ) and
305
- branch .getCondition ( ) = this and
306
- branch .getBlock ( ) = pred
379
+ final predicate controlsEdge ( IRBlock pred , IRBlock succ , boolean testIsTrue ) {
380
+ this .valueControlsEdge ( pred , succ , any ( BooleanValue bv | bv .getValue ( ) = testIsTrue ) )
307
381
}
308
382
309
383
/**
310
- * Gets the block to which `branch` jumps directly when this condition is `testIsTrue `.
384
+ * Gets the block to which `branch` jumps directly when the value of this condition is `v `.
311
385
*
312
386
* This predicate is intended to help with situations in which an inference can only be made
313
387
* based on an edge between a block with multiple successors and a block with multiple
@@ -321,14 +395,20 @@ class IRGuardCondition extends Instruction {
321
395
* return x;
322
396
* ```
323
397
*/
324
- private IRBlock getBranchSuccessor ( boolean testIsTrue ) {
325
- branch .getCondition ( ) = this and
326
- (
327
- testIsTrue = true and
328
- result .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
398
+ private IRBlock getBranchSuccessor ( AbstractValue v ) {
399
+ branch .( ConditionalBranchInstruction ) . getCondition ( ) = this and
400
+ exists ( BooleanValue bv | bv = v |
401
+ bv . getValue ( ) = true and
402
+ result .getFirstInstruction ( ) = branch .( ConditionalBranchInstruction ) . getTrueSuccessor ( )
329
403
or
330
- testIsTrue = false and
331
- result .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
404
+ bv .getValue ( ) = false and
405
+ result .getFirstInstruction ( ) = branch .( ConditionalBranchInstruction ) .getFalseSuccessor ( )
406
+ )
407
+ or
408
+ exists ( SwitchInstruction switch , CaseEdge kind | switch = branch |
409
+ switch .getExpression ( ) = this and
410
+ result .getFirstInstruction ( ) = switch .getSuccessor ( kind ) and
411
+ kind = v .( MatchValue ) .getCase ( )
332
412
)
333
413
}
334
414
@@ -396,11 +476,11 @@ class IRGuardCondition extends Instruction {
396
476
397
477
/**
398
478
* Holds if this condition controls `block`, meaning that `block` is only
399
- * entered if the value of this condition is `testIsTrue `. This helper
479
+ * entered if the value of this condition is `v `. This helper
400
480
* predicate does not necessarily hold for binary logical operations like
401
481
* `&&` and `||`. See the detailed explanation on predicate `controls`.
402
482
*/
403
- private predicate controlsBlock ( IRBlock controlled , boolean testIsTrue ) {
483
+ private predicate controlsBlock ( IRBlock controlled , AbstractValue v ) {
404
484
not isUnreachedBlock ( controlled ) and
405
485
//
406
486
// For this block to control the block `controlled` with `testIsTrue` the
@@ -441,7 +521,7 @@ class IRGuardCondition extends Instruction {
441
521
// that `this` strictly dominates `controlled` so that isn't necessary to check
442
522
// directly.
443
523
exists ( IRBlock succ |
444
- succ = this .getBranchSuccessor ( testIsTrue ) and
524
+ succ = this .getBranchSuccessor ( v ) and
445
525
this .hasDominatingEdgeTo ( succ ) and
446
526
succ .dominates ( controlled )
447
527
)
@@ -476,12 +556,14 @@ class IRGuardCondition extends Instruction {
476
556
private IRBlock getBranchBlock ( ) { result = branch .getBlock ( ) }
477
557
}
478
558
479
- private ConditionalBranchInstruction get_branch_for_condition ( Instruction guard ) {
480
- result .getCondition ( ) = guard
559
+ private Instruction getBranchForCondition ( Instruction guard ) {
560
+ result .( ConditionalBranchInstruction ) . getCondition ( ) = guard
481
561
or
482
562
exists ( LogicalNotInstruction cond |
483
- result = get_branch_for_condition ( cond ) and cond .getUnary ( ) = guard
563
+ result = getBranchForCondition ( cond ) and cond .getUnary ( ) = guard
484
564
)
565
+ or
566
+ result .( SwitchInstruction ) .getExpression ( ) = guard
485
567
}
486
568
487
569
/**
0 commit comments