Fix various UI bugs (#3216)

I recommend reviewing this PR commit-by-commit. Most of the bugs were
found using the new UI testing facility
(3d73e59).

Fixes #3228, #3227, #3215, #1648,
#1652 (comment),
#1526, #1117 and task 1+4 of #3214

.github/workflows/code_quality.yml

@@ -6,7 +6,7 @@ on:
   push:
     branches:
       - main
-      - 'releases/*'
+      - 'KeY-*'
 
 jobs:
   qodana:

.github/workflows/codeql.yml

@@ -4,8 +4,9 @@ on:
   push:
     branches: [ "main" ]
   pull_request:
-    # The branches below must be a subset of the branches above
-    branches: [ "main" ]
+    branches:
+      - "main"
+      - "KeY-*"
   schedule:
     - cron: '21 21 * * 4'
   merge_group:

.github/workflows/javadoc.yml

@@ -6,7 +6,6 @@ on:
 
 jobs:
   doc:
-    # later limit to master only!
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3

.github/workflows/tests.yml

@@ -5,7 +5,9 @@ on:
   push:
     branches: [ "main" ]
   pull_request:
-    branches: [ "main" ]
+    branches:
+      - "main"
+      - "KeY-*"
   merge_group:
 
 permissions:

LICENSE.TXT

@@ -27,8 +27,8 @@
        Sweden
 
 
-       WWW: http://key-project.org
-       e-mail: key@ira.uka.de	
+       WWW: https://www.key-project.org/
+       e-mail: support@key-project.org
 
        The KeY system is protected by the GNU General Public License.
 

key.core/build.gradle

@@ -100,6 +100,7 @@ task generateSolverPropsList {
                 list.add(file.name)
             }
         })
+        list.sort()
         if (!file("$outputDir/$pack/solvers.txt").exists()) {
             String files = ''
             for (String propsFile : list) {

key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java

@@ -237,6 +237,15 @@ private Proof(String name, Sequent problem, TacletIndex rules, BuiltInRuleIndex
         }
     }
 
+    public Proof(String name, Term problem, String header, InitConfig initConfig, File proofFile) {
+        this(name,
+            Sequent.createSuccSequent(
+                Semisequent.EMPTY_SEMISEQUENT.insert(0, new SequentFormula(problem)).semisequent()),
+            initConfig.createTacletIndex(), initConfig.createBuiltInRuleIndex(), initConfig);
+        problemHeader = header;
+        this.proofFile = proofFile;
+    }
+
     public Proof(String name, Term problem, String header, InitConfig initConfig) {
         this(name,
             Sequent.createSuccSequent(

key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java

@@ -162,7 +162,8 @@ public ProofAggregate getPO() throws ProofInputException {
         ProofSettings settings = getPreferences();
         initConfig.setSettings(settings);
         return ProofAggregate.createProofAggregate(
-            new Proof(name, problemTerm, getParseContext().getProblemHeader() + "\n", initConfig),
+            new Proof(name, problemTerm, getParseContext().getProblemHeader() + "\n", initConfig,
+                file.file()),
             name);
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java

@@ -14,6 +14,7 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.rule.NoPosTacletApp;
 import de.uka.ilkd.key.rule.merge.CloseAfterMerge;
 
 /**
@@ -39,12 +40,35 @@ public static ClosedBy findPreviousProof(DefaultListModel<Proof> previousProofs,
         if (!suitableForCloseByReference(newNode)) {
             return null;
         }
-        DefaultListModel<Proof> proofs = previousProofs;
-        for (int i = 0; i < proofs.size(); i++) {
-            Proof p = proofs.get(i);
+        for (int i = 0; i < previousProofs.size(); i++) {
+            Proof p = previousProofs.get(i);
             if (p == newNode.proof()) {
                 continue; // doesn't make sense
             }
+            // conservative check: all user-defined rules in a previous proof
+            // have to also be available in the new proof
+            var proofFile = p.getProofFile() != null ? p.getProofFile().toString() : "////";
+            var tacletIndex = p.allGoals().head().ruleAppIndex().tacletIndex();
+            var newTacletIndex = newNode.proof().allGoals().head().ruleAppIndex().tacletIndex();
+            Set<NoPosTacletApp> newTaclets = null;
+            var tacletsOk = true;
+            for (var taclet : tacletIndex.allNoPosTacletApps().stream()
+                    .filter(x -> x.taclet().getOrigin() != null
+                            && x.taclet().getOrigin().contains(proofFile))
+                    .collect(Collectors.toList())) {
+                if (newTaclets == null) {
+                    newTaclets = newTacletIndex.allNoPosTacletApps();
+                }
+                if (newTaclets.stream().noneMatch(newTaclet -> Objects
+                        .equals(taclet.taclet().toString(), newTaclet.taclet().toString()))) {
+                    tacletsOk = false;
+                    break;
+                }
+            }
+            if (!tacletsOk) {
+                continue;
+            }
+
             // only search in compatible proofs
             if (!p.getSettings().getChoiceSettings()
                     .equals(newNode.proof().getSettings().getChoiceSettings())) {

key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java

@@ -70,6 +70,9 @@ public Proof getProof() {
     // display message for the status bar
     @Override
     public String toString() {
+        if (proof.isDisposed()) {
+            return "Proof disposed";
+        }
         if (appliedRules != 0) {
             StringBuilder message = new StringBuilder();
             String timeString = (timeInMillis / 1000) + "." + ((timeInMillis % 1000) / 100);

key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java

@@ -1003,9 +1003,13 @@ public TacletExecutor<? extends Taclet> getExecutor() {
 
     @Override
     @Nullable
-    public String getOrigin() { return origin; }
+    public String getOrigin() {
+        return origin;
+    }
 
-    public void setOrigin(@Nullable String origin) { this.origin = origin; }
+    public void setOrigin(@Nullable String origin) {
+        this.origin = origin;
+    }
 
     public void setAddedBy(Node addedBy) {
         this.addedBy = addedBy;

key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java

@@ -2,6 +2,7 @@
 
 import java.util.List;
 import java.util.Set;
+import javax.swing.*;
 
 /**
  * This class encapsulates information about: 1) relative font size in the prover view 2) the
@@ -141,6 +142,9 @@ public class ViewSettings extends AbstractPropertiesSettings {
      */
     private static final String USER_FOLDER_BOOKMARKS = "[View]folderBookmarks";
 
+    private static final String LOOK_AND_FEEL_DEFAULT =
+        UIManager.getCrossPlatformLookAndFeelClassName();
+
     /**
      * Show Taclet uninstantiated in tooltip -- for learning
      */
@@ -182,7 +186,8 @@ public class ViewSettings extends AbstractPropertiesSettings {
     private final PropertyEntry<Boolean> showWholeTaclet =
         createBooleanProperty(SHOW_WHOLE_TACLET, false);
     private final PropertyEntry<Integer> sizeIndex = createIntegerProperty(FONT_INDEX, 2);
-    private final PropertyEntry<String> lookAndFeel = createStringProperty(LOOK_AND_FEEL, null);
+    private final PropertyEntry<String> lookAndFeel =
+        createStringProperty(LOOK_AND_FEEL, LOOK_AND_FEEL_DEFAULT);
     private final PropertyEntry<Boolean> showSequentViewTooltips =
         createBooleanProperty(SEQUENT_VIEW_TOOLTIP, true);
     private final PropertyEntry<Boolean> showSourceViewTooltips =

key.core/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java

@@ -79,4 +79,50 @@ void testFindsReferenceInSameProof() throws Exception {
         p.dispose();
         p2.dispose();
     }
+
+    @Test
+    void checksUserLemmas() throws Exception {
+        GeneralSettings.noPruningClosed = false;
+        // Test scenario:
+        // Proof 1 uses a user-defined lemma.
+        // Proof 2 does not.
+        // Reference searcher should not find proof 1 when considering proof 2.
+
+        KeYEnvironment<DefaultUserInterfaceControl> env =
+            KeYEnvironment.load(new File(testCaseDirectory,
+                "proofCaching/proofWithRule.proof"));
+        Proof p = env.getLoadedProof();
+        KeYEnvironment<DefaultUserInterfaceControl> env2 =
+            KeYEnvironment.load(new File(testCaseDirectory,
+                "proofCaching/proofWithoutRule.proof"));
+        Proof p2 = env2.getLoadedProof();
+        KeYEnvironment<DefaultUserInterfaceControl> env3 =
+            KeYEnvironment.load(new File(testCaseDirectory,
+                "proofCaching/proofWithRule.proof"));
+        Proof p3 = env3.getLoadedProof();
+
+        DefaultListModel<Proof> previousProofs = new DefaultListModel<>();
+        previousProofs.addElement(p);
+        DefaultListModel<Proof> newProof = new DefaultListModel<>();
+        newProof.addElement(p2);
+
+        p2.pruneProof(p2.root());
+
+        assertTrue(ReferenceSearcher.suitableForCloseByReference(p2.root()));
+        ClosedBy c = ReferenceSearcher.findPreviousProof(previousProofs, p2.root());
+        assertNull(c);
+
+        // check that result is found if the user taclet is available
+        p3.pruneProof(p3.root());
+        assertTrue(ReferenceSearcher.suitableForCloseByReference(p3.root()));
+        c = ReferenceSearcher.findPreviousProof(previousProofs, p3.root());
+        assertNotNull(c);
+        assertEquals(0, c.getNode().serialNr());
+        assertEquals(p, c.getProof());
+
+        GeneralSettings.noPruningClosed = true;
+        p.dispose();
+        p2.dispose();
+        p3.dispose();
+    }
 }

key.core/src/test/resources/logback.xml

@@ -6,7 +6,7 @@
         <file>key.log</file>
         <append>false</append>
         <encoder>
-            <pattern>%-10relative %-5level %-15thread %-25logger{5} %msg %ex{short}%n</pattern>
+            <pattern>%-10relative %-5level %-15thread %-25logger{5} %msg %ex%n</pattern>
         </encoder>
     </appender>
 

key.core/src/test/resources/testcase/proofCaching/proofWithRule.proof

@@ -0,0 +1,23 @@
+\rules {
+
+    \lemma
+    two_plus_two_is_four {
+        \find(2 + 2 = 4)
+        \sameUpdateLevel
+        \replacewith(true)
+    };
+    }
+\problem {
+add(Z(2(#)), Z(2(#))) = Z(4(#))
+}
+
+\proof {
+(keyLog "0" (keyUser "arne" ) (keyVersion "3b3afbd3c459d500948aebed1347d8d52aa969d6"))
+
+(autoModeTime "0")
+
+(branch "dummy ID"
+(rule "two_plus_two_is_four" (formula "1") (userinteraction))
+(rule "closeTrue" (formula "1") (userinteraction))
+)
+}

key.core/src/test/resources/testcase/proofCaching/proofWithoutRule.proof

@@ -0,0 +1,15 @@
+\problem {
+add(Z(2(#)), Z(2(#))) = Z(4(#))
+}
+
+\proof {
+(keyLog "0" (keyUser "arne" ) (keyVersion "3b3afbd3c459d500948aebed1347d8d52aa969d6"))
+
+(autoModeTime "17")
+
+(branch "dummy ID"
+(rule "add_literals" (formula "1") (term "0"))
+ (builtin "One Step Simplification" (formula "1"))
+(rule "closeTrue" (formula "1"))
+)
+}

key.ui/examples/firstTouch/08-Java5/src/For.java

@@ -25,6 +25,7 @@ int sum () {
     void infiniteLoop() {
         //@ maintaining \invariant_for(f);
         //@ assignable \strictly_nothing;
+        //@ diverges true;
         for (Object o: f);
     }
 

key.ui/src/main/java/de/uka/ilkd/key/core/Main.java

@@ -4,6 +4,7 @@
 import java.io.IOException;
 import java.io.PrintStream;
 import java.lang.reflect.InvocationTargetException;
+import java.net.URL;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.Locale;
@@ -542,9 +543,42 @@ private static AbstractMediatorUserInterfaceControl createUserInterface(
     public static void ensureExamplesAvailable() {
         File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples()
                 : new File(getExamplesDir());
+        if (!examplesDir.exists()) {
+            examplesDir = setupExamples();
+        }
         setExamplesDir(examplesDir.getAbsolutePath());
     }
 
+    private static File setupExamples() {
+        try {
+            URL examplesURL = Main.class.getResource("/examples.zip");
+            if (examplesURL == null) {
+                throw new IOException("Missing examples.zip in resources");
+            }
+
+            File tempDir = createTempDirectory();
+
+            if (tempDir != null) {
+                IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath());
+            }
+            return tempDir;
+        } catch (IOException e) {
+            LOGGER.warn("Error setting up examples", e);
+            return null;
+        }
+    }
+
+
+    private static File createTempDirectory() throws IOException {
+        final File tempDir = File.createTempFile("keyheap-examples-", null);
+        tempDir.delete();
+        if (!tempDir.mkdir()) {
+            return null;
+        }
+        Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir)));
+        return tempDir;
+    }
+
     private static void evaluateLemmataOptions(CommandLine options) {
 
         LemmataAutoModeOptions opt;

key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java

@@ -35,7 +35,11 @@ private Watchdog() {
      * Start the watchdog in a background thread.
      */
     public static void start() {
-        new Thread(Watchdog::run, "Watchdog").start();
+        var thread = new Thread(Watchdog::run, "Watchdog");
+        // mark as daemon
+        // (only relevant for startup exception, where this thread would prevent the JVM exiting)
+        thread.setDaemon(true);
+        thread.start();
     }
 
     private static void run() {

key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java

@@ -163,6 +163,7 @@ public HeatmapOptionsDialog() {
         pack();
         setAlwaysOnTop(true);
         setResizable(false);
+        setLocationRelativeTo(MainWindow.getInstance());
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java

@@ -546,11 +546,15 @@ private JPanel createSourcePanel(Font font) {
     /**
      * Shows the dialog with a single exception. The stacktrace is extracted and can optionally be
      * shown in the dialog.
+     * Important: make sure to also log the exception before showing the dialog!
      *
      * @param parent the parent of the dialog (will be blocked)
      * @param exception the exception to display
      */
     public static void showExceptionDialog(Window parent, Throwable exception) {
+        // make sure UI is usable after any exception
+        MainWindow.getInstance().getMediator().startInterface(true);
+
         Set<PositionedIssueString> msg = Collections.singleton(extractMessage(exception));
         IssueDialog dlg = new IssueDialog(parent, "Parser Error", msg, true, exception);
         dlg.setVisible(true);