Robust/src/Analysis/SSJava/LinearTypeCheck.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.Set;
   7 import java.util.Vector;
   8
   9 import IR.AnnotationDescriptor;
  10 import IR.ClassDescriptor;
  11 import IR.Descriptor;
  12 import IR.MethodDescriptor;
  13 import IR.State;
  14 import IR.SymbolTable;
  15 import IR.TaskDescriptor;
  16 import IR.TypeDescriptor;
  17 import IR.VarDescriptor;
  18 import IR.Tree.ArrayAccessNode;
  19 import IR.Tree.ArrayInitializerNode;
  20 import IR.Tree.AssignmentNode;
  21 import IR.Tree.AtomicNode;
  22 import IR.Tree.BlockExpressionNode;
  23 import IR.Tree.BlockNode;
  24 import IR.Tree.BlockStatementNode;
  25 import IR.Tree.CastNode;
  26 import IR.Tree.ClassTypeNode;
  27 import IR.Tree.ContinueBreakNode;
  28 import IR.Tree.CreateObjectNode;
  29 import IR.Tree.DeclarationNode;
  30 import IR.Tree.ExpressionNode;
  31 import IR.Tree.FieldAccessNode;
  32 import IR.Tree.IfStatementNode;
  33 import IR.Tree.InstanceOfNode;
  34 import IR.Tree.Kind;
  35 import IR.Tree.LiteralNode;
  36 import IR.Tree.LoopNode;
  37 import IR.Tree.MethodInvokeNode;
  38 import IR.Tree.NameNode;
  39 import IR.Tree.OffsetNode;
  40 import IR.Tree.OpNode;
  41 import IR.Tree.ReturnNode;
  42 import IR.Tree.SubBlockNode;
  43 import IR.Tree.SwitchBlockNode;
  44 import IR.Tree.SwitchLabelNode;
  45 import IR.Tree.SwitchStatementNode;
  46 import IR.Tree.SynchronizedNode;
  47 import IR.Tree.TagDeclarationNode;
  48 import IR.Tree.TaskExitNode;
  49 import IR.Tree.TertiaryNode;
  50
  51 public class LinearTypeCheck {
  52
  53   State state;
  54   SSJavaAnalysis ssjava;
  55   String needToNullify = null;
  56
  57   Hashtable<MethodDescriptor, Set<VarDescriptor>> md2DelegateParamSet;
  58
  59   public LinearTypeCheck(SSJavaAnalysis ssjava, State state) {
  60     this.ssjava = ssjava;
  61     this.state = state;
  62     md2DelegateParamSet = new Hashtable<MethodDescriptor, Set<VarDescriptor>>();
  63   }
  64
  65   public void linearTypeCheck() {
  66
  67     // first, parsing DELEGATE annotation from method declarations
  68     Iterator it = state.getClassSymbolTable().getDescriptorsIterator();
  69     while (it.hasNext()) {
  70       ClassDescriptor cd = (ClassDescriptor) it.next();
  71       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
  72         MethodDescriptor md = (MethodDescriptor) method_it.next();
  73         parseAnnotations(md);
  74       }
  75     }
  76     System.out.println("###");
  77     System.out.println("md2DelegateParamSet=" + md2DelegateParamSet);
  78
  79     // second, check the linear type
  80     it = state.getClassSymbolTable().getDescriptorsIterator();
  81     while (it.hasNext()) {
  82       ClassDescriptor cd = (ClassDescriptor) it.next();
  83       for (Iterator method_it = cd.getMethods(); method_it.hasNext();) {
  84         MethodDescriptor md = (MethodDescriptor) method_it.next();
  85         if (ssjava.needTobeAnnotated(md)) {
  86           checkMethodBody(cd, md);
  87         }
  88       }
  89     }
  90
  91   }
  92
  93   private void parseAnnotations(MethodDescriptor md) {
  94
  95     for (int i = 0; i < md.numParameters(); i++) {
  96       // process annotations on method parameters
  97       VarDescriptor vd = (VarDescriptor) md.getParameter(i);
  98
  99       Vector<AnnotationDescriptor> annotationVec = vd.getType().getAnnotationMarkers();
 100
 101       for (int anIdx = 0; anIdx < annotationVec.size(); anIdx++) {
 102         AnnotationDescriptor ad = annotationVec.elementAt(anIdx);
 103         if (ad.getMarker().equals(SSJavaAnalysis.DELEGATE)) {
 104
 105           Set<VarDescriptor> delegateSet = md2DelegateParamSet.get(md);
 106           if (delegateSet == null) {
 107             delegateSet = new HashSet<VarDescriptor>();
 108             md2DelegateParamSet.put(md, delegateSet);
 109           }
 110           delegateSet.add(vd);
 111         }
 112       }
 113
 114     }
 115
 116   }
 117
 118   private void checkMethodBody(ClassDescriptor cd, MethodDescriptor md) {
 119     BlockNode bn = state.getMethodBody(md);
 120     checkBlockNode(md, md.getParameterTable(), bn);
 121   }
 122
 123   private void checkBlockNode(MethodDescriptor md, SymbolTable nametable, BlockNode bn) {
 124     for (int i = 0; i < bn.size(); i++) {
 125       BlockStatementNode bsn = bn.get(i);
 126       checkBlockStatementNode(md, bn.getVarTable(), bsn);
 127     }
 128   }
 129
 130   private void checkBlockStatementNode(MethodDescriptor md, SymbolTable nametable,
 131       BlockStatementNode bsn) {
 132
 133     if (needToNullify != null) {
 134       if (!checkNullifying(bsn)) {
 135         throw new Error(
 136             "Reference field, which is read by a method, should be assigned to null before executing any following statement of the reference copy statement at "
 137                 + md.getClassDesc().getSourceFileName() + "::" + bsn.getNumLine());
 138       }
 139     }
 140
 141     switch (bsn.kind()) {
 142
 143     case Kind.BlockExpressionNode:
 144       checkBlockExpressionNode(md, nametable, (BlockExpressionNode) bsn);
 145       return;
 146
 147     case Kind.DeclarationNode:
 148       checkDeclarationNode(md, nametable, (DeclarationNode) bsn);
 149       return;
 150
 151     case Kind.IfStatementNode:
 152       checkIfStatementNode(md, nametable, (IfStatementNode) bsn);
 153       return;
 154
 155     case Kind.SwitchStatementNode:
 156       checkSwitchStatementNode(md, nametable, (SwitchStatementNode) bsn);
 157       return;
 158
 159     case Kind.LoopNode:
 160       checkLoopNode(md, nametable, (LoopNode) bsn);
 161       return;
 162
 163     case Kind.ReturnNode:
 164       checkReturnNode(md, nametable, (ReturnNode) bsn);
 165       return;
 166
 167     case Kind.SubBlockNode:
 168       checkSubBlockNode(md, nametable, (SubBlockNode) bsn);
 169       return;
 170
 171     case Kind.SynchronizedNode:
 172       checkSynchronizedNode(md, nametable, (SynchronizedNode) bsn);
 173       return;
 174     }
 175
 176     throw new Error();
 177   }
 178
 179   private void checkSynchronizedNode(MethodDescriptor md, SymbolTable nametable,
 180       SynchronizedNode sbn) {
 181     checkBlockNode(md, nametable, sbn.getBlockNode());
 182     // todo this could be Object
 183     checkExpressionNode(md, nametable, sbn.getExpr());
 184   }
 185
 186   private void checkReturnNode(MethodDescriptor md, SymbolTable nametable, ReturnNode rn) {
 187     if (rn.getReturnExpression() != null) {
 188       checkExpressionNode(md, nametable, rn.getReturnExpression());
 189     }
 190   }
 191
 192   private void checkSubBlockNode(MethodDescriptor md, SymbolTable nametable, SubBlockNode sbn) {
 193     checkBlockNode(md, nametable, sbn.getBlockNode());
 194   }
 195
 196   private void checkIfStatementNode(MethodDescriptor md, SymbolTable nametable, IfStatementNode isn) {
 197     checkExpressionNode(md, nametable, isn.getCondition());
 198     checkBlockNode(md, nametable, isn.getTrueBlock());
 199     if (isn.getFalseBlock() != null)
 200       checkBlockNode(md, nametable, isn.getFalseBlock());
 201   }
 202
 203   private void checkSwitchStatementNode(MethodDescriptor md, SymbolTable nametable,
 204       SwitchStatementNode ssn) {
 205
 206     checkExpressionNode(md, nametable, ssn.getCondition());
 207
 208     BlockNode sbn = ssn.getSwitchBody();
 209     for (int i = 0; i < sbn.size(); i++) {
 210       checkSwitchBlockNode(md, nametable, (SwitchBlockNode) sbn.get(i));
 211     }
 212   }
 213
 214   private void checkSwitchBlockNode(MethodDescriptor md, SymbolTable nametable, SwitchBlockNode sbn) {
 215     checkBlockNode(md, nametable, sbn.getSwitchBlockStatement());
 216   }
 217
 218   private void checkBlockExpressionNode(MethodDescriptor md, SymbolTable nametable,
 219       BlockExpressionNode ben) {
 220     checkExpressionNode(md, nametable, ben.getExpression());
 221   }
 222
 223   private void checkExpressionNode(MethodDescriptor md, SymbolTable nametable, ExpressionNode en) {
 224     switch (en.kind()) {
 225     case Kind.AssignmentNode:
 226       checkAssignmentNode(md, nametable, (AssignmentNode) en);
 227       return;
 228
 229     case Kind.CastNode:
 230       checkCastNode(md, nametable, (CastNode) en);
 231       return;
 232
 233     case Kind.CreateObjectNode:
 234       checkCreateObjectNode(md, nametable, (CreateObjectNode) en);
 235       return;
 236
 237     case Kind.FieldAccessNode:
 238       checkFieldAccessNode(md, nametable, (FieldAccessNode) en);
 239       return;
 240
 241     case Kind.ArrayAccessNode:
 242       checkArrayAccessNode(md, nametable, (ArrayAccessNode) en);
 243       return;
 244
 245       // case Kind.LiteralNode:
 246       // checkLiteralNode(md, nametable, (LiteralNode) en);
 247       // return;
 248
 249     case Kind.MethodInvokeNode:
 250       checkMethodInvokeNode(md, nametable, (MethodInvokeNode) en);
 251       return;
 252
 253     case Kind.NameNode:
 254       checkNameNode(md, nametable, (NameNode) en);
 255       return;
 256
 257     case Kind.OpNode:
 258       checkOpNode(md, nametable, (OpNode) en);
 259       return;
 260
 261     case Kind.OffsetNode:
 262       checkOffsetNode(md, nametable, (OffsetNode) en);
 263       return;
 264
 265     case Kind.TertiaryNode:
 266       checkTertiaryNode(md, nametable, (TertiaryNode) en);
 267       return;
 268
 269       // case Kind.InstanceOfNode:
 270       // checkInstanceOfNode(md, nametable, (InstanceOfNode) en);
 271       // return;
 272
 273       // case Kind.ArrayInitializerNode:
 274       // checkArrayInitializerNode(md, nametable, (ArrayInitializerNode) en);
 275       // return;
 276
 277       // case Kind.ClassTypeNode:
 278       // checkClassTypeNode(md, nametable, (ClassTypeNode) ens);
 279       // return;
 280     }
 281     throw new Error();
 282   }
 283
 284   private void checkTertiaryNode(MethodDescriptor md, SymbolTable nametable, TertiaryNode en) {
 285     // TODO Auto-generated method stub
 286
 287   }
 288
 289   private void checkOffsetNode(MethodDescriptor md, SymbolTable nametable, OffsetNode en) {
 290     // TODO Auto-generated method stub
 291
 292   }
 293
 294   private void checkOpNode(MethodDescriptor md, SymbolTable nametable, OpNode en) {
 295     // TODO Auto-generated method stub
 296
 297   }
 298
 299   private void checkNameNode(MethodDescriptor md, SymbolTable nametable, NameNode en) {
 300     // TODO Auto-generated method stub
 301
 302   }
 303
 304   private void checkMethodInvokeNode(MethodDescriptor md, SymbolTable nametable, MethodInvokeNode en) {
 305     // TODO Auto-generated method stub
 306
 307   }
 308
 309   private void checkArrayAccessNode(MethodDescriptor md, SymbolTable nametable, ArrayAccessNode en) {
 310     // TODO Auto-generated method stub
 311
 312   }
 313
 314   private void checkFieldAccessNode(MethodDescriptor md, SymbolTable nametable, FieldAccessNode fan) {
 315
 316   }
 317
 318   private void checkCreateObjectNode(MethodDescriptor md, SymbolTable nametable,
 319       CreateObjectNode con) {
 320     TypeDescriptor[] tdarray = new TypeDescriptor[con.numArgs()];
 321     for (int i = 0; i < con.numArgs(); i++) {
 322       ExpressionNode en = con.getArg(i);
 323       checkExpressionNode(md, nametable, en);
 324       tdarray[i] = en.getType();
 325     }
 326
 327     if ((con.getArrayInitializer() != null)) {
 328       checkArrayInitializerNode(md, nametable, con.getArrayInitializer());
 329     }
 330
 331   }
 332
 333   private void checkArrayInitializerNode(MethodDescriptor md, SymbolTable nametable,
 334       ArrayInitializerNode arrayInitializer) {
 335     // TODO Auto-generated method stub
 336
 337   }
 338
 339   private void checkCastNode(MethodDescriptor md, SymbolTable nametable, CastNode cn) {
 340     ExpressionNode en = cn.getExpression();
 341     checkExpressionNode(md, nametable, en);
 342   }
 343
 344   private boolean checkNullifying(BlockStatementNode bsn) {
 345
 346     if (bsn.kind() == Kind.BlockExpressionNode) {
 347       ExpressionNode en = ((BlockExpressionNode) bsn).getExpression();
 348       if (en.kind() == Kind.AssignmentNode) {
 349         AssignmentNode an = (AssignmentNode) en;
 350
 351         if (an.getSrc().getType().isNull() && an.getDest().printNode(0).equals(needToNullify)) {
 352           needToNullify = null;
 353           return true;
 354         }
 355       }
 356     }
 357
 358     return false;
 359   }
 360
 361   private void checkLoopNode(MethodDescriptor md, SymbolTable nametable, LoopNode ln) {
 362     if (ln.getType() == LoopNode.WHILELOOP || ln.getType() == LoopNode.DOWHILELOOP) {
 363       checkExpressionNode(md, nametable, ln.getCondition());
 364       checkBlockNode(md, nametable, ln.getBody());
 365     } else {
 366       // For loop case
 367       /* Link in the initializer naming environment */
 368       BlockNode bn = ln.getInitializer();
 369       for (int i = 0; i < bn.size(); i++) {
 370         BlockStatementNode bsn = bn.get(i);
 371         checkBlockStatementNode(md, bn.getVarTable(), bsn);
 372       }
 373       // check the condition
 374       checkExpressionNode(md, bn.getVarTable(), ln.getCondition());
 375       checkBlockNode(md, bn.getVarTable(), ln.getBody());
 376       checkBlockNode(md, bn.getVarTable(), ln.getUpdate());
 377     }
 378   }
 379
 380   private void checkAssignmentNode(Descriptor md, SymbolTable nametable, AssignmentNode an) {
 381     needToNullify(an.getSrc());
 382   }
 383
 384   private void checkDeclarationNode(Descriptor md, SymbolTable nametable, DeclarationNode dn) {
 385     needToNullify(dn.getExpression());
 386   }
 387
 388   private void needToNullify(ExpressionNode en) {
 389
 390     if (en != null && en.getType().isPtr() && !en.getType().isString()) {
 391       if (en.kind() != Kind.CreateObjectNode && en.kind() != Kind.LiteralNode) {
 392         if (en.kind() == Kind.CastNode) {
 393           needToNullify = ((CastNode) en).getExpression().printNode(0);
 394         } else {
 395           needToNullify = en.printNode(0);
 396         }
 397       }
 398     }
 399
 400   }
 401
 402 }