5050overlay [ local?]
5151module ;
5252
53+ private import codeql.controlflow.BasicBlock as BB
5354private import codeql.util.Boolean
5455private import codeql.util.Location
5556private import codeql.util.Unit
5657
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 ;
6259
60+ signature module SuccessorTypesSig< TypSig SuccessorType> {
6361 class ExceptionSuccessor extends SuccessorType ;
6462
6563 class ConditionalSuccessor extends SuccessorType {
@@ -70,61 +68,12 @@ signature module InputSig<LocationSig Location> {
7068 class BooleanSuccessor extends ConditionalSuccessor ;
7169
7270 class NullnessSuccessor extends ConditionalSuccessor ;
71+ }
7372
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> {
8374 /** A control flow node indicating normal termination of a callable. */
8475 class NormalExitNode extends ControlFlowNode ;
8576
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-
12877 class AstNode {
12978 /** Gets a textual representation of this AST node. */
13079 string toString ( ) ;
@@ -254,7 +203,15 @@ signature module InputSig<LocationSig Location> {
254203}
255204
256205/** 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
258215 private import Input
259216
260217 private newtype TAbstractSingleValue =
0 commit comments