001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.proof.reuse;
012:
013: import java.util.Hashtable;
014: import java.util.LinkedList;
015: import java.util.Vector;
016:
017: import org.apache.log4j.Logger;
018:
019: import de.uka.ilkd.key.collection.SLListOfString;
020: import de.uka.ilkd.key.gui.KeYMediator;
021: import de.uka.ilkd.key.java.*;
022: import de.uka.ilkd.key.java.reference.ExecutionContext;
023: import de.uka.ilkd.key.java.statement.MethodFrame;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.proof.*;
027: import de.uka.ilkd.key.rule.*;
028: import de.uka.ilkd.key.rule.inst.*;
029: import de.uka.ilkd.key.util.ExtList;
030:
031: public class ReusePoint implements Comparable {
032:
033: Node templateNode;
034: Goal targetGoal;
035: int score = 0;
036: PosInOccurrence targetPos;
037: RuleApp templateApp;
038: RuleApp reuseApp;
039: /** the rule involved is not part of the standard set */
040: private boolean goalLocalRule = false;
041:
042: private String s = "";
043:
044: private static Logger reuseLogger = Logger
045: .getLogger("key.proof.reuse");
046:
047: private ReusePoint(ReusePoint other) {
048: this .templateNode = other.templateNode;
049: this .targetGoal = other.targetGoal;
050: this .goalLocalRule = other.goalLocalRule;
051: templateApp = templateNode.getAppliedRuleApp();
052: }
053:
054: public ReusePoint(Node templateNode, Goal targetGoal) {
055: this .templateNode = templateNode;
056: this .targetGoal = targetGoal;
057: templateApp = templateNode.getAppliedRuleApp();
058: }
059:
060: public ReusePoint initialize(PosInOccurrence targetPos,
061: RuleApp tentativeApp, KeYMediator medi) {
062: ReusePoint result = new ReusePoint(this );
063: result.setTargetPos(targetPos);
064: RuleApp targetApp = result.getTargetApp(tentativeApp, medi);
065: if (targetApp == null)
066: return null;
067: result.setReuseApp(targetApp);
068: result.compare(result.sourceTerm(), targetPos.subTerm());
069: if (templateApp instanceof TacletApp) {
070: result.compareIf((TacletApp) templateApp,
071: (TacletApp) targetApp);
072: }
073: return result;
074: }
075:
076: public ReusePoint initializeNoFind(RuleApp tentativeApp,
077: KeYMediator medi) {
078: ReusePoint result = new ReusePoint(this );
079: RuleApp targetApp = result.getTargetApp(tentativeApp, medi);
080: if (targetApp == null)
081: return null;
082: result.setReuseApp(targetApp);
083: result.compareNoFind();
084: return result;
085: }
086:
087: public Goal target() {
088: return targetGoal;
089: }
090:
091: public Node source() {
092: return templateNode;
093: }
094:
095: public RuleApp getApp() {
096: return templateApp;
097: }
098:
099: public Term sourceTerm() {
100: return templateApp.posInOccurrence().subTerm();
101: }
102:
103: private void setTargetPos(PosInOccurrence pos) {
104: this .targetPos = pos;
105: }
106:
107: public PosInOccurrence getTargetPos() {
108: return targetPos;
109: }
110:
111: private void setReuseApp(RuleApp app) {
112: reuseApp = app;
113: }
114:
115: public RuleApp getReuseApp() {
116: return reuseApp;
117: }
118:
119: public void setGoalLocal(boolean b) {
120: goalLocalRule = b;
121: }
122:
123: private RuleApp getTargetApp(RuleApp tentativeApp, KeYMediator medi) {
124: if (templateApp instanceof TacletApp) {
125: TacletApp result = (TacletApp) tentativeApp;
126:
127: //if (result.tryToInstantiate(medi.getServices())!=null)
128: //System.err.println(result);
129: // result = result.tryToInstantiate(medi.getServices());
130:
131: //if (result.rule().name().toString().equals("int_induction")) return result;
132:
133: // 1st pass
134: IteratorOfSchemaVariable it = result.uninstantiatedVars()
135: .iterator();
136: while (it.hasNext()) {
137: SVInstantiations insts = ((TacletApp) templateApp)
138: .instantiations();
139: SchemaVariable sv = it.next();
140: SchemaVariable svTemplate;
141:
142: if (goalLocalRule) {
143: svTemplate = insts.lookupVar(sv.name());
144: } else {
145: svTemplate = sv;
146: }
147:
148: String text = "";
149: if (sv.isVariableSV()) {
150: Object o = insts.getInstantiation(svTemplate);
151: reuseLogger.info(result.rule().name()
152: + ": Copying instantiation of " + o
153: + " for " + sv);
154:
155: if (o == null) {
156: text = nameSuggestion(sv, medi.getServices(),
157: (TacletApp) tentativeApp);
158: } else {
159: try {
160: text = ProofSaver.printTerm((Term) o,
161: templateNode.proof().getServices())
162: .toString();
163: } catch (Exception e) {
164: System.err.println("Missing " + sv
165: + " from "
166: + tentativeApp.rule().name());
167: return null;
168: }
169: }
170: result = ProblemLoader.parseSV1(result, sv, text,
171: medi.getServices());
172: } else {
173: // leave for 2nd pass
174: }
175: }
176:
177: // 2nd pass
178: it = result.uninstantiatedVars().iterator();
179: SVInstantiations insts = ((TacletApp) templateApp)
180: .instantiations();
181: while (it.hasNext()) {
182: SchemaVariable sv = it.next();
183: SchemaVariable svTemplate;
184: if (goalLocalRule) {
185: svTemplate = insts.lookupVar(sv.name());
186: } else {
187: svTemplate = sv;
188: }
189:
190: InstantiationEntry o = insts.interesting().get(
191: svTemplate);
192:
193: if (result != null) {
194: reuseLogger.info(result.rule().name()
195: + ": Copying instantiation of " + o
196: + " for " + sv);
197: }
198:
199: String text = "";
200: if (o instanceof TermInstantiation) {
201: text = ProofSaver.printTerm(
202: ((TermInstantiation) o).getTerm(),
203: templateNode.proof().getServices())
204: .toString();
205: } else if (o instanceof ProgramInstantiation) {
206: text = ProofSaver
207: .printProgramElement(((ProgramInstantiation) o)
208: .getProgramElement());
209: } else if (o instanceof ListInstantiation) {
210: text = ProofSaver.printListInstantiation(
211: ((ListInstantiation) o).getList(),
212: templateNode.proof().getServices());
213: } else if (o == null) {
214: // throw new IllegalStateException(
215: // "Null InstantiationEntry for "+sv+" in "+templateApp);
216: text = nameSuggestion(sv, medi.getServices(),
217: (TacletApp) tentativeApp);
218: } else {
219: System.err
220: .println("What the hell is this instantiation? "
221: + sv + " of type " + o.getClass());
222: text = nameSuggestion(sv, medi.getServices(),
223: (TacletApp) tentativeApp);
224: }
225: if (text == null) {
226: return null;
227: }
228: try {
229: result = ProblemLoader.parseSV2(result, sv, text,
230: targetGoal);
231: } catch (IllegalInstantiationException e) {
232: result = null;
233: }
234: }
235:
236: return result;
237:
238: } else if (templateApp instanceof BuiltInRuleApp) {
239: IteratorOfRuleApp it = targetGoal.ruleAppIndex()
240: .getBuiltInRule(targetGoal, targetPos,
241: medi.getUserConstraint().getConstraint())
242: .iterator();
243: RuleApp result = null;
244: RuleApp tmp;
245: while (it.hasNext()) {
246: tmp = it.next();
247: if (tmp.rule().equals(templateApp.rule())) {
248: if (result != null)
249: throw new RuntimeException(templateApp.rule()
250: .name()
251: + ": found more than 1 app");
252: else
253: result = tmp;
254: }
255: }
256: if (result == null)
257: System.err.println(templateApp.rule().name()
258: + ": found 0 apps -- too bad!");
259: return result;
260: } else
261: throw new RuntimeException(templateApp.rule().name()
262: + ": neither TacletApp nor BuiltinRuleApp");
263: }
264:
265: private String nameSuggestion(SchemaVariable sv, Services services,
266: TacletApp app) {
267: String text;
268: if (sv.isProgramSV()) {
269: text = services.getVariableNamer()
270: .getSuggestiveNameProposalForProgramVariable(
271: (ProgramSV) sv, app, targetGoal, services,
272: SLListOfString.EMPTY_LIST);
273: } else {
274: text = VariableNameProposer.DEFAULT.getNameProposal(sv
275: .name().toString().replaceAll("#", ""), services,
276: targetGoal.node());
277: }
278: return text;
279: }
280:
281: public int score() {
282: return score;
283: }
284:
285: public boolean notGoodEnough() {
286: return (score < -72);
287: }
288:
289: /** implements Comparable. Sorts in descending score order. */
290: public int compareTo(Object o) {
291: ReusePoint p1 = (ReusePoint) o;
292: if (score > p1.score())
293: return -1;
294: if (score < p1.score())
295: return 1;
296: return 0;
297: }
298:
299: ExtList children(NonTerminalProgramElement p) {
300: ExtList ch = new ExtList();
301: for (int k = 0; k < p.getChildCount(); k++)
302: ch.add(p.getChildAt(k));
303: return ch;
304: }
305:
306: int diffJava(JavaProgramElement x, JavaProgramElement y) {
307: StatementCollector c1 = new StatementCollector(templateNode
308: .proof(), x);
309: StatementCollector c2 = new StatementCollector(targetGoal
310: .proof(), y);
311: c1.start();
312: c2.start();
313: DiffMyers d = new DiffMyers(c1.result(), c2.result());
314: reuseLogger.debug(c1.result());
315: reuseLogger.debug(c2.result());
316: DiffMyers.change diff = d.diff_2();
317: reuseLogger.debug(diff);
318: if (diff != null)
319: return diff.diminishingPenalty();
320: else
321: return 0;
322: }
323:
324: int scoreLogicalFindEqualsMod(Term x, Term y) {
325: if (x.depth() == y.depth()) {
326: if (x.toString().equals(y.toString()))
327: return 10;
328: }
329: if (x.equalsModRenaming(y)) {
330: // System.err.println("1:"+x+"<->"+y+" ["+x.depth());
331: return 30;
332: } else
333: return -10;
334: }
335:
336: int diffLogical(Term x, Term y) {
337: int this Score;
338: Vector xsig = new Vector(20, 20);
339: Vector ysig = new Vector(20, 20);
340: Hashtable xDiamonds = new Hashtable(5);
341: Hashtable yDiamonds = new Hashtable(5);
342: createReuseSignature(x, xsig, xDiamonds);
343: createReuseSignature(y, ysig, yDiamonds);
344: reuseLogger.debug(xsig);
345: reuseLogger.debug(ysig);
346: DiffMyers d = new DiffMyers(xsig, ysig);
347: DiffMyers.change diff = d.diff_2();
348: reuseLogger.debug(diff);
349: if (diff != null)
350: this Score = diff.uniformPenalty();
351: else
352: this Score = 0;
353:
354: DiffMyers.mapping map = d.getMapping();
355: while (map != null) {
356: int from = map.from();
357: int to = map.to();
358: if (xsig.elementAt(from).equals("diamond")) {
359: reuseLogger.debug("diamond " + from + "<->" + to);
360: Term d1 = (Term) xDiamonds.get(new Integer(from));
361: Term d2 = (Term) yDiamonds.get(new Integer(to));
362: int diamondScore = diffJava(d1.executableJavaBlock()
363: .program(), d2.executableJavaBlock().program()) / 4;
364: // System.err.println(d1);
365: // System.err.println(d2);
366: reuseLogger.debug("Diamond correspondence penalty "
367: + diamondScore);
368: this Score += diamondScore;
369:
370: }
371:
372: map = map.next();
373: }
374: this Score -= Math.abs(xDiamonds.size() - yDiamonds.size()) * 30;
375:
376: return this Score;
377: }
378:
379: int diffPosInTerm(PosInTerm x, PosInTerm y) {
380: int this Score;
381:
382: DiffMyers d = new DiffMyers(x, y);
383: DiffMyers.change diff = d.diff_2();
384: reuseLogger.debug(diff);
385: if (diff != null)
386: this Score = diff.uniformPenalty();
387: else
388: this Score = 0;
389: return this Score;
390: }
391:
392: void compareNoFind() {
393: reuseLogger.info("*-");
394: //System.err.println("Comparing terms "+x+"<->"+y);
395: int localScore;
396: localScore = scoreConnectNoFind(templateNode, targetGoal.node());
397: // localScore += scoreConnectSemiseq();
398: reuseLogger.info("Connectivity reward " + localScore);
399: score += localScore;
400: s = s + "Connectivity: " + localScore + "\n";
401:
402: localScore = scoreSiblingNr(templateNode, targetGoal.node());
403: reuseLogger.info("Sibling order penalty " + localScore);
404: score += localScore;
405: s = s + "Sibling order penalty: " + localScore + "\n";
406:
407: reuseLogger.info("Total score " + score);
408: s = s + "-------\n";
409: s = s + "Total score: " + score + "\n";
410: s = s + "Reuse source: " + templateNode.serialNr() + "\n";
411: }
412:
413: void compare(Term x, Term y) {
414: reuseLogger.info("* " + getApp().rule().name());
415: //System.err.println("Comparing terms "+x+"<->"+y);
416: int localScore;
417: JavaBlock jx = x.executableJavaBlock();
418: JavaBlock jy = y.executableJavaBlock();
419: if (jx == JavaBlock.EMPTY_JAVABLOCK
420: || jy == JavaBlock.EMPTY_JAVABLOCK) {
421:
422: // not a symbolic execution rule
423: localScore = scoreLogicalFindEqualsMod(x, y);
424: reuseLogger.info("By equalsModRenaming on find "
425: + localScore);
426: score += localScore;
427: s = s + "By equalsModRenaming on find " + localScore + "\n";
428:
429: localScore = diffLogical(templateApp.posInOccurrence()
430: .constrainedFormula().formula(), targetPos
431: .constrainedFormula().formula());
432: reuseLogger.info("By diff on complete formulae "
433: + localScore);
434: score += localScore;
435: s = s + "By diff on complete formulae " + localScore + "\n";
436:
437: localScore = diffPosInTerm(templateApp.posInOccurrence()
438: .posInTerm(), targetPos.posInTerm());
439: reuseLogger.info("By diff on PosInTerm " + localScore);
440: score += localScore;
441: s = s + "By diff on PosInTerm " + localScore + "\n";
442:
443: } else { // program similarity
444: if (jy.size() > 1) {
445: localScore = diffJava(jx.program(), jy.program());
446: reuseLogger.info("Scored java diff " + localScore);
447: score += localScore;
448: s = s + "Program similarity " + localScore + "\n";
449: } else { // small program -- look at whole formula
450: localScore = diffLogical(x, y);
451: reuseLogger
452: .info("Scored whole formula (small program) "
453: + localScore);
454: score += localScore;
455: s = s + "By whole formula (small program) "
456: + localScore + "\n";
457: }
458: }
459:
460: localScore = scoreConnect(templateNode, targetGoal.node());
461: // localScore += scoreConnectSemiseq();
462: reuseLogger.info("Connectivity reward " + localScore);
463: score += localScore;
464: s = s + "Connectivity: " + localScore + "\n";
465:
466: localScore = scoreSiblingNr(templateNode, targetGoal.node());
467: reuseLogger.info("Sibling order penalty " + localScore);
468: score += localScore;
469: s = s + "Sibling order penalty: " + localScore + "\n";
470:
471: reuseLogger.info("Total score " + score);
472: s = s + "-------\n";
473: s = s + "Total score: " + score + "\n";
474: s = s + "Reuse source: " + templateNode.serialNr() + "\n";
475: }
476:
477: void compareIf(TacletApp sourceApp, TacletApp targetApp) {
478: ListOfIfFormulaInstantiation ifl1 = sourceApp
479: .ifFormulaInstantiations();
480: ListOfIfFormulaInstantiation ifl2 = targetApp
481: .ifFormulaInstantiations();
482: Term if1;
483: ConstrainedFormula iff2;
484: Term if2;
485: boolean if2inAntec;
486: try {
487: if1 = ifl1.head().getConstrainedFormula().formula();
488: if2inAntec = ((IfFormulaInstSeq) ifl2.head()).inAntec();
489: iff2 = ifl2.head().getConstrainedFormula();
490: if2 = iff2.formula();
491: } catch (Exception e) {
492: return;
493: }
494: int i = diffLogical(if1, if2);
495: i += scoreLogicalFindEqualsMod(if1, if2);
496: score += (i * 0.2);
497:
498: boolean sameFormula;
499: PosInOccurrence findPos = targetApp.posInOccurrence();
500:
501: sameFormula = (findPos.isInAntec() == if2inAntec)
502: && (findPos.constrainedFormula().equals(iff2));
503: if (sameFormula)
504: score -= 40;
505:
506: s = s + "By IF: " + score + "\n";
507:
508: }
509:
510: boolean connect = false;
511:
512: public boolean isConnect() {
513: return connect;
514: }
515:
516: int scoreConnect(Node templateNode, Node targetNode) {
517: Node predecSource;
518: Node predecTarget;
519: try {
520: predecSource = templateNode.parent();
521: predecTarget = targetNode.parent();
522: if (predecTarget.getReuseSource().source() == predecSource) {
523: connect = true;
524: return 0;
525: } else
526: return -70;//-15;
527: } catch (NullPointerException npe) {
528: return -1; // some ingredient is missing --> neutral score
529: }
530: }
531:
532: int scoreConnectNoFind(Node templateNode, Node targetNode) {
533: Node predecSource;
534: Node predecTarget;
535: try {
536: predecSource = templateNode.parent();
537: predecTarget = targetNode.parent();
538: if (predecTarget.getReuseSource().source() == predecSource) {
539: connect = true;
540: return 0;
541: } else
542: return -100; // kill
543: } catch (NullPointerException npe) {
544: return -1; // some ingredient is missing --> too bad
545: }
546: }
547:
548: int scoreSiblingNr(Node templateNode, Node targetNode) {
549: if (templateNode.siblingNr() == targetNode.siblingNr())
550: return 0;
551: else
552: return -1;
553: }
554:
555: // not used currently
556: int scoreConnectSemiseq() {
557: boolean b1 = templateApp.posInOccurrence().isInAntec();
558: boolean b2 = targetPos.isInAntec();
559: if (b1 != b2)
560: return -10;
561: else
562: return 0;
563: }
564:
565: // not used currently
566: int twoOpAboveFind() {
567: int this Score = 0;
568: reuseLogger.debug(targetPos.posInTerm());
569: reuseLogger.debug(templateApp.posInOccurrence().posInTerm());
570:
571: // the interface is worth improving...
572: if (targetPos.up().subTerm().op() != templateApp
573: .posInOccurrence().up().subTerm().op())
574: this Score = -35;
575: if (targetPos.up().up().subTerm().op() != templateApp
576: .posInOccurrence().up().up().subTerm().op())
577: this Score = -35;
578:
579: reuseLogger.info("By two operators above " + this Score);
580: return this Score;
581: }
582:
583: public static void createReuseSignature(Term t, Vector signature,
584: Hashtable diamondCollector) {
585: if (t.op() instanceof IUpdateOperator) {
586: createReuseSignature(((IUpdateOperator) t.op()).target(t),
587: signature, diamondCollector);
588: return;
589: }
590: String termsig = t.op().toString();
591: // s = s.substring(s.lastIndexOf(".")+1, s.length());
592:
593: if ((t.op() instanceof TermSymbol)
594: || (t.op() instanceof AccessOp)) {
595: signature.add(t.sort().toString());
596: return;
597: }
598:
599: signature.add(termsig);
600: if ("diamond".equals(termsig))
601: diamondCollector.put(new Integer(signature.size() - 1), t);
602: // if (s.equals("Z:int")) return;
603: int i;
604: for (i = 0; i < t.arity(); i++)
605: createReuseSignature(t.sub(i), signature, diamondCollector);
606: }
607:
608: public String scoringInfo() {
609: return s;
610: }
611:
612: public String toString() {
613: return "RP(" + score + ") " + templateApp.rule().name() + ":"
614: + templateNode.serialNr() + "->"
615: + targetGoal.node().serialNr();//" "+sourceTerm();
616: }
617:
618: //***************************************************************
619:
620: class StatementCollector extends
621: de.uka.ilkd.key.java.visitor.JavaASTWalker {
622:
623: Proof proof;
624:
625: StatementCollector(Proof proof, ProgramElement root) {
626: super (root);
627: this .proof = proof;
628: }
629:
630: Vector result = new Vector(20, 20);
631: LinkedList executionContext = new LinkedList();
632:
633: protected void walk(ProgramElement node) {
634: if (node instanceof MethodFrame) {
635: executionContext.addFirst(((MethodFrame) node)
636: .getExecutionContext());
637: }
638: if (node != root())
639: doAction(node);
640: if (node instanceof NonTerminalProgramElement) {
641: NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
642: for (int i = 0; i < nonTerminalNode.getChildCount(); i++) {
643: walk(nonTerminalNode.getChildAt(i));
644: }
645: }
646: if (node != root())
647: doLeaveAction(node);
648: if (node instanceof MethodFrame) {
649: executionContext.removeFirst();
650: }
651: }
652:
653: protected void doAction(ProgramElement node) {
654: if (node instanceof StatementBlock) {
655: // result.add("{");
656: return;
657: }
658: // if (node instanceof Statement) result.add(node);
659: if (node instanceof Statement) {
660: final ExecutionContext ec = (ExecutionContext) (executionContext
661: .size() > 0 ? executionContext.getFirst()
662: : null);
663: result.add(((JavaProgramElement) node).reuseSignature(
664: proof.getServices(), ec));
665: }
666: }
667:
668: protected void doLeaveAction(ProgramElement node) {
669: // if (node instanceof StatementBlock) result.add("}");
670: }
671:
672: Vector result() {
673: return result;
674: }
675: }
676:
677: }
|