Robust/src/Analysis/SSJava/FlowDownCheck.java

   1 package Analysis.SSJava;
   2
   3 import java.util.HashSet;
   4 import java.util.Hashtable;
   5 import java.util.Iterator;
   6 import java.util.Map;
   7 import java.util.Set;
   8 import java.util.StringTokenizer;
   9 import java.util.Vector;
  10
  11 import IR.AnnotationDescriptor;
  12 import IR.ClassDescriptor;
  13 import IR.Descriptor;
  14 import IR.FieldDescriptor;
  15 import IR.MethodDescriptor;
  16 import IR.NameDescriptor;
  17 import IR.Operation;
  18 import IR.State;
  19 import IR.SymbolTable;
  20 import IR.TypeDescriptor;
  21 import IR.VarDescriptor;
  22 import IR.Flat.FlatFieldNode;
  23 import IR.Tree.ArrayAccessNode;
  24 import IR.Tree.ArrayInitializerNode;
  25 import IR.Tree.AssignmentNode;
  26 import IR.Tree.BlockExpressionNode;
  27 import IR.Tree.BlockNode;
  28 import IR.Tree.BlockStatementNode;
  29 import IR.Tree.CastNode;
  30 import IR.Tree.ClassTypeNode;
  31 import IR.Tree.CreateObjectNode;
  32 import IR.Tree.DeclarationNode;
  33 import IR.Tree.ExpressionNode;
  34 import IR.Tree.FieldAccessNode;
  35 import IR.Tree.InstanceOfNode;
  36 import IR.Tree.Kind;
  37 import IR.Tree.LiteralNode;
  38 import IR.Tree.MethodInvokeNode;
  39 import IR.Tree.NameNode;
  40 import IR.Tree.OffsetNode;
  41 import IR.Tree.OpNode;
  42 import IR.Tree.SubBlockNode;
  43 import IR.Tree.TertiaryNode;
  44 import Util.Lattice;
  45
  46 public class FlowDownCheck {
  47
  48   static State state;
  49   HashSet toanalyze;
  50   Hashtable<TypeDescriptor, Location> td2loc; // mapping from 'type descriptor'
  51   // to 'location'
  52   Hashtable<String, ClassDescriptor> id2cd; // mapping from 'locID' to 'class
  53
  54   // descriptor'
  55
  56   public FlowDownCheck(State state) {
  57     this.state = state;
  58     this.toanalyze = new HashSet();
  59     this.td2loc = new Hashtable<TypeDescriptor, Location>();
  60     init();
  61   }
  62
  63   public void init() {
  64     id2cd = new Hashtable<String, ClassDescriptor>();
  65     Hashtable cd2lattice = state.getCd2LocationOrder();
  66
  67     Set cdSet = cd2lattice.keySet();
  68     for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
  69       ClassDescriptor cd = (ClassDescriptor) iterator.next();
  70       Lattice<String> lattice = (Lattice<String>) cd2lattice.get(cd);
  71
  72       Set<String> locIdSet = lattice.getKeySet();
  73       for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext();) {
  74         String locID = (String) iterator2.next();
  75         id2cd.put(locID, cd);
  76       }
  77     }
  78
  79   }
  80
  81   public void flowDownCheck() {
  82     SymbolTable classtable = state.getClassSymbolTable();
  83
  84     // phase 1 : checking declaration node and creating mapping of 'type
  85     // desciptor' & 'location'
  86     toanalyze.addAll(classtable.getValueSet());
  87     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
  88     while (!toanalyze.isEmpty()) {
  89       Object obj = toanalyze.iterator().next();
  90       ClassDescriptor cd = (ClassDescriptor) obj;
  91       toanalyze.remove(cd);
  92       if (cd.isClassLibrary()) {
  93         // doesn't care about class libraries now
  94         continue;
  95       }
  96       checkDeclarationInClass(cd);
  97       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
  98         MethodDescriptor md = (MethodDescriptor) method_it.next();
  99         try {
 100           checkDeclarationInMethodBody(cd, md);
 101         } catch (Error e) {
 102           System.out.println("Error in " + md);
 103           throw e;
 104         }
 105       }
 106     }
 107
 108     // phase2 : checking assignments
 109     toanalyze.addAll(classtable.getValueSet());
 110     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
 111     while (!toanalyze.isEmpty()) {
 112       Object obj = toanalyze.iterator().next();
 113       ClassDescriptor cd = (ClassDescriptor) obj;
 114       toanalyze.remove(cd);
 115       if (cd.isClassLibrary()) {
 116         // doesn't care about class libraries now
 117         continue;
 118       }
 119       checkClass(cd);
 120       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 121         MethodDescriptor md = (MethodDescriptor) method_it.next();
 122         try {
 123           checkMethodBody(cd, md);
 124         } catch (Error e) {
 125           System.out.println("Error in " + md);
 126           throw e;
 127         }
 128       }
 129     }
 130
 131   }
 132
 133   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
 134     BlockNode bn = state.getMethodBody(md);
 135     checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
 136   }
 137
 138   public void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
 139     bn.getVarTable().setParent(nametable);
 140     for (int i = 0; i < bn.size(); i++) {
 141       BlockStatementNode bsn = bn.get(i);
 142       checkDeclarationInBlockStatementNode(md, bn.getVarTable(), bsn);
 143     }
 144   }
 145
 146   private void checkDeclarationInBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
 147       BlockStatementNode bsn) {
 148
 149     switch (bsn.kind()) {
 150     case Kind.SubBlockNode:
 151       checkDeclarationInSubBlockNode(md, nametable, (SubBlockNode) bsn);
 152       return;
 153     case Kind.DeclarationNode:
 154       checkDeclarationNode(md, (DeclarationNode) bsn);
 155       break;
 156     }
 157   }
 158
 159   public void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
 160     BlockNode bn = state.getMethodBody(md);
 161     checkBlockNode(md, md.getParameterTable(), bn);
 162   }
 163
 164   public void checkBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
 165     /* Link in the naming environment */
 166     bn.getVarTable().setParent(nametable);
 167     for (int i = 0; i < bn.size(); i++) {
 168       BlockStatementNode bsn = bn.get(i);
 169       checkBlockStatementNode(md, bn.getVarTable(), bsn);
 170     }
 171   }
 172
 173   public void checkBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
 174       BlockStatementNode bsn) {
 175
 176     switch (bsn.kind()) {
 177     case Kind.BlockExpressionNode:
 178       checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
 179       return;
 180
 181     }
 182     /*
 183      * switch (bsn.kind()) { case Kind.BlockExpressionNode:
 184      * checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
 185      * return;
 186      *
 187      * case Kind.DeclarationNode: checkDeclarationNode(md, nametable,
 188      * (DeclarationNode) bsn); return;
 189      *
 190      * case Kind.TagDeclarationNode: checkTagDeclarationNode(md, nametable,
 191      * (TagDeclarationNode) bsn); return;
 192      *
 193      * case Kind.IfStatementNode: checkIfStatementNode(md, nametable,
 194      * (IfStatementNode) bsn); return;
 195      *
 196      * case Kind.SwitchStatementNode: checkSwitchStatementNode(md, nametable,
 197      * (SwitchStatementNode) bsn); return;
 198      *
 199      * case Kind.LoopNode: checkLoopNode(md, nametable, (LoopNode) bsn); return;
 200      *
 201      * case Kind.ReturnNode: checkReturnNode(md, nametable, (ReturnNode) bsn);
 202      * return;
 203      *
 204      * case Kind.TaskExitNode: checkTaskExitNode(md, nametable, (TaskExitNode)
 205      * bsn); return;
 206      *
 207      * case Kind.SubBlockNode: checkSubBlockNode(md, nametable, (SubBlockNode)
 208      * bsn); return;
 209      *
 210      * case Kind.AtomicNode: checkAtomicNode(md, nametable, (AtomicNode) bsn);
 211      * return;
 212      *
 213      * case Kind.SynchronizedNode: checkSynchronizedNode(md, nametable,
 214      * (SynchronizedNode) bsn); return;
 215      *
 216      * case Kind.ContinueBreakNode: checkContinueBreakNode(md, nametable,
 217      * (ContinueBreakNode) bsn); return;
 218      *
 219      * case Kind.SESENode: case Kind.GenReachNode: // do nothing, no semantic
 220      * check for SESEs return; }
 221      */
 222     // throw new Error();
 223   }
 224
 225   private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable,
 226       SubBlockNode sbn) {
 227     checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode());
 228   }
 229
 230   void checkBlockExpressionNode(MethodDescriptor md, SymbolTable nametable, BlockExpressionNode ben) {
 231     checkExpressionNode(md, nametable, ben.getExpression(), null);
 232   }
 233
 234   void checkExpressionNode(MethodDescriptor md, SymbolTable nametable, ExpressionNode en,
 235       TypeDescriptor td) {
 236
 237     switch (en.kind()) {
 238     case Kind.AssignmentNode:
 239       checkAssignmentNode(md, nametable, (AssignmentNode) en, td);
 240       return;
 241
 242     case Kind.OpNode:
 243       checkOpNode(md, nametable, (OpNode) en, td);
 244       return;
 245
 246     case Kind.FieldAccessNode:
 247       checkFieldAccessNode(md, nametable, (FieldAccessNode) en, td);
 248       return;
 249
 250     case Kind.NameNode:
 251       checkNameNode(md, nametable, (NameNode) en, td);
 252       return;
 253
 254     }
 255
 256     /*
 257      * switch(en.kind()) { case Kind.AssignmentNode:
 258      * checkAssignmentNode(md,nametable,(AssignmentNode)en,td); return;
 259      *
 260      * case Kind.CastNode: checkCastNode(md,nametable,(CastNode)en,td); return;
 261      *
 262      * case Kind.CreateObjectNode:
 263      * checkCreateObjectNode(md,nametable,(CreateObjectNode)en,td); return;
 264      *
 265      * case Kind.FieldAccessNode:
 266      * checkFieldAccessNode(md,nametable,(FieldAccessNode)en,td); return;
 267      *
 268      * case Kind.ArrayAccessNode:
 269      * checkArrayAccessNode(md,nametable,(ArrayAccessNode)en,td); return;
 270      *
 271      * case Kind.LiteralNode: checkLiteralNode(md,nametable,(LiteralNode)en,td);
 272      * return;
 273      *
 274      * case Kind.MethodInvokeNode:
 275      * checkMethodInvokeNode(md,nametable,(MethodInvokeNode)en,td); return;
 276      *
 277      * case Kind.NameNode: checkNameNode(md,nametable,(NameNode)en,td); return;
 278      *
 279      * case Kind.OpNode: checkOpNode(md,nametable,(OpNode)en,td); return;
 280      *
 281      * case Kind.OffsetNode: checkOffsetNode(md, nametable, (OffsetNode)en, td);
 282      * return;
 283      *
 284      * case Kind.TertiaryNode: checkTertiaryNode(md, nametable,
 285      * (TertiaryNode)en, td); return;
 286      *
 287      * case Kind.InstanceOfNode: checkInstanceOfNode(md, nametable,
 288      * (InstanceOfNode) en, td); return;
 289      *
 290      * case Kind.ArrayInitializerNode: checkArrayInitializerNode(md, nametable,
 291      * (ArrayInitializerNode) en, td); return;
 292      *
 293      * case Kind.ClassTypeNode: checkClassTypeNode(md, nametable,
 294      * (ClassTypeNode) en, td); return; }
 295      */
 296   }
 297
 298   void checkNameNode(MethodDescriptor md, SymbolTable nametable, NameNode nn, TypeDescriptor td) {
 299
 300     NameDescriptor nd = nn.getName();
 301     System.out.println("checkNameNode=" + nn);
 302     System.out.println("nn.expression=" + nn.getExpression().printNode(0));
 303
 304     if (nd.getBase() != null) {
 305       /* Big hack */
 306       /* Rewrite NameNode */
 307       ExpressionNode en = translateNameDescriptorintoExpression(nd);
 308       System.out.println("base=" + nd.getBase() + " field=" + nn.getField() + " en="
 309           + en.printNode(0));
 310       nn.setExpression(en);
 311       System.out.println("checking expression node=" + en.printNode(0) + " with td=" + td);
 312       checkExpressionNode(md, nametable, en, td);
 313     } else {
 314       System.out.println("base=" + nd.getBase() + " field=" + nn.getField());
 315
 316     }
 317
 318     // ExpressionNode en=nn.getExpression();
 319     // if(en instanceof FieldAccessNode){
 320     // FieldAccessNode fan=(FieldAccessNode)en;
 321     // System.out.println("base="+nd.getBase()+" field="+fan.getFieldName());
 322     // }
 323
 324     // checkExpressionNode(md, nametable, nn.getExpression(), td);
 325     // NameDescriptor nd = nn.getName();
 326     // if (nd.getBase() != null) {
 327     // System.out.println("nd.getBase()="+nd.getBase());
 328     // /* Big hack */
 329     // /* Rewrite NameNode */
 330     // ExpressionNode en = translateNameDescriptorintoExpression(nd);
 331     // System.out.println("expressionsNode="+en);
 332     // nn.setExpression(en);
 333     // checkExpressionNode(md, nametable, en, td);
 334     // }
 335
 336   }
 337
 338   ExpressionNode translateNameDescriptorintoExpression(NameDescriptor nd) {
 339     String id = nd.getIdentifier();
 340     NameDescriptor base = nd.getBase();
 341     if (base == null) {
 342       NameNode nn = new NameNode(nd);
 343       return nn;
 344     } else {
 345       FieldAccessNode fan = new FieldAccessNode(translateNameDescriptorintoExpression(base), id);
 346       return fan;
 347     }
 348   }
 349
 350   void checkFieldAccessNode(MethodDescriptor md, SymbolTable nametable, FieldAccessNode fan,
 351       TypeDescriptor td) {
 352
 353     System.out.println("fan=" + fan + " field=" + fan.getFieldName());
 354     ExpressionNode left = fan.getExpression();
 355     System.out.println("checking expression from fan=" + left.printNode(0) + " with td=" + td);
 356     checkExpressionNode(md, nametable, left, null);
 357     TypeDescriptor ltd = left.getType();
 358     String fieldname = fan.getFieldName();
 359
 360   }
 361
 362   void checkOpNode(MethodDescriptor md, SymbolTable nametable, OpNode on, TypeDescriptor td) {
 363
 364     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(md.getClassDesc());
 365
 366     checkExpressionNode(md, nametable, on.getLeft(), null);
 367     if (on.getRight() != null)
 368       checkExpressionNode(md, nametable, on.getRight(), null);
 369
 370     TypeDescriptor ltd = on.getLeft().getType();
 371     TypeDescriptor rtd = on.getRight() != null ? on.getRight().getType() : null;
 372
 373     if (ltd.getAnnotationMarkers().size() == 0) {
 374       // constant value
 375       // TODO
 376       // ltd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
 377     }
 378     if (rtd != null && rtd.getAnnotationMarkers().size() == 0) {
 379       // constant value
 380       // TODO
 381       // rtd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
 382     }
 383
 384     System.out.println("checking op node");
 385     System.out.println("td=" + td);
 386     System.out.println("ltd=" + ltd);
 387     System.out.println("rtd=" + rtd);
 388
 389     Operation op = on.getOp();
 390
 391     switch (op.getOp()) {
 392
 393     case Operation.UNARYPLUS:
 394     case Operation.UNARYMINUS:
 395     case Operation.LOGIC_NOT:
 396       // single operand
 397       on.setType(new TypeDescriptor(TypeDescriptor.BOOLEAN));
 398       break;
 399
 400     case Operation.LOGIC_OR:
 401     case Operation.LOGIC_AND:
 402     case Operation.COMP:
 403     case Operation.BIT_OR:
 404     case Operation.BIT_XOR:
 405     case Operation.BIT_AND:
 406     case Operation.ISAVAILABLE:
 407     case Operation.EQUAL:
 408     case Operation.NOTEQUAL:
 409     case Operation.LT:
 410     case Operation.GT:
 411     case Operation.LTE:
 412     case Operation.GTE:
 413     case Operation.ADD:
 414     case Operation.SUB:
 415     case Operation.MULT:
 416     case Operation.DIV:
 417     case Operation.MOD:
 418     case Operation.LEFTSHIFT:
 419     case Operation.RIGHTSHIFT:
 420     case Operation.URIGHTSHIFT:
 421
 422       Set<String> operandSet = new HashSet<String>();
 423       String leftLoc = ltd.getAnnotationMarkers().get(0).getMarker();
 424       String rightLoc = rtd.getAnnotationMarkers().get(0).getMarker();
 425
 426       operandSet.add(leftLoc);
 427       operandSet.add(rightLoc);
 428
 429       // TODO
 430       // String glbLoc = locOrder.getGLB(operandSet);
 431       // on.getType().addAnnotationMarker(new AnnotationDescriptor(glbLoc));
 432       // System.out.println(glbLoc + "<-" + leftLoc + " " + rightLoc);
 433
 434       break;
 435
 436     default:
 437       throw new Error(op.toString());
 438     }
 439
 440     if (td != null) {
 441       String lhsLoc = td.getAnnotationMarkers().get(0).getMarker();
 442       if (locOrder.isGreaterThan(lhsLoc, on.getType().getAnnotationMarkers().get(0).getMarker())) {
 443         throw new Error("The location of LHS is higher than RHS: " + on.printNode(0));
 444       }
 445     }
 446
 447   }
 448
 449   protected void getLocationFromExpressionNode(MethodDescriptor md, SymbolTable nametable,
 450       ExpressionNode en, CompositeLocation loc) {
 451
 452     switch (en.kind()) {
 453
 454     case Kind.AssignmentNode:
 455       getLocationFromAssignmentNode(md, nametable, (AssignmentNode) en, loc);
 456       return;
 457
 458     case Kind.FieldAccessNode:
 459       getLocationFromFieldAccessNode(md, nametable, (FieldAccessNode) en, loc);
 460       return;
 461
 462     case Kind.NameNode:
 463       getLocationFromNameNode(md, nametable, (NameNode) en, loc);
 464       return;
 465
 466     case Kind.OpNode:
 467       getLocationFromOpNode(md, nametable, (OpNode) en, loc);
 468       // checkOpNode(md,nametable,(OpNode)en,td);
 469       return;
 470
 471     case Kind.CastNode:
 472       // checkCastNode(md,nametable,(CastNode)en,td);
 473       return;
 474
 475     case Kind.CreateObjectNode:
 476       // checkCreateObjectNode(md, nametable, (CreateObjectNode) en, td);
 477       return;
 478
 479     case Kind.ArrayAccessNode:
 480       // checkArrayAccessNode(md, nametable, (ArrayAccessNode) en, td);
 481       return;
 482
 483     case Kind.LiteralNode:
 484       getLocationFromLiteralNode(md, nametable, (LiteralNode) en, loc);
 485       return;
 486
 487     case Kind.MethodInvokeNode:
 488       // checkMethodInvokeNode(md,nametable,(MethodInvokeNode)en,td);
 489       return;
 490
 491     case Kind.OffsetNode:
 492       // checkOffsetNode(md, nametable, (OffsetNode)en, td);
 493       return;
 494
 495     case Kind.TertiaryNode:
 496       // checkTertiaryNode(md, nametable, (TertiaryNode)en, td);
 497       return;
 498
 499     case Kind.InstanceOfNode:
 500       // checkInstanceOfNode(md, nametable, (InstanceOfNode) en, td);
 501       return;
 502
 503     case Kind.ArrayInitializerNode:
 504       // checkArrayInitializerNode(md, nametable, (ArrayInitializerNode) en,
 505       // td);
 506       return;
 507
 508     case Kind.ClassTypeNode:
 509       // checkClassTypeNode(md, nametable, (ClassTypeNode) en, td);
 510       return;
 511
 512     }
 513
 514   }
 515
 516   private void getLocationFromOpNode(MethodDescriptor md, SymbolTable nametable, OpNode on,
 517       CompositeLocation loc) {
 518
 519     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(md.getClassDesc());
 520
 521     ClassDescriptor cd = md.getClassDesc();
 522     CompositeLocation leftLoc = new CompositeLocation(cd);
 523     getLocationFromExpressionNode(md, nametable, on.getLeft(), leftLoc);
 524
 525     CompositeLocation rightLoc = new CompositeLocation(cd);
 526     if (on.getRight() != null) {
 527       getLocationFromExpressionNode(md, nametable, on.getRight(), rightLoc);
 528     }
 529
 530     System.out.println("checking op node");
 531     System.out.println("left loc=" + leftLoc);
 532     System.out.println("right loc=" + rightLoc);
 533
 534     Operation op = on.getOp();
 535
 536     switch (op.getOp()) {
 537
 538     case Operation.UNARYPLUS:
 539     case Operation.UNARYMINUS:
 540     case Operation.LOGIC_NOT:
 541       // single operand
 542       on.setType(new TypeDescriptor(TypeDescriptor.BOOLEAN));
 543       break;
 544
 545     case Operation.LOGIC_OR:
 546     case Operation.LOGIC_AND:
 547     case Operation.COMP:
 548     case Operation.BIT_OR:
 549     case Operation.BIT_XOR:
 550     case Operation.BIT_AND:
 551     case Operation.ISAVAILABLE:
 552     case Operation.EQUAL:
 553     case Operation.NOTEQUAL:
 554     case Operation.LT:
 555     case Operation.GT:
 556     case Operation.LTE:
 557     case Operation.GTE:
 558     case Operation.ADD:
 559     case Operation.SUB:
 560     case Operation.MULT:
 561     case Operation.DIV:
 562     case Operation.MOD:
 563     case Operation.LEFTSHIFT:
 564     case Operation.RIGHTSHIFT:
 565     case Operation.URIGHTSHIFT:
 566
 567       // Set<String> operandSet = new HashSet<String>();
 568       // String leftLoc = ltd.getAnnotationMarkers().get(0).getMarker();
 569       // String rightLoc = rtd.getAnnotationMarkers().get(0).getMarker();
 570       //
 571       // operandSet.add(leftLoc);
 572       // operandSet.add(rightLoc);
 573
 574       // TODO
 575       // String glbLoc = locOrder.getGLB(operandSet);
 576       // on.getType().addAnnotationMarker(new AnnotationDescriptor(glbLoc));
 577       // System.out.println(glbLoc + "<-" + leftLoc + " " + rightLoc);
 578
 579       break;
 580
 581     default:
 582       throw new Error(op.toString());
 583     }
 584
 585     // if (td != null) {
 586     // String lhsLoc = td.getAnnotationMarkers().get(0).getMarker();
 587     // if (locOrder.isGreaterThan(lhsLoc,
 588     // on.getType().getAnnotationMarkers().get(0).getMarker())) {
 589     // throw new Error("The location of LHS is higher than RHS: " +
 590     // on.printNode(0));
 591     // }
 592     // }
 593
 594   }
 595
 596   private void getLocationFromLiteralNode(MethodDescriptor md, SymbolTable nametable,
 597       LiteralNode en, CompositeLocation loc) {
 598
 599     // literal value has the top location so that value can be flowed into any
 600     // location
 601     Location literalLoc = Location.createTopLocation(md.getClassDesc());
 602     loc.addLocation(literalLoc);
 603
 604   }
 605
 606   private void getLocationFromNameNode(MethodDescriptor md, SymbolTable nametable, NameNode nn,
 607       CompositeLocation loc) {
 608
 609     NameDescriptor nd = nn.getName();
 610     if (nd.getBase() != null) {
 611       getLocationFromExpressionNode(md, nametable, nn.getExpression(), loc);
 612     } else {
 613
 614       String varname = nd.toString();
 615       Descriptor d = (Descriptor) nametable.get(varname);
 616
 617       Location localLoc = null;
 618       if (d instanceof VarDescriptor) {
 619         VarDescriptor vd = (VarDescriptor) d;
 620         localLoc = td2loc.get(vd.getType());
 621       } else if (d instanceof FieldDescriptor) {
 622         FieldDescriptor fd = (FieldDescriptor) d;
 623         localLoc = td2loc.get(fd.getType());
 624       }
 625       assert (localLoc != null);
 626       loc.addLocation(localLoc);
 627     }
 628
 629   }
 630
 631   private void getLocationFromFieldAccessNode(MethodDescriptor md, SymbolTable nametable,
 632       FieldAccessNode fan, CompositeLocation loc) {
 633     FieldDescriptor fd = fan.getField();
 634     Location fieldLoc = td2loc.get(fd.getType());
 635     loc.addLocation(fieldLoc);
 636
 637     ExpressionNode left = fan.getExpression();
 638     getLocationFromExpressionNode(md, nametable, left, loc);
 639   }
 640
 641   private CompositeLocation getLocationFromAssignmentNode(Descriptor md, SymbolTable nametable,
 642       AssignmentNode en, CompositeLocation loc) {
 643     // TODO Auto-generated method stub
 644
 645     return null;
 646   }
 647
 648   private Location createCompositeLocation(FieldAccessNode fan, Location loc) {
 649
 650     FieldDescriptor field = fan.getField();
 651     ClassDescriptor fieldCD = field.getClassDescriptor();
 652
 653     assert (field.getType().getAnnotationMarkers().size() == 1);
 654
 655     AnnotationDescriptor locAnnotation = field.getType().getAnnotationMarkers().elementAt(0);
 656     if (locAnnotation.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 657       // single location
 658
 659     } else {
 660       // delta location
 661     }
 662
 663     // Location localLoc=new Location(field.getClassDescriptor(),field.get)
 664
 665     // System.out.println("creatingComposite's field="+field+" localLoc="+localLoc);
 666     ExpressionNode leftNode = fan.getExpression();
 667     System.out.println("creatingComposite's leftnode=" + leftNode.printNode(0));
 668
 669     return loc;
 670   }
 671
 672   void checkAssignmentNode(MethodDescriptor md, SymbolTable nametable, AssignmentNode an,
 673       TypeDescriptor td) {
 674
 675     CompositeLocation srcLocation = new CompositeLocation(md.getClassDesc());
 676
 677     boolean postinc = true;
 678     if (an.getOperation().getBaseOp() == null
 679         || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation()
 680             .getBaseOp().getOp() != Operation.POSTDEC))
 681       postinc = false;
 682     if (!postinc) {
 683       // checkExpressionNode(md, nametable, an.getSrc(), td);
 684       // calculateLocation(md, nametable, an.getSrc(), td);
 685       getLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
 686     }
 687
 688     ClassDescriptor cd = md.getClassDesc();
 689     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 690
 691     Location destLocation = td2loc.get(an.getDest().getType());
 692
 693     if (!CompositeLattice.isGreaterThan(srcLocation, destLocation)) {
 694       throw new Error("The value flow from " + srcLocation + " to " + destLocation
 695           + " does not respect location hierarchy on the assignment " + an.printNode(0));
 696     }
 697
 698   }
 699
 700   void checkDeclarationNode(MethodDescriptor md, DeclarationNode dn) {
 701     ClassDescriptor cd = md.getClassDesc();
 702     VarDescriptor vd = dn.getVarDescriptor();
 703     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
 704
 705     // currently enforce every variable to have corresponding location
 706     if (annotationVec.size() == 0) {
 707       throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
 708           + md.getSymbol() + " of the class " + cd.getSymbol());
 709     }
 710
 711     if (annotationVec.size() > 1) {
 712       // variable can have at most one location
 713       throw new Error(vd.getSymbol() + " has more than one location.");
 714     }
 715
 716     AnnotationDescriptor ad = annotationVec.elementAt(0);
 717
 718     if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
 719
 720       // check if location is defined
 721       String locationID = ad.getMarker();
 722       Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 723
 724       if (lattice == null || (!lattice.containsKey(locationID))) {
 725         throw new Error("Location " + locationID
 726             + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
 727       }
 728
 729       Location loc = new Location(cd, locationID);
 730       td2loc.put(vd.getType(), loc);
 731
 732     } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 733       if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
 734
 735         if (ad.getData().length() == 0) {
 736           throw new Error("Delta function of " + vd.getSymbol() + " does not have any locations: "
 737               + cd.getSymbol() + ".");
 738         }
 739
 740         StringTokenizer token = new StringTokenizer(ad.getData(), ",");
 741
 742         CompositeLocation compLoc = new CompositeLocation(cd);
 743         DeltaLocation deltaLoc = new DeltaLocation(cd);
 744
 745         while (token.hasMoreTokens()) {
 746           String deltaOperand = token.nextToken();
 747           ClassDescriptor deltaCD = id2cd.get(deltaOperand);
 748           if (deltaCD == null) {
 749             // delta operand is not defined in the location hierarchy
 750             throw new Error("Delta operand '" + deltaOperand + "' of declaration node '" + vd
 751                 + "' is not defined by location hierarchies.");
 752           }
 753
 754           Location loc = new Location(deltaCD, deltaOperand);
 755           deltaLoc.addDeltaOperand(loc);
 756         }
 757         compLoc.addLocation(deltaLoc);
 758         td2loc.put(vd.getType(), compLoc);
 759       }
 760     }
 761
 762   }
 763
 764   private void checkClass(ClassDescriptor cd) {
 765     // Check to see that methods respects ss property
 766     for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 767       MethodDescriptor md = (MethodDescriptor) method_it.next();
 768       checkMethodDeclaration(cd, md);
 769     }
 770   }
 771
 772   private void checkDeclarationInClass(ClassDescriptor cd) {
 773     // Check to see that fields are okay
 774     for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
 775       FieldDescriptor fd = (FieldDescriptor) field_it.next();
 776       checkFieldDeclaration(cd, fd);
 777     }
 778   }
 779
 780   private void checkMethodDeclaration(ClassDescriptor cd, MethodDescriptor md) {
 781
 782   }
 783
 784   private void checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
 785
 786     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
 787
 788     // currently enforce every variable to have corresponding location
 789     if (annotationVec.size() == 0) {
 790       throw new Error("Location is not assigned to the field " + fd.getSymbol() + " of the class "
 791           + cd.getSymbol());
 792     }
 793
 794     if (annotationVec.size() > 1) {
 795       // variable can have at most one location
 796       throw new Error("Field " + fd.getSymbol() + " of class " + cd
 797           + " has more than one location.");
 798     }
 799
 800     // check if location is defined
 801     AnnotationDescriptor ad = annotationVec.elementAt(0);
 802     if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
 803       String locationID = annotationVec.elementAt(0).getMarker();
 804       Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 805
 806       if (lattice == null || (!lattice.containsKey(locationID))) {
 807         throw new Error("Location " + locationID
 808             + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
 809       }
 810
 811       Location localLoc = new Location(cd, locationID);
 812       td2loc.put(fd.getType(), localLoc);
 813
 814     } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 815       if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
 816
 817         if (ad.getData().length() == 0) {
 818           throw new Error("Delta function of " + fd.getSymbol() + " does not have any locations: "
 819               + cd.getSymbol() + ".");
 820         }
 821
 822         CompositeLocation compLoc = new CompositeLocation(cd);
 823         DeltaLocation deltaLoc = new DeltaLocation(cd);
 824
 825         StringTokenizer token = new StringTokenizer(ad.getData(), ",");
 826         while (token.hasMoreTokens()) {
 827           String deltaOperand = token.nextToken();
 828           ClassDescriptor deltaCD = id2cd.get(deltaOperand);
 829           if (deltaCD == null) {
 830             // delta operand is not defined in the location hierarchy
 831             throw new Error("Delta operand '" + deltaOperand + "' of field node '" + fd
 832                 + "' is not defined by location hierarchies.");
 833           }
 834
 835           Location loc = new Location(deltaCD, deltaOperand);
 836           deltaLoc.addDeltaOperand(loc);
 837         }
 838         compLoc.addLocation(deltaLoc);
 839         td2loc.put(fd.getType(), compLoc);
 840
 841       }
 842     }
 843
 844   }
 845
 846   static class CompositeLattice {
 847
 848     public static boolean isGreaterThan(Location loc1, Location loc2) {
 849
 850       CompositeLocation compLoc1;
 851       CompositeLocation compLoc2;
 852
 853       if (loc1 instanceof CompositeLocation) {
 854         compLoc1 = (CompositeLocation) loc1;
 855       } else {
 856         // create a bogus composite location for a single location
 857         compLoc1 = new CompositeLocation(loc1.getClassDescriptor());
 858         compLoc1.addLocation(loc1);
 859       }
 860
 861       if (loc2 instanceof CompositeLocation) {
 862         compLoc2 = (CompositeLocation) loc2;
 863       } else {
 864         // create a bogus composite location for a single location
 865         compLoc2 = new CompositeLocation(loc2.getClassDescriptor());
 866         compLoc2.addLocation(loc2);
 867       }
 868
 869       // comparing two composite locations
 870       System.out.println("compare base location=" + compLoc1 + " ? " + compLoc2);
 871
 872       int baseCompareResult = compareBaseLocationSet(compLoc1, compLoc2);
 873       if (baseCompareResult == ComparisonResult.EQUAL) {
 874         // TODO
 875         // need to compare # of delta operand
 876       } else if (baseCompareResult == ComparisonResult.GREATER) {
 877         return true;
 878       } else {
 879         return false;
 880       }
 881
 882       return false;
 883     }
 884
 885     private static int compareBaseLocationSet(CompositeLocation compLoc1, CompositeLocation compLoc2) {
 886
 887       // if compLoc1 is greater than compLoc2, return true
 888       // else return false;
 889
 890       Map<ClassDescriptor, Location> cd2loc1 = compLoc1.getCd2Loc();
 891       Map<ClassDescriptor, Location> cd2loc2 = compLoc2.getCd2Loc();
 892
 893       // compare base locations by class descriptor
 894
 895       Set<ClassDescriptor> keySet1 = cd2loc1.keySet();
 896
 897       int numEqualLoc = 0;
 898
 899       for (Iterator iterator = keySet1.iterator(); iterator.hasNext();) {
 900         ClassDescriptor cd1 = (ClassDescriptor) iterator.next();
 901
 902         Location loc1 = cd2loc1.get(cd1);
 903         Location loc2 = cd2loc2.get(cd1);
 904
 905         if (loc2 == null) {
 906           // if comploc2 doesn't have corresponding location, then ignore this
 907           // element
 908           numEqualLoc++;
 909           continue;
 910         }
 911
 912         Lattice<String> locationOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd1);
 913         if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
 914           // have the same level of local hierarchy
 915           numEqualLoc++;
 916         } else if (!locationOrder.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
 917           // if one element of composite location 1 is not higher than composite
 918           // location 2
 919           // then, composite loc 1 is not higher than composite loc 2
 920
 921           System.out.println(compLoc1 + " < " + compLoc2);
 922           return ComparisonResult.LESS;
 923         }
 924
 925       }
 926
 927       if (numEqualLoc == compLoc1.getTupleSize()) {
 928         System.out.println(compLoc1 + " == " + compLoc2);
 929         return ComparisonResult.EQUAL;
 930       }
 931
 932       System.out.println(compLoc1 + " > " + compLoc2);
 933       return ComparisonResult.GREATER;
 934     }
 935
 936   }
 937
 938   class ComparisonResult {
 939
 940     public static final int GREATER = 0;
 941     public static final int EQUAL = 1;
 942     public static final int LESS = 2;
 943     int result;
 944
 945   }
 946
 947 }