C++: Tweak the bounded barrier

This commit is contained in:
Simon Friis Vindum
2024-08-29 10:32:31 +02:00
parent 047a655dec
commit e7f059ae55
5 changed files with 110 additions and 79 deletions

View File

@@ -1,6 +1,6 @@
/**
* This file provides the `bounded` predicate that is used in both `cpp/uncontrolled-arithmetic`
* and `cpp/tainted-arithmetic`.
* This file provides the `bounded` predicate that is used in `cpp/uncontrolled-arithmetic`,
* `cpp/tainted-arithmetic` and `cpp/uncontrolled-allocation-size`.
*/
private import cpp
@@ -8,20 +8,18 @@ private import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
private import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
/**
* An operand `e` of a bitwise and expression `andExpr` (i.e., `andExpr` is either an `BitwiseAndExpr`
* or an `AssignAndExpr`) with operands `operand1` and `operand2` is the operand that is not `e` is upper
* bounded by some number that is less than the maximum integer allowed by the result type of `andExpr`.
* An operand `operand` of a bitwise and expression `andExpr` (i.e., `andExpr` is either a
* `BitwiseAndExpr` or an `AssignAndExpr`) is upper bounded by some number that is less than the
* maximum integer allowed by the result type of `andExpr`.
*/
pragma[inline]
private predicate boundedBitwiseAnd(Expr e, Expr andExpr, Expr operand1, Expr operand2) {
operand1 != operand2 and
e = operand1 and
upperBound(operand2.getFullyConverted()) < exprMaxVal(andExpr.getFullyConverted())
private predicate boundedBitwiseAnd(Expr operand, Expr andExpr) {
upperBound(operand.getFullyConverted()) < exprMaxVal(andExpr.getFullyConverted())
}
/**
* Holds if `e` is an arithmetic expression that cannot overflow, or if `e` is an operand of an
* operation that may greatly reduce the range of possible values.
* Holds if `e` is an arithmetic expression that cannot overflow, or if `e` is an operation that
* may greatly reduce the range of possible values.
*/
predicate bounded(Expr e) {
// There can be two separate reasons for `convertedExprMightOverflow` not holding:
@@ -35,25 +33,25 @@ predicate bounded(Expr e) {
) and
not convertedExprMightOverflow(e)
or
// Optimistically assume that a remainder expression always yields a much smaller value.
e = any(RemExpr rem).getLeftOperand()
// Optimistically assume that the following operations always yields a much smaller value.
e instanceof RemExpr
or
e = any(AssignRemExpr rem).getLValue()
e instanceof DivExpr
or
e instanceof RShiftExpr
or
exists(BitwiseAndExpr andExpr |
boundedBitwiseAnd(e, andExpr, andExpr.getAnOperand(), andExpr.getAnOperand())
e = andExpr and boundedBitwiseAnd(andExpr.getAnOperand(), andExpr)
)
or
exists(AssignAndExpr andExpr |
boundedBitwiseAnd(e, andExpr, andExpr.getAnOperand(), andExpr.getAnOperand())
)
or
// Optimistically assume that a division always yields a much smaller value.
e = any(DivExpr div).getLeftOperand()
// For the assignment variant of the operations we place the barrier on the assigned lvalue.
e = any(AssignRemExpr rem).getLValue()
or
e = any(AssignDivExpr div).getLValue()
or
e = any(RShiftExpr shift).getLeftOperand()
or
e = any(AssignRShiftExpr div).getLValue()
or
exists(AssignAndExpr andExpr |
e = andExpr.getLValue() and boundedBitwiseAnd(andExpr.getRValue(), andExpr)
)
}