Lukas tracing

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,16 @@ private RuleSetDispatchFeature setupCostComputationF() {
                 applyTF(instOf("uSub"), IsInductionVariable.INSTANCE), longConst(0), inftyConst()));
         }
 
+        setupTracingStrategy(d);
         return d;
     }
 
+    private void setupTracingStrategy(RuleSetDispatchFeature d) {
+        bindRuleSet(d, "tracing", longConst(-200));
+        bindRuleSet(d, "traceIndexDelete", longConst(-50000));
+        bindRuleSet(d, "traceIndexInc", longConst(-500));
+    }
+
     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/proof/rules/javaRules.key

@@ -6,6 +6,7 @@
 
 
 \include assertions;
+\include tracingRules;
 
 \schemaVariables {
     \modalOperator {diamond, box, diamond_transaction, box_transaction} #allmodal;

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key

@@ -299,4 +299,9 @@
 
     // double
     executeDoubleAssignment;
+
+    // tracing
+    tracing;
+    traceIndexDelete;
+    traceIndexInc;
 }

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key

@@ -0,0 +1,101 @@
+\predicates {
+    traceIndex(int);
+    trace_I(int);
+    trace_O(int);
+    traceNext(int);
+}
+
+\schemaVariables {
+    \modalOperator {diamond, box, diamond_transaction, box_transaction} #allmodal;
+    \program SimpleExpression #se;
+    \program Statement #s1, #s2;
+    \formula post;
+    \term int idx;
+}
+
+\rules(programRules:Java) {
+
+    traceIf {
+        \assumes (trace_I(idx), traceIndex(idx) ==> )
+        \find (
+           \modality{#allmodal}{..
+               if (#se) #s1 else #s2
+           ...}\endmodality(post)
+        )
+        \replacewith(
+            #se = TRUE -> \modality{#allmodal}{..
+                #s1
+            ...}\endmodality(post)
+        )
+        \add(traceNext(idx) ==> )
+        \heuristics(tracing)
+    };
+
+    traceIfNoElse {
+        \assumes (trace_I(idx), traceIndex(idx) ==> )
+        \find (
+           \modality{#allmodal}{..
+               if (#se) #s1
+           ...}\endmodality(post)
+        )
+        \replacewith(
+            #se = TRUE -> \modality{#allmodal}{..
+                #s1
+            ...}\endmodality(post)
+        )
+        \add(traceNext(idx) ==> )
+        \heuristics(tracing)
+    };
+
+    traceElse {
+        \assumes (trace_O(idx), traceIndex(idx) ==> )
+        \find (
+            \modality{#allmodal}{..
+                if (#se) #s1 else #s2
+            ...}\endmodality(post)
+        )
+        \replacewith(
+            #se = FALSE -> \modality{#allmodal}{..
+                #s2
+            ...}\endmodality(post)
+        )
+        \add(traceNext(idx) ==> )
+        \heuristics(tracing)
+    };
+
+    traceElseNoElse {
+        \assumes (trace_O(idx), traceIndex(idx) ==> )
+        \find (
+           \modality{#allmodal}{..
+               if (#se) #s1
+           ...}\endmodality(post)
+        )
+        \replacewith(
+            #se = FALSE -> \modality{#allmodal}{..
+            ...}\endmodality(post)
+        )
+        \add(traceNext(idx) ==> )
+        \heuristics(tracing)
+    };
+
+    deleteTraceIndex {
+        \assumes (
+            traceNext(idx) ==>
+        )
+        \find (
+            traceIndex(idx) ==>
+        )
+        \replacewith( ==> )
+        \heuristics(traceIndexDelete)
+    };
+
+    nextTraceIndex {
+        \find (
+            traceNext(idx) ==>
+        )
+        \replacewith(
+            traceIndex(idx+1) ==>
+        )
+        \heuristics(traceIndexInc)
+    };
+}

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java

@@ -372,6 +372,8 @@ public static ProofCollection automaticJavaDL() throws IOException {
         g.provable("sort.key");
         g.provable("split.key");
 
+        g = c.group("path_validation");
+        g.provable("heap/pathValidation/quicksort.key");
 
         /*
          * These are simpler regression tests that show a certain feature works

key.ui/examples/heap/pathValidation/quicksort.key

@@ -0,0 +1,85 @@
+\profile "Java Profile";
+
+\settings // Proof-Settings-Config-File
+{ 
+    "Choice" : { 
+        "JavaCard" : "JavaCard:off",
+        "Strings" : "Strings:on",
+        "assertions" : "assertions:safe",
+        "bigint" : "bigint:on",
+        "floatRules" : "floatRules:strictfpOnly",
+        "initialisation" : "initialisation:disableStaticInitialisation",
+        "intRules" : "intRules:arithmeticSemanticsIgnoringOF",
+        "integerSimplificationRules" : "integerSimplificationRules:full",
+        "javaLoopTreatment" : "javaLoopTreatment:efficient",
+        "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off",
+        "methodExpansion" : "methodExpansion:modularOnly",
+        "modelFields" : "modelFields:treatAsAxiom",
+        "moreSeqRules" : "moreSeqRules:on",
+        "permissions" : "permissions:off",
+        "programRules" : "programRules:Java",
+        "reach" : "reach:on",
+        "runtimeExceptions" : "runtimeExceptions:ban",
+        "sequences" : "sequences:on",
+        "wdChecks" : "wdChecks:off",
+        "wdOperator" : "wdOperator:L"
+     },
+    "Labels" : { 
+        "UseOriginLabels" : true
+     },
+    "NewSMT" : { 
+
+     },
+    "SMTSettings" : { 
+        "SelectedTaclets" : [ 
+
+         ],
+        "UseBuiltUniqueness" : false,
+        "explicitTypeHierarchy" : false,
+        "instantiateHierarchyAssumptions" : true,
+        "integersMaximum" : 2147483645,
+        "integersMinimum" : -2147483645,
+        "invariantForall" : false,
+        "maxGenericSorts" : 2,
+        "useConstantsForBigOrSmallIntegers" : true,
+        "useUninterpretedMultiplication" : true
+     },
+    "Strategy" : { 
+        "ActiveStrategy" : "JavaCardDLStrategy",
+        "MaximumNumberOfAutomaticApplications" : 100000,
+        "Timeout" : -1,
+        "options" : { 
+            "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF",
+            "BLOCK_OPTIONS_KEY" : "BLOCK_EXPAND",
+            "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_FREE",
+            "DEP_OPTIONS_KEY" : "DEP_ON",
+            "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE",
+            "LOOP_OPTIONS_KEY" : "LOOP_EXPAND",
+            "METHOD_OPTIONS_KEY" : "METHOD_EXPAND",
+            "MPS_OPTIONS_KEY" : "MPS_MERGE",
+            "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS",
+            "OSS_OPTIONS_KEY" : "OSS_ON",
+            "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS",
+            "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON",
+            "QUERY_NEW_OPTIONS_KEY" : "QUERY_OFF",
+            "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED",
+            "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT",
+            "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER",
+            "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF",
+            "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF",
+            "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF",
+            "VBT_PHASE" : "VBT_SYM_EX"
+         }
+     }
+ } 
+
+\javaSource "quicksort";
+
+\proofObligation 
+// Proof-Obligation settings
+{ 
+    "class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
+    "contract" : "quicksort.Quicksort[quicksort.Quicksort::sort([I)].JML normal_behavior operation contract.0",
+    "name" : "quicksort.Quicksort[quicksort.Quicksort::sort([I)].JML normal_behavior operation contract.0"
+ }

key.ui/examples/heap/pathValidation/quicksort/Quicksort.java

@@ -0,0 +1,134 @@
+/**
+ * This example formalizes and verifies the wellknown quicksort
+ * algorithm for int-arrays algorithm.  It shows that the array
+ * is sorted in  the end and that it contains  a permutation of
+ * the original input.
+ *
+ * The   proofs   for   the  main   method   sort(int[])   runs
+ * automatically   while   the   other  two   methods   require
+ * interaction.  You   can  load   the  files   "sort.key"  and
+ * "split.key"  from the  example's  directory  to execute  the
+ * according proof scripts.
+ *
+ * The permutation property requires some interaction: The idea
+ * is that the only actual modification on the array are swaps
+ * within the "split" method. The sort method body contains
+ * three method invocations which each maintain the permutation
+ * property. By a repeated appeal to the transitivity of the
+ * permutation property, the entire algorithm can be proved to
+ * only permute the array.
+ *
+ * To establish  monotonicity, the key  is to specify  that the
+ * currently  handled block  contains  only  numbers which  are
+ * between   the    two   pivot   values    array[from-1]   and
+ * array[to]. The first  and last block are exempt  from one of
+ * these  conditions  since  they have  only  one  neighbouring
+ * block.
+ *
+ * The  example has  been  added  to show  the  power of  proof
+ * scripts.
+ *
+ * @author Mattias Ulbrich, 2015
+ *
+ * Modified  to run fully automatically for Retrospective  Path
+ * Validation. This is a form of partial verification. We first
+ * record a control flow trace (instrumentation for a automatic
+ * recording can be done with the help of JavaParser)  and then
+ * we validate the the single recorded control flow against the
+ * specification (the method contract). No auxialliary specifi-
+ * cation needed (no loop invariants, no contracts  for  called
+ * methods, no proof scripts)!
+ *
+ * KeY Strategy Settings:
+ *   Loop Treatment: Expand (Transformation)
+ *   Method Treatment: Expand
+ *
+ * Or just load quicksort.key
+ *
+ * Lukas Gra"tz, 2023/24
+ */
+
+package quicksort;
+
+class Quicksort {
+
+    /*@ public normal_behaviour
+      @
+      @ //-- Below is the recorded control flow trace
+      @ //-- (rules for predicates trace_O() & I(), traceIndex() are included in this KeY-version)
+      @ requires \dl_traceIndex(0);
+      @ requires \dl_trace_I(0);
+      @ requires \dl_trace_I(1);
+      @ requires \dl_trace_I(2);
+      @ requires \dl_trace_O(3);
+      @ requires \dl_trace_I(4);
+      @ requires \dl_trace_O(5);
+      @ requires \dl_trace_I(6);
+      @ requires \dl_trace_O(7);
+      @ requires \dl_trace_I(8);
+      @ requires \dl_trace_O(9);
+      @ requires \dl_trace_O(10);
+      @ requires \dl_trace_O(11);
+      @ requires \dl_trace_I(12);
+      @ requires \dl_trace_I(13);
+      @ requires \dl_trace_O(14);
+      @ requires \dl_trace_I(15);
+      @ requires \dl_trace_I(16);
+      @ requires \dl_trace_I(17);
+      @ requires \dl_trace_O(18);
+      @ requires \dl_trace_O(19);
+      @ requires \dl_trace_O(20);
+      @ requires \dl_trace_I(21);
+      @ requires \dl_trace_I(22);
+      @ requires \dl_trace_O(23);
+      @ requires \dl_trace_O(24);
+      @ requires \dl_trace_O(25);
+      @ requires \dl_trace_O(26);
+      @
+      @  //-- the following ensures with seqPerm cannot be shown in auto mode with default options:
+      @  //ensures \dl_seqPerm(\dl_array2seq(array), \old(\dl_array2seq(array)));
+      @  //-- equivalent ensures with \num_of:
+      @  ensures (\forall int j; 0<=j && j < array.length;
+      @               (\num_of int i; 0<=i && i < array.length; \old(array[i]) == array[j])
+      @            == (\num_of int i; 0<=i && i < array.length;      array[i]  == array[j])
+      @          );
+      @
+      @  ensures (\forall int i; 0<=i && i<array.length-1; array[i] <= array[i+1]);
+      @
+      @  assignable array[*];
+      @*/
+    public static void sort(int[] array) {
+        if(array.length > 0) { // 0
+            sort(array, 0, array.length-1);
+        }
+    }
+
+    private static void sort(int[] array, int from, int to) {
+        if(from < to) { // 1, 12, 21
+            int splitPoint = split(array, from, to);
+            sort(array, from, splitPoint-1);
+            sort(array, splitPoint+1, to);
+        } // 11, 20, 25, 26
+    }
+
+    private static int split(int[] array, int from, int to) {
+
+        int i = from;
+        int pivot = array[to];
+
+        for(int j = from; j < to; j++) { // 2, 4, 6, 8, 13, 15, 17, 22
+            if(array[j] <= pivot) { // 16
+                int t = array[i];
+                array[i] = array[j];
+                array[j] = t;
+                i++;
+            } // 3, 5, 7, 9, 14, 18, 23
+        } // 10, 19, 24
+
+        array[to] = array[i];
+        array[i] = pivot;
+
+        return i;
+
+    }
+}