diff --git a/README.md b/README.md index 24aa69c..8bc842a 100755 --- a/README.md +++ b/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/). diff --git a/dune b/dune index f4f59bd..3cf0148 100644 --- a/dune +++ b/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))) diff --git a/dune-project b/dune-project index ddd94d9..7c1c263 100644 --- a/dune-project +++ b/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 diff --git a/goblint-http-server/LICENSE b/goblint-http-server/LICENSE new file mode 100644 index 0000000..13b886a --- /dev/null +++ b/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. diff --git a/goblint-http-server/api.ml b/goblint-http-server/api.ml new file mode 100644 index 0000000..2b96c16 --- /dev/null +++ b/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) diff --git a/goblint-http-server/dune b/goblint-http-server/dune new file mode 100644 index 0000000..a56d548 --- /dev/null +++ b/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))) diff --git a/goblint-http-server/goblint.ml b/goblint-http-server/goblint.ml new file mode 100644 index 0000000..4cc867b --- /dev/null +++ b/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 diff --git a/goblint-http-server/goblint_http.ml b/goblint-http-server/goblint_http.ml new file mode 100644 index 0000000..78ebf5e --- /dev/null +++ b/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 "
  • %s
    • " (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 "%s/" f) + | Some Unix.S_REG -> + let link = Uri.with_path uri (Filename.concat path encoded_f) in + li link f + | Some _ -> + Printf.sprintf "
  • %s
    • " f + | None -> Printf.sprintf "
  • Error with file: %s
    • " f) + listing + in + let contents = String.concat "\n" html in + Printf.sprintf + "

    Directory Listing for %s

    " + (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 "

    Forbidden

    %s is not a normal file or \ + directory

    " 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 ()) diff --git a/goblint-http-server/json.ml b/goblint-http-server/json.ml new file mode 100644 index 0000000..f06d205 --- /dev/null +++ b/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 diff --git a/goblint-http-server/state.ml b/goblint-http-server/state.ml new file mode 100644 index 0000000..22eaa76 --- /dev/null +++ b/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 } diff --git a/goblint-http-server/utils.ml b/goblint-http-server/utils.ml new file mode 100644 index 0000000..9c86354 --- /dev/null +++ b/goblint-http-server/utils.ml @@ -0,0 +1,16 @@ +open Batteries + +let temp_dir_name = Filename.get_temp_dir_name () + +let temp_dir prefix suffix = + let rec loop count = + if count <= 0 then + failwith "Cannot create temporary directory"; + let random = Random.int 100_000 in + let name = Printf.sprintf "%s%d%s" prefix random suffix in + let path = Filename.concat temp_dir_name name in + try + Sys.mkdir path 0o700; + path + with _ -> loop (count - 1) + in loop 100 diff --git a/gobview.opam b/gobview.opam index 218d25f..04e81ac 100644 --- a/gobview.opam +++ b/gobview.opam @@ -14,6 +14,17 @@ bug-reports: "https://github.com/goblint/gobview/issues" depends: [ "dune" {>= "2.7"} "ocaml" {>= "4.10.0"} + "batteries" + "cohttp-lwt" + "cohttp-lwt-unix" + "cohttp-server-lwt-unix" + "fileutils" + "jsonrpc" + "lwt" + "lwt_ppx" + "yojson" + "ppx_yojson_conv" + "conduit-lwt-unix" "jsoo-react" "goblint-cil" {>= "2.0.0"} "ctypes_stubs_js" diff --git a/gobview.opam.locked b/gobview.opam.locked index c5e64e3..8a65907 100644 --- a/gobview.opam.locked +++ b/gobview.opam.locked @@ -13,72 +13,127 @@ license: "MIT" homepage: "https://github.com/goblint/gobview" bug-reports: "https://github.com/goblint/gobview/issues" depends: [ + "angstrom" {= "0.15.0"} + "asn1-combinators" {= "0.2.6"} "astring" {= "0.8.5"} "base" {= "v0.15.1"} "base-bigarray" {= "base"} "base-bytes" {= "base"} "base-threads" {= "base"} "base-unix" {= "base"} + "base64" {= "3.5.0"} + "batteries" {= "3.6.0"} + "bigstringaf" {= "0.9.0"} + "bos" {= "0.2.1"} + "ca-certs" {= "0.2.3"} "camlp-streams" {= "5.0.1"} "cmdliner" {= "1.1.1"} + "cohttp" {= "5.0.0"} + "cohttp-lwt" {= "5.0.0"} + "cohttp-lwt-unix" {= "5.0.0"} + "cohttp-server-lwt-unix" {= "6.0.0~alpha1"} + "conduit" {= "6.2.0"} + "conduit-lwt" {= "6.2.0"} + "conduit-lwt-unix" {= "6.2.0"} "conf-gcc" {= "1.0"} "conf-gmp" {= "4"} + "conf-gmp-powm-sec" {= "3"} + "conf-libssl" {= "4"} "conf-perl" {= "2"} + "conf-pkg-config" {= "2"} "cppo" {= "1.6.9"} "csexp" {= "1.5.1"} + "cstruct" {= "6.1.1"} "ctypes_stubs_js" {= "0.1"} + "domain-name" {= "0.4.0"} "dune" {= "3.6.1"} "dune-build-info" {= "3.6.1"} "dune-configurator" {= "3.6.1"} + "duration" {= "0.2.1"} "either" {= "1.0.0"} + "eqaf" {= "0.9"} + "fileutils" {= "0.6.4"} "fix" {= "20220121"} - "fmt" {= "0.9.0" & with-doc} + "fmt" {= "0.9.0"} "fpath" {= "0.7.3"} "gen_js_api" {= "1.0.9"} + "gmap" {= "0.3.0"} "goblint-cil" {= "2.0.1"} + "http" {= "6.0.0~alpha1"} "integers_stubs_js" {= "1.0"} + "ipaddr" {= "5.3.1"} + "ipaddr-sexp" {= "5.3.1"} "js_of_ocaml" {= "4.1.0"} "js_of_ocaml-compiler" {= "4.1.0"} "js_of_ocaml-lwt" {= "4.1.0"} "js_of_ocaml-ppx" {= "4.1.0"} + "jsonm" {= "1.0.1"} + "jsonrpc" {= "1.15.0~5.0preview1"} "jsoo-react" {= "dev"} + "logs" {= "0.7.0"} "lwt" {= "5.6.1"} "lwt_log" {= "1.1.2"} + "lwt_ppx" {= "2.1.0"} + "lwt_ssl" {= "1.1.3"} + "macaddr" {= "5.3.1"} + "magic-mime" {= "1.3.0"} "menhir" {= "20220210"} "menhirLib" {= "20220210"} "menhirSdk" {= "20220210"} "merlin-extend" {= "0.6.1"} + "mirage-crypto" {= "0.11.1"} + "mirage-crypto-ec" {= "0.11.1"} + "mirage-crypto-pk" {= "0.11.1"} + "mirage-crypto-rng" {= "0.11.1"} + "num" {= "1.4"} "ocaml" {= "4.14.0"} - "ocaml-variants" {= "4.14.0+options"} "ocaml-compiler-libs" {= "v0.12.4"} "ocaml-config" {= "2"} "ocaml-option-flambda" {= "1"} + "ocaml-syntax-shims" {= "1.0.0"} + "ocaml-variants" {= "4.14.0+options"} "ocaml-version" {= "3.5.0"} "ocamlbuild" {= "0.14.2"} "ocamlfind" {= "1.9.5"} "ocamlformat" {= "0.24.1" & dev} "ocp-indent" {= "1.8.1"} "ocplib-endian" {= "1.2"} + "octavius" {= "1.2.2"} "odoc" {= "2.2.0" & with-doc} "odoc-parser" {= "2.0.0"} "ojs" {= "1.1.1"} + "parsexp" {= "v0.15.0"} + "pbkdf" {= "1.2.0"} "ppx_blob" {= "0.7.2"} "ppx_derivers" {= "1.2.1"} "ppx_deriving" {= "5.2.1"} "ppx_deriving_yojson" {= "3.7.0"} + "ppx_js_style" {= "v0.15.0"} + "ppx_sexp_conv" {= "v0.15.1"} + "ppx_yojson_conv" {= "v0.15.1"} + "ppx_yojson_conv_lib" {= "v0.15.0"} "ppxlib" {= "0.28.0"} + "ptime" {= "1.1.0"} "re" {= "1.10.4"} "reason" {= "3.8.2"} "result" {= "1.5"} + "rresult" {= "0.7.0"} "seq" {= "base"} + "sexplib" {= "v0.15.1"} "sexplib0" {= "v0.15.1"} + "ssl" {= "0.5.13"} "stdio" {= "v0.15.0"} "stdlib-shims" {= "0.3.0"} + "stringext" {= "1.6.0"} "topkg" {= "1.0.6"} "tyxml" {= "4.5.0" & with-doc} + "uchar" {= "0.0.2"} + "uri" {= "4.2.0"} + "uri-sexp" {= "4.2.0"} "uucp" {= "15.0.0"} "uuseg" {= "15.0.0"} "uutf" {= "1.0.3"} + "x509" {= "0.16.4"} "yojson" {= "2.0.2"} "zarith" {= "1.12-gob0"} "zarith_stubs_js" {= "v0.15.0"}