generate annotated source code again but it's still not the correct one...

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

diff --git a/Robust/src/Analysis/Disjoint/ReachState.java b/Robust/src/Analysis/Disjoint/ReachState.java
index aa17556174d13a003eeae3be635f8267e7b4d7dd..537a44a01647296e6daebadf477fbaf4ac5f4fc5 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachState.java
+++ b/Robust/src/Analysis/Disjoint/ReachState.java
@@ -31,28 +31,49 @@ public class ReachState extends Canonical {
 
   protected HashSet<ReachTuple> reachTuples;
 
+  // existance predicates must be true in a caller
+  // context for this state to transfer from this
+  // callee to that context
+  protected ExistPredSet preds;
+
 
   public static ReachState factory() {
     ReachState out = new ReachState();
-    out = (ReachState) Canonical.makeCanonical( out );
+    out = (ReachState) Canonical.makeCanonical(out);
     return out;
   }
 
-  public static ReachState factory( ReachTuple rt ) {
-    assert rt != null;
-    assert rt.isCanonical();
-    ReachState out = new ReachState();    
-    out.reachTuples.add( rt );
-    out = (ReachState) Canonical.makeCanonical( out );
+  public static ReachState factory(ReachTuple... rts) {
+    ReachState out = new ReachState();
+    for( ReachTuple rt : rts ) {
+      assert rt != null;
+      assert rt.isCanonical();
+      out.reachTuples.add(rt);
+    }
+    out = (ReachState) Canonical.makeCanonical(out);
+    return out;
+  }
+
+  public static ReachState factory(HashSet<ReachTuple> reachTuples,
+                                   ExistPredSet preds
+                                   ) {
+    assert reachTuples != null;
+    assert preds != null;
+    assert preds.isCanonical();
+    ReachState out = new ReachState();
+    out.reachTuples.addAll(reachTuples);
+    out.preds = preds;
+    out = (ReachState) Canonical.makeCanonical(out);
     return out;
   }
 
   protected ReachState() {
     reachTuples = new HashSet<ReachTuple>();
+    preds       = ExistPredSet.factory();
   }
 
 
-  public Iterator iterator() {
+  public Iterator<ReachTuple> iterator() {
     return reachTuples.iterator();
   }
 
@@ -60,37 +81,40 @@ public class ReachState extends Canonical {
     return reachTuples.isEmpty();
   }
 
-  public boolean isSubset( ReachState rsIn ) {
+  public boolean isSubset(ReachState rsIn) {
     assert rsIn != null;
-    return rsIn.reachTuples.containsAll( this.reachTuples );
+    return rsIn.reachTuples.containsAll(this.reachTuples);
   }
 
-  public boolean containsTuple( ReachTuple rt ) {
+  public boolean containsTuple(ReachTuple rt) {
     assert rt != null;
-    return reachTuples.contains( rt );
+    return reachTuples.contains(rt);
   }
 
   // this should be a hash table so we can do this by key
-  public ReachTuple containsHrnID( Integer hrnID,
-                                   boolean isOutOfContext ) {
+  public ReachTuple containsHrnID(Integer hrnID,
+                                  boolean isOutOfContext) {
     assert hrnID != null;
 
     Iterator<ReachTuple> rtItr = reachTuples.iterator();
     while( rtItr.hasNext() ) {
       ReachTuple rt = rtItr.next();
-      if( hrnID.equals( rt.getHrnID() ) &&
+      if( hrnID.equals(rt.getHrnID() ) &&
           isOutOfContext == rt.isOutOfContext()
           ) {
-       return rt;
+        return rt;
       }
     }
-    
+
     return null;
   }
 
+  public ExistPredSet getPreds() {
+    return preds;
+  }
 
 
-  public boolean equals( Object o ) {
+  public boolean equalsSpecific(Object o) {
     if( o == null ) {
       return false;
     }
@@ -100,16 +124,58 @@ public class ReachState extends Canonical {
     }
 
     ReachState rs = (ReachState) o;
-    return reachTuples.equals( rs.reachTuples );
+    return
+      reachTuples.equals(rs.reachTuples) &&
+      preds.equals(rs.preds);
   }
 
 
   public int hashCodeSpecific() {
+    return
+      reachTuples.hashCode() ^
+      preds.hashCode();
+  }
+
+
+  public int hashCodeNoPreds() {
     return reachTuples.hashCode();
   }
 
 
+  public boolean equalsIgnorePreds(Object o) {
+    if( o == null ) {
+      return false;
+    }
+
+    if( !(o instanceof ReachState) ) {
+      return false;
+    }
+
+    ReachState rs = (ReachState) o;
+    return
+      reachTuples.equals(rs.reachTuples);
+  }
+
+
+
   public String toString() {
     return reachTuples.toString();
+    //return reachTuples+":"+preds;
+  }
+
+  public String toStringPreds() {
+    return reachTuples+":"+preds;
+  }
+
+  public String toString( boolean hidePreds ) {
+    if( hidePreds ) {
+      return toString();
+    }
+    return toStringPreds();
+  }
+
+
+  public long numNonzeroTuples() {
+    return reachTuples.size();
   }
 }