Token propagation implemented, stable but incorrect. This is just a capture.

[IRC.git] / Robust / src / Analysis / OwnershipAnalysis / ReferenceEdgeProperties.java

diff --git a/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdgeProperties.java b/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdgeProperties.java
index 3226d681a0ff5b28b4e5b11ed2fc5b4c38bab22f..4b85b2afa1c4c42cfceb8c679a1f2441aecf5ad5 100644 (file)
--- a/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdgeProperties.java
+++ b/Robust/src/Analysis/OwnershipAnalysis/ReferenceEdgeProperties.java
@@ -8,27 +8,20 @@ public class ReferenceEdgeProperties {
     protected ReachabilitySet beta;
     protected ReachabilitySet betaNew;
 
+    protected OwnershipNode  src;
+    protected HeapRegionNode dst;
 
     public ReferenceEdgeProperties() {
-       this.isUnique                = false;
-       this.isInitialParamReflexive = false;
-       this.beta                    = new ReachabilitySet();
-       this.betaNew                 = null;
+       this( false, false, null );
     }    
 
     public ReferenceEdgeProperties( boolean isUnique ) {
-       this.isUnique                = isUnique;
-       this.isInitialParamReflexive = false;
-       this.beta                    = new ReachabilitySet();
-       this.betaNew                 = null;
+       this( isUnique, false, null );
     }
 
     public ReferenceEdgeProperties( boolean isUnique,
                                    boolean isInitialParamReflexive ) {
-       this.isUnique                = isUnique;
-       this.isInitialParamReflexive = isInitialParamReflexive;
-       this.beta                    = new ReachabilitySet();
-       this.betaNew                 = null;
+       this( isUnique, isInitialParamReflexive, null );
     }
 
     public ReferenceEdgeProperties( boolean         isUnique,
@@ -36,11 +29,45 @@ public class ReferenceEdgeProperties {
                                    ReachabilitySet beta) {
        this.isUnique                = isUnique;
        this.isInitialParamReflexive = isInitialParamReflexive;
-       this.beta                    = beta;
-       this.betaNew                 = null;
+
+       // these members are set by higher-level code
+       // when this ReferenceEdgeProperties object is
+       // applied to an edge
+       this.src = null;
+       this.dst = null;
+
+       if( beta != null ) {
+           this.beta = beta;
+       } else {
+           this.beta = new ReachabilitySet();
+           this.beta = this.beta.makeCanonical();
+       }
+
+       betaNew = new ReachabilitySet();
+       betaNew = betaNew.makeCanonical();
+    }
+
+
+    public OwnershipNode getSrc() {
+       return src;
+    }
+
+    public void setSrc( OwnershipNode on ) {
+       assert on != null;
+       src = on;
+    }
+
+    public HeapRegionNode getDst() {
+       return dst;
+    }
+
+    public void setDst( HeapRegionNode hrn ) {
+       assert hrn != null;
+       dst = hrn;
     }
 
 
+    // copying does not copy source and destination members!
     public ReferenceEdgeProperties copy() {
        return new ReferenceEdgeProperties( isUnique,
                                            isInitialParamReflexive,
@@ -70,24 +97,34 @@ public class ReferenceEdgeProperties {
     public ReachabilitySet getBeta() {
        return beta;
     }
+
     public void setBeta( ReachabilitySet beta ) {
+       assert beta != null;
        this.beta = beta;
     }
 
     public ReachabilitySet getBetaNew() {
        return betaNew;
     }
+
     public void setBetaNew( ReachabilitySet beta ) {
+       assert beta != null;
        this.betaNew = beta;
     }
+
     public void applyBetaNew() {
        assert betaNew != null;
-       beta    = betaNew;
-       betaNew = null;
+
+       beta = betaNew;
+
+       betaNew = new ReachabilitySet();
+       betaNew = betaNew.makeCanonical();
     }
 
 
     public boolean equals( ReferenceEdgeProperties rep ) {
+       assert rep != null;
+       
        return isUnique                == rep.isUnique()                &&
               isInitialParamReflexive == rep.isInitialParamReflexive();
     }