From 8f7b21f667609707d5be5c0ab0b5d63a7cf59948 Mon Sep 17 00:00:00 2001 From: Drodt Date: Wed, 30 Oct 2024 13:57:01 +0100 Subject: [PATCH 1/9] Fix 3524 --- key.core/src/main/antlr4/KeYLexer.g4 | 1 + key.core/src/main/antlr4/KeYParser.g4 | 1 + .../key/java/SchemaRecoder2KeYConverter.java | 2 + .../java/visitor/ProgramReplaceVisitor.java | 16 +++++ .../varexp/TacletBuilderManipulators.java | 5 +- .../conditions/NewLocalVarsCondition.java | 66 +++++++++++++++++++ .../ilkd/key/rule/inst/LocationVarMap.java | 22 +++++++ .../metaconstruct/CreateBeforeLoopUpdate.java | 37 +++++++++-- .../rule/metaconstruct/CreateFrameCond.java | 31 +++++++-- .../metaconstruct/DeclareLocalLoopVars.java | 54 +++++++++++++++ .../key/rule/tacletbuilder/TacletBuilder.java | 4 ++ .../key/parser/schemajava/SchemaJavaParser.jj | 13 ++++ .../ilkd/key/proof/rules/loopScopeRules.key | 57 +++++++++++++--- 13 files changed, 284 insertions(+), 25 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java 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/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index 1b0a1f4c1bc..ed2cc8ff3d2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -134,6 +134,8 @@ public ProgramTransformer convert(de.uka.ilkd.key.java.recoderext.RKeYMetaConstr return new InitArrayCreation(mc.getFirstSV().getSV(), list.get(Expression.class)); } else if ("#reattachLoopInvariant".equals(mcName)) { return new ReattachLoopInvariant(list.get(LoopStatement.class)); + } else if ("#declare-local-loop-vars".equals(mcName)) { + return new DeclareLocalLoopVars(list.get(Expression.class)); } else { throw new ConvertException("Program meta construct " + mc + " unknown."); } 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..47ac486039f 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,11 +3,15 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.visitor; +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.SourceElement; import de.uka.ilkd.key.logic.ProgramInLogic; 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.AbstractProgramElement; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -15,6 +19,9 @@ import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.ImmutableMap; + +import org.jspecify.annotations.NonNull; /** * Walks through a java AST in depth-left-fist-order. This walker is used to transform a program @@ -82,6 +89,15 @@ public void performActionOnSchemaVariable(SchemaVariable sv) { addChildren(instArray); } else if (inst instanceof Term && ((Term) inst).op() instanceof ProgramInLogic) { addChild(services.getTypeConverter().convertToProgramElement((Term) inst)); + } else if (inst instanceof ImmutableMap) { + @SuppressWarnings("unchecked") + final ImmutableMap<@NonNull LocationVariable, LocationVariable> map = + (ImmutableMap<@NonNull LocationVariable, LocationVariable>) inst; + List lst = new ArrayList<>(); + for (var e : map) { + lst.add(e.value()); + } + addChildren(new ImmutableArray<>(lst)); } else { throw new IllegalStateException( "programreplacevisitor: Instantiation missing " + "for schema variable " + sv); 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..b0d4e67b92a 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); 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..32a6a3c5812 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/NewLocalVarsCondition.java @@ -0,0 +1,66 @@ +/* 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 de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.Statement; +import de.uka.ilkd.key.java.abstraction.KeYJavaType; +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.LocationVarMap; +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.DefaultImmutableMap; +import org.key_project.util.collection.ImmutableMap; + +import org.jspecify.annotations.NonNull; + +/** + * Collects all local variables written to in {@code bodySV} and instantiates {@code varsSV} with a + * map + * from these variables to their (newly created, unique) "before" version. + */ +public class NewLocalVarsCondition implements VariableCondition { + private final SchemaVariable varsSV; + private final SchemaVariable bodySV; + + public NewLocalVarsCondition(SchemaVariable vars, SchemaVariable body) { + this.varsSV = vars; + this.bodySV = body; + } + + @Override + public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, + MatchConditions matchCond, Services services) { + SVInstantiations svInst = matchCond.getInstantiations(); + if (svInst.getInstantiation(varsSV) != null) { + return matchCond; + } + var body = (Statement) svInst.getInstantiation(bodySV); + if (body == null) { + return matchCond; + } + + var vars = MiscTools.getLocalOuts(body, services); + ImmutableMap<@NonNull LocationVariable, LocationVariable> map = + DefaultImmutableMap.nilMap(); + for (var v : vars) { + final var newName = + services.getVariableNamer().getTemporaryNameProposal(v.name() + "_before"); + KeYJavaType type = v.getKeYJavaType(); + var locVar = new LocationVariable(newName, type); + map = map.put(v, locVar); + } + return matchCond.setInstantiations(svInst.add(varsSV, new LocationVarMap(map), services)); + } + + @Override + public String toString() { + return "\\newLocalVars(" + varsSV + ", " + bodySV + ")"; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java new file mode 100644 index 00000000000..b0f42ec1b8c --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java @@ -0,0 +1,22 @@ +/* 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.inst; + +import de.uka.ilkd.key.logic.op.LocationVariable; + +import org.key_project.util.collection.ImmutableMap; + +import org.jspecify.annotations.NonNull; + +public class LocationVarMap + extends InstantiationEntry> { + /** + * creates a new instantiation entry for the instantiation to be stored + * + * @param instantiation the instantiation to be stored + */ + public LocationVarMap(ImmutableMap<@NonNull LocationVariable, LocationVariable> instantiation) { + super(instantiation); + } +} 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..028d168d371 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,13 +7,16 @@ 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; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableMap; +import org.key_project.util.collection.ImmutableSLList; + +import org.jspecify.annotations.NonNull; /** * Initializes the "before loop" update needed for the modifiable clause. @@ -34,7 +37,7 @@ public final class CreateBeforeLoopUpdate extends AbstractTermTransformer { public CreateBeforeLoopUpdate() { - super(new Name("#createBeforeLoopUpdate"), 4); + super(new Name("#createBeforeLoopUpdate"), 5); } @Override @@ -43,10 +46,18 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { final Term anonHeapTerm = term.sub(1); final Term anonSavedHeapTerm = term.sub(2); - final Term anonPermissionsHeapTerm = term.sub(3); + final Term localVarsBeforeSV = term.sub(3); + final Term anonPermissionsHeapTerm = term.sub(4); + + // We have a SV for the local vars written to in the loop. Get its inst, which is a map from + // the original variable to its "before" version. + @SuppressWarnings("unchecked") + final var localVarsBefore = + (ImmutableMap<@NonNull LocationVariable, LocationVariable>) svInst + .getInstantiation((SchemaVariable) localVarsBeforeSV.op()); return createBeforeLoopUpdate(MiscTools.isTransaction(((Modality) loopTerm.op()).kind()), - MiscTools.isPermissions(services), anonHeapTerm, anonSavedHeapTerm, + MiscTools.isPermissions(services), anonHeapTerm, anonSavedHeapTerm, localVarsBefore, anonPermissionsHeapTerm, services); } @@ -64,7 +75,9 @@ 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, + ImmutableMap<@NonNull LocationVariable, LocationVariable> localVarsBefore, + Term anonPermissionsHeapTerm, Services services) { final TermBuilder tb = services.getTermBuilder(); final HeapLDT heapLDT = services.getTypeConverter().getHeapLDT(); @@ -83,6 +96,16 @@ private static Term createBeforeLoopUpdate(boolean isTransaction, boolean isPerm tb.var(heapLDT.getPermissionHeap()))); } + if (!localVarsBefore.isEmpty()) { + ImmutableList updates = ImmutableSLList.nil(); + for (var entry : localVarsBefore) { + // {i_before := i} + updates = updates.append(tb.elementary(tb.var(entry.value()), tb.var(entry.key()))); + } + var parUp = tb.parallel(updates); + beforeLoopUpdate = tb.parallel(beforeLoopUpdate, parUp); + } + return beforeLoopUpdate; } 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..0a98ce7ede5 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,16 +11,16 @@ 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; import de.uka.ilkd.key.util.MiscTools; import org.key_project.logic.Name; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableMap; +import org.key_project.util.collection.ImmutableSLList; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; @@ -36,7 +36,7 @@ public final class CreateFrameCond extends AbstractTermTransformer { public CreateFrameCond() { - super(new Name("#createFrameCond"), 4); + super(new Name("#createFrameCond"), 5); } @Override @@ -46,8 +46,10 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { (ProgramVariable) term.sub(1).op(); final ProgramVariable savedHeapBeforePV = // (ProgramVariable) term.sub(2).op(); + final var localVarsBeforeSV = // + (ProgramSV) term.sub(3).op(); final ProgramVariable permissionsHeapBeforePV = // - (ProgramVariable) term.sub(3).op(); + (ProgramVariable) term.sub(4).op(); final LoopSpecification loopSpec = // MiscTools.getSpecForTermWithLoopStmt(loopFormula, services); @@ -62,6 +64,22 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { final Term frameCondition = createFrameCondition(loopSpec, isTransaction, heapToBeforeLoopMap, services); + // Add update for overwritten local vars that might appear in the assignable clause. See + // Issue #3524. + @SuppressWarnings("unchecked") + final var localVarsMap = (ImmutableMap) svInst + .getInstantiation(localVarsBeforeSV); + if (localVarsMap != null && !localVarsMap.isEmpty()) { + var tb = services.getTermBuilder(); + ImmutableList updates = ImmutableSLList.nil(); + for (var entry : localVarsMap) { + updates = updates.append(tb.elementary(tb.var(entry.key()), tb.var(entry.value()))); + } + var parUp = tb.parallel(updates); + + return tb.apply(parUp, frameCondition); + } + return frameCondition; } @@ -102,7 +120,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/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java new file mode 100644 index 00000000000..7f2f4785438 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java @@ -0,0 +1,54 @@ +/* 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.metaconstruct; + +import java.util.ArrayList; + +import de.uka.ilkd.key.java.Expression; +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.Services; +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.VariableSpecification; +import de.uka.ilkd.key.java.reference.TypeRef; +import de.uka.ilkd.key.logic.op.LocationVariable; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.rule.inst.SVInstantiations; + +import org.key_project.util.collection.ImmutableMap; + +/** + * A transformer that takes a ProgramSV, which must be instantiated with a map from variable to + * variable. + * The key is the original variable; the entry its "before" version. + * A variable is only a key in the map if it's written to in the loop body. + */ +public class DeclareLocalLoopVars extends ProgramTransformer { + public static final String NAME = "declare-local-loop-vars"; + + public DeclareLocalLoopVars(Expression expr) { + super(NAME, expr); + } + + @Override + public ProgramElement[] transform(ProgramElement pe, Services services, + SVInstantiations svInst) { + var vars = (ImmutableMap) svInst + .getInstantiation((ProgramSV) body()); + var decls = new ArrayList(vars.size()); + for (var elem : vars) { + var locVar = elem.value(); + assert locVar != null; + var spec = new VariableSpecification(locVar); + int dim = 0; + KeYJavaType type = locVar.getKeYJavaType(); + if (type.getJavaType() instanceof ArrayType at) { + dim = at.getDimension(); + } + decls.add(new LocalVariableDeclaration(new TypeRef(type, dim), spec)); + } + return decls.toArray(new ProgramElement[0]); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java index a52fd22bfb0..b6de6afe933 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java @@ -324,6 +324,10 @@ public void setOrigin(String origin) { this.origin = origin; } + public void addNewLocalVars(SchemaVariable sv0, SchemaVariable sv1) { + + } + public static class TacletBuilderException extends IllegalArgumentException { 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..c2529d136f2 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,6 +4365,19 @@ RKeYMetaConstruct KeYMetaConstructStatement() : return result; } ) + | + ( + "#declare-local-loop-vars" "(" + activeAccess = PrimaryExpression() + ")" ";" + { + result = factory.createRKeYMetaConstruct(); + setPrefixInfo(result); + result.setChild((Statement)activeAccess); + result.setName("#declare-local-loop-vars"); + 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..357dd949c6f 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,7 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Variable #localVarsBefore_LOOP; \find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post))) @@ -46,6 +47,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarsBefore_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 +73,14 @@ #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; + #declare-local-loop-vars(#localVarsBefore_LOOP); }\endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #localVarsBefore_LOOP, + #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} @@ -93,7 +101,12 @@ (#x<> = TRUE -> post) & (#x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + & #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #localVarsBefore_LOOP, + #permissionsBefore_LOOP) & prec(variantTerm, #variant)) ))) ) @@ -117,6 +130,7 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Variable #localVarsBefore_LOOP; \find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post))) @@ -124,6 +138,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post))) \varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post))) @@ -140,9 +155,10 @@ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; + #declare-local-loop-vars(#localVarsBefore_LOOP); } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP,#localVarsBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} (inv & freeInv -> @@ -162,7 +178,12 @@ (#x<> = TRUE -> post) & (#x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP)) + & #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #localVarsBefore_LOOP, + #permissionsBefore_LOOP)) ))) ) ) @@ -221,6 +242,7 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Variable #localVarsBefore_LOOP; \find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post))) @@ -229,6 +251,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#dia}{ while (#nse) #body }\endmodality (post))) \varcond(\storeStmtIn(#loopStmt, \modality{#dia}{ while (#nse) #body }\endmodality (post))) @@ -247,9 +270,10 @@ #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; + #declare-local-loop-vars(#localVarsBefore_LOOP); } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} @@ -269,7 +293,12 @@ }\endmodality ( #x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + & #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #localVarsBefore_LOOP, + #permissionsBefore_LOOP) & prec(variantTerm, #variant) ))) ) @@ -286,7 +315,7 @@ #typeof(#variant) #variant; } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} @@ -327,6 +356,7 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; + \schemaVar \program [list] Variable #localVarsBefore_LOOP; \find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post))) @@ -334,6 +364,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) + \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) \varcond(\storeTermIn(loopFormula, \modality{#box}{ while (#nse) #body }\endmodality (post))) \varcond(\storeStmtIn(#loopStmt, \modality{#box}{ while (#nse) #body }\endmodality (post))) @@ -349,9 +380,10 @@ \modality{#box}{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; + #declare-local-loop-vars(#localVarsBefore_LOOP); } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} (inv & freeInv -> @@ -370,7 +402,12 @@ }\endmodality ( #x<> = FALSE -> inv - & #createFrameCond(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + & #createFrameCond( + loopFormula, + #heapBefore_LOOP, + #savedHeapBefore_LOOP, + #localVarsBefore_LOOP, + #permissionsBefore_LOOP) ))) ) ) @@ -379,7 +416,7 @@ "Use Case": \replacewith( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} (inv & freeInv -> From 8fc8c2974df61bdc96cf65ec22859a52d1687866 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 31 Oct 2024 13:34:09 +0100 Subject: [PATCH 2/9] Update taclet equality tests --- .../de/uka/ilkd/key/nparser/taclets.old.txt | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) 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..145a7497b4c 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: Thu Oct 31 13:30:17 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(#localVarsBefore_LOOP (program Variable), #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))|{{ .. + declare-local-loop-vars(#localVarsBefore_LOOP) +}}| (update-application(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_LOOP,#permissionsBefore_LOOP),#createLocalAnonUpdate(loopFormula)),#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,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_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(#localVarsBefore_LOOP (program Variable), #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))|{{ .. + declare-local-loop-vars(#localVarsBefore_LOOP) +}}| (update-application(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_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))|{{ .. 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,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_LOOP,#permissionsBefore_LOOP)),prec(variantTerm,#variant)))))))))) ; \replacewith(inv) \heuristics(loop_scope_inv_taclet) Choices: (programRules:Java & javaLoopTreatment:efficient)} From 4d0835b9ddb4ff1b2dabaa4df293700fddc8db14 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 31 Oct 2024 15:20:07 +0100 Subject: [PATCH 3/9] Fix slicing test (changed loop rules add two more rules, resulting in more slices) --- .../firstTouch/05-ReverseArray/reverseArray.proof | 2 ++ .../java/org/key_project/slicing/EndToEndTests.java | 10 +++++----- 2 files changed, 7 insertions(+), 5 deletions(-) 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/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(); From 34f582728d905bcb673c464705acd3a610f67968 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 31 Oct 2024 15:55:40 +0100 Subject: [PATCH 4/9] Fix saved proof (adapted saved proof for fixed loop invariant rule) --- key.ui/examples/heap/permutedSum/perm.proof | 1 + 1 file changed, 1 insertion(+) 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")) From 68eb108d4e41bbfb604ca9a456c2ed8762620f1e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 31 Oct 2024 16:14:47 +0100 Subject: [PATCH 5/9] update qodana linter --- qodana.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 87f4b5f11f6117db0fe7502696da302c2f5e1e2b Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 31 Oct 2024 16:49:02 +0100 Subject: [PATCH 6/9] clean up taclet builder --- .../de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java index b6de6afe933..13bbce2e3e9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java @@ -323,11 +323,7 @@ public T getTacletWithoutInactiveGoalTemplates(Set active) { public void setOrigin(String origin) { this.origin = origin; } - - public void addNewLocalVars(SchemaVariable sv0, SchemaVariable sv1) { - - } - + public static class TacletBuilderException extends IllegalArgumentException { From 20141166611fd94500b646bc0fa061a7534efc84 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 31 Oct 2024 16:49:32 +0100 Subject: [PATCH 7/9] clean up taclet builder --- .../java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java index 13bbce2e3e9..a52fd22bfb0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletBuilder.java @@ -323,7 +323,7 @@ public T getTacletWithoutInactiveGoalTemplates(Set active) { public void setOrigin(String origin) { this.origin = origin; } - + public static class TacletBuilderException extends IllegalArgumentException { From e3fdf2f8df3b9ba3560457a59b4aba7f90de0a5d Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 4 Nov 2024 08:35:43 +0100 Subject: [PATCH 8/9] Separate SVs for decls and updates --- .../key/java/SchemaRecoder2KeYConverter.java | 2 - .../java/visitor/ProgramReplaceVisitor.java | 14 ---- .../varexp/TacletBuilderManipulators.java | 2 +- .../conditions/NewLocalVarsCondition.java | 81 ++++++++++++++----- .../metaconstruct/CreateBeforeLoopUpdate.java | 29 +------ .../rule/metaconstruct/CreateFrameCond.java | 25 +----- .../metaconstruct/DeclareLocalLoopVars.java | 54 ------------- .../ilkd/key/proof/rules/loopScopeRules.key | 59 ++++++++------ 8 files changed, 102 insertions(+), 164 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java index ed2cc8ff3d2..1b0a1f4c1bc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java @@ -134,8 +134,6 @@ public ProgramTransformer convert(de.uka.ilkd.key.java.recoderext.RKeYMetaConstr return new InitArrayCreation(mc.getFirstSV().getSV(), list.get(Expression.class)); } else if ("#reattachLoopInvariant".equals(mcName)) { return new ReattachLoopInvariant(list.get(LoopStatement.class)); - } else if ("#declare-local-loop-vars".equals(mcName)) { - return new DeclareLocalLoopVars(list.get(Expression.class)); } else { throw new ConvertException("Program meta construct " + mc + " unknown."); } 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 47ac486039f..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,15 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.visitor; -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.SourceElement; import de.uka.ilkd.key.logic.ProgramInLogic; 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.AbstractProgramElement; import de.uka.ilkd.key.rule.inst.SVInstantiations; @@ -19,9 +16,7 @@ import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; -import org.key_project.util.collection.ImmutableMap; -import org.jspecify.annotations.NonNull; /** * Walks through a java AST in depth-left-fist-order. This walker is used to transform a program @@ -89,15 +84,6 @@ public void performActionOnSchemaVariable(SchemaVariable sv) { addChildren(instArray); } else if (inst instanceof Term && ((Term) inst).op() instanceof ProgramInLogic) { addChild(services.getTypeConverter().convertToProgramElement((Term) inst)); - } else if (inst instanceof ImmutableMap) { - @SuppressWarnings("unchecked") - final ImmutableMap<@NonNull LocationVariable, LocationVariable> map = - (ImmutableMap<@NonNull LocationVariable, LocationVariable>) inst; - List lst = new ArrayList<>(); - for (var e : map) { - lst.add(e.value()); - } - addChildren(new ImmutableArray<>(lst)); } else { throw new IllegalStateException( "programreplacevisitor: Instantiation missing " + "for schema variable " + sv); 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 b0d4e67b92a..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 @@ -162,7 +162,7 @@ public void apply(TacletBuilder tacletBuilder, Object[] arguments, }; public static final TacletBuilderCommand NEW_LOCAL_VARS = new ConstructorBasedBuilder( - "newLocalVars", NewLocalVarsCondition.class, SV, SV); + "newLocalVars", NewLocalVarsCondition.class, SV, SV, SV, SV); static class NotFreeInTacletBuilderCommand extends AbstractTacletBuilderCommand { public NotFreeInTacletBuilderCommand(@NonNull ArgumentType... argumentsTypes) { 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 index 32a6a3c5812..8b6946277fb 100644 --- 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 @@ -3,42 +3,74 @@ * 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.LocationVarMap; +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.DefaultImmutableMap; -import org.key_project.util.collection.ImmutableMap; - -import org.jspecify.annotations.NonNull; +import org.key_project.util.collection.*; /** - * Collects all local variables written to in {@code bodySV} and instantiates {@code varsSV} with a - * map - * from these variables to their (newly created, unique) "before" version. + * 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 { - private final SchemaVariable varsSV; + /** + * 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 vars, SchemaVariable body) { - this.varsSV = vars; - this.bodySV = body; + 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(varsSV) != null) { + if (svInst.getInstantiation(varDeclsSV) != null) { return matchCond; } var body = (Statement) svInst.getInstantiation(bodySV); @@ -47,20 +79,33 @@ public MatchConditions check(SchemaVariable var, SyntaxElement instCandidate, } var vars = MiscTools.getLocalOuts(body, services); - ImmutableMap<@NonNull LocationVariable, LocationVariable> map = - DefaultImmutableMap.nilMap(); + 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); - map = map.put(v, locVar); + 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(varsSV, new LocationVarMap(map), services)); + 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(" + varsSV + ", " + bodySV + ")"; + 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 028d168d371..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 @@ -12,11 +12,7 @@ import de.uka.ilkd.key.util.MiscTools; import org.key_project.logic.Name; -import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableMap; -import org.key_project.util.collection.ImmutableSLList; -import org.jspecify.annotations.NonNull; /** * Initializes the "before loop" update needed for the modifiable clause. @@ -37,7 +33,7 @@ public final class CreateBeforeLoopUpdate extends AbstractTermTransformer { public CreateBeforeLoopUpdate() { - super(new Name("#createBeforeLoopUpdate"), 5); + super(new Name("#createBeforeLoopUpdate"), 4); } @Override @@ -46,18 +42,10 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { final Term anonHeapTerm = term.sub(1); final Term anonSavedHeapTerm = term.sub(2); - final Term localVarsBeforeSV = term.sub(3); - final Term anonPermissionsHeapTerm = term.sub(4); - - // We have a SV for the local vars written to in the loop. Get its inst, which is a map from - // the original variable to its "before" version. - @SuppressWarnings("unchecked") - final var localVarsBefore = - (ImmutableMap<@NonNull LocationVariable, LocationVariable>) svInst - .getInstantiation((SchemaVariable) localVarsBeforeSV.op()); + final Term anonPermissionsHeapTerm = term.sub(3); return createBeforeLoopUpdate(MiscTools.isTransaction(((Modality) loopTerm.op()).kind()), - MiscTools.isPermissions(services), anonHeapTerm, anonSavedHeapTerm, localVarsBefore, + MiscTools.isPermissions(services), anonHeapTerm, anonSavedHeapTerm, anonPermissionsHeapTerm, services); } @@ -76,7 +64,6 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { */ private static Term createBeforeLoopUpdate(boolean isTransaction, boolean isPermissions, Term anonHeapTerm, Term anonSavedHeapTerm, - ImmutableMap<@NonNull LocationVariable, LocationVariable> localVarsBefore, Term anonPermissionsHeapTerm, Services services) { final TermBuilder tb = services.getTermBuilder(); @@ -96,16 +83,6 @@ private static Term createBeforeLoopUpdate(boolean isTransaction, boolean isPerm tb.var(heapLDT.getPermissionHeap()))); } - if (!localVarsBefore.isEmpty()) { - ImmutableList updates = ImmutableSLList.nil(); - for (var entry : localVarsBefore) { - // {i_before := i} - updates = updates.append(tb.elementary(tb.var(entry.value()), tb.var(entry.key()))); - } - var parUp = tb.parallel(updates); - beforeLoopUpdate = tb.parallel(beforeLoopUpdate, parUp); - } - return beforeLoopUpdate; } 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 0a98ce7ede5..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 @@ -18,9 +18,6 @@ import de.uka.ilkd.key.util.MiscTools; import org.key_project.logic.Name; -import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableMap; -import org.key_project.util.collection.ImmutableSLList; import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; @@ -36,7 +33,7 @@ public final class CreateFrameCond extends AbstractTermTransformer { public CreateFrameCond() { - super(new Name("#createFrameCond"), 5); + super(new Name("#createFrameCond"), 4); } @Override @@ -46,10 +43,8 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { (ProgramVariable) term.sub(1).op(); final ProgramVariable savedHeapBeforePV = // (ProgramVariable) term.sub(2).op(); - final var localVarsBeforeSV = // - (ProgramSV) term.sub(3).op(); final ProgramVariable permissionsHeapBeforePV = // - (ProgramVariable) term.sub(4).op(); + (ProgramVariable) term.sub(3).op(); final LoopSpecification loopSpec = // MiscTools.getSpecForTermWithLoopStmt(loopFormula, services); @@ -64,22 +59,6 @@ public Term transform(Term term, SVInstantiations svInst, Services services) { final Term frameCondition = createFrameCondition(loopSpec, isTransaction, heapToBeforeLoopMap, services); - // Add update for overwritten local vars that might appear in the assignable clause. See - // Issue #3524. - @SuppressWarnings("unchecked") - final var localVarsMap = (ImmutableMap) svInst - .getInstantiation(localVarsBeforeSV); - if (localVarsMap != null && !localVarsMap.isEmpty()) { - var tb = services.getTermBuilder(); - ImmutableList updates = ImmutableSLList.nil(); - for (var entry : localVarsMap) { - updates = updates.append(tb.elementary(tb.var(entry.key()), tb.var(entry.value()))); - } - var parUp = tb.parallel(updates); - - return tb.apply(parUp, frameCondition); - } - return frameCondition; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java deleted file mode 100644 index 7f2f4785438..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DeclareLocalLoopVars.java +++ /dev/null @@ -1,54 +0,0 @@ -/* 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.metaconstruct; - -import java.util.ArrayList; - -import de.uka.ilkd.key.java.Expression; -import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.java.Services; -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.VariableSpecification; -import de.uka.ilkd.key.java.reference.TypeRef; -import de.uka.ilkd.key.logic.op.LocationVariable; -import de.uka.ilkd.key.logic.op.ProgramSV; -import de.uka.ilkd.key.rule.inst.SVInstantiations; - -import org.key_project.util.collection.ImmutableMap; - -/** - * A transformer that takes a ProgramSV, which must be instantiated with a map from variable to - * variable. - * The key is the original variable; the entry its "before" version. - * A variable is only a key in the map if it's written to in the loop body. - */ -public class DeclareLocalLoopVars extends ProgramTransformer { - public static final String NAME = "declare-local-loop-vars"; - - public DeclareLocalLoopVars(Expression expr) { - super(NAME, expr); - } - - @Override - public ProgramElement[] transform(ProgramElement pe, Services services, - SVInstantiations svInst) { - var vars = (ImmutableMap) svInst - .getInstantiation((ProgramSV) body()); - var decls = new ArrayList(vars.size()); - for (var elem : vars) { - var locVar = elem.value(); - assert locVar != null; - var spec = new VariableSpecification(locVar); - int dim = 0; - KeYJavaType type = locVar.getKeYJavaType(); - if (type.getJavaType() instanceof ArrayType at) { - dim = at.getDimension(); - } - decls.add(new LocalVariableDeclaration(new TypeRef(type, dim), spec)); - } - return decls.toArray(new ProgramElement[0]); - } -} 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 357dd949c6f..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,7 +38,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; - \schemaVar \program [list] Variable #localVarsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post))) @@ -47,7 +49,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) - \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) + \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 @@ -73,14 +75,14 @@ #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; - #declare-local-loop-vars(#localVarsBefore_LOOP); + #localVarDeclsBefore_LOOP }\endmodality ( {#createBeforeLoopUpdate( loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, - #localVarsBefore_LOOP, #permissionsBefore_LOOP) + || #updateBefore_LOOP || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} @@ -101,11 +103,10 @@ (#x<> = TRUE -> post) & (#x<> = FALSE -> inv - & #createFrameCond( + & {#updateFrame_LOOP} #createFrameCond( loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, - #localVarsBefore_LOOP, #permissionsBefore_LOOP) & prec(variantTerm, #variant)) ))) @@ -130,7 +131,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; - \schemaVar \program [list] Variable #localVarsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post))) @@ -138,7 +141,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) - \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) + \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))) @@ -155,11 +158,12 @@ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; - #declare-local-loop-vars(#localVarsBefore_LOOP); + #localVarDeclsBefore_LOOP } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP,#localVarsBefore_LOOP, #permissionsBefore_LOOP) + {#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}{ @@ -178,11 +182,10 @@ (#x<> = TRUE -> post) & (#x<> = FALSE -> inv - & #createFrameCond( + & {#updateFrame_LOOP} #createFrameCond( loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, - #localVarsBefore_LOOP, #permissionsBefore_LOOP)) ))) ) @@ -242,7 +245,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; - \schemaVar \program [list] Variable #localVarsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#dia} {.. while (#nse) #body ... }\endmodality (post))) @@ -251,7 +256,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) - \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) + \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))) @@ -270,11 +275,12 @@ #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; - #declare-local-loop-vars(#localVarsBefore_LOOP); + #localVarDeclsBefore_LOOP } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) + {#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 -> @@ -293,11 +299,10 @@ }\endmodality ( #x<> = FALSE -> inv - & #createFrameCond( + & {#updateFrame_LOOP} #createFrameCond( loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, - #localVarsBefore_LOOP, #permissionsBefore_LOOP) & prec(variantTerm, #variant) ))) @@ -315,7 +320,7 @@ #typeof(#variant) #variant; } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} {#variant := variantTerm} @@ -356,7 +361,9 @@ \schemaVar \program Variable #heapBefore_LOOP; \schemaVar \program Variable #savedHeapBefore_LOOP; \schemaVar \program Variable #permissionsBefore_LOOP; - \schemaVar \program [list] Variable #localVarsBefore_LOOP; + \schemaVar \program [list] Statement #localVarDeclsBefore_LOOP; + \schemaVar \update #updateBefore_LOOP; + \schemaVar \update #updateFrame_LOOP; \find((\modality{#box} {.. while (#nse) #body ... }\endmodality (post))) @@ -364,7 +371,7 @@ \varcond(\new(#heapBefore_LOOP, Heap)) \varcond(\new(#savedHeapBefore_LOOP, Heap)) \varcond(\new(#permissionsBefore_LOOP, Heap)) - \varcond(\newLocalVars(#localVarsBefore_LOOP, #body)) + \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))) @@ -380,11 +387,12 @@ \modality{#box}{ #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; - #declare-local-loop-vars(#localVarsBefore_LOOP); + #localVarDeclsBefore_LOOP } \endmodality ( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) + {#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}{ @@ -402,11 +410,10 @@ }\endmodality ( #x<> = FALSE -> inv - & #createFrameCond( + & {#updateFrame_LOOP} #createFrameCond( loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, - #localVarsBefore_LOOP, #permissionsBefore_LOOP) ))) ) @@ -416,7 +423,7 @@ "Use Case": \replacewith( - {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #localVarsBefore_LOOP, #permissionsBefore_LOOP) + {#createBeforeLoopUpdate(loopFormula, #heapBefore_LOOP, #savedHeapBefore_LOOP, #permissionsBefore_LOOP) || #createLocalAnonUpdate(loopFormula) || #createHeapAnonUpdate(loopFormula, anon_heap_LOOP, anon_savedHeap_LOOP, anon_permissions_LOOP)} (inv & freeInv -> From 7a1426177d1ab56dedb8229a312536a512d06e1e Mon Sep 17 00:00:00 2001 From: Drodt Date: Mon, 4 Nov 2024 13:28:03 +0100 Subject: [PATCH 9/9] Update TacletEq tests --- .../ilkd/key/rule/inst/LocationVarMap.java | 22 ------------------- .../key/parser/schemajava/SchemaJavaParser.jj | 13 ----------- .../de/uka/ilkd/key/nparser/taclets.old.txt | 18 +++++++-------- 3 files changed, 9 insertions(+), 44 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java deleted file mode 100644 index b0f42ec1b8c..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/LocationVarMap.java +++ /dev/null @@ -1,22 +0,0 @@ -/* 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.inst; - -import de.uka.ilkd.key.logic.op.LocationVariable; - -import org.key_project.util.collection.ImmutableMap; - -import org.jspecify.annotations.NonNull; - -public class LocationVarMap - extends InstantiationEntry> { - /** - * creates a new instantiation entry for the instantiation to be stored - * - * @param instantiation the instantiation to be stored - */ - public LocationVarMap(ImmutableMap<@NonNull LocationVariable, LocationVariable> instantiation) { - super(instantiation); - } -} 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 c2529d136f2..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 @@ -4366,19 +4366,6 @@ RKeYMetaConstruct KeYMetaConstructStatement() : } ) | - ( - "#declare-local-loop-vars" "(" - activeAccess = PrimaryExpression() - ")" ";" - { - result = factory.createRKeYMetaConstruct(); - setPrefixInfo(result); - result.setChild((Statement)activeAccess); - result.setName("#declare-local-loop-vars"); - return result; - } - ) - | ( "#resolve-multiple-var-decl" "(" stat = Statement() ")" ";" { 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 145a7497b4c..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: Thu Oct 31 13:30:17 CET 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)), \newLocalVars(#localVarsBefore_LOOP (program Variable), #body (program Statement)), \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,8 +12580,8 @@ loopScopeInvBox { #typeof(#heapBefore_LOOP) #heapBefore_LOOP; #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; - declare-local-loop-vars(#localVarsBefore_LOOP) -}}| (update-application(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_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) { @@ -12591,7 +12591,7 @@ loopScopeInvBox { break; } } -... }}| (and(imp(equals(#x<>,TRUE),post),imp(equals(#x<>,FALSE),and(inv,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_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)} @@ -12601,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)), \newLocalVars(#localVarsBefore_LOOP (program Variable), #body (program Statement)), \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 @@ -12611,8 +12611,8 @@ loopScopeInvDia { #typeof(#savedHeapBefore_LOOP) #savedHeapBefore_LOOP; #typeof(#permissionsBefore_LOOP) #permissionsBefore_LOOP; #typeof(#variant) #variant; - declare-local-loop-vars(#localVarsBefore_LOOP) -}}| (update-application(parallel-upd(parallel-upd(#createBeforeLoopUpdate(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_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) { @@ -12622,7 +12622,7 @@ loopScopeInvDia { break; } } -... }}| (and(imp(equals(#x<>,TRUE),post),imp(equals(#x<>,FALSE),and(and(inv,#createFrameCond(loopFormula,#heapBefore_LOOP,#savedHeapBefore_LOOP,#localVarsBefore_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)}