Skip to content

Commit a6db2e1

Browse files
ZippeyKeys12ZippeyKeys12
committed
Basic MCP server (cn mcp)
1 parent 449e794 commit a6db2e1

File tree

5 files changed

+350
-4
lines changed

5 files changed

+350
-4
lines changed

‎bin/common.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,8 @@ open CB.Pipeline
44
open Cn
55
open Setup
66

7+
let version_str = Cn_version.git_version ^ " [" ^ Cn_version.git_version_date ^ "]"
8+
79
let print_log_file =
810
let print_count = ref 0 in
911
let print_file filename = function

‎bin/dune

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,18 @@
33
(modes exe)
44
(public_name cn)
55
(package cn)
6-
(libraries cmdliner cn menhirLib monomorphic ocamlgraph result str unix))
6+
(libraries
7+
cmdliner
8+
cn
9+
lwt
10+
lwt.unix
11+
menhirLib
12+
monomorphic
13+
ocamlgraph
14+
result
15+
str
16+
unix
17+
yojson))
718

819
; There is already a Version in Cerb_frontend, but if new commits only require
920
; rebuilding the CN backend that module will be out of date.

‎bin/main.ml

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
open Cmdliner
22

3-
let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd ]
3+
let subcommands = [ Wf.cmd; Verify.cmd; Test.cmd; Instrument.cmd; SeqTest.cmd; Mcp.cmd ]
44

55
let () =
6-
let version_str = Cn_version.git_version ^ " [" ^ Cn_version.git_version_date ^ "]" in
7-
let cn_info = Cmd.info "cn" ~version:version_str in
6+
let cn_info = Cmd.info "cn" ~version:Common.version_str in
87
Stdlib.exit @@ Cmd.(eval (group cn_info subcommands))

‎bin/mcp.ml

Lines changed: 332 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,332 @@
1+
module YB = Yojson.Basic
2+
3+
(** Basic MCP message types *)
4+
type mcp_request =
5+
{ id : int;
6+
method_ : string;
7+
params : YB.t option
8+
}
9+
10+
let parse_request json =
11+
let open YB.Util in
12+
{ id = json |> member "id" |> to_int;
13+
method_ = json |> member "method" |> to_string;
14+
params = json |> member "params" |> to_option (fun x -> x)
15+
}
16+
17+
18+
type mcp_notif = { method_ : string }
19+
20+
let parse_notif json =
21+
let open YB.Util in
22+
{ method_ = json |> member "method" |> to_string }
23+
24+
25+
let json_of_result id result =
26+
`Assoc [ ("jsonrpc", `String "2.0"); ("id", `Int id); ("result", result) ]
27+
28+
29+
let json_of_error id code ?(data : string option) message =
30+
`Assoc
31+
[ ("jsonrpc", `String "2.0");
32+
("id", `Int id);
33+
( "error",
34+
`Assoc
35+
([ ("code", `Int code); ("message", `String message) ]
36+
@ match data with Some d -> [ ("data", `String d) ] | None -> []) )
37+
]
38+
39+
40+
(** Tools available via MCP *)
41+
let available_tools =
42+
`List
43+
[ `Assoc
44+
[ ("name", `String "wellFormedness");
45+
( "description",
46+
`String
47+
"Given a C file (and optionally a list of function names), runs CN's \
48+
well-formedness check, which finds errors such as, ill-typing CN \
49+
definitions (predicates, specifications, lemmas) and ill-formed recursion \
50+
in datatypes. If given just a filename, all functions will be checked. \
51+
Otherwise, only the functions listed will be checked. NOTE: this tool \
52+
does not prove correctness, you need `verifier` for that." );
53+
( "inputSchema",
54+
`Assoc
55+
[ ("type", `String "object");
56+
( "properties",
57+
`Assoc
58+
[ ("filename", `Assoc [ ("type", `String "string") ]);
59+
( "functions",
60+
`Assoc
61+
[ ("type", `String "array");
62+
("items", `Assoc [ ("type", `String "string") ])
63+
] )
64+
] );
65+
("required", `List [ `String "filename" ])
66+
] );
67+
( "annotations",
68+
`Assoc
69+
[ ("title", `String "CN well-formedness check");
70+
("destructiveHint", `Bool false);
71+
("idempotentHint", `Bool true)
72+
] )
73+
];
74+
`Assoc
75+
[ ("name", `String "verifier");
76+
( "description",
77+
`String
78+
"Given a C file (and optionally a list of function names), use the CN \
79+
verifier to try and prove correctness. If given just a filename, it will \
80+
try to prove correctness of all functions not marked with `trusted`. \
81+
Otherwise, only the functions listed will be checked." );
82+
( "inputSchema",
83+
`Assoc
84+
[ ("type", `String "object");
85+
( "properties",
86+
`Assoc
87+
[ ("filename", `Assoc [ ("type", `String "string") ]);
88+
( "functions",
89+
`Assoc
90+
[ ("type", `String "array");
91+
("items", `Assoc [ ("type", `String "string") ])
92+
] )
93+
] );
94+
("required", `List [ `String "filename" ])
95+
] );
96+
( "annotations",
97+
`Assoc
98+
[ ("title", `String "CN verification");
99+
("destructiveHint", `Bool false);
100+
("idempotentHint", `Bool true)
101+
] )
102+
];
103+
`Assoc
104+
[ ("name", `String "instrumentAndRun");
105+
( "description",
106+
`String
107+
"Given a C file (and optionally a list of function names), instrument the \
108+
file to check CN specifications and run it. If given just a filename, all \
109+
functions with specs will be have their specs checked at runtime. \
110+
Otherwise, only the functions listed will have their specs checked at \
111+
runtime. The file must have a `main` function for this to do anything." );
112+
( "inputSchema",
113+
`Assoc
114+
[ ("type", `String "object");
115+
( "properties",
116+
`Assoc
117+
[ ("filename", `Assoc [ ("type", `String "string") ]);
118+
( "functions",
119+
`Assoc
120+
[ ("type", `String "array");
121+
("items", `Assoc [ ("type", `String "string") ])
122+
] )
123+
] );
124+
("required", `List [ `String "filename" ])
125+
] );
126+
( "annotations",
127+
`Assoc
128+
[ ("title", `String "Run with CN instrumentation");
129+
("destructiveHint", `Bool false);
130+
("idempotentHint", `Bool false)
131+
] )
132+
];
133+
`Assoc
134+
[ ("name", `String "randomTesting");
135+
( "description",
136+
`String
137+
"Given a C file (and optionally a list of function names), use \
138+
specification-based random testing. If given just a filename, as many \
139+
functions as possible will be tested. Otherwise, only the functions \
140+
listed will be tested." );
141+
( "inputSchema",
142+
`Assoc
143+
[ ("type", `String "object");
144+
( "properties",
145+
`Assoc
146+
[ ("filename", `Assoc [ ("type", `String "string") ]);
147+
( "functions",
148+
`Assoc
149+
[ ("type", `String "array");
150+
("items", `Assoc [ ("type", `String "string") ])
151+
] )
152+
] );
153+
("required", `List [ `String "filename" ])
154+
] );
155+
( "annotations",
156+
`Assoc
157+
[ ("title", `String "CN random testing");
158+
("destructiveHint", `Bool false);
159+
("idempotentHint", `Bool false)
160+
] )
161+
]
162+
]
163+
164+
165+
(** Handle different MCP methods *)
166+
let handle_request (req : mcp_request) =
167+
let open YB.Util in
168+
match req.method_ with
169+
| "ping" -> Lwt.return (json_of_result req.id (`Assoc []))
170+
| "initialize" ->
171+
let result =
172+
`Assoc
173+
[ ("protocolVersion", `String "2025-03-26");
174+
("capabilities", `Assoc [ ("tools", `Assoc [ ("listChanged", `Bool false) ]) ]);
175+
( "serverInfo",
176+
`Assoc
177+
[ ("name", `String "CN MCP Server");
178+
("version", `String Common.version_str)
179+
] )
180+
]
181+
in
182+
Lwt.return (json_of_result req.id result)
183+
| "tools/list" ->
184+
let result = `Assoc [ ("tools", available_tools) ] in
185+
Lwt.return (json_of_result req.id result)
186+
| "tools/call" ->
187+
let toolName = req.params |> Option.get |> member "name" |> to_string in
188+
let args = req.params |> Option.get |> member "arguments" in
189+
(match toolName with
190+
| "wellFormedness" ->
191+
let cmd =
192+
"cn wf "
193+
^ (args |> member "filename" |> to_string)
194+
^ (match args |> member "functions" with
195+
| `List functions when not (List.is_empty functions) ->
196+
"--only=" ^ String.concat "," (List.map to_string functions)
197+
| _ -> "")
198+
^ " 2>&1"
199+
in
200+
let inp = Unix.open_process_in cmd in
201+
let result = In_channel.input_all inp in
202+
In_channel.close inp;
203+
let resp =
204+
`Assoc
205+
[ ( "content",
206+
`List [ `Assoc [ ("type", `String "text"); ("text", `String result) ] ] );
207+
("isError", `Bool false)
208+
]
209+
in
210+
Lwt.return (json_of_result req.id resp)
211+
| "verifier" ->
212+
let cmd =
213+
"cn verify "
214+
^ (args |> member "filename" |> to_string)
215+
^ (match args |> member "functions" with
216+
| `List functions when not (List.is_empty functions) ->
217+
"--only=" ^ String.concat "," (List.map to_string functions)
218+
| _ -> "")
219+
^ " 2>&1"
220+
in
221+
let inp = Unix.open_process_in cmd in
222+
let result = In_channel.input_all inp in
223+
In_channel.close inp;
224+
let resp =
225+
`Assoc
226+
[ ( "content",
227+
`List [ `Assoc [ ("type", `String "text"); ("text", `String result) ] ] );
228+
("isError", `Bool false)
229+
]
230+
in
231+
Lwt.return (json_of_result req.id resp)
232+
| "instrumentAndRun" ->
233+
let cmd =
234+
"cn instrument --run --tmp "
235+
^ (args |> member "filename" |> to_string)
236+
^ (match args |> member "functions" with
237+
| `List functions when not (List.is_empty functions) ->
238+
"--only=" ^ String.concat "," (List.map to_string functions)
239+
| _ -> "")
240+
^ " 2>&1"
241+
in
242+
let inp = Unix.open_process_in cmd in
243+
let result = In_channel.input_all inp in
244+
In_channel.close inp;
245+
let resp =
246+
`Assoc
247+
[ ( "content",
248+
`List [ `Assoc [ ("type", `String "text"); ("text", `String result) ] ] );
249+
("isError", `Bool false)
250+
]
251+
in
252+
Lwt.return (json_of_result req.id resp)
253+
| "randomTesting" ->
254+
let cmd =
255+
"cn test --progress-level=function "
256+
^ (args |> member "filename" |> to_string)
257+
^ (match args |> member "functions" with
258+
| `List functions when not (List.is_empty functions) ->
259+
"--only=" ^ String.concat "," (List.map to_string functions)
260+
| _ -> "")
261+
^ " 2>&1"
262+
in
263+
let inp = Unix.open_process_in cmd in
264+
let result = In_channel.input_all inp in
265+
In_channel.close inp;
266+
let resp =
267+
`Assoc
268+
[ ( "content",
269+
`List [ `Assoc [ ("type", `String "text"); ("text", `String result) ] ] );
270+
("isError", `Bool false)
271+
]
272+
in
273+
Lwt.return (json_of_result req.id resp)
274+
| toolName ->
275+
output_string
276+
stderr
277+
("Invalid request: " ^ YB.pretty_to_string (Option.get req.params));
278+
flush stderr;
279+
let err = json_of_error req.id (-32602) ("Unknown tool: " ^ toolName) in
280+
Lwt.return err)
281+
| _ ->
282+
let err = json_of_error req.id (-32601) "Method not found" in
283+
Lwt.return err
284+
285+
286+
(** Handle different MCP notifications *)
287+
let handle_notif (notif : mcp_notif) = match notif.method_ with _ -> ()
288+
289+
(** Start MCP server *)
290+
let mcp () =
291+
let rec main_loop () =
292+
let open Lwt.Infix in
293+
Lwt_io.read_line_opt Lwt_io.stdin
294+
>>= function
295+
| Some line ->
296+
(try
297+
let json = YB.from_string line in
298+
if YB.equal (YB.Util.member "id" json) `Null then (
299+
(* Is a notification *)
300+
handle_notif (parse_notif json);
301+
main_loop ())
302+
else (
303+
let req = parse_request json in
304+
handle_request req
305+
>>= fun resp_json ->
306+
let resp_str = YB.to_string resp_json in
307+
Lwt_io.write_line Lwt_io.stdout resp_str
308+
>>= fun () -> Lwt_io.flush Lwt_io.stdout >>= fun () -> main_loop ())
309+
with
310+
| Yojson.Json_error exn ->
311+
let err = json_of_error (-1) (-32700) ~data:exn "Parse error" in
312+
let err_str = YB.to_string err in
313+
Lwt_io.write_line Lwt_io.stdout err_str
314+
>>= fun () -> Lwt_io.flush Lwt_io.stdout >>= fun () -> main_loop ())
315+
| None -> Lwt.return_unit
316+
in
317+
Lwt_main.run (main_loop ())
318+
319+
320+
open Cmdliner
321+
322+
module Flags = struct end
323+
324+
let cmd =
325+
let open Term in
326+
let mcp_t = const mcp $ const () in
327+
let doc =
328+
"Starts a model context protocol (MCP) server exposing CN functionality. Offers \
329+
tools for testing and verifying C functions with CN specifications."
330+
in
331+
let info = Cmd.info "mcp" ~doc in
332+
Cmd.v info mcp_t

‎cn.opam

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ depends: [
2121
"cmdliner"
2222
"ocamlgraph"
2323
"zarith" {>= "1.13"}
24+
"lwt"
25+
"yojson"
2426
]
2527
pin-depends: [
2628
["cerberus-lib.dev" "git+https://github.com/rems-project/cerberus.git#5a3c0d7"]

0 commit comments

Comments
 (0)