@@ -171,7 +171,7 @@ private class GuardConditionFromIR extends GuardCondition {
171171 exists ( Instruction li , Instruction ri |
172172 li .getUnconvertedResultExpression ( ) = left and
173173 ri .getUnconvertedResultExpression ( ) = right and
174- ir .comparesLt ( li , ri , k , isLessThan , testIsTrue )
174+ ir .comparesLt ( li . getAUse ( ) , ri . getAUse ( ) , k , isLessThan , testIsTrue )
175175 )
176176 }
177177
@@ -181,7 +181,7 @@ private class GuardConditionFromIR extends GuardCondition {
181181 exists ( Instruction li , Instruction ri , boolean testIsTrue |
182182 li .getUnconvertedResultExpression ( ) = left and
183183 ri .getUnconvertedResultExpression ( ) = right and
184- ir .comparesLt ( li , ri , k , isLessThan , testIsTrue ) and
184+ ir .comparesLt ( li . getAUse ( ) , ri . getAUse ( ) , k , isLessThan , testIsTrue ) and
185185 this .controls ( block , testIsTrue )
186186 )
187187 }
@@ -191,7 +191,7 @@ private class GuardConditionFromIR extends GuardCondition {
191191 exists ( Instruction li , Instruction ri |
192192 li .getUnconvertedResultExpression ( ) = left and
193193 ri .getUnconvertedResultExpression ( ) = right and
194- ir .comparesEq ( li , ri , k , areEqual , testIsTrue )
194+ ir .comparesEq ( li . getAUse ( ) , ri . getAUse ( ) , k , areEqual , testIsTrue )
195195 )
196196 }
197197
@@ -201,8 +201,8 @@ private class GuardConditionFromIR extends GuardCondition {
201201 exists ( Instruction li , Instruction ri , boolean testIsTrue |
202202 li .getUnconvertedResultExpression ( ) = left and
203203 ri .getUnconvertedResultExpression ( ) = right and
204- ir .comparesEq ( li , ri , k , areEqual , testIsTrue )
205- and this .controls ( block , testIsTrue )
204+ ir .comparesEq ( li . getAUse ( ) , ri . getAUse ( ) , k , areEqual , testIsTrue ) and
205+ this .controls ( block , testIsTrue )
206206 )
207207 }
208208
@@ -269,26 +269,26 @@ class IRGuardCondition extends Instruction {
269269 }
270270
271271 /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
272- cached predicate comparesLt ( Instruction left , Instruction right , int k , boolean isLessThan , boolean testIsTrue ) {
272+ cached predicate comparesLt ( Operand left , Operand right , int k , boolean isLessThan , boolean testIsTrue ) {
273273 compares_lt ( this , left , right , k , isLessThan , testIsTrue )
274274 }
275275
276276 /** Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
277277 If `isLessThan = false` then this implies `left >= right + k`. */
278- cached predicate ensuresLt ( Instruction left , Instruction right , int k , IRBlock block , boolean isLessThan ) {
278+ cached predicate ensuresLt ( Operand left , Operand right , int k , IRBlock block , boolean isLessThan ) {
279279 exists ( boolean testIsTrue |
280280 compares_lt ( this , left , right , k , isLessThan , testIsTrue ) and this .controls ( block , testIsTrue )
281281 )
282282 }
283283
284284 /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
285- cached predicate comparesEq ( Instruction left , Instruction right , int k , boolean areEqual , boolean testIsTrue ) {
285+ cached predicate comparesEq ( Operand left , Operand right , int k , boolean areEqual , boolean testIsTrue ) {
286286 compares_eq ( this , left , right , k , areEqual , testIsTrue )
287287 }
288288
289289 /** Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
290290 If `areEqual = false` then this implies `left != right + k`. */
291- cached predicate ensuresEq ( Instruction left , Instruction right , int k , IRBlock block , boolean areEqual ) {
291+ cached predicate ensuresEq ( Operand left , Operand right , int k , IRBlock block , boolean areEqual ) {
292292 exists ( boolean testIsTrue |
293293 compares_eq ( this , left , right , k , areEqual , testIsTrue ) and this .controls ( block , testIsTrue )
294294 )
@@ -328,7 +328,7 @@ private predicate is_condition(Instruction guard) {
328328 *
329329 * Beware making mistaken logical implications here relating `areEqual` and `testIsTrue`.
330330 */
331- private predicate compares_eq ( Instruction test , Instruction left , Instruction right , int k , boolean areEqual , boolean testIsTrue ) {
331+ private predicate compares_eq ( Instruction test , Operand left , Operand right , int k , boolean areEqual , boolean testIsTrue ) {
332332 /* The simple case where the test *is* the comparison so areEqual = testIsTrue xor eq. */
333333 exists ( boolean eq | simple_comparison_eq ( test , left , right , k , eq ) |
334334 areEqual = true and testIsTrue = eq or areEqual = false and testIsTrue = eq .booleanNot ( )
@@ -349,13 +349,13 @@ private predicate compares_eq(Instruction test, Instruction left, Instruction ri
349349}
350350
351351/** Rearrange various simple comparisons into `left == right + k` form. */
352- private predicate simple_comparison_eq ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean areEqual ) {
353- left = cmp .getLeftOperand ( ) and cmp instanceof CompareEQInstruction and right = cmp .getRightOperand ( ) and k = 0 and areEqual = true
352+ private predicate simple_comparison_eq ( CompareInstruction cmp , Operand left , Operand right , int k , boolean areEqual ) {
353+ left = cmp .getAnOperand ( ) . ( LeftOperand ) and cmp instanceof CompareEQInstruction and right = cmp .getAnOperand ( ) . ( RightOperand ) and k = 0 and areEqual = true
354354 or
355- left = cmp .getLeftOperand ( ) and cmp instanceof CompareNEInstruction and right = cmp .getRightOperand ( ) and k = 0 and areEqual = false
355+ left = cmp .getAnOperand ( ) . ( LeftOperand ) and cmp instanceof CompareNEInstruction and right = cmp .getAnOperand ( ) . ( RightOperand ) and k = 0 and areEqual = false
356356}
357357
358- private predicate complex_eq ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean areEqual , boolean testIsTrue ) {
358+ private predicate complex_eq ( CompareInstruction cmp , Operand left , Operand right , int k , boolean areEqual , boolean testIsTrue ) {
359359 sub_eq ( cmp , left , right , k , areEqual , testIsTrue )
360360 or
361361 add_eq ( cmp , left , right , k , areEqual , testIsTrue )
@@ -367,7 +367,7 @@ private predicate complex_eq(CompareInstruction cmp, Instruction left, Instructi
367367 */
368368
369369/** Holds if `left < right + k` evaluates to `isLt` given that test is `testIsTrue`. */
370- private predicate compares_lt ( Instruction test , Instruction left , Instruction right , int k , boolean isLt , boolean testIsTrue ) {
370+ private predicate compares_lt ( Instruction test , Operand left , Operand right , int k , boolean isLt , boolean testIsTrue ) {
371371 /* In the simple case, the test is the comparison, so isLt = testIsTrue */
372372 simple_comparison_lt ( test , left , right , k ) and isLt = true and testIsTrue = true
373373 or
@@ -387,22 +387,22 @@ private predicate compares_lt(Instruction test, Instruction left, Instruction ri
387387}
388388
389389/** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
390- private predicate compares_ge ( Instruction test , Instruction left , Instruction right , int k , boolean isGe , boolean testIsTrue ) {
390+ private predicate compares_ge ( Instruction test , Operand left , Operand right , int k , boolean isGe , boolean testIsTrue ) {
391391 exists ( int onemk | k = 1 - onemk | compares_lt ( test , right , left , onemk , isGe , testIsTrue ) )
392392}
393393
394394/** Rearrange various simple comparisons into `left < right + k` form. */
395- private predicate simple_comparison_lt ( CompareInstruction cmp , Instruction left , Instruction right , int k ) {
396- left = cmp .getLeftOperand ( ) and cmp instanceof CompareLTInstruction and right = cmp .getRightOperand ( ) and k = 0
395+ private predicate simple_comparison_lt ( CompareInstruction cmp , Operand left , Operand right , int k ) {
396+ left = cmp .getAnOperand ( ) . ( LeftOperand ) and cmp instanceof CompareLTInstruction and right = cmp .getAnOperand ( ) . ( RightOperand ) and k = 0
397397 or
398- left = cmp .getLeftOperand ( ) and cmp instanceof CompareLEInstruction and right = cmp .getRightOperand ( ) and k = 1
398+ left = cmp .getAnOperand ( ) . ( LeftOperand ) and cmp instanceof CompareLEInstruction and right = cmp .getAnOperand ( ) . ( RightOperand ) and k = 1
399399 or
400- right = cmp .getLeftOperand ( ) and cmp instanceof CompareGTInstruction and left = cmp .getRightOperand ( ) and k = 0
400+ right = cmp .getAnOperand ( ) . ( LeftOperand ) and cmp instanceof CompareGTInstruction and left = cmp .getAnOperand ( ) . ( RightOperand ) and k = 0
401401 or
402- right = cmp .getLeftOperand ( ) and cmp instanceof CompareGEInstruction and left = cmp .getRightOperand ( ) and k = 1
402+ right = cmp .getAnOperand ( ) . ( LeftOperand ) and cmp instanceof CompareGEInstruction and left = cmp .getAnOperand ( ) . ( RightOperand ) and k = 1
403403}
404404
405- private predicate complex_lt ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean isLt , boolean testIsTrue ) {
405+ private predicate complex_lt ( CompareInstruction cmp , Operand left , Operand right , int k , boolean isLt , boolean testIsTrue ) {
406406 sub_lt ( cmp , left , right , k , isLt , testIsTrue )
407407 or
408408 add_lt ( cmp , left , right , k , isLt , testIsTrue )
@@ -411,33 +411,33 @@ private predicate complex_lt(CompareInstruction cmp, Instruction left, Instructi
411411
412412/* left - x < right + c => left < right + (c+x)
413413 left < (right - x) + c => left < right + (c-x) */
414- private predicate sub_lt ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean isLt , boolean testIsTrue ) {
415- exists ( SubInstruction lhs , int c , int x | compares_lt ( cmp , lhs , right , c , isLt , testIsTrue ) and
416- left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRightOperand ( ) )
414+ private predicate sub_lt ( CompareInstruction cmp , Operand left , Operand right , int k , boolean isLt , boolean testIsTrue ) {
415+ exists ( SubInstruction lhs , int c , int x | compares_lt ( cmp , lhs . getAUse ( ) , right , c , isLt , testIsTrue ) and
416+ left = lhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( lhs .getRightOperand ( ) )
417417 and k = c + x
418418 )
419419 or
420- exists ( SubInstruction rhs , int c , int x | compares_lt ( cmp , left , rhs , c , isLt , testIsTrue ) and
421- right = rhs .getLeftOperand ( ) and x = int_value ( rhs .getRightOperand ( ) )
420+ exists ( SubInstruction rhs , int c , int x | compares_lt ( cmp , left , rhs . getAUse ( ) , c , isLt , testIsTrue ) and
421+ right = rhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( rhs .getRightOperand ( ) )
422422 and k = c - x
423423 )
424424}
425425
426426/* left + x < right + c => left < right + (c-x)
427427 left < (right + x) + c => left < right + (c+x) */
428- private predicate add_lt ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean isLt , boolean testIsTrue ) {
429- exists ( AddInstruction lhs , int c , int x | compares_lt ( cmp , lhs , right , c , isLt , testIsTrue ) and
430- ( left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRightOperand ( ) )
428+ private predicate add_lt ( CompareInstruction cmp , Operand left , Operand right , int k , boolean isLt , boolean testIsTrue ) {
429+ exists ( AddInstruction lhs , int c , int x | compares_lt ( cmp , lhs . getAUse ( ) , right , c , isLt , testIsTrue ) and
430+ ( left = lhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( lhs .getRightOperand ( ) )
431431 or
432- left = lhs .getRightOperand ( ) and x = int_value ( lhs .getLeftOperand ( ) )
432+ left = lhs .getAnOperand ( ) . ( RightOperand ) and x = int_value ( lhs .getLeftOperand ( ) )
433433 )
434434 and k = c - x
435435 )
436436 or
437- exists ( AddInstruction rhs , int c , int x | compares_lt ( cmp , left , rhs , c , isLt , testIsTrue ) and
438- ( right = rhs .getLeftOperand ( ) and x = int_value ( rhs .getRightOperand ( ) )
437+ exists ( AddInstruction rhs , int c , int x | compares_lt ( cmp , left , rhs . getAUse ( ) , c , isLt , testIsTrue ) and
438+ ( right = rhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( rhs .getRightOperand ( ) )
439439 or
440- right = rhs .getRightOperand ( ) and x = int_value ( rhs .getLeftOperand ( ) )
440+ right = rhs .getAnOperand ( ) . ( RightOperand ) and x = int_value ( rhs .getLeftOperand ( ) )
441441 )
442442 and k = c + x
443443 )
@@ -446,34 +446,34 @@ private predicate add_lt(CompareInstruction cmp, Instruction left, Instruction r
446446
447447/* left - x == right + c => left == right + (c+x)
448448 left == (right - x) + c => left == right + (c-x) */
449- private predicate sub_eq ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean areEqual , boolean testIsTrue ) {
450- exists ( SubInstruction lhs , int c , int x | compares_eq ( cmp , lhs , right , c , areEqual , testIsTrue ) and
451- left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRightOperand ( ) )
449+ private predicate sub_eq ( CompareInstruction cmp , Operand left , Operand right , int k , boolean areEqual , boolean testIsTrue ) {
450+ exists ( SubInstruction lhs , int c , int x | compares_eq ( cmp , lhs . getAUse ( ) , right , c , areEqual , testIsTrue ) and
451+ left = lhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( lhs .getRightOperand ( ) )
452452 and k = c + x
453453 )
454454 or
455- exists ( SubInstruction rhs , int c , int x | compares_eq ( cmp , left , rhs , c , areEqual , testIsTrue ) and
456- right = rhs .getLeftOperand ( ) and x = int_value ( rhs .getRightOperand ( ) )
455+ exists ( SubInstruction rhs , int c , int x | compares_eq ( cmp , left , rhs . getAUse ( ) , c , areEqual , testIsTrue ) and
456+ right = rhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( rhs .getRightOperand ( ) )
457457 and k = c - x
458458 )
459459}
460460
461461
462462/* left + x == right + c => left == right + (c-x)
463463 left == (right + x) + c => left == right + (c+x) */
464- private predicate add_eq ( CompareInstruction cmp , Instruction left , Instruction right , int k , boolean areEqual , boolean testIsTrue ) {
465- exists ( AddInstruction lhs , int c , int x | compares_eq ( cmp , lhs , right , c , areEqual , testIsTrue ) and
466- ( left = lhs .getLeftOperand ( ) and x = int_value ( lhs .getRightOperand ( ) )
464+ private predicate add_eq ( CompareInstruction cmp , Operand left , Operand right , int k , boolean areEqual , boolean testIsTrue ) {
465+ exists ( AddInstruction lhs , int c , int x | compares_eq ( cmp , lhs . getAUse ( ) , right , c , areEqual , testIsTrue ) and
466+ ( left = lhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( lhs .getRightOperand ( ) )
467467 or
468- left = lhs .getRightOperand ( ) and x = int_value ( lhs .getLeftOperand ( ) )
468+ left = lhs .getAnOperand ( ) . ( RightOperand ) and x = int_value ( lhs .getLeftOperand ( ) )
469469 )
470470 and k = c - x
471471 )
472472 or
473- exists ( AddInstruction rhs , int c , int x | compares_eq ( cmp , left , rhs , c , areEqual , testIsTrue ) and
474- ( right = rhs .getLeftOperand ( ) and x = int_value ( rhs .getRightOperand ( ) )
473+ exists ( AddInstruction rhs , int c , int x | compares_eq ( cmp , left , rhs . getAUse ( ) , c , areEqual , testIsTrue ) and
474+ ( right = rhs .getAnOperand ( ) . ( LeftOperand ) and x = int_value ( rhs .getRightOperand ( ) )
475475 or
476- right = rhs .getRightOperand ( ) and x = int_value ( rhs .getLeftOperand ( ) )
476+ right = rhs .getAnOperand ( ) . ( RightOperand ) and x = int_value ( rhs .getLeftOperand ( ) )
477477 )
478478 and k = c + x
479479 )
0 commit comments