Skip to content

Commit

Permalink
C++: Only propagate smallest/largest bound in conditional expressions
Browse files Browse the repository at this point in the history
  • Loading branch information
paldepind committed Jan 13, 2025
1 parent 847f3f1 commit 0c9ee4d
Showing 1 changed file with 38 additions and 26 deletions.
64 changes: 38 additions & 26 deletions cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
Original file line number Diff line number Diff line change
Expand Up @@ -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 |
Expand Down Expand Up @@ -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 |
Expand Down

0 comments on commit 0c9ee4d

Please sign in to comment.