@@ -281,6 +281,16 @@ class IRGuardCondition extends Instruction {
281281 ne .controls ( controlled , testIsTrue .booleanNot ( ) ) )
282282 }
283283
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+
284294 /**
285295 * Holds if `branch` jumps directly to `succ` when this condition is `testIsTrue`.
286296 *
@@ -296,7 +306,8 @@ class IRGuardCondition extends Instruction {
296306 * return x;
297307 * ```
298308 */
299- predicate hasBranchEdge ( IRBlock succ , boolean testIsTrue ) {
309+ private predicate hasBranchEdge ( IRBlock succ , boolean testIsTrue ) {
310+ branch .getCondition ( ) = this and
300311 (
301312 testIsTrue = true and
302313 succ .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
@@ -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
0 commit comments