Robust/src/Analysis/SSJava/FlowDownCheck.java

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