Uh oh!
There was an error while loading. Please reload this page.
[TS] Add usvm-mcp: MCP server exposing symbolic execution tools - #340
Draft
CaelmBleidd wants to merge 2 commits into
Draft
[TS] Add usvm-mcp: MCP server exposing symbolic execution tools#340CaelmBleidd wants to merge 2 commits into
CaelmBleidd wants to merge 2 commits into
Conversation
New module wrapping usvm-ts in a Model Context Protocol (stdio) server for hybrid LLM + symbolic analysis of TypeScript. Tools: generate_tests, check_exceptions, check_reachability, find_unreachable_code, find_counterexample (property falsification), list_methods, get_method_ir. TsTestResolver and ObjectClass are moved from the usvm-ts test source set to main so that the server can resolve symbolic states to concrete inputs.
There was a problem hiding this comment.
Pull request overview
Adds a new usvm-mcp Kotlin module that exposes the usvm-ts TypeScript symbolic execution engine via an MCP (stdio) server, and moves TS test-value resolution utilities into usvm-ts main sources so the MCP server can resolve symbolic states into concrete, JSON-serializable inputs/outcomes.
Changes:
- Introduces
usvm-mcpMCP server (stdio) with tools for method discovery, IR dumping, test generation, exception search, reachability, dead-code hints, and counterexample search. - Adds JSON DTOs +
TsTestValue/TsTest→ JSON conversion plus unit tests for JSON mapping. - Moves/introduces
TsTestResolver+Objectclass stub intousvm-tsmain to support resolving symbolic states outside tests.
Reviewed changes
Copilot reviewed 23 out of 26 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt | Adds symbolic-state → TsTest/TsTestValue resolver for TS runs (now used by MCP). |
| usvm-ts/src/main/kotlin/org/usvm/util/ObjectClass.kt | Adds helper to synthesize an Object class for resolution fallbacks. |
| usvm-mcp/src/test/kotlin/org/usvm/mcp/TsTestValueJsonTest.kt | Unit tests for TsTestValue JSON rendering and exception DTO mapping. |
| usvm-mcp/src/main/resources/logback.xml | Forces logging to stderr to avoid corrupting MCP stdio JSON-RPC stream. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/UsvmMcpServer.kt | Constructs the MCP server and registers all analysis tools. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ToolDefinitions.kt | Shared tool context, schema helpers, and argument extraction helpers (incl. timeouts). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/ListMethodsTool.kt | Implements list_methods tool (discover analyzable methods). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GetMethodIrTool.kt | Implements get_method_ir tool (CFG/statement listing). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/GenerateTestsTool.kt | Implements generate_tests tool (per-path concrete test cases). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindUnreachableCodeTool.kt | Implements find_unreachable_code tool (uncovered if-branches within budget). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/FindCounterexampleTool.kt | Implements find_counterexample tool (falsify boolean property functions). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckReachabilityTool.kt | Implements check_reachability tool (directed reachability + witness). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/tools/CheckExceptionsTool.kt | Implements check_exceptions tool (only failing paths). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/SceneCache.kt | Caches .ts → ETS IR conversion results and validates ArkAnalyzer env. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/scene/MethodLookup.kt | LLM-friendly class/method lookup with actionable errors. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/McpErrors.kt | Standardizes tool error handling into MCP isError results. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/Main.kt | Stdio server entrypoint with stdout guard (redirects System.out to stderr). |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/json/TsTestValueJson.kt | TsTestValue/TsTest → JSON conversion and exception DTO conversion. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/json/Dtos.kt | Defines serialized DTOs + shared JSON config for all tool responses. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/TsAnalysisRunner.kt | Runs analyses under a mutex and resolves collected states to concrete tests. |
| usvm-mcp/src/main/kotlin/org/usvm/mcp/exec/AnalysisOptions.kt | Provides UMachineOptions presets for coverage/targeted exploration with time budgets. |
| usvm-mcp/README.md | Documents setup, tools, result formats, and hybrid workflows. |
| usvm-mcp/build.gradle.kts | Adds the new module build: dependencies, JVM 11 target, and application packaging. |
| settings.gradle.kts | Includes usvm-mcp in the multi-module build. |
| buildSrc/src/main/kotlin/Dependencies.kt | Adds MCP Kotlin SDK dependency coordinates/version. |
| build.gradle.kts | Adds :usvm-mcp to the root project validation list. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+34
to
+42
| val stmts = method.cfg.stmts | ||
| val statements = stmts.mapIndexed { index, stmt -> | ||
| StmtDto( | ||
| index = index, | ||
| kind = stmt::class.simpleName ?: "EtsStmt", | ||
| text = stmt.toString(), | ||
| successors = method.cfg.successors(stmt).map { stmts.indexOf(it) }.sorted(), | ||
| ) | ||
| } |
Comment on lines
+50
to
+60
| val stmts = method.cfg.stmts | ||
| uncovered.map { finding -> | ||
| UnreachableFindingDto( | ||
| method = method.qualifiedName(), | ||
| ifStmtIndex = stmts.indexOf(finding.ifStmt), | ||
| ifStmt = finding.ifStmt.toString(), | ||
| uncoveredSuccessors = finding.successors.map { successor -> | ||
| StmtRefDto(index = stmts.indexOf(successor), text = successor.toString()) | ||
| }, | ||
| ) | ||
| } |
| * actionable instruction for the calling LLM/user (what went wrong and | ||
| * how to fix the call or the environment). | ||
| */ | ||
| class McpToolException(message: String) : RuntimeException(message) |
| } catch (e: McpToolException) { | ||
| errorResult(e.message ?: "Tool failed") | ||
| } catch (@Suppress("TooGenericExceptionCaught") e: Throwable) { | ||
| val frames = e.stackTrace.take(5).joinToString("\n") { " at $it" } |
| ResolvedCase(test = null, error = "${e::class.simpleName}: ${e.message}") | ||
| } | ||
| private suspend fun <T> withMachineLock(block: () -> T): T = |
| private suspend fun <T> withMachineLock(block: () -> T): T = | ||
| mutex.withLock { | ||
| runInterruptible(Dispatchers.IO) { |
| /** | ||
| * Finds a single analyzable method (a method with a non-empty CFG). | ||
| */ | ||
| fun findMethod(scene: EtsScene, className: String?, methodName: String): EtsMethod { |
| ) | ||
| } | ||
| val scene = EtsScene(listOf(etsFile)) | ||
| cache[path] = Entry(mtime, scene) |
| } | ||
| val scene = EtsScene(listOf(etsFile)) | ||
| cache[path] = Entry(mtime, scene) | ||
| return scene |
| return scene | ||
| } | ||
| private fun resolveTsFile(file: String): Path { |
| return path | ||
| } | ||
| private fun checkArkAnalyzerAvailable() { |
| import kotlin.time.Duration.Companion.milliseconds | ||
| /** Shared dependencies injected into every tool. */ | ||
| class UsvmToolContext( |
ArkAnalyzer is installed without a lockfile, so 'typescript' and '@types/node' float to the latest versions on every CI run. A recent '@types/node' release is not parseable by the TypeScript version the project builds with, failing 'npm run build' in the ci-ts job. Pin a known-good toolchain with 'npm install --no-save'.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for freeto join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
New module wrapping usvm-ts in a Model Context Protocol (stdio) server for hybrid LLM + symbolic analysis of TypeScript. Tools: generate_tests, check_exceptions, check_reachability, find_unreachable_code, find_counterexample (property falsification), list_methods, get_method_ir.
TsTestResolver and ObjectClass are moved from the usvm-ts test source set to main so that the server can resolve symbolic states to concrete inputs.