diff --git a/dune-project b/dune-project index 7c1c263..db7e269 100644 --- a/dune-project +++ b/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 diff --git a/goblint-http-server/goblint.ml b/goblint-http-server/goblint.ml index 4cc867b..5919694 100644 --- a/goblint-http-server/goblint.ml +++ b/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." "" diff --git a/goblint-http-server/goblint_http.ml b/goblint-http-server/goblint_http.ml index 78ebf5e..1512c6c 100644 --- a/goblint-http-server/goblint_http.ml +++ b/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,6 +25,13 @@ 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 () @@ -31,24 +39,24 @@ let process state name body = 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 "

Forbidden

%s is not a normal file or \ directory

" 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 () = diff --git a/gobview.opam b/gobview.opam index 04e81ac..b2d6715 100644 --- a/gobview.opam +++ b/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" diff --git a/package-lock.json b/package-lock.json index 0566ac3..c88598f 100644 --- a/package-lock.json +++ b/package-lock.json @@ -10,6 +10,7 @@ "license": "MIT", "dependencies": { "bootstrap": "^5.0.2", + "bootstrap5-autocomplete": "^1.1.14", "graphviz-react": "^1.2.0", "monaco-editor": "^0.25.2", "react": "^17.0.2", @@ -7695,6 +7696,16 @@ "integrity": "sha512-1Ge963tyEQWJJ+8qtXFU6wgmAVj9gweEjibUdbmcCEYsn38tVwRk8107rk2vzt6cfQcRr3SlZ8aQBqaD8aqf+Q==", "requires": {} }, + "bootstrap-autocomplete": { + "version": "2.3.7", + "resolved": "https://registry.npmjs.org/bootstrap-autocomplete/-/bootstrap-autocomplete-2.3.7.tgz", + "integrity": "sha512-YD2bev4bDTLsAzkr6lSTuMZOcE7k2+c2BYbtIT+j/XpPnM5ADLlbhR4NnpSsfg6Vde5xQckG/IbdRKrLlAtXOw==" + }, + "bootstrap5-autocomplete": { + "version": "1.1.14", + "resolved": "https://registry.npmjs.org/bootstrap5-autocomplete/-/bootstrap5-autocomplete-1.1.14.tgz", + "integrity": "sha512-QNV/aqW52tbdniydK3r9tibnvcs90schqHLKJH7ZnI1iGV19KalrdAYFsg6Z8eUSyKLZHiFh7v7IQOWL1qvk6g==" + }, "brace-expansion": { "version": "1.1.11", "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz", diff --git a/src/App.re b/src/App.re index 55532f4..fff73f8 100644 --- a/src/App.re +++ b/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) } | _ => () - }, + } ) ); diff --git a/src/Init.re b/src/Init.re new file mode 100644 index 0000000..ac70fcd --- /dev/null +++ b/src/Init.re @@ -0,0 +1,142 @@ +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); +}; + +// function for reloading specific files when rerunning analysis +let reload = (cil) => { + [ + // files to be reloaded + "./solver.marshalled", + "./warnings.marshalled", + "./stats.marshalled", + + // required for solver, solver alone cannot update + "./spec_marshal", + "./analyses.marshalled", + "./config.json", + ] + |> List.map(HttpClient.get) + |> Lwt.all + >>= (l) => { + Lwt.return(switch (l) { + | [solver, warnings, stats, spec, analyses, config] => { + + let goblintAndCil = + switch (solver, spec, analyses, config) { + | (Ok(s), Ok(spec), Ok(t), Ok(c)) => { + let t = Marshal.from_string(t, 0); + Some(init_goblint(s, spec, t, c, cil)) + } + | _ => { + Util.error_without_fail("Failed to load Goblint state"); + None + } + }; + print_endline("Initialized Goblint"); + + let warnings = + switch (warnings) { + | Ok(s) => Some(Marshal.from_string(s, 0)) + | _ => Util.error_without_fail("Failed to load the warning table"); None + }; + print_endline("Restored the warning table"); + + let stats = + switch (stats) { + | Ok(s) => Some(Marshal.from_string(s, 0)) + | _ => Util.error_without_fail("Failed to load runtime stats"); None + }; + + Some((goblintAndCil, warnings, stats)) + } + | _ => None + }) + } +}; \ No newline at end of file diff --git a/src/Main.re b/src/Main.re index 5ce0b10..c20e9fd 100644 --- a/src/Main.re +++ b/src/Main.re @@ -1,11 +1,65 @@ open Batteries; +open Lwt.Infix; [@react.component] let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { + let (analysisState, setAnalysisState) = React.useState(_ => Option.some(ParameterView.Executed)); + + // reloadable components of goblint due to rerunning analyses + let (cil_, setCil_) = React.useState(_ => cil); + let (goblint_, setGoblint_) = React.useState(_ => goblint); + let (warnings_, setWarnings_) = React.useState(_ => warnings); + let (stats_, setStats_) = React.useState(_ => stats); + + React.useEffect1(() => { + switch (analysisState) { + | Some(s) => { + if (ParameterView.is_successful(s)) { + // reload files + let reload = () => { + Init.reload(cil_) >>= + (result) => { + switch (result) { + | Some((goblintAndCil, warnings, stats)) => { + let _ = switch (goblintAndCil) { + | Some((goblint', cil')) => { + setGoblint_(_ => goblint') + setCil_(_ => cil'); + }; + | None => Util.error_without_fail("Could not reload goblint and cil for rerun") + }; + + switch (warnings) { + | Some(w) => setWarnings_(_ => w); + | None => Util.error_without_fail("Could not reload warnings for rerun") + }; + + switch (stats) { + | Some(s) => setStats_(_ => s); + | None => Util.error_without_fail("Could not reload stats for rerun") + }; + }; + | None => Util.error_without_fail("Could not reload metrics for rerun") + } + + setAnalysisState(_ => None); + Lwt.return(); + } + }; + + ignore(reload()); + } + } + | None => setAnalysisState(_ => None); + }; + + None + }, [|analysisState|]); + let (state, dispatch) = React.useReducer( Reducer.reducer, - State.make(~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc, ()), + State.make(~cil=cil_, ~goblint=goblint_, ~warnings=warnings_, ~meta, ~stats=stats_, ~file_loc, ()), ); let fetch_file = @@ -48,6 +102,21 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { [|state.display|], ); + // State management for ParameterView component + let (goblint_path, parameters) = state |> ParameterUtils.get_parameters; + let (destructured_params, _) = parameters |> ParameterUtils.construct_parameters; + + let (history, setHistory) = React.useState(_ => [(destructured_params, Time.get_local_time(), ParameterView.Executed, "")]); + let (inputValue, setInputValue) = React.useState(_ => destructured_params |> ParameterUtils.concat_parameter_list); + let (disableRun, setDisableRun) = React.useState(_ => false); + let (inputState, setInputState) = React.useState(_ => ParameterView.Ok); + let (sortDesc, setSortDesc) = React.useState(_ => true); + + + React.useEffect1(() => { + None + }, [|history|]); +
{React.string("Gobview")}
@@ -66,12 +135,12 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { | None =>
| Some(f) => }} - +
diff --git a/src/Util.ml b/src/Util.ml index dd2bb71..95eaa5e 100644 --- a/src/Util.ml +++ b/src/Util.ml @@ -1,4 +1,5 @@ open Js_of_ocaml let log s = Firebug.console##log (Js.string s) -let error s = Firebug.console##error (Js.string s); failwith(s) +let error_without_fail s = Firebug.console##error (Js.string s) +let error s = error_without_fail(s); failwith(s) let warning s = Firebug.console##warn (Js.string s) diff --git a/src/dune b/src/dune index 8af6dd1..beb8aeb 100644 --- a/src/dune +++ b/src/dune @@ -5,6 +5,9 @@ (modes js) (libraries batteries.unthreaded + cohttp + cohttp-lwt + cohttp-lwt-jsoo fpath gen_js_api goblint-cil @@ -20,6 +23,7 @@ lwt ppx_deriving_yojson.runtime ppx_deriving.runtime + uri yojson zarith zarith_stubs_js) diff --git a/src/ui/base/input.re b/src/ui/base/input.re index 50f18b6..cc11966 100644 --- a/src/ui/base/input.re +++ b/src/ui/base/input.re @@ -1,10 +1,12 @@ [@react.component] -let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?) => { +let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?, ~style=?, ~id=?) => { let (type_, class_, on_submit) = Utils.fix_opt_args3(type_, class_, on_submit); let type_ = Option.value(type_, ~default=`Text); let class_ = Option.value(class_, ~default=["form-control"]); - + let style_ = Option.value(style, ~default=React.Dom.Style.make()); + let id_ = Option.value(id, ~default=""); + let type_ = switch (type_) { | `Text => "text" @@ -25,5 +27,9 @@ let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?) => { Option.iter(cb => cb(), on_submit); }; - ; + switch id_ { + | "" => ; + | _ => ; + } + }; diff --git a/src/ui/base/spinner.re b/src/ui/base/spinner.re new file mode 100644 index 0000000..cb487ff --- /dev/null +++ b/src/ui/base/spinner.re @@ -0,0 +1,4 @@ +[@react.component] +let make = () => { +
+} \ No newline at end of file diff --git a/src/ui/icons/IconArrowDown.re b/src/ui/icons/IconArrowDown.re new file mode 100644 index 0000000..4c8be67 --- /dev/null +++ b/src/ui/icons/IconArrowDown.re @@ -0,0 +1,6 @@ +[@react.component] +let make = () => { + + + +} \ No newline at end of file diff --git a/src/ui/icons/IconArrowUp.re b/src/ui/icons/IconArrowUp.re new file mode 100644 index 0000000..ac91cc5 --- /dev/null +++ b/src/ui/icons/IconArrowUp.re @@ -0,0 +1,6 @@ +[@react.component] +let make = () => { + + + +} \ No newline at end of file diff --git a/src/ui/icons/IconCheckmark.re b/src/ui/icons/IconCheckmark.re new file mode 100644 index 0000000..ec9d7b6 --- /dev/null +++ b/src/ui/icons/IconCheckmark.re @@ -0,0 +1,6 @@ +[@react.component] +let make = () => { + + + ; +} \ No newline at end of file diff --git a/src/ui/icons/IconClock.re b/src/ui/icons/IconClock.re new file mode 100644 index 0000000..7e019ff --- /dev/null +++ b/src/ui/icons/IconClock.re @@ -0,0 +1,7 @@ +[@react.component] +let make = () => { + + + + +} \ No newline at end of file diff --git a/src/ui/icons/IconPlay.re b/src/ui/icons/IconPlay.re new file mode 100644 index 0000000..3bbe543 --- /dev/null +++ b/src/ui/icons/IconPlay.re @@ -0,0 +1,6 @@ +[@react.component] +let make = () => { + + + +} \ No newline at end of file diff --git a/src/ui/icons/IconWarning.re b/src/ui/icons/IconWarning.re new file mode 100644 index 0000000..8e4fd6e --- /dev/null +++ b/src/ui/icons/IconWarning.re @@ -0,0 +1,7 @@ +[@react.component] +let make = () => { + + + + +} \ No newline at end of file diff --git a/src/ui/icons/IconX.re b/src/ui/icons/IconX.re new file mode 100644 index 0000000..362907e --- /dev/null +++ b/src/ui/icons/IconX.re @@ -0,0 +1,6 @@ +[@react.component] +let make = () => { + + + +} \ No newline at end of file diff --git a/src/ui/panel/Panel.re b/src/ui/panel/Panel.re index b7ef9af..44be345 100644 --- a/src/ui/panel/Panel.re +++ b/src/ui/panel/Panel.re @@ -19,6 +19,7 @@ let make_nav_pills = (current, dispatch) => { |> List.mapi((i, (v, n)) => {
  • @@ -31,28 +32,26 @@ let make_nav_pills = (current, dispatch) => { }; [@react.component] -let make = (~state, ~dispatch) => { - let parameters = - switch (Yojson.Safe.Util.member("command", state.meta)) { - | `String(command) => command - | _ => "" - }; +let make = (~state, ~dispatch, ~goblint_path, ~inputValue, ~setInputValue, ~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory, ~setAnalysisState) => { let locations = (state.goblint)#dead_locations; let current = state.selected_panel; + + let component = switch (current) { + | Some(Warnings) => + | Some(DeadCode) => + | Some(Statistics) => + | Some(Parameters) => + | _ => React.null + }; +
    {make_nav_pills(current, dispatch)}
    - {switch (current) { - | Some(Warnings) => - | Some(DeadCode) => - | Some(Parameters) => - | Some(Statistics) => - | _ => React.null - }} + {component}
    ; -}; +}; \ No newline at end of file diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index c6c6b00..4b272f5 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,4 +1,396 @@ +open Lwt; +open Cohttp; +open Cohttp_lwt; + +module Js = Js_of_ocaml.Js; +module Client = Cohttp_lwt_jsoo.Client; +module ReactDOM = React.Dom; + +type paramState = Executed | Executing | Canceled | Error; + +// For debugging purposes and potential further use +let paramState_to_string = (p: paramState) => { + switch p { + | Executed => "Executed"; + | Executing => "Executing"; + | Canceled => "Canceled"; + | Error => "Error"; + }; +}; + +let is_successful = (p: paramState) => p == Executed; + +type inputState = Blacklisted | Malformed | Empty | Ok; + +let inputState_to_string = (i: inputState) => { + switch i { + | Blacklisted => "Blacklisted options are not allowed"; + | Malformed => "Options are malformed. Check the input again" + | Empty => "At least one parameter has to be entered"; + | Ok => ""; + } +} + +let is_ok = (i: inputState) => i == Ok; + +let option_whitelist = [ + "incremental.force-reanalyze.funs", + "incremental.reluctant.enabled", + "incremental.compare", + "incremental.detect-renames", + "incremental.restart", + "incremental.postsolver", + "annotation.goblint_precision" +]; + +let scheme = "http"; +let host = "127.0.0.1"; +let port = 8000; +let analyze_path = "/api/analyze"; +let config_path = "/api/config"; +let analyze_uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, analyze_path) |> Uri.of_string; +let config_uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, config_path) |> Uri.of_string; + +let headers = [ + ("Content-Type", "application/json"), + ("Access-Control-Allow-Origin", Printf.sprintf("%s://%s:%d", scheme, host, port)), + ("Access-Control-Allow-Headers", "Content-Type"), + ("Access-Control-Allow-Methods", "GET, POST, PUT, DELETE, OPTIONS") +] |> Header.of_list; + [@react.component] -let make = (~parameters) => { -

    {parameters |> React.string}

    +let make = (~goblint_path, ~inputValue, ~setInputValue, ~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory, ~setAnalysisState) => { + // Linked to cancelation, see reasons below in on_cancel() for why it is commented out + //let (disableCancel, setDisableCancel) = React.useState(_ => true); + + React.useEffect1(() => { + None + }, [|inputValue|]); + + React.useEffect1(() => { + None + }, [|sortDesc|]); + + React.useEffect1(() => { + None + }, [|disableRun|]); + + let on_sort = (ev) => { + React.Event.Mouse.preventDefault(ev); + setSortDesc(_ => !sortDesc); + } + + let get_input_state = (parameter_list: list((string, string)), is_malformed, input_val): inputState => { + if (String.length(input_val) == 0) { + Empty + } else if(is_malformed || List.length(parameter_list) == 0) { + Malformed + } else { + let has_found_option = + parameter_list + |> List.for_all(((option, _)) => { + let result = + option_whitelist + |> List.map (whitelisted_option => String.starts_with(~prefix=whitelisted_option, option)) + |> List.find_opt (b => b == true); + + switch (result) { + | Some(b) => b; + | None => false; + } + }); + + if (!has_found_option) { + Blacklisted + } else { + Ok + } + } + } + + let react_on_input = (parameter_list, is_malformed, inputValue) => { + let input_state = get_input_state(parameter_list, is_malformed, inputValue); + setInputState(_ => input_state); + + let isInvalid = !is_ok(input_state) + setDisableRun(_ => isInvalid); + + isInvalid + } + + let check_input = (inputValue) : bool => { + let (tuple_parameter_list, is_malformed) = + inputValue + |> ParameterUtils.construct_parameters + |> ((p,b)) => (p |> ParameterUtils.tuples_from_parameters, b); + + react_on_input(tuple_parameter_list, is_malformed, inputValue) + } + + let on_add_parameter = (ev) => { + let target = React.Event.Mouse.target(ev) |> ReactDOM.domElement_of_js; + let unresolved_parameter = target##.textContent |> Js.Opt.to_option; + + let parameter = switch unresolved_parameter { + | Some(p) => { + let resolved_parameter = Js.to_string(p); + if (String.length(inputValue) > 0) { + " " ++ resolved_parameter + } else { + resolved_parameter + } + }; + | None => "" + }; + + setInputValue(inputVal => { + let new_inputVal = String.cat(inputVal, parameter); + new_inputVal + }); + } + + let on_change = (new_inputValue) => { + let _ = check_input(new_inputValue); + setInputValue(_ => new_inputValue); + }; + + let on_submit = () => { + let (parameter_list, tuple_parameter_list, is_malformed) = + inputValue + |> ParameterUtils.construct_parameters + |> ((p,b)) => (p, p |> ParameterUtils.tuples_from_parameters, b); + + // To prevent invalid default input to be executed, with i.e. blacklisted options, we check the input value first + /*let isInvalid = react_on_input(tuple_parameter_list, is_malformed, inputValue);*/ + + if (inputState == Ok && !is_malformed && !disableRun) { + let time = Time.get_local_time(); + let init_state = Executing; + let element = (parameter_list, time, init_state, ""); + + let new_history = List.cons(element, history); + + setHistory(_ => new_history); + //setDisableCancel(_ => false); + setDisableRun(_ => true); + setAnalysisState(_ => Some(init_state)); + + let modify_history = (result: paramState, response_msg: string): unit => { + let pickedElem = new_history |> List.hd; + + if (pickedElem == element) { + let intermediateHistory = new_history |> List.tl; + let new_history = List.cons(((parameter_list, time, result, response_msg)), intermediateHistory); + setHistory(_ => new_history); + //setDisableCancel(_ => true); + setDisableRun(_ => false); + setAnalysisState(_ => Some(result)); + } + } + + let transform_resp = ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; + + Cohttp_lwt.Body.to_string(body) >>= (body) => { + if (code < 200 || code >= 400) { + Lwt.return((Error, body)); + } else { + Lwt.return((Executed, body)); + }; + } + }; + + let inner_config_api_call = (config_body): Lwt.t((paramState, string)) => { + Client.post(config_uri, ~body=config_body, ~headers=headers) >>= transform_resp + }; + + let config_api_call = (config_opts: list((string, string))) => { + let config_call_function = () => { + config_opts + |> List.map(((k,v)) => { + let v' = if (!String.equal("true", v) && + !String.equal("false", v) && + (!String.starts_with(~prefix="[", v) && !String.ends_with(~suffix="]", v) && + !Str.string_match((Str.regexp({|^[0-9]+$|})), v, 0))) { + "\"" ++ v ++ "\"" // check whether value is a string => wrap it in "" + } else { + v + }; + + `List([`String(k), Yojson.Safe.from_string(v')]) + |> Yojson.Safe.to_string + |> Body.of_string; + }) + |> List.map(inner_config_api_call) + |> Lwt.all; + }; + + let exception_handler = (exc) => { + Lwt.return([(Error, Printexc.to_string(exc))]); + }; + + Lwt.catch(config_call_function, exception_handler); + }; + + let inner_analyze_api_call = (analyze_body) => { + Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= transform_resp + }; + + let analyze_body = + `List([`String ("Functions"), `List ([])]) + |> Yojson.Safe.to_string + |> Body.of_string; + + let analyze_api_call = () => { + let exception_handler = (exc) => { + Lwt.return((Error, Printexc.to_string(exc))); + }; + + tuple_parameter_list + |> config_api_call >>= + (result) => { + let result_state = result |> List.find_opt(((state, _)) => state == Error); + + switch (result_state) { + | None => Lwt.return((Executed, "")) + | Some(r) => Lwt.return(r) + } + } >>= + (result) => { + switch result { + | (Executed, _) => Lwt.catch(() => inner_analyze_api_call(analyze_body), exception_handler); + | (_, msg) => Lwt.return((Error, msg)) + } + } >>= + ((state, msg)) => { + modify_history(state, msg); + Lwt.return() + }; + }; + + ignore(analyze_api_call()); + } + }; + + // This cancel function is here in case it will be implemented in the http-server, not far fetched. + /*let on_cancel = () => { + let (param, time, _) = history |> List.hd; + let intermediateHistory = history |> List.tl; + let new_history = List.cons(((param, time, Canceled)), intermediateHistory); + setHistory(_ => new_history); + setDisableCancel(_ => true); + };*/ + + // Check whether default parameters are "Ok" or not + let (tuple_parameter_list, is_malformed) = + inputValue + |> ParameterUtils.construct_parameters + |> ((p,b)) => (p |> ParameterUtils.tuples_from_parameters, b); + let _ = react_on_input(tuple_parameter_list, is_malformed, inputValue); + + let map_history_entry_to_list_entry = (history) => { + history + |> (history) => { + if (!sortDesc) { + history |> List.rev + } else { + history + } + } + |> List.mapi((i, (parameter_grouping, time, paramState, msg)) => + {
  • +
    +
    + {switch paramState { + | Error =>
    + | _ => { +
    + {switch paramState { + | Executing => + | Canceled => + | Executed => + | Error => + }} +
    + } + }} +
    +
    + + {time ++ " " |> React.string} +
    +
    +
    + {parameter_grouping |> List.mapi((j,e) => { + + {e |> React.string} + + }) |> React.list} +
    +
    +
    +
    • } + ); + }; + + let list_elements = history |> map_history_entry_to_list_entry; + +
    +
    + + + // Commented out because http server does not support cancelation yet + /**/ + + + // Input and tooltip are seperated due to display issues + {switch inputState { + | Malformed + | Blacklisted + | Empty => + | Ok => ; + }} + {switch inputState { + | Ok => React.null; + | _ => { +
    + {inputState |> inputState_to_string |> React.string} +
    + }; + }} +
    + +
    +
    +
      + {
    1. +
      +
      +
      + {"Status" |> React.string} +
      +
      + {"Time " |> React.string} + {if (sortDesc) { + + } else { + + }} +
      +
      + {"Parameters" |> React.string} +
      +
      +
      +
      2. } + {list_elements |> React.list} +
    +
    +
    +
    ; } \ No newline at end of file diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re new file mode 100644 index 0000000..3c2c653 --- /dev/null +++ b/src/utils/ParameterUtils.re @@ -0,0 +1,66 @@ +open State; + +let concat_parameter_list = String.concat(" "); +let concat_grouped_parameters = (parameters) => parameters |> List.map(concat_parameter_list) |> concat_parameter_list; + +let parameters_regex = Str.regexp({|\(--\(enable\|disable\) [-a-zA-Z0-9\._]+\)\|\(--set [-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)? \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)\)\|\(--[-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)? \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)\)|}); +let enable_disable_regex = Str.regexp({|--\(enable\|disable\) \([-a-zA-Z0-9\._]+\)|}); +let set_regex = Str.regexp({|--set \([-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)?\) \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)|}); +let other_regex = Str.regexp({|--\([-a-zA-Z0-9\._]+\(\[\(\+\|\-\)\]\)?\) \([-a-zA-Z0-9\._\/]+\|\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|\[\(\(\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\(\([ ]*,[ ]*\)\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\|[-a-zA-Z0-9\._\/]+\)\)*\)\|\(\("\|'\)[-a-zA-Z0-9\._, \!\?\$\*\/]*\("\|'\)\)\|[-a-zA-Z0-9\._\/]*\)\]\)|}); +let string_with_upticks_regex = Str.regexp({|'\(.*\)'|}); + +// Reads Goblint's path and the parameters which were taken into consideration by Goblint for the first analysis +let get_parameters = (state) => { + let raw_parameters = switch (Yojson.Safe.Util.member("command", state.meta)) { + | `String(command) => command + | _ => "" + } + |> String.split_on_char(' ') + |> List.map((s) => { String.sub(s, 1, String.length(s)-2) }); + + let goblint_path = raw_parameters |> List.hd; + let parameters = raw_parameters |> List.tl |> concat_parameter_list; + + (goblint_path, parameters); +}; + +// Reads and extracts every parameter and returns additionally whether the input is malformed or well formed +let construct_parameters = (parameters: string): (list(string), bool) => { + let replaced_words = ref([]); + let result = parameters |> Str.global_substitute(parameters_regex, (substring => { + replaced_words := replaced_words.contents |> List.cons(Str.matched_group(0, substring)); + "" + })); + + (replaced_words.contents, (result |> String.trim |> String.length) > 0) +}; + +let tuples_from_parameters = (grouped_parameters: list(string)): list((string,string)) => { + grouped_parameters + |> List.map((parameter) => { + // The string has to be compared to a regex instead of using String.starts_with as Str.matched_group is used in each case below; otherwise an exc will be raised + // Additionally, every Str.matched_group call has to be preceeded by an independent Str.string_match otherwise it takes the group or returns a wrong substring + // This order of cases was chosen because "--" matches to all and should be the last option therefore + if (Str.string_match(enable_disable_regex, parameter, 0)) { + switch ((Str.matched_group(1, parameter), Str.matched_group(2, parameter))) { + | ("enable", option) => Some((option, "true")) + | ("disable", option) => Some((option, "false")) + | exception Not_found => None + | _ => None + } + } else if (Str.string_match(set_regex, parameter, 0) || Str.string_match(other_regex, parameter, 0)) { + switch ((Str.matched_group(1, parameter), Str.matched_group(4, parameter))) { + | (option, value) => Some((option, value)) + | exception Not_found => None + } + } else { + None + } + }) + |> List.filter(e => !Option.is_none(e)) + |> List.map(e => { + let (o,v) = (e |> Option.get); + let v' = Str.global_replace(string_with_upticks_regex, {|"\1"|}, v); + (o,v') + }) +}; \ No newline at end of file diff --git a/src/utils/Time.re b/src/utils/Time.re new file mode 100644 index 0000000..3dfe1b3 --- /dev/null +++ b/src/utils/Time.re @@ -0,0 +1,17 @@ +open Unix + +let time_to_string = (time) => { + let rawMinutes = string_of_int(time.tm_min); + + rawMinutes + |> String.cat(if (String.length(rawMinutes) == 1) { "0" } else { "" }) + |> String.cat(":") + |> String.cat(string_of_int(time.tm_hour)) + |> String.cat(" "); +}; + +let get_local_time = () => { + Unix.time() + |> Unix.localtime + |> time_to_string; +}; \ No newline at end of file