    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    }