|
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 | + } |
| 38 | + |
| 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 | + // The base case of `reachable` is factored out for performance. If it's |
| 48 | + // written in-line in `reachable`, the compiler inserts a `n instanceof |
| 49 | + // ControlFlowNode` check because the `not ... and not ...` case doesn't |
| 50 | + // otherwise bind `n`. The problem is that this check is inserted at the |
| 51 | + // outermost level of this predicate, so it covers all cases including the |
| 52 | + // recursive case. The optimizer doesn't eliminate the check even though it's |
| 53 | + // redundant, and having the check leads to needless extra computation and a |
| 54 | + // risk of bad join orders. |
| 55 | + private predicate reachableBaseCase(ControlFlowNode n) { |
| 56 | + exists(Function f | f.getEntryPoint() = n) |
| 57 | + or |
| 58 | + // Okay to use successors_extended directly here |
| 59 | + (not successors_extended(_,n) and not successors_extended(n,_)) |
| 60 | + or |
| 61 | + n instanceof Handler |
| 62 | + } |
| 63 | + |
| 64 | + /** |
| 65 | + * Holds if the control-flow node `n` is reachable, meaning that either |
| 66 | + * it is an entry point, or there exists a path in the control-flow |
| 67 | + * graph of its function that connects an entry point to it. |
| 68 | + * Compile-time constant conditions are taken into account, so that |
| 69 | + * the call to `f` is not reachable in `if (0) f();` even if the |
| 70 | + * `if` statement as a whole is reachable. |
| 71 | + */ |
| 72 | + cached |
| 73 | + predicate reachable(ControlFlowNode n) |
| 74 | + { |
| 75 | + reachableBaseCase(n) |
| 76 | + or |
| 77 | + reachable(n.getAPredecessor()) |
| 78 | + } |
| 79 | + |
| 80 | + /** Holds if `condition` always evaluates to a nonzero value. */ |
| 81 | + cached |
| 82 | + predicate conditionAlwaysTrue(Expr condition) { |
| 83 | + conditionAlways(condition, true) |
| 84 | + } |
| 85 | + |
| 86 | + /** Holds if `condition` always evaluates to zero. */ |
| 87 | + cached |
| 88 | + predicate conditionAlwaysFalse(Expr condition) { |
| 89 | + conditionAlways(condition, false) |
| 90 | + or |
| 91 | + // If a loop condition evaluates to false upon entry, it will always |
| 92 | + // be false |
| 93 | + loopConditionAlwaysUponEntry(_, condition, false) |
| 94 | + } |
| 95 | + |
| 96 | + /** |
| 97 | + * The condition `condition` for the loop `loop` is provably `true` upon entry. |
| 98 | + * That is, at least one iteration of the loop is guaranteed. |
| 99 | + */ |
| 100 | + cached |
| 101 | + predicate loopConditionAlwaysTrueUponEntry(ControlFlowNode loop, Expr condition) { |
| 102 | + loopConditionAlwaysUponEntry(loop, condition, true) |
| 103 | + } |
| 104 | + } |
| 105 | +} |
4 | 106 |
|
5 | | -/** A call to a function known not to return. */ |
6 | | -predicate aborting(FunctionCall c) { |
7 | | - not potentiallyReturningFunctionCall(c) |
| 107 | +private predicate conditionAlways(Expr condition, boolean b) { |
| 108 | + exists(ConditionEvaluator x, int val | |
| 109 | + val = x.getValue(condition) | |
| 110 | + val != 0 and b = true |
| 111 | + or |
| 112 | + val = 0 and b = false |
| 113 | + ) |
8 | 114 | } |
9 | 115 |
|
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) |
| 116 | +private predicate loopConditionAlwaysUponEntry(ControlFlowNode loop, Expr condition, boolean b) { |
| 117 | + exists(LoopEntryConditionEvaluator x, int val | |
| 118 | + x.isLoopEntry(condition, loop) and |
| 119 | + val = x.getValue(condition) | |
| 120 | + val != 0 and b = true |
| 121 | + or |
| 122 | + val = 0 and b = false |
| 123 | + ) |
16 | 124 | } |
17 | 125 |
|
18 | 126 | /** |
@@ -201,22 +309,6 @@ private predicate possiblePredecessor(Node pred) { |
201 | 309 | potentiallyReturningFunctionCall(pred) |
202 | 310 | } |
203 | 311 |
|
204 | | -/** |
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. |
208 | | - */ |
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) |
218 | | -} |
219 | | - |
220 | 312 | private predicate compileTimeConstantInt(Expr e, int val) { |
221 | 313 | val = e.getFullyConverted().getValue().toInt() and |
222 | 314 | not e instanceof StringLiteral and |
|
0 commit comments