diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/ProofManagementApi.java b/key.core/src/main/java/de/uka/ilkd/key/api/ProofManagementApi.java index 6ef8191acf3..ace01461c55 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/api/ProofManagementApi.java +++ b/key.core/src/main/java/de/uka/ilkd/key/api/ProofManagementApi.java @@ -10,14 +10,10 @@ import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.java.abstraction.KeYJavaType; -import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.init.ProofOblInput; import de.uka.ilkd.key.speclang.Contract; -import de.uka.ilkd.key.util.KeYTypeUtil; -import org.key_project.util.collection.ImmutableSet; /** * This class serves as a facade to all functionalities that are needed for proof management, i.e., @@ -45,31 +41,7 @@ public Services getServices() { * exception here) */ public List getProofContracts() { - if (proofContracts.isEmpty()) { - buildContracts(); - } - return proofContracts; - } - - /** - * constructs the possible proof contracts from the java info in the environment. - */ - private void buildContracts() { - proofContracts.clear(); - Set kjts = currentEnv.getJavaInfo().getAllKeYJavaTypes(); - for (KeYJavaType type : kjts) { - if (!KeYTypeUtil.isLibraryClass(type)) { - ImmutableSet targets = - currentEnv.getSpecificationRepository().getContractTargets(type); - for (IObserverFunction target : targets) { - ImmutableSet contracts = - currentEnv.getSpecificationRepository().getContracts(type, target); - for (Contract contract : contracts) { - proofContracts.add(contract); - } - } - } - } + return currentEnv.getProofContracts(); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java index bc34b6eaf8a..f037dbe6482 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java @@ -4,12 +4,16 @@ package de.uka.ilkd.key.control; import java.io.File; +import java.util.ArrayList; import java.util.List; import java.util.Properties; +import java.util.Set; import java.util.function.Consumer; import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.abstraction.KeYJavaType; +import de.uka.ilkd.key.logic.op.IObserverFunction; import de.uka.ilkd.key.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.InitConfig; @@ -20,6 +24,10 @@ import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; +import de.uka.ilkd.key.speclang.Contract; +import de.uka.ilkd.key.util.KeYTypeUtil; + +import org.key_project.util.collection.ImmutableSet; import org.jspecify.annotations.Nullable; @@ -320,4 +328,26 @@ public boolean isDisposed() { public @Nullable ProofScriptEntry getProofScript() { return proofScript; } + + /** + * constructs the possible proof contracts from the java info in the environment. + */ + public List getProofContracts() { + var proofContracts = new ArrayList(); + Set kjts = getJavaInfo().getAllKeYJavaTypes(); + for (KeYJavaType type : kjts) { + if (!KeYTypeUtil.isLibraryClass(type)) { + ImmutableSet targets = + getSpecificationRepository().getContractTargets(type); + for (IObserverFunction target : targets) { + ImmutableSet contracts = + getSpecificationRepository().getContracts(type, target); + for (Contract contract : contracts) { + proofContracts.add(contract); + } + } + } + } + return proofContracts; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java index 2fd28490a66..35666caaf25 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java @@ -37,6 +37,8 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.Nullable; + /** *

* This abstract implementation of {@link ProofOblInput} extends the functionality of @@ -353,26 +355,29 @@ private static Term addTransactionPrecondition(Term pre, boolean transactionFlag return pre; } - private static Term createProgPost(final IObserverFunction target, - final LocationVariable selfVar, final ImmutableList paramVars, - final LocationVariable resultVar, final List modifiableHeaps, - final Map atPreVars, final Term saveBeforeHeaps, - final Term representsFromContract, final Term post, final TermBuilder tb) { - final Term progPost; + private static Term createProgPost(IObserverFunction target, + LocationVariable selfVar, ImmutableList paramVars, + LocationVariable resultVar, List modifiableHeaps, + Map atPreVars, Term saveBeforeHeaps, + @Nullable Term representsFromContract, Term post, TermBuilder tb) { if (representsFromContract == null) { final Term[] updateSubs = createUpdateSubs(target, selfVar, paramVars, modifiableHeaps, atPreVars, tb); - progPost = tb.apply(saveBeforeHeaps, - tb.apply(tb.elementary(tb.var(resultVar), tb.func(target, updateSubs)), post)); + var term = + tb.apply(tb.elementary(tb.var(resultVar), tb.func(target, updateSubs)), post); + if (saveBeforeHeaps == null) { // null on no_state methods + return term; + } else { + return tb.apply(saveBeforeHeaps, term); + } } else { final Term body = representsFromContract; assert body.op() == Equality.EQUALS : "Only fully functional represents clauses for model" + " methods are supported!"; - progPost = tb.apply(saveBeforeHeaps, + return tb.apply(saveBeforeHeaps, tb.apply(tb.elementary(tb.var(resultVar), body.sub(1)), post)); } - return progPost; } /** @@ -789,7 +794,7 @@ protected Term createUninterpretedPredicate(ImmutableList form /** * Builds the frame clause including the modifiable clause. * - * @param modifiableHeaps The heaps. + * @param modifiableHeaps a non-empty list of heaps variables * @param heapToAtPre The previous heap before execution. * @param selfVar The self variable. * @param paramVars The parameters {@link ProgramVariable}s. @@ -1026,13 +1031,19 @@ private ImmutableList collectLookupContracts( return lookupContracts; } - private Term getRepresentsFromContract(final IProgramMethod pm, final LocationVariable selfVar, + private @Nullable Term getRepresentsFromContract(final IProgramMethod pm, + final LocationVariable selfVar, final ImmutableList paramVars, final LocationVariable resultVar, final List heaps, final Map atPreVars, final Services proofServices) { ImmutableList lookupContracts = collectLookupContracts(pm, proofServices); Term representsFromContract = null; + + if (heaps.isEmpty()) { + return null; // represents not possible on `no_state` model methods. + } + for (FunctionalOperationContract fop : lookupContracts) { representsFromContract = fop.getRepresentsAxiom(heaps.get(0), selfVar, paramVars, resultVar, atPreVars, proofServices); @@ -1085,6 +1096,11 @@ private Term createPost(final LocationVariable selfVar, formalParamVars, exceptionVar, getUninterpretedPredicateName(), proofServices)); } + if (heaps.isEmpty()) { + // happens in cases of `no_state` model methods, than no heap can be modified. + return postTerm; + } + Term frameTerm = buildFrameClause(heaps, heapToBefore, selfVar, paramVars, proofServices); return tb.and(postTerm, frameTerm); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java index 22b80db8c9e..f2705d85f62 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java @@ -35,6 +35,7 @@ import org.key_project.util.collection.ImmutableSLList; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.java.KeYJavaASTFactory.declare; @@ -228,7 +229,7 @@ protected Term getGlobalDefs(LocationVariable heap, Term heapTerm, Term selfTerm * {@inheritDoc} */ @Override - protected Term buildFrameClause(List modifiableHeaps, + protected @Nullable Term buildFrameClause(List modifiableHeaps, Map heapToAtPre, LocationVariable selfVar, ImmutableList paramVars, Services services) { Term frameTerm = null; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java index 18f5c3ba079..6a05195e46d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java @@ -419,9 +419,13 @@ private Term functionalRepresentsSatisfiability(IObserverFunction target, TermSe for (SchemaVariable paramSV : paramSVs) { tacletBuilder.addVarsNotFreeIn(targetSV, paramSV); } - axiomSatisfiable = - TB.ex(targetSV, TB.and(targetSVReachable, OpReplacer.replace(targetTerm, - TB.var(targetSV), schemaRepresents.term, services.getTermFactory()))); + final var replaced = OpReplacer.replace(targetTerm, + TB.var(targetSV), schemaRepresents.term, services.getTermFactory()); + if (targetSVReachable == null) { // no heaps are given e.g. no_state method + axiomSatisfiable = TB.ex(targetSV, replaced); + } else { + axiomSatisfiable = TB.ex(targetSV, TB.and(targetSVReachable, replaced)); + } } return axiomSatisfiable; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java index 83548cb6e20..a391d7e343d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java @@ -34,6 +34,7 @@ import de.uka.ilkd.key.speclang.translation.SLParameters; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.util.InfFlowSpec; +import de.uka.ilkd.key.util.TermUtil; import de.uka.ilkd.key.util.mergerule.MergeParamsSpec; import de.uka.ilkd.key.util.parsing.BuildingException; @@ -2366,6 +2367,16 @@ public SLExpression visitMethod_declaration(JmlParser.Method_declarationContext SLParameters params = visitParameters(ctx.param_list()); SLExpression apply = lookupIdentifier(ctx.IDENT().getText(), null, params, ctx); + var forbiddenHeapVar = services.getTypeConverter().getHeapLDT().getHeap(); + boolean applyContainsHeap = TermUtil.contains(apply.getTerm(), forbiddenHeapVar); + boolean bodyContainsHeap = TermUtil.contains(body.getTerm(), forbiddenHeapVar); + + + if (!applyContainsHeap && bodyContainsHeap) { + // NOT (no heap in applies --> no heap in body) + raiseError(ctx, "Heap used in a `no_state` method."); + } + return termFactory.eq(apply, body); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/TermUtil.java b/key.core/src/main/java/de/uka/ilkd/key/util/TermUtil.java new file mode 100644 index 00000000000..9de8f491c5e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/util/TermUtil.java @@ -0,0 +1,44 @@ +/* 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.util; + +import java.util.LinkedList; +import java.util.Queue; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.Operator; + +import org.jspecify.annotations.NonNull; + +/** + * @author Alexander Weigl + * @version 1 (06.02.25) + */ +public class TermUtil { + + /** + * Checks if a given term contains a specific operator. + * + * This method performs a breadth-first search on the term's subterms to find + * the specified operator. + * + * Caveat: It does not return true if op (only) occurs as the target of an update in term. + * + * @param term the term to be checked + * @param op the operator to search for + * @return true if the term or any of its subterms contains the operator, false otherwise + */ + public static boolean contains(@NonNull Term term, @NonNull Operator op) { + Queue queue = new LinkedList<>(); + queue.add(term); + while (!queue.isEmpty()) { + Term current = queue.poll(); + if (current.op() == op) { + return true; + } + queue.addAll(current.subs().toList()); + } + return false; + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/nparser/Issue3452Test.java b/key.core/src/test/java/de/uka/ilkd/key/nparser/Issue3452Test.java new file mode 100644 index 00000000000..4df4b62cef0 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/nparser/Issue3452Test.java @@ -0,0 +1,57 @@ +/* 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.nparser; + +import java.io.File; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.Namespace; +import de.uka.ilkd.key.logic.op.JFunction; +import de.uka.ilkd.key.proof.init.ProofInputException; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +/** + * @author Alexander Weigl + * @version 1 (31.01.25) + */ +public class Issue3452Test { + + + @Test + void testNoStateParsedCorrectly() throws ProblemLoaderException, ProofInputException { + final var input = + new File( + "src/test/resources/de/uka/ilkd/key/nparser/fix3452/fix/Issue3452Fixture.java"); + var env = KeYEnvironment.load(input, null, null, null); + final var contract = env.getProofContracts().getFirst(); + var po = contract.createProofObl(env.getInitConfig(), contract); + var proof = env.createProof(po); // just to ensure there is exception + Services services = proof.getInitConfig().getServices(); + Namespace functions = services.getNamespaces().functions(); + assertEquals("[int]", functions.lookup("A::b").argSorts().toString()); + assertEquals("[Heap,int]", functions.lookup("A::c").argSorts().toString()); + } + + @Test + void testIllegalNoState() throws ProblemLoaderException, ProofInputException { + final var input = + new File( + "src/test/resources/de/uka/ilkd/key/nparser/fix3452/problem/Issue3452IllegalNoState.java"); + + ProblemLoaderException exception = assertThrows(ProblemLoaderException.class, () -> { + var env = KeYEnvironment.load(input, null, null, null); + System.err.println(env); + System.err.println("Unexpected load success"); + }); + + if (!exception.getMessage().startsWith("Heap used in a `no_state` method.")) { + fail("Unexpected exception message: " + exception.getMessage()); + } + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/fix/Issue3452Fixture.java b/key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/fix/Issue3452Fixture.java new file mode 100644 index 00000000000..df9ec946986 --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/fix/Issue3452Fixture.java @@ -0,0 +1,30 @@ +class A { + /*@ public model_behaviour + @ requires n >= 0; + @ ensures \result.length == n; + @ measured_by n; + @ public no_state static model \seq b(\bigint n) { + @ return n == 0 ? \seq_empty : \seq_concat(b(n-1), \seq(0)); + @ } + @*/ + + /*@ public model_behaviour + @ requires n >= 0; + @ ensures \result.length == n; + @ accessible \nothing; + @ measured_by n; + @ public static model \seq c(\bigint n) { + @ return n == 0 ? \seq_empty : \seq_concat(c(n-1), \seq(0)); + @ } + @*/ + + int someHeapField; + + //@ ensures true; + void m() { + //@ ghost \seq x = c(5); + someHeapField = 42; + //@ assert x == c(5); + } + +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/problem/Issue3452IllegalNoState.java b/key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/problem/Issue3452IllegalNoState.java new file mode 100644 index 00000000000..254c2e2b37e --- /dev/null +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/fix3452/problem/Issue3452IllegalNoState.java @@ -0,0 +1,10 @@ +class A { + + /*@ public static no_state model int obs() { + @ return A.someHeapField; + @ } + @*/ + + static int someHeapField; + +}