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