debugger: generate report json files during verification

cn-client/package.json

@@ -54,6 +54,16 @@
                     "default": null,
                     "description": "Location of the CN-DAP executable"
                 },
+                "CN.dumpStateTraces": {
+                    "type": "boolean",
+                    "default": false,
+                    "description": "When running CN verify, dump state traces to file (required for debugging)"
+                },
+                "CN.reportDir": {
+                    "type": "string",
+                    "default": null,
+                    "description": "Directory to store CN reports in (if unspecified, defaults to source directory)."
+                },                
                 "CN.showGillianDebugLenses": {
                     "type": "boolean",
                     "default": false,

cn-dap/debugger/lib/adapter.ml

@@ -41,7 +41,7 @@ let handle_launch (rpc : Rpc.t) : Debugger.t Lwt.t =
       | None -> Lwt.fail_with "no procedure name!"
       | Some procedure_name ->
         (* does debugger initialization need to be in Lwt? *)
-        (match Debugger.make launch_args.program procedure_name with
+        (match Debugger.make launch_args.report_dir launch_args.program procedure_name with
          | Error s -> Lwt.fail_with s
          | Ok debugger ->
            Lwt.wakeup_later resolver debugger;

cn-dap/debugger/lib/commands.ml

@@ -45,6 +45,7 @@ module Launch = struct
       { program : string
       ; stop_on_entry : bool [@default false] [@key "stopOnEntry"]
       ; procedure_name : string option [@default None] [@key "procedureName"]
+      ; report_dir: string option [@default None] [@key "reportDir"]
       }
     [@@deriving yojson { strict = false }]
   end

cn-dap/debugger/lib/debugger.ml

@@ -16,15 +16,15 @@ let report_from_file (file : string) : (Cn.Report.report, string) Result.t =
   Cn.Report.report_of_yojson js
 ;;
 
-let make (source_file : string) (procedure_name : string) : (t, string) Result.t =
+let make (report_dir: string option) (source_file : string) (procedure_name : string) : (t, string) Result.t =
   let ( let* ) x f = Result.bind x ~f in
   (* TODO: this improperly relies on the fact that
      `Cn.TypeErrors.mk_report_file_name` happens to only care about the filename
      in its error location parameter *)
   let source_loc =
     Cerb_location.point { Lexing.dummy_pos with pos_fname = source_file }
   in
-  let source_dir = Stdlib.Filename.dirname source_file in
+  let source_dir = Option.value report_dir ~default:(Stdlib.Filename.dirname source_file) in
   let report_file =
     Cn.TypeErrors.mk_report_file_name ~fn_name:procedure_name source_dir source_loc
   in

cn-lsp/lib/lenses.ml

@@ -3,7 +3,10 @@ module CodeLens = Lsp.Types.CodeLens
 module CodeLensOptions = Lsp.Types.CodeLensOptions
 module Command = Lsp.Types.Command
 
-let gillian_lenses_for (uri : Uri.t) : CodeLens.t list =
+let gillian_lenses_for ?(report_dir : string option) (uri : Uri.t) : CodeLens.t list =
+  let report_dir =
+    Option.value report_dir ~default:(Uri.to_path uri |> Stdlib.Filename.dirname)
+  in
   match Parse.parse_document_file uri with
   | Error e ->
     Log.e (Printf.sprintf "Unable to parse file %s: %s" (Uri.to_path uri) e);
@@ -12,13 +15,20 @@ let gillian_lenses_for (uri : Uri.t) : CodeLens.t list =
     let fns = Parse.function_declarations decls in
     let lens fn =
       let procedure_name = Parse.function_name fn in
+      let loc =
+        Cerb_location.point Lexing.{ dummy_pos with pos_fname = Uri.to_path uri }
+      in
+      let state_trace_file =
+        Cn.TypeErrors.mk_report_file_name ~fn_name:procedure_name report_dir loc
+      in
       (* Schema derived from Gillian's `debug-ui/src/activateCodeLens.ts` *)
       let argument =
         `Assoc
           [ "type", `String "CN"
           ; "request", `String "launch"
           ; "program", `String (Uri.to_path uri)
           ; "procedureName", `String procedure_name
+          ; "reportDir", `String report_dir
           ]
       in
       let command =
@@ -35,6 +45,12 @@ let gillian_lenses_for (uri : Uri.t) : CodeLens.t list =
              "No location available for Gillian lens for function `%s`"
              procedure_name);
         None
+      | Some _ when not (Stdlib.Sys.file_exists state_trace_file) ->
+        Log.d
+          (Printf.sprintf
+             "No state trace available for Gillian lens for function `%s`"
+             procedure_name);
+        None
       | Some range -> Some (CodeLens.create ~command ~range ())
     in
     List.filter_map fns ~f:lens

cn-lsp/lib/lspCn.ml

@@ -204,7 +204,24 @@ let lift_cn (x : 'a CnM.m) : ('a, error) Result.t =
 
 let setup () : cerb_env m = lift_cerb (Cerb.setup ())
 
-let run_cn (cerb_env : cerb_env) (uri : LspDocumentUri.t) : error list m =
+let dump_state_traces_json report_dir errors =
+  List.iter errors ~f:(fun (fn, (e : CnM.error)) ->
+    let report = Cn.TypeErrors.pp_message e.msg in
+    match report.state with
+    | None -> ()
+    | Some state ->
+      let report_file = Cn.TypeErrors.mk_report_file_name ~fn_name:fn report_dir e.loc in
+      let report_js = Cn.Report.report_to_yojson state in
+      Yojson.Safe.to_file report_file report_js)
+;;
+
+let run_cn
+  ?(dump_state_traces = false)
+  ?(report_dir : string option)
+  (cerb_env : cerb_env)
+  (uri : LspDocumentUri.t)
+  : error list m
+  =
   (* CLI flag? *)
   let inherit_loc : bool = true in
   let path = LspDocumentUri.to_path uri in
@@ -225,5 +242,9 @@ let run_cn (cerb_env : cerb_env) (uri : LspDocumentUri.t) : error list m =
              in
              Cn.Check.check_c_functions_all wellformedness_result)))
   in
-  return (List.map errors ~f:(fun (_fn, e) -> CnError e))
+  if dump_state_traces
+  then (
+    let outDir = Option.value report_dir ~default:(Stdlib.Filename.dirname path) in
+    dump_state_traces_json outDir errors);
+  return (List.map errors ~f:(fun (_fn, (e : CnM.error)) -> CnError e))
 ;;

cn-lsp/lib/lspCn.mli

@@ -39,5 +39,11 @@ val setup : unit -> cerb_env m
 
 (** Run CN on the given document to potentially produce errors. Use [run] to
     interpret the result, and [error_to_string] and [error_to_diagnostic] to
-    process any errors. *)
-val run_cn : cerb_env -> Lsp.Types.DocumentUri.t -> error list m
+    process any errors. The flags [dump_state_traces] and [report_dir]
+    dictate whether this command should dump the state traces to file. *)
+val run_cn
+  :  ?dump_state_traces:bool
+  -> ?report_dir:string
+  -> cerb_env
+  -> Lsp.Types.DocumentUri.t
+  -> error list m

cn-lsp/lib/server.ml

@@ -41,13 +41,15 @@ module Config = struct
   type t =
     { run_CN_on_save : bool
     ; show_Gillian_debug_lenses : bool
+    ; dump_state_traces : bool
+    ; report_dir: string option
     }
 
   (** The name of the configuration "section" the client uses to identify
       CN-specific settings *)
   let section : string = "CN"
 
-  let default : t = { run_CN_on_save = false; show_Gillian_debug_lenses = false }
+  let default : t = { run_CN_on_save = false; show_Gillian_debug_lenses = false; dump_state_traces = false; report_dir = None }
 
   let t_of_yojson (json : Json.t) : t option =
     let open Json.Util in
@@ -56,7 +58,11 @@ module Config = struct
       let show_Gillian_debug_lenses =
         json |> member "showGillianDebugLenses" |> to_bool
       in
-      Some { run_CN_on_save; show_Gillian_debug_lenses }
+      let dump_state_traces = json |> member "dumpStateTraces" |> to_bool in
+      let report_dir =
+        json |> member "reportDir" |> to_string_option
+      in
+      Some { run_CN_on_save; show_Gillian_debug_lenses; dump_state_traces; report_dir }
     with
     | _ -> None
   ;;
@@ -150,7 +156,7 @@ class lsp_server (env : LspCn.cerb_env) =
       (_ : Rpc.doc_state)
       : CodeLens.t list IO.t =
       if server_config.show_Gillian_debug_lenses
-      then IO.return (Lenses.gillian_lenses_for uri)
+      then IO.return (Lenses.gillian_lenses_for ?report_dir:server_config.report_dir uri)
       else IO.return []
 
     method on_unknown_request
@@ -259,7 +265,9 @@ class lsp_server (env : LspCn.cerb_env) =
 
     method run_cn (notify_back : Rpc.notify_back) (uri : DocumentUri.t) : unit IO.t =
       let open IO in
-      match LspCn.(run (run_cn env uri)) with
+      let { dump_state_traces; report_dir; _ } : Config.t = server_config in
+      Log.d (sprintf "Running CN on %s" (DocumentUri.to_string uri));
+      match LspCn.(run (run_cn ~dump_state_traces ?report_dir env uri)) with
       | Ok [] -> cinfo notify_back "No issues found"
       | Ok errs ->
         let diagnostics = Hashtbl.to_alist (LspCn.errors_to_diagnostics errs) in