Proof obligation loading does not work with Java source and custom function/predicate symbols

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

Description

This is the bug report created for !295.

Reproducible

always

Steps to reproduce

1. Try to load the following .key file from x.zip (example from (at)mulbrich):

   \javaSource ".";
   
   \functions { int func; }
   
   \rules {
     func42 { \find(func) \replacewith(42) };
   }
   
   \chooseContract
   

   The corresponding Java and JML is:

   class x {
   
       //@ ensures \dl_func() == 42;
       void m() { }
   }

The file is not loadable, an exception is shown that the symbol func is not known (see stacktrace below).

As indicated in the original discussion in https://git.key-project.org/key/key/-/merge_requests/295#note_14650, the problem is the loading order of Java and EnvInput (i.e., .key file).
However, the loading process in KeY is quite complex, in particular due to Recoder legacy. Since we still hope to replace Recoder in the (reasonably near) future by the combined Java+JML parser (javaparser project), we should do that first.

Additional information

Stacktrace when trying to load the above example (shortened):

java.lang.RuntimeException: de.uka.ilkd.key.speclang.translation.SLTranslationException: Unknown escaped symbol func
	at de.uka.ilkd.key.speclang.translation.SLExceptionFactory.createException0(SLExceptionFactory.java:229)
	at de.uka.ilkd.key.speclang.njml.JmlTermFactory.translateToJDLTerm(JmlTermFactory.java:1373)
	at de.uka.ilkd.key.speclang.njml.JmlTermFactory.dlKeyword(JmlTermFactory.java:533)
	at de.uka.ilkd.key.speclang.njml.Translator.visitPrimarySuffixCall(Translator.java:963)
	at de.uka.ilkd.key.speclang.njml.JmlParser$PrimarySuffixCallContext.accept(JmlParser.java:8699)
	at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:125)
	at de.uka.ilkd.key.speclang.njml.Translator.visitPostfixexpr(Translator.java:822)
	at de.uka.ilkd.key.speclang.njml.Translator.visitPostfixexpr(Translator.java:57)
	at de.uka.ilkd.key.speclang.njml.JmlParser$PostfixexprContext.accept(JmlParser.java:8049)
	at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:125)
	at de.uka.ilkd.key.speclang.njml.Translator.visitUnaryexprnotplusminus(Translator.java:804)
	at de.uka.ilkd.key.speclang.njml.JmlParser$UnaryexprnotplusminusContext.accept(JmlParser.java:7896)
	at de.uka.ilkd.key.speclang.njml.Translator.accept(Translator.java:125)
	at de.uka.ilkd.key.speclang.njml.Translator.oneOf(Translator.java:142)
	at de.uka.ilkd.key.speclang.njml.Translator.visitUnaryexpr(Translator.java:767)
...
	at de.uka.ilkd.key.speclang.njml.JmlIO.translateTerm(JmlIO.java:211)
	at de.uka.ilkd.key.speclang.njml.JmlIO.translateTerm(JmlIO.java:236)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateAndClauses(JMLSpecFactory.java:599)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateEnsures(JMLSpecFactory.java:749)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateEnsures(JMLSpecFactory.java:452)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.translateJMLClauses(JMLSpecFactory.java:377)
	at de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory.createJMLOperationContracts(JMLSpecFactory.java:1250)
	at de.uka.ilkd.key.speclang.jml.JMLSpecExtractor.extractMethodSpecs(JMLSpecExtractor.java:506)
	at de.uka.ilkd.key.speclang.SLEnvInput.createSpecs(SLEnvInput.java:337)
	at de.uka.ilkd.key.speclang.SLEnvInput.read(SLEnvInput.java:386)
	at de.uka.ilkd.key.proof.init.KeYUserProblemFile.read(KeYUserProblemFile.java:129)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.readEnvInput(ProblemInitializer.java:360)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:605)
	at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:489)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:522)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:293)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:258)
	at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:80)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:137)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:130)
	at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:304)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
	at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:343)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
	at java.base/java.lang.Thread.run(Thread.java:833)
Caused by: de.uka.ilkd.key.speclang.translation.SLTranslationException: Unknown escaped symbol func
	at de.uka.ilkd.key.speclang.translation.SLExceptionFactory.createException(SLExceptionFactory.java:203)
	... 146 more

---

• Commit: aeefa0b6c76e6516cce2c0507cfa8cc9ada29544

---

Information:

• created_at: 2021-11-04T19:00:45.313Z
• updated_at: 2021-11-08T22:12:43.544Z
• closed_at: None (closed_by: )
• milestone: v2.14.0
• user_notes_count: 2

[FliegendeWurst]

It seems this issue was fixed in the meantime. At least the provided example works for me.

[WolframPfeifer]

It seems this issue was fixed in the meantime. At least the provided example works for me.

Thanks for checking. I also used this recently and can confirm that it works on the current main branch for functions. For sorts, it is more difficult due to possible cyclic dependencies (see #3659). However, I think we can close this issue here.