@@ -9,10 +9,7 @@ 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 {
13- /** Gets a textual representation of this basic block. */
14- string toString ( ) ;
15- }
12+ class BasicBlock ;
1613
1714 /**
1815 * Gets the basic block that immediately dominates basic block `bb`, if any.
@@ -46,10 +43,7 @@ signature module InputSig {
4643 class ExitBasicBlock extends BasicBlock ;
4744
4845 /** 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 ;
5347
5448 /**
5549 * Holds if the `i`th node of basic block `bb` is a (potential) write to source
@@ -852,6 +846,8 @@ module Make<InputSig Input> {
852846 }
853847
854848 /** Provides a set of consistency queries. */
849+ // TODO: Make these `query` predicates once class signatures are supported
850+ // (`SourceVariable` and `BasicBlock` must have `toString`)
855851 module Consistency {
856852 /** A definition that is relevant for the consistency queries. */
857853 abstract class RelevantDefinition extends Definition {
@@ -862,27 +858,27 @@ module Make<InputSig Input> {
862858 }
863859
864860 /** 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 ) {
866862 ssaDefReachesRead ( v , def , bb , i ) and
867863 not exists ( unique( Definition def0 | ssaDefReachesRead ( v , def0 , bb , i ) ) )
868864 }
869865
870866 /** 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 ) {
872868 variableRead ( bb , i , v , _) and
873869 not ssaDefReachesRead ( v , _, bb , i )
874870 }
875871
876872 /** Holds if a definition cannot reach a read. */
877- query predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
873+ predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
878874 v = def .getSourceVariable ( ) and
879875 not ssaDefReachesRead ( _, def , _, _) and
880876 not phiHasInputFromBlock ( _, def , _) and
881877 not uncertainWriteDefinitionInput ( _, def )
882878 }
883879
884880 /** 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 ) {
886882 exists ( BasicBlock bbDef , int iDef | def .definesAt ( v , bbDef , iDef ) |
887883 ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
888884 ( bb != bbDef or i < iDef )
0 commit comments