|
| 1 | +/** |
| 2 | + * @name 06_MinIntNegate |
| 3 | + * @description Negating MIN_INT is an integer overflow |
| 4 | + * @kind problem |
| 5 | + * @id cpp/min-int-negate |
| 6 | + * @problem.severity warning |
| 7 | + */ |
| 8 | + |
| 9 | +import cpp |
| 10 | +import semmle.code.cpp.controlflow.Guards |
| 11 | +import semmle.code.cpp.valuenumbering.GlobalValueNumbering |
| 12 | +import semmle.code.cpp.dataflow.DataFlow |
| 13 | + |
| 14 | +// Let's add local dataflow, so that we can also handle cases like this: |
| 15 | +// |
| 16 | +// ``` |
| 17 | +// bool b = x < 0; |
| 18 | +// if (b) { |
| 19 | +// x = -x; |
| 20 | +// } |
| 21 | +// ``` |
| 22 | + |
| 23 | +/** |
| 24 | + * Holds if `cond` is a comparison of the form `lhs < rhs`. |
| 25 | + * `isStrict` is true for < and >, and false for <= and >=. |
| 26 | + */ |
| 27 | +predicate lessThan(Expr cond, Expr lhs, Expr rhs, boolean isStrict) { |
| 28 | + cond.(LTExpr).getLeftOperand() = lhs and |
| 29 | + cond.(LTExpr).getRightOperand() = rhs and |
| 30 | + isStrict = true |
| 31 | + or |
| 32 | + cond.(GTExpr).getLeftOperand() = rhs and |
| 33 | + cond.(GTExpr).getRightOperand() = lhs and |
| 34 | + isStrict = true |
| 35 | + or |
| 36 | + cond.(LEExpr).getLeftOperand() = lhs and |
| 37 | + cond.(LEExpr).getRightOperand() = rhs and |
| 38 | + isStrict = false |
| 39 | + or |
| 40 | + cond.(GEExpr).getLeftOperand() = rhs and |
| 41 | + cond.(GEExpr).getRightOperand() = lhs and |
| 42 | + isStrict = false |
| 43 | +} |
| 44 | + |
| 45 | +/** |
| 46 | + * Holds if `cond` is a comparison of the form `lhs < rhs`. |
| 47 | + * `isStrict` is true for < and >, and false for <= and >=. |
| 48 | + * `branch` is true if the comparison is true and false if it is not. |
| 49 | + */ |
| 50 | +predicate lessThanWithNegate(Expr cond, Expr lhs, Expr rhs, boolean isStrict, boolean branch) { |
| 51 | + branch = true and lessThan(cond, lhs, rhs, isStrict) |
| 52 | + or |
| 53 | + // (x < y) == !(y <= x) |
| 54 | + lessThanWithNegate(cond, rhs, lhs, isStrict.booleanNot(), branch.booleanNot()) |
| 55 | + or |
| 56 | + // bool b = x < 0; |
| 57 | + // if (b) { ... } |
| 58 | + exists(Expr prev | |
| 59 | + DataFlow::localExprFlow(prev, cond) and |
| 60 | + lessThanWithNegate(prev, lhs, rhs, branch, isStrict) |
| 61 | + ) |
| 62 | +} |
| 63 | + |
| 64 | +from |
| 65 | + GuardCondition guard, BasicBlock block, UnaryMinusExpr unaryMinus, Expr use1, Expr use2, |
| 66 | + Expr zero, boolean branch |
| 67 | +where |
| 68 | + lessThanWithNegate(guard, use1, zero, _, branch) and |
| 69 | + zero.getValue().toInt() = 0 and |
| 70 | + guard.controls(block, branch) and |
| 71 | + block.contains(unaryMinus) and |
| 72 | + unaryMinus.getOperand() = use2 and |
| 73 | + globalValueNumber(use1) = globalValueNumber(use2) |
| 74 | +select unaryMinus, "If the value of $@ is MinInt then this assignment will not make it positive", |
| 75 | + use2, use2.toString() |
0 commit comments