|
1 | 1 | import cpp |
2 | 2 | private import PrimitiveBasicBlocks |
3 | 3 | private class Node = ControlFlowNodeBase; |
| 4 | +import Cached |
| 5 | + |
| 6 | +cached |
| 7 | +private module Cached { |
| 8 | + /** A call to a function known not to return. */ |
| 9 | + cached |
| 10 | + predicate aborting(FunctionCall c) { |
| 11 | + not potentiallyReturningFunctionCall(c) |
| 12 | + } |
| 13 | + |
| 14 | + /** |
| 15 | + * Functions that are known not to return. This is normally because the function |
| 16 | + * exits the program or longjmps to another location. |
| 17 | + */ |
| 18 | + cached |
| 19 | + predicate abortingFunction(Function f) { |
| 20 | + not potentiallyReturningFunction(f) |
| 21 | + } |
| 22 | + |
| 23 | + /** |
| 24 | + * An adapted version of the `successors_extended` relation that excludes |
| 25 | + * impossible control-flow edges - flow will never occur along these |
| 26 | + * edges, so it is safe (and indeed sensible) to remove them. |
| 27 | + */ |
| 28 | + cached predicate successors_adapted(Node pred, Node succ) { |
| 29 | + successors_extended(pred, succ) |
| 30 | + and possiblePredecessor(pred) |
| 31 | + and not impossibleFalseEdge(pred, succ) |
| 32 | + and not impossibleTrueEdge(pred, succ) |
| 33 | + and not impossibleSwitchEdge(pred, succ) |
| 34 | + and not impossibleDefaultSwitchEdge(pred, succ) |
| 35 | + and not impossibleFunctionReturn(pred, succ) |
| 36 | + and not getOptions().exprExits(pred) |
| 37 | + } |
4 | 38 |
|
5 | | -/** A call to a function known not to return. */ |
6 | | -predicate aborting(FunctionCall c) { |
7 | | - not potentiallyReturningFunctionCall(c) |
| 39 | + /** |
| 40 | + * Provides predicates that should be exported as if they were top-level |
| 41 | + * predicates in `ControlFlowGraph.qll`. They have to be defined in this file |
| 42 | + * in order to be grouped in a `cached module` with other predicates that |
| 43 | + * must go in the same cached stage. |
| 44 | + */ |
| 45 | + cached |
| 46 | + module ControlFlowGraphPublic { |
| 47 | + /** |
| 48 | + * Holds if the control-flow node `n` is reachable, meaning that either |
| 49 | + * it is an entry point, or there exists a path in the control-flow |
| 50 | + * graph of its function that connects an entry point to it. |
| 51 | + * Compile-time constant conditions are taken into account, so that |
| 52 | + * the call to `f` is not reachable in `if (0) f();` even if the |
| 53 | + * `if` statement as a whole is reachable. |
| 54 | + */ |
| 55 | + cached |
| 56 | + predicate reachable(ControlFlowNode n) |
| 57 | + { |
| 58 | + // Okay to use successors_extended directly here |
| 59 | + reachableRecursive(n) |
| 60 | + or |
| 61 | + (not successors_extended(_,n) and not successors_extended(n,_)) |
| 62 | + } |
| 63 | + |
| 64 | + /** Holds if `condition` always evaluates to a nonzero value. */ |
| 65 | + cached |
| 66 | + predicate conditionAlwaysTrue(Expr condition) { |
| 67 | + conditionAlways(condition, true) |
| 68 | + } |
| 69 | + |
| 70 | + /** Holds if `condition` always evaluates to zero. */ |
| 71 | + cached |
| 72 | + predicate conditionAlwaysFalse(Expr condition) { |
| 73 | + conditionAlways(condition, false) |
| 74 | + or |
| 75 | + // If a loop condition evaluates to false upon entry, it will always |
| 76 | + // be false |
| 77 | + loopConditionAlwaysUponEntry(_, condition, false) |
| 78 | + } |
| 79 | + |
| 80 | + /** |
| 81 | + * The condition `condition` for the loop `loop` is provably `true` upon entry. |
| 82 | + * That is, at least one iteration of the loop is guaranteed. |
| 83 | + */ |
| 84 | + cached |
| 85 | + predicate loopConditionAlwaysTrueUponEntry(ControlFlowNode loop, Expr condition) { |
| 86 | + loopConditionAlwaysUponEntry(loop, condition, true) |
| 87 | + } |
| 88 | + } |
8 | 89 | } |
9 | 90 |
|
10 | | -/** |
11 | | - * Functions that are known not to return. This is normally because the function |
12 | | - * exits the program or longjmps to another location. |
13 | | - */ |
14 | | -predicate abortingFunction(Function f) { |
15 | | - not potentiallyReturningFunction(f) |
| 91 | +private predicate conditionAlways(Expr condition, boolean b) { |
| 92 | + exists(ConditionEvaluator x, int val | |
| 93 | + val = x.getValue(condition) | |
| 94 | + val != 0 and b = true |
| 95 | + or |
| 96 | + val = 0 and b = false |
| 97 | + ) |
| 98 | +} |
| 99 | + |
| 100 | +private predicate loopConditionAlwaysUponEntry(ControlFlowNode loop, Expr condition, boolean b) { |
| 101 | + exists(LoopEntryConditionEvaluator x, int val | |
| 102 | + x.isLoopEntry(condition, loop) and |
| 103 | + val = x.getValue(condition) | |
| 104 | + val != 0 and b = true |
| 105 | + or |
| 106 | + val = 0 and b = false |
| 107 | + ) |
16 | 108 | } |
17 | 109 |
|
18 | 110 | /** |
@@ -61,7 +153,7 @@ private predicate potentiallyReturningFunction(Function f) { |
61 | 153 | nonAnalyzableFunction(f) |
62 | 154 | or |
63 | 155 | // otherwise the exit-point of `f` must be reachable |
64 | | - reachable(f) |
| 156 | + reachableRecursive(f) |
65 | 157 | ) |
66 | 158 | } |
67 | 159 |
|
@@ -202,19 +294,20 @@ private predicate possiblePredecessor(Node pred) { |
202 | 294 | } |
203 | 295 |
|
204 | 296 | /** |
205 | | - * An adapted version of the `successors_extended` relation that excludes |
206 | | - * impossible control-flow edges - flow will never occur along these |
207 | | - * edges, so it is safe (and indeed sensible) to remove them. |
| 297 | + * Holds if the control-flow node `n` is reachable, meaning that either |
| 298 | + * it is an entry point, or there exists a path in the control-flow |
| 299 | + * graph of its function that connects an entry point to it. |
| 300 | + * Compile-time constant conditions are taken into account, so that |
| 301 | + * the call to `f` is not reachable in `if (0) f();` even if the |
| 302 | + * `if` statement as a whole is reachable. |
208 | 303 | */ |
209 | | -cached predicate successors_adapted(Node pred, Node succ) { |
210 | | - successors_extended(pred, succ) |
211 | | - and possiblePredecessor(pred) |
212 | | - and not impossibleFalseEdge(pred, succ) |
213 | | - and not impossibleTrueEdge(pred, succ) |
214 | | - and not impossibleSwitchEdge(pred, succ) |
215 | | - and not impossibleDefaultSwitchEdge(pred, succ) |
216 | | - and not impossibleFunctionReturn(pred, succ) |
217 | | - and not getOptions().exprExits(pred) |
| 304 | +private predicate reachableRecursive(ControlFlowNode n) |
| 305 | +{ |
| 306 | + exists(Function f | f.getEntryPoint() = n) |
| 307 | + or |
| 308 | + n instanceof Handler |
| 309 | + or |
| 310 | + reachableRecursive(n.getAPredecessor()) |
218 | 311 | } |
219 | 312 |
|
220 | 313 | private predicate compileTimeConstantInt(Expr e, int val) { |
|
0 commit comments