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