Add MCP server for LLM interaction with Goblint

docs/user-guide/mcp-server.md

@@ -0,0 +1,305 @@
+# MCP Server for Goblint
+
+This document describes the Model Context Protocol (MCP) server for Goblint, which allows Large Language Models (LLMs) and other MCP-compatible clients to interact with Goblint's static analysis capabilities.
+
+## Overview
+
+The MCP server provides a standardized JSON-RPC 2.0 based interface for:
+- Configuring Goblint analysis options
+- Running analysis on single C files
+- Running analysis on projects using compilation databases
+- Querying analysis results
+
+## Installation
+
+Build and install the MCP server:
+
+```bash
+make
+make install
+```
+
+This will install the `goblint-mcp-server` executable into your opam switch.
+
+## Usage
+
+The MCP server communicates via stdin/stdout using JSON-RPC 2.0:
+
+```bash
+goblint-mcp-server
+```
+
+The server follows the MCP protocol specification and can be integrated with any MCP-compatible client or LLM framework.
+
+## MCP Protocol
+
+### Initialization
+
+The client should initialize the connection with:
+
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 1,
+  "method": "initialize",
+  "params": {
+    "protocolVersion": "2024-11-05",
+    "capabilities": {},
+    "clientInfo": {
+      "name": "your-client-name",
+      "version": "1.0.0"
+    }
+  }
+}
+```
+
+### Available Tools
+
+The server provides the following tools (accessible via `tools/list` and `tools/call`):
+
+#### 1. configure
+
+Configure Goblint analysis options.
+
+**Input Schema:**
+```json
+{
+  "option": "string",
+  "value": "string"
+}
+```
+
+**Example:**
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 2,
+  "method": "tools/call",
+  "params": {
+    "name": "configure",
+    "arguments": {
+      "option": "ana.activated[+]",
+      "value": "'base'"
+    }
+  }
+}
+```
+
+#### 2. reset_config
+
+Reset all configuration to default values.
+
+**Input Schema:**
+```json
+{}
+```
+
+#### 3. analyze_file
+
+Run Goblint analysis on a single C source file.
+
+**Input Schema:**
+```json
+{
+  "file": "string",
+  "reset": "boolean (optional)"
+}
+```
+
+**Example:**
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 3,
+  "method": "tools/call",
+  "params": {
+    "name": "analyze_file",
+    "arguments": {
+      "file": "/path/to/source.c",
+      "reset": false
+    }
+  }
+}
+```
+
+#### 4. analyze_project
+
+Run Goblint analysis on a project using a compilation database.
+
+**Input Schema:**
+```json
+{
+  "compilation_database": "string",
+  "reset": "boolean (optional)"
+}
+```
+
+**Example:**
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 4,
+  "method": "tools/call",
+  "params": {
+    "name": "analyze_project",
+    "arguments": {
+      "compilation_database": "/path/to/compile_commands.json",
+      "reset": false
+    }
+  }
+}
+```
+
+#### 5. get_messages
+
+Retrieve all analysis messages (warnings, errors, etc.) from the last analysis run.
+
+**Input Schema:**
+```json
+{}
+```
+
+**Returns:** JSON array of message objects with location, severity, and text.
+
+#### 6. get_functions
+
+Get a list of all functions found in the analyzed code.
+
+**Input Schema:**
+```json
+{}
+```
+
+**Returns:** JSON array of function objects with name and location.
+
+#### 7. query_state
+
+Query the analysis state at a specific program location.
+
+**Input Schema:**
+```json
+{
+  "node": "string"
+}
+```
+
+**Example:**
+```json
+{
+  "jsonrpc": "2.0",
+  "id": 5,
+  "method": "tools/call",
+  "params": {
+    "name": "query_state",
+    "arguments": {
+      "node": "main:1"
+    }
+  }
+}
+```
+
+## Integration with LLM Frameworks
+
+### Claude Desktop
+
+Add to your Claude Desktop configuration (`~/Library/Application Support/Claude/claude_desktop_config.json` on macOS):
+
+```json
+{
+  "mcpServers": {
+    "goblint": {
+      "command": "goblint-mcp-server",
+      "args": []
+    }
+  }
+}
+```
+
+### Other MCP Clients
+
+The server is compatible with any MCP client that follows the Model Context Protocol specification. Refer to your client's documentation for integration instructions.
+
+## Example Workflow
+
+1. Initialize the connection
+2. (Optional) Configure analysis options using `configure`
+3. Run analysis using either `analyze_file` or `analyze_project`
+4. Query results using `get_messages`, `get_functions`, or `query_state`
+5. (Optional) Analyze another file or project
+
+## Advanced Usage
+
+### Compilation Databases
+
+For complex projects, use a compilation database (compile_commands.json) which can be generated by build systems like CMake or using tools like Bear:
+
+```bash
+# Using Bear to capture compilation commands
+bear -- make
+
+# This generates compile_commands.json
+goblint-mcp-server
+# Then use the analyze_project tool with the path to compile_commands.json
+```
+
+### Configuration Options
+
+Goblint has many configuration options. Common options include:
+
+- `ana.activated[+]`: Add an analysis (e.g., `'base'`, `'threadid'`, `'race'`)
+- `dbg.level`: Set debug level (`"info"`, `"debug"`, `"verbose"`)
+- `pre.includes[+]`: Add include directory
+- `ana.sv-comp.functions`: Enable SV-COMP mode
+
+See the [Goblint documentation](https://goblint.readthedocs.io/) for a complete list of options.
+
+## Troubleshooting
+
+### Server Not Responding
+
+Ensure the server is receiving properly formatted JSON-RPC 2.0 messages. Each message should be a single line terminated with a newline.
+
+### Analysis Errors
+
+Check the tool result's `isError` field and `content` for error messages. Common issues:
+- File not found
+- Invalid C syntax
+- Missing include files
+- Invalid configuration options
+
+### Debug Mode
+
+To enable debug logging, configure Goblint before analyzing:
+
+```json
+{
+  "method": "tools/call",
+  "params": {
+    "name": "configure",
+    "arguments": {
+      "option": "dbg.level",
+      "value": "\"debug\""
+    }
+  }
+}
+```
+
+## Limitations
+
+- The MCP server currently supports a subset of Goblint's full functionality
+- Complex queries and incremental analysis features from the standard Goblint server mode are not yet exposed via MCP
+- Large projects may take significant time to analyze
+
+## See Also
+
+- [Goblint Documentation](https://goblint.readthedocs.io/)
+- [Model Context Protocol Specification](https://modelcontextprotocol.io/)
+- [Goblint Server Mode Documentation](../user-guide/inspecting.md)
+
+## Contributing
+
+To add new MCP tools or improve the server, modify:
+- `src/util/mcpServer.ml` - Core MCP server implementation
+- `src/goblint_mcp_server.ml` - Executable entry point
+
+Follow the existing tool patterns and ensure new tools are documented in this file.