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: package de.uka.ilkd.key.rule;
0009:
0010: import java.io.*;
0011: import java.util.*;
0012:
0013: import de.uka.ilkd.key.java.*;
0014: import de.uka.ilkd.key.java.expression.Operator;
0015: import de.uka.ilkd.key.java.visitor.ProgramSVCollector;
0016: import de.uka.ilkd.key.logic.JavaBlock;
0017: import de.uka.ilkd.key.logic.Term;
0018: import de.uka.ilkd.key.logic.op.*;
0019: import de.uka.ilkd.key.logic.sort.Sort;
0020: import de.uka.ilkd.key.proof.ProofAggregate;
0021: import de.uka.ilkd.key.proof.init.EnvInput;
0022: import de.uka.ilkd.key.proof.init.InitConfig;
0023: import de.uka.ilkd.key.proof.init.JavaProfile;
0024: import de.uka.ilkd.key.proof.init.KeYFileForTests;
0025: import de.uka.ilkd.key.proof.init.ProblemInitializer;
0026: import de.uka.ilkd.key.proof.init.ProofOblInput;
0027: import de.uka.ilkd.key.util.KeYResourceManager;
0028:
0029: /**
0030: Automated use to prove sets of taclets
0031:
0032: To actually use all this on a set of taclets you have to do the
0033: following: Put the taclets you are interested in into a
0034: ``.key'' file, e.g.\ called ``rules.key''. You start the generation of
0035: the Maude input in this case by running ``bin/runJava
0036: de.uka.ilkd.key.rule.CheckPrgTransfSoundness rules.key input.maude''
0037: where the result gets put into the file ``input.maude''. Then you start
0038: Maude with the output written directly to a file, say ``result.txt'' by
0039: running your version of maude, in linux e.g.\ with ``maude-linux >
0040: result.txt''. Then you load the modified Maude Java Semantics which you
0041: can get from my homepage ``i12www.ira.uka.de/~rsasse'' with ``load
0042: java-es-m-modified.maude'' and will get some warnings printed on the
0043: monitor which you can safely ignore. When those are complete you load
0044: the input by typing ``load input.maude'' and then wait for around a
0045: minute to be on the safe side, or take a look at whether the processor
0046: is working, if not it is probably done. Then end Maude by typing ``q''.
0047:
0048: */
0049:
0050: public class CheckPrgTransfSoundness {
0051:
0052: private static final JavaProfile JAVA_PROFILE = new JavaProfile();
0053:
0054: // These two counters are basically used to give every case of every
0055: // taclet a unique identification by the combination of the two
0056: // integers.
0057: private static int caseCounter = 0;
0058: private static int tacletCounter = 0;
0059:
0060: // This variable contains the then-current taclet at all points in
0061: // the code when such a taclet exists.
0062: private static Taclet currentTaclet = null;
0063:
0064: // This variable contains the list of new variables, when
0065: // applicable, depending on each taclet.
0066: private static ListOfNewVarcond newvars = null;
0067:
0068: // This is a Map from SchemaVariables to Restrictions.
0069: private static Map svToRestriction = new HashMap();
0070:
0071: // Constant representing the case with no restriction.
0072: private static Restriction RESTRICTNONE = new RestrictionNone();
0073:
0074: // Three strings which are later on put into the Maude
0075: // configuration.
0076: private static String findString;
0077: private static String replaceWithString;
0078: private static String addNewString;
0079:
0080: // These strings are here to distinguish the cases for each
0081: // SchemaVariable, they are necessary to create the fitting string
0082: // for the Maude configuration generation.
0083: private static final String ATTRIBVAL = new String(
0084: "Attribute, value.");
0085: private static final String ATTRIBINT = new String(
0086: "Attribute, integer.");
0087: private static final String ATTRIBBOOL = new String(
0088: "Attribute, boolean.");
0089: private static final String LOCALVARVAL = new String(
0090: "Local Variable, value.");
0091: private static final String LOCALVARINT = new String(
0092: "Local Variable, integer.");
0093: private static final String LOCALVARBOOL = new String(
0094: "Local Variable, boolean.");
0095: private static final String LOCALVARATT = new String(
0096: "Local Variable, object with attribute.");
0097: private static final String ATTOBJWOTHISVAL = new String(
0098: "Attribute of the current object without this, value.");
0099: private static final String ATTOBJWOTHISINT = new String(
0100: "Attribute of the current object without this, integer.");
0101: private static final String ATTOBJWOTHISBOOL = new String(
0102: "Attribute of the current object without this, boolean.");
0103: private static final String ATTOBJWOTHISATT = new String(
0104: "Attribute of the current object without this, "
0105: + "object with attribute.");
0106: private static final String ATTOBJWITHTHISVAL = new String(
0107: "Attribute of the current object with this, value.");
0108: private static final String ATTOBJWITHTHISINT = new String(
0109: "Attribute of the current object with this, integer.");
0110: private static final String ATTOBJWITHTHISBOOL = new String(
0111: "Attribute of the current object with this, boolean.");
0112: private static final String ATTOBJWITHTHISATT = new String(
0113: "Attribute of the current object with this, "
0114: + "object with attribute.");
0115: private static final String STATATTTYPEREFVAL = new String(
0116: "Static attribute with a type reference first, value.");
0117: private static final String STATATTTYPEREFINT = new String(
0118: "Static attribute with a type reference first, integer.");
0119: private static final String STATATTTYPEREFBOOL = new String(
0120: "Static attribute with a type reference first, boolean.");
0121: private static final String STATATTTYPEREFATT = new String(
0122: "Static attribute with a type reference first, "
0123: + "object with attribute.");
0124: private static final String STATATTOBJREFVAL = new String(
0125: "Static attribute with a program variable, "
0126: + "in this case an object reference, first. Value.");
0127: private static final String STATATTOBJREFINT = new String(
0128: "Static attribute with a program variable, "
0129: + "in this case an object reference, first. Integer.");
0130: private static final String STATATTOBJREFBOOL = new String(
0131: "Static attribute with a program variable, "
0132: + "in this case an object reference, first. Boolean.");
0133: private static final String STATATTOBJREFATT = new String(
0134: "Static attribute with a program variable, "
0135: + "in this case an object reference, first. "
0136: + "Object with attribute.");
0137: private static final String LITERALINT = new String(
0138: "Generic integer literal.");
0139: private static final String LITERALVALUE = new String(
0140: "Generic value literal.");
0141: private static final String LITERALBOOL = new String(
0142: "Generic boolean literal.");
0143:
0144: private static final String EXPRESSIONVAL = new String(
0145: "Expression with VALUE return");
0146: private static final String EXPRESSIONINT = new String(
0147: "Expression with INTEGER return");
0148: private static final String EXPRESSIONBOOL = new String(
0149: "Expression with BOOLEAN return");
0150: private static final String EXPRESSIONATT = new String(
0151: "Expression with an object with attribute return");
0152:
0153: private static String[] ruleFiles = new String[] {
0154: "../proof/rules/ruleSetsDeclarations.key",
0155: "../proof/rules/javaRules.key" };
0156:
0157: // Used to write the strings out into a file.
0158: private static FileWriter fW;
0159:
0160: private CheckPrgTransfSoundness() {
0161: }
0162:
0163: // This method parses the file which includes all taclets. It
0164: // creates a "SetOfTaclet" set which includes the taclets.
0165: public static SetOfTaclet parseTaclets() {
0166:
0167: Set checkTacsName = new HashSet();
0168:
0169: try {
0170: BufferedReader r = new BufferedReader(
0171: new FileReader(
0172: KeYResourceManager
0173: .getManager()
0174: .getResourceFile(
0175: CheckPrgTransfSoundness.class,
0176: "../proof/rules/checkTacletsWithMaudeList.txt")
0177: .getFile()));
0178: for (String jl = r.readLine(); (jl != null); jl = r
0179: .readLine()) {
0180: if ((jl.length() == 0) || (jl.charAt(0) == '#')) {
0181: continue;
0182: }
0183: // add the "jl" string to the set of names of
0184: // the taclets which are to be checked
0185: checkTacsName.add(jl);
0186: }
0187: }
0188: // catch all exceptions
0189: catch (Exception e) {
0190: System.err
0191: .println("Exception occurred while parsing "
0192: + "../system/resources/de/uka/ilkd/key/proof/rules/checkTacletsWithMaudeList.txt"
0193: + "\n");
0194: e.printStackTrace();
0195: System.exit(-1);
0196: return null;
0197: }
0198:
0199: SetOfTaclet rules = SetAsListOfTaclet.EMPTY_SET;
0200: File allTacletsFile = null;
0201: try {
0202: allTacletsFile = File.createTempFile("allTaclets", "tmp");
0203: PrintWriter out = new PrintWriter(new BufferedWriter(
0204: new FileWriter(allTacletsFile)));
0205: for (int i = 0; i < ruleFiles.length; i++) {
0206: //File f = new File(ruleFiles[i]);
0207: File f = new File(KeYResourceManager.getManager()
0208: .getResourceFile(CheckPrgTransfSoundness.class,
0209: ruleFiles[i]).getFile());
0210: BufferedReader r = new BufferedReader(new FileReader(f));
0211: for (String jl = r.readLine(); (jl != null); jl = r
0212: .readLine()) {
0213: if (!jl.startsWith("\\include"))
0214: out.println(jl);
0215: }
0216: }
0217: out.close();
0218:
0219: // KeYResourceManager.getManager().getResourceFile
0220: // (CheckPrgTransfSoundness.class, ruleFiles[i])
0221: EnvInput envInput = new KeYFileForTests("Test",
0222: allTacletsFile);
0223: ProblemInitializer pi = new ProblemInitializer(JAVA_PROFILE);
0224: InitConfig ic = pi.prepare(envInput);
0225: SetOfTaclet currentRules = ic.getTaclets();
0226: //filtern von currentRules mit obigen checkTacsName, treffer in rules hinzuf�gen
0227: // schleife �ber alle elemente von currentRules
0228:
0229: IteratorOfTaclet currentRulesIt = currentRules.iterator();
0230: while (currentRulesIt.hasNext()) {
0231: Taclet cT = (Taclet) currentRulesIt.next();
0232:
0233: Iterator checkTacsNameIt = checkTacsName.iterator();
0234: while (checkTacsNameIt.hasNext()) {
0235: String tacName = (String) checkTacsNameIt.next();
0236: if (cT.name().toString().equals(tacName)) {
0237: rules = rules.add(cT);
0238: }
0239: }
0240: }
0241: } catch (Exception e) {
0242: System.err.println("Exception occured while parsing "
0243: + allTacletsFile + "\n");
0244: e.printStackTrace();
0245: System.exit(-1);
0246: return null;
0247: }
0248:
0249: return rules;
0250:
0251: }
0252:
0253: // This method iterates over all the taclets created by the parsing
0254: // process and feeds them to the "processTaclet" method.
0255: public static void processAllTaclets(SetOfTaclet taclets) {
0256: IteratorOfTaclet tacletIt = taclets.iterator();
0257: int i = 1;
0258: while (tacletIt.hasNext()) {
0259: Taclet tac = tacletIt.next();
0260: System.out.println(i + ". Taclet: " + tac.name());
0261: i++;
0262: processTaclet(tac);
0263: System.out.println();
0264: }
0265: }
0266:
0267: // This processes a taclet by using a lot of helper functions.
0268: public static void processTaclet(Taclet taclet) {
0269: // This first increases the counter for the tacletnumber and also
0270: // sets the case number back to 1, as this is another taclet to
0271: // be processed.
0272: currentTaclet = taclet;
0273: tacletCounter = tacletCounter + 1;
0274: caseCounter = 1;
0275:
0276: // This creates 2 new lines in the output file to separate this
0277: // taclet from the one before.
0278: try {
0279: fW.write("\n\n");
0280: } catch (Exception e) {
0281: System.err.println("Exception occured "
0282: + "while writing to " + fW + "\n");
0283: e.printStackTrace();
0284: System.exit(-1);
0285: return;
0286: }
0287:
0288: // Extract all parts from the taclet and put them here:
0289: Term findTerm = null;
0290: Term replaceWithTerm = null;
0291: newvars = null;
0292:
0293: // Intermediate variable.
0294: ListOfTacletGoalTemplate listTgt = taclet.goalTemplates();
0295:
0296: if (taclet instanceof RewriteTaclet && listTgt.size() == 1) {
0297: findTerm = ((RewriteTaclet) taclet).find();
0298: replaceWithTerm = ((RewriteTacletGoalTemplate) listTgt
0299: .head()).replaceWith();
0300: } else {
0301: // Error: taclet has to be rewriteTaclet!
0302: // Error: either no goaltemplate available or more than 1.
0303: System.out.println("ERROR - taclet which is no "
0304: + "RewriteTaclet or has no goalTemplate" + "used: "
0305: + taclet);
0306: }
0307:
0308: // Set of new variable conditions:
0309: newvars = taclet.varsNew();
0310:
0311: // all parts, i.e. find, replacewith and newvarcond have now
0312: // been extracted, use them: first get inside the find part and
0313: // extract the information there by "preProcessFindPart"
0314:
0315: preProcessFindPart(findTerm);
0316:
0317: System.out.println("replacewith: " + replaceWithTerm);
0318:
0319: // Here we have a Map "svToRestriction" which maps all the
0320: // schema vars from "list" to a restriction class. This was
0321: // completed within the "preProcessFindPart". Using that
0322: // information we should now be able to create all the possible
0323: // mappings from sv's to concrete elements for the MJS.
0324:
0325: // Use method "createAllPossibilities" for the purpose of
0326: // creating *all* the possibilities.
0327: Set allSVSet = svToRestriction.keySet();
0328: int svarrsize = allSVSet.size();
0329: Object[] allSVs = allSVSet.toArray();
0330: Map svToMaude = new HashMap();
0331: createAllPossibilities(findTerm, replaceWithTerm, allSVs, 0,
0332: svarrsize, new String(), svToMaude);
0333:
0334: // That is it for this method, return to here does not help.
0335: }
0336:
0337: // This method considers all code in the find part of the taclet and
0338: // checks it for necessary restrictions to the SVs.
0339: public static void preProcessFindPart(Term find) {
0340: System.out.println("find: " + find);
0341:
0342: // Extracts the StatementBlock of the find part.
0343: JavaBlock findJavaBlock = find.javaBlock();
0344: StatementBlock findStatementBlock = (StatementBlock) findJavaBlock
0345: .program();
0346:
0347: findStatementBlock = new StatementBlock(new StatementBlock(
0348: findStatementBlock.getBody()));
0349:
0350: // Collects all SVs in the code of the find part.
0351: ProgramSVCollector PSVC = new ProgramSVCollector(
0352: findStatementBlock, SLListOfSchemaVariable.EMPTY_LIST);
0353: PSVC.start();
0354: ListOfSchemaVariable list = PSVC.getSchemaVariables();
0355:
0356: // Creates a map with all the schema variables mapped to the no
0357: // restriction class.
0358: svToRestriction = new HashMap();
0359: IteratorOfSchemaVariable listIt = list.iterator();
0360: while (listIt.hasNext()) {
0361: svToRestriction.put(listIt.next(), RESTRICTNONE);
0362: }
0363:
0364: // going inside the statements, until terminalProgramElement
0365: // reached, "recurse"ing inside:
0366: for (int countStatements = 0; countStatements < findStatementBlock
0367: .getStatementCount(); countStatements++) {
0368:
0369: Statement findStatement = findStatementBlock
0370: .getStatementAt(countStatements);
0371:
0372: if (findStatement instanceof NonTerminalProgramElement) {
0373: //System.out.println("inside");
0374: recurse((NonTerminalProgramElement) findStatement, "",
0375: RESTRICTNONE);
0376: }
0377:
0378: }
0379:
0380: // done here
0381: }
0382:
0383: // This method goes inside the statement which it is given and
0384: // extracts the restrictions.
0385: public static void recurse(NonTerminalProgramElement findStat,
0386: String indent, Restriction restri) {
0387: for (int countst = 0; countst < findStat.getChildCount(); countst++) {
0388:
0389: ProgramElement findPE = findStat.getChildAt(countst);
0390: if (findPE instanceof NonTerminalProgramElement) {
0391:
0392: // In case of an arithmetic operator the SV has to have
0393: // integer type:
0394: if ((findPE instanceof Operator && TypeConverter
0395: .isArithmeticOperator((Operator) findPE))
0396: || findPE instanceof de.uka.ilkd.key.java.expression.operator.PlusAssignment
0397: || findPE instanceof de.uka.ilkd.key.java.expression.operator.MinusAssignment
0398: || findPE instanceof de.uka.ilkd.key.java.expression.operator.TimesAssignment
0399: || findPE instanceof de.uka.ilkd.key.java.expression.operator.DivideAssignment
0400: || findPE instanceof de.uka.ilkd.key.java.expression.operator.ModuloAssignment
0401: || findPE instanceof de.uka.ilkd.key.java.expression.operator.GreaterOrEquals
0402: || findPE instanceof de.uka.ilkd.key.java.expression.operator.GreaterThan
0403: || findPE instanceof de.uka.ilkd.key.java.expression.operator.LessOrEquals
0404: || findPE instanceof de.uka.ilkd.key.java.expression.operator.LessThan
0405: || findPE instanceof de.uka.ilkd.key.java.expression.operator.Equals
0406: || findPE instanceof de.uka.ilkd.key.java.expression.operator.NotEquals) {
0407: // call recurse with a RestrictionInt, the current
0408: // restriction should be either a RestrictionNone or
0409: // a RestrictionInt, otherwise bad!
0410:
0411: Restriction localRest = new RestrictionInt();
0412:
0413: // Subcase of arithmetic operator where the
0414: // restriction has to be bool, not int.
0415: if (findPE instanceof de.uka.ilkd.key.java.expression.operator.BinaryAnd
0416: || findPE instanceof de.uka.ilkd.key.java.expression.operator.BinaryNot
0417: || findPE instanceof de.uka.ilkd.key.java.expression.operator.BinaryOr
0418: || findPE instanceof de.uka.ilkd.key.java.expression.operator.BinaryXOr) {
0419: localRest = new RestrictionBool();
0420: }
0421:
0422: // Go on with the recursion.
0423: if (((NonTerminalProgramElement) findPE)
0424: .getChildCount() == 0) {
0425: finishRecurse(
0426: (NonTerminalProgramElement) findPE,
0427: indent + " ", localRest);
0428: } else {
0429: recurse((NonTerminalProgramElement) findPE,
0430: indent + " ", localRest);
0431: }
0432: }
0433:
0434: else if (findPE instanceof de.uka.ilkd.key.java.reference.SchematicFieldReference) {
0435: // call recurse (or finish the recursion) with a
0436: // RestrictionAtt which has the second child as
0437: // parameter, i.e. we have "e.a" and "e" gets the
0438: // RestrictionAtt(a) and "a" gets the restriction
0439: // which is there from a higher level of the
0440: // recursion in addition to the restriction of being
0441: // an attribute. For "a" the recursion is finished.
0442:
0443: NonTerminalProgramElement child0 = (NonTerminalProgramElement) ((NonTerminalProgramElement) findPE)
0444: .getChildAt(0);
0445: NonTerminalProgramElement child1 = (NonTerminalProgramElement) ((NonTerminalProgramElement) findPE)
0446: .getChildAt(1);
0447:
0448: if (child0.getChildCount() == 0) {
0449: finishRecurse(child0, indent + " ",
0450: new RestrictionAtt(
0451: ((SchemaVariable) child1)));
0452: } else {
0453: recurse(child0, indent + " ",
0454: new RestrictionAtt(
0455: ((SchemaVariable) child1)));
0456: }
0457:
0458: finishRecurse(child1, indent + " ",
0459: new RestrictionIsAttrib(restri));
0460: } else {
0461: // this is the standard base case when no
0462: // restriction needs to be set due to the current
0463: // operator
0464:
0465: if (((NonTerminalProgramElement) findPE)
0466: .getChildCount() == 0) {
0467: finishRecurse(
0468: (NonTerminalProgramElement) findPE,
0469: indent + " ", restri);
0470: } else {
0471: recurse((NonTerminalProgramElement) findPE,
0472: indent + " ", restri);
0473: }
0474: }
0475: } else {
0476: System.out.println("terminal found: "
0477: + ((NonTerminalProgramElement) findStat)
0478: .getChildAt(countst));
0479: System.out
0480: .println("this should not have happened, all "
0481: + "things we get by accessing "
0482: + "these children are of NTPE type");
0483: }
0484: }
0485: }
0486:
0487: // This method ends the recursion.
0488: public static void finishRecurse(
0489: NonTerminalProgramElement findStat, String indent,
0490: Restriction restri) {
0491: if (findStat instanceof TerminalProgramElement) {
0492:
0493: if (findStat instanceof SchemaVariable) {
0494:
0495: // Here we are at the bottom level, having a single
0496: // schema variable left, we now assign to that sv a
0497: // restriction globally for this taclet. This might be
0498: // overwritten, but that will only happen with another
0499: // copy of itself.
0500:
0501: if (restri instanceof RestrictionNone) {
0502: // No change at the sv to restriction mapping. There
0503: // is no need for a change due to this leaf of the
0504: // parse tree because the current restriction is
0505: // RestrictionNone, but there might be a restriction
0506: // already due to another leaf which can not be
0507: // overwritten just because here this is not
0508: // necessary.
0509: } else {
0510: // We have a restriction on the sv here, just put it
0511: // into the mapping. It could overwrite another one
0512: // already there but as we only consider
0513: // parse-correct taclets this should not bother
0514: // us. Also in the taclets we consider every
0515: // dereferencing that appears will only appear with
0516: // the left-hand side used with the same attribute
0517: // again, so there is no problem with one attribute
0518: // overwriting another.
0519: svToRestriction.put(findStat, restri);
0520: }
0521:
0522: }
0523: }
0524: }
0525:
0526: // This method splits the generation up into all possible parts
0527: // which are induced by the SVs. That happens by repeatedly calling
0528: // itself with ever more parts specified.
0529: public static void createAllPossibilities(Term find,
0530: Term replaceWith, Object[] allSVs, int svarrindex,
0531: int svarrsize, String addString, Map svToMaude) {
0532:
0533: if (svarrindex < svarrsize) {
0534: SchemaVariable sv = (SchemaVariable) allSVs[svarrindex];
0535: svarrindex = svarrindex + 1;
0536: Restriction svRestri = (Restriction) svToRestriction
0537: .get(sv);
0538:
0539: Sort svSort = ((SortedSchemaVariable) sv).sort();
0540:
0541: // Here we find out the type and restrictions for each
0542: // schema variable and accordingly create all subcases. We
0543: // save the current case in the form of a map from SVs to
0544: // the fixed strings from above, like AttribVal,
0545: // AttribInt,...
0546:
0547: // We also generate the "add" part for the Maude
0548: // configuration for each SV, they get collected into the
0549: // "addstring" string.
0550:
0551: // Then the method is called again to fix the cases of the
0552: // remaining SVs.
0553:
0554: // This is the name of the current SV, without the "#" in
0555: // the name as usual in KeY because Maude cannot use it that
0556: // way.
0557: String svName = sv.name().toString().substring(1,
0558: sv.name().toString().length());
0559: // This string is added to the recursive call to this
0560: // method, thus it starts out empty.
0561: String addNow = "";
0562:
0563: // Case distinctions depending on the SV sort and the
0564: // restriction, in each case one (or more!) subcases are
0565: // opened with a recursive call to the current method and
0566: // the case of the current SV is saved in svToMaude and put
0567: // into the string.
0568:
0569: if (svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.VARIABLE
0570: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.LEFTHANDSIDE
0571: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.NONSIMPLEEXPRESSION
0572: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.EXPRESSION) {
0573: if (svRestri instanceof RestrictionIsAttrib) {
0574: Restriction attribsRestri = ((RestrictionIsAttrib) svRestri)
0575: .getAttribsRestriction();
0576: if (attribsRestri instanceof RestrictionNone) {
0577: addNow = createStringMemoryVal(svName);
0578: svToMaude.put(sv, ATTRIBVAL);
0579: } else if (attribsRestri instanceof RestrictionInt) {
0580: addNow = createStringMemoryInt(svName);
0581: svToMaude.put(sv, ATTRIBINT);
0582: } else if (attribsRestri instanceof RestrictionBool) {
0583: addNow = createStringMemoryBool(svName);
0584: svToMaude.put(sv, ATTRIBBOOL);
0585: } else {
0586: // Bad Case, this means that the attribute is
0587: // restricted to have an attribute which cannot
0588: // happen!
0589: System.out
0590: .println("Bad Case! This is an attribute "
0591: + "which can not have another "
0592: + "attribute, but needs one.");
0593: }
0594: createAllPossibilities(find, replaceWith, allSVs,
0595: svarrindex, svarrsize, addString + addNow,
0596: svToMaude);
0597: }
0598: if (svRestri instanceof RestrictionNone) {
0599: // 1. : sv is local variable!
0600: addNow = createStringLocalEnv(svName)
0601: + createStringMemoryVal(svName);
0602: svToMaude.put(sv, LOCALVARVAL);
0603: createAllPossibilities(find, replaceWith, allSVs,
0604: svarrindex, svarrsize, addString + addNow,
0605: svToMaude);
0606:
0607: // 2. : sv is attribute of the current object w/out "this"
0608: // ATTOBJWOTHIS
0609: addNow = createStringCurrObjEnv(svName)
0610: + createStringMemoryVal(svName);
0611: svToMaude.put(sv, ATTOBJWOTHISVAL);
0612: createAllPossibilities(find, replaceWith, allSVs,
0613: svarrindex, svarrsize, addString + addNow,
0614: svToMaude);
0615:
0616: // 3. : sv is attribute of the current object w/ "this"
0617: //ATTOBJWITHTHIS
0618: addNow = createStringCurrObjEnv(svName)
0619: + createStringMemoryVal(svName);
0620: svToMaude.put(sv, ATTOBJWOTHISVAL);
0621: createAllPossibilities(find, replaceWith, allSVs,
0622: svarrindex, svarrsize, addString + addNow,
0623: svToMaude);
0624: } else if (svRestri instanceof RestrictionInt) {
0625:
0626: // 1. : sv is local variable!
0627: addNow = createStringLocalEnv(svName)
0628: + createStringMemoryInt(svName);
0629: svToMaude.put(sv, LOCALVARINT);
0630: createAllPossibilities(find, replaceWith, allSVs,
0631: svarrindex, svarrsize, addString + addNow,
0632: svToMaude);
0633:
0634: // 2. : sv is attribute of the current object w/out "this"
0635: // ATTOBJWOTHIS
0636: addNow = createStringCurrObjEnv(svName)
0637: + createStringMemoryInt(svName);
0638: svToMaude.put(sv, ATTOBJWOTHISINT);
0639: createAllPossibilities(find, replaceWith, allSVs,
0640: svarrindex, svarrsize, addString + addNow,
0641: svToMaude);
0642:
0643: // 3. : sv is attribute of the current object w/ "this"
0644: //ATTOBJWITHTHIS
0645: addNow = createStringCurrObjEnv(svName)
0646: + createStringMemoryInt(svName);
0647: svToMaude.put(sv, ATTOBJWITHTHISINT);
0648: createAllPossibilities(find, replaceWith, allSVs,
0649: svarrindex, svarrsize, addString + addNow,
0650: svToMaude);
0651: } else if (svRestri instanceof RestrictionBool) {
0652:
0653: // 1. : sv is local variable!
0654: addNow = createStringLocalEnv(svName)
0655: + createStringMemoryBool(svName);
0656: svToMaude.put(sv, LOCALVARBOOL);
0657: createAllPossibilities(find, replaceWith, allSVs,
0658: svarrindex, svarrsize, addString + addNow,
0659: svToMaude);
0660:
0661: // 2. : sv is attribute of the current object w/out "this"
0662: // ATTOBJWOTHIS
0663: addNow = createStringCurrObjEnv(svName)
0664: + createStringMemoryBool(svName);
0665: svToMaude.put(sv, ATTOBJWOTHISBOOL);
0666: createAllPossibilities(find, replaceWith, allSVs,
0667: svarrindex, svarrsize, addString + addNow,
0668: svToMaude);
0669:
0670: // 3. : sv is attribute of the current object w/ "this"
0671: //ATTOBJWITHTHIS
0672: addNow = createStringCurrObjEnv(svName)
0673: + createStringMemoryBool(svName);
0674: svToMaude.put(sv, ATTOBJWITHTHISBOOL);
0675: createAllPossibilities(find, replaceWith, allSVs,
0676: svarrindex, svarrsize, addString + addNow,
0677: svToMaude);
0678: } else if (svRestri instanceof RestrictionAtt) {
0679: String svAttName = svRestri.getAttributeVar()
0680: .name().toString().substring(
0681: 1,
0682: svRestri.getAttributeVar().name()
0683: .toString().length());
0684:
0685: // 1. : sv is local variable!
0686: addNow = createStringLocalEnv(svName)
0687: + createStringMemoryObjWAtt(svName,
0688: svAttName);
0689: svToMaude.put(sv, LOCALVARATT);
0690: createAllPossibilities(find, replaceWith, allSVs,
0691: svarrindex, svarrsize, addString + addNow,
0692: svToMaude);
0693:
0694: // 2. : sv is attribute of the current object w/out "this"
0695: // ATTOBJWOTHIS
0696: addNow = createStringCurrObjEnv(svName)
0697: + createStringMemoryObjWAtt(svName,
0698: svAttName);
0699: svToMaude.put(sv, ATTOBJWOTHISATT);
0700: createAllPossibilities(find, replaceWith, allSVs,
0701: svarrindex, svarrsize, addString + addNow,
0702: svToMaude);
0703:
0704: // 3. : sv is attribute of the current object w/ "this"
0705: //ATTOBJWITHTHIS
0706: addNow = createStringCurrObjEnv(svName)
0707: + createStringMemoryObjWAtt(svName,
0708: svAttName);
0709: svToMaude.put(sv, ATTOBJWITHTHISATT);
0710: createAllPossibilities(find, replaceWith, allSVs,
0711: svarrindex, svarrsize, addString + addNow,
0712: svToMaude);
0713: } else if (svRestri instanceof RestrictionIsAttrib) {
0714:
0715: } else {
0716: System.out
0717: .println("Problem, all cases are worked on so "
0718: + "this should not be reachable!");
0719: }
0720: }
0721:
0722: if (svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.STATICVARIABLE
0723: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.LEFTHANDSIDE
0724: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.NONSIMPLEEXPRESSION
0725: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.EXPRESSION) {
0726: if (svRestri instanceof RestrictionNone) {
0727: // 1. : sv is static attribute with STATATTTYPEREF !
0728: // I.e. type reference first
0729: addNow = createStringStaticEnv(svName)
0730: + createStringMemoryVal(svName);
0731: svToMaude.put(sv, STATATTTYPEREFVAL);
0732: createAllPossibilities(find, replaceWith, allSVs,
0733: svarrindex, svarrsize, addString + addNow,
0734: svToMaude);
0735:
0736: // 2. : sv is static attribute with STATATTOBJREF!
0737: // I.e. object reference first
0738: addNow = createStringStaticEnv(svName)
0739: + createStringMemoryVal(svName)
0740: + createStringLocalEnv(svName + "ObjRef")
0741: + createStringMemoryObj(svName);
0742: svToMaude.put(sv, STATATTOBJREFVAL);
0743: createAllPossibilities(find, replaceWith, allSVs,
0744: svarrindex, svarrsize, addString + addNow,
0745: svToMaude);
0746:
0747: } else if (svRestri instanceof RestrictionInt) {
0748:
0749: // 1. : sv is static attribute with STATATTTYPEREF !
0750: // I.e. type reference first
0751: addNow = createStringStaticEnv(svName)
0752: + createStringMemoryInt(svName);
0753: svToMaude.put(sv, STATATTTYPEREFINT);
0754: createAllPossibilities(find, replaceWith, allSVs,
0755: svarrindex, svarrsize, addString + addNow,
0756: svToMaude);
0757: // 2. : sv is static attribute with STATATTOBJREF!
0758: // I.e. object reference first
0759: addNow = createStringStaticEnv(svName)
0760: + createStringMemoryInt(svName)
0761: + createStringLocalEnv(svName + "ObjRef")
0762: + createStringMemoryObj(svName);
0763: svToMaude.put(sv, STATATTOBJREFINT);
0764: createAllPossibilities(find, replaceWith, allSVs,
0765: svarrindex, svarrsize, addString + addNow,
0766: svToMaude);
0767:
0768: } else if (svRestri instanceof RestrictionBool) {
0769:
0770: // 1. : sv is static attribute with STATATTTYPEREF !
0771: // I.e. type reference first
0772: addNow = createStringStaticEnv(svName)
0773: + createStringMemoryBool(svName);
0774: svToMaude.put(sv, STATATTTYPEREFBOOL);
0775: createAllPossibilities(find, replaceWith, allSVs,
0776: svarrindex, svarrsize, addString + addNow,
0777: svToMaude);
0778: // 2. : sv is static attribute with STATATTOBJREF!
0779: // I.e. object reference first
0780: addNow = createStringStaticEnv(svName)
0781: + createStringMemoryBool(svName)
0782: + createStringLocalEnv(svName + "ObjRef")
0783: + createStringMemoryObj(svName);
0784: svToMaude.put(sv, STATATTOBJREFBOOL);
0785: createAllPossibilities(find, replaceWith, allSVs,
0786: svarrindex, svarrsize, addString + addNow,
0787: svToMaude);
0788:
0789: } else if (svRestri instanceof RestrictionAtt) {
0790: String svAttName = svRestri.getAttributeVar()
0791: .name().toString().substring(
0792: 1,
0793: svRestri.getAttributeVar().name()
0794: .toString().length());
0795: // 1. : sv is static attribute with STATATTTYPEREF !
0796: // I.e. type reference first
0797: addNow = createStringStaticEnv(svName)
0798: + createStringMemoryObjWAtt(svName,
0799: svAttName);
0800: svToMaude.put(sv, STATATTTYPEREFATT);
0801: createAllPossibilities(find, replaceWith, allSVs,
0802: svarrindex, svarrsize, addString + addNow,
0803: svToMaude);
0804: // 2. : sv is static attribute with STATATTOBJREF!
0805: // I.e. object reference first
0806: addNow = createStringStaticEnv(svName)
0807: + createStringMemoryObjWAtt(svName,
0808: svAttName)
0809: + createStringLocalEnv(svName + "ObjRef")
0810: + createStringMemoryObj(svName);
0811: svToMaude.put(sv, STATATTOBJREFATT);
0812: createAllPossibilities(find, replaceWith, allSVs,
0813: svarrindex, svarrsize, addString + addNow,
0814: svToMaude);
0815: } else {
0816: System.out
0817: .println("Problem, all cases are worked on so "
0818: + "this should not be reachable!");
0819: }
0820: }
0821:
0822: if (svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.SIMPLEEXPRESSION
0823: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.EXPRESSION) {
0824: // see also above, this shares a case with VARIABLE
0825: if (svRestri instanceof RestrictionNone) {
0826: addNow = "";
0827: svToMaude.put(sv, LITERALVALUE);
0828: createAllPossibilities(find, replaceWith, allSVs,
0829: svarrindex, svarrsize, addString + addNow,
0830: svToMaude);
0831: } else if (svRestri instanceof RestrictionInt) {
0832: addNow = "";
0833: svToMaude.put(sv, LITERALINT);
0834: createAllPossibilities(find, replaceWith, allSVs,
0835: svarrindex, svarrsize, addString + addNow,
0836: svToMaude);
0837: } else if (svRestri instanceof RestrictionBool) {
0838: addNow = "";
0839: svToMaude.put(sv, LITERALBOOL);
0840: createAllPossibilities(find, replaceWith, allSVs,
0841: svarrindex, svarrsize, addString + addNow,
0842: svToMaude);
0843: } else if (svRestri instanceof RestrictionAtt) {
0844: // This case can not happen for variables and
0845: // lefthandsides, therefore nothing is done
0846: // here. For (nonsimple) expressions this case is
0847: // handled further down!
0848:
0849: // It actually can not happen as a literal,
0850: // i.e. there can not be an "object literal" which
0851: // makes this case moot!
0852: } else {
0853: System.out
0854: .println("Problem, all cases are worked on so "
0855: + "this should not be reachable!");
0856: }
0857: }
0858:
0859: if (svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.NONSIMPLEEXPRESSION
0860: || svSort == de.uka.ilkd.key.logic.sort.ProgramSVSort.EXPRESSION) {
0861: // for more on these cases take a look above at the
0862: // variable, static variable and simple expression
0863: // cases.
0864:
0865: // nothing needs to be put into the memory here,
0866: // i.e. into the addNow string, here an expression is
0867: // going to be evaluated!
0868: if (svRestri instanceof RestrictionNone) {
0869: addNow = "";
0870: svToMaude.put(sv, EXPRESSIONVAL);
0871: createAllPossibilities(find, replaceWith, allSVs,
0872: svarrindex, svarrsize, addString + addNow,
0873: svToMaude);
0874: } else if (svRestri instanceof RestrictionInt) {
0875: addNow = "";
0876: svToMaude.put(sv, EXPRESSIONINT);
0877: createAllPossibilities(find, replaceWith, allSVs,
0878: svarrindex, svarrsize, addString + addNow,
0879: svToMaude);
0880: } else if (svRestri instanceof RestrictionBool) {
0881: addNow = "";
0882: svToMaude.put(sv, EXPRESSIONBOOL);
0883: createAllPossibilities(find, replaceWith, allSVs,
0884: svarrindex, svarrsize, addString + addNow,
0885: svToMaude);
0886: } else if (svRestri instanceof RestrictionAtt) {
0887: addNow = "";
0888: svToMaude.put(sv, EXPRESSIONATT);
0889: createAllPossibilities(find, replaceWith, allSVs,
0890: svarrindex, svarrsize, addString + addNow,
0891: svToMaude);
0892: } else {
0893: System.out
0894: .println("Problem, all cases are worked on so "
0895: + "this should not be reachable!");
0896: }
0897: }
0898:
0899: } else {
0900: // this is the first (and only) call to
0901: // "createAllPossibilities" with the iterator used up and
0902: // thus all schemavariables have been assigned
0903: // something. now it is time to assign the fitting add for
0904: // the find part and afterwards the code for that find part;
0905: // then check the newvars, do the assignment there, then
0906: // create the add-new and the code string for the
0907: // replacewith part. All this in done in the extra methods
0908: // below.
0909:
0910: // These 3 strings are class attributes, reset all of them
0911: // to the empty string as they might have been used before
0912: findString = new String();
0913: replaceWithString = new String();
0914: addNewString = new String();
0915:
0916: // this adds a mapping from the new vars to their maude
0917: // meanings into the var to maude meaning mappings!
0918: createNewVarsAddString(svToMaude);
0919: //System.out.println("addNewString here: "+addNewString);
0920:
0921: createFindCode(find, svToMaude);
0922: createReplaceWithCode(replaceWith, svToMaude);
0923: putStringTogetherWriteToFile(addString, svToMaude);
0924: }
0925: }
0926:
0927: // Method to create a String which can be put into a Maude "add..."
0928: // part.
0929: public static String createStringLocalEnv(String svName) {
0930: return "addToLocalEnv(" + svName + "Name:Name, " + svName
0931: + "Loc:Location) ";
0932: }
0933:
0934: // Method to create a String which can be put into a Maude "add..."
0935: // part.
0936: public static String createStringCurrObjEnv(String svName) {
0937: return "addToCurrentObjEnv(" + svName + "Name:Name, " + svName
0938: + "Loc:Location) ";
0939: }
0940:
0941: // Method to create a String which can be put into a Maude "add..."
0942: // part.
0943: public static String createStringStaticEnv(String svName) {
0944: return "addToStaticEnv(" + svName + "CT:CType, " + svName
0945: + "Name:Name, " + svName + "Loc:Location) ";
0946: }
0947:
0948: // Method to create a String which can be put into a Maude "add..."
0949: // part.
0950: public static String createStringMemoryVal(String svName) {
0951: return "addToMemory(" + svName + "Loc:Location, " + svName
0952: + "Val:Value) ";
0953: }
0954:
0955: // Method to create a String which can be put into a Maude "add..."
0956: // part.
0957: public static String createStringMemoryInt(String svName) {
0958: return "addToMemory(" + svName + "Loc:Location, " + "int("
0959: + svName + "Val:Int)" + ") ";
0960: }
0961:
0962: // Method to create a String which can be put into a Maude "add..."
0963: // part.
0964: public static String createStringMemoryBool(String svName) {
0965: return "addToMemory(" + svName + "Loc:Location, " + "bool("
0966: + svName + "Val:Bool)" + ") ";
0967: }
0968:
0969: // Method to create a String which can be put into a Maude "add..."
0970: // part.
0971: public static String createStringMemoryObj(String svName) {
0972: return "addToMemory(" + svName + "ObjRef" + "Loc:Location, "
0973: + "o(" + svName + "CT:CType, " + svName + "CT:CType, "
0974: + svName + "ObjEnv:ObjEnv)) ";
0975: }
0976:
0977: // Method to create a String which can be put into a Maude "add..."
0978: // part.
0979: public static String createStringMemoryObjWAtt(String svName,
0980: String svAttName) {
0981: return "addToMemory(" + svName + "Loc:Location, " + "o("
0982: + svName + "CT:CType, " + svName + "CT:CType, "
0983: + svName + "ObjEnv:ObjEnv " + "(" + svName
0984: + "CT:CType, [" + svAttName + "Name:Name, " + svAttName
0985: + "Loc:Location]))) ";
0986: }
0987:
0988: // Method to create a String which can be put into a Maude "add..."
0989: // part.
0990: public static String createStringNewVarVal(String svName) {
0991: return "addNewToLocalEnvAndMem(" + svName
0992: + "Name:TacletNewVarName, " + svName
0993: + "Loc:TacletNewLocation, " + svName + "Val:Value) ";
0994: }
0995:
0996: // Method to create a String which can be put into a Maude "add..."
0997: // part.
0998: public static String createStringNewVarInt(String svName) {
0999: return "addNewToLocalEnvAndMem(" + svName
1000: + "Name:TacletNewVarName, " + svName
1001: + "Loc:TacletNewLocation, " + "int(" + svName
1002: + "Val:Int)) ";
1003: }
1004:
1005: // Method to create a String which can be put into a Maude "add..."
1006: // part.
1007: public static String createStringNewVarBool(String svName) {
1008: return "addNewToLocalEnvAndMem(" + svName
1009: + "Name:TacletNewVarName, " + svName
1010: + "Loc:TacletNewLocation, " + "bool(" + svName
1011: + "Val:Bool)) ";
1012: }
1013:
1014: // Method to create a String which can be put into a Maude "add..."
1015: // part.
1016: public static String createStringNewVarAtt(String svName,
1017: String svPeerName) {
1018: return "addNewToLocalEnvAndMem(" + svName
1019: + "Name:TacletNewVarName, " + svName
1020: + "Loc:TacletNewLocation, " + "o(" + svPeerName
1021: + "CT:CType, " + svPeerName + "CT:CType, " + svPeerName
1022: + "ObjEnv:ObjEnv)) ";
1023: }
1024:
1025: // In this method the new variables are assigned to their
1026: // maude-"values", the result of this is the side effect on
1027: // "addNewString"
1028: public static void createNewVarsAddString(Map svToMaude) {
1029: addNewString = "";
1030: IteratorOfNewVarcond newvarsIt = newvars.iterator();
1031: while (newvarsIt.hasNext()) {
1032: NewVarcond newVC = newvarsIt.next();
1033: SchemaVariable sv = newVC.getSchemaVariable();
1034: SchemaVariable svPeer = newVC.getPeerSchemaVariable();
1035: Sort svPeerSort = ((SortedSchemaVariable) svPeer).sort();
1036: String svMaudeCase = (String) svToMaude.get(svPeer);
1037:
1038: // New SV's name.
1039: String svName = sv.name().toString().substring(1,
1040: sv.name().toString().length());
1041: // Name of the SV which gives its type to the current new
1042: // SV.
1043: String svPeerName = svPeer.name().toString().substring(1,
1044: svPeer.name().toString().length());
1045:
1046: // Case for the new SV is stored in svToMaude.
1047: svToMaude.put(sv, svMaudeCase);
1048:
1049: // Depending on the case the add-String is extended.
1050: if (svMaudeCase == LOCALVARVAL
1051: || svMaudeCase == ATTOBJWOTHISVAL
1052: || svMaudeCase == ATTOBJWITHTHISVAL
1053: || svMaudeCase == STATATTTYPEREFVAL
1054: || svMaudeCase == STATATTOBJREFVAL
1055: || svMaudeCase == LITERALVALUE
1056: || svMaudeCase == EXPRESSIONVAL
1057: || svMaudeCase == ATTRIBVAL) {
1058: addNewString = addNewString
1059: + createStringNewVarVal(svName);
1060: } else if (svMaudeCase == LOCALVARINT
1061: || svMaudeCase == ATTOBJWOTHISINT
1062: || svMaudeCase == ATTOBJWITHTHISINT
1063: || svMaudeCase == STATATTTYPEREFINT
1064: || svMaudeCase == STATATTOBJREFINT
1065: || svMaudeCase == LITERALINT
1066: || svMaudeCase == EXPRESSIONINT
1067: || svMaudeCase == ATTRIBINT) {
1068: addNewString = addNewString
1069: + createStringNewVarInt(svName);
1070: } else if (svMaudeCase == LOCALVARBOOL
1071: || svMaudeCase == ATTOBJWOTHISBOOL
1072: || svMaudeCase == ATTOBJWITHTHISBOOL
1073: || svMaudeCase == STATATTTYPEREFBOOL
1074: || svMaudeCase == STATATTOBJREFBOOL
1075: || svMaudeCase == LITERALBOOL
1076: || svMaudeCase == EXPRESSIONBOOL
1077: || svMaudeCase == ATTRIBBOOL) {
1078: addNewString = addNewString
1079: + createStringNewVarBool(svName);
1080: } else if (svMaudeCase == LOCALVARATT
1081: || svMaudeCase == ATTOBJWOTHISATT
1082: || svMaudeCase == ATTOBJWITHTHISATT
1083: || svMaudeCase == STATATTTYPEREFATT
1084: || svMaudeCase == STATATTOBJREFATT
1085: || svMaudeCase == EXPRESSIONATT) {
1086: addNewString = addNewString
1087: + createStringNewVarAtt(svName, svPeerName);
1088: }
1089: }
1090: }
1091:
1092: // This method creates the code for the find part. It is stored in
1093: // the static findString attribute.
1094: public static void createFindCode(Term find, Map svToMaude) {
1095: JavaBlock findJavaBlock = find.javaBlock();
1096:
1097: StatementBlock findStatementBlock = (StatementBlock) findJavaBlock
1098: .program();
1099:
1100: if (findStatementBlock == null
1101: || findStatementBlock.getStatementCount() == 0) {
1102: // the code is empty
1103: findString = findString + "";
1104: return;
1105: }
1106:
1107: Statement findStatement = new StatementBlock(findStatementBlock
1108: .getBody());
1109:
1110: // Transform every statement.
1111: for (int countStatements = 0; countStatements < ((NonTerminalProgramElement) findStatementBlock)
1112: .getChildCount(); countStatements++) {
1113:
1114: ProgramElement findPE = ((NonTerminalProgramElement) findStatement)
1115: .getChildAt(countStatements);
1116:
1117: // Add the current statement to the Maude code with the help
1118: // of the recursion.
1119: findString = findString
1120: + recurseFindRepl(findPE, svToMaude) + " ; ";
1121:
1122: }
1123:
1124: }
1125:
1126: // This works the same way as in the find part case,
1127: // i.e. "createFindCode" but writes into replaceWithString as
1128: // result.
1129: public static void createReplaceWithCode(Term replaceWith,
1130: Map svToMaude) {
1131: JavaBlock replaceWithJavaBlock = replaceWith.javaBlock();
1132:
1133: StatementBlock replaceWithStatementBlock = (StatementBlock) replaceWithJavaBlock
1134: .program();
1135:
1136: if (replaceWithStatementBlock == null
1137: || replaceWithStatementBlock.getStatementCount() == 0) {
1138: // the code is empty
1139: replaceWithString = replaceWithString + "";
1140: return;
1141: }
1142:
1143: Statement replaceWithStatement = new StatementBlock(
1144: replaceWithStatementBlock.getBody());
1145:
1146: for (int countStatements = 0; countStatements < ((NonTerminalProgramElement) replaceWithStatement)
1147: .getChildCount(); countStatements++) {
1148:
1149: ProgramElement replaceWithPE = ((NonTerminalProgramElement) replaceWithStatement)
1150: .getChildAt(countStatements);
1151:
1152: replaceWithString = replaceWithString
1153: + recurseFindRepl(replaceWithPE, svToMaude) + " ; ";
1154:
1155: }
1156: }
1157:
1158: // This is the actual core of both "createFindCode" and
1159: // "createReplaceWithCode" methods. It puts the parts together by
1160: // recursing in the subparts of each operator.
1161: public static String recurseFindRepl(ProgramElement pE,
1162: Map svToMaude) {
1163: String result1;
1164: String result2;
1165: if (pE instanceof NonTerminalProgramElement
1166: && ((NonTerminalProgramElement) pE).getChildCount() == 0
1167: && pE instanceof SchemaVariable) {
1168:
1169: SchemaVariable sv = (SchemaVariable) pE;
1170:
1171: String svName = sv.name().toString().substring(1,
1172: sv.name().toString().length());
1173:
1174: String svMaudeCase = (String) svToMaude.get(sv);
1175:
1176: // in case the current sv is one of the "new schema vars"
1177: // that sv is replaced in the code by
1178: // sv+"Name:TacletNewVarName" and it does not matter what
1179: // the type of the variable is!
1180: IteratorOfNewVarcond newvarsIt = newvars.iterator();
1181: while (newvarsIt.hasNext()) {
1182: NewVarcond newVC = newvarsIt.next();
1183: SchemaVariable newSV = newVC.getSchemaVariable();
1184: if (sv == newSV) {
1185: return svName + "Name:TacletNewVarName";
1186: }
1187: }
1188:
1189: // Reaching this code we know that the sv is not a "new"
1190: // one. So we need to distinguish the "types".
1191: if (svMaudeCase == ATTRIBVAL || svMaudeCase == ATTRIBINT
1192: || svMaudeCase == ATTRIBBOOL) {
1193: return svName + "Name:Name";
1194: }
1195: if (svMaudeCase == LOCALVARVAL
1196: || svMaudeCase == LOCALVARINT
1197: || svMaudeCase == LOCALVARBOOL
1198: || svMaudeCase == LOCALVARATT
1199: || svMaudeCase == ATTOBJWOTHISVAL
1200: || svMaudeCase == ATTOBJWOTHISINT
1201: || svMaudeCase == ATTOBJWOTHISBOOL
1202: || svMaudeCase == ATTOBJWOTHISATT) {
1203: return svName + "Name:Name";
1204: }
1205: if (svMaudeCase == ATTOBJWITHTHISVAL
1206: || svMaudeCase == ATTOBJWITHTHISINT
1207: || svMaudeCase == ATTOBJWITHTHISBOOL
1208: || svMaudeCase == ATTOBJWITHTHISATT) {
1209: return "(this . " + svName + "Name:Name)";
1210: }
1211: if (svMaudeCase == STATATTTYPEREFVAL
1212: || svMaudeCase == STATATTTYPEREFINT
1213: || svMaudeCase == STATATTTYPEREFBOOL
1214: || svMaudeCase == STATATTTYPEREFATT) {
1215: return "(" + svName + "CT:CType . " + svName
1216: + "Name:Name)";
1217: }
1218: if (svMaudeCase == STATATTOBJREFVAL
1219: || svMaudeCase == STATATTOBJREFINT
1220: || svMaudeCase == STATATTOBJREFBOOL
1221: || svMaudeCase == STATATTOBJREFATT) {
1222: return "(" + svName + "ObjRefName:Name . " + svName
1223: + "Name:Name)";
1224: }
1225: if (svMaudeCase == LITERALINT) {
1226: return "#i(" + svName + "Val:Int)";
1227: }
1228: if (svMaudeCase == LITERALBOOL) {
1229: return "#b(" + svName + "Val:Bool)";
1230: }
1231: if (svMaudeCase == LITERALVALUE) {
1232: return "resIsValue(" + svName + "Val:Value)";
1233: }
1234: if (svMaudeCase == EXPRESSIONVAL) {
1235: return "eval(" + svName + "EN:ExpressionName , "
1236: + "non-primitive-result)";
1237: }
1238: if (svMaudeCase == EXPRESSIONINT) {
1239: return "eval(" + svName
1240: + "EN:ExpressionName , int-result)";
1241: }
1242: if (svMaudeCase == EXPRESSIONBOOL) {
1243: return "eval(" + svName
1244: + "EN:ExpressionName , bool-result)";
1245: }
1246: if (svMaudeCase == EXPRESSIONATT) {
1247: if (sv instanceof SortedSchemaVariable) {
1248: // It is clear from above that the "sv" is not a
1249: // "new sv" and therefore there is an entry for this
1250: // "sv" in the svToRestriction map, which would not
1251: // be the case for a "new schema var".
1252: Sort svSort = ((SortedSchemaVariable) sv).sort();
1253: RestrictionAtt restri = (RestrictionAtt) svToRestriction
1254: .get(sv);
1255: SchemaVariable svAtt = restri.getAttributeVar();
1256: String svAttName = svAtt.name().toString()
1257: .substring(1,
1258: svAtt.name().toString().length());
1259: Restriction attRestri = ((RestrictionIsAttrib) ((Restriction) svToRestriction
1260: .get(svAtt))).getAttribsRestriction();
1261: String primitiveExpressionResultType = "";
1262: if (attRestri instanceof RestrictionNone) {
1263: primitiveExpressionResultType = "non-primitive-result";
1264: } else if (attRestri instanceof RestrictionInt) {
1265: primitiveExpressionResultType = "int-result";
1266: } else if (attRestri instanceof RestrictionBool) {
1267: primitiveExpressionResultType = "bool-result";
1268: } else {
1269: System.out
1270: .println("Problem, das h�tte andere "
1271: + "Restriction haben m�ssen");
1272: }
1273: return "eval(" + svName
1274: + "EN:ExpressionName , obj-result("
1275: + svName + "CT:CType , " + svAttName
1276: + "Name:Name , "
1277: + primitiveExpressionResultType + "))";
1278: } else {
1279: System.out
1280: .println("Problem, dies sollte immer eine "
1281: + "SortedSchemaVariable sein!");
1282: }
1283: }
1284:
1285: return "ERROR!";
1286:
1287: } else if (pE instanceof TerminalProgramElement) {
1288: // This only works as long as all considered literals are
1289: // ints! If other literals are allowed that needs to be
1290: // tested and treated accordingly.
1291: return "#i(" + pE.toString() + ")";
1292: } else if (pE instanceof NonTerminalProgramElement
1293: && ((NonTerminalProgramElement) pE).getChildCount() == 1) {
1294: result1 = recurseFindRepl(((NonTerminalProgramElement) pE)
1295: .getChildAt(0), svToMaude);
1296: // The result is used with the current operator in each
1297: // case.
1298: if (pE instanceof de.uka.ilkd.key.java.expression.operator.PreIncrement) {
1299: return "++ " + result1;
1300: }
1301: if (pE instanceof de.uka.ilkd.key.java.expression.operator.PostIncrement) {
1302: return result1 + " ++";
1303: }
1304: if (pE instanceof de.uka.ilkd.key.java.expression.operator.PreDecrement) {
1305: return "-- " + result1;
1306: }
1307: if (pE instanceof de.uka.ilkd.key.java.expression.operator.PostDecrement) {
1308: return result1 + " --";
1309: }
1310: if (pE instanceof de.uka.ilkd.key.java.expression.ParenthesizedExpression) {
1311: //System.out.println(pE);
1312: return "(" + result1 + ")";
1313: }
1314: if (pE instanceof de.uka.ilkd.key.java.declaration.VariableSpecification) {
1315: return result1;
1316: }
1317: if (pE instanceof de.uka.ilkd.key.rule.metaconstruct.TypeOf) {
1318:
1319: // for now we just return an empty string and do not
1320: // care about the type this should yield
1321: return "";
1322: }
1323: System.out
1324: .println("This is an untreated 1-argument case: ");
1325: System.out.println("PE: " + pE + " TYPE: " + pE.getClass());
1326:
1327: } else if (pE instanceof NonTerminalProgramElement
1328: && ((NonTerminalProgramElement) pE).getChildCount() == 2) {
1329: result1 = recurseFindRepl(((NonTerminalProgramElement) pE)
1330: .getChildAt(0), svToMaude);
1331: result2 = recurseFindRepl(((NonTerminalProgramElement) pE)
1332: .getChildAt(1), svToMaude);
1333: // Result strings are used together with the current
1334: // operator to get the "total result".
1335: if (pE instanceof de.uka.ilkd.key.java.expression.operator.CopyAssignment) {
1336: return result1 + " = " + result2;
1337: }
1338: if (pE instanceof de.uka.ilkd.key.java.expression.operator.TypeCast) {
1339: // RESTRICTED ONLY!
1340: // as with "TypeOf" this for now only yields an empty
1341: // string instead of {type} and thus only returns the
1342: // second argument basically! (so here instead of
1343: // "{result1} result2" this only gives "result2" because
1344: // the "result1" is empty!
1345: return "" + result2;
1346: }
1347: if (pE instanceof de.uka.ilkd.key.java.declaration.LocalVariableDeclaration) {
1348: // CORRECT -- RESTRICTED ONLY DUE to "TypeOf"! The
1349: // first result is going to be from "TypeOf" and thus
1350: // will be the empty string. We leave it in here so that
1351: // if "TypeOf" is fixed, this is ok too. But for the
1352: // meantime this might end up not declaring something
1353: // new but just be the second result. No real
1354: // restriction here!
1355: return result1 + " " + result2;
1356: }
1357: if (pE instanceof de.uka.ilkd.key.java.expression.operator.Plus) {
1358: return result1 + " + " + result2;
1359: }
1360: if (pE instanceof de.uka.ilkd.key.java.expression.operator.Minus) {
1361: return result1 + " - " + result2;
1362: }
1363: if (pE instanceof de.uka.ilkd.key.java.expression.operator.Times) {
1364: return result1 + " * " + result2;
1365: }
1366: if (pE instanceof de.uka.ilkd.key.java.expression.operator.Divide) {
1367: return result1 + " / " + result2;
1368: }
1369: if (pE instanceof de.uka.ilkd.key.java.expression.operator.Modulo) {
1370: return result1 + " % " + result2;
1371: }
1372: if (pE instanceof de.uka.ilkd.key.java.expression.operator.PlusAssignment) {
1373: return result1 + " += " + result2;
1374: }
1375: if (pE instanceof de.uka.ilkd.key.java.expression.operator.MinusAssignment) {
1376: return result1 + " -= " + result2;
1377: }
1378: if (pE instanceof de.uka.ilkd.key.java.expression.operator.TimesAssignment) {
1379: return result1 + " *= " + result2;
1380: }
1381: if (pE instanceof de.uka.ilkd.key.java.expression.operator.DivideAssignment) {
1382: return result1 + " /= " + result2;
1383: }
1384: if (pE instanceof de.uka.ilkd.key.java.expression.operator.ModuloAssignment) {
1385: return result1 + " %= " + result2;
1386: }
1387:
1388: if (pE instanceof de.uka.ilkd.key.java.expression.operator.Equals) {
1389: return result1 + " == " + result2;
1390: }
1391: if (pE instanceof de.uka.ilkd.key.java.expression.operator.NotEquals) {
1392: return result1 + " != " + result2;
1393: }
1394: if (pE instanceof de.uka.ilkd.key.java.expression.operator.LessThan) {
1395: return result1 + " < " + result2;
1396: }
1397: if (pE instanceof de.uka.ilkd.key.java.expression.operator.LessOrEquals) {
1398: return result1 + " <= " + result2;
1399: }
1400: if (pE instanceof de.uka.ilkd.key.java.expression.operator.GreaterThan) {
1401: return result1 + " > " + result2;
1402: }
1403: if (pE instanceof de.uka.ilkd.key.java.expression.operator.GreaterOrEquals) {
1404: return result1 + " >= " + result2;
1405: }
1406:
1407: // binary and
1408: if (pE instanceof de.uka.ilkd.key.java.expression.operator.BinaryAnd) {
1409: return result1 + " && " + result2;
1410: }
1411: // binary or
1412: if (pE instanceof de.uka.ilkd.key.java.expression.operator.BinaryOr) {
1413: return result1 + " || " + result2;
1414: }
1415:
1416: if (pE instanceof de.uka.ilkd.key.java.declaration.VariableSpecification) {
1417: return result1 + " = " + result2;
1418: }
1419: if (pE instanceof de.uka.ilkd.key.java.reference.SchematicFieldReference) {
1420: return result1 + " . " + result2;
1421: }
1422: if (pE instanceof de.uka.ilkd.key.java.reference.ArrayReference) {
1423: return result1 + " [ " + result2 + " ]";
1424: }
1425: System.out
1426: .println("This is an untreated 2-argument case: ");
1427: System.out.println("PE: " + pE + " TYPE: " + pE.getClass());
1428: } else {
1429: // Bad, should not happen
1430: System.out.println("Problem! This should not happen!");
1431: }
1432:
1433: return "";
1434: }
1435:
1436: // This method puts the whole string together from the parts created
1437: // before. See the Maude interface to see why the string is built as
1438: // below.
1439: public static void putStringTogetherWriteToFile(String addString,
1440: Map svToMaude) {
1441: String resultString = "compareResultsModNewVars(\n"
1442: + "add(basicInitConfiguration, \n" + " "
1443: + addString
1444: + ", \n"
1445: + " "
1446: + "("
1447: + findString
1448: + ").BlockStatements"
1449: + " -> endOfInitCode\n"
1450: + " "
1451: + "), \n"
1452: + "add(basicInitConfiguration, \n"
1453: + " "
1454: + addString
1455: + " "
1456: + addNewString
1457: + ", \n"
1458: + " "
1459: + "("
1460: + replaceWithString
1461: + ").BlockStatements"
1462: + " -> endOfInitCode\n" + " " + ")) ";
1463:
1464: resultString = "search in PGM-SEMANTICS : caseInfo("
1465: + tacletCounter + ", " + caseCounter + ", "
1466: + resultString
1467: + ") =>! ResultingBoolVal:[Bool] . \n\n";
1468:
1469: String infoString = "---- tacletnumber: " + tacletCounter
1470: + ", casenumber: " + caseCounter + "\n"
1471: + "---- tacletname: " + currentTaclet.displayName()
1472: + " \n" + "---- case for each SV: \n";
1473:
1474: Set allSVs = svToMaude.keySet();
1475: Iterator allSVsIt = allSVs.iterator();
1476: while (allSVsIt.hasNext()) {
1477: SchemaVariable sv = (SchemaVariable) allSVsIt.next();
1478: String svCase = (String) svToMaude.get(sv);
1479: infoString = infoString + "---- SV: " + sv + ", Case:"
1480: + svCase + " \n";
1481: }
1482:
1483: try {
1484: fW.write(infoString + resultString);
1485: } catch (Exception e) {
1486: System.err.println("Exception occured while writing to "
1487: + fW + "\n");
1488: e.printStackTrace();
1489: System.exit(-1);
1490: return;
1491: }
1492:
1493: caseCounter = caseCounter + 1;
1494: }
1495:
1496: // Main method which starts everything.
1497: public static void main(String args[]) {
1498: try {
1499: // First overwrite the given file to make it empty,
1500: fW = new FileWriter(args[0], false);
1501: fW.write("");
1502: fW.close();
1503: // then open it and append everything which follows.
1504: fW = new FileWriter(args[0], true);
1505: } catch (Exception e) {
1506: System.err.println("Exception occured while opening file "
1507: + fW + "\n");
1508: e.printStackTrace();
1509: System.exit(-1);
1510: return;
1511: }
1512:
1513: SetOfTaclet taclets = parseTaclets();
1514: processAllTaclets(taclets);
1515:
1516: try {
1517: fW.close();
1518: } catch (Exception e) {
1519: System.err.println("Exception occured while closing file "
1520: + fW + "\n");
1521: e.printStackTrace();
1522: System.exit(-1);
1523: return;
1524: }
1525: }
1526:
1527: }
|