Merge pull request #5678 from MathiasVP/sound-expr-might-overflow-predicate

C++: Make exprMightOverflowPositively sound for unanalyzable expressions
This commit is contained in:
Geoffrey White
2021-04-26 17:38:23 +01:00
committed by GitHub
3 changed files with 25 additions and 0 deletions

View File

@@ -0,0 +1,2 @@
lgtm,codescanning
* The `exprMightOverflowPositively` and `exprMightOverflowNegatively` predicates from the `SimpleRangeAnalysis` library now recognize more expressions that might overflow.

View File

@@ -28,6 +28,7 @@ predicate outOfBoundsExpr(Expr expr, string kind) {
from Expr use, Expr origin, string kind
where
not use.getUnspecifiedType() instanceof PointerType and
outOfBoundsExpr(use, kind) and
tainted(origin, use) and
origin != use and

View File

@@ -1617,6 +1617,18 @@ private module SimpleRangeAnalysisCached {
defMightOverflowPositively(def, v)
}
/**
* Holds if `e` is an expression where the concept of overflow makes sense.
* This predicate is used to filter out some of the unanalyzable expressions
* from `exprMightOverflowPositively` and `exprMightOverflowNegatively`.
*/
pragma[inline]
private predicate exprThatCanOverflow(Expr e) {
e instanceof UnaryArithmeticOperation or
e instanceof BinaryArithmeticOperation or
e instanceof LShiftExpr
}
/**
* Holds if the expression might overflow negatively. This predicate
* does not consider the possibility that the expression might overflow
@@ -1630,6 +1642,11 @@ private module SimpleRangeAnalysisCached {
// bound of `x`, so the standard logic (above) does not work for
// detecting whether it might overflow.
getLowerBoundsImpl(expr.(PostfixDecrExpr)) = exprMinVal(expr)
or
// We can't conclude that any unanalyzable expression might overflow. This
// is because there are many expressions that the range analysis doesn't
// handle, but where the concept of overflow doesn't make sense.
exprThatCanOverflow(expr) and not analyzableExpr(expr)
}
/**
@@ -1657,6 +1674,11 @@ private module SimpleRangeAnalysisCached {
// bound of `x`, so the standard logic (above) does not work for
// detecting whether it might overflow.
getUpperBoundsImpl(expr.(PostfixIncrExpr)) = exprMaxVal(expr)
or
// We can't conclude that any unanalyzable expression might overflow. This
// is because there are many expressions that the range analysis doesn't
// handle, but where the concept of overflow doesn't make sense.
exprThatCanOverflow(expr) and not analyzableExpr(expr)
}
/**