Taclet definition added to problemHeader

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java

@@ -9,6 +9,7 @@
 import de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo;
 import de.uka.ilkd.key.informationflow.proof.InfFlowProof;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.StrategyInfoUndoMethod;
 import de.uka.ilkd.key.proof.init.AbstractOperationPO;
@@ -18,6 +19,7 @@
 
 import org.key_project.prover.sequent.SequentFormula;
 
+import org.jspecify.annotations.Nullable;
 import org.slf4j.LoggerFactory;
 
 import static de.uka.ilkd.key.informationflow.proof.InfFlowCheckInfo.INF_FLOW_CHECK_TRUE;
@@ -45,7 +47,8 @@ public Proof createProof(String proofName, JTerm poTerm, InitConfig proofConfig)
     }
 
     @Override
-    public InfFlowProof createProofObject(String proofName, String proofHeader, JTerm poTerm,
+    public InfFlowProof createProofObject(String proofName,
+            KeyAst.@Nullable Declarations proofHeader, JTerm poTerm,
             InitConfig proofConfig) {
         final InfFlowProof proof = new InfFlowProof(proofName, poTerm, proofHeader, proofConfig);
 

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowProof.java

@@ -7,6 +7,7 @@
 
 import de.uka.ilkd.key.informationflow.po.InfFlowProofSymbols;
 import de.uka.ilkd.key.logic.JTerm;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.proof.BuiltInRuleIndex;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.Statistics;
@@ -20,6 +21,8 @@
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * The proof object used by Information Flow Proofs.
  *
@@ -39,12 +42,14 @@ public class InfFlowProof extends Proof {
      */
     private SideProofStatistics sideProofStatistics = null;
 
-    public InfFlowProof(String name, Sequent sequent, String header, TacletIndex rules,
+    public InfFlowProof(String name, Sequent sequent, KeyAst.@Nullable Declarations header,
+            TacletIndex rules,
             BuiltInRuleIndex builtInRules, InitConfig initConfig) {
         super(name, sequent, header, rules, builtInRules, initConfig);
     }
 
-    public InfFlowProof(String name, JTerm problem, String header, InitConfig initConfig) {
+    public InfFlowProof(String name, JTerm problem, KeyAst.@Nullable Declarations header,
+            InitConfig initConfig) {
         super(name, problem, header, initConfig);
     }
 

key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java

@@ -5,8 +5,8 @@
 
 
 import java.util.Collection;
-import java.util.HashMap;
 import java.util.Map;
+import java.util.TreeMap;
 
 import de.uka.ilkd.key.java.abstraction.*;
 import de.uka.ilkd.key.java.expression.Literal;
@@ -41,7 +41,7 @@ public final class TypeConverter {
     private final Services services;
 
     // Maps LDT names to LDT instances.
-    private final Map<Name, LDT> LDTs = new HashMap<>();
+    private final Map<Name, LDT> LDTs = new TreeMap<>();
 
     private HeapLDT heapLDT = null;
     // private IntegerLDT integerLDT = null;

key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java

@@ -106,7 +106,10 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert
         String qualifier =
             name.lastIndexOf('.') != -1 ? name.substring(0, name.lastIndexOf('.')) : "";
         name = name.substring(name.lastIndexOf('.') + 1);
-        TypeRef tr = new TypeRef(new ProgramElementName(name, qualifier), 0, null, containingClass);
+        final ProgramElementName programName =
+            qualifier.isEmpty() ? new ProgramElementName(name)
+                    : new ProgramElementName(name, qualifier);
+        TypeRef tr = new TypeRef(programName, 0, null, containingClass);
         ExecutionContext ec = new ExecutionContext(tr, null, null);
 
         for (int i = 0; i < actual; i++) {

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

@@ -151,7 +151,6 @@ public final SortDependingFunction getExactInstanceofSymbol(Sort sort, TermServi
     @Override
     public boolean isResponsible(Operator op, JTerm[] subs, Services services,
             ExecutionContext ec) {
-        assert false;
         return false;
     }
 

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

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser;
 
+import java.io.PrintWriter;
 import java.net.URI;
 import java.net.URISyntaxException;
 import java.net.URL;
@@ -170,20 +171,9 @@ public ProblemInformation getProblemInformation() {
          * declarations of sorts, program variables, schema variables, predicates, and more.
          * See the grammar (KeYParser.g4) for more possible elements.
          */
-        public String getProblemHeader() {
+        public KeyAst.@Nullable Declarations getProblemHeader() {
             final KeYParser.DeclsContext decls = ctx.decls();
-            if (decls != null && decls.getChildCount() > 0) {
-                final Token start = decls.start;
-                final Token stop = decls.stop;
-                if (start != null && stop != null) {
-                    int a = start.getStartIndex();
-                    int b = stop.getStopIndex();
-                    Interval interval = new Interval(a, b);
-                    CharStream input = ctx.start.getInputStream();
-                    return input.getText(interval);
-                }
-            }
-            return "";
+            return new KeyAst.Declarations(decls);
         }
     }
 
@@ -319,4 +309,136 @@ private static List<ScriptCommandAst> asAst(URI file,
             return new ScriptCommandAst(it.cmd.getText(), nargs, pargs, loc);
         }
     }
+
+    /// Represents the user declarations in a KeY file.
+    ///
+    /// @author weigl
+    public static class Declarations extends KeyAst<KeYParser.DeclsContext> {
+        protected Declarations(KeYParser.DeclsContext ctx) {
+            super(ctx);
+        }
+
+        public java.io.@Nullable File getJavaSourceLocation() {
+            try {
+                KeYParser.String_valueContext value =
+                    ctx.javaSource(0).oneJavaSource().string_value(0);
+                String v = ParsingFacade.getValueDocumentation(value);
+                return new java.io.File(v);
+            } catch (NullPointerException | IndexOutOfBoundsException e) {
+                {
+                    return null;
+                }
+            }
+        }
+
+        /// Prints the definitions, independent of paths, to the given {@link PrintWriter}.
+        public void printDefinitions(PrintWriter out) {
+            ctx.accept(new KeYParserBaseVisitor<@Nullable Object>() {
+                @Override
+                public @Nullable Object visitOne_include(KeYParser.One_includeContext ctx) {
+                    if (ctx.absfile != null) {
+                        out.printf("\\include %s;", ctx.absfile.getText());
+                    }
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitOptions_choice(KeYParser.Options_choiceContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitOption_decls(KeYParser.Option_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitSort_decls(KeYParser.Sort_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitProg_var_decls(KeYParser.Prog_var_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitSchema_var_decls(
+                        KeYParser.Schema_var_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitPred_decls(KeYParser.Pred_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitFunc_decls(KeYParser.Func_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitTransform_decls(KeYParser.Transform_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitDatatype_decls(KeYParser.Datatype_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+
+                @Override
+                public @Nullable Object visitRuleset_decls(KeYParser.Ruleset_declsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+
+                @Override
+                public @Nullable Object visitContracts(KeYParser.ContractsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitInvariants(KeYParser.InvariantsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                @Override
+                public @Nullable Object visitRulesOrAxioms(KeYParser.RulesOrAxiomsContext ctx) {
+                    printAsIs(ctx);
+                    return null;
+                }
+
+                private void printAsIs(ParserRuleContext ctx) {
+                    if (ctx != null) {
+                        final Token start = ctx.start;
+                        final Token stop = ctx.stop;
+                        if (start != null && stop != null) {
+                            int a = start.getStartIndex();
+                            int b = stop.getStopIndex();
+                            Interval interval = new Interval(a, b);
+                            CharStream input = ctx.start.getInputStream();
+                            out.println(input.getText(interval));
+                        }
+                    }
+                }
+            });
+
+
+        }
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java

@@ -15,6 +15,7 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.logic.NamespaceSet;
+import de.uka.ilkd.key.nparser.KeyAst;
 import de.uka.ilkd.key.pp.AbbrevMap;
 import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit;
 import de.uka.ilkd.key.proof.event.ProofDisposedEvent;
@@ -43,7 +44,6 @@
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.lookup.Lookup;
 
-import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 
@@ -96,7 +96,7 @@ public class Proof implements ProofObject<Goal>, Named {
     /**
      * declarations &c, read from a problem file or otherwise
      */
-    private String problemHeader = "";
+    private KeyAst.@Nullable Declarations problemHeader = null;
 
     /**
      * the proof environment (optional)
@@ -136,7 +136,7 @@ public class Proof implements ProofObject<Goal>, Named {
 
     private long autoModeTime = 0;
 
-    private @Nullable Strategy<@NonNull Goal> activeStrategy;
+    private @Nullable Strategy<Goal> activeStrategy;
 
     private PropertyChangeListener settingsListener;
 
@@ -238,15 +238,17 @@ private Proof(String name, Sequent problem, TacletIndex rules, BuiltInRuleIndex
         }
     }
 
-    public Proof(String name, Sequent problem, String header, InitConfig initConfig,
+    public Proof(String name, Sequent problem, KeyAst.@Nullable Declarations header,
+            InitConfig initConfig,
             Path proofFile) {
         this(name, problem, initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(),
             initConfig);
         problemHeader = header;
         this.proofFile = proofFile;
     }
 
-    public Proof(String name, JTerm problem, String header, InitConfig initConfig) {
+    public Proof(String name, JTerm problem, KeyAst.@Nullable Declarations header,
+            InitConfig initConfig) {
         this(name,
             JavaDLSequentKit
                     .createSuccSequent(ImmutableSLList.singleton(new SequentFormula(problem))),
@@ -255,7 +257,8 @@ public Proof(String name, JTerm problem, String header, InitConfig initConfig) {
     }
 
 
-    public Proof(String name, Sequent sequent, String header, TacletIndex rules,
+    public Proof(String name, Sequent sequent, KeyAst.@Nullable Declarations header,
+            TacletIndex rules,
             BuiltInRuleIndex builtInRules, InitConfig initConfig) {
         this(name, sequent, rules, builtInRules, initConfig);
         problemHeader = header;
@@ -325,7 +328,7 @@ public Name name() {
     }
 
 
-    public String header() {
+    public KeyAst.@Nullable Declarations header() {
         return problemHeader;
     }
 
@@ -389,15 +392,15 @@ public AbbrevMap abbreviations() {
     }
 
 
-    public Strategy<@NonNull Goal> getActiveStrategy() {
+    public Strategy<Goal> getActiveStrategy() {
         if (activeStrategy == null) {
             initStrategy();
         }
         return activeStrategy;
     }
 
 
-    public void setActiveStrategy(Strategy<@NonNull Goal> activeStrategy) {
+    public void setActiveStrategy(Strategy<Goal> activeStrategy) {
         this.activeStrategy = activeStrategy;
         getSettings().getStrategySettings().setStrategy(activeStrategy.name());
         updateStrategyOnGoals();
@@ -409,7 +412,7 @@ public void setActiveStrategy(Strategy<@NonNull Goal> activeStrategy) {
 
 
     private void updateStrategyOnGoals() {
-        Strategy<@NonNull Goal> ourStrategy = getActiveStrategy();
+        Strategy<Goal> ourStrategy = getActiveStrategy();
 
         for (Goal goal : openGoals()) {
             goal.setGoalStrategy(ourStrategy);
@@ -776,7 +779,7 @@ public void breadthFirstSearch(Node startNode, ProofVisitor visitor) {
      * @param pred non-null test function
      * @return a node fulfilling {@code pred} or null
      */
-    public @Nullable Node findAny(@NonNull Predicate<Node> pred) {
+    public @Nullable Node findAny(Predicate<Node> pred) {
         Queue<Node> queue = new LinkedList<>();
         queue.add(root);
         while (!queue.isEmpty()) {
@@ -974,7 +977,7 @@ public boolean isOpenGoal(Node node) {
      *
      * @return the goal that belongs to the given node or null if the node is an inner one
      */
-    public Goal getOpenGoal(@NonNull Node node) {
+    public Goal getOpenGoal(Node node) {
         for (final Goal result : openGoals) {
             if (result.node() == node) {
                 return result;
@@ -1317,7 +1320,7 @@ public <T> void deregister(T obj, Class<T> service) {
      *
      * @return the associated lookup
      */
-    public @NonNull Lookup getUserData() {
+    public Lookup getUserData() {
         if (userData == null) {
             userData = new Lookup();
         }