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   public boolean contains( ReachState state ) {
  66     assert state != null;
  67     return reachStates.contains( state );
  68   }
  69
  70   /*
  71   public boolean containsWithZeroes( ReachState state ) {
  72     assert state != null;
  73
  74     if( reachStates.contains( state ) ) {
  75       return true;
  76     }
  77
  78     Iterator<ReachState> itr = iterator();
  79     while( itr.hasNext() ) {
  80       ReachState stateThis = itr.next();
  81       if( stateThis.containsWithZeroes( state ) ) {
  82         return true;
  83       }
  84     }
  85
  86     return false;
  87   }
  88   */
  89
  90   public boolean containsSuperSet( ReachState state ) {
  91     return containsSuperSet( state, false );
  92   }
  93
  94   public boolean containsStrictSuperSet( ReachState state ) {
  95     return containsSuperSet( state, true );
  96   }
  97
  98   public boolean containsSuperSet( ReachState state,
  99                                    boolean    strict ) {
 100     assert state != null;
 101
 102     if( !strict && reachStates.contains( state ) ) {
 103       return true;
 104     }
 105
 106     Iterator<ReachState> itr = iterator();
 107     while( itr.hasNext() ) {
 108       ReachState stateThis = itr.next();
 109       if( strict ) {
 110         if( !state.equals( stateThis ) &&
 111             state.isSubset( stateThis ) ) {
 112           return true;
 113         }
 114       } else {
 115         if( state.isSubset( stateThis ) ) {
 116           return true;
 117         }
 118       }
 119     }
 120
 121     return false;
 122   }
 123
 124
 125   public boolean containsTuple( ReachTuple rt ) {
 126     Iterator<ReachState> itr = iterator();
 127     while( itr.hasNext() ) {
 128       ReachState state = itr.next();
 129       if( state.containsTuple( rt ) ) {
 130         return true;
 131       }
 132     }
 133     return false;
 134   }
 135
 136   public boolean containsStateWithBoth( ReachTuple rt1,
 137                                         ReachTuple rt2 ) {
 138     Iterator<ReachState> itr = iterator();
 139     while( itr.hasNext() ) {
 140       ReachState state = itr.next();
 141       if( state.containsTuple( rt1 ) &&
 142           state.containsTuple( rt2 ) ) {
 143         return true;
 144       }
 145     }
 146     return false;
 147   }
 148
 149
 150
 151   public boolean equals( Object o ) {
 152     if( o == null ) {
 153       return false;
 154     }
 155
 156     if( !(o instanceof ReachSet) ) {
 157       return false;
 158     }
 159
 160     ReachSet rs = (ReachSet) o;
 161     return reachStates.equals( rs.reachStates );
 162   }
 163
 164
 165   public int hashCodeSpecific() {
 166     return reachStates.hashCode();
 167   }
 168
 169
 170   public String toStringEscNewline( boolean hideSubsetReachability ) {
 171     String s = "[";
 172
 173     Iterator<ReachState> i = this.iterator();
 174     while( i.hasNext() ) {
 175       ReachState state = i.next();
 176
 177       // skip this if there is a superset already
 178       if( hideSubsetReachability &&
 179           containsStrictSuperSet( state ) ) {
 180         continue;
 181       }
 182
 183       s += state;
 184       if( i.hasNext() ) {
 185         s += "\\n";
 186       }
 187     }
 188
 189     s += "]";
 190     return s;
 191   }
 192
 193
 194   public String toString() {
 195     return toString( false );
 196   }
 197
 198   public String toString( boolean hideSubsetReachability ) {
 199     String s = "[";
 200
 201     Iterator<ReachState> i = this.iterator();
 202     while( i.hasNext() ) {
 203       ReachState state = i.next();
 204
 205       // skip this if there is a superset already
 206       if( hideSubsetReachability &&
 207           containsStrictSuperSet( state ) ) {
 208         continue;
 209       }
 210
 211       s += state;
 212       if( i.hasNext() ) {
 213         s += "\n";
 214       }
 215     }
 216
 217     s += "]";
 218     return s;
 219   }
 220 }