Robust/src/Analysis/SSJava/FlowDownCheck.java

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