Improved treatment of final fields

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/po/TruthValuePOExtension.java

@@ -8,6 +8,7 @@
 import de.uka.ilkd.key.logic.TermFactory;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
+import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.proof.init.AbstractOperationPO;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.POExtension;
@@ -35,7 +36,9 @@ public boolean isPOSupported(ProofOblInput po) {
      * {@inheritDoc}
      */
     @Override
-    public Term modifyPostTerm(InitConfig proofConfig, Services services, Term postTerm) {
+    public Term modifyPostTerm(AbstractOperationPO abstractOperationPO, InitConfig proofConfig,
+            Services services, ProgramVariable selfTerm,
+            Term postTerm) {
         if (SymbolicExecutionJavaProfile.isTruthValueEvaluationEnabled(proofConfig)) {
             return labelPostTerm(services, postTerm);
         } else {

key.core/src/main/java/de/uka/ilkd/key/java/abstraction/Variable.java

@@ -18,6 +18,13 @@ public interface Variable extends ProgramModelElement {
      */
     boolean isFinal();
 
+    /**
+     * Checks if this variable is a model entity.
+     *
+     * @return <CODE>true</CODE> if this variable is a model entity, <CODE>false</CODE> otherwise.
+     */
+    public boolean isModel();
+
     /**
      * Returns the type of this variable.
      *

key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldSpecification.java

@@ -91,7 +91,7 @@ public String getProgramName() {
      * Test whether the declaration is static.
      */
     public boolean isStatic() {
-        return ((ProgramVariable) var).isStatic();
+        return ((ProgramVariable) programVar).isStatic();
     }
 
     /**

key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java

@@ -9,6 +9,7 @@
 import de.uka.ilkd.key.java.visitor.Visitor;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
+import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.rule.MatchConditions;
 
 import org.key_project.util.ExtList;
@@ -46,33 +47,33 @@ public class VariableSpecification extends JavaNonTerminalProgramElement
      */
     protected final Type type;
 
-    protected final IProgramVariable var;
+    protected final IProgramVariable programVar;
 
     public VariableSpecification() {
         this(null, 0, null, null, null);
     }
 
-    public VariableSpecification(IProgramVariable var) {
-        this(var, var.getKeYJavaType());
+    public VariableSpecification(IProgramVariable programVar) {
+        this(programVar, programVar.getKeYJavaType());
     }
 
-    public VariableSpecification(IProgramVariable var, Type type) {
-        this(var, 0, null, type, null);
+    public VariableSpecification(IProgramVariable programVar, Type type) {
+        this(programVar, 0, null, type, null);
     }
 
 
-    public VariableSpecification(IProgramVariable var, Expression init, Type type) {
-        this(var, 0, init, type, null);
+    public VariableSpecification(IProgramVariable programVar, Expression init, Type type) {
+        this(programVar, 0, init, type, null);
     }
 
-    public VariableSpecification(IProgramVariable var, int dim, Expression init, Type type) {
-        this(var, dim, init, type, PositionInfo.UNDEFINED);
+    public VariableSpecification(IProgramVariable programVar, int dim, Expression init, Type type) {
+        this(programVar, dim, init, type, PositionInfo.UNDEFINED);
     }
 
-    public VariableSpecification(IProgramVariable var, int dim, Expression init, Type type,
+    public VariableSpecification(IProgramVariable programVar, int dim, Expression init, Type type,
             PositionInfo pi) {
         super(pi);
-        this.var = var;
+        this.programVar = programVar;
         this.initializer = init;
         this.dimensions = dim;
         this.type = type;
@@ -86,9 +87,10 @@ public VariableSpecification(IProgramVariable var, int dim, Expression init, Typ
      *        (as initializer of the variable) a Comment
      * @param dim the dimension of this type
      */
-    public VariableSpecification(ExtList children, IProgramVariable var, int dim, Type type) {
+    public VariableSpecification(ExtList children, IProgramVariable programVar, int dim,
+            Type type) {
         super(children);
-        this.var = var;
+        this.programVar = programVar;
         initializer = children.get(Expression.class);
         dimensions = dim;
         this.type = type;
@@ -102,7 +104,7 @@ public VariableSpecification(ExtList children, IProgramVariable var, int dim, Ty
      */
     public int getChildCount() {
         int result = 0;
-        if (var != null) {
+        if (programVar != null) {
             result++;
         }
         if (initializer != null) {
@@ -119,9 +121,9 @@ public int getChildCount() {
      * @throws ArrayIndexOutOfBoundsException if <tt>index</tt> is out of bounds
      */
     public ProgramElement getChildAt(int index) {
-        if (var != null) {
+        if (programVar != null) {
             if (index == 0) {
-                return var;
+                return programVar;
             }
             index--;
         }
@@ -169,7 +171,7 @@ public Expression getExpressionAt(int index) {
      * @return the string.
      */
     public final String getName() {
-        return (var == null) ? null : var.name().toString();
+        return (programVar == null) ? null : programVar.name().toString();
     }
 
     /**
@@ -178,10 +180,10 @@ public final String getName() {
      * @return the name.
      */
     public ProgramElementName getProgramElementName() {
-        if (var.name() instanceof ProgramElementName) {
-            return (ProgramElementName) var.name();
+        if (programVar.name() instanceof ProgramElementName) {
+            return (ProgramElementName) programVar.name();
         } else {
-            return new ProgramElementName(var.name().toString()); // only with SVs
+            return new ProgramElementName(programVar.name().toString()); // only with SVs
         }
     }
 
@@ -192,7 +194,7 @@ public ProgramElementName getProgramElementName() {
      * @return the program variable.
      */
     public IProgramVariable getProgramVariable() {
-        return var;
+        return programVar;
     }
 
 
@@ -220,8 +222,19 @@ public boolean hasInitializer() {
     }
 
     public boolean isFinal() {
-        LOGGER.warn("Method in Variable Specification not implemented!");
-        return false;
+        if (programVar instanceof ProgramVariable pv) {
+            return pv.isFinal();
+        }
+        // This used to return always false.
+        throw new UnsupportedOperationException("Cannot determine finality of " + programVar);
+    }
+
+    public boolean isModel() {
+        if (programVar instanceof ProgramVariable pv) {
+            return pv.isModel();
+        }
+        // This used to return always false.
+        throw new UnsupportedOperationException("Cannot determine finality of " + programVar);
     }
 
 
@@ -235,15 +248,15 @@ public String getFullName() {
 
     @Override
     public SourceElement getFirstElement() {
-        return var;
+        return programVar;
     }
 
     @Override
     public SourceElement getLastElement() {
         if (initializer != null) {
             return initializer.getLastElement();
         } else {
-            return var;
+            return programVar;
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java

@@ -295,6 +295,12 @@ private void transformFieldDecl(TextualJMLFieldDecl decl, Comment[] originalComm
                         public boolean isStatic() {
                             return false;
                         }
+
+                        @Override
+                        public boolean isFinal() {
+                            return ((FieldDeclaration) old).getModifiers()
+                                    .contains(JMLModifier.FINAL);
+                        }
                     };
                     fieldDecl.setStartPosition(old.getStartPosition());
                     fieldDecl.setEndPosition(old.getEndPosition());

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

@@ -0,0 +1,83 @@
+/* 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 de.uka.ilkd.key.proof.init.InitConfig;
+import de.uka.ilkd.key.settings.ProofSettings;
+
+import org.jspecify.annotations.NonNull;
+
+
+/**
+ * A little helper class to resolve the settings for treatment of final fields.
+ *
+ * During the generation of {@link de.uka.ilkd.key.proof.init.ProofOblInput}s, we need to know
+ * which final-treatment is activated. Also during translation from JML to JavaDL this is needed.
+ * Unfortunately, the settings are not directly available everywhere, so there is a mechanism to
+ * remember the setting while it is available in a thread-local variable. This class provides a
+ * simple interface to access this boolean variable.
+ *
+ * The alternative would be to make the settings available at more spots ...
+ *
+ * @author Mattias Ulbrich
+ */
+public class FinalHeapResolution {
+
+    private static final ThreadLocal<Boolean> finalEnabledVariable = new ThreadLocal<>();
+    private static final String SETTING = "finalFields";
+    private static final String IMMUTABLE_OPTION = SETTING + ":immutable";
+
+    /**
+     * Returns whether final fields are treated different from normal fields as immutable data.
+     *
+     * If initConfig does not have settings yet, the default settings are used.
+     *
+     * @param initConfig the configuration to read the settings from
+     * @return true if final fields are treated as immutable
+     */
+    public static boolean isFinalEnabled(@NonNull InitConfig initConfig) {
+        ProofSettings settings = initConfig.getSettings();
+        if (settings == null) {
+            settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
+        }
+        return isFinalEnabled(settings);
+    }
+
+    /**
+     * Returns whether final fields are treated different from normal fields as immutable data.
+     *
+     * @param settings the settings to read the settings from
+     * @return true if final fields are treated as immutable
+     */
+    public static boolean isFinalEnabled(@NonNull ProofSettings settings) {
+        return settings.getChoiceSettings().getDefaultChoices().get(SETTING)
+                .equals(IMMUTABLE_OPTION);
+    }
+
+    /**
+     * Remembers if final fields are treated differently from normal fields as immutable flag
+     * in a thread-local variable that can be recalled later using {@link #recallIsFinalEnabled()}.
+     *
+     * @param initConfig the configuration to read the settings from
+     */
+    public static void rememberIfFinalEnabled(InitConfig initConfig) {
+        finalEnabledVariable.set(isFinalEnabled(initConfig));
+    }
+
+    /**
+     * Recall a previously stored status regarding the treatment of final fields.
+     * See {@link #rememberIfFinalEnabled(InitConfig)}.
+     *
+     * @return true if final fields are treated as immutable (as recorded earlier)
+     * @throws IllegalStateException if the variable has not been set before
+     */
+
+    public static boolean recallIsFinalEnabled() {
+        Boolean bool = finalEnabledVariable.get();
+        if (bool == null) {
+            throw new IllegalStateException("Unset final enabled variable");
+        }
+        return bool.booleanValue();
+    }
+}

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

@@ -27,6 +27,7 @@
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
+import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
 
@@ -41,6 +42,7 @@ public final class HeapLDT extends LDT {
 
     public static final Name SELECT_NAME = new Name("select");
     public static final Name STORE_NAME = new Name("store");
+    public static final Name FINAL_NAME = new Name("final");
     public static final Name BASE_HEAP_NAME = new Name("heap");
     public static final Name SAVED_HEAP_NAME = new Name("savedHeap");
     public static final Name PERMISSION_HEAP_NAME = new Name("permissions");
@@ -54,6 +56,7 @@ public final class HeapLDT extends LDT {
 
     // select/store
     private final SortDependingFunction select;
+    private final SortDependingFunction finalFunction;
     private final JFunction store;
     private final JFunction create;
     private final JFunction anon;
@@ -96,7 +99,8 @@ public HeapLDT(TermServices services) {
 
         fieldSort = sorts.lookup(new Name("Field"));
         select = addSortDependingFunction(services, SELECT_NAME.toString());
-        store = addFunction(services, "store");
+        finalFunction = addSortDependingFunction(services, FINAL_NAME.toString());
+        store = addFunction(services, STORE_NAME.toString());
         create = addFunction(services, "create");
         anon = addFunction(services, "anon");
         memset = addFunction(services, "memset");
@@ -233,6 +237,29 @@ public SortDependingFunction getSelect(Sort instanceSort, TermServices services)
         return select.getInstanceFor(instanceSort, services);
     }
 
+    /**
+     * Returns the function symbol to access final fields for the given instance sort.
+     *
+     * @param instanceSort the sort of the value to be read
+     * @param services the services to find/create the sort-depending function
+     * @return the function symbol to access final fields for the given instance sort
+     */
+    public @NonNull SortDependingFunction getFinal(@NonNull Sort instanceSort,
+            @NonNull Services services) {
+        return finalFunction.getInstanceFor(instanceSort, services);
+    }
+
+    /**
+     * Check if the given operator is an instance of the "final" function to access final fields.
+     *
+     * @param op the operator to check
+     * @return true if the operator is an instance of the "X::final" srot-depending function
+     */
+    public boolean isFinalOp(Operator op) {
+        return op instanceof SortDependingFunction
+                && ((SortDependingFunction) op).isSimilar(finalFunction);
+    }
+
 
     /**
      * If the passed operator is an instance of "select", this method returns the sort of the