Robust/src/Analysis/SSJava/FlowDownCheck.java

   1 package Analysis.SSJava;
   2
   3 import java.util.ArrayList;
   4 import java.util.HashSet;
   5 import java.util.Hashtable;
   6 import java.util.Iterator;
   7 import java.util.List;
   8 import java.util.Set;
   9 import java.util.StringTokenizer;
  10 import java.util.Vector;
  11
  12 import Analysis.SSJava.FlowDownCheck.ComparisonResult;
  13 import Analysis.SSJava.FlowDownCheck.CompositeLattice;
  14 import IR.AnnotationDescriptor;
  15 import IR.ClassDescriptor;
  16 import IR.Descriptor;
  17 import IR.FieldDescriptor;
  18 import IR.MethodDescriptor;
  19 import IR.NameDescriptor;
  20 import IR.Operation;
  21 import IR.State;
  22 import IR.SymbolTable;
  23 import IR.TypeDescriptor;
  24 import IR.VarDescriptor;
  25 import IR.Tree.ArrayAccessNode;
  26 import IR.Tree.AssignmentNode;
  27 import IR.Tree.BlockExpressionNode;
  28 import IR.Tree.BlockNode;
  29 import IR.Tree.BlockStatementNode;
  30 import IR.Tree.CastNode;
  31 import IR.Tree.CreateObjectNode;
  32 import IR.Tree.DeclarationNode;
  33 import IR.Tree.ExpressionNode;
  34 import IR.Tree.FieldAccessNode;
  35 import IR.Tree.IfStatementNode;
  36 import IR.Tree.Kind;
  37 import IR.Tree.LiteralNode;
  38 import IR.Tree.LoopNode;
  39 import IR.Tree.MethodInvokeNode;
  40 import IR.Tree.NameNode;
  41 import IR.Tree.OpNode;
  42 import IR.Tree.ReturnNode;
  43 import IR.Tree.SubBlockNode;
  44 import IR.Tree.SwitchBlockNode;
  45 import IR.Tree.SwitchStatementNode;
  46 import IR.Tree.SynchronizedNode;
  47 import IR.Tree.TertiaryNode;
  48 import IR.Tree.TreeNode;
  49 import Util.Pair;
  50
  51 public class FlowDownCheck {
  52
  53   State state;
  54   static SSJavaAnalysis ssjava;
  55
  56   HashSet toanalyze;
  57
  58   // mapping from 'descriptor' to 'composite location'
  59   Hashtable<Descriptor, CompositeLocation> d2loc;
  60
  61   Hashtable<MethodDescriptor, CompositeLocation> md2ReturnLoc;
  62   Hashtable<MethodDescriptor, ReturnLocGenerator> md2ReturnLocGen;
  63
  64   // mapping from 'locID' to 'class descriptor'
  65   Hashtable<String, ClassDescriptor> fieldLocName2cd;
  66
  67   public FlowDownCheck(SSJavaAnalysis ssjava, State state) {
  68     this.ssjava = ssjava;
  69     this.state = state;
  70     this.toanalyze = new HashSet();
  71     this.d2loc = new Hashtable<Descriptor, CompositeLocation>();
  72     this.fieldLocName2cd = new Hashtable<String, ClassDescriptor>();
  73     this.md2ReturnLoc = new Hashtable<MethodDescriptor, CompositeLocation>();
  74     this.md2ReturnLocGen = new Hashtable<MethodDescriptor, ReturnLocGenerator>();
  75   }
  76
  77   public void init() {
  78
  79     // construct mapping from the location name to the class descriptor
  80     // assume that the location name is unique through the whole program
  81
  82     Set<ClassDescriptor> cdSet = ssjava.getCd2lattice().keySet();
  83     for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
  84       ClassDescriptor cd = (ClassDescriptor) iterator.next();
  85       SSJavaLattice<String> lattice = ssjava.getCd2lattice().get(cd);
  86       Set<String> fieldLocNameSet = lattice.getKeySet();
  87
  88       for (Iterator iterator2 = fieldLocNameSet.iterator(); iterator2.hasNext();) {
  89         String fieldLocName = (String) iterator2.next();
  90         fieldLocName2cd.put(fieldLocName, cd);
  91       }
  92
  93     }
  94
  95   }
  96
  97   public void flowDownCheck() {
  98     SymbolTable classtable = state.getClassSymbolTable();
  99
 100     // phase 1 : checking declaration node and creating mapping of 'type
 101     // desciptor' & 'location'
 102     toanalyze.addAll(classtable.getValueSet());
 103     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
 104
 105     while (!toanalyze.isEmpty()) {
 106       Object obj = toanalyze.iterator().next();
 107       ClassDescriptor cd = (ClassDescriptor) obj;
 108       toanalyze.remove(cd);
 109
 110       if (ssjava.needToBeAnnoated(cd)) {
 111
 112         ClassDescriptor superDesc = cd.getSuperDesc();
 113
 114         if (superDesc != null && (!superDesc.getSymbol().equals("Object"))) {
 115           checkOrderingInheritance(superDesc, cd);
 116         }
 117
 118         checkDeclarationInClass(cd);
 119         for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 120           MethodDescriptor md = (MethodDescriptor) method_it.next();
 121           if (ssjava.needTobeAnnotated(md)) {
 122             checkDeclarationInMethodBody(cd, md);
 123           }
 124         }
 125       }
 126
 127     }
 128
 129     // phase2 : checking assignments
 130     toanalyze.addAll(classtable.getValueSet());
 131     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
 132     while (!toanalyze.isEmpty()) {
 133       Object obj = toanalyze.iterator().next();
 134       ClassDescriptor cd = (ClassDescriptor) obj;
 135       toanalyze.remove(cd);
 136
 137       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 138         MethodDescriptor md = (MethodDescriptor) method_it.next();
 139         if (ssjava.needTobeAnnotated(md)) {
 140           checkMethodBody(cd, md);
 141         }
 142       }
 143     }
 144
 145   }
 146
 147   private void checkOrderingInheritance(ClassDescriptor superCd, ClassDescriptor cd) {
 148     // here, we're going to check that sub class keeps same relative orderings
 149     // in respect to super class
 150
 151     SSJavaLattice<String> superLattice = ssjava.getClassLattice(superCd);
 152     SSJavaLattice<String> subLattice = ssjava.getClassLattice(cd);
 153
 154     if (superLattice != null) {
 155       // if super class doesn't define lattice, then we don't need to check its
 156       // subclass
 157       if (subLattice == null) {
 158         throw new Error("If a parent class '" + superCd
 159             + "' has a ordering lattice, its subclass '" + cd + "' should have one.");
 160       }
 161
 162       Set<Pair<String, String>> superPairSet = superLattice.getOrderingPairSet();
 163       Set<Pair<String, String>> subPairSet = subLattice.getOrderingPairSet();
 164
 165       for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) {
 166         Pair<String, String> pair = (Pair<String, String>) iterator.next();
 167
 168         if (!subPairSet.contains(pair)) {
 169           throw new Error("Subclass '" + cd + "' does not have the relative ordering '"
 170               + pair.getSecond() + " < " + pair.getFirst()
 171               + "' that is defined by its superclass '" + superCd + "'.");
 172         }
 173       }
 174     }
 175
 176     MethodLattice<String> superMethodDefaultLattice = ssjava.getMethodDefaultLattice(superCd);
 177     MethodLattice<String> subMethodDefaultLattice = ssjava.getMethodDefaultLattice(cd);
 178
 179     if (superMethodDefaultLattice != null) {
 180       if (subMethodDefaultLattice == null) {
 181         throw new Error("When a parent class '" + superCd
 182             + "' defines a default method lattice, its subclass '" + cd + "' should define one.");
 183       }
 184
 185       Set<Pair<String, String>> superPairSet = superMethodDefaultLattice.getOrderingPairSet();
 186       Set<Pair<String, String>> subPairSet = subMethodDefaultLattice.getOrderingPairSet();
 187
 188       for (Iterator iterator = superPairSet.iterator(); iterator.hasNext();) {
 189         Pair<String, String> pair = (Pair<String, String>) iterator.next();
 190
 191         if (!subPairSet.contains(pair)) {
 192           throw new Error("Subclass '" + cd + "' does not have the relative ordering '"
 193               + pair.getSecond() + " < " + pair.getFirst()
 194               + "' that is defined by its superclass '" + superCd
 195               + "' in the method default lattice.");
 196         }
 197       }
 198
 199     }
 200
 201   }
 202
 203   public Hashtable getMap() {
 204     return d2loc;
 205   }
 206
 207   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
 208     BlockNode bn = state.getMethodBody(md);
 209
 210     if (ssjava.needTobeAnnotated(md)) {
 211       // first, check annotations on method declaration
 212
 213       // parsing returnloc annotation
 214       Vector<AnnotationDescriptor> methodAnnotations = md.getModifiers().getAnnotations();
 215       if (methodAnnotations != null) {
 216         for (int i = 0; i < methodAnnotations.size(); i++) {
 217           AnnotationDescriptor an = methodAnnotations.elementAt(i);
 218           if (an.getMarker().equals(ssjava.RETURNLOC)) {
 219             // developer explicitly defines method lattice
 220             String returnLocDeclaration = an.getValue();
 221             CompositeLocation returnLocComp =
 222                 parseLocationDeclaration(md, null, returnLocDeclaration);
 223             md2ReturnLoc.put(md, returnLocComp);
 224           }
 225         }
 226         if (!md.getReturnType().isVoid() && !md2ReturnLoc.containsKey(md)) {
 227           throw new Error("Return location is not specified for the method " + md + " at "
 228               + cd.getSourceFileName());
 229         }
 230       }
 231
 232       List<CompositeLocation> paramList = new ArrayList<CompositeLocation>();
 233
 234       boolean hasReturnValue = (!md.getReturnType().isVoid());
 235       if (hasReturnValue) {
 236         MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
 237         String thisLocId = methodLattice.getThisLoc();
 238         if (thisLocId == null) {
 239           throw new Error("Method '" + md + "' does not have the definition of 'this' location at "
 240               + md.getClassDesc().getSourceFileName());
 241         }
 242         CompositeLocation thisLoc = new CompositeLocation(new Location(md, thisLocId));
 243         paramList.add(thisLoc);
 244       }
 245
 246       for (int i = 0; i < md.numParameters(); i++) {
 247         // process annotations on method parameters
 248         VarDescriptor vd = (VarDescriptor) md.getParameter(i);
 249         assignLocationOfVarDescriptor(vd, md, md.getParameterTable(), bn);
 250         if (hasReturnValue) {
 251           paramList.add(d2loc.get(vd));
 252         }
 253       }
 254
 255       if (hasReturnValue) {
 256         md2ReturnLocGen.put(md, new ReturnLocGenerator(md2ReturnLoc.get(md), paramList,
 257             generateErrorMessage(cd, null)));
 258       }
 259       checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
 260     }
 261
 262   }
 263
 264   private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
 265     bn.getVarTable().setParent(nametable);
 266     for (int i = 0; i < bn.size(); i++) {
 267       BlockStatementNode bsn = bn.get(i);
 268       checkDeclarationInBlockStatementNode(md, bn.getVarTable(), bsn);
 269     }
 270   }
 271
 272   private void checkDeclarationInBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
 273       BlockStatementNode bsn) {
 274
 275     switch (bsn.kind()) {
 276     case Kind.SubBlockNode:
 277       checkDeclarationInSubBlockNode(md, nametable, (SubBlockNode) bsn);
 278       return;
 279
 280     case Kind.DeclarationNode:
 281       checkDeclarationNode(md, nametable, (DeclarationNode) bsn);
 282       break;
 283
 284     case Kind.LoopNode:
 285       checkDeclarationInLoopNode(md, nametable, (LoopNode) bsn);
 286       break;
 287
 288     case Kind.IfStatementNode:
 289       checkDeclarationInIfStatementNode(md, nametable, (IfStatementNode) bsn);
 290       return;
 291
 292     case Kind.SwitchStatementNode:
 293       checkDeclarationInSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn);
 294       return;
 295
 296     case Kind.SynchronizedNode:
 297       checkDeclarationInSynchronizedNode(md, nametable, (SynchronizedNode) bsn);
 298       return;
 299
 300     }
 301   }
 302
 303   private void checkDeclarationInSynchronizedNode(MethodDescriptor md, SymbolTable nametable,
 304       SynchronizedNode sbn) {
 305     checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode());
 306   }
 307
 308   private void checkDeclarationInSwitchStatementNode(MethodDescriptor md, SymbolTable nametable,
 309       SwitchStatementNode ssn) {
 310     BlockNode sbn = ssn.getSwitchBody();
 311     for (int i = 0; i < sbn.size(); i++) {
 312       SwitchBlockNode node = (SwitchBlockNode) sbn.get(i);
 313       checkDeclarationInBlockNode(md, nametable, node.getSwitchBlockStatement());
 314     }
 315   }
 316
 317   private void checkDeclarationInIfStatementNode(MethodDescriptor md, SymbolTable nametable,
 318       IfStatementNode isn) {
 319     checkDeclarationInBlockNode(md, nametable, isn.getTrueBlock());
 320     if (isn.getFalseBlock() != null)
 321       checkDeclarationInBlockNode(md, nametable, isn.getFalseBlock());
 322   }
 323
 324   private void checkDeclarationInLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln) {
 325
 326     if (ln.getType() == LoopNode.FORLOOP) {
 327       // check for loop case
 328       ClassDescriptor cd = md.getClassDesc();
 329       BlockNode bn = ln.getInitializer();
 330       for (int i = 0; i < bn.size(); i++) {
 331         BlockStatementNode bsn = bn.get(i);
 332         checkDeclarationInBlockStatementNode(md, nametable, bsn);
 333       }
 334     }
 335
 336     // check loop body
 337     checkDeclarationInBlockNode(md, nametable, ln.getBody());
 338   }
 339
 340   private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
 341     BlockNode bn = state.getMethodBody(md);
 342     checkLocationFromBlockNode(md, md.getParameterTable(), bn, null);
 343   }
 344
 345   private String generateErrorMessage(ClassDescriptor cd, TreeNode tn) {
 346     if (tn != null) {
 347       return cd.getSourceFileName() + "::" + tn.getNumLine();
 348     } else {
 349       return cd.getSourceFileName();
 350     }
 351
 352   }
 353
 354   private CompositeLocation checkLocationFromBlockNode(MethodDescriptor md, SymbolTable nametable,
 355       BlockNode bn, CompositeLocation constraint) {
 356
 357     bn.getVarTable().setParent(nametable);
 358     for (int i = 0; i < bn.size(); i++) {
 359       BlockStatementNode bsn = bn.get(i);
 360       checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn, constraint);
 361     }
 362     return new CompositeLocation();
 363
 364   }
 365
 366   private CompositeLocation checkLocationFromBlockStatementNode(MethodDescriptor md,
 367       SymbolTable nametable, BlockStatementNode bsn, CompositeLocation constraint) {
 368
 369     CompositeLocation compLoc = null;
 370     switch (bsn.kind()) {
 371     case Kind.BlockExpressionNode:
 372       compLoc =
 373           checkLocationFromBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn, constraint);
 374       break;
 375
 376     case Kind.DeclarationNode:
 377       compLoc = checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn, constraint);
 378       break;
 379
 380     case Kind.IfStatementNode:
 381       compLoc = checkLocationFromIfStatementNode(md, nametable, (IfStatementNode) bsn, constraint);
 382       break;
 383
 384     case Kind.LoopNode:
 385       compLoc = checkLocationFromLoopNode(md, nametable, (LoopNode) bsn, constraint);
 386       break;
 387
 388     case Kind.ReturnNode:
 389       compLoc = checkLocationFromReturnNode(md, nametable, (ReturnNode) bsn, constraint);
 390       break;
 391
 392     case Kind.SubBlockNode:
 393       compLoc = checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn, constraint);
 394       break;
 395
 396     case Kind.ContinueBreakNode:
 397       compLoc = new CompositeLocation();
 398       break;
 399
 400     case Kind.SwitchStatementNode:
 401       compLoc =
 402           checkLocationFromSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn, constraint);
 403
 404     }
 405     return compLoc;
 406   }
 407
 408   private CompositeLocation checkLocationFromSwitchStatementNode(MethodDescriptor md,
 409       SymbolTable nametable, SwitchStatementNode ssn, CompositeLocation constraint) {
 410
 411     ClassDescriptor cd = md.getClassDesc();
 412     CompositeLocation condLoc =
 413         checkLocationFromExpressionNode(md, nametable, ssn.getCondition(), new CompositeLocation(),
 414             constraint, false);
 415     BlockNode sbn = ssn.getSwitchBody();
 416
 417     Set<CompositeLocation> blockLocSet = new HashSet<CompositeLocation>();
 418     for (int i = 0; i < sbn.size(); i++) {
 419       CompositeLocation blockLoc =
 420           checkLocationFromSwitchBlockNode(md, nametable, (SwitchBlockNode) sbn.get(i), constraint);
 421       if (!CompositeLattice.isGreaterThan(condLoc, blockLoc,
 422           generateErrorMessage(cd, ssn.getCondition()))) {
 423         throw new Error(
 424             "The location of the switch-condition statement is lower than the conditional body at "
 425                 + cd.getSourceFileName() + ":" + ssn.getCondition().getNumLine());
 426       }
 427
 428       blockLocSet.add(blockLoc);
 429     }
 430     return CompositeLattice.calculateGLB(blockLocSet);
 431   }
 432
 433   private CompositeLocation checkLocationFromSwitchBlockNode(MethodDescriptor md,
 434       SymbolTable nametable, SwitchBlockNode sbn, CompositeLocation constraint) {
 435
 436     CompositeLocation blockLoc =
 437         checkLocationFromBlockNode(md, nametable, sbn.getSwitchBlockStatement(), constraint);
 438
 439     return blockLoc;
 440
 441   }
 442
 443   private CompositeLocation checkLocationFromReturnNode(MethodDescriptor md, SymbolTable nametable,
 444       ReturnNode rn, CompositeLocation constraint) {
 445
 446     ExpressionNode returnExp = rn.getReturnExpression();
 447
 448     CompositeLocation returnValueLoc;
 449     if (returnExp != null) {
 450       returnValueLoc =
 451           checkLocationFromExpressionNode(md, nametable, returnExp, new CompositeLocation(),
 452               constraint, false);
 453
 454       // check if return value is equal or higher than RETRUNLOC of method
 455       // declaration annotation
 456       CompositeLocation declaredReturnLoc = md2ReturnLoc.get(md);
 457
 458       int compareResult =
 459           CompositeLattice.compare(returnValueLoc, declaredReturnLoc,
 460               generateErrorMessage(md.getClassDesc(), rn));
 461
 462       if (compareResult == ComparisonResult.LESS || compareResult == ComparisonResult.INCOMPARABLE) {
 463         throw new Error(
 464             "Return value location is not equal or higher than the declaraed return location at "
 465                 + md.getClassDesc().getSourceFileName() + "::" + rn.getNumLine());
 466       }
 467     }
 468
 469     return new CompositeLocation();
 470   }
 471
 472   private boolean hasOnlyLiteralValue(ExpressionNode en) {
 473     if (en.kind() == Kind.LiteralNode) {
 474       return true;
 475     } else {
 476       return false;
 477     }
 478   }
 479
 480   private CompositeLocation checkLocationFromLoopNode(MethodDescriptor md, SymbolTable nametable,
 481       LoopNode ln, CompositeLocation constraint) {
 482
 483     ClassDescriptor cd = md.getClassDesc();
 484     if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) {
 485
 486       CompositeLocation condLoc =
 487           checkLocationFromExpressionNode(md, nametable, ln.getCondition(),
 488               new CompositeLocation(), constraint, false);
 489       addLocationType(ln.getCondition().getType(), (condLoc));
 490
 491       constraint = generateNewConstraint(constraint, condLoc);
 492       checkLocationFromBlockNode(md, nametable, ln.getBody(), constraint);
 493
 494       return new CompositeLocation();
 495
 496     } else {
 497       // check 'for loop' case
 498       BlockNode bn = ln.getInitializer();
 499       bn.getVarTable().setParent(nametable);
 500
 501       // calculate glb location of condition and update statements
 502       CompositeLocation condLoc =
 503           checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(),
 504               new CompositeLocation(), constraint, false);
 505       addLocationType(ln.getCondition().getType(), condLoc);
 506
 507       constraint = generateNewConstraint(constraint, condLoc);
 508
 509       checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate(), constraint);
 510       checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody(), constraint);
 511
 512       return new CompositeLocation();
 513
 514     }
 515
 516   }
 517
 518   private CompositeLocation checkLocationFromSubBlockNode(MethodDescriptor md,
 519       SymbolTable nametable, SubBlockNode sbn, CompositeLocation constraint) {
 520     CompositeLocation compLoc =
 521         checkLocationFromBlockNode(md, nametable, sbn.getBlockNode(), constraint);
 522     return compLoc;
 523   }
 524
 525   private CompositeLocation generateNewConstraint(CompositeLocation currentCon,
 526       CompositeLocation newCon) {
 527
 528     if (currentCon == null) {
 529       return newCon;
 530     } else {
 531       // compute GLB of current constraint and new constraint
 532       Set<CompositeLocation> inputSet = new HashSet<CompositeLocation>();
 533       inputSet.add(currentCon);
 534       inputSet.add(newCon);
 535       return CompositeLattice.calculateGLB(inputSet);
 536     }
 537
 538   }
 539
 540   private CompositeLocation checkLocationFromIfStatementNode(MethodDescriptor md,
 541       SymbolTable nametable, IfStatementNode isn, CompositeLocation constraint) {
 542
 543     CompositeLocation condLoc =
 544         checkLocationFromExpressionNode(md, nametable, isn.getCondition(), new CompositeLocation(),
 545             constraint, false);
 546
 547     addLocationType(isn.getCondition().getType(), condLoc);
 548
 549     constraint = generateNewConstraint(constraint, condLoc);
 550     checkLocationFromBlockNode(md, nametable, isn.getTrueBlock(), constraint);
 551
 552     if (isn.getFalseBlock() != null) {
 553       checkLocationFromBlockNode(md, nametable, isn.getFalseBlock(), constraint);
 554     }
 555
 556     return new CompositeLocation();
 557   }
 558
 559   private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md,
 560       SymbolTable nametable, DeclarationNode dn, CompositeLocation constraint) {
 561
 562     VarDescriptor vd = dn.getVarDescriptor();
 563
 564     CompositeLocation destLoc = d2loc.get(vd);
 565
 566     if (dn.getExpression() != null) {
 567       CompositeLocation expressionLoc =
 568           checkLocationFromExpressionNode(md, nametable, dn.getExpression(),
 569               new CompositeLocation(), constraint, false);
 570       // addTypeLocation(dn.getExpression().getType(), expressionLoc);
 571
 572       if (expressionLoc != null) {
 573         // checking location order
 574         if (!CompositeLattice.isGreaterThan(expressionLoc, destLoc,
 575             generateErrorMessage(md.getClassDesc(), dn))) {
 576           throw new Error("The value flow from " + expressionLoc + " to " + destLoc
 577               + " does not respect location hierarchy on the assignment " + dn.printNode(0)
 578               + " at " + md.getClassDesc().getSourceFileName() + "::" + dn.getNumLine());
 579         }
 580       }
 581       return expressionLoc;
 582
 583     } else {
 584
 585       return new CompositeLocation();
 586
 587     }
 588
 589   }
 590
 591   private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable,
 592       SubBlockNode sbn) {
 593     checkDeclarationInBlockNode(md, nametable.getParent(), sbn.getBlockNode());
 594   }
 595
 596   private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md,
 597       SymbolTable nametable, BlockExpressionNode ben, CompositeLocation constraint) {
 598     CompositeLocation compLoc =
 599         checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null, constraint, false);
 600     // addTypeLocation(ben.getExpression().getType(), compLoc);
 601     return compLoc;
 602   }
 603
 604   private CompositeLocation checkLocationFromExpressionNode(MethodDescriptor md,
 605       SymbolTable nametable, ExpressionNode en, CompositeLocation loc,
 606       CompositeLocation constraint, boolean isLHS) {
 607
 608     CompositeLocation compLoc = null;
 609     switch (en.kind()) {
 610
 611     case Kind.AssignmentNode:
 612       compLoc =
 613           checkLocationFromAssignmentNode(md, nametable, (AssignmentNode) en, loc, constraint);
 614       break;
 615
 616     case Kind.FieldAccessNode:
 617       compLoc =
 618           checkLocationFromFieldAccessNode(md, nametable, (FieldAccessNode) en, loc, constraint);
 619       break;
 620
 621     case Kind.NameNode:
 622       compLoc = checkLocationFromNameNode(md, nametable, (NameNode) en, loc, constraint);
 623       break;
 624
 625     case Kind.OpNode:
 626       compLoc = checkLocationFromOpNode(md, nametable, (OpNode) en, constraint);
 627       break;
 628
 629     case Kind.CreateObjectNode:
 630       compLoc = checkLocationFromCreateObjectNode(md, nametable, (CreateObjectNode) en);
 631       break;
 632
 633     case Kind.ArrayAccessNode:
 634       compLoc =
 635           checkLocationFromArrayAccessNode(md, nametable, (ArrayAccessNode) en, constraint, isLHS);
 636       break;
 637
 638     case Kind.LiteralNode:
 639       compLoc = checkLocationFromLiteralNode(md, nametable, (LiteralNode) en, loc);
 640       break;
 641
 642     case Kind.MethodInvokeNode:
 643       compLoc =
 644           checkLocationFromMethodInvokeNode(md, nametable, (MethodInvokeNode) en, loc, constraint);
 645       break;
 646
 647     case Kind.TertiaryNode:
 648       compLoc = checkLocationFromTertiaryNode(md, nametable, (TertiaryNode) en, constraint);
 649       break;
 650
 651     case Kind.CastNode:
 652       compLoc = checkLocationFromCastNode(md, nametable, (CastNode) en, constraint);
 653       break;
 654
 655     // case Kind.InstanceOfNode:
 656     // checkInstanceOfNode(md, nametable, (InstanceOfNode) en, td);
 657     // return null;
 658
 659     // case Kind.ArrayInitializerNode:
 660     // checkArrayInitializerNode(md, nametable, (ArrayInitializerNode) en,
 661     // td);
 662     // return null;
 663
 664     // case Kind.ClassTypeNode:
 665     // checkClassTypeNode(md, nametable, (ClassTypeNode) en, td);
 666     // return null;
 667
 668     // case Kind.OffsetNode:
 669     // checkOffsetNode(md, nametable, (OffsetNode)en, td);
 670     // return null;
 671
 672     default:
 673       return null;
 674
 675     }
 676     // addTypeLocation(en.getType(), compLoc);
 677     return compLoc;
 678
 679   }
 680
 681   private CompositeLocation checkLocationFromCastNode(MethodDescriptor md, SymbolTable nametable,
 682       CastNode cn, CompositeLocation constraint) {
 683
 684     ExpressionNode en = cn.getExpression();
 685     return checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
 686         false);
 687
 688   }
 689
 690   private CompositeLocation checkLocationFromTertiaryNode(MethodDescriptor md,
 691       SymbolTable nametable, TertiaryNode tn, CompositeLocation constraint) {
 692     ClassDescriptor cd = md.getClassDesc();
 693
 694     CompositeLocation condLoc =
 695         checkLocationFromExpressionNode(md, nametable, tn.getCond(), new CompositeLocation(),
 696             constraint, false);
 697     addLocationType(tn.getCond().getType(), condLoc);
 698     CompositeLocation trueLoc =
 699         checkLocationFromExpressionNode(md, nametable, tn.getTrueExpr(), new CompositeLocation(),
 700             constraint, false);
 701     addLocationType(tn.getTrueExpr().getType(), trueLoc);
 702     CompositeLocation falseLoc =
 703         checkLocationFromExpressionNode(md, nametable, tn.getFalseExpr(), new CompositeLocation(),
 704             constraint, false);
 705     addLocationType(tn.getFalseExpr().getType(), falseLoc);
 706
 707     // locations from true/false branches can be TOP when there are only literal
 708     // values
 709     // in this case, we don't need to check flow down rule!
 710
 711     // check if condLoc is higher than trueLoc & falseLoc
 712     if (!trueLoc.get(0).isTop()
 713         && !CompositeLattice.isGreaterThan(condLoc, trueLoc, generateErrorMessage(cd, tn))) {
 714       throw new Error(
 715           "The location of the condition expression is lower than the true expression at "
 716               + cd.getSourceFileName() + ":" + tn.getCond().getNumLine());
 717     }
 718
 719     if (!falseLoc.get(0).isTop()
 720         && !CompositeLattice.isGreaterThan(condLoc, falseLoc,
 721             generateErrorMessage(cd, tn.getCond()))) {
 722       throw new Error(
 723           "The location of the condition expression is lower than the true expression at "
 724               + cd.getSourceFileName() + ":" + tn.getCond().getNumLine());
 725     }
 726
 727     // then, return glb of trueLoc & falseLoc
 728     Set<CompositeLocation> glbInputSet = new HashSet<CompositeLocation>();
 729     glbInputSet.add(trueLoc);
 730     glbInputSet.add(falseLoc);
 731
 732     return CompositeLattice.calculateGLB(glbInputSet);
 733   }
 734
 735   private CompositeLocation checkLocationFromMethodInvokeNode(MethodDescriptor md,
 736       SymbolTable nametable, MethodInvokeNode min, CompositeLocation loc,
 737       CompositeLocation constraint) {
 738
 739     checkCalleeConstraints(md, nametable, min, constraint);
 740
 741     CompositeLocation baseLocation = null;
 742     if (min.getExpression() != null) {
 743       baseLocation =
 744           checkLocationFromExpressionNode(md, nametable, min.getExpression(),
 745               new CompositeLocation(), constraint, false);
 746     } else {
 747       String thisLocId = ssjava.getMethodLattice(md).getThisLoc();
 748       baseLocation = new CompositeLocation(new Location(md, thisLocId));
 749     }
 750
 751     if (!min.getMethod().getReturnType().isVoid()) {
 752       // If method has a return value, compute the highest possible return
 753       // location in the caller's perspective
 754       CompositeLocation ceilingLoc =
 755           computeCeilingLocationForCaller(md, nametable, min, baseLocation, constraint);
 756       return ceilingLoc;
 757     }
 758
 759     return new CompositeLocation();
 760
 761   }
 762
 763   private CompositeLocation computeCeilingLocationForCaller(MethodDescriptor md,
 764       SymbolTable nametable, MethodInvokeNode min, CompositeLocation baseLocation,
 765       CompositeLocation constraint) {
 766     List<CompositeLocation> argList = new ArrayList<CompositeLocation>();
 767
 768     // by default, method has a THIS parameter
 769     argList.add(baseLocation);
 770
 771     for (int i = 0; i < min.numArgs(); i++) {
 772       ExpressionNode en = min.getArg(i);
 773       CompositeLocation callerArg =
 774           checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
 775               false);
 776       argList.add(callerArg);
 777     }
 778
 779     System.out.println("\n## computeReturnLocation=" + min.getMethod() + " argList=" + argList);
 780     CompositeLocation compLoc = md2ReturnLocGen.get(min.getMethod()).computeReturnLocation(argList);
 781     DeltaLocation delta = new DeltaLocation(compLoc, 1);
 782     System.out.println("##computeReturnLocation=" + delta);
 783
 784     return delta;
 785
 786   }
 787
 788   private void checkCalleeConstraints(MethodDescriptor md, SymbolTable nametable,
 789       MethodInvokeNode min, CompositeLocation constraint) {
 790
 791     if (min.numArgs() > 1) {
 792       // caller needs to guarantee that it passes arguments in regarding to
 793       // callee's hierarchy
 794       for (int i = 0; i < min.numArgs(); i++) {
 795         ExpressionNode en = min.getArg(i);
 796         CompositeLocation callerArg1 =
 797             checkLocationFromExpressionNode(md, nametable, en, new CompositeLocation(), constraint,
 798                 false);
 799
 800         VarDescriptor calleevd = (VarDescriptor) min.getMethod().getParameter(i);
 801         CompositeLocation calleeLoc1 = d2loc.get(calleevd);
 802
 803         if (!callerArg1.get(0).isTop()) {
 804           // here, check if ordering relations among caller's args respect
 805           // ordering relations in-between callee's args
 806           for (int currentIdx = 0; currentIdx < min.numArgs(); currentIdx++) {
 807             if (currentIdx != i) { // skip itself
 808               ExpressionNode argExp = min.getArg(currentIdx);
 809
 810               CompositeLocation callerArg2 =
 811                   checkLocationFromExpressionNode(md, nametable, argExp, new CompositeLocation(),
 812                       constraint, false);
 813
 814               VarDescriptor calleevd2 = (VarDescriptor) min.getMethod().getParameter(currentIdx);
 815               CompositeLocation calleeLoc2 = d2loc.get(calleevd2);
 816
 817               int callerResult =
 818                   CompositeLattice.compare(callerArg1, callerArg2,
 819                       generateErrorMessage(md.getClassDesc(), min));
 820               int calleeResult =
 821                   CompositeLattice.compare(calleeLoc1, calleeLoc2,
 822                       generateErrorMessage(md.getClassDesc(), min));
 823
 824               if (calleeResult == ComparisonResult.GREATER
 825                   && callerResult != ComparisonResult.GREATER) {
 826                 // If calleeLoc1 is higher than calleeLoc2
 827                 // then, caller should have same ordering relation in-bet
 828                 // callerLoc1 & callerLoc2
 829
 830                 throw new Error("Caller doesn't respect ordering relations among method arguments:"
 831                     + md.getClassDesc().getSourceFileName() + ":" + min.getNumLine());
 832               }
 833
 834             }
 835           }
 836         }
 837
 838       }
 839
 840     }
 841
 842   }
 843
 844   private CompositeLocation checkLocationFromArrayAccessNode(MethodDescriptor md,
 845       SymbolTable nametable, ArrayAccessNode aan, CompositeLocation constraint, boolean isLHS) {
 846
 847     ClassDescriptor cd = md.getClassDesc();
 848
 849     CompositeLocation arrayLoc =
 850         checkLocationFromExpressionNode(md, nametable, aan.getExpression(),
 851             new CompositeLocation(), constraint, isLHS);
 852     // addTypeLocation(aan.getExpression().getType(), arrayLoc);
 853     CompositeLocation indexLoc =
 854         checkLocationFromExpressionNode(md, nametable, aan.getIndex(), new CompositeLocation(),
 855             constraint, isLHS);
 856     // addTypeLocation(aan.getIndex().getType(), indexLoc);
 857
 858     if (isLHS) {
 859       if (!CompositeLattice.isGreaterThan(indexLoc, arrayLoc, generateErrorMessage(cd, aan))) {
 860         throw new Error("Array index value is not higher than array location at "
 861             + generateErrorMessage(cd, aan));
 862       }
 863       return arrayLoc;
 864     } else {
 865       Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
 866       inputGLB.add(arrayLoc);
 867       inputGLB.add(indexLoc);
 868       return CompositeLattice.calculateGLB(inputGLB);
 869     }
 870
 871   }
 872
 873   private CompositeLocation checkLocationFromCreateObjectNode(MethodDescriptor md,
 874       SymbolTable nametable, CreateObjectNode con) {
 875
 876     ClassDescriptor cd = md.getClassDesc();
 877
 878     CompositeLocation compLoc = new CompositeLocation();
 879     compLoc.addLocation(Location.createTopLocation(md));
 880     return compLoc;
 881
 882   }
 883
 884   private CompositeLocation checkLocationFromOpNode(MethodDescriptor md, SymbolTable nametable,
 885       OpNode on, CompositeLocation constraint) {
 886
 887     ClassDescriptor cd = md.getClassDesc();
 888     CompositeLocation leftLoc = new CompositeLocation();
 889     leftLoc =
 890         checkLocationFromExpressionNode(md, nametable, on.getLeft(), leftLoc, constraint, false);
 891     // addTypeLocation(on.getLeft().getType(), leftLoc);
 892
 893     CompositeLocation rightLoc = new CompositeLocation();
 894     if (on.getRight() != null) {
 895       rightLoc =
 896           checkLocationFromExpressionNode(md, nametable, on.getRight(), rightLoc, constraint, false);
 897       // addTypeLocation(on.getRight().getType(), rightLoc);
 898     }
 899
 900     System.out.println("checking op node=" + on.printNode(0)
 901         + generateErrorMessage(md.getClassDesc(), on));
 902     System.out.println("# op node=" + on.printNode(0));
 903     System.out.println("left loc=" + leftLoc + " from " + on.getLeft().getClass());
 904     if (on.getRight() != null) {
 905       System.out.println("right loc=" + rightLoc + " from " + on.getRight().kind());
 906     }
 907
 908     Operation op = on.getOp();
 909
 910     switch (op.getOp()) {
 911
 912     case Operation.UNARYPLUS:
 913     case Operation.UNARYMINUS:
 914     case Operation.LOGIC_NOT:
 915       // single operand
 916       return leftLoc;
 917
 918     case Operation.LOGIC_OR:
 919     case Operation.LOGIC_AND:
 920     case Operation.COMP:
 921     case Operation.BIT_OR:
 922     case Operation.BIT_XOR:
 923     case Operation.BIT_AND:
 924     case Operation.ISAVAILABLE:
 925     case Operation.EQUAL:
 926     case Operation.NOTEQUAL:
 927     case Operation.LT:
 928     case Operation.GT:
 929     case Operation.LTE:
 930     case Operation.GTE:
 931     case Operation.ADD:
 932     case Operation.SUB:
 933     case Operation.MULT:
 934     case Operation.DIV:
 935     case Operation.MOD:
 936     case Operation.LEFTSHIFT:
 937     case Operation.RIGHTSHIFT:
 938     case Operation.URIGHTSHIFT:
 939
 940       Set<CompositeLocation> inputSet = new HashSet<CompositeLocation>();
 941       inputSet.add(leftLoc);
 942       inputSet.add(rightLoc);
 943       CompositeLocation glbCompLoc = CompositeLattice.calculateGLB(inputSet);
 944       return glbCompLoc;
 945
 946     default:
 947       throw new Error(op.toString());
 948     }
 949
 950   }
 951
 952   private CompositeLocation checkLocationFromLiteralNode(MethodDescriptor md,
 953       SymbolTable nametable, LiteralNode en, CompositeLocation loc) {
 954
 955     // literal value has the top location so that value can be flowed into any
 956     // location
 957     Location literalLoc = Location.createTopLocation(md);
 958     loc.addLocation(literalLoc);
 959     return loc;
 960
 961   }
 962
 963   private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable,
 964       NameNode nn, CompositeLocation loc, CompositeLocation constraint) {
 965
 966     NameDescriptor nd = nn.getName();
 967     if (nd.getBase() != null) {
 968       loc =
 969           checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc, constraint, false);
 970     } else {
 971       String varname = nd.toString();
 972       if (varname.equals("this")) {
 973         // 'this' itself!
 974         MethodLattice<String> methodLattice = ssjava.getMethodLattice(md);
 975         String thisLocId = methodLattice.getThisLoc();
 976         if (thisLocId == null) {
 977           throw new Error("The location for 'this' is not defined at "
 978               + md.getClassDesc().getSourceFileName() + "::" + nn.getNumLine());
 979         }
 980         Location locElement = new Location(md, thisLocId);
 981         loc.addLocation(locElement);
 982         return loc;
 983       }
 984
 985       Descriptor d = (Descriptor) nametable.get(varname);
 986
 987       // CompositeLocation localLoc = null;
 988       if (d instanceof VarDescriptor) {
 989         VarDescriptor vd = (VarDescriptor) d;
 990         // localLoc = d2loc.get(vd);
 991         // the type of var descriptor has a composite location!
 992         loc = ((CompositeLocation) vd.getType().getExtension()).clone();
 993       } else if (d instanceof FieldDescriptor) {
 994         // the type of field descriptor has a location!
 995         FieldDescriptor fd = (FieldDescriptor) d;
 996         if (fd.isStatic()) {
 997           if (fd.isFinal()) {
 998             // if it is 'static final', the location has TOP since no one can
 999             // change its value
1000             loc.addLocation(Location.createTopLocation(md));
1001             return loc;
1002           } else {
1003             // if 'static', the location has pre-assigned global loc
1004             MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
1005             String globalLocId = localLattice.getGlobalLoc();
1006             if (globalLocId == null) {
1007               throw new Error("Global location element is not defined in the method " + md);
1008             }
1009             Location globalLoc = new Location(md, globalLocId);
1010
1011             loc.addLocation(globalLoc);
1012           }
1013         } else {
1014           // the location of field access starts from this, followed by field
1015           // location
1016           MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
1017           Location thisLoc = new Location(md, localLattice.getThisLoc());
1018           loc.addLocation(thisLoc);
1019         }
1020
1021         Location fieldLoc = (Location) fd.getType().getExtension();
1022         loc.addLocation(fieldLoc);
1023       } else if (d == null) {
1024
1025         // check if the var is a static field of the class
1026         FieldDescriptor fd = nn.getField();
1027         ClassDescriptor cd = nn.getClassDesc();
1028
1029         if (fd != null && cd != null) {
1030
1031           if (fd.isStatic() && fd.isFinal()) {
1032             loc.addLocation(Location.createTopLocation(md));
1033             return loc;
1034           } else {
1035             MethodLattice<String> localLattice = ssjava.getMethodLattice(md);
1036             Location fieldLoc = new Location(md, localLattice.getThisLoc());
1037             loc.addLocation(fieldLoc);
1038           }
1039         }
1040
1041       }
1042     }
1043     return loc;
1044   }
1045
1046   private CompositeLocation checkLocationFromFieldAccessNode(MethodDescriptor md,
1047       SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc,
1048       CompositeLocation constraint) {
1049
1050     ExpressionNode left = fan.getExpression();
1051     TypeDescriptor ltd = left.getType();
1052
1053     FieldDescriptor fd = fan.getField();
1054
1055     String varName = null;
1056     if (left.kind() == Kind.NameNode) {
1057       NameDescriptor nd = ((NameNode) left).getName();
1058       varName = nd.toString();
1059     }
1060
1061     if (ltd.isClassNameRef() || (varName != null && varName.equals("this"))) {
1062       // using a class name directly or access using this
1063       if (fd.isStatic() && fd.isFinal()) {
1064         loc.addLocation(Location.createTopLocation(md));
1065         return loc;
1066       }
1067     }
1068
1069     loc = checkLocationFromExpressionNode(md, nametable, left, loc, constraint, false);
1070     if (!left.getType().isPrimitive()) {
1071       Location fieldLoc = getFieldLocation(fd);
1072       loc.addLocation(fieldLoc);
1073     }
1074
1075     return loc;
1076   }
1077
1078   private Location getFieldLocation(FieldDescriptor fd) {
1079
1080     Location fieldLoc = (Location) fd.getType().getExtension();
1081
1082     // handle the case that method annotation checking skips checking field
1083     // declaration
1084     if (fieldLoc == null) {
1085       fieldLoc = checkFieldDeclaration(fd.getClassDescriptor(), fd);
1086     }
1087
1088     return fieldLoc;
1089
1090   }
1091
1092   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
1093       SymbolTable nametable, AssignmentNode an, CompositeLocation loc, CompositeLocation constraint) {
1094
1095     System.out.println("\n# ASSIGNMENTNODE=" + an.printNode(0));
1096
1097     ClassDescriptor cd = md.getClassDesc();
1098
1099     Set<CompositeLocation> inputGLBSet = new HashSet<CompositeLocation>();
1100
1101     boolean postinc = true;
1102     if (an.getOperation().getBaseOp() == null
1103         || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation()
1104             .getBaseOp().getOp() != Operation.POSTDEC))
1105       postinc = false;
1106
1107     // if LHS is array access node, need to check if array index is higher
1108     // than array itself
1109     CompositeLocation destLocation =
1110         checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(),
1111             constraint, true);
1112
1113     CompositeLocation rhsLocation;
1114     CompositeLocation srcLocation;
1115
1116     if (!postinc) {
1117       rhsLocation =
1118           checkLocationFromExpressionNode(md, nametable, an.getSrc(), new CompositeLocation(),
1119               constraint, false);
1120
1121       System.out.println("dstLocation=" + destLocation);
1122       System.out.println("rhsLocation=" + rhsLocation);
1123       System.out.println("constraint=" + constraint);
1124
1125       if (constraint != null) {
1126         inputGLBSet.add(rhsLocation);
1127         inputGLBSet.add(constraint);
1128         srcLocation = CompositeLattice.calculateGLB(inputGLBSet);
1129       } else {
1130         srcLocation = rhsLocation;
1131       }
1132
1133       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
1134         throw new Error("The value flow from " + srcLocation + " to " + destLocation
1135             + " does not respect location hierarchy on the assignment " + an.printNode(0) + " at "
1136             + cd.getSourceFileName() + "::" + an.getNumLine());
1137       }
1138
1139     } else {
1140       destLocation =
1141           rhsLocation =
1142               checkLocationFromExpressionNode(md, nametable, an.getDest(), new CompositeLocation(),
1143                   constraint, false);
1144
1145       if (constraint != null) {
1146         inputGLBSet.add(rhsLocation);
1147         inputGLBSet.add(constraint);
1148         srcLocation = CompositeLattice.calculateGLB(inputGLBSet);
1149       } else {
1150         srcLocation = rhsLocation;
1151       }
1152
1153       if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, generateErrorMessage(cd, an))) {
1154         throw new Error("Location " + destLocation
1155             + " is not allowed to have the value flow that moves within the same location at "
1156             + cd.getSourceFileName() + "::" + an.getNumLine());
1157       }
1158
1159     }
1160
1161     return destLocation;
1162   }
1163
1164   private void assignLocationOfVarDescriptor(VarDescriptor vd, MethodDescriptor md,
1165       SymbolTable nametable, TreeNode n) {
1166
1167     ClassDescriptor cd = md.getClassDesc();
1168     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
1169
1170     // currently enforce every variable to have corresponding location
1171     if (annotationVec.size() == 0) {
1172       throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
1173           + md.getSymbol() + " of the class " + cd.getSymbol());
1174     }
1175
1176     if (annotationVec.size() > 1) { // variable can have at most one location
1177       throw new Error(vd.getSymbol() + " has more than one location.");
1178     }
1179
1180     AnnotationDescriptor ad = annotationVec.elementAt(0);
1181
1182     if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
1183
1184       if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
1185         String locDec = ad.getValue(); // check if location is defined
1186
1187         if (locDec.startsWith(SSJavaAnalysis.DELTA)) {
1188           DeltaLocation deltaLoc = parseDeltaDeclaration(md, n, locDec);
1189           d2loc.put(vd, deltaLoc);
1190           addLocationType(vd.getType(), deltaLoc);
1191         } else {
1192           CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
1193
1194           Location lastElement = compLoc.get(compLoc.getSize() - 1);
1195           if (ssjava.isSharedLocation(lastElement)) {
1196             ssjava.mapSharedLocation2Descriptor(lastElement, vd);
1197           }
1198
1199           d2loc.put(vd, compLoc);
1200           addLocationType(vd.getType(), compLoc);
1201         }
1202
1203       }
1204     }
1205
1206   }
1207
1208   private DeltaLocation parseDeltaDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
1209
1210     int deltaCount = 0;
1211     int dIdx = locDec.indexOf(SSJavaAnalysis.DELTA);
1212     while (dIdx >= 0) {
1213       deltaCount++;
1214       int beginIdx = dIdx + 6;
1215       locDec = locDec.substring(beginIdx, locDec.length() - 1);
1216       dIdx = locDec.indexOf(SSJavaAnalysis.DELTA);
1217     }
1218
1219     CompositeLocation compLoc = parseLocationDeclaration(md, n, locDec);
1220     DeltaLocation deltaLoc = new DeltaLocation(compLoc, deltaCount);
1221
1222     return deltaLoc;
1223   }
1224
1225   private Location parseFieldLocDeclaraton(String decl, String msg) {
1226
1227     int idx = decl.indexOf(".");
1228     String className = decl.substring(0, idx);
1229     String fieldName = decl.substring(idx + 1);
1230
1231     className.replaceAll(" ", "");
1232     fieldName.replaceAll(" ", "");
1233
1234     Descriptor d = state.getClassSymbolTable().get(className);
1235
1236     if (d == null) {
1237       throw new Error("The class in the location declaration '" + decl + "' does not exist at "
1238           + msg);
1239     }
1240
1241     assert (d instanceof ClassDescriptor);
1242     SSJavaLattice<String> lattice = ssjava.getClassLattice((ClassDescriptor) d);
1243     if (!lattice.containsKey(fieldName)) {
1244       throw new Error("The location " + fieldName + " is not defined in the field lattice of '"
1245           + className + "' at " + msg);
1246     }
1247
1248     return new Location(d, fieldName);
1249   }
1250
1251   private CompositeLocation parseLocationDeclaration(MethodDescriptor md, TreeNode n, String locDec) {
1252
1253     CompositeLocation compLoc = new CompositeLocation();
1254
1255     StringTokenizer tokenizer = new StringTokenizer(locDec, ",");
1256     List<String> locIdList = new ArrayList<String>();
1257     while (tokenizer.hasMoreTokens()) {
1258       String locId = tokenizer.nextToken();
1259       locIdList.add(locId);
1260     }
1261
1262     // at least,one location element needs to be here!
1263     assert (locIdList.size() > 0);
1264
1265     // assume that loc with idx 0 comes from the local lattice
1266     // loc with idx 1 comes from the field lattice
1267
1268     String localLocId = locIdList.get(0);
1269     SSJavaLattice<String> localLattice = CompositeLattice.getLatticeByDescriptor(md);
1270     Location localLoc = new Location(md, localLocId);
1271     if (localLattice == null || (!localLattice.containsKey(localLocId))) {
1272       throw new Error("Location " + localLocId
1273           + " is not defined in the local variable lattice at "
1274           + md.getClassDesc().getSourceFileName() + "::" + (n != null ? n.getNumLine() : "") + ".");
1275     }
1276     compLoc.addLocation(localLoc);
1277
1278     for (int i = 1; i < locIdList.size(); i++) {
1279       String locName = locIdList.get(i);
1280
1281       Location fieldLoc =
1282           parseFieldLocDeclaraton(locName, generateErrorMessage(md.getClassDesc(), n));
1283       // ClassDescriptor cd = fieldLocName2cd.get(locName);
1284       // SSJavaLattice<String> fieldLattice =
1285       // CompositeLattice.getLatticeByDescriptor(cd);
1286       //
1287       // if (fieldLattice == null || (!fieldLattice.containsKey(locName))) {
1288       // throw new Error("Location " + locName +
1289       // " is not defined in the field lattice at "
1290       // + cd.getSourceFileName() + ".");
1291       // }
1292       // Location fieldLoc = new Location(cd, locName);
1293       compLoc.addLocation(fieldLoc);
1294     }
1295
1296     return compLoc;
1297
1298   }
1299
1300   private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) {
1301     VarDescriptor vd = dn.getVarDescriptor();
1302     assignLocationOfVarDescriptor(vd, md, nametable, dn);
1303   }
1304
1305   private void checkDeclarationInClass(ClassDescriptor cd) {
1306     // Check to see that fields are okay
1307     for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
1308       FieldDescriptor fd = (FieldDescriptor) field_it.next();
1309
1310       if (!(fd.isFinal() && fd.isStatic())) {
1311         checkFieldDeclaration(cd, fd);
1312       } else {
1313         // for static final, assign top location by default
1314         Location loc = Location.createTopLocation(cd);
1315         addLocationType(fd.getType(), loc);
1316       }
1317     }
1318   }
1319
1320   private Location checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
1321
1322     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
1323
1324     // currently enforce every field to have corresponding location
1325     if (annotationVec.size() == 0) {
1326       throw new Error("Location is not assigned to the field '" + fd.getSymbol()
1327           + "' of the class " + cd.getSymbol() + " at " + cd.getSourceFileName());
1328     }
1329
1330     if (annotationVec.size() > 1) {
1331       // variable can have at most one location
1332       throw new Error("Field " + fd.getSymbol() + " of class " + cd
1333           + " has more than one location.");
1334     }
1335
1336     AnnotationDescriptor ad = annotationVec.elementAt(0);
1337     Location loc = null;
1338
1339     if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
1340       if (ad.getMarker().equals(SSJavaAnalysis.LOC)) {
1341         String locationID = ad.getValue();
1342         // check if location is defined
1343         SSJavaLattice<String> lattice = ssjava.getClassLattice(cd);
1344         if (lattice == null || (!lattice.containsKey(locationID))) {
1345           throw new Error("Location " + locationID
1346               + " is not defined in the field lattice of class " + cd.getSymbol() + " at"
1347               + cd.getSourceFileName() + ".");
1348         }
1349         loc = new Location(cd, locationID);
1350
1351         if (ssjava.isSharedLocation(loc)) {
1352           ssjava.mapSharedLocation2Descriptor(loc, fd);
1353         }
1354
1355         addLocationType(fd.getType(), loc);
1356
1357       }
1358     }
1359
1360     return loc;
1361   }
1362
1363   private void addLocationType(TypeDescriptor type, CompositeLocation loc) {
1364     if (type != null) {
1365       type.setExtension(loc);
1366     }
1367   }
1368
1369   private void addLocationType(TypeDescriptor type, Location loc) {
1370     if (type != null) {
1371       type.setExtension(loc);
1372     }
1373   }
1374
1375   static class CompositeLattice {
1376
1377     public static boolean isGreaterThan(CompositeLocation loc1, CompositeLocation loc2, String msg) {
1378
1379       System.out.println("isGreaterThan=" + loc1 + " " + loc2 + " msg=" + msg);
1380       int baseCompareResult = compareBaseLocationSet(loc1, loc2, true, msg);
1381       if (baseCompareResult == ComparisonResult.EQUAL) {
1382         if (compareDelta(loc1, loc2) == ComparisonResult.GREATER) {
1383           return true;
1384         } else {
1385           return false;
1386         }
1387       } else if (baseCompareResult == ComparisonResult.GREATER) {
1388         return true;
1389       } else {
1390         return false;
1391       }
1392
1393     }
1394
1395     public static int compare(CompositeLocation loc1, CompositeLocation loc2, String msg) {
1396
1397       System.out.println("compare=" + loc1 + " " + loc2);
1398       int baseCompareResult = compareBaseLocationSet(loc1, loc2, false, msg);
1399
1400       if (baseCompareResult == ComparisonResult.EQUAL) {
1401         return compareDelta(loc1, loc2);
1402       } else {
1403         return baseCompareResult;
1404       }
1405
1406     }
1407
1408     private static int compareDelta(CompositeLocation dLoc1, CompositeLocation dLoc2) {
1409
1410       int deltaCount1 = 0;
1411       int deltaCount2 = 0;
1412       if (dLoc1 instanceof DeltaLocation) {
1413         deltaCount1 = ((DeltaLocation) dLoc1).getNumDelta();
1414       }
1415
1416       if (dLoc2 instanceof DeltaLocation) {
1417         deltaCount2 = ((DeltaLocation) dLoc2).getNumDelta();
1418       }
1419       if (deltaCount1 < deltaCount2) {
1420         return ComparisonResult.GREATER;
1421       } else if (deltaCount1 == deltaCount2) {
1422         return ComparisonResult.EQUAL;
1423       } else {
1424         return ComparisonResult.LESS;
1425       }
1426
1427     }
1428
1429     private static int compareBaseLocationSet(CompositeLocation compLoc1,
1430         CompositeLocation compLoc2, boolean awareSharedLoc, String msg) {
1431
1432       // if compLoc1 is greater than compLoc2, return true
1433       // else return false;
1434
1435       // compare one by one in according to the order of the tuple
1436       int numOfTie = 0;
1437       for (int i = 0; i < compLoc1.getSize(); i++) {
1438         Location loc1 = compLoc1.get(i);
1439         if (i >= compLoc2.getSize()) {
1440           throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1441               + " because they are not comparable.");
1442         }
1443         Location loc2 = compLoc2.get(i);
1444
1445         Descriptor d1 = loc1.getDescriptor();
1446         Descriptor d2 = loc2.getDescriptor();
1447
1448         Descriptor descriptor;
1449
1450         if (d1 instanceof ClassDescriptor && d2 instanceof ClassDescriptor) {
1451
1452           if (d1.equals(d2)) {
1453             descriptor = d1;
1454           } else {
1455             // identifying which one is parent class
1456             Set<Descriptor> d1SubClassesSet = ssjava.tu.getSubClasses((ClassDescriptor) d1);
1457             Set<Descriptor> d2SubClassesSet = ssjava.tu.getSubClasses((ClassDescriptor) d2);
1458
1459             if (d1 == null && d2 == null) {
1460               throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1461                   + " because they are not comparable at " + msg);
1462             } else if (d1SubClassesSet != null && d1SubClassesSet.contains(d2)) {
1463               descriptor = d1;
1464             } else if (d2SubClassesSet != null && d2SubClassesSet.contains(d1)) {
1465               descriptor = d2;
1466             } else {
1467               throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1468                   + " because they are not comparable at " + msg);
1469             }
1470           }
1471
1472         } else if (d1 instanceof MethodDescriptor && d2 instanceof MethodDescriptor) {
1473
1474           if (d1.equals(d2)) {
1475             descriptor = d1;
1476           } else {
1477
1478             // identifying which one is parent class
1479             MethodDescriptor md1 = (MethodDescriptor) d1;
1480             MethodDescriptor md2 = (MethodDescriptor) d2;
1481
1482             if (!md1.matches(md2)) {
1483               throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1484                   + " because they are not comparable at " + msg);
1485             }
1486
1487             Set<Descriptor> d1SubClassesSet =
1488                 ssjava.tu.getSubClasses(((MethodDescriptor) d1).getClassDesc());
1489             Set<Descriptor> d2SubClassesSet =
1490                 ssjava.tu.getSubClasses(((MethodDescriptor) d2).getClassDesc());
1491
1492             if (d1 == null && d2 == null) {
1493               throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1494                   + " because they are not comparable at " + msg);
1495             } else if (d1 != null && d1SubClassesSet.contains(d2)) {
1496               descriptor = d1;
1497             } else if (d2 != null && d2SubClassesSet.contains(d1)) {
1498               descriptor = d2;
1499             } else {
1500               throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1501                   + " because they are not comparable at " + msg);
1502             }
1503           }
1504
1505         } else {
1506           throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1507               + " because they are not comparable at " + msg);
1508         }
1509
1510         // SSJavaLattice<String> lattice1 = getLatticeByDescriptor(d1);
1511         // SSJavaLattice<String> lattice2 = getLatticeByDescriptor(d2);
1512
1513         SSJavaLattice<String> lattice = getLatticeByDescriptor(descriptor);
1514
1515         // check if the spin location is appeared only at the end of the
1516         // composite location
1517         if (lattice.getSpinLocSet().contains(loc1.getLocIdentifier())) {
1518           if (i != (compLoc1.getSize() - 1)) {
1519             throw new Error("The shared location " + loc1.getLocIdentifier()
1520                 + " cannot be appeared in the middle of composite location at" + msg);
1521           }
1522         }
1523
1524         if (lattice.getSpinLocSet().contains(loc2.getLocIdentifier())) {
1525           if (i != (compLoc2.getSize() - 1)) {
1526             throw new Error("The spin location " + loc2.getLocIdentifier()
1527                 + " cannot be appeared in the middle of composite location at " + msg);
1528           }
1529         }
1530
1531         // if (!lattice1.equals(lattice2)) {
1532         // throw new Error("Failed to compare two locations of " + compLoc1 +
1533         // " and " + compLoc2
1534         // + " because they are not comparable at " + msg);
1535         // }
1536
1537         if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
1538           numOfTie++;
1539           // check if the current location is the spinning location
1540           // note that the spinning location only can be appeared in the last
1541           // part of the composite location
1542           if (awareSharedLoc && numOfTie == compLoc1.getSize()
1543               && lattice.getSpinLocSet().contains(loc1.getLocIdentifier())) {
1544             return ComparisonResult.GREATER;
1545           }
1546           continue;
1547         } else if (lattice.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
1548           return ComparisonResult.GREATER;
1549         } else {
1550           return ComparisonResult.LESS;
1551         }
1552
1553       }
1554
1555       if (numOfTie == compLoc1.getSize()) {
1556
1557         if (numOfTie != compLoc2.getSize()) {
1558           throw new Error("Failed to compare two locations of " + compLoc1 + " and " + compLoc2
1559               + " because they are not comparable at " + msg);
1560         }
1561
1562         return ComparisonResult.EQUAL;
1563       }
1564
1565       return ComparisonResult.LESS;
1566
1567     }
1568
1569     public static CompositeLocation calculateGLB(Set<CompositeLocation> inputSet) {
1570
1571       // System.out.println("Calculating GLB=" + inputSet);
1572       CompositeLocation glbCompLoc = new CompositeLocation();
1573
1574       // calculate GLB of the first(priority) element
1575       Set<String> priorityLocIdentifierSet = new HashSet<String>();
1576       Descriptor priorityDescriptor = null;
1577
1578       Hashtable<String, Set<CompositeLocation>> locId2CompLocSet =
1579           new Hashtable<String, Set<CompositeLocation>>();
1580       // mapping from the priority loc ID to its full representation by the
1581       // composite location
1582
1583       int maxTupleSize = 0;
1584       CompositeLocation maxCompLoc = null;
1585
1586       for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) {
1587         CompositeLocation compLoc = (CompositeLocation) iterator.next();
1588         if (compLoc.getSize() > maxTupleSize) {
1589           maxTupleSize = compLoc.getSize();
1590           maxCompLoc = compLoc;
1591         }
1592         Location priorityLoc = compLoc.get(0);
1593         String priorityLocId = priorityLoc.getLocIdentifier();
1594         priorityLocIdentifierSet.add(priorityLocId);
1595
1596         if (locId2CompLocSet.containsKey(priorityLocId)) {
1597           locId2CompLocSet.get(priorityLocId).add(compLoc);
1598         } else {
1599           Set<CompositeLocation> newSet = new HashSet<CompositeLocation>();
1600           newSet.add(compLoc);
1601           locId2CompLocSet.put(priorityLocId, newSet);
1602         }
1603
1604         // check if priority location are coming from the same lattice
1605         if (priorityDescriptor == null) {
1606           priorityDescriptor = priorityLoc.getDescriptor();
1607         } else if (!priorityDescriptor.equals(priorityLoc.getDescriptor())) {
1608           throw new Error("Failed to calculate GLB of " + inputSet
1609               + " because they are from different lattices.");
1610         }
1611       }
1612
1613       SSJavaLattice<String> locOrder = getLatticeByDescriptor(priorityDescriptor);
1614       String glbOfPriorityLoc = locOrder.getGLB(priorityLocIdentifierSet);
1615
1616       glbCompLoc.addLocation(new Location(priorityDescriptor, glbOfPriorityLoc));
1617       Set<CompositeLocation> compSet = locId2CompLocSet.get(glbOfPriorityLoc);
1618
1619       if (compSet == null) {
1620         // when GLB(x1,x2)!=x1 and !=x2 : GLB case 4
1621         // mean that the result is already lower than <x1,y1> and <x2,y2>
1622         // assign TOP to the rest of the location elements
1623
1624         // in this case, do not take care about delta
1625         // CompositeLocation inputComp = inputSet.iterator().next();
1626         for (int i = 1; i < maxTupleSize; i++) {
1627           glbCompLoc.addLocation(Location.createTopLocation(maxCompLoc.get(i).getDescriptor()));
1628         }
1629       } else {
1630
1631         // here find out composite location that has a maximum length tuple
1632         // if we have three input set: [A], [A,B], [A,B,C]
1633         // maximum length tuple will be [A,B,C]
1634         int max = 0;
1635         CompositeLocation maxFromCompSet = null;
1636         for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
1637           CompositeLocation c = (CompositeLocation) iterator.next();
1638           if (c.getSize() > max) {
1639             max = c.getSize();
1640             maxFromCompSet = c;
1641           }
1642         }
1643
1644         if (compSet.size() == 1) {
1645
1646           // if GLB(x1,x2)==x1 or x2 : GLB case 2,3
1647           CompositeLocation comp = compSet.iterator().next();
1648           for (int i = 1; i < comp.getSize(); i++) {
1649             glbCompLoc.addLocation(comp.get(i));
1650           }
1651
1652           // if input location corresponding to glb is a delta, need to apply
1653           // delta to glb result
1654           if (comp instanceof DeltaLocation) {
1655             glbCompLoc = new DeltaLocation(glbCompLoc, 1);
1656           }
1657
1658         } else {
1659           // when GLB(x1,x2)==x1 and x2 : GLB case 1
1660           // if more than one location shares the same priority GLB
1661           // need to calculate the rest of GLB loc
1662
1663           // int compositeLocSize = compSet.iterator().next().getSize();
1664           int compositeLocSize = maxFromCompSet.getSize();
1665
1666           Set<String> glbInputSet = new HashSet<String>();
1667           Descriptor currentD = null;
1668           for (int i = 1; i < compositeLocSize; i++) {
1669             for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
1670               CompositeLocation compositeLocation = (CompositeLocation) iterator.next();
1671               if (compositeLocation.getSize() > i) {
1672                 Location currentLoc = compositeLocation.get(i);
1673                 currentD = currentLoc.getDescriptor();
1674                 // making set of the current location sharing the same idx
1675                 glbInputSet.add(currentLoc.getLocIdentifier());
1676               }
1677             }
1678             // calculate glb for the current lattice
1679
1680             SSJavaLattice<String> currentLattice = getLatticeByDescriptor(currentD);
1681             String currentGLBLocId = currentLattice.getGLB(glbInputSet);
1682             glbCompLoc.addLocation(new Location(currentD, currentGLBLocId));
1683           }
1684
1685           // if input location corresponding to glb is a delta, need to apply
1686           // delta to glb result
1687
1688           for (Iterator iterator = compSet.iterator(); iterator.hasNext();) {
1689             CompositeLocation compLoc = (CompositeLocation) iterator.next();
1690             if (compLoc instanceof DeltaLocation) {
1691               if (glbCompLoc.equals(compLoc)) {
1692                 glbCompLoc = new DeltaLocation(glbCompLoc, 1);
1693                 break;
1694               }
1695             }
1696           }
1697
1698         }
1699       }
1700
1701       return glbCompLoc;
1702
1703     }
1704
1705     static SSJavaLattice<String> getLatticeByDescriptor(Descriptor d) {
1706
1707       SSJavaLattice<String> lattice = null;
1708
1709       if (d instanceof ClassDescriptor) {
1710         lattice = ssjava.getCd2lattice().get(d);
1711       } else if (d instanceof MethodDescriptor) {
1712         if (ssjava.getMd2lattice().containsKey(d)) {
1713           lattice = ssjava.getMd2lattice().get(d);
1714         } else {
1715           // use default lattice for the method
1716           lattice = ssjava.getCd2methodDefault().get(((MethodDescriptor) d).getClassDesc());
1717         }
1718       }
1719
1720       return lattice;
1721     }
1722
1723   }
1724
1725   class ComparisonResult {
1726
1727     public static final int GREATER = 0;
1728     public static final int EQUAL = 1;
1729     public static final int LESS = 2;
1730     public static final int INCOMPARABLE = 3;
1731     int result;
1732
1733   }
1734
1735 }
1736
1737 class ReturnLocGenerator {
1738
1739   public static final int PARAMISHIGHER = 0;
1740   public static final int PARAMISSAME = 1;
1741   public static final int IGNORE = 2;
1742
1743   Hashtable<Integer, Integer> paramIdx2paramType;
1744
1745   public ReturnLocGenerator(CompositeLocation returnLoc, List<CompositeLocation> params, String msg) {
1746     // creating mappings
1747     paramIdx2paramType = new Hashtable<Integer, Integer>();
1748     for (int i = 0; i < params.size(); i++) {
1749       CompositeLocation param = params.get(i);
1750       int compareResult = CompositeLattice.compare(param, returnLoc, msg);
1751
1752       int type;
1753       if (compareResult == ComparisonResult.GREATER) {
1754         type = 0;
1755       } else if (compareResult == ComparisonResult.EQUAL) {
1756         type = 1;
1757       } else {
1758         type = 2;
1759       }
1760       paramIdx2paramType.put(new Integer(i), new Integer(type));
1761     }
1762
1763   }
1764
1765   public CompositeLocation computeReturnLocation(List<CompositeLocation> args) {
1766
1767     // compute the highest possible location in caller's side
1768     assert paramIdx2paramType.keySet().size() == args.size();
1769
1770     Set<CompositeLocation> inputGLB = new HashSet<CompositeLocation>();
1771     for (int i = 0; i < args.size(); i++) {
1772       int type = (paramIdx2paramType.get(new Integer(i))).intValue();
1773       CompositeLocation argLoc = args.get(i);
1774       if (type == PARAMISHIGHER) {
1775         // return loc is lower than param
1776         DeltaLocation delta = new DeltaLocation(argLoc, 1);
1777         inputGLB.add(delta);
1778       } else if (type == PARAMISSAME) {
1779         // return loc is equal or lower than param
1780         inputGLB.add(argLoc);
1781       }
1782     }
1783
1784     // compute GLB of arguments subset that are same or higher than return
1785     // location
1786     CompositeLocation glb = CompositeLattice.calculateGLB(inputGLB);
1787     return glb;
1788   }
1789 }