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

@@ -16,6 +16,8 @@ let gob_results_dir () =
 let gob_results_tmp_dir () =
   Filename.concat (gob_directory ()) results_tmp_dir
 
+let server () = GobConfig.get_bool "server"
+
 let marshal obj fileName  =
   let chan = open_out_bin fileName in
   Marshal.output chan obj;
@@ -38,22 +40,35 @@ let type_to_file_name = function
   | CilFile -> cil_file_name
   | VersionData -> version_map_filename
 
+let solver_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 -> !solver_data |> Option.get |> Obj.obj
+    | _ -> raise (Invalid_argument "Can only load solver 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 -> solver_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 () =
       print_endline command;
     );
     let file = 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" 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,12 @@
       "type": "boolean",
       "default": false
     },
+    "server": {
+      "title": "server",
+      "description": "Server mode",
+      "type": "boolean",
+      "default": false
+    },
     "ana": {
       "title": "Analyses",
       "description": "Options for analyses",

src/util/server.ml

@@ -0,0 +1,155 @@
+open Batteries
+open Jsonrpc
+
+type t = {
+  file: Cil.file;
+  do_analyze: Analyses.increment_data -> Cil.file -> unit;
+}
+
+module type Command = sig
+  val name: string
+
+  type args
+  type result
+
+  val args_of_yojson: Yojson.Safe.t -> args Ppx_deriving_yojson_runtime.error_or
+  val result_to_yojson: result -> Yojson.Safe.t
+
+  val process: args -> t -> result
+end
+
+module Registry = struct
+  type t = (string, (module Command)) Hashtbl.t
+  let make () : t = Hashtbl.create 32
+  let register (reg: t) (module R : Command) = 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 (C : Command) = struct
+  let parse params =
+    let args = 
+      params
+      |> Option.map_default Message.Structured.to_json `Null
+      |> C.args_of_yojson
+    in
+    match args with
+    | Ok args -> Ok args
+    | Error err ->
+      (* This is a hack to handle cases where C.args is primitive type like int or string. *)
+      match params with
+      | Some `List [param] -> (
+          match C.args_of_yojson param with
+          | Ok arg -> Ok arg
+          | _ -> Error err)
+      | _ -> Error err
+end
+
+let handle_request (serv: t) (message: Message.either) (id: Id.t) =
+  let cmd = Hashtbl.find_option registry message.method_ in
+  let response = match cmd with
+    | Some (module C) ->
+      let module Parser = ParamParser (C) in (
+        match Parser.parse message.params with
+        | Ok args -> (
+            try
+              C.process args serv
+              |> C.result_to_yojson
+              |> Response.ok id
+            with exn -> handle_exn id exn)
+        | 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 |> print_endline
+
+let serve serv =
+  let chan = IO.to_input_channel stdin in
+  let stream = Yojson.Safe.linestream_from_channel chan in
+  while not (Stream.is_empty stream) do
+    let line = Stream.next stream in
+    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 exn -> prerr_endline (Printexc.to_string exn))
+    | `Exn exn -> prerr_endline (Printexc.to_string exn)
+  done
+
+let make file do_analyze : t = { file; do_analyze }
+
+let start file do_analyze =
+  GobConfig.set_bool "incremental.save" true;
+  serve (make file do_analyze)
+
+let analyze ?(reset=false) { file; do_analyze } =
+  if reset then (
+    Serialize.solver_data := None;
+    Messages.Table.(MH.clear messages_table);
+    Messages.Table.messages_list := []);
+  let increment_data, fresh = match !Serialize.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
+
+let () =
+  let register = Registry.register registry in
+
+  register (module struct
+    let name = "analyze"
+    type args = { reset: bool [@default false] } [@@deriving of_yojson]
+    type result = unit [@@deriving to_yojson]
+    let process { reset } serve = analyze serve ~reset
+  end);
+
+  register (module struct
+    let name = "config"
+    type args = string * Yojson.Safe.t [@@deriving of_yojson]
+    type result = unit [@@deriving to_yojson]
+    let process (conf, json) _ = GobConfig.set_auto conf (Yojson.Safe.to_string json)
+  end);
+
+  register (module struct
+    let name = "merge_config"
+    type args = Yojson.Safe.t [@@deriving of_yojson]
+    type result = unit [@@deriving to_yojson]
+    let process json _ = GobConfig.merge json
+  end);
+
+  register (module struct
+    let name = "messages"
+    type args = unit [@@deriving of_yojson]
+    type result = Messages.Message.t list [@@deriving to_yojson]
+    let process () _ = !Messages.Table.messages_list
+  end);
+
+  register (module struct
+    let name = "exp_eval"
+    type args = ExpressionEvaluation.query [@@deriving of_yojson]
+    type result =
+      ((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 args = unit [@@deriving of_yojson]
+    type result = [`Pong] [@@deriving to_yojson]
+    let process () _ = `Pong
+  end)