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.strategy;
012:
013: import de.uka.ilkd.key.logic.IteratorOfNamed;
014: import de.uka.ilkd.key.logic.ListOfNamed;
015: import de.uka.ilkd.key.logic.Name;
016: import de.uka.ilkd.key.logic.NamespaceSet;
017: import de.uka.ilkd.key.proof.Proof;
018: import de.uka.ilkd.key.strategy.feature.*;
019: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
020:
021: /**
022: * Strategy tailored to VBT aimed symbolic execution.
023: */
024: public class DebuggerStrategy extends VBTStrategy {
025:
026: public static final String VISUAL_DEBUGGER_SPLITTING_RULES_KEY = "VD_SPLITTING_RULES_KEY";
027: public static final String VISUAL_DEBUGGER_IN_UPDATE_AND_ASSUMES_KEY = "VD_IN_UPDATE_AND_ASSUMES_RULES_KEY";
028: public static final String VISUAL_DEBUGGER_IN_INIT_PHASE_KEY = "VD_IN_INIT_PHASE_KEY";
029:
030: public static final String VISUAL_DEBUGGER_TRUE = "TRUE";
031: public static final String VISUAL_DEBUGGER_FALSE = "FALSE";
032:
033: public static StrategyProperties getDebuggerStrategyProperties(
034: boolean splittingRulesAllowed, boolean inUpdateAndAssumes,
035: boolean inInitPhase) {
036: final StrategyProperties res = new StrategyProperties();
037: res.setProperty(StrategyProperties.LOOP_OPTIONS_KEY,
038: StrategyProperties.LOOP_EXPAND);
039: res.setProperty(StrategyProperties.METHOD_OPTIONS_KEY,
040: StrategyProperties.METHOD_EXPAND);
041: res.setProperty(StrategyProperties.QUERY_OPTIONS_KEY,
042: StrategyProperties.QUERY_NONE);
043: res.setProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY,
044: StrategyProperties.NON_LIN_ARITH_DEF_OPS);
045:
046: res.setProperty(StrategyProperties.SPLITTING_OPTIONS_KEY,
047: StrategyProperties.SPLITTING_NORMAL);
048:
049: if (VisualDebugger.quan_splitting) {
050: res.setProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY,
051: StrategyProperties.QUANTIFIERS_INSTANTIATE);
052: } else {
053: res
054: .setProperty(
055: StrategyProperties.QUANTIFIERS_OPTIONS_KEY,
056: StrategyProperties.QUANTIFIERS_NON_SPLITTING_WITH_PROGS);
057: }
058:
059: res.setProperty(VISUAL_DEBUGGER_SPLITTING_RULES_KEY,
060: splittingRulesAllowed ? VISUAL_DEBUGGER_TRUE
061: : VISUAL_DEBUGGER_FALSE);
062:
063: res.setProperty(VISUAL_DEBUGGER_IN_UPDATE_AND_ASSUMES_KEY,
064: inUpdateAndAssumes ? VISUAL_DEBUGGER_TRUE
065: : VISUAL_DEBUGGER_FALSE);
066:
067: res.setProperty(VISUAL_DEBUGGER_IN_INIT_PHASE_KEY,
068: inInitPhase ? VISUAL_DEBUGGER_TRUE
069: : VISUAL_DEBUGGER_FALSE);
070:
071: return res;
072: }
073:
074: protected DebuggerStrategy(Proof p_proof, StrategyProperties props) {
075: super (p_proof, props);
076:
077: RuleSetDispatchFeature d = getCostComputationDispatcher();
078:
079: bindRuleSet(d, "simplify_autoname", ifZero(BreakpointFeature
080: .create(), inftyConst(), longConst(0)));
081: bindRuleSet(d, "method_expand", ifZero(BreakpointFeature
082: .create(), inftyConst(), longConst(0)));
083: bindRuleSet(d, "debugger", inftyConst());
084: bindRuleSet(d, "statement_sep", longConst(-200));
085:
086: bindRuleSet(d, "test_gen_empty_modality_hide", inftyConst());
087:
088: bindRuleSet(d, "test_gen_quan", inftyConst());
089:
090: bindRuleSet(d, "instanceof_to_exists", inftyConst());
091:
092: bindRuleSet(d, "split_cond", ifZero(LabelFeature.INSTANCE,
093: longConst(-3000), longConst(0)));
094:
095: bindRuleSet(d, "beta", ifZero(LabelFeature.INSTANCE,
096: longConst(-3000), longConst(0)));
097:
098: final NamespaceSet nss = p_proof.getNamespaces();
099:
100: assert nss != null : "Rule set namespace not available.";
101:
102: // FIXME: do not add it for each rule set add it as sum feature
103:
104: final ListOfNamed h = nss.ruleSets().allElements();
105:
106: final boolean isSplittingAllowed = props.get(
107: VISUAL_DEBUGGER_SPLITTING_RULES_KEY).equals(
108: VISUAL_DEBUGGER_TRUE);
109:
110: final boolean inUpdateAndAssumes = props.get(
111: VISUAL_DEBUGGER_IN_UPDATE_AND_ASSUMES_KEY).equals(
112: VISUAL_DEBUGGER_TRUE);
113:
114: final boolean inInitPhase = props.get(
115: VISUAL_DEBUGGER_IN_INIT_PHASE_KEY).equals(
116: VISUAL_DEBUGGER_TRUE);
117:
118: final Feature inUpdateFeature = InUpdateFeature.create(
119: isSplittingAllowed, inUpdateAndAssumes, inInitPhase);
120:
121: final IteratorOfNamed it = h.iterator();
122: while (it.hasNext()) {
123: final String ruleSetName = it.next().name().toString();
124: bindRuleSet(d, ruleSetName, ifZero(inUpdateFeature,
125: inftyConst(), longConst(0)));
126: }
127: }
128:
129: public Name name() {
130: return new Name("DebuggerStrategy");
131: }
132:
133: public static class Factory extends StrategyFactory {
134:
135: public Factory() {
136: }
137:
138: public Strategy create(Proof p_proof,
139: StrategyProperties strategyProperties) {
140:
141: injectDebuggerDefaultOptionsIfUnset(strategyProperties);
142:
143: return new DebuggerStrategy(p_proof, strategyProperties);
144: }
145:
146: private void injectDebuggerDefaultOptionsIfUnset(
147: StrategyProperties props) {
148:
149: if (!props.containsKey(VISUAL_DEBUGGER_SPLITTING_RULES_KEY)) {
150: props.put(VISUAL_DEBUGGER_SPLITTING_RULES_KEY,
151: VISUAL_DEBUGGER_TRUE);
152: }
153:
154: if (!props
155: .containsKey(VISUAL_DEBUGGER_IN_UPDATE_AND_ASSUMES_KEY)) {
156: props.put(VISUAL_DEBUGGER_IN_UPDATE_AND_ASSUMES_KEY,
157: VISUAL_DEBUGGER_FALSE);
158: }
159:
160: if (!props.containsKey(VISUAL_DEBUGGER_IN_INIT_PHASE_KEY)) {
161: props.put(VISUAL_DEBUGGER_IN_INIT_PHASE_KEY,
162: VISUAL_DEBUGGER_TRUE);
163: }
164: }
165:
166: public Name name() {
167: return new Name("DebuggerStrategy");
168: }
169: }
170: }
|