@@ -9,7 +9,10 @@ signature module InputSig {
99 * A basic block, that is, a maximal straight-line sequence of control flow nodes
1010 * without branches or joins.
1111 */
12- class BasicBlock ;
12+ class BasicBlock {
13+ /** Gets a textual representation of this basic block. */
14+ string toString ( ) ;
15+ }
1316
1417 /**
1518 * Gets the basic block that immediately dominates basic block `bb`, if any.
@@ -43,7 +46,10 @@ signature module InputSig {
4346 class ExitBasicBlock extends BasicBlock ;
4447
4548 /** 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+ }
4753
4854 /**
4955 * Holds if the `i`th node of basic block `bb` is a (potential) write to source
@@ -846,8 +852,6 @@ module Make<InputSig Input> {
846852 }
847853
848854 /** Provides a set of consistency queries. */
849- // TODO: Make these `query` predicates once class signatures are supported
850- // (`SourceVariable` and `BasicBlock` must have `toString`)
851855 module Consistency {
852856 /** A definition that is relevant for the consistency queries. */
853857 abstract class RelevantDefinition extends Definition {
@@ -858,27 +862,27 @@ module Make<InputSig Input> {
858862 }
859863
860864 /** 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 ) {
862866 ssaDefReachesRead ( v , def , bb , i ) and
863867 not exists ( unique( Definition def0 | ssaDefReachesRead ( v , def0 , bb , i ) ) )
864868 }
865869
866870 /** 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 ) {
868872 variableRead ( bb , i , v , _) and
869873 not ssaDefReachesRead ( v , _, bb , i )
870874 }
871875
872876 /** Holds if a definition cannot reach a read. */
873- predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
877+ query predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
874878 v = def .getSourceVariable ( ) and
875879 not ssaDefReachesRead ( _, def , _, _) and
876880 not phiHasInputFromBlock ( _, def , _) and
877881 not uncertainWriteDefinitionInput ( _, def )
878882 }
879883
880884 /** 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 ) {
882886 exists ( BasicBlock bbDef , int iDef | def .definesAt ( v , bbDef , iDef ) |
883887 ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
884888 ( bb != bbDef or i < iDef )
0 commit comments