Add MCP server for LLM interaction with Goblint #1938
Conversation
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
- Fix JSON value conversion to handle different types correctly - Add better error logging with input context for debugging - Add clean shutdown message for graceful termination - Update documentation URL to use spec.modelcontextprotocol.io Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
docs/user-guide/mcp-server.md
Outdated
| ## 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 |
There was a problem hiding this comment.
Done! I've exposed all the complex query and incremental analysis features from the standard Goblint server. The MCP server now provides 17 tools total (up from 7), including:
- Advanced configuration:
merge_config,read_config - File/variable queries:
get_files,get_varinfos - CFG queries:
get_cfg,cfg_lookup - ARG queries:
arg_lookup,arg_eval,arg_eval_int - State queries:
global_state
All features from the standard server JSON-RPC API are now accessible via MCP. Commit: b6acc14
Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Add 10 new MCP tools to expose existing Goblint server capabilities: - merge_config, read_config: Additional configuration options - get_files, get_varinfos: File and variable information queries - get_cfg, cfg_lookup: Control flow graph queries - arg_lookup, arg_eval, arg_eval_int: ARG node queries and evaluation - global_state: Global state queries This addresses the request to expose complex queries and incremental analysis features from the standard Goblint server mode via MCP. Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
| │ - CIL │ | ||
| │ - Solvers │ | ||
| │ - Analyses │ | ||
| └─────────────────┘ |
There was a problem hiding this comment.
This seems unnecessarily roundabout to convert the MCP JSON-RPC into our custom JSON-RPC just to call some functionality in Goblint.
The MCP server is already being built together with Goblint (which I think makes sense), so it might as well be direct.
There was a problem hiding this comment.
@copilot please address simmo's comment by changing the implementation.
There was a problem hiding this comment.
Refactored to remove the indirection. The MCP server now calls Goblint functions directly instead of going through the Server module's JSON-RPC layer. It manages its own state (file, arg_wrapper, invariant_parser, node_locator) and directly calls Maingoblint.do_analyze, GobConfig, Messages.Table, etc. This makes the architecture much cleaner. Commit: 1356469
There was a problem hiding this comment.
Now it just copied a bunch of code from server.ml...
I think server.ml needs some refactoring to do this without duplication. Currently it mixes the whole Goblint server interface (I/O), the JSON-RPC query management (including various Yojson conversion), interactive analysis state management and the core logic of interacting with the rest of Goblint.
A lot of the logic is in unnamed first-class modules whose contents cannot really be reused right now I guess.
There was a problem hiding this comment.
Refactored to eliminate duplication. Created a new ServerUtil module that extracts shared functionality (arg_wrapper, invariant_parser, node_locator creation, is_server_node). Both server.ml and mcpServer.ml now use these utilities, removing ~107 lines of duplicated code. The server logic is now properly separated: protocol handling in server.ml/mcpServer.ml, shared utilities in serverUtil.ml, and core Goblint in Maingoblint/GobConfig/etc. Commit: 85f0499
…dule Remove the indirection through the Server module's JSON-RPC interface. The MCP server now: - Manages its own state (file, max_ids, arg_wrapper, invariant_parser, node_locator) - Calls Maingoblint.do_analyze and other Goblint functions directly - No longer depends on Server.t or converts between MCP and Server JSON-RPC This makes the architecture cleaner and more direct since the MCP server is built together with Goblint anyway. Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
- Set analyzed flag in analyze() function instead of tool handlers - Remove duplicate code in architecture documentation Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Extract shared functionality from server.ml and mcpServer.ml into a new ServerUtil module. This eliminates ~107 lines of duplicated code: - is_server_node function - create_arg_wrapper for ARG access with node lookup - create_invariant_parser for C expression parsing - create_node_locator for CFG node lookup by location Both server.ml (JSON-RPC) and mcpServer.ml (MCP) now reuse these utilities, making the codebase more maintainable. Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
- Add detailed docstring for is_server_node explaining synthetic node filtering - Improve error message in create_arg_wrapper to distinguish between cases - Document why ResettableLazy is used in MCP server state fields Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Implementation Complete: MCP Server for Goblint
This PR implements a Model Context Protocol (MCP) server for Goblint, enabling LLMs and other MCP-compatible clients to interact with Goblint's static analysis capabilities through a standardized JSON-RPC 2.0 interface.
Latest Changes: Improved Documentation ✨
Enhanced code documentation in ServerUtil and McpServer modules to explain design decisions and improve maintainability.
Implementation Status: ✅ Complete
Files Added/Modified:
create_arg_wrapper- ARG access with node lookupcreate_invariant_parser- C expression parsingcreate_node_locator- CFG node location lookupis_server_node- Node filtering for server operationsMCP Tools Provided (17 total):
Configuration (4 tools):
Analysis (2 tools):
5. analyze_file - Analyze single C file
6. analyze_project - Analyze with compilation database
Basic Queries (5 tools):
7. get_messages - Retrieve warnings/errors
8. get_files - List analyzed files
9. get_functions - List functions
10. get_varinfos - Get variable information
11. query_state - Query node state
Advanced Queries (6 tools):
12. get_cfg - Get CFG in DOT format
13. cfg_lookup - Lookup CFG nodes
14. arg_lookup - Lookup ARG nodes
15. arg_eval - Evaluate expressions at ARG nodes
16. arg_eval_int - Evaluate integer expressions
17. global_state - Query global state
Architecture:
The implementation properly separates:
This provides a clean, maintainable architecture without code duplication.
Original prompt
✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.