From 20a3ae98c75159aa01ad7ee435c2f04ebf93e287 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 19 Nov 2025 10:12:54 +0100 Subject: [PATCH 1/7] LLM support in key.ui # Conflicts: # settings.gradle # Conflicts: # key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java # Conflicts: # key.ui/src/main/resources/logback.xml --- key.ui/build.gradle | 2 + .../java/de/uka/ilkd/key/gui/MainWindow.java | 4 +- .../gui/extension/api/KeYGuiExtension.java | 2 +- .../ilkd/key/gui/settings/SettingsPanel.java | 130 ++++++++--- key.ui/src/main/resources/logback.xml | 26 +++ keyext.llm/build.gradle | 10 + .../org/key_project/key/llm/LlmClient.java | 79 +++++++ .../org/key_project/key/llm/LlmExtension.java | 106 +++++++++ .../org/key_project/key/llm/LlmPrompt.java | 204 ++++++++++++++++++ .../org/key_project/key/llm/LlmSession.java | 32 +++ .../org/key_project/key/llm/LlmSettings.java | 66 ++++++ .../key_project/key/llm/LlmSettingsUI.java | 43 ++++ .../org/key_project/key/llm/LlmUtils.java | 28 +++ ...ilkd.key.gui.extension.api.KeYGuiExtension | 1 + settings.gradle | 2 + 15 files changed, 698 insertions(+), 37 deletions(-) create mode 100644 keyext.llm/build.gradle create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmSettings.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmSettingsUI.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java create mode 100644 keyext.llm/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 2347faba4d0..e3cbb9e0904 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -42,6 +42,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 55cf0cf2439..976880775fa 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 @@ -313,7 +313,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/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index 2ac0d426f44..ac7b21373fb 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 @@ -120,7 +120,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 2d3f91141c8..d16cfa543a3 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))); } /** @@ -119,7 +122,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; @@ -135,7 +138,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 { @@ -164,7 +167,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()); @@ -199,7 +202,7 @@ protected JTextField addFileChooserPanel(String title, String file, String info, * @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 -> { @@ -238,16 +241,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; @@ -262,7 +324,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; @@ -270,7 +332,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); @@ -287,7 +349,7 @@ 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 @@ -301,17 +363,15 @@ protected JTextField addTextField(String title, String text, String info, * 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 + * 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/resources/logback.xml b/key.ui/src/main/resources/logback.xml index 7e81d19ac27..38310965ab4 100644 --- a/key.ui/src/main/resources/logback.xml +++ b/key.ui/src/main/resources/logback.xml @@ -13,4 +13,30 @@ + + + + + [%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n + + + DEBUG + + + + + + + + + + + + + + + \ No newline at end of file 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..b48c8ed7e16 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java @@ -0,0 +1,79 @@ +package org.key_project.key.llm; + +import com.google.gson.GsonBuilder; +import org.apache.hc.client5.http.classic.methods.HttpGet; +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 org.key_project.util.java.IOUtil; +import org.slf4j.LoggerFactory; + +import java.io.IOException; +import java.util.List; +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; + + public LlmClient(LlmSession llmSession) { + this.llmSession = llmSession; + } + + @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 data = Map.of( + "model", "azure.gpt-4.1-mini", + "messages", List.of( + createMessage("system", "Du bist ein hilfreicher Assistent am KIT."), + createMessage("user", "Erkläre das Prinzip der Rayleigh-Streuung indrei Sätzen.") + ) + ); + 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 Map createMessage(String role, String content) { + return Map.of("role", role, "content", content); + } + + + 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/LlmExtension.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java new file mode 100644 index 00000000000..cf46d4bc6ba --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java @@ -0,0 +1,106 @@ +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 = new LlmPrompt(); + + @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) { + 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..e31178f4bd5 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java @@ -0,0 +1,204 @@ +package org.key_project.key.llm; + +import com.google.gson.GsonBuilder; +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.extension.api.TabPanel; +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import javax.swing.*; +import java.awt.*; +import java.awt.event.*; +import java.util.Collection; +import java.util.List; +import java.util.Map; +import java.util.concurrent.ForkJoinPool; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmPrompt extends JPanel implements TabPanel { + private static final Logger LOGGER = LoggerFactory.getLogger(LlmPrompt.class); + private final JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT); + + private final JEditorPane txtInput = new JEditorPane(); + + private final Box pOutput = new Box(BoxLayout.Y_AXIS); + + private final KeyAction actionSwitchOrientation = new SwitchOrientationAction(); + + public LlmPrompt() { + setLayout(new BorderLayout()); + add(splitPane, BorderLayout.CENTER); + splitPane.add(new JScrollPane(pOutput)); + splitPane.add(new JScrollPane(txtInput)); + + 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) { + var proof = MainWindow.getInstance().getMediator().getSelectedProof(); + var node = MainWindow.getInstance().getMediator().getSelectedNode(); + + LlmSession session = LlmUtils.getSession(proof); + LlmClient client = new LlmClient(session); + + var txt = txtInput.getText(); + addBox(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 (Exception ex) { + LOGGER.error(ex.getMessage(), ex); + handle(ex); + } + } + }; + ForkJoinPool.commonPool().submit(sw); + } + } + }); + } + + public static class OutputBox extends JPanel { + private final T userData; + private final JEditorPane output = new JEditorPane(); + private final JPanel buttons = new JPanel(); + private final JPopupMenu menu = new JPopupMenu(); + + public OutputBox(T userData) { + this(userData, userData.toString()); + } + + public OutputBox(T userData, String text) { + this.userData = 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(text); + + setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); + } + + @Override + public void setBackground(Color bg) { + super.setBackground(bg); + if (output != null) output.setBackground(bg); + } + } + + private OutputBox addInput(String text) { + var o= addBox(text, new RepromptAction(text)); + o.setBackground(new Color(130, 180, 220, 255)); + return o; + } + + private OutputBox addBox(T data, Action... action) { + OutputBox box = new OutputBox<>(data); + pOutput.add(box); + return box; + } + + private void handle(Map jsonResponse) { + LOGGER.info("LLM prompt {}", jsonResponse); + var o = new OutputBox<>(jsonResponse, + ((Map) ((Map) ((List) jsonResponse.get("choices")).get(0)).get("message")).get("content").toString()); + pOutput.add(o); + } + + private void handle(Throwable e) { + LOGGER.error("Error during LLM prompt", e); + var box = addBox(e); + box.setBackground(new Color(255, 180, 180, 255)); + } + + @Override + public @NonNull String getTitle() { + return "KiKI 2.0"; + } + + @Override + public @NonNull JComponent getComponent() { + return this; + } + + @Override + public @NonNull Collection getTitleActions() { + return List.of(actionSwitchOrientation); + } + + 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); + } + } + } + + class SelectContextAction extends KeyAction { + @Override + public void actionPerformed(ActionEvent e) { + + } + } + + class SendPromptAction extends KeyAction { + @Override + public void actionPerformed(ActionEvent e) { + String prompt = txtInput.getText(); + } + } + + 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); + } + } +} 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..2e777493737 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java @@ -0,0 +1,32 @@ +package org.key_project.key.llm; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmSession { + private String apiEndpoint; + private String authToken; + + 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; + } +} 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..b8840e30a47 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java @@ -0,0 +1,28 @@ +package org.key_project.key.llm; + +import de.uka.ilkd.key.proof.Proof; + +/** + * + * @author Alexander Weigl + * @version 1 (11/18/25) + */ +public class LlmUtils { + 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; + } + } + var session = new LlmSession(settings.getApiEndpoint(), settings.getAuthToken()); + if (proof != null) { + proof.register(session, LlmSession.class); + } + return session; + } +} 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 e217520e491..9acfd687806 100644 --- a/settings.gradle +++ b/settings.gradle @@ -30,6 +30,8 @@ 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. // System.setProperty("ENABLE_NULLNESS", "true") From 5f6439213428d4f8ea35d040c42652c0d0405da0 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 19 Nov 2025 10:43:01 +0100 Subject: [PATCH 2/7] add prompt and context --- .../ilkd/key/gui/settings/SettingsPanel.java | 71 ++++++++++--------- .../org/key_project/key/llm/LlmClient.java | 44 ++++++------ .../org/key_project/key/llm/LlmContext.java | 27 +++++++ .../org/key_project/key/llm/LlmExtension.java | 23 +++--- .../org/key_project/key/llm/LlmPrompt.java | 51 +++++++------ .../org/key_project/key/llm/LlmSession.java | 12 ++++ .../org/key_project/key/llm/LlmSettings.java | 16 +++-- .../key_project/key/llm/LlmSettingsUI.java | 18 +++-- .../org/key_project/key/llm/LlmUtils.java | 3 + 9 files changed, 167 insertions(+), 98 deletions(-) create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java 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 d16cfa543a3..5fe55210726 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,25 +4,26 @@ package de.uka.ilkd.key.gui.settings; +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; +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. @@ -39,19 +40,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))); } /** @@ -122,7 +123,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; @@ -138,7 +139,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 { @@ -167,7 +168,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()); @@ -202,7 +203,7 @@ protected JTextField addFileChooserPanel(String title, String file, String info, * @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 -> { @@ -242,8 +243,8 @@ protected void addTitledComponent(String title, JComponent component, String hel } protected JList addListBox(String title, String info, - final Validator> validator, - List seq, Function converter) { + final Validator> validator, + List seq, Function converter) { var model = new DefaultListModel(); model.addAll(seq); @@ -292,7 +293,7 @@ protected JList addListBox(String title, String info, btnAdd.addActionListener(addItem); ActionListener removeItem = e -> { - if(list.getSelectedIndex() != -1) { + if (list.getSelectedIndex() != -1) { model.removeElementAt(list.getSelectedIndex()); } }; @@ -302,14 +303,14 @@ protected JList addListBox(String title, String info, } 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; @@ -324,7 +325,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; @@ -332,7 +333,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); @@ -363,7 +364,7 @@ protected JTextField addTextField(String title, String text, String info, * the maximum value that can be entered * @param step * the step size used when changing the entered value using the JSpinner's arrow - * buttons + * buttons * @param info * arbitrary information about the text field * @param validator * a validator for checking the entered values @@ -371,7 +372,7 @@ protected JTextField addTextField(String title, String text, String info, * @return the created JSpinner */ 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/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 index b48c8ed7e16..72ea14327ae 100644 --- 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 @@ -1,7 +1,14 @@ +/* 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.key.llm; +import java.io.IOException; +import java.util.ArrayList; +import java.util.Map; +import java.util.concurrent.Callable; + import com.google.gson.GsonBuilder; -import org.apache.hc.client5.http.classic.methods.HttpGet; 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; @@ -9,13 +16,6 @@ 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 org.key_project.util.java.IOUtil; -import org.slf4j.LoggerFactory; - -import java.io.IOException; -import java.util.List; -import java.util.Map; -import java.util.concurrent.Callable; /** * @@ -24,9 +24,13 @@ */ public class LlmClient implements Callable> { private final LlmSession llmSession; + private final LlmContext context; + private final LlmContext.LlmMessage prompt; - public LlmClient(LlmSession llmSession) { + public LlmClient(LlmSession llmSession, LlmContext context, String message) { this.llmSession = llmSession; + this.context = context; + this.prompt = new LlmContext.LlmMessage("user", message); } @Override @@ -38,13 +42,13 @@ public Map call() throws Exception { 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", "azure.gpt-4.1-mini", - "messages", List.of( - createMessage("system", "Du bist ein hilfreicher Assistent am KIT."), - createMessage("user", "Erkläre das Prinzip der Rayleigh-Streuung indrei Sätzen.") - ) - ); + "model", llmSession.getModel(), + "messages", msg); + var gson = new GsonBuilder().create(); var stringBody = gson.toJson(data); request.setEntity(new StringEntity(stringBody)); @@ -54,12 +58,9 @@ public Map call() throws Exception { } } - private Map createMessage(String role, String content) { - return Map.of("role", role, "content", content); - } - - private static class GsonHttpClientResponseHandler extends AbstractHttpClientResponseHandler> { + private static class GsonHttpClientResponseHandler + extends AbstractHttpClientResponseHandler> { @Override public Map handleEntity(HttpEntity entity) throws IOException { String content = null; @@ -68,7 +69,8 @@ public Map handleEntity(HttpEntity entity) throws IOException { } catch (ParseException e) { throw new RuntimeException(e); } - //LoggerFactory.getLogger(LlmClient.class).error("Could not parse json response {}",content); + // LoggerFactory.getLogger(LlmClient.class).error("Could not parse json response + // {}",content); try { return new GsonBuilder().create().fromJson(content, Map.class); } catch (Exception 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..67348eaa2cc --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmContext.java @@ -0,0 +1,27 @@ +/* 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.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 index cf46d4bc6ba..de58a4e5c6a 100644 --- 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 @@ -1,5 +1,13 @@ +/* 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.key.llm; +import java.awt.event.ActionEvent; +import java.util.Collection; +import java.util.List; +import javax.swing.*; + import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; @@ -11,14 +19,10 @@ 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 @@ -26,13 +30,15 @@ */ @KeYGuiExtension.Info(experimental = false, description = "LLM support for KeY") public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu, - KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu { + KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, + KeYGuiExtension.MainMenu { private KeyAction actionStartLlmPromptForCurrentProof; private TabPanel uiPrompt = new LlmPrompt(); @Override public @NonNull List getContextActions( - @NonNull KeYMediator mediator, @NonNull ContextMenuKind kind, @NonNull Object underlyingObject) { + @NonNull KeYMediator mediator, @NonNull ContextMenuKind kind, + @NonNull Object underlyingObject) { return List.of(); } @@ -53,7 +59,8 @@ public void preInit(MainWindow window, KeYMediator mediator) { } @Override - public @NonNull Collection getPanels(@NonNull MainWindow window, @NonNull KeYMediator mediator) { + public @NonNull Collection getPanels(@NonNull MainWindow window, + @NonNull KeYMediator mediator) { return List.of(uiPrompt); } 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 index e31178f4bd5..e5839c38227 100644 --- 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 @@ -1,20 +1,24 @@ +/* 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.key.llm; -import com.google.gson.GsonBuilder; -import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.gui.actions.KeyAction; -import de.uka.ilkd.key.gui.extension.api.TabPanel; -import org.jspecify.annotations.NonNull; -import org.slf4j.Logger; -import org.slf4j.LoggerFactory; - -import javax.swing.*; import java.awt.*; import java.awt.event.*; import java.util.Collection; import java.util.List; import java.util.Map; import java.util.concurrent.ForkJoinPool; +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.gui.extension.api.TabPanel; + +import com.google.gson.GsonBuilder; +import org.jspecify.annotations.NonNull; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** * @@ -38,24 +42,24 @@ public LlmPrompt() { splitPane.add(new JScrollPane(txtInput)); 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)); + 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) { + if (e.getKeyChar() == KeyEvent.VK_ENTER + && (e.getModifiersEx() & InputEvent.CTRL_DOWN_MASK) > 0) { var proof = MainWindow.getInstance().getMediator().getSelectedProof(); var node = MainWindow.getInstance().getMediator().getSelectedNode(); LlmSession session = LlmUtils.getSession(proof); - LlmClient client = new LlmClient(session); - var txt = txtInput.getText(); - addBox(txt); - + LlmClient client = new LlmClient(session, new LlmContext(), txt); + addInput(txt); txtInput.setText(""); var sw = new SwingWorker, Void>() { @@ -68,9 +72,9 @@ protected Map doInBackground() throws Exception { protected void done() { try { handle(resultNow()); - } catch (Exception ex) { - LOGGER.error(ex.getMessage(), ex); - handle(ex); + } catch (IllegalStateException ex) { + LOGGER.error("Exceptional case", exceptionNow()); + handle(exceptionNow()); } } }; @@ -88,6 +92,7 @@ public static class OutputBox extends JPanel { public OutputBox(T userData) { this(userData, userData.toString()); + output.add(menu); } public OutputBox(T userData, String text) { @@ -115,12 +120,13 @@ public void mouseExited(MouseEvent e) { @Override public void setBackground(Color bg) { super.setBackground(bg); - if (output != null) output.setBackground(bg); + if (output != null) + output.setBackground(bg); } } private OutputBox addInput(String text) { - var o= addBox(text, new RepromptAction(text)); + var o = addBox(text, new RepromptAction(text)); o.setBackground(new Color(130, 180, 220, 255)); return o; } @@ -134,7 +140,8 @@ private OutputBox addBox(T data, Action... action) { private void handle(Map jsonResponse) { LOGGER.info("LLM prompt {}", jsonResponse); var o = new OutputBox<>(jsonResponse, - ((Map) ((Map) ((List) jsonResponse.get("choices")).get(0)).get("message")).get("content").toString()); + ((Map) ((Map) ((List) jsonResponse.get("choices")) + .get(0)).get("message")).get("content").toString()); pOutput.add(o); } 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 index 2e777493737..ed9421a96c0 100644 --- 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 @@ -1,3 +1,6 @@ +/* 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.key.llm; /** @@ -6,6 +9,7 @@ * @version 1 (11/18/25) */ public class LlmSession { + private String model = "azure.gpt-4.1-mini"; private String apiEndpoint; private String authToken; @@ -29,4 +33,12 @@ public String getAuthToken() { public void setAuthToken(String authToken) { this.authToken = authToken; } + + public String getModel() { + return model; + } + + public void setModel(String model) { + this.model = model; + } } 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 index 9ee39ce1abd..74ca106cdc0 100644 --- 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 @@ -1,10 +1,13 @@ +/* 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.key.llm; -import de.uka.ilkd.key.settings.AbstractPropertiesSettings; - import java.util.ArrayList; import java.util.List; +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + /** * * @author Alexander Weigl @@ -15,9 +18,12 @@ public class LlmSettings extends AbstractPropertiesSettings { 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", + 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"); 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 index 43b2e75f354..ed8e9aa31f5 100644 --- 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 @@ -1,9 +1,12 @@ +/* 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.key.llm; -import de.uka.ilkd.key.gui.settings.SettingsPanel; - import javax.swing.*; +import de.uka.ilkd.key.gui.settings.SettingsPanel; + /** * * @author Alexander Weigl @@ -19,12 +22,13 @@ public class LlmSettingsUI extends SettingsPanel { public LlmSettingsUI(LlmSettings settings) { model = new LlmSettings(settings); - txtApiBaseUrl = addTextField("API Base URL", model.getApiEndpoint(), "", model::setApiEndpoint); + 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])); + 0, + model::setDefaultModel, + model.getAvailableModels().toArray(new String[0])); model.addPropertyChangeListener("availableModels", evt -> { var seq = model.getAvailableModels().toArray(new String[0]); @@ -34,7 +38,7 @@ public LlmSettingsUI(LlmSettings settings) { }); selAvailableModels = addListBox("Available Models", "", - model::setAvailableModels, model.getAvailableModels(), s -> s); + model::setAvailableModels, model.getAvailableModels(), s -> s); } public LlmSettings getModel() { 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 index b8840e30a47..308cc50111e 100644 --- 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 @@ -1,3 +1,6 @@ +/* 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.key.llm; import de.uka.ilkd.key.proof.Proof; From e7f8f97fd520b425f7902ff7a90a8c87c1ddbc27 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 19 Nov 2025 15:32:02 +0100 Subject: [PATCH 3/7] Color management --- .../org/key_project/key/llm/LlmPrompt.java | 107 +++++++++++------- 1 file changed, 69 insertions(+), 38 deletions(-) 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 index e5839c38227..5058517d75c 100644 --- 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 @@ -13,9 +13,13 @@ 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.extension.api.TabPanel; import com.google.gson.GsonBuilder; +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; @@ -27,18 +31,33 @@ */ 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)); + + private 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 Box pOutput = new Box(BoxLayout.Y_AXIS); + 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(); public LlmPrompt() { setLayout(new BorderLayout()); add(splitPane, BorderLayout.CENTER); - splitPane.add(new JScrollPane(pOutput)); + final var comp = new JScrollPane(pOutput); + comp.getVerticalScrollBar().setUnitIncrement(16); + splitPane.add(comp); splitPane.add(new JScrollPane(txtInput)); handle(new Exception("Test Exception")); @@ -53,42 +72,17 @@ public LlmPrompt() { public void keyTyped(KeyEvent e) { if (e.getKeyChar() == KeyEvent.VK_ENTER && (e.getModifiersEx() & InputEvent.CTRL_DOWN_MASK) > 0) { - 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); + actionSendPrompt.run(); } } }); } public static class OutputBox extends JPanel { - private final T userData; - private final JEditorPane output = new JEditorPane(); - private final JPanel buttons = new JPanel(); - private final JPopupMenu menu = new JPopupMenu(); + protected final T userData; + protected final JEditorPane output = new JEditorPane(); + protected final JPanel buttons = new JPanel(); + protected final JPopupMenu menu = new JPopupMenu(); public OutputBox(T userData) { this(userData, userData.toString()); @@ -127,13 +121,16 @@ public void setBackground(Color bg) { private OutputBox addInput(String text) { var o = addBox(text, new RepromptAction(text)); - o.setBackground(new Color(130, 180, 220, 255)); + o.setBackground(COLOR_BG_INPUT.get()); return o; } - private OutputBox addBox(T data, Action... action) { + private OutputBox addBox(T data, Action... actions) { OutputBox box = new OutputBox<>(data); - pOutput.add(box); + for (Action it : actions) { + box.menu.add(it); + } + pOutput.add(box, new CC().growX()); return box; } @@ -142,13 +139,14 @@ private void handle(Map jsonResponse) { var o = new OutputBox<>(jsonResponse, ((Map) ((Map) ((List) jsonResponse.get("choices")) .get(0)).get("message")).get("content").toString()); - pOutput.add(o); + pOutput.add(o, new CC().growX()); + o.setBackground(COLOR_BG_ANSWER.get()); } private void handle(Throwable e) { LOGGER.error("Error during LLM prompt", e); var box = addBox(e); - box.setBackground(new Color(255, 180, 180, 255)); + box.setBackground(COLOR_BG_ERROR.get()); } @Override @@ -189,9 +187,42 @@ public void actionPerformed(ActionEvent e) { } class SendPromptAction extends KeyAction { + public SendPromptAction() { + setName("Send Prompt"); + } + @Override public void actionPerformed(ActionEvent e) { - String prompt = txtInput.getText(); + 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); } } From fb9d356a51b2e1cc070efa4b93fb426ffc873e0f Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 19 Nov 2025 22:25:49 +0100 Subject: [PATCH 4/7] file UI --- .../uka/ilkd/key/gui/actions/KeyAction.java | 9 + .../org/key_project/util/java/SwingUtil.java | 1 + .../org/key_project/key/llm/LlmExtension.java | 3 +- .../org/key_project/key/llm/LlmPrompt.java | 205 +++++++++++++----- .../org/key_project/key/llm/LlmSession.java | 13 ++ .../org/key_project/key/llm/LlmUtils.java | 53 ++++- 6 files changed, 226 insertions(+), 58 deletions(-) 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..ad58c71f6e8 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 @@ -9,6 +9,9 @@ import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; +import bibliothek.gui.dock.common.action.CAction; +import bibliothek.gui.dock.common.action.CButton; + import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK; /** @@ -155,4 +158,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/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/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 index de58a4e5c6a..06f2b9be13d 100644 --- 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 @@ -33,7 +33,7 @@ public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMen KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu { private KeyAction actionStartLlmPromptForCurrentProof; - private TabPanel uiPrompt = new LlmPrompt(); + private TabPanel uiPrompt; @Override public @NonNull List getContextActions( @@ -61,6 +61,7 @@ public void preInit(MainWindow window, KeYMediator mediator) { @Override public @NonNull Collection getPanels(@NonNull MainWindow window, @NonNull KeYMediator mediator) { + uiPrompt = new LlmPrompt(window, mediator); return List.of(uiPrompt); } 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 index 5058517d75c..ebf58cfe0ee 100644 --- 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 @@ -5,17 +5,31 @@ import java.awt.*; import java.awt.event.*; -import java.util.Collection; +import java.io.IOException; +import java.net.URI; +import java.util.*; import java.util.List; -import java.util.Map; import java.util.concurrent.ForkJoinPool; +import java.util.function.Supplier; import javax.swing.*; +import javax.swing.table.DefaultTableModel; +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 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 net.miginfocom.layout.CC; import net.miginfocom.layout.LC; @@ -39,7 +53,7 @@ public class LlmPrompt extends JPanel implements TabPanel { ColorSettings.define("llm.output.bg.error", "Background color in chat of LLM answers", new Color(255, 180, 180, 255)); - private static final ColorSettings.ColorProperty COLOR_BG_ANSWER = ColorSettings.define( + 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); @@ -51,21 +65,43 @@ public class LlmPrompt extends JPanel implements TabPanel { 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; - public LlmPrompt() { setLayout(new BorderLayout()); add(splitPane, BorderLayout.CENTER); final var comp = new JScrollPane(pOutput); comp.getVerticalScrollBar().setUnitIncrement(16); splitPane.add(comp); - splitPane.add(new JScrollPane(txtInput)); + 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"); - + addInput("Input data"); txtInput.addKeyListener(new KeyAdapter() { @Override @@ -78,75 +114,71 @@ public void keyTyped(KeyEvent e) { }); } - public static class OutputBox extends JPanel { - protected final T userData; - protected final JEditorPane output = new JEditorPane(); - protected final JPanel buttons = new JPanel(); - protected final JPopupMenu menu = new JPopupMenu(); + static class AddFileAction extends KeyAction { + private final Set selectedFiles; + private final URI file; - public OutputBox(T userData) { - this(userData, userData.toString()); - output.add(menu); + public AddFileAction(URI file, Set selectedFiles) { + this.file = file; + this.selectedFiles = selectedFiles; + setName(file.toString()); } - public OutputBox(T userData, String text) { - this.userData = 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(text); - - setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); + @Override + public void actionPerformed(ActionEvent e) { + var chk = (JCheckBox) e.getSource(); + if (chk.isSelected()) { + selectedFiles.add(file); + } else { + selectedFiles.remove(file); + } } + } - @Override - public void setBackground(Color bg) { - super.setBackground(bg); - if (output != null) - output.setBackground(bg); + 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(text, new RepromptAction(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(T data, Action... actions) { + 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); - var o = new OutputBox<>(jsonResponse, + final var text = ((Map) ((Map) ((List) jsonResponse.get("choices")) - .get(0)).get("message")).get("content").toString()); - pOutput.add(o, new CC().growX()); - o.setBackground(COLOR_BG_ANSWER.get()); + .get(0)).get("message")).get("content").toString(); + addBox(new LlmPromptModel<>(LlmPromptModel.Kind.OUTPUT, text, jsonResponse)); } private void handle(Throwable e) { - LOGGER.error("Error during LLM prompt", e); - var box = addBox(e); - box.setBackground(COLOR_BG_ERROR.get()); + addBox(new LlmPromptModel<>(LlmPromptModel.Kind.ERROR, e.toString(), e)); } @Override @@ -160,8 +192,36 @@ private void handle(Throwable e) { } @Override - public @NonNull Collection getTitleActions() { - return List.of(actionSwitchOrientation); + 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 { @@ -179,7 +239,7 @@ public void actionPerformed(ActionEvent e) { } } - class SelectContextAction extends KeyAction { + static class SelectContextAction extends KeyAction { @Override public void actionPerformed(ActionEvent e) { @@ -240,3 +300,42 @@ public void actionPerformed(ActionEvent e) { } } } + + +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 index ed9421a96c0..ac937a39c8c 100644 --- 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 @@ -3,6 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.key.llm; +import java.net.URI; +import java.util.Set; +import java.util.TreeSet; + /** * * @author Alexander Weigl @@ -12,6 +16,7 @@ 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; @@ -41,4 +46,12 @@ public String getModel() { 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/LlmUtils.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmUtils.java index 308cc50111e..0defd064801 100644 --- 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 @@ -3,14 +3,25 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.key.llm; +import java.io.IOException; +import java.net.URI; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.List; + +import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.proof.Proof; +import org.jspecify.annotations.Nullable; + /** * * @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); } @@ -21,11 +32,45 @@ public static LlmSession getSession(LlmSettings settings, Proof proof) { if (session != null) { return session; } - } - var session = new LlmSession(settings.getApiEndpoint(), settings.getAuthToken()); - if (proof != null) { + 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(); } - return session; } } From 0276b257c14a012733abc51ddaa2a44392804b67 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Mon, 15 Jun 2026 23:48:00 +0200 Subject: [PATCH 5/7] in the middle of work --- keyext.llm/build.gradle | 3 +++ settings.gradle | 1 + 2 files changed, 4 insertions(+) diff --git a/keyext.llm/build.gradle b/keyext.llm/build.gradle index 2744bed501b..e5a69d1bc17 100644 --- a/keyext.llm/build.gradle +++ b/keyext.llm/build.gradle @@ -7,4 +7,7 @@ dependencies { 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") + + implementation platform("io.modelcontextprotocol.sdk:mcp-bom:2.0.0") + implementation("io.modelcontextprotocol.sdk:mcp:2.0.0") } \ No newline at end of file diff --git a/settings.gradle b/settings.gradle index 9acfd687806..8b911983949 100644 --- a/settings.gradle +++ b/settings.gradle @@ -31,6 +31,7 @@ include "keyext.caching" include "keyext.isabelletranslation" include 'keyext.llm' +include 'keyext.llm.api' // ENABLE NULLNESS here or on the CLI // This flag is activated to enable the checker framework. From 5221a6ff55c88ea34774553b00f859a2562b3686 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 28 Jun 2026 07:50:17 +0200 Subject: [PATCH 6/7] got first tool call --- docs/LLM-Client-Extended.md | 282 ++++++++++++ key.ui/src/main/resources/logback.xml | 11 +- .../org/key_project/key/llm/BuiltInMCP.java | 39 ++ .../key/llm/LlmClientExtended.java | 415 +++++++++++++++++ .../org/key_project/key/llm/LlmPrompt.java | 69 +-- .../key_project/key/llm/LlmPromptModel.java | 33 ++ .../key_project/key/llm/LlmSettingsUI.java | 431 +++++++++++++++++- .../key_project/key/llm/McpClientStdio.java | 398 ++++++++++++++++ .../java/org/key_project/key/llm/Util.java | 47 ++ settings.gradle | 1 - 10 files changed, 1681 insertions(+), 45 deletions(-) create mode 100644 docs/LLM-Client-Extended.md create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/Util.java diff --git a/docs/LLM-Client-Extended.md b/docs/LLM-Client-Extended.md new file mode 100644 index 00000000000..2adc915505a --- /dev/null +++ b/docs/LLM-Client-Extended.md @@ -0,0 +1,282 @@ +# LlmClientExtended - Extended LLM Client with File Attachments and MCP Support + +## Overview + +`LlmClientExtended` is an enhanced version of the `LlmClient` class that adds support for: +1. **File Attachments** - Automatically include files from the session as multi-modal content +2. **MCP (Model Context Protocol)** - Integrate with MCP servers for tool calls and resource access + +## Package + +```java +package org.key_project.key.llm; +``` + +## Class Hierarchy + +``` +LlmClientExtended implements Callable> + └── McpClient (interface) - MCP client interface for tool/resource access +``` + +## Features + +### 1. File Attachments + +The extended client automatically includes files selected in the `LlmSession` as part of the message content. Files are formatted according to their type: + +| File Type | Format | Example | +|-----------|--------|---------| +| Text files (.java, .txt, .md, .key) | Code block with filename | ```` ```filename.java\n...content...\n``` ```` | +| Images (.png, .jpg, .jpeg, .gif, .webp) | Base64 encoded data URL | `data:image/png;base64,...` | + +### 2. MCP Support + +When an `McpClient` is provided, the extended client can: +- Discover available tools from MCP servers +- Send tool definitions to the LLM API +- Execute tool calls returned by the LLM +- Inject tool results back into the conversation +- Make follow-up API calls with results + +## Constructors + +### Without MCP Support + +```java +/** + * Creates a new extended LLM client without MCP support. + */ +public LlmClientExtended(LlmSession llmSession, LlmContext context, String message) +``` + +**Parameters:** +- `llmSession` - The LLM session containing API endpoint, authentication, and selected files +- `context` - The conversation context containing previous messages +- `message` - The user message to send + +### With MCP Support + +```java +/** + * Creates a new extended LLM client with optional MCP support. + */ +public LlmClientExtended(LlmSession llmSession, LlmContext context, String message, McpClient mcpClient) +``` + +**Parameters:** +- `llmSession` - The LLM session containing API endpoint, authentication, and selected files +- `context` - The conversation context containing previous messages +- `message` - The user message to send +- `mcpClient` - Optional MCP client for tool/resource access (may be null) + +## Usage Examples + +### Basic Usage with File Attachments + +```java +import org.key_project.key.llm.*; +import java.net.URI; +import java.util.Set; + +// Create session with API credentials +LlmSession session = new LlmSession("https://api.openai.com/v1", "sk-your-api-key"); +session.setModel("gpt-4-vision-preview"); + +// Add files to the session +Set files = session.getSelectedFiles(); +files.add(URI.create("file:///path/to/MyClass.java")); +files.add(URI.create("file:///path/to/diagram.png")); +session.setSelectedFiles(files); + +// Create context and add initial messages +LlmContext context = new LlmContext(); +context.addMessage(new LlmContext.LlmMessage("system", "You are a helpful coding assistant.")); + +// Create and execute the client +LlmClientExtended client = new LlmClientExtended(session, context, "Explain this code"); +Map response = client.call(); + +// Process response +var choices = (List) response.get("choices"); +var firstChoice = (Map) choices.get(0); +var message = (Map) firstChoice.get("message"); +String content = (String) message.get("content"); +System.out.println(content); +``` + +### Usage with MCP Server + +```java +import org.key_project.key.llm.*; + +// Start an MCP server process +ProcessBuilder pb = new ProcessBuilder( + "npx", "-y", "@modelcontextprotocol/server-filesystem", "/home/user/docs" +); +Process mcpServer = pb.start(); + +// Create and initialize MCP client +McpClientStdio mcpClient = new McpClientStdio(mcpServer); +mcpClient.initialize(); + +// Create session (no files needed when using MCP) +LlmSession session = new LlmSession("https://api.openai.com/v1", "sk-your-api-key"); +LlmContext context = new LlmContext(); + +// Create client with MCP support +LlmClientExtended client = new LlmClientExtended(session, context, + "List the files in my documents folder", mcpClient); + +// Execute and handle tool calls automatically +Map response = client.call(); + +// Cleanup +mcpClient.close(); +``` + +### Combined Usage (Files + MCP) + +```java +// Setup session with both files and MCP +LlmSession session = new LlmSession("https://api.openai.com/v1", "sk-your-api-key"); +session.setSelectedFiles(Set.of(URI.create("file:///path/to/code.java"))); + +// Initialize MCP client for additional capabilities +ProcessBuilder pb = new ProcessBuilder("npx", "-y", "@modelcontextprotocol/server-git", "/path/to/repo"); +McpClientStdio mcpClient = new McpClientStdio(pb.start()); +mcpClient.initialize(); + +// Use both features together +LlmContext context = new LlmContext(); +LlmClientExtended client = new LlmClientExtended(session, context, + "Review this code and check the git history for recent changes", mcpClient); + +Map response = client.call(); +mcpClient.close(); +``` + +## McpClient Interface + +The `McpClient` interface defines the contract for MCP implementations: + +```java +public interface McpClient { + /** Returns available tools in OpenAI API format. */ + List> getToolsAsOpenAiFormat(); + + /** Calls a tool with the given arguments. */ + Object callTool(String toolName, String arguments) throws Exception; + + /** Checks if the MCP client is still connected. */ + boolean isClosed(); + + /** Closes the MCP client and releases resources. */ + void close(); +} +``` + +## McpClientStdio Class + +`McpClientStdio` is a reference implementation that communicates with MCP servers via stdin/stdout using JSON-RPC 2.0. + +### Constructor + +```java +public McpClientStdio(Process process) throws IOException +``` + +### Methods + +| Method | Description | +|--------|-------------| +| `initialize()` | Initializes connection and discovers tools | +| `isInitialized()` | Returns true if successfully initialized | +| `getServerCapabilities()` | Returns server capabilities map | +| `close()` | Closes the connection and terminates the process | + +### Supported MCP Operations + +- `tools/list` - Discover available tools +- `tools/call` - Invoke a tool +- `resources/list` - List available resources +- `resources/read` - Read resource content + +## Architecture + +### Message Flow with File Attachments + +``` +┌─────────────┐ ┌──────────────────┐ ┌───────────────┐ +│ LlmSession │────▶│ LlmClientExtended│────▶│ OpenAI API │ +│ - files │ │ - attachments │ │ - gpt-4-vision│ +└─────────────┘ │ - multipart msg │ └───────────────┘ + └──────────────────┘ +``` + +### Message Flow with MCP + +``` +┌─────────────┐ ┌──────────────────┐ ┌───────────────┐ +│ McpClient │◀───▶│ LlmClientExtended│◀───▶│ OpenAI API │ +│ - tools │ │ - tool handling │ │ - tool_calls │ +└─────────────┘ └──────────────────┘ └───────────────┘ + │ │ │ + │ └────────────────────────┘ + │ (follow-up) + ▼ + Execute Tool + Return Result +``` + +## Thread Safety + +- `LlmClientExtended` is thread-safe for concurrent `call()` invocations +- Each call creates a new HTTP client instance +- The `McpClient` implementation should be thread-safe if used concurrently +- `ConcurrentHashMap` is used for internal data structures + +## Error Handling + +| Scenario | Behavior | +|----------|----------| +| File not found | Warning logged, file skipped | +| Unsupported file type | Treated as text content | +| MCP server timeout | IOException after 30 seconds | +| Tool execution failure | Error message returned to LLM | +| MCP process terminated | `isClosed()` returns true, tools disabled | + +## Dependencies + +The following libraries are required: + +- Apache HttpClient 5.x (`org.apache.httpcomponents.client5`) +- Gson (`com.google.gson`) +- SLF4J (`org.slf4j`) + +## Best Practices + +1. **Always close MCP clients** - Use try-with-resources or finally blocks +2. **Limit file count** - Too many attachments increase token usage +3. **Initialize before use** - Call `mcpClient.initialize()` before first use +4. **Check isClosed()** - Verify MCP connection before operations +5. **Handle exceptions** - Tool calls may fail; errors are gracefully returned to LLM + +## Related Classes + +- `LlmClient` - Original basic LLM client +- `LlmSession` - Session configuration (API endpoint, auth, files) +- `LlmContext` - Conversation history management +- `McpClientStdio` - Reference MCP implementation + +## Author + +@author Alexander Weigl + +## Version + +@version 1.0 (6/28/26) + +## License + +This file is part of KeY and is licensed under the GNU General Public License Version 2 (GPL-2.0-only). \ No newline at end of file diff --git a/key.ui/src/main/resources/logback.xml b/key.ui/src/main/resources/logback.xml index 38310965ab4..a916748c11c 100644 --- a/key.ui/src/main/resources/logback.xml +++ b/key.ui/src/main/resources/logback.xml @@ -14,10 +14,13 @@ - + + + + [%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java b/keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java new file mode 100644 index 00000000000..f418ce73875 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java @@ -0,0 +1,39 @@ +package org.key_project.key.llm; + +import java.util.List; +import java.util.Map; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public class BuiltInMCP implements LlmClientExtended.McpClient { + private boolean isClosed = false; + + @Override + public List> getToolsAsOpenAiFormat() { + return List.of( + Map.of("type", "function", + "function", Map.of( + "name", "echo", + "description", "returns the given string", + "parameters", Map.of("type", "object", "properties", Map.of())))); + } + + @Override + public Object callTool(String toolName, String arguments) throws Exception { + System.out.println("Calling tool " + toolName + " with arguments " + arguments); + return null; + } + + @Override + public boolean isClosed() { + return isClosed; + } + + @Override + public void close() { + isClosed = true; + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java new file mode 100644 index 00000000000..2ff66bd8880 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java @@ -0,0 +1,415 @@ +/* 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.key.llm; + +import java.io.IOException; +import java.net.URI; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.Base64; +import java.util.List; +import java.util.Map; +import java.util.concurrent.Callable; +import java.util.concurrent.ConcurrentHashMap; + +import com.google.gson.GsonBuilder; +import com.google.gson.JsonObject; +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 org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * Extended LLM client that supports file attachments and MCP (Model Context Protocol). + *

+ * This class extends {@link LlmClient} with the following capabilities: + *

    + *
  • File Attachments: Automatically includes attached files from {@link LlmSession#getSelectedFiles()} + * as multi-modal content in messages. Supports text files and images (base64 encoded).
    • + *
  • MCP Support: Integrates with MCP servers for tool calls and resource access. + * Handles tool result injection back into the conversation.
    • + *
+ *

+ * Thread Safety: This class is thread-safe for concurrent calls. However, the underlying + * HTTP client is created per call to ensure proper resource management. + * + * @author Alexander Weigl + * @version 1.0 (6/28/26) + * @see LlmClient + * @see LlmSession + * @see LlmContext + */ +public class LlmClientExtended implements Callable> { + private static final Logger logger = LoggerFactory.getLogger(LlmClientExtended.class); + + private final LlmSession llmSession; + private final LlmContext context; + private final LlmContext.LlmMessage prompt; + private final McpClient mcpClient; + + /** + * Creates a new extended LLM client without MCP support. + * + * @param llmSession The LLM session containing API endpoint, authentication, and selected files + * @param context The conversation context containing previous messages + * @param message The user message to send + */ + public LlmClientExtended(LlmSession llmSession, LlmContext context, String message) { + this(llmSession, context, message, null); + } + + /** + * Creates a new extended LLM client with optional MCP support. + * + * @param llmSession The LLM session containing API endpoint, authentication, and selected files + * @param context The conversation context containing previous messages + * @param message The user message to send + * @param mcpClient Optional MCP client for tool/resource access. May be null. + */ + public LlmClientExtended(LlmSession llmSession, LlmContext context, String message, McpClient mcpClient) { + this.llmSession = llmSession; + this.context = context; + this.prompt = new LlmContext.LlmMessage("user", message); + this.mcpClient = mcpClient; + } + + @Override + public Map call() throws Exception { + var url = llmSession.getApiEndpoint() + "/openai/chat/completions"; + var request = new HttpPost(url); + + request.addHeader("Authorization", "Bearer " + llmSession.getAuthToken()); + request.addHeader("Content-Type", "application/json"); + request.addHeader("Accept", "application/json"); + + // Build messages with file attachments + var messages = buildMessagesWithAttachments(); + + // Build request payload + var data = new ConcurrentHashMap(); + data.put("model", llmSession.getModel()); + data.put("messages", messages); + + // Add MCP tools if available + if (mcpClient != null && !mcpClient.isClosed()) { + var tools = mcpClient.getToolsAsOpenAiFormat(); + if (!tools.isEmpty()) { + data.put("tools", tools); + data.put("tool_choice", "auto"); + } + } + + var gson = new GsonBuilder().create(); + var stringBody = gson.toJson(data); + request.setEntity(new StringEntity(stringBody)); + + + logger.debug("Sending request to: {}", url); + + try (var client = HttpClients.createDefault()) { + var response = client.execute(request, new GsonHttpClientResponseHandler()); + + // Handle tool calls if present in response + return handleToolCallsIfPresent(response); + } + } + + /** + * Builds the complete message list including file attachments as multi-modal content. + *

+ * For each message, if there are selected files in the session, they are added as + * additional content parts to the user message. + * + * @return List of messages formatted for the OpenAI API, including file attachments + */ + private List> buildMessagesWithAttachments() { + var messages = new ArrayList>(); + var allMessages = new ArrayList<>(context.getMessages()); + allMessages.add(prompt); + + boolean isFirstUserMessage = true; + + for (var msg : allMessages) { + var messageMap = new ConcurrentHashMap(); + messageMap.put("role", msg.role()); + + // Only add file attachments to the first user message (the prompt) + if (isFirstUserMessage && "user".equals(msg.role()) && !llmSession.getSelectedFiles().isEmpty()) { + var contentList = new ArrayList>(); + + // Add text content + var textPart = new ConcurrentHashMap(); + textPart.put("type", "text"); + textPart.put("text", msg.content()); + contentList.add(textPart); + + // Add file attachments + for (URI fileUri : llmSession.getSelectedFiles()) { + try { + var filePart = readFileAsContentPart(fileUri); + if (filePart != null) { + contentList.add(filePart); + } + } catch (IOException e) { + logger.warn("Could not read file {}: {}", fileUri, e.getMessage()); + } + } + + messageMap.put("content", contentList); + isFirstUserMessage = false; + } else { + // Regular text-only message + messageMap.put("content", msg.content()); + } + + messages.add(messageMap); + } + + return messages; + } + + /** + * Reads a file from the given URI and formats it as a content part for the API. + *

+ * Supports: + *

    + *
  • Text files (.java, .txt, .md, .key, etc.) - sent as plain text
    • + *
  • Image files (.png, .jpg, .jpeg, .gif) - sent as base64 encoded data
    • + *
+ * + * @param uri The URI of the file to read + * @return A map representing the content part, or null if the file type is unsupported + * @throws IOException If reading the file fails + */ + private Map readFileAsContentPart(URI uri) throws IOException { + var path = Path.of(uri); + if (!Files.exists(path)) { + logger.warn("File does not exist: {}", uri); + return null; + } + + String fileName = path.getFileName().toString().toLowerCase(); + byte[] content = Files.readAllBytes(path); + + // Determine file type and format accordingly + if (isImageFile(fileName)) { + return createImageContentPart(content, fileName); + } else { + // Default to text content + return createTextContentPart(new String(content), fileName); + } + } + + /** + * Checks if the given filename corresponds to a supported image file. + */ + private boolean isImageFile(String fileName) { + return fileName.endsWith(".png") || fileName.endsWith(".jpg") || + fileName.endsWith(".jpeg") || fileName.endsWith(".gif") || + fileName.endsWith(".webp"); + } + + /** + * Creates a content part for an image file. + */ + private Map createImageContentPart(byte[] imageData, String fileName) { + String mimeType = getImageMimeType(fileName); + String base64Data = Base64.getEncoder().encodeToString(imageData); + + var imagePart = new ConcurrentHashMap(); + imagePart.put("type", "image_url"); + var imageUrl = new ConcurrentHashMap(); + imageUrl.put("url", "data:" + mimeType + ";base64," + base64Data); + imagePart.put("image_url", imageUrl); + + return imagePart; + } + + /** + * Gets the MIME type for an image file based on its extension. + */ + private String getImageMimeType(String fileName) { + if (fileName.endsWith(".png")) return "image/png"; + if (fileName.endsWith(".jpg") || fileName.endsWith(".jpeg")) return "image/jpeg"; + if (fileName.endsWith(".gif")) return "image/gif"; + if (fileName.endsWith(".webp")) return "image/webp"; + return "application/octet-stream"; + } + + /** + * Creates a content part for a text file. + */ + private Map createTextContentPart(String textContent, String fileName) { + var textPart = new ConcurrentHashMap(); + textPart.put("type", "text"); + textPart.put("text", "```" + fileName + "\n" + textContent + "\n```"); + return textPart; + } + + /** + * Handles tool calls in the LLM response by executing them via MCP and continuing the conversation. + *

+ * If the response contains tool calls and an MCP client is available, this method: + *

    + *
  1. Executes each tool call via the MCP client
    2. + *
  2. Adds the assistant's message and tool results to the context
    3. + *
  3. Makes a follow-up API call with the tool results
    4. + *
+ * + * @param response The initial response from the LLM API + * @return The final response after handling any tool calls + * @throws Exception If tool execution or follow-up call fails + */ + private Map handleToolCallsIfPresent(Map response) throws Exception { + if (mcpClient == null || mcpClient.isClosed()) { + return response; + } + + var choices = (List) response.get("choices"); + if (choices == null || choices.isEmpty()) { + return response; + } + + var firstChoice = (Map) choices.get(0); + var message = (Map) firstChoice.get("message"); + if (message == null) { + return response; + } + + var toolCalls = (List) message.get("tool_calls"); + if (toolCalls == null || toolCalls.isEmpty()) { + return response; + } + + logger.info("Handling {} tool calls", toolCalls.size()); + + // Add assistant's message to context + var assistantContent = (String) message.get("content"); + if (assistantContent != null) { + context.addMessage(new LlmContext.LlmMessage("assistant", assistantContent)); + } + + // Execute each tool call and collect results + var toolResults = new ArrayList>(); + for (Object toolCallObj : toolCalls) { + var toolCall = (Map) toolCallObj; + var id = (String) toolCall.get("id"); + var function = (Map) toolCall.get("function"); + var name = (String) function.get("name"); + var argumentsStr = (String) function.get("arguments"); + + logger.debug("Executing tool: {} with args: {}", name, argumentsStr); + + try { + var result = mcpClient.callTool(name, argumentsStr); + var toolResult = new ConcurrentHashMap(); + toolResult.put("role", "tool"); + toolResult.put("tool_call_id", id); + toolResult.put("content", result.toString()); + toolResults.add(toolResult); + + logger.debug("Tool {} returned: {}", name, result); + } catch (Exception e) { + logger.error("Tool {} failed: {}", name, e.getMessage()); + var errorResult = new ConcurrentHashMap(); + errorResult.put("role", "tool"); + errorResult.put("tool_call_id", id); + errorResult.put("content", "Error: " + e.getMessage()); + toolResults.add(errorResult); + } + } + + // Add tool results to context + for (var result : toolResults) { + var content = (String) result.get("content"); + context.addMessage(new LlmContext.LlmMessage("tool", content)); + } + + // Make follow-up call with tool results + logger.debug("Making follow-up call with tool results"); + return call(); + } + + /** + * MCP client interface for tool and resource access. + *

+ * Implementations should handle communication with MCP servers, + * including tool discovery, invocation, and resource retrieval. + */ + public interface McpClient { + /** + * Returns available tools in OpenAI API format. + * + * @return List of tool definitions + */ + List> getToolsAsOpenAiFormat(); + + /** + * Calls a tool with the given arguments. + * + * @param toolName The name of the tool to call + * @param arguments JSON string of arguments + * @return The tool result + * @throws Exception If the tool call fails + */ + Object callTool(String toolName, String arguments) throws Exception; + + /** + * Checks if the MCP client is still connected. + * + * @return true if connected, false otherwise + */ + boolean isClosed(); + + /** + * Closes the MCP client and releases resources. + */ + void close(); + } + + /** + * Simple HTTP-based response handler that parses JSON into a Map. + */ + public 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); + } + try { + return new GsonBuilder().create().fromJson(content, Map.class); + } catch (Exception e) { + throw new RuntimeException(e); + } + } + } + + public static class GsonHttpClientResponseHandlerObj + extends AbstractHttpClientResponseHandler { + @Override + public JsonObject handleEntity(HttpEntity entity) throws IOException { + String content = null; + try { + content = EntityUtils.toString(entity); + } catch (ParseException e) { + throw new RuntimeException(e); + } + try { + return new GsonBuilder().create().fromJson(content, JsonObject.class); + } catch (Exception e) { + throw new RuntimeException(e); + } + } + } +} \ No newline at end of file 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 index ebf58cfe0ee..6cb5ffbf117 100644 --- 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 @@ -3,17 +3,11 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.key.llm; -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; -import javax.swing.*; -import javax.swing.table.DefaultTableModel; - +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; @@ -25,12 +19,6 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.help.HelpFacade; import de.uka.ilkd.key.proof.Proof; - -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 net.miginfocom.layout.CC; import net.miginfocom.layout.LC; import net.miginfocom.swing.MigLayout; @@ -38,6 +26,17 @@ 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 @@ -46,22 +45,22 @@ 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)); + "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)); + 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); + "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))); + new JPanel(new MigLayout(new LC().fillX().debug().topToBottom().wrapAfter(1))); private final KeyAction actionSwitchOrientation = new SwitchOrientationAction(); private final SendPromptAction actionSendPrompt = new SendPromptAction(); @@ -99,8 +98,8 @@ public void selectedProofChanged(KeYSelectionEvent e) { 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)); + "{\"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() { @@ -140,7 +139,7 @@ private void populateFiles() { tblFiles.removeAll(); LlmSession session = LlmUtils.getSession(mediator.getSelectedProof()); List possibleFiles = - new ArrayList<>(LlmUtils.getPossibleFiles(mediator.getSelectedProof())); + new ArrayList<>(LlmUtils.getPossibleFiles(mediator.getSelectedProof())); Set selectedFiles = session.getSelectedFiles(); possibleFiles.sort(Comparator.comparing(URI::toString)); for (URI file : possibleFiles) { @@ -153,8 +152,9 @@ private void populateFiles() { } private OutputBox addInput(String text) { - var o = addBox(new LlmPromptModel(LlmPromptModel.Kind.INPUT, text, text), - new RepromptAction(text)); + var o = addBox( + new LlmPromptModel<>(LlmPromptModel.Kind.INPUT, text, text), + new RepromptAction(text)); o.setBackground(COLOR_BG_INPUT.get()); return o; } @@ -172,8 +172,8 @@ private OutputBox addBox(LlmPromptModel data, Action... actions) { 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(); + ((Map) ((Map) ((List) jsonResponse.get("choices")) + .get(0)).get("message")).get("content").toString(); addBox(new LlmPromptModel<>(LlmPromptModel.Kind.OUTPUT, text, jsonResponse)); } @@ -201,7 +201,7 @@ private void handle(Throwable e) { menu.add(menuModels); var groupModels = new CRadioGroup(); var llmSession = - LlmUtils.getSession(MainWindow.getInstance().getMediator().getSelectedProof()); + LlmUtils.getSession(MainWindow.getInstance().getMediator().getSelectedProof()); for (var m : LlmSettings.INSTANCE.getAvailableModels()) { var selected = m.equals(llmSession.getModel()); @@ -219,7 +219,7 @@ protected void changed() { }; var a = new DynamicCMenu("Settings", IconFactory.properties(MainWindow.TOOLBAR_ICON_SIZE), - supplier); + supplier); var help = HelpFacade.createHelpButton("user/LLM/"); return List.of(help, a); } @@ -261,8 +261,11 @@ public void run() { var node = MainWindow.getInstance().getMediator().getSelectedNode(); LlmSession session = LlmUtils.getSession(proof); + LlmClientExtended.McpClient mcpClient = new BuiltInMCP(); + var txt = txtInput.getText(); - LlmClient client = new LlmClient(session, new LlmContext(), txt); + var client = new LlmClientExtended(session, new LlmContext(), txt, mcpClient); + //var client = new LlmClient(session, new LlmContext(), txt); addInput(txt); txtInput.setText(""); diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java new file mode 100644 index 00000000000..d95140547de --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmPromptModel.java @@ -0,0 +1,33 @@ +package org.key_project.key.llm; + +import de.uka.ilkd.key.gui.colors.ColorSettings; + +import java.awt.*; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public record LlmPromptModel(Kind kind, String text, T data) { + public enum Kind { + INPUT(LlmPrompt.COLOR_BG_INPUT), + OUTPUT(LlmPrompt.COLOR_BG_ANSWER), + ERROR(LlmPrompt.COLOR_BG_ERROR); + + private final ColorSettings.ColorProperty bgColor; + + Kind(ColorSettings.ColorProperty bgColor) { + this.bgColor = bgColor; + } + + public ColorSettings.ColorProperty background() { + return bgColor; + } + } + + @Override + public String toString() { + return text; + } +} 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 index ed8e9aa31f5..bd6585279c8 100644 --- 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 @@ -3,10 +3,14 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.key.llm; -import javax.swing.*; - +import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.settings.SettingsPanel; +import javax.swing.*; +import java.awt.event.ActionEvent; +import java.util.ArrayList; +import java.util.Arrays; + /** * * @author Alexander Weigl @@ -18,17 +22,20 @@ public class LlmSettingsUI extends SettingsPanel { private final JTextField txtAuthToken; private final JComboBox cboDefaultModel; private final JList selAvailableModels; + private final JButton btnFetchModels; public LlmSettingsUI(LlmSettings settings) { model = new LlmSettings(settings); + btnFetchModels = new JButton(new FetchModelsAction()); + txtApiBaseUrl = - addTextField("API Base URL", model.getApiEndpoint(), "", model::setApiEndpoint); + 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])); + 0, + model::setDefaultModel, + model.getAvailableModels().toArray(new String[0])); model.addPropertyChangeListener("availableModels", evt -> { var seq = model.getAvailableModels().toArray(new String[0]); @@ -38,10 +45,420 @@ public LlmSettingsUI(LlmSettings settings) { }); selAvailableModels = addListBox("Available Models", "", - model::setAvailableModels, model.getAvailableModels(), s -> s); + model::setAvailableModels, model.getAvailableModels(), s -> s); + + addTitledComponent("test", btnFetchModels, "test"); } public LlmSettings getModel() { return model; } + + private class FetchModelsAction extends KeyAction { + public FetchModelsAction() { + setName("Fetch Models"); + } + + @Override + public void actionPerformed(ActionEvent e) { + var data = Util.httpGet(txtApiBaseUrl.getText() + "/openai/models", txtAuthToken.getText()); + if (data != null) { + var seq = new ArrayList(32); + for (var model : data.getAsJsonArray("data")) { + seq.add(model.getAsJsonObject().get("id").getAsString()); + } + selAvailableModels.clearSelection(); + var listModel = ((DefaultListModel) selAvailableModels.getModel()); + listModel.clear(); + listModel.addAll(seq); + cboDefaultModel.setSelectedItem(listModel.get(0)); + + /* + + "data": [ + { + "id": "kit.gpt-oss-120b", + "name": "kit.gpt-oss-120b", + "owned_by": "openai", + "openai": { + "id": "kit.gpt-oss-120b", + "name": "kit.gpt-oss-120b", + "owned_by": "openai", + "openai": { + "id": "kit.gpt-oss-120b" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.qwen3-reranker-8b", + "name": "kit.qwen3-reranker-8b", + "owned_by": "openai", + "openai": { + "id": "kit.qwen3-reranker-8b", + "name": "kit.qwen3-reranker-8b", + "owned_by": "openai", + "openai": { + "id": "kit.qwen3-reranker-8b" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.qwen3-embedding-8b", + "name": "kit.qwen3-embedding-8b", + "owned_by": "openai", + "openai": { + "id": "kit.qwen3-embedding-8b", + "name": "kit.qwen3-embedding-8b", + "owned_by": "openai", + "openai": { + "id": "kit.qwen3-embedding-8b" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.qwen3.5-397b-A17b", + "name": "kit.qwen3.5-397b-A17b", + "owned_by": "openai", + "openai": { + "id": "kit.qwen3.5-397b-A17b", + "name": "kit.qwen3.5-397b-A17b", + "owned_by": "openai", + "openai": { + "id": "kit.qwen3.5-397b-A17b" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.mistral-small-4-119b-a8b", + "name": "kit.mistral-small-4-119b-a8b", + "owned_by": "openai", + "openai": { + "id": "kit.mistral-small-4-119b-a8b", + "name": "kit.mistral-small-4-119b-a8b", + "owned_by": "openai", + "openai": { + "id": "kit.mistral-small-4-119b-a8b" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.minimax-m2.7-229b", + "name": "kit.minimax-m2.7-229b", + "owned_by": "openai", + "openai": { + "id": "kit.minimax-m2.7-229b", + "name": "kit.minimax-m2.7-229b", + "owned_by": "openai", + "openai": { + "id": "kit.minimax-m2.7-229b" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.gemma4-31b-it", + "name": "kit.gemma4-31b-it", + "owned_by": "openai", + "openai": { + "id": "kit.gemma4-31b-it", + "name": "kit.gemma4-31b-it", + "owned_by": "openai", + "openai": { + "id": "kit.gemma4-31b-it" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.flux.2-dev", + "name": "kit.flux.2-dev", + "owned_by": "openai", + "openai": { + "id": "kit.flux.2-dev", + "name": "kit.flux.2-dev", + "owned_by": "openai", + "openai": { + "id": "kit.flux.2-dev" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.voxtral-4b-tts-2603", + "name": "kit.voxtral-4b-tts-2603", + "owned_by": "openai", + "openai": { + "id": "kit.voxtral-4b-tts-2603", + "name": "kit.voxtral-4b-tts-2603", + "owned_by": "openai", + "openai": { + "id": "kit.voxtral-4b-tts-2603" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "kit.whisper-large-v3", + "name": "kit.whisper-large-v3", + "owned_by": "openai", + "openai": { + "id": "kit.whisper-large-v3", + "name": "kit.whisper-large-v3", + "owned_by": "openai", + "openai": { + "id": "kit.whisper-large-v3" + }, + "urlIdx": 0, + "connection_type": "local" + }, + "urlIdx": 0, + "connection_type": "local", + "provider": "" + }, + { + "id": "azure.gpt-4.1", + "name": "azure.gpt-4.1", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-4.1", + "name": "azure.gpt-4.1", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-4.1" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-4.1-mini", + "name": "azure.gpt-4.1-mini", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-4.1-mini", + "name": "azure.gpt-4.1-mini", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-4.1-mini" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-4.1-nano", + "name": "azure.gpt-4.1-nano", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-4.1-nano", + "name": "azure.gpt-4.1-nano", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-4.1-nano" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.o3", + "name": "azure.o3", + "owned_by": "openai", + "openai": { + "id": "azure.o3", + "name": "azure.o3", + "owned_by": "openai", + "openai": { + "id": "azure.o3" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.o4-mini", + "name": "azure.o4-mini", + "owned_by": "openai", + "openai": { + "id": "azure.o4-mini", + "name": "azure.o4-mini", + "owned_by": "openai", + "openai": { + "id": "azure.o4-mini" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-5.1", + "name": "azure.gpt-5.1", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5.1", + "name": "azure.gpt-5.1", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5.1" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-5", + "name": "azure.gpt-5", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5", + "name": "azure.gpt-5", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-5-mini", + "name": "azure.gpt-5-mini", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5-mini", + "name": "azure.gpt-5-mini", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5-mini" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-5-nano", + "name": "azure.gpt-5-nano", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5-nano", + "name": "azure.gpt-5-nano", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5-nano" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-5.4", + "name": "azure.gpt-5.4", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5.4", + "name": "azure.gpt-5.4", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5.4" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + }, + { + "id": "azure.gpt-5.5", + "name": "azure.gpt-5.5", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5.5", + "name": "azure.gpt-5.5", + "owned_by": "openai", + "openai": { + "id": "azure.gpt-5.5" + }, + "urlIdx": 1, + "connection_type": "external" + }, + "urlIdx": 1, + "connection_type": "external", + "provider": "" + } + ] +} + */ + System.out.println(data); + } + } + } } diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java b/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java new file mode 100644 index 00000000000..c3e8412a852 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java @@ -0,0 +1,398 @@ +/* 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.key.llm; + +import java.io.BufferedReader; +import java.io.IOException; +import java.io.InputStreamReader; +import java.io.OutputStream; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; +import java.util.concurrent.atomic.AtomicInteger; + +import com.google.gson.Gson; +import com.google.gson.GsonBuilder; +import com.google.gson.JsonObject; +import com.google.gson.JsonParser; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * A standard I/O-based MCP (Model Context Protocol) client implementation. + *

+ * This client communicates with MCP servers via stdin/stdout using JSON-RPC 2.0 protocol. + * It supports: + *

    + *
  • Tool discovery via {@code tools/list}
    • + *
  • Tool invocation via {@code tools/call}
    • + *
  • Resource access via {@code resources/read}
    • + *
  • Resource listing via {@code resources/list}
    • + *
+ *

+ * Usage Example: + * 

{@code
+ * // Start an MCP server process (e.g., a filesystem server)
+ * ProcessBuilder pb = new ProcessBuilder("npx", "-y", "@modelcontextprotocol/server-filesystem", "/home/user/docs");
+ * Process process = pb.start();
+ * 
+ * // Create the MCP client
+ * McpClientStdio mcpClient = new McpClientStdio(process);
+ * mcpClient.initialize();
+ * 
+ * // Use with LlmClientExtended
+ * LlmClientExtended client = new LlmClientExtended(session, context, "Hello", mcpClient);
+ * Map response = client.call();
+ * 
+ * // Cleanup
+ * mcpClient.close();
+ * }
+ * + * @author Alexander Weigl + * @version 1.0 (6/28/26) + * @see LlmClientExtended.McpClient + * @see Model Context Protocol Specification + */ +public class McpClientStdio implements LlmClientExtended.McpClient { + private static final Logger logger = LoggerFactory.getLogger(McpClientStdio.class); + private static final Gson GSON = new GsonBuilder().create(); + + private final Process process; + private final BufferedReader inputReader; + private final OutputStream outputStream; + private final AtomicInteger requestIdGenerator = new AtomicInteger(0); + private final Map serverCapabilities = new ConcurrentHashMap<>(); + private final List> cachedTools = new ArrayList<>(); + private volatile boolean closed = false; + private volatile boolean initialized = false; + + /** + * Creates a new MCP client that communicates with the given process via stdio. + *

+ * The process should already be started before calling this constructor. + * + * @param process The MCP server process + * @throws IOException If reading from the process fails during initialization + */ + public McpClientStdio(Process process) throws IOException { + this.process = process; + this.inputReader = new BufferedReader(new InputStreamReader(process.getInputStream())); + this.outputStream = process.getOutputStream(); + } + + /** + * Initializes the connection to the MCP server by sending an initialize request + * and discovering available tools. + * + * @throws IOException If communication with the server fails + * @throws InterruptedException If interrupted during initialization + */ + public void initialize() throws IOException, InterruptedException { + if (initialized) { + return; + } + + logger.debug("Initializing MCP connection..."); + + // Send initialize request + JsonObject initRequest = createJsonRpcRequest("initialize", Map.of( + "protocolVersion", "2024-11-05", + "capabilities", Map.of(), + "clientInfo", Map.of( + "name", "KeY-MCP-Client", + "version", "1.0.0" + ) + )); + + sendRequest(initRequest); + JsonObject initResponse = readResponse(); + + if (initResponse != null && initResponse.has("result")) { + JsonObject result = initResponse.getAsJsonObject("result"); + serverCapabilities.putAll(GSON.fromJson(result.get("capabilities"), Map.class)); + logger.debug("Server capabilities: {}", serverCapabilities); + } + + // Send initialized notification + JsonObject initializedNotification = createJsonRpcNotification("notifications/initialized"); + sendRequest(initializedNotification); + + // Discover tools + discoverTools(); + + initialized = true; + logger.info("MCP client initialized successfully"); + } + + /** + * Discovers available tools from the MCP server and caches them. + * + * @throws IOException If communication fails + * @throws InterruptedException If interrupted + */ + @SuppressWarnings("unchecked") + private void discoverTools() throws IOException, InterruptedException { + JsonObject toolsRequest = createJsonRpcRequest("tools/list", null); + sendRequest(toolsRequest); + JsonObject toolsResponse = readResponse(); + + cachedTools.clear(); + if (toolsResponse != null && toolsResponse.has("result")) { + JsonObject result = toolsResponse.getAsJsonObject("result"); + if (result.has("tools")) { + List toolsList = GSON.fromJson(result.get("tools"), List.class); + for (Object toolObj : toolsList) { + Map tool = (Map) toolObj; + cachedTools.add(convertToolToOpenAiFormat(tool)); + } + } + } + logger.debug("Discovered {} tools", cachedTools.size()); + } + + /** + * Converts an MCP tool definition to OpenAI API format. + * + * @param mcpTool The MCP tool definition + * @return The tool in OpenAI API format + */ + @SuppressWarnings("unchecked") + private Map convertToolToOpenAiFormat(Map mcpTool) { + var openAiTool = new HashMap(); + openAiTool.put("type", "function"); + + var function = new HashMap(); + function.put("name", mcpTool.get("name")); + function.put("description", mcpTool.getOrDefault("description", "")); + + // Convert MCP schema to JSON Schema format + if (mcpTool.containsKey("inputSchema")) { + function.put("parameters", mcpTool.get("inputSchema")); + } else { + var emptySchema = new HashMap(); + emptySchema.put("type", "object"); + emptySchema.put("properties", new HashMap<>()); + function.put("parameters", emptySchema); + } + + openAiTool.put("function", function); + return openAiTool; + } + + @Override + public List> getToolsAsOpenAiFormat() { + return new ArrayList<>(cachedTools); + } + + @Override + public Object callTool(String toolName, String argumentsJson) throws Exception { + if (!initialized) { + throw new IllegalStateException("MCP client not initialized"); + } + + logger.debug("Calling tool '{}' with args: {}", toolName, argumentsJson); + + Map args; + try { + args = GSON.fromJson(argumentsJson, Map.class); + } catch (Exception e) { + args = new HashMap<>(); + } + + JsonObject callRequest = createJsonRpcRequest("tools/call", Map.of( + "name", toolName, + "arguments", args + )); + + sendRequest(callRequest); + JsonObject response = readResponse(); + + if (response == null) { + throw new IOException("No response from MCP server"); + } + + if (response.has("error")) { + JsonObject error = response.getAsJsonObject("error"); + String errorMessage = error.has("message") ? error.get("message").getAsString() : "Unknown error"; + throw new RuntimeException("MCP tool call failed: " + errorMessage); + } + + if (response.has("result")) { + return parseToolResult(response.getAsJsonObject("result")); + } + + return null; + } + + /** + * Parses the tool result from MCP format to a human-readable string. + * + * @param result The result object from the MCP server + * @return A string representation of the result + */ + @SuppressWarnings("unchecked") + private String parseToolResult(JsonObject result) { + if (result.has("content")) { + List contentList = GSON.fromJson(result.get("content"), List.class); + StringBuilder sb = new StringBuilder(); + for (Object item : contentList) { + Map contentItem = (Map) item; + String type = (String) contentItem.get("type"); + if ("text".equals(type)) { + sb.append(contentItem.get("text")); + } else if ("image".equals(type)) { + sb.append("[Image data]"); + } else if ("resource".equals(type)) { + sb.append("[Resource data]"); + } + sb.append("\n"); + } + return sb.toString().trim(); + } + return result.toString(); + } + + @Override + public boolean isClosed() { + return closed || !process.isAlive(); + } + + @Override + public void close() { + if (closed) { + return; + } + closed = true; + + try { + // Try to send a graceful shutdown notification + try { + JsonObject shutdownNotification = createJsonRpcNotification("notifications/cancelled"); + sendRequest(shutdownNotification); + } catch (Exception e) { + // Ignore errors during shutdown + } + + outputStream.close(); + inputReader.close(); + process.destroy(); + + // Wait briefly for clean termination + try { + if (!process.waitFor(2, java.util.concurrent.TimeUnit.SECONDS)) { + process.destroyForcibly(); + } + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + process.destroyForcibly(); + } + + logger.info("MCP client closed"); + } catch (IOException e) { + logger.error("Error closing MCP client: {}", e.getMessage()); + } + } + + /** + * Sends a JSON-RPC request to the MCP server. + * + * @param request The JSON-RPC request object + * @throws IOException If writing to the process fails + */ + private void sendRequest(JsonObject request) throws IOException { + String json = GSON.toJson(request); + String message = json + "\n"; + outputStream.write(message.getBytes(java.nio.charset.StandardCharsets.UTF_8)); + outputStream.flush(); + logger.trace("Sent: {}", json); + } + + /** + * Reads a JSON-RPC response from the MCP server. + * + * @return The parsed JSON response, or null if no response + * @throws IOException If reading fails + * @throws InterruptedException If interrupted + */ + private JsonObject readResponse() throws IOException, InterruptedException { + // Read with timeout + long startTime = System.currentTimeMillis(); + long timeout = 30000; // 30 seconds + + while (System.currentTimeMillis() - startTime < timeout) { + if (inputReader.ready()) { + String line = inputReader.readLine(); + if (line != null && !line.isEmpty()) { + logger.trace("Received: {}", line); + try { + return JsonParser.parseString(line).getAsJsonObject(); + } catch (Exception e) { + logger.warn("Failed to parse JSON response: {}", line); + } + } + } + + if (!process.isAlive()) { + throw new IOException("MCP server process terminated unexpectedly"); + } + + Thread.sleep(100); + } + + throw new IOException("Timeout waiting for MCP server response"); + } + + /** + * Creates a JSON-RPC 2.0 request object. + * + * @param method The method name + * @param params The method parameters (may be null) + * @return A JSON-RPC request object + */ + private JsonObject createJsonRpcRequest(String method, Map params) { + JsonObject request = new JsonObject(); + request.addProperty("jsonrpc", "2.0"); + request.addProperty("id", requestIdGenerator.incrementAndGet()); + request.addProperty("method", method); + + if (params != null) { + request.add("params", GSON.toJsonTree(params)); + } + + return request; + } + + /** + * Creates a JSON-RPC 2.0 notification object (no ID, no response expected). + * + * @param method The method name + * @return A JSON-RPC notification object + */ + private JsonObject createJsonRpcNotification(String method) { + JsonObject notification = new JsonObject(); + notification.addProperty("jsonrpc", "2.0"); + notification.addProperty("method", method); + return notification; + } + + /** + * Returns the server capabilities received during initialization. + * + * @return A map of capability names to their values + */ + public Map getServerCapabilities() { + return new HashMap<>(serverCapabilities); + } + + /** + * Checks if the client has been successfully initialized. + * + * @return true if initialized, false otherwise + */ + public boolean isInitialized() { + return initialized; + } +} \ No newline at end of file diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/Util.java b/keyext.llm/src/main/java/org/key_project/key/llm/Util.java new file mode 100644 index 00000000000..a6afe5ed471 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/Util.java @@ -0,0 +1,47 @@ +package org.key_project.key.llm; + +import com.google.gson.GsonBuilder; +import com.google.gson.JsonObject; +import org.apache.hc.client5.http.classic.methods.HttpGet; +import org.apache.hc.client5.http.classic.methods.HttpPost; +import org.apache.hc.client5.http.impl.classic.HttpClients; +import org.apache.hc.core5.http.io.entity.StringEntity; + +import java.io.IOException; +import java.util.Map; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public class Util { + public static Object post(String url, String authToken, Map data) { + var request = new HttpPost(url); + request.addHeader("Authorization", "Bearer " + authToken); + request.addHeader("Content-Type", "application/json"); + request.addHeader("Accept", "application/json"); + // Build request payload + 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 LlmClientExtended.GsonHttpClientResponseHandler()); + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + public static JsonObject httpGet(String url, String authToken) { + var request = new HttpGet(url); + request.addHeader("Authorization", "Bearer " + authToken); + request.addHeader("Content-Type", "application/json"); + request.addHeader("Accept", "application/json"); + try (var client = HttpClients.createDefault()) { + return client.execute(request, new LlmClientExtended.GsonHttpClientResponseHandlerObj()); + } catch (IOException e) { + throw new RuntimeException(e); + } + } +} diff --git a/settings.gradle b/settings.gradle index 8b911983949..9acfd687806 100644 --- a/settings.gradle +++ b/settings.gradle @@ -31,7 +31,6 @@ include "keyext.caching" include "keyext.isabelletranslation" include 'keyext.llm' -include 'keyext.llm.api' // ENABLE NULLNESS here or on the CLI // This flag is activated to enable the checker framework. From 61cf05cfdc2d504673f465e20f37ea7c3038c7e1 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 28 Jun 2026 20:24:04 +0200 Subject: [PATCH 7/7] configuration of MCP --- .../settings/AbstractPropertiesSettings.java | 48 +- .../ilkd/key/gui/settings/SettingsPanel.java | 216 ++++++--- .../org/key_project/key/llm/BuiltInMCP.java | 39 -- .../key/llm/LlmClientExtended.java | 42 +- .../org/key_project/key/llm/LlmPrompt.java | 5 +- .../org/key_project/key/llm/LlmSession.java | 19 +- .../org/key_project/key/llm/LlmSettings.java | 35 +- .../key_project/key/llm/LlmSettingsUI.java | 435 ++---------------- .../org/key_project/key/llm/LlmUtils.java | 4 +- .../key_project/key/llm/McpClientStdio.java | 10 +- .../key/llm/mcp/BuiltInMCPClient.java | 73 +++ .../key_project/key/llm/mcp/DemoMcpTool.java | 69 +++ .../key/llm/mcp/FunctionDefinition.java | 54 +++ .../key_project/key/llm/mcp/JsonSchema.java | 213 +++++++++ .../org/key_project/key/llm/mcp/MCPTool.java | 9 + .../key_project/key/llm/mcp/McpClient.java | 40 ++ .../llm/mcp/McpToolNowAllowedException.java | 9 + .../key/llm/mcp/McpToolProvider.java | 12 + .../org/key_project/key/llm/mcp/Tool.java | 37 ++ ...rg.key_project.key.llm.mcp.McpToolProvider | 1 + 20 files changed, 811 insertions(+), 559 deletions(-) delete mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java create mode 100644 keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java create mode 100644 keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java index da5c4f1c7ba..e2cbac90027 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java @@ -4,13 +4,13 @@ package de.uka.ilkd.key.settings; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; + import java.util.*; import java.util.function.Function; import java.util.stream.Collectors; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; - /** * A base class for own settings based on properties. * @@ -128,7 +128,7 @@ public void writeSettings(Configuration props) { protected PropertyEntry createDoubleProperty(String key, double defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseDouble, - (it) -> ((Number) it).doubleValue()); + (it) -> ((Number) it).doubleValue()); propertyEntries.add(pe); return pe; } @@ -137,37 +137,47 @@ protected PropertyEntry createIntegerProperty(String key, int defValue) // A stored numeric value may deserialize as Integer or Long depending on its magnitude and // the settings format, so accept any Number rather than assuming a particular boxed type. PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseInt, - (it) -> Math.toIntExact(((Number) it).longValue())); + (it) -> Math.toIntExact(((Number) it).longValue())); propertyEntries.add(pe); return pe; } protected PropertyEntry createFloatProperty(String key, float defValue) { PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseFloat, - (it) -> ((Number) it).floatValue()); + (it) -> ((Number) it).floatValue()); propertyEntries.add(pe); return pe; } protected PropertyEntry createStringProperty(String key, String defValue) { PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString); + new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString); propertyEntries.add(pe); return pe; } protected PropertyEntry createBooleanProperty(String key, boolean defValue) { PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it); + new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it); propertyEntries.add(pe); return pe; } protected PropertyEntry> createStringSetProperty(String key, String defValue) { PropertyEntry> pe = new DefaultPropertyEntry<>(key, parseStringSet(defValue), - AbstractPropertiesSettings::parseStringSet, - AbstractPropertiesSettings::stringSetToString, - (it) -> new LinkedHashSet<>((Collection) it)); + AbstractPropertiesSettings::parseStringSet, + AbstractPropertiesSettings::stringSetToString, + (it) -> new LinkedHashSet<>((Collection) it)); + propertyEntries.add(pe); + return pe; + } + + protected PropertyEntry> createStringSetProperty(String key, Set defValue) { + PropertyEntry> pe = new DefaultPropertyEntry<>(key, defValue, + AbstractPropertiesSettings::parseStringSet, + AbstractPropertiesSettings::stringSetToString, + (it) -> + new LinkedHashSet<>(it != null ? (Collection) it : List.of())); propertyEntries.add(pe); return pe; } @@ -175,15 +185,15 @@ protected PropertyEntry> createStringSetProperty(String key, String /** * Creates a string list property. * - * @param key the key value of this property inside {@link Properties} instance + * @param key the key value of this property inside {@link Properties} instance * @param defValue a default value * @return returns a {@link PropertyEntry} */ protected PropertyEntry> createStringListProperty(@NonNull String key, - @Nullable String defValue) { + @Nullable String defValue) { PropertyEntry> pe = new DefaultPropertyEntry<>(key, parseStringList(defValue), - AbstractPropertiesSettings::parseStringList, - AbstractPropertiesSettings::stringListToString, it -> (List) it); + AbstractPropertiesSettings::parseStringList, + AbstractPropertiesSettings::stringListToString, it -> (List) it); propertyEntries.add(pe); return pe; } @@ -194,7 +204,7 @@ public interface PropertyEntry { void parseFrom(String value); - void set(T value); + void set(Object value); T get(); @@ -217,12 +227,12 @@ class DefaultPropertyEntry implements PropertyEntry { private final Function fromObject; private DefaultPropertyEntry(String key, T defaultValue, Function convert, - Function fromObject) { + Function fromObject) { this(key, defaultValue, convert, Objects::toString, fromObject); } private DefaultPropertyEntry(String key, T defaultValue, Function convert, - Function toString, Function fromObject) { + Function toString, Function fromObject) { this.key = key; this.defaultValue = defaultValue; this.convert = convert; @@ -241,7 +251,7 @@ public void parseFrom(String value) { } @Override - public void set(T value) { + public void set(Object value) { T old = get(); // only store non-null values if (value != null) { 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 5fe55210726..a3e98e2bf3b 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,26 +4,27 @@ package de.uka.ilkd.key.gui.settings; -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; -import javax.swing.*; - import de.uka.ilkd.key.gui.KeYFileChooser; +import de.uka.ilkd.key.gui.actions.KeyAction; 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 javax.swing.table.AbstractTableModel; +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. @@ -40,19 +41,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))); } /** @@ -123,7 +124,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; @@ -139,7 +140,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 { @@ -168,7 +169,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()); @@ -188,22 +189,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 selectionIndex - * which item to initially select - * @param validator - * validator - * @param items - * the items - * @param - * the type of the items + * @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 * @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 -> { @@ -242,9 +237,114 @@ protected void addTitledComponent(String title, JComponent component, String hel addRowWithHelp(helpText, label, component); } + /// Shows a list with the given `seq` items, and arbitrary actions + /// + protected JList addListBox(String title, + String info, + List seq, + KeyAction... action) { + var model = new DefaultListModel(); + model.addAll(seq); + + JList list = new JList<>(model); + JScrollPane field = new JScrollPane(list); + + var panel = new JPanel(new FlowLayout(FlowLayout.CENTER)); + for (var keyAction : action) { + panel.add(new JButton(keyAction)); + } + + 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); + + return list; + } + + + public record Column(String name, + Class clazz, + Getter value, + @Nullable Setter setValue) { + + public Column(String name, Class clazz, Getter value) { + this(name, clazz, value, null); + } + + public interface Getter extends Function { + } + + public interface Setter { + void set(T object, Object value); + } + } + + protected JTable addTableBox( + String title, String info, List seq, + Column... columns) { + var model = new AbstractTableModel() { + @Override + public Class getColumnClass(int columnIndex) { + return columns[columnIndex].clazz(); + } + + public String getColumnName(int columnIndex) { + return columns[columnIndex].name(); + } + + @Override + public void setValueAt(Object aValue, int rowIndex, int columnIndex) { + final T s = seq.get(rowIndex); + columns[columnIndex].setValue.set(s, aValue); + fireTableCellUpdated(rowIndex, columnIndex); + } + + @Override + public boolean isCellEditable(int rowIndex, int columnIndex) { + return columns[columnIndex].setValue != null; + } + + @Override + public int getRowCount() { + return seq.size(); + } + + @Override + public int getColumnCount() { + return columns.length; + } + + @Override + public Object getValueAt(int rowIndex, int columnIndex) { + return columns[columnIndex].value.apply(seq.get(rowIndex)); + } + }; + + var list = new JTable(model); + JScrollPane field = new JScrollPane(list); + var panel = new JPanel(new MigLayout(new LC().fillX())); + panel.add(field, new CC().span(3).growX().wrap()); + + 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); + + return list; + } + protected JList addListBox(String title, String info, - final Validator> validator, - List seq, Function converter) { + final Validator> validator, + List seq, Function converter) { var model = new DefaultListModel(); model.addAll(seq); @@ -303,14 +403,14 @@ protected JList addListBox(String title, String info, } 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; @@ -325,7 +425,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; @@ -333,7 +433,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); @@ -356,23 +456,18 @@ protected JTextField addTextField(String title, String text, String info, * 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 validator - * a validator for checking the entered values - * @param * the class of the minimum value + * @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 */ 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; @@ -417,8 +512,7 @@ protected void addSeparator(String titleText) { /** * Creates an empty validator instance. * - * @param - * arbitrary + * @param arbitrary * @return non-null */ protected Validator emptyValidator() { diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java b/keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java deleted file mode 100644 index f418ce73875..00000000000 --- a/keyext.llm/src/main/java/org/key_project/key/llm/BuiltInMCP.java +++ /dev/null @@ -1,39 +0,0 @@ -package org.key_project.key.llm; - -import java.util.List; -import java.util.Map; - -/** - * - * @author Alexander Weigl - * @version 1 (28.06.26) - */ -public class BuiltInMCP implements LlmClientExtended.McpClient { - private boolean isClosed = false; - - @Override - public List> getToolsAsOpenAiFormat() { - return List.of( - Map.of("type", "function", - "function", Map.of( - "name", "echo", - "description", "returns the given string", - "parameters", Map.of("type", "object", "properties", Map.of())))); - } - - @Override - public Object callTool(String toolName, String arguments) throws Exception { - System.out.println("Calling tool " + toolName + " with arguments " + arguments); - return null; - } - - @Override - public boolean isClosed() { - return isClosed; - } - - @Override - public void close() { - isClosed = true; - } -} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java index 2ff66bd8880..5eb918d04c4 100644 --- a/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java +++ b/keyext.llm/src/main/java/org/key_project/key/llm/LlmClientExtended.java @@ -23,6 +23,7 @@ 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 org.key_project.key.llm.mcp.McpClient; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -99,7 +100,7 @@ public Map call() throws Exception { // Add MCP tools if available if (mcpClient != null && !mcpClient.isClosed()) { - var tools = mcpClient.getToolsAsOpenAiFormat(); + var tools = mcpClient.getTools(); if (!tools.isEmpty()) { data.put("tools", tools); data.put("tool_choice", "auto"); @@ -120,7 +121,7 @@ public Map call() throws Exception { return handleToolCallsIfPresent(response); } } - + /** * Builds the complete message list including file attachments as multi-modal content. *

@@ -337,43 +338,6 @@ private Map handleToolCallsIfPresent(Map respons return call(); } - /** - * MCP client interface for tool and resource access. - *

- * Implementations should handle communication with MCP servers, - * including tool discovery, invocation, and resource retrieval. - */ - public interface McpClient { - /** - * Returns available tools in OpenAI API format. - * - * @return List of tool definitions - */ - List> getToolsAsOpenAiFormat(); - - /** - * Calls a tool with the given arguments. - * - * @param toolName The name of the tool to call - * @param arguments JSON string of arguments - * @return The tool result - * @throws Exception If the tool call fails - */ - Object callTool(String toolName, String arguments) throws Exception; - - /** - * Checks if the MCP client is still connected. - * - * @return true if connected, false otherwise - */ - boolean isClosed(); - - /** - * Closes the MCP client and releases resources. - */ - void close(); - } - /** * Simple HTTP-based response handler that parses JSON into a Map. */ 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 index 6cb5ffbf117..18da8c01771 100644 --- 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 @@ -23,6 +23,8 @@ import net.miginfocom.layout.LC; import net.miginfocom.swing.MigLayout; import org.jspecify.annotations.NonNull; +import org.key_project.key.llm.mcp.BuiltInMCPClient; +import org.key_project.key.llm.mcp.McpClient; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -261,10 +263,9 @@ public void run() { var node = MainWindow.getInstance().getMediator().getSelectedNode(); LlmSession session = LlmUtils.getSession(proof); - LlmClientExtended.McpClient mcpClient = new BuiltInMCP(); var txt = txtInput.getText(); - var client = new LlmClientExtended(session, new LlmContext(), txt, mcpClient); + var client = new LlmClientExtended(session, new LlmContext(), txt, session.getMcpClient()); //var client = new LlmClient(session, new LlmContext(), txt); addInput(txt); txtInput.setText(""); 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 index ac937a39c8c..553194fa9ac 100644 --- 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 @@ -3,6 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.key.llm; +import org.key_project.key.llm.mcp.BuiltInMCPClient; +import org.key_project.key.llm.mcp.McpClient; + import java.net.URI; import java.util.Set; import java.util.TreeSet; @@ -13,14 +16,24 @@ * @version 1 (11/18/25) */ public class LlmSession { + private final BuiltInMCPClient mcpClient; 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) { + /// Initialize + public static LlmSession createUsingSettings() { + return new LlmSession(LlmSettings.INSTANCE.getApiEndpoint(), + LlmSettings.INSTANCE.getAuthToken(), + LlmSettings.INSTANCE.getDefaultModel()); + } + + public LlmSession(String apiEndpoint, String authToken, String model) { this.apiEndpoint = apiEndpoint; this.authToken = authToken; + this.model = model; + mcpClient = new BuiltInMCPClient(); } public String getApiEndpoint() { @@ -54,4 +67,8 @@ public Set getSelectedFiles() { public void setSelectedFiles(Set selectedFiles) { this.selectedFiles = selectedFiles; } + + public McpClient getMcpClient() { + return mcpClient; + } } 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 index 74ca106cdc0..e779130d9bc 100644 --- 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 @@ -3,10 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.key.llm; +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + import java.util.ArrayList; import java.util.List; - -import de.uka.ilkd.key.settings.AbstractPropertiesSettings; +import java.util.Set; +import java.util.TreeSet; /** * @@ -19,13 +21,18 @@ public class LlmSettings extends AbstractPropertiesSettings { private final PropertyEntry authToken = createStringProperty("authToken", ""); private final PropertyEntry apiEndpoint = - createStringProperty("apiEndpoint", "https://ki-toolbox.scc.kit.edu/v1"); + createStringProperty("apiEndpoint", "https://ki-toolbox.scc.kit.edu/v1"); private final PropertyEntry defaultModel = - createStringProperty("defaultModel", "azure.gpt-4.1-mini"); + 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"); + createStringListProperty("availableModels", + "azure.gpt-4.1-mini,gpt-oss:120b,mixtral:8x22b,qwen3-vl:235b-a22b-instruct"); + private final PropertyEntry> allowedToolsWithApproval = + createStringSetProperty("allowedToolsWithApproval", new TreeSet<>()); + + private final PropertyEntry> allowedToolsWithoutApproval = + createStringSetProperty("allowedToolsWithoutApproval", new TreeSet<>()); public LlmSettings() { super(CATEGORY); @@ -69,4 +76,20 @@ public String getDefaultModel() { public void setDefaultModel(String defaultModel) { this.defaultModel.set(defaultModel); } + + public Set getAllowedToolsWithApproval() { + return allowedToolsWithApproval.get(); + } + + public Set getAllowedToolsWithoutApproval() { + return allowedToolsWithoutApproval.get(); + } + + public void setAllowedToolsWithApproval(Set val) { + allowedToolsWithApproval.set(val); + } + + public void setAllowedToolsWithoutApproval(Set val) { + allowedToolsWithoutApproval.set(val); + } } 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 index bd6585279c8..2f26e576a8c 100644 --- 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 @@ -5,11 +5,12 @@ import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.settings.SettingsPanel; +import org.key_project.key.llm.mcp.BuiltInMCPClient; import javax.swing.*; +import javax.swing.table.DefaultTableCellRenderer; import java.awt.event.ActionEvent; import java.util.ArrayList; -import java.util.Arrays; /** * @@ -24,6 +25,8 @@ public class LlmSettingsUI extends SettingsPanel { private final JList selAvailableModels; private final JButton btnFetchModels; + private final JTable selAvailableTools; + public LlmSettingsUI(LlmSettings settings) { model = new LlmSettings(settings); @@ -48,6 +51,51 @@ public LlmSettingsUI(LlmSettings settings) { model::setAvailableModels, model.getAvailableModels(), s -> s); addTitledComponent("test", btnFetchModels, "test"); + + var mcpClient = new BuiltInMCPClient().getAllToolNames().stream().toList(); + var name = new Column<>("Name", String.class, (String s) -> s); + var awR = new Column<>("AwR", Boolean.class, + (String s) -> model.getAllowedToolsWithApproval().contains(s), + (String s, Object value) -> { + if (value == Boolean.TRUE) + model.getAllowedToolsWithApproval().add(s); + else + model.getAllowedToolsWithApproval().remove(s); + } + ); + var awoR = new Column<>("AwoR", Boolean.class, (String s) -> model.getAllowedToolsWithoutApproval().contains(s), + (String s, Object value) -> { + if (value == Boolean.TRUE) + model.getAllowedToolsWithoutApproval().add(s); + else + model.getAllowedToolsWithoutApproval().remove(s); + } + ); + selAvailableTools = addTableBox("Tools Models", "", mcpClient, name, awR, awoR); + + // Set checkbox editor for boolean columns + selAvailableTools.setDefaultEditor(Boolean.class, new DefaultCellEditor(new JCheckBox())); + + // Set checkbox renderer for boolean columns + selAvailableTools.setDefaultRenderer(Boolean.class, new DefaultTableCellRenderer() { + @Override + public java.awt.Component getTableCellRendererComponent(JTable table, Object value, + boolean isSelected, boolean hasFocus, int row, int column) { + JCheckBox checkBox = new JCheckBox(); + if (value instanceof Boolean bool) { + checkBox.setSelected(bool); + } + checkBox.setHorizontalAlignment(JLabel.CENTER); + if (isSelected) { + checkBox.setBackground(table.getSelectionBackground()); + checkBox.setForeground(table.getSelectionForeground()); + } else { + checkBox.setBackground(table.getBackground()); + checkBox.setForeground(table.getForeground()); + } + return checkBox; + } + }); } public LlmSettings getModel() { @@ -72,391 +120,6 @@ public void actionPerformed(ActionEvent e) { listModel.clear(); listModel.addAll(seq); cboDefaultModel.setSelectedItem(listModel.get(0)); - - /* - - "data": [ - { - "id": "kit.gpt-oss-120b", - "name": "kit.gpt-oss-120b", - "owned_by": "openai", - "openai": { - "id": "kit.gpt-oss-120b", - "name": "kit.gpt-oss-120b", - "owned_by": "openai", - "openai": { - "id": "kit.gpt-oss-120b" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.qwen3-reranker-8b", - "name": "kit.qwen3-reranker-8b", - "owned_by": "openai", - "openai": { - "id": "kit.qwen3-reranker-8b", - "name": "kit.qwen3-reranker-8b", - "owned_by": "openai", - "openai": { - "id": "kit.qwen3-reranker-8b" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.qwen3-embedding-8b", - "name": "kit.qwen3-embedding-8b", - "owned_by": "openai", - "openai": { - "id": "kit.qwen3-embedding-8b", - "name": "kit.qwen3-embedding-8b", - "owned_by": "openai", - "openai": { - "id": "kit.qwen3-embedding-8b" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.qwen3.5-397b-A17b", - "name": "kit.qwen3.5-397b-A17b", - "owned_by": "openai", - "openai": { - "id": "kit.qwen3.5-397b-A17b", - "name": "kit.qwen3.5-397b-A17b", - "owned_by": "openai", - "openai": { - "id": "kit.qwen3.5-397b-A17b" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.mistral-small-4-119b-a8b", - "name": "kit.mistral-small-4-119b-a8b", - "owned_by": "openai", - "openai": { - "id": "kit.mistral-small-4-119b-a8b", - "name": "kit.mistral-small-4-119b-a8b", - "owned_by": "openai", - "openai": { - "id": "kit.mistral-small-4-119b-a8b" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.minimax-m2.7-229b", - "name": "kit.minimax-m2.7-229b", - "owned_by": "openai", - "openai": { - "id": "kit.minimax-m2.7-229b", - "name": "kit.minimax-m2.7-229b", - "owned_by": "openai", - "openai": { - "id": "kit.minimax-m2.7-229b" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.gemma4-31b-it", - "name": "kit.gemma4-31b-it", - "owned_by": "openai", - "openai": { - "id": "kit.gemma4-31b-it", - "name": "kit.gemma4-31b-it", - "owned_by": "openai", - "openai": { - "id": "kit.gemma4-31b-it" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.flux.2-dev", - "name": "kit.flux.2-dev", - "owned_by": "openai", - "openai": { - "id": "kit.flux.2-dev", - "name": "kit.flux.2-dev", - "owned_by": "openai", - "openai": { - "id": "kit.flux.2-dev" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.voxtral-4b-tts-2603", - "name": "kit.voxtral-4b-tts-2603", - "owned_by": "openai", - "openai": { - "id": "kit.voxtral-4b-tts-2603", - "name": "kit.voxtral-4b-tts-2603", - "owned_by": "openai", - "openai": { - "id": "kit.voxtral-4b-tts-2603" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "kit.whisper-large-v3", - "name": "kit.whisper-large-v3", - "owned_by": "openai", - "openai": { - "id": "kit.whisper-large-v3", - "name": "kit.whisper-large-v3", - "owned_by": "openai", - "openai": { - "id": "kit.whisper-large-v3" - }, - "urlIdx": 0, - "connection_type": "local" - }, - "urlIdx": 0, - "connection_type": "local", - "provider": "" - }, - { - "id": "azure.gpt-4.1", - "name": "azure.gpt-4.1", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-4.1", - "name": "azure.gpt-4.1", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-4.1" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-4.1-mini", - "name": "azure.gpt-4.1-mini", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-4.1-mini", - "name": "azure.gpt-4.1-mini", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-4.1-mini" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-4.1-nano", - "name": "azure.gpt-4.1-nano", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-4.1-nano", - "name": "azure.gpt-4.1-nano", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-4.1-nano" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.o3", - "name": "azure.o3", - "owned_by": "openai", - "openai": { - "id": "azure.o3", - "name": "azure.o3", - "owned_by": "openai", - "openai": { - "id": "azure.o3" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.o4-mini", - "name": "azure.o4-mini", - "owned_by": "openai", - "openai": { - "id": "azure.o4-mini", - "name": "azure.o4-mini", - "owned_by": "openai", - "openai": { - "id": "azure.o4-mini" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-5.1", - "name": "azure.gpt-5.1", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5.1", - "name": "azure.gpt-5.1", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5.1" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-5", - "name": "azure.gpt-5", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5", - "name": "azure.gpt-5", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-5-mini", - "name": "azure.gpt-5-mini", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5-mini", - "name": "azure.gpt-5-mini", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5-mini" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-5-nano", - "name": "azure.gpt-5-nano", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5-nano", - "name": "azure.gpt-5-nano", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5-nano" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-5.4", - "name": "azure.gpt-5.4", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5.4", - "name": "azure.gpt-5.4", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5.4" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - }, - { - "id": "azure.gpt-5.5", - "name": "azure.gpt-5.5", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5.5", - "name": "azure.gpt-5.5", - "owned_by": "openai", - "openai": { - "id": "azure.gpt-5.5" - }, - "urlIdx": 1, - "connection_type": "external" - }, - "urlIdx": 1, - "connection_type": "external", - "provider": "" - } - ] -} - */ System.out.println(data); } } 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 index 0defd064801..d658a19955e 100644 --- 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 @@ -32,12 +32,12 @@ public static LlmSession getSession(LlmSettings settings, Proof proof) { if (session != null) { return session; } - session = new LlmSession(settings.getApiEndpoint(), settings.getAuthToken()); + session = LlmSession.createUsingSettings(); proof.register(session, LlmSession.class); return session; } else { if (globalSession == null) { - globalSession = new LlmSession(settings.getApiEndpoint(), settings.getAuthToken()); + globalSession = LlmSession.createUsingSettings(); } return globalSession; } diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java b/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java index c3e8412a852..5c8207d622e 100644 --- a/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java +++ b/keyext.llm/src/main/java/org/key_project/key/llm/McpClientStdio.java @@ -18,6 +18,8 @@ import com.google.gson.GsonBuilder; import com.google.gson.JsonObject; import com.google.gson.JsonParser; +import org.key_project.key.llm.mcp.McpClient; +import org.key_project.key.llm.mcp.Tool; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -53,10 +55,10 @@ * * @author Alexander Weigl * @version 1.0 (6/28/26) - * @see LlmClientExtended.McpClient + * @see McpClient * @see Model Context Protocol Specification */ -public class McpClientStdio implements LlmClientExtended.McpClient { +public class McpClientStdio implements McpClient { private static final Logger logger = LoggerFactory.getLogger(McpClientStdio.class); private static final Gson GSON = new GsonBuilder().create(); @@ -183,8 +185,8 @@ private Map convertToolToOpenAiFormat(Map mcpToo } @Override - public List> getToolsAsOpenAiFormat() { - return new ArrayList<>(cachedTools); + public List getTools() { + return new ArrayList<>(); } @Override diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java new file mode 100644 index 00000000000..a29b961860e --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/BuiltInMCPClient.java @@ -0,0 +1,73 @@ +package org.key_project.key.llm.mcp; + +import org.jspecify.annotations.NullMarked; + +import java.util.List; +import java.util.ServiceLoader; +import java.util.Set; +import java.util.TreeSet; +import java.util.stream.Collectors; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +@NullMarked +public class BuiltInMCPClient implements McpClient { + private final Set allowedToolsWithApproval = new TreeSet<>(); + private final Set allowedToolsWithoutApproval = new TreeSet<>(); + + private final List tools; + private boolean isClosed = false; + + public BuiltInMCPClient() { + var loader = ServiceLoader.load(McpToolProvider.class); + tools = loader.stream().flatMap(it -> it.get().get().stream()).toList(); + } + + public Set getAllowedToolsWithApproval() { + return allowedToolsWithApproval; + } + + public Set getAllowedToolsWithoutApproval() { + return allowedToolsWithoutApproval; + } + + public Set getAllToolNames() { + return tools.stream().flatMap(it -> it.getTools().stream()) + .map(it -> it.function().name()) + .collect(Collectors.toCollection(TreeSet::new)); + } + + + @Override + public List getTools() { + var allowedTools = new TreeSet<>(allowedToolsWithApproval); + allowedToolsWithoutApproval.addAll(allowedTools); + return tools.stream().flatMap(it -> it.getTools().stream()) + .filter(it -> allowedTools.contains(it.function().name())) + .toList(); + } + + @Override + public Object callTool(String toolName, String arguments) throws McpToolNowAllowedException { + if (!allowedToolsWithApproval.contains(toolName) && + !allowedToolsWithoutApproval.contains(toolName)) { + throw new McpToolNowAllowedException(); + } + + System.out.println("Calling tool " + toolName + " with arguments " + arguments); + return new Object(); + } + + @Override + public boolean isClosed() { + return isClosed; + } + + @Override + public void close() { + isClosed = true; + } +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java new file mode 100644 index 00000000000..7608d517cf7 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/DemoMcpTool.java @@ -0,0 +1,69 @@ +package org.key_project.key.llm.mcp; + +import java.util.List; + +/** + * Demo implementation of an MCP client using type-safe record classes. + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public class DemoMcpTool implements McpToolProvider, McpClient { + @Override + public List get() { + return List.of(this); + } + + @Override + public List getTools() { + // Using the new type-safe record classes + var echoTool = new Tool(new FunctionDefinition( + "echo", + "returns the given string", + new JsonSchema("object") + )); + + // Example with parameters + var calculatorTool = new Tool(new FunctionDefinition( + "calculate", + "performs basic arithmetic operations", + JsonSchema.builder() + .withType("object") + .addProperty("operation", JsonSchema.builder() + .withType("string") + .withDescription("The operation to perform (add, subtract, multiply, divide)") + .build()) + .addProperty("a", JsonSchema.builder() + .withType("number") + .withDescription("First operand") + .build()) + .addProperty("b", JsonSchema.builder() + .withType("number") + .withDescription("Second operand") + .build()) + .addRequired("operation") + .addRequired("a") + .addRequired("b") + .build() + )); + return List.of(echoTool, calculatorTool); + } + + @Override + public Object callTool(String toolName, String arguments) { + return null; + } + + @Override + public boolean isClosed() { + return false; + } + + @Override + public void close() { + } + + +} + + diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java new file mode 100644 index 00000000000..80ef8f3704d --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/FunctionDefinition.java @@ -0,0 +1,54 @@ +package org.key_project.key.llm.mcp; + +import com.fasterxml.jackson.annotation.JsonProperty; + +import java.util.Map; + +/** + * Represents a function definition in OpenAI tool specification. + * + * @param name The name of the function + * @param description Optional description of what the function does + * @param parameters JSON Schema object defining the function's parameters + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public record FunctionDefinition( + @JsonProperty("name") String name, + @JsonProperty("description") String description, + @JsonProperty("parameters") JsonSchema parameters +) { + /** + * Creates a new FunctionDefinition with minimal required fields. + * + * @param name The name of the function + */ + public FunctionDefinition(String name) { + this(name, null, new JsonSchema()); + } + + /** + * Creates a new FunctionDefinition with name and description. + * + * @param name The name of the function + * @param description Description of what the function does + */ + public FunctionDefinition(String name, String description) { + this(name, description, new JsonSchema()); + } + + /** + * Converts this FunctionDefinition to a Map representation. + * + * @return Map containing the function definition + */ + public Map toMap() { + var mapBuilder = new java.util.HashMap(); + mapBuilder.put("name", name); + if (description != null) { + mapBuilder.put("description", description); + } + mapBuilder.put("parameters", parameters.toMap()); + return mapBuilder; + } +} \ No newline at end of file diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java new file mode 100644 index 00000000000..4b719a6bf85 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/JsonSchema.java @@ -0,0 +1,213 @@ +package org.key_project.key.llm.mcp; + +import com.fasterxml.jackson.annotation.JsonProperty; + +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; + +/** + * Represents a JSON Schema object for function parameters in OpenAI tool specification. + *

+ * This follows the JSON Schema specification as used by OpenAI's API. + * + * @param schemaType The type of the value (e.g., "object", "string", "number", "array") + * @param properties Map of property names to their schema definitions (for type "object") + * @param required List of required property names (for type "object") + * @param items Schema for array items (for type "array") + * @param enumValues List of allowed values (for enum constraints) + * @param description Optional description of the parameter + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public record JsonSchema( + @JsonProperty("type") String schemaType, + @JsonProperty("properties") Map properties, + @JsonProperty("required") List required, + @JsonProperty("items") JsonSchema items, + @JsonProperty("enum") List enumValues, + @JsonProperty("description") String description +) { + /** + * Creates an empty JSON Schema (defaults to an object type). + */ + public JsonSchema() { + this(null, null, null, null, null, null); + } + + /** + * Creates a JSON Schema with the specified type. + * + * @param schemaType The type of the value + */ + public JsonSchema(String schemaType) { + this(schemaType, null, null, null, null, null); + } + + /** + * Creates a JSON Schema for an object type with properties. + * + * @param properties Map of property names to their schema definitions + * @param required List of required property names + */ + public JsonSchema(Map properties, List required) { + this("object", properties, required, null, null, null); + } + + /** + * Converts this JsonSchema to a Map representation. + * + * @return Map containing the JSON Schema definition + */ + public Map toMap() { + var map = new LinkedHashMap(); + + if (schemaType != null) { + map.put("type", schemaType); + } + if (properties != null && !properties.isEmpty()) { + var propsMap = new LinkedHashMap(); + properties.forEach((k, v) -> propsMap.put(k, v.toMap())); + map.put("properties", propsMap); + } + if (required != null && !required.isEmpty()) { + map.put("required", required); + } + if (items != null) { + map.put("items", items.toMap()); + } + if (enumValues != null && !enumValues.isEmpty()) { + map.put("enum", enumValues); + } + if (description != null) { + map.put("description", description); + } + + return map; + } + + /** + * Creates a builder for JsonSchema. + * + * @return A new Builder instance + */ + public static Builder builder() { + return new Builder(); + } + + /** + * Builder class for creating JsonSchema instances. + */ + public static class Builder { + private String schemaType; + private Map properties; + private List required; + private JsonSchema items; + private List enumValues; + private String description; + + /** + * Sets the schema type. + * + * @param type The type (e.g., "object", "string", "number", "array", "boolean") + * @return this builder + */ + public Builder withType(String type) { + this.schemaType = type; + return this; + } + + /** + * Sets the properties map. + * + * @param properties Map of property names to their schema definitions + * @return this builder + */ + public Builder withProperties(Map properties) { + this.properties = properties; + return this; + } + + /** + * Adds a property to the schema. + * + * @param name The property name + * @param schema The property schema + * @return this builder + */ + public Builder addProperty(String name, JsonSchema schema) { + if (this.properties == null) { + this.properties = new LinkedHashMap<>(); + } + this.properties.put(name, schema); + return this; + } + + /** + * Sets the required properties list. + * + * @param required List of required property names + * @return this builder + */ + public Builder withRequired(List required) { + this.required = required; + return this; + } + + /** + * Adds a required property. + * + * @param propertyName The name of the required property + * @return this builder + */ + public Builder addRequired(String propertyName) { + if (this.required == null) { + this.required = new java.util.ArrayList<>(); + } + this.required.add(propertyName); + return this; + } + + /** + * Sets the items schema for array types. + * + * @param items The schema for array items + * @return this builder + */ + public Builder withItems(JsonSchema items) { + this.items = items; + return this; + } + + /** + * Sets the enum values. + * + * @param enumValues List of allowed values + * @return this builder + */ + public Builder withEnum(List enumValues) { + this.enumValues = enumValues; + return this; + } + + /** + * Sets the description. + * + * @param description The description + * @return this builder + */ + public Builder withDescription(String description) { + this.description = description; + return this; + } + + /** + * Builds the JsonSchema instance. + * + * @return A new JsonSchema + */ + public JsonSchema build() { + return new JsonSchema(schemaType, properties, required, items, enumValues, description); + } + } +} \ No newline at end of file diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java new file mode 100644 index 00000000000..82577095193 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/MCPTool.java @@ -0,0 +1,9 @@ +package org.key_project.key.llm.mcp; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public interface MCPTool { +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java new file mode 100644 index 00000000000..14d8b5d5a47 --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpClient.java @@ -0,0 +1,40 @@ +package org.key_project.key.llm.mcp; + +import java.util.List; + +/** + * MCP client interface for tool and resource access. + *

+ * Implementations should handle communication with MCP servers, + * including tool discovery, invocation, and resource retrieval. + */ +public interface McpClient { + /** + * Returns available tools in OpenAI API format. + * + * @return List of tool definitions + */ + List getTools(); + + /** + * Calls a tool with the given arguments. + * + * @param toolName The name of the tool to call + * @param arguments JSON string of arguments + * @return The tool result + * @throws Exception If the tool call fails + */ + Object callTool(String toolName, String arguments) throws Exception; + + /** + * Checks if the MCP client is still connected. + * + * @return true if connected, false otherwise + */ + boolean isClosed(); + + /** + * Closes the MCP client and releases resources. + */ + void close(); +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java new file mode 100644 index 00000000000..ee7756b3e7a --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolNowAllowedException.java @@ -0,0 +1,9 @@ +package org.key_project.key.llm.mcp; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public class McpToolNowAllowedException extends Exception { +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java new file mode 100644 index 00000000000..a83ab6adc7c --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/McpToolProvider.java @@ -0,0 +1,12 @@ +package org.key_project.key.llm.mcp; + +import java.util.List; + +/** + * + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +interface McpToolProvider { + List get(); +} diff --git a/keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java new file mode 100644 index 00000000000..758f721609d --- /dev/null +++ b/keyext.llm/src/main/java/org/key_project/key/llm/mcp/Tool.java @@ -0,0 +1,37 @@ +package org.key_project.key.llm.mcp; + +import com.fasterxml.jackson.annotation.JsonProperty; + +/** + * Represents a tool definition in OpenAI API format. + * + * @param type The type of the tool (e.g., "function") + * @param function The function definition + * @author Alexander Weigl + * @version 1 (28.06.26) + */ +public record Tool( + @JsonProperty("type") String type, + @JsonProperty("function") FunctionDefinition function +) { + /** + * Creates a new Tool with type "function". + * + * @param function The function definition + */ + public Tool(FunctionDefinition function) { + this("function", function); + } + + /** + * Converts this Tool to a Map representation. + * + * @return Map containing the tool definition + */ + public java.util.Map toMap() { + return java.util.Map.of( + "type", type, + "function", function.toMap() + ); + } +} \ No newline at end of file diff --git a/keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider b/keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider new file mode 100644 index 00000000000..c6d4023acc4 --- /dev/null +++ b/keyext.llm/src/main/resources/META-INF/services/org.key_project.key.llm.mcp.McpToolProvider @@ -0,0 +1 @@ +org.key_project.key.llm.mcp.DemoMcpTool \ No newline at end of file