0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: //
0009: //
0010:
0011: package de.uka.ilkd.key.rule.soundness;
0012:
0013: import java.util.Stack;
0014:
0015: import org.apache.log4j.Logger;
0016:
0017: import de.uka.ilkd.key.java.*;
0018: import de.uka.ilkd.key.java.abstraction.*;
0019: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
0020: import de.uka.ilkd.key.java.declaration.VariableDeclaration;
0021: import de.uka.ilkd.key.java.declaration.VariableSpecification;
0022: import de.uka.ilkd.key.java.expression.Assignment;
0023: import de.uka.ilkd.key.java.expression.ExpressionStatement;
0024: import de.uka.ilkd.key.java.expression.Literal;
0025: import de.uka.ilkd.key.java.expression.Operator;
0026: import de.uka.ilkd.key.java.expression.operator.*;
0027: import de.uka.ilkd.key.java.reference.*;
0028: import de.uka.ilkd.key.java.statement.*;
0029: import de.uka.ilkd.key.logic.ProgramElementName;
0030: import de.uka.ilkd.key.logic.op.*;
0031: import de.uka.ilkd.key.logic.sort.Sort;
0032: import de.uka.ilkd.key.rule.AbstractProgramElement;
0033: import de.uka.ilkd.key.util.Debug;
0034: import de.uka.ilkd.key.util.ExtList;
0035:
0036: /**
0037: * Perform static type checking on java blocks
0038: */
0039: public class StaticProgramChecker extends
0040: de.uka.ilkd.key.java.visitor.JavaASTVisitor {
0041:
0042: /**
0043: * The program is traversed in depth-left-first order. This stack
0044: * contains the types of all maximum subtrees of the AST that have
0045: * already been left
0046: */
0047: private final Stack typeStack = new Stack();
0048:
0049: /**
0050: * The result types of all method frames that enclose the current
0051: * position within the AST
0052: */
0053: private final Stack returnTypeStack = new Stack();
0054:
0055: /**
0056: * Symbolic constant that is inserted in <code>typeStack</code>
0057: * for unknown types. Unknown types are caused by untyped schema
0058: * variables
0059: */
0060: private final KeYJavaType UNKNOWN = new KeYJavaType(
0061: PrimitiveType.PROGRAM_SV);
0062:
0063: /**
0064: * Symbolic constant that is inserted for subtrees of the AST that
0065: * do not have a result (e.g. statements)
0066: */
0067: private final KeYJavaType VOID = new KeYJavaType();
0068:
0069: /**
0070: * Symbolic constant that is pushed on <code>typeStack</code>
0071: * whenever a subtree of the AST is entered. This level mark is
0072: * mostly used to make the traversal more robust against altered
0073: * arities of nodes, etc.
0074: */
0075: private final KeYJavaType LEVEL = new KeYJavaType();
0076:
0077: private final Services services;
0078:
0079: private final Logger logger = Logger
0080: .getLogger("key.taclet_soundness");
0081:
0082: public StaticProgramChecker(ProgramElement p_root,
0083: Services p_services) {
0084: super (p_root);
0085: services = p_services;
0086: }
0087:
0088: /**
0089: * Check an element of an array using the method
0090: * <code>checkNonVoidType</code>
0091: */
0092: private boolean checkNonVoidType(ArrayOfKeYJavaType p_array,
0093: int p_pos, boolean p_push) {
0094: return checkNonVoidType(p_array.getKeYJavaType(p_pos), p_push);
0095: }
0096:
0097: /**
0098: * Ensure that the given type <code>p_type</code> is a real Java
0099: * type, and that the type is in particular not unknown or void
0100: * @param p_type the type object to test
0101: * @param p_push if this parameter is true and the given type is
0102: * unknown, then the unknown-type constant is pushed as result on
0103: * the type stack
0104: * @return false if the given type is unknown, true if the type is
0105: * a legal (real) Java type
0106: * @throws StaticTypeException iff the given type is void
0107: */
0108: private boolean checkNonVoidType(KeYJavaType p_type, boolean p_push) {
0109: Debug.assertFalse(p_type == null, "Type is null");
0110: Debug.assertFalse(p_type == LEVEL,
0111: "The level mark was tested as a type");
0112:
0113: if (p_type == UNKNOWN) {
0114: if (p_push)
0115: pushUnknown();
0116: return false;
0117: }
0118: if (p_type == VOID)
0119: raiseTypeError();
0120: return true;
0121: }
0122:
0123: /**
0124: * Check all elements of an array using the method
0125: * <code>checkNonVoidType</code>.
0126: * @param p_push if this parameter is true and the array contains
0127: * the unknown-type constant, then the unknown-type constant is
0128: * pushed as result on the type stack (at most once)
0129: * @return false if the the array contains the unknown-type
0130: * constant, true if all elements of the array are legal (real)
0131: * Java types
0132: */
0133: private boolean checkNonVoidTypeArray(ArrayOfKeYJavaType p_array,
0134: boolean p_push) {
0135: int i = p_array.size();
0136: boolean ret = true;
0137: while (i-- != 0) {
0138: if (!checkNonVoidType(p_array, i, p_push))
0139: p_push = ret = false;
0140: }
0141: return ret;
0142: }
0143:
0144: /**
0145: * Ensure that the element of <code>p_array</code> at index
0146: * <code>p_pos</code> is a suitable type of a statement (i.e. void
0147: * or unknown), or that otherwise the particular child of the
0148: * program element <code>p_progEl</code> is an expression
0149: * statement
0150: */
0151: private void checkStatement(NonTerminalProgramElement p_progEl,
0152: ArrayOfKeYJavaType p_array, int p_pos) {
0153: if (!(p_array.getKeYJavaType(p_pos) == VOID
0154: || p_array.getKeYJavaType(p_pos) == UNKNOWN || p_progEl
0155: .getChildAt(p_pos) instanceof ExpressionStatement))
0156: raiseTypeError();
0157: }
0158:
0159: /** the action that is performed just before leaving the node the
0160: * last time
0161: */
0162: protected void doAction(ProgramElement node) {
0163: node.visit(this );
0164: }
0165:
0166: public void doAssignment() {
0167: // narrowing of constant expressions is not yet performed
0168: final ArrayOfKeYJavaType types = popAndCheckType(2, true);
0169: if (types != null) {
0170: if (getTypeConverter().isAssignableTo(
0171: types.getKeYJavaType(1), types.getKeYJavaType(0)))
0172: pushResult(types.getKeYJavaType(0));
0173: else
0174: raiseTypeError();
0175: }
0176: }
0177:
0178: /**
0179: * Call the binary type promotion method of the type converter
0180: * class on the two elements of the array <code>types</code>,
0181: * which has to have length <code>2</code>. The result in pushed
0182: * on the type stack
0183: */
0184: private void doBinaryPromotion(ArrayOfKeYJavaType p_types) {
0185: Debug.assertTrue(p_types.size() == 2,
0186: "doBinaryPromotion: Don't know what to do "
0187: + "with array of length " + p_types.size());
0188:
0189: doBinaryPromotion(p_types.getKeYJavaType(0), p_types
0190: .getKeYJavaType(1));
0191: }
0192:
0193: /**
0194: * Call the binary type promotion method of the type converter
0195: * class on the two given types. The result in pushed on the type
0196: * stack
0197: */
0198: private void doBinaryPromotion(KeYJavaType p_type0,
0199: KeYJavaType p_type1) {
0200: KeYJavaType promotedType = null;
0201: try {
0202: promotedType = getTypeConverter().getPromotedType(p_type0,
0203: p_type1);
0204: } catch (Exception e) {
0205: raiseTypeError();
0206: }
0207: pushResult(promotedType);
0208: }
0209:
0210: private void doBitwisePromotion(Operator x) {
0211: final ArrayOfKeYJavaType types = popAndCheckType(2, true);
0212: if (types != null) {
0213: if (!(getTypeConverter().isArithmeticType(
0214: types.getKeYJavaType(0))
0215: && getTypeConverter().isArithmeticType(
0216: types.getKeYJavaType(1)) || getTypeConverter()
0217: .isBooleanType(types.getKeYJavaType(0))
0218: && getTypeConverter().isBooleanType(
0219: types.getKeYJavaType(1))))
0220: raiseTypeError();
0221: doBinaryPromotion(types);
0222: }
0223: }
0224:
0225: /**
0226: * Cast the topmost element of the type stack to the given type
0227: * <code>p_targetType</code>, and push the type
0228: * <code>p_targetType</code> as a result on the stack
0229: */
0230: private void doCast(KeYJavaType p_targetType) {
0231: checkNonVoidType(p_targetType, false);
0232: final ArrayOfKeYJavaType types = popAndCheckType(1, false);
0233: if (types != null) {
0234: if (getTypeConverter().isCastingTo(types.getKeYJavaType(0),
0235: p_targetType))
0236: pushResult(p_targetType);
0237: else
0238: raiseTypeError();
0239: } else
0240: pushResult(p_targetType);
0241: }
0242:
0243: private void doComparison(ComparativeOperator x) {
0244: final ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0245: if (checkNonVoidType(types, 0, false)) {
0246: if (!getTypeConverter().isArithmeticType(
0247: types.getKeYJavaType(0)))
0248: raiseTypeError();
0249: }
0250: if (checkNonVoidType(types, 1, false)) {
0251: if (!getTypeConverter().isArithmeticType(
0252: types.getKeYJavaType(1)))
0253: raiseTypeError();
0254: }
0255: pushBoolean();
0256: }
0257:
0258: private void doCompoundAssignment(Assignment x) {
0259: popLevelMark();
0260: final ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0261: push(types.getKeYJavaType(1));
0262: doCast(types.getKeYJavaType(0));
0263: }
0264:
0265: private void doDecrementsIncrements(Assignment x) {
0266: final ArrayOfKeYJavaType types = popAndCheckType(1, true);
0267: if (types != null) {
0268: if (!getTypeConverter().isArithmeticType(
0269: types.getKeYJavaType(0)))
0270: raiseTypeError();
0271: pushResult(types.getKeYJavaType(0));
0272: }
0273: }
0274:
0275: protected void doDefaultAction(SourceElement x) {
0276: // Different kinds of literals and variable declarations are
0277: // treated directly
0278:
0279: if (x instanceof Literal)
0280: doLiteral((Literal) x);
0281: else if (x instanceof VariableDeclaration)
0282: doVariableDeclaration((VariableDeclaration) x);
0283: else
0284: // Catch all
0285: Debug.assertTrue(false, "Unknown source element: " + x
0286: + " " + x.getClass());
0287: }
0288:
0289: private void doEquals(ComparativeOperator x) {
0290: final ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0291: if (checkNonVoidType(types, 0, false)) {
0292: if (checkNonVoidType(types, 1, false)) {
0293: if (!(getTypeConverter().isArithmeticType(
0294: types.getKeYJavaType(0))
0295: && getTypeConverter().isArithmeticType(
0296: types.getKeYJavaType(1))
0297: || getTypeConverter().isBooleanType(
0298: types.getKeYJavaType(0))
0299: && getTypeConverter().isBooleanType(
0300: types.getKeYJavaType(1)) || (getTypeConverter()
0301: .isReferenceType(types.getKeYJavaType(0)) || getTypeConverter()
0302: .isNullType(types.getKeYJavaType(0)))
0303: && (getTypeConverter().isReferenceType(
0304: types.getKeYJavaType(1)) || getTypeConverter()
0305: .isNullType(types.getKeYJavaType(1)))))
0306: raiseTypeError();
0307: } else {
0308: if (!(getTypeConverter().isArithmeticType(
0309: types.getKeYJavaType(0))
0310: || getTypeConverter().isBooleanType(
0311: types.getKeYJavaType(0))
0312: || getTypeConverter().isReferenceType(
0313: types.getKeYJavaType(0)) || getTypeConverter()
0314: .isNullType(types.getKeYJavaType(0))))
0315: raiseTypeError();
0316: }
0317: } else if (checkNonVoidType(types, 1, false)) {
0318: if (!(getTypeConverter().isArithmeticType(
0319: types.getKeYJavaType(1))
0320: || getTypeConverter().isBooleanType(
0321: types.getKeYJavaType(1))
0322: || getTypeConverter().isReferenceType(
0323: types.getKeYJavaType(1)) || getTypeConverter()
0324: .isNullType(types.getKeYJavaType(1))))
0325: raiseTypeError();
0326: }
0327: pushBoolean();
0328: }
0329:
0330: /**
0331: * Check an <code>instanceof</code> expression
0332: */
0333: private void doInstanceof(TypeOperator x) {
0334: final ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0335: if (checkNonVoidType(types, 0, false)) {
0336: if (!(getTypeConverter().isReferenceType(
0337: types.getKeYJavaType(0)) || getTypeConverter()
0338: .isNullType(types.getKeYJavaType(0))))
0339: raiseTypeError();
0340: }
0341: if (checkNonVoidType(types, 1, false)) {
0342: if (!getTypeConverter().isReferenceType(
0343: types.getKeYJavaType(1)))
0344: raiseTypeError();
0345: }
0346: if (checkNonVoidType(types, 0, false)
0347: && checkNonVoidType(types, 1, false)) {
0348: if (!getTypeConverter().isCastingTo(
0349: types.getKeYJavaType(0), types.getKeYJavaType(1)))
0350: raiseTypeError();
0351: }
0352: pushBoolean();
0353: }
0354:
0355: private void doLiteral(Literal x) {
0356: pushResult(x.getKeYJavaType(getServices()));
0357: }
0358:
0359: private void doLogicalPromotion(Operator x) {
0360: final ArrayOfKeYJavaType types = popAndCheckType(2, true);
0361: if (types != null) {
0362: if (!getTypeConverter().isBooleanType(
0363: types.getKeYJavaType(0))
0364: || !getTypeConverter().isBooleanType(
0365: types.getKeYJavaType(1)))
0366: raiseTypeError();
0367: doBinaryPromotion(types);
0368: }
0369: }
0370:
0371: private void doNumericPromotion(Operator x) {
0372: final ArrayOfKeYJavaType types = popAndCheckType(2, true);
0373: if (types != null) {
0374: if (!getTypeConverter().isArithmeticType(
0375: types.getKeYJavaType(0))
0376: || !getTypeConverter().isArithmeticType(
0377: types.getKeYJavaType(1)))
0378: raiseTypeError();
0379: doBinaryPromotion(types);
0380: }
0381: }
0382:
0383: private void doPositiveNegative(Operator x) {
0384: final ArrayOfKeYJavaType types = popAndCheckType(1, true);
0385: if (types != null) {
0386: if (!getTypeConverter().isArithmeticType(
0387: types.getKeYJavaType(0)))
0388: raiseTypeError();
0389: doUnaryPromotion(types);
0390: }
0391: }
0392:
0393: protected void doSchemaVariable(SchemaVariable x) {
0394: pushUnknown(); //todo
0395: }
0396:
0397: private void doShiftPromotion(Operator x) {
0398: final ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0399: if (checkNonVoidType(types, 0, true)) {
0400: if (!getTypeConverter().isIntegralType(
0401: types.getKeYJavaType(0)))
0402: raiseTypeError();
0403: doUnaryPromotion(types);
0404: }
0405: if (checkNonVoidType(types, 1, false)) {
0406: if (!getTypeConverter().isIntegralType(
0407: types.getKeYJavaType(1)))
0408: raiseTypeError();
0409: }
0410: }
0411:
0412: // HACK
0413: private void doStandardStatement(NonTerminalProgramElement x) {
0414: pushVoid();
0415: }
0416:
0417: /**
0418: * Ensure that all subtrees of the AST below the current node are
0419: * represent statements compatible with the given program element
0420: * <code>x</code>
0421: */
0422: private void doStatements(NonTerminalProgramElement x) {
0423: final ArrayOfKeYJavaType types = popChildrenWithArityCheck(x);
0424: int i = types.size();
0425:
0426: while (i-- != 0)
0427: checkStatement(x, types, i);
0428: pushVoid();
0429: }
0430:
0431: /**
0432: * Call the unary type promotion method of the type converter
0433: * class on the element of the array <code>types</code>, which has
0434: * to have length <code>1</code>. The result in pushed on the type
0435: * stack
0436: */
0437: private void doUnaryPromotion(ArrayOfKeYJavaType p_types) {
0438: Debug.assertTrue(p_types.size() == 1,
0439: "doUnaryPromotion: Don't know what to do "
0440: + "with array of length " + p_types.size());
0441:
0442: final KeYJavaType type = p_types.getKeYJavaType(0);
0443: KeYJavaType promotedType = null;
0444: try {
0445: promotedType = getTypeConverter().getPromotedType(type);
0446: } catch (Exception e) {
0447: raiseTypeError();
0448: }
0449: pushResult(promotedType);
0450: }
0451:
0452: private void doVariableDeclaration(VariableDeclaration x) {
0453: doVariableDeclarationHelp(x);
0454: pushVoid();
0455: }
0456:
0457: /**
0458: * @return the type of an arbitrary variable specification of the
0459: * given variable declaration
0460: */
0461: private KeYJavaType doVariableDeclarationHelp(VariableDeclaration x) {
0462: final ArrayOfKeYJavaType types = popChildrenWithArityCheck(x);
0463: int i;
0464: KeYJavaType type = null;
0465:
0466: for (i = 0; i != types.size(); ++i) {
0467: if (x.getChildAt(i) instanceof VariableSpecification) {
0468: if (checkNonVoidType(types, i, false) && type != null) {
0469: if (!validSpecificationType(
0470: types.getKeYJavaType(i), type))
0471: raiseTypeError();
0472: }
0473: } else if (x.getChildAt(i) instanceof TypeReference) {
0474: if (checkNonVoidType(types, i, false))
0475: type = types.getKeYJavaType(i);
0476: }
0477: }
0478: return type;
0479: }
0480:
0481: protected JavaInfo getJavaInfo() {
0482: return getServices().getJavaInfo();
0483: }
0484:
0485: protected Services getServices() {
0486: return services;
0487: }
0488:
0489: public TypeConverter getTypeConverter() {
0490: return getServices().getTypeConverter();
0491: }
0492:
0493: public void performActionOnAbstractProgramElement(
0494: AbstractProgramElement x) {
0495: walk(x.getConcreteProgramElement(getServices()));
0496: // the result has to be inserted one level mark below
0497: propagateSingleResult();
0498: }
0499:
0500: public void performActionOnBinaryAnd(BinaryAnd x) {
0501: doBitwisePromotion(x);
0502: }
0503:
0504: public void performActionOnBinaryAndAssignment(BinaryAndAssignment x) {
0505: prepareCompoundAssignment(x);
0506: performActionOnBinaryAnd(null);
0507: doCompoundAssignment(x);
0508: }
0509:
0510: public void performActionOnBinaryNot(BinaryNot x) {
0511: ArrayOfKeYJavaType types = popAndCheckType(1, true);
0512: if (types != null) {
0513: if (!getTypeConverter().isArithmeticType(
0514: types.getKeYJavaType(0)))
0515: raiseTypeError();
0516: doUnaryPromotion(types);
0517: }
0518: }
0519:
0520: public void performActionOnBinaryOr(BinaryOr x) {
0521: doBitwisePromotion(x);
0522: }
0523:
0524: public void performActionOnBinaryOrAssignment(BinaryOrAssignment x) {
0525: prepareCompoundAssignment(x);
0526: performActionOnBinaryOr(null);
0527: doCompoundAssignment(x);
0528: }
0529:
0530: public void performActionOnBinaryXOr(BinaryXOr x) {
0531: doBitwisePromotion(x);
0532: }
0533:
0534: public void performActionOnBinaryXOrAssignment(BinaryXOrAssignment x) {
0535: prepareCompoundAssignment(x);
0536: performActionOnBinaryXOr(null);
0537: doCompoundAssignment(x);
0538: }
0539:
0540: public void performActionOnBreak(Break x) {
0541: doStatements(x);
0542: }
0543:
0544: public void performActionOnCatch(Catch x) {
0545: ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0546: if (checkNonVoidType(types, 0, false)) {
0547: KeYJavaType th = getJavaInfo().getTypeByClassName(
0548: "java.lang.Throwable");
0549: Sort thSort = th.getSort();
0550: Sort parSort = types.getKeYJavaType(0).getSort();
0551:
0552: if (!parSort.extendsTrans(thSort))
0553: raiseTypeError();
0554: }
0555: checkStatement(x, types, 1);
0556: pushVoid();
0557: }
0558:
0559: public void performActionOnConditional(Conditional x) {
0560: ArrayOfKeYJavaType types = popKeYJavaTypes(3);
0561: if (checkNonVoidType(types, 0, false)) {
0562: if (!getTypeConverter().isBooleanType(
0563: types.getKeYJavaType(0)))
0564: raiseTypeError();
0565: }
0566: if (checkNonVoidType(types, 1, true)
0567: && checkNonVoidType(types, 2, true)) {
0568: KeYJavaType a = types.getKeYJavaType(1);
0569: KeYJavaType b = types.getKeYJavaType(2);
0570: Type ajt = a.getJavaType();
0571: Type bjt = b.getJavaType();
0572: if (a == b) {
0573: pushResult(a);
0574: return;
0575: } else if (getTypeConverter().isArithmeticType(a)
0576: && getTypeConverter().isArithmeticType(b)) {
0577: if (ajt == PrimitiveType.JAVA_BYTE
0578: && bjt == PrimitiveType.JAVA_SHORT
0579: || bjt == PrimitiveType.JAVA_BYTE
0580: && ajt == PrimitiveType.JAVA_SHORT) {
0581: pushResult(PrimitiveType.JAVA_SHORT);
0582: return;
0583: } else {
0584: // constant expressions are not yet considered
0585: doBinaryPromotion(a, b);
0586: return;
0587: }
0588: } else if (getTypeConverter().isNullType(a)
0589: && getTypeConverter().isReferenceType(b)) {
0590: pushResult(b);
0591: return;
0592: } else if (getTypeConverter().isNullType(b)
0593: && getTypeConverter().isReferenceType(a)) {
0594: pushResult(a);
0595: return;
0596: } else if (getTypeConverter().isReferenceType(a)
0597: && getTypeConverter().isReferenceType(b)) {
0598: if (getTypeConverter().isAssignableTo(a, b)) {
0599: pushResult(b);
0600: return;
0601: } else if (getTypeConverter().isAssignableTo(b, a)) {
0602: pushResult(a);
0603: return;
0604: }
0605: }
0606:
0607: raiseTypeError();
0608: }
0609: }
0610:
0611: public void performActionOnContinue(Continue x) {
0612: doStatements(x);
0613: }
0614:
0615: public void performActionOnCopyAssignment(CopyAssignment x) {
0616: doAssignment();
0617: }
0618:
0619: public void performActionOnDivide(Divide x) {
0620: doNumericPromotion(x);
0621: }
0622:
0623: public void performActionOnDivideAssignment(DivideAssignment x) {
0624: prepareCompoundAssignment(x);
0625: performActionOnDivide(null);
0626: doCompoundAssignment(x);
0627: }
0628:
0629: public void performActionOnDo(Do x) {
0630: ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0631: if (checkNonVoidType(types, 1, false)) {
0632: if (!getTypeConverter().isBooleanType(
0633: types.getKeYJavaType(1)))
0634: raiseTypeError();
0635: }
0636: checkStatement(x, types, 0);
0637: pushVoid();
0638: }
0639:
0640: public void performActionOnElse(Else x) {
0641: doStatements(x);
0642: }
0643:
0644: public void performActionOnEmptyStatement(EmptyStatement x) {
0645: pushVoid();
0646: }
0647:
0648: public void performActionOnEquals(Equals x) {
0649: doEquals(x);
0650: }
0651:
0652: //////////////////////////////////////////////////////////////////
0653:
0654: public void performActionOnExactInstanceof(ExactInstanceof x) {
0655: doInstanceof(x);
0656: }
0657:
0658: public void performActionOnExecutionContext(ExecutionContext x) {
0659: popChildren();
0660: pushVoid();
0661: }
0662:
0663: public void performActionOnFieldReference(FieldReference x) {
0664: performActionOnVariableReference(x);
0665: }
0666:
0667: public void performActionOnFinally(Finally x) {
0668: doStatements(x);
0669: }
0670:
0671: public void performActionOnFor(For x) {
0672: ArrayOfKeYJavaType types = popKeYJavaTypes(4);
0673: checkStatement(x, types, 0);
0674: if (checkNonVoidType(types, 1, false)) {
0675: if (!getTypeConverter().isBooleanType(
0676: types.getKeYJavaType(1)))
0677: raiseTypeError();
0678: }
0679: checkStatement(x, types, 2);
0680: checkStatement(x, types, 3);
0681: pushVoid();
0682: }
0683:
0684: public void performActionOnForUpdates(ForUpdates x) {
0685: doStandardStatement(x);
0686: }
0687:
0688: public void performActionOnGreaterOrEquals(GreaterOrEquals x) {
0689: doComparison(x);
0690: }
0691:
0692: public void performActionOnGreaterThan(GreaterThan x) {
0693: doComparison(x);
0694: }
0695:
0696: public void performActionOnGuard(Guard x) {
0697: ArrayOfKeYJavaType types = popChildren();
0698: pushResult(types.getKeYJavaType(0));
0699: }
0700:
0701: public void performActionOnIf(If x) {
0702: ArrayOfKeYJavaType types = popChildrenWithArityCheck(x);
0703: if (checkNonVoidType(types, 0, false)) {
0704: if (!getTypeConverter().isBooleanType(
0705: types.getKeYJavaType(0)))
0706: raiseTypeError();
0707: }
0708: checkStatement(x, types, 1);
0709: if (x.getChildCount() == 3)
0710: checkStatement(x, types, 2);
0711: pushVoid();
0712: }
0713:
0714: public void performActionOnInstanceof(Instanceof x) {
0715: doInstanceof(x);
0716: }
0717:
0718: public void performActionOnLabeledStatement(LabeledStatement x) {
0719: doStatements(x);
0720: }
0721:
0722: public void performActionOnLessOrEquals(LessOrEquals x) {
0723: doComparison(x);
0724: }
0725:
0726: public void performActionOnLessThan(LessThan x) {
0727: doComparison(x);
0728: }
0729:
0730: public void performActionOnLocationVariable(LocationVariable x) {
0731: performActionOnProgramVariable(x);
0732: }
0733:
0734: public void performActionOnLogicalAnd(LogicalAnd x) {
0735: doLogicalPromotion(x);
0736: }
0737:
0738: public void performActionOnLogicalNot(LogicalNot x) {
0739: ArrayOfKeYJavaType types = popAndCheckType(1, true);
0740: if (types != null) {
0741: if (!getTypeConverter().isBooleanType(
0742: types.getKeYJavaType(0)))
0743: raiseTypeError();
0744: doUnaryPromotion(types);
0745: }
0746: }
0747:
0748: public void performActionOnLogicalOr(LogicalOr x) {
0749: doLogicalPromotion(x);
0750: }
0751:
0752: public void performActionOnLoopInit(LoopInit x) {
0753: doStandardStatement(x);
0754: }
0755:
0756: public void performActionOnMethodFrame(MethodFrame x) {
0757: performActionOnMethodFrame(x, false);
0758: }
0759:
0760: public void performActionOnMethodFrame(MethodFrame x,
0761: boolean p_enter) {
0762: if (p_enter) {
0763: IProgramVariable pv = x.getProgramVariable();
0764: if (pv == null)
0765: returnTypeStack.push(VOID);
0766: else {
0767: KeYJavaType t = pv.getKeYJavaType();
0768: if (t == null)
0769: t = UNKNOWN;
0770: returnTypeStack.push(t);
0771: }
0772: } else {
0773: returnTypeStack.pop();
0774: pushVoid();
0775: }
0776: }
0777:
0778: public void performActionOnMinus(Minus x) {
0779: doNumericPromotion(x);
0780: }
0781:
0782: public void performActionOnMinusAssignment(MinusAssignment x) {
0783: prepareCompoundAssignment(x);
0784: performActionOnMinus(null);
0785: doCompoundAssignment(x);
0786: }
0787:
0788: public void performActionOnModulo(Modulo x) {
0789: doNumericPromotion(x);
0790: }
0791:
0792: public void performActionOnModuloAssignment(ModuloAssignment x) {
0793: prepareCompoundAssignment(x);
0794: performActionOnModulo(null);
0795: doCompoundAssignment(x);
0796: }
0797:
0798: public void performActionOnNegative(Negative x) {
0799: doPositiveNegative(x);
0800: }
0801:
0802: public void performActionOnNotEquals(NotEquals x) {
0803: doEquals(x);
0804: }
0805:
0806: public void performActionOnPackageReference(PackageReference x) {
0807: pushVoid();
0808: }
0809:
0810: public void performActionOnParameterDeclaration(
0811: ParameterDeclaration x) {
0812: pushResult(doVariableDeclarationHelp(x));
0813: }
0814:
0815: public void performActionOnPlus(Plus x) {
0816: // strings are not considered yet
0817: doNumericPromotion(x);
0818: }
0819:
0820: public void performActionOnPlusAssignment(PlusAssignment x) {
0821: prepareCompoundAssignment(x);
0822: performActionOnPlus(null);
0823: doCompoundAssignment(x);
0824: }
0825:
0826: public void performActionOnPositive(Positive x) {
0827: doPositiveNegative(x);
0828: }
0829:
0830: public void performActionOnPostDecrement(PostDecrement x) {
0831: doDecrementsIncrements(x);
0832: }
0833:
0834: public void performActionOnPostIncrement(PostIncrement x) {
0835: doDecrementsIncrements(x);
0836: }
0837:
0838: public void performActionOnPreDecrement(PreDecrement x) {
0839: doDecrementsIncrements(x);
0840: }
0841:
0842: public void performActionOnPreIncrement(PreIncrement x) {
0843: doDecrementsIncrements(x);
0844: }
0845:
0846: public void performActionOnProgramConstant(ProgramConstant x) {
0847: performActionOnProgramConstant(x);
0848: }
0849:
0850: public void performActionOnProgramElementName(ProgramElementName x) {
0851: pushVoid();
0852: }
0853:
0854: public void performActionOnProgramSVProxy(ProgramSVProxy x) {
0855: if (x.getKeYJavaType() == null)
0856: pushVoid();
0857: else
0858: pushResult(x.getKeYJavaType());
0859: }
0860:
0861: public void performActionOnProgramSVSkolem(ProgramSVSkolem x) {
0862: if (x.getKeYJavaType() == null)
0863: pushVoid();
0864: else
0865: pushResult(x.getKeYJavaType());
0866: }
0867:
0868: public void performActionOnProgramVariable(ProgramVariable x) {
0869: pushResult(x.getKeYJavaType());
0870: }
0871:
0872: public void performActionOnReturn(Return x) {
0873: Debug.assertFalse(returnTypeStack.empty(),
0874: "Cannot determine correct return type");
0875:
0876: KeYJavaType frameType = (KeYJavaType) returnTypeStack.peek();
0877:
0878: if (x.getChildCount() == 0) {
0879: if (frameType != VOID)
0880: raiseTypeError();
0881: } else {
0882: if (frameType == VOID)
0883: raiseTypeError();
0884:
0885: ArrayOfKeYJavaType types = popAndCheckType(1, false);
0886: if (checkNonVoidType(frameType, false) && types != null) {
0887: // narrowing of constant expressions is not yet performed
0888: if (!getTypeConverter().isAssignableTo(
0889: types.getKeYJavaType(0), frameType))
0890: raiseTypeError();
0891: }
0892: }
0893: pushVoid();
0894: }
0895:
0896: public void performActionOnSchemaVariable(SchemaVariable x) {
0897: doSchemaVariable(x);
0898: }
0899:
0900: public void performActionOnShiftLeft(ShiftLeft x) {
0901: doShiftPromotion(x);
0902: }
0903:
0904: public void performActionOnShiftLeftAssignment(ShiftLeftAssignment x) {
0905: prepareCompoundAssignment(x);
0906: performActionOnShiftLeft(null);
0907: doCompoundAssignment(x);
0908: }
0909:
0910: public void performActionOnShiftRight(ShiftRight x) {
0911: doShiftPromotion(x);
0912: }
0913:
0914: public void performActionOnShiftRightAssignment(
0915: ShiftRightAssignment x) {
0916: prepareCompoundAssignment(x);
0917: performActionOnShiftRight(null);
0918: doCompoundAssignment(x);
0919: }
0920:
0921: public void performActionOnStatementBlock(StatementBlock x) {
0922: doStatements(x);
0923: }
0924:
0925: public void performActionOnSwitch(Switch x) {
0926: ArrayOfKeYJavaType types = popChildrenWithArityCheck(x);
0927: int i = types.size();
0928:
0929: if (checkNonVoidType(types, 0, false)) {
0930: Type t = types.getKeYJavaType(0).getJavaType();
0931: if (!(t == PrimitiveType.JAVA_CHAR
0932: || t == PrimitiveType.JAVA_BYTE
0933: || t == PrimitiveType.JAVA_SHORT || t == PrimitiveType.JAVA_INT))
0934: raiseTypeError();
0935: }
0936:
0937: while (i-- != 1)
0938: checkStatement(x, types, i);
0939:
0940: pushVoid();
0941: }
0942:
0943: public void performActionOnThen(Then x) {
0944: doStatements(x);
0945: }
0946:
0947: public void performActionOnThrow(Throw x) {
0948: // incomplete
0949: ArrayOfKeYJavaType types = popAndCheckType(1, false);
0950: if (types != null) {
0951: if (!(getTypeConverter().isReferenceType(
0952: types.getKeYJavaType(0)) && getTypeConverter()
0953: .isAssignableTo(
0954: types.getKeYJavaType(0),
0955: getJavaInfo().getTypeByClassName(
0956: "java.lang.Throwable"))))
0957: raiseTypeError();
0958: }
0959: pushVoid();
0960: }
0961:
0962: public void performActionOnTimes(Times x) {
0963: doNumericPromotion(x);
0964: }
0965:
0966: public void performActionOnTimesAssignment(TimesAssignment x) {
0967: prepareCompoundAssignment(x);
0968: performActionOnTimes(null);
0969: doCompoundAssignment(x);
0970: }
0971:
0972: public void performActionOnTry(Try x) {
0973: doStatements(x);
0974: }
0975:
0976: public void performActionOnTypeCast(TypeCast x) {
0977: ArrayOfKeYJavaType types = popKeYJavaTypes(2);
0978: push(types.getKeYJavaType(1));
0979: doCast(types.getKeYJavaType(0));
0980: }
0981:
0982: public void performActionOnTypeReference(TypeReference x) {
0983: pushResult(x.getKeYJavaType());
0984: }
0985:
0986: public void performActionOnUnsignedShiftRight(UnsignedShiftRight x) {
0987: doShiftPromotion(x);
0988: }
0989:
0990: public void performActionOnUnsignedShiftRightAssignment(
0991: UnsignedShiftRightAssignment x) {
0992: prepareCompoundAssignment(x);
0993: performActionOnUnsignedShiftRight(null);
0994: doCompoundAssignment(x);
0995: }
0996:
0997: public void performActionOnVariableReference(VariableReference x) {
0998: ArrayOfKeYJavaType types = popKeYJavaTypes(1);
0999: pushResult(types.getKeYJavaType(0));
1000: }
1001:
1002: public void performActionOnVariableSpecification(
1003: VariableSpecification x) {
1004: if (x.getChildCount() == 2)
1005: doAssignment();
1006: else
1007: propagateSingleResult();
1008: }
1009:
1010: public void performActionOnWhile(While x) {
1011: ArrayOfKeYJavaType types = popKeYJavaTypes(2);
1012: if (checkNonVoidType(types, 0, false)) {
1013: if (!getTypeConverter().isBooleanType(
1014: types.getKeYJavaType(0)))
1015: raiseTypeError();
1016: }
1017: checkStatement(x, types, 1);
1018: pushVoid();
1019: }
1020:
1021: private Object pop() {
1022: Debug.assertFalse(typeStack.empty(),
1023: "Stack should not be empty");
1024: return typeStack.pop();
1025: }
1026:
1027: /**
1028: * Pop the <code>p_num</code> topmost elements from the type stack
1029: * using the method <code>popKeYJavaTypes</code>, and check the
1030: * resulting array using the method
1031: * <code>checkNonVoidTypeArray</code>
1032: * @return the array with the types iff
1033: * <code>checkNonVoidTypeArray</code> returns true,
1034: * <code>null</code> otherwise
1035: */
1036: private ArrayOfKeYJavaType popAndCheckType(int p_num, boolean p_push) {
1037: final ArrayOfKeYJavaType t = popKeYJavaTypes(p_num);
1038: if (checkNonVoidTypeArray(t, p_push))
1039: return t;
1040: return null;
1041: }
1042:
1043: /**
1044: * Pop all elements from the stack that lie above the topmost
1045: * level mark
1046: * @return all elements from the stack that lie above the topmost
1047: * level mark as an array, with the first element of the array
1048: * being the lowest element removed from the stack
1049: */
1050: private ArrayOfKeYJavaType popChildren() {
1051: final ExtList res = new ExtList();
1052: Object o;
1053: while (true) {
1054: o = pop();
1055: if (o == LEVEL) {
1056: push(o);
1057: break;
1058: }
1059: res.addFirst(o);
1060: }
1061: return new ArrayOfKeYJavaType((KeYJavaType[]) res
1062: .collect(KeYJavaType.class));
1063: }
1064:
1065: private ArrayOfKeYJavaType popChildrenWithArityCheck(
1066: NonTerminalProgramElement x) {
1067: final ArrayOfKeYJavaType types = popChildren();
1068: Debug.assertTrue(types.size() == x.getChildCount(),
1069: "AST node arity mismatch: Number of subtrees "
1070: + "processed differs from arity of operator\n"
1071: + "AST subtree: " + x);
1072: return types;
1073: }
1074:
1075: /**
1076: * Pop the <code>p_num</code> topmost elements from the type
1077: * stack, which are assumed to be <code>KeYJavaType</code>s
1078: * @return The topmost elements of the type stack as an array,
1079: * with the first element of the array being the lowest element
1080: * removed from the stack
1081: */
1082: private ArrayOfKeYJavaType popKeYJavaTypes(int p_num) {
1083: final KeYJavaType[] res = new KeYJavaType[p_num];
1084: while (p_num-- != 0) {
1085: final Object stackEl = pop();
1086: Debug.assertTrue(stackEl instanceof KeYJavaType,
1087: "Found an element of wrong kind on type stack");
1088: res[p_num] = (KeYJavaType) stackEl;
1089: }
1090: return new ArrayOfKeYJavaType(res);
1091: }
1092:
1093: /**
1094: * Pop the topmost level mark from the type stack, together with
1095: * all elements above the mark
1096: */
1097: private void popLevelMark() {
1098: Object o;
1099: while (true) {
1100: o = pop();
1101: if (o == LEVEL)
1102: break;
1103: else
1104: logger.warn("Superfluous element on type stack: " + o);
1105: }
1106: }
1107:
1108: private void prepareCompoundAssignment(Assignment x) {
1109: // insert a virtual level mark for binary operator
1110: final ArrayOfKeYJavaType types = popKeYJavaTypes(2);
1111: push(types.getKeYJavaType(0));
1112: pushLevelMark();
1113: push(types.getKeYJavaType(0));
1114: push(types.getKeYJavaType(1));
1115: }
1116:
1117: private void printTypeStack() {
1118: logger.debug("StaticProgramChecker, current type stack:");
1119: logger.debug("[ ");
1120: if (typeStack.size() != 0) {
1121: int i = 0;
1122: while (true) {
1123: logger.debug(typeStack.get(i));
1124: if (++i == typeStack.size())
1125: break;
1126: logger.debug(", ");
1127: }
1128: }
1129: logger.debug(" ]");
1130: }
1131:
1132: /**
1133: * Pop the topmost element from the stack and push it as result
1134: */
1135: private void propagateSingleResult() {
1136: pushResult(pop());
1137: }
1138:
1139: private void push(Object p) {
1140: typeStack.push(p);
1141: }
1142:
1143: protected void pushBoolean() {
1144: pushResult(getTypeConverter().getKeYJavaType(
1145: PrimitiveType.JAVA_BOOLEAN));
1146: }
1147:
1148: private void pushLevelMark() {
1149: push(LEVEL);
1150: }
1151:
1152: /**
1153: * Push the type of a subtree of the AST on the type stack. The
1154: * type is inserted immediately below the topmost level mark,
1155: * i.e. after the next call of <code>popLevelMark</code> the
1156: * element <code>x</code> is the topmost element of the type stack
1157: */
1158: private void pushResult(Object x) {
1159: final Object o = pop();
1160:
1161: if (o == LEVEL)
1162: push(x);
1163: else
1164: pushResult(x);
1165:
1166: push(o);
1167: }
1168:
1169: protected void pushUnknown() {
1170: pushResult(UNKNOWN);
1171: }
1172:
1173: protected void pushVoid() {
1174: pushResult(VOID);
1175: }
1176:
1177: /**
1178: * @throws StaticTypeException to indicate that a type error has
1179: * been detected
1180: */
1181: private void raiseTypeError() {
1182: throw new StaticTypeException("Static type error");
1183: }
1184:
1185: /** starts the walker*/
1186: public void start() {
1187: walk(root());
1188: }
1189:
1190: private boolean validSpecificationType(KeYJavaType p_specType,
1191: KeYJavaType p_declType) {
1192: assert p_specType != null : "p_specType is null";
1193: assert p_declType != null : "p_declType is null";
1194:
1195: return p_specType == p_declType
1196: || p_specType.getJavaType() instanceof ArrayType
1197: && validSpecificationType(((ArrayType) p_specType
1198: .getJavaType()).getBaseType().getKeYJavaType(),
1199: p_declType);
1200: }
1201:
1202: /** walks through the AST. While keeping track of the current node
1203: * @param node the JavaProgramElement the walker is at
1204: */
1205: protected void walk(ProgramElement node) {
1206: // for each subtree a level mark is pushed on the type stack ...
1207: pushLevelMark();
1208:
1209: if (node instanceof MethodFrame)
1210: performActionOnMethodFrame((MethodFrame) node, true);
1211:
1212: if (node instanceof NonTerminalProgramElement) {
1213: NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
1214: for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
1215: walk(nonTerminalNode.getChildAt(i));
1216: }
1217: }
1218: // otherwise the node is left, so perform the action
1219: doAction(node);
1220:
1221: // ... and is removed which leaving the subtree
1222: popLevelMark();
1223: }
1224:
1225: }
|