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: package de.uka.ilkd.key.rule.metaconstruct;
011:
012: import de.uka.ilkd.key.java.*;
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
015: import de.uka.ilkd.key.java.declaration.VariableSpecification;
016: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
017: import de.uka.ilkd.key.java.reference.ExecutionContext;
018: import de.uka.ilkd.key.java.reference.MethodReference;
019: import de.uka.ilkd.key.java.reference.TypeRef;
020: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
021: import de.uka.ilkd.key.java.statement.MethodFrame;
022: import de.uka.ilkd.key.logic.*;
023: import de.uka.ilkd.key.logic.op.*;
024: import de.uka.ilkd.key.logic.sort.Sort;
025: import de.uka.ilkd.key.logic.sort.NullSort;
026: import de.uka.ilkd.key.rule.inst.SVInstantiations;
027:
028: public class ResolveQuery extends AbstractMetaOperator {
029:
030: private Term[] addUpdatesLoc = null;
031: private Term[] addUpdatesVal = null;
032: private Term addUpdatesTarget;
033: private JavaBlock addJavaBlock = null;
034: private JavaBlock addDecls = null;
035: private Services services;
036: private TermFactory tf = TermFactory.DEFAULT;
037:
038: // private boolean stop = false;
039:
040: public ResolveQuery() {
041: super (new Name("#ResolveQuery"), 2);
042: }
043:
044: /**
045: * checks whether the top level structure of the given @link Term
046: * is syntactically valid, given the assumption that the top level
047: * operator of the term is the same as this Operator. The
048: * assumption that the top level operator and the term are equal
049: * is NOT checked.
050: * @return true iff the top level structure of
051: * the @link Term is valid.
052: */
053: public boolean validTopLevel(Term term) {
054: // a meta operator accepts almost everything
055: return term.arity() == arity();
056: }
057:
058: private ArrayOfExpression createArgumentPVs(Term t) {
059: final ProgramMethod pm = ((ProgramMethod) t.op());
060: boolean staticMethod = pm.isStatic() || pm.isConstructor();
061: Expression[] result = new Expression[t.arity()
062: - (staticMethod ? 0 : 1)];
063: for (int i = 0; i < result.length; i++) {
064: final IProgramVariable parameter = pm
065: .getVariableSpecification(i).getProgramVariable();
066: final KeYJavaType argumentType = pm.getParameterType(i);
067: result[i] = createPV(parameter.name().toString(),
068: argumentType);
069: }
070: return new ArrayOfExpression(result);
071: }
072:
073: private ArrayOfQuantifiableVariable collectFreeVariables(Term t) {
074: SetOfQuantifiableVariable qvs = t.freeVars();
075: QuantifiableVariable[] qva = new QuantifiableVariable[qvs
076: .size()];
077: IteratorOfQuantifiableVariable it = qvs.iterator();
078: for (int i = 0; it.hasNext(); i++) {
079: qva[i] = it.next();
080: }
081: return new ArrayOfQuantifiableVariable(qva);
082: }
083:
084: private ProgramVariable createPV(String name, Sort s) {
085: return createPV(name, services.getJavaInfo().getKeYJavaType(s));
086: }
087:
088: private ProgramVariable createPV(String name, KeYJavaType kjt) {
089:
090: final ProgramElementName pvname = services.getVariableNamer()
091: .getTemporaryNameProposal(name);
092:
093: return new LocationVariable(pvname, kjt);
094: }
095:
096: private Term createProgramMethodSubstitute(Term t, Term rigidResTerm) {
097: ProgramMethod pm = (ProgramMethod) t.op();
098: if (t.arity() > 0 && !pm.isStatic() && !pm.isConstructor()
099: && t.sub(0).sort() instanceof NullSort) {
100: return tf.createJunctorTerm(Op.TRUE);
101: }
102: addUpdatesLoc = new Term[t.arity()];
103: addUpdatesVal = new Term[t.arity()];
104: // the last slot is for the subterm of the update term (to
105: // be set on a higher recursion level)
106: ArrayOfExpression argPVs = createArgumentPVs(t);
107:
108: final ProgramVariable callerPV = (pm.isStatic() || pm
109: .isConstructor()) ? null : createPV("queryReceiver", t
110: .sub(0).sort());
111: // create updates
112: for (int i = 0; i < argPVs.size(); i++) {
113: addUpdatesLoc[i] = tf
114: .createVariableTerm((ProgramVariable) argPVs
115: .getExpression(i));
116: addUpdatesVal[i] = t.sub(i
117: + (pm.isStatic() || pm.isConstructor() ? 0 : 1));
118: }
119: if (!pm.isStatic() || pm.isConstructor()) {
120: addUpdatesLoc[addUpdatesLoc.length - 1] = tf
121: .createVariableTerm(callerPV);
122: addUpdatesVal[addUpdatesVal.length - 1] = t.sub(0);
123: }
124: // create java block
125: final ProgramVariable res = createPV(
126: suggestResultVariableName(pm), t.sort());
127: Statement mbs = null;
128: // = new MethodBodyStatement(pm, callerPV, res, argPVs);
129: // (for always binding dynamically)
130: if (pm.isConstructor() || pm.isStatic() || pm.isPrivate()) { //static binding
131: mbs = new MethodBodyStatement(pm, callerPV, res, argPVs);
132: } else { //dynamic binding
133: mbs = new MethodReference(argPVs, pm
134: .getProgramElementName(), callerPV);
135: mbs = new CopyAssignment(res, (Expression) mbs);
136:
137: final ExecutionContext ec;
138: if (pm.getContainerType() != null) {
139: ec = new ExecutionContext(new TypeRef(pm
140: .getContainerType()), null);
141: } else {
142: ec = services.getJavaInfo()
143: .getDefaultExecutionContext();
144: }
145: mbs = new MethodFrame(null, ec, new StatementBlock(mbs));
146:
147: }
148:
149: addJavaBlock = JavaBlock
150: .createJavaBlock(new StatementBlock(mbs));
151: // create local var declaration java block
152: LocalVariableDeclaration[] vardecls = new LocalVariableDeclaration[t
153: .arity() + 1];
154: vardecls[0] = new LocalVariableDeclaration(new TypeRef(res
155: .getKeYJavaType()), new VariableSpecification(res));
156: for (int i = 0; i < argPVs.size(); i++) {
157: ProgramVariable pv = (ProgramVariable) argPVs
158: .getExpression(i);
159: vardecls[i + 1] = new LocalVariableDeclaration(new TypeRef(
160: pv.getKeYJavaType()), new VariableSpecification(pv));
161: }
162: if (!(pm.isStatic() || pm.isConstructor())) {
163: vardecls[vardecls.length - 1] = new LocalVariableDeclaration(
164: new TypeRef(callerPV.getKeYJavaType()),
165: new VariableSpecification(callerPV));
166: }
167: addDecls = JavaBlock.createJavaBlock(new StatementBlock(
168: vardecls));
169: Term resTerm = tf.createVariableTerm(res);
170: Term eq1 = tf.createEqualityTerm(resTerm, rigidResTerm);
171: Term result = tf.createBoxTerm(addJavaBlock, eq1);
172: if (addUpdatesLoc != null && addUpdatesLoc.length > 0) {
173: addUpdatesTarget = result;
174: result = tf.createUpdateTerm(addUpdatesLoc, addUpdatesVal,
175: addUpdatesTarget);
176: }
177: if (addDecls != null) {
178: result = tf.createDiamondTerm(addDecls, result);
179: }
180: ArrayOfQuantifiableVariable qvs = collectFreeVariables(t);
181: if (qvs.size() > 0) {
182: result = tf.createQuantifierTerm(Op.ALL, qvs, result);
183: }
184: return result;
185: }
186:
187: /**
188: * generates a proposal for naming the result variable depending on the
189: * methods name
190: * @param pm the ProgramMethod
191: */
192: private String suggestResultVariableName(ProgramMethod pm) {
193: String resultVarName = pm.getName();
194:
195: final String[] commonQueryPrefix = new String[] { "is", "has",
196: "get" };
197: for (int i = 0; i < commonQueryPrefix.length; i++) {
198: if (resultVarName.startsWith(commonQueryPrefix[i])) {
199: if (resultVarName.length() > commonQueryPrefix[i]
200: .length()) {
201: resultVarName = resultVarName.substring(
202: commonQueryPrefix[i].length())
203: .toLowerCase();
204: }
205: break;
206: }
207: }
208: return resultVarName;
209: }
210:
211: /** calculates the resulting term. */
212: public Term calculate(Term term, SVInstantiations svInst,
213: Services services) {
214: this .services = services;
215: return createProgramMethodSubstitute(term.sub(0), term.sub(1));
216: }
217:
218: public Sort sort(Term[] term) {
219: return Sort.FORMULA;
220: }
221: }
|