@@ -9,7 +9,10 @@ signature module InputSig {
9
9
* A basic block, that is, a maximal straight-line sequence of control flow nodes
10
10
* without branches or joins.
11
11
*/
12
- class BasicBlock ;
12
+ class BasicBlock {
13
+ /** Gets a textual representation of this basic block. */
14
+ string toString ( ) ;
15
+ }
13
16
14
17
/**
15
18
* Gets the basic block that immediately dominates basic block `bb`, if any.
@@ -43,7 +46,10 @@ signature module InputSig {
43
46
class ExitBasicBlock extends BasicBlock ;
44
47
45
48
/** A variable that can be SSA converted. */
46
- class SourceVariable ;
49
+ class SourceVariable {
50
+ /** Gets a textual representation of this variable. */
51
+ string toString ( ) ;
52
+ }
47
53
48
54
/**
49
55
* Holds if the `i`th node of basic block `bb` is a (potential) write to source
@@ -846,8 +852,6 @@ module Make<InputSig Input> {
846
852
}
847
853
848
854
/** Provides a set of consistency queries. */
849
- // TODO: Make these `query` predicates once class signatures are supported
850
- // (`SourceVariable` and `BasicBlock` must have `toString`)
851
855
module Consistency {
852
856
/** A definition that is relevant for the consistency queries. */
853
857
abstract class RelevantDefinition extends Definition {
@@ -858,27 +862,27 @@ module Make<InputSig Input> {
858
862
}
859
863
860
864
/** Holds if a read can be reached from multiple definitions. */
861
- predicate nonUniqueDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
865
+ query predicate nonUniqueDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
862
866
ssaDefReachesRead ( v , def , bb , i ) and
863
867
not exists ( unique( Definition def0 | ssaDefReachesRead ( v , def0 , bb , i ) ) )
864
868
}
865
869
866
870
/** Holds if a read cannot be reached from a definition. */
867
- predicate readWithoutDef ( SourceVariable v , BasicBlock bb , int i ) {
871
+ query predicate readWithoutDef ( SourceVariable v , BasicBlock bb , int i ) {
868
872
variableRead ( bb , i , v , _) and
869
873
not ssaDefReachesRead ( v , _, bb , i )
870
874
}
871
875
872
876
/** Holds if a definition cannot reach a read. */
873
- predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
877
+ query predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
874
878
v = def .getSourceVariable ( ) and
875
879
not ssaDefReachesRead ( _, def , _, _) and
876
880
not phiHasInputFromBlock ( _, def , _) and
877
881
not uncertainWriteDefinitionInput ( _, def )
878
882
}
879
883
880
884
/** Holds if a read is not dominated by a definition. */
881
- predicate notDominatedByDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
885
+ query predicate notDominatedByDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
882
886
exists ( BasicBlock bbDef , int iDef | def .definesAt ( v , bbDef , iDef ) |
883
887
ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
884
888
( bb != bbDef or i < iDef )
0 commit comments