|
| 1 | +/** |
| 2 | + * Wrapper for the semantic range analysis library that mimics the |
| 3 | + * interface of the simple range analysis library. |
| 4 | + */ |
| 5 | + |
| 6 | +private import cpp |
| 7 | +private import semmle.code.cpp.ir.IR |
| 8 | +private import experimental.semmle.code.cpp.semantic.SemanticBound |
| 9 | +private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific |
| 10 | +private import RangeAnalysis |
| 11 | + |
| 12 | +/** |
| 13 | + * Gets the lower bound of the expression. |
| 14 | + * |
| 15 | + * Note: expressions in C/C++ are often implicitly or explicitly cast to a |
| 16 | + * different result type. Such casts can cause the value of the expression |
| 17 | + * to overflow or to be truncated. This predicate computes the lower bound |
| 18 | + * of the expression without including the effect of the casts. To compute |
| 19 | + * the lower bound of the expression after all the casts have been applied, |
| 20 | + * call `lowerBound` like this: |
| 21 | + * |
| 22 | + * `lowerBound(expr.getFullyConverted())` |
| 23 | + */ |
| 24 | +float lowerBound(Expr expr) { |
| 25 | + exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound | |
| 26 | + semBounded(getSemanticExpr(i), b, result, false, _) |
| 27 | + ) |
| 28 | +} |
| 29 | + |
| 30 | +/** |
| 31 | + * Gets the upper bound of the expression. |
| 32 | + * |
| 33 | + * Note: expressions in C/C++ are often implicitly or explicitly cast to a |
| 34 | + * different result type. Such casts can cause the value of the expression |
| 35 | + * to overflow or to be truncated. This predicate computes the upper bound |
| 36 | + * of the expression without including the effect of the casts. To compute |
| 37 | + * the upper bound of the expression after all the casts have been applied, |
| 38 | + * call `upperBound` like this: |
| 39 | + * |
| 40 | + * `upperBound(expr.getFullyConverted())` |
| 41 | + */ |
| 42 | +float upperBound(Expr expr) { |
| 43 | + exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound | |
| 44 | + semBounded(getSemanticExpr(i), b, result, true, _) |
| 45 | + ) |
| 46 | +} |
| 47 | + |
| 48 | +/** |
| 49 | + * Holds if the upper bound of `expr` may have been widened. This means the |
| 50 | + * upper bound is in practice likely to be overly wide. |
| 51 | + */ |
| 52 | +predicate upperBoundMayBeWidened(Expr e) { none() } |
| 53 | + |
| 54 | +/** |
| 55 | + * Holds if `expr` has a provably empty range. For example: |
| 56 | + * |
| 57 | + * 10 < expr and expr < 5 |
| 58 | + * |
| 59 | + * The range of an expression can only be empty if it can never be |
| 60 | + * executed. For example: |
| 61 | + * |
| 62 | + * ```cpp |
| 63 | + * if (10 < x) { |
| 64 | + * if (x < 5) { |
| 65 | + * // Unreachable code |
| 66 | + * return x; // x has an empty range: 10 < x && x < 5 |
| 67 | + * } |
| 68 | + * } |
| 69 | + * ``` |
| 70 | + */ |
| 71 | +predicate exprWithEmptyRange(Expr expr) { lowerBound(expr) > upperBound(expr) } |
| 72 | + |
| 73 | +/** Holds if the definition might overflow negatively. */ |
| 74 | +predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) { none() } |
| 75 | + |
| 76 | +/** Holds if the definition might overflow positively. */ |
| 77 | +predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) { none() } |
| 78 | + |
| 79 | +/** |
| 80 | + * Holds if the definition might overflow (either positively or |
| 81 | + * negatively). |
| 82 | + */ |
| 83 | +predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) { |
| 84 | + defMightOverflowNegatively(def, v) or |
| 85 | + defMightOverflowPositively(def, v) |
| 86 | +} |
| 87 | + |
| 88 | +/** |
| 89 | + * Holds if the expression might overflow negatively. This predicate |
| 90 | + * does not consider the possibility that the expression might overflow |
| 91 | + * due to a conversion. |
| 92 | + */ |
| 93 | +predicate exprMightOverflowNegatively(Expr expr) { none() } |
| 94 | + |
| 95 | +/** |
| 96 | + * Holds if the expression might overflow negatively. Conversions |
| 97 | + * are also taken into account. For example the expression |
| 98 | + * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than |
| 99 | + * due to the addition. |
| 100 | + */ |
| 101 | +predicate convertedExprMightOverflowNegatively(Expr expr) { |
| 102 | + exprMightOverflowNegatively(expr) or |
| 103 | + convertedExprMightOverflowNegatively(expr.getConversion()) |
| 104 | +} |
| 105 | + |
| 106 | +/** |
| 107 | + * Holds if the expression might overflow positively. This predicate |
| 108 | + * does not consider the possibility that the expression might overflow |
| 109 | + * due to a conversion. |
| 110 | + */ |
| 111 | +predicate exprMightOverflowPositively(Expr expr) { none() } |
| 112 | + |
| 113 | +/** |
| 114 | + * Holds if the expression might overflow positively. Conversions |
| 115 | + * are also taken into account. For example the expression |
| 116 | + * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than |
| 117 | + * due to the addition. |
| 118 | + */ |
| 119 | +predicate convertedExprMightOverflowPositively(Expr expr) { |
| 120 | + exprMightOverflowPositively(expr) or |
| 121 | + convertedExprMightOverflowPositively(expr.getConversion()) |
| 122 | +} |
| 123 | + |
| 124 | +/** |
| 125 | + * Holds if the expression might overflow (either positively or |
| 126 | + * negatively). The possibility that the expression might overflow |
| 127 | + * due to an implicit or explicit cast is also considered. |
| 128 | + */ |
| 129 | +predicate convertedExprMightOverflow(Expr expr) { |
| 130 | + convertedExprMightOverflowNegatively(expr) or |
| 131 | + convertedExprMightOverflowPositively(expr) |
| 132 | +} |
0 commit comments