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.encapsulation;
0012:
0013: import java.util.HashMap;
0014: import java.util.Iterator;
0015: import java.util.Map;
0016: import java.util.Stack;
0017:
0018: import de.uka.ilkd.key.java.*;
0019: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
0020: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0021: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
0022: import de.uka.ilkd.key.java.declaration.*;
0023: import de.uka.ilkd.key.java.expression.ArrayInitializer;
0024: import de.uka.ilkd.key.java.expression.ParenthesizedExpression;
0025: import de.uka.ilkd.key.java.expression.PassiveExpression;
0026: import de.uka.ilkd.key.java.expression.literal.*;
0027: import de.uka.ilkd.key.java.expression.operator.*;
0028: import de.uka.ilkd.key.java.recoderext.ConstructorNormalformBuilder;
0029: import de.uka.ilkd.key.java.reference.*;
0030: import de.uka.ilkd.key.java.statement.*;
0031: import de.uka.ilkd.key.java.visitor.Visitor;
0032: import de.uka.ilkd.key.logic.ProgramElementName;
0033: import de.uka.ilkd.key.logic.op.*;
0034: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
0035: import de.uka.ilkd.key.logic.sort.Sort;
0036: import de.uka.ilkd.key.rule.AbstractProgramElement;
0037: import de.uka.ilkd.key.rule.inst.SVInstantiations;
0038: import de.uka.ilkd.key.rule.metaconstruct.ConstructorCall;
0039: import de.uka.ilkd.key.rule.metaconstruct.MethodCall;
0040: import de.uka.ilkd.key.rule.metaconstruct.ProgramMetaConstruct;
0041: import de.uka.ilkd.key.rule.soundness.ProgramSVProxy;
0042: import de.uka.ilkd.key.rule.soundness.ProgramSVSkolem;
0043: import de.uka.ilkd.key.util.Debug;
0044:
0045: class TypeSchemeConstraintExtractor implements Visitor {
0046:
0047: //-------------------------------------------------------------------------
0048: //member variables
0049: //-------------------------------------------------------------------------
0050:
0051: /**
0052: * Constant used to mark levels on the stack.
0053: */
0054: private static final Object LEVEL = new Object() {
0055: public String toString() {
0056: return "LEVEL";
0057: }
0058: };
0059:
0060: /**
0061: * Name used for variables which are introduced as a replacement
0062: * for more complex expressions which cannot be handled as
0063: * receivers or parameters by the MethodCall and ConstructorCall
0064: * metaconstructs.
0065: */
0066: private static final ProgramElementName INVISIBLE_NAME = new ProgramElementName(
0067: "invisible_var");
0068:
0069: /**
0070: * Stack used to propagate type scheme terms around the AST.
0071: */
0072: private final Stack /*TypeSchemeTerm*/stack = new Stack();
0073:
0074: /**
0075: * Map containing the formal result variables defined so far.
0076: */
0077: private final Map /*MethodReference -> ProgramVariable*/formalResultVars = new HashMap();
0078:
0079: /**
0080: * The services object.
0081: */
0082: private final Services services;
0083:
0084: /**
0085: * Type scheme checker.
0086: */
0087: private TypeSchemeChecker checker;
0088:
0089: /**
0090: * The methods covered so far.
0091: */
0092: private ListOfProgramMethod coveredMethods;
0093:
0094: /**
0095: * The sv instantiations, including an execution context suitable for
0096: * the currently visited method.
0097: */
0098: private SVInstantiations svInst;
0099:
0100: /**
0101: * The term of the formal result variable of the currently visited method.
0102: */
0103: private TypeSchemeTerm contextFormalResultTerm;
0104:
0105: /**
0106: * The last error message in case of failure.
0107: */
0108: private String errorString;
0109:
0110: /**
0111: * Used by walk() to signal to the visitor methods whether the node is
0112: * being entered or left.
0113: */
0114: private boolean entering;
0115:
0116: /**
0117: * Used by the visitor methods to let walk() descend into something other
0118: * than the node's regular children.
0119: */
0120: private ProgramElement[] adoptedChildren;
0121:
0122: //-------------------------------------------------------------------------
0123: //public interface
0124: //-------------------------------------------------------------------------
0125:
0126: public TypeSchemeConstraintExtractor(Services services) {
0127: this .services = services;
0128: }
0129:
0130: /**
0131: * Compares a program with the universe type rules.
0132: * @param root the program
0133: * @param annotations map from Location to TypeSchemeTerm containing
0134: * the predefined field annotations; fields not contained in the map are
0135: * taken to have type scheme rootS
0136: * @param svInst sv instantiations
0137: * @return a list of constraints describing what must hold for the program
0138: * to satisfy the type rules
0139: */
0140: public ListOfTypeSchemeConstraint extract(ProgramElement root,
0141: Map annotations, SVInstantiations svInst) {
0142: //initialise members
0143: stack.clear();
0144: formalResultVars.clear();
0145: checker = new TypeSchemeChecker(annotations);
0146: coveredMethods = SLListOfProgramMethod.EMPTY_LIST;
0147: this .svInst = svInst;
0148: contextFormalResultTerm = null;
0149: errorString = null;
0150:
0151: //walk the program, thereby generating the constraints
0152: try {
0153: walk(root);
0154: } catch (Exception e) {
0155: fail("An exception occurred during the extraction:");
0156: e.printStackTrace(System.out);
0157: checker.fail();
0158: return checker.getConstraints();
0159: }
0160:
0161: //in case of failure, repeat the reason
0162: if (errorString != null) {
0163: verbose("The extraction failed because of the following problem:");
0164: verbose(errorString);
0165: }
0166:
0167: //return the constraints
0168: return checker.getConstraints();
0169: }
0170:
0171: /**
0172: * Returns a list of the methods which have been analysed in the last run
0173: * of extract().
0174: */
0175: public ListOfProgramMethod getCoveredMethods() {
0176: return coveredMethods;
0177: }
0178:
0179: //-------------------------------------------------------------------------
0180: //helper methods
0181: //-------------------------------------------------------------------------
0182:
0183: private void verbose(Object o) {
0184: //System.out.println(o);
0185: }
0186:
0187: /**
0188: * Marks the current run as failed. Ensures that the resulting constraints
0189: * cannot be fulfilled.
0190: */
0191: private void fail(String s) {
0192: verbose(s);
0193: errorString = s;
0194: checker.fail();
0195: }
0196:
0197: private void failUnexpected(ProgramElement pe) {
0198: fail("Encountered an unexpected type of program element: " + pe
0199: + " (" + pe.getClass() + ")");
0200: }
0201:
0202: private void printStack() {
0203: verbose("Current stack:");
0204: Iterator it = stack.iterator();
0205: while (it.hasNext()) {
0206: verbose(it.next());
0207: }
0208: }
0209:
0210: /**
0211: * Pushes a term onto the stack.
0212: */
0213: private void push(TypeSchemeTerm term) {
0214: Debug.assertTrue(term != null);
0215: verbose("Pushing: " + term);
0216: stack.push(term);
0217: }
0218:
0219: /**
0220: * Pops a term off the stack.
0221: */
0222: private TypeSchemeTerm pop() {
0223: verbose("Popping: " + stack.peek());
0224: if (stack.peek() == LEVEL) {
0225: printStack();
0226: }
0227: return (TypeSchemeTerm) stack.pop();
0228: }
0229:
0230: /**
0231: * Pushes the LEVEL constant onto the stack.
0232: */
0233: private void pushLevel() {
0234: stack.push(LEVEL);
0235: }
0236:
0237: /**
0238: * Pops all elements until the next LEVEL constant (inclusive) from the
0239: * stack.
0240: * @return a list of the elements, whose the first element is the lowermost
0241: * element from the stack which is not LEVEL
0242: */
0243: private ListOfTypeSchemeTerm popLevel() {
0244: ListOfTypeSchemeTerm result = SLListOfTypeSchemeTerm.EMPTY_LIST;
0245:
0246: Object o = stack.pop();
0247: while (o != LEVEL) {
0248: verbose("Level-popping: " + o);
0249: result = result.prepend((TypeSchemeTerm) o);
0250: o = stack.pop();
0251: }
0252:
0253: return result;
0254: }
0255:
0256: private boolean haveCommonSupertype(KeYJavaType kjt1,
0257: KeYJavaType kjt2) {
0258: JavaInfo javaInfo = services.getJavaInfo();
0259:
0260: if (kjt1.equals(kjt2)) {
0261: return true;
0262: }
0263:
0264: if (kjt1.getSort() instanceof PrimitiveSort
0265: || kjt2.getSort() instanceof PrimitiveSort) {
0266: return false;
0267: }
0268:
0269: ListOfKeYJavaType super types1 = javaInfo.getAllSupertypes(kjt1);
0270: super types1 = super types1.prepend(kjt1);
0271: ListOfKeYJavaType super types2 = javaInfo.getAllSupertypes(kjt2);
0272: super types2 = super types2.prepend(kjt2);
0273:
0274: IteratorOfKeYJavaType it = super types1.iterator();
0275: while (it.hasNext()) {
0276: if (super types2.contains(it.next())) {
0277: return true;
0278: }
0279: }
0280:
0281: return false;
0282: }
0283:
0284: private boolean areInSameFamily(MethodReference mr1,
0285: MethodReference mr2) {
0286: ExecutionContext ec = svInst.getExecutionContext();
0287:
0288: if (!mr1.getProgramElementName().equals(
0289: mr2.getProgramElementName())) {
0290: return false;
0291: }
0292:
0293: if (!haveCommonSupertype(mr1.determineStaticPrefixType(
0294: services, ec), mr2.determineStaticPrefixType(services,
0295: ec))) {
0296: return false;
0297: }
0298:
0299: ListOfKeYJavaType sig1 = mr1.getMethodSignature(services, ec);
0300: ListOfKeYJavaType sig2 = mr2.getMethodSignature(services, ec);
0301: if (sig1.size() != sig2.size()) {
0302: return false;
0303: }
0304:
0305: IteratorOfKeYJavaType it1 = sig1.iterator();
0306: IteratorOfKeYJavaType it2 = sig2.iterator();
0307: while (it1.hasNext()) {
0308: if (!haveCommonSupertype(it1.next(), it2.next())) {
0309: return false;
0310: }
0311: }
0312:
0313: return true;
0314: }
0315:
0316: private ProgramVariable getFormalResultVar(MethodReference mr) {
0317: Iterator it = formalResultVars.keySet().iterator();
0318:
0319: while (it.hasNext()) {
0320: MethodReference mr2 = (MethodReference) it.next();
0321: if (areInSameFamily(mr, mr2)) {
0322: return (ProgramVariable) formalResultVars.get(mr2);
0323: }
0324: }
0325:
0326: KeYJavaType resultType = mr.getKeYJavaType(services, svInst
0327: .getExecutionContext());
0328: ProgramElementName resultName = new ProgramElementName("res_"
0329: + mr.getName());
0330: ProgramVariable formalResultVar = new LocationVariable(
0331: resultName, resultType);
0332: formalResultVars.put(mr, formalResultVar);
0333:
0334: return formalResultVar;
0335: }
0336:
0337: /**
0338: * Tells whether a method body statement describes a constructor invocation
0339: * within an allocation (i.e. not this() or super())
0340: */
0341: private boolean isAllocationConstructorInvocation(
0342: MethodBodyStatement mbs) {
0343: final ProgramMethod pm = mbs.getProgramMethod(services);
0344: return (pm
0345: .name()
0346: .toString()
0347: .endsWith(
0348: ConstructorNormalformBuilder.CONSTRUCTOR_NORMALFORM_IDENTIFIER) && mbs
0349: .getResultVariable() == null);
0350: }
0351:
0352: /**
0353: * Tells whether a program method should actually have a (non-empty)
0354: * implementation, but it is not available to KeY.
0355: */
0356: private boolean implementationIsUnavailable(ProgramMethod pm) {
0357: final TypeDeclaration typeDecl = (TypeDeclaration) pm
0358: .getContainerType().getJavaType();
0359: //pessimistically treat any library method with an empty body
0360: //as one with missing implementation, but make an exception for
0361: //those in java.lang.Object (because e.g. Object.<init>() is always
0362: //called during any object creation, and because they're harmless)
0363: return (typeDecl.isLibraryClass() && pm.getBody().isEmpty() && !typeDecl
0364: .getFullName().equals("java.lang.Object"));
0365: }
0366:
0367: /**
0368: * Tells whether the current context is static or not.
0369: */
0370: private boolean contextIsStatic() {
0371: ExecutionContext executionContext = svInst
0372: .getExecutionContext();
0373: return (executionContext == null || !(executionContext
0374: .getRuntimeInstance() instanceof Expression));
0375: }
0376:
0377: /**
0378: * Replaces an expression by a simpler one with the same static type,
0379: * so that it can be handled as a receiver or parameter by the
0380: * ConstructorCall and MethodCall metaconstructs.
0381: */
0382: private ProgramVariable simplifyExpression(Expression expression) {
0383: KeYJavaType staticKjt = expression.getKeYJavaType(services,
0384: svInst.getExecutionContext());
0385: Debug.assertTrue(staticKjt != null);
0386: return new LocationVariable(INVISIBLE_NAME, staticKjt);
0387: }
0388:
0389: private ArrayOfExpression simplifyExpressions(
0390: ArrayOfExpression expressions) {
0391: Expression[] result = new Expression[expressions.size()];
0392: for (int i = 0; i < expressions.size(); i++) {
0393: result[i] = simplifyExpression(expressions.getExpression(i));
0394: }
0395: return new ArrayOfExpression(result);
0396: }
0397:
0398: private New simplifyNew(New n) {
0399: Debug.assertFalse(n.getReferencePrefix() instanceof Expression);
0400: ArrayOfExpression simpleArgs = simplifyExpressions(n
0401: .getArguments());
0402: Expression[] simpleArgsArray = new Expression[simpleArgs.size()];
0403: for (int i = 0; i < simpleArgs.size(); i++) {
0404: simpleArgsArray[i] = simpleArgs.getExpression(i);
0405: }
0406: return new New(simpleArgsArray, n.getTypeReference(), n
0407: .getReferencePrefix());
0408: }
0409:
0410: private MethodReference simplifyMethodReference(MethodReference mr) {
0411: ReferencePrefix rp = mr.getReferencePrefix();
0412: ReferencePrefix simpleRp = (rp instanceof ThisReference
0413: || rp instanceof SuperReference
0414: || rp instanceof ProgramVariable
0415: || rp instanceof FieldReference
0416: || !(rp instanceof Expression) ? rp
0417: : simplifyExpression((Expression) rp));
0418:
0419: return new MethodReference(simplifyExpressions(mr
0420: .getArguments()), mr.getMethodName(), simpleRp);
0421: }
0422:
0423: //-------------------------------------------------------------------------
0424: //AST walking methods
0425: //-------------------------------------------------------------------------
0426:
0427: private String addSpaces(String s) {
0428: while (s.length() < 45) {
0429: s += " ";
0430: }
0431: return s;
0432: }
0433:
0434: private void walk(ProgramElement node) {
0435: //debug output
0436: String fullClassName = node.getClass().getName();
0437: String className = fullClassName.substring(fullClassName
0438: .lastIndexOf(".") + 1);
0439: String enteringString = addSpaces("Entering: " + node) + "("
0440: + className + ")";
0441: String ascendingString = addSpaces("Ascending: " + node) + "("
0442: + className + ")";
0443: verbose(enteringString);
0444:
0445: //visit the node
0446: adoptedChildren = null;
0447: entering = true;
0448: node.visit(this );
0449:
0450: //walk children (either the adopted or the normal ones)
0451: if (adoptedChildren != null) {
0452: ProgramElement[] ac = (ProgramElement[]) adoptedChildren
0453: .clone();
0454: for (int i = 0; i < ac.length; i++) {
0455: walk(ac[i]);
0456: }
0457: verbose(ascendingString);
0458: } else if (node instanceof NonTerminalProgramElement) {
0459: NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
0460: for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
0461: walk(nonTerminalNode.getChildAt(i));
0462: }
0463: verbose(ascendingString);
0464: }
0465:
0466: //visit the node again
0467: entering = false;
0468: node.visit(this );
0469: }
0470:
0471: private void performActionOnPrimitiveLiteral() {
0472: if (!entering) {
0473: TypeSchemeTerm resultTerm = checker.checkPrimitiveLiteral();
0474: push(resultTerm);
0475: }
0476: }
0477:
0478: private void performActionOnPrimitiveUnary() {
0479: if (!entering) {
0480: TypeSchemeTerm operandTerm = pop();
0481: TypeSchemeTerm resultTerm = checker
0482: .checkPrimitiveUnary(operandTerm);
0483: push(resultTerm);
0484: }
0485: }
0486:
0487: private void performActionOnPrimitiveBinary() {
0488: if (!entering) {
0489: TypeSchemeTerm operandTerm1 = pop();
0490: TypeSchemeTerm operandTerm2 = pop();
0491:
0492: TypeSchemeTerm resultTerm = checker.checkPrimitiveBinary(
0493: operandTerm1, operandTerm2);
0494:
0495: push(resultTerm);
0496: }
0497: }
0498:
0499: public void performActionOnAbstractProgramElement(
0500: AbstractProgramElement x) {
0501: failUnexpected(x);
0502: }
0503:
0504: public void performActionOnProgramElementName(ProgramElementName x) {
0505: //nothing to do
0506: }
0507:
0508: public void performActionOnProgramVariable(ProgramVariable x) {
0509: if (!entering) {
0510: TypeSchemeTerm varTerm;
0511:
0512: if (x.isMember()) {
0513: if (x.isStatic()) {
0514: varTerm = checker.checkStaticField(x);
0515: } else {
0516: varTerm = checker.checkInstanceField(x);
0517: }
0518: } else {
0519: if (contextIsStatic()) {
0520: varTerm = checker.checkStaticLocalVariable(x);
0521: } else {
0522: varTerm = checker.checkInstanceLocalVariable(x);
0523: }
0524: }
0525:
0526: push(varTerm);
0527: }
0528: }
0529:
0530: public void performActionOnSchemaVariable(SchemaVariable x) {
0531: failUnexpected((ProgramSV) x);
0532: }
0533:
0534: public void performActionOnProgramMethod(ProgramMethod x) {
0535: failUnexpected(x);
0536: }
0537:
0538: public void performActionOnProgramMetaConstruct(
0539: ProgramMetaConstruct x) {
0540: failUnexpected(x);
0541: }
0542:
0543: public void performActionOnContextStatementBlock(
0544: ContextStatementBlock x) {
0545: failUnexpected(x);
0546: }
0547:
0548: public void performActionOnIntLiteral(IntLiteral x) {
0549: performActionOnPrimitiveLiteral();
0550: }
0551:
0552: public void performActionOnBooleanLiteral(BooleanLiteral x) {
0553: performActionOnPrimitiveLiteral();
0554: }
0555:
0556: public void performActionOnStringLiteral(StringLiteral x) {
0557: if (!entering) {
0558: TypeSchemeTerm stringLiteralTerm = checker
0559: .checkStringLiteral();
0560: push(stringLiteralTerm);
0561: }
0562: }
0563:
0564: public void performActionOnNullLiteral(NullLiteral x) {
0565: if (!entering) {
0566: TypeSchemeTerm nullTerm = checker.checkNull();
0567: push(nullTerm);
0568: }
0569: }
0570:
0571: public void performActionOnCharLiteral(CharLiteral x) {
0572: performActionOnPrimitiveLiteral();
0573: }
0574:
0575: public void performActionOnDoubleLiteral(DoubleLiteral x) {
0576: performActionOnPrimitiveLiteral();
0577: }
0578:
0579: public void performActionOnLongLiteral(LongLiteral x) {
0580: performActionOnPrimitiveLiteral();
0581: }
0582:
0583: public void performActionOnFloatLiteral(FloatLiteral x) {
0584: performActionOnPrimitiveLiteral();
0585: }
0586:
0587: public void performActionOnPackageSpecification(
0588: PackageSpecification x) {
0589: failUnexpected(x);
0590: }
0591:
0592: public void performActionOnTypeReference(TypeReference x) {
0593: //nothing to do
0594: }
0595:
0596: public void performActionOnPackageReference(PackageReference x) {
0597: //nothing to do
0598: }
0599:
0600: public void performActionOnThrows(Throws x) {
0601: //nothing to do
0602: }
0603:
0604: public void performActionOnArrayInitializer(ArrayInitializer x) {
0605: //nothing to do (handled in performActionOnNewArray() and
0606: //performActionOnVariableSpecification())
0607: }
0608:
0609: public void performActionOnCompilationUnit(CompilationUnit x) {
0610: failUnexpected(x);
0611: }
0612:
0613: public void performActionOnArrayDeclaration(ArrayDeclaration x) {
0614: failUnexpected(x);
0615: }
0616:
0617: public void performActionOnSuperArrayDeclaration(
0618: SuperArrayDeclaration x) {
0619: failUnexpected(x);
0620: }
0621:
0622: public void performActionOnClassDeclaration(ClassDeclaration x) {
0623: failUnexpected(x);
0624: }
0625:
0626: public void performActionOnInterfaceDeclaration(
0627: InterfaceDeclaration x) {
0628: failUnexpected(x);
0629: }
0630:
0631: public void performActionOnFieldDeclaration(FieldDeclaration x) {
0632: failUnexpected(x);
0633: }
0634:
0635: public void performActionOnLocalVariableDeclaration(
0636: LocalVariableDeclaration x) {
0637: //nothing to do (initialisation handled in
0638: //performActionOnVariableSpecification)
0639: }
0640:
0641: public void performActionOnVariableDeclaration(VariableDeclaration x) {
0642: failUnexpected(x);
0643: }
0644:
0645: public void performActionOnParameterDeclaration(
0646: ParameterDeclaration x) {
0647: //nothing to do
0648: }
0649:
0650: public void performActionOnMethodDeclaration(MethodDeclaration x) {
0651: failUnexpected(x);
0652: }
0653:
0654: public void performActionOnClassInitializer(ClassInitializer x) {
0655: failUnexpected(x);
0656: }
0657:
0658: public void performActionOnStatementBlock(StatementBlock x) {
0659: if (entering) {
0660: pushLevel();
0661: } else {
0662: popLevel();
0663: }
0664: }
0665:
0666: public void performActionOnBreak(Break x) {
0667: //nothing to do
0668: }
0669:
0670: public void performActionOnContinue(Continue x) {
0671: //nothing to do
0672: }
0673:
0674: public void performActionOnReturn(Return x) {
0675: if (!entering) {
0676: TypeSchemeTerm actualResultTerm = null;
0677: if (contextFormalResultTerm != null) {
0678: actualResultTerm = pop();
0679: }
0680: checker.checkReturn(actualResultTerm,
0681: contextFormalResultTerm);
0682: }
0683: }
0684:
0685: public void performActionOnThrow(Throw x) {
0686: //nothing to do
0687: }
0688:
0689: public void performActionOnDo(Do x) {
0690: //nothing to do
0691: }
0692:
0693: public void performActionOnFor(For x) {
0694: //nothing to do
0695: }
0696:
0697: public void performActionOnWhile(While x) {
0698: //nothing to do
0699: }
0700:
0701: public void performActionOnIf(If x) {
0702: //nothing to do
0703: }
0704:
0705: public void performActionOnSwitch(Switch x) {
0706: //nothing to do
0707: }
0708:
0709: public void performActionOnTry(Try x) {
0710: //nothing to do
0711: }
0712:
0713: public void performActionOnLabeledStatement(LabeledStatement x) {
0714: //nothing to do
0715: }
0716:
0717: public void performActionOnMethodFrame(MethodFrame x) {
0718: failUnexpected(x);
0719: }
0720:
0721: public void performActionOnMethodBodyStatement(MethodBodyStatement x) {
0722: if (entering) {
0723: //don't descend into anything - receiver and parameters have
0724: //already been visited before entering the enclosing statement
0725: //block
0726: adoptedChildren = new ProgramElement[0];
0727: } else {
0728: final ProgramMethod pm = x.getProgramMethod(services);
0729: final StatementBlock body = pm.getBody();
0730: final boolean isAllocation = isAllocationConstructorInvocation(x);
0731: final boolean isStatic = pm.isStatic();
0732:
0733: //check for methods which cannot be handled
0734: if (implementationIsUnavailable(pm)) {
0735: fail("Encountered library method with unavailable "
0736: + "implementation: " + pm);
0737: }
0738: if (pm.isNative()) {
0739: fail("Encountered native method: " + pm);
0740: }
0741:
0742: //pop the level mark of the enclosing statement block,
0743: //thereby getting rid of result of the instanceof which
0744: //may stand before this mbs in the if-cascade
0745: popLevel();
0746:
0747: //get actual and formal parameter terms
0748: final ArrayOfParameterDeclaration parDecls = pm
0749: .getParameters();
0750: final int numPars = parDecls.size();
0751: final TypeSchemeTerm actualParTerms[] = new TypeSchemeTerm[numPars];
0752: final TypeSchemeTerm formalParTerms[] = new TypeSchemeTerm[numPars];
0753: for (int i = numPars - 1; i >= 0; i--) {
0754: actualParTerms[i] = pop();
0755:
0756: ParameterDeclaration parDecl = parDecls
0757: .getParameterDeclaration(i);
0758: VariableSpecification parSpec = parDecl
0759: .getVariableSpecification();
0760: ProgramVariable formalParVar = (ProgramVariable) parSpec
0761: .getProgramVariable();
0762: formalParTerms[i] = (pm.isStatic() ? checker
0763: .checkStaticLocalVariable(formalParVar)
0764: : checker
0765: .checkInstanceLocalVariable(formalParVar));
0766: }
0767:
0768: //get receiver term
0769: final TypeSchemeTerm receiverTerm = pop();
0770:
0771: //get formal result term
0772: final ProgramVariable formalResultVar = (ProgramVariable) x
0773: .getResultVariable();
0774: final TypeSchemeTerm formalResultTerm = (formalResultVar == null ? null
0775: : (pm.isStatic() ? checker
0776: .checkStaticLocalVariable(formalResultVar)
0777: : checker
0778: .checkInstanceLocalVariable(formalResultVar)));
0779:
0780: //generate constraints
0781: final TypeSchemeTerm actualResultTerm;
0782: if (isAllocation) {
0783: actualResultTerm = checker.checkAllocation(
0784: actualParTerms, formalParTerms);
0785: } else if (isStatic) {
0786: actualResultTerm = checker.checkStaticMethodCall(
0787: actualParTerms, formalParTerms,
0788: formalResultTerm);
0789: } else {
0790: actualResultTerm = checker.checkInstanceMethodCall(
0791: receiverTerm, actualParTerms, formalParTerms,
0792: formalResultTerm);
0793: }
0794:
0795: //go down into method, if not already covered
0796: if (!coveredMethods.contains(pm)) {
0797: coveredMethods = coveredMethods.append(pm);
0798:
0799: //determine new execution context
0800: final TypeReference classContext = new TypeRef(pm
0801: .getContainerType());
0802: final ReferencePrefix runtimeInstance = x
0803: .getDesignatedContext();
0804: final ExecutionContext executionContext = new ExecutionContext(
0805: classContext, runtimeInstance);
0806:
0807: //save context information
0808: final SVInstantiations oldSvInst = svInst;
0809: final TypeSchemeTerm oldContextFormalResultTerm = contextFormalResultTerm;
0810:
0811: //adapt context information
0812: svInst = svInst.replace(null, null, executionContext,
0813: body);
0814: contextFormalResultTerm = formalResultTerm;
0815:
0816: //walk the body
0817: verbose("=========body enter (" + pm + ")=========");
0818: pushLevel();
0819: walk(body);
0820: popLevel();
0821: verbose("=========body exit (" + pm + ")==========");
0822:
0823: //restore context information
0824: svInst = oldSvInst;
0825: contextFormalResultTerm = oldContextFormalResultTerm;
0826: }
0827:
0828: //push result term
0829: if (actualResultTerm != null) {
0830: push(actualResultTerm);
0831: }
0832:
0833: //re-push receiver and actual parameter terms, so that other
0834: //members of the the if-cascade can get them as well
0835: push(receiverTerm);
0836: for (int i = 0; i < numPars; i++) {
0837: push(actualParTerms[i]);
0838: }
0839:
0840: //re-push the enclosing statement block's level mark
0841: pushLevel();
0842: }
0843: }
0844:
0845: public void performActionOnCatchAllStatement(CatchAllStatement x) {
0846: failUnexpected(x);
0847: }
0848:
0849: public void performActionOnSynchronizedBlock(SynchronizedBlock x) {
0850: //nothing to do
0851: }
0852:
0853: public void performActionOnImport(Import x) {
0854: failUnexpected(x);
0855: }
0856:
0857: public void performActionOnExtends(Extends x) {
0858: failUnexpected(x);
0859: }
0860:
0861: public void performActionOnImplements(Implements x) {
0862: failUnexpected(x);
0863: }
0864:
0865: public void performActionOnVariableSpecification(
0866: VariableSpecification x) {
0867: if (!entering) {
0868: //skip assignments with "invisible" variables
0869: //Rationale: A method reference, say "e1.m(e2)" is simplified to
0870: //"v1.m(v2)", where v1 and v2 are "invisible" variables, and
0871: //then passed to The MethodCall metaconstruct, which replaces it
0872: //by "p#1 = v2; v1.m(p#1);". However, since
0873: //performActionOnMethodBodyStatement() actually works directly on
0874: //the real receiver e1 and the real parameter e2, none of these
0875: //intermediate helper variables occurs in the constraints which are
0876: //generated for the method call. Thus, creating constraints for the
0877: //assignments between them would be superfluous.
0878: if (x.getInitializer() instanceof ProgramVariable
0879: && ((ProgramVariable) x.getInitializer())
0880: .getProgramElementName() == INVISIBLE_NAME) {
0881: return;
0882: }
0883:
0884: if (x.getInitializer() instanceof ArrayInitializer) {
0885: ArrayInitializer ai = (ArrayInitializer) x
0886: .getInitializer();
0887:
0888: TypeSchemeTerm[] initTerms = new TypeSchemeTerm[ai
0889: .getExpressionCount()];
0890: for (int i = ai.getExpressionCount() - 1; i >= 0; i--) {
0891: initTerms[i] = pop();
0892: }
0893: TypeSchemeTerm arrayTerm = pop();
0894:
0895: Expression arrayExpr = (Expression) x.getChildAt(0);
0896: Sort arraySort = arrayExpr.getKeYJavaType(services,
0897: svInst.getExecutionContext()).getSort();
0898:
0899: TypeSchemeTerm referenceTerm = checker
0900: .checkArrayAccess(arraySort, arrayTerm, null);
0901:
0902: for (int i = 0; i < ai.getExpressionCount(); i++) {
0903: checker
0904: .checkAssignment(referenceTerm,
0905: initTerms[i]);
0906: }
0907:
0908: push(arrayTerm);
0909: } else {
0910: TypeSchemeTerm initTerm = (x.hasInitializer() ? pop()
0911: : null);
0912: TypeSchemeTerm varTerm = pop();
0913:
0914: if (initTerm != null) {
0915: checker.checkAssignment(varTerm, initTerm);
0916: }
0917:
0918: push(varTerm);
0919: }
0920: }
0921: }
0922:
0923: public void performActionOnFieldSpecification(FieldSpecification x) {
0924: failUnexpected(x);
0925: }
0926:
0927: public void performActionOnImplicitFieldSpecification(
0928: ImplicitFieldSpecification x) {
0929: failUnexpected(x);
0930: }
0931:
0932: public void performActionOnBinaryAnd(BinaryAnd x) {
0933: performActionOnPrimitiveBinary();
0934: }
0935:
0936: public void performActionOnBinaryAndAssignment(BinaryAndAssignment x) {
0937: performActionOnPrimitiveBinary();
0938: }
0939:
0940: public void performActionOnBinaryOrAssignment(BinaryOrAssignment x) {
0941: performActionOnPrimitiveBinary();
0942: }
0943:
0944: public void performActionOnBinaryXOrAssignment(BinaryXOrAssignment x) {
0945: performActionOnPrimitiveBinary();
0946: }
0947:
0948: public void performActionOnCopyAssignment(CopyAssignment x) {
0949: if (!entering) {
0950: TypeSchemeTerm rhsTerm = pop();
0951: TypeSchemeTerm lhsTerm = pop();
0952:
0953: TypeSchemeTerm assignmentTerm = checker.checkAssignment(
0954: lhsTerm, rhsTerm);
0955:
0956: push(assignmentTerm);
0957: }
0958: }
0959:
0960: public void performActionOnDivideAssignment(DivideAssignment x) {
0961: performActionOnPrimitiveBinary();
0962: }
0963:
0964: public void performActionOnMinusAssignment(MinusAssignment x) {
0965: performActionOnPrimitiveBinary();
0966: }
0967:
0968: public void performActionOnModuloAssignment(ModuloAssignment x) {
0969: performActionOnPrimitiveBinary();
0970: }
0971:
0972: public void performActionOnPlusAssignment(PlusAssignment x) {
0973: performActionOnPrimitiveBinary();
0974: }
0975:
0976: public void performActionOnPostDecrement(PostDecrement x) {
0977: performActionOnPrimitiveUnary();
0978: }
0979:
0980: public void performActionOnPostIncrement(PostIncrement x) {
0981: performActionOnPrimitiveUnary();
0982: }
0983:
0984: public void performActionOnPreDecrement(PreDecrement x) {
0985: performActionOnPrimitiveUnary();
0986: }
0987:
0988: public void performActionOnPreIncrement(PreIncrement x) {
0989: performActionOnPrimitiveUnary();
0990: }
0991:
0992: public void performActionOnShiftLeftAssignment(ShiftLeftAssignment x) {
0993: performActionOnPrimitiveBinary();
0994: }
0995:
0996: public void performActionOnShiftRightAssignment(
0997: ShiftRightAssignment x) {
0998: performActionOnPrimitiveBinary();
0999: }
1000:
1001: public void performActionOnTimesAssignment(TimesAssignment x) {
1002: performActionOnPrimitiveBinary();
1003: }
1004:
1005: public void performActionOnUnsignedShiftRightAssignment(
1006: UnsignedShiftRightAssignment x) {
1007: performActionOnPrimitiveBinary();
1008: }
1009:
1010: public void performActionOnBinaryNot(BinaryNot x) {
1011: performActionOnPrimitiveBinary();
1012: }
1013:
1014: public void performActionOnBinaryOr(BinaryOr x) {
1015: performActionOnPrimitiveBinary();
1016: }
1017:
1018: public void performActionOnBinaryXOr(BinaryXOr x) {
1019: performActionOnPrimitiveBinary();
1020: }
1021:
1022: public void performActionOnConditional(Conditional x) {
1023: if (!entering) {
1024: TypeSchemeTerm elseTerm = pop();
1025: TypeSchemeTerm thenTerm = pop();
1026: TypeSchemeTerm conditionTerm = pop();
1027:
1028: TypeSchemeTerm conditionalTerm = checker.checkConditional(
1029: conditionTerm, thenTerm, elseTerm);
1030:
1031: push(conditionalTerm);
1032: }
1033: }
1034:
1035: public void performActionOnDivide(Divide x) {
1036: performActionOnPrimitiveBinary();
1037: }
1038:
1039: public void performActionOnEquals(Equals x) {
1040: performActionOnPrimitiveBinary();
1041: }
1042:
1043: public void performActionOnGreaterOrEquals(GreaterOrEquals x) {
1044: performActionOnPrimitiveBinary();
1045: }
1046:
1047: public void performActionOnGreaterThan(GreaterThan x) {
1048: performActionOnPrimitiveBinary();
1049: }
1050:
1051: public void performActionOnLessOrEquals(LessOrEquals x) {
1052: performActionOnPrimitiveBinary();
1053: }
1054:
1055: public void performActionOnLessThan(LessThan x) {
1056: performActionOnPrimitiveBinary();
1057: }
1058:
1059: public void performActionOnNotEquals(NotEquals x) {
1060: performActionOnPrimitiveBinary();
1061: }
1062:
1063: public void performActionOnNewArray(NewArray x) {
1064: if (!entering) {
1065: ArrayInitializer ai = x.getArrayInitializer();
1066: TypeSchemeTerm sizeTerm = (ai == null ? pop() : null);
1067:
1068: TypeSchemeTerm arrayTerm = checker
1069: .checkArrayAllocation(sizeTerm);
1070:
1071: if (ai != null) {
1072: Sort arraySort = x.getKeYJavaType().getSort();
1073: TypeSchemeTerm referenceTerm = checker
1074: .checkArrayAccess(arraySort, arrayTerm, null);
1075: for (int i = 0; i < ai.getExpressionCount(); i++) {
1076: TypeSchemeTerm initTerm = pop();
1077: checker.checkAssignment(referenceTerm, initTerm);
1078: }
1079: }
1080:
1081: push(arrayTerm);
1082: }
1083: }
1084:
1085: public void performActionOnInstanceof(Instanceof x) {
1086: performActionOnPrimitiveUnary();
1087: }
1088:
1089: public void performActionOnExactInstanceof(ExactInstanceof x) {
1090: performActionOnPrimitiveUnary();
1091: }
1092:
1093: public void performActionOnNew(New x) {
1094: if (entering) {
1095: //get the new-object type
1096: KeYJavaType newObjectType = x.getKeYJavaType(services,
1097: svInst.getExecutionContext());
1098: assert newObjectType != null;
1099:
1100: //create a new-object variable and save it in an SVInstantiations
1101: //as instantiation of some SV
1102: ProgramElementName newObjectName = new ProgramElementName(
1103: "new" + newObjectType.getSort().name());
1104: ProgramVariable newObjectVar = new LocationVariable(
1105: newObjectName, newObjectType);
1106: SchemaVariable newObjectSV = new NameSV(newObjectName
1107: + "SV");
1108: SVInstantiations mySvInst = svInst.add(newObjectSV,
1109: newObjectVar);
1110:
1111: //let the ConstructorCall metaconstruct expand the constructor
1112: //reference
1113: New simpleX = simplifyNew(x);
1114: ConstructorCall cc = new ConstructorCall(newObjectSV,
1115: simpleX);
1116: ProgramElement expandedPe = cc.symbolicExecution(simpleX,
1117: services, mySvInst);
1118:
1119: //descend into prefix, parameters and expansion instead of
1120: //normal children
1121: final ArrayOfExpression args = x.getArguments();
1122: adoptedChildren = new ProgramElement[args.size() + 2];
1123: adoptedChildren[0] = new ThisReference();
1124: for (int i = 0; i < args.size(); i++) {
1125: adoptedChildren[i + 1] = args.getExpression(i);
1126: }
1127: adoptedChildren[args.size() + 1] = expandedPe;
1128:
1129: pushLevel();
1130: } else {
1131: //get rid of superfluous terms on the stack, but leave the topmost
1132: //non-LEVEL element as result
1133: ListOfTypeSchemeTerm resultTerms = popLevel();
1134: if (resultTerms.size() > 0) {
1135: push(resultTerms.head());
1136: }
1137: }
1138: }
1139:
1140: public void performActionOnTypeCast(TypeCast x) {
1141: //nothing to do
1142: }
1143:
1144: public void performActionOnLogicalAnd(LogicalAnd x) {
1145: performActionOnPrimitiveBinary();
1146: }
1147:
1148: public void performActionOnLogicalNot(LogicalNot x) {
1149: performActionOnPrimitiveUnary();
1150: }
1151:
1152: public void performActionOnLogicalOr(LogicalOr x) {
1153: performActionOnPrimitiveBinary();
1154: }
1155:
1156: public void performActionOnMinus(Minus x) {
1157: performActionOnPrimitiveBinary();
1158: }
1159:
1160: public void performActionOnModulo(Modulo x) {
1161: performActionOnPrimitiveBinary();
1162: }
1163:
1164: public void performActionOnNegative(Negative x) {
1165: performActionOnPrimitiveUnary();
1166: }
1167:
1168: public void performActionOnPlus(Plus x) {
1169: performActionOnPrimitiveBinary();
1170: }
1171:
1172: public void performActionOnPositive(Positive x) {
1173: performActionOnPrimitiveUnary();
1174: }
1175:
1176: public void performActionOnShiftLeft(ShiftLeft x) {
1177: performActionOnPrimitiveBinary();
1178: }
1179:
1180: public void performActionOnShiftRight(ShiftRight x) {
1181: performActionOnPrimitiveBinary();
1182: }
1183:
1184: public void performActionOnTimes(Times x) {
1185: performActionOnPrimitiveBinary();
1186: }
1187:
1188: public void performActionOnUnsignedShiftRight(UnsignedShiftRight x) {
1189: performActionOnPrimitiveBinary();
1190: }
1191:
1192: public void performActionOnArrayReference(ArrayReference x) {
1193: if (!entering) {
1194: TypeSchemeTerm positionTerm = pop();
1195: TypeSchemeTerm receiverTerm = pop();
1196:
1197: Expression arrayExpr = (Expression) x.getChildAt(0);
1198: Sort arraySort = arrayExpr.getKeYJavaType(services,
1199: svInst.getExecutionContext()).getSort();
1200:
1201: TypeSchemeTerm referenceTerm = checker.checkArrayAccess(
1202: arraySort, receiverTerm, positionTerm);
1203:
1204: push(referenceTerm);
1205: }
1206: }
1207:
1208: public void performActionOnMetaClassReference(MetaClassReference x) {
1209: failUnexpected(x);
1210: }
1211:
1212: public void performActionOnMethodReference(MethodReference x) {
1213: if (entering) {
1214: //try to get the method's result type
1215: final KeYJavaType resultType = x.getKeYJavaType(services,
1216: svInst.getExecutionContext());
1217:
1218: //if the method is non-void, create a result variable and save
1219: //it in an SVInstantiations as instantiation of some SV
1220: final MethodReference simpleX = simplifyMethodReference(x);
1221: final ProgramVariable formalResultVar;
1222: final SchemaVariable formalResultSV;
1223: final SVInstantiations mySvInst;
1224: if (resultType != null) {
1225: formalResultVar = getFormalResultVar(simpleX);
1226: formalResultSV = new NameSV(formalResultVar
1227: .getProgramElementName()
1228: + "SV");
1229: mySvInst = svInst.add(formalResultSV, formalResultVar);
1230: } else {
1231: formalResultVar = null;
1232: formalResultSV = null;
1233: mySvInst = svInst;
1234: }
1235:
1236: //let the MethodCall metaconstruct expand the method reference
1237: final MethodCall mc = new MethodCall(formalResultSV,
1238: simpleX);
1239: final ProgramElement expandedPe = mc.symbolicExecution(
1240: simpleX, services, mySvInst);
1241:
1242: //descend into prefix, parameters and expansion instead of
1243: //normal children
1244: final ReferencePrefix rp = x.getReferencePrefix();
1245: final ArrayOfExpression args = x.getArguments();
1246: adoptedChildren = new ProgramElement[args.size() + 2];
1247: adoptedChildren[0] = (rp instanceof Expression ? rp
1248: : new ThisReference());
1249: for (int i = 0; i < args.size(); i++) {
1250: adoptedChildren[i + 1] = args.getExpression(i);
1251: }
1252: adoptedChildren[args.size() + 1] = expandedPe;
1253:
1254: pushLevel();
1255: } else {
1256: //get rid of superfluous terms on the stack, but leave the topmost
1257: //non-LEVEL element as potential result
1258: ListOfTypeSchemeTerm resultTerms = popLevel();
1259: if (resultTerms.size() > 0) {
1260: push(resultTerms.head());
1261: }
1262: }
1263: }
1264:
1265: public void performActionOnFieldReference(FieldReference x) {
1266: if (!entering) {
1267: TypeSchemeTerm referenceTerm;
1268:
1269: TypeSchemeTerm fieldTerm = pop();
1270:
1271: if (x.getProgramVariable().isStatic()) {
1272: referenceTerm = checker
1273: .checkStaticFieldAccess(fieldTerm);
1274: } else {
1275: TypeSchemeTerm receiverTerm = (x.getReferencePrefix() == null ? checker
1276: .checkThis()
1277: : pop());
1278: referenceTerm = checker.checkInstanceFieldAccess(
1279: receiverTerm, fieldTerm);
1280: }
1281:
1282: push(referenceTerm);
1283: }
1284: }
1285:
1286: public void performActionOnSchematicFieldReference(
1287: SchematicFieldReference x) {
1288: failUnexpected(x);
1289: }
1290:
1291: public void performActionOnVariableReference(VariableReference x) {
1292: //nothing to do
1293: }
1294:
1295: public void performActionOnMethod(ProgramMethod x) {
1296: failUnexpected(x);
1297: }
1298:
1299: public void performActionOnSuperConstructorReference(
1300: SuperConstructorReference x) {
1301: //never met, because ConstructorCall replaces it with
1302: //ordinary MethodReference
1303: failUnexpected(x);
1304: }
1305:
1306: public void performActionOnExecutionContext(ExecutionContext x) {
1307: failUnexpected(x);
1308: }
1309:
1310: public void performActionOnConstructorDeclaration(
1311: ConstructorDeclaration x) {
1312: failUnexpected(x);
1313: }
1314:
1315: public void performActionOnThisConstructorReference(
1316: ThisConstructorReference x) {
1317: //never met, because ConstructorCall replaces it with
1318: //ordinary MethodReference
1319: failUnexpected(x);
1320: }
1321:
1322: public void performActionOnSuperReference(SuperReference x) {
1323: if (!entering) {
1324: TypeSchemeTerm super Term = checker.checkSuper();
1325: push(super Term);
1326: }
1327: }
1328:
1329: public void performActionOnThisReference(ThisReference x) {
1330: if (!entering) {
1331: TypeSchemeTerm this Term = checker.checkThis();
1332: push(this Term);
1333: }
1334: }
1335:
1336: public void performActionOnArrayLengthReference(
1337: ArrayLengthReference x) {
1338: performActionOnPrimitiveLiteral();
1339: }
1340:
1341: public void performActionOnThen(Then x) {
1342: //nothing to do
1343: }
1344:
1345: public void performActionOnElse(Else x) {
1346: //nothing to do
1347: }
1348:
1349: public void performActionOnCase(Case x) {
1350: //nothing to do
1351: }
1352:
1353: public void performActionOnCatch(Catch x) {
1354: if (!entering) {
1355: TypeSchemeTerm excTerm = pop();
1356: checker.checkCatch(excTerm);
1357: }
1358: }
1359:
1360: public void performActionOnDefault(Default x) {
1361: //nothing to do
1362: }
1363:
1364: public void performActionOnFinally(Finally x) {
1365: //nothing to do
1366: }
1367:
1368: public void performActionOnModifier(Modifier x) {
1369: failUnexpected(x);
1370: }
1371:
1372: public void performActionOnEmptyStatement(EmptyStatement x) {
1373: //nothing to do
1374: }
1375:
1376: public void performActionOnComment(Comment x) {
1377: //nothing to do
1378: }
1379:
1380: public void performActionOnParenthesizedExpression(
1381: ParenthesizedExpression x) {
1382: //nothing to do
1383: }
1384:
1385: public void performActionOnPassiveExpression(PassiveExpression x) {
1386: //nothing to do
1387: }
1388:
1389: public void performActionOnForUpdates(ForUpdates x) {
1390: //nothing to do
1391: }
1392:
1393: public void performActionOnGuard(Guard x) {
1394: //nothing to do
1395: }
1396:
1397: public void performActionOnLoopInit(LoopInit x) {
1398: //nothing to do
1399: }
1400:
1401: public void performActionOnAssert(Assert assert1) {
1402: //nothing to do
1403: }
1404:
1405: public void performActionOnProgramSVSkolem(ProgramSVSkolem x) {
1406: failUnexpected(x);
1407: }
1408:
1409: public void performActionOnProgramSVProxy(ProgramSVProxy x) {
1410: failUnexpected(x);
1411: }
1412:
1413: public void performActionOnLocationVariable(LocationVariable x) {
1414: performActionOnProgramVariable(x);
1415: }
1416:
1417: public void performActionOnProgramConstant(ProgramConstant x) {
1418: performActionOnProgramVariable(x);
1419: }
1420:
1421: }
|