Robust/src/Analysis/SSJava/FlowDownCheck.java

   1 package Analysis.SSJava;
   2
   3 import java.util.HashSet;
   4 import java.util.Iterator;
   5 import java.util.Set;
   6 import java.util.StringTokenizer;
   7 import java.util.Vector;
   8
   9 import IR.AnnotationDescriptor;
  10 import IR.ClassDescriptor;
  11 import IR.FieldDescriptor;
  12 import IR.MethodDescriptor;
  13 import IR.Operation;
  14 import IR.State;
  15 import IR.SymbolTable;
  16 import IR.TypeDescriptor;
  17 import IR.VarDescriptor;
  18 import IR.Tree.AssignmentNode;
  19 import IR.Tree.BlockExpressionNode;
  20 import IR.Tree.BlockNode;
  21 import IR.Tree.BlockStatementNode;
  22 import IR.Tree.DeclarationNode;
  23 import IR.Tree.ExpressionNode;
  24 import IR.Tree.Kind;
  25 import IR.Tree.OpNode;
  26 import Util.Lattice;
  27
  28 public class FlowDownCheck {
  29
  30   State state;
  31   HashSet toanalyze;
  32
  33   public FlowDownCheck(State state) {
  34     this.state = state;
  35     this.toanalyze = new HashSet();
  36   }
  37
  38   public void flowDownCheck() {
  39
  40     SymbolTable classtable = state.getClassSymbolTable();
  41     toanalyze.addAll(classtable.getValueSet());
  42     toanalyze.addAll(state.getTaskSymbolTable().getValueSet());
  43
  44     // Do methods next
  45     while (!toanalyze.isEmpty()) {
  46       Object obj = toanalyze.iterator().next();
  47       ClassDescriptor cd = (ClassDescriptor) obj;
  48       toanalyze.remove(cd);
  49       if (cd.isClassLibrary()) {
  50         // doesn't care about class libraries now
  51         continue;
  52       }
  53
  54       checkClass(cd);
  55
  56       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
  57         MethodDescriptor md = (MethodDescriptor) method_it.next();
  58         try {
  59           checkMethodBody(cd, md);
  60         } catch (Error e) {
  61           System.out.println("Error in " + md);
  62           throw e;
  63         }
  64       }
  65     }
  66   }
  67
  68   public void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
  69     ClassDescriptor superdesc = cd.getSuperDesc();
  70     if (superdesc != null) {
  71       Set possiblematches = superdesc.getMethodTable().getSet(md.getSymbol());
  72       for (Iterator methodit = possiblematches.iterator(); methodit.hasNext();) {
  73         MethodDescriptor matchmd = (MethodDescriptor) methodit.next();
  74         if (md.matches(matchmd)) {
  75           if (matchmd.getModifiers().isFinal()) {
  76             throw new Error("Try to override final method in method:" + md + " declared in  " + cd);
  77           }
  78         }
  79       }
  80     }
  81     BlockNode bn = state.getMethodBody(md);
  82     checkBlockNode(md, md.getParameterTable(), bn);
  83   }
  84
  85   public void checkBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
  86     /* Link in the naming environment */
  87     bn.getVarTable().setParent(nametable);
  88     for (int i = 0; i < bn.size(); i++) {
  89       BlockStatementNode bsn = bn.get(i);
  90       checkBlockStatementNode(md, bn.getVarTable(), bsn);
  91     }
  92   }
  93
  94   public void checkBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
  95       BlockStatementNode bsn) {
  96
  97     switch (bsn.kind()) {
  98     case Kind.BlockExpressionNode:
  99       checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
 100       return;
 101
 102     case Kind.DeclarationNode:
 103       checkDeclarationNode(md, (DeclarationNode) bsn);
 104       return;
 105     }
 106     /*
 107      * switch (bsn.kind()) { case Kind.BlockExpressionNode:
 108      * checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
 109      * return;
 110      *
 111      * case Kind.DeclarationNode: checkDeclarationNode(md, nametable,
 112      * (DeclarationNode) bsn); return;
 113      *
 114      * case Kind.TagDeclarationNode: checkTagDeclarationNode(md, nametable,
 115      * (TagDeclarationNode) bsn); return;
 116      *
 117      * case Kind.IfStatementNode: checkIfStatementNode(md, nametable,
 118      * (IfStatementNode) bsn); return;
 119      *
 120      * case Kind.SwitchStatementNode: checkSwitchStatementNode(md, nametable,
 121      * (SwitchStatementNode) bsn); return;
 122      *
 123      * case Kind.LoopNode: checkLoopNode(md, nametable, (LoopNode) bsn); return;
 124      *
 125      * case Kind.ReturnNode: checkReturnNode(md, nametable, (ReturnNode) bsn);
 126      * return;
 127      *
 128      * case Kind.TaskExitNode: checkTaskExitNode(md, nametable, (TaskExitNode)
 129      * bsn); return;
 130      *
 131      * case Kind.SubBlockNode: checkSubBlockNode(md, nametable, (SubBlockNode)
 132      * bsn); return;
 133      *
 134      * case Kind.AtomicNode: checkAtomicNode(md, nametable, (AtomicNode) bsn);
 135      * return;
 136      *
 137      * case Kind.SynchronizedNode: checkSynchronizedNode(md, nametable,
 138      * (SynchronizedNode) bsn); return;
 139      *
 140      * case Kind.ContinueBreakNode: checkContinueBreakNode(md, nametable,
 141      * (ContinueBreakNode) bsn); return;
 142      *
 143      * case Kind.SESENode: case Kind.GenReachNode: // do nothing, no semantic
 144      * check for SESEs return; }
 145      */
 146     // throw new Error();
 147   }
 148
 149   void checkBlockExpressionNode(MethodDescriptor md, SymbolTable nametable, BlockExpressionNode ben) {
 150     checkExpressionNode(md, nametable, ben.getExpression(), null);
 151   }
 152
 153   void checkExpressionNode(MethodDescriptor md, SymbolTable nametable, ExpressionNode en,
 154       TypeDescriptor td) {
 155
 156     switch (en.kind()) {
 157     case Kind.AssignmentNode:
 158       checkAssignmentNode(md, nametable, (AssignmentNode) en, td);
 159       return;
 160
 161     case Kind.OpNode:
 162       checkOpNode(md, nametable, (OpNode) en, td);
 163       return;
 164     }
 165     /*
 166      * switch(en.kind()) { case Kind.AssignmentNode:
 167      * checkAssignmentNode(md,nametable,(AssignmentNode)en,td); return;
 168      *
 169      * case Kind.CastNode: checkCastNode(md,nametable,(CastNode)en,td); return;
 170      *
 171      * case Kind.CreateObjectNode:
 172      * checkCreateObjectNode(md,nametable,(CreateObjectNode)en,td); return;
 173      *
 174      * case Kind.FieldAccessNode:
 175      * checkFieldAccessNode(md,nametable,(FieldAccessNode)en,td); return;
 176      *
 177      * case Kind.ArrayAccessNode:
 178      * checkArrayAccessNode(md,nametable,(ArrayAccessNode)en,td); return;
 179      *
 180      * case Kind.LiteralNode: checkLiteralNode(md,nametable,(LiteralNode)en,td);
 181      * return;
 182      *
 183      * case Kind.MethodInvokeNode:
 184      * checkMethodInvokeNode(md,nametable,(MethodInvokeNode)en,td); return;
 185      *
 186      * case Kind.NameNode: checkNameNode(md,nametable,(NameNode)en,td); return;
 187      *
 188      * case Kind.OpNode: checkOpNode(md,nametable,(OpNode)en,td); return;
 189      *
 190      * case Kind.OffsetNode: checkOffsetNode(md, nametable, (OffsetNode)en, td);
 191      * return;
 192      *
 193      * case Kind.TertiaryNode: checkTertiaryNode(md, nametable,
 194      * (TertiaryNode)en, td); return;
 195      *
 196      * case Kind.InstanceOfNode: checkInstanceOfNode(md, nametable,
 197      * (InstanceOfNode) en, td); return;
 198      *
 199      * case Kind.ArrayInitializerNode: checkArrayInitializerNode(md, nametable,
 200      * (ArrayInitializerNode) en, td); return;
 201      *
 202      * case Kind.ClassTypeNode: checkClassTypeNode(md, nametable,
 203      * (ClassTypeNode) en, td); return; }
 204      */
 205   }
 206
 207   void checkOpNode(MethodDescriptor md, SymbolTable nametable, OpNode on, TypeDescriptor td) {
 208
 209     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(md.getClassDesc());
 210
 211     checkExpressionNode(md, nametable, on.getLeft(), null);
 212     if (on.getRight() != null)
 213       checkExpressionNode(md, nametable, on.getRight(), null);
 214
 215     TypeDescriptor ltd = on.getLeft().getType();
 216     TypeDescriptor rtd = on.getRight() != null ? on.getRight().getType() : null;
 217
 218     if (ltd.getAnnotationMarkers().size() == 0) {
 219       // constant value
 220       // TODO
 221       // ltd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
 222     }
 223     if (rtd != null && rtd.getAnnotationMarkers().size() == 0) {
 224       // constant value
 225       // TODO
 226       // rtd.addAnnotationMarker(new AnnotationDescriptor(Lattice.TOP));
 227     }
 228
 229     System.out.println("checking op node");
 230     System.out.println("td=" + td);
 231     System.out.println("ltd=" + ltd);
 232     System.out.println("rtd=" + rtd);
 233
 234     Operation op = on.getOp();
 235
 236     switch (op.getOp()) {
 237
 238     case Operation.UNARYPLUS:
 239     case Operation.UNARYMINUS:
 240     case Operation.LOGIC_NOT:
 241       // single operand
 242       on.setType(new TypeDescriptor(TypeDescriptor.BOOLEAN));
 243       break;
 244
 245     case Operation.LOGIC_OR:
 246     case Operation.LOGIC_AND:
 247     case Operation.COMP:
 248     case Operation.BIT_OR:
 249     case Operation.BIT_XOR:
 250     case Operation.BIT_AND:
 251     case Operation.ISAVAILABLE:
 252     case Operation.EQUAL:
 253     case Operation.NOTEQUAL:
 254     case Operation.LT:
 255     case Operation.GT:
 256     case Operation.LTE:
 257     case Operation.GTE:
 258     case Operation.ADD:
 259     case Operation.SUB:
 260     case Operation.MULT:
 261     case Operation.DIV:
 262     case Operation.MOD:
 263     case Operation.LEFTSHIFT:
 264     case Operation.RIGHTSHIFT:
 265     case Operation.URIGHTSHIFT:
 266
 267       Set<String> operandSet = new HashSet<String>();
 268       String leftLoc = ltd.getAnnotationMarkers().get(0).getMarker();
 269       String rightLoc = rtd.getAnnotationMarkers().get(0).getMarker();
 270
 271       operandSet.add(leftLoc);
 272       operandSet.add(rightLoc);
 273
 274       // TODO
 275       // String glbLoc = locOrder.getGLB(operandSet);
 276       // on.getType().addAnnotationMarker(new AnnotationDescriptor(glbLoc));
 277       // System.out.println(glbLoc + "<-" + leftLoc + " " + rightLoc);
 278
 279       break;
 280
 281     default:
 282       throw new Error(op.toString());
 283     }
 284
 285     if (td != null) {
 286       String lhsLoc = td.getAnnotationMarkers().get(0).getMarker();
 287       if (locOrder.isGreaterThan(lhsLoc, on.getType().getAnnotationMarkers().get(0).getMarker())) {
 288         throw new Error("The location of LHS is higher than RHS: " + on.printNode(0));
 289       }
 290     }
 291
 292   }
 293
 294   void checkAssignmentNode(MethodDescriptor md, SymbolTable nametable, AssignmentNode an,
 295       TypeDescriptor td) {
 296
 297     boolean postinc = true;
 298     if (an.getOperation().getBaseOp() == null
 299         || (an.getOperation().getBaseOp().getOp() != Operation.POSTINC && an.getOperation()
 300             .getBaseOp().getOp() != Operation.POSTDEC))
 301       postinc = false;
 302     if (!postinc)
 303       checkExpressionNode(md, nametable, an.getSrc(), td);
 304
 305     ClassDescriptor cd = md.getClassDesc();
 306     Lattice<String> locOrder = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 307
 308     System.out.println("an=" + an.printNode(0));
 309     String destLocation = an.getDest().getType().getAnnotationMarkers().elementAt(0).getMarker();
 310     String srcLocation = an.getSrc().getType().getAnnotationMarkers().elementAt(0).getMarker();
 311
 312     if (!locOrder.isGreaterThan(srcLocation, destLocation)) {
 313       throw new Error("The value flow from " + srcLocation + " to " + destLocation
 314           + " does not respect location hierarchy.");
 315     }
 316
 317   }
 318
 319   void checkDeclarationNode(MethodDescriptor md, DeclarationNode dn) {
 320
 321     ClassDescriptor cd = md.getClassDesc();
 322     VarDescriptor vd = dn.getVarDescriptor();
 323     Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
 324
 325     // currently enforce every variable to have corresponding location
 326     if (annotationVec.size() == 0) {
 327       throw new Error("Location is not assigned to variable " + vd.getSymbol() + " in the method "
 328           + md.getSymbol() + " of the class " + cd.getSymbol());
 329     }
 330
 331     if (annotationVec.size() > 1) {
 332       // variable can have at most one location
 333       throw new Error(vd.getSymbol() + " has more than one location.");
 334     }
 335
 336     AnnotationDescriptor ad = annotationVec.elementAt(0);
 337
 338     if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
 339
 340       // check if location is defined
 341       String locationID = ad.getMarker();
 342       Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 343
 344
 345       if (lattice == null || (!lattice.containsKey(locationID))) {
 346         throw new Error("Location " + locationID
 347             + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
 348       }
 349
 350     } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 351       if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
 352
 353         if (ad.getData().length() == 0) {
 354           throw new Error("Delta function of " + vd.getSymbol() + " does not have any locations: "
 355               + cd.getSymbol() + ".");
 356         }
 357
 358         StringTokenizer token = new StringTokenizer(ad.getData(), ",");
 359         while (token.hasMoreTokens()) {
 360           String deltaOperand = token.nextToken();
 361
 362         }
 363
 364       }
 365     }
 366
 367   }
 368
 369   private void checkClass(ClassDescriptor cd) {
 370     // Check to see that fields are okay
 371     for (Iterator field_it = cd.getFields(); field_it.hasNext();) {
 372       FieldDescriptor fd = (FieldDescriptor) field_it.next();
 373       checkFieldDeclaration(cd, fd);
 374     }
 375
 376     // Check to see that methods respects ss property
 377     for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
 378       MethodDescriptor md = (MethodDescriptor) method_it.next();
 379       checkMethodDeclaration(cd, md);
 380     }
 381   }
 382
 383   private void checkMethodDeclaration(ClassDescriptor cd, MethodDescriptor md) {
 384
 385   }
 386
 387   private void checkFieldDeclaration(ClassDescriptor cd, FieldDescriptor fd) {
 388
 389     Vector<AnnotationDescriptor> annotationVec = fd.getType().getAnnotationMarkers();
 390
 391     // currently enforce every variable to have corresponding location
 392     if (annotationVec.size() == 0) {
 393       throw new Error("Location is not assigned to the field " + fd.getSymbol() + " of the class "
 394           + cd.getSymbol());
 395     }
 396
 397     if (annotationVec.size() > 1) {
 398       // variable can have at most one location
 399       throw new Error("Field " + fd.getSymbol() + " of class " + cd
 400           + " has more than one location.");
 401     }
 402
 403     // check if location is defined
 404     AnnotationDescriptor ad = annotationVec.elementAt(0);
 405     if (ad.getType() == AnnotationDescriptor.MARKER_ANNOTATION) {
 406       String locationID = annotationVec.elementAt(0).getMarker();
 407       Lattice<String> lattice = (Lattice<String>) state.getCd2LocationOrder().get(cd);
 408
 409
 410       if (lattice == null || (!lattice.containsKey(locationID))) {
 411         throw new Error("Location " + locationID
 412             + " is not defined in the location hierarchy of class " + cd.getSymbol() + ".");
 413       }
 414     } else if (ad.getType() == AnnotationDescriptor.SINGLE_ANNOTATION) {
 415       if (ad.getMarker().equals(SSJavaAnalysis.DELTA)) {
 416
 417         if (ad.getData().length() == 0) {
 418           throw new Error("Delta function of " + fd.getSymbol() + " does not have any locations: "
 419               + cd.getSymbol() + ".");
 420         }
 421
 422         StringTokenizer token = new StringTokenizer(ad.getData(), ",");
 423         while (token.hasMoreTokens()) {
 424           String deltaOperand = token.nextToken();
 425           // TODO: set delta operand to corresponding type descriptor
 426         }
 427       }
 428     }
 429
 430   }
 431 }