Robust/src/Analysis/SSJava/FlowDownCheck.java

   1 package Analysis.SSJava;
   2
   3 import java.util.ArrayList;
   4 import java.util.Collections;
   5 import java.util.Comparator;
   6 import java.util.HashSet;
   7 import java.util.Hashtable;
   8 import java.util.Iterator;
   9 import java.util.LinkedList;
  10 import java.util.List;
  11 import java.util.Set;
  12 import java.util.StringTokenizer;
  13 import java.util.Vector;
  14
  15 import Analysis.SSJava.FlowDownCheck.ComparisonResult;
  16 import Analysis.SSJava.FlowDownCheck.CompositeLattice;
  17 import IR.AnnotationDescriptor;
  18 import IR.ClassDescriptor;
  19 import IR.Descriptor;
  20 import IR.FieldDescriptor;
  21 import IR.MethodDescriptor;
  22 import IR.NameDescriptor;
  23 import IR.Operation;
  24 import IR.State;
  25 import IR.SymbolTable;
  26 import IR.TypeDescriptor;
  27 import IR.TypeExtension;
  28 import IR.VarDescriptor;
  29 import IR.Flat.FlatNode;
  30 import IR.Tree.ArrayAccessNode;
  31 import IR.Tree.AssignmentNode;
  32 import IR.Tree.BlockExpressionNode;
  33 import IR.Tree.BlockNode;
  34 import IR.Tree.BlockStatementNode;
  35 import IR.Tree.CastNode;
  36 import IR.Tree.CreateObjectNode;
  37 import IR.Tree.DeclarationNode;
  38 import IR.Tree.ExpressionNode;
  39 import IR.Tree.FieldAccessNode;
  40 import IR.Tree.IfStatementNode;
  41 import IR.Tree.Kind;
  42 import IR.Tree.LiteralNode;
  43 import IR.Tree.LoopNode;
  44 import IR.Tree.MethodInvokeNode;
  45 import IR.Tree.NameNode;
  46 import IR.Tree.OpNode;
  47 import IR.Tree.ReturnNode;
  48 import IR.Tree.SubBlockNode;
  49 import IR.Tree.SwitchBlockNode;
  50 import IR.Tree.SwitchStatementNode;
  51 import IR.Tree.SynchronizedNode;
  52 import IR.Tree.TertiaryNode;
  53 import IR.Tree.TreeNode;
  54 import Util.Pair;
  55
  56 public class FlowDownCheck {
  57
  58   State state;
  59   static SSJavaAnalysis ssjava;
  60
  61   Set<ClassDescriptor> toanalyze;
  62   List<ClassDescriptor> toanalyzeList;
  63
  64   Set<MethodDescriptor> toanalyzeMethod;
  65   List<MethodDescriptor> toanalyzeMethodList;
  66
  67   // mapping from 'descriptor' to 'composite location'
  68   Hashtable<Descriptor, CompositeLocation> d2loc;
  69
  70   Hashtable<MethodDescriptor, CompositeLocation> md2ReturnLoc;
  71   Hashtable<MethodDescriptor, ReturnLocGenerator> md2ReturnLocGen;
  72
  73   // mapping from 'locID' to 'class descriptor'
  74   Hashtable<String, ClassDescriptor> fieldLocName2cd;
  75
  76   boolean deterministic = true;
  77
  78   public FlowDownCheck(SSJavaAnalysis ssjava, State state) {
  79     this.ssjava = ssjava;
  80     this.state = state;
  81     if (deterministic) {
  82       this.toanalyzeList = new ArrayList<ClassDescriptor>();
  83     } else {
  84       this.toanalyze = new HashSet<ClassDescriptor>();
  85     }
  86     if (deterministic) {
  87       this.toanalyzeMethodList = new ArrayList<MethodDescriptor>();
  88     } else {
  89       this.toanalyzeMethod = new HashSet<MethodDescriptor>();
  90     }
  91     this.d2loc = new Hashtable<Descriptor, CompositeLocation>();
  92     this.fieldLocName2cd = new Hashtable<String, ClassDescriptor>();
  93     this.md2ReturnLoc = new Hashtable<MethodDescriptor, CompositeLocation>();
  94     this.md2ReturnLocGen = new Hashtable<MethodDescriptor, ReturnLocGenerator>();
  95   }
  96
  97   public void init() {
  98
  99     // construct mapping from the location name to the class descriptor
 100     // assume that the location name is unique through the whole program
 101
 102     Set<ClassDescriptor> cdSet = ssjava.getCd2lattice().keySet();
 103     for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
 104       ClassDescriptor cd = (ClassDescriptor) iterator.next();
 105       SSJavaLattice<String> lattice = ssjava.getCd2lattice().get(cd);
 106       Set<String> fieldLocNameSet = lattice.getKeySet();
 107
 108       for (Iterator iterator2 = fieldLocNameSet.iterator(); iterator2.hasNext();) {
 109         String fieldLocName = (String) iterator2.next();
 110         fieldLocName2cd.put(fieldLocName, cd);
 111       }
 112
 113     }
 114
 115   }
 116
 117   public boolean toAnalyzeIsEmpty() {
 118     if (deterministic) {
 119       return toanalyzeList.isEmpty();
 120     } else {
 121       return toanalyze.isEmpty();
 122     }
 123   }
 124
 125   public ClassDescriptor toAnalyzeNext() {
 126     if (deterministic) {
 127       return toanalyzeList.remove(0);
 128     } else {
 129       ClassDescriptor cd = toanalyze.iterator().next();
 130       toanalyze.remove(cd);
 131       return cd;
 132     }
 133   }
 134
 135   public void setupToAnalyze() {
 136     SymbolTable classtable = state.getClassSymbolTable();
 137     if (deterministic) {
 138       toanalyzeList.clear();
 139       toanalyzeList.addAll(classtable.getValueSet());
 140       Collections.sort(toanalyzeList, new Comparator<ClassDescriptor>() {
 141         public int compare(ClassDescriptor o1, ClassDescriptor o2) {
 142           return o1.getClassName().compareToIgnoreCase(o2.getClassName());
 143         }
 144       });
 145     } else {
 146       toanalyze.clear();
 147       toanalyze.addAll(classtable.getValueSet());
 148     }
 149   }
 150
 151   public void setupToAnalazeMethod(ClassDescriptor cd) {
 152
 153     SymbolTable methodtable = cd.getMethodTable();
 154     if (deterministic) {
 155       toanalyzeMethodList.clear();
 156       toanalyzeMethodList.addAll(methodtable.getValueSet());
 157       Collections.sort(toanalyzeMethodList, new Comparator<MethodDescriptor>() {
 158         public int compare(MethodDescriptor o1, MethodDescriptor o2) {
 159           return o1.getSymbol().compareToIgnoreCase(o2.getSymbol());
 160         }
 161       });
 162     } else {
 163       toanalyzeMethod.clear();
 164       toanalyzeMethod.addAll(methodtable.getValueSet());
 165     }
 166   }
 167
 168   public boolean toAnalyzeMethodIsEmpty() {
 169     if (deterministic) {
 170       return toanalyzeMethodList.isEmpty();
 171     } else {
 172       return toanalyzeMethod.isEmpty();
 173     }
 174   }
 175
 176   public MethodDescriptor toAnalyzeMethodNext() {
 177     if (deterministic) {
 178       return toanalyzeMethodList.remove(0);
 179     } else {
 180       MethodDescriptor md = toanalyzeMethod.iterator().next();
 181       toanalyzeMethod.remove(md);
 182       return md;
 183     }
 184   }
 185
 186   public void flowDownCheck() {
 187
 188     // phase 1 : checking declaration node and creating mapping of 'type
 189     // desciptor' & 'location'
 190     setupToAnalyze();
 191
 192     while (!toAnalyzeIsEmpty()) {
 193       ClassDescriptor cd = toAnalyzeNext();
 194
 195       if (ssjava.needToBeAnnoated(cd)) {
 196
 197         ClassDescriptor superDesc = cd.getSuperDesc();
 198
 199         if (superDesc != null && (!superDesc.getSymbol().equals("Object"))) {
 200           checkOrderingInheritance(superDesc, cd);
 201         }
 202
 203         checkDeclarationInClass(cd);
 204
 205         setupToAnalazeMethod(cd);
 206         while (!toAnalyzeMethodIsEmpty()) {
 207           MethodDescriptor md = toAnalyzeMethodNext();
 208           if (ssjava.needTobeAnnotated(md)) {
 209             checkDeclarationInMethodBody(cd, md);
 210           }
 211         }
 212
 213       }
 214
 215     }
 216
 217     // phase2 : checking assignments
 218     setupToAnalyze();
 219
 220     while (!toAnalyzeIsEmpty()) {
 221       ClassDescriptor cd = toAnalyzeNext();
 222
 223       setupToAnalazeMethod(cd);
 224       while (!toAnalyzeMethodIsEmpty()) {
 225         MethodDescriptor md = toAnalyzeMethodNext();
 226         if (ssjava.needTobeAnnotated(md)) {
 227           if (state.SSJAVADEBUG) {
 228             System.out.println("SSJAVA: Checking Flow-down Rules: " + md);
 229           }
 230           checkMethodBody(cd, md, null);
 231         }
 232       }
 233     }
 234
 235   }
 236
 237   private void checkOrderingInheritance(ClassDescriptor superCd, ClassDescriptor cd) {
 238     // here, we're going to check that sub class keeps same relative orderings
 239     // in respect to super class
 240
 241     SSJavaLattice<String> superLattice = ssjava.getClassLattice(superCd);
 242     SSJavaLattice<String> subLattice = ssjava.getClassLattice(cd);
 243
 244     if (superLattice != null) {
 245       // if super class doesn't define lattice, then we don't need to check its
 246       // subclass
 247       if (subLattice == null) {
 248         throw new Error("If a parent class '" + superCd
 249             + "' has a ordering lattice, its subclass '" + cd + "' should have one.");
 250       }
 251
 252       Set<Pair<String, String>> superPairSet = superLattice.getOrderingPairSet();
 253       Set<Pair<String, String>> subPairSet = subLattice.getOrderingPairSet();
 254
 255       for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) {
 256         Pair<String, String> pair = (Pair<String, String>) iterator.next();
 257
 258         if (!subPairSet.contains(pair)) {
 259           throw new Error("Subclass '" + cd + "' does not have the relative ordering '"
 260               + pair.getSecond() + " < " + pair.getFirst()
 261               + "' that is defined by its superclass '" + superCd + "'.");
 262         }
 263       }
 264     }
 265
 266     MethodLattice<String> superMethodDefaultLattice = ssjava.getMethodDefaultLattice(superCd);
 267     MethodLattice<String> subMethodDefaultLattice = ssjava.getMethodDefaultLattice(cd);
 268
 269     if (superMethodDefaultLattice != null) {
 270       if (subMethodDefaultLattice == null) {
 271         throw new Error("When a parent class '" + superCd
 272             + "' defines a default method lattice, its subclass '" + cd + "' should define one.");
 273       }
 274
 275       Set<Pair<String, String>> superPairSet = superMethodDefaultLattice.getOrderingPairSet();
 276       Set<Pair<String, String>> subPairSet = subMethodDefaultLattice.getOrderingPairSet();
 277
 278       for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) {
 279         Pair<String, String> pair = (Pair<String, String>) iterator.next();
 280
 281         if (!subPairSet.contains(pair)) {
 282           throw new Error("Subclass '" + cd + "' does not have the relative ordering '"
 283               + pair.getSecond() + " < " + pair.getFirst()
 284               + "' that is defined by its superclass '" + superCd
 285               + "' in the method default lattice.");
 286         }
 287       }
 288
 289     }
 290
 291   }
 292
 293   public Hashtable getMap() {
 294     return d2loc;
 295   }
 296
 297   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
 298     BlockNode bn = state.getMethodBody(md);
 299
 300     // first, check annotations on method parameters
 301     List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
 302     for (int i = 0; i < md.numParameters(); i++) {
 303       // process annotations on method parameters
 304       VarDescriptor vd = (VarDescriptor) md.getParameter(i);
 305       assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), null);
 306       paramList.add(d2loc.get(vd));
 307     }
 308     Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
 309
 310     CompositeLocation returnLocComp = null;
 311
 312     boolean hasReturnLocDeclaration = false;
 313     if (methodAnnotations != null) {
 314       for (int i = 0; i < methodAnnotations.size(); i++) {
 315         AnnotationDescriptor an = methodAnnotations.elementAt(i);
 316         if (an.getMarker().equals(ssjava.RETURNLOC)) {
 317           // this case, developer explicitly defines method lattice
 318           String returnLocDeclaration = an.getValue();
 319           returnLocComp = parseLocationDeclaration(md, null, returnLocDeclaration);
 320           hasReturnLocDeclaration = true;
 321         } else if (an.getMarker().equals(ssjava.THISLOC)) {
 322           String thisLoc = an.getValue();
 323           ssjava.getMethodLattice(md).setThisLoc(thisLoc);
 324         }
 325       }
 326     }
 327
 328     // second, check return location annotation
 329     if (!md.getReturnType().isVoid()) {
 330       if (!hasReturnLocDeclaration) {
 331         // if developer does not define method lattice
 332         // search return location in the method default lattice
 333         String rtrStr = ssjava.getMethodLattice(md).getReturnLoc();
 334         if (rtrStr != null) {
 335           returnLocComp = new CompositeLocation(new Location(md, rtrStr));
 336         }
 337       }
 338
 339       if (returnLocComp == null) {
 340         throw new Error("Return location is not specified for the method " + md + " at "
 341             + cd.getSourceFileName());
 342       }
 343
 344       md2ReturnLoc.put(md, returnLocComp);
 345
 346     }
 347
 348     if (!md.getReturnType().isVoid()) {
 349       MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
 350       String thisLocId = methodLattice.getThisLoc();
 351       if ((!md.isStatic()) && thisLocId == null) {
 352         throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
 353             + md.getClassDesc().getSourceFileName());
 354       }
 355       CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
 356       paramList.add(0, thisLoc);
 357       md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), md, paramList, md
 358           + " of " + cd.getSourceFileName()));
 359     }
 360
 361     // fourth, check declarations inside of method
 362
 363     checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
 364
 365   }
 366
 367   private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
 368     bn.getVarTable().setParent(nametable);
 369     for (int i = 0; i < bn.size(); i++) {
 370       BlockStatementNode bsn = bn.get(i);
 371       checkDeclarationInBlockStatementNode(md, bn.getVarTable(), bsn);
 372     }
 373   }
 374
 375   private void checkDeclarationInBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
 376       BlockStatementNode bsn) {
 377
 378     switch (bsn.kind()) {
 379     case Kind.SubBlockNode:
 380       checkDeclarationInSubBlockNode(md, nametable, (SubBlockNode) bsn);
 381       return;
 382
 383     case Kind.DeclarationNode:
 384       checkDeclarationNode(md, nametable, (DeclarationNode) bsn);
 385       break;
 386
 387     case Kind.LoopNode:
 388       checkDeclarationInLoopNode(md, nametable, (LoopNode) bsn);
 389       break;
 390
 391     case Kind.IfStatementNode:
 392       checkDeclarationInIfStatementNode(md, nametable, (IfStatementNode) bsn);
 393       return;
 394
 395     case Kind.SwitchStatementNode:
 396       checkDeclarationInSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn);
 397       return;
 398
 399     case Kind.SynchronizedNode:
 400       checkDeclarationInSynchronizedNode(md, nametable, (SynchronizedNode) bsn);
 401       return;
 402
 403     }
 404   }
 405
 406   private void checkDeclarationInSynchronizedNode(MethodDescriptor md, SymbolTable nametable,
 407       SynchronizedNode sbn) {
 408     checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode());
 409   }
 410
 411   private void checkDeclarationInSwitchStatementNode(MethodDescriptor md, SymbolTable nametable,
 412       SwitchStatementNode ssn) {
 413     BlockNode sbn = ssn.getSwitchBody();
 414     for (int i = 0; i < sbn.size(); i++) {
 415       SwitchBlockNode node = (SwitchBlockNode) sbn.get(i);
 416       checkDeclarationInBlockNode(md, nametable, node.getSwitchBlockStatement());
 417     }
 418   }
 419
 420   private void checkDeclarationInIfStatementNode(MethodDescriptor md, SymbolTable nametable,
 421       IfStatementNode isn) {
 422     checkDeclarationInBlockNode(md, nametable, isn.getTrueBlock());
 423     if (isn.getFalseBlock() != null)
 424       checkDeclarationInBlockNode(md, nametable, isn.getFalseBlock());
 425   }
 426
 427   private void checkDeclarationInLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln) {
 428
 429     if (ln.getType() == LoopNode.FORLOOP) {
 430       // check for loop case
 431       ClassDescriptor cd = md.getClassDesc();
 432       BlockNode bn = ln.getInitializer();
 433       for (int i = 0; i < bn.size(); i++) {
 434         BlockStatementNode bsn = bn.get(i);
 435         checkDeclarationInBlockStatementNode(md, nametable, bsn);
 436       }
 437     }
 438
 439     // check loop body
 440     checkDeclarationInBlockNode(md, nametable, ln.getBody());
 441   }
 442
 443   private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md,
 444       CompositeLocation constraints) {
 445     BlockNode bn = state.getMethodBody(md);
 446     checkLocationFromBlockNode(md, md.getParameterTable(), bn, constraints);
 447   }
 448
 449   private String generateErrorMessage(ClassDescriptor cd, TreeNode tn) {
 450     if (tn != null) {
 451       return cd.getSourceFileName() + "::" + tn.getNumLine();
 452     } else {
 453       return cd.getSourceFileName();
 454     }
 455
 456   }
 457
 458   private CompositeLocation checkLocationFromBlockNode(MethodDescriptor md, SymbolTable nametable,
 459       BlockNode bn, CompositeLocation constraint) {
 460
 461     bn.getVarTable().setParent(nametable);
 462     for (int i = 0; i < bn.size(); i++) {
 463       BlockStatementNode bsn = bn.get(i);
 464       checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn, constraint);
 465     }
 466     return new CompositeLocation();
 467
 468   }
 469
 470   private CompositeLocation checkLocationFromBlockStatementNode(MethodDescriptor md,
 471       SymbolTable nametable, BlockStatementNode bsn, CompositeLocation constraint) {
 472
 473     CompositeLocation compLoc = null;
 474     switch (bsn.kind()) {
 475     case Kind.BlockExpressionNode:
 476       compLoc =
 477           checkLocationFromBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn, constraint);
 478       break;
 479
 480     case Kind.DeclarationNode:
 481       compLoc = checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn, constraint);
 482       break;
 483
 484     case Kind.IfStatementNode:
 485       compLoc = checkLocationFromIfStatementNode(md, nametable, (IfStatementNode) bsn, constraint);
 486       break;
 487
 488     case Kind.LoopNode:
 489       compLoc = checkLocationFromLoopNode(md, nametable, (LoopNode) bsn, constraint);
 490       break;
 491
 492     case Kind.ReturnNode:
 493       compLoc = checkLocationFromReturnNode(md, nametable, (ReturnNode) bsn, constraint);
 494       break;
 495
 496     case Kind.SubBlockNode:
 497       compLoc = checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn, constraint);
 498       break;
 499
 500     case Kind.ContinueBreakNode:
 501       compLoc = new CompositeLocation();
 502       break;
 503
 504     case Kind.SwitchStatementNode:
 505       compLoc =
 506           checkLocationFromSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn, constraint);
 507
 508     }
 509     return compLoc;
 510   }
 511
 512   private CompositeLocation checkLocationFromSwitchStatementNode(MethodDescriptor md,
 513       SymbolTable nametable, SwitchStatementNode ssn, CompositeLocation constraint) {
 514
 515     ClassDescriptor cd = md.getClassDesc();
 516     CompositeLocation condLoc =
 517         checkLocationFromExpressionNode(md, nametable, ssn.getCondition(), new CompositeLocation(),
 518             constraint, false);
 519     BlockNode sbn = ssn.getSwitchBody();
 520
 521     constraint = generateNewConstraint(constraint, condLoc);
 522
 523     for (int i = 0; i < sbn.size(); i++) {
 524       checkLocationFromSwitchBlockNode(md, nametable, (SwitchBlockNode) sbn.get(i), constraint);
 525     }
 526     return new CompositeLocation();
 527   }
 528
 529   private CompositeLocation checkLocationFromSwitchBlockNode(MethodDescriptor md,
 530       SymbolTable nametable, SwitchBlockNode sbn, CompositeLocation constraint) {
 531
 532     CompositeLocation blockLoc =
 533         checkLocationFromBlockNode(md, nametable, sbn.getSwitchBlockStatement(), constraint);
 534
 535     return blockLoc;
 536
 537   }
 538
 539   private CompositeLocation checkLocationFromReturnNode(MethodDescriptor md, SymbolTable nametable,
 540       ReturnNode rn, CompositeLocation constraint) {
 541
 542     ExpressionNode returnExp = rn.getReturnExpression();
 543
 544     CompositeLocation returnValueLoc;
 545     if (returnExp != null) {
 546       returnValueLoc =
 547           checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation(),
 548               constraint, false);
 549
 550       // System.out.println("# RETURN VALUE LOC=" + returnValueLoc +
 551       // " with constraint=" + constraint);
 552
 553       // TODO: do we need to check here?
 554       // if this return statement is inside branch, return value has an implicit
 555       // flow from conditional location
 556       // if (constraint != null) {
 557       // Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
 558       // inputGLB.add(returnValueLoc);
 559       // inputGLB.add(constraint);
 560       // returnValueLoc =
 561       // CompositeLattice.calculateGLB(inputGLB,
 562       // generateErrorMessage(md.getClassDesc(), rn));
 563       // }
 564
 565       // check if return value is equal or higher than RETRUNLOC of method
 566       // declaration annotation
 567       CompositeLocation declaredReturnLoc = md2ReturnLoc.get(md);
 568
 569       int compareResult =
 570           CompositeLattice.compare(returnValueLoc, declaredReturnLoc, false,
 571               generateErrorMessage(md.getClassDesc(), rn));
 572
 573       if (compareResult == ComparisonResult.LESS || compareResult == ComparisonResult.INCOMPARABLE) {
 574         throw new Error(
 575             "Return value location is not equal or higher than the declaraed return location at "
 576                 + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine());
 577       }
 578     }
 579
 580     return new CompositeLocation();
 581   }
 582
 583   private boolean hasOnlyLiteralValue(ExpressionNode en) {
 584     if (en.kind() == Kind.LiteralNode) {
 585       return true;
 586     } else {
 587       return false;
 588     }
 589   }
 590
 591   private CompositeLocation checkLocationFromLoopNode(MethodDescriptor md, SymbolTable nametable,
 592       LoopNode ln, CompositeLocation constraint) {
 593
 594     ClassDescriptor cd = md.getClassDesc();
 595     if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) {
 596
 597       CompositeLocation condLoc =
 598           checkLocationFromExpressionNode(md, nametable, ln.getCondition(),
 599               new CompositeLocation(), constraint, false);
 600       // addLocationType(ln.getCondition().getType(), (condLoc));
 601
 602       constraint = generateNewConstraint(constraint, condLoc);
 603       checkLocationFromBlockNode(md, nametable, ln.getBody(), constraint);
 604
 605       return new CompositeLocation();
 606
 607     } else {
 608       // check 'for loop' case
 609       BlockNode bn = ln.getInitializer();
 610       // need to check initialization node
 611       checkLocationFromBlockNode(md, bn.getVarTable(), bn, constraint);
 612       bn.getVarTable().setParent(nametable);
 613
 614       // calculate glb location of condition and update statements
 615       CompositeLocation condLoc =
 616           checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(),
 617               new CompositeLocation(), constraint, false);
 618       // addLocationType(ln.getCondition().getType(), condLoc);
 619
 620       constraint = generateNewConstraint(constraint, condLoc);
 621
 622       checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate(), constraint);
 623       checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody(), constraint);
 624
 625       return new CompositeLocation();
 626
 627     }
 628
 629   }
 630
 631   private CompositeLocation checkLocationFromSubBlockNode(MethodDescriptor md,
 632       SymbolTable nametable, SubBlockNode sbn, CompositeLocation constraint) {
 633     CompositeLocation compLoc =
 634         checkLocationFromBlockNode(md, nametable, sbn.getBlockNode(), constraint);
 635     return compLoc;
 636   }
 637
 638   private CompositeLocation generateNewConstraint(CompositeLocation currentCon,
 639       CompositeLocation newCon) {
 640
 641     if (currentCon == null) {
 642       return newCon;
 643     } else {
 644       // compute GLB of current constraint and new constraint
 645       Set<CompositeLocation> inputSet = new HashSet<CompositeLocation>();
 646       inputSet.add(currentCon);
 647       inputSet.add(newCon);
 648       return CompositeLattice.calculateGLB(inputSet, "");
 649     }
 650
 651   }
 652
 653   private CompositeLocation checkLocationFromIfStatementNode(MethodDescriptor md,
 654       SymbolTable nametable, IfStatementNode isn, CompositeLocation constraint) {
 655
 656     CompositeLocation condLoc =
 657         checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation(),
 658             constraint, false);
 659
 660     // addLocationType(isn.getCondition().getType(), condLoc);
 661
 662     constraint = generateNewConstraint(constraint, condLoc);
 663     checkLocationFromBlockNode(md, nametable, isn.getTrueBlock(), constraint);
 664
 665     if (isn.getFalseBlock() != null) {
 666       checkLocationFromBlockNode(md, nametable, isn.getFalseBlock(), constraint);
 667     }
 668
 669     return new CompositeLocation();
 670   }
 671
 672   private void checkOwnership(MethodDescriptor md, TreeNode tn, ExpressionNode srcExpNode) {
 673
 674     if (srcExpNode.kind() == Kind.NameNode || srcExpNode.kind() == Kind.FieldAccessNode) {
 675       if (srcExpNode.getType().isPtr() && !srcExpNode.getType().isNull()) {
 676         // first, check the linear type
 677         // RHS reference should be owned by the current method
 678         FieldDescriptor fd = getFieldDescriptorFromExpressionNode(srcExpNode);
 679         boolean isOwned;
 680         if (fd == null) {
 681           // local var case
 682           isOwned = ((SSJavaType) srcExpNode.getType().getExtension()).isOwned();
 683         } else {
 684           // field case
 685           isOwned = ssjava.isOwnedByMethod(md, fd);
 686         }
 687         if (!isOwned) {
 688           throw new Error(
 689               "It is not allowed to create the reference alias from the reference not owned by the method at "
 690                   + generateErrorMessage(md.getClassDesc(), tn));
 691         }
 692
 693       }
 694     }
 695
 696   }
 697
 698   private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md,
 699       SymbolTable nametable, DeclarationNode dn, CompositeLocation constraint) {
 700
 701     VarDescriptor vd = dn.getVarDescriptor();
 702
 703     CompositeLocation destLoc = d2loc.get(vd);
 704
 705     if (dn.getExpression() != null) {
 706
 707       checkOwnership(md, dn, dn.getExpression());
 708
 709       CompositeLocation expressionLoc =
 710           checkLocationFromExpressionNode(md, nametable, dn.getExpression(),
 711               new CompositeLocation(), constraint, false);
 712       // addTypeLocation(dn.getExpression().getType(), expressionLoc);
 713
 714       if (expressionLoc != null) {
 715
 716         // checking location order
 717         if (!CompositeLattice.isGreaterThan(expressionLoc, destLoc,
 718             generateErrorMessage(md.getClassDesc(), dn))) {
 719           throw new Error("The value flow from " + expressionLoc + " to " + destLoc
 720               + " does not respect location hierarchy on the assignment " + dn.printNode(0)
 721               + " at " + md.getClassDesc().getSourceFileName() + "::" + dn.getNumLine());
 722         }
 723       }
 724       return expressionLoc;
 725
 726     } else {
 727
 728       return new CompositeLocation();
 729
 730     }
 731
 732   }
 733
 734   private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable,
 735       SubBlockNode sbn) {
 736     checkDeclarationInBlockNode(md, nametable.getParent(), sbn.getBlockNode());
 737   }
 738
 739   private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md,
 740       SymbolTable nametable, BlockExpressionNode ben, CompositeLocation constraint) {
 741     CompositeLocation compLoc =
 742         checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null, constraint, false);
 743     // addTypeLocation(ben.getExpression().getType(), compLoc);
 744     return compLoc;
 745   }
 746
 747   private CompositeLocation checkLocationFromExpressionNode(MethodDescriptor md,
 748       SymbolTable nametable, ExpressionNode en, CompositeLocation loc,
 749       CompositeLocation constraint, boolean isLHS) {
 750
 751     CompositeLocation compLoc = null;
 752     switch (en.kind()) {
 753
 754     case Kind.AssignmentNode:
 755       compLoc =
 756           checkLocationFromAssignmentNode(md, nametable, (AssignmentNode) en, loc, constraint);
 757       break;
 758
 759     case Kind.FieldAccessNode:
 760       compLoc =
 761           checkLocationFromFieldAccessNode(md, nametable, (FieldAccessNode) en, loc, constraint);
 762       break;
 763
 764     case Kind.NameNode:
 765       compLoc = checkLocationFromNameNode(md, nametable, (NameNode) en, loc, constraint);
 766       break;
 767
 768     case Kind.OpNode:
 769       compLoc = checkLocationFromOpNode(md, nametable, (OpNode) en, constraint);
 770       break;
 771
 772     case Kind.CreateObjectNode:
 773       compLoc = checkLocationFromCreateObjectNode(md, nametable, (CreateObjectNode) en);
 774       break;
 775
 776     case Kind.ArrayAccessNode:
 777       compLoc =
 778           checkLocationFromArrayAccessNode(md, nametable, (ArrayAccessNode) en, constraint, isLHS);
 779       break;
 780
 781     case Kind.LiteralNode:
 782       compLoc = checkLocationFromLiteralNode(md, nametable, (LiteralNode) en, loc);
 783       break;
 784
 785     case Kind.MethodInvokeNode:
 786       compLoc =
 787           checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en, loc, constraint);
 788       break;
 789
 790     case Kind.TertiaryNode:
 791       compLoc = checkLocationFromTertiaryNode(md, nametable, (TertiaryNode) en, constraint);
 792       break;
 793
 794     case Kind.CastNode:
 795       compLoc = checkLocationFromCastNode(md, nametable, (CastNode) en, constraint);
 796       break;
 797
 798     // case Kind.InstanceOfNode:
 799     // checkInstanceOfNode(md, nametable, (InstanceOfNode) en, td);
 800     // return null;
 801
 802     // case Kind.ArrayInitializerNode:
 803     // checkArrayInitializerNode(md, nametable, (ArrayInitializerNode) en,
 804     // td);
 805     // return null;
 806
 807     // case Kind.ClassTypeNode:
 808     // checkClassTypeNode(md, nametable, (ClassTypeNode) en, td);
 809     // return null;
 810
 811     // case Kind.OffsetNode:
 812     // checkOffsetNode(md, nametable, (OffsetNode)en, td);
 813     // return null;
 814
 815     default:
 816       return null;
 817
 818     }
 819     // addTypeLocation(en.getType(), compLoc);
 820     return compLoc;
 821
 822   }
 823
 824   private CompositeLocation checkLocationFromCastNode(MethodDescriptor md, SymbolTable nametable,
 825       CastNode cn, CompositeLocation constraint) {
 826
 827     ExpressionNode en = cn.getExpression();
 828     return checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
 829         false);
 830
 831   }
 832
 833   private CompositeLocation checkLocationFromTertiaryNode(MethodDescriptor md,
 834       SymbolTable nametable, TertiaryNode tn, CompositeLocation constraint) {
 835     ClassDescriptor cd = md.getClassDesc();
 836
 837     CompositeLocation condLoc =
 838         checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation(),
 839             constraint, false);
 840     // addLocationType(tn.getCond().getType(), condLoc);
 841     CompositeLocation trueLoc =
 842         checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation(),
 843             constraint, false);
 844     // addLocationType(tn.getTrueExpr().getType(), trueLoc);
 845     CompositeLocation falseLoc =
 846         checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation(),
 847             constraint, false);
 848     // addLocationType(tn.getFalseExpr().getType(), falseLoc);
 849
 850     // locations from true/false branches can be TOP when there are only literal
 851     // values
 852     // in this case, we don't need to check flow down rule!
 853
 854     // System.out.println("\n#tertiary cond=" + tn.getCond().printNode(0) +
 855     // " Loc=" + condLoc);
 856     // System.out.println("# true=" + tn.getTrueExpr().printNode(0) + " Loc=" +
 857     // trueLoc);
 858     // System.out.println("# false=" + tn.getFalseExpr().printNode(0) + " Loc="
 859     // + falseLoc);
 860
 861     // check if condLoc is higher than trueLoc & falseLoc
 862     if (!trueLoc.get(0).isTop()
 863         && !CompositeLattice.isGreaterThan(condLoc, trueLoc, generateErrorMessage(cd, tn))) {
 864       throw new Error(
 865           "The location of the condition expression is lower than the true expression at "
 866               + cd.getSourceFileName() + ":" + tn.getCond().getNumLine());
 867     }
 868
 869     if (!falseLoc.get(0).isTop()
 870         && !CompositeLattice.isGreaterThan(condLoc, falseLoc,
 871             generateErrorMessage(cd, tn.getCond()))) {
 872       throw new Error(
 873           "The location of the condition expression is lower than the false expression at "
 874               + cd.getSourceFileName() + ":" + tn.getCond().getNumLine());
 875     }
 876
 877     // then, return glb of trueLoc & falseLoc
 878     Set<CompositeLocation> glbInputSet = new HashSet<CompositeLocation>();
 879     glbInputSet.add(trueLoc);
 880     glbInputSet.add(falseLoc);
 881
 882     if (glbInputSet.size() == 1) {
 883       return trueLoc;
 884     } else {
 885       return CompositeLattice.calculateGLB(glbInputSet, generateErrorMessage(cd, tn));
 886     }
 887
 888   }
 889
 890   private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md,
 891       SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc,
 892       CompositeLocation constraint) {
 893
 894     ClassDescriptor cd = md.getClassDesc();
 895     MethodDescriptor calleeMD = min.getMethod();
 896
 897     NameDescriptor baseName = min.getBaseName();
 898     boolean isSystemout = false;
 899     if (baseName != null) {
 900       isSystemout = baseName.getSymbol().equals("System.out");
 901     }
 902
 903     if (!ssjava.isSSJavaUtil(calleeMD.getClassDesc()) && !ssjava.isTrustMethod(calleeMD)
 904         && !calleeMD.getModifiers().isNative() && !isSystemout) {
 905
 906       CompositeLocation baseLocation = null;
 907       if (min.getExpression() != null) {
 908         baseLocation =
 909             checkLocationFromExpressionNode(md, nametable, min.getExpression(),
 910                 new CompositeLocation(), constraint, false);
 911       } else {
 912         if (min.getMethod().isStatic()) {
 913           String globalLocId = ssjava.getMethodLattice(md).getGlobalLoc();
 914           if (globalLocId == null) {
 915             throw new Error("Method lattice does not define global variable location at "
 916                 + generateErrorMessage(md.getClassDesc(), min));
 917           }
 918           baseLocation = new CompositeLocation(new Location(md, globalLocId));
 919         } else {
 920           String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
 921           baseLocation = new CompositeLocation(new Location(md, thisLocId));
 922         }
 923       }
 924
 925       // System.out.println("\n#checkLocationFromMethodInvokeNode=" +
 926       // min.printNode(0)
 927       // + " baseLocation=" + baseLocation + " constraint=" + constraint);
 928
 929       if (constraint != null) {
 930         int compareResult =
 931             CompositeLattice.compare(constraint, baseLocation, true, generateErrorMessage(cd, min));
 932         if (compareResult != ComparisonResult.GREATER) {
 933           // if the current constraint is higher than method's THIS location
 934           // no need to check constraints!
 935           CompositeLocation calleeConstraint =
 936               translateCallerLocToCalleeLoc(calleeMD, baseLocation, constraint);
 937           // System.out.println("check method body for constraint:" + calleeMD +
 938           // " calleeConstraint="
 939           // + calleeConstraint);
 940           checkMethodBody(calleeMD.getClassDesc(), calleeMD, calleeConstraint);
 941         }
 942       }
 943
 944       checkCalleeConstraints(md, nametable, min, baseLocation, constraint);
 945
 946       // checkCallerArgumentLocationConstraints(md, nametable, min,
 947       // baseLocation, constraint);
 948
 949       if (!min.getMethod().getReturnType().isVoid()) {
 950         // If method has a return value, compute the highest possible return
 951         // location in the caller's perspective
 952         CompositeLocation ceilingLoc =
 953             computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint);
 954         return ceilingLoc;
 955       }
 956     }
 957
 958     return new CompositeLocation(Location.createTopLocation(md));
 959
 960   }
 961
 962   private CompositeLocation translateCallerLocToCalleeLoc(MethodDescriptor calleeMD,
 963       CompositeLocation calleeBaseLoc, CompositeLocation constraint) {
 964
 965     CompositeLocation calleeConstraint = new CompositeLocation();
 966
 967     // if (constraint.startsWith(calleeBaseLoc)) {
 968     // if the first part of constraint loc is matched with callee base loc
 969     Location thisLoc = new Location(calleeMD, ssjava.getMethodLattice(calleeMD).getThisLoc());
 970     calleeConstraint.addLocation(thisLoc);
 971     for (int i = calleeBaseLoc.getSize(); i < constraint.getSize(); i++) {
 972       calleeConstraint.addLocation(constraint.get(i));
 973     }
 974
 975     // }
 976
 977     return calleeConstraint;
 978   }
 979
 980   private void checkCallerArgumentLocationConstraints(MethodDescriptor md, SymbolTable nametable,
 981       MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
 982     // if parameter location consists of THIS and FIELD location,
 983     // caller should pass an argument that is comparable to the declared
 984     // parameter location
 985     // and is not lower than the declared parameter location in the field
 986     // lattice.
 987
 988     MethodDescriptor calleemd = min.getMethod();
 989
 990     List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
 991     List<CompositeLocation> calleeParamList = new ArrayList<CompositeLocation>();
 992
 993     MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
 994     Location calleeThisLoc = new Location(calleemd, calleeLattice.getThisLoc());
 995
 996     for (int i = 0; i < min.numArgs(); i++) {
 997       ExpressionNode en = min.getArg(i);
 998       CompositeLocation callerArgLoc =
 999           checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
1000               false);
1001       callerArgList.add(callerArgLoc);
1002     }
1003
1004     // setup callee params set
1005     for (int i = 0; i < calleemd.numParameters(); i++) {
1006       VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
1007       CompositeLocation calleeLoc = d2loc.get(calleevd);
1008       calleeParamList.add(calleeLoc);
1009     }
1010
1011     String errorMsg = generateErrorMessage(md.getClassDesc(), min);
1012
1013     // System.out.println("checkCallerArgumentLocationConstraints=" +
1014     // min.printNode(0));
1015     // System.out.println("base location=" + callerBaseLoc + " constraint=" +
1016     // constraint);
1017
1018     for (int i = 0; i < calleeParamList.size(); i++) {
1019       CompositeLocation calleeParamLoc = calleeParamList.get(i);
1020       if (calleeParamLoc.get(0).equals(calleeThisLoc) && calleeParamLoc.getSize() > 1) {
1021
1022         // callee parameter location has field information
1023         CompositeLocation callerArgLoc = callerArgList.get(i);
1024
1025         CompositeLocation paramLocation =
1026             translateCalleeParamLocToCaller(md, calleeParamLoc, callerBaseLoc, errorMsg);
1027
1028         Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
1029         if (constraint != null) {
1030           inputGLBSet.add(callerArgLoc);
1031           inputGLBSet.add(constraint);
1032           callerArgLoc =
1033               CompositeLattice.calculateGLB(inputGLBSet,
1034                   generateErrorMessage(md.getClassDesc(), min));
1035         }
1036
1037         if (!CompositeLattice.isGreaterThan(callerArgLoc, paramLocation, errorMsg)) {
1038           throw new Error("Caller argument '" + min.getArg(i).printNode(0) + " : " + callerArgLoc
1039               + "' should be higher than corresponding callee's parameter : " + paramLocation
1040               + " at " + errorMsg);
1041         }
1042
1043       }
1044     }
1045
1046   }
1047
1048   private CompositeLocation translateCalleeParamLocToCaller(MethodDescriptor md,
1049       CompositeLocation calleeParamLoc, CompositeLocation callerBaseLocation, String errorMsg) {
1050
1051     CompositeLocation translate = new CompositeLocation();
1052
1053     for (int i = 0; i < callerBaseLocation.getSize(); i++) {
1054       translate.addLocation(callerBaseLocation.get(i));
1055     }
1056
1057     for (int i = 1; i < calleeParamLoc.getSize(); i++) {
1058       translate.addLocation(calleeParamLoc.get(i));
1059     }
1060
1061     // System.out.println("TRANSLATED=" + translate + " from calleeParamLoc=" +
1062     // calleeParamLoc);
1063
1064     return translate;
1065   }
1066
1067   private CompositeLocation computeCeilingLocationForCaller(MethodDescriptor md,
1068       SymbolTable nametable, MethodInvokeNode min, CompositeLocation baseLocation,
1069       CompositeLocation constraint) {
1070     List<CompositeLocation> argList = new ArrayList<CompositeLocation>();
1071
1072     // by default, method has a THIS parameter
1073     argList.add(baseLocation);
1074
1075     for (int i = 0; i < min.numArgs(); i++) {
1076       ExpressionNode en = min.getArg(i);
1077       CompositeLocation callerArg =
1078           checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
1079               false);
1080       argList.add(callerArg);
1081     }
1082
1083     // System.out.println("\n## computeReturnLocation=" + min.getMethod() +
1084     // " argList=" + argList);
1085     CompositeLocation ceilLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
1086     // System.out.println("## ReturnLocation=" + ceilLoc);
1087
1088     return ceilLoc;
1089
1090   }
1091
1092   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
1093       MethodInvokeNode min, CompositeLocation callerBaseLoc, CompositeLocation constraint) {
1094
1095     // System.out.println("checkCalleeConstraints=" + min.printNode(0));
1096
1097     MethodDescriptor calleemd = min.getMethod();
1098
1099     MethodLattice<String> calleeLattice = ssjava.getMethodLattice(calleemd);
1100     CompositeLocation calleeThisLoc =
1101         new CompositeLocation(new Location(calleemd, calleeLattice.getThisLoc()));
1102
1103     List<CompositeLocation> callerArgList = new ArrayList<CompositeLocation>();
1104     List<CompositeLocation> calleeParamList = new ArrayList<CompositeLocation>();
1105
1106     if (min.numArgs() > 0) {
1107       // caller needs to guarantee that it passes arguments in regarding to
1108       // callee's hierarchy
1109
1110       // setup caller args set
1111       // first, add caller's base(this) location
1112       callerArgList.add(callerBaseLoc);
1113       // second, add caller's arguments
1114       for (int i = 0; i < min.numArgs(); i++) {
1115         ExpressionNode en = min.getArg(i);
1116         CompositeLocation callerArgLoc =
1117             checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
1118                 false);
1119         callerArgList.add(callerArgLoc);
1120       }
1121
1122       // setup callee params set
1123       // first, add callee's this location
1124       calleeParamList.add(calleeThisLoc);
1125       // second, add callee's parameters
1126       for (int i = 0; i < calleemd.numParameters(); i++) {
1127         VarDescriptor calleevd = (VarDescriptor) calleemd.getParameter(i);
1128         CompositeLocation calleeLoc = d2loc.get(calleevd);
1129         // System.out.println("calleevd=" + calleevd + " loc=" + calleeLoc);
1130         calleeParamList.add(calleeLoc);
1131       }
1132
1133       // here, check if ordering relations among caller's args respect
1134       // ordering relations in-between callee's args
1135       CHECK: for (int i = 0; i < calleeParamList.size(); i++) {
1136         CompositeLocation calleeLoc1 = calleeParamList.get(i);
1137         CompositeLocation callerLoc1 = callerArgList.get(i);
1138
1139         for (int j = 0; j < calleeParamList.size(); j++) {
1140           if (i != j) {
1141             CompositeLocation calleeLoc2 = calleeParamList.get(j);
1142             CompositeLocation callerLoc2 = callerArgList.get(j);
1143
1144             if (callerLoc1.get(callerLoc1.getSize() - 1).isTop()
1145                 || callerLoc2.get(callerLoc2.getSize() - 1).isTop()) {
1146               continue CHECK;
1147             }
1148
1149             // System.out.println("calleeLoc1=" + calleeLoc1);
1150             // System.out.println("calleeLoc2=" + calleeLoc2 +
1151             // "calleeParamList=" + calleeParamList);
1152
1153             int callerResult =
1154                 CompositeLattice.compare(callerLoc1, callerLoc2, true,
1155                     generateErrorMessage(md.getClassDesc(), min));
1156             // System.out.println("callerResult=" + callerResult);
1157             int calleeResult =
1158                 CompositeLattice.compare(calleeLoc1, calleeLoc2, true,
1159                     generateErrorMessage(md.getClassDesc(), min));
1160             // System.out.println("calleeResult=" + calleeResult);
1161
1162             if (callerResult == ComparisonResult.EQUAL) {
1163               if (ssjava.isSharedLocation(callerLoc1.get(callerLoc1.getSize() - 1))
1164                   && ssjava.isSharedLocation(callerLoc2.get(callerLoc2.getSize() - 1))) {
1165                 // if both of them are shared locations, promote them to
1166                 // "GREATER relation"
1167                 callerResult = ComparisonResult.GREATER;
1168               }
1169             }
1170
1171             if (calleeResult == ComparisonResult.GREATER
1172                 && callerResult != ComparisonResult.GREATER) {
1173               // If calleeLoc1 is higher than calleeLoc2
1174               // then, caller should have same ordering relation in-bet
1175               // callerLoc1 & callerLoc2
1176
1177               String paramName1, paramName2;
1178
1179               if (i == 0) {
1180                 paramName1 = "'THIS'";
1181               } else {
1182                 paramName1 = "'parameter " + calleemd.getParamName(i - 1) + "'";
1183               }
1184
1185               if (j == 0) {
1186                 paramName2 = "'THIS'";
1187               } else {
1188                 paramName2 = "'parameter " + calleemd.getParamName(j - 1) + "'";
1189               }
1190
1191               throw new Error(
1192                   "Caller doesn't respect an ordering relation among method arguments: callee expects that "
1193                       + paramName1 + " should be higher than " + paramName2 + " in " + calleemd
1194                       + " at " + md.getClassDesc().getSourceFileName() + ":" + min.getNumLine());
1195             }
1196           }
1197
1198         }
1199       }
1200
1201     }
1202
1203   }
1204
1205   private CompositeLocation checkLocationFromArrayAccessNode(MethodDescriptor md,
1206       SymbolTable nametable, ArrayAccessNode aan, CompositeLocation constraint, boolean isLHS) {
1207
1208     ClassDescriptor cd = md.getClassDesc();
1209
1210     CompositeLocation arrayLoc =
1211         checkLocationFromExpressionNode(md, nametable, aan.getExpression(),
1212             new CompositeLocation(), constraint, isLHS);
1213
1214     // addTypeLocation(aan.getExpression().getType(), arrayLoc);
1215     CompositeLocation indexLoc =
1216         checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation(),
1217             constraint, isLHS);
1218     // addTypeLocation(aan.getIndex().getType(), indexLoc);
1219
1220     if (isLHS) {
1221       if (!CompositeLattice.isGreaterThan(indexLoc, arrayLoc, generateErrorMessage(cd, aan))) {
1222         throw new Error("Array index value is not higher than array location at "
1223             + generateErrorMessage(cd, aan));
1224       }
1225       return arrayLoc;
1226     } else {
1227       Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
1228       inputGLB.add(arrayLoc);
1229       inputGLB.add(indexLoc);
1230       return CompositeLattice.calculateGLB(inputGLB, generateErrorMessage(cd, aan));
1231     }
1232
1233   }
1234
1235   private CompositeLocation checkLocationFromCreateObjectNode(MethodDescriptor md,
1236       SymbolTable nametable, CreateObjectNode con) {
1237
1238     ClassDescriptor cd = md.getClassDesc();
1239
1240     CompositeLocation compLoc = new CompositeLocation();
1241     compLoc.addLocation(Location.createTopLocation(md));
1242     return compLoc;
1243
1244   }
1245
1246   private CompositeLocation checkLocationFromOpNode(MethodDescriptor md, SymbolTable nametable,
1247       OpNode on, CompositeLocation constraint) {
1248
1249     ClassDescriptor cd = md.getClassDesc();
1250     CompositeLocation leftLoc = new CompositeLocation();
1251     leftLoc =
1252         checkLocationFromExpressionNode(md, nametable, on.getLeft(), leftLoc, constraint, false);
1253     // addTypeLocation(on.getLeft().getType(), leftLoc);
1254
1255     CompositeLocation rightLoc = new CompositeLocation();
1256     if (on.getRight() != null) {
1257       rightLoc =
1258           checkLocationFromExpressionNode(md, nametable, on.getRight(), rightLoc, constraint, false);
1259       // addTypeLocation(on.getRight().getType(), rightLoc);
1260     }
1261
1262     // System.out.println("\n# OP NODE=" + on.printNode(0));
1263     // System.out.println("# left loc=" + leftLoc + " from " +
1264     // on.getLeft().getClass());
1265     // if (on.getRight() != null) {
1266     // System.out.println("# right loc=" + rightLoc + " from " +
1267     // on.getRight().getClass());
1268     // }
1269
1270     Operation op = on.getOp();
1271
1272     switch (op.getOp()) {
1273
1274     case Operation.UNARYPLUS:
1275     case Operation.UNARYMINUS:
1276     case Operation.LOGIC_NOT:
1277       // single operand
1278       return leftLoc;
1279
1280     case Operation.LOGIC_OR:
1281     case Operation.LOGIC_AND:
1282     case Operation.COMP:
1283     case Operation.BIT_OR:
1284     case Operation.BIT_XOR:
1285     case Operation.BIT_AND:
1286     case Operation.ISAVAILABLE:
1287     case Operation.EQUAL:
1288     case Operation.NOTEQUAL:
1289     case Operation.LT:
1290     case Operation.GT:
1291     case Operation.LTE:
1292     case Operation.GTE:
1293     case Operation.ADD:
1294     case Operation.SUB:
1295     case Operation.MULT:
1296     case Operation.DIV:
1297     case Operation.MOD:
1298     case Operation.LEFTSHIFT:
1299     case Operation.RIGHTSHIFT:
1300     case Operation.URIGHTSHIFT:
1301
1302       Set<CompositeLocation> inputSet = new HashSet<CompositeLocation>();
1303       inputSet.add(leftLoc);
1304       inputSet.add(rightLoc);
1305       CompositeLocation glbCompLoc =
1306           CompositeLattice.calculateGLB(inputSet, generateErrorMessage(cd, on));
1307       return glbCompLoc;
1308
1309     default:
1310       throw new Error(op.toString());
1311     }
1312
1313   }
1314
1315   private CompositeLocation checkLocationFromLiteralNode(MethodDescriptor md,
1316       SymbolTable nametable, LiteralNode en, CompositeLocation loc) {
1317
1318     // literal value has the top location so that value can be flowed into any
1319     // location
1320     Location literalLoc = Location.createTopLocation(md);
1321     loc.addLocation(literalLoc);
1322     return loc;
1323
1324   }
1325
1326   private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable,
1327       NameNode nn, CompositeLocation loc, CompositeLocation constraint) {
1328
1329     NameDescriptor nd = nn.getName();
1330     if (nd.getBase() != null) {
1331       loc =
1332           checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc, constraint, false);
1333     } else {
1334       String varname = nd.toString();
1335       if (varname.equals("this")) {
1336         // 'this' itself!
1337         MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
1338         String thisLocId = methodLattice.getThisLoc();
1339         if (thisLocId == null) {
1340           throw new Error("The location for 'this' is not defined at "
1341               + md.getClassDesc().getSourceFileName() + "::" + nn.getNumLine());
1342         }
1343         Location locElement = new Location(md, thisLocId);
1344         loc.addLocation(locElement);
1345         return loc;
1346
1347       }
1348
1349       Descriptor d = (Descriptor) nametable.get(varname);
1350
1351       // CompositeLocation localLoc = null;
1352       if (d instanceof VarDescriptor) {
1353         VarDescriptor vd = (VarDescriptor) d;
1354         // localLoc = d2loc.get(vd);
1355         // the type of var descriptor has a composite location!
1356         loc = ((SSJavaType) vd.getType().getExtension()).getCompLoc().clone();
1357       } else if (d instanceof FieldDescriptor) {
1358         // the type of field descriptor has a location!
1359         FieldDescriptor fd = (FieldDescriptor) d;
1360         if (fd.isStatic()) {
1361           if (fd.isFinal()) {
1362             // if it is 'static final', the location has TOP since no one can
1363             // change its value
1364             loc.addLocation(Location.createTopLocation(md));
1365             return loc;
1366           } else {
1367             // if 'static', the location has pre-assigned global loc
1368             MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
1369             String globalLocId = localLattice.getGlobalLoc();
1370             if (globalLocId == null) {
1371               throw new Error("Global location element is not defined in the method " + md);
1372             }
1373             Location globalLoc = new Location(md, globalLocId);
1374
1375             loc.addLocation(globalLoc);
1376           }
1377         } else {
1378           // the location of field access starts from this, followed by field
1379           // location
1380           MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
1381           Location thisLoc = new Location(md, localLattice.getThisLoc());
1382           loc.addLocation(thisLoc);
1383         }
1384
1385         Location fieldLoc = (Location) fd.getType().getExtension();
1386         loc.addLocation(fieldLoc);
1387       } else if (d == null) {
1388         // access static field
1389         FieldDescriptor fd = nn.getField();
1390
1391         MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
1392         String globalLocId = localLattice.getGlobalLoc();
1393         if (globalLocId == null) {
1394           throw new Error("Method lattice does not define global variable location at "
1395               + generateErrorMessage(md.getClassDesc(), nn));
1396         }
1397         loc.addLocation(new Location(md, globalLocId));
1398
1399         Location fieldLoc = (Location) fd.getType().getExtension();
1400         loc.addLocation(fieldLoc);
1401
1402         return loc;
1403
1404       }
1405     }
1406     return loc;
1407   }
1408
1409   private CompositeLocation checkLocationFromFieldAccessNode(MethodDescriptor md,
1410       SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc,
1411       CompositeLocation constraint) {
1412
1413     ExpressionNode left = fan.getExpression();
1414     TypeDescriptor ltd = left.getType();
1415
1416     FieldDescriptor fd = fan.getField();
1417
1418     String varName = null;
1419     if (left.kind() == Kind.NameNode) {
1420       NameDescriptor nd = ((NameNode) left).getName();
1421       varName = nd.toString();
1422     }
1423
1424     if (ltd.isClassNameRef() || (varName != null && varName.equals("this"))) {
1425       // using a class name directly or access using this
1426       if (fd.isStatic() && fd.isFinal()) {
1427         loc.addLocation(Location.createTopLocation(md));
1428         return loc;
1429       }
1430     }
1431
1432     if (left instanceof ArrayAccessNode) {
1433       ArrayAccessNode aan = (ArrayAccessNode) left;
1434       left = aan.getExpression();
1435     }
1436
1437     loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false);
1438     // System.out.println("### checkLocationFromFieldAccessNode=" +
1439     // fan.printNode(0));
1440     // System.out.println("### left=" + left.printNode(0));
1441
1442     if (!left.getType().isPrimitive()) {
1443
1444       if (fd.getSymbol().equals("length")) {
1445         // array.length access, return the location of the array
1446         return loc;
1447       }
1448
1449       Location fieldLoc = getFieldLocation(fd);
1450       loc.addLocation(fieldLoc);
1451     }
1452     return loc;
1453   }
1454
1455   private Location getFieldLocation(FieldDescriptor fd) {
1456
1457     // System.out.println("### getFieldLocation=" + fd);
1458     // System.out.println("### fd.getType().getExtension()=" +
1459     // fd.getType().getExtension());
1460
1461     Location fieldLoc = (Location) fd.getType().getExtension();
1462
1463     // handle the case that method annotation checking skips checking field
1464     // declaration
1465     if (fieldLoc == null) {
1466       fieldLoc = checkFieldDeclaration(fd.getClassDescriptor(), fd);
1467     }
1468
1469     return fieldLoc;
1470
1471   }
1472
1473   private FieldDescriptor getFieldDescriptorFromExpressionNode(ExpressionNode en) {
1474
1475     if (en.kind() == Kind.NameNode) {
1476       NameNode nn = (NameNode) en;
1477       if (nn.getField() != null) {
1478         return nn.getField();
1479       }
1480
1481       if (nn.getName() != null && nn.getName().getBase() != null) {
1482         return getFieldDescriptorFromExpressionNode(nn.getExpression());
1483       }
1484
1485     } else if (en.kind() == Kind.FieldAccessNode) {
1486       FieldAccessNode fan = (FieldAccessNode) en;
1487       return fan.getField();
1488     }
1489
1490     return null;
1491   }
1492
1493   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
1494       SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) {
1495
1496     // System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0));
1497
1498     ClassDescriptor cd = md.getClassDesc();
1499
1500     Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
1501
1502     boolean postinc = true;
1503     if (an.getOperation().getBaseOp() == null
1504         || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation()
1505             .getBaseOp().getOp() != Operation.POSTDEC))
1506       postinc = false;
1507
1508     // if LHS is array access node, need to check if array index is higher
1509     // than array itself
1510     CompositeLocation destLocation =
1511         checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(),
1512             constraint, true);
1513
1514     CompositeLocation rhsLocation;
1515     CompositeLocation srcLocation;
1516
1517     if (!postinc) {
1518
1519       checkOwnership(md, an, an.getSrc());
1520
1521       rhsLocation =
1522           checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(),
1523               constraint, false);
1524
1525       srcLocation = rhsLocation;
1526
1527       // if (!rhsLocation.get(rhsLocation.getSize() - 1).isTop()) {
1528       if (constraint != null) {
1529         inputGLBSet.add(rhsLocation);
1530         inputGLBSet.add(constraint);
1531         srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
1532       }
1533       // }
1534
1535       // System.out.println("dstLocation=" + destLocation);
1536       // System.out.println("rhsLocation=" + rhsLocation);
1537       // System.out.println("srcLocation=" + srcLocation);
1538       // System.out.println("constraint=" + constraint);
1539
1540       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
1541
1542         String context = "";
1543         if (constraint != null) {
1544           context = " and the current context constraint is " + constraint;
1545         }
1546
1547         throw new Error("The value flow from " + srcLocation + " to " + destLocation
1548             + " does not respect location hierarchy on the assignment " + an.printNode(0) + context
1549             + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
1550       }
1551
1552       if (srcLocation.equals(destLocation)) {
1553         // keep it for definitely written analysis
1554         Set<FlatNode> flatNodeSet = ssjava.getBuildFlat().getFlatNodeSet(an);
1555         for (Iterator iterator = flatNodeSet.iterator(); iterator.hasNext();) {
1556           FlatNode fn = (FlatNode) iterator.next();
1557           ssjava.addSameHeightWriteFlatNode(fn);
1558         }
1559
1560       }
1561
1562     } else {
1563       destLocation =
1564           rhsLocation =
1565               checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(),
1566                   constraint, false);
1567
1568       if (constraint != null) {
1569         inputGLBSet.add(rhsLocation);
1570         inputGLBSet.add(constraint);
1571         srcLocation = CompositeLattice.calculateGLB(inputGLBSet, generateErrorMessage(cd, an));
1572       } else {
1573         srcLocation = rhsLocation;
1574       }
1575
1576       // System.out.println("srcLocation=" + srcLocation);
1577       // System.out.println("rhsLocation=" + rhsLocation);
1578       // System.out.println("constraint=" + constraint);
1579
1580       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
1581
1582         if (srcLocation.equals(destLocation)) {
1583           throw new Error("Location " + srcLocation
1584               + " is not allowed to have the value flow that moves within the same location at '"
1585               + an.printNode(0) + "' of " + cd.getSourceFileName() + "::" + an.getNumLine());
1586         } else {
1587           throw new Error("The value flow from " + srcLocation + " to " + destLocation
1588               + " does not respect location hierarchy on the assignment " + an.printNode(0)
1589               + " at " + cd.getSourceFileName() + "::" + an.getNumLine());
1590         }
1591
1592       }
1593
1594       if (srcLocation.equals(destLocation)) {
1595         // keep it for definitely written analysis
1596         Set<FlatNode> flatNodeSet = ssjava.getBuildFlat().getFlatNodeSet(an);
1597         for (Iterator iterator = flatNodeSet.iterator(); iterator.hasNext();) {
1598           FlatNode fn = (FlatNode) iterator.next();
1599           ssjava.addSameHeightWriteFlatNode(fn);
1600         }
1601       }
1602
1603     }
1604
1605     return destLocation;
1606   }
1607
1608   private void assignLocationOfVarDescriptor(VarDescriptor vd, MethodDescriptor md,
1609       SymbolTable nametable, TreeNode n) {
1610
1611     ClassDescriptor cd = md.getClassDesc();
1612     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
1613
1614     // currently enforce every variable to have corresponding location
1615     if (annotationVec.size() == 0) {
1616       throw new Error("Location is not assigned to variable '" + vd.getSymbol()
1617           + "' in the method '" + md + "' of the class " + cd.getSymbol() + " at "
1618           + generateErrorMessage(cd, n));
1619     }
1620
1621     int locDecCount = 0;
1622     for (int i = 0; i < annotationVec.size(); i++) {
1623       AnnotationDescriptor ad = annotationVec.elementAt(i);
1624
1625       if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
1626
1627         if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
1628           locDecCount++;
1629           if (locDecCount > 1) {// variable can have at most one location
1630             throw new Error(vd.getSymbol() + " has more than one location declaration.");
1631           }
1632           String locDec = ad.getValue(); // check if location is defined
1633
1634           if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
1635             DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
1636             d2loc.put(vd, deltaLoc);
1637             addLocationType(vd.getType(), deltaLoc);
1638           } else {
1639             CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
1640
1641             Location lastElement = compLoc.get(compLoc.getSize() - 1);
1642             if (ssjava.isSharedLocation(lastElement)) {
1643               ssjava.mapSharedLocation2Descriptor(lastElement, vd);
1644             }
1645
1646             d2loc.put(vd, compLoc);
1647             addLocationType(vd.getType(), compLoc);
1648           }
1649
1650         }
1651       }
1652     }
1653
1654   }
1655
1656   private DeltaLocation parseDeltaDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
1657
1658     int deltaCount = 0;
1659     int dIdx = locDec.indexOf(SSJavaAnalysis.DELTA);
1660     while (dIdx >= 0) {
1661       deltaCount++;
1662       int beginIdx = dIdx + 6;
1663       locDec = locDec.substring(beginIdx, locDec.length() - 1);
1664       dIdx = locDec.indexOf(SSJavaAnalysis.DELTA);
1665     }
1666
1667     CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
1668     DeltaLocation deltaLoc = new DeltaLocation(compLoc, deltaCount);
1669
1670     return deltaLoc;
1671   }
1672
1673   private Location parseFieldLocDeclaraton(String decl, String msg) throws Exception {
1674
1675     int idx = decl.indexOf(".");
1676
1677     String className = decl.substring(0, idx);
1678     String fieldName = decl.substring(idx + 1);
1679
1680     className.replaceAll(" ", "");
1681     fieldName.replaceAll(" ", "");
1682
1683     Descriptor d = state.getClassSymbolTable().get(className);
1684
1685     if (d == null) {
1686       // System.out.println("state.getClassSymbolTable()=" +
1687       // state.getClassSymbolTable());
1688       throw new Error("The class in the location declaration '" + decl + "' does not exist at "
1689           + msg);
1690     }
1691
1692     assert (d instanceof ClassDescriptor);
1693     SSJavaLattice<String> lattice = ssjava.getClassLattice((ClassDescriptor) d);
1694     if (!lattice.containsKey(fieldName)) {
1695       throw new Error("The location " + fieldName + " is not defined in the field lattice of '"
1696           + className + "' at " + msg);
1697     }
1698
1699     return new Location(d, fieldName);
1700   }
1701
1702   private CompositeLocation parseLocationDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
1703
1704     CompositeLocation compLoc = new CompositeLocation();
1705
1706     StringTokenizer tokenizer = new StringTokenizer(locDec, ",");
1707     List<String> locIdList = new ArrayList<String>();
1708     while (tokenizer.hasMoreTokens()) {
1709       String locId = tokenizer.nextToken();
1710       locIdList.add(locId);
1711     }
1712
1713     // at least,one location element needs to be here!
1714     assert (locIdList.size() > 0);
1715
1716     // assume that loc with idx 0 comes from the local lattice
1717     // loc with idx 1 comes from the field lattice
1718
1719     String localLocId = locIdList.get(0);
1720     SSJavaLattice<String> localLattice = CompositeLattice.getLatticeByDescriptor(md);
1721     Location localLoc = new Location(md, localLocId);
1722     if (localLattice == null || (!localLattice.containsKey(localLocId))) {
1723       throw new Error("Location " + localLocId
1724           + " is not defined in the local variable lattice at "
1725           + md.getClassDesc().getSourceFileName() + "::" + (n != null ? n.getNumLine() : md) + ".");
1726     }
1727     compLoc.addLocation(localLoc);
1728
1729     for (int i = 1; i < locIdList.size(); i++) {
1730       String locName = locIdList.get(i);
1731       try {
1732         Location fieldLoc =
1733             parseFieldLocDeclaraton(locName, generateErrorMessage(md.getClassDesc(), n));
1734         compLoc.addLocation(fieldLoc);
1735       } catch (Exception e) {
1736         throw new Error("The location declaration '" + locName + "' is wrong  at "
1737             + generateErrorMessage(md.getClassDesc(), n));
1738       }
1739     }
1740
1741     return compLoc;
1742
1743   }
1744
1745   private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) {
1746     VarDescriptor vd = dn.getVarDescriptor();
1747     assignLocationOfVarDescriptor(vd, md, nametable, dn);
1748   }
1749
1750   private void checkDeclarationInClass(ClassDescriptor cd) {
1751     // Check to see that fields are okay
1752     for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
1753       FieldDescriptor fd = (FieldDescriptor) field_it.next();
1754
1755       if (!(fd.isFinal() && fd.isStatic())) {
1756         checkFieldDeclaration(cd, fd);
1757       } else {
1758         // for static final, assign top location by default
1759         Location loc = Location.createTopLocation(cd);
1760         addLocationType(fd.getType(), loc);
1761       }
1762     }
1763   }
1764
1765   private Location checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
1766
1767     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
1768
1769     // currently enforce every field to have corresponding location
1770     if (annotationVec.size() == 0) {
1771       throw new Error("Location is not assigned to the field '" + fd.getSymbol()
1772           + "' of the class " + cd.getSymbol() + " at " + cd.getSourceFileName());
1773     }
1774
1775     if (annotationVec.size() > 1) {
1776       // variable can have at most one location
1777       throw new Error("Field " + fd.getSymbol() + " of class " + cd
1778           + " has more than one location.");
1779     }
1780
1781     AnnotationDescriptor ad = annotationVec.elementAt(0);
1782     Location loc = null;
1783
1784     if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
1785       if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
1786         String locationID = ad.getValue();
1787         // check if location is defined
1788         SSJavaLattice<String> lattice = ssjava.getClassLattice(cd);
1789         if (lattice == null || (!lattice.containsKey(locationID))) {
1790           throw new Error("Location " + locationID
1791               + " is not defined in the field lattice of class " + cd.getSymbol() + " at"
1792               + cd.getSourceFileName() + ".");
1793         }
1794         loc = new Location(cd, locationID);
1795
1796         if (ssjava.isSharedLocation(loc)) {
1797           ssjava.mapSharedLocation2Descriptor(loc, fd);
1798         }
1799
1800         addLocationType(fd.getType(), loc);
1801
1802       }
1803     }
1804
1805     return loc;
1806   }
1807
1808   private void addLocationType(TypeDescriptor type, CompositeLocation loc) {
1809     if (type != null) {
1810       TypeExtension te = type.getExtension();
1811       SSJavaType ssType;
1812       if (te != null) {
1813         ssType = (SSJavaType) te;
1814         ssType.setCompLoc(loc);
1815       } else {
1816         ssType = new SSJavaType(loc);
1817         type.setExtension(ssType);
1818       }
1819     }
1820   }
1821
1822   private void addLocationType(TypeDescriptor type, Location loc) {
1823     if (type != null) {
1824       type.setExtension(loc);
1825     }
1826   }
1827
1828   static class CompositeLattice {
1829
1830     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2, String msg) {
1831
1832       // System.out.println("\nisGreaterThan=" + loc1 + " " + loc2 + " msg=" +
1833       // msg);
1834       int baseCompareResult = compareBaseLocationSet(loc1, loc2, true, false, msg);
1835       if (baseCompareResult == ComparisonResult.EQUAL) {
1836         if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) {
1837           return true;
1838         } else {
1839           return false;
1840         }
1841       } else if (baseCompareResult == ComparisonResult.GREATER) {
1842         return true;
1843       } else {
1844         return false;
1845       }
1846
1847     }
1848
1849     public static int compare(CompositeLocation loc1, CompositeLocation loc2, boolean ignore,
1850         String msg) {
1851
1852       // System.out.println("compare=" + loc1 + " " + loc2);
1853       int baseCompareResult = compareBaseLocationSet(loc1, loc2, false, ignore, msg);
1854
1855       if (baseCompareResult == ComparisonResult.EQUAL) {
1856         return compareDelta(loc1, loc2);
1857       } else {
1858         return baseCompareResult;
1859       }
1860
1861     }
1862
1863     private static int compareDelta(CompositeLocation dLoc1, CompositeLocation dLoc2) {
1864
1865       int deltaCount1 = 0;
1866       int deltaCount2 = 0;
1867       if (dLoc1 instanceof DeltaLocation) {
1868         deltaCount1 = ((DeltaLocation) dLoc1).getNumDelta();
1869       }
1870
1871       if (dLoc2 instanceof DeltaLocation) {
1872         deltaCount2 = ((DeltaLocation) dLoc2).getNumDelta();
1873       }
1874       if (deltaCount1 < deltaCount2) {
1875         return ComparisonResult.GREATER;
1876       } else if (deltaCount1 == deltaCount2) {
1877         return ComparisonResult.EQUAL;
1878       } else {
1879         return ComparisonResult.LESS;
1880       }
1881
1882     }
1883
1884     private static int compareBaseLocationSet(CompositeLocation compLoc1,
1885         CompositeLocation compLoc2, boolean awareSharedLoc, boolean ignore, String msg) {
1886
1887       // if compLoc1 is greater than compLoc2, return true
1888       // else return false;
1889
1890       // compare one by one in according to the order of the tuple
1891       int numOfTie = 0;
1892       for (int i = 0; i < compLoc1.getSize(); i++) {
1893         Location loc1 = compLoc1.get(i);
1894         if (i >= compLoc2.getSize()) {
1895           if (ignore) {
1896             return ComparisonResult.INCOMPARABLE;
1897           } else {
1898             throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1899                 + " because they are not comparable at " + msg);
1900           }
1901         }
1902         Location loc2 = compLoc2.get(i);
1903
1904         Descriptor descriptor = getCommonParentDescriptor(loc1, loc2, msg);
1905         SSJavaLattice<String> lattice = getLatticeByDescriptor(descriptor);
1906
1907         // check if the shared location is appeared only at the end of the
1908         // composite location
1909         if (lattice.getSharedLocSet().contains(loc1.getLocIdentifier())) {
1910           if (i != (compLoc1.getSize() - 1)) {
1911             throw new Error("The shared location " + loc1.getLocIdentifier()
1912                 + " cannot be appeared in the middle of composite location at" + msg);
1913           }
1914         }
1915
1916         if (lattice.getSharedLocSet().contains(loc2.getLocIdentifier())) {
1917           if (i != (compLoc2.getSize() - 1)) {
1918             throw new Error("The shared location " + loc2.getLocIdentifier()
1919                 + " cannot be appeared in the middle of composite location at " + msg);
1920           }
1921         }
1922
1923         // if (!lattice1.equals(lattice2)) {
1924         // throw new Error("Failed to compare two locations of " + compLoc1 +
1925         // " and " + compLoc2
1926         // + " because they are not comparable at " + msg);
1927         // }
1928
1929         if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
1930           numOfTie++;
1931           // check if the current location is the spinning location
1932           // note that the spinning location only can be appeared in the last
1933           // part of the composite location
1934           if (awareSharedLoc && numOfTie == compLoc1.getSize()
1935               && lattice.getSharedLocSet().contains(loc1.getLocIdentifier())) {
1936             return ComparisonResult.GREATER;
1937           }
1938           continue;
1939         } else if (lattice.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
1940           return ComparisonResult.GREATER;
1941         } else {
1942           return ComparisonResult.LESS;
1943         }
1944
1945       }
1946
1947       if (numOfTie == compLoc1.getSize()) {
1948
1949         if (numOfTie != compLoc2.getSize()) {
1950
1951           if (ignore) {
1952             return ComparisonResult.INCOMPARABLE;
1953           } else {
1954             throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1955                 + " because they are not comparable at " + msg);
1956           }
1957
1958         }
1959
1960         return ComparisonResult.EQUAL;
1961       }
1962
1963       return ComparisonResult.LESS;
1964
1965     }
1966
1967     public static CompositeLocation calculateGLB(Set<CompositeLocation> inputSet, String errMsg) {
1968
1969       // System.out.println("Calculating GLB=" + inputSet);
1970       CompositeLocation glbCompLoc = new CompositeLocation();
1971
1972       // calculate GLB of the first(priority) element
1973       Set<String> priorityLocIdentifierSet = new HashSet<String>();
1974       Descriptor priorityDescriptor = null;
1975
1976       Hashtable<String, Set<CompositeLocation>> locId2CompLocSet =
1977           new Hashtable<String, Set<CompositeLocation>>();
1978       // mapping from the priority loc ID to its full representation by the
1979       // composite location
1980
1981       int maxTupleSize = 0;
1982       CompositeLocation maxCompLoc = null;
1983
1984       Location prevPriorityLoc = null;
1985       for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) {
1986         CompositeLocation compLoc = (CompositeLocation) iterator.next();
1987         if (compLoc.getSize() > maxTupleSize) {
1988           maxTupleSize = compLoc.getSize();
1989           maxCompLoc = compLoc;
1990         }
1991         Location priorityLoc = compLoc.get(0);
1992         String priorityLocId = priorityLoc.getLocIdentifier();
1993         priorityLocIdentifierSet.add(priorityLocId);
1994
1995         if (locId2CompLocSet.containsKey(priorityLocId)) {
1996           locId2CompLocSet.get(priorityLocId).add(compLoc);
1997         } else {
1998           Set<CompositeLocation> newSet = new HashSet<CompositeLocation>();
1999           newSet.add(compLoc);
2000           locId2CompLocSet.put(priorityLocId, newSet);
2001         }
2002
2003         // check if priority location are coming from the same lattice
2004         if (priorityDescriptor == null) {
2005           priorityDescriptor = priorityLoc.getDescriptor();
2006         } else {
2007           priorityDescriptor = getCommonParentDescriptor(priorityLoc, prevPriorityLoc, errMsg);
2008         }
2009         prevPriorityLoc = priorityLoc;
2010         // else if (!priorityDescriptor.equals(priorityLoc.getDescriptor())) {
2011         // throw new Error("Failed to calculate GLB of " + inputSet
2012         // + " because they are from different lattices.");
2013         // }
2014       }
2015
2016       SSJavaLattice<String> locOrder = getLatticeByDescriptor(priorityDescriptor);
2017       String glbOfPriorityLoc = locOrder.getGLB(priorityLocIdentifierSet);
2018
2019       glbCompLoc.addLocation(new Location(priorityDescriptor, glbOfPriorityLoc));
2020       Set<CompositeLocation> compSet = locId2CompLocSet.get(glbOfPriorityLoc);
2021
2022       if (compSet == null) {
2023         // when GLB(x1,x2)!=x1 and !=x2 : GLB case 4
2024         // mean that the result is already lower than <x1,y1> and <x2,y2>
2025         // assign TOP to the rest of the location elements
2026
2027         // in this case, do not take care about delta
2028         // CompositeLocation inputComp = inputSet.iterator().next();
2029         for (int i = 1; i < maxTupleSize; i++) {
2030           glbCompLoc.addLocation(Location.createTopLocation(maxCompLoc.get(i).getDescriptor()));
2031         }
2032       } else {
2033
2034         // here find out composite location that has a maximum length tuple
2035         // if we have three input set: [A], [A,B], [A,B,C]
2036         // maximum length tuple will be [A,B,C]
2037         int max = 0;
2038         CompositeLocation maxFromCompSet = null;
2039         for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
2040           CompositeLocation c = (CompositeLocation) iterator.next();
2041           if (c.getSize() > max) {
2042             max = c.getSize();
2043             maxFromCompSet = c;
2044           }
2045         }
2046
2047         if (compSet.size() == 1) {
2048           // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
2049           CompositeLocation comp = compSet.iterator().next();
2050           for (int i = 1; i < comp.getSize(); i++) {
2051             glbCompLoc.addLocation(comp.get(i));
2052           }
2053
2054           // if input location corresponding to glb is a delta, need to apply
2055           // delta to glb result
2056           if (comp instanceof DeltaLocation) {
2057             glbCompLoc = new DeltaLocation(glbCompLoc, 1);
2058           }
2059
2060         } else {
2061           // when GLB(x1,x2)==x1 and x2 : GLB case 1
2062           // if more than one location shares the same priority GLB
2063           // need to calculate the rest of GLB loc
2064
2065           // setup input set starting from the second tuple item
2066           Set<CompositeLocation> innerGLBInput = new HashSet<CompositeLocation>();
2067           for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
2068             CompositeLocation compLoc = (CompositeLocation) iterator.next();
2069             CompositeLocation innerCompLoc = new CompositeLocation();
2070             for (int idx = 1; idx < compLoc.getSize(); idx++) {
2071               innerCompLoc.addLocation(compLoc.get(idx));
2072             }
2073             if (innerCompLoc.getSize() > 0) {
2074               innerGLBInput.add(innerCompLoc);
2075             }
2076           }
2077
2078           if (innerGLBInput.size() > 0) {
2079             CompositeLocation innerGLB = CompositeLattice.calculateGLB(innerGLBInput, errMsg);
2080             for (int idx = 0; idx < innerGLB.getSize(); idx++) {
2081               glbCompLoc.addLocation(innerGLB.get(idx));
2082             }
2083           }
2084
2085           // if input location corresponding to glb is a delta, need to apply
2086           // delta to glb result
2087
2088           for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
2089             CompositeLocation compLoc = (CompositeLocation) iterator.next();
2090             if (compLoc instanceof DeltaLocation) {
2091               if (glbCompLoc.equals(compLoc)) {
2092                 glbCompLoc = new DeltaLocation(glbCompLoc, 1);
2093                 break;
2094               }
2095             }
2096           }
2097
2098         }
2099       }
2100
2101       // System.out.println("GLB=" + glbCompLoc);
2102       return glbCompLoc;
2103
2104     }
2105
2106     static SSJavaLattice<String> getLatticeByDescriptor(Descriptor d) {
2107
2108       SSJavaLattice<String> lattice = null;
2109
2110       if (d instanceof ClassDescriptor) {
2111         lattice = ssjava.getCd2lattice().get(d);
2112       } else if (d instanceof MethodDescriptor) {
2113         if (ssjava.getMd2lattice().containsKey(d)) {
2114           lattice = ssjava.getMd2lattice().get(d);
2115         } else {
2116           // use default lattice for the method
2117           lattice = ssjava.getCd2methodDefault().get(((MethodDescriptor) d).getClassDesc());
2118         }
2119       }
2120
2121       return lattice;
2122     }
2123
2124     static Descriptor getCommonParentDescriptor(Location loc1, Location loc2, String msg) {
2125
2126       Descriptor d1 = loc1.getDescriptor();
2127       Descriptor d2 = loc2.getDescriptor();
2128
2129       Descriptor descriptor;
2130
2131       if (d1 instanceof ClassDescriptor && d2 instanceof ClassDescriptor) {
2132
2133         if (d1.equals(d2)) {
2134           descriptor = d1;
2135         } else {
2136           // identifying which one is parent class
2137           Set<Descriptor> d1SubClassesSet = ssjava.tu.getSubClasses((ClassDescriptor) d1);
2138           Set<Descriptor> d2SubClassesSet = ssjava.tu.getSubClasses((ClassDescriptor) d2);
2139
2140           if (d1 == null && d2 == null) {
2141             throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2
2142                 + " because they are not comparable at " + msg);
2143           } else if (d1SubClassesSet != null && d1SubClassesSet.contains(d2)) {
2144             descriptor = d1;
2145           } else if (d2SubClassesSet != null && d2SubClassesSet.contains(d1)) {
2146             descriptor = d2;
2147           } else {
2148             throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2
2149                 + " because they are not comparable at " + msg);
2150           }
2151         }
2152
2153       } else if (d1 instanceof MethodDescriptor && d2 instanceof MethodDescriptor) {
2154
2155         if (d1.equals(d2)) {
2156           descriptor = d1;
2157         } else {
2158
2159           // identifying which one is parent class
2160           MethodDescriptor md1 = (MethodDescriptor) d1;
2161           MethodDescriptor md2 = (MethodDescriptor) d2;
2162
2163           if (!md1.matches(md2)) {
2164             throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2
2165                 + " because they are not comparable at " + msg);
2166           }
2167
2168           Set<Descriptor> d1SubClassesSet =
2169               ssjava.tu.getSubClasses(((MethodDescriptor) d1).getClassDesc());
2170           Set<Descriptor> d2SubClassesSet =
2171               ssjava.tu.getSubClasses(((MethodDescriptor) d2).getClassDesc());
2172
2173           if (d1 == null && d2 == null) {
2174             throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2
2175                 + " because they are not comparable at " + msg);
2176           } else if (d1 != null && d1SubClassesSet.contains(d2)) {
2177             descriptor = d1;
2178           } else if (d2 != null && d2SubClassesSet.contains(d1)) {
2179             descriptor = d2;
2180           } else {
2181             throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2
2182                 + " because they are not comparable at " + msg);
2183           }
2184         }
2185
2186       } else {
2187         throw new Error("Failed to compare two locations of " + loc1 + " and " + loc2
2188             + " because they are not comparable at " + msg);
2189       }
2190
2191       return descriptor;
2192
2193     }
2194
2195   }
2196
2197   class ComparisonResult {
2198
2199     public static final int GREATER = 0;
2200     public static final int EQUAL = 1;
2201     public static final int LESS = 2;
2202     public static final int INCOMPARABLE = 3;
2203     int result;
2204
2205   }
2206
2207 }
2208
2209 class ReturnLocGenerator {
2210
2211   public static final int PARAMISHIGHER = 0;
2212   public static final int PARAMISSAME = 1;
2213   public static final int IGNORE = 2;
2214
2215   private Hashtable<Integer, Integer> paramIdx2paramType;
2216
2217   private CompositeLocation declaredReturnLoc = null;
2218
2219   public ReturnLocGenerator(CompositeLocation returnLoc, MethodDescriptor md,
2220       List<CompositeLocation> params, String msg) {
2221
2222     CompositeLocation thisLoc = params.get(0);
2223     if (returnLoc.get(0).equals(thisLoc.get(0)) && returnLoc.getSize() > 1) {
2224       // if the declared return location consists of THIS and field location,
2225       // return location for the caller's side has to have same field element
2226       this.declaredReturnLoc = returnLoc;
2227     } else {
2228       // creating mappings
2229       paramIdx2paramType = new Hashtable<Integer, Integer>();
2230       for (int i = 0; i < params.size(); i++) {
2231         CompositeLocation param = params.get(i);
2232         int compareResult = CompositeLattice.compare(param, returnLoc, true, msg);
2233
2234         int type;
2235         if (compareResult == ComparisonResult.GREATER) {
2236           type = 0;
2237         } else if (compareResult == ComparisonResult.EQUAL) {
2238           type = 1;
2239         } else {
2240           type = 2;
2241         }
2242         paramIdx2paramType.put(new Integer(i), new Integer(type));
2243       }
2244     }
2245
2246   }
2247
2248   public CompositeLocation computeReturnLocation(List<CompositeLocation> args) {
2249
2250     if (declaredReturnLoc != null) {
2251       // when developer specify that the return value is [THIS,field]
2252       // needs to translate to the caller's location
2253       CompositeLocation callerLoc = new CompositeLocation();
2254       CompositeLocation callerBaseLocation = args.get(0);
2255
2256       for (int i = 0; i < callerBaseLocation.getSize(); i++) {
2257         callerLoc.addLocation(callerBaseLocation.get(i));
2258       }
2259       for (int i = 1; i < declaredReturnLoc.getSize(); i++) {
2260         callerLoc.addLocation(declaredReturnLoc.get(i));
2261       }
2262       return callerLoc;
2263     } else {
2264       // compute the highest possible location in caller's side
2265       assert paramIdx2paramType.keySet().size() == args.size();
2266
2267       Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
2268       for (int i = 0; i < args.size(); i++) {
2269         int type = (paramIdx2paramType.get(new Integer(i))).intValue();
2270         CompositeLocation argLoc = args.get(i);
2271         if (type == PARAMISHIGHER || type == PARAMISSAME) {
2272           // return loc is equal to or lower than param
2273           inputGLB.add(argLoc);
2274         }
2275       }
2276
2277       // compute GLB of arguments subset that are same or higher than return
2278       // location
2279       if (inputGLB.isEmpty()) {
2280         CompositeLocation rtr =
2281             new CompositeLocation(Location.createTopLocation(args.get(0).get(0).getDescriptor()));
2282         return rtr;
2283       } else {
2284         CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB, "");
2285         return glb;
2286       }
2287     }
2288
2289   }
2290 }