C++: Introduce wrapper for the semantic range analysis mimicking the simple one

This commit is contained in:
Jeroen Ketema
2023-03-10 13:29:00 +01:00
parent 348165205c
commit 0e45c9982b

View File

@@ -0,0 +1,120 @@
/**
* 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) { none() }
/**
* 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) { none() }
/**
* 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) { none() }
/**
* 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) { none() }