diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 33c7977ff9a..edd68fca7e3 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -145,6 +145,7 @@ EQUAL_UNIQUE : '\\equalUnique'; NEW : '\\new'; NEW_TYPE_OF: '\\newTypeOf'; NEW_DEPENDING_ON: '\\newDependingOn'; +NEW_LOCAL_VARS: '\\newLocalVars'; HAS_ELEMENTARY_SORT:'\\hasElementarySort'; NEWLABEL : '\\newLabel'; CONTAINS_ASSIGNMENT : '\\containsAssignment'; diff --git a/key.core/src/main/antlr4/KeYParser.g4 b/key.core/src/main/antlr4/KeYParser.g4 index 733c83f6882..6d255549006 100644 --- a/key.core/src/main/antlr4/KeYParser.g4 +++ b/key.core/src/main/antlr4/KeYParser.g4 @@ -688,6 +688,7 @@ varexpId: // weigl, 2021-03-12: This will be later just an arbitrary identifier. | NEW | NEW_TYPE_OF | NEW_DEPENDING_ON + | NEW_LOCAL_VARS | HAS_ELEMENTARY_SORT | SAME | ISSUBTYPE diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java index a8a738e456f..4660fec9ba8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.visitor; + import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.SourceElement; @@ -16,6 +17,7 @@ import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; + /** * Walks through a java AST in depth-left-fist-order. This walker is used to transform a program * according to the given SVInstantiations. diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java index 4ab6590dcc7..4dd36d265d9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/TacletBuilderManipulators.java @@ -161,6 +161,8 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, } }; + public static final TacletBuilderCommand NEW_LOCAL_VARS = new ConstructorBasedBuilder( + "newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV); static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand { public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) { @@ -367,7 +369,8 @@ public IsLabeledCondition build(Object[] arguments, List parameters, // region Registry static { register(SAME_OBSERVER, SIMPLIFY_ITE_UPDATE, ABSTRACT_OR_INTERFACE, SAME, IS_SUBTYPE, - STRICT, DISJOINT_MODULO_NULL, NEW_JAVATYPE, NEW_VAR, FREE_1, FREE_2, FREE_3, FREE_4, + STRICT, DISJOINT_MODULO_NULL, NEW_JAVATYPE, NEW_VAR, NEW_LOCAL_VARS, FREE_1, FREE_2, + FREE_3, FREE_4, FREE_5, NEW_TYPE_OF, NEW_DEPENDING_ON, FREE_LABEL_IN_VARIABLE, DIFFERENT, FINAL, ENUM_CONST, LOCAL_VARIABLE, ARRAY_LENGTH, ARRAY, REFERENCE_ARRAY, MAY_EXPAND_METHOD_2, MAY_EXPAND_METHOD_3, STATIC_METHOD, THIS_REFERENCE, REFERENCE, ENUM_TYPE, diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java new file mode 100644 index 00000000000..8b6946277fb --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java @@ -0,0 +1,111 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.rule.conditions; + +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.Statement; +import de.uka.ilkd.key.java.abstraction.ArrayType; +import de.uka.ilkd.key.java.abstraction.KeYJavaType; +import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration; +import de.uka.ilkd.key.java.declaration.VariableDeclaration; +import de.uka.ilkd.key.java.declaration.VariableSpecification; +import de.uka.ilkd.key.java.reference.TypeRef; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.VariableCondition; +import de.uka.ilkd.key.rule.inst.ProgramList; +import de.uka.ilkd.key.rule.inst.SVInstantiations; +import de.uka.ilkd.key.util.MiscTools; + +import org.key_project.logic.SyntaxElement; +import org.key_project.util.collection.*; + +/** + * For the loop scope rule, if a local program variable that may be altered by the loop body appears + * in the frame condition, + * it is necessary to use the value before the loop first executes in the frame condition. + *
+ * To achieve this, this condition generates (1) the "before" version of each variable that may be + * written to by the loop + * {@link MiscTools#getLocalOuts(ProgramElement, Services)}; (2) an update storing the value of each + * such PV in its "before" version, + * i.e., {@code {...||i_before := i||...}}; (3) the reverse of the update, to be applied to the + * frame condition, i.e., + * {@code {...||i := i_before||...}}. + */ +public class NewLocalVarsCondition implements VariableCondition { + /** + * A SV that will store variable declarations for the "before" version of variables. + */ + private final SchemaVariable varDeclsSV; + /** + * Will store the update {@code {...||i_before := i||...}}. + */ + private final SchemaVariable updateBeforeSV; + /** + * Will store the update {@code {...||i := i_before||...}}. + */ + private final SchemaVariable updateFrameSV; + /** + * The loop body. + */ + private final SchemaVariable bodySV; + + public NewLocalVarsCondition(SchemaVariable varDeclsSV, SchemaVariable updateBeforeSV, + SchemaVariable updateFrameSV, SchemaVariable bodySV) { + this.varDeclsSV = varDeclsSV; + this.updateBeforeSV = updateBeforeSV; + this.updateFrameSV = updateFrameSV; + this.bodySV = bodySV; + } + + @Override + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions matchCond, Services services) { + SVInstantiations svInst = matchCond.getInstantiations(); + if (svInst.getInstantiation(varDeclsSV) != null) { + return matchCond; + } + var body = (Statement) svInst.getInstantiation(bodySV); + if (body == null) { + return matchCond; + } + + var vars = MiscTools.getLocalOuts(body, services); + List decls = new ArrayList<>(vars.size()); + ImmutableList updatesBefore = ImmutableSLList.nil(); + ImmutableList updatesFrame = ImmutableSLList.nil(); + var tb = services.getTermBuilder(); + for (var v : vars) { + final var newName = + services.getVariableNamer().getTemporaryNameProposal(v.name() + "_before"); + KeYJavaType type = v.getKeYJavaType(); + var locVar = new LocationVariable(newName, type); + var spec = new VariableSpecification(locVar); + int dim = 0; + if (type.getJavaType() instanceof ArrayType at) { + dim = at.getDimension(); + } + decls.add(new LocalVariableDeclaration(new TypeRef(type, dim), spec)); + updatesBefore = updatesBefore.append(tb.elementary(tb.var(locVar), tb.var(v))); + updatesFrame = updatesFrame.append(tb.elementary(tb.var(v), tb.var(locVar))); + } + return matchCond.setInstantiations( + svInst.add(varDeclsSV, new ProgramList(new ImmutableArray<>(decls)), services) + .add(updateBeforeSV, tb.parallel(updatesBefore), services) + .add(updateFrameSV, tb.parallel(updatesFrame), services)); + } + + @Override + public String toString() { + return "\\newLocalVars(" + varDeclsSV + ", " + updateBeforeSV + ", " + updateFrameSV + ", " + + bodySV + ")"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java index 2fd78336ecd..64fa09efd47 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateBeforeLoopUpdate.java @@ -7,14 +7,13 @@ import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; -import de.uka.ilkd.key.logic.op.AbstractTermTransformer; -import de.uka.ilkd.key.logic.op.Modality; -import de.uka.ilkd.key.logic.op.UpdateableOperator; +import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.util.MiscTools; import org.key_project.logic.Name; + /** * Initializes the "before loop" update needed for the modifiable clause. * @@ -64,7 +63,8 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { * @return The anonymizing update. */ private static Term createBeforeLoopUpdate(boolean isTransaction, boolean isPermissions, - Term anonHeapTerm, Term anonSavedHeapTerm, Term anonPermissionsHeapTerm, + Term anonHeapTerm, Term anonSavedHeapTerm, + Term anonPermissionsHeapTerm, Services services) { final TermBuilder tb = services.getTermBuilder(); final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java index 664cade98d6..55bf0474207 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java @@ -11,10 +11,7 @@ import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.TermBuilder; -import de.uka.ilkd.key.logic.op.AbstractTermTransformer; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.Modality; -import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.speclang.HeapContext; import de.uka.ilkd.key.speclang.LoopSpecification; @@ -102,7 +99,6 @@ private static Term createFrameCondition(final LoopSpecification loopSpec, frameCondition = frameCondition == null ? fc : tb.and(frameCondition, fc); } - return frameCondition; } diff --git a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj index fcd2b2178e8..426a64aa21a 100644 --- a/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj +++ b/key.core/src/main/javacc/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj @@ -4365,7 +4365,7 @@ RKeYMetaConstruct KeYMetaConstructStatement() : return result; } ) - | + | ( "#resolve-multiple-var-decl" "(" stat = Statement() ")" ";" { diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopScopeRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopScopeRules.key index d6db7643b05..4742f5e01c2 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopScopeRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/loopScopeRules.key @@ -38,6 +38,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post))) @@ -46,6 +49,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post))) // Implementation Note (DS, 2019-04-11): We have to separately store the active statement @@ -71,8 +75,14 @@ #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; + #localVarDeclsBefore_LOOP }\endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #permissionsBefore_LOOP) + || #updateBefore_LOOP || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} @@ -93,7 +103,11 @@ (#x<> = TRUE -> post) & (#x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + & {#updateFrame_LOOP} #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #permissionsBefore_LOOP) & prec(variantTerm, #variant)) ))) ) @@ -117,6 +131,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post))) @@ -124,6 +141,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post))) \varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post))) @@ -140,10 +158,12 @@ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; + #localVarDeclsBefore_LOOP } \endmodality ( {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) + || #updateBefore_LOOP || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} (inv & freeInv -> (\modality{#box}{ @@ -162,7 +182,11 @@ (#x<> = TRUE -> post) & (#x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)) + & {#updateFrame_LOOP} #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #permissionsBefore_LOOP)) ))) ) ) @@ -221,6 +245,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post))) @@ -229,6 +256,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post))) \varcond(\storeStmtIn(#loopStmt, \modality{#dia}{ while (#nse) #body }\endmodality (post))) @@ -247,10 +275,12 @@ #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; + #localVarDeclsBefore_LOOP } \endmodality ( {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) + || #updateBefore_LOOP || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} (inv & freeInv -> @@ -269,7 +299,11 @@ }\endmodality ( #x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + & {#updateFrame_LOOP} #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #permissionsBefore_LOOP) & prec(variantTerm, #variant) ))) ) @@ -327,6 +361,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post))) @@ -334,6 +371,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarDeclsBefore_LOOP, #updateBefore_LOOP, #updateFrame_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post))) \varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post))) @@ -349,10 +387,12 @@ \modality{#box}{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; + #localVarDeclsBefore_LOOP } \endmodality ( {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) + || #updateBefore_LOOP || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} (inv & freeInv -> (\modality{#box}{ @@ -370,7 +410,11 @@ }\endmodality ( #x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + & {#updateFrame_LOOP} #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #permissionsBefore_LOOP) ))) ) ) diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 2e397ca646a..702b2efd048 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -1,5 +1,5 @@ # This files contains representation of taclets, which are accepted and revised. -# Date: Wed Jun 26 12:45:30 CEST 2024 +# Date: Mon Nov 04 13:26:34 CET 2024 == abortJavaCardTransactionAPI (abortJavaCardTransactionAPI) ========================================= abortJavaCardTransactionAPI { @@ -12571,7 +12571,7 @@ loopScopeInvBox { \find(#box ((modal operator))|{{ .. while (#nse) #body ... }}| (post)) -\varcond(\new(#permissionsBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#savedHeapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#heapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#x (program Variable), (type, sort): (boolean,boolean)), \varcond (\storeTermIn(loopFormula (formula), #box ((modal operator))|{{ +\varcond(\new(#permissionsBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#savedHeapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#heapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#x (program Variable), (type, sort): (boolean,boolean)), \newLocalVars(#localVarDeclsBefore_LOOP (program Statement), #updateBefore_LOOP (update), #updateFrame_LOOP (update), #body (program Statement)), \varcond (\storeTermIn(loopFormula (formula), #box ((modal operator))|{{ while (#nse) #body }}| (post))), \varcond (\storeStmtIn(#loopStmt (program Statement), #box ((modal operator))|{{ while (#nse) #body @@ -12580,7 +12580,8 @@ loopScopeInvBox { #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; -}}| (update-application(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP),#createLocalAnonUpdate(loopFormula)),#createHeapAnonUpdate(loopFormula,anon_heap_LOOP,anon_savedHeap_LOOP,anon_permissions_LOOP)),imp(and(inv,freeInv),#box ((modal operator))|{{ .. + #localVarDeclsBefore_LOOP +}}| (update-application(parallel-upd(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP),#createLocalAnonUpdate(loopFormula)),#updateBefore_LOOP),#createHeapAnonUpdate(loopFormula,anon_heap_LOOP,anon_savedHeap_LOOP,anon_permissions_LOOP)),imp(and(inv,freeInv),#box ((modal operator))|{{ .. boolean #x; loop-scope (#x) { if (#nse) { @@ -12590,7 +12591,7 @@ loopScopeInvBox { break; } } -... }}| (and(imp(equals(#x<>,TRUE),post),imp(equals(#x<>,FALSE),and(inv,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP))))))))) ; +... }}| (and(imp(equals(#x<>,TRUE),post),imp(equals(#x<>,FALSE),and(inv,update-application(#updateFrame_LOOP,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP)))))))))) ; \replacewith(inv) \heuristics(loop_scope_inv_taclet) Choices: (programRules:Java & javaLoopTreatment:efficient)} @@ -12600,7 +12601,7 @@ loopScopeInvDia { \find(#dia ((modal operator))|{{ .. while (#nse) #body ... }}| (post)) -\varcond(\new(#permissionsBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#savedHeapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#heapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#variant (program Variable), KeYJavaType:null,any), \new(#x (program Variable), (type, sort): (boolean,boolean)), \varcond (\storeTermIn(loopFormula (formula), #dia ((modal operator))|{{ +\varcond(\new(#permissionsBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#savedHeapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#heapBefore_LOOP (program Variable), KeYJavaType:null,Heap), \new(#variant (program Variable), KeYJavaType:null,any), \new(#x (program Variable), (type, sort): (boolean,boolean)), \newLocalVars(#localVarDeclsBefore_LOOP (program Statement), #updateBefore_LOOP (update), #updateFrame_LOOP (update), #body (program Statement)), \varcond (\storeTermIn(loopFormula (formula), #dia ((modal operator))|{{ while (#nse) #body }}| (post))), \varcond (\storeStmtIn(#loopStmt (program Statement), #dia ((modal operator))|{{ while (#nse) #body @@ -12610,7 +12611,8 @@ loopScopeInvDia { #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; -}}| (update-application(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP),#createLocalAnonUpdate(loopFormula)),#createHeapAnonUpdate(loopFormula,anon_heap_LOOP,anon_savedHeap_LOOP,anon_permissions_LOOP)),update-application(elem-update(#variant (program Variable))(variantTerm),imp(and(inv,freeInv),#dia ((modal operator))|{{ .. + #localVarDeclsBefore_LOOP +}}| (update-application(parallel-upd(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP),#updateBefore_LOOP),#createLocalAnonUpdate(loopFormula)),#createHeapAnonUpdate(loopFormula,anon_heap_LOOP,anon_savedHeap_LOOP,anon_permissions_LOOP)),update-application(elem-update(#variant (program Variable))(variantTerm),imp(and(inv,freeInv),#dia ((modal operator))|{{ .. boolean #x; loop-scope (#x) { if (#nse) { @@ -12620,7 +12622,7 @@ loopScopeInvDia { break; } } -... }}| (and(imp(equals(#x<>,TRUE),post),imp(equals(#x<>,FALSE),and(and(inv,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP)),prec(variantTerm,#variant)))))))))) ; +... }}| (and(imp(equals(#x<>,TRUE),post),imp(equals(#x<>,FALSE),and(and(inv,update-application(#updateFrame_LOOP,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#permissionsBefore_LOOP))),prec(variantTerm,#variant)))))))))) ; \replacewith(inv) \heuristics(loop_scope_inv_taclet) Choices: (programRules:Java & javaLoopTreatment:efficient)} diff --git a/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof b/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof index b772b95f7a1..a07ede2b6c4 100644 --- a/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof +++ b/key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof @@ -359,6 +359,7 @@ (rule "variableDeclaration" (formula "9") (term "1") (newnames "h_1") (userinteraction)) (rule "variableDeclaration" (formula "9") (term "1") (newnames "h_2") (userinteraction)) (rule "variableDeclaration" (formula "9") (term "1") (newnames "x_1") (userinteraction)) + (rule "variableDeclaration" (formula "9") (term "1") (newnames "i_before") (userinteraction)) (rule "emptyModality" (formula "9") (term "1") (userinteraction)) (rule "false_to_not_true" (formula "9") (term "0,1,0,1,1,1,1")) (rule "concrete_and_3" (formula "9") (term "0,1,1,1")) @@ -366,6 +367,7 @@ (rule "concrete_and_3" (formula "9") (term "0,0,1,0,0,0,0,1,1,1")) (rule "expandInInt" (formula "9") (term "1,0,0,0,0,0,0,0,1,1,1")) (rule "concrete_and_3" (formula "9") (term "0,0,0,0,0,0,0,1,1,1")) + (rule "simplifyUpdate2" (formula "9") (term "1,0,1,1,0,1,1,1,1") (userinteraction)) (rule "elementOfAllFields" (formula "9") (term "0,0,0,0,1,0,1,1,0,1,1,1,1")) (rule "expandInInt" (formula "9") (term "1,0,0,1,0,0,0,0,0,1,1,0,1,1,1,1")) (rule "concrete_and_3" (formula "9") (term "0,0,1,0,0,0,0,0,1,1,0,1,1,1,1")) diff --git a/key.ui/examples/heap/permutedSum/perm.proof b/key.ui/examples/heap/permutedSum/perm.proof index e2932c2455a..f887e68ffce 100644 --- a/key.ui/examples/heap/permutedSum/perm.proof +++ b/key.ui/examples/heap/permutedSum/perm.proof @@ -101,6 +101,7 @@ (rule "variableDeclaration" (formula "9") (term "1") (newnames "h_1") (userinteraction)) (rule "variableDeclaration" (formula "9") (term "1") (newnames "h_2") (userinteraction)) (rule "variableDeclaration" (formula "9") (term "1") (newnames "x") (userinteraction)) + (rule "variableDeclaration" (formula "9") (term "1") (newnames "s_before") (userinteraction)) (rule "emptyModality" (formula "9") (term "1") (userinteraction)) (builtin "One Step Simplification" (formula "9") (userinteraction)) (rule "impRight" (formula "9")) diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java b/keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java index da4981d9aea..d930d1821e3 100644 --- a/keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java +++ b/keyext.slicing/src/test/java/org/key_project/slicing/EndToEndTests.java @@ -78,15 +78,15 @@ void sliceMultipleIterations() throws Exception { Pair iteration1 = sliceProofFullFilename( new File(testCaseDirectory, "../../../../../key.ui/examples/firstTouch/05-ReverseArray/reverseArray.proof"), - 6535, 4234, true, true, true); + 6537, 4236, true, true, true); Pair iteration2 = - sliceProofFullFilename(iteration1.second, 4234, 4227, true, true, true); + sliceProofFullFilename(iteration1.second, 4236, 4229, true, true, true); Pair iteration3 = - sliceProofFullFilename(iteration2.second, 4227, 4218, true, true, true); + sliceProofFullFilename(iteration2.second, 4229, 4220, true, true, true); Pair iteration4 = - sliceProofFullFilename(iteration3.second, 4218, 4207, true, true, true); + sliceProofFullFilename(iteration3.second, 4220, 4209, true, true, true); Pair iteration5 = - sliceProofFullFilename(iteration4.second, 4207, 4195, true, true, true); + sliceProofFullFilename(iteration4.second, 4209, 4197, true, true, true); iteration5.first.dispose(); iteration4.first.dispose(); iteration3.first.dispose(); diff --git a/qodana.yaml b/qodana.yaml index b3b5169048b..c5ff020c321 100644 --- a/qodana.yaml +++ b/qodana.yaml @@ -1,4 +1,4 @@ version: "1.0" -linter: jetbrains/qodana-jvm-community:2022.1 +linter: jetbrains/qodana-jvm-community:2024.2 profile: path: ./.github/qodana.starter.full.xml