get set up for experiment: test impact of disabling components

[IRC.git] / Robust / src / Analysis / Disjoint / ReachSet.java

diff --git a/Robust/src/Analysis/Disjoint/ReachSet.java b/Robust/src/Analysis/Disjoint/ReachSet.java
index 0c40a3f1443323355667cc6978a1e116c2f46491..e7fe5134b9ebc4e1f7f010e3efb7e7c0c7100eeb 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachSet.java
+++ b/Robust/src/Analysis/Disjoint/ReachSet.java
@@ -32,20 +32,22 @@ public class ReachSet extends Canonical {
 
   public static ReachSet factory() {
     ReachSet out = new ReachSet();
-    out = (ReachSet) Canonical.makeCanonical( out );
+    out = (ReachSet) Canonical.makeCanonical(out);
     return out;
   }
 
-  public static ReachSet factory( ReachState state ) {
-    assert state != null;
-    assert state.isCanonical();
+  public static ReachSet factory(ReachState... states) {
     ReachSet out = new ReachSet();
-    out.reachStates.add( state );
-    out = (ReachSet) Canonical.makeCanonical( out );
+    for( ReachState state : states ) {
+      assert state != null;
+      assert state.isCanonical();
+      out.reachStates.add(state);
+    }
+    out = (ReachSet) Canonical.makeCanonical(out);
     return out;
   }
 
-  private ReachSet() {
+  protected ReachSet() {
     reachStates = new HashSet<ReachState>();
   }
 
@@ -62,44 +64,34 @@ public class ReachSet extends Canonical {
     return reachStates.isEmpty();
   }
 
-  public boolean contains( ReachState state ) {
+  // this should be a hash table so we can do this by key
+  public ReachState containsIgnorePreds(ReachState state) {
     assert state != null;
-    return reachStates.contains( state );
-  }
 
-  /*
-  public boolean containsWithZeroes( ReachState state ) {
-    assert state != null;
-
-    if( reachStates.contains( state ) ) {
-      return true;
-    }
-
-    Iterator<ReachState> itr = iterator();
-    while( itr.hasNext() ) {
-      ReachState stateThis = itr.next();
-      if( stateThis.containsWithZeroes( state ) ) {
-       return true;
+    Iterator<ReachState> stateItr = this.reachStates.iterator();
+    while( stateItr.hasNext() ) {
+      ReachState stateThis = stateItr.next();
+      if( stateThis.equalsIgnorePreds(state) ) {
+        return stateThis;
       }
     }
-    
-    return false;    
+
+    return null;
   }
-  */
 
-  public boolean containsSuperSet( ReachState state ) {
-    return containsSuperSet( state, false );
+  public boolean containsSuperSet(ReachState state) {
+    return containsSuperSet(state, false);
   }
 
-  public boolean containsStrictSuperSet( ReachState state ) {
-    return containsSuperSet( state, true );
+  public boolean containsStrictSuperSet(ReachState state) {
+    return containsSuperSet(state, true);
   }
 
-  public boolean containsSuperSet( ReachState state,
-                                   boolean    strict ) {
+  public boolean containsSuperSet(ReachState state,
+                                  boolean strict) {
     assert state != null;
 
-    if( !strict && reachStates.contains( state ) ) {
+    if( !strict && reachStates.contains(state) ) {
       return true;
     }
 
@@ -107,60 +99,80 @@ public class ReachSet extends Canonical {
     while( itr.hasNext() ) {
       ReachState stateThis = itr.next();
       if( strict ) {
-        if( !state.equals( stateThis ) &&
-            state.isSubset( stateThis ) ) {
+        if( !state.equals(stateThis) &&
+            state.isSubset(stateThis) ) {
           return true;
         }
       } else {
-        if( state.isSubset( stateThis ) ) {
+        if( state.isSubset(stateThis) ) {
           return true;
         }
       }
     }
-    
-    return false;    
+
+    return false;
   }
 
 
-  public boolean containsTuple( ReachTuple rt ) {
+  public boolean containsTuple(ReachTuple rt) {
     Iterator<ReachState> itr = iterator();
     while( itr.hasNext() ) {
       ReachState state = itr.next();
-      if( state.containsTuple( rt ) ) {
-       return true;
+      if( state.containsTuple(rt) ) {
+        return true;
       }
     }
     return false;
   }
 
-  public boolean containsStateWithBoth( ReachTuple rt1, 
-                                        ReachTuple rt2 ) {
+  public ReachSet getStatesWithBoth(ReachTuple rt1,
+                                    ReachTuple rt2) {
+
+    ReachSet out = new ReachSet();
+
     Iterator<ReachState> itr = iterator();
     while( itr.hasNext() ) {
       ReachState state = itr.next();
-      if( state.containsTuple( rt1 ) &&
-          state.containsTuple( rt2 ) ) {
-       return true;
+      if( state.containsTuple(rt1) &&
+          state.containsTuple(rt2) ) {
+        out.reachStates.add(state);
       }
     }
-    return false;
+
+    out = (ReachSet) Canonical.makeCanonical(out);
+    return out;
   }
 
+  // used to assert each state in the set is
+  // unique
+  public boolean containsNoDuplicates() {
+    Vector<ReachState> v = new Vector(reachStates);
+    for( int i = 0; i < v.size(); ++i ) {
+      ReachState s1 = v.get(i);
+      for( int j = i+1; j < v.size(); ++j ) {
+        ReachState s2 = v.get(j);
+        if( s1.equals(s2) ) {
+          assert s1.isCanonical();
+          assert s2.isCanonical();
+          return false;
+        }
+      }
+    }
+    return true;
+  }
 
 
-  public boolean equals( Object o ) {
+  public boolean equalsSpecific(Object o) {
     if( o == null ) {
       return false;
     }
-    
+
     if( !(o instanceof ReachSet) ) {
       return false;
     }
 
     ReachSet rs = (ReachSet) o;
-    assert this.isCanonical();
-    assert rs.isCanonical();
-    return this == rs;
+    return reachStates.equals(rs.reachStates);
   }
 
 
@@ -169,7 +181,8 @@ public class ReachSet extends Canonical {
   }
 
 
-  public String toStringEscNewline( boolean hideSubsetReachability ) {
+  public String toStringEscNewline(boolean hideSubsetReachability,
+                                   boolean hidePreds) {
     String s = "[";
 
     Iterator<ReachState> i = this.iterator();
@@ -178,45 +191,73 @@ public class ReachSet extends Canonical {
 
       // skip this if there is a superset already
       if( hideSubsetReachability &&
-          containsStrictSuperSet( state ) ) {
+          containsStrictSuperSet(state) ) {
         continue;
       }
 
-      s += state;
+      // jjenista - Use this version if you REALLY want to
+      // the see the preds for heap region nodes, edges,
+      // AND every reach state on all those elements!
+      //s += state.toString( hidePreds );
+      s += state.toString();
+
       if( i.hasNext() ) {
-       s += "\\n";
+        s += "\\n";
       }
     }
 
     s += "]";
     return s;
   }
-  
+
 
   public String toString() {
-    return toString( false );
+    return toString(false);
   }
 
-  public String toString( boolean hideSubsetReachability ) {
+  public String toString(boolean hideSubsetReachability) {
+
+    ReachSet toPrint = this;
+
+    if( hideSubsetReachability ) {
+      // make a new reach set with subset states removed
+      toPrint = ReachSet.factory();
+
+      Iterator<ReachState> i = this.iterator();
+      while( i.hasNext() ) {
+        ReachState state = i.next();
+
+        if( containsStrictSuperSet(state) ) {
+          continue;
+        }
+
+        toPrint = Canonical.add(toPrint, state);
+      }
+    }
+
     String s = "[";
 
-    Iterator<ReachState> i = this.iterator();
+    Iterator<ReachState> i = toPrint.iterator();
     while( i.hasNext() ) {
       ReachState state = i.next();
 
-      // skip this if there is a superset already
-      if( hideSubsetReachability &&
-          containsStrictSuperSet( state ) ) {
-        continue;
-      }
-
       s += state;
       if( i.hasNext() ) {
-       s += "\n";
+        s += "\n";
       }
     }
 
     s += "]";
     return s;
   }
+
+  public String toStringPreds() {
+    String s = "[\n";
+    
+    for( ReachState state: reachStates ) {
+      s += "  "+state.toStringPreds()+"\n";
+    }
+
+    return s+"]";
+  }
 }