001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package javafe.tc; 004 005 006 import javafe.ast.*; 007 import javafe.util.Assert; 008 009 010 class CheckInvariants { 011 012 //@ requires sig != null; 013 public static void checkTypeDeclOfSig(TypeSig sig) { 014 if (sig.state < TypeSig.PARSED) return; 015 016 TypeDecl decl = sig.getTypeDecl(); 017 018 // Check super links 019 for(int i = 0; i < decl.superInterfaces.size(); i++) { 020 TypeName supern = decl.superInterfaces.elementAt(i); 021 TypeSig supers = TypeSig.getRawSig(supern); 022 if (sig.state >= TypeSig.LINKSRESOLVED) 023 Assert.notNull(supers); //@ nowarn Pre; 024 if (supers != null) { 025 Assert.notFalse(supers == sig.getEnclosingEnv() //@ nowarn Pre; 026 .lookupTypeName(null,supern.name)); 027 Assert.notFalse((sig.state < TypeSig.CHECKED //@ nowarn Pre; 028 && sig.state <= supers.state) 029 || supers.state >= TypeSig.PREPPED); 030 } 031 } 032 if (decl.getTag() == TagConstants.CLASSDECL) { 033 TypeName supern = ((ClassDecl)decl).superClass; 034 if (sig == Types.javaLangObject()) { 035 if (sig.state >= TypeSig.LINKSRESOLVED) 036 Assert.notFalse(supern == null); //@ nowarn Pre; 037 } else if (supern != null) { 038 TypeSig supers = TypeSig.getRawSig(supern); 039 if (sig.state >= TypeSig.LINKSRESOLVED) 040 Assert.notNull(supers); //@ nowarn Pre; 041 if (supers != null) { 042 Assert.notFalse(supers == //@ nowarn Pre; 043 sig.getEnclosingEnv().lookupTypeName(null,supern.name)); 044 Assert.notFalse((sig.state < TypeSig.CHECKED //@ nowarn Pre; 045 && sig.state <= supers.state) 046 || supers.state >= TypeSig.PREPPED); 047 } 048 } else 049 Assert.notFalse(sig.state < TypeSig.LINKSRESOLVED); //@ nowarn Pre; 050 } 051 052 for(int i = 0; i < decl.elems.size(); i++) { 053 TypeDeclElem e = decl.elems.elementAt(i); 054 055 switch (e.getTag()) { 056 057 case TagConstants.FIELDDECL: 058 { 059 FieldDecl f = (FieldDecl)e; 060 checkType(f.type, sig.state >= TypeSig.PREPPED); 061 if (f.init != null) checkExpr(sig, f.init); 062 break; 063 } 064 065 case TagConstants.METHODDECL: 066 case TagConstants.CONSTRUCTORDECL: 067 { 068 RoutineDecl r = (RoutineDecl) e; 069 for(int j = 0; j < r.args.size(); j++) 070 checkType(r.args.elementAt(j).type, sig.state >= TypeSig.PREPPED); 071 for(int j = 0; j < r.raises.size(); j++) 072 checkType(r.raises.elementAt(j), sig.state >= TypeSig.PREPPED); 073 if (r.getTag() == TagConstants.METHODDECL) 074 checkType(((MethodDecl)r).returnType, 075 sig.state >= TypeSig.PREPPED); 076 if (r.body != null) checkStmt(sig, r.body); 077 break; 078 } 079 080 case TagConstants.INITBLOCK: 081 checkStmt(sig, ((InitBlock)e).block); 082 break; 083 084 case TagConstants.CLASSDECL: 085 case TagConstants.INTERFACEDECL: 086 checkTypeDeclOfSig(TypeSig.getSig((TypeDecl)e)); 087 break; 088 089 default: Assert.fail("Fall through."); 090 } 091 } 092 } 093 094 095 //@ requires t != null; 096 public static void checkType(Type t, boolean resolved) { 097 if (t.getTag() != TagConstants.TYPENAME) 098 return; 099 TypeSig sig = TypeSig.getRawSig((TypeName) t); 100 if (resolved) 101 Assert.notNull(sig); //@ nowarn Pre; 102 else 103 Assert.notFalse(sig == null); //@ nowarn Pre; 104 } 105 106 107 //@ requires sig != null && s != null; 108 public static void checkStmt(TypeSig sig, Stmt s) { 109 110 // System.out.println("checkStmt: sig.state = "+sig.state); 111 112 switch(s.getTag()) { 113 114 case TagConstants.SWITCHSTMT: 115 checkExpr(sig, ((SwitchStmt)s).expr); 116 // Fall through 117 case TagConstants.BLOCKSTMT: 118 { 119 GenericBlockStmt block = (GenericBlockStmt)s; 120 for(int i = 0; i < block.stmts.size(); i++) 121 checkStmt(sig, block.stmts.elementAt(i)); 122 return; 123 } 124 125 case TagConstants.VARDECLSTMT: 126 { 127 LocalVarDecl d = ((VarDeclStmt)s).decl; 128 if (d.init != null) checkExpr(sig, d.init); 129 return; 130 } 131 132 case TagConstants.CLASSDECLSTMT: 133 { 134 ClassDeclStmt cds = (ClassDeclStmt)s; 135 checkTypeDeclOfSig(TypeSig.getSig(cds.decl)); 136 return; 137 } 138 139 case TagConstants.WHILESTMT: 140 { 141 WhileStmt w = (WhileStmt)s; 142 checkExpr(sig, w.expr); 143 checkStmt(sig, w.stmt); 144 return; 145 } 146 147 case TagConstants.DOSTMT: 148 { 149 DoStmt d = (DoStmt)s; 150 checkExpr(sig, d.expr); 151 checkStmt(sig, d.stmt); 152 return; 153 } 154 155 case TagConstants.SYNCHRONIZESTMT: 156 { 157 SynchronizeStmt ss = (SynchronizeStmt)s; 158 checkExpr(sig, ss.expr); 159 checkStmt(sig, ss.stmt); 160 return; 161 } 162 163 case TagConstants.EVALSTMT: 164 { 165 EvalStmt v = (EvalStmt) s; 166 checkExpr(sig, v.expr); 167 return; 168 } 169 170 171 case TagConstants.RETURNSTMT: 172 { 173 ReturnStmt r = (ReturnStmt)s; 174 if( r.expr != null ) checkExpr(sig, r.expr); 175 return; 176 } 177 178 case TagConstants.THROWSTMT: 179 { 180 ThrowStmt t = (ThrowStmt)s; 181 checkExpr(sig, t.expr); 182 return; 183 } 184 185 case TagConstants.BREAKSTMT: 186 case TagConstants.CONTINUESTMT: 187 return; 188 189 case TagConstants.LABELSTMT: 190 checkStmt(sig, ((LabelStmt)s).stmt); 191 return; 192 193 case TagConstants.IFSTMT: 194 { 195 IfStmt i = (IfStmt)s; 196 checkExpr(sig, i.expr); 197 checkStmt(sig, i.thn); 198 checkStmt(sig, i.els); 199 return; 200 } 201 202 case TagConstants.FORSTMT: 203 { 204 ForStmt f = (ForStmt) s; 205 for(int i = 0; i < f.forInit.size(); i++) 206 checkStmt(sig, f.forInit.elementAt(i)); 207 checkExpr(sig, f.test); 208 for(int i = 0; i < f.forUpdate.size(); i++) 209 checkExpr(sig, f.forUpdate.elementAt(i)); 210 checkStmt(sig, f.body); 211 return; 212 } 213 214 case TagConstants.SKIPSTMT: 215 return; 216 217 case TagConstants.ASSERTSTMT: 218 { 219 AssertStmt a = (AssertStmt)s; 220 checkExpr(sig,a.pred); 221 if (a.label != null) checkExpr(sig,a.label); 222 } 223 return; 224 225 case TagConstants.SWITCHLABEL: 226 { 227 SwitchLabel sl = (SwitchLabel) s; 228 if (sl.expr != null) checkExpr(sig, sl.expr); 229 return; 230 } 231 232 case TagConstants.TRYFINALLYSTMT: 233 { 234 TryFinallyStmt tf = (TryFinallyStmt)s; 235 checkStmt(sig, tf.tryClause); 236 checkStmt(sig, tf.finallyClause); 237 return; 238 } 239 240 case TagConstants.TRYCATCHSTMT: 241 { 242 TryCatchStmt tc = (TryCatchStmt)s; 243 checkStmt(sig, tc.tryClause); 244 for(int i = 0; i < tc.catchClauses.size(); i++) 245 checkStmt(sig, tc.catchClauses.elementAt(i).body); 246 return; 247 } 248 249 case TagConstants.CONSTRUCTORINVOCATION: 250 { 251 ConstructorInvocation ci = (ConstructorInvocation) s; 252 if (ci.enclosingInstance != null) 253 checkExpr(sig, ci.enclosingInstance); 254 for(int i = 0; i < ci.args.size(); i++) 255 checkExpr(sig, ci.args.elementAt(i)); 256 if (sig.state < TypeSig.CHECKED) 257 Assert.notFalse(ci.decl == null); //@ nowarn Pre; 258 else 259 Assert.notNull(ci.decl); //@ nowarn Pre; 260 return; 261 } 262 263 default: 264 Assert.fail("Switch fall through"); 265 } 266 } 267 268 269 //@ requires sig != null && expr != null; 270 public static void checkExpr(TypeSig sig, VarInit expr) { 271 272 // System.out.println("Checking inv on "+PrettyPrint.inst.toString(expr)); 273 274 if( sig.state >= TypeSig.CHECKED ) { 275 // All expressions should have types 276 if( expr instanceof Expr ) 277 FlowInsensitiveChecks.getType((Expr)expr); 278 } 279 280 switch (expr.getTag()) { 281 case TagConstants.ARRAYINIT: 282 { 283 ArrayInit ai = (ArrayInit)expr; 284 for(int i = 0; i < ai.elems.size(); i++) 285 checkExpr(sig, ai.elems.elementAt(i)); 286 return; 287 } 288 289 case TagConstants.THISEXPR: 290 case TagConstants.STRINGLIT: 291 case TagConstants.CHARLIT: 292 case TagConstants.BOOLEANLIT: 293 case TagConstants.FLOATLIT: case TagConstants.DOUBLELIT: 294 case TagConstants.INTLIT: case TagConstants.LONGLIT: 295 case TagConstants.NULLLIT: 296 return; 297 298 case TagConstants.ARRAYREFEXPR: 299 { 300 ArrayRefExpr r = (ArrayRefExpr) expr; 301 checkExpr(sig, r.array); 302 checkExpr(sig, r.index); 303 return; 304 } 305 306 case TagConstants.NEWINSTANCEEXPR: 307 { 308 NewInstanceExpr ne = (NewInstanceExpr) expr; 309 if (ne.enclosingInstance != null) 310 checkExpr(sig, ne.enclosingInstance); 311 checkType(ne.type, sig.state >= TypeSig.CHECKED); 312 for(int i = 0; i < ne.args.size(); i++) 313 checkExpr(sig, ne.args.elementAt(i)); 314 315 if (ne.anonDecl != null && sig.state>=TypeSig.CHECKED) 316 checkTypeDeclOfSig(TypeSig.getSig(ne.anonDecl)); 317 318 // if (sig.state < TypeSig.CHECKED) Assert.notFalse(ne.decl == null); 319 // else Assert.notNull(ne.decl); 320 321 return; 322 } 323 324 case TagConstants.NEWARRAYEXPR: 325 { 326 NewArrayExpr na = (NewArrayExpr) expr; 327 checkType(na.type, sig.state >= TypeSig.CHECKED); 328 for(int i = 0; i < na.dims.size(); i++) 329 checkExpr(sig, na.dims.elementAt(i)); 330 return; 331 } 332 333 case TagConstants.CONDEXPR: 334 { 335 CondExpr ce = (CondExpr) expr; 336 checkExpr(sig, ce.test); 337 checkExpr(sig, ce.thn); 338 checkExpr(sig, ce.els); 339 return; 340 } 341 342 case TagConstants.INSTANCEOFEXPR: 343 { 344 InstanceOfExpr ie = (InstanceOfExpr) expr; 345 checkExpr(sig, ie.expr); 346 checkType(ie.type, sig.state >= TypeSig.CHECKED); 347 return; 348 } 349 350 case TagConstants.CASTEXPR: 351 { 352 CastExpr ce = (CastExpr) expr; 353 checkExpr(sig, ce.expr); 354 checkType(ce.type, sig.state >= TypeSig.CHECKED); 355 return; 356 } 357 358 case TagConstants.CLASSLITERAL: 359 { 360 ClassLiteral cl = (ClassLiteral) expr; 361 checkType(cl.type, sig.state >= TypeSig.CHECKED); 362 return; 363 } 364 365 case TagConstants.OR: case TagConstants.AND: 366 case TagConstants.BITOR: case TagConstants.BITXOR: 367 case TagConstants.BITAND: case TagConstants.NE: 368 case TagConstants.EQ: case TagConstants.GE: 369 case TagConstants.GT: case TagConstants.LE: 370 case TagConstants.LT: case TagConstants.LSHIFT: 371 case TagConstants.RSHIFT: case TagConstants.URSHIFT: 372 case TagConstants.ADD: case TagConstants.SUB: 373 case TagConstants.DIV: case TagConstants.MOD: 374 case TagConstants.STAR: 375 case TagConstants.ASSIGN: case TagConstants.ASGMUL: 376 case TagConstants.ASGDIV: case TagConstants.ASGREM: 377 case TagConstants.ASGADD: case TagConstants.ASGSUB: 378 case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT: 379 case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND: 380 case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR: 381 { 382 BinaryExpr be = (BinaryExpr) expr; 383 checkExpr(sig, be.left); 384 checkExpr(sig, be.right); 385 return; 386 } 387 388 case TagConstants.UNARYSUB: case TagConstants.UNARYADD: 389 case TagConstants.NOT: case TagConstants.BITNOT: 390 case TagConstants.INC: case TagConstants.DEC: 391 case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC: 392 checkExpr(sig, ((UnaryExpr)expr).expr); 393 return; 394 395 case TagConstants.PARENEXPR: 396 checkExpr(sig, ((ParenExpr)expr).expr); 397 return; 398 399 case TagConstants.AMBIGUOUSVARIABLEACCESS: 400 Assert.notFalse(sig.state < TypeSig.CHECKED); //@ nowarn Pre; 401 return; 402 403 case TagConstants.VARIABLEACCESS: 404 Assert.notFalse(sig.state >= TypeSig.CHECKED); //@ nowarn Pre; 405 Assert.notNull(((VariableAccess)expr).decl); //@ nowarn Pre; 406 return; 407 408 case TagConstants.FIELDACCESS: 409 { 410 FieldAccess xp = (FieldAccess)expr; 411 checkObjectDesignator( sig, xp.od ); 412 Assert.notFalse( //@ nowarn Pre; 413 (sig.state < TypeSig.CHECKED && xp.decl == null) 414 || xp.decl != null); 415 return; 416 } 417 418 case TagConstants.AMBIGUOUSMETHODINVOCATION: 419 { 420 Assert.notFalse(sig.state < TypeSig.CHECKED); //@ nowarn Pre; 421 AmbiguousMethodInvocation ami = (AmbiguousMethodInvocation)expr; 422 for(int i = 0; i < ami.args.size(); i++) 423 checkExpr(sig, ami.args.elementAt(i)); 424 return; 425 } 426 427 case TagConstants.METHODINVOCATION: 428 { 429 MethodInvocation mi = (MethodInvocation)expr; 430 checkObjectDesignator( sig, mi.od ); 431 for(int i = 0; i < mi.args.size(); i++) 432 checkExpr(sig, mi.args.elementAt(i)); 433 Assert.notFalse((sig.state < TypeSig.CHECKED //@ nowarn Pre; 434 && mi.decl == null) 435 || mi.decl != null); 436 return; 437 } 438 439 default: Assert.fail("Unexpected tag "+expr.getTag()); 440 } 441 } 442 443 444 //@ requires sig != null && od != null; 445 public static void checkObjectDesignator(TypeSig sig, ObjectDesignator od) { 446 switch (od.getTag()) { 447 448 case TagConstants.EXPROBJECTDESIGNATOR: 449 { 450 ExprObjectDesignator eod = (ExprObjectDesignator)od; 451 checkExpr(sig, eod.expr); 452 break; 453 } 454 455 case TagConstants.TYPEOBJECTDESIGNATOR: 456 { 457 Assert.notFalse(sig.state >= TypeSig.CHECKED); //@ nowarn Pre; 458 TypeObjectDesignator tod = (TypeObjectDesignator)od; 459 checkType(tod.type, sig.state >= TypeSig.CHECKED); 460 Assert.notFalse(tod.type instanceof TypeName || 461 tod.type instanceof TypeSig); 462 break; 463 } 464 465 case TagConstants.SUPEROBJECTDESIGNATOR: 466 { 467 SuperObjectDesignator sod = (SuperObjectDesignator)od; 468 break; 469 } 470 471 default: Assert.fail("Unexpected tag "+od.getTag()); 472 } 473 } 474 475 476 477 }