1 package Analysis.SSJava;
3 import java.util.HashSet;
4 import java.util.Hashtable;
5 import java.util.Iterator;
8 import java.util.StringTokenizer;
9 import java.util.Vector;
11 import IR.AnnotationDescriptor;
12 import IR.ClassDescriptor;
14 import IR.FieldDescriptor;
15 import IR.MethodDescriptor;
16 import IR.NameDescriptor;
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.DeclarationNode;
27 import IR.Tree.ExpressionNode;
28 import IR.Tree.FieldAccessNode;
30 import IR.Tree.NameNode;
31 import IR.Tree.OpNode;
34 public class FlowDownCheck {
38 Hashtable<TypeDescriptor, Location> td2loc;
39 Hashtable<String, ClassDescriptor> id2cd;
41 public FlowDownCheck(State state) {
43 this.toanalyze = new HashSet();
44 this.td2loc = new Hashtable<TypeDescriptor, Location>();
49 id2cd = new Hashtable<String, ClassDescriptor>();
50 Hashtable cd2lattice = state.getCd2LocationOrder();
52 Set cdSet = cd2lattice.keySet();
53 for (Iterator iterator = cdSet.iterator(); iterator.hasNext();) {
54 ClassDescriptor cd = (ClassDescriptor) iterator.next();
55 Lattice<String> lattice = (Lattice<String>) cd2lattice.get(cd);
57 Set<String> locIdSet = lattice.getKeySet();
58 for (Iterator iterator2 = locIdSet.iterator(); iterator2.hasNext();) {
59 String locID = (String) iterator2.next();
66 public void flowDownCheck() {
68 SymbolTable classtable = state.getClassSymbolTable();
69 toanalyze.addAll(classtable.getValueSet());
70 toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
73 while (!toanalyze.isEmpty()) {
74 Object obj = toanalyze.iterator().next();
75 ClassDescriptor cd = (ClassDescriptor) obj;
77 if (cd.isClassLibrary()) {
78 // doesn't care about class libraries now
84 for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
85 MethodDescriptor md = (MethodDescriptor) method_it.next();
87 checkMethodBody(cd, md);
89 System.out.println("Error in " + md);
96 public void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
97 ClassDescriptor superdesc = cd.getSuperDesc();
98 if (superdesc != null) {
99 Set possiblematches = superdesc.getMethodTable().getSet(md.getSymbol());
100 for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) {
101 MethodDescriptor matchmd = (MethodDescriptor) methodit.next();
102 if (md.matches(matchmd)) {
103 if (matchmd.getModifiers().isFinal()) {
104 throw new Error("Try to override final method in method:" + md + " declared in " + cd);
109 BlockNode bn = state.getMethodBody(md);
110 checkBlockNode(md, md.getParameterTable(), bn);
113 public void checkBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
114 /* Link in the naming environment */
115 bn.getVarTable().setParent(nametable);
116 for (int i = 0; i < bn.size(); i++) {
117 BlockStatementNode bsn = bn.get(i);
118 checkBlockStatementNode(md, bn.getVarTable(), bsn);
122 public void checkBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
123 BlockStatementNode bsn) {
125 switch (bsn.kind()) {
126 case Kind.BlockExpressionNode:
127 checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
130 case Kind.DeclarationNode:
131 checkDeclarationNode(md, (DeclarationNode) bsn);
135 * switch (bsn.kind()) { case Kind.BlockExpressionNode:
136 * checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
139 * case Kind.DeclarationNode: checkDeclarationNode(md, nametable,
140 * (DeclarationNode) bsn); return;
142 * case Kind.TagDeclarationNode: checkTagDeclarationNode(md, nametable,
143 * (TagDeclarationNode) bsn); return;
145 * case Kind.IfStatementNode: checkIfStatementNode(md, nametable,
146 * (IfStatementNode) bsn); return;
148 * case Kind.SwitchStatementNode: checkSwitchStatementNode(md, nametable,
149 * (SwitchStatementNode) bsn); return;
151 * case Kind.LoopNode: checkLoopNode(md, nametable, (LoopNode) bsn); return;
153 * case Kind.ReturnNode: checkReturnNode(md, nametable, (ReturnNode) bsn);
156 * case Kind.TaskExitNode: checkTaskExitNode(md, nametable, (TaskExitNode)
159 * case Kind.SubBlockNode: checkSubBlockNode(md, nametable, (SubBlockNode)
162 * case Kind.AtomicNode: checkAtomicNode(md, nametable, (AtomicNode) bsn);
165 * case Kind.SynchronizedNode: checkSynchronizedNode(md, nametable,
166 * (SynchronizedNode) bsn); return;
168 * case Kind.ContinueBreakNode: checkContinueBreakNode(md, nametable,
169 * (ContinueBreakNode) bsn); return;
171 * case Kind.SESENode: case Kind.GenReachNode: // do nothing, no semantic
172 * check for SESEs return; }
174 // throw new Error();
177 void checkBlockExpressionNode(MethodDescriptor md, SymbolTable nametable, BlockExpressionNode ben) {
178 checkExpressionNode(md, nametable, ben.getExpression(), null);
181 void checkExpressionNode(MethodDescriptor md, SymbolTable nametable, ExpressionNode en,
185 case Kind.AssignmentNode:
186 checkAssignmentNode(md, nametable, (AssignmentNode) en, td);
190 checkOpNode(md, nametable, (OpNode) en, td);
193 case Kind.FieldAccessNode:
194 checkFieldAccessNode(md, nametable, (FieldAccessNode) en, td);
198 checkNameNode(md, nametable, (NameNode) en, td);
204 * switch(en.kind()) { case Kind.AssignmentNode:
205 * checkAssignmentNode(md,nametable,(AssignmentNode)en,td); return;
207 * case Kind.CastNode: checkCastNode(md,nametable,(CastNode)en,td); return;
209 * case Kind.CreateObjectNode:
210 * checkCreateObjectNode(md,nametable,(CreateObjectNode)en,td); return;
212 * case Kind.FieldAccessNode:
213 * checkFieldAccessNode(md,nametable,(FieldAccessNode)en,td); return;
215 * case Kind.ArrayAccessNode:
216 * checkArrayAccessNode(md,nametable,(ArrayAccessNode)en,td); return;
218 * case Kind.LiteralNode: checkLiteralNode(md,nametable,(LiteralNode)en,td);
221 * case Kind.MethodInvokeNode:
222 * checkMethodInvokeNode(md,nametable,(MethodInvokeNode)en,td); return;
224 * case Kind.NameNode: checkNameNode(md,nametable,(NameNode)en,td); return;
226 * case Kind.OpNode: checkOpNode(md,nametable,(OpNode)en,td); return;
228 * case Kind.OffsetNode: checkOffsetNode(md, nametable, (OffsetNode)en, td);
231 * case Kind.TertiaryNode: checkTertiaryNode(md, nametable,
232 * (TertiaryNode)en, td); return;
234 * case Kind.InstanceOfNode: checkInstanceOfNode(md, nametable,
235 * (InstanceOfNode) en, td); return;
237 * case Kind.ArrayInitializerNode: checkArrayInitializerNode(md, nametable,
238 * (ArrayInitializerNode) en, td); return;
240 * case Kind.ClassTypeNode: checkClassTypeNode(md, nametable,
241 * (ClassTypeNode) en, td); return; }
245 void checkNameNode(MethodDescriptor md, SymbolTable nametable, NameNode nn, TypeDescriptor td) {
249 void checkFieldAccessNode(MethodDescriptor md, SymbolTable nametable, FieldAccessNode fan,
252 ExpressionNode left = fan.getExpression();
253 checkExpressionNode(md, nametable, left, null);
254 TypeDescriptor ltd = left.getType();
255 String fieldname = fan.getFieldName();
260 void checkOpNode(MethodDescriptor md, SymbolTable nametable, OpNode on, TypeDescriptor td) {
262 Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(md.getClassDesc());
264 checkExpressionNode(md, nametable, on.getLeft(), null);
265 if (on.getRight() != null)
266 checkExpressionNode(md, nametable, on.getRight(), null);
268 TypeDescriptor ltd = on.getLeft().getType();
269 TypeDescriptor rtd = on.getRight() != null ? on.getRight().getType() : null;
271 if (ltd.getAnnotationMarkers().size() == 0) {
274 // ltd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
276 if (rtd != null && rtd.getAnnotationMarkers().size() == 0) {
279 // rtd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
282 System.out.println("checking op node");
283 System.out.println("td=" + td);
284 System.out.println("ltd=" + ltd);
285 System.out.println("rtd=" + rtd);
287 Operation op = on.getOp();
289 switch (op.getOp()) {
291 case Operation.UNARYPLUS:
292 case Operation.UNARYMINUS:
293 case Operation.LOGIC_NOT:
295 on.setType(new TypeDescriptor(TypeDescriptor.BOOLEAN));
298 case Operation.LOGIC_OR:
299 case Operation.LOGIC_AND:
301 case Operation.BIT_OR:
302 case Operation.BIT_XOR:
303 case Operation.BIT_AND:
304 case Operation.ISAVAILABLE:
305 case Operation.EQUAL:
306 case Operation.NOTEQUAL:
316 case Operation.LEFTSHIFT:
317 case Operation.RIGHTSHIFT:
318 case Operation.URIGHTSHIFT:
320 Set<String> operandSet = new HashSet<String>();
321 String leftLoc = ltd.getAnnotationMarkers().get(0).getMarker();
322 String rightLoc = rtd.getAnnotationMarkers().get(0).getMarker();
324 operandSet.add(leftLoc);
325 operandSet.add(rightLoc);
328 // String glbLoc = locOrder.getGLB(operandSet);
329 // on.getType().addAnnotationMarker(new AnnotationDescriptor(glbLoc));
330 // System.out.println(glbLoc + "<-" + leftLoc + " " + rightLoc);
335 throw new Error(op.toString());
339 String lhsLoc = td.getAnnotationMarkers().get(0).getMarker();
340 if (locOrder.isGreaterThan(lhsLoc, on.getType().getAnnotationMarkers().get(0).getMarker())) {
341 throw new Error("The location of LHS is higher than RHS: " + on.printNode(0));
347 void checkAssignmentNode(MethodDescriptor md, SymbolTable nametable, AssignmentNode an,
350 boolean postinc = true;
351 if (an.getOperation().getBaseOp() == null
352 || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation()
353 .getBaseOp().getOp() != Operation.POSTDEC))
356 checkExpressionNode(md, nametable, an.getSrc(), td);
359 ClassDescriptor cd = md.getClassDesc();
360 Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd);
363 Location destLocation = td2loc.get(an.getDest().getType());
364 Location srcLocation = td2loc.get(an.getSrc().getType());
367 if (!CompositeLattice.isGreaterThan(srcLocation, destLocation)) {
368 throw new Error("The value flow from " + srcLocation + " to " + destLocation
369 + " does not respect location hierarchy on the assignment " + an.printNode(0));
375 void checkDeclarationNode(MethodDescriptor md, DeclarationNode dn) {
377 ClassDescriptor cd = md.getClassDesc();
378 VarDescriptor vd = dn.getVarDescriptor();
379 Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
381 // currently enforce every variable to have corresponding location
382 if (annotationVec.size() == 0) {
383 throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
384 + md.getSymbol() + " of the class " + cd.getSymbol());
387 if (annotationVec.size() > 1) {
388 // variable can have at most one location
389 throw new Error(vd.getSymbol() + " has more than one location.");
392 AnnotationDescriptor ad = annotationVec.elementAt(0);
394 if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
396 // check if location is defined
397 String locationID = ad.getMarker();
398 Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
400 if (lattice == null || (!lattice.containsKey(locationID))) {
401 throw new Error("Location " + locationID
402 + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
405 Location loc = new Location(cd, locationID);
406 td2loc.put(vd.getType(), loc);
408 } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
409 if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
411 if (ad.getData().length() == 0) {
412 throw new Error("Delta function of " + vd.getSymbol() + " does not have any locations: "
413 + cd.getSymbol() + ".");
416 StringTokenizer token = new StringTokenizer(ad.getData(), ",");
418 CompositeLocation compLoc = new CompositeLocation(cd);
419 DeltaLocation deltaLoc = new DeltaLocation(cd);
421 while (token.hasMoreTokens()) {
422 String deltaOperand = token.nextToken();
423 ClassDescriptor deltaCD = id2cd.get(deltaOperand);
424 if (deltaCD == null) {
425 // delta operand is not defined in the location hierarchy
426 throw new Error("Delta operand '" + deltaOperand + "' of declaration node '" + vd
427 + "' is not defined by location hierarchies.");
430 Location loc = new Location(deltaCD, deltaOperand);
431 deltaLoc.addDeltaOperand(loc);
433 compLoc.addLocation(deltaLoc);
434 td2loc.put(vd.getType(), compLoc);
440 private void checkClass(ClassDescriptor cd) {
441 // Check to see that fields are okay
442 for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
443 FieldDescriptor fd = (FieldDescriptor) field_it.next();
444 checkFieldDeclaration(cd, fd);
447 // Check to see that methods respects ss property
448 for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
449 MethodDescriptor md = (MethodDescriptor) method_it.next();
450 checkMethodDeclaration(cd, md);
454 private void checkMethodDeclaration(ClassDescriptor cd, MethodDescriptor md) {
458 private void checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
460 Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
462 // currently enforce every variable to have corresponding location
463 if (annotationVec.size() == 0) {
464 throw new Error("Location is not assigned to the field " + fd.getSymbol() + " of the class "
468 if (annotationVec.size() > 1) {
469 // variable can have at most one location
470 throw new Error("Field " + fd.getSymbol() + " of class " + cd
471 + " has more than one location.");
474 // check if location is defined
475 AnnotationDescriptor ad = annotationVec.elementAt(0);
476 if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
477 String locationID = annotationVec.elementAt(0).getMarker();
478 Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
480 if (lattice == null || (!lattice.containsKey(locationID))) {
481 throw new Error("Location " + locationID
482 + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
484 } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
485 if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
487 if (ad.getData().length() == 0) {
488 throw new Error("Delta function of " + fd.getSymbol() + " does not have any locations: "
489 + cd.getSymbol() + ".");
492 CompositeLocation compLoc = new CompositeLocation(cd);
493 DeltaLocation deltaLoc = new DeltaLocation(cd);
495 StringTokenizer token = new StringTokenizer(ad.getData(), ",");
496 while (token.hasMoreTokens()) {
497 String deltaOperand = token.nextToken();
498 ClassDescriptor deltaCD = id2cd.get(deltaOperand);
499 if (deltaCD == null) {
500 // delta operand is not defined in the location hierarchy
501 throw new Error("Delta operand '" + deltaOperand + "' of field node '" + fd
502 + "' is not defined by location hierarchies.");
505 Location loc = new Location(deltaCD, deltaOperand);
506 deltaLoc.addDeltaOperand(loc);
508 compLoc.addLocation(deltaLoc);
509 td2loc.put(fd.getType(), compLoc);
516 static class CompositeLattice {
518 public static boolean isGreaterThan(Location loc1, Location loc2) {
520 CompositeLocation compLoc1;
521 CompositeLocation compLoc2;
523 if (loc1 instanceof CompositeLocation) {
524 compLoc1 = (CompositeLocation) loc1;
526 // create a bogus composite location for a single location
527 compLoc1 = new CompositeLocation(loc1.getClassDescriptor());
528 compLoc1.addLocation(loc1);
531 if (loc2 instanceof CompositeLocation) {
532 compLoc2 = (CompositeLocation) loc2;
534 // create a bogus composite location for a single location
535 compLoc2 = new CompositeLocation(loc2.getClassDescriptor());
536 compLoc2.addLocation(loc2);
539 // comparing two composite locations
541 System.out.println("compare base location=" + compLoc1 + " ? " + compLoc2);
543 int baseCompareResult = compareBaseLocationSet(compLoc1, compLoc2);
544 if (baseCompareResult == ComparisonResult.EQUAL) {
546 // need to compare # of delta operand
547 } else if (baseCompareResult == ComparisonResult.GREATER) {
556 private static int compareBaseLocationSet(CompositeLocation compLoc1, CompositeLocation compLoc2) {
558 // if compLoc1 is greater than compLoc2, return true
559 // else return false;
561 Map<ClassDescriptor, Location> cd2loc1 = compLoc1.getCd2Loc();
562 Map<ClassDescriptor, Location> cd2loc2 = compLoc2.getCd2Loc();
564 // compare base locations by class descriptor
566 Set<ClassDescriptor> keySet1 = cd2loc1.keySet();
570 for (Iterator iterator = keySet1.iterator(); iterator.hasNext();) {
571 ClassDescriptor cd1 = (ClassDescriptor) iterator.next();
573 Location loc1 = cd2loc1.get(cd1);
574 Location loc2 = cd2loc2.get(cd1);
577 // if comploc2 doesn't have corresponding location, then ignore this
583 Lattice<String> locationOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd1);
584 if (loc1.getLocIdentifier().equals(loc2.getLocIdentifier())) {
585 // have the same level of local hierarchy
587 } else if (!locationOrder.isGreaterThan(loc1.getLocIdentifier(), loc2.getLocIdentifier())) {
588 // if one element of composite location 1 is not higher than composite
590 // then, composite loc 1 is not higher than composite loc 2
592 System.out.println(compLoc1 + " < " + compLoc2);
593 return ComparisonResult.LESS;
598 if (numEqualLoc == compLoc1.getTupleSize()) {
599 System.out.println(compLoc1 + " == " + compLoc2);
600 return ComparisonResult.EQUAL;
603 System.out.println(compLoc1 + " > " + compLoc2);
604 return ComparisonResult.GREATER;
609 class ComparisonResult {
611 public static final int GREATER = 0;
612 public static final int EQUAL = 1;
613 public static final int LESS = 2;