Fix deadlock when showing JML warnings dialog

[FliegendeWurst]

Intended Change

It seems this method is called on the worker thread, which may lead to a deadlock when creating the dialog.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)

Ensuring quality

• I have tested the feature as follows: loaded a file with JML warnings (specifically, missing decreases). Now works fine, previously it got stuck on "Reading project.key".

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 47.99%. Comparing base (1c76f67) to head (8a479c2).
⚠️ Report is 4 commits behind head on main.

Additional details and impacted files

@@            Coverage Diff            @@
##               main    #3692   +/-   ##
=========================================
  Coverage     47.99%   47.99%           
  Complexity    16044    16044           
=========================================
  Files          1683     1683           
  Lines         96044    96044           
  Branches      15387    15387           
=========================================
  Hits          46093    46093           
  Misses        44681    44681           
  Partials       5270     5270           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

[wadoon]

I would say, that this is not the patch we would want in just a case.

Could you provide a stack trace showing the location from which the method is invoked?

[FliegendeWurst]

Sure, here you go:

showWarningsIfNecessary:580, IssueDialog (de.uka.ilkd.key.gui)
reportWarnings:595, WindowUserInterfaceControl (de.uka.ilkd.key.gui)
loadEnvironment:309, AbstractProblemLoader (de.uka.ilkd.key.proof.io)
load:268, AbstractProblemLoader (de.uka.ilkd.key.proof.io)
doWork:75, ProblemLoader (de.uka.ilkd.key.proof.io)
doInBackground:125, ProblemLoader$1 (de.uka.ilkd.key.proof.io)
4 hidden frames
 - Async stack trace
2 hidden frames
<init>:118, ProblemLoader$1 (de.uka.ilkd.key.proof.io)
runAsynchronously:118, ProblemLoader (de.uka.ilkd.key.proof.io)
loadProblem:109, WindowUserInterfaceControl (de.uka.ilkd.key.gui)
loadProblem:114, WindowUserInterfaceControl (de.uka.ilkd.key.gui)
loadProblem:1400, MainWindow (de.uka.ilkd.key.gui)
actionPerformed:61, OpenFileAction (de.uka.ilkd.key.gui.actions)
49 hidden frames

[wadoon]

I would say the responsibility for EDT is in WindowUserInterfaceControl#reportWarnings. This would be my patch.

diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
index 8f738947e8..5ab4910923 100644
--- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
+++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
@@ -592,7 +592,9 @@ public class WindowUserInterfaceControl extends AbstractMediatorUserInterfaceCon
 
     @Override
     public void reportWarnings(ImmutableSet<PositionedString> warnings) {
-        IssueDialog.showWarningsIfNecessary(mainWindow, warnings);
+        SwingUtilities.invokeLater(() ->
+            IssueDialog.showWarningsIfNecessary(mainWindow, warnings)
+        );
     }
 
     /**

[FliegendeWurst]

Now the warnings dialog will be shown in parallel to the contract chooser, which is a bit odd.

[WolframPfeifer]

Now the warnings dialog will be shown in parallel to the contract chooser, which is a bit odd.

In our meeting, we agreed that this is very difficult to prevent (probably involves writing a class that has an explicit queue of dialogs to show), so we decided to ignore that for the moment.
Thanks, @FliegendeWurst and @wadoon.

Review was supposed to accept, not to request change ;-)

[WolframPfeifer]

Now the warnings dialog will be shown in parallel to the contract chooser, which is a bit odd.

In our meeting, we decided to ignore that shortcoming, since a fix would be difficult (probably requires writing a class that keeps an explicit queue of dialogs to show).

Thanks, @FliegendeWurst and @wadoon!