@@ -460,6 +460,39 @@ private predicate isRecursiveDef(RangeSsaDefinition def, StackVariable v) {
460460 defDependsOnDefTransitively ( def , v , def , v )
461461}
462462
463+ /**
464+ * Holds if the bounds of `e` depend on a recursive definition, meaning that
465+ * `e` is likely to have many candidate bounds during the main recursion.
466+ */
467+ private predicate isRecursiveExpr ( Expr e ) {
468+ exists ( RangeSsaDefinition def , StackVariable v | exprDependsOnDef ( e , def , v ) |
469+ isRecursiveDef ( def , v )
470+ )
471+ }
472+
473+ /**
474+ * Holds if `binop` is a binary operation that's likely to be assigned a
475+ * quadratic (or more) number of candidate bounds during the analysis. This can
476+ * happen when two conditions are satisfied:
477+ * 1. It is likely there are many more candidate bounds for `binop` than for
478+ * its operands. For example, the number of candidate bounds for `x + y`,
479+ * denoted here nbounds(`x + y`), will be O(nbounds(`x`) * nbounds(`y`)).
480+ * In contrast, nbounds(`b ? x : y`) is only O(nbounds(`x`) + nbounds(`y`)).
481+ * 2. Both operands of `binop` are recursively determined and are therefore
482+ * likely to have a large number of candidate bounds.
483+ */
484+ private predicate isRecursiveBinary ( BinaryOperation binop ) {
485+ (
486+ binop instanceof UnsignedMulExpr
487+ or
488+ binop instanceof AddExpr
489+ or
490+ binop instanceof SubExpr
491+ ) and
492+ isRecursiveExpr ( binop .getLeftOperand ( ) ) and
493+ isRecursiveExpr ( binop .getRightOperand ( ) )
494+ }
495+
463496/**
464497 * We distinguish 3 kinds of RangeSsaDefinition:
465498 *
@@ -581,7 +614,16 @@ private float getTruncatedLowerBounds(Expr expr) {
581614 // overflow, so we replace invalid bounds with exprMinVal.
582615 exists ( float newLB | newLB = normalizeFloatUp ( getLowerBoundsImpl ( expr ) ) |
583616 if exprMinVal ( expr ) <= newLB and newLB <= exprMaxVal ( expr )
584- then result = newLB
617+ then
618+ // Apply widening where we might get a combinatorial explosion.
619+ if isRecursiveBinary ( expr )
620+ then
621+ result =
622+ max ( float widenLB |
623+ widenLB = wideningLowerBounds ( expr .getUnspecifiedType ( ) ) and
624+ not widenLB > newLB
625+ )
626+ else result = newLB
585627 else result = exprMinVal ( expr )
586628 )
587629 or
@@ -628,7 +670,16 @@ private float getTruncatedUpperBounds(Expr expr) {
628670 // `exprMaxVal`.
629671 exists ( float newUB | newUB = normalizeFloatUp ( getUpperBoundsImpl ( expr ) ) |
630672 if exprMinVal ( expr ) <= newUB and newUB <= exprMaxVal ( expr )
631- then result = newUB
673+ then
674+ // Apply widening where we might get a combinatorial explosion.
675+ if isRecursiveBinary ( expr )
676+ then
677+ result =
678+ min ( float widenUB |
679+ widenUB = wideningUpperBounds ( expr .getUnspecifiedType ( ) ) and
680+ not widenUB < newUB
681+ )
682+ else result = newUB
632683 else result = exprMaxVal ( expr )
633684 )
634685 or
0 commit comments