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: package de.uka.ilkd.key.logic.sort;
0011:
0012: import java.util.HashMap;
0013: import java.util.Iterator;
0014:
0015: import de.uka.ilkd.key.java.*;
0016: import de.uka.ilkd.key.java.abstraction.*;
0017: import de.uka.ilkd.key.java.declaration.*;
0018: import de.uka.ilkd.key.java.expression.ArrayInitializer;
0019: import de.uka.ilkd.key.java.expression.Literal;
0020: import de.uka.ilkd.key.java.expression.PassiveExpression;
0021: import de.uka.ilkd.key.java.expression.literal.StringLiteral;
0022: import de.uka.ilkd.key.java.expression.operator.Instanceof;
0023: import de.uka.ilkd.key.java.expression.operator.Negative;
0024: import de.uka.ilkd.key.java.expression.operator.New;
0025: import de.uka.ilkd.key.java.expression.operator.NewArray;
0026: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
0027: import de.uka.ilkd.key.java.recoderext.InstanceAllocationMethodBuilder;
0028: import de.uka.ilkd.key.java.recoderext.JVMIsTransientMethodBuilder;
0029: import de.uka.ilkd.key.java.reference.*;
0030: import de.uka.ilkd.key.java.statement.*;
0031: import de.uka.ilkd.key.logic.*;
0032: import de.uka.ilkd.key.logic.op.*;
0033: import de.uka.ilkd.key.rule.soundness.ProgramSVProxy;
0034: import de.uka.ilkd.key.util.ExtList;
0035:
0036: public abstract class ProgramSVSort extends PrimitiveSort {
0037:
0038: // Keeps the mapping of ProgramSVSort names to
0039: // ProgramSVSort instances (helpful in parsing
0040: // schema variable declarations)
0041: private static HashMap name2sort = new HashMap(60);
0042:
0043: //----------- Types of Expression Program SVs ----------------------------
0044:
0045: public static final ProgramSVSort LEFTHANDSIDE = new LeftHandSideSort();
0046:
0047: public static final ProgramSVSort VARIABLE = new ProgramVariableSort();
0048:
0049: public static final ProgramSVSort STATICVARIABLE = new StaticVariableSort();
0050:
0051: public static final ProgramSVSort SIMPLEEXPRESSION = new SimpleExpressionSort();
0052:
0053: public static final ProgramSVSort NONSIMPLEEXPRESSION = new NonSimpleExpressionSort();
0054:
0055: public static final ProgramSVSort EXPRESSION = new ExpressionSort();
0056:
0057: //----------- Initialisation and Creation expressions -------------------
0058:
0059: public static final ProgramSVSort NEW = new NewSVSort();
0060:
0061: public static final ProgramSVSort NEWARRAY = new NewArraySVSort();
0062:
0063: public static final ProgramSVSort ARRAYINITIALIZER = new ArrayInitializerSVSort();
0064:
0065: public static final ProgramSVSort SPECIALCONSTRUCTORREFERENCE = new SpecialConstructorReferenceSort();
0066:
0067: //----------- Expressions with restrictions on kind of type -------------
0068:
0069: // public static final ModelMethodSort MODELMETHOD
0070: // = new ModelMethodSort();
0071:
0072: public static final NonSimpleMethodReferenceSort NONSIMPLEMETHODREFERENCE = new NonSimpleMethodReferenceSort();
0073:
0074: //----------- Types of Statement Program SVs -----------------------------
0075:
0076: public static final ProgramSVSort STATEMENT = new StatementSort();
0077:
0078: public static final ProgramSVSort CATCH = new CatchSort();
0079:
0080: public static final ProgramSVSort METHODBODY = new MethodBodySort();
0081:
0082: public static final ProgramSVSort NONMODELMETHODBODY = new NonModelMethodBodySort();
0083:
0084: //-----------Types--------------------------------------------------------
0085:
0086: public static final ProgramSVSort TYPE = new TypeReferenceSort();
0087:
0088: public static final ProgramSVSort TYPENOTPRIMITIVE = new TypeReferenceNotPrimitiveSort();
0089:
0090: //-----------Others-------------------------------------------------------
0091:
0092: public static final ProgramSVSort METHODNAME = new MethodNameSort();
0093:
0094: public static final ProgramSVSort LABEL = new LabelSort();
0095:
0096: //-----------Specials for primitive types---------------------------------
0097:
0098: public static final ProgramSVSort JAVABOOLEANEXPRESSION = new ExpressionSpecialPrimitiveTypeSort(
0099: "JavaBooleanExpression",
0100: new PrimitiveType[] { PrimitiveType.JAVA_BOOLEAN });
0101:
0102: public static final ProgramSVSort SIMPLEJAVABYTEEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0103: "JavaByteExpression",
0104: new PrimitiveType[] { PrimitiveType.JAVA_BYTE });
0105:
0106: public static final ProgramSVSort SIMPLEJAVACHAREXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0107: "JavaCharExpression",
0108: new PrimitiveType[] { PrimitiveType.JAVA_CHAR });
0109:
0110: public static final ProgramSVSort SIMPLEJAVASHORTEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0111: "JavaShortExpression",
0112: new PrimitiveType[] { PrimitiveType.JAVA_SHORT });
0113:
0114: public static final ProgramSVSort SIMPLEJAVAINTEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0115: "JavaIntExpression",
0116: new PrimitiveType[] { PrimitiveType.JAVA_INT });
0117:
0118: public static final ProgramSVSort SIMPLEJAVALONGEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0119: "JavaLongExpression",
0120: new PrimitiveType[] { PrimitiveType.JAVA_LONG });
0121:
0122: public static final ProgramSVSort SIMPLEJAVABYTESHORTEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0123: "JavaByteShortExpression", new PrimitiveType[] {
0124: PrimitiveType.JAVA_BYTE, PrimitiveType.JAVA_SHORT });
0125:
0126: public static final ProgramSVSort SIMPLEJAVABYTESHORTINTEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0127: "JavaByteShortIntExpression", new PrimitiveType[] {
0128: PrimitiveType.JAVA_BYTE, PrimitiveType.JAVA_SHORT,
0129: PrimitiveType.JAVA_INT });
0130:
0131: public static final ProgramSVSort SIMPLEANYJAVATYPEEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0132: "AnyJavaTypeExpression", new PrimitiveType[] {
0133: PrimitiveType.JAVA_BYTE, PrimitiveType.JAVA_SHORT,
0134: PrimitiveType.JAVA_INT, PrimitiveType.JAVA_LONG });
0135:
0136: public static final ProgramSVSort SIMPLEANYNUMBERTYPEEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0137: "AnyNumberTypeExpression", new PrimitiveType[] {
0138: PrimitiveType.JAVA_BYTE, PrimitiveType.JAVA_SHORT,
0139: PrimitiveType.JAVA_INT, PrimitiveType.JAVA_LONG,
0140: PrimitiveType.JAVA_CHAR });
0141:
0142: public static final ProgramSVSort SIMPLEJAVASHORTINTLONGEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0143: "JavaShortIntLongExpression", new PrimitiveType[] {
0144: PrimitiveType.JAVA_SHORT, PrimitiveType.JAVA_INT,
0145: PrimitiveType.JAVA_LONG });
0146:
0147: public static final ProgramSVSort SIMPLEJAVAINTLONGEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0148: "JavaIntLongExpression", new PrimitiveType[] {
0149: PrimitiveType.JAVA_INT, PrimitiveType.JAVA_LONG });
0150:
0151: public static final ProgramSVSort SIMPLEJAVACHARBYTESHORTINTEXPRESSION = new SimpleExpressionSpecialPrimitiveTypeSort(
0152: "JavaCharByteShortIntExpression", new PrimitiveType[] {
0153: PrimitiveType.JAVA_CHAR, PrimitiveType.JAVA_BYTE,
0154: PrimitiveType.JAVA_SHORT, PrimitiveType.JAVA_INT });
0155:
0156: public static final ProgramSVSort SIMPLESTRINGEXPRESSION = new SimpleExpressionStringSort(
0157: "SimpleStringExpression");
0158:
0159: //--------------- Specials that can be get rid of perhaps--------------
0160:
0161: public static final ProgramSVSort LOOPINIT = new LoopInitSort();
0162:
0163: public static final ProgramSVSort GUARD = new GuardSort();
0164:
0165: public static final ProgramSVSort FORUPDATES = new ForUpdatesSort();
0166:
0167: public static final ProgramSVSort MULTIPLEVARDECL = new MultipleVariableDeclarationSort();
0168:
0169: public static final ProgramSVSort ARRAYPOSTDECL = new ArrayPostDeclarationSort();
0170:
0171: public static final ProgramSVSort SWITCH = new SwitchSVSort();
0172:
0173: public static final ProgramSVSort IMPLICITVARIABLE = new ImplicitProgramVariableSort();
0174:
0175: public static final ProgramSVSort EXPLICITVARIABLE = new ExplicitProgramVariableSort();
0176:
0177: public static final ProgramSVSort CONSTANTVARIABLE = new ConstantProgramVariableSort();
0178:
0179: // implict field match
0180: public static final ProgramSVSort IMPLICITREFERENCE = new ImplicitFieldReferenceSort();
0181:
0182: public static final ProgramSVSort VARIABLEINIT = new ProgramSVSort(
0183: new Name("VariableInitializer")) {
0184: public boolean canStandFor(ProgramElement pe, Services services) {
0185: return true;
0186: }
0187: };
0188:
0189: public static final ProgramSVSort LITERAL = new LiteralSort();
0190:
0191: //--------------- Specials that match on certain names-----------------
0192:
0193: public static final ProgramSVSort IMPLICITCLINIT = new ImplicitFieldSort(
0194: new Name("ImplicitClassInitialized"),
0195: ImplicitFieldAdder.IMPLICIT_CLASS_INITIALIZED, true);
0196:
0197: public static final ProgramSVSort IMPLICITINITINPROGRESS = new ImplicitFieldSort(
0198: new Name("ImplicitClassInitializationInProgress"),
0199: ImplicitFieldAdder.IMPLICIT_CLASS_INIT_IN_PROGRESS, true);
0200:
0201: public static final ProgramSVSort IMPLICITERRONEOUS = new ImplicitFieldSort(
0202: new Name("ImplicitClassErroneous"),
0203: ImplicitFieldAdder.IMPLICIT_CLASS_ERRONEOUS, true);
0204:
0205: public static final ProgramSVSort IMPLICITPREPARED = new ImplicitFieldSort(
0206: new Name("ImplicitClassPrepared"),
0207: ImplicitFieldAdder.IMPLICIT_CLASS_PREPARED, true);
0208:
0209: public static final ProgramSVSort IMPLICITNEXTTOCREATE = new ImplicitFieldSort(
0210: new Name("ImplicitNextToCreate"),
0211: ImplicitFieldAdder.IMPLICIT_NEXT_TO_CREATE, true);
0212:
0213: public static final ProgramSVSort IMPLICITCREATED = new ImplicitFieldSort(
0214: new Name("ImplicitCreated"),
0215: ImplicitFieldAdder.IMPLICIT_CREATED, true);
0216:
0217: public static final ProgramSVSort IMPLICITTRAINITIALIZED = new ImplicitFieldSort(
0218: new Name("ImplicitTraInitialized"),
0219: ImplicitFieldAdder.IMPLICT_ARRAY_TRA_INITIALIZED, true);
0220:
0221: public static final ProgramSVSort IMPLICITTRANSACTIONCOUNTER = new ImplicitFieldSort(
0222: new Name("ImplicitTransactionCounter"),
0223: "de.uka.ilkd.key.javacard.KeYJCSystem"
0224: + "::"
0225: + JVMIsTransientMethodBuilder.IMPLICIT_TRANSACTION_COUNTER,
0226: false);
0227:
0228: public static final ProgramSVSort ARRAYLENGTH = new ArrayLengthSort();
0229:
0230: public static final ProgramSVSort JCMAKETRANSIENTARRAY = new MethodNameReferenceSort(
0231: new Name("makeTransientArray"), new String[] {
0232: "jvmMakeTransientBooleanArray",
0233: "jvmMakeTransientByteArray",
0234: "jvmMakeTransientShortArray",
0235: "jvmMakeTransientObjectArray" },
0236: "de.uka.ilkd.key.javacard.KeYJCSystem",
0237: SLListOfName.EMPTY_LIST.append(new Name("byte")).append(
0238: new Name("short")));
0239:
0240: public static final ProgramSVSort JCARRAYCOPY = new SpecificMethodNameSort(
0241: new ProgramElementName("jvmArrayCopy"));
0242: public static final ProgramSVSort JCARRAYCOPYNONATOMIC = new SpecificMethodNameSort(
0243: new ProgramElementName("jvmArrayCopyNonAtomic"));
0244: public static final ProgramSVSort JCARRAYFILLNONATOMIC = new SpecificMethodNameSort(
0245: new ProgramElementName("jvmArrayFillNonAtomic"));
0246: public static final ProgramSVSort JCARRAYCOMPARE = new SpecificMethodNameSort(
0247: new ProgramElementName("jvmArrayCompare"));
0248:
0249: public static final ProgramSVSort JCMAKESHORT = new SpecificMethodNameSort(
0250: new ProgramElementName("jvmMakeShort"));
0251: public static final ProgramSVSort JCSETSHORT = new SpecificMethodNameSort(
0252: new ProgramElementName("jvmSetShort"));
0253:
0254: public static final ProgramSVSort JCISTRANSIENT = new SpecificMethodNameSort(
0255: new ProgramElementName("jvmIsTransient"));
0256: public static final ProgramSVSort JCBEGINTRANSACTION = new SpecificMethodNameSort(
0257: new ProgramElementName("jvmBeginTransaction"));
0258: public static final ProgramSVSort JCCOMMITTRANSACTION = new SpecificMethodNameSort(
0259: new ProgramElementName("jvmCommitTransaction"));
0260: public static final ProgramSVSort JCABORTTRANSACTION = new SpecificMethodNameSort(
0261: new ProgramElementName("jvmAbortTransaction"));
0262: public static final ProgramSVSort JCSUSPENDTRANSACTION = new SpecificMethodNameSort(
0263: new ProgramElementName("jvmSuspendTransaction"));
0264: public static final ProgramSVSort JCRESUMETRANSACTION = new SpecificMethodNameSort(
0265: new ProgramElementName("jvmResumeTransaction"));
0266:
0267: public static final ProgramSVSort ALLOCATE = new SpecificMethodNameSort(
0268: new ProgramElementName(
0269: InstanceAllocationMethodBuilder.IMPLICIT_INSTANCE_ALLOCATE));
0270:
0271: public static final ProgramSVSort SEP //TODO
0272: = new SpecificMethodNameSort(new ProgramElementName("sep"));
0273:
0274: public static final ProgramSVSort DEBUGGERTYPEREF = new DebuggerTypeReferenceSort();
0275:
0276: //---------------REFERENCE SORTS ------------------------
0277: public static final ProgramSVSort EXECUTIONCONTEXT = new ExecutionContextSort();
0278:
0279: //---------------UNNECESSARY ONES------------------------
0280:
0281: //--------------------------------------------------------------------------
0282:
0283: public ProgramSVSort(Name name) {
0284: super (name);
0285: name2sort.put(name, this );
0286: }
0287:
0288: public boolean canStandFor(Term t) {
0289: return true;
0290: }
0291:
0292: public boolean canStandFor(ProgramElement check,
0293: ExecutionContext ec, Services services) {
0294: return canStandFor(check, services);
0295: }
0296:
0297: protected abstract boolean canStandFor(ProgramElement check,
0298: Services services);
0299:
0300: //-------------Now the inner classes representing the-----------------------
0301: //-------------different kinds of program SVs-------------------------------
0302:
0303: /**
0304: * This sort represents a type of program schema variables that match
0305: * only on <ul> <li>program variables or <li>static field references with
0306: * a prefix that consists of <ul> <li>a program variable followed by a
0307: * sequence of attribute accesses or <li>of a type reference followed by
0308: * a sequence of attribute accesses</ul></ul>
0309: */
0310: private static class LeftHandSideSort extends ProgramSVSort {
0311:
0312: public LeftHandSideSort() {
0313: super (new Name("LeftHandSide"));
0314: }
0315:
0316: public LeftHandSideSort(Name name) {
0317: super (name);
0318: }
0319:
0320: public boolean canStandFor(Term t) {
0321: if (t.op() instanceof ProgramVariable) {
0322: return true;
0323: }
0324: return false;
0325: }
0326:
0327: protected boolean canStandFor(ProgramElement pe,
0328: Services services) {
0329:
0330: if (pe instanceof ProgramVariable
0331: || pe instanceof VariableSpecification) {
0332: return true;
0333: }
0334:
0335: if (pe instanceof FieldReference) {
0336: FieldReference fr = (FieldReference) pe;
0337: // we allow only static field references with a
0338: // sequence of PVs or TypeRef
0339: ReferencePrefix rp = fr.getReferencePrefix();
0340: if ((fr.getProgramVariable()).isStatic()) {
0341: return (rp == null || rp instanceof ThisReference
0342: || rp instanceof TypeReference || canStandFor(
0343: rp, services));
0344: } else if (rp == null || //AR was in SimpleEx
0345: rp instanceof ThisReference) {
0346: return canStandFor(fr.getProgramVariable(),
0347: services);
0348: }
0349: }
0350:
0351: if (pe instanceof PassiveExpression) {
0352: return canStandFor(((NonTerminalProgramElement) pe)
0353: .getChildAt(0), services);
0354: }
0355:
0356: return false;
0357: }
0358: }
0359:
0360: /**
0361: * This sort represents a type of program schema variables that match
0362: * only on <ul> <li>program variables or <li>static field references with
0363: * a prefix that consists of <ul> <li>a program variable followed by a
0364: * sequence of attribute accesses or <li>of a type reference followed by
0365: * a sequence of attribute accesses</ul></ul>. In opposite to its
0366: * super class it matches only if the field reference does not
0367: * trigger static initialisation (i.e. if it is no active reference)
0368: */
0369: private static class ProgramVariableSort extends LeftHandSideSort {
0370:
0371: public ProgramVariableSort() {
0372: super (new Name("Variable"));
0373: }
0374:
0375: ProgramVariableSort(Name name) {
0376: super (name);
0377: }
0378:
0379: public boolean canStandFor(Term t) {
0380: return t.op() instanceof ProgramVariable;
0381: }
0382:
0383: protected boolean canStandFor(ProgramElement pe,
0384: Services services) {
0385:
0386: ProgramVariable accessedField = null;
0387: if (pe instanceof FieldReference) {
0388: accessedField = ((FieldReference) pe)
0389: .getProgramVariable();
0390: } else if (pe instanceof ProgramVariable) {
0391: accessedField = (ProgramVariable) pe;
0392: } else if (pe instanceof PassiveExpression) {
0393: return super .canStandFor(((PassiveExpression) pe)
0394: .getChildAt(0), services);
0395: }
0396:
0397: if (accessedField != null && accessedField.isStatic()
0398: && !(accessedField instanceof ProgramConstant)) {
0399: return false;
0400: }
0401:
0402: return super .canStandFor(pe, services);
0403: }
0404:
0405: }
0406:
0407: private static class StaticVariableSort extends LeftHandSideSort {
0408:
0409: public StaticVariableSort() {
0410: super (new Name("StaticVariable"));
0411: }
0412:
0413: public boolean canStandFor(Term t) {
0414: return t.op() instanceof ProgramVariable
0415: && ((ProgramVariable) t.op()).isStatic();
0416: }
0417:
0418: protected boolean canStandFor(ProgramElement pe,
0419: Services services) {
0420:
0421: ProgramVariable accessedField = null;
0422: if (pe instanceof FieldReference) {
0423: accessedField = ((FieldReference) pe)
0424: .getProgramVariable();
0425: } else if (pe instanceof ProgramVariable) {
0426: accessedField = (ProgramVariable) pe;
0427: }
0428: if (accessedField != null) {
0429: return accessedField.isStatic()
0430: && !(accessedField instanceof ProgramConstant)
0431: && super .canStandFor(pe, services);
0432: }
0433: return false;
0434: }
0435:
0436: }
0437:
0438: /**
0439: * This sort represents a type of program schema variables that match
0440: * only on <ul> <li>program variables or <li>static field references with
0441: * a prefix that consists of <ul> <li>a program variable followed by a
0442: * sequence of attribute accesses or <li>of a type reference followed by
0443: * a sequence of attribute accesses</ul> <li> (negated) literal
0444: * expressions or <li> instanceof expressions v instanceof T with an
0445: * expression v that matches on a program variable SV </ul>
0446: */
0447: private static class SimpleExpressionSort extends ProgramSVSort {
0448:
0449: public SimpleExpressionSort() {
0450: super (new Name("SimpleExpression"));
0451: }
0452:
0453: protected SimpleExpressionSort(Name n) {
0454: super (n);
0455: }
0456:
0457: public boolean canStandFor(Term t) {
0458: return true;
0459: }
0460:
0461: protected boolean canStandFor(ProgramElement pe,
0462: Services services) {
0463: if (pe instanceof Negative) {
0464: return ((Negative) pe).getChildAt(0) instanceof Literal;
0465: }
0466:
0467: if (pe instanceof Literal) {
0468: return true;
0469: }
0470: if (pe instanceof Instanceof) {
0471: ProgramElement v = ((Instanceof) pe).getChildAt(0);
0472: return (v instanceof ThisReference)
0473: || VARIABLE.canStandFor(v, services);
0474: }
0475:
0476: if (pe instanceof ThisReference) {
0477: return true;
0478: }
0479:
0480: return VARIABLE.canStandFor(pe, services);
0481: }
0482: }
0483:
0484: /**
0485: * This sort represents a type of program schema variables that match
0486: * only on all expressions which are not matched by simple expression
0487: * SVs.
0488: */
0489: private static class NonSimpleExpressionSort extends ProgramSVSort {
0490:
0491: public NonSimpleExpressionSort() {
0492: super (new Name("NonSimpleExpression"));
0493: }
0494:
0495: protected NonSimpleExpressionSort(Name n) {
0496: super (n);
0497: }
0498:
0499: protected boolean canStandFor(ProgramElement check,
0500: Services services) {
0501: if (!(check instanceof Expression)
0502: || check instanceof SuperReference) {
0503: return false;
0504: }
0505: if (check instanceof FieldReference
0506: && ((FieldReference) check)
0507: .referencesOwnInstanceField()) {
0508: return false;
0509: }
0510: return !SIMPLEEXPRESSION.canStandFor(check, services);
0511: }
0512: }
0513:
0514: /**
0515: * This sort represents a type of program schema variables that match on
0516: * all expressions only.
0517: */
0518: private static class ExpressionSort extends ProgramSVSort {
0519:
0520: public ExpressionSort() {
0521: super (new Name("Expression"));
0522: }
0523:
0524: protected ExpressionSort(Name n) {
0525: super (n);
0526: }
0527:
0528: protected boolean canStandFor(ProgramElement pe,
0529: Services services) {
0530: return (pe instanceof Expression);
0531: }
0532:
0533: }
0534:
0535: /**
0536: * This sort represents a type of program schema variables that match
0537: * only on literals
0538: */
0539: private static class LiteralSort extends ProgramSVSort {
0540:
0541: public LiteralSort() {
0542: super (new Name("Literal"));
0543: }
0544:
0545: protected LiteralSort(Name n) {
0546: super (n);
0547: }
0548:
0549: // not designed to match on terms
0550: public boolean canStandFor(Term t) {
0551: return false;
0552: }
0553:
0554: protected boolean canStandFor(ProgramElement pe,
0555: Services services) {
0556: return (pe instanceof Literal);
0557: }
0558: }
0559:
0560: //----------- Initialisation and Creation expressions -------------------
0561:
0562: /**
0563: * This sort represents a type of program schema variables that match
0564: * only on Class Instance Creation Expressions, new C()
0565: */
0566: private static class NewSVSort extends ProgramSVSort {
0567:
0568: public NewSVSort() {
0569: super (new Name("InstanceCreation"));
0570: }
0571:
0572: protected boolean canStandFor(ProgramElement check,
0573: Services services) {
0574: return (check instanceof New);
0575: }
0576: }
0577:
0578: /**
0579: * This sort represents a type of program schema variables that match
0580: * only on Array Creation Expressions, new A[]
0581: */
0582: private static class NewArraySVSort extends ProgramSVSort {
0583: public NewArraySVSort() {
0584: super (new Name("ArrayCreation"));
0585: }
0586:
0587: protected boolean canStandFor(ProgramElement check,
0588: Services services) {
0589: return (check instanceof NewArray);
0590: }
0591: }
0592:
0593: /**
0594: * This sort represents a type of program schema variables that
0595: * match only on Array Initializers.
0596: */
0597: private static class ArrayInitializerSVSort extends ProgramSVSort {
0598:
0599: public ArrayInitializerSVSort() {
0600: super (new Name("ArrayInitializer"));
0601: }
0602:
0603: protected boolean canStandFor(ProgramElement check,
0604: Services services) {
0605: return (check instanceof ArrayInitializer);
0606: }
0607: }
0608:
0609: /**
0610: * This sort represents a type of program schema variables that
0611: * match only on Special Constructor References.
0612: */
0613: private static class SpecialConstructorReferenceSort extends
0614: ProgramSVSort {
0615:
0616: public SpecialConstructorReferenceSort() {
0617: super (new Name("SpecialConstructorReference"));
0618: }
0619:
0620: protected boolean canStandFor(ProgramElement pe,
0621: Services services) {
0622: return (pe instanceof SpecialConstructorReference);
0623: }
0624:
0625: public boolean canStandFor(Term t) {
0626: return (t.op() instanceof ProgramMethod && !((ProgramMethod) t
0627: .op()).isModel());
0628: }
0629: }
0630:
0631: //----------- Types of Statement Program SVs -----------------------------
0632:
0633: /**
0634: * This sort represents a type of program schema variables that
0635: * match only on statements
0636: */
0637: private static class StatementSort extends ProgramSVSort {
0638:
0639: public StatementSort() {
0640: super (new Name("Statement"));
0641: }
0642:
0643: protected boolean canStandFor(ProgramElement pe,
0644: Services services) {
0645: return (pe instanceof Statement);
0646: }
0647:
0648: }
0649:
0650: /**
0651: * This sort represents a type of program schema variables that
0652: * match only on catch branches of try-catch-finally blocks
0653: */
0654: private static class CatchSort extends ProgramSVSort {
0655:
0656: public CatchSort() {
0657: super (new Name("Catch"));
0658: }
0659:
0660: protected boolean canStandFor(ProgramElement pe,
0661: Services services) {
0662: return (pe instanceof Catch);
0663: }
0664: }
0665:
0666: /**
0667: * This sort represents a type of program schema variables that
0668: * match only on method body statements
0669: */
0670: private static class MethodBodySort extends ProgramSVSort {
0671:
0672: public MethodBodySort() {
0673: super (new Name("MethodBody"));
0674: }
0675:
0676: protected boolean canStandFor(ProgramElement check,
0677: Services services) {
0678: return (check instanceof MethodBodyStatement);
0679: }
0680: }
0681:
0682: /**
0683: * This sort represents a type of program schema variables that
0684: * match only on method body statements for nonmodel methods for which
0685: * an implementation is present.
0686: */
0687: private static class NonModelMethodBodySort extends ProgramSVSort {
0688:
0689: public NonModelMethodBodySort() {
0690: super (new Name("NonModelMethodBody"));
0691: }
0692:
0693: protected boolean canStandFor(ProgramElement pe,
0694: Services services) {
0695: if (!(pe instanceof MethodBodyStatement)) {
0696: return false;
0697: }
0698:
0699: final ProgramMethod pm = ((MethodBodyStatement) pe)
0700: .getProgramMethod(services);
0701: final MethodDeclaration methodDeclaration = pm
0702: .getMethodDeclaration();
0703:
0704: return !(pm.isModel() || methodDeclaration.getBody() == null)
0705: || (methodDeclaration instanceof ConstructorDeclaration);
0706: }
0707:
0708: }
0709:
0710: /**
0711: * This sort represents a type of program schema variables that
0712: * match on a method call with SIMPLE PREFIX and AT LEAST a
0713: * NONSIMPLE expression in the ARGUMENTS.
0714: */
0715: private static class NonSimpleMethodReferenceSort extends
0716: ProgramSVSort {
0717:
0718: public NonSimpleMethodReferenceSort() {
0719: super (new Name("NonSimpleMethodReference"));
0720: }
0721:
0722: protected boolean canStandFor(ProgramElement pe,
0723: Services services) {
0724: if (pe instanceof MethodReference) {
0725: MethodReference mr = (MethodReference) pe;
0726: Name localname = mr.getProgramElementName();
0727: if (excludedMethodName(localname))
0728: return false;
0729: if (mr.getReferencePrefix() instanceof SuperReference
0730: || mr.getReferencePrefix() instanceof TypeReference) {
0731: return false;
0732: }
0733: if (mr.getReferencePrefix() != null
0734: && NONSIMPLEEXPRESSION.canStandFor(mr
0735: .getReferencePrefix(), services)) {
0736: return false;
0737: }
0738: if (mr.getArguments() == null) {
0739: return false;
0740: }
0741: for (int i = 0; i < mr.getArguments().size(); i++) {
0742: if (NONSIMPLEEXPRESSION.canStandFor(mr
0743: .getArgumentAt(i), services)) {
0744: return true;
0745: }
0746: }
0747: }
0748: return false;
0749: }
0750:
0751: public boolean canStandFor(Term t) {
0752: return (t.op() instanceof ProgramMethod);
0753: }
0754: }
0755:
0756: //-----------Types--------------------------------------------------------
0757:
0758: /**
0759: * This sort represents a type of program schema variables that
0760: * match only on type references.
0761: */
0762: private static class TypeReferenceSort extends ProgramSVSort {
0763:
0764: public TypeReferenceSort() {
0765: super (new Name("Type"));
0766: }
0767:
0768: protected boolean canStandFor(ProgramElement check,
0769: Services services) {
0770: return (check instanceof TypeReference);
0771: }
0772: }
0773:
0774: /**
0775: * This sort represents a type of program schema variables that
0776: * match only on type references.
0777: */
0778: private static class DebuggerTypeReferenceSort extends
0779: ProgramSVSort {
0780:
0781: public DebuggerTypeReferenceSort() {
0782: super (new Name("DebuggerType"));
0783: }
0784:
0785: protected boolean canStandFor(ProgramElement check,
0786: Services services) {
0787: if (check instanceof TypeReference) {
0788: TypeReference tr = (TypeReference) check;
0789: System.out.println(tr.getReferencePrefix());
0790:
0791: }
0792: return false;
0793: }
0794: }
0795:
0796: /**
0797: * This sort represents a type of program schema variables that
0798: * match anything except byte, char, short, int, and long.
0799: */
0800: private static class TypeReferenceNotPrimitiveSort extends
0801: ProgramSVSort {
0802:
0803: public TypeReferenceNotPrimitiveSort() {
0804: super (new Name("NonPrimitiveType"));
0805: }
0806:
0807: protected boolean canStandFor(ProgramElement check,
0808: Services services) {
0809: if (!(check instanceof TypeReference))
0810: return false;
0811: return !(((TypeReference) (check)).getKeYJavaType()
0812: .getJavaType() instanceof PrimitiveType);
0813:
0814: }
0815: }
0816:
0817: //-----------Names--------------------------------------------------------
0818:
0819: /**
0820: * This sort represents a type of program schema variables that match
0821: * on names of method references, i.e. the "m" of o.m(p1,pn).
0822: */
0823: private static class MethodNameSort extends ProgramSVSort {
0824:
0825: public MethodNameSort() {
0826: super (new Name("MethodName"));
0827: }
0828:
0829: protected MethodNameSort(Name n) {
0830: super (n);
0831: }
0832:
0833: protected boolean canStandFor(ProgramElement pe,
0834: Services services) {
0835: if (pe instanceof MethodName) {
0836: Name localname = (ProgramElementName) pe;
0837: return (!excludedMethodName(localname));
0838: }
0839: return false;
0840: }
0841:
0842: }
0843:
0844: /**
0845: * allows to match on a specific method name
0846: */
0847: private static class SpecificMethodNameSort extends MethodNameSort {
0848:
0849: private ProgramElementName methodName;
0850:
0851: public SpecificMethodNameSort(Name sortName,
0852: ProgramElementName methodName) {
0853: super (sortName);
0854: this .methodName = methodName;
0855: }
0856:
0857: public SpecificMethodNameSort(ProgramElementName name) {
0858: super (name);
0859: this .methodName = name;
0860: }
0861:
0862: protected boolean canStandFor(ProgramElement pe,
0863: Services services) {
0864: if (pe instanceof MethodName) {
0865: return pe.equals(methodName);
0866: }
0867: return false;
0868: }
0869:
0870: }
0871:
0872: /**
0873: * This sort represents a type of program schema variables that match
0874: * on labels.
0875: */
0876: private static class LabelSort extends ProgramSVSort {
0877:
0878: public LabelSort() {
0879: super (new Name("Label"));
0880: }
0881:
0882: protected boolean canStandFor(ProgramElement pe,
0883: Services services) {
0884: return (pe instanceof Label);
0885: }
0886:
0887: }
0888:
0889: /**
0890: * This sort represents a type of program schema variables that match
0891: * on string literals and string variables.
0892: */
0893: public static class SimpleExpressionStringSort extends
0894: SimpleExpressionSort {
0895:
0896: public SimpleExpressionStringSort(String name) {
0897: super (new Name(name));
0898: }
0899:
0900: public boolean canStandFor(ProgramElement check,
0901: ExecutionContext ec, Services services) {
0902: if (!super .canStandFor(check, ec, services)) {
0903: return false;
0904: }
0905: if (check instanceof StringLiteral)
0906: return true;
0907: if (check instanceof ProgramVariable) {
0908: Namespace ns = services.getNamespaces().sorts();
0909: Sort stringSort = (Sort) ns.lookup(new Name(
0910: "java.lang.String"));
0911: return ((ProgramVariable) check).getKeYJavaType()
0912: .getSort().equals(stringSort);
0913: }
0914: return false;
0915: }
0916: }
0917:
0918: //-----------Specials for primitive types---------------------------------
0919:
0920: /**
0921: * This sort represents a type of program schema variables that match
0922: * on simple expressions which have a special primitive type.
0923: */
0924: private static class SimpleExpressionSpecialPrimitiveTypeSort
0925: extends SimpleExpressionSort {
0926:
0927: private final PrimitiveType[] allowed_types;
0928:
0929: public SimpleExpressionSpecialPrimitiveTypeSort(String name,
0930: PrimitiveType[] allowed_types) {
0931:
0932: super (new Name(name));
0933: this .allowed_types = allowed_types;
0934: }
0935:
0936: public boolean canStandFor(ProgramElement check,
0937: ExecutionContext ec, Services services) {
0938: if (!super .canStandFor(check, ec, services)) {
0939: return false;
0940: }
0941: final KeYJavaType kjt = getKeYJavaType(check, ec, services);
0942: if (kjt != null) {
0943: final Type type = kjt.getJavaType();
0944: for (int i = 0; i < allowed_types.length; i++) {
0945: if (type == allowed_types[i])
0946: return true;
0947: }
0948: }
0949: return false;
0950: }
0951: }
0952:
0953: /**
0954: * This sort represents a type of program schema variables that match
0955: * on simple expressions which have a special primitive type.
0956: */
0957: private static class ExpressionSpecialPrimitiveTypeSort extends
0958: ExpressionSort {
0959:
0960: private PrimitiveType[] allowed_types;
0961:
0962: public ExpressionSpecialPrimitiveTypeSort(String name,
0963: PrimitiveType[] allowed_types) {
0964:
0965: super (new Name(name));
0966: this .allowed_types = allowed_types;
0967: }
0968:
0969: public boolean canStandFor(ProgramElement check,
0970: ExecutionContext ec, Services services) {
0971: if (!super .canStandFor(check, ec, services)) {
0972: return false;
0973: }
0974:
0975: final KeYJavaType kjt = getKeYJavaType(check, ec, services);
0976: if (kjt != null) {
0977: final Type type = kjt.getJavaType();
0978:
0979: for (int i = 0; i < allowed_types.length; i++) {
0980: if (type == allowed_types[i])
0981: return true;
0982: }
0983: }
0984: return false;
0985: }
0986: }
0987:
0988: //-----------Specials (unnecessary?)--------------------------------------
0989:
0990: private static class LoopInitSort extends ProgramSVSort {
0991:
0992: public LoopInitSort() {
0993: super (new Name("LoopInit"));
0994: }
0995:
0996: protected boolean canStandFor(ProgramElement check,
0997: Services services) {
0998: return (check instanceof LoopInit);
0999: }
1000: }
1001:
1002: private static class GuardSort extends ProgramSVSort {
1003: public GuardSort() {
1004: super (new Name("Guard"));
1005: }
1006:
1007: protected boolean canStandFor(ProgramElement check,
1008: Services services) {
1009: return (check instanceof Guard);
1010: }
1011: }
1012:
1013: private static class ForUpdatesSort extends ProgramSVSort {
1014: public ForUpdatesSort() {
1015: super (new Name("ForUpdates"));
1016: }
1017:
1018: protected boolean canStandFor(ProgramElement check,
1019: Services services) {
1020: return (check instanceof ForUpdates);
1021:
1022: }
1023: }
1024:
1025: private static class SwitchSVSort extends ProgramSVSort {
1026: public SwitchSVSort() {
1027: super (new Name("Switch"));
1028: }
1029:
1030: protected boolean canStandFor(ProgramElement pe,
1031: Services services) {
1032: return (pe instanceof Switch);
1033: }
1034: }
1035:
1036: private static class MultipleVariableDeclarationSort extends
1037: ProgramSVSort {
1038:
1039: public MultipleVariableDeclarationSort() {
1040: super (new Name("MultipleVariableDeclaration"));
1041: }
1042:
1043: protected boolean canStandFor(ProgramElement pe,
1044: Services services) {
1045: if (pe instanceof VariableDeclaration
1046: && ((VariableDeclaration) pe).getVariables().size() > 1)
1047: return true;
1048: return false;
1049: }
1050:
1051: }
1052:
1053: private static class ArrayPostDeclarationSort extends ProgramSVSort {
1054:
1055: public ArrayPostDeclarationSort() {
1056: super (new Name("ArrayPostDeclaration"));
1057: }
1058:
1059: protected boolean canStandFor(ProgramElement pe,
1060: Services services) {
1061: if (pe instanceof VariableDeclaration
1062: && ((VariableDeclaration) pe).getVariables().size() == 1
1063: && ((VariableDeclaration) pe).getVariables()
1064: .getVariableSpecification(0)
1065: .getDimensions() > 0) {
1066: return true;
1067: }
1068:
1069: return false;
1070: }
1071:
1072: }
1073:
1074: //------------------ stuff concerned with explicit and implicit elements----
1075:
1076: private static class ExplicitProgramVariableSort extends
1077: LeftHandSideSort {
1078:
1079: public ExplicitProgramVariableSort() {
1080: super (new Name("ExplicitVariable"));
1081: }
1082:
1083: public boolean canStandFor(Term t) {
1084: return (t.op() instanceof ProgramVariable);
1085: }
1086:
1087: protected boolean canStandFor(ProgramElement pe,
1088: Services services) {
1089: return (super .canStandFor(pe, services) && !implicit(pe));
1090: }
1091: }
1092:
1093: private static class ImplicitProgramVariableSort extends
1094: LeftHandSideSort {
1095:
1096: public ImplicitProgramVariableSort() {
1097: super (new Name("ImplicitVariable"));
1098: }
1099:
1100: public boolean canStandFor(Term t) {
1101: return (t.op() instanceof ProgramVariable && implicit((ProgramVariable) t
1102: .op()));
1103: }
1104:
1105: protected boolean canStandFor(ProgramElement pe,
1106: Services services) {
1107: return super .canStandFor(pe, services) && implicit(pe);
1108: }
1109: }
1110:
1111: private static class ConstantProgramVariableSort extends
1112: ProgramSVSort {
1113:
1114: public ConstantProgramVariableSort() {
1115: super (new Name("ConstantVariable"));
1116: }
1117:
1118: public boolean canStandFor(Term t) {
1119: return t.op() instanceof ProgramConstant;
1120: }
1121:
1122: protected boolean canStandFor(ProgramElement pe,
1123: Services services) {
1124: return false;
1125: }
1126: }
1127:
1128: private abstract static class NameMatchingSort extends
1129: ProgramSVSort {
1130:
1131: protected final String[] matchingNames;
1132:
1133: private final boolean ignorePrivatePrefix;
1134:
1135: public NameMatchingSort(Name name, boolean ignorePrivatePrefix) {
1136: super (name);
1137: this .matchingNames = new String[1];
1138: this .ignorePrivatePrefix = ignorePrivatePrefix;
1139: }
1140:
1141: public NameMatchingSort(Name name, String nameStr,
1142: boolean ignorePrivatePrefix) {
1143: super (name);
1144: this .matchingNames = new String[] { nameStr };
1145: this .ignorePrivatePrefix = ignorePrivatePrefix;
1146: }
1147:
1148: public NameMatchingSort(Name name, String[] nameStrs,
1149: boolean ignorePrivatePrefix) {
1150: super (name);
1151: this .matchingNames = nameStrs;
1152: this .ignorePrivatePrefix = ignorePrivatePrefix;
1153: }
1154:
1155: protected int compareNames(Name name) {
1156: final String toCmp;
1157: if (ignorePrivatePrefix
1158: && name instanceof ProgramElementName) {
1159: toCmp = ((ProgramElementName) name).getProgramName();
1160: for (int i = 0; i < matchingNames.length; i++) {
1161: if (toCmp.equals(matchingNames[i]))
1162: return i;
1163: }
1164: return -1;
1165: } else {
1166: toCmp = name.toString();
1167: for (int i = 0; i < matchingNames.length; i++) {
1168: if (toCmp.equals(matchingNames[i]))
1169: return i;
1170: }
1171: return -1;
1172: }
1173: }
1174:
1175: protected boolean allowed(ProgramElement pe, Services services) {
1176: final Name peName;
1177: if (pe instanceof Named) {
1178: peName = ((Named) pe).name();
1179: } else if (pe instanceof NamedProgramElement) {
1180: peName = ((NamedProgramElement) pe)
1181: .getProgramElementName();
1182: } else {
1183: return false;
1184: }
1185: return (compareNames(peName) >= 0);
1186: }
1187:
1188: public boolean canStandFor(Term t) {
1189: if (t.op() instanceof ProgramInLogic) {
1190: return (compareNames(t.op().name()) >= 0);
1191: }
1192: return false;
1193: }
1194:
1195: protected boolean canStandFor(ProgramElement pe,
1196: Services services) {
1197: return allowed(pe, services);
1198: }
1199:
1200: }
1201:
1202: private static class MethodNameReferenceSort extends
1203: NameMatchingSort {
1204:
1205: private ListOfName reverseSignature = SLListOfName.EMPTY_LIST;
1206: private String fullTypeName;
1207:
1208: public MethodNameReferenceSort(Name name, String methodName,
1209: String declaredInType) {
1210: super (name, methodName, false);
1211: this .fullTypeName = declaredInType;
1212: }
1213:
1214: public MethodNameReferenceSort(Name name, String[] methodNames,
1215: String declaredInType) {
1216: super (name, methodNames, false);
1217: this .fullTypeName = declaredInType;
1218: }
1219:
1220: public MethodNameReferenceSort(Name name, String methodName,
1221: String declaredInType, ListOfName signature) {
1222: this (name, methodName, declaredInType);
1223: this .reverseSignature = reverse(signature);
1224: }
1225:
1226: public MethodNameReferenceSort(Name name, String[] methodNames,
1227: String declaredInType, ListOfName signature) {
1228: this (name, methodNames, declaredInType);
1229: this .reverseSignature = reverse(signature);
1230: }
1231:
1232: private ListOfName reverse(ListOfName names) {
1233: ListOfName result = SLListOfName.EMPTY_LIST;
1234: IteratorOfName it = names.iterator();
1235: while (it.hasNext()) {
1236: result = result.append(it.next());
1237: }
1238: return result;
1239: }
1240:
1241: private ListOfType createSignature(Services services) {
1242: ListOfType result = SLListOfType.EMPTY_LIST;
1243: IteratorOfName ownSig = reverseSignature.iterator();
1244: while (ownSig.hasNext()) {
1245: result = result.prepend(services.getJavaInfo()
1246: .getKeYJavaType("" + ownSig.next()));
1247: }
1248: return result;
1249: }
1250:
1251: public boolean canStandFor(ProgramElement pe,
1252: ExecutionContext ec, Services services) {
1253:
1254: if (pe instanceof MethodReference) {
1255: final MethodReference mr = (MethodReference) pe;
1256: final int cmpRes = compareNames(mr
1257: .getProgramElementName());
1258: if (cmpRes >= 0) {
1259: final KeYJavaType kjt = services.getJavaInfo()
1260: .getKeYJavaType(fullTypeName);
1261: final MethodDeclaration master = services
1262: .getJavaInfo().getProgramMethod(kjt,
1263: matchingNames[cmpRes],
1264: createSignature(services), kjt)
1265: .getMethodDeclaration();
1266: return master == mr.method(services,
1267: mr.determineStaticPrefixType(services, ec),
1268: ec).getMethodDeclaration();
1269: }
1270: }
1271: return false;
1272: }
1273:
1274: public boolean canStandFor(Term t) {
1275: return (t.op() instanceof ProgramMethod && !((ProgramMethod) t
1276: .op()).isModel());
1277: }
1278:
1279: }
1280:
1281: private static class FieldSort extends NameMatchingSort {
1282:
1283: public FieldSort(Name name, boolean ignorePrivatePrefix) {
1284: super (name, ignorePrivatePrefix);
1285: }
1286:
1287: public FieldSort(Name name, String field,
1288: boolean ignorePrivatePrefix) {
1289: super (name, field, ignorePrivatePrefix);
1290: }
1291:
1292: public FieldSort(String field) {
1293: this (new Name("Field"), field, true);
1294: }
1295:
1296: protected boolean allowed(ProgramElement pe, Services services) {
1297: if (pe instanceof ProgramVariable) {
1298: return super .allowed(pe, services);
1299: }
1300: if (pe instanceof ProgramSVProxy) {
1301: return true;
1302: }
1303: return false;
1304: }
1305:
1306: public boolean canStandFor(Term t) {
1307: if (t.op() instanceof ProgramVariable) {
1308: return super .canStandFor(t);
1309: }
1310: return false;
1311: }
1312:
1313: protected boolean canStandFor(ProgramElement pe,
1314: Services services) {
1315: return allowed(pe, services);
1316: }
1317:
1318: }
1319:
1320: private static class ImplicitFieldSort extends FieldSort {
1321:
1322: public ImplicitFieldSort(Name name, boolean ignorePrivatePrefix) {
1323: super (name, ignorePrivatePrefix);
1324: }
1325:
1326: public ImplicitFieldSort(boolean ignorePrivatePrefix) {
1327: this (new Name("ImplicitField"), ignorePrivatePrefix);
1328: }
1329:
1330: public ImplicitFieldSort(String field,
1331: boolean ignorePrivatePrefix) {
1332: super (new Name("ImplicitField"), field, ignorePrivatePrefix);
1333: }
1334:
1335: public ImplicitFieldSort(Name name, String field,
1336: boolean ignorePrivatePrefix) {
1337: super (name, field, ignorePrivatePrefix);
1338: }
1339:
1340: // %%% we should move information from the variable
1341: // specification to the program variable %RB
1342: protected boolean allowed(ProgramElement pe, Services services) {
1343: if (pe instanceof ProgramSVProxy) {
1344: return true;
1345: }
1346: return super .allowed(pe, services)
1347: || (matchingNames[0] == null
1348: && pe instanceof ProgramVariable && implicit(pe));
1349: }
1350:
1351: public boolean canStandFor(Term t) {
1352: boolean result = false;
1353: if (t.op() instanceof ProgramVariable) {
1354: result = allowed((ProgramVariable) t.op(), null);
1355: }
1356: return result;
1357: }
1358:
1359: protected boolean canStandFor(ProgramElement pe,
1360: Services services) {
1361: ProgramElement var = pe;
1362: if (pe instanceof ImplicitFieldSpecification) {
1363: var = ((ImplicitFieldSpecification) pe)
1364: .getProgramVariable();
1365: } else if (pe instanceof FieldReference) {
1366: var = ((FieldReference) pe).getProgramVariable();
1367: }
1368: return allowed(var, services);
1369: }
1370: }
1371:
1372: private static class ImplicitFieldReferenceSort extends
1373: ImplicitFieldSort {
1374:
1375: public ImplicitFieldReferenceSort() {
1376: super (new Name("ImplicitReferenceField"), true);
1377: }
1378:
1379: // %%% we should move information from the variable
1380: // specification to the program variable %RB
1381: // implicit fields are not of array type so we do not check for
1382: // this reference type
1383: protected boolean allowed(ProgramElement pe, Services services) {
1384: return super .allowed(pe, services)
1385: && ((ProgramVariable) pe).getKeYJavaType()
1386: .getJavaType() instanceof ClassType;
1387: }
1388: }
1389:
1390: private static class ArrayLengthSort extends ProgramSVSort {
1391:
1392: public ArrayLengthSort() {
1393: super (new Name("ArrayLength"));
1394: }
1395:
1396: protected boolean canStandFor(ProgramElement check,
1397: Services services) {
1398: if (check instanceof ProgramVariable) {
1399: return check == services.getJavaInfo().getArrayLength();
1400: }
1401: return false;
1402: }
1403:
1404: }
1405:
1406: private static class ExecutionContextSort extends ProgramSVSort {
1407:
1408: public ExecutionContextSort() {
1409: super (new Name("ExecutionContext"));
1410: }
1411:
1412: protected boolean canStandFor(ProgramElement check,
1413: Services services) {
1414: return (check instanceof ExecutionContext);
1415: }
1416: }
1417:
1418: //-------------------helper methods ------------------------------------
1419:
1420: static boolean methodConstrReference(ProgramElement pe) {
1421: return ((pe instanceof MethodReference)
1422: || (pe instanceof ConstructorReference) || (pe instanceof SpecialConstructorReference));
1423: }
1424:
1425: public ProgramElement getSVWithSort(ExtList l, Class alternative) {
1426: Iterator it = l.iterator();
1427: while (it.hasNext()) {
1428: Object o = it.next();
1429: if (o instanceof SortedSchemaVariable
1430: && (((SortedSchemaVariable) o).sort() == this )) {
1431: return (ProgramElement) o;
1432: } else if ((alternative.isInstance(o))
1433: && (!(o instanceof SchemaVariable))) {
1434: return (ProgramElement) o;
1435: }
1436: }
1437: return null;
1438: }
1439:
1440: static KeYJavaType getKeYJavaType(ProgramElement pe,
1441: ExecutionContext ec, Services services) {
1442: return services.getTypeConverter().getKeYJavaType(
1443: (Expression) pe, ec);
1444: }
1445:
1446: static boolean excludedMethodName(Name name) {
1447: if (((MethodNameReferenceSort) JCMAKETRANSIENTARRAY)
1448: .compareNames(name) >= 0)
1449: return true;
1450: return false;
1451: }
1452:
1453: static boolean implicit(ProgramElement pe) {
1454: if (pe instanceof ProgramVariable) {
1455: if (!((ProgramVariable) pe).isMember())
1456: return false;
1457: }
1458:
1459: final String elemname;
1460: if (pe instanceof NamedProgramElement) {
1461: elemname = ((NamedProgramElement) pe)
1462: .getProgramElementName().getProgramName();
1463: } else if (pe instanceof Named) {
1464: final Name n = ((Named) pe).name();
1465: if (n instanceof ProgramElementName) {
1466: elemname = ((ProgramElementName) n).getProgramName();
1467: } else {
1468: elemname = n.toString();
1469: }
1470: } else {
1471: System.err
1472: .println("Please check implicit in ProgramSVSort");
1473: return false;
1474: }
1475: return elemname.charAt(0) == '<';
1476: }
1477:
1478: public static HashMap name2sort() {
1479: return name2sort;
1480: }
1481:
1482: }
|