addressing the review

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/pp/FieldPrinter.java

@@ -131,6 +131,9 @@ protected static boolean isFieldConstant(Term fieldTerm, HeapLDT heapLDT) {
     protected static boolean isJavaFieldConstant(Term fieldTerm, HeapLDT heapLDT,
             Services services) {
         try {
+            // the called method either returns a ProgramVariable or throws an exception
+            // We are only interested in whether the method throws an exception or not, so we
+            // ignore the return value.
             getJavaFieldConstant(fieldTerm, heapLDT, services);
             return true;
         } catch (RuntimeException e) {

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldCodeValidator.java

@@ -10,7 +10,9 @@
 import de.uka.ilkd.key.java.*;
 import de.uka.ilkd.key.java.abstraction.ClassType;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
+import de.uka.ilkd.key.java.abstraction.Type;
 import de.uka.ilkd.key.java.expression.Assignment;
+import de.uka.ilkd.key.java.expression.operator.New;
 import de.uka.ilkd.key.java.reference.*;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.logic.op.ProgramMethod;
@@ -139,8 +141,8 @@ private void validate(IProgramMethod method) {
     private void validateProgramElement(SyntaxElement element) {
         if (element instanceof MethodReference methodReference) {
             validateMethodReference(methodReference);
-        } else if (element instanceof ConstructorReference constructorReference) {
-            validateConstructorReference(constructorReference);
+        } else if (element instanceof New _new) {
+            validateNew(_new);
         } else if (element instanceof FieldReference fieldReference) {
             validateFieldReference(fieldReference);
         } else if (element instanceof Assignment assignment) {
@@ -165,18 +167,27 @@ private void validateChildren(SyntaxElement element) {
     /*
      * Constructor calls must not leak 'this' to the called constructor.
      */
-    private void validateConstructorReference(ConstructorReference methodReference) {
-        // TODO We have to make sure that on non-static subclass is instantiated here
+    private void validateNew(New _new) {
+
+        TypeReference typeRef = _new.getTypeReference();
+        Type type = typeRef.getKeYJavaType().getJavaType();
+        if (type instanceof ClassType classType && !classType.isStatic()) {
+            // This also disallows things like "a.new B()" which would not like this. However,
+            // KeY cannot deal with this anyway, so we can do the easy check here.
+            throw new FinalViolationException(
+                "Call to non-static inner class " + classType + " leaks 'this' to the constructor",
+                _new);
+        }
+
         var hasThisArgument =
-            methodReference.getArguments().stream().anyMatch(ThisReference.class::isInstance);
+            _new.getArguments().stream().anyMatch(ThisReference.class::isInstance);
 
         if (hasThisArgument) {
             throw new FinalViolationException(
-                "Method call " + methodReference + " leaks 'this' to called method.",
-                methodReference);
+                "Method call " + _new + " leaks 'this' to called method.", _new);
         }
 
-        validateChildren(methodReference);
+        validateChildren(_new);
     }
 
     /*

key.core/src/main/java/de/uka/ilkd/key/proof/init/FinalFieldsPOExtension.java

@@ -57,7 +57,8 @@ public Term modifyPostTerm(AbstractOperationPO abstractPO, InitConfig proofConfi
         // We know this holds because of isPOSupported:
         FunctionalOperationContractPO fpo = (FunctionalOperationContractPO) abstractPO;
         IProgramMethod iconstructor = fpo.getProgramMethod();
-        assert iconstructor instanceof ProgramMethod : "Contracts cannot have schema ";
+        assert iconstructor instanceof ProgramMethod
+                : "Expected a ProgramMethod not a schema variable, since we need the actual implementation";
         ProgramMethod constructor = (ProgramMethod) iconstructor;
 
         FinalFieldCodeValidator.validateFinalFields(constructor, proofConfig);

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key

@@ -22,7 +22,7 @@
     // default value for a field
     alpha alpha::defaultValue;
 
-    // reading from final attributes (corr. to select for non-final fields)
+    // reading from final attributes (corresponds to select for non-final fields)
     alpha alpha::final(Object, Field);
 
     // fields

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/javaRules.key

@@ -3804,7 +3804,9 @@
         \heuristics(simplify_prog, simplify_prog_subset)
         \displayname "active_attribute_access"
     };
+}
 
+\rules(programRules:Java, finalFields:onHeap) {
     // TODO 2 variants with different taclet options
     assignment_read_static_attribute {
         \find(\modality{#allmodal}{.. #v0 = @(#sv); ...}\endmodality (post))
@@ -3819,7 +3821,9 @@
         }
         \heuristics(simplify_prog, simplify_prog_subset)
     };
+}
 
+\rules(programRules:Java, finalFields:immutable) {
     assignment_read_static_attribute_final {
         \find(\modality{#allmodal}{.. #v0 = @(#sv); ...}\endmodality (post))
         \sameUpdateLevel
@@ -3833,7 +3837,9 @@
         }
         \heuristics(simplify_prog, simplify_prog_subset)
     };
+}
 
+\rules(programRules:Java) {
     // constant case cannot occur as no static initilisation handling happens
     assignment_read_static_attribute_with_variable_prefix {
         \find(\modality{#allmodal}{.. #loc = @(#v.#sv); ...}\endmodality (post))

key.core/src/test/java/de/uka/ilkd/key/pp/FinalPrinterTest.java

@@ -6,7 +6,6 @@
 import java.io.File;
 import java.net.URL;
 import java.util.List;
-import java.util.stream.Stream;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Choice;
@@ -18,8 +17,7 @@
 import org.junit.jupiter.api.AfterAll;
 import org.junit.jupiter.api.BeforeAll;
 import org.junit.jupiter.params.ParameterizedTest;
-import org.junit.jupiter.params.provider.Arguments;
-import org.junit.jupiter.params.provider.MethodSource;
+import org.junit.jupiter.params.provider.CsvSource;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
 import static org.junit.jupiter.api.Assertions.assertTrue;
@@ -45,18 +43,15 @@ public static void tearDown() {
         io = null;
     }
 
-    public static Stream<Arguments> casesWithFinal() {
-        return Stream.of(
-            Arguments.of("int::select(heap, self, C::$f)", "self.f"),
-            Arguments.of("int::select(heap, self, C::$finf)", "int::select(heap, self, C::$finf)"),
-            Arguments.of("int::final(sub, Csub::$finf)", "sub.finf"),
-            Arguments.of("int::final(sub, C::$finf)", "sub.(C::finf)"),
-            Arguments.of("int::final(self, C::$finf)", "self.finf"),
-            Arguments.of("int::final(sub, C::$finf)", "sub.(C::finf)"));
-    }
-
     @ParameterizedTest(name = "{0} => {1}")
-    @MethodSource("casesWithFinal")
+    @CsvSource(delimiter = ';', textBlock = """
+            int::select(heap, self, C::$f); self.f
+            int::select(heap, self, C::$finf); int::select(heap, self, C::$finf)
+            int::final(sub, Csub::$finf); sub.finf
+            int::final(sub, C::$finf); sub.(C::finf)
+            int::final(self, C::$finf); self.finf
+            int::final(sub, C::$finf); sub.(C::finf)
+            """)
     public void testPPWithFinal(String termString, String expected) throws Exception {
         services.getProof().getSettings().getChoiceSettings()
                 .updateWith(List.of(PrettyPrinterRoundtripTest.WITH_FINAL));
@@ -68,18 +63,14 @@ public void testPPWithFinal(String termString, String expected) throws Exception
         assertEquals(expected, printed);
     }
 
-    public static Stream<Arguments> casesWithoutFinal() {
-        return Stream.of(
-            Arguments.of("int::final(sub, Csub::$finf)", "sub.finf"),
-            Arguments.of("int::final(sub, C::$finf)", "sub.(C::finf)"),
-            Arguments.of("int::final(self, C::$finf)", "self.finf"),
-            Arguments.of("int::select(heap, self, C::$f)", "self.f"),
-            Arguments.of("int::select(heap, self, C::$finf)", "self.finf"));
-    }
-
-
     @ParameterizedTest(name = "{0} => {1}")
-    @MethodSource("casesWithoutFinal")
+    @CsvSource(delimiter = ';', textBlock = """
+            int::final(sub, Csub::$finf); sub.finf
+            int::final(sub, C::$finf); sub.(C::finf)
+            int::final(self, C::$finf); self.finf
+            int::select(heap, self, C::$f); self.f
+            int::select(heap, self, C::$finf); self.finf
+            """)
     public void testPPWithoutFinal(String termString, String expected) throws Exception {
         services.getProof().getSettings().getChoiceSettings()
                 .updateWith(List.of(PrettyPrinterRoundtripTest.WITHOUT_FINAL));

key.ui/src/main/resources/de/uka/ilkd/key/gui/help/choiceExplanations.xml

@@ -231,5 +231,22 @@ Treatment of formulas and terms for welldefinedness checks:
 <entry key="wdChecks">
 Welldefinedness checks of JML specifications can be turned on/off. This includes class invariants, operation contracts, model fields as well as JML (annotation) statements as loop invariants and block contracts. The former ones are checked "on-the-fly", i.e., directly when they are applied in the code while proving an operation contract, since the context is needed.
 </entry>
+
+<entry key="finalFields">
+Final fields can only be written to from within the constructor. This is a
+Java language feature. KeY can exploit this restriction by treating final fields
+as immutable. This can simplify the reasoning about the program significantly.
+But it is still possible to tread final fields as normal mutable fields to
+ensure backward compatibility. If constructor code is to be inlined, there
+can be cases where the immutable treatment is incomplete.
+
+immutable:
+    Final fields are treated as immutable entities.
+    This is the default option.
+
+onHeap:
+    Final fields are treated like all Java fields.
+    This is the original behaviour of KeY.
+</entry>
 </properties>