50
50
overlay [ local?]
51
51
module ;
52
52
53
+ private import codeql.controlflow.BasicBlock as BB
53
54
private import codeql.util.Boolean
54
55
private import codeql.util.Location
55
56
private import codeql.util.Unit
56
57
57
- signature module InputSig< LocationSig Location> {
58
- class SuccessorType {
59
- /** Gets a textual representation of this successor type. */
60
- string toString ( ) ;
61
- }
58
+ signature class TypSig ;
62
59
60
+ signature module SuccessorTypesSig< TypSig SuccessorType> {
63
61
class ExceptionSuccessor extends SuccessorType ;
64
62
65
63
class ConditionalSuccessor extends SuccessorType {
@@ -70,61 +68,12 @@ signature module InputSig<LocationSig Location> {
70
68
class BooleanSuccessor extends ConditionalSuccessor ;
71
69
72
70
class NullnessSuccessor extends ConditionalSuccessor ;
71
+ }
73
72
74
- /** A control flow node. */
75
- class ControlFlowNode {
76
- /** Gets a textual representation of this control flow node. */
77
- string toString ( ) ;
78
-
79
- /** Gets the location of this control flow node. */
80
- Location getLocation ( ) ;
81
- }
82
-
73
+ signature module InputSig< LocationSig Location, TypSig ControlFlowNode, TypSig BasicBlock> {
83
74
/** A control flow node indicating normal termination of a callable. */
84
75
class NormalExitNode extends ControlFlowNode ;
85
76
86
- /**
87
- * A basic block, that is, a maximal straight-line sequence of control flow nodes
88
- * without branches or joins.
89
- */
90
- class BasicBlock {
91
- /** Gets a textual representation of this basic block. */
92
- string toString ( ) ;
93
-
94
- /** Gets the `i`th node in this basic block. */
95
- ControlFlowNode getNode ( int i ) ;
96
-
97
- /** Gets the last control flow node in this basic block. */
98
- ControlFlowNode getLastNode ( ) ;
99
-
100
- /** Gets the length of this basic block. */
101
- int length ( ) ;
102
-
103
- /** Gets the location of this basic block. */
104
- Location getLocation ( ) ;
105
-
106
- BasicBlock getASuccessor ( SuccessorType t ) ;
107
-
108
- predicate dominates ( BasicBlock bb ) ;
109
-
110
- predicate strictlyDominates ( BasicBlock bb ) ;
111
- }
112
-
113
- /**
114
- * Holds if `bb1` has `bb2` as a direct successor and the edge between `bb1`
115
- * and `bb2` is a dominating edge.
116
- *
117
- * An edge `(bb1, bb2)` is dominating if there exists a basic block that can
118
- * only be reached from the entry block by going through `(bb1, bb2)`. This
119
- * implies that `(bb1, bb2)` dominates its endpoint `bb2`. I.e., `bb2` can
120
- * only be reached from the entry block by going via `(bb1, bb2)`.
121
- *
122
- * This is a necessary and sufficient condition for an edge to dominate some
123
- * block, and therefore `dominatingEdge(bb1, bb2) and bb2.dominates(bb3)`
124
- * means that the edge `(bb1, bb2)` dominates `bb3`.
125
- */
126
- predicate dominatingEdge ( BasicBlock bb1 , BasicBlock bb2 ) ;
127
-
128
77
class AstNode {
129
78
/** Gets a textual representation of this AST node. */
130
79
string toString ( ) ;
@@ -254,7 +203,15 @@ signature module InputSig<LocationSig Location> {
254
203
}
255
204
256
205
/** Provides guards-related predicates and classes. */
257
- module Make< LocationSig Location, InputSig< Location > Input> {
206
+ module Make<
207
+ LocationSig Location, BB:: CfgSig< Location > Cfg,
208
+ SuccessorTypesSig< Cfg:: SuccessorType > SuccessorTypes,
209
+ InputSig< Location , Cfg:: ControlFlowNode , Cfg:: BasicBlock > Input>
210
+ {
211
+ private module Cfg_ = Cfg;
212
+
213
+ private import Cfg_
214
+ private import SuccessorTypes
258
215
private import Input
259
216
260
217
private newtype TAbstractSingleValue =
0 commit comments