001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017: package de.uka.ilkd.key.proof;
018:
019: import java.io.StringReader;
020: import java.util.Vector;
021:
022: import javax.swing.JOptionPane;
023:
024: import de.uka.ilkd.key.casetool.ModelMethod;
025: import de.uka.ilkd.key.java.JavaInfo;
026: import de.uka.ilkd.key.java.Services;
027: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
028: import de.uka.ilkd.key.logic.*;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.parser.KeYLexer;
031: import de.uka.ilkd.key.parser.KeYParser;
032: import de.uka.ilkd.key.parser.ParserMode;
033:
034: /**
035: * Parses modifies clauses.
036: * @deprecated
037: */
038: public class ModifiesParserHelper {
039: private final ModelMethod modelMethod;
040: private final Services services;
041: private final NamespaceSet nss;
042: private final JavaInfo javaInfo;
043:
044: private ProgramVariable self;
045: private ListOfProgramVariable params = SLListOfProgramVariable.EMPTY_LIST;
046:
047: private Namespace ns = new Namespace();
048:
049: /**
050: * @deprecated
051: */
052: private SetOfTerm modifiesElements;
053:
054: public ModifiesParserHelper(ModelMethod modelMethod,
055: Services services, NamespaceSet nss) {
056: this .modelMethod = modelMethod;
057: this .javaInfo = services.getJavaInfo();
058: this .services = services;
059: this .nss = nss;
060: }
061:
062: /**
063: * @deprecated Use parseModifiesClause(String modifiesString) instead.
064: */
065: public void parseModifiesClauseToHashSet(String modifiesString) {
066:
067: // create program variables for "self" and the parameters
068: parseSignatureStringAndFillNamespace();
069:
070: // puts the parsed modifies clause into the set modifiesElements
071: parseModifiesString(modifiesString);
072: }
073:
074: /**
075: * @deprecated Use parseModifiesClause(String modifiesString) instead.
076: */
077: public void parseModifiesClause(Namespace ns, String modifiesString) {
078: this .ns = ns;
079:
080: // create program variables for "self" and the parameters
081: parseSignatureStringAndFillNamespace();
082:
083: // puts the parsed modifies clause into the set modifiesElements
084: parseModifiesString(modifiesString);
085: }
086:
087: public SetOfLocationDescriptor parseModifiesClause(
088: String modifiesString) {
089: // create program variables for "self" and the parameters
090: parseSignatureStringAndFillNamespace();
091:
092: if (modifiesString == null || "".equals(modifiesString)) {
093: return SetAsListOfLocationDescriptor.EMPTY_SET;
094: }
095:
096: if (modelMethod.isQuery()) {
097: // query but non-empty modifies string; not allowed to happen!
098: JOptionPane
099: .showMessageDialog(
100: null,
101: "Inconsistent Modifies Set",
102: "Non-empty modifies set but the method is a query!",
103: JOptionPane.ERROR_MESSAGE);
104: throw new IllegalStateException(
105: "Non-empty modifies set but the method is a query!");
106: }
107:
108: Namespace originalProgramVariables = nss.programVariables();
109: nss.setProgramVariables(ns);
110:
111: KeYParser parser = new KeYParser(ParserMode.TERM, new KeYLexer(
112: new StringReader(modifiesString), null), "",
113: TermFactory.DEFAULT, services, nss);
114: SetOfLocationDescriptor result = SetAsListOfLocationDescriptor.EMPTY_SET;
115: try {
116: result = parser.location_list();
117: } catch (antlr.RecognitionException e) {
118: System.out.println("RecognitionException occurred");
119: e.printStackTrace();
120: } catch (antlr.TokenStreamException e) {
121: System.out.println("TokenStreamException occurred");
122: e.printStackTrace();
123: } finally {
124: nss.setProgramVariables(originalProgramVariables);
125: }
126:
127: return result;
128: }
129:
130: private void parseSignatureStringAndFillNamespace() {
131: // create "self" and add it to the namespace
132: self = new LocationVariable(new ProgramElementName("self"),
133: javaInfo.getKeYJavaType(modelMethod
134: .getContainingClass().getFullClassName()));
135: ns.add(self);
136:
137: String signatureString = modelMethod.getCallSignature(false);
138:
139: // first extract the name of the method
140: int index = signatureString.indexOf("(");
141: signatureString = signatureString.substring(index + 1).trim();
142:
143: // then extract the names and types of parameters
144: index = signatureString.indexOf(")");
145: String type = null;
146: while (index > 0) {
147: String paramName;
148: KeYJavaType paramType;
149:
150: index = signatureString.indexOf(":");
151: paramName = signatureString.substring(0, index).trim();
152: signatureString = signatureString.substring(index + 1)
153: .trim();
154:
155: index = signatureString.indexOf(";");
156: // index = -1 if there is no ";" in the string because we are
157: // parsing the last element
158: if (index < 0) {
159: index = signatureString.indexOf(")");
160: type = signatureString.substring(0, index).trim();
161: // convert to KeYJavaType and add to the vector
162: paramType = javaInfo.getKeYJavaType(type);
163:
164: // the ")" is at the very end of the string so don't add
165: // 1 to the index in this case otherwise there is a string
166: // out of bounds error
167: // by this the index calculated below will be 0
168: signatureString = signatureString.substring(index + 0)
169: .trim();
170: } else {
171: type = signatureString.substring(0, index).trim();
172: // convert to KeYJavaType and add to the vector
173: paramType = javaInfo.getKeYJavaType(type);
174: signatureString = signatureString.substring(index + 1)
175: .trim();
176: }
177: index = signatureString.indexOf(")");
178:
179: // create the parameter variable and add it to the namespace
180: ProgramVariable paramVar = new LocationVariable(
181: new ProgramElementName(paramName), paramType);
182: params = params.prepend(paramVar);
183: ns.add(paramVar);
184: }
185: }
186:
187: /**
188: * @deprecated
189: */
190: private void parseModifiesString(String modifiesString) {
191: if (modelMethod.isQuery()) {
192: // query and empty or non-existing modifies string;
193: // make an empty modifies string
194: if (modifiesString == null || "".equals(modifiesString)) {
195: modifiesString = "";
196: }
197: // query but non-empty modifies string; not allowed to happen!
198: else {
199: JOptionPane
200: .showMessageDialog(
201: null,
202: "Inconsistent Modifies Set",
203: "Non-empty modifies set but the method is a query!",
204: JOptionPane.ERROR_MESSAGE);
205: throw new IllegalStateException(
206: "Non-empty modifies set but the method is a query!");
207: }
208: }
209: // otherwise no changes need to be done
210:
211: if (modifiesString == null || "".equals(modifiesString)) {
212: modifiesElements = SetAsListOfTerm.EMPTY_SET;
213: } else {
214: modifiesElements = useTermParser(modifiesString);
215: }
216: }
217:
218: /**
219: * @deprecated
220: */
221: private SetOfTerm useTermParser(String modifiesString) {
222: modifiesString = "{" + modifiesString + "}";
223: Namespace originalProgramVariables = nss.programVariables();
224: nss.setProgramVariables(ns);
225: KeYParser parser = new KeYParser(ParserMode.TERM, new KeYLexer(
226: new StringReader(modifiesString), null), "",
227: TermFactory.DEFAULT, services, nss);
228: SetOfTerm accessTerms = SetAsListOfTerm.EMPTY_SET;
229: try {
230: SetOfLocationDescriptor locs = parser.location_list();
231: IteratorOfLocationDescriptor it = locs.iterator();
232: while (it.hasNext()) {
233: accessTerms = accessTerms
234: .add(((BasicLocationDescriptor) it.next())
235: .getLocTerm());
236: }
237: } catch (antlr.RecognitionException e0) {
238: System.out.println("RecognitionException occurred");
239: e0.printStackTrace();
240: } catch (antlr.TokenStreamException e1) {
241: System.out.println("TokenStreamException occurred");
242: e1.printStackTrace();
243: }
244: nss.setProgramVariables(originalProgramVariables);
245: return accessTerms;
246: }
247:
248: /**
249: * @deprecated
250: */
251: public SetOfTerm getModifiesElements() {
252: return (modifiesElements == null ? SetAsListOfTerm.EMPTY_SET
253: : modifiesElements);
254: }
255:
256: public String getMethodName() {
257: return modelMethod.getName();
258: }
259:
260: public ProgramVariable getPVSelf() {
261: return self;
262: }
263:
264: public ListOfProgramVariable getPVParams() {
265: return params;
266: }
267:
268: /**
269: * @deprecated
270: */
271: public Vector getPVVector() {
272: Vector result = new Vector();
273: IteratorOfProgramVariable it = params.iterator();
274: while (it.hasNext()) {
275: result.add(it.next());
276: }
277: return result;
278: }
279:
280: /**
281: * @deprecated
282: */
283: public Vector getParameterTypesVector() {
284: Vector result = new Vector();
285: IteratorOfProgramVariable it = params.iterator();
286: while (it.hasNext()) {
287: result.add(it.next().getKeYJavaType());
288: }
289: return result;
290: }
291: }
|