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   public boolean containsSuperSet(ReachState state) {
  81     return containsSuperSet(state, false);
  82   }
  83
  84   public boolean containsStrictSuperSet(ReachState state) {
  85     return containsSuperSet(state, true);
  86   }
  87
  88   public boolean containsSuperSet(ReachState state,
  89                                   boolean strict) {
  90     assert state != null;
  91
  92     if( !strict && reachStates.contains(state) ) {
  93       return true;
  94     }
  95
  96     Iterator<ReachState> itr = iterator();
  97     while( itr.hasNext() ) {
  98       ReachState stateThis = itr.next();
  99       if( strict ) {
 100         if( !state.equals(stateThis) &&
 101             state.isSubset(stateThis) ) {
 102           return true;
 103         }
 104       } else {
 105         if( state.isSubset(stateThis) ) {
 106           return true;
 107         }
 108       }
 109     }
 110
 111     return false;
 112   }
 113
 114
 115   public boolean containsTuple(ReachTuple rt) {
 116     Iterator<ReachState> itr = iterator();
 117     while( itr.hasNext() ) {
 118       ReachState state = itr.next();
 119       if( state.containsTuple(rt) ) {
 120         return true;
 121       }
 122     }
 123     return false;
 124   }
 125
 126   public ReachSet getStatesWithBoth(ReachTuple rt1,
 127                                     ReachTuple rt2) {
 128
 129     ReachSet out = new ReachSet();
 130
 131     Iterator<ReachState> itr = iterator();
 132     while( itr.hasNext() ) {
 133       ReachState state = itr.next();
 134       if( state.containsTuple(rt1) &&
 135           state.containsTuple(rt2) ) {
 136         out.reachStates.add(state);
 137       }
 138     }
 139
 140     out = (ReachSet) Canonical.makeCanonical(out);
 141     return out;
 142   }
 143
 144   // used to assert each state in the set is
 145   // unique
 146   public boolean containsNoDuplicates() {
 147     Vector<ReachState> v = new Vector(reachStates);
 148     for( int i = 0; i < v.size(); ++i ) {
 149       ReachState s1 = v.get(i);
 150       for( int j = i+1; j < v.size(); ++j ) {
 151         ReachState s2 = v.get(j);
 152         if( s1.equals(s2) ) {
 153           assert s1.isCanonical();
 154           assert s2.isCanonical();
 155           return false;
 156         }
 157       }
 158     }
 159     return true;
 160   }
 161
 162
 163   public boolean equalsSpecific(Object o) {
 164     if( o == null ) {
 165       return false;
 166     }
 167
 168     if( !(o instanceof ReachSet) ) {
 169       return false;
 170     }
 171
 172     ReachSet rs = (ReachSet) o;
 173     return reachStates.equals(rs.reachStates);
 174   }
 175
 176
 177   public int hashCodeSpecific() {
 178     return reachStates.hashCode();
 179   }
 180
 181
 182   public String toStringEscNewline(boolean hideSubsetReachability) {
 183     String s = "[";
 184
 185     Iterator<ReachState> i = this.iterator();
 186     while( i.hasNext() ) {
 187       ReachState state = i.next();
 188
 189       // skip this if there is a superset already
 190       if( hideSubsetReachability &&
 191           containsStrictSuperSet(state) ) {
 192         continue;
 193       }
 194
 195       s += state;
 196       if( i.hasNext() ) {
 197         s += "\\n";
 198       }
 199     }
 200
 201     s += "]";
 202     return s;
 203   }
 204
 205
 206   public String toString() {
 207     return toString(false);
 208   }
 209
 210   public String toString(boolean hideSubsetReachability) {
 211
 212     ReachSet toPrint = this;
 213
 214     if( hideSubsetReachability ) {
 215       // make a new reach set with subset states removed
 216       toPrint = ReachSet.factory();
 217
 218       Iterator<ReachState> i = this.iterator();
 219       while( i.hasNext() ) {
 220         ReachState state = i.next();
 221
 222         if( containsStrictSuperSet(state) ) {
 223           continue;
 224         }
 225
 226         toPrint = Canonical.add(toPrint, state);
 227       }
 228     }
 229
 230     String s = "[";
 231
 232     Iterator<ReachState> i = toPrint.iterator();
 233     while( i.hasNext() ) {
 234       ReachState state = i.next();
 235
 236       s += state;
 237       if( i.hasNext() ) {
 238         s += "\n";
 239       }
 240     }
 241
 242     s += "]";
 243     return s;
 244   }
 245 }