changes: now Inference engine works fine with the EyeTracking benchmark.
[IRC.git] / Robust / src / Analysis / SSJava / DefinitelyWrittenCheck.java
index 9f27398acbbab3e1b4d86aa0a5d55b53ba521a79..fabdf9dbbdbe09f2fb0f0f7c7c9b9618d53be0de 100644 (file)
@@ -8,6 +8,7 @@ import java.util.LinkedList;
 import java.util.Set;
 import java.util.Stack;
 
+import Analysis.Liveness;
 import Analysis.CallGraph.CallGraph;
 import Analysis.Loops.LoopFinder;
 import IR.Descriptor;
@@ -37,12 +38,9 @@ public class DefinitelyWrittenCheck {
   State state;
   CallGraph callGraph;
 
-  int debugcount = 0;
+  Liveness liveness;
 
-  // maps a descriptor to its known dependents: namely
-  // methods or tasks that call the descriptor's method
-  // AND are part of this analysis (reachable from main)
-  private Hashtable<Descriptor, Set<MethodDescriptor>> mapDescriptorToSetDependents;
+  int debugcount = 0;
 
   // maps a flat node to its WrittenSet: this keeps all heap path overwritten
   // previously.
@@ -69,6 +67,8 @@ public class DefinitelyWrittenCheck {
   // written to but not overwritten by the higher value
   private Hashtable<FlatMethod, SharedLocMap> mapFlatMethodToDeleteSet;
 
+  private Hashtable<FlatMethod, SharedLocMap> mapFlatMethodToMustClearMap;
+
   // maps a flat method to the S SET that is a set of heap path to shared
   // locations that are overwritten by the higher value
   private Hashtable<FlatMethod, SharedLocMap> mapFlatMethodToSharedLocMap;
@@ -115,10 +115,7 @@ public class DefinitelyWrittenCheck {
 
   private Hashtable<FlatNode, SharedLocMap> mapFlatNodeToSharedLocMapping;
   private Hashtable<FlatNode, SharedLocMap> mapFlatNodeToDeleteSet;
-
-  private Hashtable<Location, Set<Descriptor>> mapSharedLocationToCoverSet;
-
-  private LinkedList<MethodDescriptor> sortedDescriptors;
+  private Hashtable<FlatNode, SharedLocMap> mapFlatNodeToMustClearMap;
 
   private LoopFinder ssjavaLoop;
   private Set<FlatNode> loopIncElements;
@@ -128,6 +125,9 @@ public class DefinitelyWrittenCheck {
   private Set<NTuple<Descriptor>> calleeUnionBoundMayWriteSet;
   private SharedLocMap calleeUnionBoundDeleteSet;
   private SharedLocMap calleeIntersectBoundSharedSet;
+  private SharedLocMap calleeIntersectBoundMustClearSet;
+
+  Set<TempDescriptor> liveInTempSetToEventLoop;
 
   private Hashtable<Descriptor, Location> mapDescToLocation;
 
@@ -140,7 +140,6 @@ public class DefinitelyWrittenCheck {
     this.ssjava = ssjava;
     this.callGraph = ssjava.getCallGraph();
     this.mapFlatNodeToMustWriteSet = new Hashtable<FlatNode, Set<NTuple<Descriptor>>>();
-    this.mapDescriptorToSetDependents = new Hashtable<Descriptor, Set<MethodDescriptor>>();
     this.mapHeapPath = new Hashtable<Descriptor, NTuple<Descriptor>>();
     this.mapDescriptorToLocationPath = new Hashtable<TempDescriptor, NTuple<Location>>();
     this.mapFlatMethodToReadSet = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
@@ -162,7 +161,6 @@ public class DefinitelyWrittenCheck {
     this.mapFlatNodeToBoundReadSet = new Hashtable<FlatNode, Set<NTuple<Descriptor>>>();
     this.mapFlatNodeToBoundMustWriteSet = new Hashtable<FlatNode, Set<NTuple<Descriptor>>>();
     this.mapFlatNodeToBoundMayWriteSet = new Hashtable<FlatNode, Set<NTuple<Descriptor>>>();
-    this.mapSharedLocationToCoverSet = new Hashtable<Location, Set<Descriptor>>();
     this.mapFlatNodeToSharedLocMapping = new Hashtable<FlatNode, SharedLocMap>();
     this.mapFlatMethodToDeleteSet = new Hashtable<FlatMethod, SharedLocMap>();
     this.calleeUnionBoundDeleteSet = new SharedLocMap();
@@ -171,6 +169,11 @@ public class DefinitelyWrittenCheck {
     this.mapMethodToSharedLocCoverSet =
         new Hashtable<MethodDescriptor, MultiSourceMap<NTuple<Location>, NTuple<Descriptor>>>();
     this.mapFlatNodeToDeleteSet = new Hashtable<FlatNode, SharedLocMap>();
+    this.liveness = new Liveness();
+    this.liveInTempSetToEventLoop = new HashSet<TempDescriptor>();
+    this.mapFlatNodeToMustClearMap = new Hashtable<FlatNode, SharedLocMap>();
+    this.calleeIntersectBoundMustClearSet = new SharedLocMap();
+    this.mapFlatMethodToMustClearMap = new Hashtable<FlatMethod, SharedLocMap>();
   }
 
   public void definitelyWrittenCheck() {
@@ -190,8 +193,7 @@ public class DefinitelyWrittenCheck {
   private void sharedLocAnalysis() {
 
     // perform method READ/OVERWRITE analysis
-    LinkedList<MethodDescriptor> descriptorListToAnalyze =
-        (LinkedList<MethodDescriptor>) sortedDescriptors.clone();
+    LinkedList<MethodDescriptor> descriptorListToAnalyze = ssjava.getSortedDescriptors();
 
     // current descriptors to visit in fixed-point interprocedural analysis,
     // prioritized by
@@ -216,19 +218,23 @@ public class DefinitelyWrittenCheck {
 
       SharedLocMap sharedLocMap = new SharedLocMap();
       SharedLocMap deleteSet = new SharedLocMap();
+      SharedLocMap mustClearMap = new SharedLocMap();
 
-      sharedLoc_analyzeMethod(fm, sharedLocMap, deleteSet);
+      sharedLoc_analyzeMethod(fm, sharedLocMap, deleteSet, mustClearMap);
       SharedLocMap prevSharedLocMap = mapFlatMethodToSharedLocMap.get(fm);
       SharedLocMap prevDeleteSet = mapFlatMethodToDeleteSet.get(fm);
+      SharedLocMap prevMustClearMap = mapFlatMethodToMustClearMap.get(fm);
 
-      if (!(deleteSet.equals(prevDeleteSet) && sharedLocMap.equals(prevSharedLocMap))) {
+      if (!(deleteSet.equals(prevDeleteSet) && sharedLocMap.equals(prevSharedLocMap) && mustClearMap
+          .equals(prevMustClearMap))) {
         mapFlatMethodToSharedLocMap.put(fm, sharedLocMap);
         mapFlatMethodToDeleteSet.put(fm, deleteSet);
+        mapFlatMethodToMustClearMap.put(fm, mustClearMap);
 
         // results for callee changed, so enqueue dependents caller for
         // further
         // analysis
-        Iterator<MethodDescriptor> depsItr = getDependents(md).iterator();
+        Iterator<MethodDescriptor> depsItr = ssjava.getDependents(md).iterator();
         while (depsItr.hasNext()) {
           MethodDescriptor methodNext = depsItr.next();
           if (!methodDescriptorsToVisitStack.contains(methodNext)
@@ -252,23 +258,24 @@ public class DefinitelyWrittenCheck {
     }
     SharedLocMap sharedLocMap = new SharedLocMap();
     SharedLocMap deleteSet = new SharedLocMap();
+    SharedLocMap mustClearMap = new SharedLocMap();
     sharedLoc_analyzeBody(state.getMethodFlat(methodContainingSSJavaLoop),
-        ssjava.getSSJavaLoopEntrance(), sharedLocMap, deleteSet, true);
+        ssjava.getSSJavaLoopEntrance(), sharedLocMap, deleteSet, mustClearMap, true);
 
   }
 
   private void sharedLoc_analyzeMethod(FlatMethod fm, SharedLocMap sharedLocMap,
-      SharedLocMap deleteSet) {
+      SharedLocMap deleteSet, SharedLocMap mustClearMap) {
     if (state.SSJAVADEBUG) {
       System.out.println("SSJAVA: Definite clearance for shared locations Analyzing: " + fm);
     }
 
-    sharedLoc_analyzeBody(fm, fm, sharedLocMap, deleteSet, false);
+    sharedLoc_analyzeBody(fm, fm, sharedLocMap, deleteSet, mustClearMap, false);
 
   }
 
   private void sharedLoc_analyzeBody(FlatMethod fm, FlatNode startNode, SharedLocMap sharedLocMap,
-      SharedLocMap deleteSet, boolean isEventLoopBody) {
+      SharedLocMap deleteSet, SharedLocMap mustClearMap, boolean isEventLoopBody) {
 
     // intraprocedural analysis
     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
@@ -280,6 +287,7 @@ public class DefinitelyWrittenCheck {
 
       SharedLocMap currSharedSet = new SharedLocMap();
       SharedLocMap currDeleteSet = new SharedLocMap();
+      SharedLocMap currMustClearMap = new SharedLocMap();
 
       for (int i = 0; i < fn.numPrev(); i++) {
         FlatNode prevFn = fn.getPrev(i);
@@ -292,17 +300,26 @@ public class DefinitelyWrittenCheck {
         if (inDeleteLoc != null) {
           mergeDeleteSet(currDeleteSet, inDeleteLoc);
         }
+
+        SharedLocMap inMustClearMap = mapFlatNodeToMustClearMap.get(prevFn);
+        if (inMustClearMap != null) {
+          mergeSharedLocMap(currMustClearMap, inMustClearMap);
+        }
+
       }
 
-      sharedLoc_nodeActions(fm, fn, currSharedSet, currDeleteSet, sharedLocMap, deleteSet,
-          isEventLoopBody);
+      sharedLoc_nodeActions(fm, fn, currSharedSet, currDeleteSet, currMustClearMap, sharedLocMap,
+          deleteSet, mustClearMap, isEventLoopBody);
 
       SharedLocMap prevSharedSet = mapFlatNodeToSharedLocMapping.get(fn);
       SharedLocMap prevDeleteSet = mapFlatNodeToDeleteSet.get(fn);
+      SharedLocMap prevMustClearMap = mapFlatNodeToMustClearMap.get(fn);
 
-      if (!(currSharedSet.equals(prevSharedSet) && currDeleteSet.equals(prevDeleteSet))) {
+      if (!(currSharedSet.equals(prevSharedSet) && currDeleteSet.equals(prevDeleteSet) && currMustClearMap
+          .equals(prevMustClearMap))) {
         mapFlatNodeToSharedLocMapping.put(fn, currSharedSet);
         mapFlatNodeToDeleteSet.put(fn, currDeleteSet);
+        mapFlatNodeToMustClearMap.put(fn, currMustClearMap);
         for (int i = 0; i < fn.numNext(); i++) {
           FlatNode nn = fn.getNext(i);
           if ((!isEventLoopBody) || loopIncElements.contains(nn)) {
@@ -317,8 +334,8 @@ public class DefinitelyWrittenCheck {
   }
 
   private void sharedLoc_nodeActions(FlatMethod fm, FlatNode fn, SharedLocMap curr,
-      SharedLocMap currDeleteSet, SharedLocMap sharedLocMap, SharedLocMap deleteSet,
-      boolean isEventLoopBody) {
+      SharedLocMap currDeleteSet, SharedLocMap currMustClearMap, SharedLocMap sharedLocMap,
+      SharedLocMap deleteSet, SharedLocMap mustClearMap, boolean isEventLoopBody) {
 
     MethodDescriptor md = fm.getMethod();
 
@@ -329,6 +346,10 @@ public class DefinitelyWrittenCheck {
     TempDescriptor rhs;
     FieldDescriptor fld;
 
+    NTuple<Location> fieldLocTuple = null;
+    Location fieldLoc = null;
+    boolean isHigherWriteCase = false;
+
     switch (fn.kind()) {
 
     case FKind.FlatOpNode: {
@@ -343,31 +364,28 @@ public class DefinitelyWrittenCheck {
           if (!lhs.getSymbol().startsWith("neverused") && !lhs.getSymbol().startsWith("leftop")
               && !lhs.getSymbol().startsWith("rightop") && rhs.getType().isImmutable()) {
 
-            Location dstLoc = getLocation(lhs);
-            if (dstLoc != null && ssjava.isSharedLocation(dstLoc)) {
-              NTuple<Descriptor> lhsHeapPath = computePath(lhs);
-              NTuple<Location> lhsLocTuple = mapDescriptorToLocationPath.get(lhs);
+            if (mapHeapPath.containsKey(rhs)) {
+              Location dstLoc = getLocation(lhs);
+              if (dstLoc != null && ssjava.isSharedLocation(dstLoc)) {
+                NTuple<Descriptor> lhsHeapPath = computePath(lhs);
+                NTuple<Location> lhsLocTuple = mapDescriptorToLocationPath.get(lhs);
 
-              Location srcLoc = getLocation(lhs);
+                Location srcLoc = getLocation(lhs);
 
-              // computing gen/kill set
-              computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
-              if (!dstLoc.equals(srcLoc)) {
-                computeGENSetForHigherWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
-                updateDeleteSetForHigherWrite(currDeleteSet, lhsLocTuple, lhsHeapPath);
-              } else {
-                computeGENSetForSameHeightWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
-                updateDeleteSetForSameHeightWrite(currDeleteSet, lhsLocTuple, lhsHeapPath);
-              }
+                // computing gen/kill set
+                computeKILLSetForWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
 
-              // System.out.println("VAR WRITE:" + fn);
-              // System.out.println("lhsLocTuple=" + lhsLocTuple +
-              // " lhsHeapPath=" + lhsHeapPath);
-              // System.out.println("dstLoc=" + dstLoc + " srcLoc=" + srcLoc);
-              // System.out.println("KILLSET=" + killSet);
-              // System.out.println("GENSet=" + genSet);
-              // System.out.println("DELETESET=" + currDeleteSet);
+                if (!ssjava.isSameHeightWrite(fn)) {
+                  computeGENSetForHigherWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
+                  updateDeleteSetForHigherWrite(currDeleteSet, lhsLocTuple, lhsHeapPath);
+                } else {
+                  computeGENSetForSameHeightWrite(curr, killSet, lhsLocTuple, lhsHeapPath);
+                  updateDeleteSetForSameHeightWrite(currDeleteSet, lhsLocTuple, lhsHeapPath);
+                }
 
+              }
+            } else {
+              break;
             }
 
           }
@@ -382,7 +400,6 @@ public class DefinitelyWrittenCheck {
     case FKind.FlatSetFieldNode:
     case FKind.FlatSetElementNode: {
 
-      Location fieldLoc;
       if (fn.kind() == FKind.FlatSetFieldNode) {
         FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
         lhs = fsfn.getDst();
@@ -390,14 +407,7 @@ public class DefinitelyWrittenCheck {
         rhs = fsfn.getSrc();
         fieldLoc = (Location) fld.getType().getExtension();
       } else {
-        FlatSetElementNode fsen = (FlatSetElementNode) fn;
-        lhs = fsen.getDst();
-        rhs = fsen.getSrc();
-        TypeDescriptor td = lhs.getType().dereference();
-        fld = getArrayField(td);
-
-        NTuple<Location> locTuple = deriveLocationTuple(md, lhs);
-        fieldLoc = locTuple.get(locTuple.size() - 1);
+        break;
       }
 
       if (!isEventLoopBody && fieldLoc.getDescriptor().equals(md)) {
@@ -406,7 +416,7 @@ public class DefinitelyWrittenCheck {
         break;
       }
 
-      NTuple<Location> fieldLocTuple = new NTuple<Location>();
+      fieldLocTuple = new NTuple<Location>();
       if (fld.isStatic()) {
         if (fld.isFinal()) {
           // in this case, fld has TOP location
@@ -438,26 +448,24 @@ public class DefinitelyWrittenCheck {
 
         NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>();
         fldHeapPath.addAll(computePath(lhs));
-        fldHeapPath.add(fld);
+        if (fn.kind() == FKind.FlatSetFieldNode) {
+          fldHeapPath.add(fld);
+        }
 
         // computing gen/kill set
         computeKILLSetForWrite(curr, killSet, fieldLocTuple, fldHeapPath);
-        if (!fieldLoc.equals(srcLoc)) {
+
+        if (!ssjava.isSameHeightWrite(fn)) {
           computeGENSetForHigherWrite(curr, genSet, fieldLocTuple, fldHeapPath);
           updateDeleteSetForHigherWrite(currDeleteSet, fieldLocTuple, fldHeapPath);
+
+          isHigherWriteCase = true;
+
         } else {
           computeGENSetForSameHeightWrite(curr, genSet, fieldLocTuple, fldHeapPath);
           updateDeleteSetForSameHeightWrite(currDeleteSet, fieldLocTuple, fldHeapPath);
         }
 
-        // System.out.println("################");
-        // System.out.println("FIELD WRITE:" + fn);
-        // System.out.println("FldHeapPath=" + fldHeapPath);
-        // System.out.println("fieldLocTuple=" + fieldLocTuple + " srcLoc=" +
-        // srcLoc);
-        // System.out.println("KILLSET=" + killSet);
-        // System.out.println("GENSet=" + genSet);
-        // System.out.println("DELETESET=" + currDeleteSet);
       }
 
     }
@@ -466,19 +474,17 @@ public class DefinitelyWrittenCheck {
     case FKind.FlatCall: {
       FlatCall fc = (FlatCall) fn;
 
-      if (ssjava.needTobeAnnotated(fc.getMethod())) {
+      bindHeapPathCallerArgWithCaleeParamForSharedLoc(fm.getMethod(), fc);
 
-        bindHeapPathCallerArgWithCaleeParamForSharedLoc(fm.getMethod(), fc);
-
-        // computing gen/kill set
-        generateKILLSetForFlatCall(curr, killSet);
-        generateGENSetForFlatCall(curr, genSet);
+      // computing gen/kill set
+      generateKILLSetForFlatCall(curr, killSet);
+      generateGENSetForFlatCall(curr, genSet);
 
+      Set<NTuple<Location>> locTupleSet = calleeIntersectBoundMustClearSet.keySet();
+      for (Iterator iterator = locTupleSet.iterator(); iterator.hasNext();) {
+        NTuple<Location> locTupleKey = (NTuple<Location>) iterator.next();
+        currMustClearMap.addWrite(locTupleKey, calleeIntersectBoundMustClearSet.get(locTupleKey));
       }
-//      System.out.println("#FLATCALL=" + fc);
-//      System.out.println("KILLSET=" + killSet);
-//      System.out.println("GENSet=" + genSet);
-//      System.out.println("bound DELETE Set=" + calleeUnionBoundDeleteSet);
 
     }
       break;
@@ -487,17 +493,38 @@ public class DefinitelyWrittenCheck {
       // merge the current delete/shared loc mapping
       mergeSharedLocMap(sharedLocMap, curr);
       mergeDeleteSet(deleteSet, currDeleteSet);
-
-      // System.out.println("#FLATEXIT sharedLocMap=" + sharedLocMap);
+      mergeSharedLocMap(mustClearMap, currMustClearMap);
     }
       break;
 
     }
 
     computeNewMapping(curr, killSet, genSet);
-    if (!curr.map.isEmpty()) {
-//      System.out.println(fn + "#######" + curr);
+    if (isHigherWriteCase) {
+      // check all locations with the same shared location are cleared out at this point
+      Set<NTuple<Descriptor>> writtenSet = curr.get(fieldLocTuple);
+      Set<Descriptor> requirementSet = ssjava.getSharedDescSet(fieldLoc);
+
+      if (checkAllSharedLocationsAreOverwritten(requirementSet, writtenSet)) {
+        currMustClearMap.addWrite(fieldLocTuple, writtenSet);
+      }
     }
+  }
+
+  private boolean checkAllSharedLocationsAreOverwritten(Set<Descriptor> sharedDescSet,
+      Set<NTuple<Descriptor>> writtenSet) {
+
+    if (sharedDescSet == null || writtenSet == null) {
+      return false;
+    }
+    Set<Descriptor> writtenDescSet = new HashSet<Descriptor>();
+    for (Iterator iterator = writtenSet.iterator(); iterator.hasNext();) {
+      NTuple<Descriptor> tuple = (NTuple<Descriptor>) iterator.next();
+      writtenDescSet.add(tuple.get(tuple.size() - 1));
+    }
+
+    return writtenDescSet.containsAll(sharedDescSet);
+    // return sharedDescSet.containsAll(writtenDescSet);
 
   }
 
@@ -559,7 +586,6 @@ public class DefinitelyWrittenCheck {
     if (currWriteSet != null) {
       genSet.addWrite(locTuple, currWriteSet);
     }
-
     genSet.addWrite(locTuple, hp);
   }
 
@@ -602,8 +628,7 @@ public class DefinitelyWrittenCheck {
   }
 
   private void computeSharedCoverSet() {
-    LinkedList<MethodDescriptor> descriptorListToAnalyze =
-        (LinkedList<MethodDescriptor>) sortedDescriptors.clone();
+    LinkedList<MethodDescriptor> descriptorListToAnalyze = ssjava.getSortedDescriptors();
 
     // current descriptors to visit in fixed-point interprocedural analysis,
     // prioritized by
@@ -637,8 +662,8 @@ public class DefinitelyWrittenCheck {
 
   private void computeSharedCoverSet_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) {
 
-    System.out.println("computeSharedCoverSet_analyzeMethod=" + fm);
     MethodDescriptor md = fm.getMethod();
+
     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
 
     Set<FlatNode> visited = new HashSet<FlatNode>();
@@ -693,10 +718,6 @@ public class DefinitelyWrittenCheck {
         if (lhs.getType().getExtension() instanceof SSJavaType) {
           CompositeLocation compLoc = ((SSJavaType) lhs.getType().getExtension()).getCompLoc();
           Location lastLocElement = compLoc.get(compLoc.getSize() - 1);
-          // check if the last one is shared loc
-          if (ssjava.isSharedLocation(lastLocElement)) {
-            addSharedLocDescriptor(lastLocElement, lhs);
-          }
         }
       }
 
@@ -714,53 +735,59 @@ public class DefinitelyWrittenCheck {
         if (!lhs.getSymbol().startsWith("neverused") && !lhs.getSymbol().startsWith("leftop")
             && !lhs.getSymbol().startsWith("rightop")) {
 
-          NTuple<Location> rhsLocTuple = new NTuple<Location>();
-          NTuple<Location> lhsLocTuple = new NTuple<Location>();
-          if (mapDescriptorToLocationPath.containsKey(rhs)) {
-            mapDescriptorToLocationPath.put(lhs, mapDescriptorToLocationPath.get(rhs));
-          } else {
-            // rhs side
-            if (rhs.getType().getExtension() != null
-                && rhs.getType().getExtension() instanceof SSJavaType) {
+          if (mapHeapPath.containsKey(rhs)) {
+            NTuple<Location> rhsLocTuple = new NTuple<Location>();
+            NTuple<Location> lhsLocTuple = new NTuple<Location>();
+            if (mapDescriptorToLocationPath.containsKey(rhs)) {
+              mapDescriptorToLocationPath.put(lhs, deriveLocationTuple(md, rhs));
+              lhsLocTuple = mapDescriptorToLocationPath.get(lhs);
+            } else {
+              // rhs side
+              if (rhs.getType().getExtension() != null
+                  && rhs.getType().getExtension() instanceof SSJavaType) {
 
-              if (((SSJavaType) rhs.getType().getExtension()).getCompLoc() != null) {
-                rhsLocTuple.addAll(((SSJavaType) rhs.getType().getExtension()).getCompLoc()
-                    .getTuple());
-              }
+                if (((SSJavaType) rhs.getType().getExtension()).getCompLoc() != null) {
+                  rhsLocTuple.addAll(((SSJavaType) rhs.getType().getExtension()).getCompLoc()
+                      .getTuple());
+                }
 
-            } else {
-              NTuple<Location> locTuple = deriveLocationTuple(md, rhs);
-              if (locTuple != null) {
-                rhsLocTuple.addAll(locTuple);
+              } else {
+                NTuple<Location> locTuple = deriveLocationTuple(md, rhs);
+                if (locTuple != null) {
+                  rhsLocTuple.addAll(locTuple);
+                }
+              }
+              if (rhsLocTuple.size() > 0) {
+                mapDescriptorToLocationPath.put(rhs, rhsLocTuple);
               }
-            }
-            if (rhsLocTuple.size() > 0) {
-              mapDescriptorToLocationPath.put(rhs, rhsLocTuple);
-            }
 
-            // lhs side
-            if (lhs.getType().getExtension() != null
-                && lhs.getType().getExtension() instanceof SSJavaType) {
-              lhsLocTuple.addAll(((SSJavaType) lhs.getType().getExtension()).getCompLoc()
-                  .getTuple());
-              mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
-            } else if (mapDescriptorToLocationPath.get(rhs) != null) {
-              // propagate rhs's location to lhs
-              lhsLocTuple.addAll(mapDescriptorToLocationPath.get(rhs));
-              mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+              // lhs side
+              if (lhs.getType().getExtension() != null
+                  && lhs.getType().getExtension() instanceof SSJavaType) {
+                lhsLocTuple.addAll(((SSJavaType) lhs.getType().getExtension()).getCompLoc()
+                    .getTuple());
+                mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+              } else if (mapDescriptorToLocationPath.get(rhs) != null) {
+                // propagate rhs's location to lhs
+                lhsLocTuple.addAll(mapDescriptorToLocationPath.get(rhs));
+                mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+              }
             }
 
-          }
+            if (isEventLoopBody && lhs.getType().isPrimitive()
+                && !lhs.getSymbol().startsWith("srctmp")) {
 
-          if (lhs.getType().isPrimitive() && !lhs.getSymbol().startsWith("srctmp")) {
+              NTuple<Descriptor> lhsHeapPath = computePath(lhs);
 
-            NTuple<Descriptor> lhsHeapPath = computePath(lhs);
+              if (lhsLocTuple != null) {
+                addMayWrittenSet(md, lhsLocTuple, lhsHeapPath);
+              }
 
-            if (lhsLocTuple != null) {
-              addMayWrittenSet(md, lhsLocTuple, lhsHeapPath);
             }
-
+          } else {
+            break;
           }
+
         }
 
       }
@@ -785,57 +812,58 @@ public class DefinitelyWrittenCheck {
         fld = getArrayField(td);
       }
 
-      Location fieldLocation;
-      if (fn.kind() == FKind.FlatSetFieldNode) {
-        fieldLocation = (Location) fld.getType().getExtension();
-      } else {
-        NTuple<Location> locTuple = mapDescriptorToLocationPath.get(lhs);
-        fieldLocation = locTuple.get(locTuple.size() - 1);
-      }
-
-      if (!isEventLoopBody && fieldLocation.getDescriptor().equals(md)) {
-        // if the field belongs to the local lattice, no reason to calculate
-        // shared location
-        break;
-      }
-
-      NTuple<Location> fieldLocTuple = new NTuple<Location>();
+      NTuple<Location> lhsLocTuple = new NTuple<Location>();
       if (fld.isStatic()) {
         if (fld.isFinal()) {
           // in this case, fld has TOP location
           Location topLocation = Location.createTopLocation(md);
-          fieldLocTuple.add(topLocation);
+          lhsLocTuple.add(topLocation);
         } else {
-          fieldLocTuple.addAll(deriveGlobalLocationTuple(md));
-          if (fn.kind() == FKind.FlatSetFieldNode) {
-            fieldLocTuple.add((Location) fld.getType().getExtension());
-          }
+          lhsLocTuple.addAll(deriveGlobalLocationTuple(md));
         }
-
       } else {
-        fieldLocTuple.addAll(deriveLocationTuple(md, lhs));
-        if (fn.kind() == FKind.FlatSetFieldNode) {
-          fieldLocTuple.add((Location) fld.getType().getExtension());
-        }
+        lhsLocTuple.addAll(deriveLocationTuple(md, lhs));
       }
 
-      NTuple<Location> lTuple = deriveLocationTuple(md, lhs);
-      if (lTuple != null) {
-        NTuple<Location> lhsLocTuple = new NTuple<Location>();
-        lhsLocTuple.addAll(lTuple);
-        mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+      mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+
+      NTuple<Location> fieldLocTuple = new NTuple<Location>();
+      fieldLocTuple.addAll(lhsLocTuple);
+
+      if (fn.kind() == FKind.FlatSetFieldNode) {
+        fieldLocTuple.add((Location) fld.getType().getExtension());
       }
 
-      if (ssjava.isSharedLocation(fieldLocation)) {
-        addSharedLocDescriptor(fieldLocation, fld);
+      if (mapHeapPath.containsKey(lhs)) {
+        // fields reachable from the param can have heap path entry.
+        NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
+        lhsHeapPath.addAll(mapHeapPath.get(lhs));
 
-        NTuple<Descriptor> fieldHeapPath = new NTuple<Descriptor>();
-        fieldHeapPath.addAll(computePath(lhs));
-        fieldHeapPath.add(fld);
+        Location fieldLocation;
+        if (fn.kind() == FKind.FlatSetFieldNode) {
+          fieldLocation = getLocation(fld);
+        } else {
+          fieldLocation = getLocation(lhsHeapPath.get(getArrayBaseDescriptorIdx(lhsHeapPath)));
+        }
+
+        // Location fieldLocation = getLocation(lhs);
+        if (!isEventLoopBody && fieldLocation.getDescriptor().equals(md)) {
+          // if the field belongs to the local lattice, no reason to calculate
+          // shared location
+          break;
+        }
 
-        // mapLocationPathToMayWrittenSet.put(locTuple, null, fld);
-        addMayWrittenSet(md, fieldLocTuple, fieldHeapPath);
+        if (ssjava.isSharedLocation(fieldLocation)) {
 
+          NTuple<Descriptor> fieldHeapPath = new NTuple<Descriptor>();
+          fieldHeapPath.addAll(computePath(lhs));
+          if (fn.kind() == FKind.FlatSetFieldNode) {
+            fieldHeapPath.add(fld);
+          }
+
+          addMayWrittenSet(md, fieldLocTuple, fieldHeapPath);
+
+        }
       }
 
     }
@@ -890,9 +918,7 @@ public class DefinitelyWrittenCheck {
 
       FlatCall fc = (FlatCall) fn;
 
-      if (ssjava.needTobeAnnotated(fc.getMethod())) {
-        bindLocationPathCallerArgWithCalleeParam(md, fc);
-      }
+      bindLocationPathCallerArgWithCalleeParam(md, fc);
 
     }
       break;
@@ -941,7 +967,7 @@ public class DefinitelyWrittenCheck {
       NTuple<Location> argLocationPath = deriveLocationTuple(mdCaller, arg);
       NTuple<Descriptor> argHeapPath = computePath(arg);
       addMayWrittenSet(mdCaller, argLocationPath, argHeapPath);
-    } else {
+    } else if (ssjava.needTobeAnnotated(fc.getMethod())) {
 
       // if arg is not primitive type, we need to propagate maywritten set to
       // the caller's location path
@@ -958,52 +984,46 @@ public class DefinitelyWrittenCheck {
       Hashtable<Integer, NTuple<Location>> mapArgIdx2CallerArgLocationPath =
           new Hashtable<Integer, NTuple<Location>>();
 
-      // arg idx is starting from 'this' arg
       if (fc.getThis() != null) {
-        // loc path for 'this'
-        NTuple<Location> thisLocationPath = deriveLocationTuple(mdCaller, fc.getThis());
-        if (thisLocationPath != null) {
-          mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(0), thisLocationPath);
 
-          // heap path for 'this'
-          NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
-          if (thisHeapPath == null) {
-            // method is called without creating new flat node representing
-            // 'this'
-            thisHeapPath = new NTuple<Descriptor>();
-            thisHeapPath.add(fc.getThis());
-          }
+        if (mapHeapPath.containsKey(fc.getThis())) {
+
+          // setup heap path for 'this'
+          NTuple<Descriptor> thisHeapPath = new NTuple<Descriptor>();
+          thisHeapPath.addAll(mapHeapPath.get(fc.getThis()));
           mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
-        }
 
+          // setup location path for 'this'
+          NTuple<Location> thisLocationPath = deriveLocationTuple(mdCaller, fc.getThis());
+          mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(0), thisLocationPath);
+
+        }
       }
 
       for (int i = 0; i < fc.numArgs(); i++) {
         TempDescriptor arg = fc.getArg(i);
         // create mapping arg to loc path
-        NTuple<Location> argLocationPath = deriveLocationTuple(mdCaller, arg);
-        if (argLocationPath != null) {
-          mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(i + 1), argLocationPath);
-          // create mapping arg to heap path
-          NTuple<Descriptor> argHeapPath = computePath(arg);
+
+        if (mapHeapPath.containsKey(arg)) {
+          // setup heap path
+          NTuple<Descriptor> argHeapPath = mapHeapPath.get(arg);
           mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
+          // setup loc path
+          NTuple<Location> argLocationPath = deriveLocationTuple(mdCaller, arg);
+          mapArgIdx2CallerArgLocationPath.put(Integer.valueOf(i + 1), argLocationPath);
         }
 
       }
 
-      Hashtable<Integer, Set<NTuple<Descriptor>>> mapParamIdx2WriteSet =
-          new Hashtable<Integer, Set<NTuple<Descriptor>>>();
-
-      for (int i = 0; i < fc.numArgs() + 1; i++) {
-        mapParamIdx2WriteSet.put(Integer.valueOf(i), new HashSet<NTuple<Descriptor>>());
-      }
-
       for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
         MethodDescriptor callee = (MethodDescriptor) iterator.next();
         FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
 
         // binding caller's args and callee's params
 
+        Hashtable<NTuple<Descriptor>, NTuple<Descriptor>> mapParamHeapPathToCallerArgHeapPath =
+            new Hashtable<NTuple<Descriptor>, NTuple<Descriptor>>();
+
         Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
             new Hashtable<Integer, TempDescriptor>();
         int offset = 0;
@@ -1011,26 +1031,40 @@ public class DefinitelyWrittenCheck {
           // static method does not have implicit 'this' arg
           offset = 1;
         }
+
         for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
           TempDescriptor param = calleeFlatMethod.getParameter(i);
           mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param);
+
+          NTuple<Descriptor> calleeHeapPath = computePath(param);
+
+          NTuple<Descriptor> argHeapPath =
+              mapArgIdx2CallerArgHeapPath.get(Integer.valueOf(i + offset));
+
+          if (argHeapPath != null) {
+            mapParamHeapPathToCallerArgHeapPath.put(calleeHeapPath, argHeapPath);
+
+          }
+
         }
 
         Set<Integer> keySet = mapArgIdx2CallerArgLocationPath.keySet();
         for (Iterator iterator2 = keySet.iterator(); iterator2.hasNext();) {
           Integer idx = (Integer) iterator2.next();
+
           NTuple<Location> callerArgLocationPath = mapArgIdx2CallerArgLocationPath.get(idx);
 
           TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx);
+          NTuple<Location> calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam);
 
           NTuple<Descriptor> callerArgHeapPath = mapArgIdx2CallerArgHeapPath.get(idx);
-          NTuple<Location> calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam);
           NTuple<Descriptor> calleeHeapPath = computePath(calleeParam);
 
-          createNewMappingOfMayWrittenSet(mdCaller, callee, callerArgHeapPath,
-              callerArgLocationPath, calleeHeapPath, calleeLocationPath,
-              mapParamIdx2WriteSet.get(idx));
-
+          if (!calleeParam.getType().isPrimitive()) {
+            createNewMappingOfMayWrittenSet(mdCaller, callee, callerArgHeapPath,
+                callerArgLocationPath, calleeHeapPath, calleeLocationPath,
+                mapParamHeapPathToCallerArgHeapPath);
+          }
         }
 
       }
@@ -1061,7 +1095,7 @@ public class DefinitelyWrittenCheck {
   private void createNewMappingOfMayWrittenSet(MethodDescriptor caller, MethodDescriptor callee,
       NTuple<Descriptor> callerArgHeapPath, NTuple<Location> callerArgLocPath,
       NTuple<Descriptor> calleeParamHeapPath, NTuple<Location> calleeParamLocPath,
-      Set<NTuple<Descriptor>> writeSet) {
+      Hashtable<NTuple<Descriptor>, NTuple<Descriptor>> mapParamHeapPathToCallerArgHeapPath) {
 
     // propagate may-written-set associated with the key that is started with
     // calleepath to the caller
@@ -1073,6 +1107,10 @@ public class DefinitelyWrittenCheck {
     MultiSourceMap<NTuple<Location>, NTuple<Descriptor>> calleeMapping =
         mapMethodToSharedLocCoverSet.get(callee);
 
+    if (calleeMapping == null) {
+      return;
+    }
+
     MultiSourceMap<NTuple<Location>, NTuple<Descriptor>> callerMapping =
         mapMethodToSharedLocCoverSet.get(caller);
 
@@ -1081,24 +1119,25 @@ public class DefinitelyWrittenCheck {
       mapMethodToSharedLocCoverSet.put(caller, callerMapping);
     }
 
-    if (calleeMapping == null) {
-      return;
-    }
-
     Hashtable<NTuple<Location>, Set<NTuple<Descriptor>>> paramMapping =
         getMappingByStartedWith(calleeMapping, calleeParamLocPath);
 
-    Set<NTuple<Location>> calleeKeySet = calleeMapping.keySet();
+    Set<NTuple<Location>> calleeKeySet = paramMapping.keySet();
+
     for (Iterator iterator = calleeKeySet.iterator(); iterator.hasNext();) {
       NTuple<Location> calleeKey = (NTuple<Location>) iterator.next();
+
       Set<NTuple<Descriptor>> calleeMayWriteSet = paramMapping.get(calleeKey);
 
       if (calleeMayWriteSet != null) {
 
-        Set<NTuple<Descriptor>> boundWriteSet =
-            convertCallerMayWriteSet(callerArgHeapPath, calleeParamHeapPath, calleeMayWriteSet);
+        Set<NTuple<Descriptor>> boundMayWriteSet = new HashSet<NTuple<Descriptor>>();
 
-        writeSet.addAll(boundWriteSet);
+        Set<NTuple<Descriptor>> boundSet =
+            convertToCallerMayWriteSet(calleeParamHeapPath, calleeMayWriteSet, callerMapping,
+                mapParamHeapPathToCallerArgHeapPath);
+
+        boundMayWriteSet.addAll(boundSet);
 
         NTuple<Location> newKey = new NTuple<Location>();
         newKey.addAll(callerArgLocPath);
@@ -1108,16 +1147,17 @@ public class DefinitelyWrittenCheck {
           newKey.add(calleeKey.get(i));
         }
 
-        callerMapping.union(newKey, writeSet);
-        // mapLocationPathToMayWrittenSet.put(calleeKey, newKey, writeSet);
+        callerMapping.union(newKey, boundMayWriteSet);
       }
 
     }
 
   }
 
-  private Set<NTuple<Descriptor>> convertCallerMayWriteSet(NTuple<Descriptor> callerArgHeapPath,
-      NTuple<Descriptor> calleeParamHeapPath, Set<NTuple<Descriptor>> calleeMayWriteSet) {
+  private Set<NTuple<Descriptor>> convertToCallerMayWriteSet(
+      NTuple<Descriptor> calleeParamHeapPath, Set<NTuple<Descriptor>> calleeMayWriteSet,
+      MultiSourceMap<NTuple<Location>, NTuple<Descriptor>> callerMapping,
+      Hashtable<NTuple<Descriptor>, NTuple<Descriptor>> mapParamHeapPathToCallerArgHeapPath) {
 
     Set<NTuple<Descriptor>> boundSet = new HashSet<NTuple<Descriptor>>();
 
@@ -1125,12 +1165,15 @@ public class DefinitelyWrittenCheck {
     for (Iterator iterator = calleeMayWriteSet.iterator(); iterator.hasNext();) {
       NTuple<Descriptor> calleeWriteHeapPath = (NTuple<Descriptor>) iterator.next();
 
+      NTuple<Descriptor> writeHeapPathParamHeapPath = calleeWriteHeapPath.subList(0, 1);
+
+      NTuple<Descriptor> callerArgHeapPath =
+          mapParamHeapPathToCallerArgHeapPath.get(writeHeapPathParamHeapPath);
+
       NTuple<Descriptor> boundHeapPath = new NTuple<Descriptor>();
       boundHeapPath.addAll(callerArgHeapPath);
 
-      int startIdx = calleeParamHeapPath.size();
-
-      for (int i = startIdx; i < calleeWriteHeapPath.size(); i++) {
+      for (int i = 1; i < calleeWriteHeapPath.size(); i++) {
         boundHeapPath.add(calleeWriteHeapPath.get(i));
       }
 
@@ -1141,18 +1184,6 @@ public class DefinitelyWrittenCheck {
     return boundSet;
   }
 
-  private void addSharedLocDescriptor(Location sharedLoc, Descriptor desc) {
-
-    Set<Descriptor> descSet = mapSharedLocationToCoverSet.get(sharedLoc);
-    if (descSet == null) {
-      descSet = new HashSet<Descriptor>();
-      mapSharedLocationToCoverSet.put(sharedLoc, descSet);
-    }
-
-    descSet.add(desc);
-
-  }
-
   private Location getLocation(Descriptor d) {
 
     if (d instanceof FieldDescriptor) {
@@ -1289,7 +1320,6 @@ public class DefinitelyWrittenCheck {
               && !lhs.getSymbol().startsWith("rightop")) {
 
             boolean hasWriteEffect = false;
-            NTuple<Descriptor> rhsHeapPath = computePath(rhs);
 
             if (rhs.getType().getExtension() instanceof SSJavaType
                 && lhs.getType().getExtension() instanceof SSJavaType) {
@@ -1309,10 +1339,11 @@ public class DefinitelyWrittenCheck {
               hasWriteEffect = true;
             }
 
-            if (hasWriteEffect) {
+            if (hasWriteEffect && mapHeapPath.containsKey(lhs)) {
               // write(lhs)
-              NTuple<Descriptor> lhsPath = new NTuple<Descriptor>();
-              lhsPath.add(lhs);
+              NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
+              lhsHeapPath.addAll(mapHeapPath.get(lhs));
+
               Location lhsLoc = getLocation(lhs);
               if (ssjava.isSharedLocation(lhsLoc)) {
 
@@ -1322,7 +1353,10 @@ public class DefinitelyWrittenCheck {
                 Set<NTuple<Descriptor>> writtenSet =
                     mapFlatNodeToSharedLocMapping.get(fn).get(varLocTuple);
 
-                if (isCovered(varLocTuple, writtenSet)) {
+                Set<NTuple<Descriptor>> mustClearSet =
+                    mapFlatNodeToMustClearMap.get(fn).get(varLocTuple);
+
+                if (isCovered(varLocTuple, writtenSet, mustClearSet)) {
                   computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet);
                   computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet);
                 } else {
@@ -1331,15 +1365,12 @@ public class DefinitelyWrittenCheck {
 
               } else {
 
-                computeKILLSetForWrite(curr, lhsPath, readWriteKillSet);
-                computeGENSetForWrite(lhsPath, readWriteGenSet);
+                computeKILLSetForWrite(curr, lhsHeapPath, readWriteKillSet);
+                computeGENSetForWrite(lhsHeapPath, readWriteGenSet);
               }
 
-              // System.out.println("#KILLSET=" + readWriteKillSet);
-              // System.out.println("#GENSet=" + readWriteGenSet + "\n");
-
-              Set<WriteAge> writeAgeSet = curr.get(lhsPath);
-              checkWriteAgeSet(writeAgeSet, lhsPath, fn);
+              Set<WriteAge> writeAgeSet = curr.get(lhsHeapPath);
+              checkWriteAgeSet(writeAgeSet, lhsHeapPath, fn);
             }
 
           }
@@ -1399,61 +1430,67 @@ public class DefinitelyWrittenCheck {
           fld = getArrayField(td);
         }
 
-        // System.out.println("FIELD WRITE:" + fn);
+        // set up heap path
+        NTuple<Descriptor> lhsHeapPath = mapHeapPath.get(lhs);
+        if (lhsHeapPath != null) {
+          // write(field)
+          NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
+          if (fn.kind() == FKind.FlatSetFieldNode) {
+            fldHeapPath.add(fld);
+          }
 
-        // write(field)
-        NTuple<Descriptor> lhsHeapPath = computePath(lhs);
-        NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
-        fldHeapPath.add(fld);
+          // shared loc extension
+          Location fieldLoc;
+          if (fn.kind() == FKind.FlatSetFieldNode) {
+            fieldLoc = (Location) fld.getType().getExtension();
+          } else {
+            NTuple<Location> locTuple = mapDescriptorToLocationPath.get(lhs);
+            fieldLoc = locTuple.get(locTuple.size() - 1);
+          }
 
-        // shared loc extension
-        Location fieldLoc = (Location) fld.getType().getExtension();
-        if (ssjava.isSharedLocation(fieldLoc)) {
+          if (ssjava.isSharedLocation(fieldLoc)) {
 
-          NTuple<Location> fieldLocTuple = new NTuple<Location>();
-          fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs));
-          fieldLocTuple.add(fieldLoc);
+            NTuple<Location> fieldLocTuple = new NTuple<Location>();
+            fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs));
+            if (fn.kind() == FKind.FlatSetFieldNode) {
+              fieldLocTuple.add(fieldLoc);
+            }
 
-          Set<NTuple<Descriptor>> writtenSet =
-              mapFlatNodeToSharedLocMapping.get(fn).get(fieldLocTuple);
+            Set<NTuple<Descriptor>> writtenSet =
+                mapFlatNodeToSharedLocMapping.get(fn).get(fieldLocTuple);
+            if (isCovered(fieldLocTuple, writtenSet)) {
+              computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet);
+              computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet);
+            } else {
+              computeGENSetForSharedNonCoverWrite(curr, fldHeapPath, readWriteGenSet);
+            }
 
-          if (isCovered(fieldLocTuple, writtenSet)) {
-            computeKILLSetForSharedWrite(curr, writtenSet, readWriteKillSet);
-            computeGENSetForSharedAllCoverWrite(curr, writtenSet, readWriteGenSet);
           } else {
-            computeGENSetForSharedNonCoverWrite(curr, fldHeapPath, readWriteGenSet);
+            computeKILLSetForWrite(curr, fldHeapPath, readWriteKillSet);
+            computeGENSetForWrite(fldHeapPath, readWriteGenSet);
           }
 
-        } else {
-          computeKILLSetForWrite(curr, fldHeapPath, readWriteKillSet);
-          computeGENSetForWrite(fldHeapPath, readWriteGenSet);
         }
 
-        // System.out.println("KILLSET=" + readWriteKillSet);
-        // System.out.println("GENSet=" + readWriteGenSet);
-
       }
         break;
 
       case FKind.FlatCall: {
         FlatCall fc = (FlatCall) fn;
-
         SharedLocMap sharedLocMap = mapFlatNodeToSharedLocMapping.get(fc);
-        // System.out.println("FLATCALL:" + fn);
-        generateKILLSetForFlatCall(fc, curr, sharedLocMap, readWriteKillSet);
-        generateGENSetForFlatCall(fc, sharedLocMap, readWriteGenSet);
-
-//        System.out.println("KILLSET=" + readWriteKillSet);
-//        System.out.println("GENSet=" + readWriteGenSet);
+        SharedLocMap mustClearMap = mapFlatNodeToMustClearMap.get(fc);
+        generateKILLSetForFlatCall(fc, curr, sharedLocMap, mustClearMap, readWriteKillSet);
+        generateGENSetForFlatCall(fc, sharedLocMap, mustClearMap, readWriteGenSet);
 
-        checkManyRead(fc, curr);
       }
         break;
 
       }
 
       computeNewMapping(curr, readWriteKillSet, readWriteGenSet);
-//      System.out.println("#######" + curr);
+      if (fn instanceof FlatCall) {
+        checkManyRead((FlatCall) fn, curr);
+      }
 
     }
 
@@ -1501,22 +1538,37 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  private boolean isCovered(NTuple<Location> locTuple, Set<NTuple<Descriptor>> inSet) {
+  private boolean isCovered(NTuple<Location> locTuple, Set<NTuple<Descriptor>> curWrittenSet) {
+
+    Set<NTuple<Descriptor>> coverSet =
+        mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
 
-    if (inSet == null) {
+    if (curWrittenSet == null) {
       return false;
     }
 
+    return curWrittenSet.containsAll(coverSet);
+  }
+
+  private boolean isCovered(NTuple<Location> locTuple, Set<NTuple<Descriptor>> curWrittenSet,
+      Set<NTuple<Descriptor>> mustClearSet) {
+
     Set<NTuple<Descriptor>> coverSet =
         mapMethodToSharedLocCoverSet.get(methodContainingSSJavaLoop).get(locTuple);
 
-    return inSet.containsAll(coverSet);
+    if (mustClearSet != null && mustClearSet.containsAll(coverSet)) {
+      return true;
+    }
+
+    if (curWrittenSet == null) {
+      return false;
+    }
+
+    return curWrittenSet.containsAll(coverSet);
   }
 
   private void checkManyRead(FlatCall fc, Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr) {
-
     Set<NTuple<Descriptor>> boundReadSet = mapFlatNodeToBoundReadSet.get(fc);
-
     for (Iterator iterator = boundReadSet.iterator(); iterator.hasNext();) {
       NTuple<Descriptor> readHeapPath = (NTuple<Descriptor>) iterator.next();
       Set<WriteAge> writeAgeSet = curr.get(readHeapPath);
@@ -1527,9 +1579,6 @@ public class DefinitelyWrittenCheck {
 
   private void checkWriteAgeSet(Set<WriteAge> writeAgeSet, NTuple<Descriptor> path, FlatNode fn) {
 
-    // System.out.println("# CHECK WRITE AGE of " + path + " from set=" +
-    // writeAgeSet);
-
     if (writeAgeSet != null) {
       for (Iterator iterator = writeAgeSet.iterator(); iterator.hasNext();) {
         WriteAge writeAge = (WriteAge) iterator.next();
@@ -1542,7 +1591,7 @@ public class DefinitelyWrittenCheck {
 
   private void generateErrorMessage(NTuple<Descriptor> path, FlatNode fn) {
 
-    Descriptor lastDesc = path.get(path.size() - 1);
+    Descriptor lastDesc = path.get(getArrayBaseDescriptorIdx(path));
     if (ssjava.isSharedLocation(getLocation(lastDesc))) {
 
       NTuple<Location> locPathTuple = getLocationTuple(path);
@@ -1565,10 +1614,9 @@ public class DefinitelyWrittenCheck {
   }
 
   private void generateGENSetForFlatCall(FlatCall fc, SharedLocMap sharedLocMap,
-      Hashtable<NTuple<Descriptor>, Set<WriteAge>> GENSet) {
+      SharedLocMap mustClearMap, Hashtable<NTuple<Descriptor>, Set<WriteAge>> GENSet) {
 
     Set<NTuple<Descriptor>> boundMayWriteSet = mapFlatNodeToBoundMayWriteSet.get(fc);
-//    System.out.println("boundMayWriteSet=" + boundMayWriteSet);
 
     for (Iterator iterator = boundMayWriteSet.iterator(); iterator.hasNext();) {
       NTuple<Descriptor> heapPath = (NTuple<Descriptor>) iterator.next();
@@ -1582,10 +1630,9 @@ public class DefinitelyWrittenCheck {
 
         Set<NTuple<Descriptor>> sharedWriteHeapPathSet = sharedLocMap.get(locTuple);
 
-        if (isCovered(locTuple, sharedLocMap.get(locTuple))) {
+        if (isCovered(locTuple, sharedLocMap.get(locTuple), mustClearMap.get(locTuple))) {
           // if it is covered, add all of heap paths belong to the same shared
           // loc with write age 0
-
           for (Iterator iterator2 = sharedWriteHeapPathSet.iterator(); iterator2.hasNext();) {
             NTuple<Descriptor> sharedHeapPath = (NTuple<Descriptor>) iterator2.next();
             addWriteAgeToSet(sharedHeapPath, GENSet, new WriteAge(0));
@@ -1617,10 +1664,9 @@ public class DefinitelyWrittenCheck {
 
   private void generateKILLSetForFlatCall(FlatCall fc,
       Hashtable<NTuple<Descriptor>, Set<WriteAge>> curr, SharedLocMap sharedLocMap,
-      Hashtable<NTuple<Descriptor>, Set<WriteAge>> KILLSet) {
+      SharedLocMap mustClearMap, Hashtable<NTuple<Descriptor>, Set<WriteAge>> KILLSet) {
 
     Set<NTuple<Descriptor>> boundMustWriteSet = mapFlatNodeToBoundMustWriteSet.get(fc);
-//    System.out.println("boundMustWriteSet=" + boundMustWriteSet);
 
     for (Iterator iterator = boundMustWriteSet.iterator(); iterator.hasNext();) {
       NTuple<Descriptor> heapPath = (NTuple<Descriptor>) iterator.next();
@@ -1628,14 +1674,20 @@ public class DefinitelyWrittenCheck {
       if (isSharedLocation(heapPath)) {
         NTuple<Location> locTuple = getLocationTuple(heapPath);
 
-        if (isCovered(locTuple, sharedLocMap.get(locTuple))) {
+        if (isCovered(locTuple, sharedLocMap.get(locTuple), mustClearMap.get(locTuple))
+            && curr.containsKey(heapPath)) {
           // if it is shared loc and corresponding shared loc has been covered
           KILLSet.put(heapPath, curr.get(heapPath));
         }
       } else {
-        if (curr.get(heapPath) != null) {
-          KILLSet.put(heapPath, curr.get(heapPath));
+
+        for (Enumeration<NTuple<Descriptor>> e = curr.keys(); e.hasMoreElements();) {
+          NTuple<Descriptor> key = e.nextElement();
+          if (key.startsWith(heapPath)) {
+            KILLSet.put(key, curr.get(key));
+          }
         }
+
       }
 
     }
@@ -1644,7 +1696,7 @@ public class DefinitelyWrittenCheck {
 
   private int getArrayBaseDescriptorIdx(NTuple<Descriptor> heapPath) {
 
-    for (int i = heapPath.size() - 1; i > 1; i--) {
+    for (int i = heapPath.size() - 1; i >= 0; i--) {
       if (!heapPath.get(i).getSymbol().equals(arrayElementFieldName)) {
         return i;
       }
@@ -1656,16 +1708,10 @@ public class DefinitelyWrittenCheck {
 
   private boolean isSharedLocation(NTuple<Descriptor> heapPath) {
 
-    Descriptor d = heapPath.get(heapPath.size() - 1);
-
-    if (d instanceof FieldDescriptor) {
+    Descriptor d = heapPath.get(getArrayBaseDescriptorIdx(heapPath));
 
-      return ssjava
-          .isSharedLocation(getLocation(heapPath.get(getArrayBaseDescriptorIdx(heapPath))));
+    return ssjava.isSharedLocation(getLocation(heapPath.get(getArrayBaseDescriptorIdx(heapPath))));
 
-    } else {
-      return ssjava.isSharedLocation(getLocation(heapPath.get(heapPath.size() - 1)));
-    }
   }
 
   private NTuple<Location> getLocationTuple(NTuple<Descriptor> heapPath) {
@@ -1763,13 +1809,10 @@ public class DefinitelyWrittenCheck {
       // arg idx is starting from 'this' arg
       if (fc.getThis() != null) {
         NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
-        if (thisHeapPath == null) {
-          // method is called without creating new flat node representing 'this'
-          thisHeapPath = new NTuple<Descriptor>();
-          thisHeapPath.add(fc.getThis());
+        if (thisHeapPath != null) {
+          // if 'this' does not have heap path, it is local reference
+          mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
         }
-
-        mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
       }
 
       for (int i = 0; i < fc.numArgs(); i++) {
@@ -1846,94 +1889,142 @@ public class DefinitelyWrittenCheck {
     calleeIntersectBoundSharedSet.clear();
     calleeUnionBoundDeleteSet.clear();
 
-    // if arg is not primitive type, we need to propagate maywritten set to
-    // the caller's location path
+    if (ssjava.isSSJavaUtil(fc.getMethod().getClassDesc())) {
+      // ssjava util case!
+      // have write effects on the first argument
+      TempDescriptor arg = fc.getArg(0);
+      NTuple<Descriptor> argHeapPath = computePath(arg);
 
-    MethodDescriptor mdCallee = fc.getMethod();
-    Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
-    setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
+      // convert heap path to location path
+      NTuple<Location> argLocTuple = new NTuple<Location>();
+      argLocTuple.addAll(deriveLocationTuple(mdCaller, (TempDescriptor) argHeapPath.get(0)));
+      for (int i = 1; i < argHeapPath.size(); i++) {
+        argLocTuple.add(getLocation(argHeapPath.get(i)));
+      }
 
-    // create mapping from arg idx to its heap paths
-    Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
-        new Hashtable<Integer, NTuple<Descriptor>>();
+      calleeIntersectBoundSharedSet.addWrite(argLocTuple, argHeapPath);
 
-    // arg idx is starting from 'this' arg
-    if (fc.getThis() != null) {
-      NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
-      if (thisHeapPath == null) {
-        // method is called without creating new flat node representing 'this'
-        thisHeapPath = new NTuple<Descriptor>();
-        thisHeapPath.add(fc.getThis());
-      }
+    } else if (ssjava.needTobeAnnotated(fc.getMethod())) {
 
-      mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
-    }
+      // if arg is not primitive type, we need to propagate maywritten set to
+      // the caller's location path
 
-    for (int i = 0; i < fc.numArgs(); i++) {
-      TempDescriptor arg = fc.getArg(i);
-      NTuple<Descriptor> argHeapPath = computePath(arg);
-      mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
-    }
+      MethodDescriptor mdCallee = fc.getMethod();
+      Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
+      setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
 
-    // create mapping from arg idx to its location paths
-    Hashtable<Integer, NTuple<Location>> mapArgIdx2CallerAgLocationPath =
-        new Hashtable<Integer, NTuple<Location>>();
+      // create mapping from arg idx to its heap paths
+      Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
+          new Hashtable<Integer, NTuple<Descriptor>>();
 
-    // arg idx is starting from 'this' arg
-    if (fc.getThis() != null) {
-      NTuple<Location> thisLocationPath = deriveLocationTuple(mdCaller, fc.getThis());
-      mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(0), thisLocationPath);
-    }
+      // arg idx is starting from 'this' arg
+      if (fc.getThis() != null) {
+        NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
+        if (thisHeapPath == null) {
+          // method is called without creating new flat node representing 'this'
+          thisHeapPath = new NTuple<Descriptor>();
+          thisHeapPath.add(fc.getThis());
+        }
 
-    for (int i = 0; i < fc.numArgs(); i++) {
-      TempDescriptor arg = fc.getArg(i);
-      NTuple<Location> argLocationPath = deriveLocationTuple(mdCaller, arg);
-      if (argLocationPath != null) {
-        mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(i + 1), argLocationPath);
+        mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
       }
-    }
 
-    for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
-      MethodDescriptor callee = (MethodDescriptor) iterator.next();
-      FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
+      for (int i = 0; i < fc.numArgs(); i++) {
+        TempDescriptor arg = fc.getArg(i);
+        NTuple<Descriptor> argHeapPath = computePath(arg);
+        mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
+      }
 
-      // binding caller's args and callee's params
+      // create mapping from arg idx to its location paths
+      Hashtable<Integer, NTuple<Location>> mapArgIdx2CallerAgLocationPath =
+          new Hashtable<Integer, NTuple<Location>>();
 
-      Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
-          new Hashtable<Integer, TempDescriptor>();
-      int offset = 0;
-      if (calleeFlatMethod.getMethod().isStatic()) {
-        // static method does not have implicit 'this' arg
-        offset = 1;
+      // arg idx is starting from 'this' arg
+      if (fc.getThis() != null) {
+        NTuple<Location> thisLocationPath = deriveLocationTuple(fc.getMethod(), fc.getThis());
+        if (thisLocationPath != null) {
+          mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(0), thisLocationPath);
+        }
       }
-      for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
-        TempDescriptor param = calleeFlatMethod.getParameter(i);
-        mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param);
+
+      for (int i = 0; i < fc.numArgs(); i++) {
+        TempDescriptor arg = fc.getArg(i);
+        NTuple<Location> argLocationPath = deriveLocationTuple(mdCaller, arg);
+        if (argLocationPath != null) {
+          mapArgIdx2CallerAgLocationPath.put(Integer.valueOf(i + 1), argLocationPath);
+        }
       }
 
-      Set<Integer> keySet = mapArgIdx2CallerAgLocationPath.keySet();
-      for (Iterator iterator2 = keySet.iterator(); iterator2.hasNext();) {
-        Integer idx = (Integer) iterator2.next();
-        NTuple<Location> callerArgLocationPath = mapArgIdx2CallerAgLocationPath.get(idx);
-        NTuple<Descriptor> callerArgHeapPath = mapArgIdx2CallerArgHeapPath.get(idx);
+      for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
+        MethodDescriptor callee = (MethodDescriptor) iterator.next();
+        FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
 
-        TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx);
-        NTuple<Location> calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam);
-        SharedLocMap calleeDeleteSet = mapFlatMethodToDeleteSet.get(calleeFlatMethod);
-        SharedLocMap calleeSharedLocMap = mapFlatMethodToSharedLocMap.get(calleeFlatMethod);
+        // binding caller's args and callee's params
 
-        if (calleeDeleteSet != null) {
-          createNewMappingOfDeleteSet(callerArgLocationPath, callerArgHeapPath, calleeLocationPath,
-              calleeDeleteSet);
+        Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
+            new Hashtable<Integer, TempDescriptor>();
+        int offset = 0;
+        if (calleeFlatMethod.getMethod().isStatic()) {
+          // static method does not have implicit 'this' arg
+          offset = 1;
+        }
+        for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
+          TempDescriptor param = calleeFlatMethod.getParameter(i);
+          mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param);
         }
 
-        if (calleeSharedLocMap != null) {
-          createNewMappingOfSharedSet(callerArgLocationPath, callerArgHeapPath, calleeLocationPath,
-              calleeSharedLocMap);
+        Set<Integer> keySet = mapArgIdx2CallerAgLocationPath.keySet();
+        for (Iterator iterator2 = keySet.iterator(); iterator2.hasNext();) {
+          Integer idx = (Integer) iterator2.next();
+          NTuple<Location> callerArgLocationPath = mapArgIdx2CallerAgLocationPath.get(idx);
+          NTuple<Descriptor> callerArgHeapPath = mapArgIdx2CallerArgHeapPath.get(idx);
+
+          TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx);
+          NTuple<Location> calleeLocationPath = deriveLocationTuple(mdCallee, calleeParam);
+          SharedLocMap calleeDeleteSet = mapFlatMethodToDeleteSet.get(calleeFlatMethod);
+          SharedLocMap calleeSharedLocMap = mapFlatMethodToSharedLocMap.get(calleeFlatMethod);
+          SharedLocMap calleeMustClearMap = mapFlatMethodToMustClearMap.get(calleeFlatMethod);
+
+          if (calleeDeleteSet != null) {
+            createNewMappingOfDeleteSet(callerArgLocationPath, callerArgHeapPath,
+                calleeLocationPath, calleeDeleteSet);
+          }
+
+          if (calleeSharedLocMap != null) {
+            createNewMappingOfSharedSet(callerArgLocationPath, callerArgHeapPath,
+                calleeLocationPath, calleeSharedLocMap);
+          }
+
+          if (calleeMustClearMap != null) {
+            createNewMappingOfMustClearMap(callerArgLocationPath, callerArgHeapPath,
+                calleeLocationPath, calleeMustClearMap);
+          }
+
         }
 
       }
+    }
+
+  }
 
+  private void createNewMappingOfMustClearMap(NTuple<Location> callerArgLocationPath,
+      NTuple<Descriptor> callerArgHeapPath, NTuple<Location> calleeLocationPath,
+      SharedLocMap calleeMustClearMap) {
+
+    SharedLocMap calleeParamSharedSet =
+        calleeMustClearMap.getHeapPathStartedWith(calleeLocationPath);
+
+    Set<NTuple<Location>> keySet = calleeParamSharedSet.keySet();
+    for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
+      NTuple<Location> calleeLocTupleKey = (NTuple<Location>) iterator.next();
+      Set<NTuple<Descriptor>> heapPathSet = calleeParamSharedSet.get(calleeLocTupleKey);
+      Set<NTuple<Descriptor>> boundHeapPathSet = new HashSet<NTuple<Descriptor>>();
+      for (Iterator iterator2 = heapPathSet.iterator(); iterator2.hasNext();) {
+        NTuple<Descriptor> calleeHeapPath = (NTuple<Descriptor>) iterator2.next();
+        boundHeapPathSet.add(bindHeapPath(callerArgHeapPath, calleeHeapPath));
+      }
+      calleeIntersectBoundMustClearSet.intersect(
+          bindLocationPath(callerArgLocationPath, calleeLocTupleKey), boundHeapPathSet);
     }
 
   }
@@ -2046,15 +2137,19 @@ public class DefinitelyWrittenCheck {
 
     // perform topological sort over the set of methods accessed by the main
     // event loop
-    Set<MethodDescriptor> methodDescriptorsToAnalyze = new HashSet<MethodDescriptor>();
-    methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet());
-    sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze);
+    // Set<MethodDescriptor> methodDescriptorsToAnalyze = new
+    // HashSet<MethodDescriptor>();
+    // methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet());
+    // sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze);
+
+    liveInTempSetToEventLoop =
+        liveness.getLiveInTemps(state.getMethodFlat(methodContainingSSJavaLoop),
+            ssjava.getSSJavaLoopEntrance());
   }
 
   private void methodReadWriteSetAnalysis() {
     // perform method READ/OVERWRITE analysis
-    LinkedList<MethodDescriptor> descriptorListToAnalyze =
-        (LinkedList<MethodDescriptor>) sortedDescriptors.clone();
+    LinkedList<MethodDescriptor> descriptorListToAnalyze = ssjava.getSortedDescriptors();
 
     // current descriptors to visit in fixed-point interprocedural analysis,
     // prioritized by
@@ -2096,7 +2191,7 @@ public class DefinitelyWrittenCheck {
         // results for callee changed, so enqueue dependents caller for
         // further
         // analysis
-        Iterator<MethodDescriptor> depsItr = getDependents(md).iterator();
+        Iterator<MethodDescriptor> depsItr = ssjava.getDependents(md).iterator();
         while (depsItr.hasNext()) {
           MethodDescriptor methodNext = depsItr.next();
           if (!methodDescriptorsToVisitStack.contains(methodNext)
@@ -2143,6 +2238,13 @@ public class DefinitelyWrittenCheck {
     mapFlatMethodToMustWriteSet.put(flatMethodContainingSSJavaLoop, mustWriteSet);
     mapFlatMethodToMayWriteSet.put(flatMethodContainingSSJavaLoop, mayWriteSet);
 
+    for (Iterator iterator = liveInTempSetToEventLoop.iterator(); iterator.hasNext();) {
+      TempDescriptor liveIn = (TempDescriptor) iterator.next();
+      NTuple<Descriptor> heapPath = new NTuple<Descriptor>();
+      heapPath.add(liveIn);
+      mapHeapPath.put(liveIn, heapPath);
+    }
+
     methodReadWriteSet_analyzeBody(ssjava.getSSJavaLoopEntrance(), readSet, mustWriteSet,
         mayWriteSet, true);
 
@@ -2224,16 +2326,23 @@ public class DefinitelyWrittenCheck {
 
         NTuple<Descriptor> rhsHeapPath = mapHeapPath.get(rhs);
 
-        if (lhs.getType().isPrimitive()) {
-          NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
-          lhsHeapPath.add(lhs);
-          mapHeapPath.put(lhs, lhsHeapPath);
-        } else if (rhsHeapPath != null) {
+        // if (lhs.getType().isPrimitive()) {
+        // NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
+        // lhsHeapPath.add(lhs);
+        // mapHeapPath.put(lhs, lhsHeapPath);
+        // } else
+
+        if (rhsHeapPath != null && (!lhs.getType().isPrimitive())) {
           mapHeapPath.put(lhs, mapHeapPath.get(rhs));
         } else {
-          NTuple<Descriptor> heapPath = new NTuple<Descriptor>();
-          heapPath.add(rhs);
-          mapHeapPath.put(lhs, heapPath);
+          break;
+          // if (isEventLoopBody) {
+          // NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
+          // lhsHeapPath.add(rhs);
+          // mapHeapPath.put(lhs, lhsHeapPath);
+          // } else {
+          // break;
+          // }
         }
 
         // shared loc extension
@@ -2295,7 +2404,10 @@ public class DefinitelyWrittenCheck {
         // callee's parameters. so just ignore it
 
         NTuple<Descriptor> readingHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
-        readingHeapPath.add(fld);
+        if (fn.kind() == FKind.FlatFieldNode) {
+          readingHeapPath.add(fld);
+        }
+
         mapHeapPath.put(lhs, readingHeapPath);
 
         // read (x.f)
@@ -2337,12 +2449,16 @@ public class DefinitelyWrittenCheck {
         // if lhs heap path is null, it means that it is not reachable from
         // callee's parameters. so just ignore it
         NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
-        fldHeapPath.add(fld);
-        mapHeapPath.put(fld, fldHeapPath);
+        if (fn.kind() != FKind.FlatSetElementNode) {
+          fldHeapPath.add(fld);
+        }
+        // mapHeapPath.put(fld, fldHeapPath);
 
         // write(x.f)
         // need to add hp(y) to WT
-        currMustWriteSet.add(fldHeapPath);
+        if (fn.kind() != FKind.FlatSetElementNode) {
+          currMustWriteSet.add(fldHeapPath);
+        }
         mayWriteSet.add(fldHeapPath);
 
       }
@@ -2474,78 +2590,6 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  // Borrowed it from disjoint analysis
-  private LinkedList<MethodDescriptor> topologicalSort(Set<MethodDescriptor> toSort) {
-
-    Set<MethodDescriptor> discovered = new HashSet<MethodDescriptor>();
-
-    LinkedList<MethodDescriptor> sorted = new LinkedList<MethodDescriptor>();
-
-    Iterator<MethodDescriptor> itr = toSort.iterator();
-    while (itr.hasNext()) {
-      MethodDescriptor d = itr.next();
-
-      if (!discovered.contains(d)) {
-        dfsVisit(d, toSort, sorted, discovered);
-      }
-    }
-
-    return sorted;
-  }
-
-  // While we're doing DFS on call graph, remember
-  // dependencies for efficient queuing of methods
-  // during interprocedural analysis:
-  //
-  // a dependent of a method decriptor d for this analysis is:
-  // 1) a method or task that invokes d
-  // 2) in the descriptorsToAnalyze set
-  private void dfsVisit(MethodDescriptor md, Set<MethodDescriptor> toSort,
-      LinkedList<MethodDescriptor> sorted, Set<MethodDescriptor> discovered) {
-
-    discovered.add(md);
-
-    Iterator itr = callGraph.getCallerSet(md).iterator();
-    while (itr.hasNext()) {
-      MethodDescriptor dCaller = (MethodDescriptor) itr.next();
-      // only consider callers in the original set to analyze
-      if (!toSort.contains(dCaller)) {
-        continue;
-      }
-      if (!discovered.contains(dCaller)) {
-        addDependent(md, // callee
-            dCaller // caller
-        );
-
-        dfsVisit(dCaller, toSort, sorted, discovered);
-      }
-    }
-
-    // for leaf-nodes last now!
-    sorted.addLast(md);
-  }
-
-  // a dependent of a method decriptor d for this analysis is:
-  // 1) a method or task that invokes d
-  // 2) in the descriptorsToAnalyze set
-  private void addDependent(MethodDescriptor callee, MethodDescriptor caller) {
-    Set<MethodDescriptor> deps = mapDescriptorToSetDependents.get(callee);
-    if (deps == null) {
-      deps = new HashSet<MethodDescriptor>();
-    }
-    deps.add(caller);
-    mapDescriptorToSetDependents.put(callee, deps);
-  }
-
-  private Set<MethodDescriptor> getDependents(MethodDescriptor callee) {
-    Set<MethodDescriptor> deps = mapDescriptorToSetDependents.get(callee);
-    if (deps == null) {
-      deps = new HashSet<MethodDescriptor>();
-      mapDescriptorToSetDependents.put(callee, deps);
-    }
-    return deps;
-  }
-
   private NTuple<Descriptor> computePath(Descriptor td) {
     // generate proper path fot input td
     // if td is local variable, it just generate one element tuple path
@@ -2577,7 +2621,6 @@ public class DefinitelyWrittenCheck {
   }
 
   private NTuple<Location> deriveLocationTuple(MethodDescriptor md, TempDescriptor td) {
-
     assert td.getType() != null;
 
     if (mapDescriptorToLocationPath.containsKey(td)) {
@@ -2588,10 +2631,8 @@ public class DefinitelyWrittenCheck {
     } else {
       if (td.getSymbol().startsWith("this")) {
         NTuple<Location> thisPath = deriveThisLocationTuple(md);
-
         NTuple<Location> rtrPath = new NTuple<Location>();
         rtrPath.addAll(thisPath);
-
         return rtrPath;
       } else {