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.rule.metaconstruct;
012:
013: import java.util.Iterator;
014: import java.util.LinkedList;
015: import java.util.List;
016:
017: import de.uka.ilkd.key.java.*;
018: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
019: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
020: import de.uka.ilkd.key.java.declaration.VariableSpecification;
021: import de.uka.ilkd.key.java.expression.Literal;
022: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
023: import de.uka.ilkd.key.java.reference.*;
024: import de.uka.ilkd.key.logic.VariableNamer;
025: import de.uka.ilkd.key.logic.op.LocationVariable;
026: import de.uka.ilkd.key.logic.op.ProgramVariable;
027: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
028: import de.uka.ilkd.key.rule.inst.SVInstantiations;
029:
030: public class EvaluateArgs extends ProgramMetaConstruct {
031:
032: /** creates a typeof ProgramMetaConstruct
033: * @param expr the instance of expression contained by
034: * the meta construct
035: */
036: public EvaluateArgs(ProgramElement pe) {
037: super ("#evaluate-arguments", pe);
038: }
039:
040: public static ProgramVariable evaluate(Expression e, List l,
041: Services services, ExecutionContext ec) {
042:
043: final VariableNamer varNamer = services.getVariableNamer();
044: final KeYJavaType t = e.getKeYJavaType(services, ec);
045: final ProgramVariable pv = new LocationVariable(
046: VariableNamer.parseName(varNamer
047: .getSuggestiveNameProposalForSchemaVariable(e)),
048: t);
049:
050: l.add(new LocalVariableDeclaration(new TypeRef(t),
051: new VariableSpecification(pv, e, t)));
052: return pv;
053: }
054:
055: /** performs the program transformation needed for symbolic
056: * program execution
057: * @param services the Services with all necessary information
058: * about the java programs
059: * @param svInst the instantiations esp. of the inner and outer label
060: * @return the transformed program
061: */
062: public ProgramElement symbolicExecution(ProgramElement pe,
063: Services services, SVInstantiations svInst) {
064:
065: final ExecutionContext ec = svInst.getExecutionContext();
066:
067: MethodReference mr = (MethodReference) (pe instanceof CopyAssignment ? ((CopyAssignment) pe)
068: .getChildAt(1)
069: : pe);
070:
071: int lastNonSimple = -1;
072: boolean skip = false;
073:
074: List evalstat = new LinkedList();
075:
076: final ReferencePrefix newCalled;
077: final ReferencePrefix invocationTarget = mr
078: .getReferencePrefix();
079:
080: if (invocationTarget instanceof Expression
081: && !(invocationTarget instanceof ThisReference)) {
082: newCalled = evaluate((Expression) invocationTarget,
083: evalstat, services, ec);
084: skip = true;
085: } else {
086: newCalled = mr.getReferencePrefix();
087: }
088:
089: ArrayOfExpression args = mr.getArguments();
090: Expression[] newArgs = new Expression[args.size()];
091: for (int i = 0; i < args.size(); i++) {
092: newArgs[i] = evaluate(args.getExpression(i), evalstat,
093: services, ec);
094:
095: if (ProgramSVSort.NONSIMPLEEXPRESSION.canStandFor(args
096: .getExpression(i), ec, services)) {
097: lastNonSimple = i;
098: }
099: }
100:
101: //Optimisation: If there is a tail of simple expressions they
102: //cannot be influenced by side effects and thus need not to be
103: //evaluated. Also, literals need not to be evaluated.
104: Iterator statIt = evalstat.iterator();
105: if (skip)
106: statIt.next(); //leave the first always
107: if (statIt.hasNext()) {
108: for (int i = 0; i < args.size(); i++) {
109: Object o = statIt.next();
110: if ((args.getExpression(i) instanceof Literal)
111: || (i > lastNonSimple)) {
112: statIt.remove();
113: newArgs[i] = args.getExpression(i);
114: }
115: }
116: } // end of optimisation
117:
118: Statement[] res = new Statement[1 + evalstat.size()];
119: Iterator it = evalstat.iterator();
120:
121: for (int i = 0; i < evalstat.size(); i++) {
122: res[i] = (Statement) it.next();
123: }
124:
125: final MethodReference resMR = new MethodReference(
126: new ArrayOfExpression(newArgs), mr.getMethodName(),
127: newCalled);
128:
129: if (pe instanceof CopyAssignment) {
130: res[res.length - 1] = new CopyAssignment(
131: ((CopyAssignment) pe).getExpressionAt(0), resMR);
132: } else {
133: res[res.length - 1] = resMR;
134: }
135:
136: return new StatementBlock(res);
137: }
138:
139: }
|