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..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 @@ -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?! 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..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 @@ -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/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); 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/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..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 @@ -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..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 @@ -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); 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..87555c0304c --- /dev/null +++ b/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()); + } +} 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