|
12 | 12 | */ |
13 | 13 |
|
14 | 14 | import cpp |
| 15 | +import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils |
| 16 | +import semmle.code.cpp.dataflow.DataFlow |
15 | 17 |
|
16 | | -Loop getAnEnclosingLoopOfExpr(Expr e) { |
17 | | - result = e.getEnclosingStmt().getParent*() or |
18 | | - result = getAnEnclosingLoopOfStmt(e.getEnclosingStmt()) |
19 | | -} |
| 18 | +/** Gets a loop that contains `e`. */ |
| 19 | +Loop getAnEnclosingLoopOfExpr(Expr e) { result = getAnEnclosingLoopOfStmt(e.getEnclosingStmt()) } |
20 | 20 |
|
| 21 | +/** Gets a loop that contains `s`. */ |
21 | 22 | Loop getAnEnclosingLoopOfStmt(Stmt s) { |
22 | | - result = s.getParent*() or |
| 23 | + result = s.getParent*() and |
| 24 | + not s = result.(ForStmt).getInitialization() |
| 25 | + or |
23 | 26 | result = getAnEnclosingLoopOfExpr(s.getParent*()) |
24 | 27 | } |
25 | 28 |
|
26 | | -from Loop l, FunctionCall fc |
27 | | -where |
28 | | - getAnEnclosingLoopOfExpr(fc) = l and |
29 | | - ( |
30 | | - fc.getTarget().getName() = "__builtin_alloca" |
| 29 | +/** A call to `alloca` in one of its forms. */ |
| 30 | +class AllocaCall extends FunctionCall { |
| 31 | + AllocaCall() { |
| 32 | + this.getTarget().getName() = "__builtin_alloca" |
| 33 | + or |
| 34 | + (this.getTarget().getName() = "_alloca" or this.getTarget().getName() = "_malloca") and |
| 35 | + this.getTarget().getADeclarationEntry().getFile().getBaseName() = "malloc.h" |
| 36 | + } |
| 37 | +} |
| 38 | + |
| 39 | +/** |
| 40 | + * A loop that contains an `alloca` call. |
| 41 | + */ |
| 42 | +class LoopWithAlloca extends Stmt { |
| 43 | + LoopWithAlloca() { this = getAnEnclosingLoopOfExpr(any(AllocaCall ac)) } |
| 44 | + |
| 45 | + /** Get an `alloca` call inside this loop. It may be in a nested loop. */ |
| 46 | + AllocaCall getAnAllocaCall() { this = getAnEnclosingLoopOfExpr(result) } |
| 47 | + |
| 48 | + /** |
| 49 | + * Holds if the condition of this loop will only be true if `e` is `truth`. |
| 50 | + * For example, if the loop condition is `a == 0 && b`, then |
| 51 | + * `conditionRequires(a, false)` and `conditionRequires(b, true)`. |
| 52 | + */ |
| 53 | + private predicate conditionRequires(Expr e, boolean truth) { |
| 54 | + e = this.(Loop).getCondition() and |
| 55 | + truth = true |
| 56 | + or |
| 57 | + // `e == 0` |
| 58 | + exists(EQExpr eq | |
| 59 | + conditionRequires(eq, truth.booleanNot()) and |
| 60 | + eq.getAnOperand().getValue().toInt() = 0 and |
| 61 | + e = eq.getAnOperand() and |
| 62 | + not exists(e.getValue()) |
| 63 | + ) |
| 64 | + or |
| 65 | + // `e != 0` |
| 66 | + exists(NEExpr eq | |
| 67 | + conditionRequires(eq, truth) and |
| 68 | + eq.getAnOperand().getValue().toInt() = 0 and |
| 69 | + e = eq.getAnOperand() and |
| 70 | + not exists(e.getValue()) |
| 71 | + ) |
| 72 | + or |
| 73 | + // `(bool)e == true` |
| 74 | + exists(EQExpr eq | |
| 75 | + conditionRequires(eq, truth) and |
| 76 | + eq.getAnOperand().getValue().toInt() = 1 and |
| 77 | + e = eq.getAnOperand() and |
| 78 | + e.getType().getUnspecifiedType() instanceof BoolType and |
| 79 | + not exists(e.getValue()) |
| 80 | + ) |
| 81 | + or |
| 82 | + // `(bool)e != true` |
| 83 | + exists(NEExpr eq | |
| 84 | + conditionRequires(eq, truth.booleanNot()) and |
| 85 | + eq.getAnOperand().getValue().toInt() = 1 and |
| 86 | + e = eq.getAnOperand() and |
| 87 | + e.getType().getUnspecifiedType() instanceof BoolType and |
| 88 | + not exists(e.getValue()) |
| 89 | + ) |
| 90 | + or |
| 91 | + exists(NotExpr notExpr | |
| 92 | + conditionRequires(notExpr, truth.booleanNot()) and |
| 93 | + e = notExpr.getOperand() |
| 94 | + ) |
| 95 | + or |
| 96 | + // If the e of `this` requires `andExpr` to be true, then it |
| 97 | + // requires both of its operand to be true as well. |
| 98 | + exists(LogicalAndExpr andExpr | |
| 99 | + truth = true and |
| 100 | + conditionRequires(andExpr, truth) and |
| 101 | + e = andExpr.getAnOperand() |
| 102 | + ) |
| 103 | + or |
| 104 | + // Dually, if the e of `this` requires `orExpr` to be false, then |
| 105 | + // it requires both of its operand to be false as well. |
| 106 | + exists(LogicalOrExpr orExpr | |
| 107 | + truth = false and |
| 108 | + conditionRequires(orExpr, truth) and |
| 109 | + e = orExpr.getAnOperand() |
| 110 | + ) |
| 111 | + } |
| 112 | + |
| 113 | + /** |
| 114 | + * Holds if the condition of this loop will only be true if `e` relates to |
| 115 | + * `value` as `dir`. We don't keep track of whether the equality is strict |
| 116 | + * since this predicate is only used to heuristically determine whether |
| 117 | + * there's a reasonably tight upper bound on the number of loop iterations. |
| 118 | + * |
| 119 | + * For example, if the loop condition is `a < 2 && b`, then |
| 120 | + * `conditionRequiresInequality(a, 2, Lesser())`. |
| 121 | + */ |
| 122 | + private predicate conditionRequiresInequality(Expr e, int value, RelationDirection dir) { |
| 123 | + exists(RelationalOperation rel, Expr constant, boolean branch | |
| 124 | + this.conditionRequires(rel, branch) and |
| 125 | + relOpWithSwapAndNegate(rel, e.getFullyConverted(), constant, dir, _, branch) and |
| 126 | + value = constant.getValue().toInt() and |
| 127 | + not exists(e.getValue()) |
| 128 | + ) |
| 129 | + or |
| 130 | + // Because we're not worried about off-by-one, it's not important whether |
| 131 | + // the `CrementOperation` is a {pre,post}-{inc,dec}rement. |
| 132 | + exists(CrementOperation inc | |
| 133 | + this.conditionRequiresInequality(inc, value, dir) and |
| 134 | + e = inc.getOperand() |
| 135 | + ) |
| 136 | + } |
| 137 | + |
| 138 | + /** |
| 139 | + * Gets a variable that's restricted by `conditionRequires` or |
| 140 | + * `conditionRequiresInequality`. |
| 141 | + */ |
| 142 | + private Variable getAControllingVariable() { |
| 143 | + conditionRequires(result.getAnAccess(), _) |
31 | 144 | or |
| 145 | + conditionRequiresInequality(result.getAnAccess(), _, _) |
| 146 | + } |
| 147 | + |
| 148 | + /** |
| 149 | + * Gets a `VariableAccess` that changes `var` inside the loop body, where |
| 150 | + * `var` is a controlling variable of this loop. |
| 151 | + */ |
| 152 | + private VariableAccess getAControllingVariableUpdate(Variable var) { |
| 153 | + var = result.getTarget() and |
| 154 | + var = this.getAControllingVariable() and |
| 155 | + this = getAnEnclosingLoopOfExpr(result) and |
| 156 | + result.isUsedAsLValue() |
| 157 | + } |
| 158 | + |
| 159 | + /** |
| 160 | + * Holds if there is a control-flow path from the condition of this loop to |
| 161 | + * `node` that doesn't update `var`, where `var` is a controlling variable of |
| 162 | + * this loop. The path has to stay within the loop. The path will start at |
| 163 | + * the successor of the loop condition. If the path reaches all the way back |
| 164 | + * to the loop condition, then it's possible to go around the loop without |
| 165 | + * updating `var`. |
| 166 | + */ |
| 167 | + private predicate conditionReachesWithoutUpdate(Variable var, ControlFlowNode node) { |
| 168 | + // Don't leave the loop. It might cause us to leave the scope of `var` |
| 169 | + (node instanceof Stmt implies this = getAnEnclosingLoopOfStmt(node)) and |
32 | 170 | ( |
33 | | - (fc.getTarget().getName() = "_alloca" or fc.getTarget().getName() = "_malloca") and |
34 | | - fc.getTarget().getADeclarationEntry().getFile().getBaseName() = "malloc.h" |
| 171 | + node = this.(Loop).getCondition().getASuccessor() and |
| 172 | + var = this.getAControllingVariable() |
| 173 | + or |
| 174 | + this.conditionReachesWithoutUpdate(var, node.getAPredecessor()) and |
| 175 | + not node = this.getAControllingVariableUpdate(var) |
| 176 | + ) |
| 177 | + } |
| 178 | + |
| 179 | + /** |
| 180 | + * Holds if all paths around the loop will update `var`, where `var` is a |
| 181 | + * controlling variable of this loop. |
| 182 | + */ |
| 183 | + private predicate hasMandatoryUpdate(Variable var) { |
| 184 | + not this.conditionReachesWithoutUpdate(var, this.(Loop).getCondition()) |
| 185 | + } |
| 186 | + |
| 187 | + /** |
| 188 | + * Gets a definition that may be the most recent definition of the |
| 189 | + * controlling variable `var` before this loop. |
| 190 | + */ |
| 191 | + private DataFlow::Node getAPrecedingDef(Variable var) { |
| 192 | + exists(VariableAccess va | |
| 193 | + va = var.getAnAccess() and |
| 194 | + this.conditionRequiresInequality(va, _, _) and |
| 195 | + DataFlow::localFlow(result, DataFlow::exprNode(va)) and |
| 196 | + // A source is outside the loop if it's not inside the loop |
| 197 | + not exists(Expr e | |
| 198 | + e = result.asExpr() |
| 199 | + or |
| 200 | + e = result.asDefiningArgument() |
| 201 | + | |
| 202 | + this = getAnEnclosingLoopOfExpr(e) |
| 203 | + ) |
35 | 204 | ) |
36 | | - ) and |
37 | | - not l.(DoStmt).getCondition().getValue() = "0" |
38 | | -select fc, "Stack allocation is inside a $@ and could lead to stack overflow.", l, l.toString() |
| 205 | + } |
| 206 | + |
| 207 | + /** |
| 208 | + * Gets a number that may be the most recent value assigned to the |
| 209 | + * controlling variable `var` before this loop. |
| 210 | + */ |
| 211 | + private int getAControllingVarInitialValue(Variable var, DataFlow::Node source) { |
| 212 | + source = this.getAPrecedingDef(var) and |
| 213 | + result = source.asExpr().getValue().toInt() |
| 214 | + } |
| 215 | + |
| 216 | + /** |
| 217 | + * Holds if the most recent definition of `var` before this loop may assign a |
| 218 | + * value that is not a compile-time constant. |
| 219 | + */ |
| 220 | + private predicate controllingVarHasUnknownInitialValue(Variable var) { |
| 221 | + // A definition without a constant value was reached |
| 222 | + exists(DataFlow::Node source | |
| 223 | + source = this.getAPrecedingDef(var) and |
| 224 | + not exists(this.getAControllingVarInitialValue(var, source)) |
| 225 | + ) |
| 226 | + } |
| 227 | + |
| 228 | + /** |
| 229 | + * Gets the least possible value that the controlling variable `var` may have |
| 230 | + * before this loop, if such a value can be deduced. |
| 231 | + */ |
| 232 | + private int getMinPrecedingDef(Variable var) { |
| 233 | + not this.controllingVarHasUnknownInitialValue(var) and |
| 234 | + result = min(this.getAControllingVarInitialValue(var, _)) |
| 235 | + or |
| 236 | + this.controllingVarHasUnknownInitialValue(var) and |
| 237 | + var.getType().(IntegralType).isUnsigned() and |
| 238 | + result = 0 |
| 239 | + } |
| 240 | + |
| 241 | + /** |
| 242 | + * Gets the greatest possible value that the controlling variable `var` may |
| 243 | + * have before this loop, if such a value can be deduced. |
| 244 | + */ |
| 245 | + private int getMaxPrecedingDef(Variable var) { |
| 246 | + not this.controllingVarHasUnknownInitialValue(var) and |
| 247 | + result = max(this.getAControllingVarInitialValue(var, _)) |
| 248 | + } |
| 249 | + |
| 250 | + /** |
| 251 | + * Holds if this loop has a "small" number of iterations. The meaning of |
| 252 | + * "small" should be such that the loop wouldn't be unreasonably large if |
| 253 | + * manually unrolled. |
| 254 | + */ |
| 255 | + predicate isTightlyBounded() { |
| 256 | + exists(Variable var | this.hasMandatoryUpdate(var) | |
| 257 | + this.conditionRequires(var.getAnAccess(), false) and |
| 258 | + forall(VariableAccess update | update = this.getAControllingVariableUpdate(var) | |
| 259 | + exists(AssignExpr assign | |
| 260 | + assign.getLValue() = update and |
| 261 | + assign.getRValue().getValue().toInt() != 0 |
| 262 | + ) |
| 263 | + ) |
| 264 | + or |
| 265 | + this.conditionRequires(var.getAnAccess(), true) and |
| 266 | + forall(VariableAccess update | update = this.getAControllingVariableUpdate(var) | |
| 267 | + exists(AssignExpr assign | |
| 268 | + assign.getLValue() = update and |
| 269 | + assign.getRValue().getValue().toInt() = 0 |
| 270 | + ) |
| 271 | + ) |
| 272 | + or |
| 273 | + exists(int bound | |
| 274 | + this.conditionRequiresInequality(var.getAnAccess(), bound, Lesser()) and |
| 275 | + bound - this.getMinPrecedingDef(var) <= 16 and |
| 276 | + forall(VariableAccess update | update = this.getAControllingVariableUpdate(var) | |
| 277 | + // var++; |
| 278 | + // ++var; |
| 279 | + exists(IncrementOperation inc | inc.getOperand() = update) |
| 280 | + or |
| 281 | + // var += positive_number; |
| 282 | + exists(AssignAddExpr aa | |
| 283 | + aa.getLValue() = update and |
| 284 | + aa.getRValue().getValue().toInt() > 0 |
| 285 | + ) |
| 286 | + or |
| 287 | + // var = var + positive_number; |
| 288 | + // var = positive_number + var; |
| 289 | + exists(AssignExpr assign, AddExpr add | |
| 290 | + assign.getLValue() = update and |
| 291 | + assign.getRValue() = add and |
| 292 | + add.getAnOperand() = var.getAnAccess() and |
| 293 | + add.getAnOperand().getValue().toInt() > 0 |
| 294 | + ) |
| 295 | + ) |
| 296 | + ) |
| 297 | + or |
| 298 | + exists(int bound | |
| 299 | + this.conditionRequiresInequality(var.getAnAccess(), bound, Greater()) and |
| 300 | + this.getMaxPrecedingDef(var) - bound <= 16 and |
| 301 | + forall(VariableAccess update | update = this.getAControllingVariableUpdate(var) | |
| 302 | + // var--; |
| 303 | + // --var; |
| 304 | + exists(DecrementOperation inc | inc.getOperand() = update) |
| 305 | + or |
| 306 | + // var -= positive_number; |
| 307 | + exists(AssignSubExpr aa | |
| 308 | + aa.getLValue() = update and |
| 309 | + aa.getRValue().getValue().toInt() > 0 |
| 310 | + ) |
| 311 | + or |
| 312 | + // var = var - positive_number; |
| 313 | + exists(AssignExpr assign, SubExpr add | |
| 314 | + assign.getLValue() = update and |
| 315 | + assign.getRValue() = add and |
| 316 | + add.getLeftOperand() = var.getAnAccess() and |
| 317 | + add.getRightOperand().getValue().toInt() > 0 |
| 318 | + ) |
| 319 | + ) |
| 320 | + ) |
| 321 | + ) |
| 322 | + } |
| 323 | +} |
| 324 | + |
| 325 | +from LoopWithAlloca l |
| 326 | +where |
| 327 | + not l.(DoStmt).getCondition().getValue() = "0" and |
| 328 | + not l.isTightlyBounded() |
| 329 | +select l.getAnAllocaCall(), "Stack allocation is inside a $@ and could lead to stack overflow.", l, |
| 330 | + l.toString() |
0 commit comments