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 }