make sure change sets ignore predicates hanging off reach states and alter reach...

diff --git a/Robust/src/Analysis/Disjoint/Canonical.java b/Robust/src/Analysis/Disjoint/Canonical.java
index c74bad4dff063b39148ead6e56fc9e3222ae5b36..7f380b58a95864845578e3135ef923e6677bf829 100644 (file)
--- a/Robust/src/Analysis/Disjoint/Canonical.java
+++ b/Robust/src/Analysis/Disjoint/Canonical.java
@@ -173,7 +173,7 @@ abstract public class Canonical {
     out.reachTuples.addAll( rs.reachTuples );
     out.preds = Canonical.join( rs.preds,
                                 preds );
-
+    
     out = (ReachState) makeCanonical( out );
     op2result.put( op, out );
     return out;
@@ -451,6 +451,13 @@ abstract public class Canonical {
   }
 
 
+  // NOTE: when taking the intersection of two reach sets it
+  // is possible for a reach state to be in both sets, but
+  // have different predicates.  Conceptully the best new
+  // predicate is an AND of the source predicates, but to
+  // avoid eploding states we'll take an overapproximation
+  // by preferring the predicates from the state in the FIRST
+  // set, so order of arguments matters
   public static ReachSet intersection( ReachSet rs1,
                                        ReachSet rs2 ) {
     assert rs1 != null;
@@ -472,9 +479,12 @@ abstract public class Canonical {
     ReachSet out = new ReachSet();
     Iterator<ReachState> itr = rs1.iterator();
     while( itr.hasNext() ) {
-      ReachState state = (ReachState) itr.next();
-      if( rs2.reachStates.contains( state ) ) {
-        out.reachStates.add( state );
+      ReachState state1 = (ReachState) itr.next();
+      ReachState state2 = rs2.containsIgnorePreds( state1 );
+      if( state2 != null ) {
+        // prefer the predicates on state1, an overapproximation
+        // of state1 preds AND state2 preds
+        out.reachStates.add( state1 );
       }
     }
 
@@ -552,7 +562,7 @@ abstract public class Canonical {
 
     Iterator<ReachState> stateItr = rs.iterator();
     while( stateItr.hasNext() ) {
-      ReachState state = stateItr.next();
+      ReachState stateOrig = stateItr.next();
 
       boolean changeFound = false;
 
@@ -560,14 +570,19 @@ abstract public class Canonical {
       while( ctItr.hasNext() ) {
        ChangeTuple ct = ctItr.next();
 
-       if( state.equals( ct.getSetToMatch() ) ) {
-         out.reachStates.add( ct.getSetToAdd() );
+       if( stateOrig.equalsIgnorePreds( ct.getStateToMatch() ) ) {
+          // use the new state, but the original predicates
+          ReachState stateNew = 
+            ReachState.factory( ct.getStateToAdd().reachTuples,
+                                stateOrig.preds
+                                );
+          out.reachStates.add( stateNew );
          changeFound = true;
        }
       }
 
       if( keepSourceState || !changeFound ) {
-       out.reachStates.add( state );
+       out.reachStates.add( stateOrig );
       }
     }
 
@@ -761,8 +776,8 @@ abstract public class Canonical {
     return out;    
   }
 
-  public static ChangeSet union( ChangeSet   cs, 
-                                 ChangeTuple ct ) {
+  public static ChangeSet add( ChangeSet   cs, 
+                               ChangeTuple ct ) {
     assert cs != null;
     assert ct != null;
     assert cs.isCanonical();
@@ -1171,13 +1186,6 @@ abstract public class Canonical {
   }
 
 
-
-
-
-
-
-
-
   public static ReachSet unshadow( ReachSet  rs,
                                    AllocSite as ) {
     assert rs != null;

diff --git a/Robust/src/Analysis/Disjoint/ChangeTuple.java b/Robust/src/Analysis/Disjoint/ChangeTuple.java
index 01bff33b0704f347eeabe0c079071b4d5f2bbf70..99bf8326633387cddc8a428789bf32ed41ee41ae 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ChangeTuple.java
+++ b/Robust/src/Analysis/Disjoint/ChangeTuple.java
@@ -34,8 +34,19 @@ public class ChangeTuple extends Canonical
 
   public static ChangeTuple factory( ReachState toMatch,
                                      ReachState toAdd ) {
-    ChangeTuple out = new ChangeTuple( toMatch,
-                                       toAdd );
+    // we don't care about the predicates hanging on
+    // change tuple states, so always set them to empty
+    // to ensure change tuple sets work out
+    ReachState toMatchNoPreds =
+      ReachState.factory( toMatch.reachTuples,
+                          ExistPredSet.factory()
+                          );
+    ReachState toAddNoPreds =
+      ReachState.factory( toAdd.reachTuples,
+                          ExistPredSet.factory()
+                          );
+    ChangeTuple out = new ChangeTuple( toMatchNoPreds,
+                                       toAddNoPreds );
     out = (ChangeTuple) Canonical.makeCanonical( out );
     return out;
   }
@@ -46,10 +57,10 @@ public class ChangeTuple extends Canonical
     this.toAdd   = toAdd;
   }
 
-  public ReachState getSetToMatch() {
+  public ReachState getStateToMatch() {
     return toMatch;
   }
-  public ReachState getSetToAdd() {
+  public ReachState getStateToAdd() {
     return toAdd;
   }
   

diff --git a/Robust/src/Analysis/Disjoint/ExistPredSet.java b/Robust/src/Analysis/Disjoint/ExistPredSet.java
index 48d9affff8b3dc1db9938238c802af325e86c708..c026624a8a6677bb5b4ffd50da32ba9a8378fd9b 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ExistPredSet.java
+++ b/Robust/src/Analysis/Disjoint/ExistPredSet.java
@@ -49,6 +49,11 @@ public class ExistPredSet extends Canonical {
     preds = new HashSet<ExistPred>();
   }
 
+  
+  public Iterator<ExistPred> iterator() {
+    return preds.iterator();
+  }
+  
 
   // only consider the subest of the caller elements that
   // are reachable by callee when testing predicates

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index f6deaab2f2d4e04eeac52326248f1c47d353e5a9..778c9387ec8e14983ac3f3c5d24d419342278e1b 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -1080,8 +1080,10 @@ public class ReachGraph {
        Iterator<ChangeTuple> itrCprime = C.iterator();
        while( itrCprime.hasNext() ) {
          ChangeTuple c = itrCprime.next();
-         if( edgeF.getBeta().contains( c.getSetToMatch() ) ) {
-           changesToPass = Canonical.union( changesToPass, c );
+         if( edgeF.getBeta().containsIgnorePreds( c.getStateToMatch() ) 
+              != null
+              ) {
+           changesToPass = Canonical.add( changesToPass, c );
          }
        }
 
@@ -1160,8 +1162,10 @@ public class ReachGraph {
       Iterator<ChangeTuple> itrC = C.iterator();
       while( itrC.hasNext() ) {
        ChangeTuple c = itrC.next();
-       if( edgeE.getBeta().contains( c.getSetToMatch() ) ) {
-         changesToPass = Canonical.union( changesToPass, c );
+       if( edgeE.getBeta().containsIgnorePreds( c.getStateToMatch() ) 
+            != null
+            ) {
+         changesToPass = Canonical.add( changesToPass, c );
        }
       }
 
@@ -2384,28 +2388,28 @@ public class ReachGraph {
         ChangeSet cs = ChangeSet.factory();
         Iterator<ReachState> rsItr = reCaller.getBeta().iterator();
         while( rsItr.hasNext() ) {
-          ReachState   state = rsItr.next();
-          ExistPredSet preds2 = state.getPreds();
-          assert preds2.preds.size() == 1;
+          ReachState   state          = rsItr.next();
+          ExistPredSet predsPreCallee = state.getPreds();
 
           if( state.isEmpty() ) {
             continue;
           }
 
-          ExistPred pred = preds2.preds.iterator().next();
-          ReachState old = pred.ne_state;
-
-          if( old == null ) {
-            old = rstateEmpty;
-          }
+          Iterator<ExistPred> predItr = predsPreCallee.iterator();
+          while( predItr.hasNext() ) {            
+            ExistPred pred = predItr.next();
+            ReachState old = pred.ne_state;
 
-          assert old != null;
+            if( old == null ) {
+              old = rstateEmpty;
+            }
 
-          cs = Canonical.union( cs,
+            cs = Canonical.add( cs,
                                 ChangeTuple.factory( old,
                                                      state
                                                      )
                                 );
+          }
         }
         
         // look to see if an edge with same field exists
@@ -2985,19 +2989,21 @@ public class ReachGraph {
           
             if( prevResult == null || 
                 Canonical.unionORpreds( prevResult,
-                                 intersection ).size() > prevResult.size() ) {
+                                        intersection ).size() 
+                > prevResult.size() 
+                ) {
             
               if( prevResult == null ) {
                 boldB_f.put( edgePrime, 
                              Canonical.unionORpreds( edgePrime.getBeta(),
-                                              intersection 
-                                              )
+                                                     intersection 
+                                                     )
                              );
               } else {
                 boldB_f.put( edgePrime, 
                              Canonical.unionORpreds( prevResult,
-                                              intersection 
-                                              )
+                                                     intersection 
+                                                     )
                              );
               }
               workSetEdges.add( edgePrime );   
@@ -3095,8 +3101,8 @@ public class ReachGraph {
        // if there is nothing marked, just move on
        if( markedHrnIDs.isEmpty() ) {
          hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(),
-                                            stateOld
-                                            )
+                                          stateOld
+                                          )
                            );
          continue;
        }
@@ -3115,13 +3121,13 @@ public class ReachGraph {
        assert !stateOld.equals( statePruned );
 
        hrn.setAlphaNew( Canonical.add( hrn.getAlphaNew(),
-                                          statePruned
-                                          )
+                                        statePruned
+                                        )
                          );
        ChangeTuple ct = ChangeTuple.factory( stateOld,
                                               statePruned
                                               );
-       cts = Canonical.union( cts, ct );
+       cts = Canonical.add( cts, ct );
       }
 
       // throw change tuple set on all incident edges
@@ -3216,7 +3222,10 @@ public class ReachGraph {
                    
        if( Canonical.unionORpreds( prevResult,
                                     intersection
-                                    ).size() > prevResult.size() ) {
+                                    ).size() 
+            > prevResult.size() 
+            ) {
+          
          edge.setBetaNew( 
                           Canonical.unionORpreds( prevResult,
                                                   intersection 
@@ -4044,10 +4053,10 @@ public class ReachGraph {
                        }
                }
 
-               Set<HeapRegionNode> intersection = new HashSet<HeapRegionNode>(
-                               reachableNodes1);
+               Set<HeapRegionNode> intersection =
+                  new HashSet<HeapRegionNode>( reachableNodes1 );
 
-               intersection.retainAll(reachableNodes2);
+               intersection.retainAll( reachableNodes2 );
 
                return intersection;
        }