From 21776197bae9f3611d264e1c16e2a64a6c645da7 Mon Sep 17 00:00:00 2001 From: Tobias Date: Fri, 23 Feb 2024 21:51:16 +0100 Subject: [PATCH 01/46] remove old taclet options dialog and make "proof not loaded" header invisible when proof is loaded --- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 3 ++- .../key/gui/actions/ShowActiveTactletOptionsAction.java | 3 ++- .../de/uka/ilkd/key/gui/actions/TacletOptionsAction.java | 2 ++ .../uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java | 3 ++- .../uka/ilkd/key/gui/settings/TacletOptionsSettings.java | 8 +++++++- 5 files changed, 15 insertions(+), 4 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index e25b78cf31f..4e0163af49f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1027,7 +1027,8 @@ private JMenu createOptionsMenu() { options.setMnemonic(KeyEvent.VK_O); options.add(SettingsManager.getActionShowSettings(this)); - options.add(new TacletOptionsAction(this)); + // remove since taclet options should only be set through the general settings dialog + // options.add(new TacletOptionsAction(this)); options.add(new SMTOptionsAction(this)); // options.add(setupSpeclangMenu()); // legacy since only JML supported options.addSeparator(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java index 7ca4d776f79..cc41b976c0f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java @@ -55,7 +55,8 @@ private void showActivatedChoices() { final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns); activeOptions.setEditable(false); Object[] toDisplay = - { activeOptions, "These options can be changed in Options->Taclet Options" }; + { activeOptions, + "These options can be changed in Options->Show Settings->Taclet Options" }; JOptionPane.showMessageDialog(mainWindow, toDisplay, "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java index ffe05fd5e5d..faabacc3b5f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java @@ -11,6 +11,8 @@ import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; import de.uka.ilkd.key.settings.ProofSettings; +// This class is not used anymore as taclet options should be set through the general settings +// dialog public class TacletOptionsAction extends MainWindowAction { /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java index 1151dd47db8..b54d9b00823 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java @@ -108,7 +108,8 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings { defineDefault(SaveBundleAction.class, KeyEvent.VK_B, SHORTCUT_KEY_MASK); defineDefault(SaveFileAction.class, KeyEvent.VK_S, SHORTCUT_KEY_MASK); defineDefault(SettingsManager.ShowSettingsAction.class, KeyEvent.VK_N, SHORTCUT_KEY_MASK); - defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK); + // remove as the old menu should not be accessible anymore + // defineDefault(TacletOptionsAction.class, KeyEvent.VK_T, SHORTCUT_KEY_MASK); defineDefault(OpenFileAction.class, KeyEvent.VK_O, SHORTCUT_KEY_MASK); defineDefault(SearchInSequentAction.class, KeyEvent.VK_F, SHORTCUT_KEY_MASK); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 9ffa6aee27c..92fb727c5b3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -43,6 +43,10 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin private ChoiceSettings settings; private boolean warnNoProof = true; + // to make the "No Proof Loaded" header invisible when a proof is loaded + private JLabel lblHead2; + + public TacletOptionsSettings() { setHeaderText(getDescription()); pCenter.setLayout(new MigLayout(new LC().fillX(), new AC().fill().grow().gap("3mm"))); @@ -174,7 +178,7 @@ public static ChoiceEntry createChoiceEntry(String choice) { protected void layoutHead() { if (warnNoProof) { - JLabel lblHead2 = new JLabel("No Proof loaded. Taclet options may not be parsed."); + this.lblHead2 = new JLabel("No Proof loaded. Taclet options may not be parsed."); lblHead2.setIcon(IconFactory.WARNING_INCOMPLETE.get()); lblHead2.setFont(lblHead2.getFont().deriveFont(14f)); pNorth.add(lblHead2); @@ -292,6 +296,8 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { warnNoProof = window.getMediator().getSelectedProof() == null; + // this makes the wrong lblhead2 invisible + this.lblHead2.setVisible(warnNoProof); setChoiceSettings(SettingsManager.getChoiceSettings(window)); return this; } From b93592bc0c65c078221283875d00a2abba1c1bb9 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 7 Mar 2024 14:46:18 +0100 Subject: [PATCH 02/46] better error message for destroyed configuration files --- key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 6dde2f9ba5e..491a5d8ee7f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -156,7 +156,8 @@ public Configuration asConfiguration() { if (!res.isEmpty()) return (Configuration) res.get(0); else - throw new RuntimeException(); + throw new RuntimeException("Error in configuration. Source: " + + ctx.start.getTokenSource().getSourceName()); } } From 84078cc991aa704e1fae0769e612199f940b6fea Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 8 Mar 2024 10:52:02 +0100 Subject: [PATCH 03/46] no tooltip help --- .../ilkd/key/gui/settings/SimpleSettingsPanel.java | 14 ++++++++++++++ .../key/gui/settings/TacletOptionsSettings.java | 2 +- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java index 64de412bda9..550361a6465 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java @@ -190,6 +190,20 @@ public static JLabel createHelpLabel(String s) { return infoButton; } + public static JLabel createHelpTextLabel(String s) { + if (s == null || s.isEmpty()) { + s = ""; + } + if(s.contains("\n")){ + s = s.substring(0, s.indexOf('\n')); + } + + JLabel infoButton = new JLabel(s); + infoButton.setFont(infoButton.getFont().deriveFont(10f)); + infoButton.setBackground(Color.orange); + return infoButton; + } + public static JButton createHelpButton(Runnable callback) { var infoButton = new JButton(IconFontSwing.buildIcon(FontAwesomeSolid.QUESTION_CIRCLE, 16f)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 92fb727c5b3..2809e656b64 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -275,7 +275,7 @@ private JRadioButton addRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { b.add(lbl); } if (c.information != null) { - JLabel lbl = SettingsPanel.createHelpLabel(c.information); + JLabel lbl = SettingsPanel.createHelpTextLabel(c.information); b.add(lbl); } pCenter.add(b, new CC().newline()); From d62282b45bff7b96cfd1859bba5b1a182ee38ac3 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 20 Jul 2024 14:25:14 +0200 Subject: [PATCH 04/46] Remove Ctrl+C handling, see #3456 --- .../ilkd/key/gui/WindowUserInterfaceControl.java | 15 --------------- 1 file changed, 15 deletions(-) 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 f9066745de7..fa0578538d8 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 @@ -18,7 +18,6 @@ import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel; import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.gui.actions.ExitMainAction; import de.uka.ilkd.key.gui.mergerule.MergeRuleCompletion; import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; @@ -55,7 +54,6 @@ import org.antlr.v4.runtime.misc.ParseCancellationException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import sun.misc.Signal; /** * Implementation of {@link UserInterfaceControl} which controls the {@link MainWindow} with the @@ -79,19 +77,6 @@ public WindowUserInterfaceControl(MainWindow mainWindow) { completions.add(new BlockContractInternalCompletion(mainWindow)); completions.add(new BlockContractExternalCompletion(mainWindow)); completions.add(MergeRuleCompletion.INSTANCE); - try { - Signal.handle(new Signal("INT"), sig -> { - if (getMediator().isInAutoMode()) { - LOGGER.warn("Caught SIGINT, stopping automode..."); - getMediator().getUI().getProofControl().stopAutoMode(); - } else { - LOGGER.warn("Caught SIGINT, exiting..."); - new ExitMainAction(mainWindow).exitMainWithoutInteraction(); - } - }); - } catch (Exception e) { - // the above is optional functionality and may not work on every OS - } } @Override From 76585a949b2824efa394339a3af8a20bccbf0a6f Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 6 Aug 2024 14:09:01 +0200 Subject: [PATCH 05/46] refreshing the active settings dialogue --- build.gradle | 2 + .../java/de/uka/ilkd/key/nparser/KeyAst.java | 2 +- .../java/de/uka/ilkd/key/gui/MainWindow.java | 2 +- .../key/gui/actions/SettingsTreeModel.java | 21 ++--- .../gui/actions/ShowActiveSettingsAction.java | 46 ++++++----- .../ShowActiveTactletOptionsAction.java | 80 +++++++++---------- .../key/gui/settings/SimpleSettingsPanel.java | 2 +- 7 files changed, 83 insertions(+), 72 deletions(-) diff --git a/build.gradle b/build.gradle index 0cace069f6c..f46b3c74247 100644 --- a/build.gradle +++ b/build.gradle @@ -321,6 +321,8 @@ subprojects { targetExclude 'build/**' // allows us to use spotless:off / spotless:on to keep pre-formatted sections + // MU: Only ... because of the eclipse(...) below, it is "@formatter:off" and "@formatter:on" + // that must be used instead. toggleOffOn() removeUnusedImports() diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 491a5d8ee7f..5668ecac47e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -157,7 +157,7 @@ public Configuration asConfiguration() { return (Configuration) res.get(0); else throw new RuntimeException("Error in configuration. Source: " - + ctx.start.getTokenSource().getSourceName()); + + ctx.start.getTokenSource().getSourceName()); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 4e0163af49f..5199961da28 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1015,7 +1015,7 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(this, selected)); - proof.add(new ShowActiveTactletOptionsAction(this, selected)); + proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); proof.add(showActiveSettingsAction); proof.add(new ShowProofStatistics(this, selected)); proof.add(new ShowKnownTypesAction(this, selected)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java index c3d39655ee0..1d51d6895e6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java @@ -3,12 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions; +import java.util.Arrays; import java.util.Map.Entry; import java.util.Properties; -import javax.swing.JComponent; -import javax.swing.JScrollPane; -import javax.swing.JTable; -import javax.swing.JTextArea; +import javax.swing.*; import javax.swing.table.DefaultTableModel; import javax.swing.tree.DefaultMutableTreeNode; import javax.swing.tree.DefaultTreeModel; @@ -34,6 +32,7 @@ public class SettingsTreeModel extends DefaultTreeModel { private final ProofSettings proofSettings; private final ProofIndependentSettings independentSettings; + private OptionContentNode tacletOptionsItem; public SettingsTreeModel(ProofSettings proofSettings, ProofIndependentSettings independentSettings) { @@ -52,7 +51,8 @@ private void generateTree() { // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - proofSettingsNode.add(generateTableNode("Taclets", choiceSettings)); + tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); + proofSettingsNode.add(tacletOptionsItem); Settings strategySettings = proofSettings.getStrategySettings(); proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); @@ -115,6 +115,7 @@ private JComponent generateScrollPane(String text) { JTextArea ta = new JTextArea(5, 20); ta.append(text); ta.setEditable(false); + ta.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); JScrollPane scrollpane = new JScrollPane(ta); return scrollpane; } @@ -130,6 +131,8 @@ private JComponent generateJTable(Properties properties) { i++; } + Arrays.sort(data, (a, b) -> a[0].toString().compareToIgnoreCase(b[0].toString())); + JTable table = new JTable(); DefaultTableModel tableModel = new DefaultTableModel() { @@ -143,9 +146,8 @@ public boolean isCellEditable(int row, int column) { }; tableModel.setDataVector(data, columnNames); - table.setModel(tableModel); - + table.setRowHeight(table.getRowHeight() + 10); JScrollPane scrollpane = new JScrollPane(table); return scrollpane; @@ -157,6 +159,7 @@ private OptionContentNode generateOptionContentNode(String title, String text) { return new OptionContentNode(title, generateScrollPane(text)); } - - + public OptionContentNode getTacletOptionsItem() { + return tacletOptionsItem; + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java index e32b368b999..bbc3e484b77 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java @@ -22,9 +22,6 @@ */ public class ShowActiveSettingsAction extends MainWindowAction { - /** - * - */ private static final long serialVersionUID = -3038735283059371442L; public ShowActiveSettingsAction(MainWindow mainWindow) { @@ -35,6 +32,10 @@ public ShowActiveSettingsAction(MainWindow mainWindow) { @Override public void actionPerformed(ActionEvent e) { + showDialog(); + } + + private ViewSettingsDialog showDialog() { ProofSettings settings = (getMediator().getSelectedProof() == null) ? ProofSettings.DEFAULT_SETTINGS : getMediator().getSelectedProof().getSettings(); @@ -44,6 +45,14 @@ public void actionPerformed(ActionEvent e) { dialog.setTitle("All active settings"); dialog.setLocationRelativeTo(mainWindow); dialog.setVisible(true); + return dialog; + } + + public void showAndFocusTacletOptions() { + ViewSettingsDialog dialog = showDialog(); + SettingsTreeModel model = (SettingsTreeModel) dialog.optionTree.getModel(); + OptionContentNode item = model.getTacletOptionsItem(); + dialog.getOptionTree().setSelectionPath(new TreePath(item.getPath())); } /** @@ -57,31 +66,33 @@ private class ViewSettingsDialog extends JDialog { public ViewSettingsDialog(TreeModel model, JComponent startComponent) { super(mainWindow); - this.getContentPane().setLayout(new BoxLayout(getContentPane(), BoxLayout.Y_AXIS)); - Box box = Box.createHorizontalBox(); - box.add(getSplitPane()); - this.getContentPane().add(box); - this.getContentPane().add(Box.createVerticalStrut(5)); - box = Box.createHorizontalBox(); - box.add(Box.createHorizontalStrut(5)); + Container cp = this.getContentPane(); + cp.setLayout(new BorderLayout()); + cp.add(getSplitPane(), BorderLayout.CENTER); + JButton okButton = new JButton("OK"); okButton.addActionListener(e -> dispose()); setDefaultCloseOperation(DISPOSE_ON_CLOSE); - box.add(okButton); - box.add(Box.createHorizontalStrut(5)); - this.getContentPane().add(box); + JPanel buttons = new JPanel(new FlowLayout()); + buttons.add(okButton); + cp.add(buttons, BorderLayout.SOUTH); + + JLabel announce = + new JLabel("This shows the active settings for the current proof.
" + + "To change settings for future proofs, use Options > Show Settings."); + announce.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); + cp.add(announce, BorderLayout.NORTH); + this.getOptionTree().setModel(model); getSplitPane().setRightComponent(startComponent); this.getOptionTree().getParent().setMinimumSize(getOptionTree().getPreferredSize()); - this.getContentPane().setPreferredSize(computePreferredSize(model)); + cp.setPreferredSize(computePreferredSize(model)); this.setDefaultCloseOperation(DISPOSE_ON_CLOSE); setIconImage(IconFactory.keyLogo()); this.pack(); this.setLocationRelativeTo(MainWindow.getInstance()); - - getRootPane().registerKeyboardAction((e) -> dispose(), KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_IN_FOCUSED_WINDOW); getRootPane().setDefaultButton(okButton); @@ -127,15 +138,14 @@ private JTree getOptionTree() { } } }); + optionTree.setBorder(BorderFactory.createEmptyBorder(5, 5, 5, 5)); } return optionTree; } private JSplitPane getSplitPane() { if (splitPane == null) { - splitPane = new JSplitPane(); - splitPane.setAlignmentX(LEFT_ALIGNMENT); splitPane.setLeftComponent(new JScrollPane(getOptionTree())); splitPane.setRightComponent(getOptionPanel()); // splitPane.setResizeWeight(0.2); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java index cc41b976c0f..46a724e3a02 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveTactletOptionsAction.java @@ -4,61 +4,57 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; -import javax.swing.JOptionPane; -import javax.swing.JTextArea; -import javax.swing.text.JTextComponent; import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.notification.events.GeneralInformationEvent; -import de.uka.ilkd.key.proof.Proof; +/** + * Action to show a dialog with the taclet options valid for the currently + * selected proof. + * + * Now defers to the "Show Active Settings" action to show the taclet options. + */ public class ShowActiveTactletOptionsAction extends MainWindowAction { - /** - * - */ private static final long serialVersionUID = -7012564698194718532L; + private final ShowActiveSettingsAction action; - private final Proof proof; - - public ShowActiveTactletOptionsAction(MainWindow mainWindow, Proof proof) { + public ShowActiveTactletOptionsAction(MainWindow mainWindow, ShowActiveSettingsAction action) { super(mainWindow); setName("Show Active Taclet Options"); - - getMediator().enableWhenProofLoaded(this); - - this.proof = proof; + this.action = action; } @Override public void actionPerformed(ActionEvent e) { - showActivatedChoices(); + action.showAndFocusTacletOptions(); } - private void showActivatedChoices() { - Proof currentProof = proof == null ? getMediator().getSelectedProof() : proof; - if (currentProof == null) { - mainWindow.notify(new GeneralInformationEvent("No Options available.", - "If you wish to see Taclet Options " + "for a proof you have to load one first")); - } else { - StringBuilder message = new StringBuilder("Active Taclet Options:\n"); - int rows = 0; - int columns = 0; - for (final String choice : currentProof.getSettings().getChoiceSettings() - .getDefaultChoices().values()) { - message.append(choice).append("\n"); - rows++; - if (columns < choice.length()) { - columns = choice.length(); - } - } - final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns); - activeOptions.setEditable(false); - Object[] toDisplay = - { activeOptions, - "These options can be changed in Options->Show Settings->Taclet Options" }; - JOptionPane.showMessageDialog(mainWindow, toDisplay, - "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE); - } - } + // @formatter:off + +// private void showActivatedChoices() { +// Proof currentProof = proof == null ? getMediator().getSelectedProof() : proof; +// if (currentProof == null) { +// mainWindow.notify(new GeneralInformationEvent("No Options available.", +// "If you wish to see Taclet Options " + "for a proof you have to load one first")); +// } else { +// StringBuilder message = new StringBuilder("Active Taclet Options:\n"); +// int rows = 0; +// int columns = 0; +// for (final String choice : currentProof.getSettings().getChoiceSettings() +// .getDefaultChoices().values()) { +// message.append(choice).append("\n"); +// rows++; +// if (columns < choice.length()) { +// columns = choice.length(); +// } +// } +// final JTextComponent activeOptions = new JTextArea(message.toString(), rows, columns); +// activeOptions.setEditable(false); +// Object[] toDisplay = +// { activeOptions, +// "These options can be changed in Options->Show Settings->Taclet Options" }; +// JOptionPane.showMessageDialog(mainWindow, toDisplay, +// "Taclet options used in the current proof", JOptionPane.INFORMATION_MESSAGE); +// } +// } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java index 550361a6465..828b8852f0c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java @@ -194,7 +194,7 @@ public static JLabel createHelpTextLabel(String s) { if (s == null || s.isEmpty()) { s = ""; } - if(s.contains("\n")){ + if (s.contains("\n")) { s = s.substring(0, s.indexOf('\n')); } From 8304e292a086a5449e2c3648d52ad9711deb8bdb Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 6 Aug 2024 16:34:51 +0200 Subject: [PATCH 06/46] taclet option settings dialog refactored --- .../gui/settings/TacletOptionsSettings.java | 109 ++++++++++++------ 1 file changed, 73 insertions(+), 36 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 2809e656b64..319a57df3ff 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -15,6 +15,7 @@ import java.util.List; import java.util.stream.Collectors; import javax.swing.*; +import javax.swing.plaf.ColorUIResource; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; @@ -192,7 +193,8 @@ protected void layoutHead() { protected void layoutChoiceSelector() { pCenter.removeAll(); - category2Choice.keySet().stream().sorted().forEach(this::addCategory); + category2Choice.keySet().stream().sorted(String::compareToIgnoreCase) + .forEach(this::addCategory); } protected void addCategory(String cat) { @@ -200,47 +202,52 @@ protected void addCategory(String cat) { ChoiceEntry selectedChoice = findChoice(choices, category2Choice.get(cat)); String explanation = getExplanation(cat); - addTitleRow(cat); + JLabel title = createTitleRow(cat, selectedChoice); + JPanel selectPanel = new JPanel(new MigLayout(new LC().fillX(), new AC().fill().grow())); ButtonGroup btnGroup = new ButtonGroup(); for (ChoiceEntry c : choices) { - JRadioButton btn = addRadioButton(c, btnGroup); + JRadioButton btn = mkRadioButton(c, btnGroup); if (c.equals(selectedChoice)) { btn.setSelected(true); } - btn.addActionListener(new ChoiceSettingsSetter(cat, c.choice)); + btn.addActionListener(new ChoiceSettingsSetter(title, cat, c)); + selectPanel.add(btn, new CC().newline()); } - addExplanation(explanation); + selectPanel.add(mkExplanation(explanation), new CC().pad(0, 20, 0, 0).newline()); + + JPanel catEntry = createCollapsableTitlePane(title, selectPanel); + pCenter.add(catEntry, new CC().newline()); } - protected void addExplanation(String explanation) { - JTextArea explanationArea = new JTextArea(); + protected JComponent mkExplanation(String explanation) { + JTextArea explanationArea = new JTextArea() { + @Override + public void setBackground(Color bg) { + super.setBackground(bg); + } + }; explanationArea.setEditable(false); explanationArea.setLineWrap(true); explanationArea.setWrapStyleWord(true); - explanationArea.setText(explanation); + explanationArea.setText(explanation.trim()); explanationArea.setCaretPosition(0); - explanationArea.setBackground(getBackground()); - JPanel p = createCollapsibleTitlePane("Info", explanationArea); - pCenter.add(p, new CC().span().newline()); + explanationArea.setBackground(toNonUIColor(getBackground())); + return explanationArea; } @NonNull - private JPanel createCollapsibleTitlePane(String titleText, JComponent child) { + private JPanel createCollapsableTitlePane(JComponent title, JComponent child) { JPanel p = new JPanel(new BorderLayout()); - JPanel north = new JPanel(new BorderLayout()); - - p.setBorder(BorderFactory.createLineBorder(Color.black)); - JButton title = new JButton(titleText); - title.setContentAreaFilled(false); - title.setBorderPainted(false); - north.add(title, BorderLayout.WEST); + JPanel north = new JPanel(new FlowLayout(FlowLayout.LEFT)); + JLabel more = new JLabel(IconFactory.TREE_NODE_RETRACTED.get()); + north.add(more); + north.add(title); p.add(north, BorderLayout.NORTH); p.add(child); - child.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); + // child.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); child.setVisible(false); - title.setIcon(IconFactory.TREE_NODE_RETRACTED.get()); - title.addMouseListener(new MouseAdapter() { + var mouse = new MouseAdapter() { private boolean opened = false; @Override @@ -248,20 +255,23 @@ public void mouseClicked(MouseEvent e) { opened = !opened; child.setVisible(opened); if (opened) { - title.setIcon(IconFactory.TREE_NODE_EXPANDED.get()); + more.setIcon(IconFactory.TREE_NODE_EXPANDED.get()); } else { - title.setIcon(IconFactory.TREE_NODE_RETRACTED.get()); + more.setIcon(IconFactory.TREE_NODE_RETRACTED.get()); } } - }); + }; + + title.addMouseListener(mouse); + more.addMouseListener(mouse); + return p; } - private JRadioButton addRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { + private JRadioButton mkRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { Box b = new Box(BoxLayout.X_AXIS); JRadioButton button = new JRadioButton(c.choice); btnGroup.add(button); - // add(new JLabel(c.choice)); b.add(button); if (c.incomplete) { @@ -278,14 +288,20 @@ private JRadioButton addRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { JLabel lbl = SettingsPanel.createHelpTextLabel(c.information); b.add(lbl); } - pCenter.add(b, new CC().newline()); return button; } - private void addTitleRow(String cat) { - JLabel lbl = new JLabel(cat); + private JLabel createTitleRow(String cat, ChoiceEntry entry) { + JLabel lbl = new JLabel(createCatTitleText(cat, entry)); lbl.setFont(lbl.getFont().deriveFont(14f)); - pCenter.add(lbl, new CC().span().newline()); + return lbl; + } + + private static String createCatTitleText(String cat, ChoiceEntry entry) { + // strip the leading "cat:" from "cat:value" + return cat + (entry == null ? "" + : " (set to '" + + entry.choice.substring(cat.length() + 1) + "')"); } @Override @@ -466,17 +482,38 @@ public String toString() { } private class ChoiceSettingsSetter implements ActionListener { + private final JLabel title; private final String category; - private final String options; + private final ChoiceEntry choice; - public ChoiceSettingsSetter(String cat, String choice) { - category = cat; - options = choice; + public ChoiceSettingsSetter(JLabel title, String cat, ChoiceEntry choice) { + this.title = title; + this.category = cat; + this.choice = choice; } @Override public void actionPerformed(ActionEvent e) { - category2Choice.put(category, options); + category2Choice.put(category, choice.choice); + title.setText(createCatTitleText(category, choice)); + title.repaint(); + } + } + + /** + * Converts a color to a non-UI color. + * + * There is a call to "SwingUtilities.updateComponentTreeUI(comp);" somewhere which resets all + * resources to original colors. To override, we have to convert the color to a non-UI color. + * + * @param color The color to convert. + * @return The non-UI color. + */ + private static Color toNonUIColor(Color color) { + if (color instanceof ColorUIResource) { + return new Color(color.getRGB(), true); + } else { + return color; } } } From 57069e2a01832736074a90fb974616f930fa537a Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Tue, 30 Jan 2024 11:21:05 +0100 Subject: [PATCH 07/46] Revert "Fix CurrentGoalView highlights not being removed" This reverts commit 4759370f719ed506746e7a2a13832eac48cfc6c1. As discussed during a developers meeting, the highlighting is quite important during drag'n'drop. --- .../main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java | 1 - 1 file changed, 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java index 5704821655d..8370e15b7bc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java @@ -203,7 +203,6 @@ synchronized void printSequentImmediately() { return; } var time = System.nanoTime(); - getHighlighter().removeAllHighlights(); removeMouseListener(listener); From 48c083c8da1d87b9689627abf0441186c6d68ba6 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Wed, 7 Aug 2024 16:11:03 +0200 Subject: [PATCH 08/46] bringing color definitions to one point, highlight mouse selection --- .../key/gui/nodeviews/CurrentGoalView.java | 17 +-- .../ilkd/key/gui/nodeviews/SequentView.java | 42 ++++--- .../de/uka/ilkd/key/util/DoNothingCaret.java | 108 ++++++++++++++++++ 3 files changed, 137 insertions(+), 30 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/util/DoNothingCaret.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java index 8370e15b7bc..35d5c8fefe1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java @@ -16,7 +16,6 @@ import de.uka.ilkd.key.gui.ApplyTacletDialog; import de.uka.ilkd.key.gui.GUIListener; import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.colors.ColorSettings; import de.uka.ilkd.key.pp.InitialPositionTable; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.pp.Range; @@ -35,22 +34,10 @@ */ public final class CurrentGoalView extends SequentView implements Autoscroll { - /** - * - */ private static final long serialVersionUID = 8494000234215913553L; - public static final ColorSettings.ColorProperty DEFAULT_HIGHLIGHT_COLOR = - ColorSettings.define("[currentGoal]defaultHighlight", "", new Color(70, 100, 170, 76)); - - public static final ColorSettings.ColorProperty ADDITIONAL_HIGHLIGHT_COLOR = - ColorSettings.define("[currentGoal]addtionalHighlight", "", new Color(0, 0, 0, 38)); - - private static final ColorSettings.ColorProperty UPDATE_HIGHLIGHT_COLOR = - ColorSettings.define("[currentGoal]updateHighlight", "", new Color(0, 150, 130, 38)); - - public static final ColorSettings.ColorProperty DND_HIGHLIGHT_COLOR = - ColorSettings.define("[currentGoal]dndHighlight", "", new Color(0, 150, 130, 104)); + // The color constants that used to be here have been moved to SequentView to collect them in + // one place. private static final Logger LOGGER = LoggerFactory.getLogger(CurrentGoalView.class); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java index 0db35e40024..ab49bd2a6a1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java @@ -7,12 +7,9 @@ import java.awt.event.MouseEvent; import java.util.*; import javax.swing.*; -import javax.swing.text.BadLocationException; -import javax.swing.text.DefaultHighlighter; +import javax.swing.text.*; import javax.swing.text.DefaultHighlighter.DefaultHighlightPainter; -import javax.swing.text.Highlighter; import javax.swing.text.Highlighter.HighlightPainter; -import javax.swing.text.JTextComponent; import javax.swing.text.html.HTMLDocument; import de.uka.ilkd.key.gui.MainWindow; @@ -29,6 +26,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ViewSettings; +import de.uka.ilkd.key.util.DoNothingCaret; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -49,18 +47,33 @@ public abstract class SequentView extends JEditorPane { public static final Color PERMANENT_HIGHLIGHT_COLOR = new Color(110, 85, 181, 76); - public static final Color DND_HIGHLIGHT_COLOR = new Color(0, 150, 130, 104); + public static final ColorSettings.ColorProperty DEFAULT_HIGHLIGHT_COLOR = + ColorSettings.define("[currentGoal]defaultHighlight", "", new Color(70, 100, 170, 76)); - protected static final Color UPDATE_HIGHLIGHT_COLOR = new Color(0, 150, 130, 38); + public static final ColorSettings.ColorProperty ADDITIONAL_HIGHLIGHT_COLOR = + ColorSettings.define("[currentGoal]addtionalHighlight", "", new Color(0, 0, 0, 38)); - protected static final Color INACTIVE_BACKGROUND_COLOR = - new Color(UIManager.getColor("Panel.background").getRGB()); + public static final ColorSettings.ColorProperty UPDATE_HIGHLIGHT_COLOR = + ColorSettings.define("[currentGoal]updateHighlight", "", new Color(0, 150, 130, 38)); - // - private static final ColorSettings.ColorProperty HEATMAP_COLOR = ColorSettings.define( + public static final ColorSettings.ColorProperty DND_HIGHLIGHT_COLOR = + ColorSettings.define("[currentGoal]dndHighlight", "", new Color(0, 150, 130, 255)); + + public static final ColorSettings.ColorProperty HEATMAP_COLOR = ColorSettings.define( "[Heatmap]basecolor", "Base color of the heatmap. Other colors are derived from this one.", new Color(252, 202, 80)); + public static final ColorSettings.ColorProperty MOUSE_SELECTION_COLOR = ColorSettings.define( + "[currentGoal]mouseSelectionColor", "Color of the mouse selection in the sequent view.", + new Color(230, 230, 230, 255)); + + protected static final Color INACTIVE_BACKGROUND_COLOR = + new Color(UIManager.getColor("Panel.background").getRGB()); + + private static final HighlightPainter MOUSE_SELECTION_PAINTER = + new DefaultHighlightPainter(MOUSE_SELECTION_COLOR.get()); + + // maximum opacity of heatmap color private static final float HEATMAP_DEFAULT_START_OPACITY = .7f; public static final String PROP_LAST_MOUSE_POSITION = "lastMousePosition"; @@ -173,6 +186,9 @@ protected SequentView(MainWindow mainWindow) { KeYGuiExtensionFacade.installKeyboardShortcuts(getMainWindow().getMediator(), this, KeYGuiExtension.KeyboardShortcuts.SEQUENT_VIEW); + // MU 2024: The (colourless) mouse selection would sometimes get in the way of the other + // highlights. This disables the caret altogether. + setCaret(DoNothingCaret.INSTANCE); } public final void setFont() { @@ -318,6 +334,7 @@ public void paint(Graphics g, int p0, int p1, Shape bounds, JTextComponent c) { * * @see javax.swing.JEditorPane#getText() */ + /** * Returns the plain text of this sequent view. */ @@ -631,10 +648,8 @@ protected void removeUserSelectionHighlight() { } /** - * * @param point a point. * @return {@code true} if and only if the argument points to the user selection. - * * @see #setUserSelectionHighlight(PosInSequent) * @see #setUserSelectionHighlight(Point) * @see #removeUserSelectionHighlight() @@ -649,7 +664,6 @@ protected boolean isInUserSelectionHighlight(Point point) { * Highlights the term at the specified position as the user's selection. * * @param pis the term to select. - * * @see #setUserSelectionHighlight(Point) * @see #removeUserSelectionHighlight() * @see #isInUserSelectionHighlight(Point) @@ -1017,7 +1031,6 @@ public boolean isHiding() { } /** - * * @return {@code true} if this sequent view is supposed to be shown in the {@link MainFrame}, * {@code false} if it is only supposed to be shown in some other frame. */ @@ -1030,7 +1043,6 @@ public boolean isMainSequentView() { * term heatmap highlighting. * * @author jschiffl - * */ static class PIO_age { PosInOccurrence pio; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/DoNothingCaret.java b/key.ui/src/main/java/de/uka/ilkd/key/util/DoNothingCaret.java new file mode 100644 index 00000000000..426019a923d --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/util/DoNothingCaret.java @@ -0,0 +1,108 @@ +/* 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.awt.*; +import javax.swing.event.ChangeListener; +import javax.swing.text.Caret; +import javax.swing.text.JTextComponent; + +/** + * A caret that does nothing. + * + * This implementation is used disable in SequentViews. The problem is that manually selected text + * interferes with the automatic highlights for drag-n-drop and mouseover. + * + * All methods return default values or do nothing. + * + * @author Mattias Ulbrich + */ +public class DoNothingCaret implements Caret { + public static final Caret INSTANCE = new DoNothingCaret(); + + @Override + public void install(JTextComponent c) { + + } + + @Override + public void deinstall(JTextComponent c) { + + } + + @Override + public void paint(Graphics g) { + + } + + @Override + public void addChangeListener(ChangeListener l) { + + } + + @Override + public void removeChangeListener(ChangeListener l) { + + } + + @Override + public boolean isVisible() { + return false; + } + + @Override + public void setVisible(boolean v) { + + } + + @Override + public boolean isSelectionVisible() { + return false; + } + + @Override + public void setSelectionVisible(boolean v) { + + } + + @Override + public void setMagicCaretPosition(Point p) { + + } + + @Override + public Point getMagicCaretPosition() { + return new Point(0, 0); + } + + @Override + public void setBlinkRate(int rate) { + + } + + @Override + public int getBlinkRate() { + return 0; + } + + @Override + public int getDot() { + return 0; + } + + @Override + public int getMark() { + return 0; + } + + @Override + public void setDot(int dot) { + + } + + @Override + public void moveDot(int dot) { + + } +} From 0df9c3c4d0bb1a91708067cb923bc4eee846f4ac Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Wed, 7 Aug 2024 17:23:35 +0200 Subject: [PATCH 09/46] make heatmap setting changes visible --- .../key/gui/actions/HeatmapToggleAction.java | 3 ++ .../key/gui/nodeviews/CurrentGoalView.java | 2 +- .../nodeviews/CurrentGoalViewListener.java | 8 +++-- .../ilkd/key/gui/nodeviews/SequentView.java | 29 +++++++------------ .../gui/nodeviews/SequentViewSearchBar.java | 7 +++-- 5 files changed, 24 insertions(+), 25 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java index b7df2f6c0b5..aa196ab72f0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java @@ -64,5 +64,8 @@ public void actionPerformed(ActionEvent e) { ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(); vs.setHeatmapOptions(!vs.isShowHeatmap(), vs.isHeatmapSF(), vs.isHeatmapNewest(), vs.getMaxAgeForHeatmap()); + // this updates the heatmap highlights + mainWindow.getCurrentGoalView().getHighlighter().removeAllHighlights(); + mainWindow.getCurrentGoalView().printSequent(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java index 35d5c8fefe1..379d45a13e6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java @@ -156,7 +156,7 @@ void updateUpdateHighlights() { // be a starting place to find the mistake. range = new Range(range.start() + 1, range.end() + 1); - Object tag = getColorHighlight(UPDATE_HIGHLIGHT_COLOR.get()); + Object tag = createColorHighlight(UPDATE_HIGHLIGHT_COLOR.get()); updateHighlights.add(tag); paintHighlight(range, tag); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java index 16a2d2d2ac8..746b874c031 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java @@ -120,7 +120,9 @@ public synchronized boolean modalDragNDropEnabled() { @Override public void dragGestureRecognized(DragGestureEvent dgEvent) { final Object oldHighlight = getSequentView().getCurrentHighlight(); - getSequentView().setCurrentHighlight(getSequentView().dndHighlight); + Object dndHighlight = + getSequentView().createColorHighlight(SequentView.DND_HIGHLIGHT_COLOR.get()); + getSequentView().setCurrentHighlight(dndHighlight); hideMenu(menu); Point dragOrigin = dgEvent.getDragOrigin(); PosInSequent localMousePos = getSequentView().getPosInSequent(dragOrigin); @@ -134,7 +136,7 @@ public void dragGestureRecognized(DragGestureEvent dgEvent) { public void dragDropEnd(DragSourceDropEvent event) { // Enable updating the subterm // highlightning ... - getSequentView().disableHighlight(getSequentView().dndHighlight); + getSequentView().disableHighlight(dndHighlight); getSequentView().setCurrentHighlight(oldHighlight); } }); @@ -142,7 +144,7 @@ public void dragDropEnd(DragSourceDropEvent event) { // system not in proper dnd state // Enable updating the subterm // highlightning ... - getSequentView().disableHighlight(getSequentView().dndHighlight); + getSequentView().disableHighlight(dndHighlight); getSequentView().setCurrentHighlight(oldHighlight); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java index ab49bd2a6a1..8dd79d96681 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java @@ -34,9 +34,6 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import static de.uka.ilkd.key.gui.nodeviews.CurrentGoalView.ADDITIONAL_HIGHLIGHT_COLOR; -import static de.uka.ilkd.key.gui.nodeviews.CurrentGoalView.DEFAULT_HIGHLIGHT_COLOR; - /* * Parent class of CurrentGoalView and InnerNodeView. */ @@ -122,9 +119,6 @@ public VisibleTermLabels getVisibleTermLabels() { // an additional highlight to mark the first active java statement private Object additionalJavaHighlight; - // Highlighting color during drag and drop action. - public final Object dndHighlight; - /* * Store highlights in a HashMap in order to prevent duplicate highlights. */ @@ -169,9 +163,8 @@ protected SequentView(MainWindow mainWindow) { // sets the painter for the highlighting setHighlighter(new DefaultHighlighter()); - additionalJavaHighlight = getColorHighlight(ADDITIONAL_HIGHLIGHT_COLOR.get()); - defaultHighlight = getColorHighlight(DEFAULT_HIGHLIGHT_COLOR.get()); - dndHighlight = getColorHighlight(CurrentGoalView.DND_HIGHLIGHT_COLOR.get()); + additionalJavaHighlight = createColorHighlight(ADDITIONAL_HIGHLIGHT_COLOR.get()); + defaultHighlight = createColorHighlight(DEFAULT_HIGHLIGHT_COLOR.get()); currentHighlight = defaultHighlight; // add a SeqViewChangeListener to this component @@ -296,13 +289,14 @@ public void paintHighlight(Range range, Object highlighter) { } /** - * registers a highlighter that marks the regions specified by the returned tag with the given + * creates and registers a highlighter that marks the regions specified by the returned tag with + * the given * color * * @param color the Color used to highlight regions of the sequent * @return the highlight for the specified color */ - public final Object getColorHighlight(Color color) { + public final Object createColorHighlight(Color color) { Object highlight = null; if (!color2Highlight.containsKey(color)) { // show highlights above each other @@ -502,11 +496,10 @@ public Object getCurrentHighlight() { public void paintHighlights(Point p) { // re-initialize highlights if needed if (!Arrays.asList(getHighlighter().getHighlights()).contains(additionalJavaHighlight)) { - additionalJavaHighlight = getColorHighlight(ADDITIONAL_HIGHLIGHT_COLOR.get()); + additionalJavaHighlight = createColorHighlight(ADDITIONAL_HIGHLIGHT_COLOR.get()); } if (!Arrays.asList(getHighlighter().getHighlights()).contains(defaultHighlight)) { - defaultHighlight = getColorHighlight(DEFAULT_HIGHLIGHT_COLOR.get()); - currentHighlight = defaultHighlight; + defaultHighlight = createColorHighlight(DEFAULT_HIGHLIGHT_COLOR.get()); } // Change highlight for additional Java statement ... @@ -767,7 +760,7 @@ protected void updateHeatmapSFHighlights(int max_age, boolean newest) { // Off-by-one: siehe updateUpdateHighlights bzw in InnerNodeView. // rangeForPath ist schuld Range newR = new Range(r.start() + 1, r.end() + 1); - Object tag = getColorHighlight(color); + Object tag = createColorHighlight(color); paintHighlight(newR, tag); } } @@ -786,7 +779,7 @@ protected void updateHeatmapSFHighlights(int max_age, boolean newest) { // Off-by-one: siehe updateUpdateHighlights bzw in InnerNodeView. rangeForPath // ist schuld Range newR = new Range(r.start() + 1, r.end() + 1); - Object tag = getColorHighlight(color); + Object tag = createColorHighlight(color); paintHighlight(newR, tag); } ++i; @@ -895,7 +888,7 @@ protected void updateHeatmapTermHighlights(int max_age, boolean newest) { // Off-by-one: siehe updateUpdateHighlights bzw in InnerNodeView. rangeForPath // ist schuld Range newR = new Range(r.start() + 1, r.end() + 1); - Object tag = getColorHighlight(color); + Object tag = createColorHighlight(color); paintHighlight(newR, tag); } } @@ -912,7 +905,7 @@ protected void updateHeatmapTermHighlights(int max_age, boolean newest) { // Off-by-one: siehe updateUpdateHighlights bzw in InnerNodeView. rangeForPath // ist schuld Range newR = new Range(r.start() + 1, r.end() + 1); - Object tag = getColorHighlight(color); + Object tag = createColorHighlight(color); paintHighlight(newR, tag); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java index 622b4adeb1c..408270aa64f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java @@ -203,7 +203,7 @@ public boolean search(@NonNull String search) { boolean loopEntered = false; while (m.find()) { int foundAt = m.start(); - Object highlight = sequentView.getColorHighlight(SEARCH_HIGHLIGHT_COLOR_2.get()); + Object highlight = sequentView.createColorHighlight(SEARCH_HIGHLIGHT_COLOR_2.get()); searchResults.add(new Pair<>(foundAt, highlight)); sequentView.paintHighlight(new Range(foundAt, m.end()), highlight); loopEntered = true; @@ -229,13 +229,14 @@ public void searchFor(String searchTerm) { } private void setExtraHighlight(int resultIndex) { - resetHighlight(resultIndex, sequentView.getColorHighlight(SEARCH_HIGHLIGHT_COLOR_1.get())); + resetHighlight(resultIndex, + sequentView.createColorHighlight(SEARCH_HIGHLIGHT_COLOR_1.get())); sequentView.setCaretPosition(searchResults.get(resultIndex).first); } private void resetExtraHighlight() { resetHighlight(resultIteratorPos, - sequentView.getColorHighlight(SEARCH_HIGHLIGHT_COLOR_2.get())); + sequentView.createColorHighlight(SEARCH_HIGHLIGHT_COLOR_2.get())); } private void resetHighlight(int resultIndex, Object highlight) { From d33375e55b34379faf3d3e4e4bf96bb4e5207970 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Tue, 13 Aug 2024 12:18:15 +0200 Subject: [PATCH 10/46] fix for #3501: decrease log level of duplicate sort warnings --- .../de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java index 048588c7717..825279099a1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java @@ -183,7 +183,7 @@ public Object visitOne_sort_decl(KeYParser.One_sort_declContext ctx) { // weigl: agreement on KaKeY meeting: this should be ignored until we finally have // local namespaces for generic sorts // addWarning(ctx, "Sort declaration is ignored, due to collision."); - LOGGER.info("Sort declaration of {} in {} is ignored due to collision (already " + LOGGER.debug("Sort declaration of {} in {} is ignored due to collision (already " + "present in {}).", sortName, BuilderHelpers.getPosition(ctx), existingSort.getOrigin()); } From de47ab77b701d34d1213707026eb1918526732d1 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Wed, 20 Dec 2023 10:18:34 +0100 Subject: [PATCH 11/46] Fix the loop invariant dialog --- .../uka/ilkd/key/speclang/LoopSpecImpl.java | 20 +++++++------------ .../ilkd/key/gui/InvariantConfigurator.java | 12 +++++------ 2 files changed, 13 insertions(+), 19 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java index f6882b75863..b9b1c68d605 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java @@ -252,8 +252,7 @@ public Term getModifiable(LocationVariable heap, Term selfTerm, } @Override - public Term getModifiable(Term selfTerm, Map atPres, - Services services) { + public Term getModifiable(Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); LocationVariable baseHeap = services.getTypeConverter().getHeapLDT().getHeap(); Map replaceMap = getReplaceMap(selfTerm, atPres, services); @@ -267,17 +266,12 @@ public Term getFreeModifiable(LocationVariable heap, Term selfTerm, assert (selfTerm == null) == (originalSelfTerm == null); Map replaceMap = getReplaceMap(selfTerm, atPres, services); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); - return or.replace(originalFreeModifiable.get(heap)); - } - - @Override - public Term getFreeModifiable(Term selfTerm, Map atPres, - Services services) { - assert (selfTerm == null) == (originalSelfTerm == null); - LocationVariable baseHeap = services.getTypeConverter().getHeapLDT().getHeap(); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); - OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); - return or.replace(originalFreeModifiable.get(baseHeap)); + final Term originalFreeModForHeap = originalFreeModifiable.get(heap); + if (originalFreeModForHeap != null) { + return or.replace(originalFreeModForHeap); + } else { + return services.getTermBuilder().strictlyNothing(); + } } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java index 4e6cf87faf9..89448bb99ff 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java @@ -102,8 +102,6 @@ public LoopSpecification getLoopInvariant(final LoopSpecification loopInv, index = 0; class InvariantDialog extends JDialog { - private final LocationVariable HEAP_LDT = - services.getTypeConverter().getHeapLDT().getHeap(); private final Color COLOR_SUCCESS = Color.GREEN; private final Color COLOR_ERROR = Color.RED; @@ -593,15 +591,17 @@ private JPanel createErrorPanel(Map invMsgs, JTabbedPane modPane = new JTabbedPane(JTabbedPane.BOTTOM); for (LocationVariable heap : services.getTypeConverter().getHeapLDT() .getAllHeaps()) { + + final LocationVariable baseHeap = + services.getTypeConverter().getHeapLDT().getHeap(); final String k = heap.name().toString(); String title = - format("Invariant%s - Status: ", heap == HEAP_LDT ? "" : "[" + k + "]"); + format("Invariant%s - Status: ", heap == baseHeap ? "" : "[" + k + "]"); String errorMessage = invMsgs == null ? "OK" : invMsgs.get(k); Color invColor = invColors == null ? COLOR_SUCCESS : invColors.get(k); JTextArea textArea = createErrorTextField(title, errorMessage, invColor); invPane.add(k, textArea); - title = - format("Modifiable%s - Status: ", heap == HEAP_LDT ? "" : "[" + k + "]"); + title = format("Modifiable%s - Status: ", heap == baseHeap ? "" : "[" + k + "]"); String errorMessage2 = modMsgs == null ? "OK" : modMsgs.get(k); Color modColor = modColors == null ? COLOR_SUCCESS : modColors.get(k); textArea = createErrorTextField(title, errorMessage2, modColor); @@ -852,7 +852,7 @@ private void parse() { setError(modErrors, modCols, heap.toString(), e.getMessage()); } } - LocationVariable baseHeap = HEAP_LDT; + LocationVariable baseHeap = services.getTypeConverter().getHeapLDT().getHeap(); // TODO: add post expressions and new objects try { infFlowSpecs.put(baseHeap, parseInfFlowSpec(baseHeap)); From 6df4c4c57ee0b886d9935e7083fc7f1afe63c0e8 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Thu, 21 Dec 2023 11:12:31 +0100 Subject: [PATCH 12/46] Fix duplicate self in namespaces --- .../uka/ilkd/key/speclang/LoopSpecImpl.java | 21 ++++++++++--------- .../ilkd/key/speclang/LoopSpecification.java | 12 ----------- .../ilkd/key/gui/InvariantConfigurator.java | 9 ++------ 3 files changed, 13 insertions(+), 29 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java index b9b1c68d605..8fa080e2c1a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java @@ -136,7 +136,7 @@ public LoopSpecImpl(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, Term // ------------------------------------------------------------------------- private Map /* Operator, Operator, Term -> Term */ getReplaceMap(Term selfTerm, - Map atPres, Services services) { + Map atPres) { final Map result = new LinkedHashMap<>(); // self @@ -169,7 +169,7 @@ public LoopSpecImpl(LoopStatement loop, IProgramMethod pm, KeYJavaType kjt, Term private Map getInverseReplaceMap(Term selfTerm, Map atPres, Services services) { final Map result = new LinkedHashMap<>(); - final Map replaceMap = getReplaceMap(selfTerm, atPres, services); + final Map replaceMap = getReplaceMap(selfTerm, atPres); for (Map.Entry next : replaceMap.entrySet()) { result.put(next.getValue(), next.getKey()); } @@ -218,7 +218,7 @@ public LoopStatement getLoop() { public Term getInvariant(LocationVariable heap, Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); return or.replace(originalInvariants.get(heap)); } @@ -232,7 +232,7 @@ public Term getInvariant(Services services) { public Term getFreeInvariant(LocationVariable heap, Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); return or.replace(originalFreeInvariants.get(heap)); } @@ -246,16 +246,17 @@ public Term getFreeInvariant(Services services) { public Term getModifiable(LocationVariable heap, Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); return or.replace(originalModifiable.get(heap)); } @Override - public Term getModifiable(Term selfTerm, Map atPres, Services services) { + public Term getModifiable(Term selfTerm, Map atPres, + Services services) { assert (selfTerm == null) == (originalSelfTerm == null); LocationVariable baseHeap = services.getTypeConverter().getHeapLDT().getHeap(); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); return or.replace(originalModifiable.get(baseHeap)); } @@ -264,7 +265,7 @@ public Term getModifiable(Term selfTerm, Map atPres, Ser public Term getFreeModifiable(LocationVariable heap, Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); final Term originalFreeModForHeap = originalFreeModifiable.get(heap); if (originalFreeModForHeap != null) { @@ -278,7 +279,7 @@ public Term getFreeModifiable(LocationVariable heap, Term selfTerm, public ImmutableList getInfFlowSpecs(LocationVariable heap, Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); return or.replaceInfFlowSpec(originalInfFlowSpecs.get(heap)); } @@ -297,7 +298,7 @@ public ImmutableList getInfFlowSpecs(Services services) { @Override public Term getVariant(Term selfTerm, Map atPres, Services services) { assert (selfTerm == null) == (originalSelfTerm == null); - Map replaceMap = getReplaceMap(selfTerm, atPres, services); + Map replaceMap = getReplaceMap(selfTerm, atPres); OpReplacer or = new OpReplacer(replaceMap, services.getTermFactory(), services.getProof()); return or.replace(originalVariant); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java index cffc8f7607f..892a2208bac 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecification.java @@ -95,18 +95,6 @@ Term getFreeModifiable(LocationVariable heap, Term selfTerm, Map atPres, Services services); - /** - * Returns the free modifiable clause. - * - * @param selfTerm the self term. - * @param atPres the operators used for the pre-heap. - * @param services the Services object. - * @return The modifiable clause as a term. - */ - Term getFreeModifiable(Term selfTerm, - Map atPres, - Services services); - /** * Returns the information flow specification clause. */ diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java index 89448bb99ff..4ee96af1360 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java @@ -18,7 +18,6 @@ import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.NamespaceSet; -import de.uka.ilkd.key.logic.ProgramElementName; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.nparser.KeyIO; @@ -185,11 +184,6 @@ public InvariantDialog() throws RuleAbortException { setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE); final NamespaceSet nss = services.getNamespaces().copyWithParent(); - Term self = loopInv.getInternalSelfTerm(); - if (self != null) { - nss.programVariables() - .add(new LocationVariable(new ProgramElementName("self"), self.sort())); - } parser = new KeyIO(services, nss); parser.setAbbrevMap(getAbbrevMap()); @@ -601,7 +595,8 @@ private JPanel createErrorPanel(Map invMsgs, Color invColor = invColors == null ? COLOR_SUCCESS : invColors.get(k); JTextArea textArea = createErrorTextField(title, errorMessage, invColor); invPane.add(k, textArea); - title = format("Modifiable%s - Status: ", heap == baseHeap ? "" : "[" + k + "]"); + title = + format("Modifiable%s - Status: ", heap == baseHeap ? "" : "[" + k + "]"); String errorMessage2 = modMsgs == null ? "OK" : modMsgs.get(k); Color modColor = modColors == null ? COLOR_SUCCESS : modColors.get(k); textArea = createErrorTextField(title, errorMessage2, modColor); From 514d2a1560cfafe4461c00e9a48cac0e886c3abc Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 13 Aug 2024 19:10:00 +0200 Subject: [PATCH 13/46] fix proof tab --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 3 +- .../key/gui/actions/SettingsTreeModel.java | 40 +++++++++++-------- .../gui/actions/ShowActiveSettingsAction.java | 2 +- .../key/gui/settings/SettingsManager.java | 2 +- 4 files changed, 28 insertions(+), 19 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 5199961da28..08972da1a3b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1015,7 +1015,8 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(this, selected)); - proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); + // We merge the old window to view the active taclet options with the window for all active settings + //proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); proof.add(showActiveSettingsAction); proof.add(new ShowProofStatistics(this, selected)); proof.add(new ShowKnownTypesAction(this, selected)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java index 1d51d6895e6..8b31a9f0814 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java @@ -45,23 +45,29 @@ public SettingsTreeModel(ProofSettings proofSettings, private void generateTree() { DefaultMutableTreeNode root = (DefaultMutableTreeNode) this.getRoot(); - OptionContentNode proofSettingsNode = - generateOptionContentNode("Proof Settings", "These are the proof dependent settings."); - root.add(proofSettingsNode); - - // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); - ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings(); - tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); - proofSettingsNode.add(tacletOptionsItem); - - Settings strategySettings = proofSettings.getStrategySettings(); - proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); - - Settings smtSettings = proofSettings.getSMTSettings(); - proofSettingsNode.add(generateTableNode("SMT", smtSettings)); + if (proofSettings == null) { + OptionContentNode proofSettingsNode = + generateOptionContentNode("Proof Settings", "There is currently no proof loaded!"); + root.add(proofSettingsNode); + } else { + OptionContentNode proofSettingsNode = + generateOptionContentNode("Proof Settings", "These are the proof dependent settings."); + root.add(proofSettingsNode); + + // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); + ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); + tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); + proofSettingsNode.add(tacletOptionsItem); + + Settings strategySettings = proofSettings.getStrategySettings(); + proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); + + Settings smtSettings = proofSettings.getSMTSettings(); + proofSettingsNode.add(generateTableNode("SMT", smtSettings)); + } OptionContentNode independentSettingsNode = generateOptionContentNode( - "Proof-Independent Settings", "These are the proof independent settings."); + "Proof-Independent Settings", "These are the proof independent settings."); root.add(independentSettingsNode); Settings generalSettings = independentSettings.getGeneralSettings(); @@ -75,7 +81,9 @@ private void generateTree() { Settings viewSettings = independentSettings.getViewSettings(); independentSettingsNode.add(generateTableNode("View", viewSettings)); Settings termLabelSettings = independentSettings.getTermLabelSettings(); - proofSettingsNode.add(generateTableNode("Term Labels", termLabelSettings)); + // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the previous line, + // it should really be added to the independentSettingsNode + independentSettingsNode.add(generateTableNode("Term Labels", termLabelSettings)); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java index bbc3e484b77..40d266773b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java @@ -37,7 +37,7 @@ public void actionPerformed(ActionEvent e) { private ViewSettingsDialog showDialog() { ProofSettings settings = - (getMediator().getSelectedProof() == null) ? ProofSettings.DEFAULT_SETTINGS + (getMediator().getSelectedProof() == null) ? null : getMediator().getSelectedProof().getSettings(); SettingsTreeModel model = new SettingsTreeModel(settings, ProofIndependentSettings.DEFAULT_INSTANCE); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java index d0d0b1ef541..91bb112e251 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java @@ -158,7 +158,7 @@ public boolean remove(SettingsProvider o) { public static class ShowSettingsAction extends MainWindowAction { public ShowSettingsAction(MainWindow mainWindow) { super(mainWindow); - setName("Show Settings"); + setName("Settings"); setIcon(IconFactory.editFile(16)); } From 30bd5329407d8ce94a9465d43dfd0e4b2df29cf8 Mon Sep 17 00:00:00 2001 From: Tobias Date: Fri, 16 Aug 2024 16:46:59 +0200 Subject: [PATCH 14/46] disable taclet option settings when no proof is loaded --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 6 +-- .../gui/settings/TacletOptionsSettings.java | 41 +++++++++++-------- 2 files changed, 27 insertions(+), 20 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 08972da1a3b..9ca06df9927 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1015,8 +1015,9 @@ public void menuCanceled(MenuEvent e) { } proof.addSeparator(); proof.add(new ShowUsedContractsAction(this, selected)); - // We merge the old window to view the active taclet options with the window for all active settings - //proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); + // We merge the old window to view the active taclet options with the window for all active + // settings + // proof.add(new ShowActiveTactletOptionsAction(this, showActiveSettingsAction)); proof.add(showActiveSettingsAction); proof.add(new ShowProofStatistics(this, selected)); proof.add(new ShowKnownTypesAction(this, selected)); @@ -1040,7 +1041,6 @@ private JMenu createOptionsMenu() { options.add(new JCheckBoxMenuItem(new EnsureSourceConsistencyToggleAction(this))); return options; - } private JMenu createHelpMenu() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index 319a57df3ff..dc1f9881658 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -45,7 +45,7 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin private boolean warnNoProof = true; // to make the "No Proof Loaded" header invisible when a proof is loaded - private JLabel lblHead2; + private JLabel noProofLoadedHeader; public TacletOptionsSettings() { @@ -178,12 +178,10 @@ public static ChoiceEntry createChoiceEntry(String choice) { } protected void layoutHead() { - if (warnNoProof) { - this.lblHead2 = new JLabel("No Proof loaded. Taclet options may not be parsed."); - lblHead2.setIcon(IconFactory.WARNING_INCOMPLETE.get()); - lblHead2.setFont(lblHead2.getFont().deriveFont(14f)); - pNorth.add(lblHead2); - } + this.noProofLoadedHeader = new JLabel("No Proof loaded. Taclet options may not be parsed."); + noProofLoadedHeader.setIcon(IconFactory.WARNING_INCOMPLETE.get()); + noProofLoadedHeader.setFont(noProofLoadedHeader.getFont().deriveFont(14f)); + pNorth.add(noProofLoadedHeader); JLabel lblHead2 = new JLabel("Taclet options will take effect only on new proofs."); lblHead2.setIcon(IconFactory.WARNING_INCOMPLETE.get()); @@ -204,14 +202,17 @@ protected void addCategory(String cat) { JLabel title = createTitleRow(cat, selectedChoice); JPanel selectPanel = new JPanel(new MigLayout(new LC().fillX(), new AC().fill().grow())); - ButtonGroup btnGroup = new ButtonGroup(); - for (ChoiceEntry c : choices) { - JRadioButton btn = mkRadioButton(c, btnGroup); - if (c.equals(selectedChoice)) { - btn.setSelected(true); + + if (!warnNoProof) { + ButtonGroup btnGroup = new ButtonGroup(); + for (ChoiceEntry c : choices) { + JRadioButton btn = mkRadioButton(c, btnGroup); + if (c.equals(selectedChoice)) { + btn.setSelected(true); + } + btn.addActionListener(new ChoiceSettingsSetter(title, cat, c)); + selectPanel.add(btn, new CC().newline()); } - btn.addActionListener(new ChoiceSettingsSetter(title, cat, c)); - selectPanel.add(btn, new CC().newline()); } selectPanel.add(mkExplanation(explanation), new CC().pad(0, 20, 0, 0).newline()); @@ -297,7 +298,13 @@ private JLabel createTitleRow(String cat, ChoiceEntry entry) { return lbl; } - private static String createCatTitleText(String cat, ChoiceEntry entry) { + private String createCatTitleText(String cat, ChoiceEntry entry) { + // TODO: magic to say what is set in the current proof + // if no proof is loaded, we do not want to display current settings + if (warnNoProof) { + return cat; + } + // strip the leading "cat:" from "cat:value" return cat + (entry == null ? "" : " (set to '" + @@ -312,8 +319,8 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { warnNoProof = window.getMediator().getSelectedProof() == null; - // this makes the wrong lblhead2 invisible - this.lblHead2.setVisible(warnNoProof); + // this makes the header invisible + this.noProofLoadedHeader.setVisible(warnNoProof); setChoiceSettings(SettingsManager.getChoiceSettings(window)); return this; } From 4b682347726456e1aecc2cb218a5e42498e4b842 Mon Sep 17 00:00:00 2001 From: Tobias Date: Sat, 17 Aug 2024 01:46:14 +0200 Subject: [PATCH 15/46] show a warning when the taclet options differ from the currently loaded proof --- .../key/gui/actions/SettingsTreeModel.java | 10 +++-- .../ilkd/key/gui/settings/SettingsDialog.java | 1 + .../gui/settings/TacletOptionsSettings.java | 40 ++++++++++++++++++- 3 files changed, 45 insertions(+), 6 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java index 8b31a9f0814..2478d14958a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java @@ -47,11 +47,12 @@ private void generateTree() { if (proofSettings == null) { OptionContentNode proofSettingsNode = - generateOptionContentNode("Proof Settings", "There is currently no proof loaded!"); + generateOptionContentNode("Proof Settings", "There is currently no proof loaded!"); root.add(proofSettingsNode); } else { OptionContentNode proofSettingsNode = - generateOptionContentNode("Proof Settings", "These are the proof dependent settings."); + generateOptionContentNode("Proof Settings", + "These are the proof dependent settings."); root.add(proofSettingsNode); // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); @@ -67,7 +68,7 @@ private void generateTree() { } OptionContentNode independentSettingsNode = generateOptionContentNode( - "Proof-Independent Settings", "These are the proof independent settings."); + "Proof-Independent Settings", "These are the proof independent settings."); root.add(independentSettingsNode); Settings generalSettings = independentSettings.getGeneralSettings(); @@ -81,7 +82,8 @@ private void generateTree() { Settings viewSettings = independentSettings.getViewSettings(); independentSettingsNode.add(generateTableNode("View", viewSettings)); Settings termLabelSettings = independentSettings.getTermLabelSettings(); - // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the previous line, + // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the + // previous line, // it should really be added to the independentSettingsNode independentSettingsNode.add(generateTableNode("Term Labels", termLabelSettings)); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java index c5a4f69b4af..e17eee82592 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java @@ -78,6 +78,7 @@ SettingsUi getUi() { private List apply() { List exc = new LinkedList<>(); apply(providers, exc); + return exc; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java index dc1f9881658..791f4e663a3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java @@ -19,6 +19,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ChoiceSettings; import de.uka.ilkd.key.settings.ProofSettings; @@ -47,6 +48,8 @@ public class TacletOptionsSettings extends SimpleSettingsPanel implements Settin // to make the "No Proof Loaded" header invisible when a proof is loaded private JLabel noProofLoadedHeader; + private Proof loadedProof = null; + public TacletOptionsSettings() { setHeaderText(getDescription()); @@ -295,11 +298,14 @@ private JRadioButton mkRadioButton(ChoiceEntry c, ButtonGroup btnGroup) { private JLabel createTitleRow(String cat, ChoiceEntry entry) { JLabel lbl = new JLabel(createCatTitleText(cat, entry)); lbl.setFont(lbl.getFont().deriveFont(14f)); + + // we want to display a warning if the current choice differs from the loaded proof + checkForDifferingOptions(lbl, cat, entry); + return lbl; } private String createCatTitleText(String cat, ChoiceEntry entry) { - // TODO: magic to say what is set in the current proof // if no proof is loaded, we do not want to display current settings if (warnNoProof) { return cat; @@ -311,6 +317,34 @@ private String createCatTitleText(String cat, ChoiceEntry entry) { entry.choice.substring(cat.length() + 1) + "')"); } + /** + * Checks if the current choice {@code entry} differs from the loaded proof and sets the icon to + * show a warning if necessary. + * + * @param lbl The label to set the icon on + * @param cat The category of the choice + * @param entry The current choice + */ + private void checkForDifferingOptions(JLabel lbl, String cat, ChoiceEntry entry) { + if (loadedProof != null) { + String choiceOfLoadedProof = + loadedProof.getSettings().getChoiceSettings().getDefaultChoices().get(cat); + boolean choiceDiffers = entry != null && !entry.choice.equals(choiceOfLoadedProof); + if (choiceDiffers) { + lbl.setIcon(IconFactory.WARNING_INCOMPLETE.get()); + lbl.setHorizontalTextPosition(JLabel.LEFT); + lbl.setIconTextGap(10); + lbl.setToolTipText( + "The current choice of this option differs from the loaded proof.
" + + "The loaded proof uses: " + choiceOfLoadedProof + ""); + + } else { + lbl.setIcon(null); + lbl.setToolTipText(null); + } + } + } + @Override public String getDescription() { return "Taclet Options"; @@ -318,7 +352,8 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { - warnNoProof = window.getMediator().getSelectedProof() == null; + loadedProof = window.getMediator().getSelectedProof(); + warnNoProof = loadedProof == null; // this makes the header invisible this.noProofLoadedHeader.setVisible(warnNoProof); setChoiceSettings(SettingsManager.getChoiceSettings(window)); @@ -503,6 +538,7 @@ public ChoiceSettingsSetter(JLabel title, String cat, ChoiceEntry choice) { public void actionPerformed(ActionEvent e) { category2Choice.put(category, choice.choice); title.setText(createCatTitleText(category, choice)); + checkForDifferingOptions(title, category, choice); title.repaint(); } } From 8f4ee86e046f23dfee5bf8e25b21ea1b4f268675 Mon Sep 17 00:00:00 2001 From: Tobias Date: Sun, 18 Aug 2024 14:35:06 +0200 Subject: [PATCH 16/46] mark TacletOptionsAction as deprecated --- .../java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java | 1 + 1 file changed, 1 insertion(+) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java index faabacc3b5f..215114b6d7e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java @@ -13,6 +13,7 @@ // This class is not used anymore as taclet options should be set through the general settings // dialog +@Deprecated public class TacletOptionsAction extends MainWindowAction { /** From 4f35bb4baa804a89675d6f928e33d7d1893bb6eb Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Thu, 22 Aug 2024 21:47:24 +0200 Subject: [PATCH 17/46] repairing heatmap updates for inner nodes --- key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 9 +++++++++ .../de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java | 8 ++++++++ .../java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java | 4 ++++ 3 files changed, 21 insertions(+) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index e25b78cf31f..31aa9b0eeb2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1254,6 +1254,15 @@ public void scrollTo(int y) { mainFrame.scrollTo(y); } + /** + * Get the main frame for access to the sequent view + * + * @return the container for this main window. + */ + public MainFrame getMainFrame() { + return mainFrame; + } + void displayResults(String message) { LOGGER.debug("displaying results: {}", message); setStatusLine(message); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java index aa196ab72f0..87a8998dee4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java @@ -3,6 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions; +import java.awt.*; import java.awt.event.ActionEvent; import java.beans.PropertyChangeListener; import javax.swing.*; @@ -11,6 +12,7 @@ import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.gui.nodeviews.SequentView; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ViewSettings; @@ -67,5 +69,11 @@ public void actionPerformed(ActionEvent e) { // this updates the heatmap highlights mainWindow.getCurrentGoalView().getHighlighter().removeAllHighlights(); mainWindow.getCurrentGoalView().printSequent(); + Component component = mainWindow.getMainFrame().getContent(); + if (component instanceof SequentView) { + SequentView seqView = (SequentView) component; + seqView.getHighlighter().removeAllHighlights(); + seqView.printSequent(); + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java index 5a8abd84bb9..61b87ee7905 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java @@ -113,4 +113,8 @@ public boolean isShowTacletInfo() { public void scrollTo(int y) { scrollPane.getVerticalScrollBar().setValue(y); } + + public Component getContent() { + return content; + } } From 76d4825a228233233ecd4655dc09966faf97b63e Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 26 Aug 2024 21:40:30 +0200 Subject: [PATCH 18/46] repairing type annotations in key.util ... it compiles again. thanks to Florian and Werner --- .../key_project/util/collection/ImmutableMapEntry.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMapEntry.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMapEntry.java index c7d5876752c..17af02c803e 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMapEntry.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMapEntry.java @@ -3,12 +3,18 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.collection; +import org.checkerframework.checker.nullness.qual.KeyForBottom; +import org.jspecify.annotations.Nullable; + /** * This interface declares a tupel of two values. The first one is of type and named key, the * second one is of type and named value + * + * For type annotations see Florian Lanzinger or Werner Dietl. :) + * https://eisop.github.io/cf/manual/manual.html#map-key-defaults-lowerbound */ -public interface ImmutableMapEntry { +public interface ImmutableMapEntry<@KeyForBottom S, @KeyForBottom T extends @Nullable Object> { /** @return the first part of the tupel */ S key(); From 436669bde38af4f4ce8bd3b52a4fd887af06d835 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 26 Aug 2024 21:41:29 +0200 Subject: [PATCH 19/46] extending the nonnull type system to the immutable maps --- .../util/collection/DefaultImmutableMap.java | 320 +++++++----------- .../util/collection/ImmutableMap.java | 94 +++-- .../util/collection/Immutables.java | 2 +- 3 files changed, 190 insertions(+), 226 deletions(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java index 04ebd8b85cf..0bab4a58487 100644 --- a/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/DefaultImmutableMap.java @@ -4,33 +4,38 @@ package org.key_project.util.collection; import java.util.Iterator; +import java.util.Objects; import org.key_project.util.Strings; +import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + /** * This class implements {@code ImmutableMap} and provides a persistent map. * It is a simple implementation like lists */ -@SuppressWarnings("nullness") -public class DefaultImmutableMap implements ImmutableMap { +public final class DefaultImmutableMap implements ImmutableMap { /** the empty map */ + private static final DefaultImmutableMap EMPTY_MAP = new DefaultImmutableMap<>(); @SuppressWarnings("unchecked") public static DefaultImmutableMap nilMap() { - return (DefaultImmutableMap) NILMap.EMPTY_MAP; + return (DefaultImmutableMap) EMPTY_MAP; } /** * The map this map builds on. Lookups will also consider entries in this map if the key * does not match {@link #entry}. */ - private final DefaultImmutableMap parent; + private final @Nullable DefaultImmutableMap parent; /** * The (key, value) mapping last inserted into this map. */ - private final ImmutableMapEntry entry; + private final @Nullable ImmutableMapEntry entry; /** * Number of entries in the map. Equal to 1 + parent.size if entry is not null, @@ -39,34 +44,19 @@ public static DefaultImmutableMap nilMap() { private final int size; /** only for use by NILMap */ - protected DefaultImmutableMap() { - entry = null; + private DefaultImmutableMap() { + this.entry = null; this.parent = null; this.size = 0; } - - /** creates new map with mapping entry */ - protected DefaultImmutableMap(ImmutableMapEntry entry) { - if (entry == null) { - throw new RuntimeException("'null' is not allowed as entry"); - } - this.entry = entry; - this.parent = DefaultImmutableMap.nilMap(); - this.size = 1; - } - /** creates new map with mapping entry and parent map */ - protected DefaultImmutableMap(ImmutableMapEntry entry, DefaultImmutableMap parent) { - if (entry == null) { - throw new IllegalArgumentException("'null' is not allowed as entry"); - } - this.entry = entry; + private DefaultImmutableMap(ImmutableMapEntry entry, DefaultImmutableMap parent) { + this.entry = Objects.requireNonNull(entry); this.parent = parent; this.size = parent.size + 1; } - /** * inserts mapping {@code } into the map (old map is not modified) if key exists old * entry has @@ -82,10 +72,13 @@ public ImmutableMap put(S key, T value) { return new DefaultImmutableMap<>(new MapEntry<>(key, value), this.remove(key)); } - - - /** @return value of type T that is mapped by key of type S */ - public T get(S key) { + /** + * Retrieves the value mapped to key in this map. + * + * @param key key to look up + * @return value of type T that is mapped by key of type S, null if key is not in the map + */ + public @Nullable T get(S key) { DefaultImmutableMap queue = this; while (!queue.isEmpty()) { final ImmutableMapEntry e = queue.entry; @@ -106,8 +99,15 @@ public int size() { } /** returns true if the map is empty */ + @EnsuresNonNullIf(result = false, expression = { "entry", "parent" }) public boolean isEmpty() { - return false; + if (parent == null) { + return true; + } else { + assert entry != null + : "@AssumeAssertion(nullness): entry and parent are both nonnull ..."; + return false; + } } /** @return true iff the map includes key */ @@ -225,26 +225,28 @@ public String toString() { return Strings.formatAsList(this, "[", ",", "]"); } + /** + * The equality checks if the argument is another immutable map with the same + * entries. + * + * @return true iff the other object is an immutable map with the same entries + */ @SuppressWarnings("unchecked") - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { if (!(o instanceof ImmutableMap)) { return false; } + if (o == this) { return true; } - ImmutableMap o1 = null; - try { - o1 = (ImmutableMap) o; - if (o1.size() != size()) { - return false; - } - } catch (ClassCastException cce) { + // TODO: This unchecked cast is a bit blunt but seems safe in the current implementations + ImmutableMap o1 = (ImmutableMap) o; + if (o1.size() != size()) { return false; } - for (ImmutableMapEntry e : this) { if (!e.value().equals(o1.get(e.key()))) { return false; @@ -262,206 +264,114 @@ public int hashCode() { return hashCode; } - /** the empty map */ - private static class NILMap extends DefaultImmutableMap { - - @SuppressWarnings("rawtypes") - static final NILMap EMPTY_MAP = new NILMap(); - - /** - * generated serial - */ - private static final long serialVersionUID = 412820308341055305L; + /** iterator for the values */ + private static abstract class MapIterator { + // stores the entry iterator + private DefaultImmutableMap map; - private NILMap() { + // creates the iterator + MapIterator(DefaultImmutableMap map) { + this.map = map; } - public ImmutableMap put(S key, T value) { - return new DefaultImmutableMap<>(new MapEntry<>(key, value)); + /** @return true iff there are more elements */ + public boolean hasNext() { + return !map.isEmpty(); } - public T get(S key) { - return null; + /** @return next value in list */ + protected final ImmutableMapEntry nextEntry() { + if (map.isEmpty()) { + throw new IllegalStateException("No more elements in iterator"); + } + final @NonNull ImmutableMapEntry entry = map.entry; + map = map.parent; + return entry; } - public boolean isEmpty() { - return true; + /** + * throws an unsupported operation exception as removing elements is not allowed on + * immutable maps + */ + public void remove() { + throw new UnsupportedOperationException( + "Removing elements via an iterator" + " is not supported for immutable maps."); } + } - public boolean containsKey(S key) { - return false; - } - public boolean containsValue(T val) { - return false; - } + /** iterator for the values */ + private static final class MapEntryIterator extends MapIterator + implements Iterator> { - public DefaultImmutableMap remove(S key) { - return this; + MapEntryIterator(DefaultImmutableMap map) { + super(map); } - public ImmutableMap removeAll(T value) { - return this; + /** @return next value in list */ + public ImmutableMapEntry next() { + return nextEntry(); } + } - /** @return iterator for keys */ - public Iterator keyIterator() { - return ImmutableSLList.nil().iterator(); - } - /** @return iterator for values */ - public Iterator valueIterator() { - return ImmutableSLList.nil().iterator(); + private static final class MapValueIterator extends MapIterator + implements Iterator { + + MapValueIterator(DefaultImmutableMap map) { + super(map); } - /** @return iterator for entries */ - public Iterator> iterator() { - return ImmutableSLList.>nil().iterator(); + /** @return next value in list */ + public T next() { + return nextEntry().value(); } + } + - public int size() { - return 0; + private static final class MapKeyIterator extends MapIterator + implements Iterator { + + MapKeyIterator(DefaultImmutableMap map) { + super(map); } - public String toString() { - return "[(,)]"; + /** @return next value in list */ + public S next() { + return nextEntry().key(); } } /** - * inner class for the entries + * class for the map entries * * @param key the key * @param value the value */ - private record MapEntry( - S key, T value)implements ImmutableMapEntry - { - /** - * - */ - private static final long serialVersionUID = -6785625761293313622L; - - /** - * creates a new map entry that contains key and value - */ - private MapEntry - { - } - - /** - * @return the key stored in this entry - */ - @Override - public S key() { - return key; - } - - /** - * @return the value stored in this entry - */ - @Override - public T value() { - return value; - } + // @formatter:off Spotless cannot deal with inner records yet or so it seems :( + private record MapEntry(S key, T value) implements ImmutableMapEntry { - /** - * @return true iff both objects have equal pairs of key and value - */ - public boolean equals(Object obj) { - if (obj == this) { - return true; - } - if (!(obj instanceof ImmutableMapEntry)) { - return false; + /** + * @return true iff both objects have equal pairs of key and value + */ + public boolean equals(@Nullable Object obj) { + if (obj == this) { + return true; + } + if (!(obj instanceof ImmutableMapEntry)) { + return false; + } + @SuppressWarnings("unchecked") + final ImmutableMapEntry cmp = (ImmutableMapEntry) obj; + final S cmpKey = cmp.key(); + final T cmpVal = cmp.value(); + return (key == cmpKey && value == cmpVal) + || (key.equals(cmpKey) && value.equals(cmpVal)); } - @SuppressWarnings("unchecked") - final ImmutableMapEntry cmp = (ImmutableMapEntry) obj; - final S cmpKey = cmp.key(); - final T cmpVal = cmp.value(); - return (key == cmpKey && value == cmpVal) - || (key.equals(cmpKey) && value.equals(cmpVal)); - } - - public String toString() { - return key + "->" + value; - } -} - -/** iterator for the values */ -private static abstract class MapIterator { - // stores the entry iterator - private DefaultImmutableMap map; - - // creates the iterator - MapIterator(DefaultImmutableMap map) { - this.map = map; - } - - /** @return true iff there are more elements */ - public boolean hasNext() { - return !map.isEmpty(); - } - - /** @return next value in list */ - protected final ImmutableMapEntry nextEntry() { - final ImmutableMapEntry entry = map.entry; - map = map.parent; - return entry; - } - - /** - * throws an unsupported operation exception as removing elements is not allowed on - * immutable maps - */ - public void remove() { - throw new UnsupportedOperationException( - "Removing elements via an iterator" + " is not supported for immutable maps."); - } -} - - -/** iterator for the values */ -private static final class MapEntryIterator extends MapIterator - implements Iterator> { - - MapEntryIterator(DefaultImmutableMap map) { - super(map); - } - - /** @return next value in list */ - public ImmutableMapEntry next() { - return nextEntry(); - } -} - - -private static final class MapValueIterator extends MapIterator - implements Iterator { - - MapValueIterator(DefaultImmutableMap map) { - super(map); - } - - /** @return next value in list */ - public T next() { - return nextEntry().value(); - } -} - - -private static final class MapKeyIterator extends MapIterator - implements Iterator { - - MapKeyIterator(DefaultImmutableMap map) { - super(map); - } - - /** @return next value in list */ - public S next() { - return nextEntry().key(); + public String toString() { + return key + "->" + value; + } } -} } diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java index 0c13b30233b..eb518e29d3d 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java @@ -5,59 +5,113 @@ import java.util.Iterator; +import org.jspecify.annotations.Nullable; /** - * This interface has to be implemented by a Class providing a persistent Map. + * An immutable data structure mapping keys to values. The map is not modified by any operation + * after creation. + * + * @param the type of keys for this map + * @param the type of contained mapped values */ -public interface ImmutableMap +public interface ImmutableMap extends Iterable> { /** - * adds a mapping {@code } to the Map (old map is not modified) if key exists old entry - * has to - * be removed + * Adds a mapping {@code } to the map (old map is not modified) * + * If the key exists, the old entry will be overwritten. + * + * @param key the key with which the specified value is to be associated + * @param value the value to be associated with the specified key * @return the new mapping */ ImmutableMap put(S key, T value); - /** @return value of type that is mapped by key of type */ - T get(S key); + /** + * Retrieves the value mapped to the specified key in this map. + * + * @param key the key whose associated value is to be returned + * @return the value to which the specified key is mapped, or {@code null} if this map contains + * no mapping for the key + */ + @Nullable T get(S key); - /** @return number of entries as int */ + /** + * Returns the number of entries in this map. + * + * @return the number of entries in this map + */ int size(); - /** @return true iff the map is empty */ + /** + * Returns {@code true} if this map contains no entries. + * + * @return {@code true} if this map contains no entries + */ boolean isEmpty(); - /** @return true iff the map includes key */ + /** + * Returns {@code true} if this map contains a mapping for the specified key. + * + * @param key the key whose presence in this map is to be tested + * @return {@code true} if this map contains a mapping for the specified key + */ boolean containsKey(S key); - /** @return true iff the map includes value */ + /** + * Returns {@code true} if this map maps one or more keys to the specified value. + * + * Comparison is modulo {@link Object#equals(Object)}. + * + * @param value the value whose presence in this map is to be tested + * @return {@code true} if this map maps one or more keys to the specified value + */ boolean containsValue(T value); /** - * removes mapping (key,...) from map + * Removes the mapping for a key from this map if it is present. * - * @return the new map (the same if key is not in the map) + * @param key the key whose mapping is to be removed from the map + * @return the new map (the same if the key is not in the map) */ ImmutableMap remove(S key); /** - * removes all mappings (...,value) from map + * Removes all mappings for the specified value from this map. + * + * Comparison is modulo {@link Object#equals(Object)}. * - * @return the new map (the same if value is not mapped) + * @param value the value whose mappings are to be removed from the map + * @return the new map (the same if the value is not mapped) */ ImmutableMap removeAll(T value); - /** @return iterator about all keys */ + /** + * Returns an iterator over the keys in this map. + * + * The order is most recent first. + * + * @return an iterator over the keys in this map + */ Iterator keyIterator(); - /** @return iterator about all values */ + /** + * Returns an iterator over the values in this map. + * + * If a value is contained multiple times, it will be returned multiple times. + * The order is most recent first. + * + * @return an iterator over the values in this map + */ Iterator valueIterator(); - /** @return iterator for entries */ - Iterator> iterator(); - + /** + * Returns an iterator over the entries in this map. + * The order is most recent first. + * + * @return an iterator over the entries in this map + */ + Iterator> iterator(); } diff --git a/key.util/src/main/java/org/key_project/util/collection/Immutables.java b/key.util/src/main/java/org/key_project/util/collection/Immutables.java index 9dc51e9218e..03e7aca6e37 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Immutables.java +++ b/key.util/src/main/java/org/key_project/util/collection/Immutables.java @@ -210,7 +210,7 @@ public static ImmutableList createListFrom(Iterable iterable public static ImmutableList map( ImmutableList ts, Function function) { // This must be a loop. A tail recursive implementation is not optimised - // by the compiler and quickly leads to a stack overlow. + // by the compiler and quickly leads to a stack overflow. ImmutableList acc = ImmutableSLList.nil(); while (!ts.isEmpty()) { T hd = ts.head(); From d437992cd5a6cef2de5469e85507eea12cf45bc7 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 26 Aug 2024 21:41:49 +0200 Subject: [PATCH 20/46] Adding a test case for immutable maps. Thanks, co-pilot. --- .../collection/DefaultImmutableMapTest.java | 124 ++++++++++++++++++ 1 file changed, 124 insertions(+) create mode 100644 key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java diff --git a/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java b/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java new file mode 100644 index 00000000000..760671b9905 --- /dev/null +++ b/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java @@ -0,0 +1,124 @@ +/* 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 org.key_project.util.collection; + +import java.util.Iterator; + +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.*; + +public class DefaultImmutableMapTest { + + private ImmutableMap map; + + @BeforeEach + public void setUp() { + map = DefaultImmutableMap.nilMap(); + } + + @Test + public void testPutAndGet() { + map = map.put("one", 1); + assertEquals(1, map.get("one")); + } + + @Test + public void testSize() { + assertEquals(0, map.size()); + map = map.put("one", 1); + assertEquals(1, map.size()); + map = map.put("two", 1); + assertEquals(2, map.size()); + map = map.put("two", 2); + assertEquals(2, map.size()); + map = map.put("one", 3); + assertEquals(2, map.size()); + } + + @Test + public void testIsEmpty() { + assertTrue(map.isEmpty()); + map = map.put("one", 1); + assertFalse(map.isEmpty()); + } + + @Test + public void testContainsKey() { + map = map.put("one", 1); + assertTrue(map.containsKey("one")); + assertFalse(map.containsKey("two")); + } + + @Test + public void testContainsValue() { + map = map.put("one", 1); + assertTrue(map.containsValue(1)); + assertFalse(map.containsValue(2)); + } + + @Test + public void testRemove() { + map = map.put("one", 1); + map = map.remove("one"); + assertFalse(map.containsKey("one")); + assertEquals(0, map.size()); + + map = DefaultImmutableMap.nilMap(); + map = map.put("one", 1); + map = map.remove("two"); + assertTrue(map.containsKey("one")); + assertEquals(1, map.size()); + } + + @Test + public void testRemoveAll() { + map = map.put("one", 1); + map = map.put("two", 1); + map = map.removeAll(1); + assertFalse(map.containsValue(1)); + assertEquals(0, map.size()); + } + + @Test + public void testKeyIterator() { + map = map.put("one", 1); + map = map.put("two", 2); + Iterator iterator = map.keyIterator(); + assertTrue(iterator.hasNext()); + assertEquals("two", iterator.next()); + assertTrue(iterator.hasNext()); + assertEquals("one", iterator.next()); + assertFalse(iterator.hasNext()); + } + + @Test + public void testValueIterator() { + map = map.put("one", 1); + map = map.put("two", 2); + Iterator iterator = map.valueIterator(); + assertTrue(iterator.hasNext()); + assertEquals(2, iterator.next()); + assertTrue(iterator.hasNext()); + assertEquals(1, iterator.next()); + assertFalse(iterator.hasNext()); + } + + @Test + public void testIterator() { + map = map.put("one", 1); + map = map.put("two", 2); + Iterator> iterator = map.iterator(); + assertTrue(iterator.hasNext()); + ImmutableMapEntry entry = iterator.next(); + assertEquals("two", entry.key()); + assertEquals(2, entry.value()); + assertTrue(iterator.hasNext()); + entry = iterator.next(); + assertEquals("one", entry.key()); + assertEquals(1, entry.value()); + assertFalse(iterator.hasNext()); + } +} From b8fa5bbb87aa4f2b76f20f196293ca498d7498ea Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Mon, 26 Aug 2024 22:46:22 +0200 Subject: [PATCH 21/46] some more NonNull annotations --- .../util/collection/ImmutableArray.java | 35 ++++++++----------- .../util/collection/ImmutableSLList.java | 3 +- 2 files changed, 16 insertions(+), 22 deletions(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index e102f797603..2b6f9c7ef5e 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -4,24 +4,17 @@ package org.key_project.util.collection; import java.lang.reflect.Array; -import java.util.ArrayList; -import java.util.Arrays; -import java.util.Collection; -import java.util.Iterator; -import java.util.List; +import java.util.*; import java.util.stream.Stream; import java.util.stream.StreamSupport; +import org.jspecify.annotations.Nullable; import org.key_project.util.Strings; import org.jspecify.annotations.NonNull; -@SuppressWarnings("nullness") -public class ImmutableArray implements java.lang.Iterable, java.io.Serializable { +public class ImmutableArray implements java.lang.Iterable, java.io.Serializable { - /** - * - */ private static final long serialVersionUID = -9041545065066866250L; private final S[] content; @@ -41,13 +34,14 @@ public ImmutableArray() { */ @SuppressWarnings("unchecked") public ImmutableArray(S... arr) { - content = (S[]) Array.newInstance(arr.getClass().getComponentType(), arr.length); - System.arraycopy(arr, 0, content, 0, arr.length); + this(arr, 0, arr.length); } @SuppressWarnings("unchecked") public ImmutableArray(S[] arr, int lower, int upper) { - content = (S[]) Array.newInstance(arr.getClass().getComponentType(), upper - lower); + Class arrayClass = arr.getClass(); + assert arrayClass.isArray() : "@AssumeAssertion(nullness): arrayClass is an array"; + content = (S[]) Array.newInstance(arrayClass.getComponentType(), upper - lower); System.arraycopy(arr, lower, content, 0, upper - lower); } @@ -101,7 +95,7 @@ public final boolean isEmpty() { public boolean contains(S op) { for (S el : content) { - if (el.equals(op)) { + if (Objects.equals(el, op)) { return true; } } @@ -117,7 +111,9 @@ public boolean contains(S op) { public T[] toArray(T[] array) { T[] result; if (array.length < size()) { - result = (T[]) Array.newInstance(array.getClass().getComponentType(), content.length); + Class arrayClass = array.getClass(); + assert arrayClass.isArray() : "@AssumeAssertion(nullness): arrayClass is an array"; + result = (T[]) Array.newInstance(arrayClass.getComponentType(), content.length); } else { result = array; } @@ -131,15 +127,14 @@ public int hashCode() { } @Override - @SuppressWarnings("unchecked") - public boolean equals(Object o) { + public boolean equals(@Nullable Object o) { if (o == this) { return true; } - final S[] cmp; + final @Nullable Object @Nullable [] cmp; if (o instanceof ImmutableArray) { - cmp = ((ImmutableArray) o).content; + cmp = ((ImmutableArray) o).content; } else { return false; } @@ -149,7 +144,7 @@ public boolean equals(Object o) { } for (int i = 0; i < content.length; i++) { - if (!content[i].equals(cmp[i])) { + if (!Objects.equals(content[i], cmp[i])) { return false; } } diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java index 7e52f453ee0..fbcbf440766 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java @@ -91,14 +91,13 @@ public ImmutableList reverse() { * Convert the list to a Java array (O(n)) */ @Override - @SuppressWarnings("nullness") public S[] toArray(Class type) { S[] result = (S[]) Array.newInstance(type, size()); ImmutableList rest = this; for (int i = 0, sz = size(); i < sz; i++) { // @ assert !rest.isEmpty(); T head = rest.head(); - result[i] = (S) type.cast(head); + result[i] = type.cast(head); rest = rest.tail(); } return result; From 5ab92c4d715f8efe2ce5a30a502bfe1ae456f278 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Wed, 28 Aug 2024 23:09:32 +0200 Subject: [PATCH 22/46] repairing a nullness type error --- .../java/org/key_project/util/collection/ImmutableSLList.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java index fbcbf440766..c6bc12ed41b 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableSLList.java @@ -97,7 +97,8 @@ public ImmutableList reverse() { for (int i = 0, sz = size(); i < sz; i++) { // @ assert !rest.isEmpty(); T head = rest.head(); - result[i] = type.cast(head); + // Somehow the nullness checker needs this cast to be explicit. + result[i] = (S)type.cast(head); rest = rest.tail(); } return result; From 370ac99488767f22a564cfb6475856ada6fe55d9 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Wed, 28 Aug 2024 23:28:31 +0200 Subject: [PATCH 23/46] type annotations for test cases --- key.util/build.gradle | 2 +- .../collection/DefaultImmutableMapTest.java | 18 ++++++++++++++++-- .../TestMapAsListFromIntegerToString.java | 8 ++++++-- 3 files changed, 23 insertions(+), 5 deletions(-) diff --git a/key.util/build.gradle b/key.util/build.gradle index 25700d3ec91..59f50b8398f 100644 --- a/key.util/build.gradle +++ b/key.util/build.gradle @@ -12,7 +12,7 @@ checkerFramework { extraJavacArgs = [ "-AonlyDefs=^org\\.key_project\\.util", "-Xmaxerrs", "10000", - "-Astubs=$projectDir/src/main/checkerframework:permit-nullness-assertion-exception.astub", + "-Astubs=$projectDir/src/main/checkerframework:permit-nullness-assertion-exception.astub:checker.jar/junit-assertions.astub", "-AstubNoWarnIfNotFound", "-Werror", "-Aversion", diff --git a/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java b/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java index 760671b9905..e595635ff13 100644 --- a/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java +++ b/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java @@ -5,6 +5,8 @@ import java.util.Iterator; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; +import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; @@ -12,7 +14,7 @@ public class DefaultImmutableMapTest { - private ImmutableMap map; + private @MonotonicNonNull ImmutableMap map; @BeforeEach public void setUp() { @@ -21,12 +23,16 @@ public void setUp() { @Test public void testPutAndGet() { + assertNotNull(map); map = map.put("one", 1); - assertEquals(1, map.get("one")); + Integer one = map.get("one"); + assertNotNull(one); + assertEquals(1, one); } @Test public void testSize() { + assertNotNull(map); assertEquals(0, map.size()); map = map.put("one", 1); assertEquals(1, map.size()); @@ -40,6 +46,7 @@ public void testSize() { @Test public void testIsEmpty() { + assertNotNull(map); assertTrue(map.isEmpty()); map = map.put("one", 1); assertFalse(map.isEmpty()); @@ -47,6 +54,7 @@ public void testIsEmpty() { @Test public void testContainsKey() { + assertNotNull(map); map = map.put("one", 1); assertTrue(map.containsKey("one")); assertFalse(map.containsKey("two")); @@ -54,6 +62,7 @@ public void testContainsKey() { @Test public void testContainsValue() { + assertNotNull(map); map = map.put("one", 1); assertTrue(map.containsValue(1)); assertFalse(map.containsValue(2)); @@ -61,6 +70,7 @@ public void testContainsValue() { @Test public void testRemove() { + assertNotNull(map); map = map.put("one", 1); map = map.remove("one"); assertFalse(map.containsKey("one")); @@ -75,6 +85,7 @@ public void testRemove() { @Test public void testRemoveAll() { + assertNotNull(map); map = map.put("one", 1); map = map.put("two", 1); map = map.removeAll(1); @@ -84,6 +95,7 @@ public void testRemoveAll() { @Test public void testKeyIterator() { + assertNotNull(map); map = map.put("one", 1); map = map.put("two", 2); Iterator iterator = map.keyIterator(); @@ -96,6 +108,7 @@ public void testKeyIterator() { @Test public void testValueIterator() { + assertNotNull(map); map = map.put("one", 1); map = map.put("two", 2); Iterator iterator = map.valueIterator(); @@ -108,6 +121,7 @@ public void testValueIterator() { @Test public void testIterator() { + assertNotNull(map); map = map.put("one", 1); map = map.put("two", 2); Iterator> iterator = map.iterator(); diff --git a/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java b/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java index 7d492d19e3a..5f42b25a526 100644 --- a/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java +++ b/key.util/src/test/java/org/key_project/util/testcase/collection/TestMapAsListFromIntegerToString.java @@ -86,9 +86,13 @@ public void testMapCanContainSameValueWithDifferentKeys() { // another key before Integer hundred = 100; map = map.put(hundred, entryStr[1]); - assertSame(map.get(hundred), entryStr[1], + String valHundred = map.get(hundred); + assertNotNull(valHundred); + assertSame(valHundred, entryStr[1], entryStr[1] + " is not mapped to the newer key 100"); - assertSame(map.get(entryInt[1]), entryStr[1], + String val1 = map.get(entryInt[1]); + assertNotNull(val1); + assertSame(val1, entryStr[1], entryStr[1] + " is not mapped to the older key " + entryInt[1]); } From 215e93ce6bdb67ac1ceada5fdd4728261856a21c Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Wed, 28 Aug 2024 23:56:07 +0200 Subject: [PATCH 24/46] Missed nonnullness of map keys. --- .../java/org/key_project/util/collection/ImmutableMap.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java index eb518e29d3d..a5d0476738a 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java @@ -5,6 +5,7 @@ import java.util.Iterator; +import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; /** @@ -14,7 +15,7 @@ * @param the type of keys for this map * @param the type of contained mapped values */ -public interface ImmutableMap +public interface ImmutableMap extends Iterable> { /** From 1aa4052e3657c4f2ca2c3cdfb2102572bf918774 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Thu, 29 Aug 2024 10:12:08 +0200 Subject: [PATCH 25/46] applied spotless --- .../java/org/key_project/util/collection/ImmutableArray.java | 5 +++-- .../java/org/key_project/util/collection/ImmutableMap.java | 3 ++- .../org/key_project/util/collection/ImmutableSLList.java | 2 +- .../key_project/util/collection/DefaultImmutableMapTest.java | 1 - 4 files changed, 6 insertions(+), 5 deletions(-) diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java index 2b6f9c7ef5e..9f4a0bf8ff0 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableArray.java @@ -8,12 +8,13 @@ import java.util.stream.Stream; import java.util.stream.StreamSupport; -import org.jspecify.annotations.Nullable; import org.key_project.util.Strings; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; -public class ImmutableArray implements java.lang.Iterable, java.io.Serializable { +public class ImmutableArray + implements java.lang.Iterable, java.io.Serializable { private static final long serialVersionUID = -9041545065066866250L; diff --git a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java index a5d0476738a..6fea252ef06 100644 --- a/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java +++ b/key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java @@ -36,7 +36,8 @@ public interface ImmutableMap reverse() { // @ assert !rest.isEmpty(); T head = rest.head(); // Somehow the nullness checker needs this cast to be explicit. - result[i] = (S)type.cast(head); + result[i] = (S) type.cast(head); rest = rest.tail(); } return result; diff --git a/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java b/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java index e595635ff13..fe9520c2400 100644 --- a/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java +++ b/key.util/src/test/java/org/key_project/util/collection/DefaultImmutableMapTest.java @@ -6,7 +6,6 @@ import java.util.Iterator; import org.checkerframework.checker.nullness.qual.MonotonicNonNull; -import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; From 8a8fbfaf9cb8f5be320387d5b89678786de82318 Mon Sep 17 00:00:00 2001 From: Mattias Ulbrich Date: Thu, 29 Aug 2024 10:17:58 +0200 Subject: [PATCH 26/46] improving code for heatmap activation avoiding double paint refining types Authored mainly by Wolfram --- .../java/de/uka/ilkd/key/gui/MainWindow.java | 2 +- .../key/gui/actions/HeatmapToggleAction.java | 11 +++---- .../uka/ilkd/key/gui/nodeviews/MainFrame.java | 33 +++++++++---------- 3 files changed, 21 insertions(+), 25 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 31aa9b0eeb2..3af00c689a7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1223,7 +1223,7 @@ private synchronized void updateSequentView() { } Runnable sequentUpdater = () -> { - mainFrame.setContent(newSequentView); + mainFrame.setSequentView(newSequentView); // always does printSequent if on the event thread sequentViewSearchBar.setSequentView(newSequentView); }; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java index 87a8998dee4..762d119aa04 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java @@ -67,13 +67,10 @@ public void actionPerformed(ActionEvent e) { vs.setHeatmapOptions(!vs.isShowHeatmap(), vs.isHeatmapSF(), vs.isHeatmapNewest(), vs.getMaxAgeForHeatmap()); // this updates the heatmap highlights - mainWindow.getCurrentGoalView().getHighlighter().removeAllHighlights(); - mainWindow.getCurrentGoalView().printSequent(); - Component component = mainWindow.getMainFrame().getContent(); - if (component instanceof SequentView) { - SequentView seqView = (SequentView) component; - seqView.getHighlighter().removeAllHighlights(); - seqView.printSequent(); + SequentView sequentView = mainWindow.getMainFrame().getSequentView(); + if (sequentView != null) { + sequentView.getHighlighter().removeAllHighlights(); + sequentView.printSequent(); } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java index 61b87ee7905..e71e60db09a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java @@ -26,15 +26,15 @@ public final class MainFrame extends JPanel { private static final long serialVersionUID = -2412537422601138379L; private final JScrollPane scrollPane = new JScrollPane(); - private Component content; + private SequentView sequentView; private boolean showTacletInfo = false; - public Component setContent(Component component) { - Component oldContent = content; - content = component; - if (component instanceof SequentView sequentView) { + public void setSequentView(SequentView component) { + SequentView oldSequentView = sequentView; + sequentView = component; + if (component != null) { Point oldSequentViewPosition = scrollPane.getViewport().getViewPosition(); - scrollPane.setViewportView(new SequentViewPanel(sequentView)); + scrollPane.setViewportView(new SequentViewPanel(component)); scrollPane.getViewport().setViewPosition(oldSequentViewPosition); setShowTacletInfo(showTacletInfo); @@ -42,11 +42,10 @@ public Component setContent(Component component) { scrollPane.setViewportView(component); } - if (oldContent instanceof SequentView) { - ((SequentView) oldContent).removeUserSelectionHighlight(); + if (oldSequentView != null) { + oldSequentView.removeUserSelectionHighlight(); } - return oldContent; } public MainFrame(final MainWindow mainWindow, EmptySequent emptySequent) { @@ -58,8 +57,8 @@ public MainFrame(final MainWindow mainWindow, EmptySequent emptySequent) { @Override public void mouseClicked(MouseEvent e) { - if (content != null) { - for (MouseListener listener : content.getMouseListeners()) { + if (sequentView != null) { + for (MouseListener listener : sequentView.getMouseListeners()) { if (listener instanceof SequentViewInputListener) { listener.mouseClicked(e); } @@ -72,8 +71,8 @@ public void mouseClicked(MouseEvent e) { @Override public void ancestorRemoved(AncestorEvent event) { - if (content instanceof SequentView) { - ((SequentView) content).removeUserSelectionHighlight(); + if (sequentView != null) { + sequentView.removeUserSelectionHighlight(); } } @@ -90,13 +89,13 @@ public void ancestorAdded(AncestorEvent event) {} getActionMap().put("copy", new CopyToClipboardAction(mainWindow)); setLayout(new BorderLayout()); add(scrollPane); - setContent(emptySequent); + setSequentView(emptySequent); } public void setShowTacletInfo(boolean showTacletInfo) { this.showTacletInfo = showTacletInfo; - if (content instanceof InnerNodeView view) { + if (sequentView instanceof InnerNodeView view) { view.tacletInfo.setVisible(this.showTacletInfo); } } @@ -114,7 +113,7 @@ public void scrollTo(int y) { scrollPane.getVerticalScrollBar().setValue(y); } - public Component getContent() { - return content; + public SequentView getSequentView() { + return sequentView; } } From 1f02a56a5cd8e2d4c93cff2967370c84a12be45b Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 1 Aug 2024 20:50:28 +0000 Subject: [PATCH 27/46] Bump the gradle-deps group with 6 updates Bumps the gradle-deps group with 6 updates: | Package | From | To | | --- | --- | --- | | [org.jspecify:jspecify](https://github.com/jspecify/jspecify) | `0.3.0` | `1.0.0` | | [io.github.eisop:checker-qual](https://github.com/eisop/checker-framework) | `3.42.0-eisop3` | `3.42.0-eisop4` | | [io.github.eisop:checker-util](https://github.com/eisop/checker-framework) | `3.42.0-eisop3` | `3.42.0-eisop4` | | [io.github.eisop:checker](https://github.com/eisop/checker-framework) | `3.42.0-eisop3` | `3.42.0-eisop4` | | org.checkerframework | `0.6.41` | `0.6.43` | | [com.miglayout:miglayout-swing](https://github.com/mikaelgrev/miglayout) | `11.3` | `11.4` | Updates `org.jspecify:jspecify` from 0.3.0 to 1.0.0 - [Release notes](https://github.com/jspecify/jspecify/releases) - [Commits](https://github.com/jspecify/jspecify/compare/v0.3.0...v1.0.0) Updates `io.github.eisop:checker-qual` from 3.42.0-eisop3 to 3.42.0-eisop4 - [Release notes](https://github.com/eisop/checker-framework/releases) - [Changelog](https://github.com/eisop/checker-framework/blob/master/docs/CHANGELOG.md) - [Commits](https://github.com/eisop/checker-framework/compare/checker-framework-3.42.0-eisop3...checker-framework-3.42.0-eisop4) Updates `io.github.eisop:checker-util` from 3.42.0-eisop3 to 3.42.0-eisop4 - [Release notes](https://github.com/eisop/checker-framework/releases) - [Changelog](https://github.com/eisop/checker-framework/blob/master/docs/CHANGELOG.md) - [Commits](https://github.com/eisop/checker-framework/compare/checker-framework-3.42.0-eisop3...checker-framework-3.42.0-eisop4) Updates `io.github.eisop:checker` from 3.42.0-eisop3 to 3.42.0-eisop4 - [Release notes](https://github.com/eisop/checker-framework/releases) - [Changelog](https://github.com/eisop/checker-framework/blob/master/docs/CHANGELOG.md) - [Commits](https://github.com/eisop/checker-framework/compare/checker-framework-3.42.0-eisop3...checker-framework-3.42.0-eisop4) Updates `io.github.eisop:checker-util` from 3.42.0-eisop3 to 3.42.0-eisop4 - [Release notes](https://github.com/eisop/checker-framework/releases) - [Changelog](https://github.com/eisop/checker-framework/blob/master/docs/CHANGELOG.md) - [Commits](https://github.com/eisop/checker-framework/compare/checker-framework-3.42.0-eisop3...checker-framework-3.42.0-eisop4) Updates `io.github.eisop:checker` from 3.42.0-eisop3 to 3.42.0-eisop4 - [Release notes](https://github.com/eisop/checker-framework/releases) - [Changelog](https://github.com/eisop/checker-framework/blob/master/docs/CHANGELOG.md) - [Commits](https://github.com/eisop/checker-framework/compare/checker-framework-3.42.0-eisop3...checker-framework-3.42.0-eisop4) Updates `org.checkerframework` from 0.6.41 to 0.6.43 Updates `com.miglayout:miglayout-swing` from 11.3 to 11.4 - [Release notes](https://github.com/mikaelgrev/miglayout/releases) - [Changelog](https://github.com/mikaelgrev/miglayout/blob/master/release.txt) - [Commits](https://github.com/mikaelgrev/miglayout/compare/v11.3...v11.4) --- updated-dependencies: - dependency-name: org.jspecify:jspecify dependency-type: direct:production update-type: version-update:semver-major dependency-group: gradle-deps - dependency-name: io.github.eisop:checker-qual dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: io.github.eisop:checker-util dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: io.github.eisop:checker dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: io.github.eisop:checker-util dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: io.github.eisop:checker dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.checkerframework dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: com.miglayout:miglayout-swing dependency-type: direct:production update-type: version-update:semver-minor dependency-group: gradle-deps ... Signed-off-by: dependabot[bot] --- build.gradle | 8 ++++---- key.ncore/build.gradle | 2 +- key.ui/build.gradle | 2 +- key.util/build.gradle | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/build.gradle b/build.gradle index 61364ce00d4..43eb5ac4f0a 100644 --- a/build.gradle +++ b/build.gradle @@ -24,7 +24,7 @@ plugins { id "com.diffplug.spotless" version "6.25.0" // EISOP Checker Framework - id "org.checkerframework" version "0.6.41" + id "org.checkerframework" version "0.6.43" } // Configure this project for use inside IntelliJ: @@ -81,9 +81,9 @@ subprojects { //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0' //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0' - compileOnly("org.jspecify:jspecify:0.3.0") - testCompileOnly("org.jspecify:jspecify:0.3.0") - def eisop_version = "3.42.0-eisop3" + compileOnly("org.jspecify:jspecify:1.0.0") + testCompileOnly("org.jspecify:jspecify:1.0.0") + def eisop_version = "3.42.0-eisop4" compileOnly "io.github.eisop:checker-qual:$eisop_version" compileOnly "io.github.eisop:checker-util:$eisop_version" testCompileOnly "io.github.eisop:checker-qual:$eisop_version" diff --git a/key.ncore/build.gradle b/key.ncore/build.gradle index 05c37191647..04eabab0a84 100644 --- a/key.ncore/build.gradle +++ b/key.ncore/build.gradle @@ -7,7 +7,7 @@ configurations { } dependencies { api project(':key.util') - implementation 'org.jspecify:jspecify:0.3.0' + implementation 'org.jspecify:jspecify:1.0.0' } tasks.withType(Test) { diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 93edbc44890..1d5b7172224 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -20,7 +20,7 @@ dependencies { implementation project(":key.core.symbolic_execution") implementation project(":key.removegenerics") - api 'com.miglayout:miglayout-swing:11.3' + api 'com.miglayout:miglayout-swing:11.4' //logging implementation used by the slf4j implementation 'ch.qos.logback:logback-classic:1.5.6' diff --git a/key.util/build.gradle b/key.util/build.gradle index 59f50b8398f..382a103b60a 100644 --- a/key.util/build.gradle +++ b/key.util/build.gradle @@ -1,7 +1,7 @@ description "Utility library of the key-project" dependencies { - implementation("org.jspecify:jspecify:0.3.0") + implementation("org.jspecify:jspecify:1.0.0") } checkerFramework { From 4121eccca50a8850536b02762c3cc639b515c164 Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Fri, 30 Aug 2024 14:40:47 +0200 Subject: [PATCH 28/46] Fox copyright year --- key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java b/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java index edc69202cbf..ad764324f60 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java @@ -10,6 +10,6 @@ public interface KeYConstants { KeYResourceManager.getManager().getVersion() + " (internal: " + INTERNAL_VERSION + ")"; String COPYRIGHT = UnicodeHelper.COPYRIGHT + " Copyright 2001" - + UnicodeHelper.ENDASH + "2023 " + "Karlsruhe Institute of Technology, " + + UnicodeHelper.ENDASH + "2024 " + "Karlsruhe Institute of Technology, " + "Chalmers University of Technology, and Technische Universit\u00e4t Darmstadt"; } From 6f0b5ae359d1a9d3433aed2eabe719896ecc3c4f Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 30 Aug 2024 14:52:34 +0200 Subject: [PATCH 29/46] fix for visual bug with overlapping/unreadable text in color settings --- .../uka/ilkd/key/gui/colors/ColorSettingsProvider.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java index 89293e55cac..97358372bc3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java @@ -75,7 +75,10 @@ public Component getTableCellRendererComponent(JTable table, Object value, } private Icon drawRect(Color c, int size) { - BufferedImage bi = new BufferedImage(size, size, BufferedImage.TYPE_INT_RGB); + /* Not sure if the alpha channel is used. Highlights seem to be blended correctly + * even if the color is not transparent at all. However, make sure to use ARGB to + * avoid black icons here ... */ + BufferedImage bi = new BufferedImage(size, size, BufferedImage.TYPE_INT_ARGB); Graphics g = bi.getGraphics(); g.setColor(c); g.fillRect(0, 0, size, size); @@ -167,6 +170,10 @@ class HexColorCellEditor extends DefaultCellEditor { HexColorCellEditor(JTextField textField) { super(textField); + + // this is somehow important to avoid visual artifacts such as overlapping text: + textField.setOpaque(false); + textField.addActionListener(e -> stopCellEditing()); textField.getDocument().addDocumentListener(new DocumentListener() { @Override From 76f163e5d8bf764aa3da46e64d71936a2d01cdf8 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 30 Aug 2024 19:38:33 +0200 Subject: [PATCH 30/46] generating ProofTree tooltips lazily, options to disable them completely --- .../uka/ilkd/key/settings/ViewSettings.java | 13 ++++ .../java/de/uka/ilkd/key/gui/MainWindow.java | 7 +++ .../actions/ToggleProofTreeTooltipAction.java | 58 +++++++++++++++++ .../ProofTreeSettingsMenuFactory.java | 21 +++++++ .../ilkd/key/gui/prooftree/ProofTreeView.java | 62 +++++++++++++++---- 5 files changed, 149 insertions(+), 12 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java index 9fa5efc461f..1acbc33aed4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java @@ -112,6 +112,9 @@ public class ViewSettings extends AbstractPropertiesSettings { /** this setting enables/disables tool tips in the source view */ private static final String SOURCE_VIEW_TOOLTIP = "SourceViewTooltips"; + /** this setting enables/disables tool tips in the proof tree */ + private static final String PROOF_TREE_TOOLTIP = "ProofTreeTooltips"; + private static final String HIGHLIGHT_ORIGIN = "HighlightOrigin"; /** * @@ -202,6 +205,8 @@ public class ViewSettings extends AbstractPropertiesSettings { createBooleanProperty(SEQUENT_VIEW_TOOLTIP, true); private final PropertyEntry showSourceViewTooltips = createBooleanProperty(SOURCE_VIEW_TOOLTIP, true); + private final PropertyEntry showProofTreeTooltips = + createBooleanProperty(PROOF_TREE_TOOLTIP, true); private final PropertyEntry highlightOrigin = createBooleanProperty(HIGHLIGHT_ORIGIN, true); private final PropertyEntry> clutterRules = @@ -539,6 +544,14 @@ public void setShowSourceViewTooltips(boolean showSourceViewTooltips) { this.showSourceViewTooltips.set(showSourceViewTooltips); } + public boolean isShowProofTreeTooltips() { + return showProofTreeTooltips.get(); + } + + public void setShowProofTreeTooltips(boolean showProofTreeTooltips) { + this.showProofTreeTooltips.set(showProofTreeTooltips); + } + public double getUIFontSizeFactor() { return uiFontSizeFactor.get(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 4863623dce8..73d16e31bcd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -164,6 +164,8 @@ public final class MainWindow extends JFrame { new ToggleSequentViewTooltipAction(this); private final ToggleSourceViewTooltipAction toggleSourceViewTooltipAction = new ToggleSourceViewTooltipAction(this); + private final ToggleProofTreeTooltipAction toogleProofTreeTooltipAction = + new ToggleProofTreeTooltipAction(this); private final TermLabelMenu termLabelMenu; private boolean frozen = false; /** @@ -930,6 +932,7 @@ private JMenu createViewMenu() { view.add(new JCheckBoxMenuItem(hidePackagePrefixToggleAction)); view.add(new JCheckBoxMenuItem(toggleSequentViewTooltipAction)); view.add(new JCheckBoxMenuItem(toggleSourceViewTooltipAction)); + view.add(new JCheckBoxMenuItem(toogleProofTreeTooltipAction)); view.addSeparator(); { @@ -1457,6 +1460,10 @@ public boolean isShowTacletInfo() { return mainFrame.isShowTacletInfo(); } + public void setShowProofTreeTooltip(Object source) { + toogleProofTreeTooltipAction.actionPerformed(new ActionEvent(proofTreeView, ActionEvent.ACTION_PERFORMED, "")); + } + public AutoModeAction getAutoModeAction() { return autoModeAction; } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java new file mode 100644 index 00000000000..4d89b9a5a74 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java @@ -0,0 +1,58 @@ +/* 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.gui.actions; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.ViewSettings; + +import javax.swing.*; +import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; + +/** + * Toggles the tooltips of the proof tree. + * + * @author Wolfram Pfeifer + */ +public class ToggleProofTreeTooltipAction extends MainWindowAction { + /** This action's name. */ + public static final String NAME = "Show Tooltips in Proof Tree"; + + /** This action's tooltip. */ + public static final String TOOL_TIP = "If ticked, moving the mouse over a node in the proof" + + " tree will show a tooltip with additional information."; + + /** + * Create a new action. + * + * @param mainWindow the main window. + */ + public ToggleProofTreeTooltipAction(MainWindow mainWindow) { + super(mainWindow); + setName(NAME); + setTooltip(TOOL_TIP); + // Listens to changes to the view settings to call {@link #updateSelectedState()}. + PropertyChangeListener viewSettingsListener = e -> updateSelectedState(); + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() + .addPropertyChangeListener(viewSettingsListener); + updateSelectedState(); + } + + /** + * Updates the state of this action according to {@link ViewSettings#isShowProofTreeTooltips()} + */ + protected void updateSelectedState() { + final boolean setting = + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isShowProofTreeTooltips(); + setSelected(setting); + } + + @Override + public void actionPerformed(ActionEvent e) { + boolean selected = ((JCheckBoxMenuItem) e.getSource()).isSelected(); + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() + .setShowProofTreeTooltips(selected); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java index 9e83ad4c04e..de237069ad5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java @@ -15,6 +15,7 @@ import bibliothek.gui.dock.common.action.CButton; import bibliothek.gui.dock.common.action.CCheckBox; import bibliothek.gui.dock.common.action.CMenu; +import de.uka.ilkd.key.settings.ProofIndependentSettings; import static de.uka.ilkd.key.gui.prooftree.ProofTreePopupFactory.ICON_SIZE; @@ -39,6 +40,7 @@ public static CAction create(ProofTreeView view) { menu.addSeparator(); menu.add(createExpandOSSToggle(view)); + menu.add(createTooltipToggle()); menu.add(createTacletInfoToggle()); return menu; }; @@ -134,6 +136,25 @@ protected void changed() { return check; } + private static CCheckBox createTooltipToggle() { + CCheckBox check = new CCheckBox() { + @Override + protected void changed() { + /* The ToogleProofTreeTooltipAction (in the View menu) is updated via + * PropertyChangeListener, no manual update needed! */ + final boolean selected = isSelected(); + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() + .setShowProofTreeTooltips(selected); + } + }; + check.setText("Show Tooltips"); + // No PropertyChangeListener needed, since the menu is always freshly generated. + final boolean setting = + ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings().isShowProofTreeTooltips(); + check.setSelected(setting); + return check; + } + /** * The checkbox used in the proof tree settings. * diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index 5ccd3abc9fc..ac4bd402939 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -176,6 +176,33 @@ public ProofTreeView() { delegateView = new JTree(new DefaultMutableTreeNode("No proof loaded")) { private static final long serialVersionUID = 6555955929759162324L; + @Override + public String getToolTipText(MouseEvent mouseEvent) { + /* For performance reasons, we want to make sure that the tooltips are only rendered + * when they are really needed. Therefore, they are now lazily generated and can + * also be disabled completely. */ + if (!ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() + .isShowProofTreeTooltips()) { + return null; + } + TreePath path = delegateView.getPathForLocation(mouseEvent.getX(), + mouseEvent.getY()); + if (path == null) { + return null; + } + var last = path.getLastPathComponent(); + + if (last instanceof GUIAbstractTreeNode node) { + + Style style = renderer.initStyleForNode(node); + if (style.tooltip != null) { + return renderTooltip(style.tooltip); + } + } + + return super.getToolTipText(mouseEvent); + } + @Override public void setFont(Font font) { iconHeight = font.getSize(); @@ -1243,16 +1270,7 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean super.getTreeCellRendererComponent(tree, value, sel, expanded, leaf, row, hasFocus); - Style style = new Style(); - style.foreground = getForeground(); - style.background = getBackground(); - // Normalize whitespace - style.text = value.toString().replaceAll("\\s+", " "); - style.border = null; - style.tooltip = new Style.Tooltip(); - style.icon = null; - - stylers.forEach(it -> it.style(style, node)); + Style style = initStyleForNode(node); setForeground(style.foreground); setBackground(style.background); @@ -1265,13 +1283,33 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean } setFont(getFont().deriveFont(Font.PLAIN)); - String tooltip = renderTooltip(style.tooltip); - setToolTipText(tooltip); + // For performance reasons, we render the tooltips now lazily ... + // String tooltip = renderTooltip(style.tooltip); + // setToolTipText(tooltip); setText(style.text); setIcon(style.icon); return this; } + + /** + * Creates a new Style object and fills it for the given node. + * @param node the tree node + * @return the created Style with all the info about the node + */ + public Style initStyleForNode(GUIAbstractTreeNode node) { + Style style = new Style(); + style.foreground = getForeground(); + style.background = getBackground(); + // Normalize whitespace + style.text = node.toString().replaceAll("\\s+", " "); + style.border = null; + style.tooltip = new Style.Tooltip(); + style.icon = null; + + stylers.forEach(it -> it.style(style, node)); + return style; + } } public Node getSelectedNode() { From afab77f4cec52f14a7a70fd5c848170f452a2d85 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Sun, 1 Sep 2024 14:40:10 +0200 Subject: [PATCH 31/46] spotless --- .../de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java index 97358372bc3..bce0647327e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java @@ -75,9 +75,11 @@ public Component getTableCellRendererComponent(JTable table, Object value, } private Icon drawRect(Color c, int size) { - /* Not sure if the alpha channel is used. Highlights seem to be blended correctly + /* + * Not sure if the alpha channel is used. Highlights seem to be blended correctly * even if the color is not transparent at all. However, make sure to use ARGB to - * avoid black icons here ... */ + * avoid black icons here ... + */ BufferedImage bi = new BufferedImage(size, size, BufferedImage.TYPE_INT_ARGB); Graphics g = bi.getGraphics(); g.setColor(c); From 2b9d126f81e6d19036accc4de6c360ef5afc94bc Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Sun, 1 Sep 2024 20:02:08 +0000 Subject: [PATCH 32/46] Bump the gradle-deps group with 8 updates Bumps the gradle-deps group with 8 updates: | Package | From | To | | --- | --- | --- | | org.slf4j:slf4j-api | `2.0.13` | `2.0.16` | | [ch.qos.logback:logback-classic](https://github.com/qos-ch/logback) | `1.5.6` | `1.5.7` | | [org.junit.jupiter:junit-jupiter-api](https://github.com/junit-team/junit5) | `5.10.3` | `5.11.0` | | [org.junit.jupiter:junit-jupiter-params](https://github.com/junit-team/junit5) | `5.10.3` | `5.11.0` | | [org.junit.jupiter:junit-jupiter-engine](https://github.com/junit-team/junit5) | `5.10.3` | `5.11.0` | | [com.miglayout:miglayout-swing](https://github.com/mikaelgrev/miglayout) | `11.4` | `11.4.2` | | [org.antlr:antlr4](https://github.com/antlr/antlr4) | `4.13.1` | `4.13.2` | | [org.antlr:antlr4-runtime](https://github.com/antlr/antlr4) | `4.13.1` | `4.13.2` | Updates `org.slf4j:slf4j-api` from 2.0.13 to 2.0.16 Updates `ch.qos.logback:logback-classic` from 1.5.6 to 1.5.7 - [Commits](https://github.com/qos-ch/logback/compare/v_1.5.6...v_1.5.7) Updates `org.junit.jupiter:junit-jupiter-api` from 5.10.3 to 5.11.0 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.10.3...r5.11.0) Updates `org.junit.jupiter:junit-jupiter-params` from 5.10.3 to 5.11.0 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.10.3...r5.11.0) Updates `org.junit.jupiter:junit-jupiter-engine` from 5.10.3 to 5.11.0 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.10.3...r5.11.0) Updates `com.miglayout:miglayout-swing` from 11.4 to 11.4.2 - [Release notes](https://github.com/mikaelgrev/miglayout/releases) - [Changelog](https://github.com/mikaelgrev/miglayout/blob/master/release.txt) - [Commits](https://github.com/mikaelgrev/miglayout/compare/v11.4...v11.4.2) Updates `org.antlr:antlr4` from 4.13.1 to 4.13.2 - [Release notes](https://github.com/antlr/antlr4/releases) - [Changelog](https://github.com/antlr/antlr4/blob/dev/CHANGES.txt) - [Commits](https://github.com/antlr/antlr4/compare/4.13.1...4.13.2) Updates `org.antlr:antlr4-runtime` from 4.13.1 to 4.13.2 - [Release notes](https://github.com/antlr/antlr4/releases) - [Changelog](https://github.com/antlr/antlr4/blob/dev/CHANGES.txt) - [Commits](https://github.com/antlr/antlr4/compare/4.13.1...4.13.2) --- updated-dependencies: - dependency-name: org.slf4j:slf4j-api dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: ch.qos.logback:logback-classic dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-api dependency-type: direct:production update-type: version-update:semver-minor dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-params dependency-type: direct:production update-type: version-update:semver-minor dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-engine dependency-type: direct:production update-type: version-update:semver-minor dependency-group: gradle-deps - dependency-name: com.miglayout:miglayout-swing dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.antlr:antlr4 dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.antlr:antlr4-runtime dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps ... Signed-off-by: dependabot[bot] --- build.gradle | 14 +++++++------- key.core/build.gradle | 4 ++-- key.ui/build.gradle | 4 ++-- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/build.gradle b/build.gradle index 43eb5ac4f0a..210188b7364 100644 --- a/build.gradle +++ b/build.gradle @@ -74,9 +74,9 @@ subprojects { } dependencies { - implementation("org.slf4j:slf4j-api:2.0.13") - implementation("org.slf4j:slf4j-api:2.0.13") - testImplementation("ch.qos.logback:logback-classic:1.5.6") + implementation("org.slf4j:slf4j-api:2.0.16") + implementation("org.slf4j:slf4j-api:2.0.16") + testImplementation("ch.qos.logback:logback-classic:1.5.7") //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0' //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0' @@ -89,12 +89,12 @@ subprojects { testCompileOnly "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker:$eisop_version" - testImplementation("ch.qos.logback:logback-classic:1.5.6") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.3' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.3' + testImplementation("ch.qos.logback:logback-classic:1.5.7") + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.0' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.0' testImplementation project(':key.util') - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.3' + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.0' } tasks.withType(JavaCompile) { diff --git a/key.core/build.gradle b/key.core/build.gradle index 80e648e785c..054104438c0 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -19,8 +19,8 @@ dependencies { javacc group: 'net.java.dev.javacc', name: 'javacc', version: '4.0' antlr group: 'org.antlr', name: 'antlr', version: '3.5.3' // use ANTLR version 3 - antlr4 "org.antlr:antlr4:4.13.1" - api "org.antlr:antlr4-runtime:4.13.1" + antlr4 "org.antlr:antlr4:4.13.2" + api "org.antlr:antlr4-runtime:4.13.2" //implementation group: 'com.google.guava', name: 'guava', version: '28.1-jre' } diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 1d5b7172224..0636b253181 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -20,10 +20,10 @@ dependencies { implementation project(":key.core.symbolic_execution") implementation project(":key.removegenerics") - api 'com.miglayout:miglayout-swing:11.4' + api 'com.miglayout:miglayout-swing:11.4.2' //logging implementation used by the slf4j - implementation 'ch.qos.logback:logback-classic:1.5.6' + implementation 'ch.qos.logback:logback-classic:1.5.7' api 'org.key-project:docking-frames-common:1.1.3p1' api 'org.key-project:docking-frames-core:1.1.3p1' From 255ff7d9776ed7f3ca949aa16b67161aa7f158d9 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Sun, 1 Sep 2024 20:07:27 +0000 Subject: [PATCH 33/46] Bump the github-actions-deps group with 2 updates Bumps the github-actions-deps group with 2 updates: [gradle/actions](https://github.com/gradle/actions) and [JetBrains/qodana-action](https://github.com/jetbrains/qodana-action). Updates `gradle/actions` from 3.5.0 to 4.0.1 - [Release notes](https://github.com/gradle/actions/releases) - [Commits](https://github.com/gradle/actions/compare/v3.5.0...v4.0.1) Updates `JetBrains/qodana-action` from 2024.1.8 to 2024.1.9 - [Release notes](https://github.com/jetbrains/qodana-action/releases) - [Commits](https://github.com/jetbrains/qodana-action/compare/v2024.1.8...v2024.1.9) --- updated-dependencies: - dependency-name: gradle/actions dependency-type: direct:production update-type: version-update:semver-major dependency-group: github-actions-deps - dependency-name: JetBrains/qodana-action dependency-type: direct:production update-type: version-update:semver-patch dependency-group: github-actions-deps ... Signed-off-by: dependabot[bot] --- .github/workflows/code_quality.yml | 10 +++++----- .github/workflows/gradle-publish.yml | 2 +- .github/workflows/javadoc.yml | 2 +- .github/workflows/nightlydeploy.yml | 2 +- .github/workflows/opttest.yml | 2 +- .github/workflows/tests.yml | 4 ++-- .github/workflows/tests_winmac.yml | 4 ++-- 7 files changed, 13 insertions(+), 13 deletions(-) diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index c6fd0d577c3..a544efa0209 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -20,7 +20,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Build with Gradle run: ./gradlew -DENABLE_NULLNESS=true compileTest @@ -32,7 +32,7 @@ jobs: with: fetch-depth: 0 - name: 'Qodana Scan' - uses: JetBrains/qodana-action@v2024.1.8 + uses: JetBrains/qodana-action@v2024.1.9 - uses: github/codeql-action/upload-sarif@v3 if: success() || failure() @@ -49,7 +49,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: SpotlessCheck run: ./gradlew --continue spotlessCheck @@ -81,7 +81,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Checkstyle run: ./gradlew --continue checkstyleMainChanged - run: | @@ -108,7 +108,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: PMD checks run: ./gradlew --continue pmdMainChanged diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml index 0a1ed3eb07e..0e55e6d06bc 100644 --- a/.github/workflows/gradle-publish.yml +++ b/.github/workflows/gradle-publish.yml @@ -22,7 +22,7 @@ jobs: server-id: github # Value of the distributionManagement/repository/id field of the pom.xml - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Assemble with Gradle run: ./gradlew assemble diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index 8c3ed455250..de6f338d99a 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -19,7 +19,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Build Documentation with Gradle run: ./gradlew alldoc diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 33b62b2c5c9..2a90bd75f3e 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -31,7 +31,7 @@ jobs: distribution: 'temurin' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Build with Gradle run: ./gradlew --parallel assemble diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index 75839cd76c5..bfb8a2be814 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -25,7 +25,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Test with Gradle run: ./gradlew --continue ${{ matrix.tests }} diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index e5f0041c442..4ee2c6ad557 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -38,7 +38,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: Test with Gradle run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -87,7 +87,7 @@ jobs: shell: bash - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml index 28335bd0998..2242add7460 100644 --- a/.github/workflows/tests_winmac.yml +++ b/.github/workflows/tests_winmac.yml @@ -30,7 +30,7 @@ jobs: - name: Setup Gradle uses: - gradle/actions/setup-gradle@v3.5.0 + gradle/actions/setup-gradle@v4.0.1 - name: Test with Gradle run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -76,7 +76,7 @@ jobs: run: .github/dlsmt.sh - name: Setup Gradle - uses: gradle/actions/setup-gradle@v3.5.0 + uses: gradle/actions/setup-gradle@v4.0.1 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} From 2c8c7e214cd32f29ced4bb1312abd1e4d07ecd60 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Tue, 3 Sep 2024 19:36:56 +0200 Subject: [PATCH 34/46] formatting --- .../src/main/java/de/uka/ilkd/key/gui/MainWindow.java | 3 ++- .../key/gui/actions/ToggleProofTreeTooltipAction.java | 8 ++++---- .../gui/prooftree/ProofTreeSettingsMenuFactory.java | 10 ++++++---- .../de/uka/ilkd/key/gui/prooftree/ProofTreeView.java | 9 ++++++--- 4 files changed, 18 insertions(+), 12 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index 73d16e31bcd..870acc2b682 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -1461,7 +1461,8 @@ public boolean isShowTacletInfo() { } public void setShowProofTreeTooltip(Object source) { - toogleProofTreeTooltipAction.actionPerformed(new ActionEvent(proofTreeView, ActionEvent.ACTION_PERFORMED, "")); + toogleProofTreeTooltipAction + .actionPerformed(new ActionEvent(proofTreeView, ActionEvent.ACTION_PERFORMED, "")); } public AutoModeAction getAutoModeAction() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java index 4d89b9a5a74..fdc1637ab10 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ToggleProofTreeTooltipAction.java @@ -3,14 +3,14 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions; +import java.awt.event.ActionEvent; +import java.beans.PropertyChangeListener; +import javax.swing.*; + import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ViewSettings; -import javax.swing.*; -import java.awt.event.ActionEvent; -import java.beans.PropertyChangeListener; - /** * Toggles the tooltips of the proof tree. * diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java index de237069ad5..057bf1fc44c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java @@ -10,12 +10,12 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.settings.ProofIndependentSettings; import bibliothek.gui.dock.common.action.CAction; import bibliothek.gui.dock.common.action.CButton; import bibliothek.gui.dock.common.action.CCheckBox; import bibliothek.gui.dock.common.action.CMenu; -import de.uka.ilkd.key.settings.ProofIndependentSettings; import static de.uka.ilkd.key.gui.prooftree.ProofTreePopupFactory.ICON_SIZE; @@ -140,11 +140,13 @@ private static CCheckBox createTooltipToggle() { CCheckBox check = new CCheckBox() { @Override protected void changed() { - /* The ToogleProofTreeTooltipAction (in the View menu) is updated via - * PropertyChangeListener, no manual update needed! */ + /* + * The ToogleProofTreeTooltipAction (in the View menu) is updated via + * PropertyChangeListener, no manual update needed! + */ final boolean selected = isSelected(); ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .setShowProofTreeTooltips(selected); + .setShowProofTreeTooltips(selected); } }; check.setText("Show Tooltips"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index ac4bd402939..45fe758240f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -178,11 +178,13 @@ public ProofTreeView() { @Override public String getToolTipText(MouseEvent mouseEvent) { - /* For performance reasons, we want to make sure that the tooltips are only rendered + /* + * For performance reasons, we want to make sure that the tooltips are only rendered * when they are really needed. Therefore, they are now lazily generated and can - * also be disabled completely. */ + * also be disabled completely. + */ if (!ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings() - .isShowProofTreeTooltips()) { + .isShowProofTreeTooltips()) { return null; } TreePath path = delegateView.getPathForLocation(mouseEvent.getX(), @@ -1294,6 +1296,7 @@ public Component getTreeCellRendererComponent(JTree tree, Object value, boolean /** * Creates a new Style object and fills it for the given node. + * * @param node the tree node * @return the created Style with all the info about the node */ From 22e42796f6c9b5f0444523671c3c53654420e180 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 1 Oct 2024 20:49:31 +0000 Subject: [PATCH 35/46] Bump the gradle-deps group with 5 updates Bumps the gradle-deps group with 5 updates: | Package | From | To | | --- | --- | --- | | [ch.qos.logback:logback-classic](https://github.com/qos-ch/logback) | `1.5.7` | `1.5.8` | | [org.junit.jupiter:junit-jupiter-api](https://github.com/junit-team/junit5) | `5.11.0` | `5.11.1` | | [org.junit.jupiter:junit-jupiter-params](https://github.com/junit-team/junit5) | `5.11.0` | `5.11.1` | | [org.junit.jupiter:junit-jupiter-engine](https://github.com/junit-team/junit5) | `5.11.0` | `5.11.1` | | org.checkerframework | `0.6.43` | `0.6.44` | Updates `ch.qos.logback:logback-classic` from 1.5.7 to 1.5.8 - [Commits](https://github.com/qos-ch/logback/compare/v_1.5.7...v_1.5.8) Updates `org.junit.jupiter:junit-jupiter-api` from 5.11.0 to 5.11.1 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.11.0...r5.11.1) Updates `org.junit.jupiter:junit-jupiter-params` from 5.11.0 to 5.11.1 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.11.0...r5.11.1) Updates `org.junit.jupiter:junit-jupiter-engine` from 5.11.0 to 5.11.1 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.11.0...r5.11.1) Updates `org.checkerframework` from 0.6.43 to 0.6.44 --- updated-dependencies: - dependency-name: ch.qos.logback:logback-classic dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-api dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-params dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-engine dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.checkerframework dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps ... Signed-off-by: dependabot[bot] --- build.gradle | 12 ++++++------ key.ui/build.gradle | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/build.gradle b/build.gradle index 210188b7364..763c746afd6 100644 --- a/build.gradle +++ b/build.gradle @@ -24,7 +24,7 @@ plugins { id "com.diffplug.spotless" version "6.25.0" // EISOP Checker Framework - id "org.checkerframework" version "0.6.43" + id "org.checkerframework" version "0.6.44" } // Configure this project for use inside IntelliJ: @@ -76,7 +76,7 @@ subprojects { dependencies { implementation("org.slf4j:slf4j-api:2.0.16") implementation("org.slf4j:slf4j-api:2.0.16") - testImplementation("ch.qos.logback:logback-classic:1.5.7") + testImplementation("ch.qos.logback:logback-classic:1.5.8") //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0' //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0' @@ -89,12 +89,12 @@ subprojects { testCompileOnly "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker:$eisop_version" - testImplementation("ch.qos.logback:logback-classic:1.5.7") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.0' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.0' + testImplementation("ch.qos.logback:logback-classic:1.5.8") + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.1' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.1' testImplementation project(':key.util') - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.0' + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.1' } tasks.withType(JavaCompile) { diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 0636b253181..1a8ab25c39e 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -23,7 +23,7 @@ dependencies { api 'com.miglayout:miglayout-swing:11.4.2' //logging implementation used by the slf4j - implementation 'ch.qos.logback:logback-classic:1.5.7' + implementation 'ch.qos.logback:logback-classic:1.5.8' api 'org.key-project:docking-frames-common:1.1.3p1' api 'org.key-project:docking-frames-core:1.1.3p1' From ed82b5ae47a646af449f2f6ee09184e38f4cbd04 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Tue, 1 Oct 2024 20:57:02 +0000 Subject: [PATCH 36/46] Bump the github-actions-deps group with 2 updates Bumps the github-actions-deps group with 2 updates: [gradle/actions](https://github.com/gradle/actions) and [JetBrains/qodana-action](https://github.com/jetbrains/qodana-action). Updates `gradle/actions` from 4.0.1 to 4.1.0 - [Release notes](https://github.com/gradle/actions/releases) - [Commits](https://github.com/gradle/actions/compare/v4.0.1...v4.1.0) Updates `JetBrains/qodana-action` from 2024.1.9 to 2024.2.3 - [Release notes](https://github.com/jetbrains/qodana-action/releases) - [Commits](https://github.com/jetbrains/qodana-action/compare/v2024.1.9...v2024.2.3) --- updated-dependencies: - dependency-name: gradle/actions dependency-type: direct:production update-type: version-update:semver-minor dependency-group: github-actions-deps - dependency-name: JetBrains/qodana-action dependency-type: direct:production update-type: version-update:semver-minor dependency-group: github-actions-deps ... Signed-off-by: dependabot[bot] --- .github/workflows/code_quality.yml | 10 +++++----- .github/workflows/gradle-publish.yml | 2 +- .github/workflows/javadoc.yml | 2 +- .github/workflows/nightlydeploy.yml | 2 +- .github/workflows/opttest.yml | 2 +- .github/workflows/tests.yml | 4 ++-- .github/workflows/tests_winmac.yml | 4 ++-- 7 files changed, 13 insertions(+), 13 deletions(-) diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index a544efa0209..b2c2b33d44a 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -20,7 +20,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Build with Gradle run: ./gradlew -DENABLE_NULLNESS=true compileTest @@ -32,7 +32,7 @@ jobs: with: fetch-depth: 0 - name: 'Qodana Scan' - uses: JetBrains/qodana-action@v2024.1.9 + uses: JetBrains/qodana-action@v2024.2.3 - uses: github/codeql-action/upload-sarif@v3 if: success() || failure() @@ -49,7 +49,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: SpotlessCheck run: ./gradlew --continue spotlessCheck @@ -81,7 +81,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Checkstyle run: ./gradlew --continue checkstyleMainChanged - run: | @@ -108,7 +108,7 @@ jobs: java-version: '21' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: PMD checks run: ./gradlew --continue pmdMainChanged diff --git a/.github/workflows/gradle-publish.yml b/.github/workflows/gradle-publish.yml index 0e55e6d06bc..b541c403818 100644 --- a/.github/workflows/gradle-publish.yml +++ b/.github/workflows/gradle-publish.yml @@ -22,7 +22,7 @@ jobs: server-id: github # Value of the distributionManagement/repository/id field of the pom.xml - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Assemble with Gradle run: ./gradlew assemble diff --git a/.github/workflows/javadoc.yml b/.github/workflows/javadoc.yml index de6f338d99a..7e8b4e1dc89 100644 --- a/.github/workflows/javadoc.yml +++ b/.github/workflows/javadoc.yml @@ -19,7 +19,7 @@ jobs: distribution: 'corretto' cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Build Documentation with Gradle run: ./gradlew alldoc diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 2a90bd75f3e..2f28e9a8050 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -31,7 +31,7 @@ jobs: distribution: 'temurin' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Build with Gradle run: ./gradlew --parallel assemble diff --git a/.github/workflows/opttest.yml b/.github/workflows/opttest.yml index bfb8a2be814..7b81b938679 100644 --- a/.github/workflows/opttest.yml +++ b/.github/workflows/opttest.yml @@ -25,7 +25,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Test with Gradle run: ./gradlew --continue ${{ matrix.tests }} diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 4ee2c6ad557..cb9563601b8 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -38,7 +38,7 @@ jobs: cache: 'gradle' - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: Test with Gradle run: ./gradlew --continue -DjacocoEnabled=true -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -87,7 +87,7 @@ jobs: shell: bash - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} diff --git a/.github/workflows/tests_winmac.yml b/.github/workflows/tests_winmac.yml index 2242add7460..c3c185ce95f 100644 --- a/.github/workflows/tests_winmac.yml +++ b/.github/workflows/tests_winmac.yml @@ -30,7 +30,7 @@ jobs: - name: Setup Gradle uses: - gradle/actions/setup-gradle@v4.0.1 + gradle/actions/setup-gradle@v4.1.0 - name: Test with Gradle run: ./gradlew --continue -x :key.core.symbolic_execution:test -x :key.core.proof_references:test test @@ -76,7 +76,7 @@ jobs: run: .github/dlsmt.sh - name: Setup Gradle - uses: gradle/actions/setup-gradle@v4.0.1 + uses: gradle/actions/setup-gradle@v4.1.0 - name: "Running tests: ${{ matrix.test }}" run: ./gradlew --continue ${{ matrix.test }} From 3ebff5ecb59627b0425d2bf94a93c4a46d736e9e Mon Sep 17 00:00:00 2001 From: BookWood Date: Mon, 21 Oct 2024 15:04:26 +0200 Subject: [PATCH 37/46] fixes NullPointerException, when using compareTo with locations that dont have a URI or position --- key.core/src/main/java/de/uka/ilkd/key/parser/Location.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java b/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java index 46b4b813bbf..83b5e395817 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java @@ -95,7 +95,8 @@ public int hashCode() { @Override public int compareTo(@NonNull Location o) { return Comparator - .comparing(l -> l.fileUri) - .thenComparing(Location::getPosition).compare(this, o); + .comparing(l -> l.fileUri, Comparator.nullsLast(Comparator.naturalOrder())) + .thenComparing(Location::getPosition, Comparator.nullsLast(Comparator.naturalOrder())) + .compare(this, o); } } From 3bdb527880bea77759a4cc720a2392fd8a78573a Mon Sep 17 00:00:00 2001 From: Nils Buchholz Date: Wed, 23 Oct 2024 11:23:19 +0200 Subject: [PATCH 38/46] add AbstractExternalSolverRuleApp to allow other external solvers to close goals --- .../main/java/de/uka/ilkd/key/proof/Goal.java | 3 +- .../rule/AbstractExternalSolverRuleApp.java | 178 ++++++++++++++++++ .../java/de/uka/ilkd/key/smt/SMTRuleApp.java | 54 ++---- 3 files changed, 195 insertions(+), 40 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 9885acd6145..5f9bc869cdb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -22,7 +22,6 @@ import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.rule.merge.MergeRule; -import de.uka.ilkd.key.smt.SMTRuleApp; import de.uka.ilkd.key.strategy.AutomatedRuleApplicationManager; import de.uka.ilkd.key.strategy.QueueRuleApplicationManager; import de.uka.ilkd.key.strategy.Strategy; @@ -627,7 +626,7 @@ public ImmutableList apply(final RuleApp ruleApp) { } else { proof.replace(this, goalList); if (ruleApp instanceof TacletApp tacletApp && tacletApp.taclet().closeGoal() - || ruleApp instanceof SMTRuleApp) { + || ruleApp instanceof AbstractExternalSolverRuleApp) { // the first new goal is the one to be closed proof.closeGoal(goalList.head()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java new file mode 100644 index 00000000000..f5c03dd030e --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java @@ -0,0 +1,178 @@ +/* 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.rule; + +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.logic.Name; +import org.key_project.util.collection.ImmutableList; + +/** + * The rule application that is used when a goal is closed by means of an external solver. So far it + * stores the rule that that has been used and a title containing some information for the user. + *

+ * {@link de.uka.ilkd.key.smt.SMTRuleApp} + */ +public abstract class AbstractExternalSolverRuleApp extends AbstractBuiltInRuleApp { + protected final ExternalSolverRule rule; + protected final String title; + protected final String successfulSolverName; + + /** + * Creates a new AbstractExternalSolverRuleApp, + * + * @param rule the ExternalSolverRule to apply + * @param pio the position in the term to apply the rule to + * @param unsatCore an unsat core consisting of the formulas that are needed to prove the goal + * (optional null) + * @param successfulSolverName the name of the solver used to find the proof + * @param title the title of this rule app + */ + protected AbstractExternalSolverRuleApp(ExternalSolverRule rule, PosInOccurrence pio, + ImmutableList unsatCore, + String successfulSolverName, String title) { + super(rule, pio, unsatCore); + this.rule = rule.newRule(); + this.title = title; + this.successfulSolverName = successfulSolverName; + } + + /** + * Gets the title of this rule application + * + * @return title of this application + */ + public String getTitle() { + return title; + } + + /** + * Gets the name of the successful solver + * + * @return name of the successful solver + */ + public String getSuccessfulSolverName() { + return successfulSolverName; + } + + @Override + public BuiltInRule rule() { + return rule; + } + + @Override + public String displayName() { + return title; + } + + /** + * Interface for the rules of external solvers + */ + public interface ExternalSolverRule extends BuiltInRule { + Name name = new Name("ExternalSolverRule"); + + ExternalSolverRule newRule(); + + AbstractExternalSolverRuleApp createApp(String successfulSolverName); + + /** + * Create a new rule application with the given solver name and unsat core. + * + * @param successfulSolverName solver that produced this result + * @param unsatCore formulas required to prove the result + * @return rule application instance + */ + AbstractExternalSolverRuleApp createApp(String successfulSolverName, + ImmutableList unsatCore); + + @Override + AbstractExternalSolverRuleApp createApp(PosInOccurrence pos, TermServices services); + + + @Override + default boolean isApplicable(Goal goal, PosInOccurrence pio) { + return false; + } + + + /** + * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards) + * with the same sequent as the given one. + * + * @param goal the Goal on which to apply ruleApp + * @param services the Services with the necessary information about the java programs + * @param ruleApp the rule application to be executed + * @return a list with an identical goal as the given goal + */ + @Override + default ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) { + if (goal.proof().getInitConfig().getJustifInfo().getJustification(newRule()) == null) { + goal.proof().getInitConfig().registerRule(newRule(), () -> false); + } + return goal.split(1); + } + + @Override + default boolean isApplicableOnSubTerms() { + return false; + } + + @Override + default String displayName() { + return "ExternalSolver"; + } + + @Override + String toString(); + + @Override + default Name name() { + return name; + } + + } + + /** + * Sets the title (needs to create a new instance for this) + * + * @param title new title for rule app + * @return copy of this with the new title + */ + public abstract AbstractExternalSolverRuleApp setTitle(String title); + + @Override + public AbstractExternalSolverRuleApp setIfInsts(ImmutableList ifInsts) { + setMutable(ifInsts); + return this; + } + + /** + * Create a new RuleApp with the same pio (in this case, that will probably be null as the + * AbstractExternalSolver rule is applied to the complete sequent) as this one. + * Add all top level formulas of the goal + * to the RuleApp's ifInsts. + * + * @param goal the goal to instantiate the current RuleApp on + * @return a new RuleApp with the same pio and all top level formulas of the goal as ifInsts + */ + @Override + public AbstractExternalSolverRuleApp tryToInstantiate(Goal goal) { + AbstractExternalSolverRuleApp app = rule.createApp(pio, goal.proof().getServices()); + Sequent seq = goal.sequent(); + List ifInsts = new ArrayList<>(); + for (SequentFormula ante : seq.antecedent()) { + ifInsts.add(new PosInOccurrence(ante, PosInTerm.getTopLevel(), true)); + } + for (SequentFormula succ : seq.succedent()) { + ifInsts.add(new PosInOccurrence(succ, PosInTerm.getTopLevel(), false)); + } + return app.setIfInsts(ImmutableList.fromList(ifInsts)); + } + +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java index 9674a9ed1b8..ef4b9b38087 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java @@ -9,7 +9,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.rule.AbstractBuiltInRuleApp; +import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.RuleApp; @@ -17,14 +17,11 @@ import org.key_project.util.collection.ImmutableList; /** - * The rule application that is used when a goal is closed by means of an external solver. So far it + * The rule application that is used when a goal is closed by means of an SMT solver. So far it * stores the rule that that has been used and a title containing some information for the user. */ -public class SMTRuleApp extends AbstractBuiltInRuleApp { - +public class SMTRuleApp extends AbstractExternalSolverRuleApp { public static final SMTRule RULE = new SMTRule(); - private final String title; - private final String successfulSolverName; /** * Create a new rule app without ifInsts (will be null). @@ -37,11 +34,10 @@ public class SMTRuleApp extends AbstractBuiltInRuleApp { this(rule, pio, null, successfulSolverName); } - SMTRuleApp(SMTRule rule, PosInOccurrence pio, ImmutableList unsatCore, + SMTRuleApp(ExternalSolverRule rule, PosInOccurrence pio, + ImmutableList unsatCore, String successfulSolverName) { - super(rule, pio, unsatCore); - this.title = "SMT: " + successfulSolverName; - this.successfulSolverName = successfulSolverName; + super(rule, pio, unsatCore, successfulSolverName, "SMT: " + successfulSolverName); } @Override @@ -49,27 +45,20 @@ public SMTRuleApp replacePos(PosInOccurrence newPos) { return new SMTRuleApp(RULE, newPos, ifInsts, successfulSolverName); } - public String getTitle() { - return title; - } - - public String getSuccessfulSolverName() { - return successfulSolverName; - } - @Override public BuiltInRule rule() { return RULE; } - @Override - public String displayName() { - return title; - } - - public static class SMTRule implements BuiltInRule { + public static class SMTRule implements ExternalSolverRule { public static final Name name = new Name("SMTRule"); + @Override + public ExternalSolverRule newRule() { + return new SMTRule(); + } + + @Override public SMTRuleApp createApp(String successfulSolverName) { return new SMTRuleApp(this, null, successfulSolverName); } @@ -81,6 +70,7 @@ public SMTRuleApp createApp(String successfulSolverName) { * @param unsatCore formulas required to prove the result * @return rule application instance */ + @Override public SMTRuleApp createApp(String successfulSolverName, ImmutableList unsatCore) { return new SMTRuleApp(this, null, unsatCore, successfulSolverName); @@ -91,13 +81,6 @@ public SMTRuleApp createApp(PosInOccurrence pos, TermServices services) { return new SMTRuleApp(this, null, ""); } - - @Override - public boolean isApplicable(Goal goal, PosInOccurrence pio) { - return false; - } - - /** * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards) * with the same sequent as the given one. @@ -115,16 +98,12 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) return goal.split(1); } - @Override - public boolean isApplicableOnSubTerms() { - return false; - } - @Override public String displayName() { return "SMT"; } + @Override public String toString() { return displayName(); } @@ -133,9 +112,9 @@ public String toString() { public Name name() { return name; } - } + @Override public SMTRuleApp setTitle(String title) { return new SMTRuleApp(RULE, pio, ifInsts, title); } @@ -168,5 +147,4 @@ public SMTRuleApp tryToInstantiate(Goal goal) { } return app.setIfInsts(ImmutableList.fromList(ifInsts)); } - } From 1989ce9fa794a6f54b294daee216d6d8047ba748 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Wed, 23 Oct 2024 11:52:01 +0200 Subject: [PATCH 39/46] added missing conversion rules from javaUnaryMinusFloat/Double to negFloat/Double --- .../ilkd/key/proof/rules/floatRulesAssumeStrictfp.key | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key index 6e011de1bf2..39603644b9c 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesAssumeStrictfp.key @@ -8,6 +8,11 @@ } \rules(programRules:Java, floatRules:assumeStrictfp) { + translateJavaUnaryMinusFloat { + \find(javaUnaryMinusFloat(f1)) + \replacewith(negFloat(f1)) + \heuristics(javaFloatSemantics) + }; translateJavaAddFloat { \find(javaAddFloat(f1, f2)) @@ -33,6 +38,12 @@ \heuristics(javaFloatSemantics) }; + translateJavaUnaryMinusDouble { + \find(javaUnaryMinusDouble(d1)) + \replacewith(negDouble(d1)) + \heuristics(javaFloatSemantics) + }; + translateJavaAddDouble { \find(javaAddDouble(d1, d2)) \replacewith(addDouble(d1, d2)) From f1d9bb9a3b6a55b67530707b1068e656abb1dfad Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 23 Oct 2024 18:35:03 +0200 Subject: [PATCH 40/46] increase java version to 21 --- build.gradle | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/build.gradle b/build.gradle index 763c746afd6..41a43556ec4 100644 --- a/build.gradle +++ b/build.gradle @@ -62,8 +62,8 @@ subprojects { version = rootProject.version java { - sourceCompatibility = 17 - targetCompatibility = 17 + sourceCompatibility = 21 + targetCompatibility = 21 } repositories { @@ -100,8 +100,8 @@ subprojects { tasks.withType(JavaCompile) { // Setting UTF-8 as the java source encoding. options.encoding = "UTF-8" - // Setting the release to Java 17 - options.release = 17 + // Setting the release to Java 21 + options.release = 21 } tasks.withType(Javadoc) { @@ -109,9 +109,7 @@ subprojects { options.addBooleanOption 'Xdoclint:none', true //options.verbose() options.encoding = 'UTF-8' - if (JavaVersion.current().isJava9Compatible()) { - options.addBooleanOption('html5', true) - } + options.addBooleanOption('html5', true) } tasks.withType(Test) {//Configure all tests From a779724765bdfe1dc94cefc66cfa1f6c30cf48bc Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Fri, 25 Oct 2024 15:05:35 +0200 Subject: [PATCH 41/46] set version to 2.12.4-dev --- build.gradle | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/build.gradle b/build.gradle index 41a43556ec4..84fbcfdd43a 100644 --- a/build.gradle +++ b/build.gradle @@ -40,10 +40,10 @@ static def getDate() { } // The $BUILD_NUMBER is an environment variable set by Jenkins. -def build = System.env.BUILD_NUMBER == null ? "" : "-${System.env.BUILD_NUMBER}" +def build = System.env.BUILD_NUMBER == null ? "-dev" : "-${System.env.BUILD_NUMBER}" group = "org.key-project" -version = "2.13.0$build" +version = "2.12.4$build" subprojects { apply plugin: "java" From 0a6178fe012189791e326093474e0d37460f1910 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Fri, 1 Nov 2024 20:14:40 +0000 Subject: [PATCH 42/46] Bump JetBrains/qodana-action in the github-actions-deps group Bumps the github-actions-deps group with 1 update: [JetBrains/qodana-action](https://github.com/jetbrains/qodana-action). Updates `JetBrains/qodana-action` from 2024.2.3 to 2024.2.6 - [Release notes](https://github.com/jetbrains/qodana-action/releases) - [Commits](https://github.com/jetbrains/qodana-action/compare/v2024.2.3...v2024.2.6) --- updated-dependencies: - dependency-name: JetBrains/qodana-action dependency-type: direct:production update-type: version-update:semver-patch dependency-group: github-actions-deps ... Signed-off-by: dependabot[bot] --- .github/workflows/code_quality.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index b2c2b33d44a..bfe52b73ebd 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -32,7 +32,7 @@ jobs: with: fetch-depth: 0 - name: 'Qodana Scan' - uses: JetBrains/qodana-action@v2024.2.3 + uses: JetBrains/qodana-action@v2024.2.6 - uses: github/codeql-action/upload-sarif@v3 if: success() || failure() From 1b92b2da4f0f5a7f7f14a5399af6662da92e021f Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Fri, 1 Nov 2024 20:20:50 +0000 Subject: [PATCH 43/46] Bump the gradle-deps group with 6 updates Bumps the gradle-deps group with 6 updates: | Package | From | To | | --- | --- | --- | | [ch.qos.logback:logback-classic](https://github.com/qos-ch/logback) | `1.5.8` | `1.5.12` | | [org.junit.jupiter:junit-jupiter-api](https://github.com/junit-team/junit5) | `5.11.1` | `5.11.3` | | [org.junit.jupiter:junit-jupiter-params](https://github.com/junit-team/junit5) | `5.11.1` | `5.11.3` | | [org.junit.jupiter:junit-jupiter-engine](https://github.com/junit-team/junit5) | `5.11.1` | `5.11.3` | | org.checkerframework | `0.6.44` | `0.6.45` | | org.ow2.asm:asm | `9.7` | `9.7.1` | Updates `ch.qos.logback:logback-classic` from 1.5.8 to 1.5.12 - [Commits](https://github.com/qos-ch/logback/compare/v_1.5.8...v_1.5.12) Updates `org.junit.jupiter:junit-jupiter-api` from 5.11.1 to 5.11.3 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.11.1...r5.11.3) Updates `org.junit.jupiter:junit-jupiter-params` from 5.11.1 to 5.11.3 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.11.1...r5.11.3) Updates `org.junit.jupiter:junit-jupiter-engine` from 5.11.1 to 5.11.3 - [Release notes](https://github.com/junit-team/junit5/releases) - [Commits](https://github.com/junit-team/junit5/compare/r5.11.1...r5.11.3) Updates `org.checkerframework` from 0.6.44 to 0.6.45 Updates `org.ow2.asm:asm` from 9.7 to 9.7.1 --- updated-dependencies: - dependency-name: ch.qos.logback:logback-classic dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-api dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-params dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.junit.jupiter:junit-jupiter-engine dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.checkerframework dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps - dependency-name: org.ow2.asm:asm dependency-type: direct:production update-type: version-update:semver-patch dependency-group: gradle-deps ... Signed-off-by: dependabot[bot] --- build.gradle | 12 ++++++------ key.ui/build.gradle | 2 +- recoder/build.gradle | 2 +- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/build.gradle b/build.gradle index 84fbcfdd43a..b4f19cb68d2 100644 --- a/build.gradle +++ b/build.gradle @@ -24,7 +24,7 @@ plugins { id "com.diffplug.spotless" version "6.25.0" // EISOP Checker Framework - id "org.checkerframework" version "0.6.44" + id "org.checkerframework" version "0.6.45" } // Configure this project for use inside IntelliJ: @@ -76,7 +76,7 @@ subprojects { dependencies { implementation("org.slf4j:slf4j-api:2.0.16") implementation("org.slf4j:slf4j-api:2.0.16") - testImplementation("ch.qos.logback:logback-classic:1.5.8") + testImplementation("ch.qos.logback:logback-classic:1.5.12") //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0' //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0' @@ -89,12 +89,12 @@ subprojects { testCompileOnly "io.github.eisop:checker-qual:$eisop_version" checkerFramework "io.github.eisop:checker:$eisop_version" - testImplementation("ch.qos.logback:logback-classic:1.5.8") - testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.1' - testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.1' + testImplementation("ch.qos.logback:logback-classic:1.5.12") + testImplementation 'org.junit.jupiter:junit-jupiter-api:5.11.3' + testImplementation 'org.junit.jupiter:junit-jupiter-params:5.11.3' testImplementation project(':key.util') - testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.1' + testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.11.3' } tasks.withType(JavaCompile) { diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 1a8ab25c39e..4356dd52796 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -23,7 +23,7 @@ dependencies { api 'com.miglayout:miglayout-swing:11.4.2' //logging implementation used by the slf4j - implementation 'ch.qos.logback:logback-classic:1.5.8' + implementation 'ch.qos.logback:logback-classic:1.5.12' api 'org.key-project:docking-frames-common:1.1.3p1' api 'org.key-project:docking-frames-core:1.1.3p1' diff --git a/recoder/build.gradle b/recoder/build.gradle index 45eac2a335d..ace63d2ab38 100644 --- a/recoder/build.gradle +++ b/recoder/build.gradle @@ -5,7 +5,7 @@ repositories { mavenCentral() } dependencies { - implementation 'org.ow2.asm:asm:9.7' + implementation 'org.ow2.asm:asm:9.7.1' implementation 'org.apache-extras.beanshell:bsh:2.0b6' implementation 'net.sf.retrotranslator:retrotranslator-runtime:1.2.9' implementation 'net.sf.retrotranslator:retrotranslator-transformer:1.2.9' From 591fea6db5e36a9712fb7787b521bbd41b7f2dc0 Mon Sep 17 00:00:00 2001 From: BookWood Date: Tue, 12 Nov 2024 14:48:02 +0100 Subject: [PATCH 44/46] small formatting change --- key.core/src/main/java/de/uka/ilkd/key/parser/Location.java | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java b/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java index 83b5e395817..4a82961a52f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java +++ b/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java @@ -94,9 +94,7 @@ public int hashCode() { @Override public int compareTo(@NonNull Location o) { - return Comparator - .comparing(l -> l.fileUri, Comparator.nullsLast(Comparator.naturalOrder())) - .thenComparing(Location::getPosition, Comparator.nullsLast(Comparator.naturalOrder())) - .compare(this, o); + return Comparator.comparing(l -> l.fileUri, Comparator.nullsLast(Comparator.naturalOrder())) + .thenComparing(Location::getPosition, Comparator.nullsLast(Comparator.naturalOrder())).compare(this, o); } } From 5c7566ac360aa38ea24ea9895e49e2e612510645 Mon Sep 17 00:00:00 2001 From: Nils Buchholz Date: Tue, 12 Nov 2024 22:26:50 +0100 Subject: [PATCH 45/46] removed default implementations for AbstractExternalSolverRuleApp around RULE field --- .../rule/AbstractExternalSolverRuleApp.java | 68 +------------------ .../java/de/uka/ilkd/key/smt/SMTRuleApp.java | 7 +- 2 files changed, 3 insertions(+), 72 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java index f5c03dd030e..1e61eff79db 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractExternalSolverRuleApp.java @@ -3,14 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule; -import java.util.ArrayList; -import java.util.List; - -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.proof.Goal; -import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; /** @@ -20,7 +15,6 @@ * {@link de.uka.ilkd.key.smt.SMTRuleApp} */ public abstract class AbstractExternalSolverRuleApp extends AbstractBuiltInRuleApp { - protected final ExternalSolverRule rule; protected final String title; protected final String successfulSolverName; @@ -38,7 +32,6 @@ protected AbstractExternalSolverRuleApp(ExternalSolverRule rule, PosInOccurrence ImmutableList unsatCore, String successfulSolverName, String title) { super(rule, pio, unsatCore); - this.rule = rule.newRule(); this.title = title; this.successfulSolverName = successfulSolverName; } @@ -61,11 +54,6 @@ public String getSuccessfulSolverName() { return successfulSolverName; } - @Override - public BuiltInRule rule() { - return rule; - } - @Override public String displayName() { return title; @@ -75,10 +63,6 @@ public String displayName() { * Interface for the rules of external solvers */ public interface ExternalSolverRule extends BuiltInRule { - Name name = new Name("ExternalSolverRule"); - - ExternalSolverRule newRule(); - AbstractExternalSolverRuleApp createApp(String successfulSolverName); /** @@ -100,42 +84,16 @@ default boolean isApplicable(Goal goal, PosInOccurrence pio) { return false; } - - /** - * Create a new goal (to be closed in {@link Goal#apply(RuleApp)} directly afterwards) - * with the same sequent as the given one. - * - * @param goal the Goal on which to apply ruleApp - * @param services the Services with the necessary information about the java programs - * @param ruleApp the rule application to be executed - * @return a list with an identical goal as the given goal - */ - @Override - default ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) { - if (goal.proof().getInitConfig().getJustifInfo().getJustification(newRule()) == null) { - goal.proof().getInitConfig().registerRule(newRule(), () -> false); - } - return goal.split(1); - } - @Override default boolean isApplicableOnSubTerms() { return false; } @Override - default String displayName() { - return "ExternalSolver"; - } + String displayName(); @Override String toString(); - - @Override - default Name name() { - return name; - } - } /** @@ -151,28 +109,4 @@ public AbstractExternalSolverRuleApp setIfInsts(ImmutableList i setMutable(ifInsts); return this; } - - /** - * Create a new RuleApp with the same pio (in this case, that will probably be null as the - * AbstractExternalSolver rule is applied to the complete sequent) as this one. - * Add all top level formulas of the goal - * to the RuleApp's ifInsts. - * - * @param goal the goal to instantiate the current RuleApp on - * @return a new RuleApp with the same pio and all top level formulas of the goal as ifInsts - */ - @Override - public AbstractExternalSolverRuleApp tryToInstantiate(Goal goal) { - AbstractExternalSolverRuleApp app = rule.createApp(pio, goal.proof().getServices()); - Sequent seq = goal.sequent(); - List ifInsts = new ArrayList<>(); - for (SequentFormula ante : seq.antecedent()) { - ifInsts.add(new PosInOccurrence(ante, PosInTerm.getTopLevel(), true)); - } - for (SequentFormula succ : seq.succedent()) { - ifInsts.add(new PosInOccurrence(succ, PosInTerm.getTopLevel(), false)); - } - return app.setIfInsts(ImmutableList.fromList(ifInsts)); - } - } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java index ef4b9b38087..115833419ef 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java @@ -13,6 +13,7 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.RuleApp; +import org.jspecify.annotations.NonNull; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; @@ -53,11 +54,6 @@ public BuiltInRule rule() { public static class SMTRule implements ExternalSolverRule { public static final Name name = new Name("SMTRule"); - @Override - public ExternalSolverRule newRule() { - return new SMTRule(); - } - @Override public SMTRuleApp createApp(String successfulSolverName) { return new SMTRuleApp(this, null, successfulSolverName); @@ -91,6 +87,7 @@ public SMTRuleApp createApp(PosInOccurrence pos, TermServices services) { * @return a list with an identical goal as the given goal */ @Override + @NonNull public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) { if (goal.proof().getInitConfig().getJustifInfo().getJustification(RULE) == null) { goal.proof().getInitConfig().registerRule(RULE, () -> false); From 3c41ebbd31e8e8171189a7714064631b549ae55e Mon Sep 17 00:00:00 2001 From: Nils Buchholz Date: Tue, 12 Nov 2024 22:39:40 +0100 Subject: [PATCH 46/46] spotless update --- key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java index 115833419ef..b7254570b20 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTRuleApp.java @@ -13,10 +13,11 @@ import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.RuleApp; -import org.jspecify.annotations.NonNull; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; +import org.jspecify.annotations.NonNull; + /** * The rule application that is used when a goal is closed by means of an SMT solver. So far it * stores the rule that that has been used and a title containing some information for the user.