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: package de.uka.ilkd.key.proof;
009:
010: import java.util.ArrayList;
011: import java.util.List;
012: import java.util.regex.Matcher;
013: import java.util.regex.Pattern;
014:
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.logic.Name;
017: import de.uka.ilkd.key.logic.ProgramPrefix;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.rule.*;
020: import de.uka.ilkd.key.visualdebugger.VisualDebuggerState;
021:
022: /**
023: * The node info object contains additional information about a node used to
024: * give user feedback. The content does not have any influence on the proof or
025: * carry something of logical value.
026: */
027: public class NodeInfo {
028:
029: /** firstStatement stripped of method frames */
030: private SourceElement activeStatement = null;
031:
032: private String branchLabel = null;
033:
034: /** flag true if the first and active statement have been determined */
035: private boolean determinedFstAndActiveStatement = false;
036:
037: /** used for proof tree annotation when applicable */
038: private SourceElement firstStatement = null;
039:
040: private String firstStatementString = null;
041:
042: /** the node this info object belongs to */
043: private final Node node;
044:
045: /** has the rule app of the node been applied interactively? */
046: private boolean interactiveApplication = false;
047:
048: // ALL fields below are for the eclipse symbolic debugger plug-in
049: // THEY HAVE TO BE MOVED OUT TO THE DEBUGGER package
050: // where a separate mapping node <-> debugger status has to be maintained
051: private final VisualDebuggerState visualDebuggerState = new VisualDebuggerState();
052:
053: public NodeInfo(Node node) {
054: this .node = node;
055: }
056:
057: private static List symbolicExecNames = new ArrayList(5);
058: static {
059: symbolicExecNames.add(new Name("simplify_prog"));
060: symbolicExecNames.add(new Name("simplify_autoname"));
061: symbolicExecNames.add(new Name("executeIntegerAssignment"));
062: symbolicExecNames.add(new Name("simplify_object_creation"));
063: }
064:
065: /**
066: * determines the first and active statement if the applied
067: * taclet worked on a modality
068: */
069: private void determineFirstAndActiveStatement() {
070: if (determinedFstAndActiveStatement)
071: return;
072: final RuleApp ruleApp = node.getAppliedRuleApp();
073: if (ruleApp instanceof PosTacletApp) {
074: PosTacletApp pta = (PosTacletApp) ruleApp;
075: if (!isSymbolicExecution(pta.taclet()))
076: return;
077: Term t = pta.posInOccurrence().subTerm();
078: final ProgramElement pe = t.executableJavaBlock().program();
079: if (pe != null) {
080: firstStatement = pe.getFirstElement();
081: firstStatementString = null;
082:
083: activeStatement = firstStatement;
084: while ((activeStatement instanceof ProgramPrefix)
085: && !(activeStatement instanceof StatementBlock)) {
086: activeStatement = activeStatement.getFirstElement();
087: }
088: }
089: determinedFstAndActiveStatement = true;
090: }
091: }
092:
093: private boolean isSymbolicExecution(Taclet t) {
094: ListOfRuleSet list = t.getRuleSets();
095: RuleSet rs;
096: while (!list.isEmpty()) {
097: rs = list.head();
098: Name name = rs.name();
099: if (symbolicExecNames.contains(name))
100: return true;
101: list = list.tail();
102: }
103: return false;
104: }
105:
106: /**
107: * returns the active statement of the JavaBlock the applied
108: * rule has been matched against or null if no rule has been applied yet
109: * or the applied rule was no taclet or program transformation rule
110: */
111: public SourceElement getActiveStatement() {
112: determineFirstAndActiveStatement();
113: return activeStatement;
114: }
115:
116: /**
117: * returns the branch label
118: */
119: public String getBranchLabel() {
120: return branchLabel;
121: }
122:
123: /**
124: * returns the name of the source file where the active statement
125: * occurs or the string <tt>NONE</tt> if the statement does not originate from a
126: * source file (e.g. created by a taclet application or part of a
127: * generated implicit method)
128: */
129: public String getExecStatementParentClass() {
130: determineFirstAndActiveStatement();
131: if (activeStatement instanceof JavaSourceElement)
132: return ((JavaSourceElement) activeStatement)
133: .getPositionInfo().getFileName();
134: return "<NONE>";
135: }
136:
137: /**
138: * returns the position of the executed statement in its source code
139: * or Position.UNDEFINED
140: */
141: public Position getExecStatementPosition() {
142: determineFirstAndActiveStatement();
143: return (activeStatement == null) ? Position.UNDEFINED
144: : activeStatement.getStartPosition();
145: }
146:
147: /**
148: * returns a string representation of the first statement or null if no such
149: * exists
150: */
151: public String getFirstStatementString() {
152: determineFirstAndActiveStatement();
153: if (firstStatement != null) {
154: if (firstStatementString == null) {
155: firstStatementString = "" + firstStatement;
156: }
157: firstStatementString = "" + activeStatement;
158: return firstStatementString;
159: }
160: return null;
161: }
162:
163: /**
164: * sets the branch label of a node. Schema variables occuring
165: * in string <tt>s</tt> are replaced by their instantiations if
166: * possible
167: * @param s the String to be set
168: */
169: public void setBranchLabel(String s) {
170: determineFirstAndActiveStatement();
171: if (s == null)
172: return;
173: RuleApp ruleApp = node.parent().getAppliedRuleApp();
174: if (ruleApp instanceof TacletApp) {
175: TacletApp tacletApp = (TacletApp) ruleApp; // XXX
176:
177: Pattern p = Pattern.compile("#\\w+");
178: Matcher m = p.matcher(s);
179: StringBuffer sb = new StringBuffer();
180: while (m.find()) {
181: String arg = m.group();
182: Object val = tacletApp.instantiations().lookupValue(
183: new Name(arg));
184: if (val == null) {
185: // chop off the leading '#'
186: String arg2 = arg.substring(1, arg.length());
187: val = tacletApp.instantiations().lookupValue(
188: new Name(arg2));
189: }
190: String res;
191: if (val == null) {
192: System.err
193: .println("No instantiation for "
194: + arg
195: + ". Probably branch label not up to date in "
196: + tacletApp.rule().name());
197: res = arg; // use sv name instead
198: } else
199: res = ProofSaver.printAnything(val, node.proof()
200: .getServices());
201: m.appendReplacement(sb, res);
202: }
203: m.appendTail(sb);
204: branchLabel = sb.toString();
205: } else {
206: branchLabel = s;
207: }
208: }
209:
210: /**
211: * parameter indicated if the rule has been applied interactively or
212: * not
213: * @param b a boolean indicating interactive application
214: */
215: public void setInteractiveRuleApplication(boolean b) {
216: interactiveApplication = b;
217: }
218:
219: /**
220: * returns true if the rule applied on this node has been performed
221: * manually by the user
222: */
223: public boolean getInteractiveRuleApplication() {
224: return interactiveApplication;
225: }
226:
227: /**
228: * returns the visual debugger state
229: * @return the visual debugger state
230: */
231: public VisualDebuggerState getVisualDebuggerState() {
232: return visualDebuggerState;
233: }
234:
235: }
|