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.parser;
012:
013: import java.io.PrintWriter;
014: import java.io.StringReader;
015: import java.io.StringWriter;
016:
017: import junit.framework.TestCase;
018: import de.uka.ilkd.key.java.ContextStatementBlock;
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
021: import de.uka.ilkd.key.java.declaration.VariableSpecification;
022: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
023: import de.uka.ilkd.key.java.reference.ArrayReference;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.SchemaVariable;
026: import de.uka.ilkd.key.logic.op.TermSymbol;
027: import de.uka.ilkd.key.rule.*;
028:
029: /** class tests the parser for Taclets
030: */
031:
032: public class TestTacletParser extends TestCase {
033:
034: public NamespaceSet nss;
035: public Services services;
036:
037: TermFactory tf = TermFactory.DEFAULT;
038:
039: public TestTacletParser(String name) {
040: super (name);
041: }
042:
043: //
044: // set up
045: //
046:
047: public void setUp() {
048: nss = new NamespaceSet();
049: services = TacletForTests.services();
050:
051: parseDecls("\\sorts { s; }\n" + "\\functions {\n"
052: + " s f(s);\n" + "}\n" + "\\schemaVariables {\n"
053: + " \\formula b,b0,post;\n"
054: + " \\program Statement #p1, #s ; \n"
055: + " \\program Expression #e2, #e ; \n"
056: + " \\program SimpleExpression #se ; \n"
057: + " \\program Variable #slhs, #arr, #ar, #ar1 ; \n"
058: + " \\program LoopInit #i ; \n"
059: + " \\program Label #lab, #lb0, #lb1 ; \n"
060: + " \\program Label #inner, #outer ; \n"
061: + " \\program Type #typ ; \n"
062: + " \\program Variable #v0, #v, #v1, #k, #boolv ; \n"
063: + " \\program[list] Catch #cf ; \n"
064: + " \\term s x,x0 ;\n" + " \\skolemTerm s sk ;\n"
065: + " \\variables s z,z0 ;\n" + "}\n");
066: }
067:
068: //
069: // Utility methods for setUp:
070: //
071:
072: TermSymbol lookup_var(String name) {
073: return (TermSymbol) nss.variables().lookup(new Name(name));
074: }
075:
076: private KeYParser stringDeclParser(String s) {
077: return new KeYParser(ParserMode.DECLARATION, new KeYLexer(
078: new StringReader(s), null),
079: "No file. parser/TestTacletParser.stringDeclParser("
080: + s + ")", services, nss);
081: }
082:
083: public void parseDecls(String s) {
084: try {
085: KeYParser p = stringDeclParser(s);
086: p.decls();
087: } catch (Exception e) {
088: StringWriter sw = new StringWriter();
089: PrintWriter pw = new PrintWriter(sw);
090: e.printStackTrace(pw);
091: throw new RuntimeException("Exc while Parsing:\n" + sw);
092: }
093: }
094:
095: //
096: // Utility Methods for test cases.
097: //
098: private KeYParser stringTacletParser(String s) {
099: return new KeYParser(ParserMode.TACLET, new KeYLexer(
100: new StringReader(s), null),
101: "No file. parser/TestTacletParser.stringTacletParser("
102: + s + ")", tf, services, nss);
103: }
104:
105: public Term parseTerm(String s) {
106: try {
107: KeYParser p = stringTacletParser(s);
108: return p.term();
109: } catch (Exception e) {
110: StringWriter sw = new StringWriter();
111: PrintWriter pw = new PrintWriter(sw);
112: e.printStackTrace(pw);
113: throw new RuntimeException("Exc while Parsing:\n" + sw);
114: }
115: }
116:
117: public Term parseFma(String s) {
118: try {
119: KeYParser p = stringTacletParser(s);
120:
121: return p.formula();
122: } catch (Exception e) {
123: StringWriter sw = new StringWriter();
124: PrintWriter pw = new PrintWriter(sw);
125: e.printStackTrace(pw);
126: throw new RuntimeException("Exc while Parsing:\n" + sw);
127: }
128: }
129:
130: public ConstrainedFormula cf(String s) {
131: return new ConstrainedFormula(parseFma(s), Constraint.BOTTOM);
132: }
133:
134: public Semisequent sseq(String s) {
135: return Semisequent.EMPTY_SEMISEQUENT.insertFirst(cf(s))
136: .semisequent();
137: }
138:
139: public Sequent sequent(String a, String s) {
140: Semisequent ass = Semisequent.EMPTY_SEMISEQUENT;
141: Semisequent sss = Semisequent.EMPTY_SEMISEQUENT;
142: if (a != null) {
143: ass = sseq(a);
144: }
145: if (s != null) {
146: sss = sseq(s);
147: }
148: return Sequent.createSequent(ass, sss);
149: }
150:
151: Taclet parseTaclet(String s) {
152: try {
153: KeYParser p = stringTacletParser(s);
154:
155: return p.taclet(SetAsListOfChoice.EMPTY_SET);
156: } catch (Exception e) {
157: StringWriter sw = new StringWriter();
158: PrintWriter pw = new PrintWriter(sw);
159: e.printStackTrace(pw);
160: throw new RuntimeException("Exc while Parsing:\n" + sw);
161: }
162: }
163:
164: //
165: // Test cases.
166: //
167:
168: public void testImpLeft() {
169: // imp-left rule
170: // find(b->b0 =>) replacewith(b0 =>) replacewith(=> b)
171: AntecTacletBuilder builder = new AntecTacletBuilder();
172: builder.setFind(parseFma("b->b0"));
173: builder.setName(new Name("imp_left"));
174: builder.addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
175: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
176: sequent("b0", null)));
177:
178: builder.addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
179: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
180: sequent(null, "b")));
181:
182: Taclet impleft = builder.getAntecTaclet();
183: String impleftString = "imp_left{\\find(b->b0 ==>) \\replacewith(b0 ==>); \\replacewith(==> b)}";
184: assertEquals("imp-left", impleft, parseTaclet(impleftString));
185: }
186:
187: public void testImpRight() {
188: // imp-right rule
189: // find(=> b->b0) replacewith(b => b0)
190: SuccTacletBuilder builder = new SuccTacletBuilder();
191: builder.setFind(parseFma("b->b0"));
192: builder.addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
193: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
194: sequent("b", "b0")));
195: builder.setName(new Name("imp_right"));
196: Taclet impright = builder.getSuccTaclet();
197: String imprightString = "imp_right{\\find(==> b->b0) \\replacewith(b ==> b0)}";
198:
199: assertEquals("imp-right", impright, parseTaclet(imprightString));
200: }
201:
202: public void testCut() {
203: // cut rule
204: // add(b=>) add(=>b)
205: NoFindTacletBuilder builder = new NoFindTacletBuilder();
206: builder.addTacletGoalTemplate(new TacletGoalTemplate(sequent(
207: "b", null), SLListOfTaclet.EMPTY_LIST));
208:
209: builder.addTacletGoalTemplate(new TacletGoalTemplate(sequent(
210: null, "b"), SLListOfTaclet.EMPTY_LIST));
211: builder.setName(new Name("cut"));
212:
213: Taclet cut = builder.getNoFindTaclet();
214: String cutString = "cut{\\add(b==>); \\add(==>b)}";
215: assertEquals("cut", cut, parseTaclet(cutString));
216: }
217:
218: public void testClose() {
219: // close rule
220: // if (b=>) find(=>b)
221: SuccTacletBuilder builder = new SuccTacletBuilder();
222: builder.setFind(parseFma("b"));
223: builder.setIfSequent(sequent("b", null));
224: builder.setName(new Name("close_goal"));
225: Taclet close = builder.getSuccTaclet();
226: String closeString = "close_goal{\\assumes (b==>) \\find(==>b) \\closegoal}";
227: assertEquals("close", close, parseTaclet(closeString));
228: }
229:
230: public void testContraposition() {
231: // contraposition rule
232: // find(b->b0) replacewith(-b0 -> -b)
233:
234: RewriteTacletBuilder builder = new RewriteTacletBuilder();
235: builder.setFind(parseFma("b->b0"));
236: builder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
237: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
238: parseFma("!b0->!b")));
239: builder.setName(new Name("contraposition"));
240: Taclet contraposition = builder.getRewriteTaclet();
241: String contrapositionString = "contraposition{\\find(b->b0) \\replacewith(!b0 -> !b)}";
242:
243: assertEquals("contraposition", contraposition,
244: parseTaclet(contrapositionString));
245: }
246:
247: public void testAllRight() {
248: // all-right rule
249: // find (==> all z.b) varcond ( sk new depending on b ) replacewith (==> {z sk}b)
250: SuccTacletBuilder builder = new SuccTacletBuilder();
251:
252: builder.setFind(parseFma("\\forall z; b"));
253: builder.addTacletGoalTemplate(new AntecSuccTacletGoalTemplate(
254: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
255: sequent(null, "{\\subst z; sk}b")));
256: builder.addVarsNewDependingOn(
257: (SchemaVariable) lookup_var("sk"),
258: (SchemaVariable) lookup_var("b"));
259: builder.setName(new Name("all_right"));
260: Taclet allright = builder.getSuccTaclet();
261: String allrightString = "all_right{\\find (==> \\forall z; b) \\varcond ( \\new(sk,\\dependingOn(b)) ) \\replacewith (==> {\\subst z; sk}b)}";
262: assertEquals("all-right", allright, parseTaclet(allrightString));
263: }
264:
265: public void testAllLeft() {
266: // all-left rule
267: // find(all z . b==>) add({z x}b==>)
268: AntecTacletBuilder builder = new AntecTacletBuilder();
269:
270: builder.setFind(parseFma("\\forall z; b"));
271:
272: builder.addTacletGoalTemplate(new TacletGoalTemplate(sequent(
273: "{\\subst z; x}b", null), SLListOfTaclet.EMPTY_LIST));
274: builder.setName(new Name("all_left"));
275: Taclet allleft = builder.getAntecTaclet();
276: String allleftString = "all_left{\\find(\\forall z; b==>) \\add({\\subst z; x}b==>)}";
277: assertEquals("all-left", allleft, parseTaclet(allleftString));
278: }
279:
280: public void testExConjSplit() {
281: //exists-conj-split rule
282: //find(ex z . ( b & b0 )) varcond(z not free in b)
283: // replacewith( b & ex z.b0 )
284:
285: RewriteTacletBuilder builder = new RewriteTacletBuilder();
286: builder.setFind(parseFma("\\exists z; (b & b0)"));
287: builder.addVarsNotFreeIn((SchemaVariable) lookup_var("z"),
288: (SchemaVariable) lookup_var("b"));
289: builder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
290: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
291: parseFma("b & \\exists z; b0")));
292: builder.setName(new Name("exists_conj_split"));
293: Taclet exconjsplit = builder.getRewriteTaclet();
294: String exconjsplitString = "exists_conj_split{"
295: + "\\find(\\exists z; ( b & b0 )) \\varcond(\\notFreeIn(z, b)) \n"
296: + "\\replacewith( b & \\exists z; b0 )}";
297: assertEquals("ex-conj-split", exconjsplit,
298: parseTaclet(exconjsplitString));
299: }
300:
301: public void testFIdempotent() {
302: // f-idempotent-rule
303: // find(f(f(x))) replacewith( f(x) )
304:
305: RewriteTacletBuilder builder = new RewriteTacletBuilder();
306:
307: builder.setFind(parseTerm("f(f(x))"));
308: builder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(
309: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST,
310: parseTerm("f(x)")));
311: builder.setName(new Name("f_idempotent"));
312: Taclet fidempotent = builder.getRewriteTaclet();
313: String fidempotentString = "f_idempotent{\\find(f(f(x))) \\replacewith(f(x))}";
314: assertEquals("f-idempotent", fidempotent,
315: parseTaclet(fidempotentString));
316: }
317:
318: public void testMakeInsertEq() {
319: // make-insert-eq rule
320: // find (x = x0 =>) addrules ( find (x) replacewith (x0) )
321: RewriteTacletBuilder insertbuilder = new RewriteTacletBuilder();
322: insertbuilder.setFind(parseTerm("x"));
323: insertbuilder
324: .addTacletGoalTemplate(new RewriteTacletGoalTemplate(
325: Sequent.EMPTY_SEQUENT,
326: SLListOfTaclet.EMPTY_LIST, parseTerm("x0")));
327: insertbuilder.setName(new Name("insert_eq"));
328: Taclet inserteq = insertbuilder.getTaclet();
329:
330: AntecTacletBuilder builder = new AntecTacletBuilder();
331:
332: builder.setFind(parseFma("x=x0"));
333: builder.addTacletGoalTemplate(new TacletGoalTemplate(
334: Sequent.EMPTY_SEQUENT, SLListOfTaclet.EMPTY_LIST
335: .prepend(inserteq)));
336: builder.setName(new Name("make_insert_eq"));
337: Taclet makeinserteq = builder.getAntecTaclet();
338: String makeinserteqString = "make_insert_eq"
339: + "{\\find (x = x0 ==>)"
340: + "\\addrules ( insert_eq{\\find (x) \\replacewith (x0)} )}";
341: assertEquals("make-insert-eq", makeinserteq,
342: parseTaclet(makeinserteqString));
343: }
344:
345: public void testSchemaJava0() {
346:
347: parseTaclet("while_right { \\find (\\<{.. while(#e2) {#p1} ...}\\>post)"
348: + "\\replacewith (\\<{.. #unwind-loop (#inner, #outer, while(#e2) {#p1}); ...}\\>post) } ");
349:
350: }
351:
352: public void testSchemaJava4() {
353: FindTaclet taclet = (FindTaclet) parseTaclet("variable_declaration{ \\find (\\<{.. #typ #v0; ...}\\>post)"
354: + " \\replacewith (\\<{.. #typ #v0; if (true); ...}\\>post) }");
355: Term find = taclet.find();
356: JavaBlock jb = find.javaBlock();
357:
358: ContextStatementBlock ct = (ContextStatementBlock) jb.program();
359: LocalVariableDeclaration lvd = (LocalVariableDeclaration) ct
360: .getChildAt(0);
361: VariableSpecification vs = (VariableSpecification) lvd
362: .getChildAt(1);
363:
364: }
365:
366: public void testVarcondNew() {
367: FindTaclet taclet = (FindTaclet) parseTaclet("xy{ \\find (true) \\varcond(\\new(#boolv,s)) \\replacewith(true)}");
368:
369: taclet = (FindTaclet) parseTaclet("xy{ \\find (true) \\varcond (\\new(#v0, \\typeof(#e2))) \\replacewith(true)}");
370:
371: }
372:
373: public void testSchemaJava6() {
374: FindTaclet taclet = (FindTaclet) parseTaclet("xy{ \\find (\\<{.. boolean #boolv; ...}\\>post)"
375: + " \\replacewith (\\<{.. if (true); ...}\\>post) }");
376: Term find = taclet.find();
377: JavaBlock jb = find.javaBlock();
378:
379: ContextStatementBlock ct = (ContextStatementBlock) jb.program();
380: LocalVariableDeclaration lvd = (LocalVariableDeclaration) ct
381: .getChildAt(0);
382: VariableSpecification vs = (VariableSpecification) lvd
383: .getChildAt(1);
384: }
385:
386: public void testSchemaJava8() {
387: FindTaclet taclet = (FindTaclet) parseTaclet("break_test {\\find(\\<{.. #lb0:{ break #lb1; } ...}\\>post)"
388: + " \\replacewith (\\<{.. ...}\\>post)}");
389: Term find = taclet.find();
390: JavaBlock jb = find.javaBlock();
391: ContextStatementBlock ct = (ContextStatementBlock) jb.program();
392: }
393:
394: public void testSchemaJava10() {
395: FindTaclet taclet = (FindTaclet) parseTaclet("array_test {\\find(\\<{..#arr[#e][#e2]=#e2;...}\\>true) \\replacewith (true)}");
396: Term find = taclet.find();
397: JavaBlock jb = find.javaBlock();
398: ContextStatementBlock ct = (ContextStatementBlock) jb.program();
399: CopyAssignment ca = (CopyAssignment) ct.getChildAt(0);
400: ArrayReference ar = (ArrayReference) ca.getChildAt(0);
401: for (int i = 0; i < 2; i++) {
402: assertTrue(ar.getChildAt(i) != null);
403: }
404: ar = (ArrayReference) ar.getChildAt(0);
405: for (int i = 0; i < 2; i++) {
406: assertTrue(ar.getChildAt(i) != null);
407: }
408: }
409:
410: public void testSchemaJava11() {
411: FindTaclet taclet = (FindTaclet) parseTaclet("eval_order_array_access_right{"
412: + " \\find(\\<{..#v=#ar[#e];...}\\>post)"
413: + "\\varcond(\\new(#ar1,\\typeof(#ar)),"
414: + "\\new(#v0,\\typeof(#e)), \\new(#k, \\typeof(#e)))"
415: + "\\replacewith(\\<{..for(#k=0;#k<#length-reference(#ar);#k++){"
416: + "#ar1[#k]=#ar[#k];}"
417: + "#v0=#e; #v=#ar1[#v0];...}\\>post)"
418: + "\\displayname \"eval_order_array_access_right\"};");
419: }
420:
421: public void testFreeReplacewithVariables() {
422: // broken taclet with free variable SV in replacewith
423: // buggy { find(==>b) replacewith(==>b,z=z) }
424:
425: String brokenTacletString = "buggy { \\find(==>b)"
426: + "\\replacewith(==>b,z=z) }";
427: boolean builderExceptionThrown = false;
428: try {
429: stringTacletParser(brokenTacletString).taclet(
430: SetAsListOfChoice.EMPTY_SET);
431: } catch (Exception e) {
432: assertTrue("Expected IllegalArgumentException, but got "
433: + e, e instanceof IllegalArgumentException);
434: builderExceptionThrown = true;
435: }
436: assertTrue("Expected the taclet builder to throw an exception "
437: + "because of free variables in replacewith",
438: builderExceptionThrown);
439: }
440:
441: //Following tests should work, if parser didn't exit system but propagated
442: // exceptions until here.
443:
444: public void testSchemaJava1() {
445: boolean thrown = false;
446: try {
447: parseTaclet("xyz { find (<{.. int j=0; for(#i;j<9;j++)"
448: + "; ...}>post)"
449: + "replacewith (<{.. #unwind-loop (while(#e2) {#p1});"
450: + " ...}>post) } ");
451: } catch (RuntimeException e) {
452: thrown = true;
453: }
454: assertTrue("forinit only valid in initializer of for", thrown);
455: }
456:
457: public void testSchemaJava2() {
458: boolean thrown = false;
459: try {
460: parseTaclet("xyz { find (<{.. int j=0; for(#lab;j<42;j++) ; ...}>post)"
461: + "replacewith (<{.. #unwind-loop (while(#e2) {#p1}); ...}>post) } ");
462: } catch (RuntimeException e) {
463: thrown = true;
464: }
465: assertTrue("label SV not valid here", thrown);
466: }
467:
468: //more SchemaJava tests are in ../rule/TestMatchTaclet
469:
470: }
|