@@ -585,6 +585,12 @@ private float addRoundingDownSmall(float x, float small) {
585585 if ( x + small ) - x > small then result = ( x + small ) .nextDown ( ) else result = ( x + small )
586586}
587587
588+ private predicate lowerBoundableExpr ( Expr expr ) {
589+ analyzableExpr ( expr ) and
590+ getUpperBoundsImpl ( expr ) <= exprMaxVal ( expr ) and
591+ not exists ( getValue ( expr ) .toFloat ( ) )
592+ }
593+
588594/**
589595 * Gets the lower bounds of the expression.
590596 *
@@ -603,41 +609,42 @@ private float addRoundingDownSmall(float x, float small) {
603609 * this predicate.
604610 */
605611private float getTruncatedLowerBounds ( Expr expr ) {
606- if analyzableExpr ( expr )
607- then
608- // If the expression evaluates to a constant, then there is no
609- // need to call getLowerBoundsImpl.
610- if exists ( getValue ( expr ) .toFloat ( ) )
611- then result = getValue ( expr ) .toFloat ( )
612- else (
613- // Some of the bounds computed by getLowerBoundsImpl might
614- // overflow, so we replace invalid bounds with exprMinVal.
615- exists ( float newLB | newLB = normalizeFloatUp ( getLowerBoundsImpl ( expr ) ) |
616- if exprMinVal ( expr ) <= newLB and newLB <= exprMaxVal ( expr )
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
627- else result = exprMinVal ( expr )
628- )
629- or
630- // The expression might overflow and wrap. If so, the
631- // lower bound is exprMinVal.
632- exprMightOverflowPositively ( expr ) and
633- result = exprMinVal ( expr )
634- )
635- else
636- // The expression is not analyzable, so its lower bound is
637- // unknown. Note that the call to exprMinVal restricts the
638- // expressions to just those with arithmetic types. There is no
639- // need to return results for non-arithmetic expressions.
640- result = exprMinVal ( expr )
612+ // If the expression evaluates to a constant, then there is no
613+ // need to call getLowerBoundsImpl.
614+ analyzableExpr ( expr ) and
615+ result = getValue ( expr ) .toFloat ( )
616+ or
617+ // Some of the bounds computed by getLowerBoundsImpl might
618+ // overflow, so we replace invalid bounds with exprMinVal.
619+ exists ( float newLB | newLB = normalizeFloatUp ( getLowerBoundsImpl ( expr ) ) |
620+ if exprMinVal ( expr ) <= newLB and newLB <= exprMaxVal ( expr )
621+ then
622+ // Apply widening where we might get a combinatorial explosion.
623+ if isRecursiveBinary ( expr )
624+ then
625+ result =
626+ max ( float widenLB |
627+ widenLB = wideningLowerBounds ( expr .getUnspecifiedType ( ) ) and
628+ not widenLB > newLB
629+ )
630+ else result = newLB
631+ else result = exprMinVal ( expr )
632+ ) and
633+ lowerBoundableExpr ( expr )
634+ or
635+ // The expression might overflow and wrap. If so, the
636+ // lower bound is exprMinVal.
637+ analyzableExpr ( expr ) and
638+ exprMightOverflowPositively ( expr ) and
639+ not result = getValue ( expr ) .toFloat ( ) and
640+ result = exprMinVal ( expr )
641+ or
642+ // The expression is not analyzable, so its lower bound is
643+ // unknown. Note that the call to exprMinVal restricts the
644+ // expressions to just those with arithmetic types. There is no
645+ // need to return results for non-arithmetic expressions.
646+ not analyzableExpr ( expr ) and
647+ result = exprMinVal ( expr )
641648}
642649
643650/**
0 commit comments