@@ -20,6 +20,44 @@ private predicate isUnreachedBlock(IRBlock block) {
2020 block .getFirstInstruction ( ) instanceof UnreachedInstruction
2121}
2222
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+
2361/**
2462 * A Boolean condition in the AST that guards one or more basic blocks. This includes
2563 * operands of logical operators but not switch statements.
@@ -34,6 +72,15 @@ class GuardCondition extends Expr {
3472 this .( BinaryLogicalOperation ) .getAnOperand ( ) instanceof GuardCondition
3573 }
3674
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+
3784 /**
3885 * Holds if this condition controls `controlled`, meaning that `controlled` is only
3986 * entered if the value of this condition is `testIsTrue`.
@@ -61,7 +108,9 @@ class GuardCondition extends Expr {
61108 * true (for `&&`) or false (for `||`) branch.
62109 */
63110 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+ }
65114
66115 /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
67116 cached
@@ -98,13 +147,13 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardCondition {
98147 this .( BinaryLogicalOperation ) .getAnOperand ( ) instanceof GuardCondition
99148 }
100149
101- override predicate controls ( BasicBlock controlled , boolean testIsTrue ) {
150+ override predicate valueControls ( BasicBlock controlled , AbstractValue v ) {
102151 exists ( BinaryLogicalOperation binop , GuardCondition lhs , GuardCondition rhs |
103152 this = binop and
104153 lhs = binop .getLeftOperand ( ) and
105154 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 )
108157 )
109158 }
110159
@@ -146,10 +195,10 @@ private class GuardConditionFromIR extends GuardCondition {
146195
147196 GuardConditionFromIR ( ) { this = ir .getUnconvertedResultExpression ( ) }
148197
149- override predicate controls ( BasicBlock controlled , boolean testIsTrue ) {
198+ override predicate valueControls ( BasicBlock controlled , AbstractValue v ) {
150199 // This condition must determine the flow of control; that is, this
151200 // node must be a top-level condition.
152- this .controlsBlock ( controlled , testIsTrue )
201+ this .controlsBlock ( controlled , v )
153202 }
154203
155204 /** 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 {
198247
199248 /**
200249 * 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
202251 * predicate does not necessarily hold for binary logical operations like
203252 * `&&` and `||`. See the detailed explanation on predicate `controls`.
204253 */
205- private predicate controlsBlock ( BasicBlock controlled , boolean testIsTrue ) {
254+ private predicate controlsBlock ( BasicBlock controlled , AbstractValue v ) {
206255 exists ( IRBlock irb |
207- ir .controls ( irb , testIsTrue ) and
256+ ir .valueControls ( irb , v ) and
208257 nonExcludedIRAndBasicBlock ( irb , controlled ) and
209258 not isUnreachedBlock ( irb )
210259 )
@@ -249,10 +298,28 @@ private predicate nonExcludedIRAndBasicBlock(IRBlock irb, BasicBlock controlled)
249298 */
250299cached
251300class IRGuardCondition extends Instruction {
252- ConditionalBranchInstruction branch ;
301+ Instruction branch ;
253302
254303 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+ }
256323
257324 /**
258325 * Holds if this condition controls `controlled`, meaning that `controlled` is only
@@ -282,13 +349,25 @@ class IRGuardCondition extends Instruction {
282349 */
283350 cached
284351 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 )
288363 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
292371 )
293372 }
294373
@@ -297,17 +376,12 @@ class IRGuardCondition extends Instruction {
297376 * the value of this condition is `testIsTrue`.
298377 */
299378 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 ) )
307381 }
308382
309383 /**
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 `.
311385 *
312386 * This predicate is intended to help with situations in which an inference can only be made
313387 * based on an edge between a block with multiple successors and a block with multiple
@@ -321,14 +395,20 @@ class IRGuardCondition extends Instruction {
321395 * return x;
322396 * ```
323397 */
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 ( )
329403 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 ( )
332412 )
333413 }
334414
@@ -396,11 +476,11 @@ class IRGuardCondition extends Instruction {
396476
397477 /**
398478 * 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
400480 * predicate does not necessarily hold for binary logical operations like
401481 * `&&` and `||`. See the detailed explanation on predicate `controls`.
402482 */
403- private predicate controlsBlock ( IRBlock controlled , boolean testIsTrue ) {
483+ private predicate controlsBlock ( IRBlock controlled , AbstractValue v ) {
404484 not isUnreachedBlock ( controlled ) and
405485 //
406486 // For this block to control the block `controlled` with `testIsTrue` the
@@ -441,7 +521,7 @@ class IRGuardCondition extends Instruction {
441521 // that `this` strictly dominates `controlled` so that isn't necessary to check
442522 // directly.
443523 exists ( IRBlock succ |
444- succ = this .getBranchSuccessor ( testIsTrue ) and
524+ succ = this .getBranchSuccessor ( v ) and
445525 this .hasDominatingEdgeTo ( succ ) and
446526 succ .dominates ( controlled )
447527 )
@@ -476,12 +556,14 @@ class IRGuardCondition extends Instruction {
476556 private IRBlock getBranchBlock ( ) { result = branch .getBlock ( ) }
477557}
478558
479- private ConditionalBranchInstruction get_branch_for_condition ( Instruction guard ) {
480- result .getCondition ( ) = guard
559+ private Instruction getBranchForCondition ( Instruction guard ) {
560+ result .( ConditionalBranchInstruction ) . getCondition ( ) = guard
481561 or
482562 exists ( LogicalNotInstruction cond |
483- result = get_branch_for_condition ( cond ) and cond .getUnary ( ) = guard
563+ result = getBranchForCondition ( cond ) and cond .getUnary ( ) = guard
484564 )
565+ or
566+ result .( SwitchInstruction ) .getExpression ( ) = guard
485567}
486568
487569/**
0 commit comments