From ae8f8c5974234568ec7bcbd6b4bb3f0191b0ff67 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sat, 8 Apr 2023 20:53:16 +0200 Subject: [PATCH 01/48] Use textfield instead of raw parameter string --- src/ui/panel/ParameterView.re | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index c6c6b00..b3da8a0 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,4 +1,5 @@ [@react.component] let make = (~parameters) => { -

{parameters |> React.string}

+ //

{parameters |> React.string}

+ React.string> } \ No newline at end of file From 834b4a4bbecc4eee686126b3e866fb57191b89f8 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sat, 15 Apr 2023 22:38:21 +0200 Subject: [PATCH 02/48] Use Input component for better input field in ParameterView --- src/ui/panel/ParameterView.re | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index b3da8a0..8f4e6ad 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,5 +1,7 @@ [@react.component] let make = (~parameters) => { - //

{parameters |> React.string}

- React.string> + let on_change = (_) => (); + let value = parameters; + + ; } \ No newline at end of file From 621bd6fe48ede5769fd1facccecf0640a0222d5b Mon Sep 17 00:00:00 2001 From: sxprz Date: Sat, 22 Apr 2023 21:34:22 +0200 Subject: [PATCH 03/48] Add replay button for different params and add history for prev params --- src/ui/icons/IconPlay.re | 13 +++++++++++++ src/ui/panel/ParameterView.re | 29 ++++++++++++++++++++++++++--- 2 files changed, 39 insertions(+), 3 deletions(-) create mode 100644 src/ui/icons/IconPlay.re diff --git a/src/ui/icons/IconPlay.re b/src/ui/icons/IconPlay.re new file mode 100644 index 0000000..e40ef8e --- /dev/null +++ b/src/ui/icons/IconPlay.re @@ -0,0 +1,13 @@ +[@react.component] +let make = (~fill) => { + let key = switch (fill) { + | "fill" => "bi bi-play-fill" + | "btn" => "bi bi-play-btn" + | "circle" => "bi bi-play-circle" + | _ => "bi bi-play" + }; + + + + ; +} \ No newline at end of file diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 8f4e6ad..6b8aaed 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,7 +1,30 @@ [@react.component] let make = (~parameters) => { - let on_change = (_) => (); - let value = parameters; + let on_change = (_) => (); // not needed, but required... + let on_submit = (_) => (); // TODO later needed for new exec of params + let value = parameters; // TODO maybe use |> and maps to transform ''-args into whole string (concat) - ; + <> +
+ + +
+
{"History" |> React.string}
+
    +
  1. + {"Hello World" |> React.string} +
    2. +
  2. + {"Hello World" |> React.string} +
    3. +
  3. + {"Hello World" |> React.string} +
    4. +
  4. + {"Hello World" |> React.string} +
    5. +
+ ; } \ No newline at end of file From da69b7effe514844853702ec08782345cef704e8 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sat, 6 May 2023 12:41:38 +0200 Subject: [PATCH 04/48] Implement history list under param rerun (WIP) --- src/ui/icons/IconPlay.re | 6 +-- src/ui/panel/ParameterView.re | 71 ++++++++++++++++++++++++----------- 2 files changed, 52 insertions(+), 25 deletions(-) diff --git a/src/ui/icons/IconPlay.re b/src/ui/icons/IconPlay.re index e40ef8e..6b4ec22 100644 --- a/src/ui/icons/IconPlay.re +++ b/src/ui/icons/IconPlay.re @@ -1,13 +1,13 @@ [@react.component] let make = (~fill) => { - let key = switch (fill) { + /*let key = switch (fill) { | "fill" => "bi bi-play-fill" | "btn" => "bi bi-play-btn" | "circle" => "bi bi-play-circle" | _ => "bi bi-play" - }; + };*/ - + ; } \ No newline at end of file diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 6b8aaed..58456c8 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,30 +1,57 @@ [@react.component] let make = (~parameters) => { + + let params = + parameters + |> String.split_on_char(' ') + |> List.map((s) => { String.sub(s, 1, String.length(s)-2)}) + |> String.concat(" "); + + let (history, setHistory) = React.useState(_ => [|params|]); + + let map_history_entry_to_list_entry = (arr) => { + arr |> Array.map(entry => { +
  • + {entry |> React.string} +
    • + }) + } + + let list_elements = map_history_entry_to_list_entry(history) + + React.useEffect1(() => { + //list_elements = history |> map_history_entry_to_list_entry + None + }, [|history|]); + let on_change = (_) => (); // not needed, but required... - let on_submit = (_) => (); // TODO later needed for new exec of params - let value = parameters; // TODO maybe use |> and maps to transform ''-args into whole string (concat) + let on_submit = (_) => { + let new_history = Array.append(history, [|"Hello World!"|]) + setHistory(_ => new_history) + + // TODO transform param string with "' '" seperation mask + // TODO execute newly transformed params + }; <> -
    - - + //
    + //
    +
    +
    + + +
    +
    + {"History" |> React.string} +
    +
    +
      + {list_elements |> Array.to_list |> React.list} +
    +
    -
    {"History" |> React.string}
    -
      -
    1. - {"Hello World" |> React.string} -
      2. -
    2. - {"Hello World" |> React.string} -
      3. -
    3. - {"Hello World" |> React.string} -
      4. -
    4. - {"Hello World" |> React.string} -
      5. -
    ; } \ No newline at end of file From a28ded23ccdb2214bc718e0a02133467718b788b Mon Sep 17 00:00:00 2001 From: sxprz Date: Sun, 7 May 2023 16:07:51 +0200 Subject: [PATCH 05/48] Add keys to each list elem and try to manipulate input on Input component --- src/ui/panel/ParameterView.re | 35 +++++++++++++++++++++++------------ 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 58456c8..1e542ed 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -8,13 +8,14 @@ let make = (~parameters) => { |> String.concat(" "); let (history, setHistory) = React.useState(_ => [|params|]); + let (value, setValue) = React.useState(_ => params) let map_history_entry_to_list_entry = (arr) => { - arr |> Array.map(entry => { -
  • + arr |> Array.mapi((i, entry) => + {
  • {entry |> React.string} -
    • - }) + } + ) } let list_elements = map_history_entry_to_list_entry(history) @@ -24,34 +25,44 @@ let make = (~parameters) => { None }, [|history|]); - let on_change = (_) => (); // not needed, but required... - let on_submit = (_) => { - let new_history = Array.append(history, [|"Hello World!"|]) + React.useEffect1(() => { + None + }, [|value|]); + + let on_change = (new_value) => { + setValue(_ => new_value) + }; + + let on_submit = () => { + let new_history = Array.append(history, [|value|]) setHistory(_ => new_history) // TODO transform param string with "' '" seperation mask // TODO execute newly transformed params }; - <> +
    //
    //
    -
    +
    - +
    +
    {"History" |> React.string}
    -
      +
        {list_elements |> Array.to_list |> React.list}
    - ; +
    ; } \ No newline at end of file From 55abb6856c3e16967f4d501eacc922c03f23e8a8 Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 8 May 2023 19:17:26 +0200 Subject: [PATCH 06/48] Change style of first param row --- src/ui/panel/ParameterView.re | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 1e542ed..7da7be2 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -21,7 +21,6 @@ let make = (~parameters) => { let list_elements = map_history_entry_to_list_entry(history) React.useEffect1(() => { - //list_elements = history |> map_history_entry_to_list_entry None }, [|history|]); @@ -46,15 +45,14 @@ let make = (~parameters) => { //
    - - +
    + + +
    -
    {"History" |> React.string}
    From 42333501b5199b777d94cae3d78355bda6d0a13b Mon Sep 17 00:00:00 2001 From: sxprz Date: Tue, 9 May 2023 18:07:26 +0200 Subject: [PATCH 07/48] Group input and buttons --- src/ui/panel/ParameterView.re | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 7da7be2..973c849 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,3 +1,5 @@ +module ReactDOM = React.Dom + [@react.component] let make = (~parameters) => { @@ -43,16 +45,17 @@ let make = (~parameters) => {
    //
    //
    -
    -
    -
    - - -
    -
    +
    + + + +
    +
    {"History" |> React.string}
    From b74ad4306ebb9741b0bf565a7fc263774778584b Mon Sep 17 00:00:00 2001 From: sxprz Date: Fri, 12 May 2023 00:23:36 +0200 Subject: [PATCH 08/48] Implement correct scroll bar behaviour for param history --- src/ui/panel/Panel.re | 16 +++++++++------- src/ui/panel/ParameterView.re | 6 ++---- 2 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/ui/panel/Panel.re b/src/ui/panel/Panel.re index b7ef9af..7e1c01f 100644 --- a/src/ui/panel/Panel.re +++ b/src/ui/panel/Panel.re @@ -40,18 +40,20 @@ let make = (~state, ~dispatch) => { let locations = (state.goblint)#dead_locations; + let panel = switch (current) { + | Some(Warnings) => + | Some(DeadCode) => + | Some(Parameters) => + | Some(Statistics) => + | _ => React.null + }; + let current = state.selected_panel;
    {make_nav_pills(current, dispatch)}
    - {switch (current) { - | Some(Warnings) => - | Some(DeadCode) => - | Some(Parameters) => - | Some(Statistics) => - | _ => React.null - }} + {panel}
    ; diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 973c849..ce87a81 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -43,8 +43,6 @@ let make = (~parameters) => { };
    - //
    - //
    -
    +
    {"History" |> React.string}
    -
    +
      {list_elements |> Array.to_list |> React.list}
    From ec42bf6aaeec469e5eeeec25902a94af83376b45 Mon Sep 17 00:00:00 2001 From: sxprz Date: Fri, 12 May 2023 00:29:35 +0200 Subject: [PATCH 09/48] Fix missing variable 'current' --- src/ui/panel/Panel.re | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/ui/panel/Panel.re b/src/ui/panel/Panel.re index 7e1c01f..de5fd5a 100644 --- a/src/ui/panel/Panel.re +++ b/src/ui/panel/Panel.re @@ -40,21 +40,22 @@ let make = (~state, ~dispatch) => { let locations = (state.goblint)#dead_locations; - let panel = switch (current) { + let current = state.selected_panel; + + let component = switch (current) { | Some(Warnings) => | Some(DeadCode) => - | Some(Parameters) => | Some(Statistics) => + | Some(Parameters) => | _ => React.null }; - let current = state.selected_panel;
    {make_nav_pills(current, dispatch)}
    - {panel} + {component}
    ; -}; +}; \ No newline at end of file From 6a5770885b33da7f2a607caea878b3e3606c0523 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sat, 13 May 2023 13:00:27 +0200 Subject: [PATCH 10/48] Move code further down --- src/ui/panel/ParameterView.re | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index ce87a81..0a9a330 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -10,17 +10,8 @@ let make = (~parameters) => { |> String.concat(" "); let (history, setHistory) = React.useState(_ => [|params|]); - let (value, setValue) = React.useState(_ => params) + let (value, setValue) = React.useState(_ => params); - let map_history_entry_to_list_entry = (arr) => { - arr |> Array.mapi((i, entry) => - {
  • - {entry |> React.string} -
    • } - ) - } - - let list_elements = map_history_entry_to_list_entry(history) React.useEffect1(() => { None @@ -42,12 +33,24 @@ let make = (~parameters) => { // TODO execute newly transformed params }; + let playButton = ; + + let map_history_entry_to_list_entry = (arr) => { + arr |> Array.mapi((i, entry) => + {
  • + {entry |> React.string} +
    • } + ) + }; + + let list_elements = map_history_entry_to_list_entry(history); +
    - + {playButton} From 575f74aea347f51b95ba287cc71f3e482bb3b640 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sat, 13 May 2023 13:34:48 +0200 Subject: [PATCH 11/48] Add checkmark indication for normal run; x symbol WIP for canceled runs --- src/ui/icons/IconCheckmark.re | 6 ++++++ src/ui/panel/ParameterView.re | 11 ++++++++++- 2 files changed, 16 insertions(+), 1 deletion(-) create mode 100644 src/ui/icons/IconCheckmark.re 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/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 0a9a330..b5224bb 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -41,7 +41,16 @@ let make = (~parameters) => { let map_history_entry_to_list_entry = (arr) => { arr |> Array.mapi((i, entry) => {
  • - {entry |> React.string} +
    +
    +
    + +
    +
    + {entry |> React.string} +
    +
    +
    • } ) }; From dc2de42267a296c59653d2d19a2f8ae539a343f3 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sun, 14 May 2023 10:16:51 +0200 Subject: [PATCH 12/48] Add time for when run was started and redesign param history --- src/ui/icons/IconClock.re | 7 ++++++ src/ui/panel/ParameterView.re | 46 ++++++++++++++++++++++++++++++----- 2 files changed, 47 insertions(+), 6 deletions(-) create mode 100644 src/ui/icons/IconClock.re 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/panel/ParameterView.re b/src/ui/panel/ParameterView.re index b5224bb..c5463e8 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,3 +1,5 @@ +open Unix + module ReactDOM = React.Dom [@react.component] @@ -9,7 +11,20 @@ let make = (~parameters) => { |> List.map((s) => { String.sub(s, 1, String.length(s)-2)}) |> String.concat(" "); - let (history, setHistory) = React.useState(_ => [|params|]); + let timeToString = (time) => { + string_of_int(time.tm_min) + |> String.cat(":") + |> String.cat(string_of_int(time.tm_hour)) + |> String.cat(" "); + } + + let getLocalTime = () => { + Unix.time() + |> Unix.localtime + |> timeToString; + } + + let (history, setHistory) = React.useState(_ => [|(params, getLocalTime())|]); let (value, setValue) = React.useState(_ => params); @@ -26,7 +41,7 @@ let make = (~parameters) => { }; let on_submit = () => { - let new_history = Array.append(history, [|value|]) + let new_history = Array.append(history, [|(value, getLocalTime())|]) setHistory(_ => new_history) // TODO transform param string with "' '" seperation mask @@ -39,13 +54,17 @@ let make = (~parameters) => { ; let map_history_entry_to_list_entry = (arr) => { - arr |> Array.mapi((i, entry) => + arr |> Array.mapi((i, (entry, time)) => {
  • -
    +
    +
    + + {time |> React.string} +
    {entry |> React.string}
    @@ -58,7 +77,7 @@ let make = (~parameters) => { let list_elements = map_history_entry_to_list_entry(history);
    -
    +
    {playButton} ; let map_history_entry_to_list_entry = (arr) => { - arr |> Array.mapi((i, (entry, time)) => + arr |> Array.mapi((i, (entry, time, paramState)) => {
  • - + {switch paramState { + | Executing => + | Canceled => + | Executed => + | Error => + }}
    @@ -79,7 +105,7 @@ let make = (~parameters) => {
    {playButton} - From e6c49a90aea60120ed399b82204628cc55a2fe87 Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 15 May 2023 22:40:52 +0200 Subject: [PATCH 14/48] Add important state management TODO for whole App --- src/ui/panel/ParameterView.re | 1 + 1 file changed, 1 insertion(+) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 16386aa..dac3436 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -8,6 +8,7 @@ module ReactDOM = React.Dom type paramState = Executed | Executing | Canceled | Error; +// TODO FIX BUG: make param history permanently available until GobView is closed again => clear afterwards [@react.component] let make = (~parameters) => { From 29641bf0801cb7b7314e315666bf94bd0a0e258b Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 17 May 2023 21:41:20 +0200 Subject: [PATCH 15/48] Fix non-permanent state of history table after switching tabs --- src/Main.re | 12 +++++++++++- src/ui/panel/Panel.re | 9 ++------- src/ui/panel/ParameterView.re | 34 ++++------------------------------ src/utils/ParameterUtils.re | 21 +++++++++++++++++++++ src/utils/Time.re | 21 +++++++++++++++++++++ 5 files changed, 59 insertions(+), 38 deletions(-) create mode 100644 src/utils/ParameterUtils.re create mode 100644 src/utils/Time.re diff --git a/src/Main.re b/src/Main.re index 5ce0b10..a2ee231 100644 --- a/src/Main.re +++ b/src/Main.re @@ -48,6 +48,16 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { [|state.display|], ); + let parameters = state |> ParameterUtils.getParameters; + Util.log(parameters); + + let destructuredParameters = parameters |> ParameterUtils.concatParameters; + let (history, setHistory) = React.useState(_ => [|(destructuredParameters, Time.getLocalTime(), ParameterView.Executed)|]); + + React.useEffect1(() => { + None + }, [|history|]); +
    {React.string("Gobview")}
    @@ -66,7 +76,7 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { | None =>
    | Some(f) => }} - +
    { }; [@react.component] -let make = (~state, ~dispatch) => { - let parameters = - switch (Yojson.Safe.Util.member("command", state.meta)) { - | `String(command) => command - | _ => "" - }; +let make = (~state, ~dispatch, ~parameters, ~history, ~setHistory) => { let locations = (state.goblint)#dead_locations; @@ -46,7 +41,7 @@ let make = (~state, ~dispatch) => { | Some(Warnings) => | Some(DeadCode) => | Some(Statistics) => - | Some(Parameters) => + | Some(Parameters) => | _ => React.null }; diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index dac3436..2105ab7 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,4 +1,3 @@ -open Unix //open Lwt //open Cohttp //open Cohttp_lwt_unix @@ -8,37 +7,12 @@ module ReactDOM = React.Dom type paramState = Executed | Executing | Canceled | Error; -// TODO FIX BUG: make param history permanently available until GobView is closed again => clear afterwards [@react.component] -let make = (~parameters) => { - - let initParams = - parameters - |> String.split_on_char(' ') - |> List.map((s) => { String.sub(s, 1, String.length(s)-2)}) - |> String.concat(" "); - - let timeToString = (time) => { - string_of_int(time.tm_min) - |> String.cat(":") - |> String.cat(string_of_int(time.tm_hour)) - |> String.cat(" "); - } - - let getLocalTime = () => { - Unix.time() - |> Unix.localtime - |> timeToString; - } +let make = (~parameters, ~history, ~setHistory) => { - let (history, setHistory) = React.useState(_ => [|(initParams, getLocalTime(), Executed)|]); - let (value, setValue) = React.useState(_ => initParams); + let (value, setValue) = React.useState(_ => parameters); let (disableCancel, setDisableCancel) = React.useState(_ => true); - React.useEffect1(() => { - None - }, [|history|]); - React.useEffect1(() => { None }, [|value|]); @@ -48,7 +22,7 @@ let make = (~parameters) => { }; let on_submit = () => { - let newHistory = Array.append(history, [|(value, getLocalTime(), Executing)|]) + let newHistory = Array.append(history, [|(value, Time.getLocalTime(), Executing)|]) setHistory(_ => newHistory) // TODO transform param string with "' '" seperation mask @@ -101,7 +75,7 @@ let make = (~parameters) => { ) }; - let list_elements = map_history_entry_to_list_entry(history); + let list_elements = history |> map_history_entry_to_list_entry;
    diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re new file mode 100644 index 0000000..a635c6f --- /dev/null +++ b/src/utils/ParameterUtils.re @@ -0,0 +1,21 @@ +open State + +let concatParameters = (parameters) => { + parameters + |> String.split_on_char(' ') + |> List.map((s) => { String.sub(s, 1, String.length(s)-2)}) + |> String.concat(" ") +}; + +let getParameters = (state) => { + switch (Yojson.Safe.Util.member("command", state.meta)) { + | `String(command) => command + | _ => "" + } +}; + +let constructParameters = (parameters) => { + parameters + |> String.split_on_char(' ') + |> List.map((s) => "'" |> String.cat(s) |> String.cat("'")) +} \ No newline at end of file diff --git a/src/utils/Time.re b/src/utils/Time.re new file mode 100644 index 0000000..32d6fdb --- /dev/null +++ b/src/utils/Time.re @@ -0,0 +1,21 @@ +open Unix + +let timeToString = (time) => { + let rawMinutes = string_of_int(time.tm_min); + let minutes = if (String.length(rawMinutes) == 1) { + "0" + } else { + "" + } ++ rawMinutes; + + minutes + |> String.cat(":") + |> String.cat(string_of_int(time.tm_hour)) + |> String.cat(" "); +}; + +let getLocalTime = () => { + Unix.time() + |> Unix.localtime + |> timeToString; +}; \ No newline at end of file From 31b35bef04fd83fb9414d57d935e485428feca43 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 17 May 2023 22:09:30 +0200 Subject: [PATCH 16/48] Remove logging in Main.re --- src/Main.re | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/Main.re b/src/Main.re index a2ee231..860d29b 100644 --- a/src/Main.re +++ b/src/Main.re @@ -49,8 +49,6 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { ); let parameters = state |> ParameterUtils.getParameters; - Util.log(parameters); - let destructuredParameters = parameters |> ParameterUtils.concatParameters; let (history, setHistory) = React.useState(_ => [|(destructuredParameters, Time.getLocalTime(), ParameterView.Executed)|]); From 1d98255b31062f58844db0168859732d696a3973 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 17 May 2023 22:10:54 +0200 Subject: [PATCH 17/48] Fix Time.timeToString() not showing leading 0 in minute on clock --- src/utils/Time.re | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/utils/Time.re b/src/utils/Time.re index 32d6fdb..712447c 100644 --- a/src/utils/Time.re +++ b/src/utils/Time.re @@ -2,13 +2,9 @@ open Unix let timeToString = (time) => { let rawMinutes = string_of_int(time.tm_min); - let minutes = if (String.length(rawMinutes) == 1) { - "0" - } else { - "" - } ++ rawMinutes; - minutes + rawMinutes + |> String.cat(if (String.length(rawMinutes) == 1) { "0" } else { "" }) |> String.cat(":") |> String.cat(string_of_int(time.tm_hour)) |> String.cat(" "); From fb00202d38add3bb89024502b2aab33ba1784899 Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 29 May 2023 18:29:47 +0200 Subject: [PATCH 18/48] Impl requests for reruns via REST calls --- dune-project | 5 +++++ gobview.opam | 5 +++++ src/dune | 4 ++++ src/ui/panel/ParameterView.re | 34 ++++++++++++++++++++++++---------- 4 files changed, 38 insertions(+), 10 deletions(-) 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/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/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/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 2105ab7..6e9941d 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,8 +1,8 @@ -//open Lwt -//open Cohttp -//open Cohttp_lwt_unix -// TODO use above mentioned packages for http client to call goblint http server +open Lwt +open Cohttp +open Cohttp_lwt +module Client = Cohttp_lwt_jsoo.Client module ReactDOM = React.Dom type paramState = Executed | Executing | Canceled | Error; @@ -18,17 +18,31 @@ let make = (~parameters, ~history, ~setHistory) => { }, [|value|]); let on_change = (new_value) => { - setValue(_ => new_value) + setValue(_ => new_value); }; let on_submit = () => { let newHistory = Array.append(history, [|(value, Time.getLocalTime(), Executing)|]) - setHistory(_ => newHistory) - - // TODO transform param string with "' '" seperation mask - // TODO execute newly transformed params + setHistory(_ => newHistory); - // TODO use cohttp to call goblint server + let /*parameterList*/ _ = ParameterUtils.constructParameters(value); + let headers = Header.init_with("Content-Type", "application/json"); + let body = "{ + \"jsonrpc\": \"2.0\", + \"id\": \"5\", + \"method\": \"analyze\", + \"params\": {\"reset\": false} + }" + |> Body.of_string; + let url = "127.0.0.1:8001" |> Uri.of_string; + + let _ = Client.put(url, ~body=body, ~headers=headers) >>= ((res, _ /*body*/)) => { + res |> Response.status |> Code.code_of_status |> string_of_int |> Util.log; + /*body |> Body.to_string >|= (b) => { + Util.log(b); + };*/ + Lwt.return (); + }; setDisableCancel(_ => false); }; From c7c1fc044b10aca42ae19ae433caf172278afee2 Mon Sep 17 00:00:00 2001 From: sxprz Date: Tue, 30 May 2023 11:55:34 +0200 Subject: [PATCH 19/48] Impl correct success/error indication for rerun --- src/ui/panel/ParameterView.re | 63 ++++++++++++++++++++++++++++++----- 1 file changed, 54 insertions(+), 9 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 6e9941d..9111a98 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -7,6 +7,16 @@ 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"; + }; +}; + [@react.component] let make = (~parameters, ~history, ~setHistory) => { @@ -22,8 +32,15 @@ let make = (~parameters, ~history, ~setHistory) => { }; let on_submit = () => { - let newHistory = Array.append(history, [|(value, Time.getLocalTime(), Executing)|]) - setHistory(_ => newHistory); + history |> Array.length |> string_of_int |> Util.log; + + let time = Time.getLocalTime(); + let state = ref(Executing); + let element = (value, time, state.contents); + + let new_history = Array.append(history, [|element|]); + setHistory(_ => new_history); + setDisableCancel(_ => false); let /*parameterList*/ _ = ParameterUtils.constructParameters(value); let headers = Header.init_with("Content-Type", "application/json"); @@ -34,17 +51,45 @@ let make = (~parameters, ~history, ~setHistory) => { \"params\": {\"reset\": false} }" |> Body.of_string; - let url = "127.0.0.1:8001" |> Uri.of_string; - let _ = Client.put(url, ~body=body, ~headers=headers) >>= ((res, _ /*body*/)) => { - res |> Response.status |> Code.code_of_status |> string_of_int |> Util.log; + let scheme = "http"; + let host = "localhost"; + let port = 8080; + let path = "/api/analyze"; + + let uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, path) |> Uri.of_string; + + let new_state = Client.post(uri, ~body=body, ~headers=headers) >>= ((res, _ /*body*/)) => { + let code = res |> Response.status |> Code.code_of_status /*body |> Body.to_string >|= (b) => { Util.log(b); };*/ - Lwt.return (); + + if (code < 200 || code >= 400) { + Lwt.return(Error) + } else { + Lwt.return(Executed) + }; }; - setDisableCancel(_ => false); + let res_state = switch (new_state |> Lwt.poll) { + | Some(p) => p + | None => Error + }; + + let lastElemIndexInHistory = Array.length(new_history) - 1; + let lastElement = lastElemIndexInHistory |> Array.get(new_history); + + if (element == lastElement) { + let intermediateHistory = lastElemIndexInHistory |> Array.sub(new_history, 0); + + let new_element = (value, time, res_state); + + let new_history = Array.append(intermediateHistory, [|new_element|]); + setHistory(_ => new_history); + setDisableCancel(_ => true); + } + }; let on_cancel = () => { @@ -52,8 +97,8 @@ let make = (~parameters, ~history, ~setHistory) => { let (param, time, _) = Array.get(history, lastElemIndex); let intermediateHistory = Array.sub(history, 0, lastElemIndex); - let newHistory = Array.append(intermediateHistory, [|(param, time, Canceled)|]); - setHistory(_ => newHistory); + let new_history = Array.append(intermediateHistory, [|(param, time, Canceled)|]); + setHistory(_ => new_history); setDisableCancel(_ => true); } From f43193bedf58eaea214ca439b5256c0599be0ed9 Mon Sep 17 00:00:00 2001 From: sxprz Date: Tue, 30 May 2023 17:00:51 +0200 Subject: [PATCH 20/48] Refactor code --- src/ui/panel/ParameterView.re | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 9111a98..158f29b 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -38,7 +38,7 @@ let make = (~parameters, ~history, ~setHistory) => { let state = ref(Executing); let element = (value, time, state.contents); - let new_history = Array.append(history, [|element|]); + let new_history = [|element|] |> Array.append(history); setHistory(_ => new_history); setDisableCancel(_ => false); @@ -59,11 +59,8 @@ let make = (~parameters, ~history, ~setHistory) => { let uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, path) |> Uri.of_string; - let new_state = Client.post(uri, ~body=body, ~headers=headers) >>= ((res, _ /*body*/)) => { + let new_state = Client.post(uri, ~body=body, ~headers=headers) >>= ((res, _)) => { let code = res |> Response.status |> Code.code_of_status - /*body |> Body.to_string >|= (b) => { - Util.log(b); - };*/ if (code < 200 || code >= 400) { Lwt.return(Error) @@ -85,7 +82,7 @@ let make = (~parameters, ~history, ~setHistory) => { let new_element = (value, time, res_state); - let new_history = Array.append(intermediateHistory, [|new_element|]); + let new_history = [|new_element|] |> Array.append(intermediateHistory); setHistory(_ => new_history); setDisableCancel(_ => true); } From fd726fa4cefd25c5a95bcbd06211982b0903dd31 Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 5 Jun 2023 11:03:05 +0200 Subject: [PATCH 21/48] Fix CORS errors on API call; WIP on bad requests --- goblint-http-server/goblint_http.ml | 26 ++++++++++------ src/ui/panel/ParameterView.re | 48 +++++++++++++++++++---------- 2 files changed, 47 insertions(+), 27 deletions(-) diff --git a/goblint-http-server/goblint_http.ml b/goblint-http-server/goblint_http.ml index 78ebf5e..2302761 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,10 @@ let specs = let paths = ref [] +let cors_headers = Header.of_list [("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")] + let process state name body = match Hashtbl.find_option Api.registry name with | None -> Server.respond_not_found () @@ -31,24 +36,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) () + | exception Yojson_conv.Of_yojson_error (exn, json) -> + Server.respond_error ~headers:cors_headers ~status:`Bad_request ~body:(Printf.sprintf "Exception: %s\nJson:%s" (Printexc.to_string exn) (Yojson.Safe.pretty_to_string json)) () | 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 +107,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 +127,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 +148,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/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 158f29b..b7328ed 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -17,6 +17,18 @@ let paramState_to_string = (p: paramState) => { }; }; +let scheme = "http"; +let host = "127.0.0.1"; +let port = 8000; +let path = "/api/analyze"; + +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, ~history, ~setHistory) => { @@ -32,30 +44,32 @@ let make = (~parameters, ~history, ~setHistory) => { }; let on_submit = () => { - history |> Array.length |> string_of_int |> Util.log; - let time = Time.getLocalTime(); - let state = ref(Executing); - let element = (value, time, state.contents); + let element = (value, time, Executing); let new_history = [|element|] |> Array.append(history); setHistory(_ => new_history); setDisableCancel(_ => false); let /*parameterList*/ _ = ParameterUtils.constructParameters(value); - let headers = Header.init_with("Content-Type", "application/json"); - let body = "{ - \"jsonrpc\": \"2.0\", - \"id\": \"5\", - \"method\": \"analyze\", - \"params\": {\"reset\": false} - }" - |> Body.of_string; - - let scheme = "http"; - let host = "localhost"; - let port = 8080; - let path = "/api/analyze"; + + // TODO fix body to remove Yojson raised exceptions + /* "{ + \"jsonrpc\": \"2.0\", + \"id\": \"5\", + \"method\": \"analyze\", + \"params\": {\"reset\": false} + }" */ + + let body = `Assoc([ + ("jsonrpc", `String("2.0")), + ("id", `String("5")), + ("method", `String("analyze")), + ("params", `Assoc ([ + ("reset", `Bool (false)) + ]) + ) + ])|> Yojson.Basic.Util.to_string |> Body.of_string; let uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, path) |> Uri.of_string; From a1a75b495820fef13f02e4166d69c8a197b3a422 Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 5 Jun 2023 11:22:58 +0200 Subject: [PATCH 22/48] Fix for Yojson Type_error --- src/ui/panel/ParameterView.re | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index b7328ed..03b49eb 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -53,14 +53,6 @@ let make = (~parameters, ~history, ~setHistory) => { let /*parameterList*/ _ = ParameterUtils.constructParameters(value); - // TODO fix body to remove Yojson raised exceptions - /* "{ - \"jsonrpc\": \"2.0\", - \"id\": \"5\", - \"method\": \"analyze\", - \"params\": {\"reset\": false} - }" */ - let body = `Assoc([ ("jsonrpc", `String("2.0")), ("id", `String("5")), @@ -69,7 +61,7 @@ let make = (~parameters, ~history, ~setHistory) => { ("reset", `Bool (false)) ]) ) - ])|> Yojson.Basic.Util.to_string |> Body.of_string; + ])|> Yojson.Basic.to_string |> Body.of_string; let uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, path) |> Uri.of_string; From 3efbb87e5fcb621b99d14b1afe1817de834673d2 Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 5 Jun 2023 23:41:07 +0200 Subject: [PATCH 23/48] Fix errors and introduce tooltip in input WIP --- goblint-http-server/goblint_http.ml | 4 ++-- src/Main.re | 2 +- src/ui/panel/ParameterView.re | 29 +++++++++++++++++------------ src/utils/ParameterUtils.re | 10 ++++++---- src/utils/Time.re | 6 +++--- 5 files changed, 29 insertions(+), 22 deletions(-) diff --git a/goblint-http-server/goblint_http.ml b/goblint-http-server/goblint_http.ml index 2302761..8e24815 100644 --- a/goblint-http-server/goblint_http.ml +++ b/goblint-http-server/goblint_http.ml @@ -39,8 +39,8 @@ let process state name body = | 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, json) -> - Server.respond_error ~headers:cors_headers ~status:`Bad_request ~body:(Printf.sprintf "Exception: %s\nJson:%s" (Printexc.to_string exn) (Yojson.Safe.pretty_to_string json)) () + | exception Yojson_conv.Of_yojson_error (exn, _) -> + Server.respond_error ~headers:cors_headers ~status:`Bad_request ~body:(Printexc.to_string exn) () | body -> Lwt.catch (fun () -> diff --git a/src/Main.re b/src/Main.re index 860d29b..5242ff1 100644 --- a/src/Main.re +++ b/src/Main.re @@ -50,7 +50,7 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { let parameters = state |> ParameterUtils.getParameters; let destructuredParameters = parameters |> ParameterUtils.concatParameters; - let (history, setHistory) = React.useState(_ => [|(destructuredParameters, Time.getLocalTime(), ParameterView.Executed)|]); + let (history, setHistory) = React.useState(_ => [|(destructuredParameters, Time.get_local_time(), ParameterView.Executed)|]); React.useEffect1(() => { None diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 03b49eb..e38dd42 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -23,7 +23,7 @@ let port = 8000; let path = "/api/analyze"; let headers = [ - ("Content-Type", "application/json"), + ("Content-Type", "application/json-rpc"), ("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") @@ -44,24 +44,27 @@ let make = (~parameters, ~history, ~setHistory) => { }; let on_submit = () => { - let time = Time.getLocalTime(); + let time = Time.get_local_time(); let element = (value, time, Executing); let new_history = [|element|] |> Array.append(history); setHistory(_ => new_history); setDisableCancel(_ => false); - let /*parameterList*/ _ = ParameterUtils.constructParameters(value); + let /*(_, parameter_list)*/ _ = ParameterUtils.constructParameters(value); - let body = `Assoc([ - ("jsonrpc", `String("2.0")), - ("id", `String("5")), - ("method", `String("analyze")), - ("params", `Assoc ([ - ("reset", `Bool (false)) + let body = `List([ + //("jsonrpc", `String("2.0")), + //("id", `String("5")), + //("method", `String("analyze")), + /*("params", `Assoc ([ + //("reset", `Bool (false)) + ("Functions", `List ([])) // Either you give a list of functions to be reanalyzed or "All" functions will be re-evaluated ]) - ) - ])|> Yojson.Basic.to_string |> Body.of_string; + )*/ + `String ("Functions"), + `List ([`String ("main"), `String ("bsearch"), `String ("qsort")]) + ])|> Yojson.Safe.to_string |> Body.of_string; let uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, path) |> Uri.of_string; @@ -139,13 +142,15 @@ let make = (~parameters, ~history, ~setHistory) => { let list_elements = history |> map_history_entry_to_list_entry; + // TODO Show real goblint path in tooltip
    {playButton} - + +
    diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index a635c6f..2f89b3e 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -13,9 +13,11 @@ let getParameters = (state) => { | _ => "" } }; - + let constructParameters = (parameters) => { - parameters - |> String.split_on_char(' ') - |> List.map((s) => "'" |> String.cat(s) |> String.cat("'")) + let param_list = parameters + |> String.split_on_char(' ') + |> List.map((s) => "'" |> String.cat(s) |> String.cat("'")); + + (param_list |> List.hd, param_list) } \ No newline at end of file diff --git a/src/utils/Time.re b/src/utils/Time.re index 712447c..3dfe1b3 100644 --- a/src/utils/Time.re +++ b/src/utils/Time.re @@ -1,6 +1,6 @@ open Unix -let timeToString = (time) => { +let time_to_string = (time) => { let rawMinutes = string_of_int(time.tm_min); rawMinutes @@ -10,8 +10,8 @@ let timeToString = (time) => { |> String.cat(" "); }; -let getLocalTime = () => { +let get_local_time = () => { Unix.time() |> Unix.localtime - |> timeToString; + |> time_to_string; }; \ No newline at end of file From 9b96091bedd28f4c1ddc9e8e50737c162645901c Mon Sep 17 00:00:00 2001 From: sxprz Date: Tue, 6 Jun 2023 22:58:30 +0200 Subject: [PATCH 24/48] Introduce tooltip, refactor and WIP fix requests --- src/Main.re | 9 +++-- src/ui/panel/Panel.re | 4 +- src/ui/panel/ParameterView.re | 69 +++++++++++++++++++++++------------ src/utils/ParameterUtils.re | 50 ++++++++++++++++++++----- 4 files changed, 94 insertions(+), 38 deletions(-) diff --git a/src/Main.re b/src/Main.re index 5242ff1..a2cebf2 100644 --- a/src/Main.re +++ b/src/Main.re @@ -48,9 +48,10 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { [|state.display|], ); - let parameters = state |> ParameterUtils.getParameters; - let destructuredParameters = parameters |> ParameterUtils.concatParameters; - let (history, setHistory) = React.useState(_ => [|(destructuredParameters, Time.get_local_time(), ParameterView.Executed)|]); + let (goblint_path, parameters) = state |> ParameterUtils.get_parameters; + let destructured_params = parameters |> ParameterUtils.concat_parameter_list; + + let (history, setHistory) = React.useState(_ => [|(destructured_params, Time.get_local_time(), ParameterView.Executed)|]); React.useEffect1(() => { None @@ -74,7 +75,7 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { | None =>
    | Some(f) => }} - +
    { }; [@react.component] -let make = (~state, ~dispatch, ~parameters, ~history, ~setHistory) => { +let make = (~state, ~dispatch, ~goblint_path, ~parameters, ~history, ~setHistory) => { let locations = (state.goblint)#dead_locations; @@ -41,7 +41,7 @@ let make = (~state, ~dispatch, ~parameters, ~history, ~setHistory) => { | Some(Warnings) => | Some(DeadCode) => | Some(Statistics) => - | Some(Parameters) => + | Some(Parameters) => | _ => React.null }; diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index e38dd42..9a7e24e 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -20,17 +20,20 @@ let paramState_to_string = (p: paramState) => { let scheme = "http"; let host = "127.0.0.1"; let port = 8000; -let path = "/api/analyze"; +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-rpc"), + ("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, ~history, ~setHistory) => { +let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let (value, setValue) = React.useState(_ => parameters); let (disableCancel, setDisableCancel) = React.useState(_ => true); @@ -51,24 +54,24 @@ let make = (~parameters, ~history, ~setHistory) => { setHistory(_ => new_history); setDisableCancel(_ => false); - let /*(_, parameter_list)*/ _ = ParameterUtils.constructParameters(value); - - let body = `List([ - //("jsonrpc", `String("2.0")), - //("id", `String("5")), - //("method", `String("analyze")), - /*("params", `Assoc ([ - //("reset", `Bool (false)) - ("Functions", `List ([])) // Either you give a list of functions to be reanalyzed or "All" functions will be re-evaluated - ]) - )*/ + let parameter_list = + value + |> ParameterUtils.construct_parameters + |> ParameterUtils.tuples_from_parameters; + + // TODO create config body and request per created tuple in parameter_list + let config_body = + `Tuple (parameter_list |> List.map(s => `String (s))) // WIP, does not compile here + |> Yojson.Safe.to_string + |> Body.of_string; + + let analyze_body = `List([ `String ("Functions"), - `List ([`String ("main"), `String ("bsearch"), `String ("qsort")]) + `List ([]) ])|> Yojson.Safe.to_string |> Body.of_string; - let uri = Printf.sprintf("%s://%s:%d%s", scheme, host, port, path) |> Uri.of_string; - - let new_state = Client.post(uri, ~body=body, ~headers=headers) >>= ((res, _)) => { + // config endpoint + let config_res = Client.post(config_uri, ~body=/*config_body*/`Empty, ~headers=headers) >>= ((res, _)) => { let code = res |> Response.status |> Code.code_of_status if (code < 200 || code >= 400) { @@ -76,12 +79,32 @@ let make = (~parameters, ~history, ~setHistory) => { } else { Lwt.return(Executed) }; - }; + } - let res_state = switch (new_state |> Lwt.poll) { + let res_state = ref(switch (config_res |> Lwt.poll) { | Some(p) => p | None => Error - }; + }); + + if (res_state.contents != Error && res_state.contents != Canceled) { + + // analyze endpoint + let new_state = Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= ((res, _)) => { + let code = res |> Response.status |> Code.code_of_status + + if (code < 200 || code >= 400) { + Lwt.return(Error) + } else { + Lwt.return(Executed) + }; + }; + + res_state := switch (new_state |> Lwt.poll) { + | Some(p) => p + | None => Error + }; + + } let lastElemIndexInHistory = Array.length(new_history) - 1; let lastElement = lastElemIndexInHistory |> Array.get(new_history); @@ -89,7 +112,7 @@ let make = (~parameters, ~history, ~setHistory) => { if (element == lastElement) { let intermediateHistory = lastElemIndexInHistory |> Array.sub(new_history, 0); - let new_element = (value, time, res_state); + let new_element = (value, time, res_state.contents); let new_history = [|new_element|] |> Array.append(intermediateHistory); setHistory(_ => new_history); @@ -149,7 +172,7 @@ let make = (~parameters, ~history, ~setHistory) => { - +
    diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index 2f89b3e..4a29888 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -1,23 +1,55 @@ open State -let concatParameters = (parameters) => { +let concat_parameters = (parameters) => { parameters |> String.split_on_char(' ') |> List.map((s) => { String.sub(s, 1, String.length(s)-2)}) |> String.concat(" ") }; -let getParameters = (state) => { - switch (Yojson.Safe.Util.member("command", state.meta)) { +let concat_parameter_list = String.concat(" "); + +let get_parameters = (state) => { + let raw_params = 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)}); + + (raw_params |> List.hd, raw_params |> List.tl) }; -let constructParameters = (parameters) => { - let param_list = parameters - |> String.split_on_char(' ') - |> List.map((s) => "'" |> String.cat(s) |> String.cat("'")); - - (param_list |> List.hd, param_list) +let construct_parameters = (parameters) => { + parameters + |> String.split_on_char(' ') + //|> List.map((s) => /*"'" |> String.cat(*/s/*) |> String.cat("'")*/) +} + +// TODO combine --set and the following
    • } - ) + ); }; let list_elements = history |> map_history_entry_to_list_entry; - // TODO Show real goblint path in tooltip
    {playButton} - - + +
    -
    - {"History" |> React.string} -
    -
    +
      {
    1. diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index 4a29888..86e05df 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -20,15 +20,9 @@ let get_parameters = (state) => { (raw_params |> List.hd, raw_params |> List.tl) }; -let construct_parameters = (parameters) => { - parameters - |> String.split_on_char(' ') - //|> List.map((s) => /*"'" |> String.cat(*/s/*) |> String.cat("'")*/) -} +let construct_parameters = (parameters) => parameters |> String.split_on_char(' ');//|> List.map((s) => "'" |> String.cat(s) |> String.cat("'")) -// TODO combine --set and the following
    2. + {
    3. @@ -166,14 +196,14 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }}
      -
      // TODO fix margin between icon and text +
      - {time |> React.string} + {time ++ " " |> React.string}
      {parameter_grouping |> List.mapi((j,e) => { - {e |> React.string} + {e |> React.string} }) |> React.list}
      @@ -184,6 +214,12 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let list_elements = history |> map_history_entry_to_list_entry; + let icon_for_sort_dir = if (sortDesc) { + + } else { + + }; +
      {playButton} @@ -200,10 +236,11 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => {
      - {"Status" |> React.string} + {"Status" |> React.string}
      - {"Time" |> React.string} + {"Time " |> React.string} + {icon_for_sort_dir}
      {"Parameters" |> React.string} From 1347bec6900149436ed6e119c96c8ae8c7ce564b Mon Sep 17 00:00:00 2001 From: sxprz Date: Tue, 13 Jun 2023 23:38:03 +0200 Subject: [PATCH 27/48] Fix API calls WIP, not compilable due to let%lwt --- src/dune | 2 +- src/ui/panel/ParameterView.re | 94 ++++++++++++++++------------------- src/utils/ParameterUtils.re | 1 + 3 files changed, 46 insertions(+), 51 deletions(-) diff --git a/src/dune b/src/dune index beb8aeb..b5ba254 100644 --- a/src/dune +++ b/src/dune @@ -35,7 +35,7 @@ react-requires.js static-requires.js)) (preprocess - (pps gen_js_api.ppx js_of_ocaml-ppx jsoo-react.ppx))) + (pps gen_js_api.ppx js_of_ocaml-ppx lwt_ppx jsoo-react.ppx))) (rule (targets Graphviz.ml) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 824371c..8519671 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -2,6 +2,8 @@ open Lwt open Cohttp open Cohttp_lwt +module Lwt_js = Js_of_ocaml_lwt.Lwt_js +module Lwt_js_events = Js_of_ocaml_lwt.Lwt_js_events module Client = Cohttp_lwt_jsoo.Client module ReactDOM = React.Dom @@ -17,9 +19,7 @@ let paramState_to_string = (p: paramState) => { }; }; -let is_successful = (p: paramState) => { - p == Executed -}; +let is_successful = (p: paramState) => p == Executed; let scheme = "http"; let host = "127.0.0.1"; @@ -67,7 +67,8 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let parameter_list = value |> ParameterUtils.construct_parameters - |> ParameterUtils.group_parameters; + |> ParameterUtils.group_parameters + |> List.filter(s => !(String.starts_with(~prefix="server.", s))) // TODO in whitelist: Don't allow server modifications; let time = Time.get_local_time(); let element = (parameter_list, time, Executing); @@ -81,63 +82,55 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { setHistory(_ => new_history); setDisableCancel(_ => false); - let res_state = Error |> ref; - - let config_res_states = - parameter_list - |> ParameterUtils.tuples_from_parameters - |> List.map(((a,b)) => { - - let config_body = - `List([`String(a), `String(b)]) - |> Yojson.Safe.to_string - |> Body.of_string; - - // config endpoint - let config_res = Client.post(config_uri, ~body=config_body, ~headers=headers) >>= ((res, _)) => { - let code = res |> Response.status |> Code.code_of_status; - - if (code < 200 || code >= 400) { - Lwt.return(Error); - } else { - Lwt.return(Executed); - }; - }; - - switch (config_res |> Lwt.poll) { - | Some(p) => p - | None => Error - } - - }) - |> List.map(is_successful) - |> List.fold_left((a,b) => a && b, true); + + // TODO remove preliminary body and replace with actual params + let config_body = + `List([`String("files[+]"), `String("")]) + |> Yojson.Safe.to_string + |> Body.of_string; + + // config endpoint + let config_req () = Client.post(config_uri, ~body=config_body, ~headers=headers) >>= ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; + let _ = Body.drain_body(body); + + if (code < 200 || code >= 400) { + Lwt.return(Error); + } else { + Lwt.return(Executed); + }; + }; // Body indicates full reanalysis because of empty list - let analyze_body = `List([ - `String ("Functions"), - `List ([]) - ])|> Yojson.Safe.to_string |> Body.of_string; + /*let analyze_body = + `List([`String ("Functions"), `List ([])]) + |> Yojson.Safe.to_string + |> Body.of_string;*/ + + // analyze endpoint + /*let analyze_req (state) = Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= ((res, body)) => { + let p = switch (state |> Lwt.state) { + | Lwt.Return(Executed) => Executed + | _ => Error + }; - if (config_res_states) { + if (p == Executed) { - // analyze endpoint - let new_state = Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= ((res, _)) => { let code = res |> Response.status |> Code.code_of_status + let _ = Body.drain_body(body); if (code < 200 || code >= 400) { Lwt.return(Error) } else { Lwt.return(Executed) }; - }; - res_state := switch (new_state |> Lwt.poll) { - | Some(p) => p - | None => Error - }; + } else { + Lwt.return(Error); + } + };*/ - } + let%lwt res = config_req()/* >>= analyze_req*/; let lastIndex = Array.length(new_history) - 1; // This tuple is used to calculate where to update the last added history/parameter element @@ -152,17 +145,18 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { if (pickedElem == element) { let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); - let new_element = (parameter_list, time, res_state.contents); + let new_element = (parameter_list, time, res); let new_history = if (sortDesc) { intermediateHistory |> Array.append([|new_element|]) } else { [|new_element|] |> Array.append(intermediateHistory) }; + setHistory(_ => new_history); setDisableCancel(_ => true); } - + }; // This cancel function will be commented out as the feature is not implemented yet, but the option for it is there. diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index 86e05df..fc015b0 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -86,4 +86,5 @@ let tuples_from_parameters = (parameters) => { }) |> List.filter(e => e != None) |> List.map(e => e |> Option.get) + |> List.filter(((k,_)) => !(String.starts_with(~prefix="server.", k))) // Don't allow server modifications }; \ No newline at end of file From d271f268aab7625bcb10e49991947195af9c05dd Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 14 Jun 2023 22:01:22 +0200 Subject: [PATCH 28/48] Impl working config endpoint, analyze WIP --- src/Main.re | 12 ++- src/ui/panel/ParameterView.re | 135 ++++++++++++++++++++++++++++------ src/utils/ParameterUtils.re | 2 +- 3 files changed, 126 insertions(+), 23 deletions(-) diff --git a/src/Main.re b/src/Main.re index 6810d83..af2096b 100644 --- a/src/Main.re +++ b/src/Main.re @@ -49,7 +49,17 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { ); let (goblint_path, parameters) = state |> ParameterUtils.get_parameters; - let destructured_params = parameters |> ParameterUtils.group_parameters; + let destructured_params = + parameters + |> ParameterUtils.group_parameters + |> List.filter(s => { + let regex = Str.regexp_string("server."); + + switch (Str.search_forward(regex, s, 0)) { + | exception Not_found => true; + | _ => false; + } + }); let (history, setHistory) = React.useState(_ => [|(destructured_params, Time.get_local_time(), ParameterView.Executed)|]); diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 8519671..6e92430 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -2,8 +2,6 @@ open Lwt open Cohttp open Cohttp_lwt -module Lwt_js = Js_of_ocaml_lwt.Lwt_js -module Lwt_js_events = Js_of_ocaml_lwt.Lwt_js_events module Client = Cohttp_lwt_jsoo.Client module ReactDOM = React.Dom @@ -68,8 +66,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { value |> ParameterUtils.construct_parameters |> ParameterUtils.group_parameters - |> List.filter(s => !(String.starts_with(~prefix="server.", s))) // TODO in whitelist: Don't allow server modifications; - + let time = Time.get_local_time(); let element = (parameter_list, time, Executing); @@ -82,25 +79,98 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { setHistory(_ => new_history); setDisableCancel(_ => false); - - // TODO remove preliminary body and replace with actual params - let config_body = - `List([`String("files[+]"), `String("")]) - |> Yojson.Safe.to_string - |> Body.of_string; + let modify_history = (result: paramState): unit => { + let lastIndex = Array.length(new_history) - 1; + // This tuple is used to calculate where to update the last added history/parameter element + let (index, startIndex, endIndex) = if (sortDesc) { + (0, 1, lastIndex) + } else { + (lastIndex, 0, lastIndex) + }; + + let pickedElem = index |> Array.get(new_history); + + if (pickedElem == element) { + let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); + + let new_element = (parameter_list, time, result); + + let new_history = if (sortDesc) { + intermediateHistory |> Array.append([|new_element|]) + } else { + [|new_element|] |> Array.append(intermediateHistory) + }; + + setHistory(_ => new_history); + setDisableCancel(_ => true); + } + } // config endpoint - let config_req () = Client.post(config_uri, ~body=config_body, ~headers=headers) >>= ((res, body)) => { - let code = res |> Response.status |> Code.code_of_status; - let _ = Body.drain_body(body); + /*let inner_config_api_call = (): Lwt.t(paramState) => { + let (promise, resolver) = Lwt.task(); + let config_req = Js.wrap_callback(() => { + Client.post(config_uri, ~body=config_body, ~headers=headers) >>= + ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; + let _ = Body.drain_body(body); + + if (code < 200 || code >= 400) { + Lwt.return(Error); + } else { + Lwt.return(Executed); + }; + }} + ); + let wakeup_call_promise = Js.wrap_callback((p: paramState) => Lwt.wakeup(resolver, p)); + + let promise_from_js = Js.Unsafe.fun_call(config_req, [||]); + let () = ignore @@ promise_from_js##then_(wakeup_call_promise); + promise + };*/ - if (code < 200 || code >= 400) { - Lwt.return(Error); - } else { - Lwt.return(Executed); + let inner_config_api_call = (config_body): Lwt.t(paramState) => { + Client.post(config_uri, ~body=config_body, ~headers=headers) >>= + ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; + let _ = Body.drain_body(body); + + if (code < 200 || code >= 400) { + Lwt.return(Error); + } else { + Lwt.return(Executed); + }; }; }; + let config_api_call = (config_opts: list((string, string))) => { + config_opts + |> List.map(((k,v)) => { + `List([`String(k), `String(v)]) + |> Yojson.Safe.to_string + |> Body.of_string; + }) + |> List.map(inner_config_api_call) + |> Lwt.npick; + }; + + let analyze_api_call = () => { + let config_opts = parameter_list |> ParameterUtils.tuples_from_parameters; + + config_opts |> config_api_call >>= (result) => { + + let result_state = result + |> List.map(is_successful) + |> List.fold_left((a,b) => a && b, true); + + // TODO analyze call + modify_history(if (result_state) { Executed } else { Error }); + Lwt.return(); + } + } + + let () = analyze_api_call() |> ignore + // Body indicates full reanalysis because of empty list /*let analyze_body = `List([`String ("Functions"), `List ([])]) @@ -130,9 +200,32 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { } };*/ - let%lwt res = config_req()/* >>= analyze_req*/; + /*let eval_config_req = Js.wrap_callback (() => { + Lwt_js.sleep(3.) >>= () => config_req//() => { + //let _ = Lwt_js.sleep(3.); + //Lwt.return(res) + /*switch (config_req |> Lwt.state) { + | Lwt.Return(o) => o + | Lwt.Sleep => Executing + | _ => Error + }}*/ + //} + }); + + let res = Js.Unsafe.fun_call(eval_config_req, [| /*Js.Unsafe.inject Js.undefined*/ |]); + res |> paramState_to_string |> Util.log*/ + + //let%lwt res = config_req()/* >>= analyze_req*/; + /*let res = + switch (ClientApi.resolve_promise(config_req)) |> Lwt.state) { + | Lwt.Return(Executed) => Executed + | Lwt.Sleep => Executing + | _ => Error + }*/ - let lastIndex = Array.length(new_history) - 1; + // TODO restore code if needed, all from below + + /*let lastIndex = Array.length(new_history) - 1; // This tuple is used to calculate where to update the last added history/parameter element let (index, startIndex, endIndex) = if (sortDesc) { (0, 1, lastIndex) @@ -145,7 +238,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { if (pickedElem == element) { let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); - let new_element = (parameter_list, time, res); + let new_element = (parameter_list, time, res.contents); let new_history = if (sortDesc) { intermediateHistory |> Array.append([|new_element|]) @@ -155,7 +248,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { setHistory(_ => new_history); setDisableCancel(_ => true); - } + }*/ }; diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index fc015b0..2b9c146 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -22,7 +22,7 @@ let get_parameters = (state) => { let construct_parameters = (parameters) => parameters |> String.split_on_char(' ');//|> List.map((s) => "'" |> String.cat(s) |> String.cat("'")) -let rec group_parameters = (parameters) => { +let rec group_parameters = (parameters: list(string)): list(string) => { if (parameters |> List.length > 0) { let (command, tail) = (parameters |> List.hd, parameters |> List.tl); From eb52852197f45878b239b7060bdc6eb9c4e5d282 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 14 Jun 2023 22:16:22 +0200 Subject: [PATCH 29/48] Remove lwt_ppx usage and unused code --- src/dune | 2 +- src/ui/panel/ParameterView.re | 141 ++++++++-------------------------- 2 files changed, 35 insertions(+), 108 deletions(-) diff --git a/src/dune b/src/dune index b5ba254..beb8aeb 100644 --- a/src/dune +++ b/src/dune @@ -35,7 +35,7 @@ react-requires.js static-requires.js)) (preprocess - (pps gen_js_api.ppx js_of_ocaml-ppx lwt_ppx jsoo-react.ppx))) + (pps gen_js_api.ppx js_of_ocaml-ppx jsoo-react.ppx))) (rule (targets Graphviz.ml) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 6e92430..7461f2b 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -106,29 +106,6 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { } } - // config endpoint - /*let inner_config_api_call = (): Lwt.t(paramState) => { - let (promise, resolver) = Lwt.task(); - let config_req = Js.wrap_callback(() => { - Client.post(config_uri, ~body=config_body, ~headers=headers) >>= - ((res, body)) => { - let code = res |> Response.status |> Code.code_of_status; - let _ = Body.drain_body(body); - - if (code < 200 || code >= 400) { - Lwt.return(Error); - } else { - Lwt.return(Executed); - }; - }} - ); - let wakeup_call_promise = Js.wrap_callback((p: paramState) => Lwt.wakeup(resolver, p)); - - let promise_from_js = Js.Unsafe.fun_call(config_req, [||]); - let () = ignore @@ promise_from_js##then_(wakeup_call_promise); - promise - };*/ - let inner_config_api_call = (config_body): Lwt.t(paramState) => { Client.post(config_uri, ~body=config_body, ~headers=headers) >>= ((res, body)) => { @@ -154,101 +131,51 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { |> Lwt.npick; }; - let analyze_api_call = () => { - let config_opts = parameter_list |> ParameterUtils.tuples_from_parameters; - - config_opts |> config_api_call >>= (result) => { - - let result_state = result - |> List.map(is_successful) - |> List.fold_left((a,b) => a && b, true); - - // TODO analyze call - modify_history(if (result_state) { Executed } else { Error }); - Lwt.return(); - } - } - - let () = analyze_api_call() |> ignore - - // Body indicates full reanalysis because of empty list - /*let analyze_body = - `List([`String ("Functions"), `List ([])]) - |> Yojson.Safe.to_string - |> Body.of_string;*/ - - // analyze endpoint - /*let analyze_req (state) = Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= ((res, body)) => { - let p = switch (state |> Lwt.state) { - | Lwt.Return(Executed) => Executed - | _ => Error - }; - - if (p == Executed) { - - let code = res |> Response.status |> Code.code_of_status + let inner_analyze_api_call = (analyze_body): Lwt.t(paramState) => { + Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= + ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; let _ = Body.drain_body(body); if (code < 200 || code >= 400) { - Lwt.return(Error) + Lwt.return(Error); } else { - Lwt.return(Executed) + Lwt.return(Executed); }; - - } else { - Lwt.return(Error); - } - };*/ - - /*let eval_config_req = Js.wrap_callback (() => { - Lwt_js.sleep(3.) >>= () => config_req//() => { - //let _ = Lwt_js.sleep(3.); - //Lwt.return(res) - /*switch (config_req |> Lwt.state) { - | Lwt.Return(o) => o - | Lwt.Sleep => Executing - | _ => Error - }}*/ - //} - }); - - let res = Js.Unsafe.fun_call(eval_config_req, [| /*Js.Unsafe.inject Js.undefined*/ |]); - res |> paramState_to_string |> Util.log*/ - - //let%lwt res = config_req()/* >>= analyze_req*/; - /*let res = - switch (ClientApi.resolve_promise(config_req)) |> Lwt.state) { - | Lwt.Return(Executed) => Executed - | Lwt.Sleep => Executing - | _ => Error - }*/ - - // TODO restore code if needed, all from below - - /*let lastIndex = Array.length(new_history) - 1; - // This tuple is used to calculate where to update the last added history/parameter element - let (index, startIndex, endIndex) = if (sortDesc) { - (0, 1, lastIndex) - } else { - (lastIndex, 0, lastIndex) + }; }; - let pickedElem = index |> Array.get(new_history); - - if (pickedElem == element) { - let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); + let analyze_body = + `List([`String ("Functions"), `List ([])]) + |> Yojson.Safe.to_string + |> Body.of_string; - let new_element = (parameter_list, time, res.contents); + let analyze_api_call = () => { + let config_opts = parameter_list |> ParameterUtils.tuples_from_parameters; - let new_history = if (sortDesc) { - intermediateHistory |> Array.append([|new_element|]) - } else { - [|new_element|] |> Array.append(intermediateHistory) + config_opts + |> config_api_call >>= + (result) => { + let result_state = result + |> List.map(is_successful) + |> List.fold_left((a,b) => a && b, true) + |> ((s) => if (s) { Executed } else { Error }); + + Lwt.return(result_state); + } >>= + (result) => { + switch result { + | Executed => inner_analyze_api_call(analyze_body); + | _ => Lwt.return(Error); + } + } >>= + (result) => { + modify_history(result); + Lwt.return() }; + }; - setHistory(_ => new_history); - setDisableCancel(_ => true); - }*/ + let () = analyze_api_call() |> ignore; }; From d9d028231ecb012b0d083b11ce619ca786097f3b Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 14 Jun 2023 22:41:19 +0200 Subject: [PATCH 30/48] Use other icon for history orientation --- src/ui/icons/IconArrowDown.re | 6 ++++++ src/ui/icons/IconArrowUp.re | 6 ++++++ src/ui/icons/IconCaretDownFilled.re | 6 ------ src/ui/icons/IconCaretUpFilled.re | 6 ------ src/ui/panel/ParameterView.re | 4 ++-- 5 files changed, 14 insertions(+), 14 deletions(-) create mode 100644 src/ui/icons/IconArrowDown.re create mode 100644 src/ui/icons/IconArrowUp.re delete mode 100644 src/ui/icons/IconCaretDownFilled.re delete mode 100644 src/ui/icons/IconCaretUpFilled.re diff --git a/src/ui/icons/IconArrowDown.re b/src/ui/icons/IconArrowDown.re new file mode 100644 index 0000000..2f5766d --- /dev/null +++ b/src/ui/icons/IconArrowDown.re @@ -0,0 +1,6 @@ +[@react.component] +let make = (~on_click) => { + + + +} \ 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..296c3d4 --- /dev/null +++ b/src/ui/icons/IconArrowUp.re @@ -0,0 +1,6 @@ +[@react.component] +let make = (~on_click) => { + + + +} \ No newline at end of file diff --git a/src/ui/icons/IconCaretDownFilled.re b/src/ui/icons/IconCaretDownFilled.re deleted file mode 100644 index 7f5f224..0000000 --- a/src/ui/icons/IconCaretDownFilled.re +++ /dev/null @@ -1,6 +0,0 @@ -[@react.component] -let make = (~on_click) => { - - - -} \ No newline at end of file diff --git a/src/ui/icons/IconCaretUpFilled.re b/src/ui/icons/IconCaretUpFilled.re deleted file mode 100644 index 4599ddb..0000000 --- a/src/ui/icons/IconCaretUpFilled.re +++ /dev/null @@ -1,6 +0,0 @@ -[@react.component] -let make = (~on_click) => { - - - -} \ No newline at end of file diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 7461f2b..f378993 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -229,9 +229,9 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let list_elements = history |> map_history_entry_to_list_entry; let icon_for_sort_dir = if (sortDesc) { - + } else { - + };
      From 262f184553182f19c80e6b0f2efe6b6b1a1b930b Mon Sep 17 00:00:00 2001 From: sxprz Date: Thu, 15 Jun 2023 10:54:23 +0200 Subject: [PATCH 31/48] Add input validation for server opts, UI WIP --- src/ui/panel/ParameterView.re | 48 +++++++++++++++++++++++++++-------- 1 file changed, 37 insertions(+), 11 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index f378993..83a1fa7 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -40,8 +40,11 @@ let rev_arr = (array) => array |> Array.to_list |> List.rev |> Array.of_list; let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let (value, setValue) = React.useState(_ => parameters |> ParameterUtils.concat_parameter_list); - let (disableCancel, setDisableCancel) = React.useState(_ => true); + // Linked to cancelation, see reasons below for why it is commented out + //let (disableCancel, setDisableCancel) = React.useState(_ => true); + let (disableRun, setDisableRun) = React.useState(_ => false); let (sortDesc, setSortDesc) = React.useState(_ => true); + let (hasServerOpts, setHasServerOpts) = React.useState(_ => false); React.useEffect1(() => { None @@ -57,7 +60,16 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { setSortDesc(_ => !sortDesc); } + let on_change = (new_value) => { + let server_opt_regex = Str.regexp_string("server."); + let server_opts_found = switch (Str.search_forward(server_opt_regex, new_value, 0)) { + | exception Not_found => false; + | _ => true + } + setHasServerOpts(_ => server_opts_found); + setDisableRun(_ => server_opts_found); + setValue(_ => new_value); }; @@ -77,7 +89,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; setHistory(_ => new_history); - setDisableCancel(_ => false); + //setDisableCancel(_ => false); let modify_history = (result: paramState): unit => { let lastIndex = Array.length(new_history) - 1; @@ -102,7 +114,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; setHistory(_ => new_history); - setDisableCancel(_ => true); + //setDisableCancel(_ => true); } } @@ -179,8 +191,8 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; - // This cancel function will be commented out as the feature is not implemented yet, but the option for it is there. - let on_cancel = () => { + // This cancel function is here in case it will be implemented in the http-server, not far fetched. + /*let on_cancel = () => { let lastElemIndex = Array.length(history) - 1; let (param, time, _) = Array.get(history, lastElemIndex); @@ -189,9 +201,9 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { setHistory(_ => new_history); setDisableCancel(_ => true); - }; + };*/ - let playButton = ; @@ -234,15 +246,29 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; + let input = switch hasServerOpts { + | true => { +
      + +
      + {"Server options are not allowed" |> React.string} +
      +
      + }; + | _ => ; + }; +
      -
      +
      {playButton} - + */ - + {input}
      +
        From 2e6c6b71225d0628f3022b85aec2ef51dd268f04 Mon Sep 17 00:00:00 2001 From: sxprz Date: Thu, 15 Jun 2023 21:56:32 +0200 Subject: [PATCH 32/48] Improve UI design for validation --- src/ui/panel/ParameterView.re | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 83a1fa7..dad3835 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -229,7 +229,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => {
      {parameter_grouping |> List.mapi((j,e) => { - {e |> React.string} + {e |> React.string} }) |> React.list}
      @@ -250,7 +250,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { | true => {
      -
      +
      {"Server options are not allowed" |> React.string}
      From 5b3c8594d824b793838f24711eb49caa56b681aa Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 19 Jun 2023 20:33:12 +0200 Subject: [PATCH 33/48] Add fully functioning validation for server opts --- src/ui/base/input.re | 5 +- src/ui/panel/ParameterView.re | 224 +++++++++++++++++----------------- 2 files changed, 117 insertions(+), 112 deletions(-) diff --git a/src/ui/base/input.re b/src/ui/base/input.re index 50f18b6..6f743f6 100644 --- a/src/ui/base/input.re +++ b/src/ui/base/input.re @@ -1,9 +1,10 @@ [@react.component] -let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?) => { +let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?, ~style=?) => { 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 type_ = switch (type_) { @@ -25,5 +26,5 @@ let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?) => { Option.iter(cb => cb(), on_submit); }; - ; + ; }; diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index dad3835..cceb015 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -74,121 +74,123 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; let on_submit = () => { - let parameter_list = - value - |> ParameterUtils.construct_parameters - |> ParameterUtils.group_parameters - - let time = Time.get_local_time(); - let element = (parameter_list, time, Executing); - - let new_history = if (sortDesc) { - history |> Array.append([|element|]) - } else { - [|element|] |> Array.append(history) - }; - - setHistory(_ => new_history); - //setDisableCancel(_ => false); - - let modify_history = (result: paramState): unit => { - let lastIndex = Array.length(new_history) - 1; - // This tuple is used to calculate where to update the last added history/parameter element - let (index, startIndex, endIndex) = if (sortDesc) { - (0, 1, lastIndex) + if (!hasServerOpts) { + let parameter_list = + value + |> ParameterUtils.construct_parameters + |> ParameterUtils.group_parameters + + let time = Time.get_local_time(); + let element = (parameter_list, time, Executing); + + let new_history = if (sortDesc) { + history |> Array.append([|element|]) } else { - (lastIndex, 0, lastIndex) + [|element|] |> Array.append(history) }; - let pickedElem = index |> Array.get(new_history); - - if (pickedElem == element) { - let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); + setHistory(_ => new_history); + //setDisableCancel(_ => false); - let new_element = (parameter_list, time, result); - - let new_history = if (sortDesc) { - intermediateHistory |> Array.append([|new_element|]) + let modify_history = (result: paramState): unit => { + let lastIndex = Array.length(new_history) - 1; + // This tuple is used to calculate where to update the last added history/parameter element + let (index, startIndex, endIndex) = if (sortDesc) { + (0, 1, lastIndex) } else { - [|new_element|] |> Array.append(intermediateHistory) + (lastIndex, 0, lastIndex) }; - setHistory(_ => new_history); - //setDisableCancel(_ => true); + let pickedElem = index |> Array.get(new_history); + + if (pickedElem == element) { + let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); + + let new_element = (parameter_list, time, result); + + let new_history = if (sortDesc) { + intermediateHistory |> Array.append([|new_element|]) + } else { + [|new_element|] |> Array.append(intermediateHistory) + }; + + setHistory(_ => new_history); + //setDisableCancel(_ => true); + } } - } - let inner_config_api_call = (config_body): Lwt.t(paramState) => { - Client.post(config_uri, ~body=config_body, ~headers=headers) >>= - ((res, body)) => { - let code = res |> Response.status |> Code.code_of_status; - let _ = Body.drain_body(body); + let inner_config_api_call = (config_body): Lwt.t(paramState) => { + Client.post(config_uri, ~body=config_body, ~headers=headers) >>= + ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; + let _ = Body.drain_body(body); + + if (code < 200 || code >= 400) { + Lwt.return(Error); + } else { + Lwt.return(Executed); + }; + }; + }; - if (code < 200 || code >= 400) { - Lwt.return(Error); - } else { - Lwt.return(Executed); + let config_api_call = (config_opts: list((string, string))) => { + config_opts + |> List.map(((k,v)) => { + `List([`String(k), `String(v)]) + |> Yojson.Safe.to_string + |> Body.of_string; + }) + |> List.map(inner_config_api_call) + |> Lwt.npick; + }; + + let inner_analyze_api_call = (analyze_body): Lwt.t(paramState) => { + Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= + ((res, body)) => { + let code = res |> Response.status |> Code.code_of_status; + let _ = Body.drain_body(body); + + if (code < 200 || code >= 400) { + Lwt.return(Error); + } else { + Lwt.return(Executed); + }; }; }; - }; - let config_api_call = (config_opts: list((string, string))) => { - config_opts - |> List.map(((k,v)) => { - `List([`String(k), `String(v)]) + let analyze_body = + `List([`String ("Functions"), `List ([])]) |> Yojson.Safe.to_string |> Body.of_string; - }) - |> List.map(inner_config_api_call) - |> Lwt.npick; - }; - - let inner_analyze_api_call = (analyze_body): Lwt.t(paramState) => { - Client.post(analyze_uri, ~body=analyze_body, ~headers=headers) >>= - ((res, body)) => { - let code = res |> Response.status |> Code.code_of_status; - let _ = Body.drain_body(body); - - if (code < 200 || code >= 400) { - Lwt.return(Error); - } else { - Lwt.return(Executed); + + let analyze_api_call = () => { + let config_opts = parameter_list |> ParameterUtils.tuples_from_parameters; + + config_opts + |> config_api_call >>= + (result) => { + let result_state = result + |> List.map(is_successful) + |> List.fold_left((a,b) => a && b, true) + |> ((s) => if (s) { Executed } else { Error }); + + Lwt.return(result_state); + } >>= + (result) => { + switch result { + | Executed => inner_analyze_api_call(analyze_body); + | _ => Lwt.return(Error); + } + } >>= + (result) => { + modify_history(result); + Lwt.return() }; }; - }; - - let analyze_body = - `List([`String ("Functions"), `List ([])]) - |> Yojson.Safe.to_string - |> Body.of_string; - - let analyze_api_call = () => { - let config_opts = parameter_list |> ParameterUtils.tuples_from_parameters; - - config_opts - |> config_api_call >>= - (result) => { - let result_state = result - |> List.map(is_successful) - |> List.fold_left((a,b) => a && b, true) - |> ((s) => if (s) { Executed } else { Error }); - - Lwt.return(result_state); - } >>= - (result) => { - switch result { - | Executed => inner_analyze_api_call(analyze_body); - | _ => Lwt.return(Error); - } - } >>= - (result) => { - modify_history(result); - Lwt.return() - }; - }; - - let () = analyze_api_call() |> ignore; + let () = analyze_api_call() |> ignore; + + } }; // This cancel function is here in case it will be implemented in the http-server, not far fetched. @@ -246,27 +248,29 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; - let input = switch hasServerOpts { - | true => { -
      - -
      - {"Server options are not allowed" |> React.string} -
      -
      - }; - | _ => ; - }; -
      {playButton} + // Commented out because http server does not support cancelation yet /**/ + - {input} + // Input and tooltip are seperated due to display issues + {switch hasServerOpts { + | true => + | false => ; + }} + {switch hasServerOpts { + | true => { +
      + {"Server options are not allowed" |> React.string} +
      + }; + | _ => React.null; + }}
      From 4c19464ad3323dd090af4f798a6f01b002506edb Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 19 Jun 2023 20:34:17 +0200 Subject: [PATCH 34/48] Add bootstrap autocomplete library --- package-lock.json | 21 +++++++++++++++++++++ package.json | 1 + src/bindings/autocompleteBS.mli | 8 ++++++++ src/bindings/dune | 6 ++++++ src/static-requires.js | 3 +++ src/ui/panel/ParameterView.re | 1 + 6 files changed, 40 insertions(+) create mode 100644 src/bindings/autocompleteBS.mli diff --git a/package-lock.json b/package-lock.json index 0566ac3..5709761 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", @@ -737,6 +738,16 @@ "@popperjs/core": "^2.9.2" } }, + "node_modules/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==" + }, + "node_modules/bootstrap5-autocomplete": { + "version": "1.1.14", + "resolved": "https://registry.npmjs.org/bootstrap5-autocomplete/-/bootstrap5-autocomplete-1.1.14.tgz", + "integrity": "sha512-QNV/aqW52tbdniydK3r9tibnvcs90schqHLKJH7ZnI1iGV19KalrdAYFsg6Z8eUSyKLZHiFh7v7IQOWL1qvk6g==" + }, "node_modules/brace-expansion": { "version": "1.1.11", "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz", @@ -7695,6 +7706,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/package.json b/package.json index b8a0858..51fde2d 100644 --- a/package.json +++ b/package.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", diff --git a/src/bindings/autocompleteBS.mli b/src/bindings/autocompleteBS.mli new file mode 100644 index 0000000..9fa0689 --- /dev/null +++ b/src/bindings/autocompleteBS.mli @@ -0,0 +1,8 @@ +open Js_of_ocaml + +type options +val options : unit -> options + +val autocompleteBS : + options -> + (Dom_html.inputElement Js.t -> unit) [@@js.global "autocompleteBS"] \ No newline at end of file diff --git a/src/bindings/dune b/src/bindings/dune index d26ca66..bd45521 100644 --- a/src/bindings/dune +++ b/src/bindings/dune @@ -9,3 +9,9 @@ (deps monaco.mli) (action (run %{bin:gen_js_api} -o %{targets} %{deps}))) + +(rule + (targets autocompleteBS.ml) + (deps autocompleteBS.mli) + (action + (run %{bin:gen_js_api} -o %{targets} %{deps}))) diff --git a/src/static-requires.js b/src/static-requires.js index e8cc86b..37e465d 100644 --- a/src/static-requires.js +++ b/src/static-requires.js @@ -6,3 +6,6 @@ require('./stylesheet.scss'); joo_global_object.monaco = require('monaco-editor/esm/vs/editor/editor.api'); require('monaco-editor/esm/vs/basic-languages/cpp/cpp.contribution'); require('monaco-editor/esm/vs/editor/contrib/hover/hover'); + +var autocompleteBS = require("bootstrap5-autocomplete"); +joo_global_object.autocompleteBS = autocompleteBS; diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index cceb015..3fa47f3 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,6 +1,7 @@ open Lwt open Cohttp open Cohttp_lwt +//open AutocompleteBS module Client = Cohttp_lwt_jsoo.Client module ReactDOM = React.Dom From 4aed0fd40487e2134e63a4c4c52c8dd7b3bcc886 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 28 Jun 2023 15:23:20 +0200 Subject: [PATCH 35/48] Use regexes to parse input --- goblint-http-server/goblint.ml | 4 - src/Main.re | 12 +-- src/ui/base/input.re | 11 ++- src/ui/icons/IconArrowDown.re | 4 +- src/ui/icons/IconArrowUp.re | 4 +- src/ui/panel/ParameterView.re | 160 +++++++++++++++++++++++---------- src/utils/ParameterUtils.re | 118 ++++++++++-------------- 7 files changed, 171 insertions(+), 142 deletions(-) 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/src/Main.re b/src/Main.re index af2096b..b82a2d6 100644 --- a/src/Main.re +++ b/src/Main.re @@ -49,17 +49,7 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { ); let (goblint_path, parameters) = state |> ParameterUtils.get_parameters; - let destructured_params = - parameters - |> ParameterUtils.group_parameters - |> List.filter(s => { - let regex = Str.regexp_string("server."); - - switch (Str.search_forward(regex, s, 0)) { - | exception Not_found => true; - | _ => false; - } - }); + let (destructured_params, _) = parameters |> ParameterUtils.construct_parameters; let (history, setHistory) = React.useState(_ => [|(destructured_params, Time.get_local_time(), ParameterView.Executed)|]); diff --git a/src/ui/base/input.re b/src/ui/base/input.re index 6f743f6..cc11966 100644 --- a/src/ui/base/input.re +++ b/src/ui/base/input.re @@ -1,11 +1,12 @@ [@react.component] -let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?, ~style=?) => { +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" @@ -26,5 +27,9 @@ let make = (~type_=?, ~class_=?, ~value, ~on_change, ~on_submit=?, ~style=?) => Option.iter(cb => cb(), on_submit); }; - ; + switch id_ { + | "" => ; + | _ => ; + } + }; diff --git a/src/ui/icons/IconArrowDown.re b/src/ui/icons/IconArrowDown.re index 2f5766d..4c8be67 100644 --- a/src/ui/icons/IconArrowDown.re +++ b/src/ui/icons/IconArrowDown.re @@ -1,6 +1,6 @@ [@react.component] -let make = (~on_click) => { - +let make = () => { + } \ No newline at end of file diff --git a/src/ui/icons/IconArrowUp.re b/src/ui/icons/IconArrowUp.re index 296c3d4..ac91cc5 100644 --- a/src/ui/icons/IconArrowUp.re +++ b/src/ui/icons/IconArrowUp.re @@ -1,6 +1,6 @@ [@react.component] -let make = (~on_click) => { - +let make = () => { + } \ No newline at end of file diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 3fa47f3..4a13dc9 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -1,7 +1,6 @@ open Lwt open Cohttp open Cohttp_lwt -//open AutocompleteBS module Client = Cohttp_lwt_jsoo.Client module ReactDOM = React.Dom @@ -20,6 +19,29 @@ let paramState_to_string = (p: paramState) => { 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; @@ -41,11 +63,11 @@ let rev_arr = (array) => array |> Array.to_list |> List.rev |> Array.of_list; let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let (value, setValue) = React.useState(_ => parameters |> ParameterUtils.concat_parameter_list); - // Linked to cancelation, see reasons below for why it is commented out + // Linked to cancelation, see reasons below in on_cancel() for why it is commented out //let (disableCancel, setDisableCancel) = React.useState(_ => true); let (disableRun, setDisableRun) = React.useState(_ => false); + let (inputState, setInputState) = React.useState(_ => Ok); let (sortDesc, setSortDesc) = React.useState(_ => true); - let (hasServerOpts, setHasServerOpts) = React.useState(_ => false); React.useEffect1(() => { None @@ -61,26 +83,64 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { setSortDesc(_ => !sortDesc); } - - let on_change = (new_value) => { - let server_opt_regex = Str.regexp_string("server."); - let server_opts_found = switch (Str.search_forward(server_opt_regex, new_value, 0)) { - | exception Not_found => false; - | _ => true + let is_input_invalid = (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 + } } - setHasServerOpts(_ => server_opts_found); - setDisableRun(_ => server_opts_found); + } + + let react_on_input = (parameter_list, is_malformed, value) => { + let input_state = is_input_invalid(parameter_list, is_malformed, value); + setInputState(_ => input_state); + + let isInvalid = !is_ok(input_state) + setDisableRun(_ => isInvalid); + isInvalid + } + + let on_change = (new_value) => { + let (tuple_parameter_list, is_malformed) = + new_value + |> ParameterUtils.construct_parameters + |> ((p,b)) => (p |> ParameterUtils.tuples_from_parameters, b); + + let _ = react_on_input(tuple_parameter_list, is_malformed, new_value); setValue(_ => new_value); }; let on_submit = () => { - if (!hasServerOpts) { - let parameter_list = - value - |> ParameterUtils.construct_parameters - |> ParameterUtils.group_parameters - + let (parameter_list, tuple_parameter_list, is_malformed) = + value + |> 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, value); + + if (!isInvalid) { let time = Time.get_local_time(); let element = (parameter_list, time, Executing); @@ -135,14 +195,18 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; let config_api_call = (config_opts: list((string, string))) => { - config_opts - |> List.map(((k,v)) => { - `List([`String(k), `String(v)]) - |> Yojson.Safe.to_string - |> Body.of_string; - }) - |> List.map(inner_config_api_call) - |> Lwt.npick; + if (List.length(config_opts) == 0) { + Lwt.return([Error]) + } else { + config_opts + |> List.map(((k,v)) => { + `List([`String(k), Yojson.Safe.from_string(v)]) + |> Yojson.Safe.to_string + |> Body.of_string; + }) + |> List.map(inner_config_api_call) + |> Lwt.npick; + } }; let inner_analyze_api_call = (analyze_body): Lwt.t(paramState) => { @@ -165,15 +229,14 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { |> Body.of_string; let analyze_api_call = () => { - let config_opts = parameter_list |> ParameterUtils.tuples_from_parameters; - - config_opts + tuple_parameter_list |> config_api_call >>= (result) => { - let result_state = result - |> List.map(is_successful) - |> List.fold_left((a,b) => a && b, true) - |> ((s) => if (s) { Executed } else { Error }); + let result_state = + result + |> List.map(is_successful) + |> List.fold_left((a,b) => a && b, true) + |> ((s) => if (s) { Executed } else { Error }); Lwt.return(result_state); } >>= @@ -189,8 +252,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { }; }; - let () = analyze_api_call() |> ignore; - + ignore(analyze_api_call()); } }; @@ -243,12 +305,6 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { let list_elements = history |> map_history_entry_to_list_entry; - let icon_for_sort_dir = if (sortDesc) { - - } else { - - }; -
      {playButton} @@ -260,17 +316,19 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { // Input and tooltip are seperated due to display issues - {switch hasServerOpts { - | true => - | false => ; + {switch inputState { + | Malformed + | Blacklisted + | Empty => + | Ok => ; }} - {switch hasServerOpts { - | true => { + {switch inputState { + | Ok => React.null; + | _ => {
      - {"Server options are not allowed" |> React.string} + {inputState |> inputState_to_string |> React.string}
      }; - | _ => React.null; }}
      @@ -283,9 +341,13 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => {
      {"Status" |> React.string}
      -
      +
      {"Time " |> React.string} - {icon_for_sort_dir} + {switch sortDesc { + | true => + | _ => + }; + }
      {"Parameters" |> React.string} diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index 2b9c146..a65d8c2 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -1,90 +1,66 @@ open State -let concat_parameters = (parameters) => { - parameters - |> String.split_on_char(' ') - |> List.map((s) => { String.sub(s, 1, String.length(s)-2)}) - |> String.concat(" ") -}; - 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_params = switch (Yojson.Safe.Util.member("command", state.meta)) { + 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)}); - - (raw_params |> List.hd, raw_params |> List.tl) -}; - -let construct_parameters = (parameters) => parameters |> String.split_on_char(' ');//|> List.map((s) => "'" |> String.cat(s) |> String.cat("'")) - -let rec group_parameters = (parameters: list(string)): list(string) => { - if (parameters |> List.length > 0) { - - let (command, tail) = (parameters |> List.hd, parameters |> List.tl); - switch command { - | "--set" => { - let (option, tail') = (tail |> List.hd, tail |> List.tl); - let (value, tail'') = (tail' |> List.hd, tail' |> List.tl); - - let parameter = Printf.sprintf("--set %s %s", option, value); - tail'' |> group_parameters |> List.cons(parameter) - } - | "--enable" => { - let (option, tail') = (tail |> List.hd, tail |> List.tl); - - let parameter = Printf.sprintf("--enable %s", option); - tail' |> group_parameters |> List.cons(parameter) - } - | "--disable" => { - let (option, tail') = (tail |> List.hd, tail |> List.tl); + |> List.map((s) => { String.sub(s, 1, String.length(s)-2) }); - let parameter = Printf.sprintf("--disable %s", option); - tail' |> group_parameters |> List.cons(parameter) - } - | _ => [] - } - } else { - [] - } -} + let goblint_path = raw_parameters |> List.hd; + let parameters = raw_parameters |> List.tl |> concat_parameter_list; -let contains_empty_string = (string_list) => - string_list - |> List.map(String.length) - |> List.filter(i => i == 0) - |> List.length > 0 + (goblint_path, parameters); +}; -let tuples_from_parameters = (parameters) => { - parameters - |> List.map(params => { - let params_split = params |> String.split_on_char(' '); - let command = params_split |> List.hd; - let param' = params_split |> List.tl; +// 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)); + "" + })); - switch command { - | "--set" => { - let (option, tail') = (param' |> List.hd, param' |> List.tl); - let value = tail' |> List.hd; + (replaced_words.contents, (result |> String.trim |> String.length) > 0) +}; - Some((option, value)) +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 } - | "--enable" => { - let option = param' |> List.hd; - Some((option, "true")) - } - | "--disable" => { - let option = param' |> List.hd; - Some((option, "false")) + } 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 } - | _ => None + } else { + None } }) - |> List.filter(e => e != None) - |> List.map(e => e |> Option.get) - |> List.filter(((k,_)) => !(String.starts_with(~prefix="server.", k))) // Don't allow server modifications + |> 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 From 29dc7194e5fae43bbe062899574b8db94a2f1c36 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 28 Jun 2023 20:11:08 +0200 Subject: [PATCH 36/48] Fix UI bugs and improve adding items to history --- src/Main.re | 10 ++++- src/ui/panel/Panel.re | 4 +- src/ui/panel/ParameterView.re | 85 +++++++++++++---------------------- 3 files changed, 41 insertions(+), 58 deletions(-) diff --git a/src/Main.re b/src/Main.re index b82a2d6..de261e5 100644 --- a/src/Main.re +++ b/src/Main.re @@ -48,10 +48,16 @@ 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 (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 @@ -75,7 +81,7 @@ let make = (~cil, ~goblint, ~warnings, ~meta, ~stats, ~file_loc) => { | None =>
      | Some(f) => }} - +
      { }; [@react.component] -let make = (~state, ~dispatch, ~goblint_path, ~parameters, ~history, ~setHistory) => { +let make = (~state, ~dispatch, ~goblint_path, ~inputValue, ~setInputValue, ~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory) => { let locations = (state.goblint)#dead_locations; @@ -41,7 +41,7 @@ let make = (~state, ~dispatch, ~goblint_path, ~parameters, ~history, ~setHistory | Some(Warnings) => | Some(DeadCode) => | Some(Statistics) => - | Some(Parameters) => + | Some(Parameters) => | _ => React.null }; diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 4a13dc9..ef476ca 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -57,24 +57,16 @@ let headers = [ ("Access-Control-Allow-Methods", "GET, POST, PUT, DELETE, OPTIONS") ] |> Header.of_list; -let rev_arr = (array) => array |> Array.to_list |> List.rev |> Array.of_list; - [@react.component] -let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { - - let (value, setValue) = React.useState(_ => parameters |> ParameterUtils.concat_parameter_list); +let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory) => { // Linked to cancelation, see reasons below in on_cancel() for why it is commented out //let (disableCancel, setDisableCancel) = React.useState(_ => true); - let (disableRun, setDisableRun) = React.useState(_ => false); - let (inputState, setInputState) = React.useState(_ => Ok); - let (sortDesc, setSortDesc) = React.useState(_ => true); - + React.useEffect1(() => { None - }, [|value|]); + }, [|inputValue|]); React.useEffect1(() => { - setHistory(_ => history |> rev_arr); None }, [|sortDesc|]); @@ -111,8 +103,8 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { } } - let react_on_input = (parameter_list, is_malformed, value) => { - let input_state = is_input_invalid(parameter_list, is_malformed, value); + let react_on_input = (parameter_list, is_malformed, inputValue) => { + let input_state = is_input_invalid(parameter_list, is_malformed, inputValue); setInputState(_ => input_state); let isInvalid = !is_ok(input_state) @@ -121,60 +113,40 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { isInvalid } - let on_change = (new_value) => { + let on_change = (new_inputValue) => { let (tuple_parameter_list, is_malformed) = - new_value + new_inputValue |> ParameterUtils.construct_parameters |> ((p,b)) => (p |> ParameterUtils.tuples_from_parameters, b); - let _ = react_on_input(tuple_parameter_list, is_malformed, new_value); - setValue(_ => new_value); + let _ = react_on_input(tuple_parameter_list, is_malformed, new_inputValue); + setInputValue(_ => new_inputValue); }; let on_submit = () => { let (parameter_list, tuple_parameter_list, is_malformed) = - value + 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, value); + let isInvalid = react_on_input(tuple_parameter_list, is_malformed, inputValue); if (!isInvalid) { let time = Time.get_local_time(); let element = (parameter_list, time, Executing); - let new_history = if (sortDesc) { - history |> Array.append([|element|]) - } else { - [|element|] |> Array.append(history) - }; + let new_history = List.cons(element, history); setHistory(_ => new_history); //setDisableCancel(_ => false); let modify_history = (result: paramState): unit => { - let lastIndex = Array.length(new_history) - 1; - // This tuple is used to calculate where to update the last added history/parameter element - let (index, startIndex, endIndex) = if (sortDesc) { - (0, 1, lastIndex) - } else { - (lastIndex, 0, lastIndex) - }; - - let pickedElem = index |> Array.get(new_history); + let pickedElem = new_history |> List.hd; if (pickedElem == element) { - let intermediateHistory = endIndex |> Array.sub(new_history, startIndex); - - let new_element = (parameter_list, time, result); - - let new_history = if (sortDesc) { - intermediateHistory |> Array.append([|new_element|]) - } else { - [|new_element|] |> Array.append(intermediateHistory) - }; - + let intermediateHistory = new_history |> List.tl; + let new_history = List.cons(((parameter_list, time, result)), intermediateHistory); setHistory(_ => new_history); //setDisableCancel(_ => true); } @@ -258,13 +230,10 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { // This cancel function is here in case it will be implemented in the http-server, not far fetched. /*let on_cancel = () => { - let lastElemIndex = Array.length(history) - 1; - let (param, time, _) = Array.get(history, lastElemIndex); - - let intermediateHistory = Array.sub(history, 0, lastElemIndex); - let new_history = Array.append(intermediateHistory, [|(param, time, Canceled)|]); + 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); };*/ @@ -273,8 +242,16 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { {"Run" |> React.string} ; - let map_history_entry_to_list_entry = (arr) => { - arr |> Array.mapi((i, (parameter_grouping, time, paramState)) => + let map_history_entry_to_list_entry = (history) => { + history + |> (history) => { + if (!sortDesc) { + history |> List.rev + } else { + history + } + } + |> List.mapi((i, (parameter_grouping, time, paramState)) => {
    4. @@ -319,8 +296,8 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => { {switch inputState { | Malformed | Blacklisted - | Empty => - | Ok => ; + | Empty => + | Ok => ; }} {switch inputState { | Ok => React.null; @@ -355,7 +332,7 @@ let make = (~goblint_path, ~parameters, ~history, ~setHistory) => {
      5. } - {list_elements |> Array.to_list |> React.list} + {list_elements |> React.list}
    From b210584462dfe491b2a921aa4b5fbe530cc8d245 Mon Sep 17 00:00:00 2001 From: sxprz Date: Sun, 2 Jul 2023 19:35:10 +0200 Subject: [PATCH 37/48] Impl clickable parameter chips --- src/ui/panel/ParameterView.re | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index ef476ca..54df2ac 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -2,6 +2,7 @@ open Lwt open Cohttp open Cohttp_lwt +module Js = Js_of_ocaml.Js module Client = Cohttp_lwt_jsoo.Client module ReactDOM = React.Dom @@ -75,6 +76,18 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR setSortDesc(_ => !sortDesc); } + 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) => Js.to_string(p) ++ " " + | None => "" + }; + + setInputValue(inputVal => String.cat(parameter, inputVal)); + } + let is_input_invalid = (parameter_list: list((string, string)), is_malformed, input_val): inputState => { if (String.length(input_val) == 0) { Empty @@ -156,6 +169,9 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR Client.post(config_uri, ~body=config_body, ~headers=headers) >>= ((res, body)) => { let code = res |> Response.status |> Code.code_of_status; + /*let msg_from_body = Cohttp_lwt.Body.to_string(body) >|= (body) => { + Lwt.return(body) + }*/ let _ = Body.drain_body(body); if (code < 200 || code >= 400) { @@ -271,7 +287,9 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR
    {parameter_grouping |> List.mapi((j,e) => { - {e |> React.string} + + {e |> React.string} + }) |> React.list}
    From 5372d0835c58e793d972b490e49331e1eb1d871d Mon Sep 17 00:00:00 2001 From: sxprz Date: Sun, 2 Jul 2023 22:33:12 +0200 Subject: [PATCH 38/48] Improve input feedback and clickable chip --- src/ui/panel/ParameterView.re | 58 ++++++++++++++++++++++++----------- 1 file changed, 40 insertions(+), 18 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 54df2ac..0799cab 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -62,7 +62,7 @@ let headers = [ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory) => { // 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|]); @@ -76,19 +76,7 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR setSortDesc(_ => !sortDesc); } - 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) => Js.to_string(p) ++ " " - | None => "" - }; - - setInputValue(inputVal => String.cat(parameter, inputVal)); - } - - let is_input_invalid = (parameter_list: list((string, string)), is_malformed, input_val): inputState => { + 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) { @@ -117,7 +105,7 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR } let react_on_input = (parameter_list, is_malformed, inputValue) => { - let input_state = is_input_invalid(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) @@ -126,13 +114,40 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR isInvalid } - let on_change = (new_inputValue) => { + let check_input = (inputValue) : bool => { let (tuple_parameter_list, is_malformed) = - new_inputValue + 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 => "" + }; - let _ = react_on_input(tuple_parameter_list, is_malformed, new_inputValue); + setInputValue(inputVal => { + let new_inputVal = String.cat(parameter, inputVal); + let _ = check_input(new_inputVal); + new_inputVal + }); + } + + let on_change = (new_inputValue) => { + let _ = check_input(new_inputValue); setInputValue(_ => new_inputValue); }; @@ -253,6 +268,13 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR 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 playButton = */ - + // Input and tooltip are seperated due to display issues {switch inputState { | Malformed From 34c72c30721de2edc12565939486ea7f19b77332 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 5 Jul 2023 19:56:53 +0200 Subject: [PATCH 40/48] Improve parameter recognition and fix bugs --- src/ui/panel/ParameterView.re | 28 ++++++++++++++++++---------- src/utils/ParameterUtils.re | 6 +++--- 2 files changed, 21 insertions(+), 13 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 7fc09f5..6c4663b 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -141,7 +141,6 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR setInputValue(inputVal => { let new_inputVal = String.cat(parameter, inputVal); - let _ = check_input(new_inputVal); new_inputVal }); } @@ -158,9 +157,9 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR |> ((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); + /*let isInvalid = react_on_input(tuple_parameter_list, is_malformed, inputValue);*/ - if (!isInvalid) { + if (inputState == Ok && !is_malformed) { let time = Time.get_local_time(); let element = (parameter_list, time, Executing, ""); @@ -199,7 +198,16 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR let config_call_function = () => { config_opts |> List.map(((k,v)) => { - `List([`String(k), Yojson.Safe.from_string(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; }) @@ -348,7 +356,7 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR | Malformed | Blacklisted | Empty => - | Ok => ; + | Ok => ; }} {switch inputState { | Ok => React.null; @@ -371,11 +379,11 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR
    {"Time " |> React.string} - {switch sortDesc { - | true => - | _ => - }; - } + {if (sortDesc) { + + } else { + + }}
    {"Parameters" |> React.string} diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index a65d8c2..f5886fd 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -3,10 +3,10 @@ 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 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 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 From 1cc6942b8d8d93571f159eb9fc0ba0d439f41913 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 5 Jul 2023 20:58:58 +0200 Subject: [PATCH 41/48] Rearrange code for headers --- goblint-http-server/goblint_http.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/goblint-http-server/goblint_http.ml b/goblint-http-server/goblint_http.ml index 8e24815..1512c6c 100644 --- a/goblint-http-server/goblint_http.ml +++ b/goblint-http-server/goblint_http.ml @@ -25,9 +25,12 @@ let specs = let paths = ref [] -let cors_headers = Header.of_list [("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")] +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 From 9d38eca33887cda4699e2d1949f20eaf7f1149f4 Mon Sep 17 00:00:00 2001 From: sxprz Date: Wed, 5 Jul 2023 22:44:37 +0200 Subject: [PATCH 42/48] Fix wrong regex for --set --- src/utils/ParameterUtils.re | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/utils/ParameterUtils.re b/src/utils/ParameterUtils.re index f5886fd..84ecf51 100644 --- a/src/utils/ParameterUtils.re +++ b/src/utils/ParameterUtils.re @@ -3,7 +3,7 @@ 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 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\._\/]*\)\]\)|}); From de06648e03ddf591b7825ada22f2a0466a1ddbbb Mon Sep 17 00:00:00 2001 From: sxprz Date: Mon, 10 Jul 2023 21:29:05 +0200 Subject: [PATCH 43/48] Refactor code and optimize calls --- src/ui/panel/ParameterView.re | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/ui/panel/ParameterView.re b/src/ui/panel/ParameterView.re index 6c4663b..1a6b928 100644 --- a/src/ui/panel/ParameterView.re +++ b/src/ui/panel/ParameterView.re @@ -59,7 +59,7 @@ let headers = [ ] |> Header.of_list; [@react.component] -let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory) => { +let make = (~goblint_path, ~inputValue, ~setInputValue, ~disableRun, ~setDisableRun, ~inputState, ~setInputState, ~sortDesc, ~setSortDesc, ~history, ~setHistory) => { // Linked to cancelation, see reasons below in on_cancel() for why it is commented out //let (disableCancel, setDisableCancel) = React.useState(_ => true); @@ -71,6 +71,10 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR None }, [|sortDesc|]); + React.useEffect1(() => { + None + }, [|disableRun|]); + let on_sort = (ev) => { React.Event.Mouse.preventDefault(ev); setSortDesc(_ => !sortDesc); @@ -159,7 +163,7 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR // 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) { + if (inputState == Ok && !is_malformed && !disableRun) { let time = Time.get_local_time(); let element = (parameter_list, time, Executing, ""); @@ -167,6 +171,7 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR setHistory(_ => new_history); //setDisableCancel(_ => false); + setDisableRun(_ => true); let modify_history = (result: paramState, response_msg: string): unit => { let pickedElem = new_history |> List.hd; @@ -176,6 +181,7 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR let new_history = List.cons(((parameter_list, time, result, response_msg)), intermediateHistory); setHistory(_ => new_history); //setDisableCancel(_ => true); + setDisableRun(_ => false); } } @@ -289,11 +295,6 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR |> ((p,b)) => (p |> ParameterUtils.tuples_from_parameters, b); let _ = react_on_input(tuple_parameter_list, is_malformed, inputValue); - let playButton = ; - let map_history_entry_to_list_entry = (history) => { history |> (history) => { @@ -343,7 +344,10 @@ let make = (~goblint_path, ~inputValue, ~setInputValue,~disableRun, ~setDisableR
    - {playButton} + // Commented out because http server does not support cancelation yet /*