Skip to content

mcp-server.md

Latest commit

 

History

History
305 lines (229 loc) · 6.13 KB

mcp-server.md

File metadata and controls

305 lines (229 loc) · 6.13 KB
Raw

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:

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:

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:

{
  "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:

{
  "option": "string",
  "value": "string"
}

Example:

{
  "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:

{}

3. analyze_file

Run Goblint analysis on a single C source file.

Input Schema:

{
  "file": "string",
  "reset": "boolean (optional)"
}

Example:

{
  "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:

{
  "compilation_database": "string",
  "reset": "boolean (optional)"
}

Example:

{
  "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:

{}

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:

{}

Returns: JSON array of function objects with name and location.

7. query_state

Query the analysis state at a specific program location.

Input Schema:

{
  "node": "string"
}

Example:

{
  "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):

{
  "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:

# 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 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:

{
  "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

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.