@@ -239,9 +239,10 @@ private class GuardConditionFromIR extends GuardCondition {
239239 * IRGuardConditions.
240240 */
241241class IRGuardCondition extends Instruction {
242-
242+ ConditionalBranchInstruction branch ;
243+
243244 IRGuardCondition ( ) {
244- is_condition ( this )
245+ branch = get_branch_for_condition ( this )
245246 }
246247
247248 /**
@@ -280,6 +281,16 @@ class IRGuardCondition extends Instruction {
280281 ne .controls ( controlled , testIsTrue .booleanNot ( ) ) )
281282 }
282283
284+ predicate controlsEdge ( IRBlock pred , IRBlock succ , boolean testIsTrue ) {
285+ pred .getASuccessor ( ) = succ and
286+ controls ( pred , testIsTrue )
287+ or
288+ hasBranchEdge ( succ , testIsTrue ) and
289+ branch .getCondition ( ) = this and
290+ branch .getBlock ( ) = pred
291+ }
292+
293+
283294 /**
284295 * Holds if `branch` jumps directly to `succ` when this condition is `testIsTrue`.
285296 *
@@ -295,7 +306,7 @@ class IRGuardCondition extends Instruction {
295306 * return x;
296307 * ```
297308 */
298- predicate hasBranchEdge ( ConditionalBranchInstruction branch , IRBlock succ , boolean testIsTrue ) {
309+ private predicate hasBranchEdge ( IRBlock succ , boolean testIsTrue ) {
299310 branch .getCondition ( ) = this and
300311 (
301312 testIsTrue = true and
@@ -319,6 +330,14 @@ class IRGuardCondition extends Instruction {
319330 )
320331 }
321332
333+ /** Holds if (determined by this guard) `left < right + k` must be `isLessThan` on the edge from
334+ * `pred` to `succ`. If `isLessThan = false` then this implies `left >= right + k`. */
335+ cached predicate ensuresLtEdge ( Operand left , Operand right , int k , IRBlock pred , IRBlock succ , boolean isLessThan ) {
336+ exists ( boolean testIsTrue |
337+ compares_lt ( this , left , right , k , isLessThan , testIsTrue ) and this .controlsEdge ( pred , succ , testIsTrue )
338+ )
339+ }
340+
322341 /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
323342 cached predicate comparesEq ( Operand left , Operand right , int k , boolean areEqual , boolean testIsTrue ) {
324343 compares_eq ( this , left , right , k , areEqual , testIsTrue )
@@ -331,6 +350,13 @@ class IRGuardCondition extends Instruction {
331350 compares_eq ( this , left , right , k , areEqual , testIsTrue ) and this .controls ( block , testIsTrue )
332351 )
333352 }
353+ /** Holds if (determined by this guard) `left == right + k` must be `areEqual` on the edge from
354+ * `pred` to `succ`. If `areEqual = false` then this implies `left != right + k`. */
355+ cached predicate ensuresEqEdge ( Operand left , Operand right , int k , IRBlock pred , IRBlock succ , boolean areEqual ) {
356+ exists ( boolean testIsTrue |
357+ compares_eq ( this , left , right , k , areEqual , testIsTrue ) and this .controlsEdge ( pred , succ , testIsTrue )
358+ )
359+ }
334360
335361 /**
336362 * Holds if this condition controls `block`, meaning that `block` is only
@@ -340,26 +366,26 @@ class IRGuardCondition extends Instruction {
340366 */
341367 private predicate controlsBlock ( IRBlock controlled , boolean testIsTrue ) {
342368 not isUnreachedBlock ( controlled ) and
343- exists ( IRBlock thisblock
344- | thisblock .getAnInstruction ( ) = this
345- | exists ( IRBlock succ , ConditionalBranchInstruction branch
369+ exists ( IRBlock branchBlock
370+ | branchBlock .getAnInstruction ( ) = branch
371+ | exists ( IRBlock succ
346372 | testIsTrue = true and succ .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
347373 or
348374 testIsTrue = false and succ .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
349375 | branch .getCondition ( ) = this and
350376 succ .dominates ( controlled ) and
351377 forall ( IRBlock pred
352378 | pred .getASuccessor ( ) = succ
353- | pred = thisblock or succ .dominates ( pred ) or not pred .isReachableFromFunctionEntry ( ) ) ) )
379+ | pred = branchBlock or succ .dominates ( pred ) or not pred .isReachableFromFunctionEntry ( ) ) ) )
354380 }
355381}
356382
357- private predicate is_condition ( Instruction guard ) {
383+ private ConditionalBranchInstruction get_branch_for_condition ( Instruction guard ) {
358384 exists ( ConditionalBranchInstruction branch |
359385 branch .getCondition ( ) = guard
360386 )
361387 or
362- exists ( LogicalNotInstruction cond | is_condition ( cond ) and cond .getUnary ( ) = guard )
388+ exists ( LogicalNotInstruction cond | result = get_branch_for_condition ( cond ) and cond .getUnary ( ) = guard )
363389}
364390
365391/**
0 commit comments