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... states) {
  40     ReachSet out = new ReachSet();
  41     for( ReachState state : states ) {
  42       assert state != null;
  43       assert state.isCanonical();
  44       out.reachStates.add(state);
  45     }
  46     out = (ReachSet) Canonical.makeCanonical(out);
  47     return out;
  48   }
  49
  50   protected ReachSet() {
  51     reachStates = new HashSet<ReachState>();
  52   }
  53
  54
  55   public Iterator<ReachState> iterator() {
  56     return reachStates.iterator();
  57   }
  58
  59   public int size() {
  60     return reachStates.size();
  61   }
  62
  63   public boolean isEmpty() {
  64     return reachStates.isEmpty();
  65   }
  66
  67   // this should be a hash table so we can do this by key
  68   public ReachState containsIgnorePreds(ReachState state) {
  69     assert state != null;
  70
  71     Iterator<ReachState> stateItr = this.reachStates.iterator();
  72     while( stateItr.hasNext() ) {
  73       ReachState stateThis = stateItr.next();
  74       if( stateThis.equalsIgnorePreds(state) ) {
  75         return stateThis;
  76       }
  77     }
  78
  79     return null;
  80   }
  81
  82   public boolean containsSuperSet(ReachState state) {
  83     return containsSuperSet(state, false);
  84   }
  85
  86   public boolean containsStrictSuperSet(ReachState state) {
  87     return containsSuperSet(state, true);
  88   }
  89
  90   public boolean containsSuperSet(ReachState state,
  91                                   boolean strict) {
  92     assert state != null;
  93
  94     if( !strict && reachStates.contains(state) ) {
  95       return true;
  96     }
  97
  98     Iterator<ReachState> itr = iterator();
  99     while( itr.hasNext() ) {
 100       ReachState stateThis = itr.next();
 101       if( strict ) {
 102         if( !state.equals(stateThis) &&
 103             state.isSubset(stateThis) ) {
 104           return true;
 105         }
 106       } else {
 107         if( state.isSubset(stateThis) ) {
 108           return true;
 109         }
 110       }
 111     }
 112
 113     return false;
 114   }
 115
 116
 117   public boolean containsTuple(ReachTuple rt) {
 118     Iterator<ReachState> itr = iterator();
 119     while( itr.hasNext() ) {
 120       ReachState state = itr.next();
 121       if( state.containsTuple(rt) ) {
 122         return true;
 123       }
 124     }
 125     return false;
 126   }
 127
 128   public ReachSet getStatesWithBoth(ReachTuple rt1,
 129                                     ReachTuple rt2) {
 130
 131     ReachSet out = new ReachSet();
 132
 133     Iterator<ReachState> itr = iterator();
 134     while( itr.hasNext() ) {
 135       ReachState state = itr.next();
 136       if( state.containsTuple(rt1) &&
 137           state.containsTuple(rt2) ) {
 138         out.reachStates.add(state);
 139       }
 140     }
 141
 142     out = (ReachSet) Canonical.makeCanonical(out);
 143     return out;
 144   }
 145
 146   // used to assert each state in the set is
 147   // unique
 148   public boolean containsNoDuplicates() {
 149     Vector<ReachState> v = new Vector(reachStates);
 150     for( int i = 0; i < v.size(); ++i ) {
 151       ReachState s1 = v.get(i);
 152       for( int j = i+1; j < v.size(); ++j ) {
 153         ReachState s2 = v.get(j);
 154         if( s1.equals(s2) ) {
 155           assert s1.isCanonical();
 156           assert s2.isCanonical();
 157           return false;
 158         }
 159       }
 160     }
 161     return true;
 162   }
 163
 164
 165   public boolean equalsSpecific(Object o) {
 166     if( o == null ) {
 167       return false;
 168     }
 169
 170     if( !(o instanceof ReachSet) ) {
 171       return false;
 172     }
 173
 174     ReachSet rs = (ReachSet) o;
 175     return reachStates.equals(rs.reachStates);
 176   }
 177
 178
 179   public int hashCodeSpecific() {
 180     return reachStates.hashCode();
 181   }
 182
 183
 184   public String toStringEscNewline(boolean hideSubsetReachability,
 185                                    boolean hidePreds) {
 186     String s = "[";
 187
 188     Iterator<ReachState> i = this.iterator();
 189     while( i.hasNext() ) {
 190       ReachState state = i.next();
 191
 192       // skip this if there is a superset already
 193       if( hideSubsetReachability &&
 194           containsStrictSuperSet(state) ) {
 195         continue;
 196       }
 197
 198       // jjenista - Use this version if you REALLY want to
 199       // the see the preds for heap region nodes, edges,
 200       // AND every reach state on all those elements!
 201       //s += state.toString( hidePreds );
 202       s += state.toString();
 203
 204       if( i.hasNext() ) {
 205         s += "\\n";
 206       }
 207     }
 208
 209     s += "]";
 210     return s;
 211   }
 212
 213
 214   public String toString() {
 215     return toString(false);
 216   }
 217
 218   public String toString(boolean hideSubsetReachability) {
 219
 220     ReachSet toPrint = this;
 221
 222     if( hideSubsetReachability ) {
 223       // make a new reach set with subset states removed
 224       toPrint = ReachSet.factory();
 225
 226       Iterator<ReachState> i = this.iterator();
 227       while( i.hasNext() ) {
 228         ReachState state = i.next();
 229
 230         if( containsStrictSuperSet(state) ) {
 231           continue;
 232         }
 233
 234         toPrint = Canonical.add(toPrint, state);
 235       }
 236     }
 237
 238     String s = "[";
 239
 240     Iterator<ReachState> i = toPrint.iterator();
 241     while( i.hasNext() ) {
 242       ReachState state = i.next();
 243
 244       s += state;
 245       if( i.hasNext() ) {
 246         s += "\n";
 247       }
 248     }
 249
 250     s += "]";
 251     return s;
 252   }
 253
 254   public String toStringPreds() {
 255     String s = "[\n";
 256
 257     for( ReachState state: reachStates ) {
 258       s += "  "+state.toStringPreds()+"\n";
 259     }
 260
 261     return s+"]";
 262   }
 263 }