Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improve GobView build #1215

Merged
merged 18 commits into from
Feb 16, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/locked.yml
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,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
Expand Down
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ goblint
goblint.byte
goblint.json
goblint.domaintest
goblint_http.exe
src/config*.ml
tests/bench.txt
.DS_Store
Expand Down
9 changes: 4 additions & 5 deletions docs/user-guide/inspecting.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,10 @@ 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"`

4. Visit <http://localhost:8080>
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`
3. Visit <http://localhost:8080>

## Witnesses

Expand Down
2 changes: 1 addition & 1 deletion gobview
3 changes: 3 additions & 0 deletions make.sh
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,9 @@ rule() {
dune build --profile=release $TARGET.exe &&
rm -f goblint &&
cp _build/default/$TARGET.exe goblint
;; view)
eval $(opam config env)
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 &&
Expand Down
6 changes: 2 additions & 4 deletions scripts/test-gobview.py
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +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,
'-with-goblint', '../analyzer/goblint',
'-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"'])
goblint_http_path = './goblint_http.exe'
p = subprocess.Popen([goblint_http_path, 'tests/regression/00-sanity/01-assert.c'])

print("serving at port", PORT)
thread = Thread(target=serve, args=())
Expand Down
17 changes: 0 additions & 17 deletions src/maingoblint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -597,11 +597,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
stilscher marked this conversation as resolved.
Show resolved Hide resolved
(* copy relevant c files to gobview directory *)
Expand All @@ -625,20 +621,7 @@ 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
Logs.error "Warning: Cannot locate GobView."
)

let handle_extraspecials () =
let funs = get_string_list "exp.extraspecials" in
Expand Down