diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll new file mode 100644 index 00000000000..bd234390e3d --- /dev/null +++ b/cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SimpleRangeAnalysis.qll @@ -0,0 +1,132 @@ +/** + * Wrapper for the semantic range analysis library that mimics the + * interface of the simple range analysis library. + */ + +private import cpp +private import semmle.code.cpp.ir.IR +private import experimental.semmle.code.cpp.semantic.SemanticBound +private import experimental.semmle.code.cpp.semantic.SemanticExprSpecific +private import RangeAnalysis + +/** + * Gets the lower bound of the expression. + * + * Note: expressions in C/C++ are often implicitly or explicitly cast to a + * different result type. Such casts can cause the value of the expression + * to overflow or to be truncated. This predicate computes the lower bound + * of the expression without including the effect of the casts. To compute + * the lower bound of the expression after all the casts have been applied, + * call `lowerBound` like this: + * + * `lowerBound(expr.getFullyConverted())` + */ +float lowerBound(Expr expr) { + exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound | + semBounded(getSemanticExpr(i), b, result, false, _) + ) +} + +/** + * Gets the upper bound of the expression. + * + * Note: expressions in C/C++ are often implicitly or explicitly cast to a + * different result type. Such casts can cause the value of the expression + * to overflow or to be truncated. This predicate computes the upper bound + * of the expression without including the effect of the casts. To compute + * the upper bound of the expression after all the casts have been applied, + * call `upperBound` like this: + * + * `upperBound(expr.getFullyConverted())` + */ +float upperBound(Expr expr) { + exists(Instruction i, SemBound b | i.getAst() = expr and b instanceof SemZeroBound | + semBounded(getSemanticExpr(i), b, result, true, _) + ) +} + +/** + * Holds if the upper bound of `expr` may have been widened. This means the + * upper bound is in practice likely to be overly wide. + */ +predicate upperBoundMayBeWidened(Expr e) { none() } + +/** + * Holds if `expr` has a provably empty range. For example: + * + * 10 < expr and expr < 5 + * + * The range of an expression can only be empty if it can never be + * executed. For example: + * + * ```cpp + * if (10 < x) { + * if (x < 5) { + * // Unreachable code + * return x; // x has an empty range: 10 < x && x < 5 + * } + * } + * ``` + */ +predicate exprWithEmptyRange(Expr expr) { lowerBound(expr) > upperBound(expr) } + +/** Holds if the definition might overflow negatively. */ +predicate defMightOverflowNegatively(RangeSsaDefinition def, StackVariable v) { none() } + +/** Holds if the definition might overflow positively. */ +predicate defMightOverflowPositively(RangeSsaDefinition def, StackVariable v) { none() } + +/** + * Holds if the definition might overflow (either positively or + * negatively). + */ +predicate defMightOverflow(RangeSsaDefinition def, StackVariable v) { + defMightOverflowNegatively(def, v) or + defMightOverflowPositively(def, v) +} + +/** + * Holds if the expression might overflow negatively. This predicate + * does not consider the possibility that the expression might overflow + * due to a conversion. + */ +predicate exprMightOverflowNegatively(Expr expr) { none() } + +/** + * Holds if the expression might overflow negatively. Conversions + * are also taken into account. For example the expression + * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than + * due to the addition. + */ +predicate convertedExprMightOverflowNegatively(Expr expr) { + exprMightOverflowNegatively(expr) or + convertedExprMightOverflowNegatively(expr.getConversion()) +} + +/** + * Holds if the expression might overflow positively. This predicate + * does not consider the possibility that the expression might overflow + * due to a conversion. + */ +predicate exprMightOverflowPositively(Expr expr) { none() } + +/** + * Holds if the expression might overflow positively. Conversions + * are also taken into account. For example the expression + * `(int16)(x+y)` might overflow due to the `(int16)` cast, rather than + * due to the addition. + */ +predicate convertedExprMightOverflowPositively(Expr expr) { + exprMightOverflowPositively(expr) or + convertedExprMightOverflowPositively(expr.getConversion()) +} + +/** + * Holds if the expression might overflow (either positively or + * negatively). The possibility that the expression might overflow + * due to an implicit or explicit cast is also considered. + */ +predicate convertedExprMightOverflow(Expr expr) { + convertedExprMightOverflowNegatively(expr) or + convertedExprMightOverflowPositively(expr) +}