|
| 1 | +private import cpp |
| 2 | +private import experimental.semmle.code.cpp.models.interfaces.SimpleRangeAnalysisExpr |
| 3 | +private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils |
| 4 | + |
| 5 | +/** |
| 6 | + * Holds if `e` is a constant or if it is a variable with a constant value |
| 7 | + */ |
| 8 | +float evaluateConstantExpr(Expr e) { |
| 9 | + result = e.getValue().toFloat() |
| 10 | + or |
| 11 | + exists(SsaDefinition defn, StackVariable sv | |
| 12 | + defn.getAUse(sv) = e and |
| 13 | + result = defn.getDefiningValue(sv).getValue().toFloat() |
| 14 | + ) |
| 15 | +} |
| 16 | + |
| 17 | +/** |
| 18 | + * The current implementation for `BitwiseAndExpr` only handles cases where both operands are |
| 19 | + * either unsigned or non-negative constants. This class not only covers these cases, but also |
| 20 | + * adds support for `&` expressions between a signed integer with a non-negative range and a |
| 21 | + * non-negative constant. It also adds support for `&=` for the same set of cases as `&`. |
| 22 | + */ |
| 23 | +private class ConstantBitwiseAndExprRange extends SimpleRangeAnalysisExpr { |
| 24 | + ConstantBitwiseAndExprRange() { |
| 25 | + exists(Expr l, Expr r | |
| 26 | + l = this.(BitwiseAndExpr).getLeftOperand() and |
| 27 | + r = this.(BitwiseAndExpr).getRightOperand() |
| 28 | + or |
| 29 | + l = this.(AssignAndExpr).getLValue() and |
| 30 | + r = this.(AssignAndExpr).getRValue() |
| 31 | + | |
| 32 | + // No operands can be negative constants |
| 33 | + not (evaluateConstantExpr(l) < 0 or evaluateConstantExpr(r) < 0) and |
| 34 | + // At least one operand must be a non-negative constant |
| 35 | + (evaluateConstantExpr(l) >= 0 or evaluateConstantExpr(r) >= 0) |
| 36 | + ) |
| 37 | + } |
| 38 | + |
| 39 | + Expr getLeftOperand() { |
| 40 | + result = this.(BitwiseAndExpr).getLeftOperand() or |
| 41 | + result = this.(AssignAndExpr).getLValue() |
| 42 | + } |
| 43 | + |
| 44 | + Expr getRightOperand() { |
| 45 | + result = this.(BitwiseAndExpr).getRightOperand() or |
| 46 | + result = this.(AssignAndExpr).getRValue() |
| 47 | + } |
| 48 | + |
| 49 | + override float getLowerBounds() { |
| 50 | + // If an operand can have negative values, the lower bound is unconstrained. |
| 51 | + // Otherwise, the lower bound is zero. |
| 52 | + exists(float lLower, float rLower | |
| 53 | + lLower = getFullyConvertedLowerBounds(getLeftOperand()) and |
| 54 | + rLower = getFullyConvertedLowerBounds(getRightOperand()) and |
| 55 | + ( |
| 56 | + (lLower < 0 or rLower < 0) and |
| 57 | + result = exprMinVal(this) |
| 58 | + or |
| 59 | + // This technically results in two lowerBounds when an operand range is negative, but |
| 60 | + // that's fine since `exprMinVal(x) <= 0`. We can't use an if statement here without |
| 61 | + // non-monotonic recursion issues |
| 62 | + result = 0 |
| 63 | + ) |
| 64 | + ) |
| 65 | + } |
| 66 | + |
| 67 | + override float getUpperBounds() { |
| 68 | + // If an operand can have negative values, the upper bound is unconstrained. |
| 69 | + // Otherwise, the upper bound is the minimum of the upper bounds of the operands |
| 70 | + exists(float lLower, float lUpper, float rLower, float rUpper | |
| 71 | + lLower = getFullyConvertedLowerBounds(getLeftOperand()) and |
| 72 | + lUpper = getFullyConvertedUpperBounds(getLeftOperand()) and |
| 73 | + rLower = getFullyConvertedLowerBounds(getRightOperand()) and |
| 74 | + rUpper = getFullyConvertedUpperBounds(getRightOperand()) and |
| 75 | + ( |
| 76 | + (lLower < 0 or rLower < 0) and |
| 77 | + result = exprMaxVal(this) |
| 78 | + or |
| 79 | + // This technically results in two upperBounds when an operand range is negative, but |
| 80 | + // that's fine since `exprMaxVal(b) >= result`. We can't use an if statement here without |
| 81 | + // non-monotonic recursion issues |
| 82 | + result = rUpper.minimum(lUpper) |
| 83 | + ) |
| 84 | + ) |
| 85 | + } |
| 86 | + |
| 87 | + override predicate dependsOnChild(Expr child) { |
| 88 | + child = getLeftOperand() or child = getRightOperand() |
| 89 | + } |
| 90 | +} |
0 commit comments