Fix #3452 (#3540)

Author: mattulbrich

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<Contract> 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<KeYJavaType> kjts = currentEnv.getJavaInfo().getAllKeYJavaTypes();
-        for (KeYJavaType type : kjts) {
-            if (!KeYTypeUtil.isLibraryClass(type)) {
-                ImmutableSet<IObserverFunction> targets =
-                    currentEnv.getSpecificationRepository().getContractTargets(type);
-                for (IObserverFunction target : targets) {
-                    ImmutableSet<Contract> contracts =
-                        currentEnv.getSpecificationRepository().getContracts(type, target);
-                    for (Contract contract : contracts) {
-                        proofContracts.add(contract);
-                    }
-                }
-            }
-        }
+        return currentEnv.getProofContracts();
     }
 
     /**

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<Contract> getProofContracts() {
+        var proofContracts = new ArrayList<Contract>();
+        Set<KeYJavaType> kjts = getJavaInfo().getAllKeYJavaTypes();
+        for (KeYJavaType type : kjts) {
+            if (!KeYTypeUtil.isLibraryClass(type)) {
+                ImmutableSet<IObserverFunction> targets =
+                    getSpecificationRepository().getContractTargets(type);
+                for (IObserverFunction target : targets) {
+                    ImmutableSet<Contract> contracts =
+                        getSpecificationRepository().getContracts(type, target);
+                    for (Contract contract : contracts) {
+                        proofContracts.add(contract);
+                    }
+                }
+            }
+        }
+        return proofContracts;
+    }
 }

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;
+
 /**
  * <p>
  * 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<LocationVariable> paramVars,
-            final LocationVariable resultVar, final List<LocationVariable> modifiableHeaps,
-            final Map<LocationVariable, LocationVariable> 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<LocationVariable> paramVars,
+            LocationVariable resultVar, List<LocationVariable> modifiableHeaps,
+            Map<LocationVariable, LocationVariable> 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<LocationVariable> 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<FunctionalOperationContract> collectLookupContracts(
         return lookupContracts;
     }
 
-    private Term getRepresentsFromContract(final IProgramMethod pm, final LocationVariable selfVar,
+    private @Nullable Term getRepresentsFromContract(final IProgramMethod pm,
+            final LocationVariable selfVar,
             final ImmutableList<LocationVariable> paramVars, final LocationVariable resultVar,
             final List<LocationVariable> heaps,
             final Map<LocationVariable, LocationVariable> atPreVars, final Services proofServices) {
         ImmutableList<FunctionalOperationContract> 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);
     }

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<LocationVariable> modifiableHeaps,
+    protected @Nullable Term buildFrameClause(List<LocationVariable> modifiableHeaps,
             Map<Term, Term> heapToAtPre, LocationVariable selfVar,
             ImmutableList<LocationVariable> paramVars, Services services) {
         Term frameTerm = null;

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;
     }

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);
     }
 

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<Term> 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;
+    }
+}

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<JFunction> 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());
+        }
+    }
+}

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);
+    }
+
+}

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;
+
+}