Server mode

dune-project

@@ -38,6 +38,7 @@
     (odoc :with-doc)
     dune-site
     json-data-encoding
+    jsonrpc
     (sha (>= 1.12))
     (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS
     (conf-ruby :with-test)

goblint.opam

@@ -34,6 +34,7 @@ depends: [
   "odoc" {with-doc}
   "dune-site"
   "json-data-encoding"
+  "jsonrpc"
   "sha" {>= "1.12"}
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}

goblint.opam.locked

@@ -46,6 +46,7 @@ depends: [
   "fpath" {= "0.7.3" & with-doc}
   "goblint-cil" {= "1.8.2"}
   "json-data-encoding" {= "0.10"}
+  "jsonrpc" {= "1.9.1"}
   "logs" {= "0.7.0" & with-doc}
   "mlgmpidl" {= "1.2.13"}
   "num" {= "1.4"}

src/dune

@@ -8,7 +8,7 @@
   (public_name goblint.lib)
   (wrapped false)
   (modules :standard \ goblint mainarinc maindomaintest mainspec privPrecCompare apronPrecCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.

src/incremental/serialize.ml

@@ -17,6 +17,8 @@ let gob_results_dir () =
 let gob_results_tmp_dir () =
   Filename.concat (gob_directory ()) results_tmp_dir
 
+let server () = GobConfig.get_bool "server.enabled"
+
 let marshal obj fileName  =
   let chan = open_out_bin fileName in
   Marshal.output chan obj;
@@ -40,22 +42,39 @@ let type_to_file_name = function
   | VersionData -> version_map_filename
   | AnalysisData -> analysis_data_file_name
 
+(** Used by the server mode to avoid serializing the solver state to the filesystem *)
+let server_solver_data : Obj.t option ref = ref None
+let server_analysis_data : Obj.t option ref = ref None
+
 (** Loads data for incremental runs from the appropriate file *)
 let load_data (data_type: incremental_data_kind) =
-  let p = Filename.concat (gob_results_dir ()) (type_to_file_name data_type) in
-  unmarshal p
+  if server () then
+    match data_type with
+    | SolverData -> !server_solver_data |> Option.get |> Obj.obj
+    | AnalysisData -> !server_analysis_data |> Option.get |> Obj.obj
+    | _ -> failwith "Can only load solver and analysis data"
+  else
+    let p = Filename.concat (gob_results_dir ()) (type_to_file_name data_type) in
+    unmarshal p
 
 (** Stores data for future incremental runs at the appropriate file, given the data and what kind of data it is. *)
-let store_data (data: 'a) (data_type: incremental_data_kind) =
-  ignore @@ Goblintutil.create_dir (gob_directory ());
-  let d = gob_results_tmp_dir () in
-  ignore @@ Goblintutil.create_dir d;
-  let p = Filename.concat (d) (type_to_file_name data_type) in
-  marshal data p
+let store_data (data : 'a) (data_type : incremental_data_kind) =
+  if server () then
+    match data_type with
+    | SolverData -> server_solver_data := Some (Obj.repr data)
+    | AnalysisData -> server_analysis_data := Some (Obj.repr data)
+    | _ -> ()
+  else (
+    ignore @@ Goblintutil.create_dir (gob_directory ());
+    let d = gob_results_tmp_dir () in
+    ignore @@ Goblintutil.create_dir d;
+    let p = Filename.concat d (type_to_file_name data_type) in
+    marshal data p)
 
 (** Deletes previous analysis results and moves the freshly created results there.*)
 let move_tmp_results_to_results () =
-  if Sys.file_exists (gob_results_dir ()) then begin
-    Goblintutil.rm_rf (gob_results_dir ());
-  end;
-  Sys.rename (gob_results_tmp_dir ()) (gob_results_dir ())
+  if not (server ()) then (
+    if Sys.file_exists (gob_results_dir ()) then begin
+      Goblintutil.rm_rf (gob_results_dir ());
+    end;
+    Sys.rename (gob_results_tmp_dir ()) (gob_results_dir ()))

src/maingoblint.ml

@@ -497,19 +497,20 @@ let main () =
         preprocess_files () |> merge_preprocessed
       )
     in
-    let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
-    file|> do_analyze changeInfo;
-    do_stats ();
-    do_html_output ();
-    do_gobview ();
-    if !verified = Some false then exit 3;  (* verifier failed! *)
+    if get_bool "server.enabled" then Server.start file do_analyze else (
+      let changeInfo = if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then diff_and_rename file else Analyses.empty_increment_data file in
+      file|> do_analyze changeInfo;
+      do_stats ();
+      do_html_output ();
+      do_gobview ();
+      if !verified = Some false then exit 3)  (* verifier failed! *)
   with
-    | Exit ->
-      exit 1
-    | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *)
-      (* Printexc.print_backtrace BatInnerIO.stderr *)
-      eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
-      exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *)
-    | Timeout ->
-      eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!"));
-      exit 124
+  | Exit ->
+    exit 1
+  | Sys.Break -> (* raised on Ctrl-C if `Sys.catch_break true` *)
+    (* Printexc.print_backtrace BatInnerIO.stderr *)
+    eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted by SIGINT (Ctrl-C)!"));
+    exit 131 (* same exit code as without `Sys.catch_break true`, otherwise 0 *)
+  | Timeout ->
+    eprintf "%s\n" (MessageUtil.colorize ~fd:Unix.stderr ("{RED}Analysis was aborted because it reached the set timeout of " ^ get_string "dbg.timeout" ^ " or was signalled SIGPROF!"));
+    exit 124

src/util/gobConfig.ml

@@ -75,9 +75,12 @@ sig
   (** Write the current configuration to [filename] *)
   val write_file: string -> unit
 
-  (** Merge configurations form a file with current. *)
+  (** Merge configurations from a file with current. *)
   val merge_file : string -> unit
 
+  (** Merge configurations from a JSON object with current. *)
+  val merge : Yojson.Safe.t -> unit
+
   val json_conf: Yojson.Safe.t ref
 end
 
@@ -343,13 +346,16 @@ struct
       eprintf "Cannot set %s to '%s'.\n" st s;
       raise e
 
+  let merge json =
+    Validator.validate_exn json;
+    json_conf := GobYojson.merge !json_conf json;
+    ValidatorRequireAll.validate_exn !json_conf;
+    drop_memo ()
+
   (** Merge configurations form a file with current. *)
   let merge_file fn =
     let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in fn in
-    Validator.validate_exn v;
-    json_conf := GobYojson.merge !json_conf v;
-    ValidatorRequireAll.validate_exn !json_conf;
-    drop_memo ();
+    merge v;
     if tracing then trace "conf" "Merging with '%s', resulting\n%a.\n" fn GobYojson.pretty !json_conf
 end
 

src/util/options.schema.json

@@ -217,6 +217,33 @@
       "type": "boolean",
       "default": false
     },
+    "server": {
+      "title": "Server",
+      "description": "Server mode",
+      "type": "object",
+      "properties": {
+        "enabled": {
+          "title": "server.enabled",
+          "description": "Enable server mode",
+          "type": "boolean",
+          "default": false
+        },
+        "mode": {
+          "title": "server.mode",
+          "description": "Server transport mode",
+          "type": "string",
+          "enum": ["stdio", "unix"],
+          "default": "stdio"
+        },
+        "unix-socket": {
+          "title": "server.unix-socket",
+          "description": "The path to the UNIX socket",
+          "type": "string",
+          "default": "goblint.sock"
+        }
+      },
+      "additionalProperties": false
+    },
     "ana": {
       "title": "Analyses",
       "description": "Options for analyses",

src/util/server.ml

@@ -0,0 +1,184 @@
+open Batteries
+open Jsonrpc
+
+exception Failure of Response.Error.Code.t * string
+
+type t = {
+  file: Cil.file;
+  do_analyze: Analyses.increment_data -> Cil.file -> unit;
+  input: IO.input;
+  output: unit IO.output;
+}
+
+module type Request = sig
+  val name: string
+
+  type params
+  type response
+
+  val params_of_yojson: Yojson.Safe.t -> (params, string) result
+  val response_to_yojson: response -> Yojson.Safe.t
+
+  val process: params -> t -> response
+end
+
+module Registry = struct
+  type t = (string, (module Request)) Hashtbl.t
+  let make () : t = Hashtbl.create 32
+  let register (reg: t) (module R : Request) = Hashtbl.add reg R.name (module R)
+end
+
+let registry = Registry.make ()
+
+let handle_exn id exn =
+  Response.Error.(make Code.InternalError (Printexc.to_string exn) () |> Response.error id)
+
+module ParamParser (R : Request) = struct
+  let parse params =
+    let maybe_params =
+      params
+      |> Option.map_default Message.Structured.to_json `Null
+      |> R.params_of_yojson
+    in
+    match maybe_params with
+    | Ok params -> Ok params
+    | Error err ->
+      (* This is a hack to handle cases where R.params is a primitive type like int or string. *)
+      match params with
+      | Some `List [param] -> R.params_of_yojson param |> Result.map_error (fun _ -> err)
+      | _ -> Error err
+end
+
+let handle_request (serv: t) (message: Message.either) (id: Id.t) =
+  let req = Hashtbl.find_option registry message.method_ in
+  let response = match req with
+    | Some (module R) ->
+      let module Parser = ParamParser (R) in (
+        match Parser.parse message.params with
+        | Ok params -> (
+            try
+              R.process params serv
+              |> R.response_to_yojson
+              |> Response.ok id
+            with Failure (code, msg) -> Response.Error.(make code msg () |> Response.error id))
+        | Error s -> Response.Error.(make Code.InvalidParams s () |> Response.error id))
+    | _ -> Response.Error.(make Code.MethodNotFound message.method_ () |> Response.error id)
+  in
+  Response.yojson_of_t response |> Yojson.Safe.to_string |> IO.write_line serv.output;
+  IO.flush serv.output
+
+let serve serv =
+  serv.input
+  |> IO.to_input_channel
+  |> Yojson.Safe.linestream_from_channel
+  |> Stream.iter (fun line ->
+      match line with
+      | `Json json -> (
+          try
+            let message = Message.either_of_yojson json in
+            match message.id with
+            | Some id -> handle_request serv message id
+            | _ -> () (* We just ignore notifications for now. *)
+          with Json.Of_json (s, _) -> prerr_endline s)
+      | `Exn exn -> prerr_endline (Printexc.to_string exn))
+
+let make ?(input=stdin) ?(output=stdout) file do_analyze : t = { file; do_analyze; input; output }
+
+let bind () =
+  let mode = GobConfig.get_string "server.mode" in
+  if mode = "stdio" then None, None else (
+    let path = GobConfig.get_string "server.unix-socket" in
+    if Sys.file_exists path then
+      Sys.remove path;
+    let socket = Unix.socket PF_UNIX SOCK_STREAM 0 in
+    Unix.bind socket (ADDR_UNIX path);
+    Unix.listen socket 1;
+    let conn, _ = Unix.accept socket in
+    Unix.close socket;
+    Sys.remove path;
+    Some (Unix.input_of_descr conn), Some (Unix.output_of_descr conn))
+
+let start file do_analyze =
+  let input, output = bind () in
+  GobConfig.set_bool "incremental.save" true;
+  serve (make file do_analyze ?input ?output)
+
+let analyze ?(reset=false) ({ file; do_analyze; _ }: t)=
+  if reset then (
+    Serialize.server_solver_data := None;
+    Serialize.server_analysis_data := None;
+    Messages.Table.(MH.clear messages_table);
+    Messages.Table.messages_list := []);
+  let increment_data, fresh = match !Serialize.server_solver_data with
+    | Some solver_data ->
+      let changes = CompareCIL.compareCilFiles file file in
+      let old_data = Some { Analyses.cil_file = file; solver_data } in
+      { Analyses.changes; old_data; new_file = file }, false
+    | _ -> Analyses.empty_increment_data file, true
+  in
+  GobConfig.set_bool "incremental.load" (not fresh);
+  do_analyze increment_data file;
+  GobConfig.set_bool "incremental.load" true
+
+(* TODO: Add command to abort the analysis in progress. *)
+let () =
+  let register = Registry.register registry in
+
+  register (module struct
+    let name = "analyze"
+    type params = { reset: bool [@default false] } [@@deriving of_yojson]
+    (* TODO: Return analysis results as JSON. Useful for GobPie. *)
+    type response = unit [@@deriving to_yojson]
+    (* TODO: Add option to re-parse the input files. *)
+    (* TODO: Add options to control the analysis precision/context for specific functions. *)
+    (* TODO: Add option to mark functions as modified. *)
+    let process { reset } serve = analyze serve ~reset
+  end);
+
+  register (module struct
+    let name = "config"
+    type params = string * Yojson.Safe.t [@@deriving of_yojson]
+    type response = unit [@@deriving to_yojson]
+    (* TODO: Make it possible to change the non-optional parameters. (i.e., the set of input files) *)
+    (* TODO: Check options for compatibility with the incremental analysis. *)
+    let process (conf, json) _ =
+      try
+        GobConfig.set_auto conf (Yojson.Safe.to_string json)
+      with exn -> raise (Failure (InvalidParams, Printexc.to_string exn))
+  end);
+
+  register (module struct
+    let name = "merge_config"
+    type params = Yojson.Safe.t [@@deriving of_yojson]
+    type response = unit [@@deriving to_yojson]
+    let process json _ =
+      try GobConfig.merge json with exn -> (* TODO: Be more specific in what we catch. *)
+        raise (Failure (InvalidParams, Printexc.to_string exn))
+  end);
+
+  register (module struct
+    let name = "messages"
+    type params = unit [@@deriving of_yojson]
+    type response = Messages.Message.t list [@@deriving to_yojson]
+    let process () _ = !Messages.Table.messages_list
+  end);
+
+  register (module struct
+    let name = "exp_eval"
+    type params = ExpressionEvaluation.query [@@deriving of_yojson]
+    type response =
+      ((string * CilType.Location.t * string * int) * bool option) list [@@deriving to_yojson]
+    let process query serv =
+      GobConfig.set_auto "trans.activated[+]" "'expeval'";
+      ExpressionEvaluation.gv_query := Some query;
+      analyze serv;
+      GobConfig.set_auto "trans.activated[-]" "'expeval'";
+      !ExpressionEvaluation.gv_results
+  end);
+
+  register (module struct
+    let name = "ping"
+    type params = unit [@@deriving of_yojson]
+    type response = [`Pong] [@@deriving to_yojson]
+    let process () _ = `Pong
+  end)