Update the InfoTree component

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java

@@ -3,9 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.informationflow.macros;
 
-import java.util.Map;
-import java.util.Set;
-
 import de.uka.ilkd.key.informationflow.ProofObligationVars;
 import de.uka.ilkd.key.informationflow.po.IFProofObligationVars;
 import de.uka.ilkd.key.java.Services;
@@ -17,16 +14,15 @@
 import de.uka.ilkd.key.macros.AbstractProofMacro;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.Taclet;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.util.InfFlowProgVarRenamer;
-
 import org.key_project.logic.Named;
 import org.key_project.logic.Namespace;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
 
+import java.util.Map;
+
 
 /**
  *
@@ -51,9 +47,9 @@ public String getDescription() {
 
     static JTerm calculateResultingTerm(Proof proof, IFProofObligationVars ifVars, Goal initGoal) {
         final JTerm[] goalFormulas1 =
-            buildExecution(ifVars.c1, ifVars.getMapFor(ifVars.c1), proof.openGoals(), initGoal);
+                buildExecution(ifVars.c1, ifVars.getMapFor(ifVars.c1), proof.openGoals(), initGoal);
         final JTerm[] goalFormulas2 =
-            buildExecution(ifVars.c2, ifVars.getMapFor(ifVars.c2), proof.openGoals(), initGoal);
+                buildExecution(ifVars.c2, ifVars.getMapFor(ifVars.c2), proof.openGoals(), initGoal);
         final TermBuilder tb = proof.getServices().getTermBuilder();
         JTerm composedStates = tb.ff();
         for (int i = 0; i < goalFormulas1.length; i++) {
@@ -69,7 +65,7 @@ static JTerm calculateResultingTerm(Proof proof, IFProofObligationVars ifVars, G
      * Merge namespaces.
      *
      * @param initiatingProof the initiating proof
-     * @param sideProof the side proof
+     * @param sideProof       the side proof
      */
     protected final void mergeNamespaces(Proof initiatingProof, Proof sideProof) {
         NamespaceSet initiatingProofNS = initiatingProof.getServices().getNamespaces();
@@ -95,11 +91,11 @@ private final <E extends Named> void mergeNamespace(Namespace<E> tar, Namespace<
     }
 
     private static JTerm[] buildExecution(ProofObligationVars c, Map<JTerm, JTerm> vsMap,
-            ImmutableList<Goal> symbExecGoals, Goal initGoal) {
+                                          ImmutableList<Goal> symbExecGoals, Goal initGoal) {
         Services services = initGoal.proof().getServices();
         final JTerm[] goalFormulas = buildFormulasFromGoals(symbExecGoals);
         final InfFlowProgVarRenamer renamer = new InfFlowProgVarRenamer(goalFormulas, vsMap,
-            c.postfix, initGoal, services.getOverlay(initGoal.getLocalNamespaces()));
+                c.postfix, initGoal, services.getOverlay(initGoal.getLocalNamespaces()));
         final JTerm[] renamedGoalFormulas = renamer.renameVariablesAndSkolemConstants();
         JTerm[] result = new JTerm[renamedGoalFormulas.length];
         final TermBuilder tb = services.getTermBuilder();
@@ -137,13 +133,11 @@ private static JTerm buildFormulaFromGoal(Goal symbExecGoal) {
     protected static void addContractApplicationTaclets(Goal initiatingGoal, Proof symbExecProof) {
         final ImmutableList<Goal> openGoals = symbExecProof.openGoals();
         for (final Goal openGoal : openGoals) {
-            final Set<NoPosTacletApp> ruleApps = openGoal.indexOfTaclets().allNoPosTacletApps();
-            for (final NoPosTacletApp ruleApp : ruleApps) {
-                final Taclet t = ruleApp.taclet();
-                if (t.getSurviveSymbExec()) {
-                    initiatingGoal.addTaclet(t, SVInstantiations.EMPTY_SVINSTANTIATIONS, true);
-                }
-            }
+            openGoal.indexOfTaclets()
+                    .allNoPosTacletAppsStream()
+                    .filter(it -> it.taclet().getSurviveSymbExec())
+                    .forEach(it ->
+                            initiatingGoal.addTaclet(it.taclet(), SVInstantiations.EMPTY_SVINSTANTIATIONS, true));
         }
     }
 }

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.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java

@@ -5,6 +5,7 @@
 
 import java.net.URL;
 import java.util.Objects;
+import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.proof.Proof;
@@ -15,11 +16,15 @@
 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;
+
 /**
  * @author Alexander Weigl
  * @version 1 (7/27/25)
@@ -97,9 +102,34 @@ public RuleCollection getStandardRules() {
         return wdStandardRules;
     }
 
+    /// {@inheritDoc}
+    ///
+    /// @param additionalProfileOptions a string representing the choice of `wdOperator`
     @Override
-    public void prepareInitConfig(InitConfig baseConfig) {
+    public void prepareInitConfig(InitConfig baseConfig,
+            @Nullable Configuration additionalProfileOptions) {
         var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
         baseConfig.activateChoice(wdChoice);
+
+        if (additionalProfileOptions != null) {
+            final var selectedWdOperator = additionalProfileOptions.getString("wdOperator");
+            if (selectedWdOperator == null) {
+                return;
+            }
+
+            var wdOperator = baseConfig.choiceNS().lookup(selectedWdOperator);
+            if (wdOperator == null) {
+                var choices = baseConfig.choiceNS().allElements()
+                        .stream()
+                        .filter(it -> it.category().equals("wdOperator"))
+                        .map(Choice::toString)
+                        .collect(Collectors.joining(", "));
+
+                throw new IllegalStateException("Could not find choice for %s. \n Choices known %s."
+                        .formatted(additionalProfileOptions, choices));
+            } else {
+                baseConfig.activateChoice(wdOperator);
+            }
+        }
     }
 }

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

@@ -38,10 +38,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/antlr4/KeYParser.g4

@@ -90,17 +90,18 @@ one_sort_decl
 :
   doc=DOC_COMMENT?
   (
-     GENERIC  sortIds=simple_ident_dots_comma_list
+     GENERIC  sortIds=simple_ident_dots_comma_list_with_docs
         (ONEOF sortOneOf = oneof_sorts)?
         (EXTENDS sortExt = extends_sorts)? SEMI
-    | PROXY  sortIds=simple_ident_dots_comma_list (EXTENDS sortExt=extends_sorts)? SEMI
-    | ABSTRACT? (sortIds=simple_ident_dots_comma_list | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)?  SEMI
+    | PROXY  sortIds=simple_ident_dots_comma_list_with_docs (EXTENDS sortExt=extends_sorts)? SEMI
+    | ABSTRACT? (sortIds=simple_ident_dots_comma_list_with_docs | parametric_sort_decl) (EXTENDS sortExt=extends_sorts)?  SEMI
     | ALIAS simple_ident_dots EQUALS sortId SEMI
   )
 ;
 
 parametric_sort_decl
 :
+    DOC_COMMENT?
     simple_ident_dots
     formal_sort_param_decls
 ;
@@ -115,6 +116,13 @@ simple_ident_dots_comma_list
   simple_ident_dots (COMMA simple_ident_dots)*
 ;
 
+simple_ident_dots_comma_list_with_docs
+:
+    simple_ident_dots_with_docs (COMMA simple_ident_dots_with_docs)*
+;
+
+simple_ident_dots_with_docs: DOC_COMMENT? simple_ident_dots;
+
 
 extends_sorts
 :
@@ -139,7 +147,7 @@ prog_var_decls
     LBRACE
     (
         kjt = keyjavatype
-        var_names = simple_ident_comma_list
+        var_names = simple_ident_comma_list_with_docs
         SEMI
     )*
     RBRACE
@@ -161,6 +169,10 @@ simple_ident_comma_list
     id = simple_ident (COMMA id = simple_ident )*
 ;
 
+simple_ident_comma_list_with_docs
+:
+    id+=simple_ident_with_doc (COMMA id+=simple_ident_with_doc)*
+;
 
 schema_var_decls :
     SCHEMAVARIABLES LBRACE
@@ -259,6 +271,7 @@ datatype_decl:
 ;
 
 datatype_constructor:
+  doc=DOC_COMMENT?
   name=simple_ident
   (
     LPAREN
@@ -341,7 +354,12 @@ where_to_bind:
 
 ruleset_decls
 :
-  HEURISTICSDECL LBRACE  (doc+=DOC_COMMENT? id+=simple_ident SEMI)* RBRACE
+  HEURISTICSDECL LBRACE  (id+=simple_ident_with_doc SEMI)* RBRACE
+;
+
+simple_ident_with_doc
+:
+    doc=DOC_COMMENT? id=simple_ident
 ;
 
 sortId

key.core/src/main/java/de/uka/ilkd/key/java/loader/JP2KeYConverter.java

@@ -1736,13 +1736,13 @@ public Object handleSpecialFunctionInvocation(Node n, String name,
                     "Requested to find the default value of an unknown sort '%s'.", sortName));
             }
 
-            var doc = sort.getDocumentation();
-
+            String doc = services.getNamespaces().docs().findDocumentation(sort);
+            String origin = services.getNamespaces().docs().findOrigin(sort);
             if (doc == null) {
                 return reportError(n,
                     format("Requested to find the default value for the sort '%s', " +
                         "which does not have a documentary comment. The sort is defined at %s. ",
-                        sortName, sort.getOrigin()));
+                        sortName, origin));
             }
 
             int pos = doc.indexOf(DEFVALUE);
@@ -1754,7 +1754,7 @@ public Object handleSpecialFunctionInvocation(Node n, String name,
                     return reportError(n,
                         format(
                             "Forgotten closing parenthesis on @defaultValue annotation for sort '%s' in '%s'",
-                            sortName, sort.getOrigin()));
+                            sortName, origin));
                 }
 
                 // set this as the function name, as the user had written \dl_XXX

key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java

@@ -16,7 +16,6 @@
 import org.key_project.util.collection.ImmutableSet;
 
 import org.jspecify.annotations.NonNull;
-import org.jspecify.annotations.Nullable;
 
 /**
  * In contrast to the distinction of formulas and terms as made by most of the inductive definitions
@@ -118,9 +117,4 @@ public interface JTerm
      *         non-empty {@link JavaBlock}, {@code false} no {@link JavaBlock} available.
      */
     boolean containsJavaBlockRecursive();
-
-    /**
-     * Returns a human-readable source of this term. For example the filename with line and offset.
-     */
-    default @Nullable String getOrigin() { return null; }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java

@@ -52,7 +52,7 @@ public class LabeledTermImpl extends TermImpl {
     public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
             ImmutableArray<QuantifiableVariable> boundVars,
             ImmutableArray<TermLabel> labels, String origin) {
-        super(op, subs, boundVars, origin);
+        super(op, subs, boundVars);
         assert labels != null : "Term labels must not be null";
         assert !labels.isEmpty() : "There must be at least one term label";
         this.labels = labels;
@@ -69,7 +69,7 @@ public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
     public LabeledTermImpl(Operator op, ImmutableArray<JTerm> subs,
             ImmutableArray<QuantifiableVariable> boundVars,
             ImmutableArray<TermLabel> labels) {
-        super(op, subs, boundVars, "");
+        super(op, subs, boundVars);
         assert labels != null : "Term labels must not be null";
         assert !labels.isEmpty() : "There must be at least one term label";
         this.labels = labels;

key.core/src/main/java/de/uka/ilkd/key/logic/MetaSpace.java

@@ -0,0 +1,89 @@
+/* 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.logic;
+
+import java.util.Map;
+import java.util.TreeMap;
+
+import org.key_project.logic.HasMeta;
+
+import org.jspecify.annotations.NullMarked;
+import org.jspecify.annotations.Nullable;
+
+/// MetaSpace is a namespace for storing additional information
+///
+/// @author weigl
+@NullMarked
+public class MetaSpace {
+    public static final String SPACE_PREFIX_DOC = "doc/";
+    public static final String SPACE_PREFIX_ORIGIN = "origin/";
+
+    private @Nullable MetaSpace parent;
+    private final Map<String, Object> metadata = new TreeMap<>();
+
+    public MetaSpace() {
+    }
+
+    public MetaSpace(Map<String, Object> documentation) {
+        this.metadata.putAll(documentation);
+    }
+
+    public MetaSpace(MetaSpace parent) {
+        this.parent = parent;
+    }
+
+    private @Nullable Object findMetadata(String key) {
+        return metadata.get(key);
+    }
+
+    public @Nullable String findDocumentation(HasMeta entity) {
+        if (entity.getDocumentation() != null) {
+            return entity.getDocumentation();
+        }
+        return (String) findMetadata(SPACE_PREFIX_DOC + entity.getMetaKey());
+    }
+
+    /**
+     * Returns a human-readable source of this term. For example the filename with line and offset.
+     */
+    public @Nullable String findOrigin(HasMeta entity) {
+        return (String) findMetadata(SPACE_PREFIX_ORIGIN + entity.getMetaKey());
+    }
+
+    public void add(MetaSpace space) {
+        this.metadata.putAll(space.metadata);
+    }
+
+    public @Nullable MetaSpace parent() {
+        return parent;
+    }
+
+    public void setDocumentation(HasMeta entity, @Nullable String doc) {
+        if (doc != null && doc.isBlank()) {
+            return;
+        }
+        setMetadata(SPACE_PREFIX_DOC, entity, doc);
+    }
+
+    public void setOrigin(HasMeta entity, @Nullable String origin) {
+        if (origin != null && origin.isBlank()) {
+            return;
+        }
+        setMetadata(SPACE_PREFIX_ORIGIN, entity, origin);
+    }
+
+    private void setMetadata(String prefix, HasMeta entity, @Nullable Object val) {
+        var key = prefix + entity.getMetaKey();
+        if (val == null) {
+            metadata.remove(key);
+        } else {
+            metadata.put(key, val);
+        }
+    }
+
+
+    public MetaSpace copy() {
+        return new MetaSpace(metadata);
+    }
+}