Finally, all benchmarks pass the definitely written analysis
[IRC.git] / Robust / src / Analysis / SSJava / DefinitelyWrittenCheck.java
index a8f1be47bdea15105777666e3ecd39a739bb1860..f187a38d027af700918b77e204cdce2f6a511e14 100644 (file)
@@ -1,8 +1,5 @@
 package Analysis.SSJava;
 
-import java.io.BufferedWriter;
-import java.io.FileWriter;
-import java.io.IOException;
 import java.util.Enumeration;
 import java.util.HashSet;
 import java.util.Hashtable;
@@ -11,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;
@@ -33,7 +31,6 @@ import IR.Flat.FlatSetElementNode;
 import IR.Flat.FlatSetFieldNode;
 import IR.Flat.TempDescriptor;
 import IR.Tree.Modifiers;
-import Util.Pair;
 
 public class DefinitelyWrittenCheck {
 
@@ -41,6 +38,8 @@ public class DefinitelyWrittenCheck {
   State state;
   CallGraph callGraph;
 
+  Liveness liveness;
+
   int debugcount = 0;
 
   // maps a descriptor to its known dependents: namely
@@ -120,8 +119,6 @@ public class DefinitelyWrittenCheck {
   private Hashtable<FlatNode, SharedLocMap> mapFlatNodeToSharedLocMapping;
   private Hashtable<FlatNode, SharedLocMap> mapFlatNodeToDeleteSet;
 
-  private Hashtable<Location, Set<Descriptor>> mapSharedLocationToCoverSet;
-
   private LinkedList<MethodDescriptor> sortedDescriptors;
 
   private LoopFinder ssjavaLoop;
@@ -133,6 +130,8 @@ public class DefinitelyWrittenCheck {
   private SharedLocMap calleeUnionBoundDeleteSet;
   private SharedLocMap calleeIntersectBoundSharedSet;
 
+  Set<TempDescriptor> liveInTempSetToEventLoop;
+
   private Hashtable<Descriptor, Location> mapDescToLocation;
 
   private TempDescriptor LOCAL;
@@ -166,7 +165,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();
@@ -175,6 +173,8 @@ 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>();
   }
 
   public void definitelyWrittenCheck() {
@@ -347,31 +347,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;
             }
 
           }
@@ -394,14 +391,13 @@ 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);
+        break;
+      }
 
-        NTuple<Location> locTuple = mapDescriptorToLocationPath.get(lhs);
-        fieldLoc = locTuple.get(locTuple.size() - 1);
+      if (!isEventLoopBody && fieldLoc.getDescriptor().equals(md)) {
+        // if the field belongs to the local lattice, no reason to calculate
+        // shared location
+        break;
       }
 
       NTuple<Location> fieldLocTuple = new NTuple<Location>();
@@ -412,12 +408,16 @@ public class DefinitelyWrittenCheck {
           fieldLocTuple.add(topLocation);
         } else {
           fieldLocTuple.addAll(deriveGlobalLocationTuple(md));
-          fieldLocTuple.add((Location) fld.getType().getExtension());
+          if (fn.kind() == FKind.FlatSetFieldNode) {
+            fieldLocTuple.add((Location) fld.getType().getExtension());
+          }
         }
 
       } else {
         fieldLocTuple.addAll(deriveLocationTuple(md, lhs));
-        fieldLocTuple.add((Location) fld.getType().getExtension());
+        if (fn.kind() == FKind.FlatSetFieldNode) {
+          fieldLocTuple.add((Location) fld.getType().getExtension());
+        }
       }
 
       // shared loc extension
@@ -432,11 +432,14 @@ 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);
         } else {
@@ -444,14 +447,6 @@ public class DefinitelyWrittenCheck {
           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);
       }
 
     }
@@ -460,19 +455,11 @@ 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);
-
-      }
-      // System.out.println("#FLATCALL=" + fc);
-      // System.out.println("KILLSET=" + killSet);
-      // System.out.println("GENSet=" + genSet);
-      // System.out.println("bound DELETE Set=" + calleeUnionBoundDeleteSet);
+      // computing gen/kill set
+      generateKILLSetForFlatCall(curr, killSet);
+      generateGENSetForFlatCall(curr, genSet);
 
     }
       break;
@@ -482,14 +469,12 @@ public class DefinitelyWrittenCheck {
       mergeSharedLocMap(sharedLocMap, curr);
       mergeDeleteSet(deleteSet, currDeleteSet);
 
-      // System.out.println("#FLATEXIT sharedLocMap=" + sharedLocMap);
     }
       break;
 
     }
 
     computeNewMapping(curr, killSet, genSet);
-    // System.out.println("#######" + curr);
 
   }
 
@@ -629,8 +614,9 @@ public class DefinitelyWrittenCheck {
 
   private void computeSharedCoverSet_analyzeMethod(FlatMethod fm, boolean onlyVisitSSJavaLoop) {
 
-    System.out.println("computeSharedCoverSet_analyzeMethod=" + fm);
+    // System.out.println("computeSharedCoverSet_analyzeMethod=" + fm);
     MethodDescriptor md = fm.getMethod();
+
     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
 
     Set<FlatNode> visited = new HashSet<FlatNode>();
@@ -646,7 +632,7 @@ public class DefinitelyWrittenCheck {
       flatNodesToVisit.remove(fn);
       visited.add(fn);
 
-      computeSharedCoverSet_nodeActions(md, fn);
+      computeSharedCoverSet_nodeActions(md, fn, onlyVisitSSJavaLoop);
 
       for (int i = 0; i < fn.numNext(); i++) {
         FlatNode nn = fn.getNext(i);
@@ -663,7 +649,8 @@ public class DefinitelyWrittenCheck {
 
   }
 
-  private void computeSharedCoverSet_nodeActions(MethodDescriptor md, FlatNode fn) {
+  private void computeSharedCoverSet_nodeActions(MethodDescriptor md, FlatNode fn,
+      boolean isEventLoopBody) {
     TempDescriptor lhs;
     TempDescriptor rhs;
     FieldDescriptor fld;
@@ -684,10 +671,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);
-          }
         }
       }
 
@@ -705,53 +688,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;
           }
+
         }
 
       }
@@ -776,51 +765,58 @@ public class DefinitelyWrittenCheck {
         fld = getArrayField(td);
       }
 
-      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));
       }
 
-      Location fieldLocation;
+      mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
+
+      NTuple<Location> fieldLocTuple = new NTuple<Location>();
+      fieldLocTuple.addAll(lhsLocTuple);
+
       if (fn.kind() == FKind.FlatSetFieldNode) {
-        fieldLocation = (Location) fld.getType().getExtension();
-      } else {
-        NTuple<Location> locTuple = mapDescriptorToLocationPath.get(lhs);
-        fieldLocation = locTuple.get(locTuple.size() - 1);
+        fieldLocTuple.add((Location) fld.getType().getExtension());
       }
 
-      NTuple<Location> lTuple = deriveLocationTuple(md, lhs);
-      if (lTuple != null) {
-        NTuple<Location> lhsLocTuple = new NTuple<Location>();
-        lhsLocTuple.addAll(lTuple);
-        mapDescriptorToLocationPath.put(lhs, lhsLocTuple);
-      }
+      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));
 
-      if (ssjava.isSharedLocation(fieldLocation)) {
-        addSharedLocDescriptor(fieldLocation, fld);
+        Location fieldLocation;
+        if (fn.kind() == FKind.FlatSetFieldNode) {
+          fieldLocation = getLocation(fld);
+        } else {
+          fieldLocation = getLocation(lhsHeapPath.get(getArrayBaseDescriptorIdx(lhsHeapPath)));
+        }
 
-        NTuple<Descriptor> fieldHeapPath = new NTuple<Descriptor>();
-        fieldHeapPath.addAll(computePath(lhs));
-        fieldHeapPath.add(fld);
+        // 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);
+
+        }
       }
 
     }
@@ -875,9 +871,7 @@ public class DefinitelyWrittenCheck {
 
       FlatCall fc = (FlatCall) fn;
 
-      if (ssjava.needTobeAnnotated(fc.getMethod())) {
-        bindLocationPathCallerArgWithCalleeParam(md, fc);
-      }
+      bindLocationPathCallerArgWithCalleeParam(md, fc);
 
     }
       break;
@@ -926,7 +920,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
@@ -943,52 +937,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;
@@ -996,26 +984,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);
+          }
         }
 
       }
@@ -1046,7 +1048,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
@@ -1058,6 +1060,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);
 
@@ -1066,24 +1072,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>>();
+
+        Set<NTuple<Descriptor>> boundSet =
+            convertToCallerMayWriteSet(calleeParamHeapPath, calleeMayWriteSet, callerMapping,
+                mapParamHeapPathToCallerArgHeapPath);
 
-        writeSet.addAll(boundWriteSet);
+        boundMayWriteSet.addAll(boundSet);
 
         NTuple<Location> newKey = new NTuple<Location>();
         newKey.addAll(callerArgLocPath);
@@ -1093,16 +1100,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>>();
 
@@ -1110,12 +1118,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));
       }
 
@@ -1126,18 +1137,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) {
@@ -1274,7 +1273,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) {
@@ -1294,10 +1292,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)) {
 
@@ -1316,15 +1315,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);
             }
 
           }
@@ -1384,39 +1380,49 @@ 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));
+            if (fn.kind() == FKind.FlatSetFieldNode) {
+              fieldLocTuple.add(fieldLoc);
+            }
 
-          NTuple<Location> fieldLocTuple = new NTuple<Location>();
-          fieldLocTuple.addAll(mapDescriptorToLocationPath.get(lhs));
-          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;
 
@@ -1424,21 +1430,18 @@ public class DefinitelyWrittenCheck {
         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);
-
-        checkManyRead(fc, curr);
       }
         break;
 
       }
 
       computeNewMapping(curr, readWriteKillSet, readWriteGenSet);
-      // System.out.println("#######" + curr);
+      if (fn instanceof FlatCall) {
+        checkManyRead((FlatCall) fn, curr);
+      }
 
     }
 
@@ -1512,9 +1515,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();
@@ -1527,7 +1527,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);
@@ -1611,14 +1611,19 @@ public class DefinitelyWrittenCheck {
       if (isSharedLocation(heapPath)) {
         NTuple<Location> locTuple = getLocationTuple(heapPath);
 
-        if (isCovered(locTuple, sharedLocMap.get(locTuple))) {
+        if (isCovered(locTuple, sharedLocMap.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));
+          }
         }
+
       }
 
     }
@@ -1627,7 +1632,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;
       }
@@ -1639,16 +1644,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) {
@@ -1746,13 +1745,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++) {
@@ -1829,94 +1825,114 @@ 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(mdCaller, 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);
+
+          if (calleeDeleteSet != null) {
+            createNewMappingOfDeleteSet(callerArgLocationPath, callerArgHeapPath,
+                calleeLocationPath, calleeDeleteSet);
+          }
+
+          if (calleeSharedLocMap != null) {
+            createNewMappingOfSharedSet(callerArgLocationPath, callerArgHeapPath,
+                calleeLocationPath, calleeSharedLocMap);
+          }
+
         }
 
       }
-
     }
 
   }
@@ -2032,6 +2048,10 @@ public class DefinitelyWrittenCheck {
     Set<MethodDescriptor> methodDescriptorsToAnalyze = new HashSet<MethodDescriptor>();
     methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet());
     sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze);
+
+    liveInTempSetToEventLoop =
+        liveness.getLiveInTemps(state.getMethodFlat(methodContainingSSJavaLoop),
+            ssjava.getSSJavaLoopEntrance());
   }
 
   private void methodReadWriteSetAnalysis() {
@@ -2126,6 +2146,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);
 
@@ -2207,16 +2234,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
@@ -2278,7 +2312,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)
@@ -2320,12 +2357,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);
 
       }
@@ -2533,11 +2574,13 @@ public class DefinitelyWrittenCheck {
     // generate proper path fot input td
     // if td is local variable, it just generate one element tuple path
     if (mapHeapPath.containsKey(td)) {
-      return mapHeapPath.get(td);
+      NTuple<Descriptor> rtrHeapPath = new NTuple<Descriptor>();
+      rtrHeapPath.addAll(mapHeapPath.get(td));
+      return rtrHeapPath;
     } else {
-      NTuple<Descriptor> path = new NTuple<Descriptor>();
-      path.add(td);
-      return path;
+      NTuple<Descriptor> rtrHeapPath = new NTuple<Descriptor>();
+      rtrHeapPath.add(td);
+      return rtrHeapPath;
     }
   }
 
@@ -2562,19 +2605,24 @@ public class DefinitelyWrittenCheck {
     assert td.getType() != null;
 
     if (mapDescriptorToLocationPath.containsKey(td)) {
-      return mapDescriptorToLocationPath.get(td);
+      NTuple<Location> locPath = mapDescriptorToLocationPath.get(td);
+      NTuple<Location> rtrPath = new NTuple<Location>();
+      rtrPath.addAll(locPath);
+      return rtrPath;
     } else {
       if (td.getSymbol().startsWith("this")) {
-        return deriveThisLocationTuple(md);
+        NTuple<Location> thisPath = deriveThisLocationTuple(md);
+        NTuple<Location> rtrPath = new NTuple<Location>();
+        rtrPath.addAll(thisPath);
+        return rtrPath;
       } else {
 
         if (td.getType().getExtension() != null) {
-          System.out.println("td.getType().getExtension() =" + td.getType().getExtension());
           SSJavaType ssJavaType = (SSJavaType) td.getType().getExtension();
           if (ssJavaType.getCompLoc() != null) {
-            NTuple<Location> locTuple = new NTuple<Location>();
-            locTuple.addAll(ssJavaType.getCompLoc().getTuple());
-            return locTuple;
+            NTuple<Location> rtrPath = new NTuple<Location>();
+            rtrPath.addAll(ssJavaType.getCompLoc().getTuple());
+            return rtrPath;
           }
         }