diff --git a/key.ui/build.gradle b/key.ui/build.gradle index e7b21debf31..f8fa7ba8a4a 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -39,6 +39,8 @@ dependencies { runtimeOnly project(":keyext.slicing") runtimeOnly project(":keyext.proofmanagement") runtimeOnly project(":keyext.isabelletranslation") + + runtimeOnly project(":keyext.llm") } tasks.register('createExamplesZip', Zip) { 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 4de042cfcf2..87400d620f9 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 @@ -305,7 +305,9 @@ private MainWindow() { proofListener = new MainProofListener(); userInterface = new WindowUserInterfaceControl(this); mediator = getMainWindowMediator(userInterface); - KeYGuiExtensionFacade.getStartupExtensions().forEach(it -> it.preInit(this, mediator)); + KeYGuiExtensionFacade.getStartupExtensions() + .stream().filter(Objects::nonNull) + .forEach(it -> it.preInit(this, mediator)); Config.DEFAULT.setDefaultFonts(); ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java index 76eca687b4b..86479c24687 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeyAction.java @@ -7,6 +7,8 @@ import javax.swing.Icon; import javax.swing.KeyStroke; +import bibliothek.gui.dock.common.action.CAction; +import bibliothek.gui.dock.common.action.CButton; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK; @@ -155,4 +157,10 @@ public int getPriority() { protected void setPriority(int priority) { putValue(PRIORITY, priority); } + + public CAction toCAction() { + final var btn = new CButton(getName(), null); + btn.addActionListener(this); + return btn; + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index ef94d9dc7df..7751d0d4386 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java @@ -121,7 +121,7 @@ default void preInit(MainWindow window, KeYMediator mediator) { } - void init(MainWindow window, KeYMediator mediator); + default void init(MainWindow window, KeYMediator mediator) {}; } /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java index af3bf9cbfe4..7958cfe3f9f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java @@ -4,22 +4,25 @@ package de.uka.ilkd.key.gui.settings; -import java.awt.*; -import java.io.File; -import java.util.Arrays; -import java.util.List; -import javax.swing.*; - import de.uka.ilkd.key.gui.KeYFileChooser; import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid; +import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.fonticons.IconFontSwing; - import net.miginfocom.layout.AC; import net.miginfocom.layout.CC; import net.miginfocom.layout.LC; import net.miginfocom.swing.MigLayout; import org.jspecify.annotations.Nullable; +import javax.swing.*; +import java.awt.*; +import java.awt.event.ActionListener; +import java.io.File; +import java.util.Arrays; +import java.util.Collections; +import java.util.List; +import java.util.function.Function; + /** * Extension of {@link SimpleSettingsPanel} which uses {@link MigLayout} to create a nice * three-column view. @@ -36,19 +39,19 @@ public abstract class SettingsPanel extends SimpleSettingsPanel { protected SettingsPanel() { pCenter.setLayout(new MigLayout( - // set up rows: - new LC().fillX() - // remove the padding after the help icon - .insets(null, null, null, "0").wrapAfter(3), - // set up columns: - new AC().count(3).fill(1) - // label column does not grow - .grow(0f, 0) - // input area does grow - .grow(1000f, 1) - // help icon always has the same size - .size("16px", 2) - .align("right", 0))); + // set up rows: + new LC().fillX() + // remove the padding after the help icon + .insets(null, null, null, "0").wrapAfter(3), + // set up columns: + new AC().count(3).fill(1) + // label column does not grow + .grow(0f, 0) + // input area does grow + .grow(1000f, 1) + // help icon always has the same size + .size("16px", 2) + .align("right", 0))); } /** @@ -116,7 +119,7 @@ protected JComboBox createSelection(T[] elements, Validator validator) * @return */ protected JCheckBox addCheckBox(String title, String info, boolean value, - final Validator validator) { + final Validator validator) { JCheckBox checkBox = createCheckBox(title, value, validator); addRowWithHelp(info, new JLabel(), checkBox); return checkBox; @@ -132,7 +135,7 @@ protected JCheckBox addCheckBox(String title, String info, boolean value, * @return */ protected JTextField addFileChooserPanel(String title, String file, String info, boolean isSave, - final Validator validator) { + final Validator validator) { JTextField textField = new JTextField(file); textField.addActionListener(e -> { try { @@ -161,7 +164,7 @@ protected JTextField addFileChooserPanel(String title, String file, String info, fileChooser = KeYFileChooser.getFileChooser("Save file"); fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter()); result = fileChooser.showSaveDialog((Component) e.getSource(), - new File(textField.getText())); + new File(textField.getText())); } else { fileChooser = KeYFileChooser.getFileChooser("Open file"); fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter()); @@ -181,16 +184,16 @@ protected JTextField addFileChooserPanel(String title, String file, String info, /** * Adds a new combobox to the panel. * - * @param title label of the combo box - * @param info help text + * @param title label of the combo box + * @param info help text * @param selectionIndex which item to initially select - * @param validator validator - * @param items the items - * @param the type of the items + * @param validator validator + * @param items the items + * @param the type of the items * @return the combo box */ protected JComboBox addComboBox(String title, String info, int selectionIndex, - @Nullable Validator validator, T... items) { + @Nullable Validator validator, T... items) { JComboBox comboBox = new JComboBox<>(items); comboBox.setSelectedIndex(selectionIndex); comboBox.addActionListener(e -> { @@ -229,16 +232,75 @@ protected void addTitledComponent(String title, JComponent component, String hel addRowWithHelp(helpText, label, component); } + protected JList addListBox(String title, String info, + final Validator> validator, + List seq, Function converter) { + var model = new DefaultListModel(); + model.addAll(seq); + + JList list = new JList<>(model); + + var txtAdd = new JTextField(); + var btnAdd = new JButton(IconFactory.PLUS_SQUARED.get(16f)); + var btnRemove = new JButton(IconFactory.MINUS.get(16f)); + + JScrollPane field = new JScrollPane(list); + + var panel = new JPanel(new MigLayout(new LC().fillX())); + panel.add(field, new CC().span(3).growX().wrap()); + panel.add(txtAdd, new CC().growX()); + panel.add(btnAdd, new CC().gapAfter("16px")); + panel.add(btnRemove); + + JLabel lblTitle = new JLabel(title); + lblTitle.setLabelFor(list); + pCenter.add(lblTitle); + pCenter.add(new JSeparator(JSeparator.HORIZONTAL)); + JLabel infoButton = createHelpLabel(info); + pCenter.add(infoButton, new CC().wrap()); + pCenter.add(new JLabel()); + pCenter.add(panel); + + list.addListSelectionListener(e -> { + try { + if (validator != null) { + List ary = Collections.list(model.elements()); + validator.validate(ary); + } + demarkComponentAsErrornous(list); + } catch (Exception ex) { + markComponentAsErrornous(list, ex.getMessage()); + } + }); + + final ActionListener addItem = e -> { + String value = txtAdd.getText(); + if (value != null && !value.isEmpty()) { + model.addElement(converter.apply(value)); + } + }; + txtAdd.addActionListener(addItem); + btnAdd.addActionListener(addItem); + + ActionListener removeItem = e -> { + if(list.getSelectedIndex() != -1) { + model.removeElementAt(list.getSelectedIndex()); + } + }; + btnRemove.addActionListener(removeItem); + + return list; + } protected JTextArea addTextArea(String title, String text, String info, - final Validator validator) { + final Validator validator) { JScrollPane field = createTextArea(text, validator); addTitledComponent(title, field, info); return (JTextArea) field.getViewport().getView(); } protected JTextArea addTextAreaWithoutScroll(String title, String text, String info, - final Validator validator) { + final Validator validator) { JTextArea field = createTextAreaWithoutScroll(text, validator); addTitledComponent(title, field, info); return field; @@ -253,7 +315,7 @@ protected JTextArea addTextAreaWithoutScroll(String title, String text, String i * @return */ protected JTextField addTextField(String title, String text, String info, - final Validator validator) { + final Validator validator) { JTextField field = createTextField(text, validator); addTitledComponent(title, field, info); return field; @@ -261,7 +323,7 @@ protected JTextField addTextField(String title, String text, String info, protected JTextField addTextField(String title, String text, String info, - final Validator validator, JComponent additionalActions) { + final Validator validator, JComponent additionalActions) { JTextField field = createTextField(text, validator); JLabel label = new JLabel(title); label.setLabelFor(field); @@ -278,24 +340,24 @@ protected JTextField addTextField(String title, String text, String info, * also determines how the default {@link javax.swing.text.NumberFormatter} used by the * {@link JSpinner} formats entered Strings * (see {@link javax.swing.text.NumberFormatter#stringToValue(String)}). - * + *

* If there are additional restrictions for the entered values, the passed validator can check * those. The entered values have to be of a subclass of {@link Number} (as this is a number * text * field), otherwise the {@link Validator} will fail. * - * @param title the title of the text field - * @param min the minimum value that can be entered - * @param max the maximum value that can be entered - * @param step the step size used when changing the entered value using the JSpinner's arrow - * buttons - * @param info arbitrary information about the text field + * @param title the title of the text field + * @param min the minimum value that can be entered + * @param max the maximum value that can be entered + * @param step the step size used when changing the entered value using the JSpinner's arrow + * buttons + * @param info arbitrary information about the text field * @param validator a validator for checking the entered values + * @param the class of the minimum value * @return the created JSpinner - * @param the class of the minimum value */ protected > JSpinner addNumberField(String title, T min, - Comparable max, Number step, String info, final Validator validator) { + Comparable max, Number step, String info, final Validator validator) { JSpinner field = createNumberTextField(min, max, step, validator); addTitledComponent(title, field, info); return field; diff --git a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java b/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java index 8285a9b99da..27d3651ec9d 100644 --- a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java +++ b/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java @@ -40,6 +40,7 @@ private SwingUtil() { * @param uri the URI to be displayed in the user's default browser */ public static void browse(URI uri) throws IOException { + LOGGER.info("Open {}", uri); try { Desktop.getDesktop().browse(uri); } catch (UnsupportedOperationException e) { diff --git a/key.ui/src/main/resources/logback.xml b/key.ui/src/main/resources/logback.xml index f22b587756a..825e68fe580 100644 --- a/key.ui/src/main/resources/logback.xml +++ b/key.ui/src/main/resources/logback.xml @@ -46,11 +46,20 @@ [%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n - TRACE + DEBUG + + + + + + + + + diff --git a/keyext.llm/build.gradle b/keyext.llm/build.gradle new file mode 100644 index 00000000000..2744bed501b --- /dev/null +++ b/keyext.llm/build.gradle @@ -0,0 +1,10 @@ +description = "LLM UI" + +dependencies { + implementation project(":key.core") + implementation project(":key.ui") + + implementation("org.apache.httpcomponents.client5:httpclient5:5.5.1") + implementation("com.google.code.gson:gson:2.13.2") + implementation("org.slf4j:jcl-over-slf4j:1.7.5") +} \ No newline at end of file diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java new file mode 100644 index 00000000000..44274b49fac --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java @@ -0,0 +1,76 @@ +package org.key_project.key.llm; + +import com.google.gson.GsonBuilder; +import org.apache.hc.client5.http.classic.methods.HttpPost; +import org.apache.hc.client5.http.impl.classic.AbstractHttpClientResponseHandler; +import org.apache.hc.client5.http.impl.classic.HttpClients; +import org.apache.hc.core5.http.HttpEntity; +import org.apache.hc.core5.http.ParseException; +import org.apache.hc.core5.http.io.entity.EntityUtils; +import org.apache.hc.core5.http.io.entity.StringEntity; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.Map; +import java.util.concurrent.Callable; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmClient implements Callable> { + private final LlmSession llmSession; + private final LlmContext context; + private final LlmContext.LlmMessage prompt; + + public LlmClient(LlmSession llmSession, LlmContext context, String message) { + this.llmSession = llmSession; + this.context = context; + this.prompt = new LlmContext.LlmMessage("user", message); + } + + @Override + public Map call() throws Exception { + var url = llmSession.getApiEndpoint() + "/chat/completions"; + var request = new HttpPost(url); + + request.addHeader("Authorization", "Bearer " + llmSession.getAuthToken()); + request.addHeader("Content-Type", "application/json"); + request.addHeader("Accept", "application/json"); + + var msg = new ArrayList<>(context.getMessages()); + msg.add(prompt); + + var data = Map.of( + "model", llmSession.getModel(), + "messages", msg); + + var gson = new GsonBuilder().create(); + var stringBody = gson.toJson(data); + request.setEntity(new StringEntity(stringBody)); + + try (var client = HttpClients.createDefault()) { + return client.execute(request, new GsonHttpClientResponseHandler()); + } + } + + + private static class GsonHttpClientResponseHandler extends AbstractHttpClientResponseHandler> { + @Override + public Map handleEntity(HttpEntity entity) throws IOException { + String content = null; + try { + content = EntityUtils.toString(entity); + } catch (ParseException e) { + throw new RuntimeException(e); + } + //LoggerFactory.getLogger(LlmClient.class).error("Could not parse json response {}",content); + try { + return new GsonBuilder().create().fromJson(content, Map.class); + } catch (Exception e) { + throw new RuntimeException(e); + } + } + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java new file mode 100644 index 00000000000..e5c2dd16937 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java @@ -0,0 +1,24 @@ +package org.key_project.key.llm; + +import java.util.ArrayList; +import java.util.List; + +/** + * + * @author Alexander Weigl + * @version 1 (11/19/25) + */ +public class LlmContext { + private final List messages = new ArrayList<>(); + + public void addMessage(LlmMessage message) { + messages.add(message); + } + + public List getMessages() { + return messages; + } + + public record LlmMessage(String role, String content) { + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java new file mode 100644 index 00000000000..5422cf9b185 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java @@ -0,0 +1,107 @@ +package org.key_project.key.llm; + +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.actions.MainWindowAction; +import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.extension.api.TabPanel; +import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; +import de.uka.ilkd.key.gui.settings.InvalidSettingsInputException; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + +import javax.swing.*; +import java.awt.event.ActionEvent; +import java.util.Collection; +import java.util.List; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +@KeYGuiExtension.Info(experimental = false, description = "LLM support for KeY") +public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu, + KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu { + private KeyAction actionStartLlmPromptForCurrentProof; + private TabPanel uiPrompt; + + @Override + public @NonNull List getContextActions( + @NonNull KeYMediator mediator, @NonNull ContextMenuKind kind, @NonNull Object underlyingObject) { + return List.of(); + } + + @Override + public LlmSettingsProvider getSettings() { + return new LlmSettingsProvider(); + } + + @Override + public void preInit(MainWindow window, KeYMediator mediator) { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(LlmSettings.INSTANCE); + actionStartLlmPromptForCurrentProof = new StartLlmPromptForCurrentProofAction(window); + } + + @Override + public @NonNull List getMainMenuActions(@NonNull MainWindow mainWindow) { + return List.of(actionStartLlmPromptForCurrentProof); + } + + @Override + public @NonNull Collection getPanels(@NonNull MainWindow window, @NonNull KeYMediator mediator) { + uiPrompt = new LlmPrompt(window,mediator); + return List.of(uiPrompt); + } + + public static class LlmSettingsProvider implements SettingsProvider { + public static @Nullable LlmSettingsUI ui; + + @Override + public String getDescription() { + return "LLM Settings"; + } + + @Override + public JPanel getPanel(MainWindow window) { + return ui = new LlmSettingsUI(LlmSettings.INSTANCE); + } + + @Override + public void applySettings(MainWindow window) throws InvalidSettingsInputException { + LlmSettings.INSTANCE.setApiEndpoint(ui.getModel().getApiEndpoint()); + LlmSettings.INSTANCE.setDefaultModel(ui.getModel().getDefaultModel()); + LlmSettings.INSTANCE.setAuthToken(ui.getModel().getAuthToken()); + LlmSettings.INSTANCE.setAvailableModels(ui.getModel().getAvailableModels()); + } + } + +} + + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +class StartLlmPromptForCurrentProofAction extends MainWindowAction { + protected StartLlmPromptForCurrentProofAction(MainWindow mainWindow) { + super(mainWindow, true); + + setName("Open LLM prompt"); + setMenuPath("Proof.LLM"); + KeyStrokeManager.get(this, "ctrl P"); + setAcceleratorLetter('L'); + } + + @Override + public void actionPerformed(ActionEvent e) { + var proof = mainWindow.getMediator().getSelectedProof(); + + + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java new file mode 100644 index 00000000000..693e433bc04 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java @@ -0,0 +1,326 @@ +package org.key_project.key.llm; + +import bibliothek.gui.dock.common.action.CAction; +import bibliothek.gui.dock.common.action.CMenu; +import bibliothek.gui.dock.common.action.CRadioButton; +import bibliothek.gui.dock.common.action.CRadioGroup; +import com.google.gson.GsonBuilder; +import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.core.KeYSelectionEvent; +import de.uka.ilkd.key.core.KeYSelectionListener; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.colors.ColorSettings; +import de.uka.ilkd.key.gui.docking.DynamicCMenu; +import de.uka.ilkd.key.gui.extension.api.TabPanel; +import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.gui.help.HelpFacade; +import de.uka.ilkd.key.proof.Proof; +import net.miginfocom.layout.CC; +import net.miginfocom.layout.LC; +import net.miginfocom.swing.MigLayout; +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import javax.swing.*; +import javax.swing.table.DefaultTableModel; +import java.awt.*; +import java.awt.event.*; +import java.io.IOException; +import java.net.URI; +import java.util.*; +import java.util.List; +import java.util.concurrent.ForkJoinPool; +import java.util.function.Supplier; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmPrompt extends JPanel implements TabPanel { + private static final Logger LOGGER = LoggerFactory.getLogger(LlmPrompt.class); + public static final ColorSettings.ColorProperty COLOR_BG_INPUT = ColorSettings.define( + "llm.output.bg.input", + "Background color in chat of LLM answers", new Color(130, 180, 220, 255)); + + public static final ColorSettings.ColorProperty COLOR_BG_ERROR + = ColorSettings.define("llm.output.bg.error", "Background color in chat of LLM answers", new Color(255, 180, 180, 255)); + + public static final ColorSettings.ColorProperty COLOR_BG_ANSWER + = ColorSettings.define("llm.output.bg.answer", "Background color in chat of LLM answers", Color.LIGHT_GRAY); + + private final JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT); + + private final JEditorPane txtInput = new JEditorPane(); + + private final JPanel pOutput = new JPanel(new MigLayout(new LC().fillX().debug().topToBottom().wrapAfter(1))); + + private final KeyAction actionSwitchOrientation = new SwitchOrientationAction(); + private final SendPromptAction actionSendPrompt = new SendPromptAction(); + private final JPanel tblFiles = new JPanel(new MigLayout(new LC().fillX().wrapAfter(1))); + private final DefaultTableModel modelFiles = new DefaultTableModel(); + + private final DefaultListModel> model = new DefaultListModel<>(); + private final MainWindow mainWindow; + private final KeYMediator mediator; + + public LlmPrompt(MainWindow mainWindow, @NonNull KeYMediator mediator) { + this.mainWindow = mainWindow; + this.mediator = mediator; + + setLayout(new BorderLayout()); + add(splitPane, BorderLayout.CENTER); + final var comp = new JScrollPane(pOutput); + comp.getVerticalScrollBar().setUnitIncrement(16); + splitPane.add(comp); + var scrpInput = new JScrollPane(txtInput); + var scrpFiles = new JScrollPane(tblFiles); + var tabInputPanes = new JTabbedPane(); + tabInputPanes.addTab("Prompt", scrpInput); + tabInputPanes.addTab("Files", scrpFiles); + splitPane.add(tabInputPanes); + + SwingUtilities.invokeLater(this::populateFiles); + mediator.addKeYSelectionListener(new KeYSelectionListener() { + @Override + public void selectedProofChanged(KeYSelectionEvent e) { + populateFiles(); + } + }); + + + handle(new Exception("Test Exception")); + handle(new GsonBuilder().create().fromJson("{\"id\":\"chatcmpl-CdLvyHhYLoKFk3F28rE6JgNJVGZHU\",\"created\":1763495142,\"model\":\"gpt-4.1-mini-2025-04-14\",\"object\":\"chat.completion\",\"system_fingerprint\":\"fp_3dcd5944f5\",\"choices\":[{\"finish_reason\":\"stop\",\"index\":0,\"message\":{\"content\":\"Die Rayleigh-Streuung beschreibt die Streuung von Licht an kleinen Teilchen, deren Größe viel kleiner ist als die Lichtwellenlänge. Dabei wird kurzwelliges Licht (blaues und violettes) stärker gestreut als langwelliges (rotes), was z.B. den blauen Himmel erklärt. Die Intensität der Streuung ist proportional zur vierten Potenz der Frequenz des Lichts.\",\"role\":\"assistant\",\"annotations\":[]},\"provider_specific_fields\":{\"content_filter_results\":{\"hate\":{\"filtered\":false,\"severity\":\"safe\"},\"protected_material_text\":{\"filtered\":false,\"detected\":false},\"self_harm\":{\"filtered\":false,\"severity\":\"safe\"},\"sexual\":{\"filtered\":false,\"severity\":\"safe\"},\"violence\":{\"filtered\":false,\"severity\":\"safe\"}}}}],\"usage\":{\"completion_tokens\":91,\"prompt_tokens\":36,\"total_tokens\":127,\"completion_tokens_details\":{\"accepted_prediction_tokens\":0,\"audio_tokens\":0,\"reasoning_tokens\":0,\"rejected_prediction_tokens\":0},\"prompt_tokens_details\":{\"audio_tokens\":0,\"cached_tokens\":0}},\"prompt_filter_results\":[{\"prompt_index\":0,\"content_filter_results\":{\"hate\":{\"filtered\":false,\"severity\":\"safe\"},\"jailbreak\":{\"filtered\":false,\"detected\":false},\"self_harm\":{\"filtered\":false,\"severity\":\"safe\"},\"sexual\":{\"filtered\":false,\"severity\":\"safe\"},\"violence\":{\"filtered\":false,\"severity\":\"safe\"}}}]}", + Map.class)); + addInput("Input data"); + + txtInput.addKeyListener(new KeyAdapter() { + @Override + public void keyTyped(KeyEvent e) { + if (e.getKeyChar() == KeyEvent.VK_ENTER && (e.getModifiersEx() & InputEvent.CTRL_DOWN_MASK) > 0) { + actionSendPrompt.run(); + } + } + }); + } + + static class AddFileAction extends KeyAction { + private final Set selectedFiles; + private final URI file; + + public AddFileAction(URI file, Set selectedFiles) { + this.file = file; + this.selectedFiles = selectedFiles; + setName(file.toString()); + } + + @Override + public void actionPerformed(ActionEvent e) { + var chk = (JCheckBox) e.getSource(); + if (chk.isSelected()) { + selectedFiles.add(file); + } else { + selectedFiles.remove(file); + } + } + } + + private void populateFiles() { + try { + tblFiles.removeAll(); + LlmSession session = LlmUtils.getSession(mediator.getSelectedProof()); + List possibleFiles = new ArrayList<>(LlmUtils.getPossibleFiles(mediator.getSelectedProof())); + Set selectedFiles = session.getSelectedFiles(); + possibleFiles.sort(Comparator.comparing(URI::toString)); + for (URI file : possibleFiles) { + tblFiles.add(new JCheckBox(new AddFileAction(file, selectedFiles))); + } + tblFiles.invalidate(); + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + private OutputBox addInput(String text) { + var o = addBox(new LlmPromptModel(LlmPromptModel.Kind.INPUT, text, text), new RepromptAction(text)); + o.setBackground(COLOR_BG_INPUT.get()); + return o; + } + + private OutputBox addBox(LlmPromptModel data, Action... actions) { + OutputBox box = new OutputBox<>(data); + for (Action it : actions) { + box.menu.add(it); + } + pOutput.add(box, new CC().growX()); + box.setBackground(data.kind().background().get()); + return box; + } + + private void handle(Map jsonResponse) { + LOGGER.info("LLM prompt {}", jsonResponse); + final var text = ((Map) ((Map) ((List) + jsonResponse.get("choices")).get(0)).get("message")).get("content").toString(); + addBox(new LlmPromptModel<>(LlmPromptModel.Kind.OUTPUT, text, jsonResponse)); + } + + private void handle(Throwable e) { + addBox(new LlmPromptModel<>(LlmPromptModel.Kind.ERROR, e.toString(), e)); + } + + @Override + public @NonNull String getTitle() { + return "KiKI 2.0"; + } + + @Override + public @NonNull JComponent getComponent() { + return this; + } + + @Override + public @NonNull Collection getTitleCActions() { + Supplier supplier = () -> { + CMenu menu = new CMenu(); + menu.add(actionSwitchOrientation.toCAction()); + + CMenu menuModels = new CMenu("Models", null); + menu.add(menuModels); + var groupModels = new CRadioGroup(); + var llmSession = LlmUtils.getSession(MainWindow.getInstance().getMediator().getSelectedProof()); + + for (var m : LlmSettings.INSTANCE.getAvailableModels()) { + var selected = m.equals(llmSession.getModel()); + final var action = new CRadioButton(m, null) { + @Override + protected void changed() { + llmSession.setModel(m); + } + }; + action.setSelected(selected); + groupModels.add(action); + menuModels.add(action); + } + return menu; + }; + + var a = new DynamicCMenu("Settings", IconFactory.properties(MainWindow.TOOLBAR_ICON_SIZE), supplier); + var help = HelpFacade.createHelpButton("user/LLM/"); + return List.of(help, a); + } + + class SwitchOrientationAction extends KeyAction { + public SwitchOrientationAction() { + setName("Switch Orientation"); + } + + @Override + public void actionPerformed(ActionEvent e) { + if (splitPane.getOrientation() == JSplitPane.HORIZONTAL_SPLIT) { + splitPane.setOrientation(JSplitPane.VERTICAL_SPLIT); + } else { + splitPane.setOrientation(JSplitPane.HORIZONTAL_SPLIT); + } + } + } + + static class SelectContextAction extends KeyAction { + @Override + public void actionPerformed(ActionEvent e) { + + } + } + + class SendPromptAction extends KeyAction { + public SendPromptAction() { + setName("Send Prompt"); + } + + @Override + public void actionPerformed(ActionEvent e) { + run(); + } + + public void run() { + var proof = MainWindow.getInstance().getMediator().getSelectedProof(); + var node = MainWindow.getInstance().getMediator().getSelectedNode(); + + LlmSession session = LlmUtils.getSession(proof); + var txt = txtInput.getText(); + LlmClient client = new LlmClient(session, new LlmContext(), txt); + addInput(txt); + txtInput.setText(""); + + var sw = new SwingWorker, Void>() { + @Override + protected Map doInBackground() throws Exception { + return client.call(); + } + + @Override + protected void done() { + try { + handle(resultNow()); + } catch (IllegalStateException ex) { + LOGGER.error("Exceptional case", exceptionNow()); + handle(exceptionNow()); + } + } + }; + ForkJoinPool.commonPool().submit(sw); + } + } + + private class RepromptAction extends KeyAction { + private final String prompt; + + public RepromptAction(String prompt) { + this.prompt = prompt; + setName("into input"); + } + + @Override + public void actionPerformed(ActionEvent e) { + txtInput.setText(prompt); + } + } +} + +class OutputBox extends JPanel { + protected final LlmPromptModel model; + protected final JTextArea output = new JTextArea(); + protected final JPanel buttons = new JPanel(); + protected final JPopupMenu menu = new JPopupMenu(); + + public OutputBox(LlmPromptModel userData) { + this.model = userData; + setLayout(new BorderLayout()); + output.setEditable(false); + add(output, 0); + buttons.setVisible(false); + output.addMouseListener(new MouseAdapter() { + @Override + public void mouseEntered(MouseEvent e) { + buttons.setVisible(true); + } + + @Override + public void mouseExited(MouseEvent e) { + buttons.setVisible(false); + } + }); + output.setText(userData.text()); + output.setLineWrap(true); //Makes the text wrap to the next line + output.setWrapStyleWord(true); //Makes the text wrap full words, not just letters + output.setComponentPopupMenu(menu); + setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); + } + + @Override + public void setBackground(Color bg) { + super.setBackground(bg); + if (output != null) output.setBackground(bg); + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java new file mode 100644 index 00000000000..332fbfa29d1 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java @@ -0,0 +1,54 @@ +package org.key_project.key.llm; + +import java.net.URI; +import java.util.Set; +import java.util.TreeSet; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmSession { + private String model = "azure.gpt-4.1-mini"; + private String apiEndpoint; + private String authToken; + private Set selectedFiles = new TreeSet<>(); + + public LlmSession(String apiEndpoint, String authToken) { + this.apiEndpoint = apiEndpoint; + this.authToken = authToken; + } + + public String getApiEndpoint() { + return apiEndpoint; + } + + public void setApiEndpoint(String apiEndpoint) { + this.apiEndpoint = apiEndpoint; + } + + public String getAuthToken() { + return authToken; + } + + public void setAuthToken(String authToken) { + this.authToken = authToken; + } + + public String getModel() { + return model; + } + + public void setModel(String model) { + this.model = model; + } + + public Set getSelectedFiles() { + return selectedFiles; + } + + public void setSelectedFiles(Set selectedFiles) { + this.selectedFiles = selectedFiles; + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java new file mode 100644 index 00000000000..9ee39ce1abd --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java @@ -0,0 +1,66 @@ +package org.key_project.key.llm; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + +import java.util.ArrayList; +import java.util.List; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmSettings extends AbstractPropertiesSettings { + public static final LlmSettings INSTANCE = new LlmSettings(); + private static final String CATEGORY = "llm"; + + private final PropertyEntry authToken = createStringProperty("authToken", ""); + private final PropertyEntry apiEndpoint = createStringProperty("apiEndpoint", "https://ki-toolbox.scc.kit.edu/v1"); + private final PropertyEntry defaultModel = createStringProperty("defaultModel", "azure.gpt-4.1-mini"); + private final PropertyEntry> availableModels = createStringListProperty("availableModels", + "azure.gpt-4.1-mini,gpt-oss:120b,mixtral:8x22b,qwen3-vl:235b-a22b-instruct"); + + + public LlmSettings() { + super(CATEGORY); + } + + public LlmSettings(LlmSettings settings) { + this(); + setAvailableModels(new ArrayList<>(settings.getAvailableModels())); + setApiEndpoint(settings.getApiEndpoint()); + setAuthToken(settings.getAuthToken()); + } + + public String getApiEndpoint() { + return apiEndpoint.get(); + } + + public void setApiEndpoint(String apiEndpoint) { + this.apiEndpoint.set(apiEndpoint); + } + + public String getAuthToken() { + return authToken.get(); + } + + public void setAuthToken(String authToken) { + this.authToken.set(authToken); + } + + public List getAvailableModels() { + return availableModels.get(); + } + + public void setAvailableModels(List availableModels) { + this.availableModels.set(availableModels); + } + + public String getDefaultModel() { + return defaultModel.get(); + } + + public void setDefaultModel(String defaultModel) { + this.defaultModel.set(defaultModel); + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java new file mode 100644 index 00000000000..43b2e75f354 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java @@ -0,0 +1,43 @@ +package org.key_project.key.llm; + +import de.uka.ilkd.key.gui.settings.SettingsPanel; + +import javax.swing.*; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmSettingsUI extends SettingsPanel { + private final LlmSettings model; + private final JTextField txtApiBaseUrl; + private final JTextField txtAuthToken; + private final JComboBox cboDefaultModel; + private final JList selAvailableModels; + + public LlmSettingsUI(LlmSettings settings) { + model = new LlmSettings(settings); + + txtApiBaseUrl = addTextField("API Base URL", model.getApiEndpoint(), "", model::setApiEndpoint); + txtAuthToken = addTextField("Auth Token", model.getAuthToken(), "", model::setAuthToken); + cboDefaultModel = addComboBox("Default model", "Select the default model", + 0, + model::setDefaultModel, + model.getAvailableModels().toArray(new String[0])); + + model.addPropertyChangeListener("availableModels", evt -> { + var seq = model.getAvailableModels().toArray(new String[0]); + final var cboModel = new DefaultComboBoxModel<>(seq); + cboModel.setSelectedItem(cboDefaultModel.getSelectedItem()); + cboDefaultModel.setModel(cboModel); + }); + + selAvailableModels = addListBox("Available Models", "", + model::setAvailableModels, model.getAvailableModels(), s -> s); + } + + public LlmSettings getModel() { + return model; + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java new file mode 100644 index 00000000000..37dc4f5e7f7 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java @@ -0,0 +1,72 @@ +package org.key_project.key.llm; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.proof.Proof; +import org.jspecify.annotations.Nullable; + +import java.io.IOException; +import java.net.URI; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.List; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmUtils { + private static @Nullable LlmSession globalSession; + + public static LlmSession getSession(Proof proof) { + return getSession(LlmSettings.INSTANCE, proof); + } + + public static LlmSession getSession(LlmSettings settings, Proof proof) { + if (proof != null) { + var session = proof.lookup(LlmSession.class); + if (session != null) { + return session; + } + session = new LlmSession(settings.getApiEndpoint(), settings.getAuthToken()); + proof.register(session, LlmSession.class); + return session; + } else { + if (globalSession == null) { + globalSession = new LlmSession(settings.getApiEndpoint(), settings.getAuthToken()); + } + return globalSession; + } + } + + public static LlmSession getSession() { + return getSession(MainWindow.getInstance().getMediator().getSelectedProof()); + } + + public static List getPossibleFiles() throws IOException { + return getPossibleFiles(MainWindow.getInstance().getMediator().getSelectedProof()); + } + + public static List getPossibleFiles(@Nullable Proof selectedProof) throws IOException { + if (selectedProof == null) { + return List.of(); + } + + // selectedProof.getEnv().getServicesForEnvironment().getJavaModel().getBootClassPath(); + // selectedProof.getEnv().getServicesForEnvironment().getJavaModel().getClassPath(); + final var javaModel = selectedProof.getEnv().getServicesForEnvironment().getJavaModel(); + if (javaModel == null) { + return List.of(); + } + + var javaSrc = javaModel.getModelDir(); + + if (Files.isRegularFile(javaSrc)) { + return List.of(javaSrc.toUri()); + } + + try (var walker = Files.walk(javaSrc)) { + return walker.filter(Files::isRegularFile).map(Path::toUri).toList(); + } + } +} diff --git a/keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension new file mode 100644 index 00000000000..0f47a0e8cae --- /dev/null +++ b/keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -0,0 +1 @@ +org.key_project.key.llm.LlmExtension \ No newline at end of file diff --git a/settings.gradle b/settings.gradle index 063d12034fa..0efac9aead4 100644 --- a/settings.gradle +++ b/settings.gradle @@ -21,6 +21,7 @@ include 'keyext.exploration' include 'keyext.slicing' include 'keyext.caching' include 'keyext.isabelletranslation' +include 'keyext.llm' // ENABLE NULLNESS here or on the CLI // This flag is activated to enable the checker framework.