Fix finalFields default in FinalHeapResolution.isFinalEnabled (#3895)

Author: unp1

key.core/src/main/java/de/uka/ilkd/key/ldt/FinalHeapResolution.java

@@ -48,8 +48,17 @@ public static boolean isFinalEnabled(InitConfig initConfig) {
      * @return true if final fields are treated as immutable
      */
     public static boolean isFinalEnabled(ProofSettings settings) {
+        // When the finalFields choice is absent from the settings (e.g. a freshly
+        // created environment, or settings that predate this option), the taclet base
+        // still activates the *declaration default* of the category. That default is
+        // the first option listed in optionsDeclarations.key, which is "immutable"
+        // (see ChoiceFinder#visitChoice, which uses choices.getFirst()). Falling back
+        // to onHeap here would contradict the rules actually applied during symbolic
+        // execution and produce an inconsistent mix of final(o, f) and
+        // select(heap, o, f) for the very same field. The fallback must therefore
+        // match the declaration default.
         return settings.getChoiceSettings().getDefaultChoices()
-                .getOrDefault(SETTING, "")
+                .getOrDefault(SETTING, IMMUTABLE_OPTION)
                 .equals(IMMUTABLE_OPTION);
     }
 

key.core/src/test/java/de/uka/ilkd/key/ldt/FinalHeapResolutionTest.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 de.uka.ilkd.key.ldt;
+
+import java.util.TreeMap;
+
+import de.uka.ilkd.key.settings.ProofSettings;
+
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertFalse;
+import static org.junit.jupiter.api.Assertions.assertTrue;
+
+/**
+ * Tests for {@link FinalHeapResolution#isFinalEnabled(ProofSettings)}.
+ *
+ * <p>
+ * In particular this pins down that an <em>absent</em> {@code finalFields} choice is resolved to
+ * the declaration default {@code immutable} (the first option in the category, see
+ * {@code optionsDeclarations.key} and {@code ChoiceFinder#visitChoice}). If it were resolved to
+ * {@code onHeap} instead, the setting would disagree with the taclets that symbolic execution
+ * actually applies, and reads of a final field would appear both as {@code final(o, f)} (from the
+ * taclet base) and as {@code select(heap, o, f)} (from JML translation), which blocks otherwise
+ * closable proofs.
+ * </p>
+ */
+class FinalHeapResolutionTest {
+
+    private static final String FINAL_FIELDS = "finalFields";
+
+    private static ProofSettings settingsWith(String finalFieldsValue) {
+        ProofSettings settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
+        var choices = new TreeMap<>(settings.getChoiceSettings().getDefaultChoices());
+        if (finalFieldsValue == null) {
+            choices.remove(FINAL_FIELDS);
+        } else {
+            choices.put(FINAL_FIELDS, finalFieldsValue);
+        }
+        settings.getChoiceSettings().setDefaultChoices(choices);
+        return settings;
+    }
+
+    @Test
+    void absentChoiceDefaultsToImmutable() {
+        assertTrue(FinalHeapResolution.isFinalEnabled(settingsWith(null)),
+            "an absent finalFields choice must resolve to the declaration default 'immutable'");
+    }
+
+    @Test
+    void explicitImmutableIsEnabled() {
+        assertTrue(FinalHeapResolution.isFinalEnabled(settingsWith("finalFields:immutable")));
+    }
+
+    @Test
+    void explicitOnHeapIsDisabled() {
+        assertFalse(FinalHeapResolution.isFinalEnabled(settingsWith("finalFields:onHeap")));
+    }
+}