Adding the possibility to have a Profile-dependent option panel

# Conflicts:
#	key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java

# Conflicts:
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

Author: wadoon

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java

@@ -325,4 +325,9 @@ public static boolean isTruthValueEvaluationEnabled(Profile profile) {
             return false;
         }
     }
+
+    @Override
+    public String displayName() {
+        return NAME;
+    }
 }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java

@@ -27,7 +27,6 @@
 import de.uka.ilkd.key.rule.BuiltInRule;
 import de.uka.ilkd.key.rule.OneStepSimplifier;
 import de.uka.ilkd.key.rule.Taclet;
-import de.uka.ilkd.key.rule.tacletbuilder.TacletBuilder;
 import de.uka.ilkd.key.settings.ProofSettings;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile;
@@ -818,8 +817,7 @@ protected ImmutableList<TermLabelConfiguration> computeTermLabelConfiguration()
                 : null;
         initConfig.setSettings(clonedSettings);
         initConfig.setTaclet2Builder(
-            (HashMap<Taclet, TacletBuilder<? extends Taclet>>) sourceInitConfig.getTaclet2Builder()
-                    .clone());
+            new HashMap<>(sourceInitConfig.getTaclet2Builder()));
         initConfig.setTaclets(sourceInitConfig.getTaclets());
         // Create new ProofEnvironment and initialize it with values from initial one.
         ProofEnvironment env = new ProofEnvironment(initConfig);

key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java

@@ -4,7 +4,10 @@
 package de.uka.ilkd.key.wd;
 
 import java.net.URL;
+import java.util.ArrayList;
+import java.util.List;
 import java.util.Objects;
+import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.proof.Proof;
@@ -15,21 +18,30 @@
 import de.uka.ilkd.key.proof.io.RuleSourceFactory;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
 import de.uka.ilkd.key.rule.*;
+import de.uka.ilkd.key.settings.Configuration;
 import de.uka.ilkd.key.util.KeYResourceManager;
 
+import org.key_project.logic.Choice;
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
 /**
  * @author Alexander Weigl
  * @version 1 (7/27/25)
  */
 public class WdProfile extends JavaProfile {
+    private static final Logger LOGGER = LoggerFactory.getLogger(WdProfile.class);
+
     public static final String PROFILE_ID = "java-wd";
     public static final String DISPLAY_NAME = "Java Profile + Well-Definedness Checks";
 
     public static final WdProfile INSTANCE = new WdProfile();
 
+
     private final RuleCollection wdStandardRules;
 
     public WdProfile() {
@@ -97,9 +109,54 @@ public RuleCollection getStandardRules() {
         return wdStandardRules;
     }
 
+    /// {@inheritDoc}
+    ///
+    /// @param additionalProfileOptions a string representing the choice of `wdOperator`
+    /// @return
     @Override
-    public void prepareInitConfig(InitConfig baseConfig) {
-        var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
-        baseConfig.activateChoice(wdChoice);
+    public List<String> prepareInitConfig(InitConfig baseConfig,
+            @Nullable Configuration additionalProfileOptions) {
+        var warnings = new ArrayList<String>(2);
+        var wdChoiceOn = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
+        var wdChoiceOff = baseConfig.choiceNS().lookup(new Name("wdChecks:off"));
+
+        if (baseConfig.isChoiceActive(wdChoiceOff)) {
+            final var message =
+                "wdChecks:off was set by in the init config, probably given in KeY file. This setting will be ignored";
+            warnings.add(message);
+            LOGGER.warn(message); // this logging is for finding the spot.
+        }
+        baseConfig.activateChoice(wdChoiceOn);
+
+
+        if (additionalProfileOptions != null) {
+            final var wdOperator = "wdOperator";
+            final var selectedWdOperator = additionalProfileOptions.getString(wdOperator);
+            if (selectedWdOperator == null) {
+                return warnings;
+            }
+
+            var wdOperatorChoice = baseConfig.choiceNS().lookup(selectedWdOperator);
+            if (wdOperatorChoice == null) {
+                var choices = baseConfig.choiceNS().allElements()
+                        .stream()
+                        .filter(it -> wdOperator.equals(it.category()))
+                        .map(Choice::toString)
+                        .collect(Collectors.joining(", "));
+
+                throw new IllegalStateException("Could not find choice for %s.\n  Choices known %s."
+                        .formatted(additionalProfileOptions, choices));
+            } else {
+                if (baseConfig.isChoiceCategorySet(wdOperator)
+                        && !baseConfig.isChoiceActive(wdOperatorChoice)) {
+                    final var message = "Choice for wdOperator will be overwritten " +
+                        "by profile as defined by user in the additional profile options.";
+                    warnings.add(message);
+                    LOGGER.warn(message); // this logging is for finding the spot.
+                }
+                baseConfig.activateChoice(wdOperatorChoice);
+            }
+        }
+        return warnings;
     }
 }

key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java

@@ -17,7 +17,6 @@
 
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
-import org.jspecify.annotations.Nullable;
 
 
 @NullMarked
@@ -38,10 +37,6 @@ public Name name() {
         return NAME;
     }
 
-    @Override
-    public @Nullable String getOrigin() {
-        return super.getOrigin();
-    }
 
     protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier {
         public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp<?> ruleApp) {

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

@@ -6,8 +6,6 @@
 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.
@@ -23,8 +21,7 @@
  * @author Mattias Ulbrich
  */
 public class FinalHeapResolution {
-
-    private static final ThreadLocal<Boolean> finalEnabledVariable = new ThreadLocal<>();
+    private static volatile boolean finalEnabledVariable;
     private static final String SETTING = "finalFields";
     private static final String IMMUTABLE_OPTION = SETTING + ":immutable";
 
@@ -36,7 +33,7 @@ public class FinalHeapResolution {
      * @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) {
+    public static boolean isFinalEnabled(InitConfig initConfig) {
         ProofSettings settings = initConfig.getSettings();
         if (settings == null) {
             settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
@@ -50,8 +47,9 @@ public static boolean isFinalEnabled(@NonNull InitConfig initConfig) {
      * @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)
+    public static boolean isFinalEnabled(ProofSettings settings) {
+        return settings.getChoiceSettings().getDefaultChoices()
+                .getOrDefault(SETTING, "")
                 .equals(IMMUTABLE_OPTION);
     }
 
@@ -62,7 +60,7 @@ public static boolean isFinalEnabled(@NonNull ProofSettings settings) {
      * @param initConfig the configuration to read the settings from
      */
     public static void rememberIfFinalEnabled(InitConfig initConfig) {
-        finalEnabledVariable.set(isFinalEnabled(initConfig));
+        finalEnabledVariable = isFinalEnabled(initConfig);
     }
 
     /**
@@ -74,7 +72,7 @@ public static void rememberIfFinalEnabled(InitConfig initConfig) {
      */
 
     public static boolean recallIsFinalEnabled() {
-        Boolean bool = finalEnabledVariable.get();
+        Boolean bool = finalEnabledVariable;
         if (bool == null) {
             throw new IllegalStateException("Unset final enabled variable");
         }

key.core/src/main/java/de/uka/ilkd/key/nparser/ChoiceInformation.java

@@ -42,7 +42,7 @@ public class ChoiceInformation {
     /**
      * This map contains the default option for every category.
      */
-    private final Map<String, String> defaultOptions = new TreeMap<>();
+    private final Map<String, Choice> defaultOptions = new TreeMap<>();
 
     public ChoiceInformation() {
         this(new Namespace<>());
@@ -68,11 +68,11 @@ public Namespace<Choice> getChoices() {
         return choices;
     }
 
-    public void setDefaultOption(String category, String choice) {
-        defaultOptions.put(category, category + ":" + choice);
+    public void setDefaultOption(String category, Choice choice) {
+        defaultOptions.put(category, choice);
     }
 
-    public Map<String, String> getDefaultOptions() {
+    public Map<String, Choice> getDefaultOptions() {
         return defaultOptions;
     }
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -191,6 +191,16 @@ public Configuration asConfiguration() {
                 throw new RuntimeException("Error in configuration. Source: "
                     + ctx.start.getTokenSource().getSourceName());
         }
+
+        public List<Configuration> asConfigurationList() {
+            final var cfg = new ConfigurationBuilder();
+            List<Object> res = cfg.visitCfile(ctx);
+            if (!res.isEmpty())
+                return (List<Configuration>) res.getFirst();
+            else
+                throw new RuntimeException("Error in configuration. Source: "
+                    + ctx.start.getTokenSource().getSourceName());
+        }
     }
 
     public static class SetStatementContext extends KeyAst<JmlParser.Set_statementContext> {

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java

@@ -56,8 +56,9 @@ public Object visitChoice(KeYParser.ChoiceContext ctx) {
         }
 
         seq().put(category, new HashSet<>(options));
-        choiceInformation.setDefaultOption(category, options.get(0));
-        options.forEach(it -> choices().add(new Choice(it, category)));
+        var choices = options.stream().map(it -> new Choice(it, category)).toList();
+        choices.forEach(it -> choices().add(it));
+        choiceInformation.setDefaultOption(category, choices.getFirst());
         return null;
     }