Fixed a few minor bugs in token propagation, and major bug that every

reachability set should have the empty token tuple set as a member.
Also, propagation does not go back up edges yet.

diff --git a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
index 6fb336a04c50c2d1f1f7e65405b353ede9ca3208..14bcff27e2f1a1b2edb04f530d14bff73fe9123a 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/OwnershipGraph.java
@@ -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 );
@@ -180,10 +182,14 @@ public class OwnershipGraph {
        Hashtable<ReferenceEdgeProperties, ChangeTupleSet> edgeChangesMade
            = new Hashtable<ReferenceEdgeProperties, ChangeTupleSet>();
 
+       System.out.println( "New propagation with changes "+c0 );
+
        while( !todoNodes.isEmpty() ) {
            HeapRegionNode n = todoNodes.iterator().next();
            todoNodes.remove( n );
 
+           System.out.println( "  Propagating tokens over "+n );
+
            if( !nodeChangesMade.containsKey( n ) ) {
                nodeChangesMade.put( n, new ChangeTupleSet().makeCanonical() );
            }
@@ -194,8 +200,11 @@ public class OwnershipGraph {
            while( itrC.hasNext() ) {
                ChangeTuple c = (ChangeTuple) itrC.next();
 
+               System.out.println( "    Considering applying "+c );
+
                if( n.getAlpha().contains( c.getSetToMatch() ) ) {
-                   n.setAlphaNew( n.getAlphaNew().union( c.getSetToAdd() ) );              
+                   n.setAlphaNew( n.getAlpha().union( c.getSetToAdd() ) );
+                   nodesWithNewAlpha.add( n );
                    nodeChangesMade.put( n, nodeChangesMade.get( n ).union( c ) );
                }
            }
@@ -356,7 +365,7 @@ public class OwnershipGraph {
                
                ReachabilitySet O = srcln.getReferenceTo( hrnSrc ).getBeta();
                ChangeTupleSet  C = O.unionUpArity( R );
-               propagateTokens( hrnSrc, C );
+               propagateTokens( hrnSrc, C, nodesWithNewAlpha, edgesWithNewBeta );
            }
        }       
 
@@ -427,7 +436,8 @@ public class OwnershipGraph {
        LabelNode dst = getLabelNodeFromTemp( td );
        
        clearReferenceEdgesFrom( dst );
-       addReferenceEdge( dst, hrnNewest, new ReferenceEdgeProperties( false ) );
+
+       addReferenceEdge( dst, hrnNewest, new ReferenceEdgeProperties( false, false, null ) );
     }
 
 

diff --git a/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java b/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java
index 842098d10d09d1fdd401090a3a0c8c731c4e8ea1..9439f4050d8c0d124ad4ca26900983e19e14c3ff 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/ReachabilitySet.java
@@ -12,16 +12,18 @@ public class ReachabilitySet extends Canonical {
 
     public ReachabilitySet() {
        possibleReachabilities = new HashSet<TokenTupleSet>();
+       TokenTupleSet ttsEmpty = new TokenTupleSet().makeCanonical();
+       possibleReachabilities.add( ttsEmpty ); 
     }
 
     public ReachabilitySet( TokenTupleSet tts ) {
+       this();
        assert tts != null;
-       possibleReachabilities = new HashSet<TokenTupleSet>();
        possibleReachabilities.add( tts );
     }
 
     public ReachabilitySet( TokenTuple tt ) {
-       this( new TokenTupleSet( tt ) );
+       this( new TokenTupleSet( tt ).makeCanonical() );
     }
 
     public ReachabilitySet( ReachabilitySet rs ) {
@@ -46,7 +48,14 @@ public class ReachabilitySet extends Canonical {
        assert rsIn != null;
 
        ReachabilitySet rsOut = new ReachabilitySet( this );
+
+       System.out.println( "rsIn  = "+rsIn );
+       System.out.println( "rsOut = "+rsOut );
+
        rsOut.possibleReachabilities.addAll( rsIn.possibleReachabilities );
+
+       System.out.println( "union = "+rsOut );
+
        return rsOut.makeCanonical();
     }
 
@@ -140,10 +149,17 @@ public class ReachabilitySet extends Canonical {
 
        Iterator i = this.iterator();
        while( i.hasNext() ) {
-           s += "\\n  "+i.next();
+           if( possibleReachabilities.size() > 1 ) {
+               s += "\\n";
+           }
+           s += " "+i.next();
+       }
+
+       if( possibleReachabilities.size() > 1 ) {
+           s += "\\n";
        }
 
-       s += "]";
+       s += " ]";
 
        return s;       
     }
@@ -153,10 +169,17 @@ public class ReachabilitySet extends Canonical {
 
        Iterator i = this.iterator();
        while( i.hasNext() ) {
-           s += "\n  "+i.next();
+           if( possibleReachabilities.size() > 1 ) {
+               s += "\n";
+           }
+           s += " "+i.next();
+       }
+       
+       if( possibleReachabilities.size() > 1 ) {
+           s += "\n";
        }
 
-       s += "\n]";
+       s += " ]";
 
        return s;       
     }

diff --git a/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java b/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java
index 7c3e770fe8a829b7420610a4e7ab8473ea97cc57..443375d078fb7b67a24f4e7c7d1ab354655a868a 100644 (file)
--- a/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java
+++ b/Robust/src/Tests/OwnershipAnalysisTest/test01/test01.java
@@ -54,11 +54,13 @@ public class Foo {
 // a heap region that is multi-object, flagged, not summary
 task Startup( StartupObject s{ initialstate } ) {
 
+    /*
     while( false ) {
        Foo a = new Foo();
        a.x   = new Foo();
        a.x.x = new Foo();
     }
+    */
 
     taskexit( s{ !initialstate } );
 }