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: package de.uka.ilkd.key.rule;
009:
010: import java.util.Iterator;
011:
012: import javax.swing.JOptionPane;
013:
014: import de.uka.ilkd.key.gui.Main;
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.java.abstraction.ArrayType;
017: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
020: import de.uka.ilkd.key.java.statement.MethodFrame;
021: import de.uka.ilkd.key.java.statement.Throw;
022: import de.uka.ilkd.key.java.visitor.ProgramContextAdder;
023: import de.uka.ilkd.key.logic.*;
024: import de.uka.ilkd.key.logic.op.*;
025: import de.uka.ilkd.key.proof.*;
026: import de.uka.ilkd.key.proof.mgt.*;
027: import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
028: import de.uka.ilkd.key.rule.updatesimplifier.Update;
029: import de.uka.ilkd.key.speclang.IteratorOfClassInvariant;
030: import de.uka.ilkd.key.speclang.SLTranslationError;
031:
032: /**
033: * implements the rule which inserts method contracts for a method body
034: * statement
035: *
036: * @author andreas
037: *
038: */
039: public class UseMethodContractRule implements BuiltInRule {
040:
041: private final Name name = new Name("Use Method Contract");
042: private final TermBuilder tb = TermBuilder.DF;
043:
044: /** The only instance of this rule */
045: public static UseMethodContractRule INSTANCE = new UseMethodContractRule();
046:
047: protected UseMethodContractRule() {
048: }
049:
050: /**
051: * returns true iff this rule is applicable at the given position, that is,
052: * if there is a contract applicable for a method body statement at that
053: * position in the specification repository belonging to the proof of the
054: * given goal. This does not necessarily mean that a rule application will
055: * change the goal (this decision is made due to performance reasons)
056: */
057: public boolean isApplicable(Goal goal, PosInOccurrence pos,
058: Constraint userConstraint) {
059: final Services services = goal.node().proof().getServices();
060: final MbsInfo mbsInfo = getMbsInfo(pos);
061:
062: return mbsInfo != null
063: && getContracts(mbsInfo.mbs.getProgramMethod(services),
064: mbsInfo.modality, services, goal.proof(), pos)
065: .size() != 0;
066: }
067:
068: /**
069: * returns the list of all program methods overriden
070: * by the given method <tt>pm</tt> inclusive <tt>pm</tt>
071: * @param pm the ProgramMethod
072: * @param services the Services
073: * @return list of all overridden methods
074: */
075: private ListOfProgramMethod getProgramMethodsInSupertypes(
076: ProgramMethod pm, Services services) {
077: final IteratorOfKeYJavaType types = services.getJavaInfo()
078: .getAllSupertypes(pm.getContainerType()).iterator();
079:
080: ListOfProgramMethod allMethods = SLListOfProgramMethod.EMPTY_LIST;
081: while (types.hasNext()) {
082: if (!(types instanceof ArrayType)) {
083: allMethods = allMethods.prepend(services.getJavaInfo()
084: .getAllProgramMethodsLocallyDeclared(
085: types.next()));
086: }
087: }
088:
089: final String pmName = pm.getMethodDeclaration().getName();
090:
091: ListOfProgramMethod result = SLListOfProgramMethod.EMPTY_LIST;
092: final IteratorOfProgramMethod it = allMethods.iterator();
093: nextOverriddenMethod: while (it.hasNext()) {
094: final ProgramMethod p = it.next();
095: if (p != pm
096: && p.getMethodDeclaration().getName()
097: .equals(pmName)
098: && p.getParameterDeclarationCount() == pm
099: .getParameterDeclarationCount()) {
100: for (int i = 0; i < p.getParameterDeclarationCount(); i++) {
101: if (p.getParameterDeclarationAt(i)
102: .getTypeReference().getKeYJavaType() != pm
103: .getParameterDeclarationAt(i)
104: .getTypeReference().getKeYJavaType()) {
105: continue nextOverriddenMethod;
106: }
107: }
108: result = result.prepend(p);
109: }
110: }
111: return result.prepend(pm);
112: }
113:
114: private static MbsInfo getMbsInfo(PosInOccurrence pio) {
115: if (pio == null || pio.isInAntec()) {
116: return null;
117: }
118:
119: Term t = pio.subTerm();
120:
121: while (t.op() instanceof IUpdateOperator) {
122: pio = pio.down(((IUpdateOperator) t.op()).targetPos());
123: t = pio.subTerm();
124: }
125:
126: if (!(t.op() instanceof Modality)) {
127: return null;
128: }
129:
130: final Modality modality = (Modality) t.op();
131: final ProgramElement pe = t.executableJavaBlock().program();
132:
133: if (pe == null) { // TODO: can this situation occurr?
134: return null;
135: }
136:
137: PosInProgram res = PosInProgram.TOP;
138: ProgramElement activeStatement = (Statement) pe;
139: ExecutionContext ec = null;
140:
141: if (activeStatement instanceof ProgramPrefix) {
142:
143: ProgramPrefix curPrefix = (ProgramPrefix) activeStatement;
144:
145: final ArrayOfProgramPrefix prefix = curPrefix
146: .getPrefixElements();
147: final int length = prefix.size();
148:
149: // fail fast check
150: curPrefix = prefix.getProgramPrefix(length - 1);// length -1 >= 0 as prefix array
151: //contains curPrefix as first element
152:
153: activeStatement = curPrefix.getFirstActiveChildPos()
154: .getProgram(curPrefix);
155:
156: if (!(activeStatement instanceof MethodBodyStatement)) {
157: return null;
158: }
159:
160: int i = length - 1;
161: do {
162: if (ec == null && curPrefix instanceof MethodFrame) {
163: ec = (ExecutionContext) ((MethodFrame) curPrefix)
164: .getExecutionContext();
165: }
166: res = curPrefix.getFirstActiveChildPos().append(res);
167: i--;
168: if (i >= 0) {
169: curPrefix = prefix.getProgramPrefix(i);
170: }
171: } while (i >= 0);
172:
173: } else if (!(activeStatement instanceof MethodBodyStatement)) {
174: return null;
175: }
176: return new MbsInfo(pio, res, ec,
177: (MethodBodyStatement) activeStatement, modality);
178: }
179:
180: /**
181: * return the set of all contracts for the given method (including
182: * the contracts of possible overriden methods) and termination marker
183: * @param pm the ProgramMethod whose contracts are collected
184: * @param modality the Modality serving as termination marker
185: * @param services the Services
186: * @return all contracts applicable for the given method
187: */
188: private ContractSet getContracts(ProgramMethod pm,
189: Modality modality, Services services, Proof proof,
190: PosInOccurrence pos) {
191:
192: ContractSet ctSet = new ContractSet();
193: IteratorOfProgramMethod it = getProgramMethodsInSupertypes(pm,
194: services).iterator();
195: while (it.hasNext()) {
196: ContractSet contracts = services
197: .getSpecificationRepository().getContract(
198: it.next(), modality);
199:
200: //prevent application of contracts with "everything" modifier sets
201: //if metavariables are involved (hackish, see Bug 810)
202: if (getAllMetavariables(pos.topLevel().subTerm()).size() > 0) {
203: Iterator it2 = contracts.iterator();
204: while (it2.hasNext()) {
205: OldOperationContract ct = (OldOperationContract) it2
206: .next();
207: if (ct
208: .createDLMethodContract(proof)
209: .getModifies()
210: .contains(
211: EverythingLocationDescriptor.INSTANCE)) {
212: it2.remove();
213: }
214: }
215: }
216:
217: ctSet.addAll(contracts);
218: }
219: return ctSet;
220: }
221:
222: /**
223: * calls the given contract configurator and returns the selected contract
224: * or creates a new DLMethodContract from the results of the
225: * configuration. The selected / configured contract suits to the given
226: * position. It is added to the proof environment of the given proof.
227: *
228: */
229: private OldOperationContract selectContract(Services services,
230: Proof proof, PosInOccurrence pos, ContractConfigurator cc,
231: boolean allowConfiguration) {
232: final SpecificationRepository repos = services
233: .getSpecificationRepository();
234: MbsInfo mbsPos = getMbsInfo(pos);
235: MethodBodyStatement mbs = mbsPos.mbs;
236: Modality modality = mbsPos.modality;
237: ProgramMethod pm = mbs.getProgramMethod(services);
238: ContractSet ctSet = getContracts(pm, modality, services, proof,
239: pos);
240: if (ctSet.size() == 0) {
241: return null;
242: }
243: cc.setSpecification(repos);
244: cc
245: .setProgramMethods(getProgramMethodsInSupertypes(pm,
246: services));
247: cc.setModality(modality);
248: cc.allowConfiguration(allowConfiguration);
249: cc.start();
250: if (!cc.wasSuccessful())
251: return null;
252: DLMethodContract dlhResultCt = null;
253: if (cc.getPreInvariants().isEmpty()
254: && cc.getPostInvariants().isEmpty()) {
255: return cc.getMethodContract();
256: } else {
257: dlhResultCt = cc.getMethodContract()
258: .createDLMethodContract(proof);
259:
260: IteratorOfClassInvariant it = cc.getPreInvariants()
261: .iterator();
262: while (it.hasNext()) {
263: try {
264: dlhResultCt.addPre(it.next().getInv(services)
265: .getFormula());
266: } catch (SLTranslationError e) {
267: // too bad (error in invariant)
268: // TODO:
269: // user should be informed about what happend here!
270: }
271: }
272: it = cc.getPostInvariants().iterator();
273: while (it.hasNext()) {
274: try {
275: dlhResultCt.addPost(it.next().getInv(services)
276: .getFormula());
277: } catch (SLTranslationError e) {
278: // too bad (error in invariant)
279: // TODO:
280: // user should be informed about what happend here!
281: }
282: }
283: dlhResultCt = (DLMethodContract) proof.env()
284: .addMethodContract(dlhResultCt);
285: }
286:
287: return dlhResultCt;
288: }
289:
290: /**
291: * calls the given contract configurator and returns the selected contract
292: * or creates a new DLMethodContract from the results of the
293: * configuration. The selected / configured contract suits to the given
294: * position. It is added to the proof environment of the given proof.
295: *
296: */
297: public OldOperationContract selectContract(Proof proof,
298: PosInOccurrence pos, ContractConfigurator cc) {
299: return selectContract(proof.getServices(), proof, pos, cc, true);
300: }
301:
302: /**
303: * calls the given contract configurator and returns the selected contract
304: * or creates a new DLMethodContract from the results of the
305: * configuration. The selected / configured contract suits to the given
306: * position. It is added to the proof environment of the given proof.
307: *
308: */
309: public OldOperationContract selectExistingContract(
310: Services services, PosInOccurrence pos,
311: ContractConfigurator cc) {
312: return selectContract(services, null, pos, cc, false);
313: }
314:
315: private OldOperationContract getSelectedMethodContract(
316: RuleApp ruleApp, Proof proof) {
317: if (ruleApp instanceof MethodContractRuleApp) {
318: // selected beforehand
319: return ((MethodContractRuleApp) ruleApp)
320: .getMethodContract();
321: }
322: return selectContract(proof, ruleApp.posInOccurrence(),
323: AutomatedContractConfigurator.INSTANCE);
324: }
325:
326: private static ProgramElementName getNewName(Services services,
327: String baseName) {
328: NamespaceSet namespaces = services.getNamespaces();
329:
330: int i = 0;
331: ProgramElementName name;
332: do {
333: name = new ProgramElementName(baseName + "_" + i++);
334: } while (namespaces.lookup(name) != null);
335:
336: return name;
337: }
338:
339: /**
340: * the rule is applied based on the information of the given rule application:
341: * if the given rule application is a
342: * {@link MethodContractRuleApp} then the contained method contract is applied,
343: * otherwise a contract is selected based on the
344: * {@link AutomatedContractConfigurator}.
345: * @param goal the goal that the rule application should refer to
346: * @param services the Services with the necessary information about
347: * the java programs
348: * @param ruleApp the rule application that is executed.
349: */
350: public ListOfGoal apply(Goal goal, Services services,
351: RuleApp ruleApp) {
352: OldOperationContract ct = getSelectedMethodContract(ruleApp,
353: goal.node().proof());
354:
355: MbsInfo mbsPos = getMbsInfo(ruleApp.posInOccurrence());
356: MethodBodyStatement mbs = mbsPos.mbs;
357: Modality modality = mbsPos.modality;
358:
359: Expression[] insts = new Expression[mbs.getArguments().size()];
360: mbs.getArguments().arraycopy(0, insts, 0,
361: mbs.getArguments().size());
362: Expression receiver = null;
363: if (mbs.getDesignatedContext() instanceof Expression) {
364: receiver = (Expression) mbs.getDesignatedContext();
365: }
366:
367: ProgramVariable resultVar = (ProgramVariable) mbs
368: .getResultVariable();
369: ProgramMethod pm = mbs.getProgramMethod(services);
370: if (resultVar == null && pm.getKeYJavaType() != null) {
371: //method is non-void, but its result is discarded; we need to create a
372: //result variable anyway
373: ProgramElementName pen = getNewName(services, "res");
374: resultVar = new LocationVariable(pen, pm.getKeYJavaType());
375: services.getNamespaces().programVariables().add(resultVar);
376: }
377:
378: MethodContractInstantiation mci = new MethodContractInstantiation(
379: receiver, insts, resultVar, modality);
380: final InstantiatedMethodContract ctInst = ct.instantiate(mci,
381: goal.node().proof());
382:
383: if (ctInst == null) {
384: return SLListOfGoal.EMPTY_LIST.prepend(goal.split(1));
385: }
386:
387: return applyInstantiatedContract(goal, ruleApp
388: .posInOccurrence(), ctInst, mbsPos, services);
389: }
390:
391: /**
392: * executes the instantiated method contract and returns the newly created goals
393: * @param goal the Goal where the method contract rule has been applies
394: * @param pos the PosInOccurunce describing the rules focus
395: * @param iCt the InstantiatedMethodContract
396: * @param mbsPos information about the method body statement on which the rule matched
397: * @param services the Services
398: * @return the new goals created by applying the method contract rule
399: */
400: private ListOfGoal applyInstantiatedContract(Goal goal,
401: PosInOccurrence pos, InstantiatedMethodContract iCt,
402: MbsInfo mbsPos, Services services) {
403:
404: services.getNamespaces().functions().add(
405: iCt.getAdditionalFunctions());
406:
407: final UpdateFactory uf = new UpdateFactory(services, goal
408: .simplifier());
409: final Update u = updateToRigid(iCt, uf, services, pos);
410:
411: final boolean openExceptionalBranch = iCt
412: .getExceptionVariable() != null;
413:
414: final ListOfGoal result = (openExceptionalBranch ? goal
415: .split(3) : goal.split(2));
416:
417: final IteratorOfGoal goalIt = result.iterator();
418:
419: if (openExceptionalBranch) {
420: openBranch(pos, iCt, mbsPos, excPostFma(iCt, mbsPos, uf, u,
421: services), goalIt.next(), getExceptionalLabel(),
422: services);
423: }
424:
425: openBranch(pos, iCt, mbsPos, postFma(iCt, mbsPos, uf, u,
426: services), goalIt.next(), getPostLabel(), services);
427:
428: openBranch(pos, iCt, mbsPos, preFma(iCt, mbsPos, uf, u,
429: services), goalIt.next(), getPreLabel(), services);
430: return result;
431: }
432:
433: /**
434: * opens a new branch with branch label <code>branchLabel</code>, replaces
435: * the formula the rule has in focus (described by <code>mbsPos</code>) by formula
436: * <code>newFormula</code>
437: * @param pos the Position of the focus term
438: * @param iCt the InstantiatedMethodContract
439: * @param mbsPos position of the method body statement (the one in focus of the rule)
440: * @param newFormula the Term with the new formula
441: * @param branchGoal the new Goal where to replace the formula
442: * @param branchLabel a String labelling the branch
443: * @param services the Services
444: */
445: private void openBranch(PosInOccurrence pos,
446: InstantiatedMethodContract iCt, MbsInfo mbsPos,
447: final Term newFormula, final Goal branchGoal,
448: String branchLabel, Services services) {
449: branchGoal.node().getNodeInfo().setBranchLabel(branchLabel);
450: replaceFormula(mbsPos.pio, branchGoal, newFormula);
451: addAdditionalProgramVariables(iCt, pos, branchGoal, services);
452: }
453:
454: /**
455: * adds and renames if necessary the newly introduced program variables to
456: * the given goal
457: * @param iCt the InstantiatedMethodContract containing a set of all newly added
458: * program variables
459: * @param pos the PosInOccurrence of the find focus
460: * @param goal the Goal
461: * @param services the Services
462: */
463: private void addAdditionalProgramVariables(
464: InstantiatedMethodContract iCt, PosInOccurrence pos,
465: Goal goal, Services services) {
466: final IteratorOfNamed it = iCt.getAdditionalProgramVariables()
467: .allElements().iterator();
468: while (it.hasNext()) {
469: final ProgramVariable next = (ProgramVariable) it.next();
470: assert !next.isMember();
471: final ProgramVariable renamed = services.getVariableNamer()
472: .rename(next, goal, pos);
473: goal.addProgramVariable(renamed);
474: }
475: }
476:
477: /**
478: * replace the formula at position <tt>pio</tt> of goal <tt>g</tt>
479: * by the new formula <tt>fma</tt>
480: * @param pio the PosInOccurrence of the formula to be replaced
481: * @param g the Goal where to replace the formula
482: * @param fma the Term that is the new formula
483: */
484: private void replaceFormula(PosInOccurrence pio, Goal g, Term fma) {
485: final ConstrainedFormula cf = pio.constrainedFormula();
486: final ConstrainedFormula newCf = new ConstrainedFormula(
487: replace(cf.formula(), fma, pio.posInTerm().iterator()),
488: cf.constraint());
489: g.changeFormula(newCf, pio);
490: }
491:
492: private Term replace(Term term, Term with, IntIterator it) {
493: if (it.hasNext()) {
494: int sub = it.next();
495: Term[] subs = new Term[term.arity()];
496: final ArrayOfQuantifiableVariable[] vars = new ArrayOfQuantifiableVariable[term
497: .arity()];
498: for (int i = 0; i < term.arity(); i++) {
499: if (i != sub) {
500: subs[i] = term.sub(i);
501: } else {
502: subs[i] = replace(term.sub(i), with, it);
503: }
504: vars[i] = term.varsBoundHere(i);
505: }
506:
507: return TermFactory.DEFAULT.createTerm(term.op(), subs,
508: vars, term.javaBlock());
509: }
510: return with;
511: }
512:
513: protected String getPreLabel() {
514: return "Pre";
515: }
516:
517: protected Term preFma(InstantiatedMethodContract iCt,
518: MbsInfo mbsPos, UpdateFactory uf, Update u,
519: Services services) {
520: return iCt.getPre();
521: }
522:
523: protected String getPostLabel() {
524: return "Post";
525: }
526:
527: protected Term postFma(InstantiatedMethodContract iCt,
528: MbsInfo mbsPos, UpdateFactory uf, Update u,
529: Services services) {
530: StatementBlock methodReplaceStatements = new StatementBlock();
531: Term extraPre;
532: if (iCt.getExceptionVariable() != null) {
533: extraPre = tb.equals(tb.var(iCt.getExceptionVariable()), tb
534: .NULL(services));
535: } else {
536: extraPre = tb.tt();
537: }
538: extraPre = tb.and(extraPre, iCt.getAtPreAxioms());
539: return postFmaHelp(iCt, mbsPos, uf, u, methodReplaceStatements,
540: extraPre);
541: }
542:
543: protected String getExceptionalLabel() {
544: return "Exceptional Post";
545: }
546:
547: protected Term excPostFma(InstantiatedMethodContract iCt,
548: MbsInfo mbsPos, UpdateFactory uf, Update u,
549: Services services) {
550:
551: final StatementBlock methodReplaceStatements = new StatementBlock(
552: new Throw(iCt.getExceptionVariable()));
553: final Term extraPre = tb.and(tb.not(tb.equals(tb.var(iCt
554: .getExceptionVariable()), tb.NULL(services))), iCt
555: .getAtPreAxioms());
556: return postFmaHelp(iCt, mbsPos, uf, u, methodReplaceStatements,
557: extraPre);
558: }
559:
560: private Term postFmaHelp(InstantiatedMethodContract iCt,
561: MbsInfo mbsPos, UpdateFactory uf, Update u,
562: StatementBlock methodReplaceStmts, Term extraPre) {
563: JavaNonTerminalProgramElement all = (JavaNonTerminalProgramElement) mbsPos.pio
564: .subTerm().javaBlock().program();
565: NonTerminalProgramElement npe = replaceStatement(all, mbsPos,
566: methodReplaceStmts);
567: Term restFma = tb.tf().createProgramTerm(iCt.getModality(),
568: JavaBlock.createJavaBlock((StatementBlock) npe),
569: mbsPos.pio.subTerm().sub(0));
570:
571: restFma = uf.apply(u, restFma);
572: final Term methodReplacement = tb.and(tb.and(extraPre, iCt
573: .getPre()), uf.apply(u, iCt.getPost()));
574: return tb.imp(methodReplacement, restFma);
575: }
576:
577: protected NonTerminalProgramElement replaceStatement(
578: JavaNonTerminalProgramElement all, MbsInfo mbsPos,
579: StatementBlock with) {
580: int lastPos = mbsPos.pos.last();
581: ContextStatementBlockInstantiation csbi = new ContextStatementBlockInstantiation(
582: mbsPos.pos, mbsPos.pos.up().down(lastPos + 1),
583: mbsPos.execContext, all);
584: final NonTerminalProgramElement npe = ProgramContextAdder.INSTANCE
585: .start(all, with, csbi);
586: return npe;
587: }
588:
589: private SetOfMetavariable getAllMetavariables(Term term) {
590: SetOfMetavariable result = SetAsListOfMetavariable.EMPTY_SET;
591:
592: if (term.op() instanceof Metavariable) {
593: result = result.add((Metavariable) term.op());
594: }
595:
596: for (int i = 0; i < term.arity(); i++) {
597: result = result.union(getAllMetavariables(term.sub(i)));
598: }
599:
600: return result;
601: }
602:
603: private Update updateToRigid(InstantiatedMethodContract iCt,
604: UpdateFactory uf, Services services, PosInOccurrence pio) {
605: SetOfMetavariable mvs = getAllMetavariables(pio.topLevel()
606: .subTerm());
607: Term[] mvTerms = new Term[mvs.size()];
608: IteratorOfMetavariable it = mvs.iterator();
609: for (int i = 0; i < mvTerms.length; i++) {
610: mvTerms[i] = TermBuilder.DF.func(it.next());
611: }
612:
613: AnonymisingUpdateFactory auf = new AnonymisingUpdateFactory(uf);
614: return auf.createAnonymisingUpdate(iCt.getModifies(), mvTerms,
615: services);
616: }
617:
618: /**
619: * returns the name of this rule
620: */
621: public Name name() {
622: return name;
623: }
624:
625: /**
626: * returns the display name of this rule
627: */
628: public String displayName() {
629: return name.toString();
630: }
631:
632: /**
633: * toString
634: */
635: public String toString() {
636: return displayName();
637: }
638:
639: /**
640: * A helper container class to store information on a method body statement
641: * @author andreas
642: *
643: */
644: protected static class MbsInfo {
645: public PosInProgram pos;
646: public ExecutionContext execContext;
647: public MethodBodyStatement mbs;
648: public Modality modality;
649: public PosInOccurrence pio;
650:
651: public MbsInfo(PosInOccurrence pio, PosInProgram pos,
652: ExecutionContext ec, MethodBodyStatement mbs,
653: Modality mod) {
654: this.pos = pos;
655: this.execContext = ec;
656: this.mbs = mbs;
657: this.modality = mod;
658: this.pio = pio;
659: }
660: }
661:
662: }
|