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.soundness;
012:
013: import org.apache.log4j.Logger;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.logic.IteratorOfNamed;
017: import de.uka.ilkd.key.logic.Namespace;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.logic.TermFactory;
020: import de.uka.ilkd.key.logic.op.Op;
021: import de.uka.ilkd.key.rule.ListOfTacletApp;
022: import de.uka.ilkd.key.rule.SLListOfTacletApp;
023: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
024: import de.uka.ilkd.key.rule.TacletApp;
025:
026: public class POBuilder {
027:
028: private final TacletApp app;
029: private final Namespace functions;
030: private final Namespace variables;
031: private final Services services;
032:
033: private ListOfTacletApp taclets;
034: private Term meaningTerm;
035: private Term poTerm;
036: private int numberOfPOParts = 0;
037:
038: private JumpStatementPrefixes jsp;
039: private ProgramVariablePrefixes pvp;
040: private RawProgramVariablePrefixes rpvp;
041:
042: private boolean contextFitting;
043:
044: private final Logger logger = Logger
045: .getLogger("key.taclet_soundness");
046:
047: public POBuilder(TacletApp p_app, Services p_services) {
048: app = p_app;
049: services = p_services;
050: poTerm = null;
051: functions = new Namespace();
052: variables = new Namespace();
053: taclets = SLListOfTacletApp.EMPTY_LIST;
054: }
055:
056: public void build() {
057: buildMeaningTerm();
058:
059: SkolemSet ss = new SkolemSet.DefaultSkolemSet(getTacletApp(),
060: getMeaningTerm());
061:
062: buildContext(ss);
063: }
064:
065: private void buildContext(SkolemSet p_ss) {
066: SkolemBuilder sb = new ContextSkolemBuilder(p_ss, getServices());
067: IteratorOfSkolemSet it = sb.build();
068:
069: while (it.hasNext()) {
070: contextFitting = false;
071:
072: buildLabels(it.next());
073:
074: if (contextFitting)
075: // It's not necessary to use different result types
076: // for the method frame, so we just use the first one
077: // leading to correct results
078: break;
079: }
080: }
081:
082: private void buildLabels(SkolemSet p_ss) {
083: SkolemBuilder sb = new LabelSkolemBuilder(p_ss, getServices());
084: IteratorOfSkolemSet it = sb.build();
085:
086: while (it.hasNext())
087: buildLogicVariables(it.next());
088: }
089:
090: private void buildLogicVariables(SkolemSet p_ss) {
091: SkolemBuilder sb = new LogicVariableSkolemBuilder(p_ss,
092: getServices());
093: IteratorOfSkolemSet it = sb.build();
094:
095: while (it.hasNext())
096: buildPartitioning(it.next());
097: }
098:
099: private void buildPartitioning(SkolemSet p_ss) {
100: p_ss = collectPrefixes(p_ss);
101:
102: SkolemBuilder sb = new SVPartitioningBuilder(p_ss,
103: getRawProgramVariablePrefixes(), getServices());
104: IteratorOfSkolemSet it = sb.build();
105:
106: while (it.hasNext())
107: buildTypeInfos(it.next());
108: }
109:
110: private void buildTypeInfos(SkolemSet p_ss) {
111: SkolemBuilder sb = new TypeInfoBuilder(p_ss,
112: getRawProgramVariablePrefixes(), getServices());
113: IteratorOfSkolemSet it = sb.build();
114:
115: while (it.hasNext())
116: buildProgramVariables(it.next());
117: }
118:
119: private void buildProgramVariables(SkolemSet p_ss) {
120: SkolemBuilder sb = new ProgramVariableSkolemBuilder(p_ss,
121: getRawProgramVariablePrefixes(), getServices());
122: IteratorOfSkolemSet it = sb.build();
123:
124: while (it.hasNext()) {
125: final SkolemSet ss = it.next();
126: instantiatePrefixes(ss);
127: buildFunctions(ss);
128: }
129: }
130:
131: private void buildFunctions(SkolemSet p_ss) {
132: SkolemBuilder sb = new FunctionSkolemBuilder(getTacletApp()
133: .taclet(), p_ss, getProgramVariablePrefixes(),
134: getServices());
135: IteratorOfSkolemSet it = sb.build();
136:
137: while (it.hasNext())
138: buildStatements(it.next());
139: }
140:
141: private void buildStatements(SkolemSet p_ss) {
142: SkolemBuilder sb = new StatementSkolemBuilder(p_ss,
143: getProgramVariablePrefixes(),
144: getJumpStatementPrefixes(), getServices());
145: IteratorOfSkolemSet it = sb.build();
146:
147: while (it.hasNext())
148: buildExpressions(it.next());
149: }
150:
151: private void buildExpressions(SkolemSet p_ss) {
152: SkolemBuilder sb = new ExpressionSkolemBuilder(p_ss,
153: getProgramVariablePrefixes(),
154: getJumpStatementPrefixes(), getServices());
155: IteratorOfSkolemSet it = sb.build();
156:
157: while (it.hasNext())
158: addPOPart(it.next());
159: }
160:
161: private void buildMeaningTerm() {
162: final MeaningFormulaBuilder b = new MeaningFormulaBuilder(
163: getTacletApp());
164:
165: meaningTerm = b.build();
166: logger.debug("Meaning formula: " + meaningTerm);
167: }
168:
169: private void addPOPart(SkolemSet p_skolemSet) {
170: contextFitting = true;
171: ++numberOfPOParts;
172:
173: logger.debug("addPOPart() with "
174: + p_skolemSet.getInstantiations());
175: addPOPart(createPOPart(p_skolemSet));
176:
177: copyNamespace(p_skolemSet.getFunctions(), functions);
178: copyNamespace(p_skolemSet.getVariables(), variables);
179:
180: taclets = taclets.prepend(p_skolemSet.getTaclets());
181: }
182:
183: private Term createPOPart(SkolemSet p_skolemSet) {
184: SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
185: getServices(), p_skolemSet.getInstantiations());
186: p_skolemSet.getFormula().execPostOrder(srv);
187:
188: return srv.getTerm();
189: }
190:
191: private void addPOPart(Term p_formula) {
192: if (poTerm == null)
193: poTerm = p_formula;
194: else
195: poTerm = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
196: p_formula, poTerm);
197: }
198:
199: private SkolemSet collectPrefixes(SkolemSet p_ss) {
200: SVPrefixCollectorSVI c = new SVPrefixCollectorSVI(p_ss
201: .getInstantiations(), p_ss.getSVTypeInfos(),
202: getServices());
203: c.collect(p_ss.getFormula());
204: jsp = c.getJumpStatementPrefixes();
205: rpvp = c.getRawProgramVariablePrefixes();
206: p_ss = p_ss.setSVTypeInfos(c.getSVTypeInfos());
207: logger.debug("Free schema variables: "
208: + rpvp.getFreeSchemaVariables());
209: logger.debug("Bound schema variables: "
210: + rpvp.getBoundSchemaVariables());
211: logger.debug("Free program variables: "
212: + rpvp.getFreeProgramVariables());
213:
214: return p_ss;
215: }
216:
217: private void instantiatePrefixes(final SkolemSet ss) {
218: pvp = getRawProgramVariablePrefixes().instantiate(
219: ss.getInstantiations());
220: logger.debug("instantiatePrefixes() with "
221: + ss.getInstantiations());
222: }
223:
224: public Namespace getFunctions() {
225: return functions;
226: }
227:
228: public Namespace getVariables() {
229: return variables;
230: }
231:
232: public ListOfTacletApp getTaclets() {
233: return taclets;
234: }
235:
236: public Term getPOTerm() {
237: if (poTerm == null)
238: return TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
239: else
240: return poTerm;
241: }
242:
243: public int getNumberOfPOParts() {
244: return numberOfPOParts;
245: }
246:
247: public TacletApp getTacletApp() {
248: return app;
249: }
250:
251: public Services getServices() {
252: return services;
253: }
254:
255: private JumpStatementPrefixes getJumpStatementPrefixes() {
256: return jsp;
257: }
258:
259: private ProgramVariablePrefixes getProgramVariablePrefixes() {
260: return pvp;
261: }
262:
263: private RawProgramVariablePrefixes getRawProgramVariablePrefixes() {
264: return rpvp;
265: }
266:
267: private Term getMeaningTerm() {
268: return meaningTerm;
269: }
270:
271: private void copyNamespace(Namespace p_source, Namespace p_target) {
272: IteratorOfNamed it = p_source.allElements().iterator();
273: while (it.hasNext())
274: p_target.add(it.next());
275: }
276: }
|