From d4acd2017c93513f6df00a3cb972333d89e896bd Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Wed, 11 Oct 2023 11:18:05 +0200 Subject: [PATCH 01/16] refine build process, create make target --- .gitignore | 1 + make.sh | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/.gitignore b/.gitignore index 75bd23d36b..86c8760466 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,7 @@ goblint goblint.byte goblint.json goblint.domaintest +goblint-http src/config*.ml tests/bench.txt .DS_Store diff --git a/make.sh b/make.sh index af1411a8d3..c70ae4870d 100755 --- a/make.sh +++ b/make.sh @@ -33,6 +33,11 @@ rule() { dune build --profile=release $TARGET.exe && rm -f goblint && cp _build/default/$TARGET.exe goblint + ;; view) + eval $(opam config env) + dune build gobview && + rm -f goblint-http && + cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && From 74b8d6d8d920562bc010f80ce729cfb82fc1d558 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Wed, 11 Oct 2023 11:20:38 +0200 Subject: [PATCH 02/16] adapt documentation --- docs/user-guide/inspecting.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md index f4f6036f1b..ba6c151ff1 100644 --- a/docs/user-guide/inspecting.md +++ b/docs/user-guide/inspecting.md @@ -18,8 +18,8 @@ For the initial setup: To build GobView (also for development): -1. Run `dune build gobview` in the analyzer directory to build the web UI -2. The executable for the http-server can then be found in the directory `./_build/default/gobview/goblint-http-server`. It takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ -`./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"` +1. Run `make view` in the analyzer directory to build the web UI +2. The executable `goblint-http` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ +`./goblint-http -with-goblint ./goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"` -4. Visit +3. Visit From d5aa890887c4427778354c04f9820737275e00c4 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Wed, 11 Oct 2023 16:57:34 +0200 Subject: [PATCH 03/16] copy gobview dist files during build instead of goblint run --- make.sh | 4 +++- src/maingoblint.ml | 17 ----------------- 2 files changed, 3 insertions(+), 18 deletions(-) diff --git a/make.sh b/make.sh index c70ae4870d..8137368f6f 100755 --- a/make.sh +++ b/make.sh @@ -37,7 +37,9 @@ rule() { eval $(opam config env) dune build gobview && rm -f goblint-http && - cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http + cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http && + mkdir -p run && + cp -R ./_build/default/gobview/dist/* ./run/ # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 7808cbcd3f..4b5130d8d0 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -577,11 +577,7 @@ let do_html_output () = let do_gobview cilfile = let gobview = GobConfig.get_bool "gobview" in - let goblint_root = GobFpath.cwd_append (fst (Fpath.split_base (Fpath.v Sys.argv.(0)))) in - let dist_dir = Fpath.(goblint_root // (Fpath.v "_build/default/gobview/dist")) in - let js_file = Fpath.(dist_dir / "main.js") in if gobview then ( - if Sys.file_exists (Fpath.to_string js_file) then ( let save_run = GobConfig.get_string "save_run" in let run_dir = Fpath.v(if save_run <> "" then save_run else "run") in (* copy relevant c files to gobview directory *) @@ -605,19 +601,6 @@ let do_gobview cilfile = (* marshal timing statistics *) let stats = Fpath.(run_dir / "stats.marshalled") in Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats; - let dist_files = - Sys.files_of (Fpath.to_string dist_dir) - |> Enum.filter (fun n -> n <> "dune") - |> List.of_enum - in - List.iter (fun n -> - FileUtil.cp - [Fpath.to_string (Fpath.(dist_dir / n))] - (Fpath.to_string (Fpath.(run_dir / n))) - ) dist_files - ) - else - eprintf "Warning: Cannot locate GobView.\n" ) let handle_extraspecials () = From 42a32ea0aefb98f0cf16c21157c95dc83cd8ab90 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 12 Oct 2023 10:53:27 +0200 Subject: [PATCH 04/16] simplify docs --- docs/user-guide/inspecting.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md index ba6c151ff1..c03f4c8be9 100644 --- a/docs/user-guide/inspecting.md +++ b/docs/user-guide/inspecting.md @@ -20,6 +20,6 @@ To build GobView (also for development): 1. Run `make view` in the analyzer directory to build the web UI 2. The executable `goblint-http` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ -`./goblint-http -with-goblint ./goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"` +`./goblint-http tests/regression/00-sanity/01-assert.c` 3. Visit From 292262a3a23143de927c28297fe330fe52d98776 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 12 Oct 2023 13:24:23 +0200 Subject: [PATCH 05/16] update gobview submodule --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index b373d06174..6302bb2515 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit b373d06174667537b671f3122daf4ebd4b195aea +Subproject commit 6302bb25153a05a80068324cb6eea046a5c70f6f From 248673a8dac7f998bc0f3e50c9d051cb4c6569fc Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 12 Oct 2023 15:41:41 +0200 Subject: [PATCH 06/16] adapt gobview test --- .github/workflows/locked.yml | 2 +- scripts/test-gobview.py | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index 007ea34619..d9c26fa797 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -167,7 +167,7 @@ jobs: run: ./make.sh nat - name: Build Gobview - run: opam exec -- dune build gobview + run: ./make.sh view - name: Install selenium run: pip3 install selenium webdriver-manager diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py index 1ac8f6a76c..56978c5d37 100644 --- a/scripts/test-gobview.py +++ b/scripts/test-gobview.py @@ -24,8 +24,8 @@ def cleanup(browser, thread): # serve GobView in different thread so it does not block the testing def serve(): global p - goblint_http_path = '_build/default/gobview/goblint-http-server/goblint_http.exe' - p = subprocess.Popen(['./' + goblint_http_path, + goblint_http_path = './goblint-http' + p = subprocess.Popen([goblint_http_path, '-with-goblint', '../analyzer/goblint', '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"']) From 1e7c6fe5241f77a9e134c8d4ff99dce6a7a827ac Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 2 Nov 2023 16:54:16 +0100 Subject: [PATCH 07/16] copy gobview distribution files to gobview_dist --- .gitignore | 1 + make.sh | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index 86c8760466..1e72c94544 100644 --- a/.gitignore +++ b/.gitignore @@ -85,6 +85,7 @@ dune-workspace # gobview run/ gobview_out/* +gobview_dist/* # witnesses witness.yml diff --git a/make.sh b/make.sh index 8137368f6f..80143a7034 100755 --- a/make.sh +++ b/make.sh @@ -38,8 +38,8 @@ rule() { dune build gobview && rm -f goblint-http && cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http && - mkdir -p run && - cp -R ./_build/default/gobview/dist/* ./run/ + mkdir -p gobview_dist && + cp -R ./_build/default/gobview/dist/* ./gobview_dist/ # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && From 8b834df035bf9ecf6cbf0ea4a3e20a8d5b750265 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 8 Dec 2023 15:31:01 +0100 Subject: [PATCH 08/16] use dist directory within gobview --- .gitignore | 1 - make.sh | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/.gitignore b/.gitignore index 1e72c94544..86c8760466 100644 --- a/.gitignore +++ b/.gitignore @@ -85,7 +85,6 @@ dune-workspace # gobview run/ gobview_out/* -gobview_dist/* # witnesses witness.yml diff --git a/make.sh b/make.sh index 80143a7034..040063235a 100755 --- a/make.sh +++ b/make.sh @@ -38,8 +38,8 @@ rule() { dune build gobview && rm -f goblint-http && cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http && - mkdir -p gobview_dist && - cp -R ./_build/default/gobview/dist/* ./gobview_dist/ + mkdir -p gobview/dist && + cp -R ./_build/default/gobview/dist/* ./gobview/dist/ # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && From dd4f9669ef201ccfae4e3617f53d9d9c077a9e97 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 8 Dec 2023 15:32:42 +0100 Subject: [PATCH 09/16] copy dist files using dune --- make.sh | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/make.sh b/make.sh index 040063235a..c70ae4870d 100755 --- a/make.sh +++ b/make.sh @@ -37,9 +37,7 @@ rule() { eval $(opam config env) dune build gobview && rm -f goblint-http && - cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http && - mkdir -p gobview/dist && - cp -R ./_build/default/gobview/dist/* ./gobview/dist/ + cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && From ed75229c739b11ddc217875a356017b3b2ebec95 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 8 Dec 2023 18:24:57 +0100 Subject: [PATCH 10/16] copy dist files to _dist directory --- make.sh | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/make.sh b/make.sh index c70ae4870d..9eee68325b 100755 --- a/make.sh +++ b/make.sh @@ -37,7 +37,10 @@ rule() { eval $(opam config env) dune build gobview && rm -f goblint-http && - cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http + cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http && + rm -rf gobview/_dist && + mkdir gobview/_dist + cp ./_build/default/gobview/dist/* gobview/_dist/ # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && From 2a543f57859d33a0ffc0df9fc349fb26a934a878 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Tue, 30 Jan 2024 18:41:48 +0100 Subject: [PATCH 11/16] copy dist folder and promote executable with dune --- docs/user-guide/inspecting.md | 4 ++-- make.sh | 7 +------ 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md index c03f4c8be9..9df965381f 100644 --- a/docs/user-guide/inspecting.md +++ b/docs/user-guide/inspecting.md @@ -19,7 +19,7 @@ For the initial setup: To build GobView (also for development): 1. Run `make view` in the analyzer directory to build the web UI -2. The executable `goblint-http` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ -`./goblint-http tests/regression/00-sanity/01-assert.c` +2. The executable `goblint-http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ +`./goblint-http.exe tests/regression/00-sanity/01-assert.c` 3. Visit diff --git a/make.sh b/make.sh index 9eee68325b..75da2b154b 100755 --- a/make.sh +++ b/make.sh @@ -35,12 +35,7 @@ rule() { cp _build/default/$TARGET.exe goblint ;; view) eval $(opam config env) - dune build gobview && - rm -f goblint-http && - cp ./_build/default/gobview/goblint-http-server/goblint_http.exe goblint-http && - rm -rf gobview/_dist && - mkdir gobview/_dist - cp ./_build/default/gobview/dist/* gobview/_dist/ + dune build gobview # alternatives to .exe: .bc (bytecode), .bc.js (js_of_ocaml), see https://dune.readthedocs.io/en/stable/dune-files.html#executable ;; js) # https://dune.readthedocs.io/en/stable/jsoo.html dune build $TARGET.bc.js && From 9e5aa87b3f58813fc3d3597bb563aad49513404c Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 15 Feb 2024 19:39:03 +0100 Subject: [PATCH 12/16] fix inconsistent naming of executable --- .gitignore | 2 +- docs/user-guide/inspecting.md | 4 ++-- scripts/test-gobview.py | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.gitignore b/.gitignore index 9455467fe4..c3fe37f6ab 100644 --- a/.gitignore +++ b/.gitignore @@ -10,7 +10,7 @@ goblint goblint.byte goblint.json goblint.domaintest -goblint-http +goblint_http.exe src/config*.ml tests/bench.txt .DS_Store diff --git a/docs/user-guide/inspecting.md b/docs/user-guide/inspecting.md index 43a354cc4c..6ea08db1f4 100644 --- a/docs/user-guide/inspecting.md +++ b/docs/user-guide/inspecting.md @@ -19,8 +19,8 @@ For the initial setup: To build GobView (also for development): 1. Run `make view` in the analyzer directory to build the web UI -2. The executable `goblint-http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ -`./goblint-http.exe tests/regression/00-sanity/01-assert.c` +2. The executable `goblint_http.exe` takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\ +`./goblint_http.exe tests/regression/00-sanity/01-assert.c` 3. Visit ## Witnesses diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py index 5483a21b82..3b3052a3c5 100644 --- a/scripts/test-gobview.py +++ b/scripts/test-gobview.py @@ -24,7 +24,7 @@ def cleanup(browser, thread): # serve GobView in different thread so it does not block the testing def serve(): global p - goblint_http_path = './goblint-http' + goblint_http_path = './goblint_http.exe' p = subprocess.Popen([goblint_http_path, '-with-goblint', '../analyzer/goblint', '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"']) From 037e1bcf9dc62c682c939a93c469e972b580a672 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 15 Feb 2024 19:39:43 +0100 Subject: [PATCH 13/16] update submodule gobview --- gobview | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gobview b/gobview index 649451b76d..543c48f143 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit 649451b76de7294b736ff863d1c1479bf5be2270 +Subproject commit 543c48f143532a024c75001a176792acacc9421c From 674eb9feee0007e7f6704df2a72256bb8fe492e6 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Thu, 15 Feb 2024 19:43:12 +0100 Subject: [PATCH 14/16] adapt GobView test to use shorter command --- scripts/test-gobview.py | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/scripts/test-gobview.py b/scripts/test-gobview.py index 3b3052a3c5..f5961108d7 100644 --- a/scripts/test-gobview.py +++ b/scripts/test-gobview.py @@ -25,9 +25,7 @@ def cleanup(browser, thread): def serve(): global p goblint_http_path = './goblint_http.exe' - p = subprocess.Popen([goblint_http_path, - '-with-goblint', '../analyzer/goblint', - '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"']) + p = subprocess.Popen([goblint_http_path, 'tests/regression/00-sanity/01-assert.c']) print("serving at port", PORT) thread = Thread(target=serve, args=()) From 56655c19176ecfb3e78bed979ad32d51e0714af6 Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 16 Feb 2024 15:31:46 +0100 Subject: [PATCH 15/16] fix error message --- src/maingoblint.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 0d36ce7226..365d1779c3 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -623,7 +623,7 @@ let do_gobview cilfile = Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats; ) else - Logs.error "Warning: Cannot locate GobView." + Logs.error "Cannot locate GobView." let handle_extraspecials () = let funs = get_string_list "exp.extraspecials" in From bcbbcd8767e9c2c3847ed79e26378ebeb8e2b50b Mon Sep 17 00:00:00 2001 From: stilscher <66023521+stilscher@users.noreply.github.com> Date: Fri, 16 Feb 2024 15:34:57 +0100 Subject: [PATCH 16/16] fix wrong merge --- src/maingoblint.ml | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/maingoblint.ml b/src/maingoblint.ml index 365d1779c3..2c81ee7fd7 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -622,8 +622,6 @@ let do_gobview cilfile = let stats = Fpath.(run_dir / "stats.marshalled") in Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats; ) - else - Logs.error "Cannot locate GobView." let handle_extraspecials () = let funs = get_string_list "exp.extraspecials" in