Make user-defined sorts accessible in "\dl_" escapes

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

@@ -745,56 +745,61 @@ public EmptyMapLiteral convert(de.uka.ilkd.key.java.recoderext.adt.EmptyMapLiter
     }
 
     /**
-     * Resolve the function symbol which is embedded here to its logical counterpart.
+     * Resolve the function symbol with the given name. Also supports sort-dependent functions
+     * (where the name contains "::").
+     *
+     * @param name
+     * @param e
+     * @return
      */
-    public DLEmbeddedExpression convert(EscapeExpression e) {
-        final var PREFIX = "\\dl_DEFAULT_VALUE_";
-        final var DEFVALUE = "@defaultValue(";
-        ExtList children = collectChildren(e);
-        String name = e.getFunctionName();
+    private Function resolveFunction(String name, EscapeExpression e) {
+
+        final Function named = namespaceSet.functions().lookup(new Name(name));
+
+        if (named != null) {
+            // found a non-sort-depending function
+            return named;
+        }
 
-        if (name.startsWith(PREFIX)) { // handle default value resolution
-            String sortName = name.substring(PREFIX.length()).trim();
+        // check for sort-depending function
+        if (name.contains("::")) {
+            String sortName = name.substring(0, name.indexOf("::"));
+            String fName = name.substring(name.indexOf("::") + 2);
             Sort sort = namespaceSet.sorts().lookup(sortName);
+            if (!fName.equals("defaultValue")) {
+                // only defaultValue is supported here (for other names we should get an earlier
+                // parser error)
+                throw new ConvertException(format(
+                    "Requested to find the default value of a sort-dependent function '%s', "
+                        + "but the function name '%s' is not 'defaultValue'. Line/Col:%s",
+                    name, fName, e.getStartPosition()));
+            }
+
             if (sort == null) {
                 throw new ConvertException(format(
                     "Requested to find the default value of an unknown sort '%s'. " + "Line/Col:%s",
                     sortName, e.getStartPosition()));
             }
-
-            var doc = sort.getDocumentation();
-
-            if (doc == null) {
-                throw new ConvertException(
-                    format("Requested to find the default value for the sort '%s', "
-                        + "which does not have a documentary comment. The sort is defined at %s. "
-                        + "Line/Col: %s", sortName, sort.getOrigin(), e.getStartPosition()));
-            }
-
-            int pos = doc.indexOf(DEFVALUE);
-            if (pos >= 0) {
-                int start = doc.indexOf('(', pos) + 1;
-                int closing = doc.indexOf(')', pos);
-
-                if (closing < 0) {
-                    throw new ConvertException(format(
-                        "Forgotten closing parenthesis on @defaultValue annotation for sort '%s' in '%s'",
-                        sortName, sort.getOrigin()));
-                }
-
-                // set this as the function name, as the user had written \dl_XXX
-                name = doc.substring(start, closing);
+            SortDependingFunction firstInstance = SortDependingFunction.getFirstInstance(
+                new Name(fName), services);
+            if (firstInstance != null) {
+                return firstInstance.getInstanceFor(sort, services);
             } else {
-                throw new ConvertException(format(
-                    "Could not infer the default value for the given sort '%s'. "
-                        + "The sort found was as '%s' and the sort's documentation is '%s'. "
-                        + "Did you forget @defaultValue(XXX) in the documentation?Line/Col: %s",
-                    sortName, sort, doc, e.getStartPosition()));
+                return null;
             }
+        } else {
+            return null;
         }
+    }
 
+    /**
+     * Resolve the function symbol which is embedded here to its logical counterpart.
+     */
+    public DLEmbeddedExpression convert(EscapeExpression e) {
+        ExtList children = collectChildren(e);
+        String name = e.getFunctionName();
 
-        final Function named = namespaceSet.functions().lookup(new Name(name));
+        final Function named = resolveFunction(name, e);
 
         if (named == null) {
             // TODO provide position information?!

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

@@ -106,7 +106,9 @@ 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);
+        ProgramElementName pen = qualifier.isEmpty() ? new ProgramElementName(name)
+                : new ProgramElementName(name, qualifier);
+        TypeRef tr = new TypeRef(pen, 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/java/recoderext/RecoderModelTransformer.java

@@ -84,10 +84,9 @@ public Expression getDefaultValue(Type type) {
                 default -> {
                     if (type.getName().startsWith("\\dl_")) {
                         // The default value of a type is resolved later, then we know the Sort of
-                        // the
-                        // type
+                        // the type
                         yield new DLEmbeddedExpression(
-                            "\\dl_DEFAULT_VALUE_" + type.getName().substring(4),
+                            type.getName().substring(4) + "::defaultValue",
                             Collections.emptyList());
                     }
                     Debug.fail("makeImplicitMembersExplicit: unknown primitive type" + type);

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/proof/init/KeYUserProblemFile.java

@@ -102,7 +102,8 @@ public ImmutableSet<PositionedString> read() throws ProofInputException {
         ImmutableSet<PositionedString> warnings = DefaultImmutableSet.nil();
 
         // read key file itself (except contracts)
-        warnings = warnings.union(super.readExtendedSignature());
+        // should have been read earlier (TODO: find a clean solution)
+        // warnings = warnings.union(super.readExtendedSignature());
 
         // read in-code specifications
         SLEnvInput slEnvInput = new SLEnvInput(readJavaPath(), readClassPath(), readBootClassPath(),

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

@@ -523,6 +523,13 @@ private InitConfig prepare(EnvInput envInput, InitConfig referenceConfig)
 
         configureTermLabelSupport(initConfig);
 
+        // hacky, but allows to use sorts and functions from user .key files in JML via \dl_ escape
+        if (envInput instanceof KeYUserProblemFile kf) {
+            envInput.setInitConfig(initConfig);
+            // warnings.add(kf.readSorts());
+            warnings.add(kf.readExtendedSignature());
+        }
+
         // read Java
         readJava(envInput, initConfig);
 

key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java

@@ -0,0 +1,40 @@
+/* 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.speclang.njml;
+
+import java.nio.file.Files;
+import java.nio.file.Path;
+
+import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.init.ContractPO;
+import de.uka.ilkd.key.proof.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
+import de.uka.ilkd.key.speclang.Contract;
+import de.uka.ilkd.key.util.HelperClassForTests;
+
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.api.Assumptions;
+import org.junit.jupiter.api.Test;
+
+public class DLEscapeParsingTest {
+    @Test
+    public void dlEscapeParsingTest() throws ProblemLoaderException, ProofInputException {
+        final Path keyFile = HelperClassForTests.TESTCASE_DIRECTORY
+                .resolve("speclang/dlEscapeParsing/dlEscapeTest.key");
+        Assumptions.assumeTrue(Files.exists(keyFile));
+        KeYEnvironment<?> env = KeYEnvironment.load(keyFile);
+        // both contracts are provable automatically within a few steps
+        Contract contr = env.getProofContracts().getFirst();
+        ContractPO po1 = contr.createProofObl(env.getInitConfig());
+        Proof proof1 = env.createProof(po1);
+        env.getProofControl().startAndWaitForAutoMode(proof1);
+        Assertions.assertTrue(proof1.closed());
+
+        ContractPO po2 = contr.createProofObl(env.getInitConfig());
+        Proof proof2 = env.createProof(po2);
+        env.getProofControl().startAndWaitForAutoMode(proof2);
+        Assertions.assertTrue(proof2.closed());
+    }
+}

key.core/src/test/resources/testcase/speclang/dlEscapeParsing/IntTriple.java

@@ -0,0 +1,23 @@
+class IntTriple {
+    // abstract state
+    //@ ghost int x;
+    //@ ghost \dl_IntPair yz;                     // default value is needed here!
+    int a, b, c;        // concrete state
+
+
+    // coupling invariant
+    //@ invariant a == x && \dl_fst(yz) == b && \dl_snd(yz) == c;
+
+    //@ ensures yz == \dl_ip(0,0);      // (auto) provable
+    IntTriple() {
+    }
+
+    /*@ normal_behavior
+      @  requires true;
+      @  ensures \result == \dl_fst(yz);   // (auto) provable
+      @  assignable \nothing;
+      @*/
+    int getSecond() {
+        return b;
+    }
+}

key.core/src/test/resources/testcase/speclang/dlEscapeParsing/dlEscapeTest.key

@@ -0,0 +1,37 @@
+\sorts {
+    /*  ! @defaultValue(emptyPair) */    // <-- not needed anymore with this PR
+    IntPair;
+}
+
+\functions {
+    // IntPair emptyPair;              // <-- not needed anymore with this PR
+    \unique IntPair ip(int, int);   // constructor
+    int fst(IntPair);               // selector function
+    int snd(IntPair);               // selector function
+}
+
+\rules {
+    defaultValueOfIntPair {
+        \find (IntPair::defaultValue)
+        \replacewith (ip(0,0))
+        \heuristics(simplify)
+    };
+
+    fstOfIp {
+        \schemaVar \term int a, b;
+        \find (fst(ip(a, b)))
+        \replacewith (a)
+        \heuristics(simplify)
+    };
+
+    sndOfIp {
+        \schemaVar \term int a, b;
+        \find (snd(ip(a, b)))
+        \replacewith (b)
+        \heuristics(simplify)
+    };
+}
+
+\javaSource ".";
+
+\chooseContract