Robust/src/Analysis/SSJava/DefinitelyWrittenCheck.java

   1 package Analysis.SSJava;
   2
   3 import java.util.HashSet;
   4 import java.util.Hashtable;
   5 import java.util.Iterator;
   6 import java.util.LinkedList;
   7 import java.util.Set;
   8 import java.util.Stack;
   9
  10 import Analysis.CallGraph.CallGraph;
  11 import Analysis.Loops.LoopFinder;
  12 import IR.Descriptor;
  13 import IR.FieldDescriptor;
  14 import IR.MethodDescriptor;
  15 import IR.Operation;
  16 import IR.State;
  17 import IR.TypeDescriptor;
  18 import IR.Flat.FKind;
  19 import IR.Flat.FlatCall;
  20 import IR.Flat.FlatElementNode;
  21 import IR.Flat.FlatFieldNode;
  22 import IR.Flat.FlatLiteralNode;
  23 import IR.Flat.FlatMethod;
  24 import IR.Flat.FlatNode;
  25 import IR.Flat.FlatOpNode;
  26 import IR.Flat.FlatSetElementNode;
  27 import IR.Flat.FlatSetFieldNode;
  28 import IR.Flat.TempDescriptor;
  29 import IR.Tree.Modifiers;
  30 import Util.Pair;
  31
  32 public class DefinitelyWrittenCheck {
  33
  34   SSJavaAnalysis ssjava;
  35   State state;
  36   CallGraph callGraph;
  37
  38   int debugcount = 0;
  39
  40   // maps a descriptor to its known dependents: namely
  41   // methods or tasks that call the descriptor's method
  42   // AND are part of this analysis (reachable from main)
  43   private Hashtable<Descriptor, Set<MethodDescriptor>> mapDescriptorToSetDependents;
  44
  45   // maps a flat node to its WrittenSet: this keeps all heap path overwritten
  46   // previously.
  47   private Hashtable<FlatNode, Set<NTuple<Descriptor>>> mapFlatNodeToWrittenSet;
  48
  49   // maps a temp descriptor to its heap path
  50   // each temp descriptor has a unique heap path since we do not allow any
  51   // alias.
  52   private Hashtable<Descriptor, NTuple<Descriptor>> mapHeapPath;
  53
  54   // maps a flat method to the READ that is the set of heap path that is
  55   // expected to be written before method invocation
  56   private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToRead;
  57
  58   // maps a flat method to the OVERWRITE that is the set of heap path that is
  59   // overwritten on every possible path during method invocation
  60   private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToOverWrite;
  61
  62   // maps a flat method to the WRITE that is the set of heap path that is
  63   // written to
  64   private Hashtable<FlatMethod, Set<NTuple<Descriptor>>> mapFlatMethodToWrite;
  65
  66   // points to method containing SSJAVA Loop
  67   private MethodDescriptor methodContainingSSJavaLoop;
  68
  69   // maps a flatnode to definitely written analysis mapping M
  70   private Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>>> definitelyWrittenResults;
  71
  72   // maps a method descriptor to its current summary during the analysis
  73   // then analysis reaches fixed-point, this mapping will have the final summary
  74   // for each method descriptor
  75   private Hashtable<MethodDescriptor, ClearingSummary> mapMethodDescriptorToCompleteClearingSummary;
  76
  77   // maps a method descriptor to the merged incoming caller's current
  78   // overwritten status
  79   private Hashtable<MethodDescriptor, ClearingSummary> mapMethodDescriptorToInitialClearingSummary;
  80
  81   // maps a flat node to current partial results
  82   private Hashtable<FlatNode, ClearingSummary> mapFlatNodeToClearingSummary;
  83
  84   // maps shared location to the set of descriptors which belong to the shared
  85   // location
  86   private Hashtable<Location, Set<Descriptor>> mapSharedLocation2DescriptorSet;
  87
  88   // keep current descriptors to visit in fixed-point interprocedural analysis,
  89   private Stack<MethodDescriptor> methodDescriptorsToVisitStack;
  90
  91   // when analyzing flatcall, need to re-schedule set of callee
  92   private Set<MethodDescriptor> calleesToEnqueue;
  93
  94   public static final String arrayElementFieldName = "___element_";
  95   static protected Hashtable<TypeDescriptor, FieldDescriptor> mapTypeToArrayField;
  96
  97   private Set<ClearingSummary> possibleCalleeCompleteSummarySetToCaller;
  98
  99   private LinkedList<MethodDescriptor> sortedDescriptors;
 100
 101   private FlatNode ssjavaLoopEntrance;
 102   private LoopFinder ssjavaLoop;
 103   private Set<FlatNode> loopIncElements;
 104
 105   private Set<NTuple<Descriptor>> calleeUnionBoundReadSet;
 106   private Set<NTuple<Descriptor>> calleeIntersectBoundOverWriteSet;
 107   private Set<NTuple<Descriptor>> calleeBoundWriteSet;
 108
 109   private TempDescriptor LOCAL;
 110
 111   public DefinitelyWrittenCheck(SSJavaAnalysis ssjava, State state) {
 112     this.state = state;
 113     this.ssjava = ssjava;
 114     this.callGraph = ssjava.getCallGraph();
 115     this.mapFlatNodeToWrittenSet = new Hashtable<FlatNode, Set<NTuple<Descriptor>>>();
 116     this.mapDescriptorToSetDependents = new Hashtable<Descriptor, Set<MethodDescriptor>>();
 117     this.mapHeapPath = new Hashtable<Descriptor, NTuple<Descriptor>>();
 118     this.mapFlatMethodToRead = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
 119     this.mapFlatMethodToOverWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
 120     this.mapFlatMethodToWrite = new Hashtable<FlatMethod, Set<NTuple<Descriptor>>>();
 121     this.definitelyWrittenResults =
 122         new Hashtable<FlatNode, Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>>>();
 123     this.calleeUnionBoundReadSet = new HashSet<NTuple<Descriptor>>();
 124     this.calleeIntersectBoundOverWriteSet = new HashSet<NTuple<Descriptor>>();
 125     this.calleeBoundWriteSet = new HashSet<NTuple<Descriptor>>();
 126
 127     this.mapMethodDescriptorToCompleteClearingSummary =
 128         new Hashtable<MethodDescriptor, ClearingSummary>();
 129     this.mapMethodDescriptorToInitialClearingSummary =
 130         new Hashtable<MethodDescriptor, ClearingSummary>();
 131     this.mapSharedLocation2DescriptorSet = new Hashtable<Location, Set<Descriptor>>();
 132     this.methodDescriptorsToVisitStack = new Stack<MethodDescriptor>();
 133     this.calleesToEnqueue = new HashSet<MethodDescriptor>();
 134     this.possibleCalleeCompleteSummarySetToCaller = new HashSet<ClearingSummary>();
 135     this.mapTypeToArrayField = new Hashtable<TypeDescriptor, FieldDescriptor>();
 136     this.LOCAL = new TempDescriptor("LOCAL");
 137   }
 138
 139   public void definitelyWrittenCheck() {
 140     if (!ssjava.getAnnotationRequireSet().isEmpty()) {
 141       methodReadOverWriteAnalysis();
 142       writtenAnalyis();
 143       // sharedLocationAnalysis();
 144       // checkSharedLocationResult();
 145     }
 146   }
 147
 148   private void checkSharedLocationResult() {
 149
 150     // mapping of method containing ssjava loop has the final result of
 151     // shared location analysis
 152     ClearingSummary result =
 153         mapMethodDescriptorToCompleteClearingSummary.get(sortedDescriptors.peekFirst());
 154
 155     Set<NTuple<Descriptor>> hpKeySet = result.keySet();
 156     for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
 157       NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
 158       SharedStatus state = result.get(hpKey);
 159       Set<Location> locKeySet = state.getLocationSet();
 160       for (Iterator iterator2 = locKeySet.iterator(); iterator2.hasNext();) {
 161         Location locKey = (Location) iterator2.next();
 162         if (!state.getFlag(locKey)) {
 163           throw new Error(
 164               "Some concrete locations of the shared abstract location are not cleared at the same time.");
 165         }
 166       }
 167     }
 168
 169   }
 170
 171   private void sharedLocationAnalysis() {
 172     // verify that all concrete locations of shared location are cleared out at
 173     // the same time once per the out-most loop
 174
 175     computeReadSharedDescriptorSet();
 176
 177     methodDescriptorsToVisitStack.clear();
 178
 179     methodDescriptorsToVisitStack.add(sortedDescriptors.peekFirst());
 180
 181     // analyze scheduled methods until there are no more to visit
 182     while (!methodDescriptorsToVisitStack.isEmpty()) {
 183       MethodDescriptor md = methodDescriptorsToVisitStack.pop();
 184
 185       ClearingSummary completeSummary =
 186           sharedLocation_analyzeMethod(md, (md.equals(methodContainingSSJavaLoop)));
 187
 188       ClearingSummary prevCompleteSummary = mapMethodDescriptorToCompleteClearingSummary.get(md);
 189
 190       if (!completeSummary.equals(prevCompleteSummary)) {
 191
 192         mapMethodDescriptorToCompleteClearingSummary.put(md, completeSummary);
 193
 194         // results for callee changed, so enqueue dependents caller for
 195         // further analysis
 196         Iterator<MethodDescriptor> depsItr = getDependents(md).iterator();
 197         while (depsItr.hasNext()) {
 198           MethodDescriptor methodNext = depsItr.next();
 199           if (!methodDescriptorsToVisitStack.contains(methodNext)) {
 200             methodDescriptorsToVisitStack.add(methodNext);
 201           }
 202         }
 203
 204         // if there is set of callee to be analyzed,
 205         // add this set into the top of stack
 206         Iterator<MethodDescriptor> calleeIter = calleesToEnqueue.iterator();
 207         while (calleeIter.hasNext()) {
 208           MethodDescriptor mdNext = calleeIter.next();
 209           if (!methodDescriptorsToVisitStack.contains(mdNext)) {
 210             methodDescriptorsToVisitStack.add(mdNext);
 211           }
 212         }
 213         calleesToEnqueue.clear();
 214
 215       }
 216
 217     }
 218
 219   }
 220
 221   private ClearingSummary sharedLocation_analyzeMethod(MethodDescriptor md,
 222       boolean onlyVisitSSJavaLoop) {
 223
 224     if (state.SSJAVADEBUG) {
 225       System.out.println("Definitely written for shared locations Analyzing: " + md + " "
 226           + onlyVisitSSJavaLoop);
 227     }
 228
 229     FlatMethod fm = state.getMethodFlat(md);
 230
 231     // intraprocedural analysis
 232     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
 233
 234     // start a new mapping of partial results for each flat node
 235     mapFlatNodeToClearingSummary = new Hashtable<FlatNode, ClearingSummary>();
 236
 237     if (onlyVisitSSJavaLoop) {
 238       flatNodesToVisit.add(ssjavaLoopEntrance);
 239     } else {
 240       flatNodesToVisit.add(fm);
 241     }
 242
 243     Set<FlatNode> returnNodeSet = new HashSet<FlatNode>();
 244
 245     while (!flatNodesToVisit.isEmpty()) {
 246       FlatNode fn = flatNodesToVisit.iterator().next();
 247       flatNodesToVisit.remove(fn);
 248
 249       ClearingSummary curr = new ClearingSummary();
 250
 251       Set<ClearingSummary> prevSet = new HashSet<ClearingSummary>();
 252       for (int i = 0; i < fn.numPrev(); i++) {
 253         FlatNode prevFn = fn.getPrev(i);
 254         ClearingSummary in = mapFlatNodeToClearingSummary.get(prevFn);
 255         if (in != null) {
 256           prevSet.add(in);
 257         }
 258       }
 259       mergeSharedLocationAnaylsis(curr, prevSet);
 260
 261       sharedLocation_nodeActions(md, fn, curr, returnNodeSet, onlyVisitSSJavaLoop);
 262       ClearingSummary clearingPrev = mapFlatNodeToClearingSummary.get(fn);
 263
 264       if (!curr.equals(clearingPrev)) {
 265         mapFlatNodeToClearingSummary.put(fn, curr);
 266
 267         for (int i = 0; i < fn.numNext(); i++) {
 268           FlatNode nn = fn.getNext(i);
 269
 270           if (!onlyVisitSSJavaLoop || (onlyVisitSSJavaLoop && loopIncElements.contains(nn))) {
 271             flatNodesToVisit.add(nn);
 272           }
 273
 274         }
 275       }
 276
 277     }
 278
 279     ClearingSummary completeSummary = new ClearingSummary();
 280     Set<ClearingSummary> summarySet = new HashSet<ClearingSummary>();
 281
 282     if (onlyVisitSSJavaLoop) {
 283       // when analyzing ssjava loop,
 284       // complete summary is merging of all previous nodes of ssjava loop
 285       // entrance
 286       for (int i = 0; i < ssjavaLoopEntrance.numPrev(); i++) {
 287         ClearingSummary frnSummary =
 288             mapFlatNodeToClearingSummary.get(ssjavaLoopEntrance.getPrev(i));
 289         if (frnSummary != null) {
 290           summarySet.add(frnSummary);
 291         }
 292       }
 293     } else {
 294       // merging all exit node summary into the complete summary
 295       if (!returnNodeSet.isEmpty()) {
 296         for (Iterator iterator = returnNodeSet.iterator(); iterator.hasNext();) {
 297           FlatNode frn = (FlatNode) iterator.next();
 298           ClearingSummary frnSummary = mapFlatNodeToClearingSummary.get(frn);
 299           summarySet.add(frnSummary);
 300         }
 301       }
 302     }
 303     mergeSharedLocationAnaylsis(completeSummary, summarySet);
 304     return completeSummary;
 305   }
 306
 307   private void sharedLocation_nodeActions(MethodDescriptor caller, FlatNode fn,
 308       ClearingSummary curr, Set<FlatNode> returnNodeSet, boolean isSSJavaLoop) {
 309
 310     TempDescriptor lhs;
 311     TempDescriptor rhs;
 312     FieldDescriptor fld;
 313     switch (fn.kind()) {
 314
 315     case FKind.FlatMethod: {
 316       FlatMethod fm = (FlatMethod) fn;
 317
 318       ClearingSummary summaryFromCaller =
 319           mapMethodDescriptorToInitialClearingSummary.get(fm.getMethod());
 320
 321       Set<ClearingSummary> inSet = new HashSet<ClearingSummary>();
 322       inSet.add(summaryFromCaller);
 323       mergeSharedLocationAnaylsis(curr, inSet);
 324
 325     }
 326       break;
 327
 328     case FKind.FlatOpNode: {
 329       FlatOpNode fon = (FlatOpNode) fn;
 330       lhs = fon.getDest();
 331       rhs = fon.getLeft();
 332
 333       if (fon.getOp().getOp() == Operation.ASSIGN) {
 334         if (rhs.getType().isImmutable() && isSSJavaLoop) {
 335           // in ssjavaloop, we need to take care about reading local variables!
 336           NTuple<Descriptor> rhsHeapPath = new NTuple<Descriptor>();
 337           NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
 338           rhsHeapPath.add(LOCAL);
 339           lhsHeapPath.add(LOCAL);
 340           if (!lhs.getSymbol().startsWith("neverused")) {
 341             readLocation(curr, rhsHeapPath, rhs);
 342             writeLocation(curr, lhsHeapPath, lhs);
 343           }
 344         }
 345       }
 346
 347     }
 348       break;
 349
 350     case FKind.FlatFieldNode:
 351     case FKind.FlatElementNode: {
 352
 353       if (fn.kind() == FKind.FlatFieldNode) {
 354         FlatFieldNode ffn = (FlatFieldNode) fn;
 355         lhs = ffn.getDst();
 356         rhs = ffn.getSrc();
 357         fld = ffn.getField();
 358       } else {
 359         FlatElementNode fen = (FlatElementNode) fn;
 360         lhs = fen.getDst();
 361         rhs = fen.getSrc();
 362         TypeDescriptor td = rhs.getType().dereference();
 363         fld = getArrayField(td);
 364       }
 365
 366       // FlatFieldNode ffn = (FlatFieldNode) fn;
 367       // lhs = ffn.getDst();
 368       // rhs = ffn.getSrc();
 369       // fld = ffn.getField();
 370
 371       // read field
 372       NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
 373
 374       // if (srcHeapPath != null) {
 375       // // if lhs srcHeapPath is null, it means that it is not reachable from
 376       // // callee's parameters. so just ignore it
 377       NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
 378
 379       if (fld.getType().isImmutable()) {
 380         readLocation(curr, fldHeapPath, fld);
 381       }
 382       // }
 383
 384     }
 385       break;
 386
 387     case FKind.FlatSetFieldNode:
 388     case FKind.FlatSetElementNode: {
 389
 390       FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
 391       lhs = fsfn.getDst();
 392       fld = fsfn.getField();
 393
 394       // write(field)
 395       NTuple<Descriptor> lhsHeapPath = computePath(lhs);
 396       NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
 397       if (fld.getType().isImmutable()) {
 398         writeLocation(curr, fldHeapPath, fld);
 399       } else {
 400         // updates reference field case:
 401         // 2. if there exists a tuple t in sharing summary that starts with
 402         // hp(x) then, set flag of tuple t to 'true'
 403         fldHeapPath.add(fld);
 404         Set<NTuple<Descriptor>> hpKeySet = curr.keySet();
 405         for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
 406           NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
 407           if (hpKey.startsWith(fldHeapPath)) {
 408             curr.get(hpKey).updateFlag(true);
 409           }
 410         }
 411       }
 412
 413     }
 414       break;
 415
 416     case FKind.FlatCall: {
 417
 418       FlatCall fc = (FlatCall) fn;
 419
 420       // find out the set of callees
 421       MethodDescriptor mdCallee = fc.getMethod();
 422       FlatMethod fmCallee = state.getMethodFlat(mdCallee);
 423       Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
 424       // TypeDescriptor typeDesc = fc.getThis().getType();
 425       setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
 426
 427       possibleCalleeCompleteSummarySetToCaller.clear();
 428
 429       for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
 430         MethodDescriptor mdPossibleCallee = (MethodDescriptor) iterator.next();
 431         FlatMethod calleeFlatMethod = state.getMethodFlat(mdPossibleCallee);
 432
 433         addDependent(mdPossibleCallee, // callee
 434             caller); // caller
 435
 436         calleesToEnqueue.add(mdPossibleCallee);
 437
 438         // updates possible callee's initial summary using caller's current
 439         // writing status
 440         ClearingSummary prevCalleeInitSummary =
 441             mapMethodDescriptorToInitialClearingSummary.get(mdPossibleCallee);
 442
 443         ClearingSummary calleeInitSummary =
 444             bindHeapPathOfCalleeCallerEffects(fc, calleeFlatMethod, curr);
 445
 446         // if changes, update the init summary
 447         // and reschedule the callee for analysis
 448         if (!calleeInitSummary.equals(prevCalleeInitSummary)) {
 449
 450           if (!methodDescriptorsToVisitStack.contains(mdPossibleCallee)) {
 451             methodDescriptorsToVisitStack.add(mdPossibleCallee);
 452           }
 453           mapMethodDescriptorToInitialClearingSummary.put(mdPossibleCallee, calleeInitSummary);
 454         }
 455
 456       }
 457
 458       // contribute callee's writing effects to the caller
 459       mergeSharedLocationAnaylsis(curr, possibleCalleeCompleteSummarySetToCaller);
 460
 461     }
 462       break;
 463
 464     case FKind.FlatReturnNode: {
 465       returnNodeSet.add(fn);
 466     }
 467       break;
 468
 469     }
 470
 471   }
 472
 473   private ClearingSummary bindHeapPathOfCalleeCallerEffects(FlatCall fc,
 474       FlatMethod calleeFlatMethod, ClearingSummary curr) {
 475
 476     ClearingSummary boundSet = new ClearingSummary();
 477
 478     // create mapping from arg idx to its heap paths
 479     Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
 480         new Hashtable<Integer, NTuple<Descriptor>>();
 481
 482     if (fc.getThis() != null) {
 483       // arg idx is starting from 'this' arg
 484       NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
 485       if (thisHeapPath == null) {
 486         // method is called without creating new flat node representing 'this'
 487         thisHeapPath = new NTuple<Descriptor>();
 488         thisHeapPath.add(fc.getThis());
 489       }
 490
 491       mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
 492     }
 493
 494     for (int i = 0; i < fc.numArgs(); i++) {
 495       TempDescriptor arg = fc.getArg(i);
 496       NTuple<Descriptor> argHeapPath = computePath(arg);
 497       mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
 498     }
 499
 500     Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
 501         new Hashtable<Integer, TempDescriptor>();
 502     for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
 503       TempDescriptor param = calleeFlatMethod.getParameter(i);
 504       mapParamIdx2ParamTempDesc.put(Integer.valueOf(i), param);
 505     }
 506
 507     // binding caller's writing effects to callee's params
 508     for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
 509       NTuple<Descriptor> argHeapPath = mapArgIdx2CallerArgHeapPath.get(Integer.valueOf(i));
 510       TempDescriptor calleeParamHeapPath = mapParamIdx2ParamTempDesc.get(Integer.valueOf(i));
 511
 512       // iterate over caller's writing effect set
 513       Set<NTuple<Descriptor>> hpKeySet = curr.keySet();
 514       for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
 515         NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
 516         // current element is reachable caller's arg
 517         // so need to bind it to the caller's side and add it to the callee's
 518         // init summary
 519         if (hpKey.startsWith(argHeapPath)) {
 520           NTuple<Descriptor> boundHeapPath = replace(hpKey, argHeapPath, calleeParamHeapPath);
 521           boundSet.put(boundHeapPath, curr.get(hpKey).clone());
 522         }
 523
 524       }
 525
 526     }
 527
 528     // contribute callee's complete summary into the caller's current summary
 529     ClearingSummary calleeCompleteSummary =
 530         mapMethodDescriptorToCompleteClearingSummary.get(calleeFlatMethod.getMethod());
 531
 532     if (calleeCompleteSummary != null) {
 533       ClearingSummary boundCalleeEfffects = new ClearingSummary();
 534       for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
 535         NTuple<Descriptor> argHeapPath = mapArgIdx2CallerArgHeapPath.get(Integer.valueOf(i));
 536         TempDescriptor calleeParamHeapPath = mapParamIdx2ParamTempDesc.get(Integer.valueOf(i));
 537
 538         // iterate over callee's writing effect set
 539         Set<NTuple<Descriptor>> hpKeySet = calleeCompleteSummary.keySet();
 540         for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
 541           NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
 542           // current element is reachable caller's arg
 543           // so need to bind it to the caller's side and add it to the callee's
 544           // init summary
 545           if (hpKey.startsWith(calleeParamHeapPath)) {
 546
 547             NTuple<Descriptor> boundHeapPathForCaller = replace(hpKey, argHeapPath);
 548
 549             boundCalleeEfffects.put(boundHeapPathForCaller, calleeCompleteSummary.get(hpKey)
 550                 .clone());
 551
 552           }
 553         }
 554       }
 555       possibleCalleeCompleteSummarySetToCaller.add(boundCalleeEfffects);
 556     }
 557
 558     return boundSet;
 559   }
 560
 561   private NTuple<Descriptor> replace(NTuple<Descriptor> hpKey, NTuple<Descriptor> argHeapPath) {
 562
 563     // replace the head of heap path with caller's arg path
 564     // for example, heap path 'param.a.b' in callee's side will be replaced with
 565     // (corresponding arg heap path).a.b for caller's side
 566
 567     NTuple<Descriptor> bound = new NTuple<Descriptor>();
 568
 569     for (int i = 0; i < argHeapPath.size(); i++) {
 570       bound.add(argHeapPath.get(i));
 571     }
 572
 573     for (int i = 1; i < hpKey.size(); i++) {
 574       bound.add(hpKey.get(i));
 575     }
 576
 577     return bound;
 578   }
 579
 580   private NTuple<Descriptor> replace(NTuple<Descriptor> effectHeapPath,
 581       NTuple<Descriptor> argHeapPath, TempDescriptor calleeParamHeapPath) {
 582     // replace the head of caller's heap path with callee's param heap path
 583
 584     NTuple<Descriptor> boundHeapPath = new NTuple<Descriptor>();
 585     boundHeapPath.add(calleeParamHeapPath);
 586
 587     for (int i = argHeapPath.size(); i < effectHeapPath.size(); i++) {
 588       boundHeapPath.add(effectHeapPath.get(i));
 589     }
 590
 591     return boundHeapPath;
 592   }
 593
 594   private void computeReadSharedDescriptorSet() {
 595     Set<MethodDescriptor> methodDescriptorsToAnalyze = new HashSet<MethodDescriptor>();
 596     methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet());
 597
 598     for (Iterator iterator = methodDescriptorsToAnalyze.iterator(); iterator.hasNext();) {
 599       MethodDescriptor md = (MethodDescriptor) iterator.next();
 600       FlatMethod fm = state.getMethodFlat(md);
 601       computeReadSharedDescriptorSet_analyzeMethod(fm, md.equals(methodContainingSSJavaLoop));
 602     }
 603
 604   }
 605
 606   private void computeReadSharedDescriptorSet_analyzeMethod(FlatMethod fm,
 607       boolean onlyVisitSSJavaLoop) {
 608
 609     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
 610     Set<FlatNode> visited = new HashSet<FlatNode>();
 611
 612     if (onlyVisitSSJavaLoop) {
 613       flatNodesToVisit.add(ssjavaLoopEntrance);
 614     } else {
 615       flatNodesToVisit.add(fm);
 616     }
 617
 618     while (!flatNodesToVisit.isEmpty()) {
 619       FlatNode fn = flatNodesToVisit.iterator().next();
 620       flatNodesToVisit.remove(fn);
 621       visited.add(fn);
 622
 623       computeReadSharedDescriptorSet_nodeActions(fn, onlyVisitSSJavaLoop);
 624
 625       for (int i = 0; i < fn.numNext(); i++) {
 626         FlatNode nn = fn.getNext(i);
 627         if (!visited.contains(nn)) {
 628           if (!onlyVisitSSJavaLoop || (onlyVisitSSJavaLoop && loopIncElements.contains(nn))) {
 629             flatNodesToVisit.add(nn);
 630           }
 631         }
 632       }
 633
 634     }
 635
 636   }
 637
 638   private void computeReadSharedDescriptorSet_nodeActions(FlatNode fn, boolean isSSJavaLoop) {
 639
 640     TempDescriptor lhs;
 641     TempDescriptor rhs;
 642     FieldDescriptor fld;
 643
 644     switch (fn.kind()) {
 645     case FKind.FlatOpNode: {
 646       FlatOpNode fon = (FlatOpNode) fn;
 647       lhs = fon.getDest();
 648       rhs = fon.getLeft();
 649
 650       if (fon.getOp().getOp() == Operation.ASSIGN) {
 651         if (rhs.getType().isImmutable() && isSSJavaLoop && (!rhs.getSymbol().startsWith("srctmp"))) {
 652           // in ssjavaloop, we need to take care about reading local variables!
 653           NTuple<Descriptor> rhsHeapPath = new NTuple<Descriptor>();
 654           NTuple<Descriptor> lhsHeapPath = new NTuple<Descriptor>();
 655           rhsHeapPath.add(LOCAL);
 656           addReadDescriptor(rhsHeapPath, rhs);
 657         }
 658       }
 659
 660     }
 661       break;
 662
 663     case FKind.FlatFieldNode:
 664     case FKind.FlatElementNode: {
 665
 666       if (fn.kind() == FKind.FlatFieldNode) {
 667         FlatFieldNode ffn = (FlatFieldNode) fn;
 668         lhs = ffn.getDst();
 669         rhs = ffn.getSrc();
 670         fld = ffn.getField();
 671       } else {
 672         FlatElementNode fen = (FlatElementNode) fn;
 673         lhs = fen.getDst();
 674         rhs = fen.getSrc();
 675         TypeDescriptor td = rhs.getType().dereference();
 676         fld = getArrayField(td);
 677       }
 678
 679       // FlatFieldNode ffn = (FlatFieldNode) fn;
 680       // lhs = ffn.getDst();
 681       // rhs = ffn.getSrc();
 682       // fld = ffn.getField();
 683
 684       // read field
 685       NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
 686       NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
 687       // fldHeapPath.add(fld);
 688
 689       if (fld.getType().isImmutable()) {
 690         addReadDescriptor(fldHeapPath, fld);
 691       }
 692
 693       // propagate rhs's heap path to the lhs
 694       mapHeapPath.put(lhs, fldHeapPath);
 695
 696     }
 697       break;
 698
 699     case FKind.FlatSetFieldNode:
 700     case FKind.FlatSetElementNode: {
 701
 702       FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
 703       lhs = fsfn.getDst();
 704       fld = fsfn.getField();
 705
 706       // write(field)
 707       NTuple<Descriptor> lhsHeapPath = computePath(lhs);
 708       NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
 709       // writeLocation(curr, fldHeapPath, fld, getLocation(fld));
 710
 711     }
 712       break;
 713
 714     }
 715   }
 716
 717   private boolean hasReadingEffectOnSharedLocation(NTuple<Descriptor> hp, Location loc, Descriptor d) {
 718     if (!mapSharedLocation2DescriptorSet.containsKey(loc)) {
 719       return false;
 720     } else {
 721       return mapSharedLocation2DescriptorSet.get(loc).contains(d);
 722     }
 723   }
 724
 725   private void addReadDescriptor(NTuple<Descriptor> hp, Descriptor d) {
 726
 727     Location loc = getLocation(d);
 728
 729     if (loc != null && ssjava.isSharedLocation(loc)) {
 730
 731       Set<Descriptor> set = mapSharedLocation2DescriptorSet.get(loc);
 732       if (set == null) {
 733         set = new HashSet<Descriptor>();
 734         mapSharedLocation2DescriptorSet.put(loc, set);
 735       }
 736       set.add(d);
 737     }
 738
 739   }
 740
 741   private Location getLocation(Descriptor d) {
 742
 743     if (d instanceof FieldDescriptor) {
 744       return (Location) ((FieldDescriptor) d).getType().getExtension();
 745     } else {
 746       assert d instanceof TempDescriptor;
 747       CompositeLocation comp = (CompositeLocation) ((TempDescriptor) d).getType().getExtension();
 748       if (comp == null) {
 749         return null;
 750       } else {
 751         return comp.get(comp.getSize() - 1);
 752       }
 753     }
 754
 755   }
 756
 757   private void writeLocation(ClearingSummary curr, NTuple<Descriptor> hp, Descriptor d) {
 758     Location loc = getLocation(d);
 759     if (loc != null && hasReadingEffectOnSharedLocation(hp, loc, d)) {
 760
 761       // 1. add field x to the clearing set
 762       SharedStatus state = getState(curr, hp);
 763       state.addVar(loc, d);
 764
 765       // 3. if the set v contains all of variables belonging to the shared
 766       // location, set flag to true
 767       Set<Descriptor> sharedVarSet = mapSharedLocation2DescriptorSet.get(loc);
 768       if (state.getVarSet(loc).containsAll(sharedVarSet)) {
 769         state.updateFlag(loc, true);
 770       }
 771     }
 772   }
 773
 774   private void readLocation(ClearingSummary curr, NTuple<Descriptor> hp, Descriptor d) {
 775     // remove reading var x from written set
 776     Location loc = getLocation(d);
 777     if (loc != null && hasReadingEffectOnSharedLocation(hp, loc, d)) {
 778       SharedStatus state = getState(curr, hp);
 779       state.removeVar(loc, d);
 780     }
 781   }
 782
 783   private SharedStatus getState(ClearingSummary curr, NTuple<Descriptor> hp) {
 784     SharedStatus state = curr.get(hp);
 785     if (state == null) {
 786       state = new SharedStatus();
 787       curr.put(hp, state);
 788     }
 789     return state;
 790   }
 791
 792   private void writtenAnalyis() {
 793     // perform second stage analysis: intraprocedural analysis ensure that
 794     // all
 795     // variables are definitely written in-between the same read
 796
 797     // First, identify ssjava loop entrace
 798     FlatMethod fm = state.getMethodFlat(methodContainingSSJavaLoop);
 799     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
 800     flatNodesToVisit.add(fm);
 801
 802     LoopFinder loopFinder = new LoopFinder(fm);
 803
 804     while (!flatNodesToVisit.isEmpty()) {
 805       FlatNode fn = flatNodesToVisit.iterator().next();
 806       flatNodesToVisit.remove(fn);
 807
 808       String label = (String) state.fn2labelMap.get(fn);
 809       if (label != null) {
 810
 811         if (label.equals(ssjava.SSJAVA)) {
 812           ssjavaLoopEntrance = fn;
 813           break;
 814         }
 815       }
 816
 817       for (int i = 0; i < fn.numNext(); i++) {
 818         FlatNode nn = fn.getNext(i);
 819         flatNodesToVisit.add(nn);
 820       }
 821     }
 822
 823     assert ssjavaLoopEntrance != null;
 824
 825     // assume that ssjava loop is top-level loop in method, not nested loop
 826     Set nestedLoop = loopFinder.nestedLoops();
 827     for (Iterator loopIter = nestedLoop.iterator(); loopIter.hasNext();) {
 828       LoopFinder lf = (LoopFinder) loopIter.next();
 829       if (lf.loopEntrances().iterator().next().equals(ssjavaLoopEntrance)) {
 830         ssjavaLoop = lf;
 831       }
 832     }
 833
 834     assert ssjavaLoop != null;
 835
 836     writtenAnalysis_analyzeLoop();
 837
 838     if (debugcount > 0) {
 839       throw new Error();
 840     }
 841
 842   }
 843
 844   private void writtenAnalysis_analyzeLoop() {
 845
 846     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
 847     flatNodesToVisit.add(ssjavaLoopEntrance);
 848
 849     loopIncElements = (Set<FlatNode>) ssjavaLoop.loopIncElements();
 850
 851     while (!flatNodesToVisit.isEmpty()) {
 852       FlatNode fn = (FlatNode) flatNodesToVisit.iterator().next();
 853       flatNodesToVisit.remove(fn);
 854
 855       Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> prev =
 856           definitelyWrittenResults.get(fn);
 857
 858       Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr =
 859           new Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>>();
 860       for (int i = 0; i < fn.numPrev(); i++) {
 861         FlatNode nn = fn.getPrev(i);
 862         Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> dwIn =
 863             definitelyWrittenResults.get(nn);
 864         if (dwIn != null) {
 865           merge(curr, dwIn);
 866         }
 867       }
 868
 869       writtenAnalysis_nodeAction(fn, curr, ssjavaLoopEntrance);
 870
 871       // if a new result, schedule forward nodes for analysis
 872       if (!curr.equals(prev)) {
 873         definitelyWrittenResults.put(fn, curr);
 874
 875         for (int i = 0; i < fn.numNext(); i++) {
 876           FlatNode nn = fn.getNext(i);
 877           if (loopIncElements.contains(nn)) {
 878             flatNodesToVisit.add(nn);
 879           }
 880
 881         }
 882       }
 883     }
 884   }
 885
 886   private void writtenAnalysis_nodeAction(FlatNode fn,
 887       Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr, FlatNode loopEntrance) {
 888
 889     if (fn.equals(loopEntrance)) {
 890       // it reaches loop entrance: changes all flag to true
 891       Set<NTuple<Descriptor>> keySet = curr.keySet();
 892       for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
 893         NTuple<Descriptor> key = (NTuple<Descriptor>) iterator.next();
 894         Hashtable<FlatNode, Boolean> pair = curr.get(key);
 895         if (pair != null) {
 896           Set<FlatNode> pairKeySet = pair.keySet();
 897           for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) {
 898             FlatNode pairKey = (FlatNode) iterator2.next();
 899             pair.put(pairKey, Boolean.TRUE);
 900           }
 901         }
 902       }
 903     } else {
 904       TempDescriptor lhs;
 905       TempDescriptor rhs;
 906       FieldDescriptor fld;
 907
 908       switch (fn.kind()) {
 909       case FKind.FlatOpNode: {
 910         FlatOpNode fon = (FlatOpNode) fn;
 911         lhs = fon.getDest();
 912         rhs = fon.getLeft();
 913
 914         NTuple<Descriptor> rhsHeapPath = computePath(rhs);
 915         if (!rhs.getType().isImmutable()) {
 916           mapHeapPath.put(lhs, rhsHeapPath);
 917         } else {
 918           if (fon.getOp().getOp() == Operation.ASSIGN) {
 919             // read(rhs)
 920             readValue(fn, rhsHeapPath, curr);
 921           }
 922           // write(lhs)
 923           NTuple<Descriptor> lhsHeapPath = computePath(lhs);
 924           removeHeapPath(curr, lhsHeapPath);
 925         }
 926       }
 927         break;
 928
 929       case FKind.FlatLiteralNode: {
 930         FlatLiteralNode fln = (FlatLiteralNode) fn;
 931         lhs = fln.getDst();
 932
 933         // write(lhs)
 934         NTuple<Descriptor> lhsHeapPath = computePath(lhs);
 935         removeHeapPath(curr, lhsHeapPath);
 936
 937       }
 938         break;
 939
 940       case FKind.FlatFieldNode:
 941       case FKind.FlatElementNode: {
 942
 943         if (fn.kind() == FKind.FlatFieldNode) {
 944           FlatFieldNode ffn = (FlatFieldNode) fn;
 945           lhs = ffn.getDst();
 946           rhs = ffn.getSrc();
 947           fld = ffn.getField();
 948         } else {
 949           FlatElementNode fen = (FlatElementNode) fn;
 950           lhs = fen.getDst();
 951           rhs = fen.getSrc();
 952           TypeDescriptor td = rhs.getType().dereference();
 953           fld = getArrayField(td);
 954         }
 955
 956         if (fld.isFinal() /* && fld.isStatic() */) {
 957           // if field is final and static, no need to check
 958           break;
 959         }
 960
 961         // read field
 962         NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
 963         NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
 964         fldHeapPath.add(fld);
 965
 966         if (fld.getType().isImmutable()) {
 967           readValue(fn, fldHeapPath, curr);
 968         }
 969
 970         // propagate rhs's heap path to the lhs
 971         mapHeapPath.put(lhs, fldHeapPath);
 972
 973       }
 974         break;
 975
 976       case FKind.FlatSetFieldNode:
 977       case FKind.FlatSetElementNode: {
 978
 979         if (fn.kind() == FKind.FlatSetFieldNode) {
 980           FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
 981           lhs = fsfn.getDst();
 982           fld = fsfn.getField();
 983         } else {
 984           FlatSetElementNode fsen = (FlatSetElementNode) fn;
 985           lhs = fsen.getDst();
 986           rhs = fsen.getSrc();
 987           TypeDescriptor td = lhs.getType().dereference();
 988           fld = getArrayField(td);
 989         }
 990
 991         // write(field)
 992         NTuple<Descriptor> lhsHeapPath = computePath(lhs);
 993         NTuple<Descriptor> fldHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
 994         fldHeapPath.add(fld);
 995         removeHeapPath(curr, fldHeapPath);
 996
 997       }
 998         break;
 999
1000       case FKind.FlatCall: {
1001         FlatCall fc = (FlatCall) fn;
1002
1003         bindHeapPathCallerArgWithCaleeParam(fc);
1004         // add <hp,statement,false> in which hp is an element of
1005         // READ_bound set
1006         // of callee: callee has 'read' requirement!
1007
1008         for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
1009           NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
1010           Hashtable<FlatNode, Boolean> gen = curr.get(read);
1011           if (gen == null) {
1012             gen = new Hashtable<FlatNode, Boolean>();
1013             curr.put(read, gen);
1014           }
1015           Boolean currentStatus = gen.get(fn);
1016           if (currentStatus == null) {
1017             gen.put(fn, Boolean.FALSE);
1018           } else {
1019             checkFlag(currentStatus.booleanValue(), fn, read);
1020           }
1021         }
1022
1023         // removes <hp,statement,flag> if hp is an element of
1024         // OVERWRITE_bound
1025         // set of callee. it means that callee will overwrite it
1026         for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
1027           NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
1028           removeHeapPath(curr, write);
1029         }
1030       }
1031         break;
1032
1033       }
1034     }
1035
1036   }
1037
1038   private void readValue(FlatNode fn, NTuple<Descriptor> hp,
1039       Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr) {
1040     Hashtable<FlatNode, Boolean> gen = curr.get(hp);
1041     if (gen == null) {
1042       gen = new Hashtable<FlatNode, Boolean>();
1043       curr.put(hp, gen);
1044     }
1045     Boolean currentStatus = gen.get(fn);
1046     if (currentStatus == null) {
1047       gen.put(fn, Boolean.FALSE);
1048     } else {
1049       checkFlag(currentStatus.booleanValue(), fn, hp);
1050     }
1051
1052   }
1053
1054   private void removeHeapPath(Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr,
1055       NTuple<Descriptor> hp) {
1056
1057     // removes all of heap path that starts with prefix 'hp'
1058     // since any reference overwrite along heap path gives overwriting side
1059     // effects on the value
1060
1061     Set<NTuple<Descriptor>> keySet = curr.keySet();
1062     for (Iterator<NTuple<Descriptor>> iter = keySet.iterator(); iter.hasNext();) {
1063       NTuple<Descriptor> key = iter.next();
1064       if (key.startsWith(hp)) {
1065         curr.put(key, new Hashtable<FlatNode, Boolean>());
1066       }
1067     }
1068
1069   }
1070
1071   private void bindHeapPathCallerArgWithCaleeParam(FlatCall fc) {
1072     // compute all possible callee set
1073     // transform all READ/OVERWRITE set from the any possible
1074     // callees to the
1075     // caller
1076     calleeUnionBoundReadSet.clear();
1077     calleeIntersectBoundOverWriteSet.clear();
1078     calleeBoundWriteSet.clear();
1079
1080     if (ssjava.isSSJavaUtil(fc.getMethod().getClassDesc())) {
1081       // ssjava util case!
1082       // have write effects on the first argument
1083       TempDescriptor arg = fc.getArg(0);
1084       NTuple<Descriptor> argHeapPath = computePath(arg);
1085       calleeIntersectBoundOverWriteSet.add(argHeapPath);
1086     } else {
1087       MethodDescriptor mdCallee = fc.getMethod();
1088       // FlatMethod fmCallee = state.getMethodFlat(mdCallee);
1089       Set<MethodDescriptor> setPossibleCallees = new HashSet<MethodDescriptor>();
1090       // setPossibleCallees.addAll(callGraph.getMethods(mdCallee, typeDesc));
1091       setPossibleCallees.addAll(callGraph.getMethods(mdCallee));
1092
1093       // create mapping from arg idx to its heap paths
1094       Hashtable<Integer, NTuple<Descriptor>> mapArgIdx2CallerArgHeapPath =
1095           new Hashtable<Integer, NTuple<Descriptor>>();
1096
1097       // arg idx is starting from 'this' arg
1098       if (fc.getThis() != null) {
1099         NTuple<Descriptor> thisHeapPath = mapHeapPath.get(fc.getThis());
1100         if (thisHeapPath == null) {
1101           // method is called without creating new flat node representing 'this'
1102           thisHeapPath = new NTuple<Descriptor>();
1103           thisHeapPath.add(fc.getThis());
1104         }
1105
1106         mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(0), thisHeapPath);
1107       }
1108
1109       for (int i = 0; i < fc.numArgs(); i++) {
1110         TempDescriptor arg = fc.getArg(i);
1111         NTuple<Descriptor> argHeapPath = computePath(arg);
1112         mapArgIdx2CallerArgHeapPath.put(Integer.valueOf(i + 1), argHeapPath);
1113       }
1114
1115       for (Iterator iterator = setPossibleCallees.iterator(); iterator.hasNext();) {
1116         MethodDescriptor callee = (MethodDescriptor) iterator.next();
1117         FlatMethod calleeFlatMethod = state.getMethodFlat(callee);
1118
1119         // binding caller's args and callee's params
1120
1121         Set<NTuple<Descriptor>> calleeReadSet = mapFlatMethodToRead.get(calleeFlatMethod);
1122         if (calleeReadSet == null) {
1123           calleeReadSet = new HashSet<NTuple<Descriptor>>();
1124           mapFlatMethodToRead.put(calleeFlatMethod, calleeReadSet);
1125         }
1126
1127         Set<NTuple<Descriptor>> calleeOverWriteSet = mapFlatMethodToOverWrite.get(calleeFlatMethod);
1128
1129         if (calleeOverWriteSet == null) {
1130           calleeOverWriteSet = new HashSet<NTuple<Descriptor>>();
1131           mapFlatMethodToOverWrite.put(calleeFlatMethod, calleeOverWriteSet);
1132         }
1133
1134         Set<NTuple<Descriptor>> calleeWriteSet = mapFlatMethodToWrite.get(calleeFlatMethod);
1135
1136         if (calleeWriteSet == null) {
1137           calleeWriteSet = new HashSet<NTuple<Descriptor>>();
1138           mapFlatMethodToWrite.put(calleeFlatMethod, calleeWriteSet);
1139         }
1140
1141         Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc =
1142             new Hashtable<Integer, TempDescriptor>();
1143         int offset = 0;
1144         if (calleeFlatMethod.getMethod().isStatic()) {
1145           // static method does not have implicit 'this' arg
1146           offset = 1;
1147         }
1148         for (int i = 0; i < calleeFlatMethod.numParameters(); i++) {
1149           TempDescriptor param = calleeFlatMethod.getParameter(i);
1150           mapParamIdx2ParamTempDesc.put(Integer.valueOf(i + offset), param);
1151         }
1152
1153         Set<NTuple<Descriptor>> calleeBoundReadSet =
1154             bindSet(calleeReadSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
1155         // union of the current read set and the current callee's
1156         // read set
1157         calleeUnionBoundReadSet.addAll(calleeBoundReadSet);
1158         Set<NTuple<Descriptor>> calleeBoundOverWriteSet =
1159             bindSet(calleeOverWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
1160         // intersection of the current overwrite set and the current
1161         // callee's
1162         // overwrite set
1163         merge(calleeIntersectBoundOverWriteSet, calleeBoundOverWriteSet);
1164
1165         Set<NTuple<Descriptor>> boundWriteSetFromCallee =
1166             bindSet(calleeWriteSet, mapParamIdx2ParamTempDesc, mapArgIdx2CallerArgHeapPath);
1167         calleeBoundWriteSet.addAll(boundWriteSetFromCallee);
1168       }
1169
1170     }
1171
1172   }
1173
1174   private void checkFlag(boolean booleanValue, FlatNode fn, NTuple<Descriptor> hp) {
1175     if (booleanValue) {
1176       // the definitely written analysis only takes care about locations that
1177       // are written to inside of the SSJava loop
1178       for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) {
1179         NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
1180         if (hp.startsWith(write)) {
1181           // it has write effect!
1182           // throw new Error(
1183           System.out
1184               .println("###"
1185                   + "There is a variable, which is reachable through references "
1186                   + hp
1187                   + ", who comes back to the same read statement without being overwritten at the out-most iteration at "
1188                   + methodContainingSSJavaLoop.getClassDesc().getSourceFileName() + "::"
1189                   + fn.getNumLine());
1190           debugcount++;
1191         }
1192       }
1193     }
1194   }
1195
1196   private void merge(Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> curr,
1197       Hashtable<NTuple<Descriptor>, Hashtable<FlatNode, Boolean>> in) {
1198
1199     Set<NTuple<Descriptor>> inKeySet = in.keySet();
1200     for (Iterator iterator = inKeySet.iterator(); iterator.hasNext();) {
1201       NTuple<Descriptor> inKey = (NTuple<Descriptor>) iterator.next();
1202       Hashtable<FlatNode, Boolean> inPair = in.get(inKey);
1203
1204       Set<FlatNode> pairKeySet = inPair.keySet();
1205       for (Iterator iterator2 = pairKeySet.iterator(); iterator2.hasNext();) {
1206         FlatNode pairKey = (FlatNode) iterator2.next();
1207         Boolean inFlag = inPair.get(pairKey);
1208
1209         Hashtable<FlatNode, Boolean> currPair = curr.get(inKey);
1210         if (currPair == null) {
1211           currPair = new Hashtable<FlatNode, Boolean>();
1212           curr.put(inKey, currPair);
1213         }
1214
1215         Boolean currFlag = currPair.get(pairKey);
1216         // by default, flag is set by false
1217         if (currFlag == null) {
1218           currFlag = Boolean.FALSE;
1219         }
1220         currFlag = Boolean.valueOf(inFlag.booleanValue() | currFlag.booleanValue());
1221         currPair.put(pairKey, currFlag);
1222       }
1223
1224     }
1225
1226   }
1227
1228   private void methodReadOverWriteAnalysis() {
1229     // perform method READ/OVERWRITE analysis
1230     Set<MethodDescriptor> methodDescriptorsToAnalyze = new HashSet<MethodDescriptor>();
1231     methodDescriptorsToAnalyze.addAll(ssjava.getAnnotationRequireSet());
1232
1233     sortedDescriptors = topologicalSort(methodDescriptorsToAnalyze);
1234
1235     LinkedList<MethodDescriptor> descriptorListToAnalyze =
1236         (LinkedList<MethodDescriptor>) sortedDescriptors.clone();
1237
1238     // no need to analyze method having ssjava loop
1239     // methodContainingSSJavaLoop = descriptorListToAnalyze.removeFirst();
1240     methodContainingSSJavaLoop = ssjava.getMethodContainingSSJavaLoop();
1241
1242     // current descriptors to visit in fixed-point interprocedural analysis,
1243     // prioritized by
1244     // dependency in the call graph
1245     methodDescriptorsToVisitStack.clear();
1246
1247     Set<MethodDescriptor> methodDescriptorToVistSet = new HashSet<MethodDescriptor>();
1248     methodDescriptorToVistSet.addAll(descriptorListToAnalyze);
1249
1250     while (!descriptorListToAnalyze.isEmpty()) {
1251       MethodDescriptor md = descriptorListToAnalyze.removeFirst();
1252       methodDescriptorsToVisitStack.add(md);
1253     }
1254
1255     // analyze scheduled methods until there are no more to visit
1256     while (!methodDescriptorsToVisitStack.isEmpty()) {
1257       // start to analyze leaf node
1258       MethodDescriptor md = methodDescriptorsToVisitStack.pop();
1259       FlatMethod fm = state.getMethodFlat(md);
1260
1261       Set<NTuple<Descriptor>> readSet = new HashSet<NTuple<Descriptor>>();
1262       Set<NTuple<Descriptor>> overWriteSet = new HashSet<NTuple<Descriptor>>();
1263       Set<NTuple<Descriptor>> writeSet = new HashSet<NTuple<Descriptor>>();
1264
1265       methodReadOverWrite_analyzeMethod(fm, readSet, overWriteSet, writeSet);
1266
1267       Set<NTuple<Descriptor>> prevRead = mapFlatMethodToRead.get(fm);
1268       Set<NTuple<Descriptor>> prevOverWrite = mapFlatMethodToOverWrite.get(fm);
1269       Set<NTuple<Descriptor>> prevWrite = mapFlatMethodToWrite.get(fm);
1270
1271       if (!(readSet.equals(prevRead) && overWriteSet.equals(prevOverWrite) && writeSet
1272           .equals(prevWrite))) {
1273         mapFlatMethodToRead.put(fm, readSet);
1274         mapFlatMethodToOverWrite.put(fm, overWriteSet);
1275         mapFlatMethodToWrite.put(fm, writeSet);
1276
1277         // results for callee changed, so enqueue dependents caller for
1278         // further
1279         // analysis
1280         Iterator<MethodDescriptor> depsItr = getDependents(md).iterator();
1281         while (depsItr.hasNext()) {
1282           MethodDescriptor methodNext = depsItr.next();
1283           if (!methodDescriptorsToVisitStack.contains(methodNext)
1284               && methodDescriptorToVistSet.contains(methodNext)) {
1285             methodDescriptorsToVisitStack.add(methodNext);
1286           }
1287
1288         }
1289
1290       }
1291
1292     }
1293
1294   }
1295
1296   private void methodReadOverWrite_analyzeMethod(FlatMethod fm, Set<NTuple<Descriptor>> readSet,
1297       Set<NTuple<Descriptor>> overWriteSet, Set<NTuple<Descriptor>> writeSet) {
1298     if (state.SSJAVADEBUG) {
1299       System.out.println("Definitely written Analyzing: " + fm);
1300     }
1301
1302     // intraprocedural analysis
1303     Set<FlatNode> flatNodesToVisit = new HashSet<FlatNode>();
1304     flatNodesToVisit.add(fm);
1305
1306     while (!flatNodesToVisit.isEmpty()) {
1307       FlatNode fn = flatNodesToVisit.iterator().next();
1308       flatNodesToVisit.remove(fn);
1309
1310       Set<NTuple<Descriptor>> curr = new HashSet<NTuple<Descriptor>>();
1311
1312       for (int i = 0; i < fn.numPrev(); i++) {
1313         FlatNode prevFn = fn.getPrev(i);
1314         Set<NTuple<Descriptor>> in = mapFlatNodeToWrittenSet.get(prevFn);
1315         if (in != null) {
1316           merge(curr, in);
1317         }
1318       }
1319
1320       methodReadOverWrite_nodeActions(fn, curr, readSet, overWriteSet, writeSet);
1321
1322       Set<NTuple<Descriptor>> writtenSetPrev = mapFlatNodeToWrittenSet.get(fn);
1323       if (!curr.equals(writtenSetPrev)) {
1324         mapFlatNodeToWrittenSet.put(fn, curr);
1325         for (int i = 0; i < fn.numNext(); i++) {
1326           FlatNode nn = fn.getNext(i);
1327           flatNodesToVisit.add(nn);
1328         }
1329       }
1330
1331     }
1332
1333   }
1334
1335   private void methodReadOverWrite_nodeActions(FlatNode fn, Set<NTuple<Descriptor>> writtenSet,
1336       Set<NTuple<Descriptor>> readSet, Set<NTuple<Descriptor>> overWriteSet,
1337       Set<NTuple<Descriptor>> writeSet) {
1338     TempDescriptor lhs;
1339     TempDescriptor rhs;
1340     FieldDescriptor fld;
1341
1342     switch (fn.kind()) {
1343     case FKind.FlatMethod: {
1344
1345       // set up initial heap paths for method parameters
1346       FlatMethod fm = (FlatMethod) fn;
1347       for (int i = 0; i < fm.numParameters(); i++) {
1348         TempDescriptor param = fm.getParameter(i);
1349         NTuple<Descriptor> heapPath = new NTuple<Descriptor>();
1350         heapPath.add(param);
1351         mapHeapPath.put(param, heapPath);
1352       }
1353     }
1354       break;
1355
1356     case FKind.FlatOpNode: {
1357       FlatOpNode fon = (FlatOpNode) fn;
1358       // for a normal assign node, need to propagate lhs's heap path to
1359       // rhs
1360       if (fon.getOp().getOp() == Operation.ASSIGN) {
1361         rhs = fon.getLeft();
1362         lhs = fon.getDest();
1363
1364         NTuple<Descriptor> rhsHeapPath = mapHeapPath.get(rhs);
1365         if (rhsHeapPath != null) {
1366           mapHeapPath.put(lhs, mapHeapPath.get(rhs));
1367         }
1368
1369       }
1370     }
1371       break;
1372
1373     case FKind.FlatElementNode:
1374     case FKind.FlatFieldNode: {
1375
1376       // y=x.f;
1377
1378       if (fn.kind() == FKind.FlatFieldNode) {
1379         FlatFieldNode ffn = (FlatFieldNode) fn;
1380         lhs = ffn.getDst();
1381         rhs = ffn.getSrc();
1382         fld = ffn.getField();
1383       } else {
1384         FlatElementNode fen = (FlatElementNode) fn;
1385         lhs = fen.getDst();
1386         rhs = fen.getSrc();
1387         TypeDescriptor td = rhs.getType().dereference();
1388         fld = getArrayField(td);
1389       }
1390
1391       if (fld.isFinal() /* && fld.isStatic() */) {
1392         // if field is final and static, no need to check
1393         break;
1394       }
1395
1396       // set up heap path
1397       NTuple<Descriptor> srcHeapPath = mapHeapPath.get(rhs);
1398       if (srcHeapPath != null) {
1399         // if lhs srcHeapPath is null, it means that it is not reachable from
1400         // callee's parameters. so just ignore it
1401
1402         NTuple<Descriptor> readingHeapPath = new NTuple<Descriptor>(srcHeapPath.getList());
1403         readingHeapPath.add(fld);
1404         mapHeapPath.put(lhs, readingHeapPath);
1405
1406         // read (x.f)
1407         if (fld.getType().isImmutable()) {
1408           // if WT doesnot have hp(x.f), add hp(x.f) to READ
1409           if (!writtenSet.contains(readingHeapPath)) {
1410             readSet.add(readingHeapPath);
1411           }
1412         }
1413
1414         // no need to kill hp(x.f) from WT
1415       }
1416
1417     }
1418       break;
1419
1420     case FKind.FlatSetFieldNode:
1421     case FKind.FlatSetElementNode: {
1422
1423       // x.f=y;
1424
1425       if (fn.kind() == FKind.FlatSetFieldNode) {
1426         FlatSetFieldNode fsfn = (FlatSetFieldNode) fn;
1427         lhs = fsfn.getDst();
1428         fld = fsfn.getField();
1429         rhs = fsfn.getSrc();
1430       } else {
1431         FlatSetElementNode fsen = (FlatSetElementNode) fn;
1432         lhs = fsen.getDst();
1433         rhs = fsen.getSrc();
1434         TypeDescriptor td = lhs.getType().dereference();
1435         fld = getArrayField(td);
1436       }
1437
1438       // set up heap path
1439       NTuple<Descriptor> lhsHeapPath = mapHeapPath.get(lhs);
1440       if (lhsHeapPath != null) {
1441         // if lhs heap path is null, it means that it is not reachable from
1442         // callee's parameters. so just ignore it
1443         NTuple<Descriptor> newHeapPath = new NTuple<Descriptor>(lhsHeapPath.getList());
1444         newHeapPath.add(fld);
1445         mapHeapPath.put(fld, newHeapPath);
1446
1447         // write(x.f)
1448         // need to add hp(y) to WT
1449         writtenSet.add(newHeapPath);
1450
1451         writeSet.add(newHeapPath);
1452       }
1453
1454     }
1455       break;
1456
1457     case FKind.FlatCall: {
1458
1459       FlatCall fc = (FlatCall) fn;
1460
1461       bindHeapPathCallerArgWithCaleeParam(fc);
1462
1463       // add heap path, which is an element of READ_bound set and is not
1464       // an
1465       // element of WT set, to the caller's READ set
1466       for (Iterator iterator = calleeUnionBoundReadSet.iterator(); iterator.hasNext();) {
1467         NTuple<Descriptor> read = (NTuple<Descriptor>) iterator.next();
1468         if (!writtenSet.contains(read)) {
1469           readSet.add(read);
1470         }
1471       }
1472
1473       // add heap path, which is an element of OVERWRITE_bound set, to the
1474       // caller's WT set
1475       for (Iterator iterator = calleeIntersectBoundOverWriteSet.iterator(); iterator.hasNext();) {
1476         NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
1477         writtenSet.add(write);
1478       }
1479
1480       // add heap path, which is an element of WRITE_BOUND set, to the
1481       // caller's writeSet
1482       for (Iterator iterator = calleeBoundWriteSet.iterator(); iterator.hasNext();) {
1483         NTuple<Descriptor> write = (NTuple<Descriptor>) iterator.next();
1484         writeSet.add(write);
1485       }
1486
1487     }
1488       break;
1489
1490     case FKind.FlatExit: {
1491       // merge the current written set with OVERWRITE set
1492       merge(overWriteSet, writtenSet);
1493     }
1494       break;
1495
1496     }
1497
1498   }
1499
1500   static public FieldDescriptor getArrayField(TypeDescriptor td) {
1501     FieldDescriptor fd = mapTypeToArrayField.get(td);
1502     if (fd == null) {
1503       fd =
1504           new FieldDescriptor(new Modifiers(Modifiers.PUBLIC), td, arrayElementFieldName, null,
1505               false);
1506       mapTypeToArrayField.put(td, fd);
1507     }
1508     return fd;
1509   }
1510
1511   private void mergeSharedLocationAnaylsis(ClearingSummary curr, Set<ClearingSummary> inSet) {
1512
1513     if (inSet.size() == 0) {
1514       return;
1515     }
1516
1517     Hashtable<Pair<NTuple<Descriptor>, Location>, Boolean> mapHeapPathLoc2Flag =
1518         new Hashtable<Pair<NTuple<Descriptor>, Location>, Boolean>();
1519
1520     for (Iterator inIterator = inSet.iterator(); inIterator.hasNext();) {
1521
1522       ClearingSummary inTable = (ClearingSummary) inIterator.next();
1523
1524       Set<NTuple<Descriptor>> keySet = inTable.keySet();
1525
1526       for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
1527         NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
1528         SharedStatus inState = inTable.get(hpKey);
1529
1530         SharedStatus currState = curr.get(hpKey);
1531         if (currState == null) {
1532           currState = new SharedStatus();
1533           curr.put(hpKey, currState);
1534         }
1535         currState.merge(inState);
1536
1537         Set<Location> locSet = inState.getMap().keySet();
1538         for (Iterator iterator2 = locSet.iterator(); iterator2.hasNext();) {
1539           Location loc = (Location) iterator2.next();
1540           Pair<Set<Descriptor>, Boolean> pair = inState.getMap().get(loc);
1541           boolean inFlag = pair.getSecond().booleanValue();
1542
1543           Pair<NTuple<Descriptor>, Location> flagKey =
1544               new Pair<NTuple<Descriptor>, Location>(hpKey, loc);
1545           Boolean current = mapHeapPathLoc2Flag.get(flagKey);
1546           if (current == null) {
1547             current = new Boolean(true);
1548           }
1549           boolean newInFlag = current.booleanValue() & inFlag;
1550           mapHeapPathLoc2Flag.put(flagKey, Boolean.valueOf(newInFlag));
1551         }
1552
1553       }
1554
1555     }
1556
1557     // merge flag status
1558     Set<NTuple<Descriptor>> hpKeySet = curr.keySet();
1559     for (Iterator iterator = hpKeySet.iterator(); iterator.hasNext();) {
1560       NTuple<Descriptor> hpKey = (NTuple<Descriptor>) iterator.next();
1561       SharedStatus currState = curr.get(hpKey);
1562       Set<Location> locKeySet = currState.getMap().keySet();
1563       for (Iterator iterator2 = locKeySet.iterator(); iterator2.hasNext();) {
1564         Location locKey = (Location) iterator2.next();
1565         Pair<Set<Descriptor>, Boolean> pair = currState.getMap().get(locKey);
1566         boolean currentFlag = pair.getSecond().booleanValue();
1567         Boolean inFlag = mapHeapPathLoc2Flag.get(new Pair(hpKey, locKey));
1568         if (inFlag != null) {
1569           boolean newFlag = currentFlag | inFlag.booleanValue();
1570           if (currentFlag != newFlag) {
1571             currState.getMap().put(locKey, new Pair(pair.getFirst(), new Boolean(newFlag)));
1572           }
1573         }
1574       }
1575     }
1576
1577   }
1578
1579   private void merge(Set<NTuple<Descriptor>> curr, Set<NTuple<Descriptor>> in) {
1580     if (curr.isEmpty()) {
1581       // WrittenSet has a special initial value which covers all possible
1582       // elements
1583       // For the first time of intersection, we can take all previous set
1584       curr.addAll(in);
1585     } else {
1586       // otherwise, current set is the intersection of the two sets
1587       curr.retainAll(in);
1588     }
1589
1590   }
1591
1592   // combine two heap path
1593   private NTuple<Descriptor> combine(NTuple<Descriptor> callerIn, NTuple<Descriptor> calleeIn) {
1594     NTuple<Descriptor> combined = new NTuple<Descriptor>();
1595
1596     for (int i = 0; i < callerIn.size(); i++) {
1597       combined.add(callerIn.get(i));
1598     }
1599
1600     // the first element of callee's heap path represents parameter
1601     // so we skip the first one since it is already added from caller's heap
1602     // path
1603     for (int i = 1; i < calleeIn.size(); i++) {
1604       combined.add(calleeIn.get(i));
1605     }
1606
1607     return combined;
1608   }
1609
1610   private Set<NTuple<Descriptor>> bindSet(Set<NTuple<Descriptor>> calleeSet,
1611       Hashtable<Integer, TempDescriptor> mapParamIdx2ParamTempDesc,
1612       Hashtable<Integer, NTuple<Descriptor>> mapCallerArgIdx2HeapPath) {
1613
1614     Set<NTuple<Descriptor>> boundedCalleeSet = new HashSet<NTuple<Descriptor>>();
1615
1616     Set<Integer> keySet = mapCallerArgIdx2HeapPath.keySet();
1617     for (Iterator iterator = keySet.iterator(); iterator.hasNext();) {
1618       Integer idx = (Integer) iterator.next();
1619
1620       NTuple<Descriptor> callerArgHeapPath = mapCallerArgIdx2HeapPath.get(idx);
1621       TempDescriptor calleeParam = mapParamIdx2ParamTempDesc.get(idx);
1622       for (Iterator iterator2 = calleeSet.iterator(); iterator2.hasNext();) {
1623         NTuple<Descriptor> element = (NTuple<Descriptor>) iterator2.next();
1624         if (element.startsWith(calleeParam)) {
1625           NTuple<Descriptor> boundElement = combine(callerArgHeapPath, element);
1626           boundedCalleeSet.add(boundElement);
1627         }
1628
1629       }
1630
1631     }
1632     return boundedCalleeSet;
1633
1634   }
1635
1636   // Borrowed it from disjoint analysis
1637   private LinkedList<MethodDescriptor> topologicalSort(Set<MethodDescriptor> toSort) {
1638
1639     Set<MethodDescriptor> discovered = new HashSet<MethodDescriptor>();
1640
1641     LinkedList<MethodDescriptor> sorted = new LinkedList<MethodDescriptor>();
1642
1643     Iterator<MethodDescriptor> itr = toSort.iterator();
1644     while (itr.hasNext()) {
1645       MethodDescriptor d = itr.next();
1646
1647       if (!discovered.contains(d)) {
1648         dfsVisit(d, toSort, sorted, discovered);
1649       }
1650     }
1651
1652     return sorted;
1653   }
1654
1655   // While we're doing DFS on call graph, remember
1656   // dependencies for efficient queuing of methods
1657   // during interprocedural analysis:
1658   //
1659   // a dependent of a method decriptor d for this analysis is:
1660   // 1) a method or task that invokes d
1661   // 2) in the descriptorsToAnalyze set
1662   private void dfsVisit(MethodDescriptor md, Set<MethodDescriptor> toSort,
1663       LinkedList<MethodDescriptor> sorted, Set<MethodDescriptor> discovered) {
1664
1665     discovered.add(md);
1666
1667     Iterator itr = callGraph.getCallerSet(md).iterator();
1668     while (itr.hasNext()) {
1669       MethodDescriptor dCaller = (MethodDescriptor) itr.next();
1670       // only consider callers in the original set to analyze
1671       if (!toSort.contains(dCaller)) {
1672         continue;
1673       }
1674       if (!discovered.contains(dCaller)) {
1675         addDependent(md, // callee
1676             dCaller // caller
1677         );
1678
1679         dfsVisit(dCaller, toSort, sorted, discovered);
1680       }
1681     }
1682
1683     // for leaf-nodes last now!
1684     sorted.addLast(md);
1685   }
1686
1687   // a dependent of a method decriptor d for this analysis is:
1688   // 1) a method or task that invokes d
1689   // 2) in the descriptorsToAnalyze set
1690   private void addDependent(MethodDescriptor callee, MethodDescriptor caller) {
1691     Set<MethodDescriptor> deps = mapDescriptorToSetDependents.get(callee);
1692     if (deps == null) {
1693       deps = new HashSet<MethodDescriptor>();
1694     }
1695     deps.add(caller);
1696     mapDescriptorToSetDependents.put(callee, deps);
1697   }
1698
1699   private Set<MethodDescriptor> getDependents(MethodDescriptor callee) {
1700     Set<MethodDescriptor> deps = mapDescriptorToSetDependents.get(callee);
1701     if (deps == null) {
1702       deps = new HashSet<MethodDescriptor>();
1703       mapDescriptorToSetDependents.put(callee, deps);
1704     }
1705     return deps;
1706   }
1707
1708   private NTuple<Descriptor> computePath(TempDescriptor td) {
1709     // generate proper path fot input td
1710     // if td is local variable, it just generate one element tuple path
1711     if (mapHeapPath.containsKey(td)) {
1712       return mapHeapPath.get(td);
1713     } else {
1714       NTuple<Descriptor> path = new NTuple<Descriptor>();
1715       path.add(td);
1716       return path;
1717     }
1718   }
1719
1720 }