|
| 1 | +private import codeql.util.Location |
| 2 | + |
| 3 | +/** Provides language-specific control flow parameters. */ |
| 4 | +signature module InputSig<LocationSig Location> { |
| 5 | + /** |
| 6 | + * A node in the control flow graph. |
| 7 | + */ |
| 8 | + class Node { |
| 9 | + /** Gets a textual representation of this element. */ |
| 10 | + string toString(); |
| 11 | + |
| 12 | + /** Gets the location of this node. */ |
| 13 | + Location getLocation(); |
| 14 | + } |
| 15 | + |
| 16 | + class CallNode extends Node; |
| 17 | + |
| 18 | + class Callable; |
| 19 | + |
| 20 | + predicate edge(Node n1, Node n2); |
| 21 | + |
| 22 | + predicate callTarget(CallNode call, Callable target); |
| 23 | + |
| 24 | + predicate flowEntry(Callable c, Node entry); |
| 25 | + |
| 26 | + predicate flowExit(Callable c, Node exitNode); |
| 27 | + |
| 28 | + Callable getEnclosingCallable(Node n); |
| 29 | + |
| 30 | + predicate hiddenNode(Node n); |
| 31 | + |
| 32 | + class Split { |
| 33 | + string toString(); |
| 34 | + |
| 35 | + Location getLocation(); |
| 36 | + |
| 37 | + predicate entry(Node n1, Node n2); |
| 38 | + |
| 39 | + predicate exit(Node n1, Node n2); |
| 40 | + |
| 41 | + predicate blocked(Node n1, Node n2); |
| 42 | + } |
| 43 | +} |
| 44 | + |
| 45 | +private module Configs<LocationSig Location, InputSig<Location> Lang> { |
| 46 | + private import Lang |
| 47 | + |
| 48 | + /** An input configuration for control flow. */ |
| 49 | + signature module ConfigSig { |
| 50 | + /** Holds if `source` is a relevant control flow source. */ |
| 51 | + predicate isSource(Node src); |
| 52 | + |
| 53 | + /** Holds if `sink` is a relevant control flow sink. */ |
| 54 | + predicate isSink(Node sink); |
| 55 | + |
| 56 | + /** Holds if control flow should not proceed along the edge `n1 -> n2`. */ |
| 57 | + default predicate isBarrierEdge(Node n1, Node n2) { none() } |
| 58 | + |
| 59 | + /** |
| 60 | + * Holds if control flow through `node` is prohibited. This completely |
| 61 | + * removes `node` from the control flow graph. |
| 62 | + */ |
| 63 | + default predicate isBarrier(Node n) { none() } |
| 64 | + } |
| 65 | + |
| 66 | + /** An input configuration for control flow using a label. */ |
| 67 | + signature module LabelConfigSig { |
| 68 | + class Label; |
| 69 | + |
| 70 | + /** |
| 71 | + * Holds if `source` is a relevant control flow source with the given |
| 72 | + * initial `l`. |
| 73 | + */ |
| 74 | + predicate isSource(Node src, Label l); |
| 75 | + |
| 76 | + /** |
| 77 | + * Holds if `sink` is a relevant control flow sink accepting `l`. |
| 78 | + */ |
| 79 | + predicate isSink(Node sink, Label l); |
| 80 | + |
| 81 | + /** |
| 82 | + * Holds if control flow should not proceed along the edge `n1 -> n2` when |
| 83 | + * the label is `l`. |
| 84 | + */ |
| 85 | + default predicate isBarrierEdge(Node n1, Node n2, Label l) { none() } |
| 86 | + |
| 87 | + /** |
| 88 | + * Holds if control flow through `node` is prohibited when the label |
| 89 | + * is `l`. |
| 90 | + */ |
| 91 | + default predicate isBarrier(Node n, Label l) { none() } |
| 92 | + } |
| 93 | +} |
| 94 | + |
| 95 | +module ControlFlowMake<LocationSig Location, InputSig<Location> Lang> { |
| 96 | + private import Lang |
| 97 | + private import internal.ControlFlowImpl::MakeImpl<Location, Lang> |
| 98 | + import Configs<Location, Lang> |
| 99 | + |
| 100 | + /** |
| 101 | + * The output of a global control flow computation. |
| 102 | + */ |
| 103 | + signature module GlobalFlowSig { |
| 104 | + /** |
| 105 | + * A `Node` that is reachable from a source, and which can reach a sink. |
| 106 | + */ |
| 107 | + class PathNode; |
| 108 | + |
| 109 | + /** |
| 110 | + * Holds if control can flow from `source` to `sink`. |
| 111 | + * |
| 112 | + * The corresponding paths are generated from the end-points and the graph |
| 113 | + * included in the module `PathGraph`. |
| 114 | + */ |
| 115 | + predicate flowPath(PathNode source, PathNode sink); |
| 116 | + } |
| 117 | + |
| 118 | + /** |
| 119 | + * Constructs a global control flow computation. |
| 120 | + */ |
| 121 | + module Global<ConfigSig Config> implements GlobalFlowSig { |
| 122 | + private module C implements FullConfigSig { |
| 123 | + import DefaultLabel<Config> |
| 124 | + import Config |
| 125 | + } |
| 126 | + |
| 127 | + import Impl<C> |
| 128 | + } |
| 129 | + |
| 130 | + /** |
| 131 | + * Constructs a global control flow computation using a flow label. |
| 132 | + */ |
| 133 | + module GlobalWithLabel<LabelConfigSig Config> implements GlobalFlowSig { |
| 134 | + private module C implements FullConfigSig { |
| 135 | + import Config |
| 136 | + } |
| 137 | + |
| 138 | + import Impl<C> |
| 139 | + } |
| 140 | +} |
0 commit comments