Fix newnames handling for new local vars

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;

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);
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/NameRecorder.java

@@ -14,17 +14,40 @@ public class NameRecorder {
     private ImmutableList<Name> post = ImmutableSLList.nil();
 
     public void setProposals(ImmutableList<Name> 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<Name> getProposals() {
         return post;
     }
 
+    /**
+     * Get the name proposals previously set using {@link #setProposals(ImmutableList)}.
+     *
+     * @return the name proposals
+     */
+    public ImmutableList<Name> 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;
 

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<Statem
 
         Expression checkDimensions = BooleanLiteral.FALSE;
         ProgramVariable[] pvars = new ProgramVariable[dimExpr.size()];
+        final NameRecorder nameRecorder = services.getNameRecorder();
         final VariableNamer varNamer = services.getVariableNamer();
         final KeYJavaType intType = services.getJavaInfo().getKeYJavaType(PrimitiveType.JAVA_INT);
 
         for (int i = 0; i < pvars.length; i++) {
-            final ProgramElementName name = varNamer.getTemporaryNameProposal("dim" + i);
+            // first check for previously saved name
+            Name proposedName = null;
+            for (var name : nameRecorder.getSetProposals()) {
+                if (name.toString().startsWith("dim" + i + VariableNamer.TEMPORARY_VAR_SEPARATOR)) {
+                    proposedName = name;
+                    break;
+                }
+            }
+            final ProgramElementName name;
+            if (proposedName != null) {
+                name = new ProgramElementName(proposedName.toString());
+            } else {
+                // if there is no previous name, create a new one
+                name = varNamer.getTemporaryNameProposal("dim" + i);
+                nameRecorder.addProposal(new Name(name.getProgramName()));
+            }
 
             final LocalVariableDeclaration argDecl =
                 KeYJavaASTFactory.declare(name, dimExpr.get(i), intType);

keyext.slicing/src/test/java/org/key_project/slicing/Issue3437Test.java

@@ -0,0 +1,59 @@
+/* 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 org.key_project.slicing;
+
+import java.io.File;
+import java.io.IOException;
+
+import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.proof.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.IntermediateProofReplayer;
+import de.uka.ilkd.key.proof.io.ProblemLoaderControl;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.settings.GeneralSettings;
+
+import org.key_project.util.helper.FindResources;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+public class Issue3437Test {
+    public static final File testCaseDirectory = FindResources.getTestCasesDirectory();
+
+    @Test
+    void loadsAndSlicesCorrectly() throws ProblemLoaderException, ProofInputException, IOException,
+            IntermediateProofReplayer.BuiltInConstructionException {
+        GeneralSettings.noPruningClosed = false;
+
+        var file = new File(testCaseDirectory,
+            "issues/3437/Newnames(Newnames__createArray()).JML normal_behavior operation contract.0.proof");
+        var env = KeYEnvironment.load(file);
+        var proof = env.getLoadedProof();
+        var tracker = new DependencyTracker(proof);
+        env.getProofControl().startAutoMode(proof, proof.openEnabledGoals());
+        env.getProofControl().waitWhileAutoMode();
+        assertTrue(proof.closed());
+        // prune and re-run automode to ensure the counters on the temporary variables are different
+        proof.pruneProof(proof.findAny(x -> 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;
+    }
+}

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)<<origin(\"requires (implicit)\",\"[]\")>>       & (!(  self<<origin(\"requires (implicit)\", \"[]\")>>            = null)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>       & (  boolean::select(heap,                            self,                            java.lang.Object::<created>)          = TRUE)<<origin(\"requires (implicit)\", \"[]\")>>)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>       & (Newnames::exactInstance(self) = TRUE)<<origin(\"requires (implicit)\",\"[]\")>>)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>       & measuredByEmpty<<origin(\"requires (implicit)\",\"[]\")>>)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>       & java.lang.Object::<inv>(heap, self)<<impl>>)<<origin(\"requires (implicit)\",\"[requires (implicit)]\")>>   -> ({heapAtPre:=heap}         (\\<{           exc = null;           try {             self.createArray()@Newnames;           } catch (java.lang.Throwable e) {             exc = e;           }         }\\> ((  (java.lang.Object::<inv>(heap, self)<<impl>>               & (  exc<<origin(\"ensures (implicit)\",\"[]\")>>                  = null)<<impl,                           origin(\"ensures (implicit)\",\"[ensures (implicit)]\")>>)<<origin(\"ensures (implicit)\",\"[ensures (implicit)]\")>>               & (\\forall Field f;                    (\\forall java.lang.Object o;                       ((  (elementOf(o, f, allLocs)<<origin(\"assignable (implicit)\",\"[]\")>>                         | ((!(o = null)<<origin(\"assignable (implicit)\",\"[]\")>>)<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>                         & (!(  boolean::select(heapAtPre,                                                o,                                                java.lang.Object::<created>)                              = TRUE)<<origin(\"assignable (implicit)\",\"[]\")>>)<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>)<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>)<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>                         | (  any::select(heap, o, f)                            = any::select(heapAtPre,                                          o,                                          f))<<origin(\"assignable (implicit)\",\"[]\")>>)<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>))<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>)<<origin(\"assignable (implicit)\",\"[assignable (implicit)]\")>>)<<origin(\"<none> (implicit)\",\"[ensures (implicit), assignable (implicit)]\")>>))<<origin(\"<none> (implicit)\",\"[ensures (implicit), assignable (implicit)]\")>>)<<origin(\"<none> (implicit)\",\"[ensures (implicit), assignable (implicit)]\")>>)<<origin(\"<none> (implicit)\",\"[requires (implicit), ensures (implicit), assignable (implicit)]\")>>")
+)
+}

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];
+    }
+}