Skip to content

Commit

Permalink
enable use of ocamldebug
Browse files Browse the repository at this point in the history
This introduces a few changes:
1. the dune config is changed to generate bytecode objects for all modules
2. an option is added that makes sail load bytecode plugins instead of native plugins (ocamldebug requires them to be bytecode)
3. adds a wrapper called debug_sail which runs ocamldebug with the right options and environment to make it work
  • Loading branch information
lexbailey committed Dec 5, 2024
1 parent 59c282f commit 24c59bd
Show file tree
Hide file tree
Showing 14 changed files with 47 additions and 22 deletions.
11 changes: 11 additions & 0 deletions debug_sail
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#!/usr/bin/env bash

SAIL_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
if [ ! -f "$SAIL_DIR/_build/default/src/bin/sail.bc" ]; then
echo "Unable to find debug build of sail, please build it first."
echo " dune build --profile debug"
exit 1
fi
export SAIL_DIR
export DUNE_DIR_LOCATIONS="libsail:share:$SAIL_DIR/_build/install/default/share/libsail"
exec rlwrap ocamldebug $(bash -c "find . -iname '*.cmo' ; find . -iname '*.cma'" | xargs dirname | sort | uniq | sed 's/^\(.*\)$/-I \1/' | tr '\n' ' ') "$SAIL_DIR/_build/default/src/bin/sail.bc" $*
1 change: 1 addition & 0 deletions src/bin/dune
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@

(executable
(name sail)
(modes native byte)
(public_name sail)
(package sail)
(link_flags -linkall)
Expand Down
6 changes: 4 additions & 2 deletions src/bin/sail.ml
Original file line number Diff line number Diff line change
Expand Up @@ -147,7 +147,7 @@ let add_target_header plugin opts =

let load_plugin opts plugin =
try
Dynlink.loadfile_private plugin;
Dynlink.loadfile plugin;
let plugin_opts = Target.extract_options () |> fix_options |> target_align in
opts := add_target_header plugin !opts @ plugin_opts
with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
Expand Down Expand Up @@ -583,6 +583,8 @@ let main () =

options := Arg.align (fix_options !options);

let is_bytecode = Sys.backend_type = Bytecode in
let plugin_extension = if is_bytecode then ".cma" else ".cmxs" in
begin
match Sys.getenv_opt "SAIL_NO_PLUGINS" with
| Some _ -> ()
Expand All @@ -592,7 +594,7 @@ let main () =
List.iter
(fun plugin ->
let path = Filename.concat dir plugin in
if Filename.extension plugin = ".cmxs" then load_plugin options path
if Filename.extension plugin = plugin_extension then load_plugin options path
)
(Array.to_list (Sys.readdir dir))
| [] -> ()
Expand Down
1 change: 1 addition & 0 deletions src/lib/dune
Original file line number Diff line number Diff line change
Expand Up @@ -107,5 +107,6 @@
(name libsail)
(public_name libsail)
(libraries lem linksem pprint dune-site yojson menhirLib)
(modes byte native)
(instrumentation
(backend bisect_ppx)))
5 changes: 3 additions & 2 deletions src/sail_c_backend/dune
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
(executable
(name sail_plugin_c)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(install
(section
(site
(libsail plugins)))
(package sail_c_backend)
(files sail_plugin_c.cmxs))
(files sail_plugin_c.cmxs sail_plugin_c.cma))
5 changes: 3 additions & 2 deletions src/sail_coq_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,13 @@
(executable
(name sail_plugin_coq)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(install
(section
(site
(libsail plugins)))
(package sail_coq_backend)
(files sail_plugin_coq.cmxs))
(files sail_plugin_coq.cmxs sail_plugin_coq.cma))
5 changes: 3 additions & 2 deletions src/sail_doc_backend/dune
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
(executable
(name sail_plugin_doc)
(modes
(native plugin))
(native plugin)
(byte plugin))
(link_flags -linkall)
(libraries libsail omd yojson base64)
(embed_in_plugin_libraries omd base64))
Expand All @@ -11,4 +12,4 @@
(site
(libsail plugins)))
(package sail_doc_backend)
(files sail_plugin_doc.cmxs))
(files sail_plugin_doc.cmxs sail_plugin_doc.cma))
5 changes: 3 additions & 2 deletions src/sail_latex_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@
(executable
(name sail_plugin_latex)
(modes
(native plugin))
(native plugin)
(byte plugin))
(link_flags -linkall)
(libraries libsail omd)
(embed_in_plugin_libraries omd))
Expand All @@ -19,4 +20,4 @@
(site
(libsail plugins)))
(package sail_latex_backend)
(files sail_plugin_latex.cmxs))
(files sail_plugin_latex.cmxs sail_plugin_latex.cma))
5 changes: 3 additions & 2 deletions src/sail_lean_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,13 @@
(executable
(name sail_plugin_lean)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(install
(section
(site
(libsail plugins)))
(package sail_lean_backend)
(files sail_plugin_lean.cmxs))
(files sail_plugin_lean.cmxs sail_plugin_lean.cma))
5 changes: 3 additions & 2 deletions src/sail_lem_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,13 @@
(executable
(name sail_plugin_lem)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(install
(section
(site
(libsail plugins)))
(package sail_lem_backend)
(files sail_plugin_lem.cmxs))
(files sail_plugin_lem.cmxs sail_plugin_lem.cma))
5 changes: 3 additions & 2 deletions src/sail_ocaml_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@
(executable
(name sail_plugin_ocaml)
(modes
(native plugin))
(native plugin)
(byte plugin))
(link_flags -linkall)
(libraries libsail base64)
(embed_in_plugin_libraries base64))
Expand All @@ -19,4 +20,4 @@
(site
(libsail plugins)))
(package sail_ocaml_backend)
(files sail_plugin_ocaml.cmxs))
(files sail_plugin_ocaml.cmxs sail_plugin_ocaml.cma))
5 changes: 3 additions & 2 deletions src/sail_output/dune
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
(executable
(name sail_plugin_output)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(install
(section
(site
(libsail plugins)))
(package sail_output)
(files sail_plugin_output.cmxs))
(files sail_plugin_output.cmxs sail_plugin_output.cma))
5 changes: 3 additions & 2 deletions src/sail_smt_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,13 @@
(executable
(name sail_plugin_smt)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(install
(section
(site
(libsail plugins)))
(package sail_smt_backend)
(files sail_plugin_smt.cmxs))
(files sail_plugin_smt.cmxs sail_plugin_smt.cma))
5 changes: 3 additions & 2 deletions src/sail_sv_backend/dune
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@
(executable
(name sail_plugin_sv)
(modes
(native plugin))
(native plugin)
(byte plugin))
(libraries libsail))

(menhir
Expand All @@ -22,4 +23,4 @@
(site
(libsail plugins)))
(package sail_sv_backend)
(files sail_plugin_sv.cmxs))
(files sail_plugin_sv.cmxs sail_plugin_sv.cma))

0 comments on commit 24c59bd

Please sign in to comment.