Robust/src/Analysis/Disjoint/ReachSet.java

   1 package Analysis.Disjoint;
   2
   3 import IR.*;
   4 import IR.Flat.*;
   5 import java.util.*;
   6 import java.io.*;
   7
   8 ///////////////////////////////////////////
   9 //  IMPORTANT
  10 //  This class is an immutable Canonical, so
  11 //
  12 //  0) construct them with a factory pattern
  13 //  to ensure only canonical versions escape
  14 //
  15 //  1) any operation that modifies a Canonical
  16 //  is a static method in the Canonical class
  17 //
  18 //  2) operations that just read this object
  19 //  should be defined here
  20 //
  21 //  3) every Canonical subclass hashCode should
  22 //  throw an error if the hash ever changes
  23 //
  24 ///////////////////////////////////////////
  25
  26 // a reach set is a set of reach states
  27
  28 public class ReachSet extends Canonical {
  29
  30   protected HashSet<ReachState> reachStates;
  31
  32
  33   public static ReachSet factory() {
  34     ReachSet out = new ReachSet();
  35     out = (ReachSet) Canonical.makeCanonical( out );
  36     return out;
  37   }
  38
  39   public static ReachSet factory( ReachState state ) {
  40     assert state != null;
  41     assert state.isCanonical();
  42     ReachSet out = new ReachSet();
  43     out.reachStates.add( state );
  44     out = (ReachSet) Canonical.makeCanonical( out );
  45     return out;
  46   }
  47
  48   protected ReachSet() {
  49     reachStates = new HashSet<ReachState>();
  50   }
  51
  52
  53   public Iterator<ReachState> iterator() {
  54     return reachStates.iterator();
  55   }
  56
  57   public int size() {
  58     return reachStates.size();
  59   }
  60
  61   public boolean isEmpty() {
  62     return reachStates.isEmpty();
  63   }
  64
  65   // this should be a hash table so we can do this by key
  66   public ReachState containsIgnorePreds( ReachState state ) {
  67     assert state != null;
  68
  69     Iterator<ReachState> stateItr = this.reachStates.iterator();
  70     while( stateItr.hasNext() ) {
  71       ReachState stateThis = stateItr.next();
  72       if( stateThis.equalsIgnorePreds( state ) ) {
  73         return stateThis;
  74       }
  75     }
  76
  77     return null;
  78   }
  79
  80   /*
  81   public boolean containsWithZeroes( ReachState state ) {
  82     assert state != null;
  83
  84     if( reachStates.contains( state ) ) {
  85       return true;
  86     }
  87
  88     Iterator<ReachState> itr = iterator();
  89     while( itr.hasNext() ) {
  90       ReachState stateThis = itr.next();
  91       if( stateThis.containsWithZeroes( state ) ) {
  92         return true;
  93       }
  94     }
  95
  96     return false;
  97   }
  98   */
  99
 100   public boolean containsSuperSet( ReachState state ) {
 101     return containsSuperSet( state, false );
 102   }
 103
 104   public boolean containsStrictSuperSet( ReachState state ) {
 105     return containsSuperSet( state, true );
 106   }
 107
 108   public boolean containsSuperSet( ReachState state,
 109                                    boolean    strict ) {
 110     assert state != null;
 111
 112     if( !strict && reachStates.contains( state ) ) {
 113       return true;
 114     }
 115
 116     Iterator<ReachState> itr = iterator();
 117     while( itr.hasNext() ) {
 118       ReachState stateThis = itr.next();
 119       if( strict ) {
 120         if( !state.equals( stateThis ) &&
 121             state.isSubset( stateThis ) ) {
 122           return true;
 123         }
 124       } else {
 125         if( state.isSubset( stateThis ) ) {
 126           return true;
 127         }
 128       }
 129     }
 130
 131     return false;
 132   }
 133
 134
 135   public boolean containsTuple( ReachTuple rt ) {
 136     Iterator<ReachState> itr = iterator();
 137     while( itr.hasNext() ) {
 138       ReachState state = itr.next();
 139       if( state.containsTuple( rt ) ) {
 140         return true;
 141       }
 142     }
 143     return false;
 144   }
 145
 146   public ReachSet getStatesWithBoth( ReachTuple rt1,
 147                                      ReachTuple rt2 ) {
 148
 149     ReachSet out = new ReachSet();
 150
 151     Iterator<ReachState> itr = iterator();
 152     while( itr.hasNext() ) {
 153       ReachState state = itr.next();
 154       if( state.containsTuple( rt1 ) &&
 155           state.containsTuple( rt2 ) ) {
 156         out.reachStates.add( state );
 157       }
 158     }
 159
 160     out = (ReachSet) Canonical.makeCanonical( out );
 161     return out;
 162   }
 163
 164   // used to assert each state in the set is
 165   // unique
 166   public boolean containsNoDuplicates() {
 167     Vector<ReachState> v = new Vector( reachStates );
 168     for( int i = 0; i < v.size(); ++i ) {
 169       ReachState s1 = v.get( i );
 170       for( int j = i+1; j < v.size(); ++j ) {
 171         ReachState s2 = v.get( j );
 172         if( s1.equals( s2 ) ) {
 173           assert s1.isCanonical();
 174           assert s2.isCanonical();
 175           return false;
 176         }
 177       }
 178     }
 179     return true;
 180   }
 181
 182
 183   public boolean equals( Object o ) {
 184     if( o == null ) {
 185       return false;
 186     }
 187
 188     if( !(o instanceof ReachSet) ) {
 189       return false;
 190     }
 191
 192     ReachSet rs = (ReachSet) o;
 193     return reachStates.equals( rs.reachStates );
 194   }
 195
 196
 197   public int hashCodeSpecific() {
 198     return reachStates.hashCode();
 199   }
 200
 201
 202   public String toStringEscNewline( boolean hideSubsetReachability ) {
 203     String s = "[";
 204
 205     Iterator<ReachState> i = this.iterator();
 206     while( i.hasNext() ) {
 207       ReachState state = i.next();
 208
 209       // skip this if there is a superset already
 210       if( hideSubsetReachability &&
 211           containsStrictSuperSet( state ) ) {
 212         continue;
 213       }
 214
 215       s += state;
 216       if( i.hasNext() ) {
 217         s += "\\n";
 218       }
 219     }
 220
 221     s += "]";
 222     return s;
 223   }
 224
 225
 226   public String toString() {
 227     return toString( false );
 228   }
 229
 230   public String toString( boolean hideSubsetReachability ) {
 231     String s = "[";
 232
 233     Iterator<ReachState> i = this.iterator();
 234     while( i.hasNext() ) {
 235       ReachState state = i.next();
 236
 237       // skip this if there is a superset already
 238       if( hideSubsetReachability &&
 239           containsStrictSuperSet( state ) ) {
 240         continue;
 241       }
 242
 243       s += state;
 244       if( i.hasNext() ) {
 245         s += "\n";
 246       }
 247     }
 248
 249     s += "]";
 250     return s;
 251   }
 252 }