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