MetaSpace for documentation and origin

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

@@ -4,7 +4,6 @@
 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;
@@ -17,8 +16,6 @@
 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;
 
@@ -137,13 +134,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.wd/src/main/java/de/uka/ilkd/key/wd/WdWhileInvariantRule.java

@@ -37,7 +37,6 @@ public Name name() {
         return NAME;
     }
 
-
     protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier {
         public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp<?> ruleApp) {
             super(goal, ruleApp);

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

@@ -32,6 +32,7 @@
 import de.uka.ilkd.key.java.transformations.pipeline.JMLTransformer;
 import de.uka.ilkd.key.ldt.HeapLDT;
 import de.uka.ilkd.key.ldt.JavaDLTheory;
+import de.uka.ilkd.key.logic.MetaSpace;
 import de.uka.ilkd.key.logic.ProgramElementName;
 import de.uka.ilkd.key.logic.VariableNamer;
 import de.uka.ilkd.key.logic.op.*;
@@ -1694,6 +1695,10 @@ public Object visit(KeyCcatchParameter n, Void arg) {
         return new Ccatch(pi, c, parameter, null, body);
     }
 
+    public MetaSpace docSpace() {
+        return services.getNamespaces().docs();
+    }
+
     @Override
     public Object visit(KeyCcatchReturn n, Void arg) {
         var pi = createPositionInfo(n);
@@ -1738,13 +1743,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);
@@ -1756,7 +1761,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);
+    }
+}