0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: package de.uka.ilkd.key.visualdebugger;
0009:
0010: import java.io.File;
0011: import java.io.IOException;
0012: import java.util.*;
0013:
0014: import javax.swing.SwingUtilities;
0015:
0016: import de.uka.ilkd.key.gui.KeYMediator;
0017: import de.uka.ilkd.key.gui.Main;
0018: import de.uka.ilkd.key.java.ArrayOfExpression;
0019: import de.uka.ilkd.key.java.JavaInfo;
0020: import de.uka.ilkd.key.java.ProgramElement;
0021: import de.uka.ilkd.key.java.SourceElement;
0022: import de.uka.ilkd.key.java.abstraction.ClassType;
0023: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0024: import de.uka.ilkd.key.java.declaration.ArrayOfParameterDeclaration;
0025: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
0026: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
0027: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
0028: import de.uka.ilkd.key.java.reference.ExecutionContext;
0029: import de.uka.ilkd.key.java.reference.MethodReference;
0030: import de.uka.ilkd.key.java.reference.ReferencePrefix;
0031: import de.uka.ilkd.key.java.reference.TypeRef;
0032: import de.uka.ilkd.key.java.statement.LabeledStatement;
0033: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
0034: import de.uka.ilkd.key.java.statement.MethodFrame;
0035: import de.uka.ilkd.key.java.visitor.ProgramVariableCollector;
0036: import de.uka.ilkd.key.logic.*;
0037: import de.uka.ilkd.key.logic.op.*;
0038: import de.uka.ilkd.key.pp.AbbrevMap;
0039: import de.uka.ilkd.key.pp.LogicPrinter;
0040: import de.uka.ilkd.key.pp.ProgramPrinter;
0041: import de.uka.ilkd.key.proof.*;
0042: import de.uka.ilkd.key.proof.init.InitConfig;
0043: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
0044: import de.uka.ilkd.key.rule.*;
0045: import de.uka.ilkd.key.strategy.DebuggerStrategy;
0046: import de.uka.ilkd.key.strategy.StrategyFactory;
0047: import de.uka.ilkd.key.strategy.StrategyProperties;
0048: import de.uka.ilkd.key.visualdebugger.executiontree.ExecutionTree;
0049: import de.uka.ilkd.key.visualdebugger.executiontree.ITNode;
0050: import de.uka.ilkd.key.visualdebugger.statevisualisation.StateVisualization;
0051: import de.uka.ilkd.key.visualdebugger.statevisualisation.SymbolicObject;
0052:
0053: public class VisualDebugger {
0054: public static final String debugClass = "Debug";
0055:
0056: private static boolean debuggingMode = false;
0057:
0058: public static final String debugPackage = "visualdebugger";
0059:
0060: static boolean keyBuggerMode;
0061:
0062: public static boolean quan_splitting = false;
0063:
0064: public static final String sepName = "sep";
0065:
0066: public static boolean showImpliciteAttr = false;
0067:
0068: public static boolean showMainWindow = false;
0069:
0070: private static VisualDebugger singleton;
0071:
0072: private static List symbolicExecNames = new ArrayList(5);
0073:
0074: public static final String tempDir = System
0075: .getProperty("user.home")
0076: + File.separator
0077: + "tmp"
0078: + File.separator
0079: + "visualdebugger" + File.separator;
0080:
0081: public static final boolean vdInDebugMode = false;
0082:
0083: private static final Name POST_PREDICATE_NAME = new Name("POST");
0084:
0085: static {
0086: symbolicExecNames.add(new Name("simplify_prog"));
0087: symbolicExecNames.add(new Name("simplify_autoname"));
0088: symbolicExecNames.add(new Name("simplify_int"));
0089: symbolicExecNames.add(new Name("simplify_object_creation"));
0090: symbolicExecNames.add(new Name("method_expand"));
0091: }
0092:
0093: public static boolean containsImplicitAttr(Term t) {
0094: if (t.op() instanceof AttributeOp
0095: && ((ProgramVariable) ((AttributeOp) t.op())
0096: .attribute()).isImplicit()
0097: || t.op() instanceof ProgramVariable
0098: && ((ProgramVariable) t.op()).isImplicit()) {
0099: return true;
0100: }
0101: for (int i = 0; i < t.arity(); i++) {
0102: if (containsImplicitAttr(t.sub(i))) {
0103: return true;
0104: }
0105: }
0106: return false;
0107: }
0108:
0109: public static String getMethodString(MethodDeclaration md) {
0110: String result = md.getProgramElementName().toString() + "( ";
0111: final ArrayOfParameterDeclaration paraDecl = md.getParameters();
0112: if (paraDecl.size() > 0) {
0113: for (int i = 0; i < paraDecl.size() - 1; i++) {
0114: result += paraDecl.getParameterDeclaration(i) + " ,";
0115: }
0116: result += paraDecl
0117: .getParameterDeclaration(paraDecl.size() - 1);
0118: }
0119: result += " )";
0120: return result;
0121:
0122: }
0123:
0124: public static VisualDebugger getVisualDebugger() {
0125: if (singleton == null) {
0126: singleton = new VisualDebugger();
0127: String[] args = new String[2];
0128:
0129: args[0] = "DEBUGGER";
0130: args[1] = "LOOP";
0131:
0132: Main.evaluateOptions(args);
0133: Main key = Main.getInstance(false);
0134: key.loadCommandLineFile();
0135:
0136: singleton.main = Main.getInstance(false);
0137: singleton.mediator = singleton.main.mediator();
0138: }
0139: return singleton;
0140: }
0141:
0142: public static boolean isDebuggingMode() {
0143: return debuggingMode;
0144: }
0145:
0146: public static void print(Object o) {
0147: if (vdInDebugMode)
0148: System.out.println(o.toString());
0149: }
0150:
0151: public static void print(String s) {
0152: if (vdInDebugMode)
0153: System.out.println(s);
0154: }
0155:
0156: public static void setDebuggingMode(boolean mode) {
0157: debuggingMode = mode;
0158: }
0159:
0160: private BreakpointManager bpManager;
0161:
0162: private StateVisualization currentState;
0163:
0164: private ITNode currentTree;
0165:
0166: private ProgramMethod debuggingMethod;
0167:
0168: private boolean initPhase = false;
0169:
0170: private HashMap inputPV2term = new HashMap();
0171:
0172: private LinkedList listeners = new LinkedList();
0173:
0174: private Main main;
0175:
0176: protected int maxProofStepsForStateVisComputation = 8000;
0177:
0178: // InteractiveProver ip;
0179: private KeYMediator mediator;
0180:
0181: private Sequent precondition;
0182:
0183: private int runLimit = 5;
0184:
0185: private ProgramVariable selfPV;
0186:
0187: private boolean staticMethod;
0188:
0189: private ListOfTerm symbolicInputValuesAsList = SLListOfTerm.EMPTY_LIST;
0190:
0191: private HashMap tc2node = new HashMap();
0192:
0193: private HashMap term2InputPV = new HashMap();
0194:
0195: private ClassType type;
0196:
0197: private boolean useDecisionProcedures = false;
0198:
0199: private Function postPredicate;
0200:
0201: protected VisualDebugger() {
0202: bpManager = new BreakpointManager(this );
0203:
0204: // main = Main.getInstance();
0205: }
0206:
0207: public void addListener(DebuggerListener listener) {
0208: listeners.add(listener);
0209: }
0210:
0211: public void addTestCase(String file, String method, Node n) {
0212: tc2node.put(new TestCaseIdentifier(file, method), n);
0213:
0214: }
0215:
0216: public ListOfProgramVariable arrayOfExpression2ListOfProgVar(
0217: ArrayOfExpression aoe, int start) {
0218: ListOfProgramVariable lopv = SLListOfProgramVariable.EMPTY_LIST;
0219: for (int i = start; i < aoe.size(); i++) {
0220: lopv = lopv.append((ProgramVariable) aoe.getExpression(i));
0221: }
0222: return lopv;
0223: }
0224:
0225: private ListOfTerm collectResult(Sequent s) {
0226: IteratorOfConstrainedFormula itc = s.antecedent().iterator();
0227: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
0228: while (itc.hasNext()) {
0229: result = result.append(itc.next().formula());
0230: }
0231: itc = s.succedent().iterator();
0232: while (itc.hasNext()) {
0233: result = result.append(TermFactory.DEFAULT
0234: .createJunctorTerm(Op.NOT, itc.next().formula()));
0235: }
0236:
0237: return result;
0238: }
0239:
0240: private boolean contains(ArrayOfExpression aoe, ProgramVariable pv) {
0241: for (int i = 0; i < aoe.size(); i++) {
0242: if (aoe.getExpression(i) == pv) {
0243: return true;
0244: }
0245: }
0246: return false;
0247:
0248: }
0249:
0250: /**
0251: * determines and returns the first and active statement if the applied
0252: * taclet worked on a modality. If the applied taclet performs no symbolic
0253: * execution <tt>null</tt> is returned
0254: */
0255: public SourceElement determineFirstAndActiveStatement(Node node) {
0256: final RuleApp ruleApp = node.getAppliedRuleApp();
0257: SourceElement activeStatement = null;
0258: if (ruleApp instanceof PosTacletApp) {
0259: final PosTacletApp pta = (PosTacletApp) ruleApp;
0260: if (!isSymbolicExecution(pta.taclet())) {
0261: return null;
0262: }
0263: final Term t = pta.posInOccurrence().subTerm();
0264: final ProgramElement pe = t.executableJavaBlock().program();
0265: if (pe != null) {
0266: activeStatement = getActStatement(pe.getFirstElement());
0267: }
0268: }
0269: return activeStatement;
0270: }
0271:
0272: public void extractInput(Node n, PosInOccurrence pio) {
0273: JavaBlock jb = this .modalityTopLevel(pio);
0274: print("Extracting Symbolic Input Values-----------------------");
0275: ProgramVariable selfPV2 = null;
0276: MethodBodyStatement mbs = (MethodBodyStatement) this
0277: .getActStatement(modalityTopLevel(pio).program());
0278: ReferencePrefix ref = mbs.getMethodReference()
0279: .getReferencePrefix();
0280:
0281: if (ref instanceof ProgramVariable) {
0282: setSelfPV((ProgramVariable) ref);
0283: setStaticMethod(false);
0284: selfPV2 = (ProgramVariable) ref;
0285:
0286: print("SelfPV " + ref);
0287:
0288: } else {
0289:
0290: final KeYJavaType kjt = ((TypeRef) ref).getKeYJavaType();
0291: setStaticMethod(true);
0292: setType((ClassType) kjt.getJavaType());
0293: print("Static Method of Type " + kjt.getJavaType());
0294:
0295: }
0296:
0297: debuggingMethod = mbs.getProgramMethod(mediator.getServices());
0298: // debuggingMethod.getVariableSpecification(index)
0299:
0300: ArrayOfExpression args = mbs.getArguments();
0301: HashMap map = new HashMap();
0302: HashMap map2 = new HashMap();
0303: if (jb != null) {
0304: Term f = pio.constrainedFormula().formula();
0305: if (f.op() instanceof QuanUpdateOperator) {
0306: final QuanUpdateOperator op = (QuanUpdateOperator) f
0307: .op();
0308: for (int i = 0; i < op.locationCount(); i++) {
0309: if (op.location(f, i).op() instanceof ProgramVariable) {
0310: if (contains(args, (ProgramVariable) op
0311: .location(f, i).op())
0312: || (selfPV2 != null && selfPV2
0313: .equals(op.location(f, i).op()))) {
0314: map.put(op.value(f, i), op.location(f, i));
0315: map2.put(op.location(f, i), op.value(f, i));
0316: }
0317: }
0318: }
0319:
0320: }
0321:
0322: }
0323:
0324: // set symb input values as list;
0325: this .symbolicInputValuesAsList = SLListOfTerm.EMPTY_LIST;
0326: for (int i = 0; i < args.size(); i++) {
0327: ProgramVariable next = (ProgramVariable) args
0328: .getExpression(i);
0329: Term val = (Term) map2.get(TermFactory.DEFAULT
0330: .createVariableTerm(next));// TODO
0331: this .symbolicInputValuesAsList = this .symbolicInputValuesAsList
0332: .append(val);
0333:
0334: }
0335:
0336: setTerm2InputPV(map);
0337: setInputPV2term(map2);
0338: print("t2i " + map);
0339: print("i2t " + map2);
0340: print("Symbolic Input Values as list "
0341: + this .symbolicInputValuesAsList);
0342:
0343: }
0344:
0345: public void extractPrecondition(Node node, PosInOccurrence pio) {
0346: this .precondition = node.sequent().removeFormula(pio).sequent();
0347: }
0348:
0349: public void fireDebuggerEvent(DebuggerEvent event) {
0350: synchronized (listeners) {
0351: if (event.getType() == DebuggerEvent.TREE_CHANGED) {
0352: currentTree = (ITNode) event.getSubject();
0353: } else if (event.getType() == DebuggerEvent.VIS_STATE) {
0354: currentState = (StateVisualization) event.getSubject();
0355: }
0356:
0357: Iterator it = listeners.iterator();
0358: while (it.hasNext()) {
0359: ((DebuggerListener) it.next()).update(event);
0360: }
0361: }
0362: }
0363:
0364: private SourceElement getActStatement(SourceElement statement) {
0365: while ((statement instanceof ProgramPrefix)
0366: || statement instanceof ProgramElementName) {
0367: if (statement instanceof LabeledStatement) {
0368: statement = ((LabeledStatement) statement).getBody();
0369: } else if (statement == statement.getFirstElement()) {
0370: break;
0371: } else {
0372: statement = statement.getFirstElement();
0373: }
0374: }
0375: return statement;
0376: }
0377:
0378: public SetOfTerm getArrayIndex(PosInOccurrence pio2) {
0379: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0380: PosInOccurrence pio = pio2;
0381: if (pio.constrainedFormula().formula().op() instanceof QuanUpdateOperator) {
0382: QuanUpdateOperator op = (QuanUpdateOperator) pio
0383: .constrainedFormula().formula().op();
0384: Term f = pio.constrainedFormula().formula();
0385: for (int i = 0; i < op.locationCount(); i++) {
0386: Term t = (op.location(f, i));
0387:
0388: if (t.op() instanceof ArrayOp) {
0389: result = result.add(t.sub(1));
0390: }
0391: }
0392:
0393: } else
0394: throw new RuntimeException("Expected QuanUpd as top op");
0395: return result;
0396: }
0397:
0398: public SetOfTerm getArrayLocations(PosInOccurrence pio2) {
0399: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0400: PosInOccurrence pio = pio2;
0401: if (pio.constrainedFormula().formula().op() instanceof QuanUpdateOperator) {
0402: QuanUpdateOperator op = (QuanUpdateOperator) pio
0403: .constrainedFormula().formula().op();
0404: Term f = pio.constrainedFormula().formula();
0405: for (int i = 0; i < op.locationCount(); i++) {
0406: Term t = (op.location(f, i));
0407:
0408: if (t.op() instanceof ArrayOp) {
0409: result = result.add(t);
0410: }
0411: }
0412:
0413: } else
0414: throw new RuntimeException("Expected QuanUpd as top op");
0415: return result;
0416: }
0417:
0418: public BreakpointManager getBpManager() {
0419: return bpManager;
0420: }
0421:
0422: public StateVisualization getCurrentState() {
0423: return currentState;
0424: }
0425:
0426: public ITNode getCurrentTree() {
0427: return ExecutionTree.getITNode();
0428: }
0429:
0430: public ProgramMethod getDebuggingMethod() {
0431: return debuggingMethod;
0432: }
0433:
0434: public PosInOccurrence getExecutionTerminatedNormal(Node n) {
0435: final Sequent s = n.sequent();
0436: for (IteratorOfConstrainedFormula it = s.succedent().iterator(); it
0437: .hasNext();) {
0438: ConstrainedFormula cfm = it.next();
0439: final Term f = cfm.formula();
0440: if (f.op() instanceof QuanUpdateOperator) {
0441: final Term subOp = f.sub(f.arity() - 1);
0442: if (subOp.op() == postPredicate) {
0443: return new PosInOccurrence(cfm,
0444: PosInTerm.TOP_LEVEL, false);
0445: }
0446: }
0447: }
0448: return null;
0449: }
0450:
0451: /**
0452: * term 2 term
0453: *
0454: * @return
0455: */
0456: public HashMap getInputPV2term() {
0457: return inputPV2term;
0458: }
0459:
0460: public ListOfTerm getLocations(PosInOccurrence pio2) {
0461: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
0462: PosInOccurrence pio = pio2;
0463:
0464: if (pio.constrainedFormula().formula().op() instanceof QuanUpdateOperator) {
0465: QuanUpdateOperator op = (QuanUpdateOperator) pio
0466: .constrainedFormula().formula().op();
0467: Term f = pio.constrainedFormula().formula();
0468: for (int i = 0; i < op.locationCount(); i++) {
0469: Term t = (op.location(f, i));
0470: if (t.op() instanceof AttributeOp /*
0471: * && !((ProgramVariable)
0472: * ((AttributeOp)
0473: * t.op()).attribute()).isImplicit()
0474: */) {
0475: result = result.append(t);
0476: } else if (t.op() instanceof ProgramVariable) {
0477: final ProgramVariable pv = (ProgramVariable) t.op();
0478: KeYJavaType kjt = pv.getContainerType();
0479: if (kjt != null) {
0480: result = result.append(t);
0481: }
0482: } else if (t.op() instanceof ArrayOp) {
0483: result = result.append(t);
0484: }
0485: }
0486:
0487: } else {
0488: throw new RuntimeException("Expected QuanUpd as top op");
0489: }
0490: return result;
0491: }
0492:
0493: public KeYMediator getMediator() {
0494: return mediator;
0495: }
0496:
0497: public MethodFrame getMethodFrame(SourceElement context) {
0498: MethodFrame frame = null;
0499: if (context instanceof ProgramPrefix) {
0500: final ArrayOfProgramPrefix prefixElements = ((ProgramPrefix) context)
0501: .getPrefixElements();
0502: for (int i = 0, len = prefixElements.size(); i < len; i++) {
0503: if (prefixElements.getProgramPrefix(i) instanceof MethodFrame) {
0504: frame = (MethodFrame) prefixElements
0505: .getProgramPrefix(i);
0506: }
0507: }
0508: }
0509: return frame;
0510: }
0511:
0512: public int getMethodStackSize(Node n) {
0513: final PosInOccurrence pio = this .getProgramPIO(n.sequent());
0514: if (pio == null) {
0515: return -1;
0516: }
0517: return this .getMethodStackSize(modalityTopLevel(pio).program());
0518: }
0519:
0520: /**
0521: * computes the depth of the method frame stack up to the first active
0522: * statement
0523: */
0524: private int getMethodStackSize(SourceElement context) {
0525: int size = 0;
0526: if (context instanceof ProgramPrefix) {
0527: final ArrayOfProgramPrefix prefixElements = ((ProgramPrefix) context)
0528: .getPrefixElements();
0529: for (int i = 0, len = prefixElements.size(); i < len; i++)
0530: if (prefixElements.getProgramPrefix(i) instanceof MethodFrame) {
0531: size++;
0532: }
0533: }
0534: return size;
0535: }
0536:
0537: public Node getNodeForTC(String file, String method) {
0538: Object result = tc2node
0539: .get(new TestCaseIdentifier(file, method));
0540: if (result instanceof Node) {
0541: return (Node) result;
0542: }
0543: return null;
0544: }
0545:
0546: public HashSet getParam(MethodBodyStatement mbs) {
0547: HashSet result = new HashSet();
0548: for (int i = 0; i < mbs.getArguments().size(); i++) {
0549: result.add(mbs.getArguments().getExpression(i));
0550: }
0551: return result;
0552: }
0553:
0554: public Function getPostPredicate() {
0555: return postPredicate;
0556: }
0557:
0558: public Sequent getPrecondition() {
0559: return precondition;
0560: }
0561:
0562: public SourceElementId getProgramCounter(JavaBlock jb) {
0563: SourceElement se = getActStatement(jb.program());
0564: if (se != null && se instanceof MethodReference) {
0565: MethodReference mr = (MethodReference) se;
0566: // mr.getT
0567: if (mr.getMethodName().toString().equals(sepName)
0568: && mr.getArgumentAt(0) instanceof IntLiteral) {
0569: MethodFrame mf = getMethodFrame(jb.program());
0570: if (mf == null)
0571: return null;
0572: ExecutionContext ec = (ExecutionContext) mf
0573: .getExecutionContext();
0574: return new SourceElementId(ec.getTypeReference()
0575: .toString(),
0576: ((IntLiteral) (mr.getArgumentAt(0))).getValue());
0577: }
0578:
0579: }
0580: return null;
0581:
0582: }
0583:
0584: public SourceElementId getProgramCounter(Node n) {
0585: IteratorOfPosInOccurrence it = n.getNodeInfo()
0586: .getVisualDebuggerState().getLabels().keyIterator();
0587: JavaBlock jb = null;
0588: SourceElement se = null;
0589: while (it.hasNext()) {
0590: PosInOccurrence pio = it.next();
0591: jb = modalityTopLevel(pio); // TODO !!!!!!!!!!!!!!!!!!!!!!
0592: if (jb != null) {
0593: se = getActStatement(jb.program());
0594: break;
0595: }
0596: }
0597:
0598: if (jb != null && se != null && se instanceof MethodReference) {
0599: MethodReference mr = (MethodReference) se;
0600: if (mr.getMethodName().toString().equals(sepName)
0601: && mr.getArgumentAt(0) instanceof IntLiteral) {
0602: MethodFrame mf = getMethodFrame(jb.program());
0603: if (mf == null)
0604: return null;
0605: ExecutionContext ec = (ExecutionContext) mf
0606: .getExecutionContext();
0607: return new SourceElementId(ec.getTypeReference()
0608: .toString(),
0609: ((IntLiteral) (mr.getArgumentAt(0))).getValue());
0610: }
0611:
0612: }
0613: return null;
0614: }
0615:
0616: public SourceElementId getProgramCounter(PosInOccurrence pio) {
0617: final JavaBlock jb = modalityTopLevel(pio);
0618: if (jb != null) {
0619: return this .getProgramCounter(jb);
0620: }
0621: return null;
0622:
0623: }
0624:
0625: public PosInOccurrence getProgramPIO(Sequent s) {
0626: IteratorOfConstrainedFormula it = s.succedent().iterator();
0627: while (it.hasNext()) {
0628: PosInOccurrence pio = new PosInOccurrence(it.next(),
0629: PosInTerm.TOP_LEVEL, false);
0630:
0631: if (modalityTopLevel(pio) != null) {
0632: return pio;
0633: }
0634: }
0635: return null;
0636:
0637: }
0638:
0639: public int getRunLimit() {
0640: return runLimit;
0641: }
0642:
0643: public ProgramVariable getSelfPV() {
0644: return selfPV;
0645: }
0646:
0647: public Term getSelfTerm() {
0648: return TermFactory.DEFAULT.createVariableTerm(selfPV);
0649: }
0650:
0651: public SetOfTerm getSymbolicInputValues() {
0652: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0653: for (Iterator it = this .term2InputPV.keySet().iterator(); it
0654: .hasNext();) {
0655: result = result.add((Term) it.next());
0656: }
0657: return result;
0658:
0659: }
0660:
0661: public ListOfTerm getSymbolicInputValuesAsList() {
0662: return this .symbolicInputValuesAsList;
0663: }
0664:
0665: public HashMap getTerm2InputPV() {
0666: return term2InputPV;
0667: }
0668:
0669: public ClassType getType() {
0670: return type;
0671: }
0672:
0673: /**
0674: * @param locs
0675: * set of Terms (ops)
0676: * @return term2term
0677: */
0678: public HashMap getValuesForLocation(HashSet locs,
0679: PosInOccurrence pio) {
0680: HashMap result = new HashMap();
0681:
0682: Term f = pio.constrainedFormula().formula();
0683: if (f.op() instanceof QuanUpdateOperator) {
0684: final QuanUpdateOperator op = (QuanUpdateOperator) f.op();
0685: for (int i = 0; i < op.locationCount(); i++) {
0686: if (op.location(f, i).op() instanceof ProgramVariable) {
0687: if (locs.contains(op.location(f, i).op())
0688: || (selfPV != null && selfPV.equals(op
0689: .location(f, i).op()))) {
0690:
0691: result.put(op.location(f, i), op.value(f, i));
0692:
0693: }
0694:
0695: }
0696: }
0697:
0698: }
0699:
0700: return result;
0701: }
0702:
0703: public void initialize() {
0704:
0705: UpdateLabelListener lListener = new UpdateLabelListener();
0706: // lListener.setListeners(listeners);
0707: Goal.addRuleAppListener(lListener);
0708: mediator.setMaxAutomaticSteps(20000);
0709:
0710: // Extract ProgramVariables of the context program
0711: JavaInfo info = mediator.getServices().getJavaInfo();
0712: Set kjts = info.getAllKeYJavaTypes();
0713: // info.getKeYProgModelInfo().getMethods(ct)
0714: HashSet pvs = new HashSet();
0715: for (Iterator it = kjts.iterator(); it.hasNext();) {
0716: KeYJavaType kjt = (KeYJavaType) it.next();
0717: if (kjt.getJavaType() instanceof ClassDeclaration) {
0718: final ListOfProgramMethod methods = info
0719: .getAllProgramMethods(kjt);
0720: for (IteratorOfProgramMethod mit = methods.iterator(); mit
0721: .hasNext();) {
0722: ProgramMethod m = mit.next();
0723:
0724: if (m != null) {
0725: ProgramVariableCollector pvc = new ProgramVariableCollector(
0726: m);
0727: pvc.start();
0728: pvs.addAll(pvc.result());
0729: }
0730:
0731: }
0732: }
0733: }
0734:
0735: final Proof proof = mediator.getProof();
0736: ExecutionTree pl = new ExecutionTree(proof, mediator, true);
0737: pl.setListeners(listeners);
0738: mediator.addAutoModeListener(pl);
0739:
0740: this .initPhase = true;
0741: bpManager.setNoEx(true);
0742:
0743: postPredicate = (Function) proof.getNamespaces().functions()
0744: .lookup(POST_PREDICATE_NAME);
0745:
0746: setProofStrategy(proof, true, false);
0747: run();
0748: }
0749:
0750: public boolean isInitPhase() {
0751: return initPhase;
0752: }
0753:
0754: public boolean isSepStatement(ProgramElement pe) {
0755: if (pe instanceof MethodReference) {
0756: MethodReference mr = (MethodReference) pe;
0757: if (mr.getMethodName().toString().equals(sepName))
0758: return true;
0759:
0760: }
0761: return false;
0762:
0763: }
0764:
0765: public boolean isStaticMethod() {
0766: return staticMethod;
0767: }
0768:
0769: private boolean isSymbolicExecution(Taclet t) {
0770: ListOfRuleSet list = t.getRuleSets();
0771: RuleSet rs;
0772: while (!list.isEmpty()) {
0773: rs = list.head();
0774: Name name = rs.name();
0775: if (symbolicExecNames.contains(name))
0776: return true;
0777: list = list.tail();
0778: }
0779: return false;
0780: }
0781:
0782: public JavaBlock modalityTopLevel(PosInOccurrence pio) {
0783: Term cf = pio.constrainedFormula().formula();
0784: if (cf.arity() > 0) {
0785: // CHECK: if --> while ?
0786: if (cf.op() instanceof QuanUpdateOperator) {
0787: cf = ((QuanUpdateOperator) cf.op()).target(cf);
0788: }
0789: if (cf.op() instanceof Modality) {
0790: return cf.javaBlock();
0791: }
0792: }
0793: return null;
0794: }
0795:
0796: public String prettyPrint(ListOfTerm l) {
0797: // KeYMediator mediator=
0798: // VisualDebugger.getVisualDebugger().getMediator();
0799: final LogicPrinter lp = new DebuggerLP(
0800: new ProgramPrinter(null), mediator.getNotationInfo(),
0801: mediator.getServices(), term2InputPV);
0802:
0803: String result = "";
0804: IteratorOfTerm it = l.iterator();
0805: while (it.hasNext()) {
0806: try {
0807: lp.printTerm(it.next());
0808: } catch (IOException e) {
0809: // TODO Auto-generated catch block
0810: e.printStackTrace();
0811: }
0812: result = result + lp.toString();
0813: lp.reset();
0814: if (it.hasNext())
0815: result = result + " AND ";
0816:
0817: }
0818: mediator.getNotationInfo().setAbbrevMap(new AbbrevMap());
0819: return removeLineBreaks(result);
0820: }
0821:
0822: public String prettyPrint(ListOfTerm l, LinkedList objects,
0823: SymbolicObject this Object) {
0824: // KeYMediator mediator=
0825: // VisualDebugger.getVisualDebugger().getMediator();
0826: final LogicPrinter lp = new DebuggerLP(
0827: new ProgramPrinter(null), mediator.getNotationInfo(),
0828: mediator.getServices(), term2InputPV, objects,
0829: this Object);
0830:
0831: String result = "";
0832: IteratorOfTerm it = l.iterator();
0833: while (it.hasNext()) {
0834: try {
0835: lp.printTerm(it.next());
0836: } catch (IOException e) {
0837: // TODO Auto-generated catch block
0838: e.printStackTrace();
0839: }
0840: result = result + lp.toString();
0841: lp.reset();
0842: if (it.hasNext())
0843: result = result + " AND ";
0844:
0845: }
0846: mediator.getNotationInfo().setAbbrevMap(new AbbrevMap());
0847: return removeLineBreaks(result);
0848: }
0849:
0850: public String prettyPrint(SetOfTerm l, LinkedList objects,
0851: SymbolicObject this Object) {
0852: return prettyPrint(SLListOfTerm.EMPTY_LIST.append(l.toArray()),
0853: objects, this Object);
0854: }
0855:
0856: public String prettyPrint(Term l) {
0857: // KeYMediator mediator=
0858: // VisualDebugger.getVisualDebugger().getMediator();
0859: final LogicPrinter lp = new DebuggerLP(
0860: new ProgramPrinter(null), mediator.getNotationInfo(),
0861: mediator.getServices(), term2InputPV);
0862:
0863: String result = "";
0864:
0865: try {
0866: lp.printTerm(l);
0867: } catch (IOException e) {
0868: // TODO Auto-generated catch block
0869: e.printStackTrace();
0870: }
0871: result = result + lp.toString();
0872:
0873: mediator.getNotationInfo().setAbbrevMap(new AbbrevMap());
0874: return removeLineBreaks(result);
0875: }
0876:
0877: // TODO {u}POST, execution is finished...
0878: // alternative: { } <sep(-1);>\phi
0879:
0880: public String prettyPrint(Term l, LinkedList sos, SymbolicObject so) {
0881: final LogicPrinter lp = new DebuggerLP(
0882: new ProgramPrinter(null), mediator.getNotationInfo(),
0883: mediator.getServices(), term2InputPV, sos, so);
0884:
0885: String result = "";
0886:
0887: try {
0888: lp.printTerm(l);
0889: } catch (IOException e) {
0890: // TODO Auto-generated catch block
0891: e.printStackTrace();
0892: }
0893: result = result + lp.toString();
0894:
0895: mediator.getNotationInfo().setAbbrevMap(new AbbrevMap());
0896: return removeLineBreaks(result);
0897: }
0898:
0899: public void printTestCases() {
0900: print(this .tc2node.toString());
0901: }
0902:
0903: private void refreshRuleApps() {
0904: ListOfGoal goals = mediator.getProof().openGoals();
0905: // g.getRuleAppManager().clearCache();
0906: IteratorOfGoal it = goals.iterator();
0907: while (it.hasNext()) {
0908: Goal g = it.next();
0909: g.ruleAppIndex().clearIndexes();
0910: g.ruleAppIndex().fillCache();
0911: }
0912:
0913: }
0914:
0915: public ListOfTerm removeImplicite(ListOfTerm list) {
0916: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
0917:
0918: for (IteratorOfTerm it = list.iterator(); it.hasNext();) {
0919: final Term n = it.next();
0920: if (!VisualDebugger.containsImplicitAttr(n))
0921: result = result.append(n);
0922:
0923: }
0924: return result;
0925: }
0926:
0927: private String removeLineBreaks(String s) {
0928: return s.replace('\n', ' ');
0929: }
0930:
0931: private void removeStepOver(ListOfGoal goals) {
0932: IteratorOfGoal it = goals.iterator();
0933: while (it.hasNext()) {
0934: Node next = it.next().node();
0935: next.getNodeInfo().getVisualDebuggerState().setStepOver(-1);
0936: next.getNodeInfo().getVisualDebuggerState()
0937: .setStepOverFrom(-1);
0938: print("StepOver of " + next.serialNr() + " set to -1");
0939: }
0940:
0941: }
0942:
0943: public boolean run() {
0944: // this.refreshRuleApps();
0945: if (!mediator.autoMode()) {
0946: run(mediator.getProof().openGoals());
0947: return true;
0948: } else {
0949: return false;
0950: }
0951: }
0952:
0953: public boolean run(ListOfGoal goals) {
0954: if (!mediator.autoMode()) {
0955: this .removeStepOver(goals);
0956: this .setSteps(goals, this .runLimit);
0957: setProofStrategy(mediator.getProof(), true, false);
0958: runProver(goals);
0959: return true;
0960: }
0961: return false;
0962: }
0963:
0964: private void runProver(final ListOfGoal goals) {
0965: this .refreshRuleApps();
0966: mediator.startAutoMode(goals);
0967: }
0968:
0969: public void setInitPhase(boolean initPhase) {
0970: this .initPhase = initPhase;
0971: }
0972:
0973: public void setInputPV2term(HashMap inputPV2term) {
0974: this .inputPV2term = inputPV2term;
0975: }
0976:
0977: public void setProofStrategy(final Proof proof,
0978: boolean splittingAllowed, boolean inUpdateAndAssumes) {
0979: StrategyProperties strategyProperties = DebuggerStrategy
0980: .getDebuggerStrategyProperties(splittingAllowed,
0981: inUpdateAndAssumes, isInitPhase());
0982:
0983: final StrategyFactory factory = new DebuggerStrategy.Factory();
0984:
0985: proof.setActiveStrategy((factory.create(proof,
0986: strategyProperties)));
0987: }
0988:
0989: public void setSelfPV(ProgramVariable selfPV) {
0990: this .selfPV = selfPV;
0991: }
0992:
0993: public void setStaticMethod(boolean staticMethod) {
0994: this .staticMethod = staticMethod;
0995: }
0996:
0997: private void setStepOver(ListOfGoal goals) {
0998: IteratorOfGoal it = goals.iterator();
0999: while (it.hasNext()) {
1000: Node next = it.next().node();
1001: final int size = this .getMethodStackSize(next);
1002: next.getNodeInfo().getVisualDebuggerState().setStepOver(
1003: size);
1004: next.getNodeInfo().getVisualDebuggerState()
1005: .setStepOverFrom(next.serialNr());
1006: print("StepOver of " + next.serialNr() + " set to " + size);
1007: // nodes = nodes.prepend();
1008: }
1009:
1010: }
1011:
1012: private void setSteps(ListOfGoal goals, int steps) {
1013: IteratorOfGoal it = goals.iterator();
1014: while (it.hasNext()) {
1015: Node next = it.next().node();
1016: if (!next.root())
1017: next.parent().getNodeInfo().getVisualDebuggerState()
1018: .setStatementIdcount(steps);
1019: next.getNodeInfo().getVisualDebuggerState()
1020: .setStatementIdcount(steps);
1021: print("Steps of " + next.serialNr() + " set to " + steps);
1022: // nodes = nodes.prepend();
1023: }
1024:
1025: }
1026:
1027: public void setTerm2InputPV(HashMap inputValues) {
1028: this .term2InputPV = inputValues;
1029: }
1030:
1031: public void setType(ClassType type) {
1032: this .type = type;
1033: }
1034:
1035: public ListOfTerm simplify(ListOfTerm terms) {
1036: if (terms.size() == 0)
1037: return terms;
1038: final DebuggerPO po = new DebuggerPO("DebuggerPo");
1039: final ProofStarter ps = new ProofStarter();
1040: po.setTerms(terms);
1041:
1042: final ProofEnvironment proofEnvironment = mediator.getProof()
1043: .env();
1044: final InitConfig initConfig = proofEnvironment.getInitConfig();
1045:
1046: po.setIndices(initConfig.createTacletIndex(), initConfig
1047: .createBuiltInRuleIndex());
1048: po.setProofSettings(mediator.getProof().getSettings());
1049: po.setConfig(initConfig);
1050: po.setTerms(terms);
1051: ps.init(po);
1052:
1053: final Proof proof = ps.getProof();
1054:
1055: setProofStrategy(proof, false, false);
1056:
1057: ps.setUseDecisionProcedure(useDecisionProcedures);
1058: ps.run(proofEnvironment);
1059:
1060: setProofStrategy(proof, true, false);
1061:
1062: return collectResult(proof.openGoals().iterator().next().node()
1063: .sequent());
1064: }
1065:
1066: private void startThread(final Runnable r) {
1067: mediator.stopInterface(false);
1068: Thread appThread = new Thread() {
1069: public void run() {
1070: try {
1071: SwingUtilities.invokeAndWait(r);
1072: // worker.start();
1073: } catch (Exception e) {
1074: e.printStackTrace();
1075: }
1076: mediator.startInterface(false);
1077: mediator.setInteractive(true);
1078: print("Finished on " + Thread.currentThread());
1079: }
1080: };
1081: appThread.start();
1082: }
1083:
1084: public boolean stepInto() {
1085: return stepInto(mediator.getProof().openGoals());
1086: }
1087:
1088: public boolean stepInto(ListOfGoal goals) {
1089: return this .stepInto(goals, 1);
1090: }
1091:
1092: public boolean stepInto(ListOfGoal goals, int steps) {
1093: if (!mediator.autoMode()) {
1094: final Proof proof = mediator.getProof();
1095: removeStepOver(proof.openGoals());
1096: this .setSteps(goals, steps);
1097: setProofStrategy(proof, true, false);
1098: runProver(goals);
1099: return true;
1100: }
1101: return false;
1102: }
1103:
1104: public void stepOver() {
1105: this .stepOver(mediator.getProof().openGoals());
1106: }
1107:
1108: public void stepOver(ListOfGoal goals) {
1109: setStepOver(goals);
1110: this .setSteps(goals, runLimit);
1111: setProofStrategy(mediator.getProof(), true, false);
1112: runProver(goals);
1113: }
1114:
1115: public boolean stepToFirstSep() {
1116: if (!mediator.autoMode()) {
1117:
1118: final Proof proof = mediator.getProof();
1119: removeStepOver(proof.openGoals());
1120: setSteps(proof.openGoals(), 0);
1121: setProofStrategy(proof, true, false);
1122: runProver(proof.openGoals());
1123: return true;
1124: }
1125: return false;
1126: }
1127:
1128: public synchronized void visualize(ITNode n) {
1129: mediator = main.mediator();
1130: final ITNode node = n;
1131:
1132: final Runnable interfaceSignaller = new Runnable() {
1133: public void run() {
1134: new StateVisualization(node, mediator,
1135: maxProofStepsForStateVisComputation,
1136: useDecisionProcedures);
1137: }
1138: };
1139: startThread(interfaceSignaller);
1140: }
1141:
1142: public class TestCaseIdentifier {
1143:
1144: private final String file;
1145:
1146: private final String method;
1147:
1148: public TestCaseIdentifier(String file, String method) {
1149: this .file = file;
1150: this .method = method;
1151: }
1152:
1153: public boolean equals(Object o) {
1154: if (o instanceof TestCaseIdentifier) {
1155: TestCaseIdentifier tci = (TestCaseIdentifier) o;
1156: return file.equals(tci.getFile())
1157: && method.equals(tci.getMethod());
1158: }
1159:
1160: return false;
1161: }
1162:
1163: public String getFile() {
1164: return file;
1165: }
1166:
1167: public String getMethod() {
1168: return method;
1169: }
1170:
1171: public int hashCode() {
1172: return (method.concat(file)).hashCode();
1173: }
1174:
1175: public String toString() {
1176: return "File: " + file + " Method: " + method;
1177: }
1178: }
1179: }
|