Include Goblint-Http Server in GobView repository

README.md

@@ -5,6 +5,10 @@ A Web Frontend for Goblint.
 It allows inspecting the analyzed files and results of an analysis run with Goblint.
 It is based on [jsoo-react](https://github.com/jchavarri/jsoo-react) and was originally developed by Alex Micheli for his Bachelor's thesis at TUM i2, significantly extended by Kerem Cakirer, and is now maintained by the Goblint team.
 
+## Goblint Http-Server
+
+Http-Server for the communication between GobView and Goblint in server mode. It also serves the files for the web page.
+
 ## Installing
 
 Follow the instructions in the [Read the Docs](https://goblint.readthedocs.io/en/latest/user-guide/inspecting/).

dune

@@ -1,7 +1,7 @@
 (rule
  (alias gobview)
  (targets dist)
- (deps src/App.bc.js node_modules webpack.config.js)
+ (deps src/App.bc.js goblint-http-server/goblint_http.exe node_modules webpack.config.js)
  (action
   (run npx webpack build)))
 

dune-project

@@ -24,8 +24,18 @@
  (synopsis "Web frontend for Goblint")
  (depends
   dune
-  (ocaml
-   (>= 4.10.0))
+  (ocaml (>= 4.10.0))
+  batteries
+  cohttp-lwt
+  cohttp-lwt-unix
+  cohttp-server-lwt-unix
+  fileutils
+  jsonrpc
+  lwt
+  lwt_ppx
+  yojson
+  ppx_yojson_conv ; TODO: switch to ppx_deriving_yojson like Goblint itself
+  conduit-lwt-unix
   jsoo-react
   (goblint-cil (>= 2.0.0))
   ctypes_stubs_js

goblint-http-server/LICENSE

@@ -0,0 +1,13 @@
+Copyright 2022 Kerem Çakırer
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH
+REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY
+AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT,
+INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM
+LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR
+OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR
+PERFORMANCE OF THIS SOFTWARE.

goblint-http-server/api.ml

@@ -0,0 +1,47 @@
+open Batteries
+open State
+
+module type Request = sig
+  val name: string
+
+  type body
+  type response
+
+  val body_of_yojson: Yojson.Safe.t -> body
+  val yojson_of_response: response -> Yojson.Safe.t
+
+  val process: State.t -> body -> response Lwt.t
+end
+
+let registry = Hashtbl.create 16
+
+let register (module R : Request) = Hashtbl.add registry R.name (module R : Request)
+
+module Ping = struct
+  let name = "ping"
+  type body = unit [@@deriving yojson]
+  type response = unit [@@deriving yojson]
+  let process state () = Goblint.ping state.goblint
+end
+
+module Config = struct
+  let name = "config"
+  type body = string * Json.t [@@deriving yojson]
+  type response = unit [@@deriving yojson]
+  let process state (conf, json) = Goblint.config state.goblint conf json
+end
+
+module Analyze = struct
+  let name = "analyze"
+  type body = [`All | `Functions of string list] option [@@deriving yojson]
+  type response = unit [@@deriving yojson]
+  let process state reanalyze =
+    let%lwt save_run = Goblint.analyze state.goblint ?reanalyze in
+    state.save_run <- Some save_run;
+    Lwt.return_unit
+end
+
+let () =
+  register (module Ping);
+  register (module Config);
+  register (module Analyze)

goblint-http-server/dune

@@ -0,0 +1,16 @@
+(executable
+ (name goblint_http)
+ (public_name goblint-http)
+ (libraries
+  batteries
+  cohttp
+  cohttp-lwt
+  cohttp-lwt-unix
+  cohttp-server-lwt-unix
+  conduit-lwt-unix
+  jsonrpc
+  lwt.unix
+  yojson
+  uri)
+ (preprocess
+  (pps lwt_ppx ppx_yojson_conv)))

goblint-http-server/goblint.ml

@@ -0,0 +1,103 @@
+open Batteries
+open Lwt.Infix
+
+type t = {
+  input: Lwt_io.input_channel;
+  output: Lwt_io.output_channel;
+  mutex: Lwt_mutex.t;
+  mutable counter: int;
+}
+
+let spawn path args =
+  let base_args = [| path; "--enable"; "server.enabled"; "--set"; "server.mode"; "unix" |] in
+  let cmd = args |> Array.of_list |> Array.append base_args in
+  let _proc = Lwt_process.open_process_none (path, cmd) in
+  let sock = Lwt_unix.socket PF_UNIX SOCK_STREAM 0 in
+  (* Wait a bit for the server to be initialized. *)
+  let%lwt () = Lwt_unix.sleep 0.5 in
+  let%lwt () = Lwt_unix.connect sock (ADDR_UNIX "goblint.sock") in
+  let input = Lwt_io.of_fd ~mode:Lwt_io.Input sock in
+  let output = Lwt_io.of_fd ~mode:Lwt_io.Output sock in
+  Lwt.return { input; output; mutex = Lwt_mutex.create (); counter = 0 }
+
+let with_lock goblint = Lwt_mutex.with_lock goblint.mutex
+
+let assert_ok (resp: Jsonrpc.Response.t) s = match resp.result with
+  | Ok _ -> ()
+  | Error e -> failwith (Format.sprintf "%s (%s)" s e.message)
+
+let send goblint name params =
+  let id = `Int goblint.counter in
+  goblint.counter <- goblint.counter + 1;
+  let req =
+    Jsonrpc.Request.create ?params ~id ~method_:name ()
+    |> Jsonrpc.Request.yojson_of_t
+    |> Yojson.Safe.to_string in
+  Printf.printf "send jsonrpc message:\n%s\n" req;
+  let%lwt () = Lwt_io.fprintl goblint.output req in
+  let%lwt resp =
+    Lwt_io.read_line goblint.input
+    >|= Yojson.Safe.from_string
+    >|= Jsonrpc.Response.t_of_yojson in
+  if resp.id <> id then
+    failwith "Response ID doesn't match request ID";
+  Lwt.return resp
+
+let ping goblint =
+  let ping () =
+    let%lwt resp = send goblint "ping" None in
+    assert_ok resp "Ping failed";
+    Lwt.return_unit
+  in with_lock goblint ping
+
+let config_raw goblint name value =
+  let params = `List [`String name; value] in
+  let%lwt resp = send goblint "config" (Some params) in
+  match resp.result with
+  | Ok _ -> Lwt.return_unit
+  | Error err -> invalid_arg err.message
+
+let option_whitelist = [] |> Set.of_list
+
+let config goblint name value =
+  if not (Set.mem name option_whitelist) then
+    invalid_arg (Printf.sprintf "Option '%s' is not in the whitelist" name);
+  with_lock goblint (fun () -> config_raw goblint name value)
+
+let temp_dir () = Utils.temp_dir "goblint-http-server." ""
+
+let analyze ?reanalyze ?save_dir ?(gobview = false) goblint =
+  let set_force_reanalyze () = match reanalyze with
+    | Some `Functions xs ->
+      config_raw goblint "incremental.force-reanalyze.funs" (`List (List.map (fun s -> `String s) xs))
+    | _ -> Lwt.return_unit
+  in
+  let reset_force_reanalyze () = match reanalyze with
+    | Some `Functions _ ->
+      config_raw goblint "incremental.force-reanalyze.funs" (`List [])
+    | _ -> Lwt.return_unit
+  in
+  let set_gobview () = if gobview then config_raw goblint "gobview" (`Bool true) else Lwt.return_unit in
+  let reset_gobview () = if gobview then config_raw goblint "gobview" (`Bool false) else Lwt.return_unit in
+  let analyze () =
+    let reset = match reanalyze with
+      | Some `All -> true
+      | _ -> false
+    in
+    let params = `Assoc [("reset", `Bool reset)] in
+    Lwt.finalize
+      (fun () ->
+          let save_run = match save_dir with
+          | None -> temp_dir ()
+          | Some d -> d in
+          let%lwt () = config_raw goblint "save_run" (`String save_run) in
+          let%lwt () = set_force_reanalyze () in
+          let%lwt () = set_gobview () in
+          let%lwt resp = send goblint "analyze" (Some params) in
+          assert_ok resp "Analysis failed";
+          Lwt.return save_run)
+      (fun () ->
+          let%lwt () = reset_force_reanalyze () in
+          let%lwt () = reset_gobview () in
+          Lwt.return_unit)
+  in with_lock goblint analyze

goblint-http-server/goblint_http.ml

@@ -0,0 +1,160 @@
+open Batteries
+open Cohttp_lwt
+open Cohttp_lwt_unix
+open Lwt.Infix
+
+module Yojson_conv = Ppx_yojson_conv_lib.Yojson_conv
+
+let docroot = ref "run"
+let index = ref "index.html"
+let addr = ref "127.0.0.1"
+let port = ref 8080
+let goblint = ref "goblint"
+let rest = ref []
+
+let specs =
+  [
+    ("-docroot", Arg.Set_string docroot, "Serving directory");
+    ("-index", Arg.Set_string index, "Name of index file in directory");
+    ("-addr", Arg.Set_string addr, "Listen address");
+    ("-port", Arg.Set_int port, "Listen port");
+    ("-with-goblint", Arg.Set_string goblint, "Path to the Goblint executable");
+    ("-goblint", Arg.Rest_all (fun args -> rest := args), "Pass the rest of the arguments to Goblint");
+  ]
+
+let paths = ref []
+
+let process state name body =
+  match Hashtbl.find_option Api.registry name with
+  | None -> Server.respond_not_found ()
+  | Some (module R) ->
+    let%lwt body = Body.to_string body in
+    let body = if body = "" then "null" else body in
+    match Yojson.Safe.from_string body with
+    | exception Yojson.Json_error err -> Server.respond_error ~status:`Bad_request ~body:err ()
+    | json ->
+      match R.body_of_yojson json with
+      | exception Yojson_conv.Of_yojson_error (exn, _) ->
+        Server.respond_error ~status:`Bad_request ~body:(Printexc.to_string exn) ()
+      | body ->
+        Lwt.catch
+          (fun () ->
+             R.process state body
+             >|= R.yojson_of_response
+             >|= Yojson.Safe.to_string
+             >>= fun body -> Server.respond_string ~status:`OK ~body ())
+          (fun exn -> Server.respond_error ~status:`Bad_request ~body:(Printexc.to_string exn) ())
+
+(* The serving of files is implemented similar as in the binary https://github.com/mirage/ocaml-cohttp/blob/master/cohttp-lwt-unix/bin/cohttp_server_lwt.ml *)
+let serve_file ~docroot ~uri =
+  let fname = Cohttp.Path.resolve_local_file ~docroot ~uri in
+  Server.respond_file ~fname ()
+
+let sort lst =
+  let compare_kind = function
+    | Some Unix.S_DIR, Some Unix.S_DIR -> 0
+    | Some Unix.S_DIR, _ -> -1
+    | _, Some Unix.S_DIR -> 1
+    | Some Unix.S_REG, Some Unix.S_REG -> 0
+    | Some Unix.S_REG, _ -> 1
+    | _, Some Unix.S_REG -> -1
+    | _, _ -> 0 in
+  List.sort
+    (fun (ka, a) (kb, b) ->
+      let c = compare_kind (ka, kb) in
+      if c <> 0 then c
+      else String.compare (String.lowercase_ascii a) (String.lowercase_ascii b))
+    lst
+
+let html_of_listing uri path listing =
+  let li l =
+    Printf.sprintf "<li><a href=\"%s\">%s</a></li>" (Uri.to_string l) in
+  let html =
+    List.map
+      (fun (kind, f) ->
+        let encoded_f = Uri.pct_encode f in
+        match kind with
+        | Some Unix.S_DIR ->
+            let link = Uri.with_path uri (Filename.concat path (Filename.concat encoded_f "")) in
+            li link (Printf.sprintf "<i>%s/</i>" f)
+        | Some Unix.S_REG ->
+            let link = Uri.with_path uri (Filename.concat path encoded_f) in
+            li link f
+        | Some _ ->
+            Printf.sprintf "<li><s>%s</s></li>" f
+        | None -> Printf.sprintf "<li>Error with file: %s</li>" f)
+      listing
+  in
+  let contents = String.concat "\n" html in
+  Printf.sprintf
+    "<html><body><h2>Directory Listing for <em>%s</em></h2><ul>%s</ul><hr \
+      /></body></html>"
+    (Uri.pct_decode path) contents
+
+let serve uri path =
+  let file_name = Cohttp.Path.resolve_local_file ~docroot:!docroot ~uri in
+  Lwt.catch
+    (fun () ->
+      Lwt_unix.lstat file_name >>= fun stat -> (* for symbolic links lstat returns S_LNK, which will result in a
+        forbidden error in this implementation. Use stat instead if symbolic links to folders or files should be handled
+        just like folders or files respectively *)
+      match stat.Unix.st_kind with
+      | Unix.S_DIR -> (
+          let path_len = String.length path in
+          if path_len <> 0 && path.[path_len - 1] <> '/' then (
+            Server.respond_redirect ~uri:(Uri.with_path uri (path ^ "/")) ())
+          else (
+            match Sys.file_exists (Filename.concat file_name !index) with
+            | true -> (
+                let uri = Uri.with_path uri (Filename.concat path !index) in
+                serve_file ~docroot:!docroot ~uri)
+            | false ->
+                let%lwt files = Lwt_stream.to_list
+                  (Lwt_stream.filter (fun s -> s <> "." && s <> "..") (Lwt_unix.files_of_directory file_name)) in
+                let%lwt listing = Lwt_list.map_s (fun f ->
+                        let file_name = Filename.concat file_name f in
+                        Lwt.try_bind
+                          (fun () -> Lwt_unix.LargeFile.stat file_name)
+                          (fun stat ->
+                            Lwt.return
+                              ( Some
+                                  stat.Unix.LargeFile.st_kind,
+                                f ))
+                          (fun _exn -> Lwt.return (None, f))) files in
+                let body = html_of_listing uri path (sort listing) in
+                Server.respond_string ~status:`OK ~body ()))
+      | Unix.S_REG -> serve_file ~docroot:!docroot ~uri
+      | _ -> (
+          let body = Printf.sprintf "<html><body><h2>Forbidden</h2><p><b>%s</b> is not a normal file or \
+          directory</p><hr/></body></html>" path in
+          Server.respond_string ~status:`OK ~body ()))
+    (function
+      | Unix.Unix_error (Unix.ENOENT, "stat", p) as e ->
+          if p = file_name then (
+            Server.respond_not_found ())
+          else Lwt.fail e
+      | e -> Lwt.fail e)
+
+let callback state _ req body =
+  let uri = Request.uri req in
+  let path = Uri.path uri in
+  let parts = String.split_on_char '/' path |> List.filter (not % String.is_empty) in
+  let meth = Request.meth req in
+  match meth, parts with
+  | `POST, ["api"; name] -> process state name body
+  | `GET, _ -> serve uri path
+  | _ -> Server.respond_not_found ()
+
+let main () =
+  let%lwt state = Goblint.spawn !goblint (!rest @ !paths) >|= State.make in
+  (* run Goblint once with option gobview enabled to copy the index.html and main.js files into the served directory *)
+  let%lwt _ = Goblint.analyze ~save_dir:!docroot ~gobview:true state.goblint in
+  let callback = callback state in
+  let server = Server.make ~callback () in
+  Server.create ~mode:(`TCP (`Port !port)) server
+
+let () =
+  let program = Sys.argv.(0) in
+  let usage = Printf.sprintf "%s [-docroot DOCROOT] [-index INDEX] [-addr ADDR] [-port PORT] ... path [path ...]" program in
+  Arg.parse specs (fun s -> paths := s :: !paths) usage;
+  Lwt_main.run (main ())

goblint-http-server/json.ml

@@ -0,0 +1,4 @@
+type t = Yojson.Safe.t
+
+let t_of_yojson x = x
+let yojson_of_t x = x

goblint-http-server/state.ml

@@ -0,0 +1,8 @@
+type t = {
+  goblint: Goblint.t;
+  (* Descriptor for the Goblint server instance *)
+  mutable save_run: string option;
+  (* The directory from which we serve the marshalled analysis state *)
+}
+
+let make (goblint: Goblint.t) = { goblint; save_run = None }