From b0b7b5fd0383bc4b461a74418bd924dcfc0a538e Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 7 Mar 2024 13:29:07 +0100 Subject: [PATCH 1/2] Fix newnames handling for new local vars Fixes #3437 --- .../uka/ilkd/key/java/KeYJavaASTFactory.java | 11 +++ .../de/uka/ilkd/key/logic/VariableNamer.java | 11 ++- .../de/uka/ilkd/key/proof/NameRecorder.java | 25 ++++- .../rule/metaconstruct/InitArrayCreation.java | 20 +++- .../key_project/slicing/Issue3437Test.java | 59 ++++++++++++ ...normal_behavior operation contract.0.proof | 94 +++++++++++++++++++ .../testcase/issues/3437/Newnames.java | 8 ++ 7 files changed, 221 insertions(+), 7 deletions(-) create mode 100644 keyext.slicing/src/test/java/org/key_project/slicing/Issue3437Test.java create mode 100644 keyext.slicing/src/test/resources/testcase/issues/3437/Newnames(Newnames__createArray()).JML normal_behavior operation contract.0.proof create mode 100644 keyext.slicing/src/test/resources/testcase/issues/3437/Newnames.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java index 2473def2307..766523cab3b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java @@ -67,7 +67,9 @@ import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.ProgramVariable; +import de.uka.ilkd.key.proof.NameRecorder; +import org.key_project.logic.Name; import org.key_project.util.ExtList; import org.key_project.util.collection.ImmutableArray; @@ -302,8 +304,17 @@ public static ProgramVariable localVariable(ProgramElementName name, KeYJavaType */ public static ProgramVariable localVariable(final Services services, final String name, final KeYJavaType type) { + // first check for a saved name for this variable + final NameRecorder nameRecorder = services.getNameRecorder(); + for (var prop : nameRecorder.getSetProposals()) { + if (prop.toString().startsWith(name + VariableNamer.TEMPORARY_VAR_SEPARATOR)) { + return KeYJavaASTFactory.localVariable(new ProgramElementName(prop.toString()), + type); + } + } final ProgramElementName uniqueName = services.getVariableNamer().getTemporaryNameProposal(name); + nameRecorder.addProposal(new Name(uniqueName.getProgramName())); final ProgramVariable variable = KeYJavaASTFactory.localVariable(uniqueName, type); return variable; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java index 101bad74ced..2a7c20fdfa8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java @@ -48,6 +48,8 @@ public abstract class VariableNamer implements InstantiationProposer { private static final Logger LOGGER = LoggerFactory.getLogger(VariableNamer.class); + public static final char TEMPORARY_VAR_SEPARATOR = '#'; + // ------------------------------------------------------------------------- // member variables // ------------------------------------------------------------------------- @@ -507,7 +509,7 @@ public static ProgramElementName parseName(String name, NameCreationInfo creatio Comment[] comments) { ProgramElementName result; - int sepPos = name.lastIndexOf(TempIndProgramElementName.SEPARATOR); + int sepPos = name.lastIndexOf(TEMPORARY_VAR_SEPARATOR); if (sepPos > 0) { String basename = name.substring(0, sepPos); int index = Integer.parseInt(name.substring(sepPos + 1)); @@ -663,15 +665,14 @@ public int getIndex() { * temporary indexed ProgramElementName */ private static class TempIndProgramElementName extends IndProgramElementName { - static final char SEPARATOR = '#'; - TempIndProgramElementName(String basename, int index, NameCreationInfo creationInfo) { - super(basename + SEPARATOR + index, basename, index, creationInfo); + super(basename + TEMPORARY_VAR_SEPARATOR + index, basename, index, creationInfo); } TempIndProgramElementName(String basename, int index, NameCreationInfo creationInfo, Comment[] comments) { - super(basename + SEPARATOR + index, basename, index, creationInfo, comments); + super(basename + TEMPORARY_VAR_SEPARATOR + index, basename, index, creationInfo, + comments); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/NameRecorder.java b/key.core/src/main/java/de/uka/ilkd/key/proof/NameRecorder.java index 66ad5d6005b..03d4f5c0d1e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/NameRecorder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/NameRecorder.java @@ -14,17 +14,40 @@ public class NameRecorder { private ImmutableList post = ImmutableSLList.nil(); public void setProposals(ImmutableList proposals) { - pre = proposals; + if (proposals == null) { + pre = ImmutableSLList.nil(); + } else { + pre = proposals; + } } + /** + * Get the name proposals added using {@link #addProposal(Name)}. + * + * @return the name proposals + */ public ImmutableList getProposals() { return post; } + /** + * Get the name proposals previously set using {@link #setProposals(ImmutableList)}. + * + * @return the name proposals + */ + public ImmutableList getSetProposals() { + return pre; + } + public void addProposal(Name proposal) { post = post.append(proposal); } + /** + * Get a proposal and remove it from this recorder. + * + * @return the first proposal + */ public Name getProposal() { Name proposal = null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java index 133d296616d..f44add8db96 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java @@ -28,8 +28,10 @@ import de.uka.ilkd.key.logic.VariableNamer; import de.uka.ilkd.key.logic.op.ProgramVariable; import de.uka.ilkd.key.logic.op.SchemaVariable; +import de.uka.ilkd.key.proof.NameRecorder; import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; /** @@ -85,11 +87,27 @@ private ProgramVariable[] evaluateAndCheckDimensionExpressions(LinkedList x.serialNr() == 13)); + env.getProofControl().startAutoMode(proof, proof.openEnabledGoals()); + env.getProofControl().waitWhileAutoMode(); + assertTrue(proof.closed()); + + var results = tracker.analyze(true, false); + + ProblemLoaderControl control = new DefaultUserInterfaceControl(); + SlicingProofReplayer replayer = SlicingProofReplayer + .constructSlicer(control, proof, results, env.getUi()); + var newFile = replayer.slice(); + var env2 = KeYEnvironment.load(newFile); + var proof2 = env.getLoadedProof(); + assertTrue(proof2.closed()); + + env.dispose(); + env2.dispose(); + GeneralSettings.noPruningClosed = true; + } +} diff --git a/keyext.slicing/src/test/resources/testcase/issues/3437/Newnames(Newnames__createArray()).JML normal_behavior operation contract.0.proof b/keyext.slicing/src/test/resources/testcase/issues/3437/Newnames(Newnames__createArray()).JML normal_behavior operation contract.0.proof new file mode 100644 index 00000000000..e0644d94eca --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/issues/3437/Newnames(Newnames__createArray()).JML normal_behavior operation contract.0.proof @@ -0,0 +1,94 @@ +\profile "Java Profile"; + +\settings // Proof-Settings-Config-File +{ + "Choice" : { + "JavaCard" : "JavaCard:off", + "Strings" : "Strings:on", + "assertions" : "assertions:safe", + "bigint" : "bigint:on", + "floatRules" : "floatRules:strictfpOnly", + "initialisation" : "initialisation:disableStaticInitialisation", + "intRules" : "intRules:arithmeticSemanticsIgnoringOF", + "integerSimplificationRules" : "integerSimplificationRules:full", + "javaLoopTreatment" : "javaLoopTreatment:efficient", + "mergeGenerateIsWeakeningGoal" : "mergeGenerateIsWeakeningGoal:off", + "methodExpansion" : "methodExpansion:modularOnly", + "modelFields" : "modelFields:treatAsAxiom", + "moreSeqRules" : "moreSeqRules:off", + "permissions" : "permissions:off", + "programRules" : "programRules:Java", + "reach" : "reach:on", + "runtimeExceptions" : "runtimeExceptions:ban", + "sequences" : "sequences:on", + "wdChecks" : "wdChecks:off", + "wdOperator" : "wdOperator:L" + }, + "Labels" : { + "UseOriginLabels" : true + }, + "NewSMT" : { + + }, + "SMTSettings" : { + "SelectedTaclets" : [ + + ], + "UseBuiltUniqueness" : false, + "explicitTypeHierarchy" : false, + "instantiateHierarchyAssumptions" : true, + "integersMaximum" : 2147483645, + "integersMinimum" : -2147483645, + "invariantForall" : false, + "maxGenericSorts" : 2, + "useConstantsForBigOrSmallIntegers" : true, + "useUninterpretedMultiplication" : true + }, + "Strategy" : { + "ActiveStrategy" : "JavaCardDLStrategy", + "MaximumNumberOfAutomaticApplications" : 7000, + "Timeout" : -1, + "options" : { + "AUTO_INDUCTION_OPTIONS_KEY" : "AUTO_INDUCTION_OFF", + "BLOCK_OPTIONS_KEY" : "BLOCK_CONTRACT_INTERNAL", + "CLASS_AXIOM_OPTIONS_KEY" : "CLASS_AXIOM_DELAYED", + "DEP_OPTIONS_KEY" : "DEP_ON", + "INF_FLOW_CHECK_PROPERTY" : "INF_FLOW_CHECK_FALSE", + "LOOP_OPTIONS_KEY" : "LOOP_SCOPE_INV_TACLET", + "METHOD_OPTIONS_KEY" : "METHOD_CONTRACT", + "MPS_OPTIONS_KEY" : "MPS_MERGE", + "NON_LIN_ARITH_OPTIONS_KEY" : "NON_LIN_ARITH_DEF_OPS", + "OSS_OPTIONS_KEY" : "OSS_ON", + "QUANTIFIERS_OPTIONS_KEY" : "QUANTIFIERS_NON_SPLITTING_WITH_PROGS", + "QUERYAXIOM_OPTIONS_KEY" : "QUERYAXIOM_ON", + "QUERY_NEW_OPTIONS_KEY" : "QUERY_ON", + "SPLITTING_OPTIONS_KEY" : "SPLITTING_DELAYED", + "STOPMODE_OPTIONS_KEY" : "STOPMODE_DEFAULT", + "SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER", + "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY" : "SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF", + "USER_TACLETS_OPTIONS_KEY1" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY2" : "USER_TACLETS_OFF", + "USER_TACLETS_OPTIONS_KEY3" : "USER_TACLETS_OFF", + "VBT_PHASE" : "VBT_SYM_EX" + } + } + } + +\javaSource "."; + +\proofObligation "#Proof Obligation Settings +#Thu Mar 07 13:11:27 CET 2024 +class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO +contract=Newnames[Newnames\\:\\:createArray()].JML normal_behavior operation contract.0 +name=Newnames[Newnames\\:\\:createArray()].JML normal_behavior operation contract.0 +"; + +\proof { +(keyLog "0" (keyUser "arne" ) (keyVersion "9ad6cc893ef6e61574fac6994511791b8411ccfc")) + +(autoModeTime "0") + +(branch "dummy ID" + (opengoal "==> ( ( ((((wellFormed(heap)<> & (!( self<> = null)<>)<>)<> & ( boolean::select(heap, self, java.lang.Object::) = TRUE)<>)<> & (Newnames::exactInstance(self) = TRUE)<>)<> & measuredByEmpty<>)<> & java.lang.Object::(heap, self)<>)<> -> ({heapAtPre:=heap} (\\<{ exc = null; try { self.createArray()@Newnames; } catch (java.lang.Throwable e) { exc = e; } }\\> (( (java.lang.Object::(heap, self)<> & ( exc<> = null)<>)<> & (\\forall Field f; (\\forall java.lang.Object o; (( (elementOf(o, f, allLocs)<> | ((!(o = null)<>)<> & (!( boolean::select(heapAtPre, o, java.lang.Object::) = TRUE)<>)<>)<>)<> | ( any::select(heap, o, f) = any::select(heapAtPre, o, f))<>)<>))<>)<>)< (implicit)\",\"[ensures (implicit), assignable (implicit)]\")>>))< (implicit)\",\"[ensures (implicit), assignable (implicit)]\")>>)< (implicit)\",\"[ensures (implicit), assignable (implicit)]\")>>)< (implicit)\",\"[requires (implicit), ensures (implicit), assignable (implicit)]\")>>") +) +} diff --git a/keyext.slicing/src/test/resources/testcase/issues/3437/Newnames.java b/keyext.slicing/src/test/resources/testcase/issues/3437/Newnames.java new file mode 100644 index 00000000000..e85a8c2b2e8 --- /dev/null +++ b/keyext.slicing/src/test/resources/testcase/issues/3437/Newnames.java @@ -0,0 +1,8 @@ +class Newnames { + /*@ normal_behaviour + @ ensures true; + @*/ + void createArray() { + int[] a = new int[5 + 1]; + } +} From 2f229d0c2214183b0a207227a74267534ead515b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 21 Mar 2024 15:33:22 +0100 Subject: [PATCH 2/2] Rename constant to TEMP_INDEX_SEPARATOR --- .../de/uka/ilkd/key/java/KeYJavaASTFactory.java | 2 +- .../java/de/uka/ilkd/key/logic/VariableNamer.java | 15 ++++++++++----- .../key/rule/metaconstruct/InitArrayCreation.java | 2 +- 3 files changed, 12 insertions(+), 7 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java index 766523cab3b..91bff0e5084 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYJavaASTFactory.java @@ -307,7 +307,7 @@ public static ProgramVariable localVariable(final Services services, final Strin // first check for a saved name for this variable final NameRecorder nameRecorder = services.getNameRecorder(); for (var prop : nameRecorder.getSetProposals()) { - if (prop.toString().startsWith(name + VariableNamer.TEMPORARY_VAR_SEPARATOR)) { + if (prop.toString().startsWith(name + VariableNamer.TEMP_INDEX_SEPARATOR)) { return KeYJavaASTFactory.localVariable(new ProgramElementName(prop.toString()), type); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java index 2a7c20fdfa8..256710c7613 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/VariableNamer.java @@ -46,9 +46,14 @@ * Responsible for program variable naming issues. */ public abstract class VariableNamer implements InstantiationProposer { - private static final Logger LOGGER = LoggerFactory.getLogger(VariableNamer.class); + /** + * Separator used for {@link TempIndProgramElementName} instances. + * This will separate the name and the index of the "temporary" + * program element name. + */ + public static final char TEMP_INDEX_SEPARATOR = '#'; - public static final char TEMPORARY_VAR_SEPARATOR = '#'; + private static final Logger LOGGER = LoggerFactory.getLogger(VariableNamer.class); // ------------------------------------------------------------------------- // member variables @@ -509,7 +514,7 @@ public static ProgramElementName parseName(String name, NameCreationInfo creatio Comment[] comments) { ProgramElementName result; - int sepPos = name.lastIndexOf(TEMPORARY_VAR_SEPARATOR); + int sepPos = name.lastIndexOf(TEMP_INDEX_SEPARATOR); if (sepPos > 0) { String basename = name.substring(0, sepPos); int index = Integer.parseInt(name.substring(sepPos + 1)); @@ -666,12 +671,12 @@ public int getIndex() { */ private static class TempIndProgramElementName extends IndProgramElementName { TempIndProgramElementName(String basename, int index, NameCreationInfo creationInfo) { - super(basename + TEMPORARY_VAR_SEPARATOR + index, basename, index, creationInfo); + super(basename + TEMP_INDEX_SEPARATOR + index, basename, index, creationInfo); } TempIndProgramElementName(String basename, int index, NameCreationInfo creationInfo, Comment[] comments) { - super(basename + TEMPORARY_VAR_SEPARATOR + index, basename, index, creationInfo, + super(basename + TEMP_INDEX_SEPARATOR + index, basename, index, creationInfo, comments); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java index f44add8db96..9b76f4cb418 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java @@ -95,7 +95,7 @@ private ProgramVariable[] evaluateAndCheckDimensionExpressions(LinkedList