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    }