1 package Analysis.Disjoint;
8 ///////////////////////////////////////////
10 // This class is an immutable Canonical, so
12 // 0) construct them with a factory pattern
13 // to ensure only canonical versions escape
15 // 1) any operation that modifies a Canonical
16 // is a static method in the Canonical class
18 // 2) operations that just read this object
19 // should be defined here
21 // 3) every Canonical subclass hashCode should
22 // throw an error if the hash ever changes
24 ///////////////////////////////////////////
26 // a reach set is a set of reach states
28 public class ReachSet extends Canonical {
30 protected HashSet<ReachState> reachStates;
33 public static ReachSet factory() {
34 ReachSet out = new ReachSet();
35 out = (ReachSet) Canonical.makeCanonical(out);
39 public static ReachSet factory(ReachState... states) {
40 ReachSet out = new ReachSet();
41 for( ReachState state : states ) {
43 assert state.isCanonical();
44 out.reachStates.add(state);
46 out = (ReachSet) Canonical.makeCanonical(out);
50 protected ReachSet() {
51 reachStates = new HashSet<ReachState>();
55 public Iterator<ReachState> iterator() {
56 return reachStates.iterator();
60 return reachStates.size();
63 public boolean isEmpty() {
64 return reachStates.isEmpty();
67 // this should be a hash table so we can do this by key
68 public ReachState containsIgnorePreds(ReachState state) {
71 Iterator<ReachState> stateItr = this.reachStates.iterator();
72 while( stateItr.hasNext() ) {
73 ReachState stateThis = stateItr.next();
74 if( stateThis.equalsIgnorePreds(state) ) {
82 public boolean containsSuperSet(ReachState state) {
83 return containsSuperSet(state, false);
86 public boolean containsStrictSuperSet(ReachState state) {
87 return containsSuperSet(state, true);
90 public boolean containsSuperSet(ReachState state,
94 if( !strict && reachStates.contains(state) ) {
98 Iterator<ReachState> itr = iterator();
99 while( itr.hasNext() ) {
100 ReachState stateThis = itr.next();
102 if( !state.equals(stateThis) &&
103 state.isSubset(stateThis) ) {
107 if( state.isSubset(stateThis) ) {
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) ) {
128 public ReachSet getStatesWithBoth(ReachTuple rt1,
131 ReachSet out = new ReachSet();
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);
142 out = (ReachSet) Canonical.makeCanonical(out);
146 // used to assert each state in the set is
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();
165 public boolean equalsSpecific(Object o) {
170 if( !(o instanceof ReachSet) ) {
174 ReachSet rs = (ReachSet) o;
175 return reachStates.equals(rs.reachStates);
179 public int hashCodeSpecific() {
180 return reachStates.hashCode();
184 public String toStringEscNewline(boolean hideSubsetReachability,
188 Iterator<ReachState> i = this.iterator();
189 while( i.hasNext() ) {
190 ReachState state = i.next();
192 // skip this if there is a superset already
193 if( hideSubsetReachability &&
194 containsStrictSuperSet(state) ) {
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();
214 public String toString() {
215 return toString(false);
218 public String toString(boolean hideSubsetReachability) {
220 ReachSet toPrint = this;
222 if( hideSubsetReachability ) {
223 // make a new reach set with subset states removed
224 toPrint = ReachSet.factory();
226 Iterator<ReachState> i = this.iterator();
227 while( i.hasNext() ) {
228 ReachState state = i.next();
230 if( containsStrictSuperSet(state) ) {
234 toPrint = Canonical.add(toPrint, state);
240 Iterator<ReachState> i = toPrint.iterator();
241 while( i.hasNext() ) {
242 ReachState state = i.next();
254 public String toStringPreds() {
257 for( ReachState state: reachStates ) {
258 s += " "+state.toStringPreds()+"\n";