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:
012: package de.uka.ilkd.key.logic.op;
013:
014: import java.util.HashMap;
015:
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.logic.Name;
018: import de.uka.ilkd.key.logic.Namespace;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.TermFactory;
021: import de.uka.ilkd.key.logic.ldt.LDT;
022: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.rule.MatchConditions;
025: import de.uka.ilkd.key.rule.inst.SVInstantiations;
026: import de.uka.ilkd.key.rule.metaconstruct.*;
027: import de.uka.ilkd.key.rule.metaconstruct.arith.*;
028: import de.uka.ilkd.key.util.Debug;
029:
030: /**
031: * this class implements the interface for
032: * MetaOperators. MetaOperators are used to do complex term
033: * transformation when applying a taclet. Often these transformation
034: * caanot be described with the taclet scheme (or trying to do so would
035: * result in a huge number of rules)
036: */
037: public abstract class AbstractMetaOperator extends Op implements
038: MetaOperator {
039:
040: private static HashMap name2metaop = new HashMap(70);
041:
042: public static final AbstractMetaOperator META_LENGTH = new MetaLength();
043:
044: public static final AbstractMetaOperator META_ATTRIBUTE = new MetaAttribute();
045:
046: public static final AbstractMetaOperator META_CREATED = new MetaCreated();
047:
048: public static final AbstractMetaOperator META_NEXT_TO_CREATE = new MetaNextToCreate();
049:
050: public static final AbstractMetaOperator META_TRAINITIALIZED = new MetaTraInitialized();
051:
052: public static final AbstractMetaOperator META_TRANSIENT = new MetaTransient();
053:
054: public static final AbstractMetaOperator META_TRANSACTIONCOUNTER = new MetaTransactionCounter();
055:
056: /** the shadow operator for transactions */
057: public static final AbstractMetaOperator META_SHADOW = new MetaShadow();
058:
059: /** used to add integers */
060: public static final AbstractMetaOperator META_ADD = new MetaAdd();
061:
062: public static final AbstractMetaOperator META_SUB = new MetaSub();
063:
064: public static final AbstractMetaOperator META_MUL = new MetaMul();
065:
066: public static final AbstractMetaOperator META_DIV = new MetaDiv();
067:
068: public static final AbstractMetaOperator META_LESS = new MetaLess();
069:
070: public static final AbstractMetaOperator META_GREATER = new MetaGreater();
071:
072: public static final AbstractMetaOperator META_LEQ = new MetaLeq();
073:
074: public static final AbstractMetaOperator META_GEQ = new MetaGeq();
075:
076: public static final AbstractMetaOperator META_EQ = new MetaEqual();
077:
078: public static final AbstractMetaOperator META_INT_AND = new MetaJavaIntAnd();
079:
080: public static final AbstractMetaOperator META_INT_OR = new MetaJavaIntOr();
081:
082: public static final AbstractMetaOperator META_INT_XOR = new MetaJavaIntXor();
083:
084: public static final AbstractMetaOperator META_INT_SHIFTRIGHT = new MetaJavaIntShiftRight();
085:
086: public static final AbstractMetaOperator META_INT_SHIFTLEFT = new MetaJavaIntShiftLeft();
087:
088: public static final AbstractMetaOperator META_INT_UNSIGNEDSHIFTRIGHT = new MetaJavaIntUnsignedShiftRight();
089:
090: public static final AbstractMetaOperator META_LONG_AND = new MetaJavaLongAnd();
091:
092: public static final AbstractMetaOperator META_LONG_OR = new MetaJavaLongOr();
093:
094: public static final AbstractMetaOperator META_LONG_XOR = new MetaJavaLongXor();
095:
096: public static final AbstractMetaOperator META_LONG_SHIFTRIGHT = new MetaJavaLongShiftRight();
097:
098: public static final AbstractMetaOperator META_LONG_SHIFTLEFT = new MetaJavaLongShiftLeft();
099:
100: public static final AbstractMetaOperator META_LONG_UNSIGNEDSHIFTRIGHT = new MetaJavaLongUnsignedShiftRight();
101:
102: public static final AbstractMetaOperator WHILE_INV_RULE = new WhileInvRule();
103:
104: public static final AbstractMetaOperator INTRODUCE_NEW_ANON_UPDATE = new IntroNewAnonUpdateOp();
105:
106: public static final AbstractMetaOperator ARRAY_BASE_INSTANCE_OF = new ArrayBaseInstanceOf();
107:
108: public static final AbstractMetaOperator ARRAY_STORE_STATIC_ANALYSE = new ArrayStoreStaticAnalyse();
109:
110: public static final AbstractMetaOperator EXPAND_DYNAMIC_TYPE = new ExpandDynamicType();
111:
112: public static final AbstractMetaOperator RESOLVE_QUERY = new ResolveQuery();
113:
114: public static final AbstractMetaOperator CONSTANT_VALUE = new ConstantValue();
115:
116: public static final AbstractMetaOperator UNIVERSES = new Universes();
117:
118: public static final AbstractMetaOperator DIVIDE_MONOMIALS = new DivideMonomials();
119:
120: public static final AbstractMetaOperator DIVIDE_LCR_MONOMIALS = new DivideLCRMonomials();
121:
122: public static final AbstractMetaOperator CREATE_IN_REACHABLE_STATE_PO = new CreateInReachableStatePO();
123:
124: public static final AbstractMetaOperator AT_PRE_EQUATIONS = new AtPreEquations();
125:
126: public static final AbstractMetaOperator LOCATION_DEPENDENT_FUNCTION = new LocationDependentFunction();
127:
128: /** metaconstructs for OCL simplification */
129: public static final AbstractMetaOperator METAALLSUBTYPES = new MetaAllSubtypes();
130:
131: /** metaconstruct for the updateCut rule*/
132: public static final AbstractMetaOperator METAEQUALUPDATES = new MetaEquivalentUpdates();
133:
134: public static final Sort METASORT = new PrimitiveSort(new Name(
135: "Meta"));
136:
137: protected TermFactory termFactory = TermFactory.DEFAULT;
138:
139: private int arity;
140:
141: public AbstractMetaOperator(Name name, int arity) {
142: super (name);
143: this .arity = arity;
144: name2metaop.put(name.toString(), this );
145: }
146:
147: /**
148: * checks whether the top level structure of the given @link Term
149: * is syntactically valid, given the assumption that the top level
150: * operator of the term is the same as this Operator. The
151: * assumption that the top level operator and the term are equal
152: * is NOT checked.
153: * @return true iff the top level structure of
154: * the @link Term is valid.
155: */
156: public boolean validTopLevel(Term term) {
157: // a meta operator accepts almost everything
158: return term.op() instanceof AbstractMetaOperator;
159: }
160:
161: public static MetaOperator name2metaop(String s) {
162: return (MetaOperator) name2metaop.get(s);
163: }
164:
165: /**
166: * determines the sort of the {@link Term} if it would be created using this
167: * Operator as top level operator and the given terms as sub terms. The
168: * assumption that the constructed term would be allowed is not checked.
169: * @param term an array of Term containing the subterms of a (potential)
170: * term with this operator as top level operator
171: * @return sort of the term with this operator as top level operator of the
172: * given substerms
173: */
174: public Sort sort(Term[] term) {
175: return METASORT;
176: }
177:
178: /** @return arity of the Operator as int */
179: public int arity() {
180: return arity;
181: }
182:
183: /** @return String representing a logical integer literal
184: * in decimal representation
185: */
186: public static String convertToDecimalString(Term term,
187: Services services) {
188: String result = "";
189: boolean neg = false;
190: Operator top = term.op();
191: LDT intModel = services.getTypeConverter().getIntegerLDT();
192: Namespace intFunctions = intModel.functions();
193: Operator numbers = (Operator) intFunctions
194: .lookup(new Name("Z"));
195: Operator base = (Operator) intFunctions.lookup(new Name("#"));
196: Operator minus = (Operator) intFunctions.lookup(new Name(
197: "neglit"));
198:
199: // check whether term is really a "literal"
200: if (!top.name().equals(numbers.name())) {
201: Debug.out(
202: "abstractmetaoperator: Cannot convert to number:",
203: term);
204: throw (new NumberFormatException());
205: }
206: term = term.sub(0);
207: top = term.op();
208:
209: while (top.name().equals(minus.name())) {
210: neg = !neg;
211: term = term.sub(0);
212: top = term.op();
213: }
214:
215: while (!top.name().equals(base.name())) {
216: result = top.name() + result;
217: term = term.sub(0);
218: top = term.op();
219: }
220:
221: if (neg)
222: return "-" + result;
223: else
224: return result;
225: }
226:
227: public MetaOperator getParamMetaOperator(String param) {
228: return null;
229: }
230:
231: /** (non-Javadoc)
232: * by default meta operators do not match anything
233: * @see de.uka.ilkd.key.logic.op.Operator#match(SVSubstitute, de.uka.ilkd.key.rule.MatchConditions, de.uka.ilkd.key.java.Services)
234: */
235: public MatchConditions match(SVSubstitute subst,
236: MatchConditions mc, Services services) {
237: return null;
238: }
239:
240: /** calculates the resulting term. */
241: public abstract Term calculate(Term term, SVInstantiations svInst,
242: Services services);
243:
244: }
|