Tracing2

key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java

@@ -15,10 +15,7 @@
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.PosInTerm;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.logic.op.Equality;
-import de.uka.ilkd.key.logic.op.Junctor;
-import de.uka.ilkd.key.logic.op.Quantifier;
-import de.uka.ilkd.key.logic.op.SortDependingFunction;
+import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.rulefilter.SetRuleFilter;
@@ -525,9 +522,14 @@ private RuleSetDispatchFeature setupCostComputationF() {
                 applyTF(instOf("uSub"), IsInductionVariable.INSTANCE), longConst(0), inftyConst()));
         }
 
+        setupTracingStrategy(d);
         return d;
     }
 
+    private void setupTracingStrategy(RuleSetDispatchFeature d) {
+        bindRuleSet(d, "retrace", longConst(-200));
+    }
+
     private void setupSelectSimplification(final RuleSetDispatchFeature d) {
         bindRuleSet(d, "pull_out_select",
             // pull out select only if it can be simplified

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/JAVALANG.TXT

@@ -58,4 +58,4 @@ java.util.ListIteratorImpl
 java.util.Date
 java.util.LinkedHashMap
 java.util.LinkedList
-
+tracer.Trace

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.java

@@ -0,0 +1,7 @@
+package tracer;
+
+import java.lang.String;
+
+public class Trace {
+    //@ public static ghost int index;
+}

key.core/src/main/resources/de/uka/ilkd/key/java/JavaRedux/tracer/Trace.key

@@ -0,0 +1,300 @@
+
+\predicates {
+    /* use this as input */
+    traceAfter(int, java.lang.String);
+    traceBefore(int, java.lang.String);
+
+    /* used this to display current trace string */
+    traced(int, int, Seq);
+
+    /* used on the sequent */
+    traceIf(int);
+}
+
+\functions {
+    /* helper function without meaning */
+    Seq seqConcatEnd(Seq, Seq);
+}
+
+\schemaVariables {
+    \modalOperator {diamond, box, diamond_transaction, box_transaction} #allmodal;
+    \program Expression #e, #e0, #e1, #e2;
+    \program SimpleExpression #se, #se0, #se1, #se2;
+    \program SimpleJavaBooleanExpression #seBool, #seBool0, #seBool1, #seBool2;
+    \program NonSimpleExpression #nse, #nse0, #nse1, #nse2;
+    \program Statement #s0, #s1, #s2;
+    \program LeftHandSide #lhs;
+    \program Variable #v0;
+    \formula post;
+    \term int idx, idx0;
+    \term java.lang.String str;
+    \term Seq #seq;
+}
+
+\rules(programRules:Java, tracing:on) {
+
+    /*
+     * Initialization (only interactively)
+     */
+    traceIndexInit {
+       \add( tracer.Trace.index = 0 ==> )
+    };
+    traceRetraceInit {
+       \add( traced(tracer.Trace.index, tracer.Trace.index, "") ==> )
+    };
+
+
+    /*
+     * Symbolic execution rules, using (!) traceIf(int)
+     */
+    traceIf {
+        \find(
+            ==> \modality{#allmodal}{..
+                if(#se) #s0
+            ...}\endmodality (post)
+        )
+        \replacewith(
+            ==>
+            \if(traceIf(tracer.Trace.index))
+            \then(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                    #s0
+                ...}\endmodality (post)
+            )
+            \else(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                ...}\endmodality (post)
+            )
+        )
+        \add(
+            (#se = TRUE) <-> traceIf(tracer.Trace.index)
+            ==>
+        )
+        \heuristics(retrace)
+    };
+
+    traceIfElse {
+        \find(
+            ==> \modality{#allmodal}{..
+                if(#se) #s0 else #s1
+            ...}\endmodality (post)
+        )
+        \replacewith(
+            ==>
+            \if(traceIf(tracer.Trace.index))
+            \then(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                    #s0
+                ...}\endmodality (post)
+            )
+            \else(
+                {tracer.Trace.index := tracer.Trace.index+1}\modality{#allmodal}{..
+                    #s1
+                ...}\endmodality (post)
+            )
+        )
+        \add(
+            (#se = TRUE) <-> traceIf(tracer.Trace.index)
+            ==>
+        )
+        \heuristics(retrace)
+    };
+
+
+    /*
+     * Rules to convert string traces to sets of traceIf(int) in sequent
+     */
+    traceFollowElse {
+      \find(
+          traceAfter(idx, strPool(seqConcat(seqSingleton('0'), #seq)))
+      )
+      \replacewith(
+          !traceIf(idx) & traceAfter(idx + 1, strPool(#seq))
+      )
+      \heuristics(simplify)
+    };
+
+    traceFollowElseEnd {
+      \find(
+         traceAfter(idx, strPool(seqSingleton('0')))
+      )
+      \replacewith(
+         !traceIf(idx)
+      )
+      \heuristics(simplify)
+    };
+
+    traceFollowIf {
+      \find(
+          traceAfter(idx, strPool(seqConcat(seqSingleton('1'), #seq)))
+      )
+      \replacewith(
+          traceIf(idx) & traceAfter(idx + 1, strPool(#seq))
+      )
+      \heuristics(simplify)
+    };
+
+    traceFollowIfEnd {
+      \find(
+         traceAfter(idx, strPool(seqSingleton('1')))
+      )
+      \replacewith(
+         traceIf(idx)
+      )
+      \heuristics(simplify)
+    };
+
+    traceBeforeElim {
+        \find(
+            traceBefore(idx, strPool(#seq))
+        )
+        \replacewith(
+            traceAfter(idx - seqLen(#seq), strPool(#seq))
+        )
+        \heuristics(simplify)
+    };
+
+
+    /*
+     * Rules to reconvert traceIf(int) sets for displaying the current trace
+     */
+    printTracedIf {
+      \assumes(
+          traceIf(idx) ==>
+      )
+      \find(
+          traced(idx0, idx, #seq) ==>
+      )
+      \replacewith(
+          traced(idx0, idx + 1, seqConcatEnd(#seq, seqSingleton('1'))) ==>
+      )
+      \heuristics(simplify)
+    };
+
+    printTracedElse {
+      \assumes(
+          ==> traceIf(idx)
+      )
+      \find(
+          traced(idx0, idx, #seq) ==>
+      )
+      \replacewith(
+          traced(idx0, idx + 1, seqConcatEnd(#seq, seqSingleton('0'))) ==>
+      )
+      \heuristics(simplify)
+    };
+
+    seqConcatEndNormalize {
+       \schemaVar \term Seq slit1, slit2;
+       \schemaVar \term int v;
+       \find (seqConcatEnd(seqConcat(slit1, slit2),seqSingleton(v)))
+       \replacewith( seqConcat(slit1,seqConcatEnd(slit2,seqSingleton(v))))
+       \heuristics(simplify)
+    };
+
+    seqConcatEndNormalize2 {
+       \schemaVar \term int v;
+       \find (seqConcatEnd(seqEmpty,seqSingleton(v)))
+       \replacewith( seqSingleton(v))
+       \heuristics(simplify)
+    };
+
+    seqConcatEndNormalize3 {
+       \schemaVar \term int v1, v2;
+       \find (seqConcatEnd(seqSingleton(v1),seqSingleton(v2)))
+       \replacewith(seqConcat(seqSingleton(v1),seqSingleton(v2)))
+       \heuristics(simplify)
+    };
+
+
+    /*
+     * Short circuit rules that don't interfere with if/else tracing
+     * [they don't translate to if (*) * else *, only to JavaDL \if(*) \then (*) \else (*)]
+     */
+    compound_assignment_3_nonsimple_new {
+        \find(\modality{#allmodal}{.. #lhs=#nse0 && #nse1; ...}\endmodality (post))
+
+        \varcond(\new(#v0, boolean))
+        \replacewith(\modality{#allmodal}{.. boolean #v0 = #nse0;
+                #lhs = #v0 && #nse1; ...}\endmodality (post))
+
+        \heuristics(simplify_expression)
+        \displayname "compound_assignment"
+    };
+
+    compound_assignment_3_reverse_mixed {
+        \find(\modality{#allmodal}{.. #lhs=#seBool0 && #nse1; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#seBool0 = TRUE)
+            \then(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+            \else({#lhs := FALSE}\modality{#allmodal}{.. ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_expression)
+        \displayname "assignment_and"
+    };
+
+    compound_assignment_5_nonsimple_new {
+        \find(\modality{#allmodal}{.. #lhs=#nse0 || #nse1; ...}\endmodality (post))
+
+        \varcond(\new(#v0, boolean))
+        \replacewith(\modality{#allmodal}{.. boolean #v0 = #nse0;
+                #lhs = #v0 || #nse1; ...}\endmodality (post))
+
+        \heuristics(simplify_expression)
+        \displayname "compound_assignment"
+    };
+
+    compound_assignment_5_reverse_mixed {
+        \find(\modality{#allmodal}{.. #lhs=#seBool0 || #nse1; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#seBool0 = TRUE)
+            \then({#lhs := TRUE}\modality{#allmodal}{.. ...}\endmodality (post))
+            \else(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_expression)
+        \displayname "assignment_or"
+    };
+
+    condition_mixed_left {
+        \find(\modality{#allmodal}{.. #lhs = #se0 ? #nse1 : #se2; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#se0 = TRUE)
+            \then(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+            \else({#lhs := #se2}\modality{#allmodal}{.. ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_prog)
+        \displayname "condition"
+    };
+
+    condition_mixed_right {
+        \find(\modality{#allmodal}{.. #lhs = #se0 ? #se1 : #nse2; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#se0 = TRUE)
+            \then({#lhs := #se1}\modality{#allmodal}{.. ...}\endmodality (post))
+            \else(\modality{#allmodal}{.. #lhs = #nse2; ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_prog)
+        \displayname "condidion"
+    };
+
+    condition_mixed {
+        \find(\modality{#allmodal}{.. #lhs = #se0 ? #nse1 : #nse2; ...}\endmodality (post))
+
+        \replacewith(
+            \if(#se0 = TRUE)
+            \then(\modality{#allmodal}{.. #lhs = #nse1; ...}\endmodality (post))
+            \else(\modality{#allmodal}{.. #lhs = #nse2; ...}\endmodality (post))
+        )
+
+        \heuristics(simplify_prog)
+        \displayname "condition"
+    };
+}