changes.

diff --git a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
index d3e41d34ec4c05310694c5bde663eef4dc37f67d..b62472b4ee8fe4d3b39eae37365b072ec1c04604 100644 (file)
--- a/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
+++ b/Robust/src/Analysis/Disjoint/DisjointAnalysis.java
@@ -1349,7 +1349,8 @@ public class DisjointAnalysis {
         rg.removeAllStallSiteTaints();
 
         // inject taints for in-set vars      
-        rg.taintInSetVars( sese );                         
+        rg.taintInSetVars( sese );
+
       }
       break;
 
@@ -1382,24 +1383,7 @@ public class DisjointAnalysis {
       FlatCall         fc       = (FlatCall) fn;
       MethodDescriptor mdCallee = fc.getMethod();
       FlatMethod       fmCallee = state.getMethodFlat( mdCallee );
-      
-      // before transfer func, possibly inject
-      // stall-site taints
-      if( doEffectsAnalysis && fmContaining != fmAnalysisEntry ) {
-          
-        if(rblockStatus.isInCriticalRegion(fmContaining, fn)){
-          // x.y=f , stall x and y if they are not accessible
-          // also contribute write effects on stall site of x
-          if(!rg.isAccessible(fc.getThis())) {
-            rg.taintStallSite(fn, fc.getThis());
-          }
-            
-          // accessible status update
-          rg.makeAccessible(fc.getThis());
-        }
-      }
-      
-
+  
       boolean debugCallSite =
         mdCaller.getSymbol().equals( state.DISJOINTDEBUGCALLER ) &&
         mdCallee.getSymbol().equals( state.DISJOINTDEBUGCALLEE );

diff --git a/Robust/src/Analysis/Disjoint/ReachGraph.java b/Robust/src/Analysis/Disjoint/ReachGraph.java
index fee219b41af5022714a20c5ffce99b740bd94eb5..7ea4ebc466c286b430901fa8330293744302e929 100644 (file)
--- a/Robust/src/Analysis/Disjoint/ReachGraph.java
+++ b/Robust/src/Analysis/Disjoint/ReachGraph.java
@@ -460,6 +460,7 @@ public class ReachGraph {
       ReachSet       betaY = edgeY.getBeta();
 
       Iterator<RefEdge> itrHrnFhrn = hrnY.iteratorToReferencees();
+
       while( itrHrnFhrn.hasNext() ) {
        RefEdge        edgeHrn = itrHrnFhrn.next();
        HeapRegionNode hrnHrn  = edgeHrn.getDst();
@@ -489,7 +490,7 @@ public class ReachGraph {
                                        null,
                                        Canonical.intersection( betaY, betaHrn ),
                                        predsTrue,
-                                       edgeY.getTaints()
+                                       edgeHrn.getTaints()
                                        );
 
         addEdgeOrMergeWithExisting( edgeNew );
@@ -656,8 +657,7 @@ public class ReachGraph {
                                                predsTrue
                                                ),
                        predsTrue,
-                       Canonical.changePredsTo( edgeY.getTaints(),
-                                                predsTrue )
+                       edgeY.getTaints()
                        );
 
         addEdgeOrMergeWithExisting( edgeNew );
@@ -1296,6 +1296,9 @@ public class ReachGraph {
                  isv,
                  predsEmpty
                  );
+      
+      System.out.println("taint "+isv+" for "+sese);
+      writeGraph("taint");
     }
   }
 
@@ -1974,7 +1977,8 @@ public class ReachGraph {
                                       oocHrnIdOoc2callee 
                                       ),
                      preds,
-                     TaintSet.factory() // no taints for in-context edges
+                     toCalleeContext( reCaller.getTaints(),
+                         preds )
                      );
       
       rg.addRefEdge( hrnSrcCallee,
@@ -2200,7 +2204,7 @@ public class ReachGraph {
   private static boolean resolveMethodDebugDOThideReach       = true;
   private static boolean resolveMethodDebugDOThideSubsetReach = true;
   private static boolean resolveMethodDebugDOThidePreds       = true;
-  private static boolean resolveMethodDebugDOThideEdgeTaints  = true;
+  private static boolean resolveMethodDebugDOThideEdgeTaints  = false;
 
   static String debugGraphPrefix;
   static int debugCallSiteVisitCounter;
@@ -4363,7 +4367,7 @@ public class ReachGraph {
                 false, // hide reachability
                 true,  // hide subset reachability
                 true,  // hide predicates
-                true,  // hide edge taints                
+                false,  // hide edge taints                
                 null   // in-context boundary
                 );
   }