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: //
009: //
010:
011: package de.uka.ilkd.key.casetool.patternimplementor;
012:
013: import java.io.BufferedReader;
014: import java.io.File;
015: import java.io.FileReader;
016: import java.util.Stack;
017: import java.util.StringTokenizer;
018: import java.util.Vector;
019:
020: public class ConstraintMechanism {
021:
022: private static final String POST = "@postconditions ";
023:
024: private static final String PRE = "@preconditions ";
025:
026: private static final String INV = "@invariants ";
027:
028: private static final String DEF = "@definitions ";
029:
030: // private static final String EPOST= "@extended_postcondition ";
031: // private static final String SINV = "@static_invariant ";
032: private static final String KeyBOOLEAN = "[Boolean]";
033:
034: private static final String KeyVOID = "[Void]";
035:
036: private static final String KeySTRING = "[String]";
037:
038: private static final String KeyMSTRING = "[MultiString]";
039:
040: private static final String KeyGROUP = "[Group]";
041:
042: private static final String KeyENDGROUP = "[EndGroup]";
043:
044: private static final String KeyDEPEND = "[Dependent]";
045:
046: private static final String KeyCONTEXT = "[Context]";
047:
048: private static final String KeyPOST = "[PostCondition]";
049:
050: private static final String KeyPRE = "[PreCondition]";
051:
052: private static final String KeyINV = "[Invariant]";
053:
054: private static final String KeyDEF = "[Definition]";
055:
056: //String filename;
057: PIParameterGroup parameterGroup;
058:
059: Vector constraints;
060:
061: /*
062: * public ConstraintMechanism(PIParameterGroup parameterGroup) { }
063: */
064: public ConstraintMechanism(String filename,
065: PIParameterGroup parameterGroup,
066: AbstractPatternImplementor api) {
067: //this(parameterGroup);
068: this .parameterGroup = parameterGroup;
069: this .constraints = new Vector();
070:
071: String packagePath = api.getClass().getPackage().toString();
072: packagePath = packagePath
073: .substring(packagePath.indexOf(" ") + 1);
074:
075: byte[] pathArray = packagePath.getBytes();
076:
077: for (int i = 0; i < pathArray.length; i++) {
078: if (pathArray[i] == '.') {
079: pathArray[i] = (byte) File.separatorChar;
080: }
081: }
082:
083: parseFile(new String(pathArray) + File.separatorChar + filename);
084: }
085:
086: private void parseFile(String filename) {
087: //System.err.println("Trying to parse " + filename);
088:
089: try {
090: BufferedReader infile = null;
091:
092: String classPath = System.getProperty("java.class.path",
093: ".");
094:
095: StringTokenizer cp = new StringTokenizer(classPath,
096: File.pathSeparator);
097:
098: while (cp.hasMoreTokens()) {
099: String cPath = cp.nextToken();
100: //System.err.println("looking in " + cPath + File.separatorChar
101: // + filename);
102: File f = new File(cPath + File.separatorChar + filename);
103: if (f.exists()) {
104: FileReader fr = new FileReader(cPath
105: + File.separatorChar + filename);
106: infile = new BufferedReader(fr);
107: break;
108: }
109: }
110: if (infile == null) {
111: return;
112: }
113:
114: String indata;
115: Stack groupStack = new Stack();
116: int linenumber = 0;
117:
118: String currentContext = null;
119:
120: groupStack.push(new PIParameterGroup("constraintGroup",
121: "Constraints"));
122:
123: while ((indata = infile.readLine()) != null) {
124: linenumber++;
125:
126: // remove comments
127: int index = indata.indexOf("//");
128:
129: if (index != -1) {
130: indata = indata.substring(0,
131: ((index - 1) > 0) ? (index - 1) : 0);
132: }
133:
134: indata = indata.trim();
135:
136: try {
137: if (indata.indexOf(KeyBOOLEAN) != -1) {
138: parseBoolean(indata, groupStack);
139: } else if (indata.indexOf(KeyDEPEND) != -1) {
140: // [Dependent]
141: //System.out.print("DEPEND");
142: } else if (indata.indexOf(KeyENDGROUP) != -1) {
143: // [EndGroup]
144: groupStack.pop();
145: } else if (indata.indexOf(KeyGROUP) != -1) {
146: parseGroupBegin(indata, groupStack);
147: } else if (indata.indexOf(KeyMSTRING) != -1) {
148: parseMultiString(indata, groupStack);
149: } else if (indata.indexOf(KeySTRING) != -1) {
150: parseString(indata, groupStack);
151: } else if (indata.indexOf(KeyVOID) != -1) {
152: parseVoid(indata, groupStack);
153: } else if (indata.indexOf(KeyCONTEXT) != -1) {
154: currentContext = parseContext(indata);
155: } else if (indata.indexOf(KeyPOST) != -1) {
156: parseConstraint(indata, currentContext, POST);
157: } else if (indata.indexOf(KeyPRE) != -1) {
158: parseConstraint(indata, currentContext, PRE);
159: } else if (indata.indexOf(KeyINV) != -1) {
160: parseConstraint(indata, currentContext, INV);
161: } else if (indata.indexOf(KeyDEF) != -1) {
162: parseConstraint(indata, currentContext, DEF);
163: } else {
164: }
165: } catch (Exception e) {
166: // ignore syntax error for now
167: System.err.println("Syntax error in " + filename
168: + " at line " + linenumber);
169: }
170: }
171:
172: if (groupStack.size() == 1) {
173: //parameterGroup = (PIParameterGroup)groupStack.pop();
174: //System.out.println("Doesn't assign parameterGroup");
175: //return (PIParameterGroup)groupStack.pop();
176: parameterGroup.add((PIParameterGroup) groupStack.pop());
177: } else {
178: System.err.println("Unbalanced [Group]-[EndGroup] in "
179: + filename);
180: }
181: } catch (Exception e) {
182: System.err.println("Couldn't open file : " + filename);
183: e.printStackTrace();
184: }
185:
186: //System.out.println("ConstraintMechanism.parseFile - returns null");
187: //return null;
188: }
189:
190: private void parseConstraint(String indata, String currentContext,
191: String type) {
192: // [PostCondition] ocl-expression
193: // [PreCondition] ocl-expression
194: // [Invariant] ocl-expression
195: // [Definition] ocl-expression
196: if (currentContext == null) {
197: System.err.println("Skipping " + indata
198: + " since context unknown");
199: } else {
200: int a = indata.indexOf(']');
201: String constraint = indata.substring(a + 1).trim();
202:
203: //System.out.println(POST+ " " + postcond);
204: Constraint c = new Constraint(currentContext, constraint,
205: type);
206: constraints.add(c);
207: }
208: }
209:
210: private String parseContext(String indata) {
211: String currentContext;
212:
213: // [Context] context::context
214: int a = indata.indexOf(']');
215:
216: currentContext = new String(indata.substring(a + 1).trim());
217:
218: /*
219: * a = indata.indexOf('"'); int b = indata.indexOf('"',a+1);
220: * currentContext = currentContext.substring(a+1,b);
221: */
222: return currentContext;
223: }
224:
225: private void parseVoid(String indata, Stack groupStack) {
226: // [Void] "name"
227: int a = indata.indexOf('"');
228: int b = indata.indexOf('"', a + 1);
229: String name = indata.substring(a + 1, b);
230: ((PIParameterGroup) groupStack.peek()).add(new PIParameterVoid(
231: name));
232: }
233:
234: private void parseString(String indata, Stack groupStack) {
235: // [String] "internalName", "name", "value"
236: String internalName;
237: String name;
238: String value;
239:
240: int a = indata.indexOf('"');
241: int b = indata.indexOf('"', a + 1);
242: internalName = indata.substring(a + 1, b);
243:
244: a = indata.indexOf('"', b + 1);
245: b = indata.indexOf('"', a + 1);
246: name = indata.substring(a + 1, b);
247:
248: a = indata.indexOf('"', b + 1);
249: b = indata.indexOf('"', a + 1);
250: value = indata.substring(a + 1, b);
251:
252: //System.out.print("STRING ->"+internalName+","+name+","+value+"<-");
253: ((PIParameterGroup) groupStack.peek())
254: .add(new PIParameterString(internalName, name, value));
255: }
256:
257: private void parseMultiString(String indata, Stack groupStack) {
258: // [MultiString] "internalName", "name", "value"
259: String internalName;
260: String name;
261: String value;
262:
263: int a = indata.indexOf('"');
264: int b = indata.indexOf('"', a + 1);
265: internalName = indata.substring(a + 1, b);
266:
267: a = indata.indexOf('"', b + 1);
268: b = indata.indexOf('"', a + 1);
269: name = indata.substring(a + 1, b);
270:
271: a = indata.indexOf('"', b + 1);
272: b = indata.indexOf('"', a + 1);
273: value = indata.substring(a + 1, b);
274:
275: //System.out.print("MSTR ->"+internalName+","+name+","+value+"<-");
276: ((PIParameterGroup) groupStack.peek())
277: .add(new PIParameterMultiString(internalName, name,
278: value));
279: }
280:
281: private void parseGroupBegin(String indata, Stack groupStack) {
282: // [Group] "internalName", "name"
283: String internalName;
284: String name;
285:
286: int a = indata.indexOf('"');
287: int b = indata.indexOf('"', a + 1);
288: internalName = indata.substring(a + 1, b);
289:
290: a = indata.indexOf('"', b + 1);
291: b = indata.indexOf('"', a + 1);
292: name = indata.substring(a + 1, b);
293:
294: //System.out.print("GROUP ->"+internalName+","+name+"<-");
295: PIParameterGroup newgrp = new PIParameterGroup(internalName,
296: name);
297:
298: ((PIParameterGroup) groupStack.peek()).add(newgrp);
299: groupStack.push(newgrp);
300: }
301:
302: private void parseBoolean(String indata, Stack groupStack) {
303: // [Boolean] "internalName", "name", "value"
304: String internalName;
305: String name;
306: String value;
307:
308: int a = indata.indexOf('"');
309: int b = indata.indexOf('"', a + 1);
310: internalName = indata.substring(a + 1, b);
311:
312: a = indata.indexOf('"', b + 1);
313: b = indata.indexOf('"', a + 1);
314: name = indata.substring(a + 1, b);
315:
316: a = indata.indexOf('"', b + 1);
317: b = indata.indexOf('"', a + 1);
318: value = indata.substring(a + 1, b);
319:
320: //System.out.print("BOOL ->"+internalName+","+name+","+value+"<-");
321: ((PIParameterGroup) groupStack.peek())
322: .add(new PIParameterBoolean(internalName, name, value));
323: }
324:
325: public PIParameterGroup getPIParameterGroup() {
326: return parameterGroup; //parameterGroup;
327: }
328:
329: public String getConstraints(String prefix, String context,
330: String realContext) {
331: Vector postconditions = new Vector();
332: Vector preconditions = new Vector();
333: Vector invariants = new Vector();
334: Vector definitions = new Vector();
335:
336: //Vector staticinv = new Vector();
337: //Vector extendedpost = new Vector();
338: String retval = new String();
339:
340: for (int i = 0; i < constraints.size(); i++) {
341: //System.out.println("...."+((Constraint)constraints.elementAt(i)));
342: if (((Constraint) constraints.elementAt(i)).getContext()
343: .equals(context)) {
344: String constraint = "("
345: + ((Constraint) constraints.elementAt(i))
346: .getConstraint(context, parameterGroup)
347: + ")";
348: String type = ((Constraint) constraints.elementAt(i))
349: .getType();
350:
351: if (type.equals(POST)) {
352: postconditions.add(constraint);
353: } else if (type.equals(PRE)) {
354: preconditions.add(constraint);
355: } else if (type.equals(INV)) {
356: invariants.add(constraint);
357: } else if (type.equals(DEF)) {
358: definitions.add(constraint);
359: } else {
360: System.err
361: .println("ConstraintMechanism.getConstraints - unknown Constraint type : \""
362: + type + "\"");
363: }
364: }
365: }
366:
367: retval = retval
368: + constraintConjunction(prefix + PRE, preconditions);
369: retval = retval
370: + constraintConjunction(prefix + INV, invariants);
371: retval = retval
372: + constraintConjunction(prefix + DEF, definitions);
373: retval = retval
374: + constraintConjunction(prefix + POST, postconditions);
375:
376: if (retval.equals("")) {
377: retval = null;
378: }
379:
380: return retval;
381: }
382:
383: private String constraintConjunction(String prefix,
384: Vector constraints) {
385: String retval = new String();
386:
387: for (int i = 0; i < constraints.size(); i++) {
388: if (i == 0) {
389: retval = retval + prefix + constraints.elementAt(i);
390: } else {
391: retval = retval + " and " + constraints.elementAt(i);
392: }
393: }
394:
395: return retval;
396: }
397:
398: class Constraint {
399:
400: private static final String BEGIN = "<:";
401:
402: private static final String END = ":>";
403:
404: private String context;
405:
406: private String constraint;
407:
408: private String type;
409:
410: Constraint(String context, String constraint, String type) {
411: this .type = type;
412: this .context = context;
413: this .constraint = constraint;
414: }
415:
416: public String getContext() {
417: return context;
418: }
419:
420: /*
421: * alternativ psuedokod - varken testad eller anv�nd :| input = 1234
422: * <:5678:>90abc <:def:>ghi ^ ^ ^ ^ ^ p0 p1 p2 p3 p4
423: *
424: * String result = new String(); boolean textmode = input.indexOf(" <:") ==
425: * p[0]; for(int i = 0; i < p.size()-1 ; i++) { if(textmode) { result =
426: * result + input.substring(p[i], p[i+1]); } else // replacemode {
427: * String replaceval = getReplaceval(input.substring(p[i],p[i+1]);
428: * result = result + replaceval; } textmode != textmode; }
429: *
430: */
431: public String getConstraint(String context,
432: PIParameterGroup pipg) {
433: String instantiatedConstraint = new String();
434:
435: if (context.equals(this .context)) {
436: instantiatedConstraint = constraint;
437:
438: Vector placeholders = searchPlaceholders(instantiatedConstraint);
439: int size = placeholders.size();
440:
441: for (int i = 0; i < size; i++) {
442: placeholders = searchPlaceholders(instantiatedConstraint);
443:
444: int a = ((int[]) placeholders.elementAt(0))[0];
445: int b = ((int[]) placeholders.elementAt(0))[1];
446: String pre = instantiatedConstraint.substring(0, a
447: - BEGIN.length());
448: String tmp = instantiatedConstraint.substring(a, b);
449: String post = instantiatedConstraint.substring(b
450: + END.length(), instantiatedConstraint
451: .length());
452:
453: //System.out.println("...'"+pre+"'"+tmp+"'"+post+"'...");
454: //System.out.println("Trying to get things from
455: // "+pipg.getInternalName());
456: PIParameter value = pipg.get(tmp);
457:
458: if (value != null) {
459: instantiatedConstraint = pre + value.getValue()
460: + post;
461: }
462: }
463: } else {
464: System.out.println("wrong context" + this .context
465: + " != " + context);
466: }
467:
468: return instantiatedConstraint;
469: }
470:
471: public Vector searchPlaceholders(String constraint) {
472: Vector placeholders = new Vector();
473:
474: int a = 0;
475: int b = 0;
476: int pointer = 0;
477:
478: while (true) {
479: a = constraint.indexOf(BEGIN, pointer);
480: b = constraint.indexOf(END, a + 1);
481: pointer = b + 1;
482:
483: if ((a == -1) || (b == -1)) {
484: break;
485: } else {
486: a = a + BEGIN.length();
487:
488: //b = b;
489: //System.out.println("Start " + a + " \tEnd " +b);
490: int[] tmp = new int[2];
491: tmp[0] = a;
492: tmp[1] = b;
493: placeholders.add(tmp);
494: }
495: }
496:
497: return placeholders;
498: }
499:
500: public String toString() {
501: return "context " + context + "\n" + type + ": "
502: + constraint;
503: }
504:
505: public String getType() {
506: return type;
507: }
508: }
509: }
|