00001: package clogs.staticanalysis;
00002:
00003: import clogs.ast.*;
00004: import clogs.util.List;
00005: import clogs.util.Optional;
00006:
00007:
00008: public class TypeCheck
00009: {
00010: public class TypeCheckException extends Exception
00011: {
00012: TypeCheckException (String s)
00013: {
00014: super (s);
00015: }
00016: }
00017:
00018:
00019: private final List<Decl> globalDecls;
00020: private final List<FunDef> fundefsOnly;
00021: private final List<FunDefSig> fundefsigs;
00022:
00023:
00024: public TypeCheck (List<ExtDecl> edecls, List<FunDefSig> fundefsigs)
00025: {
00026: List<Decl> declsTmp = List.nil ();
00027: List<FunDef> fundefsOnlyTmp = List.nil ();
00028: List<FunDefSig> fundefsigsTmp = fundefsigs;
00029: for (ExtDecl edecl : edecls) {
00030: if (edecl instanceof Decl) {
00031: Decl decl = (Decl) edecl;
00032: declsTmp = declsTmp.snoc (decl);
00033:
00034: } else if (edecl instanceof FunDef) {
00035: FunDef fundef = (FunDef) edecl;
00036: fundefsOnlyTmp = fundefsOnlyTmp.snoc (fundef);
00037: fundefsigsTmp = fundefsigsTmp.snoc (fundef);
00038:
00039: } else {
00040: throw new RuntimeException ("Missing ExtDecl case: " + edecl.getClass ().getName ());
00041: }
00042: }
00043:
00044: this.globalDecls = declsTmp;
00045: this.fundefsOnly = fundefsOnlyTmp;
00046: this.fundefsigs = fundefsigsTmp;
00047: }
00048:
00049:
00050: // In comments, let S and T range over types and G over contexts.
00051: // Contexts have the form:
00052: //
00053: // G ::= empty
00054: // | G,x:T (variable declaration)
00055: // | G,f:(S1,...,Sn)->T (function declaration)
00056: //
00057: // The judgments are written:
00058: //
00059: // |- extdecl1 ... extdecln : Program
00060: // G |- extdecl : Declaration
00061: // G |- stat : Statement<declaredReturnType>
00062: // G |- exp : T
00063: // |- exp is lvalue
00064: //
00065:
00066:
00067: // To check a bunch of global variable and function declarations, we
00068: // put them in the context, then start checking them; this allows
00069: // mutually recursive definitions.
00070: //
00071: // context(extdecl1 ... extdecln) |- extdecl1 : Declaration
00072: // ...
00073: // context(extdecl1 ... extdecln) |- extdecln : Declaration
00074: // ------------------------------------------------------------------
00075: // |- extdecl1 ... extdecln : Program
00076: //
00077: public List<ExtDecl> check ()
00078: throws TypeCheckException
00079: {
00080: Context context = Context.emptyContext;
00081:
00082: context = context.addGlobalVariables (globalDecls);
00083: context = context.addFunDefSigs (fundefsigs);
00084:
00085: List<Decl> declsNew = checkDecls (context, globalDecls);
00086: List<FunDef> fundefsOnlyNew = checkFunDefSigs (context);
00087:
00088: List<ExtDecl> result = List.nil ();
00089: for (Decl decl : declsNew) {
00090: result = result.snoc (decl);
00091: }
00092: for (FunDef fundef : fundefsOnlyNew) {
00093: result = result.snoc (fundef);
00094: }
00095:
00096: return result;
00097: }
00098:
00099:
00100: // To check a variable declaration, we just need to make sure that
00101: // the initializer has the correct type:
00102: //
00103: // ------------------------------
00104: // G |- (T x;) : Declaration
00105: //
00106: // G |- exp : T
00107: // -------------------------------
00108: // G |- (T x = exp;) : Declaration
00109: //
00110: List<Decl> checkDecls (Context context, List<Decl> decls)
00111: throws TypeCheckException
00112: {
00113: List<Decl> result = List.nil ();
00114: for (Decl decl : decls) {
00115: if (decl.eo.isEmpty ()) {
00116: result = result.snoc (decl);
00117: } else {
00118: Exp exp = checkExp (context, decl.eo.get ());
00119: if (!matchesDeclaredType (decl.type, exp)) {
00120: throw new TypeCheckException ("Declared type " + decl.type + " does not match computed type for " + exp);
00121: }
00122: result = result.snoc (new Decl (decl.type, decl.name, new Optional<Exp> (exp)));
00123: }
00124: }
00125: return result;
00126: }
00127:
00128:
00129: // To check a function declaration, we check the body:
00130: //
00131: // G,x1:S1,...,xn:Sn |- compoundStat : T
00132: // -------------------------------------------------------
00133: // G |- (T f (S1 x1,...,Sn xn) compoundStat) : Declaration
00134: //
00135: List<FunDef> checkFunDefSigs (Context context)
00136: throws TypeCheckException
00137: {
00138: List<FunDef> fundefsOnlyNew = List.nil ();
00139: for (FunDef fundef : fundefsOnly) {
00140: StatCompound bodyNew = checkStatCompound (context.addFunParams (fundef), fundef.type, fundef.body);
00141: FunDef fundefNew = new FunDef (fundef.type, fundef.name, fundef.params, bodyNew);
00142: fundefsOnlyNew = fundefsOnlyNew.snoc (fundefNew);
00143: }
00144: return fundefsOnlyNew;
00145: }
00146:
00147:
00148: // To check a compound statement, check each statement and initializer
00149: // G,x1:T1,...,xn:Tn |- (T1 x1 = exp1;) : Declaration
00150: // ...
00151: // G,x1:T1,...,xn:Tn |- (Tn xn = expn;) : Declaration
00152: // G,x1:T1,...,xn:Tn |- stat1 : Statement<T>
00153: // ...
00154: // G,x1:T1,...,xn:Tn |- statm : Statement<T>
00155: // -----------------------------------------------------------------------
00156: // G |- { T1 x1 = exp1; ... Tn xn = expn; stat1 ... statm } : Statement<T>
00157: //
00158: StatCompound checkStatCompound (Context context, Type declaredReturnType, StatCompound statC)
00159: throws TypeCheckException
00160: {
00161: context = context.addLocalVariables (statC.decls);
00162: List<Decl> declsNew = checkDecls (context, statC.decls);
00163: List<Stat> statsNew = List.nil ();
00164: for (Stat stat : statC.stats) {
00165: Stat statNew = checkStat (context, declaredReturnType, stat);
00166: statsNew = statsNew.snoc (statNew);
00167: }
00168: return new StatCompound (declsNew, statsNew);
00169: }
00170:
00171:
00172: // To check a statment, do a case analysis.
00173: Stat checkStat (Context context, Type declaredReturnType, Stat stat)
00174: throws TypeCheckException
00175: {
00176: if (stat instanceof StatCompound) {
00177: // G,decls |- stats : Statement<T>
00178: // ------------------------------------
00179: // G |- { decls stats } : Statement<T>
00180: //
00181: StatCompound statC = (StatCompound) stat;
00182: return checkStatCompound (context, declaredReturnType, statC).addLabels (stat.labels);
00183:
00184: } else if (stat instanceof StatExp) {
00185: // G |- exp : S (for some type S)
00186: // ---------------------------------------
00187: // G |- (exp;) : Statement<T>
00188: //
00189: StatExp statE = (StatExp) stat;
00190: return new StatExp (checkExp (context, statE.exp)).addLabels (stat.labels);
00191:
00192: } else if (stat instanceof StatGoto) {
00193: // -----------------------------------
00194: // G |- (goto l;) : Statement<T>
00195: //
00196: return stat;
00197:
00198: } else if (stat instanceof StatIf) {
00199: // G |- exp : int
00200: // G |- statT : Statement<T>
00201: // G |- statF : Statement<T>
00202: // -----------------------------------------------------
00203: // G |- (if (exp) statT else statF) : Statement<T>
00204: //
00205: StatIf statI = (StatIf) stat;
00206: Exp expNew = checkExp (context, statI.exp);
00207: if (!matchesDeclaredType (new TypeInt (), expNew)) {
00208: throw new TypeCheckException ("Expression in conditional has non-integer type " + expNew);
00209: }
00210: return new StatIf (expNew, checkStat (context, declaredReturnType, statI.statT), checkStat (context, declaredReturnType, statI.statF)).addLabels (stat.labels);
00211:
00212: } else if (stat instanceof StatReturn) {
00213: // ---------------------------------------
00214: // G |- (return;) : Statement<void>
00215: //
00216: // G |- exp : T
00217: // ---------------------------------------
00218: // G |- (return exp;) : Statement<T>
00219: //
00220: StatReturn statR = (StatReturn) stat;
00221: if (statR.oe.isEmpty ()) {
00222: if (!testTypeEquality (declaredReturnType, new TypeVoid ())) {
00223: throw new TypeCheckException ("Empty return for function with non-void type");
00224: }
00225: return statR;
00226: } else {
00227: Exp expNew = checkExp (context, statR.oe.get ());
00228: if (!matchesDeclaredType (declaredReturnType, expNew)) {
00229: throw new TypeCheckException ("Declared return type " + declaredReturnType + " does not match computed type for " + expNew);
00230: }
00231: return new StatReturn (new Optional<Exp> (expNew)).addLabels (stat.labels);
00232: }
00233:
00234: } else if (stat instanceof StatSkip) {
00235: // ---------------------------------
00236: // G |- (skip;) : Statement<T>
00237: return stat;
00238:
00239: } else if (stat instanceof StatWhile) {
00240: // G |- exp : int
00241: // G |- statW : Statement<T>
00242: // -----------------------------------------------------
00243: // G |- (while (exp) statW) : Statement<T>
00244: //
00245: StatWhile statW = (StatWhile) stat;
00246: Exp expNew = checkExp (context, statW.exp);
00247: if (!matchesDeclaredType (new TypeInt (), expNew)) {
00248: throw new TypeCheckException ("Expression in while has non-integer type " + expNew);
00249: }
00250: return new StatWhile (expNew, checkStat (context, declaredReturnType, statW.stat)).addLabels (stat.labels);
00251:
00252: } else {
00253: throw new RuntimeException ("Missing Stat case: " + stat.getClass ().getName ());
00254: }
00255: }
00256:
00257:
00258: // To check an expression, do a case analysis.
00259: Exp checkExp (Context context, Exp exp)
00260: throws TypeCheckException
00261: {
00262: Exp result;
00263:
00264: if (exp instanceof ExpArrayAccess) {
00265: // G |- array : T[]
00266: // G |- index : int
00267: // -----------------------------
00268: // G |- (array[index]) : T
00269: //
00270: ExpArrayAccess expA = (ExpArrayAccess) exp;
00271: Exp exp1 = checkExp (context, expA.array);
00272: Exp exp2 = checkExp (context, expA.index);
00273: assert (!exp1.to.isEmpty ());
00274: Type type1 = exp1.to.get ();
00275: if (!(type1 instanceof TypeArray)) {
00276: throw new TypeCheckException ("Array expression has non-array type " + exp1);
00277: }
00278: Type typeResult = ((TypeArray) type1).type;
00279: if (!matchesDeclaredType (new TypeInt (), exp2)) {
00280: throw new TypeCheckException ("Array index expression has non-integer type " + exp2);
00281: }
00282: result = new ExpArrayAccess (exp1, exp2).setType (typeResult);
00283:
00284: } else if (exp instanceof ExpAssign) {
00285: // G |- left : T
00286: // G |- right : T
00287: // |- left is lval
00288: // ------------------------------
00289: // G |- (left = right) : T
00290: //
00291: ExpAssign expA = (ExpAssign) exp;
00292: Exp exp1 = checkExp (context, expA.left);
00293: Exp exp2 = checkExp (context, expA.right);
00294: assert (!exp1.to.isEmpty ());
00295: assert (!exp2.to.isEmpty ());
00296: if (!testTypeEquality (exp1.to.get (), exp2.to.get ())) {
00297: throw new TypeCheckException ("Unequal types in assignment from " + exp2 + " to " + exp1);
00298: }
00299: if (!isLValue (exp1)) {
00300: throw new TypeCheckException ("Assignment to non-lvalue " + exp1);
00301: }
00302: result = new ExpAssign (exp1, exp2).setType (exp2.to.get ());
00303:
00304: } else if (exp instanceof ExpBinOp) {
00305: // G |- left : int
00306: // G |- right : int
00307: // -----------------------------------
00308: // G |- (left binop right) : int
00309: //
00310: ExpBinOp expB = (ExpBinOp) exp;
00311: Exp exp1 = checkExp (context, expB.left);
00312: Exp exp2 = checkExp (context, expB.right);
00313: // At present, all binary operators have type "int * int ->
00314: // int", so we do not need to perform a case analysis on the
00315: // operator.
00316: if (!matchesDeclaredType (new TypeInt (), exp1)) {
00317: throw new TypeCheckException ("Argument to " + expB.op + " has non-integer type " + exp1);
00318: }
00319: if (!matchesDeclaredType (new TypeInt (), exp2)) {
00320: throw new TypeCheckException ("Argument to " + expB.op + " has non-integer type " + exp2);
00321: }
00322: result = new ExpBinOp (expB.op, exp1, exp2).setType (new TypeInt ());
00323:
00324: } else if (exp instanceof ExpComma) {
00325: // G |- left : S
00326: // G |- right : T
00327: // -----------------------------
00328: // G |- (left , right) : T
00329: //
00330: ExpComma expC = (ExpComma) exp;
00331: Exp exp1 = checkExp (context, expC.left);
00332: Exp exp2 = checkExp (context, expC.right);
00333: assert (!exp2.to.isEmpty ());
00334: result = new ExpComma (exp1, exp2).setType (exp2.to.get ());
00335:
00336: } else if (exp instanceof ExpFunCall) {
00337: // G(name) = (S1,...,Sn)->T
00338: // G |- arg1 : S1
00339: // ...
00340: // G |- argn : Sn
00341: // ------------------------------------
00342: // G |- (name(arg1,...,argn)) : T
00343: //
00344: ExpFunCall expF = (ExpFunCall) exp;
00345: if (!context.containsFunDefSig (expF.name)) {
00346: throw new TypeCheckException ("Function " + expF.name + " not found in context " + context);
00347: }
00348: FunDefSig fundefsig = context.getFunDefSig (expF.name);
00349: if (fundefsig.params.size () != expF.args.size ()) {
00350: throw new TypeCheckException ("Function " + expF.name + " requires " + fundefsig.params.size () + " arguments, " +
00351: "but " + expF.args.size () + " arguments were given in " + expF);
00352: }
00353: List<Decl> decls = fundefsig.params;
00354: List<Exp> argsNew = List.nil ();
00355: for (Exp arg : expF.args) {
00356: Exp argNew = checkExp (context, arg);
00357: if (!matchesDeclaredType (decls.head ().type, argNew)) {
00358: throw new TypeCheckException ("Function " + expF.name + " parameter type " + decls.head () + " does not match computed type for " + arg);
00359: }
00360: argsNew = argsNew.snoc (argNew);
00361: decls = decls.tail ();
00362: }
00363: result = new ExpFunCall (expF.name, argsNew).setType (fundefsig.type);
00364:
00365: } else if (exp instanceof ExpInt) {
00366: // ------------
00367: // G |- n : int
00368: //
00369: ExpInt expI = (ExpInt) exp;
00370: result = expI.setType (new TypeInt ());
00371:
00372: } else if (exp instanceof ExpNew) {
00373: // G |- size : int
00374: // --------------------------------------------
00375: // G |- (new contentType[size]) : contentType[]
00376: //
00377: ExpNew expN = (ExpNew) exp;
00378: Exp exp1 = checkExp (context, expN.size);
00379: if (!matchesDeclaredType (new TypeInt (), exp1)) {
00380: throw new TypeCheckException ("Argument to new " + expN + " has non-integer type " + exp1);
00381: }
00382: result = new ExpNew (expN.contentType, exp1).setType (new TypeArray (expN.contentType));
00383:
00384: } else if (exp instanceof ExpString) {
00385: // --------------------
00386: // G |- "value" : int[]
00387: //
00388: ExpString expS = (ExpString) exp;
00389: result = expS.setType (new TypeArray (new TypeInt ()));
00390:
00391: } else if (exp instanceof ExpUnOp) {
00392: // G |- exp : int
00393: // ---------------------
00394: // G |- (unop exp) : int
00395: //
00396: ExpUnOp expU = (ExpUnOp) exp;
00397: Exp exp1 = checkExp (context, expU.exp);
00398: // At present, all unary operators have type "int -> int", so we
00399: // do not need to perform a case analysis on the operator.
00400: if (!matchesDeclaredType (new TypeInt (), exp1)) {
00401: throw new TypeCheckException ("Argument to " + expU.op + " has non-integer type " + exp1);
00402: }
00403: result = new ExpUnOp (expU.op, exp1).setType (new TypeInt ());
00404:
00405: } else if (exp instanceof ExpVar) {
00406: // G(x) = T
00407: // ----------
00408: // G |- x : T
00409: //
00410: ExpVar expV = (ExpVar) exp;
00411: if (!context.containsVariable (expV.name)) {
00412: throw new TypeCheckException ("Variable " + expV.name + " not found in context " + context);
00413: }
00414: result = expV.setType (context.getVariableType (expV.name));
00415:
00416: } else {
00417: throw new RuntimeException ("Missing Exp case: " + exp.getClass ().getName ());
00418: }
00419:
00420: if (!exp.to.isEmpty () && !matchesDeclaredType (exp.to.get (), result)) {
00421: throw new TypeCheckException ("Declared type for expression " + exp + " does not match computed type for expression " + result);
00422: }
00423:
00424: return result;
00425: }
00426:
00427:
00428: boolean matchesDeclaredType (Type declared, Exp exp)
00429: {
00430: assert (!exp.to.isEmpty ());
00431: Type computed = exp.to.get ();
00432: return testTypeEquality (declared, computed);
00433: }
00434:
00435:
00436: boolean testTypeEquality (Type t1, Type t2)
00437: {
00438: if ((t1 instanceof TypeVoid) && (t2 instanceof TypeVoid)) {
00439: return true;
00440: } else if ((t1 instanceof TypeInt) && (t2 instanceof TypeInt)) {
00441: return true;
00442: } else if ((t1 instanceof TypeArray) && (t2 instanceof TypeArray)) {
00443: TypeArray t1A = (TypeArray) t1;
00444: TypeArray t2A = (TypeArray) t2;
00445: return testTypeEquality (t1A.type, t2A.type);
00446: } else {
00447: return false;
00448: }
00449: }
00450:
00451:
00452: // Every variable and array access is an lvalue.
00453: // Nothing else is an lvalue.
00454: boolean isLValue (Exp exp)
00455: {
00456: if (exp instanceof ExpArrayAccess) {
00457: // -------------------------
00458: // |- (array[index]) is lvalue
00459: //
00460: return true;
00461: } else if (exp instanceof ExpVar) {
00462: // --------------
00463: // |- x is lvalue
00464: //
00465: return true;
00466: } else {
00467: return false;
00468: }
00469: }
00470: }
00471:
|
