changes.
[IRC.git] / 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.Tree.AssignmentNode;
23 import IR.Tree.BlockExpressionNode;
24 import IR.Tree.BlockNode;
25 import IR.Tree.BlockStatementNode;
26 import IR.Tree.CreateObjectNode;
27 import IR.Tree.DeclarationNode;
28 import IR.Tree.ExpressionNode;
29 import IR.Tree.FieldAccessNode;
30 import IR.Tree.IfStatementNode;
31 import IR.Tree.Kind;
32 import IR.Tree.LiteralNode;
33 import IR.Tree.LoopNode;
34 import IR.Tree.NameNode;
35 import IR.Tree.OpNode;
36 import IR.Tree.SubBlockNode;
37 import Util.Lattice;
38
39 public class FlowDownCheck {
40
41   static State state;
42   HashSet toanalyze;
43   Hashtable<TypeDescriptor, Location> td2loc; // mapping from 'type descriptor'
44   // to 'location'
45   Hashtable<String, ClassDescriptor> id2cd; // mapping from 'locID' to 'class
46
47   // descriptor'
48
49   public FlowDownCheck(State state) {
50     this.state = state;
51     this.toanalyze = new HashSet();
52     this.td2loc = new Hashtable<TypeDescriptor, Location>();
53     init();
54   }
55
56   public void init() {
57     id2cd = new Hashtable<String, ClassDescriptor>();
58     Hashtable cd2lattice = state.getCd2LocationOrder();
59
60     Set cdSet = cd2lattice.keySet();
61     for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
62       ClassDescriptor cd = (ClassDescriptor) iterator.next();
63       Lattice<String> lattice = (Lattice<String>) cd2lattice.get(cd);
64
65       Set<String> locIdSet = lattice.getKeySet();
66       for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext();) {
67         String locID = (String) iterator2.next();
68         id2cd.put(locID, cd);
69       }
70     }
71
72   }
73
74   public void flowDownCheck() {
75     SymbolTable classtable = state.getClassSymbolTable();
76
77     // phase 1 : checking declaration node and creating mapping of 'type
78     // desciptor' & 'location'
79     toanalyze.addAll(classtable.getValueSet());
80     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
81     while (!toanalyze.isEmpty()) {
82       Object obj = toanalyze.iterator().next();
83       ClassDescriptor cd = (ClassDescriptor) obj;
84       toanalyze.remove(cd);
85       if (cd.isClassLibrary()) {
86         // doesn't care about class libraries now
87         continue;
88       }
89       checkDeclarationInClass(cd);
90       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
91         MethodDescriptor md = (MethodDescriptor) method_it.next();
92         try {
93           checkDeclarationInMethodBody(cd, md);
94         } catch (Error e) {
95           System.out.println("Error in " + md);
96           throw e;
97         }
98       }
99     }
100
101     // post-processing for delta location
102     // for a nested delta location, assigning a concrete reference to delta
103     // operand
104     Set<TypeDescriptor> tdSet = td2loc.keySet();
105     for (Iterator iterator = tdSet.iterator(); iterator.hasNext();) {
106       TypeDescriptor td = (TypeDescriptor) iterator.next();
107       Location loc = td2loc.get(td);
108
109       if (loc.getType() == Location.DELTA) {
110         // if it contains delta reference pointing to another location element
111         CompositeLocation compLoc = (CompositeLocation) loc;
112
113         Location locElement = compLoc.getTuple().at(0);
114         assert (locElement instanceof DeltaLocation);
115
116         DeltaLocation delta = (DeltaLocation) locElement;
117         TypeDescriptor refType = delta.getRefLocationId();
118         if (refType != null) {
119           Location refLoc = td2loc.get(refType);
120
121           assert (refLoc instanceof CompositeLocation);
122           CompositeLocation refCompLoc = (CompositeLocation) refLoc;
123
124           assert (refCompLoc.getTuple().at(0) instanceof DeltaLocation);
125           DeltaLocation refDelta = (DeltaLocation) refCompLoc.getTuple().at(0);
126
127           delta.addDeltaOperand(refDelta);
128           // compLoc.addLocation(refDelta);
129         }
130
131       }
132     }
133
134     // phase2 : checking assignments
135     toanalyze.addAll(classtable.getValueSet());
136     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
137     while (!toanalyze.isEmpty()) {
138       Object obj = toanalyze.iterator().next();
139       ClassDescriptor cd = (ClassDescriptor) obj;
140       toanalyze.remove(cd);
141       if (cd.isClassLibrary()) {
142         // doesn't care about class libraries now
143         continue;
144       }
145       checkClass(cd);
146       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
147         MethodDescriptor md = (MethodDescriptor) method_it.next();
148         try {
149           checkMethodBody(cd, md);
150         } catch (Error e) {
151           System.out.println("Error in " + md);
152           throw e;
153         }
154       }
155     }
156
157   }
158
159   private void checkDeclarationInMethodBody(ClassDescriptor cd, MethodDescriptor md) {
160     BlockNode bn = state.getMethodBody(md);
161     checkDeclarationInBlockNode(md, md.getParameterTable(), bn);
162   }
163
164   private void checkDeclarationInBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
165     bn.getVarTable().setParent(nametable);
166     for (int i = 0; i < bn.size(); i++) {
167       BlockStatementNode bsn = bn.get(i);
168       checkDeclarationInBlockStatementNode(md, bn.getVarTable(), bsn);
169     }
170   }
171
172   private void checkDeclarationInBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
173       BlockStatementNode bsn) {
174
175     switch (bsn.kind()) {
176     case Kind.SubBlockNode:
177       checkDeclarationInSubBlockNode(md, nametable, (SubBlockNode) bsn);
178       return;
179     case Kind.DeclarationNode:
180       checkDeclarationNode(md, nametable, (DeclarationNode) bsn);
181       break;
182     case Kind.LoopNode:
183       checkDeclarationInLoopNode(md, nametable, (LoopNode) bsn);
184     }
185   }
186
187   private void checkDeclarationInLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln) {
188
189     if (ln.getType() == LoopNode.FORLOOP) {
190       // check for loop case
191       ClassDescriptor cd = md.getClassDesc();
192       BlockNode bn = ln.getInitializer();
193       for (int i = 0; i < bn.size(); i++) {
194         BlockStatementNode bsn = bn.get(i);
195         checkDeclarationInBlockStatementNode(md, nametable, bsn);
196       }
197     }
198   }
199
200   private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
201     BlockNode bn = state.getMethodBody(md);
202     checkLocationFromBlockNode(md, md.getParameterTable(), bn);
203   }
204
205   private CompositeLocation checkLocationFromBlockNode(MethodDescriptor md, SymbolTable nametable,
206       BlockNode bn) {
207     // it will return the lowest location in the block node
208     CompositeLocation lowestLoc = null;
209     for (int i = 0; i < bn.size(); i++) {
210       BlockStatementNode bsn = bn.get(i);
211       CompositeLocation bLoc = checkLocationFromBlockStatementNode(md, bn.getVarTable(), bsn);
212
213       if (lowestLoc == null) {
214         lowestLoc = bLoc;
215       } else {
216         if (CompositeLattice.isGreaterThan(lowestLoc, bLoc, md.getClassDesc())) {
217           lowestLoc = bLoc;
218         }
219       }
220     }
221     return lowestLoc;
222   }
223
224   private CompositeLocation checkLocationFromBlockStatementNode(MethodDescriptor md,
225       SymbolTable nametable, BlockStatementNode bsn) {
226
227     switch (bsn.kind()) {
228     case Kind.BlockExpressionNode:
229       return checkLocationFromBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
230
231     case Kind.DeclarationNode:
232       return checkLocationFromDeclarationNode(md, nametable, (DeclarationNode) bsn);
233
234     case Kind.IfStatementNode:
235       return checkLocationFromIfStatementNode(md, nametable, (IfStatementNode) bsn);
236
237     case Kind.LoopNode:
238       return checkLocationFromLoopNode(md, nametable, (LoopNode) bsn);
239
240     case Kind.ReturnNode:
241       // checkLocationFromReturnNode(md, nametable, (ReturnNode) bsn);
242       return null;
243
244     case Kind.SubBlockNode:
245       return checkLocationFromSubBlockNode(md, nametable, (SubBlockNode) bsn);
246
247     case Kind.ContinueBreakNode:
248       // checkLocationFromContinueBreakNode(md, nametable,(ContinueBreakNode)
249       // bsn);
250       return null;
251     }
252     return null;
253   }
254
255   private CompositeLocation checkLocationFromLoopNode(MethodDescriptor md, SymbolTable nametable,
256       LoopNode ln) {
257
258     ClassDescriptor cd = md.getClassDesc();
259     if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) {
260
261       CompositeLocation condLoc =
262           checkLocationFromExpressionNode(md, nametable, ln.getCondition(), new CompositeLocation(
263               cd));
264       CompositeLocation bodyLoc = checkLocationFromBlockNode(md, nametable, ln.getBody());
265
266       if (!CompositeLattice.isGreaterThan(condLoc, bodyLoc, cd)) {
267         // loop condition should be higher than loop body
268         throw new Error(
269             "The location of the while-condition statement is lower than the loop body at "
270                 + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine());
271       }
272
273       return bodyLoc;
274
275     } else {
276       // check for loop case
277       BlockNode bn = ln.getInitializer();
278
279       // calculate glb location of condition and update statements
280       CompositeLocation condLoc =
281           checkLocationFromExpressionNode(md, bn.getVarTable(), ln.getCondition(),
282               new CompositeLocation(cd));
283       CompositeLocation updateLoc =
284           checkLocationFromBlockNode(md, bn.getVarTable(), ln.getUpdate());
285
286       Set<CompositeLocation> glbInputSet = new HashSet<CompositeLocation>();
287       glbInputSet.add(condLoc);
288       glbInputSet.add(updateLoc);
289
290       CompositeLocation glbLocOfForLoopCond = CompositeLattice.calculateGLB(cd, glbInputSet, cd);
291       CompositeLocation blockLoc = checkLocationFromBlockNode(md, bn.getVarTable(), ln.getBody());
292
293       if (blockLoc == null) {
294         // when there is no statement in the loop body
295         return glbLocOfForLoopCond;
296       }
297
298       if (!CompositeLattice.isGreaterThan(glbLocOfForLoopCond, blockLoc, cd)) {
299         throw new Error(
300             "The location of the for-condition statement is lower than the for-loop body at "
301                 + cd.getSourceFileName() + ":" + ln.getCondition().getNumLine());
302       }
303       return blockLoc;
304     }
305
306   }
307
308   private CompositeLocation checkLocationFromSubBlockNode(MethodDescriptor md,
309       SymbolTable nametable, SubBlockNode sbn) {
310     return checkLocationFromBlockNode(md, nametable, sbn.getBlockNode());
311   }
312
313   private CompositeLocation checkLocationFromIfStatementNode(MethodDescriptor md,
314       SymbolTable nametable, IfStatementNode isn) {
315
316     ClassDescriptor localCD = md.getClassDesc();
317     Set<CompositeLocation> glbInputSet = new HashSet<CompositeLocation>();
318
319     CompositeLocation condLoc = new CompositeLocation(localCD);
320     condLoc = checkLocationFromExpressionNode(md, nametable, isn.getCondition(), condLoc);
321     glbInputSet.add(condLoc);
322
323     System.out.println(isn.getCondition().printNode(0) + ":::condLoc=" + condLoc);
324
325     CompositeLocation locTrueBlock = checkLocationFromBlockNode(md, nametable, isn.getTrueBlock());
326     glbInputSet.add(locTrueBlock);
327     System.out.println(isn.getTrueBlock().printNode(0) + ":::trueLoc=" + locTrueBlock);
328
329     // here, the location of conditional block should be higher than the
330     // location of true/false blocks
331
332     if (!CompositeLattice.isGreaterThan(condLoc, locTrueBlock, localCD)) {
333       // error
334       throw new Error(
335           "The location of the if-condition statement is lower than the conditional block at "
336               + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine());
337     }
338
339     if (isn.getFalseBlock() != null) {
340       CompositeLocation locFalseBlock =
341           checkLocationFromBlockNode(md, nametable, isn.getFalseBlock());
342       glbInputSet.add(locFalseBlock);
343       System.out.println(isn.getFalseBlock().printNode(0) + ":::falseLoc=" + locFalseBlock);
344
345       if (!CompositeLattice.isGreaterThan(condLoc, locFalseBlock, localCD)) {
346         // error
347         throw new Error(
348             "The location of the if-condition statement is lower than the conditional block at "
349                 + localCD.getSourceFileName() + ":" + isn.getCondition().getNumLine());
350       }
351
352     }
353
354     // return GLB location of condition, true, and false block
355     CompositeLocation glbLoc = CompositeLattice.calculateGLB(localCD, glbInputSet, localCD);
356
357     return glbLoc;
358   }
359
360   private CompositeLocation checkLocationFromDeclarationNode(MethodDescriptor md,
361       SymbolTable nametable, DeclarationNode dn) {
362     VarDescriptor vd = dn.getVarDescriptor();
363
364     Location destLoc = td2loc.get(vd.getType());
365
366     ClassDescriptor localCD = md.getClassDesc();
367     if (dn.getExpression() != null) {
368       CompositeLocation expressionLoc = new CompositeLocation(localCD);
369       expressionLoc =
370           checkLocationFromExpressionNode(md, nametable, dn.getExpression(), expressionLoc);
371
372       if (expressionLoc != null) {
373         System.out.println("expressionLoc=" + expressionLoc + " and destLoc=" + destLoc);
374
375         // checking location order
376         if (!CompositeLattice.isGreaterThan(expressionLoc, destLoc, localCD)) {
377           throw new Error("The value flow from " + expressionLoc + " to " + destLoc
378               + " does not respect location hierarchy on the assignment " + dn.printNode(0));
379         }
380       }
381       return expressionLoc;
382
383     } else {
384       return null;
385     }
386
387   }
388
389   private void checkDeclarationInSubBlockNode(MethodDescriptor md, SymbolTable nametable,
390       SubBlockNode sbn) {
391     checkDeclarationInBlockNode(md, nametable, sbn.getBlockNode());
392   }
393
394   private CompositeLocation checkLocationFromBlockExpressionNode(MethodDescriptor md,
395       SymbolTable nametable, BlockExpressionNode ben) {
396     return checkLocationFromExpressionNode(md, nametable, ben.getExpression(), null);
397   }
398
399   private CompositeLocation checkLocationFromExpressionNode(MethodDescriptor md,
400       SymbolTable nametable, ExpressionNode en, CompositeLocation loc) {
401
402     switch (en.kind()) {
403
404     case Kind.AssignmentNode:
405       return checkLocationFromAssignmentNode(md, nametable, (AssignmentNode) en, loc);
406
407     case Kind.FieldAccessNode:
408       return checkLocationFromFieldAccessNode(md, nametable, (FieldAccessNode) en, loc);
409
410     case Kind.NameNode:
411       return checkLocationFromNameNode(md, nametable, (NameNode) en, loc);
412
413     case Kind.OpNode:
414       return checkLocationFromOpNode(md, nametable, (OpNode) en);
415
416     case Kind.CreateObjectNode:
417       // checkCreateObjectNode(md, nametable, (CreateObjectNode) en, td);
418       return null;
419
420     case Kind.ArrayAccessNode:
421       // checkArrayAccessNode(md, nametable, (ArrayAccessNode) en, td);
422       return null;
423
424     case Kind.LiteralNode:
425       return checkLocationFromLiteralNode(md, nametable, (LiteralNode) en, loc);
426
427     case Kind.MethodInvokeNode:
428       // checkMethodInvokeNode(md,nametable,(MethodInvokeNode)en,td);
429       return null;
430
431     case Kind.OffsetNode:
432       // checkOffsetNode(md, nametable, (OffsetNode)en, td);
433       return null;
434
435     case Kind.TertiaryNode:
436       // checkTertiaryNode(md, nametable, (TertiaryNode)en, td);
437       return null;
438
439     case Kind.InstanceOfNode:
440       // checkInstanceOfNode(md, nametable, (InstanceOfNode) en, td);
441       return null;
442
443     case Kind.ArrayInitializerNode:
444       // checkArrayInitializerNode(md, nametable, (ArrayInitializerNode) en,
445       // td);
446       return null;
447
448     case Kind.ClassTypeNode:
449       // checkClassTypeNode(md, nametable, (ClassTypeNode) en, td);
450       return null;
451
452     default:
453       return null;
454
455     }
456
457   }
458
459   private CompositeLocation checkLocationFromOpNode(MethodDescriptor md, SymbolTable nametable,
460       OpNode on) {
461
462     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(md.getClassDesc());
463
464     ClassDescriptor cd = md.getClassDesc();
465     CompositeLocation leftLoc = new CompositeLocation(cd);
466     leftLoc = checkLocationFromExpressionNode(md, nametable, on.getLeft(), leftLoc);
467
468     CompositeLocation rightLoc = new CompositeLocation(cd);
469     if (on.getRight() != null) {
470       rightLoc = checkLocationFromExpressionNode(md, nametable, on.getRight(), rightLoc);
471     }
472
473     System.out.println("checking op node=" + on.printNode(0));
474     System.out.println("left loc=" + leftLoc + " from " + on.getLeft().getClass());
475     System.out.println("right loc=" + rightLoc);
476
477     Operation op = on.getOp();
478
479     switch (op.getOp()) {
480
481     case Operation.UNARYPLUS:
482     case Operation.UNARYMINUS:
483     case Operation.LOGIC_NOT:
484       // single operand
485       on.setType(new TypeDescriptor(TypeDescriptor.BOOLEAN));
486       break;
487
488     case Operation.LOGIC_OR:
489     case Operation.LOGIC_AND:
490     case Operation.COMP:
491     case Operation.BIT_OR:
492     case Operation.BIT_XOR:
493     case Operation.BIT_AND:
494     case Operation.ISAVAILABLE:
495     case Operation.EQUAL:
496     case Operation.NOTEQUAL:
497     case Operation.LT:
498     case Operation.GT:
499     case Operation.LTE:
500     case Operation.GTE:
501     case Operation.ADD:
502     case Operation.SUB:
503     case Operation.MULT:
504     case Operation.DIV:
505     case Operation.MOD:
506     case Operation.LEFTSHIFT:
507     case Operation.RIGHTSHIFT:
508     case Operation.URIGHTSHIFT:
509
510       Set<CompositeLocation> inputSet = new HashSet<CompositeLocation>();
511       inputSet.add(leftLoc);
512       inputSet.add(rightLoc);
513       CompositeLocation glbCompLoc = CompositeLattice.calculateGLB(cd, inputSet, cd);
514       return glbCompLoc;
515
516     default:
517       throw new Error(op.toString());
518     }
519
520     return null;
521
522   }
523
524   private CompositeLocation checkLocationFromLiteralNode(MethodDescriptor md,
525       SymbolTable nametable, LiteralNode en, CompositeLocation loc) {
526
527     // literal value has the top location so that value can be flowed into any
528     // location
529     Location literalLoc = Location.createTopLocation(md.getClassDesc());
530     loc.addLocation(literalLoc);
531     return loc;
532
533   }
534
535   private CompositeLocation checkLocationFromNameNode(MethodDescriptor md, SymbolTable nametable,
536       NameNode nn, CompositeLocation loc) {
537
538     NameDescriptor nd = nn.getName();
539     if (nd.getBase() != null) {
540       loc = checkLocationFromExpressionNode(md, nametable, nn.getExpression(), loc);
541     } else {
542
543       String varname = nd.toString();
544       Descriptor d = (Descriptor) nametable.get(varname);
545
546       Location localLoc = null;
547       if (d instanceof VarDescriptor) {
548         VarDescriptor vd = (VarDescriptor) d;
549         localLoc = td2loc.get(vd.getType());
550       } else if (d instanceof FieldDescriptor) {
551         FieldDescriptor fd = (FieldDescriptor) d;
552         localLoc = td2loc.get(fd.getType());
553       }
554       assert (localLoc != null);
555
556       if (localLoc instanceof CompositeLocation) {
557         loc = (CompositeLocation) localLoc;
558       } else {
559         loc.addLocation(localLoc);
560       }
561     }
562
563     return loc;
564   }
565
566   private CompositeLocation checkLocationFromFieldAccessNode(MethodDescriptor md,
567       SymbolTable nametable, FieldAccessNode fan, CompositeLocation loc) {
568     FieldDescriptor fd = fan.getField();
569     Location fieldLoc = td2loc.get(fd.getType());
570     loc.addLocation(fieldLoc);
571
572     ExpressionNode left = fan.getExpression();
573     return checkLocationFromExpressionNode(md, nametable, left, loc);
574   }
575
576   private CompositeLocation checkLocationFromAssignmentNode(MethodDescriptor md,
577       SymbolTable nametable, AssignmentNode an, CompositeLocation loc) {
578     System.out.println("checkAssignmentNode=" + an.printNode(0));
579
580     ClassDescriptor localCD = md.getClassDesc();
581
582     boolean postinc = true;
583     if (an.getOperation().getBaseOp() == null
584         || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation()
585             .getBaseOp().getOp() != Operation.POSTDEC))
586       postinc = false;
587
588     CompositeLocation srcLocation = new CompositeLocation(localCD);
589     if (!postinc) {
590       if (an.getSrc() instanceof CreateObjectNode) {
591         srcLocation = new CompositeLocation(localCD);
592         srcLocation.addLocation(Location.createTopLocation(localCD));
593       } else {
594         srcLocation = new CompositeLocation(localCD);
595         srcLocation = checkLocationFromExpressionNode(md, nametable, an.getSrc(), srcLocation);
596       }
597     }
598
599     CompositeLocation destLocation = new CompositeLocation(localCD);
600
601     destLocation = checkLocationFromExpressionNode(md, nametable, an.getDest(), destLocation);
602
603     if (!CompositeLattice.isGreaterThan(srcLocation, destLocation, localCD)) {
604       throw new Error("The value flow from " + srcLocation + " to " + destLocation
605           + " does not respect location hierarchy on the assignment " + an.printNode(0));
606     }
607
608     return destLocation;
609   }
610
611   private Location createCompositeLocation(FieldAccessNode fan, Location loc) {
612
613     FieldDescriptor field = fan.getField();
614     ClassDescriptor fieldCD = field.getClassDescriptor();
615
616     assert (field.getType().getAnnotationMarkers().size() == 1);
617
618     AnnotationDescriptor locAnnotation = field.getType().getAnnotationMarkers().elementAt(0);
619     if (locAnnotation.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
620       // single location
621
622     } else {
623       // delta location
624     }
625
626     // Location localLoc=new Location(field.getClassDescriptor(),field.get)
627
628     // System.out.println("creatingComposite's field="+field+" localLoc="+localLoc);
629     ExpressionNode leftNode = fan.getExpression();
630     System.out.println("creatingComposite's leftnode=" + leftNode.printNode(0));
631
632     return loc;
633   }
634
635   private void checkDeclarationNode(MethodDescriptor md, SymbolTable nametable, DeclarationNode dn) {
636
637     ClassDescriptor cd = md.getClassDesc();
638     VarDescriptor vd = dn.getVarDescriptor();
639     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
640
641     // currently enforce every variable to have corresponding location
642     if (annotationVec.size() == 0) {
643       throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
644           + md.getSymbol() + " of the class " + cd.getSymbol());
645     }
646
647     if (annotationVec.size() > 1) {
648       // variable can have at most one location
649       throw new Error(vd.getSymbol() + " has more than one location.");
650     }
651
652     AnnotationDescriptor ad = annotationVec.elementAt(0);
653
654     if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
655
656       // check if location is defined
657       String locationID = ad.getMarker();
658       Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
659
660       if (lattice == null || (!lattice.containsKey(locationID))) {
661         throw new Error("Location " + locationID
662             + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
663       }
664
665       Location loc = new Location(cd, locationID);
666       td2loc.put(vd.getType(), loc);
667
668     } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
669       if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
670
671         CompositeLocation compLoc = new CompositeLocation(cd);
672
673         if (ad.getData().length() == 0) {
674           throw new Error("Delta function of " + vd.getSymbol() + " does not have any locations: "
675               + cd.getSymbol() + ".");
676         }
677
678         String deltaStr = ad.getData();
679         if (deltaStr.startsWith("LOC(")) {
680
681           if (!deltaStr.endsWith(")")) {
682             throw new Error("The declaration of the delta location is wrong at "
683                 + cd.getSourceFileName() + ":" + dn.getNumLine());
684           }
685           String locationOperand = deltaStr.substring(4, deltaStr.length() - 1);
686
687           nametable.get(locationOperand);
688           Descriptor d = (Descriptor) nametable.get(locationOperand);
689
690           if (d instanceof VarDescriptor) {
691             VarDescriptor varDescriptor = (VarDescriptor) d;
692             DeltaLocation deltaLoc = new DeltaLocation(cd, varDescriptor.getType());
693             // td2loc.put(vd.getType(), compLoc);
694             compLoc.addLocation(deltaLoc);
695           } else if (d instanceof FieldDescriptor) {
696             throw new Error("Applying delta operation to the field " + locationOperand
697                 + " is not allowed at " + cd.getSourceFileName() + ":" + dn.getNumLine());
698           }
699         } else {
700           StringTokenizer token = new StringTokenizer(deltaStr, ",");
701           DeltaLocation deltaLoc = new DeltaLocation(cd);
702
703           while (token.hasMoreTokens()) {
704             String deltaOperand = token.nextToken();
705             ClassDescriptor deltaCD = id2cd.get(deltaOperand);
706             if (deltaCD == null) {
707               // delta operand is not defined in the location hierarchy
708               throw new Error("Delta operand '" + deltaOperand + "' of declaration node '" + vd
709                   + "' is not defined by location hierarchies.");
710             }
711
712             Location loc = new Location(deltaCD, deltaOperand);
713             deltaLoc.addDeltaOperand(loc);
714           }
715           compLoc.addLocation(deltaLoc);
716
717         }
718
719         td2loc.put(vd.getType(), compLoc);
720         System.out.println("vd=" + vd + " is assigned by " + compLoc);
721
722       }
723     }
724
725   }
726
727   private void checkClass(ClassDescriptor cd) {
728     // Check to see that methods respects ss property
729     for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
730       MethodDescriptor md = (MethodDescriptor) method_it.next();
731       checkMethodDeclaration(cd, md);
732     }
733   }
734
735   private void checkDeclarationInClass(ClassDescriptor cd) {
736     // Check to see that fields are okay
737     for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
738       FieldDescriptor fd = (FieldDescriptor) field_it.next();
739       checkFieldDeclaration(cd, fd);
740     }
741   }
742
743   private void checkMethodDeclaration(ClassDescriptor cd, MethodDescriptor md) {
744     // TODO
745   }
746
747   private void checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
748
749     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
750
751     // currently enforce every variable to have corresponding location
752     if (annotationVec.size() == 0) {
753       throw new Error("Location is not assigned to the field " + fd.getSymbol() + " of the class "
754           + cd.getSymbol());
755     }
756
757     if (annotationVec.size() > 1) {
758       // variable can have at most one location
759       throw new Error("Field " + fd.getSymbol() + " of class " + cd
760           + " has more than one location.");
761     }
762
763     // check if location is defined
764     AnnotationDescriptor ad = annotationVec.elementAt(0);
765     if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
766       String locationID = annotationVec.elementAt(0).getMarker();
767       Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
768
769       if (lattice == null || (!lattice.containsKey(locationID))) {
770         throw new Error("Location " + locationID
771             + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
772       }
773
774       Location localLoc = new Location(cd, locationID);
775       td2loc.put(fd.getType(), localLoc);
776
777     } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
778       if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
779
780         if (ad.getData().length() == 0) {
781           throw new Error("Delta function of " + fd.getSymbol() + " does not have any locations: "
782               + cd.getSymbol() + ".");
783         }
784
785         CompositeLocation compLoc = new CompositeLocation(cd);
786         DeltaLocation deltaLoc = new DeltaLocation(cd);
787
788         StringTokenizer token = new StringTokenizer(ad.getData(), ",");
789         while (token.hasMoreTokens()) {
790           String deltaOperand = token.nextToken();
791           ClassDescriptor deltaCD = id2cd.get(deltaOperand);
792           if (deltaCD == null) {
793             // delta operand is not defined in the location hierarchy
794             throw new Error("Delta operand '" + deltaOperand + "' of field node '" + fd
795                 + "' is not defined by location hierarchies.");
796           }
797
798           Location loc = new Location(deltaCD, deltaOperand);
799           deltaLoc.addDeltaOperand(loc);
800         }
801         compLoc.addLocation(deltaLoc);
802         td2loc.put(fd.getType(), compLoc);
803
804       }
805     }
806
807   }
808
809   static class CompositeLattice {
810
811     public static boolean isGreaterThan(Location loc1, Location loc2, ClassDescriptor priorityCD) {
812
813       System.out.println("isGreaterThan=" + loc1 + " ? " + loc2);
814       CompositeLocation compLoc1;
815       CompositeLocation compLoc2;
816
817       if (loc1 instanceof CompositeLocation) {
818         compLoc1 = (CompositeLocation) loc1;
819       } else {
820         // create a bogus composite location for a single location
821         compLoc1 = new CompositeLocation(loc1.getClassDescriptor());
822         compLoc1.addLocation(loc1);
823       }
824
825       if (loc2 instanceof CompositeLocation) {
826         compLoc2 = (CompositeLocation) loc2;
827       } else {
828         // create a bogus composite location for a single location
829         compLoc2 = new CompositeLocation(loc2.getClassDescriptor());
830         compLoc2.addLocation(loc2);
831       }
832
833       // comparing two composite locations
834       System.out.println("compare base location=" + compLoc1 + " ? " + compLoc2);
835
836       int baseCompareResult = compareBaseLocationSet(compLoc1, compLoc2, priorityCD);
837       if (baseCompareResult == ComparisonResult.EQUAL) {
838         if (compareDelta(compLoc1, compLoc2) == ComparisonResult.GREATER) {
839           return true;
840         } else {
841           return false;
842         }
843       } else if (baseCompareResult == ComparisonResult.GREATER) {
844         return true;
845       } else {
846         return false;
847       }
848
849     }
850
851     private static int compareDelta(CompositeLocation compLoc1, CompositeLocation compLoc2) {
852
853       if (compLoc1.getNumofDelta() < compLoc2.getNumofDelta()) {
854         return ComparisonResult.GREATER;
855       } else {
856         return ComparisonResult.LESS;
857       }
858     }
859
860     private static int compareBaseLocationSet(CompositeLocation compLoc1,
861         CompositeLocation compLoc2, ClassDescriptor priorityCD) {
862
863       // if compLoc1 is greater than compLoc2, return true
864       // else return false;
865
866       Map<ClassDescriptor, Location> cd2loc1 = compLoc1.getCd2Loc();
867       Map<ClassDescriptor, Location> cd2loc2 = compLoc2.getCd2Loc();
868
869       // compare first the priority loc elements
870       Location priorityLoc1 = cd2loc1.get(priorityCD);
871       Location priorityLoc2 = cd2loc2.get(priorityCD);
872
873       assert (priorityLoc1.getClassDescriptor().equals(priorityLoc2.getClassDescriptor()));
874
875       ClassDescriptor cd = priorityLoc1.getClassDescriptor();
876       Lattice<String> locationOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd);
877
878       if (priorityLoc1.getLocIdentifier().equals(priorityLoc2.getLocIdentifier())) {
879         // have the same level of local hierarchy
880       } else if (locationOrder.isGreaterThan(priorityLoc1.getLocIdentifier(), priorityLoc2
881           .getLocIdentifier())) {
882         // if priority loc of compLoc1 is higher than compLoc2
883         // then, compLoc 1 is higher than compLoc2
884         return ComparisonResult.GREATER;
885       } else {
886         // if priority loc of compLoc1 is NOT higher than compLoc2
887         // then, compLoc 1 is NOT higher than compLoc2
888         return ComparisonResult.LESS;
889       }
890
891       // compare base locations except priority by class descriptor
892       Set<ClassDescriptor> keySet1 = cd2loc1.keySet();
893       int numEqualLoc = 0;
894
895       for (Iterator iterator = keySet1.iterator(); iterator.hasNext();) {
896         ClassDescriptor cd1 = (ClassDescriptor) iterator.next();
897
898         Location loc1 = cd2loc1.get(cd1);
899         Location loc2 = cd2loc2.get(cd1);
900
901         if (priorityLoc1.equals(loc1)) {
902           continue;
903         }
904
905         if (loc2 == null) {
906           // if comploc2 doesn't have corresponding location,
907           // then we determines that comploc1 is lower than comploc 2
908           return ComparisonResult.LESS;
909         }
910
911         System.out.println("lattice comparison:" + loc1.getLocIdentifier() + " ? "
912             + loc2.getLocIdentifier());
913         locationOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd1);
914         if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
915           // have the same level of local hierarchy
916           numEqualLoc++;
917         } else if (!locationOrder.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
918           // if one element of composite location 1 is not higher than composite
919           // location 2
920           // then, composite loc 1 is not higher than composite loc 2
921
922           System.out.println(compLoc1 + " < " + compLoc2);
923           return ComparisonResult.LESS;
924         }
925
926       }
927
928       if (numEqualLoc == compLoc1.getBaseLocationSize()) {
929         System.out.println(compLoc1 + " == " + compLoc2);
930         return ComparisonResult.EQUAL;
931       }
932
933       System.out.println(compLoc1 + " > " + compLoc2);
934       return ComparisonResult.GREATER;
935     }
936
937     public static CompositeLocation calculateGLB(ClassDescriptor cd,
938         Set<CompositeLocation> inputSet, ClassDescriptor priorityCD) {
939
940       CompositeLocation glbCompLoc = new CompositeLocation(cd);
941       int maxDeltaFunction = 0;
942
943       // calculate GLB of priority element first
944
945       Hashtable<ClassDescriptor, Set<Location>> cd2locSet =
946           new Hashtable<ClassDescriptor, Set<Location>>();
947
948       // creating mapping from class to set of locations
949       for (Iterator iterator = inputSet.iterator(); iterator.hasNext();) {
950         CompositeLocation compLoc = (CompositeLocation) iterator.next();
951
952         int numOfDelta = compLoc.getNumofDelta();
953         if (numOfDelta > maxDeltaFunction) {
954           maxDeltaFunction = numOfDelta;
955         }
956
957         Set<Location> baseLocationSet = compLoc.getBaseLocationSet();
958         for (Iterator iterator2 = baseLocationSet.iterator(); iterator2.hasNext();) {
959           Location locElement = (Location) iterator2.next();
960           ClassDescriptor locCD = locElement.getClassDescriptor();
961
962           Set<Location> locSet = cd2locSet.get(locCD);
963           if (locSet == null) {
964             locSet = new HashSet<Location>();
965           }
966           locSet.add(locElement);
967
968           cd2locSet.put(locCD, locSet);
969
970         }
971       }
972
973       Set<Location> locSetofClass = cd2locSet.get(priorityCD);
974       Set<String> locIdentifierSet = new HashSet<String>();
975
976       for (Iterator<Location> locIterator = locSetofClass.iterator(); locIterator.hasNext();) {
977         Location locElement = locIterator.next();
978         locIdentifierSet.add(locElement.getLocIdentifier());
979       }
980
981       Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(priorityCD);
982       String glbLocIdentifer = locOrder.getGLB(locIdentifierSet);
983
984       Location priorityGLB = new Location(priorityCD, glbLocIdentifer);
985
986       Set<CompositeLocation> sameGLBLoc = new HashSet<CompositeLocation>();
987
988       for (Iterator<CompositeLocation> iterator = inputSet.iterator(); iterator.hasNext();) {
989         CompositeLocation inputComploc = iterator.next();
990         Location locElement = inputComploc.getLocation(priorityCD);
991
992         if (locElement.equals(priorityGLB)) {
993           sameGLBLoc.add(inputComploc);
994         }
995       }
996       glbCompLoc.addLocation(priorityGLB);
997       if (sameGLBLoc.size() > 0) {
998         // if more than one location shares the same priority GLB
999         // need to calculate the rest of GLB loc
1000
1001         Set<Location> glbElementSet = new HashSet<Location>();
1002
1003         for (Iterator<ClassDescriptor> iterator = cd2locSet.keySet().iterator(); iterator.hasNext();) {
1004           ClassDescriptor localCD = iterator.next();
1005           if (!localCD.equals(priorityCD)) {
1006             Set<Location> localLocSet = cd2locSet.get(localCD);
1007             Set<String> LocalLocIdSet = new HashSet<String>();
1008
1009             for (Iterator<Location> locIterator = localLocSet.iterator(); locIterator.hasNext();) {
1010               Location locElement = locIterator.next();
1011               LocalLocIdSet.add(locElement.getLocIdentifier());
1012             }
1013
1014             Lattice<String> localOrder = (Lattice<String>) state.getCd2LocationOrder().get(localCD);
1015             Location localGLBLoc = new Location(localCD, localOrder.getGLB(LocalLocIdSet));
1016             glbCompLoc.addLocation(localGLBLoc);
1017           }
1018         }
1019       } else {
1020         // if priority glb loc is lower than all of input loc
1021         // assign top location to the rest of loc element
1022
1023         for (Iterator<ClassDescriptor> iterator = cd2locSet.keySet().iterator(); iterator.hasNext();) {
1024           ClassDescriptor localCD = iterator.next();
1025           if (!localCD.equals(priorityCD)) {
1026             Location localGLBLoc = Location.createTopLocation(localCD);
1027             glbCompLoc.addLocation(localGLBLoc);
1028           }
1029
1030         }
1031
1032       }
1033
1034       return glbCompLoc;
1035
1036     }
1037
1038   }
1039
1040   class ComparisonResult {
1041
1042     public static final int GREATER = 0;
1043     public static final int EQUAL = 1;
1044     public static final int LESS = 2;
1045     int result;
1046
1047   }
1048
1049 }