From 3871d896b61ad149cd620d1df384b07ccbb5d503 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Fri, 7 Jun 2024 11:56:27 +0200 Subject: [PATCH 1/5] retracing rules for if/else in Java --- .../ilkd/key/strategy/JavaCardDLStrategy.java | 12 ++-- .../de/uka/ilkd/key/proof/rules/javaRules.key | 1 + .../key/proof/rules/ruleSetsDeclarations.key | 5 ++ .../uka/ilkd/key/proof/rules/tracingRules.key | 70 +++++++++++++++++++ 4 files changed, 84 insertions(+), 4 deletions(-) create mode 100644 key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java index 960cd033f50..38713ebb099 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/JavaCardDLStrategy.java +++ b/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 diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key index c4317a71342..f3a9b7c6d97 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key +++ b/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; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key index 8141bd44ac4..f98576ea15f 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/ruleSetsDeclarations.key @@ -299,4 +299,9 @@ // double executeDoubleAssignment; + + // tracing + tracing; + traceIndexDelete; + traceIndexInc; } diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key new file mode 100644 index 00000000000..444803c7d04 --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key @@ -0,0 +1,70 @@ +\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) + }; + + 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) + }; + + deleteTraceIndex { + \assumes ( + traceNext(idx) ==> + ) + \find ( + traceIndex(idx) ==> + ) + \replacewith( ==> ) + \heuristics(traceIndexDelete) + }; + + nextTraceIndex { + \find ( + traceNext(idx) ==> + ) + \replacewith( + traceIndex(idx+1) ==> + ) + \heuristics(traceIndexInc) + }; +} From e5ca98aadf4b01f247d02157e766b411ad8983d0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Fri, 21 Jun 2024 21:41:28 +0200 Subject: [PATCH 2/5] added traceIfNoElse, traceElseNoElse tracing rules --- .../uka/ilkd/key/proof/rules/tracingRules.key | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key index 444803c7d04..1e6b5e2c097 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key @@ -31,6 +31,22 @@ \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 ( @@ -47,6 +63,21 @@ \heuristics(tracing) }; + traceElseNoElse { + \assumes (trace_O(idx), traceIndex(idx) ==> ) + \find ( + \modality{#allmodal}{.. + if (#se) #s1 + ...}\endmodality(post) + ) + \replacewith( + #se = TRUE -> \modality{#allmodal}{.. + ...}\endmodality(post) + ) + \add(traceNext(idx) ==> ) + \heuristics(tracing) + }; + deleteTraceIndex { \assumes ( traceNext(idx) ==> From 5976ad6411450da4a5a64ce2fef01edfc3cebe05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Tue, 25 Jun 2024 15:05:31 +0200 Subject: [PATCH 3/5] fix traceElseNoElse rule --- .../main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key index 1e6b5e2c097..174f2f684ca 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/tracingRules.key @@ -71,7 +71,7 @@ ...}\endmodality(post) ) \replacewith( - #se = TRUE -> \modality{#allmodal}{.. + #se = FALSE -> \modality{#allmodal}{.. ...}\endmodality(post) ) \add(traceNext(idx) ==> ) From 2ea6787fb77b87c1adf076acca1faf707a028e0e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Wed, 26 Jun 2024 09:29:27 +0200 Subject: [PATCH 4/5] added quicksort example --- .../heap/pathValidation/quicksort.key | 85 +++++++++++ .../pathValidation/quicksort/Quicksort.java | 134 ++++++++++++++++++ 2 files changed, 219 insertions(+) create mode 100644 key.ui/examples/heap/pathValidation/quicksort.key create mode 100644 key.ui/examples/heap/pathValidation/quicksort/Quicksort.java diff --git a/key.ui/examples/heap/pathValidation/quicksort.key b/key.ui/examples/heap/pathValidation/quicksort.key new file mode 100644 index 00000000000..e1e6b5d929e --- /dev/null +++ b/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" + } diff --git a/key.ui/examples/heap/pathValidation/quicksort/Quicksort.java b/key.ui/examples/heap/pathValidation/quicksort/Quicksort.java new file mode 100644 index 00000000000..086469f9c03 --- /dev/null +++ b/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 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; + + } +} From 5174398bce80c3d7bcd196351abe2f6673d4a293 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Lukas=20Gr=C3=A4tz?= Date: Sun, 30 Jun 2024 18:16:44 +0200 Subject: [PATCH 5/5] quicksort retrace in runallproofs --- .../de/uka/ilkd/key/proof/runallproofs/ProofCollections.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index c97e7ac2437..b2eddf49dba 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/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