Added some functionality to reachability classes that is apparently
[IRC.git] / Robust / src / Analysis / OwnershipAnalysis / OwnershipGraph.java
index 6fb336a04c50c2d1f1f7e65405b353ede9ca3208..ef55faed9564a09611306d3755dd834ba7b7963c 100644 (file)
@@ -157,9 +157,11 @@ public class OwnershipGraph {
        }    
     }
     
+    protected void propagateTokens( HeapRegionNode                   nPrime,
+                                   ChangeTupleSet                   c0,
+                                   HashSet<HeapRegionNode>          nodesWithNewAlpha,
+                                   HashSet<ReferenceEdgeProperties> edgesWithNewBeta ) {
 
-
-    protected void propagateTokens( HeapRegionNode nPrime, ChangeTupleSet c0 ) {
        HashSet<HeapRegionNode> todoNodes
            = new HashSet<HeapRegionNode>();
        todoNodes.add( nPrime );
@@ -177,25 +179,24 @@ public class OwnershipGraph {
        Hashtable<HeapRegionNode, ChangeTupleSet> nodeChangesMade
            = new Hashtable<HeapRegionNode, ChangeTupleSet>();
 
-       Hashtable<ReferenceEdgeProperties, ChangeTupleSet> edgeChangesMade
-           = new Hashtable<ReferenceEdgeProperties, ChangeTupleSet>();
-
        while( !todoNodes.isEmpty() ) {
            HeapRegionNode n = todoNodes.iterator().next();
            todoNodes.remove( n );
+           
+           ChangeTupleSet C = nodePlannedChanges.get( n );
 
            if( !nodeChangesMade.containsKey( n ) ) {
                nodeChangesMade.put( n, new ChangeTupleSet().makeCanonical() );
            }
-           
-           ChangeTupleSet C = nodePlannedChanges.get( n );
 
            Iterator itrC = C.iterator();
            while( itrC.hasNext() ) {
                ChangeTuple c = (ChangeTuple) itrC.next();
 
                if( n.getAlpha().contains( c.getSetToMatch() ) ) {
-                   n.setAlphaNew( n.getAlphaNew().union( c.getSetToAdd() ) );              
+                   ReachabilitySet withChange = n.getAlpha().union( c.getSetToAdd() );
+                   n.setAlphaNew( n.getAlphaNew().union( withChange ) );
+                   nodesWithNewAlpha.add( n );
                    nodeChangesMade.put( n, nodeChangesMade.get( n ).union( c ) );
                }
            }
@@ -223,7 +224,7 @@ public class OwnershipGraph {
                m            = (HeapRegionNode)          me.getKey();
                f            = (ReferenceEdgeProperties) me.getValue();
 
-               ChangeTupleSet changesToPass = new ChangeTupleSet();
+               ChangeTupleSet changesToPass = new ChangeTupleSet().makeCanonical();
 
                Iterator itrCprime = Cprime.iterator();
                while( itrCprime.hasNext() ) {
@@ -247,7 +248,54 @@ public class OwnershipGraph {
                }
            }
        }
-       
+
+       
+       while( !todoEdges.isEmpty() ) {
+           ReferenceEdgeProperties e = todoEdges.iterator().next();
+           todoEdges.remove( e );
+
+           if( !edgePlannedChanges.containsKey( e ) ) {
+               edgePlannedChanges.put( e, new ChangeTupleSet().makeCanonical() );
+           }
+           
+           ChangeTupleSet C = edgePlannedChanges.get( e );
+
+           ChangeTupleSet changesToPass = new ChangeTupleSet().makeCanonical();
+
+           Iterator itrC = C.iterator();
+           while( itrC.hasNext() ) {
+               ChangeTuple c = (ChangeTuple) itrC.next();
+               if( e.getBeta().contains( c.getSetToMatch() ) ) {
+                   ReachabilitySet withChange = e.getBeta().union( c.getSetToAdd() );
+                   e.setBetaNew( e.getBetaNew().union( withChange ) );
+                   edgesWithNewBeta.add( e );
+                   changesToPass = changesToPass.union( c );
+               }
+           }
+
+           OwnershipNode onSrc = e.getSrc();
+
+           if( !changesToPass.isEmpty() && onSrc instanceof HeapRegionNode ) {         
+               HeapRegionNode n = (HeapRegionNode) onSrc;
+               Iterator referItr = n.iteratorToReferencers();
+
+               while( referItr.hasNext() ) {
+                   OwnershipNode onRef = (OwnershipNode) referItr.next();
+                   ReferenceEdgeProperties f = onRef.getReferenceTo( n );
+                   
+                   if( !edgePlannedChanges.containsKey( f ) ) {
+                       edgePlannedChanges.put( f, new ChangeTupleSet().makeCanonical() );
+                   }
+                 
+                   ChangeTupleSet currentChanges = edgePlannedChanges.get( f );
+               
+                   if( !changesToPass.isSubset( currentChanges ) ) {
+                       todoEdges.add( f );
+                       edgePlannedChanges.put( f, currentChanges.union( changesToPass ) );
+                   }
+               }
+           }       
+       }       
     }
 
 
@@ -348,15 +396,21 @@ public class OwnershipGraph {
                Map.Entry meS = (Map.Entry)               srcRegionsItr.next();
                hrnSrc        = (HeapRegionNode)          meS.getKey();
                repSrc        = (ReferenceEdgeProperties) meS.getValue();
+               
+               ReachabilitySet O = srcln.getReferenceTo( hrnSrc ).getBeta();
 
+               ChangeTupleSet Cy = O.unionUpArityToChangeSet( R );
+               ChangeTupleSet Cx = R.unionUpArityToChangeSet( O );
+
+               propagateTokens( hrnSrc, Cy, nodesWithNewAlpha, edgesWithNewBeta );
+               propagateTokens( hrn,    Cx, nodesWithNewAlpha, edgesWithNewBeta );
+
+               // note that this picks up the beta after the propogation has
+               // been applied
                ReferenceEdgeProperties repNew 
-                   = new ReferenceEdgeProperties( false, false, null );
+                   = new ReferenceEdgeProperties( false, false, repSrc.getBetaNew() );
 
                addReferenceEdge( hrn, hrnSrc, repNew );
-               
-               ReachabilitySet O = srcln.getReferenceTo( hrnSrc ).getBeta();
-               ChangeTupleSet  C = O.unionUpArity( R );
-               propagateTokens( hrnSrc, C );
            }
        }       
 
@@ -427,7 +481,8 @@ public class OwnershipGraph {
        LabelNode dst = getLabelNodeFromTemp( td );
        
        clearReferenceEdgesFrom( dst );
-       addReferenceEdge( dst, hrnNewest, new ReferenceEdgeProperties( false ) );
+       
+       addReferenceEdge( dst, hrnNewest, new ReferenceEdgeProperties( false, false, hrnNewest.getAlpha() ) );
     }
 
 
@@ -486,7 +541,7 @@ public class OwnershipGraph {
 
            boolean hasFlags = false;
            if( as.getType().isClass() ) {
-               hasFlags =  as.getType().getClassDesc().hasFlags();
+               hasFlags = as.getType().getClassDesc().hasFlags();
            }
 
            hrnSummary = createNewHeapRegionNode( idSummary,
@@ -549,9 +604,19 @@ public class OwnershipGraph {
            onReferencer = (OwnershipNode) itrReferencer.next();
            
            ReferenceEdgeProperties rep = onReferencer.getReferenceTo( hrnK );
-           assert rep != null;
-           
-           addReferenceEdge( onReferencer, hrnSummary, rep.copy() );
+           assert rep != null;     
+           ReferenceEdgeProperties repSummary = onReferencer.getReferenceTo( hrnSummary );
+           ReferenceEdgeProperties repMerged = rep.copy();
+
+           if( repSummary == null ) {      
+               // the merge is trivial, nothing to be done
+           } else {
+               // otherwise an edge from the referencer to alpha_S exists already
+               // and the edge referencer->alpha_K should be merged with it
+               repMerged.setBeta( repMerged.getBeta().union( repSummary.getBeta() ) );
+           }
+
+           addReferenceEdge( onReferencer, hrnSummary, repMerged );
        }
 
        
@@ -1463,7 +1528,7 @@ public class OwnershipGraph {
                    bw.write( "  "        + ln.toString() +
                              " -> "      + hrn.toString() +
                              "[label=\"" + rep.toEdgeLabelString() +
-                             "\"];\n" );
+                             "\",decorate];\n" );
                }
            }
        }
@@ -1544,7 +1609,7 @@ public class OwnershipGraph {
                bw.write( "  "        + hrn.toString() +
                          " -> "      + hrnChild.toString() +
                          "[label=\"" + rep.toEdgeLabelString() +
-                         "\"];\n" );
+                         "\",decorate];\n" );
                break;
            }