Robust/src/Analysis/SSJava/FlowDownCheck.java

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