From 9e3a2200797e3fa837f97d42b80f5dc3489be02c Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 11 Sep 2025 18:54:54 +0200 Subject: [PATCH 1/6] hack to allow user-defined sorts from .key file in JML via dl escape --- .../de/uka/ilkd/key/proof/init/KeYUserProblemFile.java | 3 ++- .../de/uka/ilkd/key/proof/init/ProblemInitializer.java | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 7e9e1fe64b9..2ecc45be5b4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -102,7 +102,8 @@ public ImmutableSet read() throws ProofInputException { ImmutableSet 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(), diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index f8138c31c75..39879c4ab57 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/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 KeYFile kf) { + envInput.setInitConfig(initConfig); + //warnings.add(kf.readSorts()); + warnings.add(kf.readExtendedSignature()); + } + // read Java readJava(envInput, initConfig); From 154e55b57228bd94cdc8f2f4ade098e6faf411d9 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 12 Sep 2025 18:40:52 +0200 Subject: [PATCH 2/6] use logical symbol instead of doc comment for default value of user defined sort --- .../ilkd/key/java/Recoder2KeYConverter.java | 78 ++++++++++--------- .../recoderext/RecoderModelTransformer.java | 5 +- 2 files changed, 43 insertions(+), 40 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 02cb218f130..7a975930ffa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -745,56 +745,60 @@ 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?! diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java index 7aae7cf4448..e1def4169e3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java +++ b/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); From 93034983457d397469c4f55bb0542ff56c349a08 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 29 Oct 2025 14:54:09 +0100 Subject: [PATCH 3/6] new test case for user-def. sorts in dl escape, fix assertion error --- .../operator/DLEmbeddedExpression.java | 4 +- .../speclang/njml/DLEscapeParsingTest.java | 34 +++++++++++++++++ .../speclang/dlEscapeParsing/IntTriple.java | 23 ++++++++++++ .../speclang/dlEscapeParsing/dlEscapeTest.key | 37 +++++++++++++++++++ 4 files changed, 97 insertions(+), 1 deletion(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java create mode 100644 key.core/src/test/resources/testcase/speclang/dlEscapeParsing/IntTriple.java create mode 100644 key.core/src/test/resources/testcase/speclang/dlEscapeParsing/dlEscapeTest.key diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java index 6821c7a8efa..cbe2eaae0cf 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java +++ b/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++) { diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java new file mode 100644 index 00000000000..31d47396e14 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java @@ -0,0 +1,34 @@ +package de.uka.ilkd.key.speclang.njml; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.java.Services; +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; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.io.File; +import java.nio.file.Files; +import java.nio.file.Path; + +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); + Contract contr = env.getProofContracts().getFirst(); + ContractPO po = contr.createProofObl(env.getInitConfig()); + Proof proof = env.createProof(po); + env.getProofControl().startAndWaitForAutoMode(proof); + Assertions.assertTrue(proof.closed()); + } +} diff --git a/key.core/src/test/resources/testcase/speclang/dlEscapeParsing/IntTriple.java b/key.core/src/test/resources/testcase/speclang/dlEscapeParsing/IntTriple.java new file mode 100644 index 00000000000..7e9d384a8c5 --- /dev/null +++ b/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; + } +} diff --git a/key.core/src/test/resources/testcase/speclang/dlEscapeParsing/dlEscapeTest.key b/key.core/src/test/resources/testcase/speclang/dlEscapeParsing/dlEscapeTest.key new file mode 100644 index 00000000000..2e7ee1ecfc7 --- /dev/null +++ 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 From bc81409eec3a85cdc0366aba9feb906ebbe0a2f2 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 29 Oct 2025 15:50:45 +0100 Subject: [PATCH 4/6] removed assertion that seems unnecessary and makes test case fail, extended test case --- .../java/de/uka/ilkd/key/ldt/JavaDLTheory.java | 1 - .../key/speclang/njml/DLEscapeParsingTest.java | 18 ++++++++++-------- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java b/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java index 404a945b60e..07666941c70 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/ldt/JavaDLTheory.java +++ b/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; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java index 31d47396e14..5608ac4ed8a 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java @@ -1,7 +1,6 @@ package de.uka.ilkd.key.speclang.njml; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ContractPO; import de.uka.ilkd.key.proof.init.ProofInputException; @@ -11,10 +10,7 @@ import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.Test; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; -import java.io.File; import java.nio.file.Files; import java.nio.file.Path; @@ -25,10 +21,16 @@ public void dlEscapeParsingTest() throws ProblemLoaderException, ProofInputExcep .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 po = contr.createProofObl(env.getInitConfig()); - Proof proof = env.createProof(po); - env.getProofControl().startAndWaitForAutoMode(proof); - Assertions.assertTrue(proof.closed()); + 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()); } } From efa67a78b651d0a10c565e0d27bfb4918c46919c Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 5 Nov 2025 19:02:53 +0100 Subject: [PATCH 5/6] trying to fix test failures --- .../java/de/uka/ilkd/key/proof/init/ProblemInitializer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index 39879c4ab57..bbc9cb9440d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -524,7 +524,7 @@ 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 KeYFile kf) { + if (envInput instanceof KeYUserProblemFile kf) { envInput.setInitConfig(initConfig); //warnings.add(kf.readSorts()); warnings.add(kf.readExtendedSignature()); From 9f47079be82c3b4325fa61cf8894ce5a09c952b9 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 5 Nov 2025 19:09:02 +0100 Subject: [PATCH 6/6] formatting --- .../de/uka/ilkd/key/java/Recoder2KeYConverter.java | 1 + .../java/expression/operator/DLEmbeddedExpression.java | 2 +- .../de/uka/ilkd/key/proof/init/KeYUserProblemFile.java | 2 +- .../de/uka/ilkd/key/proof/init/ProblemInitializer.java | 2 +- .../ilkd/key/speclang/njml/DLEscapeParsingTest.java | 10 +++++++--- 5 files changed, 11 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java index 7a975930ffa..71d2a859238 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java @@ -747,6 +747,7 @@ public EmptyMapLiteral convert(de.uka.ilkd.key.java.recoderext.adt.EmptyMapLiter /** * Resolve the function symbol with the given name. Also supports sort-dependent functions * (where the name contains "::"). + * * @param name * @param e * @return diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java index cbe2eaae0cf..b84c687985c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java @@ -107,7 +107,7 @@ public void check(Services javaServ, KeYJavaType containingClass) throws Convert name.lastIndexOf('.') != -1 ? name.substring(0, name.lastIndexOf('.')) : ""; name = name.substring(name.lastIndexOf('.') + 1); ProgramElementName pen = qualifier.isEmpty() ? new ProgramElementName(name) - : new ProgramElementName(name, qualifier); + : new ProgramElementName(name, qualifier); TypeRef tr = new TypeRef(pen, 0, null, containingClass); ExecutionContext ec = new ExecutionContext(tr, null, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 2ecc45be5b4..80cf720d415 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -103,7 +103,7 @@ public ImmutableSet read() throws ProofInputException { // read key file itself (except contracts) // should have been read earlier (TODO: find a clean solution) - //warnings = warnings.union(super.readExtendedSignature()); + // warnings = warnings.union(super.readExtendedSignature()); // read in-code specifications SLEnvInput slEnvInput = new SLEnvInput(readJavaPath(), readClassPath(), readBootClassPath(), diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java index bbc9cb9440d..ce1dd8abffb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java @@ -526,7 +526,7 @@ private InitConfig prepare(EnvInput envInput, InitConfig referenceConfig) // 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.readSorts()); warnings.add(kf.readExtendedSignature()); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java index 5608ac4ed8a..87555c0304c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/njml/DLEscapeParsingTest.java @@ -1,5 +1,11 @@ +/* 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; @@ -7,13 +13,11 @@ 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; -import java.nio.file.Files; -import java.nio.file.Path; - public class DLEscapeParsingTest { @Test public void dlEscapeParsingTest() throws ProblemLoaderException, ProofInputException {