C++: Only propagate smallest/largest bound in conditional expressions

This commit is contained in:
Simon Friis Vindum
2025-01-13 12:11:45 +01:00
parent 847f3f1fc2
commit 0c9ee4d029

View File

@@ -773,22 +773,28 @@ private float getLowerBoundsImpl(Expr expr) {
)
)
or
// ConditionalExpr (true branch)
exists(ConditionalExpr condExpr |
exists(ConditionalExpr condExpr, Expr conv, float ub, float lb |
expr = condExpr and
conv = condExpr.getCondition().getFullyConverted() and
// Use `boolConversionUpperBound` to determine whether the condition
// might evaluate to `true`.
boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
result = getFullyConvertedLowerBounds(condExpr.getThen())
)
or
// ConditionalExpr (false branch)
exists(ConditionalExpr condExpr |
expr = condExpr and
// Use `boolConversionLowerBound` to determine whether the condition
// might evaluate to `false`.
boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
result = getFullyConvertedLowerBounds(condExpr.getElse())
lb = boolConversionLowerBound(conv) and
ub = boolConversionUpperBound(conv)
|
// Both branches can be taken
ub = 1 and
lb = 0 and
exists(float thenLb, float elseLb |
thenLb = getFullyConvertedLowerBounds(condExpr.getThen()) and
elseLb = getFullyConvertedLowerBounds(condExpr.getElse()) and
result = thenLb.minimum(elseLb)
)
or
// Only the `true` branch can be taken
ub = 1 and lb != 0 and result = getFullyConvertedLowerBounds(condExpr.getThen())
or
// Only the `false` branch can be taken
ub != 1 and lb = 0 and result = getFullyConvertedLowerBounds(condExpr.getElse())
)
or
exists(AddExpr addExpr, float xLow, float yLow |
@@ -977,22 +983,28 @@ private float getUpperBoundsImpl(Expr expr) {
)
)
or
// ConditionalExpr (true branch)
exists(ConditionalExpr condExpr |
exists(ConditionalExpr condExpr, Expr conv, float ub, float lb |
expr = condExpr and
conv = condExpr.getCondition().getFullyConverted() and
// Use `boolConversionUpperBound` to determine whether the condition
// might evaluate to `true`.
boolConversionUpperBound(condExpr.getCondition().getFullyConverted()) = 1 and
result = getFullyConvertedUpperBounds(condExpr.getThen())
)
or
// ConditionalExpr (false branch)
exists(ConditionalExpr condExpr |
expr = condExpr and
// Use `boolConversionLowerBound` to determine whether the condition
// might evaluate to `false`.
boolConversionLowerBound(condExpr.getCondition().getFullyConverted()) = 0 and
result = getFullyConvertedUpperBounds(condExpr.getElse())
lb = boolConversionLowerBound(conv) and
ub = boolConversionUpperBound(conv)
|
// Both branches can be taken
ub = 1 and
lb = 0 and
exists(float thenLb, float elseLb |
thenLb = getFullyConvertedUpperBounds(condExpr.getThen()) and
elseLb = getFullyConvertedUpperBounds(condExpr.getElse()) and
result = thenLb.maximum(elseLb)
)
or
// Only the `true` branch can be taken
ub = 1 and lb != 0 and result = getFullyConvertedUpperBounds(condExpr.getThen())
or
// Only the `false` branch can be taken
ub != 1 and lb = 0 and result = getFullyConvertedUpperBounds(condExpr.getElse())
)
or
exists(AddExpr addExpr, float xHigh, float yHigh |