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