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.visualization;
0009:
0010: import java.util.*;
0011:
0012: import de.uka.ilkd.key.java.*;
0013: import de.uka.ilkd.key.java.reference.IExecutionContext;
0014: import de.uka.ilkd.key.java.reference.MethodReference;
0015: import de.uka.ilkd.key.java.statement.BranchStatement;
0016: import de.uka.ilkd.key.java.statement.LoopStatement;
0017: import de.uka.ilkd.key.java.statement.MethodFrame;
0018: import de.uka.ilkd.key.java.visitor.JavaASTWalker;
0019: import de.uka.ilkd.key.logic.*;
0020: import de.uka.ilkd.key.logic.op.*;
0021: import de.uka.ilkd.key.logic.sort.AbstractSort;
0022: import de.uka.ilkd.key.logic.sort.Sort;
0023: import de.uka.ilkd.key.proof.IteratorOfNode;
0024: import de.uka.ilkd.key.proof.Node;
0025: import de.uka.ilkd.key.proof.ProgVarReplacer;
0026: import de.uka.ilkd.key.rule.*;
0027: import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
0028: import de.uka.ilkd.key.rule.inst.SVInstantiations;
0029: import de.uka.ilkd.key.rule.metaconstruct.ResolveQuery;
0030: import de.uka.ilkd.key.rule.metaconstruct.WhileInvRule;
0031: import de.uka.ilkd.key.util.ExtList;
0032:
0033: public class SimpleVisualizationStrategy implements
0034: VisualizationStrategy {
0035:
0036: static boolean DEBUG = false;
0037:
0038: /** used to extract branch labels
0039: */
0040: private static final String LOOP_INVARIANT_PROPOSAL_RULESET = "loop_invariant_proposal";
0041:
0042: private Services services;
0043:
0044: public SimpleVisualizationStrategy() {
0045: }
0046:
0047: public SimpleVisualizationStrategy(Services serv) {
0048: this .services = serv;
0049: }
0050:
0051: private void computeAdditionalInformation(TraceElement te) {
0052: ContextTraceElement currentHe = firstSourceTraceElement(te);
0053: while (currentHe != TraceElement.END) {
0054: computeNumberUnwindings(currentHe);
0055: setLabel(currentHe);
0056: currentHe = currentHe.getNextExecuted();
0057: }
0058: }
0059:
0060: /** Computes how often the statement of cte was unwound.
0061: * For details see minor thesis Proof Visualization.
0062: */
0063: private void computeNumberUnwindings(ContextTraceElement cte) {
0064: if (cte.getParent() != TraceElement.PARENTROOT
0065: && cte.getParent().getSrcElement() instanceof LoopStatement) {
0066: final PositionInfo pos = cte.getSrcElement()
0067: .getPositionInfo();
0068: final ContextTraceElement[] children = cte.getParent()
0069: .getChildren();
0070:
0071: int n = 0;
0072: for (int i = 0; i < children.length; i++) {
0073: if (pos.equals(children[i].getSrcElement()
0074: .getPositionInfo())) {
0075: n++;
0076: }
0077: if (children[i] == cte) {
0078: break;
0079: }
0080: }
0081: cte.setNumberOfExecutions(n);
0082:
0083: } else {
0084: cte.setNumberOfExecutions(1);
0085: }
0086: }
0087:
0088: /** Computes the associations stepInto and parent of an execution trace model,
0089: * that starts with the TraceElement te
0090: * For details see minor thesis Proof Visualization, Chapter Building
0091: * the Execution Trace Model
0092: */
0093:
0094: private void computeStepIntoAndParent(TraceElement te) {
0095: LinkedList stack = new LinkedList();
0096: stack.add(TraceElement.PARENTROOT);
0097:
0098: ContextTraceElement cte = firstSourceTraceElement(te);
0099:
0100: while (cte != TraceElement.END) {
0101: ParentContextTraceElement currentParent = (ParentContextTraceElement) stack
0102: .getFirst();
0103:
0104: while (currentParent != TraceElement.PARENTROOT
0105: && !contains(currentParent, cte)) {
0106: stack.removeFirst();
0107: currentParent.setStepOver(cte);
0108: currentParent = (ParentContextTraceElement) stack
0109: .getFirst();
0110: }
0111:
0112: cte.setParent(currentParent);
0113:
0114: if (cte instanceof ParentContextTraceElement) {
0115: ((ParentContextTraceElement) cte)
0116: .setStepOver(TraceElement.END);
0117: stack.addFirst(cte);
0118: }
0119:
0120: cte = cte.getNextExecuted();
0121: }
0122: }
0123:
0124: private boolean contains(ParentContextTraceElement pcte,
0125: ContextTraceElement cte) {
0126:
0127: final ProgramElement p1 = pcte.getProgram();
0128: final ProgramElement p2 = cte.getProgram();
0129:
0130: if (getMethodStackSize(p1) >= getMethodStackSize(p2)) {
0131: // per definition a statement does not contain itself
0132: if (pcte.getSrcElement().getPositionInfo().equals(
0133: cte.getSrcElement().getPositionInfo())) {
0134: return false;
0135: }
0136:
0137: final StatementByPositionWalker walker = new StatementByPositionWalker(
0138: (ProgramElement) pcte.getSrcElement(), cte
0139: .getSrcElement().getPositionInfo());
0140: walker.start();
0141:
0142: return walker.getResult() != null;
0143: }
0144:
0145: return true;
0146: }
0147:
0148: /** @return the number of Java blocks in the term t */
0149:
0150: private int countJavaBlocks(Term t) {
0151: int p = 0;
0152: if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
0153: p++;
0154: }
0155: for (int i = 0; i < t.arity(); i++) {
0156: p = p + countJavaBlocks(t.sub(i));
0157: }
0158: return p;
0159: }
0160:
0161: /**
0162: * @param t term
0163: * @param inst instantions
0164: * @return the number of java blocks in the term t instatiated with inst
0165: */
0166:
0167: private int countJavaBlocksWithSV(Term t, SVInstantiations inst) {
0168: return countJavaBlocks(syntacticalReplace(t, services, inst));
0169: }
0170:
0171: /** creates the visualization model for a node by
0172: * extracting the execution traces and building the
0173: * execution trace models
0174: */
0175: public VisualizationModel createVisualizationModel(Node node) {
0176: return createVisualizationModel(node, new HashSet(), false);
0177: }
0178:
0179: /** creates the visualization model for a node by
0180: * extracting the execution traces and building the
0181: * execution trace models
0182: */
0183: public VisualizationModel createVisualizationModel(Node node,
0184: HashSet ignoreNodes, boolean ignoreAntec) {
0185: Node currentNode = node;
0186: LinkedList executionTraceModelsList = new LinkedList();
0187: boolean jbInLastNode = false;
0188:
0189: // traces of the modalities in Node node
0190: if (getJavaBlocks(currentNode.sequent(), ignoreAntec).length > 0) {
0191: Occ[] javaBlocks = getJavaBlocks(currentNode.sequent(),
0192: ignoreAntec);
0193: jbInLastNode = true;
0194: for (int i = 0; i < javaBlocks.length; i++) {
0195: ExecutionTraceModel etm = getExecutionTraceModel(
0196: currentNode, javaBlocks[i],
0197: ExecutionTraceModel.TYPE1);
0198: if (etm != null) {
0199: executionTraceModelsList.add(etm);
0200: }
0201: }
0202: }
0203:
0204: // traces of modalities that ended "on the way" to Node node
0205: while (!currentNode.root()
0206: && !ignoreNodes.contains(currentNode)) {
0207: final LinkedList types = new LinkedList();
0208: final Occ[] ends = getTraceEnds(currentNode, types);
0209: for (int i = 0; i < ends.length; i++) {
0210: print("Node " + currentNode.parent().serialNr() + " ",
0211: ends[i]);
0212: final ExecutionTraceModel etm = getExecutionTraceModel(
0213: currentNode.parent(), ends[i], (Integer) types
0214: .get(i));
0215:
0216: if (etm != null) {
0217: etm.setTerminated(!jbInLastNode);
0218: executionTraceModelsList.add(etm);
0219: }
0220: }
0221: ignoreNodes.add(currentNode);
0222: currentNode = currentNode.parent();
0223: }
0224:
0225: final ExecutionTraceModel[] exTraceModels = removeRedundandTraces((ExecutionTraceModel[]) executionTraceModelsList
0226: .toArray(new ExecutionTraceModel[executionTraceModelsList
0227: .size()]));
0228:
0229: printTraces(exTraceModels);
0230:
0231: return new VisualizationModel(node, exTraceModels);
0232: }
0233:
0234: /**
0235: * Computes the execution trace for the Java block occurrence occ in the
0236: * sequent of Node n
0237: */
0238:
0239: private ExecutionTraceModel extractExecutionTrace(Node node,
0240: Occ occ, Integer type) {
0241: TraceElement firstTraceElement = null;
0242: TraceElement lastTraceElement = TraceElement.END;
0243: TraceElement lastSource = null;
0244: ContextTraceElement lastExecuted = TraceElement.END;
0245:
0246: print("------------- Creating Trace ");
0247: print("");
0248:
0249: TraceElement te;
0250: long rating = 0;
0251:
0252: Node currentNode = node;
0253: Occ currentJB = occ;
0254: while (!currentNode.root()) {
0255:
0256: Occ result = new Occ(false, -1, -1);
0257: boolean inTrace = occInParent(currentNode, currentJB,
0258: result);
0259: currentJB = result;
0260:
0261: if (result.cfm == -1) {
0262: break;
0263: }
0264: currentNode = currentNode.parent();
0265: print("--");
0266: if (inTrace) {
0267: print("ACTIVE STATEMENT IN EXECUTION TRACE");
0268: final PosTacletApp pta = (PosTacletApp) currentNode
0269: .getAppliedRuleApp();
0270: final ContextInstantiationEntry cie = pta
0271: .instantiations().getContextInstantiation();
0272: final SourceElement actStatement = getActStatement(currentNode);
0273: if (isContextStatement(actStatement)) {
0274: rating++;
0275: if (!isParentContextTE(actStatement)) {
0276: te = new ContextTraceElement(actStatement,
0277: currentNode, lastTraceElement,
0278: lastExecuted, getExecutionContext(cie
0279: .contextProgram()));
0280: } else {
0281: te = new ParentContextTraceElement(
0282: actStatement, currentNode,
0283: lastTraceElement, lastExecuted, null,
0284: getExecutionContext(cie
0285: .contextProgram()));
0286: }
0287: // sets contextStatement
0288: final MethodFrame frame = getMethodFrame(cie
0289: .contextProgram());
0290:
0291: if (frame != null
0292: && frame.getProgramMethod() != null) {
0293: final StatementBlock methodBody = frame
0294: .getProgramMethod().getBody();
0295: if (methodBody != null) {
0296: StatementByPositionWalker w = new StatementByPositionWalker(
0297: methodBody, actStatement
0298: .getPositionInfo());
0299: w.start();
0300: if (w.getResult() != null) {
0301: ((ContextTraceElement) te)
0302: .setContextStatement(w
0303: .getResult());
0304: }
0305: }
0306: }
0307:
0308: if (lastSource == null) {
0309: lastSource = te;
0310: }
0311: } else {
0312: te = new TraceElement(actStatement, currentNode,
0313: lastTraceElement, lastExecuted,
0314: getExecutionContext(cie.contextProgram()));
0315: }
0316: if (firstTraceElement == null) {
0317: firstTraceElement = te;
0318: }
0319:
0320: lastTraceElement = te;
0321:
0322: if (te instanceof ContextTraceElement) {
0323: lastExecuted = (ContextTraceElement) te;
0324: }
0325: }
0326: }
0327:
0328: if (lastTraceElement != TraceElement.END) {
0329: return new ExecutionTraceModel(lastTraceElement,
0330: firstTraceElement,
0331: (ContextTraceElement) lastSource, rating,
0332: currentNode, node, type, occ);
0333: }
0334: return null;
0335: }
0336:
0337: /**
0338: * @param ant
0339: * determines if t occures in the antecedent or succedent in a
0340: * formula
0341: * @param cfm position of <tt>t</tt>'s enclosing constrained formula
0342: *
0343: * @param t
0344: * the term
0345: * @param pos
0346: * offset that is added to the occurrences, needed for recursion
0347: * @return a list containing the occurrences of the java blocks in the term
0348: */
0349: private LinkedList findJavaBlocks(boolean ant, int cfm, Term t,
0350: int pos) {
0351: LinkedList ll = new LinkedList();
0352:
0353: int p = pos;
0354: if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
0355: ll.add(new Occ(ant, cfm, p));
0356: p++;
0357: }
0358:
0359: for (int i = 0; i < t.arity(); i++) {
0360: final LinkedList ll2 = findJavaBlocks(ant, cfm, t.sub(i), p);
0361: p += ll2.size();
0362: ll.addAll(ll2);
0363: }
0364:
0365: return ll;
0366: }
0367:
0368: private ContextTraceElement firstSourceTraceElement(TraceElement te) {
0369: if (te instanceof ContextTraceElement) {
0370: return (ContextTraceElement) te;
0371: } else {
0372: return te.getNextExecuted();
0373: }
0374: }
0375:
0376: private SourceElement getActStatement(Node n) {
0377: SourceElement statement = n.getNodeInfo().getActiveStatement();
0378: while ((statement instanceof ProgramPrefix)
0379: || statement instanceof ProgramElementName) {
0380: if (statement == statement.getFirstElement()) {
0381: break;
0382: }
0383: statement = statement.getFirstElement();
0384: }
0385: return statement;
0386: }
0387:
0388: private IExecutionContext getExecutionContext(SourceElement cp) {
0389: MethodFrame frame = getMethodFrame(cp);
0390: if (frame != null) {
0391: return frame.getExecutionContext();
0392: }
0393: return null;
0394: }
0395:
0396: private ExecutionTraceModel getExecutionTraceModel(Node node,
0397: Occ javaBlock, Integer type) {
0398: print("-------------------------------");
0399: print("Extracting Execution Trace Model for Node "
0400: + node.serialNr() + " and ", javaBlock);
0401:
0402: final ExecutionTraceModel trace = extractExecutionTrace(node,
0403: javaBlock, type);
0404: if (trace == null) {
0405: return null;
0406: }
0407:
0408: computeStepIntoAndParent(trace.getFirstTraceElement());
0409: computeAdditionalInformation(trace.getFirstTraceElement());
0410:
0411: return trace;
0412: }
0413:
0414: /**
0415: * @param n Node
0416: * @return the goal template that yields to node n
0417: */
0418:
0419: private TacletGoalTemplate getGoalTemplate(Node n) {
0420: final Node parent = n.parent();
0421:
0422: final int nodeIndex = parent == null ? -1 : parent
0423: .getChildNr(n);
0424:
0425: if (nodeIndex != -1) {
0426: // if parent is null then nodeIndex has been set to -1 and
0427: // this branch is not entered
0428: if (parent.getAppliedRuleApp() instanceof TacletApp) {
0429: final ListOfTacletGoalTemplate l = ((TacletApp) parent
0430: .getAppliedRuleApp()).taclet().goalTemplates();
0431: final TacletGoalTemplate[] gt = l.toArray();
0432: if (gt == null || gt.length == 0) {
0433: return null;
0434: }
0435: return gt[gt.length - nodeIndex - 1];
0436: }
0437: }
0438: print(
0439: "Proof Visualization WARNING: "
0440: + "Could not find goal template that yields to sequent of node ",
0441: n.serialNr());
0442: return null;
0443: }
0444:
0445: /** @return an array containing the occurrences of the Java
0446: * blocks in the sequent
0447: */
0448: private Occ[] getJavaBlocks(Sequent sequent, boolean ignoreAntec) {
0449: LinkedList list = new LinkedList();
0450:
0451: final IteratorOfConstrainedFormula iterator = sequent
0452: .succedent().iterator();
0453: for (int i = 0; iterator.hasNext(); i++) {
0454: list.addAll(findJavaBlocks(false, i, iterator.next()
0455: .formula(), 0));
0456: }
0457:
0458: if (!ignoreAntec) {
0459: final IteratorOfConstrainedFormula antec = sequent
0460: .antecedent().iterator();
0461: for (int i = 0; antec.hasNext(); i++) {
0462: list.addAll(findJavaBlocks(true, i, antec.next()
0463: .formula(), 0));
0464: }
0465: }
0466:
0467: return (Occ[]) list.toArray(new Occ[list.size()]);
0468: }
0469:
0470: /**
0471: * collects all occurrences of schema variables or program blocks
0472: * that occur in the given goal template in linear order
0473: * @see #getList(Term)
0474: * @param tgt the TacletGoalTemplate
0475: * @return all occurrences of schema variables or program blocks
0476: * that occur in the given goal template in linear order
0477: */
0478: private ExtList getList(TacletGoalTemplate tgt) {
0479: ExtList templateList = new ExtList();
0480:
0481: List sequents = new LinkedList();
0482:
0483: if (tgt instanceof RewriteTacletGoalTemplate) {
0484: templateList
0485: .addAll(getList(((RewriteTacletGoalTemplate) tgt)
0486: .replaceWith()));
0487: } else if (tgt instanceof AntecSuccTacletGoalTemplate) {
0488: sequents.add(((AntecSuccTacletGoalTemplate) tgt)
0489: .replaceWith());
0490: }
0491:
0492: assert tgt.sequent() != null : "Sequent should always be != null";
0493:
0494: sequents.add(tgt.sequent());
0495:
0496: for (Iterator sequentIt = sequents.iterator(); sequentIt
0497: .hasNext();) {
0498: final Sequent seq = (Sequent) sequentIt.next();
0499: final IteratorOfConstrainedFormula it = seq.iterator();
0500: while (it.hasNext()) {
0501: templateList.addAll(getList(it.next().formula()));
0502: }
0503: }
0504: return templateList;
0505: }
0506:
0507: /**
0508: * returns all occurrences of schema variables or program blocks in the
0509: * given term <tt>t</tt> in linear order
0510: *
0511: * @param t the term to be linearized
0512: * @return a list of all schema variable and Java blocks that occur in t
0513: * Example: \< int i;\> sv
0514: * --> [int i;, sv]
0515: */
0516: private ExtList getList(Term t) {
0517: final Operator op = t.op();
0518: ExtList result = new ExtList();
0519:
0520: if (op instanceof Modality || op instanceof ModalOperatorSV) {
0521: result.add(t.javaBlock());
0522: }
0523:
0524: if (op instanceof SchemaVariable) {
0525: result.add(op);
0526: }
0527:
0528: for (int i = 0; i < t.arity(); i++) {
0529: result.addAll(getList(t.sub(i)));
0530: }
0531:
0532: return result;
0533: }
0534:
0535: /**
0536: * returns the inner most method frame of the abstract syntax tree
0537: * <tt>context</tt>
0538: * @param context the SourceElement
0539: */
0540: private MethodFrame getMethodFrame(SourceElement context) {
0541: SourceElement se = context;
0542: MethodFrame frame = null;
0543:
0544: if (se instanceof MethodFrame) {
0545: frame = (MethodFrame) se;
0546: }
0547:
0548: while (se != se.getFirstElement()) {
0549: se = se.getFirstElement();
0550: if (se instanceof MethodFrame) {
0551: frame = (MethodFrame) se;
0552: }
0553: }
0554: return frame;
0555: }
0556:
0557: /**
0558: * computes the depth of the method frame stack up to the first active
0559: * statement
0560: */
0561: private int getMethodStackSize(SourceElement context) {
0562: SourceElement se = context;
0563: int size = 0;
0564: if (se instanceof MethodFrame) {
0565: size++;
0566: }
0567: while (se != se.getFirstElement()) {
0568: se = se.getFirstElement();
0569: if (se instanceof MethodFrame) {
0570: size++;
0571: }
0572: }
0573: return size;
0574: }
0575:
0576: /**
0577: * formula whose index in the parent node of <tt>n</tt> is
0578: * <tt>indexInParent</tt> was not added to sequent of node n and
0579: * is not the result of replacing or rewriting a formula,
0580: * so it occurs in the parent node.
0581: * @return the index of the formula in the parent node.
0582: * See minor thesis Proof Visualization for details.
0583: */
0584: private int getIndexOfUnchangedFormula(Node n, boolean antec,
0585: int indexInParent) {
0586:
0587: Semisequent parentSemi, semi;
0588:
0589: if (antec) {
0590: parentSemi = n.parent().sequent().antecedent();
0591: semi = n.sequent().antecedent();
0592: } else {
0593: parentSemi = n.parent().sequent().succedent();
0594: semi = n.sequent().succedent();
0595: }
0596:
0597: if (indexInParent < 0 || indexInParent >= semi.size()) {
0598: return -1;
0599: }
0600: return indexOf(rename(parentSemi, n.getRenamingTable()), semi
0601: .get(indexInParent));
0602: }
0603:
0604: /**
0605: * computes the occurrence of the formula in the sequent of node
0606: * <tt>n</tt>, which has been in the focus of the rule application
0607: * performed at node <tt>n</tt>
0608: * @param n the Node
0609: * @return the occurrence of the focus formula in the sequent of node n
0610: */
0611:
0612: private Occ getOccOfFind(Node n) {
0613: if (!(n.getAppliedRuleApp() instanceof PosTacletApp)) {
0614: return null;
0615: }
0616: final PosInOccurrence pio = ((PosTacletApp) n
0617: .getAppliedRuleApp()).posInOccurrence();
0618:
0619: final Semisequent semisequent;
0620:
0621: if (pio.isInAntec()) {
0622: semisequent = n.sequent().antecedent();
0623: } else {
0624: semisequent = n.sequent().succedent();
0625: }
0626:
0627: final int formulaIndex = semisequent.indexOf(pio
0628: .constrainedFormula());
0629: final int jb = getSubformulaOccurrence(pio.constrainedFormula()
0630: .formula(), pio.posInTerm().iterator());
0631:
0632: return new Occ(pio.isInAntec(), formulaIndex, jb);
0633: }
0634:
0635: /**
0636: *
0637: * @param t
0638: * @param inst
0639: * @return the occurrence of the first Java block in the instantiation of
0640: * term t
0641: */
0642: private int getOccurrenceOfJavaBlock(Term t, SVInstantiations inst) {
0643: int p = 0;
0644: final Iterator it = getList(t).iterator();
0645: while (it.hasNext()) {
0646: final Object next = it.next();
0647: int jbs = 0;
0648: if (next instanceof SchemaVariable) {
0649: Object instantiation = inst
0650: .getInstantiation((SchemaVariable) next);
0651: if (instantiation instanceof Term) {
0652: jbs = countJavaBlocks((Term) instantiation);
0653: }
0654: } else {
0655: return p;
0656: }
0657: p += jbs;
0658: }
0659:
0660: return -1;
0661: }
0662:
0663: /**
0664: * determines the occurrence of schemavariable <code>svToFind</code> in
0665: * the schematic term <code>t</code>.
0666: * The occurrence of schemavariable <code>svToFind</code> is here defined as
0667: * the number of java blocks of the instantiated version of term <code>t</code>
0668: * before the first time <code>svToFind</code> occurs in
0669: * <code>t</code> (linearized <code>t</code>).
0670: * For example:
0671: * <code>
0672: * #b = TRUE | <{.. #t #i; ...}>#post -> #fml | #svToFind = 3
0673: * </code>
0674: * has occurrence <code>1</coode> if the instantiations of
0675: * <code>#b,#post,#fml</code> contain no java block.
0676: *
0677: * Assumption: no metaoperators in t
0678: *
0679: * @param t the Term relative to which the occurrence of <code>svToFind</code>
0680: * (it is assumed that <code>t</code> does not contain a metaoperator) has to
0681: * be determind
0682: * @param svToFind the SchemaVariable to look for
0683: * @param inst the SVInstantiations
0684: * @return occurrence of <code>svToFind</code> in <code>t</code>
0685: */
0686: private int getOccurrenceOfSV(Term t, SchemaVariable svToFind,
0687: SVInstantiations inst) {
0688: final Iterator it = getList(t).iterator();
0689: int p = 0;
0690: while (it.hasNext()) {
0691: final Object next = it.next();
0692: int jbs = 0;
0693: if (next instanceof SchemaVariable) {
0694: final SchemaVariable sv = (SchemaVariable) next;
0695: if (sv.equals(svToFind)) {
0696: return p;
0697: } else {
0698: Object instantiation = inst.getInstantiation(sv);
0699: if (instantiation instanceof Term) {
0700: jbs = countJavaBlocks((Term) instantiation);
0701: }
0702: }
0703: } else {
0704: jbs = 1;
0705: }
0706: p += jbs;
0707: }
0708: return -1;
0709: }
0710:
0711: /**
0712: *
0713: * computes the formula index <tt>idx</tt> in node <tt>n</tt>'s
0714: * sequent for the formulas occuring in the given sequent being instantiated by
0715: * the mapping used by the taclet application in <tt>n</tt>'s parent node.
0716: *
0717: * @param schemaSeq the Sequent to be instantiated, i.e. replacewith or add sequent
0718: * in the goal template of the taclet applied at <tt>n.parent()</tt>
0719: * @param n the Node where to look for the instantiated formulas
0720: * @param antec boolean value indicating if the antec or succedent of the sequent shall
0721: * be instantiated
0722: * @param services the Services
0723: * @return a hashmap that maps the position of replaced cfm given by the index to the template
0724: * of the formula
0725: * These are the formulas that build by the part replacewith(S) where S is a sequent
0726: */
0727:
0728: private HashMap getIndexedInstantiatedFormulas(Sequent schemaSeq,
0729: Node n, boolean antec, Services services) {
0730: // index to schematic formula
0731: final HashMap index2cfm = new HashMap();
0732:
0733: final TacletApp tacletApp = (TacletApp) n.parent()
0734: .getAppliedRuleApp();
0735: final IteratorOfConstrainedFormula it = (antec ? schemaSeq
0736: .antecedent() : schemaSeq.succedent()).iterator();
0737:
0738: while (it.hasNext()) {
0739: final ConstrainedFormula cfm = it.next();
0740:
0741: final ConstrainedFormula newCfm = instantiateReplacement(
0742: cfm, tacletApp.matchConditions(), services);
0743:
0744: int index = antec ? indexOf(n.sequent().antecedent(),
0745: newCfm) : indexOf(n.sequent().succedent(), newCfm);
0746:
0747: if (index == -1) {
0748: print(
0749: "Proof Visualization WARNING: CFM INST NOT FOUND: ",
0750: cfm);
0751: print("instantiated with ", newCfm);
0752: } else {
0753: index2cfm.put(new Integer(index), cfm);
0754: }
0755: }
0756:
0757: return index2cfm;
0758:
0759: }
0760:
0761: /**
0762: * determines the index of the constrained formula in the the antecedent
0763: * (<code>antec == true</code>) or succedent (<code>antec == false</code>) of
0764: * <code>n</code> which is the result of the rewrite described by the goal template
0765: * <code>gt</code> of a formula in <code>n.parent</code>
0766: * @param gt the {@link RewriteTacletGoalTemplate} describing the rewrite
0767: * @param n the Node which resulting from an application of a taclet <code>gt</code>
0768: * belongs to and where to look for the rewritten formula
0769: * @param antec a boolean indicating in which semisequent to look for
0770: * @param services the Services
0771: * @return the index of the reritten formula relative to the specified
0772: * semisequent or <code>-1</code> if none has been found
0773: */
0774: private int getIndexedInstantiatedRewrittenFormula(
0775: RewriteTacletGoalTemplate gt, Node n, boolean antec,
0776: Services services) {
0777:
0778: final TacletApp tacletApp = ((TacletApp) n.parent()
0779: .getAppliedRuleApp());
0780: final PosInOccurrence posOfFind = tacletApp.posInOccurrence();
0781:
0782: if (posOfFind.isInAntec() != antec) {
0783: print("nothing rewritten in the semisequent");
0784: return -1;
0785: }
0786:
0787: final MatchConditions matchCond = tacletApp.matchConditions();
0788: final PosInOccurrence flatPos = flatten(posOfFind, services);
0789:
0790: final Term term = flatPos.constrainedFormula().formula();
0791:
0792: final Term result = replace(term, gt.replaceWith(), flatPos
0793: .posInTerm().iterator(), services, matchCond
0794: .getInstantiations(), term.sort());
0795:
0796: final Semisequent semi = antec ? n.sequent().antecedent() : n
0797: .sequent().succedent();
0798:
0799: int index = indexOf(semi, new ConstrainedFormula(rename(result,
0800: n.getRenamingTable()), matchCond.getConstraint()));
0801: if (index == -1) {
0802: print("Proof Visualization WARNING: Replacewith not"
0803: + " found in node ", n.serialNr());
0804: }
0805: return index;
0806: }
0807:
0808: /**
0809: * @param t term
0810: * @param it a path to subformula in the tree representation of t
0811: * @return the number of Java blocks that occur "on the left" of
0812: * the subformula,that is given by it, in t
0813: */
0814:
0815: private int getSubformulaOccurrence(Term t, IntIterator it) {
0816: int result = 0;
0817: if (it.hasNext()) {
0818: if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
0819: result++;
0820: }
0821:
0822: int sub = it.next();
0823: for (int i = 0; i < sub; i++) {
0824: result += countJavaBlocks(t.sub(i));
0825: }
0826: result += getSubformulaOccurrence(t.sub(sub), it);
0827: }
0828: return result;
0829: }
0830:
0831: /**
0832: * @param t a schematic term
0833: * @param occ an occurrence of a Java block in the instantiated term t
0834: * @param inst the instantions
0835: * @return the occurrence of the Java block in the instantiation of a
0836: * schema variable in t or a modality
0837: * or null if there is no such schema variable or modality
0838: */
0839:
0840: private OccInSchema getSVofOcc(Term t, int occ,
0841: SVInstantiations inst) {
0842: final Operator op = t.op();
0843: if ((op instanceof ModalOperatorSV) && (occ == 0)) {
0844: // if t.javaBlock() is not a ContextStatementBlock,
0845: // the tracing ends
0846: if (isContextBlock(t.javaBlock())) {
0847: return new OccInSchema(t.javaBlock());
0848: }
0849: return null;
0850: } else if (op instanceof SchemaVariable
0851: && !(op instanceof ModalOperatorSV)) {
0852: return new OccInSchema((SchemaVariable) op, occ);
0853: } else if ((op instanceof Modality) && (occ == 0)) {
0854: // if t.javaBlock() is not a ContextStatementBlock,
0855: // the tracing ends
0856: if (isContextBlock(t.javaBlock())) {
0857: return new OccInSchema(t.javaBlock());
0858: }
0859: return null;
0860: } else {
0861:
0862: if (op instanceof Modality || op instanceof ModalOperatorSV) {
0863: occ--;
0864: }
0865:
0866: // special handling for some metaoperators
0867: if (op instanceof WhileInvRule) {
0868: if (occ == 0) {
0869: return new OccInSchema(t.javaBlock());
0870: } else if (occ == 1) {
0871: return null;
0872: } else if (occ < countJavaBlocksWithSV(t.sub(0), inst) + 1) {
0873: return new OccInSchema((SchemaVariable) t.sub(0)
0874: .sub(0).op(), occ - 2);
0875: } else {
0876: if (!(t.sub(1).op() instanceof SchemaVariable)) {
0877: // termination branch
0878: return null;
0879: }
0880: return new OccInSchema((SchemaVariable) t.sub(1)
0881: .op(), occ
0882: - countJavaBlocksWithSV(t.sub(0), inst) - 1);
0883: }
0884: } else if (op instanceof ResolveQuery) {
0885: // ResolveQuery only introduces new Java blocks
0886: return null;
0887: } else {
0888: for (int i = 0; i < t.arity(); i++) {
0889: int blocks = countJavaBlocksWithSV(t.sub(i), inst);
0890: if (blocks <= occ) {
0891: occ = occ - blocks;
0892: } else {
0893: OccInSchema result = getSVofOcc(t.sub(i), occ,
0894: inst);
0895: if (result == null) {
0896: return null;
0897: } else {
0898: if (result.isJavaBlock) {
0899: return new OccInSchema(t.javaBlock());
0900: } else {
0901: return new OccInSchema(result.sv,
0902: result.occ);
0903: }
0904: }
0905: }
0906: }
0907: }
0908: }
0909: print("Proof Visualization WARNING: Something went wrong in method getSVofOcc");
0910: return null;
0911: }
0912:
0913: /**
0914: *
0915: * @param n a node with <code>parent != null</code>
0916: * @param types
0917: * @return the occurrence of all Java blocks that occure
0918: * in the sequent of the parent of n and not in
0919: * the sequent of n
0920: */
0921: private Occ[] getTraceEnds(final Node n, LinkedList types) {
0922: LinkedList result = new LinkedList();
0923: final Node parent = n.parent();
0924:
0925: print("TraceEnds for Node " + n.serialNr() + " ----------");
0926: if (parent.getAppliedRuleApp() instanceof TacletApp) {
0927: final TacletApp tacletApp = (TacletApp) parent
0928: .getAppliedRuleApp();
0929: if (tacletApp.taclet() instanceof FindTaclet) {
0930: final TacletGoalTemplate tgt = getGoalTemplate(n);
0931: if (tgt == null) {
0932: return new Occ[0];
0933: }
0934:
0935: ExtList otherTgts = new ExtList();
0936: final IteratorOfTacletGoalTemplate it = tacletApp
0937: .taclet().goalTemplates().iterator();
0938: while (it.hasNext()) {
0939: final TacletGoalTemplate currentTgt = it.next();
0940: if (!currentTgt.equals(tgt)) {
0941: otherTgts.addAll(getList(currentTgt));
0942: }
0943: }
0944:
0945: final Term findTerm = ((FindTaclet) tacletApp.taclet())
0946: .find();
0947:
0948: ExtList templateList = getList(tgt);
0949: ExtList findList = removeCommonSVsOrPrograms(
0950: getList(findTerm), templateList);
0951:
0952: final Occ occOfFind = getOccOfFind(parent);
0953:
0954: final SVInstantiations inst = tacletApp
0955: .instantiations();
0956: final Iterator findIterator = findList.iterator();
0957: while (findIterator.hasNext()) {
0958: Object current = findIterator.next();
0959: if (current instanceof SchemaVariable) {
0960: SchemaVariable sv = (SchemaVariable) current;
0961: int occOfSV = getOccurrenceOfSV(findTerm, sv,
0962: inst);
0963: if (occOfSV > -1
0964: && inst.getInstantiation(sv) instanceof Term) {
0965:
0966: int jbCount = countJavaBlocks((Term) inst
0967: .getInstantiation(sv));
0968:
0969: final Integer type = otherTgts.contains(sv) ? ExecutionTraceModel.TYPE2
0970: : ExecutionTraceModel.TYPE1;
0971:
0972: for (int i = 0; i < jbCount; i++) {
0973: Occ newOcc = new Occ(occOfFind.ant,
0974: occOfFind.cfm, occOfFind.jb
0975: + occOfSV + i);
0976: result.add(newOcc);
0977: types.add(type);
0978: }
0979: }
0980: } else {
0981: result.add(occOfFind.copy());
0982: types.add(ExecutionTraceModel.TYPE1);
0983: }
0984: print("ends: ", findList);
0985: }
0986: }
0987: }
0988: return (Occ[]) result.toArray(new Occ[result.size()]);
0989: }
0990:
0991: /**
0992: * removes SVs or programs (TODO: is the implementation correct
0993: * (only remove context blocks?)) from find list
0994: * Attention: the list returned == <tt>findList</tt> (works destructively on
0995: * <tt>findList</tt>)
0996: * @param findList the List from which elements are removed
0997: * @param templateList the List where to look for common elements
0998: * @return returns findList (attention same object as first parameter)
0999: */
1000: private ExtList removeCommonSVsOrPrograms(ExtList findList,
1001: ExtList templateList) {
1002: final JavaBlock first = (JavaBlock) findList
1003: .get(JavaBlock.class);
1004: final Iterator iterator = templateList.iterator();
1005:
1006: while (iterator.hasNext()) {
1007: Object current = iterator.next();
1008: print(current);
1009: if (current instanceof SchemaVariable) {
1010: if (findList.contains(current)) {
1011: findList.remove(current);
1012: }
1013: } else {
1014: JavaBlock jb = (JavaBlock) current;
1015: if ((first != null) && isContextBlock(jb)
1016: && isContextBlock(first)) {
1017: findList.remove(first);
1018: }
1019: }
1020: }
1021: return findList;
1022: }
1023:
1024: /**
1025: * @param semisequent semi
1026: * @param formula toFind that should be found in semi
1027: * @return index of the formula toFind in the semisequent semi or -1 if it
1028: * does not exist. Equality is checked modulu renamings
1029: */
1030:
1031: private int indexOf(Semisequent semi, ConstrainedFormula toFind) {
1032: final IteratorOfConstrainedFormula iterator = semi.iterator();
1033: int i = 0;
1034: while (iterator.hasNext()) {
1035: final ConstrainedFormula cfm = iterator.next();
1036: try {
1037: if (cfm.formula().equalsModRenaming(toFind.formula())) {
1038: return i;
1039: }
1040: i++;
1041: } catch (Exception e) {
1042: return i;
1043: }
1044: }
1045: return -1;
1046: }
1047:
1048: private ConstrainedFormula instantiateReplacement(
1049: ConstrainedFormula schemaFormula,
1050: MatchConditions matchCond, Services services) {
1051: final SVInstantiations svInst = matchCond.getInstantiations();
1052:
1053: Term replaced = syntacticalReplace(schemaFormula.formula(),
1054: services, svInst);
1055:
1056: if (!svInst.getUpdateContext().isEmpty()) {
1057: replaced = TermFactory.DEFAULT.createUpdateTerm(svInst
1058: .getUpdateContext(), replaced);
1059: }
1060:
1061: return new ConstrainedFormula(replaced, matchCond
1062: .getConstraint());
1063: }
1064:
1065: private boolean isContextBlock(JavaBlock jb) {
1066: return jb.program() instanceof ContextStatementBlock;
1067: }
1068:
1069: protected boolean isContextStatement(SourceElement s) {
1070: if (s != null) {
1071: final PositionInfo pos = s.getPositionInfo();
1072: return pos != null && pos.getFileName() != null
1073: && pos != PositionInfo.UNDEFINED
1074: && pos.getStartPosition() != null
1075: && pos.getStartPosition().getLine() > -1;
1076: }
1077: return false;
1078: }
1079:
1080: /**
1081: * @param se a SourceElement
1082: * @return true iff se is associated with a ParentContextTraceElment.
1083: * This means that se contains statements or a method invokation
1084: */
1085: private boolean isParentContextTE(SourceElement se) {
1086: if (se instanceof MethodReference
1087: || se instanceof LoopStatement
1088: || se instanceof BranchStatement) {
1089: return true;
1090: }
1091:
1092: boolean isParentContextTE = false;
1093: if (se instanceof ProgramElement) {
1094: final MethodReferenceWalker tw = new MethodReferenceWalker(
1095: (ProgramElement) se);
1096: tw.start();
1097: isParentContextTE = (tw.containsMethodRef().size() > 0);
1098: }
1099:
1100: return isParentContextTE;
1101: }
1102:
1103: /**
1104: * For details see minor thesis about Proof Visualization:
1105: * Section Extracting Execution Traces.
1106: * This method corresponds to the methods OccIn, codeTransformation
1107: * and formulaInvolved in the minor thesis.
1108: *
1109: * @param A node
1110: * @param occ a Java block occurrence in the sequent of Node n
1111: * @param newOcc the occurrence of occ in the sequent of the parent node, that
1112: * is computed by this method
1113: * @return a boolean that is true iff the java block was changed
1114: * and the occurrence result of the Java block in the parent node
1115: */
1116:
1117: private boolean occInParent(Node n, Occ occ, Occ result) {
1118:
1119: print("Node " + n.serialNr() + " Occ: ", occ);
1120: final Node parent = n.parent();
1121: final RuleApp appliedRuleApp = parent.getAppliedRuleApp();
1122:
1123: if (appliedRuleApp instanceof BuiltInRuleApp) {
1124: return indexAfterBuiltInRuleApplication(n, occ, result);
1125: }
1126:
1127: final TacletGoalTemplate tgt = getGoalTemplate(n);
1128:
1129: if (tgt == null) {
1130: print("ProofVisualization WARNING: No goal template found");
1131: result.copy(occ);
1132: return false;
1133: }
1134: print("Goal Template: ", tgt);
1135:
1136: HashMap index2cfmAnt = getIndexedInstantiatedFormulas(tgt
1137: .sequent(), n, true, services);
1138: HashMap index2cfmSuc = getIndexedInstantiatedFormulas(tgt
1139: .sequent(), n, false, services);
1140:
1141: print("Added Formulas: Ant: ", index2cfmAnt.keySet());
1142: print(" Suc:", index2cfmSuc.keySet());
1143:
1144: final Integer cfmIndexKey = new Integer(occ.cfm);
1145:
1146: if (!(appliedRuleApp instanceof PosTacletApp)) {
1147: print("NoPosTacletApp");
1148: if ((index2cfmAnt.containsKey(cfmIndexKey) && occ.ant)
1149: || (index2cfmSuc.containsKey(cfmIndexKey) && !occ.ant)) {
1150: // occ was added, tracing ends since there is no find part
1151: result.set(false, -1, -1);
1152: return false;
1153: }
1154: // otherwise occ occurres in parent
1155: result.set(occ.ant, getIndexOfUnchangedFormula(n, occ.ant,
1156: occ.cfm), occ.jb);
1157: print("Occ was not changed or added");
1158: return false;
1159: }
1160:
1161: final PosTacletApp pta = (PosTacletApp) appliedRuleApp;
1162: final Taclet taclet = pta.taclet();
1163:
1164: assert cfmIndexKey.intValue() == occ.cfm;
1165: if (taclet instanceof RewriteTaclet) {
1166: return indexAfterRewriteTacletApplication(occ, result, tgt,
1167: n, pta, index2cfmAnt, index2cfmSuc);
1168: } else if (taclet instanceof AntecTaclet
1169: || taclet instanceof SuccTaclet) {
1170: // Case 2.2
1171: return indexAfterAntecSuccTacletapplication(occ, result,
1172: tgt, n, pta, index2cfmAnt, index2cfmSuc);
1173: }
1174:
1175: result.set(occ.ant, occ.cfm, occ.jb);
1176: return false;
1177: }
1178:
1179: /**
1180: *
1181: * @param n
1182: * @param parent
1183: * @param occ
1184: * @param result
1185: * @return
1186: */
1187: private boolean indexAfterBuiltInRuleApplication(Node n, Occ occ,
1188: Occ result) {
1189: final Node parent = n.parent();
1190: final BuiltInRuleApp bira = (BuiltInRuleApp) parent
1191: .getAppliedRuleApp();
1192: boolean ant = bira.posInOccurrence().isInAntec();
1193: int indexOfUpSimpl = parent.sequent().formulaNumberInSequent(
1194: ant, bira.posInOccurrence().constrainedFormula());
1195: if (!ant) {
1196: indexOfUpSimpl = indexOfUpSimpl
1197: - parent.sequent().antecedent().size();
1198: }
1199: indexOfUpSimpl--;
1200: int newCfm = getIndexOfUnchangedFormula(n, occ.ant, occ.cfm);
1201: print("Index Of simplified Formula: ", indexOfUpSimpl);
1202:
1203: /*
1204: * if occ does not occure in the sequent of the parent it was
1205: * changed by an update simplification rule
1206: */
1207: if (newCfm == -1) {
1208: newCfm = indexOfUpSimpl;
1209: }
1210: result.set(occ.ant, newCfm, occ.jb);
1211: return false;
1212: }
1213:
1214: /**
1215: * return occInParentOfRewriteTaclet(occOfFind, occ, result, tgt,
1216: n, pta, inst, cfmIndexKey, index2cfmAnt, index2cfmSuc);
1217: */
1218: private boolean indexAfterAntecSuccTacletapplication(Occ occ,
1219: Occ result, TacletGoalTemplate tgt, Node n,
1220: PosTacletApp pta, HashMap index2cfmAnt, HashMap index2cfmSuc) {
1221:
1222: final Occ occOfFind = getOccOfFind(n.parent());
1223: print("Occ of Find ", occOfFind);
1224:
1225: final FindTaclet taclet = (FindTaclet) pta.taclet();
1226:
1227: if ((tgt instanceof AntecSuccTacletGoalTemplate)) {
1228:
1229: final HashMap indexToReplaceAnt = getIndexedInstantiatedFormulas(
1230: ((AntecSuccTacletGoalTemplate) tgt).replaceWith(),
1231: n, true, services);
1232:
1233: final HashMap indexToReplaceSucc = getIndexedInstantiatedFormulas(
1234: ((AntecSuccTacletGoalTemplate) tgt).replaceWith(),
1235: n, false, services);
1236:
1237: print("Repl: Ant:", indexToReplaceAnt.keySet());
1238: print("Suc:", indexToReplaceSucc.keySet());
1239:
1240: index2cfmAnt.putAll(indexToReplaceAnt);
1241: index2cfmSuc.putAll(indexToReplaceSucc);
1242: }
1243:
1244: final Integer cfmIndexKey = new Integer(occ.cfm);
1245: if ((index2cfmAnt.containsKey(cfmIndexKey) && occ.ant)
1246: || (index2cfmSuc.containsKey(cfmIndexKey) && !occ.ant)) {
1247: // pos.cfm was added or replaced
1248: print("pos was replaced or added");
1249:
1250: final Term findTerm = taclet.find();
1251: final ConstrainedFormula newCfm;
1252:
1253: if (occ.ant) {
1254: newCfm = (ConstrainedFormula) index2cfmAnt
1255: .get(cfmIndexKey);
1256: } else {
1257: newCfm = (ConstrainedFormula) index2cfmSuc
1258: .get(cfmIndexKey);
1259: }
1260:
1261: print("changed Formula template", newCfm);
1262: final SVInstantiations inst = pta.matchConditions()
1263: .getInstantiations();
1264: final OccInSchema occInSV = getSVofOcc(newCfm.formula(),
1265: occ.jb, inst);
1266:
1267: print("Occ in SV", occInSV);
1268:
1269: int occOfSV = -1;
1270:
1271: if (occInSV != null) {
1272: print("Occurrence in Schema Variable: " + occInSV.sv
1273: + " occ ", occInSV.occ);
1274: if (occInSV.isJavaBlock) {
1275: result.set(occOfFind.ant, occOfFind.cfm,
1276: getOccurrenceOfJavaBlock(findTerm, inst));
1277: return true;
1278: } else {
1279: occOfSV = getOccurrenceOfSV(findTerm, occInSV.sv,
1280: inst);
1281: }
1282: }
1283:
1284: print("" + occOfSV);
1285:
1286: if (occOfSV == -1) {
1287: // the schema variable does not occure in the find
1288: // part, so an execution trace starts at this node
1289: result.set(occOfFind.ant, -1, -1);
1290: return false;
1291: }
1292:
1293: print("Occurrence of sv in find ", occOfSV);
1294: result.set(occOfFind.ant, occOfFind.cfm, occOfSV
1295: + occInSV.occ);
1296: return false;
1297: } else {
1298: // Case 1
1299: print("occ was not replaced or added");
1300: int newCfm = getIndexOfUnchangedFormula(n, occ.ant, occ.cfm);
1301: print("newCfm ", newCfm);
1302:
1303: if (newCfm == -1) {
1304: newCfm = occ.cfm;
1305: }
1306:
1307: result.set(occ.ant, newCfm, occ.jb);
1308: return false;
1309: }
1310: }
1311:
1312: /**
1313: */
1314: private boolean occInParentHelper(Occ occOfFind, Term find,
1315: Term newTerm, int javaBlockOcc, Occ result,
1316: SVInstantiations inst) {
1317:
1318: final OccInSchema pisv = getSVofOcc(newTerm, javaBlockOcc, inst);
1319: int occOfSV = -1;
1320:
1321: if (pisv != null) {
1322: print("SchemaVariable of Occ: " + pisv.sv + " occInSV ",
1323: pisv.occ);
1324: result.set(occOfFind.ant, occOfFind.cfm, result.jb);
1325:
1326: if (pisv.isJavaBlock) {
1327: occOfSV = getOccurrenceOfJavaBlock(find, inst);
1328: } else {
1329: occOfSV = getOccurrenceOfSV(find, pisv.sv, inst);
1330: }
1331: }
1332:
1333: print("occOfSV in find part ", occOfSV);
1334:
1335: if (occOfSV == -1) {
1336: // the schema variable does not occure in the find
1337: // part, so an execution trace starts at this node
1338: result.cfm = -1;
1339: result.jb = -1;
1340: return false;
1341: }
1342:
1343: result.jb = occOfFind.jb + occOfSV + pisv.occ;
1344: return pisv.isJavaBlock;
1345: }
1346:
1347: /**
1348: * returns the index of the rewritten formula
1349: */
1350: private int getIndexOfRewrittenFormula(TacletGoalTemplate tgt,
1351: Node n, Occ occOfFind, Occ occ, Services services) {
1352: int indexOfRewrite = -1;
1353: if (tgt instanceof RewriteTacletGoalTemplate) {
1354: final RewriteTacletGoalTemplate rwGoalTemplate = (RewriteTacletGoalTemplate) tgt;
1355:
1356: indexOfRewrite = getIndexedInstantiatedRewrittenFormula(
1357: rwGoalTemplate, n, occ.ant, services);
1358: print("Rewritten Formula: ", indexOfRewrite);
1359: // occ.cfm was not added
1360: // occ.cfm was replaced?
1361: // TODO HACK
1362: if (indexOfRewrite == -1) {
1363: indexOfRewrite = occOfFind.cfm;
1364: }
1365: }
1366:
1367: return indexOfRewrite;
1368: }
1369:
1370: /**
1371: * @param occOfFind
1372: * @param occ
1373: * @param result
1374: * @param tgt
1375: * @param n
1376: * @param pta
1377: * @param index2cfmAnt
1378: * @param index2cfmSuc
1379: * @return
1380: */
1381: private boolean indexAfterRewriteTacletApplication(Occ occ,
1382: Occ result, TacletGoalTemplate tgt, Node n,
1383: PosTacletApp pta, HashMap index2cfmAnt, HashMap index2cfmSuc) {
1384: //Case 2.1
1385: final Occ occOfFind = getOccOfFind(n.parent());
1386: print("Occ of Find ", occOfFind);
1387:
1388: final RewriteTaclet rwTaclet = (RewriteTaclet) pta.taclet();
1389: final SVInstantiations inst = pta.matchConditions()
1390: .getInstantiations();
1391: final Term findTerm = rwTaclet.find();
1392:
1393: final Integer cfmIndexKey = new Integer(occ.cfm);
1394: if ((index2cfmAnt.containsKey(cfmIndexKey) && occ.ant)
1395: || (index2cfmSuc.containsKey(cfmIndexKey) && !occ.ant)) {
1396: // Case 2.1.2: occ.cfm was added
1397: print("occ was added");
1398: ConstrainedFormula addCfm;
1399: if (occ.ant) {
1400: addCfm = (ConstrainedFormula) index2cfmAnt
1401: .get(cfmIndexKey);
1402: } else {
1403: addCfm = (ConstrainedFormula) index2cfmSuc
1404: .get(cfmIndexKey);
1405: }
1406: return occInParentHelper(occOfFind, findTerm, addCfm
1407: .formula(), occ.jb, result, inst);
1408: } else {
1409: final int indexOfRewrite = getIndexOfRewrittenFormula(tgt,
1410: n, occOfFind, occ, services);
1411: // check for replacewith part
1412: if ((indexOfRewrite == occ.cfm)
1413: && (occ.ant == occOfFind.ant)) {
1414: print("pos.cfm was replaced");
1415: int javaBlocksInFind = countJavaBlocks(pta
1416: .posInOccurrence().subTerm());
1417: //Case 2.1.1
1418: if (occ.jb >= occOfFind.jb) {
1419: final Term replaceTerm = ((RewriteTacletGoalTemplate) tgt)
1420: .replaceWith();
1421: int javaBlocksInRepl = countJavaBlocksWithSV(
1422: replaceTerm, inst);
1423:
1424: print("Blocks in Repl: ", javaBlocksInRepl);
1425: print("Blocks in Find: ", javaBlocksInFind);
1426:
1427: // Case 2.1.1.3: occ "after" replace
1428: if (occ.jb >= occOfFind.jb + javaBlocksInRepl) {
1429: print("occ after replace");
1430: result
1431: .set(
1432: occOfFind.ant,
1433: occOfFind.cfm,
1434: occ.jb
1435: + (javaBlocksInFind - javaBlocksInRepl));
1436: return false;
1437: }
1438:
1439: // Case 2.1.1.2: occ "in" replace
1440: print("Occ is result of rewriting a subformula");
1441:
1442: return occInParentHelper(occOfFind, findTerm,
1443: replaceTerm, occ.jb - occOfFind.jb, result,
1444: inst);
1445: } else {
1446: // Case 2.1.1.1: occ "before" replace
1447: print("Occ before replace occ");
1448:
1449: result.copy(occ);
1450: return false;
1451: }
1452: } else {
1453: // Case 1
1454: result.set(occ.ant, getIndexOfUnchangedFormula(n,
1455: occ.ant, occ.cfm), occ.jb);
1456: print("Occ was not changed or added");
1457: return false;
1458: }
1459:
1460: }
1461: }
1462:
1463: private void print(Object o, Object o2) {
1464: if (DEBUG) {
1465: System.out.println(o + "" + o2);
1466: }
1467: }
1468:
1469: private void print(Object o, int i) {
1470: if (DEBUG) {
1471: System.out.println(o + "" + i);
1472: }
1473: }
1474:
1475: private void print(Object o) {
1476: if (DEBUG) {
1477: System.out.println(o);
1478: }
1479: }
1480:
1481: /**
1482: * prints the extracted execution trace models
1483: */
1484: private void printTraces(ExecutionTraceModel[] exTraceModels) {
1485: if (DEBUG) {
1486: print("Number of traces ", exTraceModels.length);
1487: for (int i = 0; i < exTraceModels.length; i++) {
1488: print("Trace Start ", exTraceModels[i].getFirstNode()
1489: .serialNr());
1490: print(" End ", exTraceModels[i].getLastNode()
1491: .serialNr());
1492: print("Type ", exTraceModels[i].getType());
1493: TraceElement te = exTraceModels[i]
1494: .getFirstTraceElement();
1495: while (te != TraceElement.END) {
1496: print("", te.node().serialNr());
1497: te = te.getNextInProof();
1498: }
1499: }
1500: }
1501: }
1502:
1503: /**
1504: *
1505: * @param t1 ExecutionTraceModel
1506: * @param t2 ExecutionTraceModel
1507: * @return true iff t1 is a part of t2
1508: *
1509: */
1510:
1511: private boolean redundant(ExecutionTraceModel t1,
1512: ExecutionTraceModel t2) {
1513: if (t1.getLastTraceElement().serialNr() > t2
1514: .getLastTraceElement().serialNr()) {
1515: return false;
1516: }
1517: TraceElement te1 = t1.getFirstTraceElement();
1518: TraceElement te2 = t2.getFirstTraceElement();
1519: while (te1 != TraceElement.END) {
1520: if (te1.serialNr() != te2.serialNr()) {
1521: return false;
1522: }
1523: te2 = te2.nextInProof;
1524: te1 = te1.nextInProof;
1525: }
1526: return true;
1527: }
1528:
1529: /**
1530: * @param traces
1531: * @return removes every trace that is a part of another
1532: */
1533:
1534: private ExecutionTraceModel[] removeRedundandTraces(
1535: ExecutionTraceModel[] traces) {
1536: LinkedList result = new LinkedList();
1537: for (int i = 0; i < traces.length; i++) {
1538: if (traces[i] == null) {
1539: continue;
1540: }
1541: boolean redundant = false;
1542: for (int j = 0; j < traces.length; j++) {
1543: if (j != i && (traces[j] != null)
1544: && redundant(traces[i], traces[j])) {
1545: redundant = true;
1546: }
1547: }
1548: if (!redundant) {
1549: result.add(traces[i]);
1550: } else {
1551: traces[i] = null;
1552: }
1553: }
1554: ExecutionTraceModel[] exTraceModels = new ExecutionTraceModel[result
1555: .size()];
1556: result.toArray(exTraceModels);
1557: return exTraceModels;
1558: }
1559:
1560: /** renames a sequent
1561: *
1562: * @param semi
1563: * @param renamings: a list of HashMaps, that contains the renamings
1564: * @return a sequent that is the result of renaming variables in the order
1565: * the renamings appear in the list;
1566: */
1567: private Semisequent rename(Semisequent semi,
1568: ListOfRenamingTable renamings) {
1569: if (renamings != null) {
1570: IteratorOfRenamingTable it = renamings.iterator();
1571: while (it.hasNext()) {
1572: RenamingTable rt = it.next();
1573: HashMap hm = rt.getHashMap();
1574: ProgVarReplacer pvr = new ProgVarReplacer(hm);
1575: SemisequentChangeInfo sci = pvr.replace(semi);
1576: semi = sci.semisequent();
1577: }
1578: }
1579: return semi;
1580: }
1581:
1582: private Term rename(Term formula, ListOfRenamingTable renamings) {
1583: if (renamings != null) {
1584: IteratorOfRenamingTable it = renamings.iterator();
1585: while (it.hasNext()) {
1586: RenamingTable rt = it.next();
1587: HashMap hm = rt.getHashMap();
1588: ProgVarReplacer pvr = new ProgVarReplacer(hm);
1589: formula = pvr.replace(formula);
1590: }
1591: }
1592: return formula;
1593: }
1594:
1595: /**
1596: * @param ste a ContextTraceElement
1597: */
1598:
1599: private void setLabel(ContextTraceElement ste) {
1600: if (tacletWithLabel(ste.node(), LOOP_INVARIANT_PROPOSAL_RULESET)) {
1601: final TraceElement next = ste.getNextInProof();
1602: if (next != TraceElement.END) {
1603: final IteratorOfNode it = ste.node().childrenIterator();
1604: while (it.hasNext()) {
1605: final Node subTree = it.next();
1606: if (subTree.find(next.node())) {
1607: ste.setLabel(subTree.getNodeInfo()
1608: .getBranchLabel());
1609: break;
1610: }
1611: }
1612: }
1613: }
1614: }
1615:
1616: private boolean tacletWithLabel(Node n, String ruleSet) {
1617: if (n.getAppliedRuleApp() instanceof TacletApp) {
1618: final Name ruleSetName = new Name(ruleSet);
1619: final IteratorOfRuleSet rs = ((TacletApp) n
1620: .getAppliedRuleApp()).taclet().ruleSets();
1621:
1622: while (rs.hasNext()) {
1623: if (rs.next().name().equals(ruleSetName)) {
1624: return true;
1625: }
1626: }
1627: }
1628: return false;
1629: }
1630:
1631: /** The following methods are needed to replay the taclet application
1632: * in order to figure out which formulas are added or rewritten.
1633: * Copied from Taclet.java
1634: * TODO remove these methods
1635: *
1636: **/
1637: private Term syntacticalReplace(Term term, Services services,
1638: SVInstantiations svInst) {
1639: SyntacticalReplaceVisitor srVisitor = new SyntacticalReplaceVisitor(
1640: services, svInst);
1641: term.execPostOrder(srVisitor);
1642:
1643: return srVisitor.getTerm();
1644: }
1645:
1646: /**
1647: * Check if p_pos contains an explicit metavariable instantiation,
1648: * and creates in this case a new simple term by replacing the
1649: * metavariable with the instantiation
1650: */
1651: private PosInOccurrence flatten(PosInOccurrence p_pos,
1652: Services p_services) {
1653: if (p_pos.termBelowMetavariable() != null) {
1654: Term flatTerm = replace(p_pos.constrainedFormula()
1655: .formula(), p_pos.termBelowMetavariable(), p_pos
1656: .posInTerm().iterator(), p_services,
1657: SVInstantiations.EMPTY_SVINSTANTIATIONS,
1658: Sort.FORMULA);
1659:
1660: PosInOccurrence pos = new PosInOccurrence(
1661: new ConstrainedFormula(flatTerm, p_pos
1662: .constrainedFormula().constraint()), p_pos
1663: .posInTerm(), p_pos.isInAntec());
1664:
1665: IntIterator it = p_pos.posInTermBelowMetavariable()
1666: .iterator();
1667: while (it.hasNext()) {
1668: pos = pos.down(it.next());
1669: }
1670:
1671: return pos;
1672: }
1673:
1674: return p_pos;
1675: }
1676:
1677: /**
1678: * does the work for applyReplacewith (wraps recursion)
1679: */
1680: private Term replace(Term term, Term with, IntIterator it,
1681: Services services, SVInstantiations svInst, Sort maxSort) {
1682: if (it.hasNext()) {
1683: int sub = it.next();
1684:
1685: ArrayOfQuantifiableVariable[] origvars = new ArrayOfQuantifiableVariable[term
1686: .arity()];
1687: final Term[] subs = new Term[term.arity()];
1688:
1689: boolean containsBoundVar = false;
1690: for (int i = 0, arity = term.arity(); i < arity; i++) {
1691: final Term tSub = term.sub(i);
1692: if (i != sub) {
1693: subs[i] = tSub;
1694: } else {
1695: final Sort newMaxSort;
1696: if (term.op() instanceof Function) {
1697: newMaxSort = ((Function) term.op()).argSort(i);
1698: } else {
1699: newMaxSort = tSub.sort();
1700: }
1701: subs[i] = replace(tSub, with, it, services, svInst,
1702: newMaxSort);
1703: }
1704: origvars[i] = term.varsBoundHere(i);
1705:
1706: if (origvars[i].size() > 0) {
1707: containsBoundVar = true;
1708: }
1709: }
1710:
1711: if (!containsBoundVar) {
1712: // for quantified updates there seems to be a distinction
1713: // if no variables are quantified or quantification over
1714: // the empty set
1715: origvars = null;
1716: }
1717:
1718: return TermFactory.DEFAULT.createTerm(term.op(), subs,
1719: origvars, term.javaBlock());
1720: }
1721:
1722: with = syntacticalReplace(with, services, svInst);
1723:
1724: if (maxSort instanceof AbstractSort) {
1725: boolean noCastNecessary = with.sort().extendsTrans(maxSort);
1726: if (!noCastNecessary) {
1727: with = TermFactory.DEFAULT.createCastTerm(
1728: (AbstractSort) maxSort, with);
1729: }
1730: } else {
1731: // maybe move getCastSymbol to sort interface
1732: // in the meantime no casts are inserted
1733: }
1734:
1735: return with;
1736: }
1737:
1738: //------------------------------------------------------------------------
1739:
1740: public class MethodReferenceWalker extends JavaASTWalker {
1741: private LinkedList methodRefs;
1742:
1743: public MethodReferenceWalker(ProgramElement root) {
1744: super (root);
1745: methodRefs = new LinkedList();
1746: }
1747:
1748: public LinkedList containsMethodRef() {
1749: return methodRefs;
1750: }
1751:
1752: public void doAction(ProgramElement node) {
1753: if (node instanceof MethodReference) {
1754: methodRefs.add(node);
1755: }
1756: }
1757: }
1758:
1759: /** Determines the occurrence of a Java
1760: * block in a Sequent by the number of
1761: * the Java blocks that are "on the left" of the Java block
1762: */
1763: public class Occ {
1764:
1765: public boolean ant;
1766: public int cfm, jb;
1767:
1768: /** @param ant determines if the Java block occures in
1769: * the antecedent or succedent of the sequent
1770: * @param cfm the index of the formula in the semisequent
1771: * @param jb determines the occurrence of the Java block
1772: * in the formula
1773: */
1774:
1775: public Occ(boolean ant, int cfm, int jb) {
1776: set(ant, cfm, jb);
1777: }
1778:
1779: public void copy(Occ occ) {
1780: set(occ.ant, occ.cfm, occ.jb);
1781: }
1782:
1783: public void set(boolean p_ant, int p_cfm, int p_jb) {
1784: this .ant = p_ant;
1785: this .cfm = p_cfm;
1786: this .jb = p_jb;
1787: }
1788:
1789: public Occ copy() {
1790: return new Occ(ant, cfm, jb);
1791: }
1792:
1793: public String toString() {
1794: return ("Occurrence: " + ant + " / " + cfm + " / " + jb);
1795: }
1796: }
1797:
1798: /** Determines the occurrence of a Java block in
1799: * an instantiated schema variable or
1800: * determines the schematic
1801: * Java block
1802: */
1803:
1804: class OccInSchema {
1805: public boolean isJavaBlock = false;
1806: public JavaBlock jb;
1807: public int occ = -1;
1808: public SchemaVariable sv = null;
1809:
1810: public OccInSchema(JavaBlock jb) {
1811: this .jb = jb;
1812: occ = 0;
1813: isJavaBlock = true;
1814: }
1815:
1816: public OccInSchema(SchemaVariable sv, int svOcc) {
1817: this .sv = sv;
1818: this .occ = svOcc;
1819: }
1820:
1821: public String toString() {
1822: if (isJavaBlock) {
1823: return "Occ in Java block: " + jb;
1824: } else {
1825: return ("Occ in SV: " + sv + " " + occ + " " + isJavaBlock);
1826: }
1827: }
1828:
1829: }
1830:
1831: public class StatementByPositionWalker extends JavaASTWalker {
1832:
1833: ProgramElement result = null;
1834:
1835: PositionInfo toFind = null;
1836:
1837: public StatementByPositionWalker(ProgramElement root,
1838: PositionInfo toFind) {
1839: super (root);
1840: this .toFind = toFind;
1841: }
1842:
1843: public void doAction(ProgramElement node) {
1844: if (node.getPositionInfo().equals(toFind)) {
1845: result = node;
1846: }
1847:
1848: }
1849:
1850: public SourceElement getResult() {
1851: return result;
1852: }
1853: }
1854:
1855: }
|