Add feature to allow reruns with different parameters in GobView

dune-project

@@ -23,6 +23,9 @@
  (name gobview)
  (synopsis "Web frontend for Goblint")
  (depends
+  cohttp
+  cohttp-lwt
+  cohttp-lwt-jsoo
   dune
   (ocaml (>= 4.10.0))
   batteries
@@ -37,6 +40,8 @@
   ppx_yojson_conv ; TODO: switch to ppx_deriving_yojson like Goblint itself
   conduit-lwt-unix
   jsoo-react
+  lwt
+  uri
   (goblint-cil (>= 2.0.0))
   ctypes_stubs_js
   integers_stubs_js

goblint-http-server/goblint.ml

@@ -57,11 +57,7 @@ let config_raw goblint name value =
   | 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." ""

goblint-http-server/goblint_http.ml

@@ -3,12 +3,13 @@ open Cohttp_lwt
 open Cohttp_lwt_unix
 open Lwt.Infix
 
+module Header = Cohttp.Header
 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 port = ref 8000
 let goblint = ref "goblint"
 let rest = ref []
 
@@ -24,31 +25,38 @@ let specs =
 
 let paths = ref []
 
+let cors_headers =
+  [
+    ("Access-Control-Allow-Origin", "*");
+    ("Access-Control-Allow-Headers", "Content-Type, Access-Control-Allow-Origin, Access-Control-Allow-Methods, Access-Control-Allow-Headers");
+    ("Access-Control-Allow-Methods", "GET, POST, PUT, DELETE, OPTIONS")
+  ] |> Header.of_list
+
 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 ()
+    | exception Yojson.Json_error err -> Server.respond_error ~headers:cors_headers ~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) ()
+        Server.respond_error ~headers:cors_headers ~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) ())
+             >>= fun body -> Server.respond_string ~headers:cors_headers ~status:`OK ~body ())
+          (fun exn -> Server.respond_error ~headers:cors_headers ~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 ()
+  Server.respond_file ~headers:cors_headers ~fname ()
 
 let sort lst =
   let compare_kind = function
@@ -102,7 +110,7 @@ let serve uri path =
       | 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 ^ "/")) ())
+            Server.respond_redirect ~headers:cors_headers ~uri:(Uri.with_path uri (path ^ "/")) ())
           else (
             match Sys.file_exists (Filename.concat file_name !index) with
             | true -> (
@@ -122,12 +130,12 @@ let serve uri path =
                                 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 ()))
+                Server.respond_string ~headers:cors_headers ~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 ()))
+          Server.respond_string ~headers:cors_headers ~status:`OK ~body ()))
     (function
       | Unix.Unix_error (Unix.ENOENT, "stat", p) as e ->
           if p = file_name then (
@@ -143,6 +151,7 @@ let callback state _ req body =
   match meth, parts with
   | `POST, ["api"; name] -> process state name body
   | `GET, _ -> serve uri path
+  | `OPTIONS, _ -> Server.respond ~headers:cors_headers ~status:`OK ~body:`Empty () (* Used for preflight and CORS requests *)
   | _ -> Server.respond_not_found ()
 
 let main () =

gobview.opam

@@ -12,6 +12,9 @@ license: "MIT"
 homepage: "https://github.com/goblint/gobview"
 bug-reports: "https://github.com/goblint/gobview/issues"
 depends: [
+  "cohttp"
+  "cohttp-lwt"
+  "cohttp-lwt-jsoo"
   "dune" {>= "2.7"}
   "ocaml" {>= "4.10.0"}
   "batteries"
@@ -26,6 +29,8 @@ depends: [
   "ppx_yojson_conv"
   "conduit-lwt-unix"
   "jsoo-react"
+  "lwt"
+  "uri"
   "goblint-cil" {>= "2.0.0"}
   "ctypes_stubs_js"
   "integers_stubs_js"

src/App.re

@@ -1,100 +1,12 @@
-open Goblint_lib;
-open Batteries;
-open Js_of_ocaml;
 open Lwt.Infix;
-module Cabs2cil = GoblintCil.Cabs2cil;
-
-exception InitFailed(string);
-
-let init_cil = environment => {
-  // Restore the environment hash table, which
-  // syntacticsearch uses to map temporary variables created
-  // by CIL to their original counterparts.
-  Hashtbl.clear(Cabs2cil.environment);
-  environment
-  |> Hashtbl.enum
-  |> Enum.iter(((k, v)) => Hashtbl.add(Cabs2cil.environment, k, v));
-};
-
-// Each Goblint analysis module is assigned an ID, and this
-// ID depends on the module registration order, which might
-// differ from build to build. This function reorders the
-// analysis list to match the native version of Goblint.
-let renumber_goblint_analyses = registered_name => {
-  let old_registered = Hashtbl.copy(MCP.registered);
-  let old_registered_name = Hashtbl.copy(MCP.registered_name);
-  Hashtbl.clear(MCP.registered);
-  Hashtbl.clear(MCP.registered_name);
-  Hashtbl.iter((name, id) => {
-    let old_id = Hashtbl.find(old_registered_name, name);
-    let spec = Hashtbl.find(old_registered, old_id);
-    Hashtbl.replace(MCP.registered, id, spec);
-    Hashtbl.replace(MCP.registered_name, name, id);
-  }, registered_name);
-};
-
-let init_goblint = (solver, spec, registered_name, config, cil) => {
-  AfterConfig.run(); // This registers the "base" analysis
-
-  try(renumber_goblint_analyses(registered_name)) {
-  | Not_found =>
-    raise(InitFailed("Failed to renumber Goblint analyses"))
-  };
-
-  Sys.chdir("/"); // Don't remove this
-
-  Sys_js.create_file(~name="/goblint/solver.marshalled", ~content=solver);
-  Sys_js.create_file(~name="/goblint/config.json", ~content=config);
-  Sys_js.create_file(~name="/goblint/spec_marshal", ~content=spec);
-
-  GobConfig.merge_file(Fpath.v("/goblint/config.json"));
-
-  GobConfig.set_bool("dbg.verbose", true);
-  // TODO: Uncomment this to improve performance in future
-  // GobConfig.set_bool("verify", false);
-
-  // For some reason, the standard Batteries output channels
-  // appear to be closed by default and writing to them
-  // raises [BatInnerIO.Output_closed]. This fixes it.
-  let out = IO.output_channel(Stdlib.stdout);
-  Messages.formatter := Format.formatter_of_output(out);
-
-  GobConfig.set_string("load_run", "goblint");
-
-  // These two will be set by config.json. Reset them.
-  GobConfig.set_string("save_run", "");
-  GobConfig.set_bool("gobview", false);
-
-  GobConfig.set_auto("trans.activated[+]", "'expeval'");
-
-  Cilfacade.init();
-  Maingoblint.handle_extraspecials();
-  Maingoblint.handle_flags();
-
-  // NOTE: Commenting this out since it breaks the node view. Semantic search
-  // may depend on this code but it is currently broken because of unrelated
-  // (and uknown) reasons anyway.
-  // Cil.iterGlobals(cil, glob =>
-  //   switch (glob) {
-  //   | GFun(fd, _) =>
-  //     Cil.prepareCFG(fd);
-  //     Cil.computeCFGInfo(fd, true);
-  //   | _ => ()
-  //   }
-  // );
-  Cilfacade.current_file := cil;
-
-  let goblint = GvGoblint.unmarshal(spec, cil);
-
-  (goblint, cil);
-};
+open Init;
 
 let init = (solver, spec, config, meta, cil, analyses, warnings, stats, file_loc) => {
   let cil =
     switch (cil) {
     | Ok(s) =>
       let (c, e) = Marshal.from_string(s, 0);
-      init_cil(e);
+      Init.init_cil(e);
       c;
     | _ => raise(InitFailed("Failed to load CIL state"))
     };
@@ -172,6 +84,6 @@ let handle_error = exc => {
         | exc => handle_error(exc)
         }
       | _ => ()
-      },
+      }
     )
 );