From 24c59bda5a17eff40ee2c6cb01c3605dbf047edc Mon Sep 17 00:00:00 2001 From: Lex Bailey Date: Wed, 4 Dec 2024 18:25:20 +0000 Subject: [PATCH] enable use of ocamldebug 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 --- debug_sail | 11 +++++++++++ src/bin/dune | 1 + src/bin/sail.ml | 6 ++++-- src/lib/dune | 1 + src/sail_c_backend/dune | 5 +++-- src/sail_coq_backend/dune | 5 +++-- src/sail_doc_backend/dune | 5 +++-- src/sail_latex_backend/dune | 5 +++-- src/sail_lean_backend/dune | 5 +++-- src/sail_lem_backend/dune | 5 +++-- src/sail_ocaml_backend/dune | 5 +++-- src/sail_output/dune | 5 +++-- src/sail_smt_backend/dune | 5 +++-- src/sail_sv_backend/dune | 5 +++-- 14 files changed, 47 insertions(+), 22 deletions(-) create mode 100755 debug_sail diff --git a/debug_sail b/debug_sail new file mode 100755 index 000000000..ce69e093d --- /dev/null +++ b/debug_sail @@ -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" $* diff --git a/src/bin/dune b/src/bin/dune index 396ddad7c..1d5e4c4df 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -10,6 +10,7 @@ (executable (name sail) + (modes native byte) (public_name sail) (package sail) (link_flags -linkall) diff --git a/src/bin/sail.ml b/src/bin/sail.ml index 8dca5aa08..4bbecbcaa 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -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) @@ -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 _ -> () @@ -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)) | [] -> () diff --git a/src/lib/dune b/src/lib/dune index 022d440bb..f1a0905bb 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -107,5 +107,6 @@ (name libsail) (public_name libsail) (libraries lem linksem pprint dune-site yojson menhirLib) + (modes byte native) (instrumentation (backend bisect_ppx))) diff --git a/src/sail_c_backend/dune b/src/sail_c_backend/dune index 3b6b2657a..ebdee10c2 100644 --- a/src/sail_c_backend/dune +++ b/src/sail_c_backend/dune @@ -1,7 +1,8 @@ (executable (name sail_plugin_c) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (install @@ -9,4 +10,4 @@ (site (libsail plugins))) (package sail_c_backend) - (files sail_plugin_c.cmxs)) + (files sail_plugin_c.cmxs sail_plugin_c.cma)) diff --git a/src/sail_coq_backend/dune b/src/sail_coq_backend/dune index 4524ede4a..d88fd39b1 100644 --- a/src/sail_coq_backend/dune +++ b/src/sail_coq_backend/dune @@ -9,7 +9,8 @@ (executable (name sail_plugin_coq) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (install @@ -17,4 +18,4 @@ (site (libsail plugins))) (package sail_coq_backend) - (files sail_plugin_coq.cmxs)) + (files sail_plugin_coq.cmxs sail_plugin_coq.cma)) diff --git a/src/sail_doc_backend/dune b/src/sail_doc_backend/dune index 0377e7dbe..ad43a9545 100644 --- a/src/sail_doc_backend/dune +++ b/src/sail_doc_backend/dune @@ -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)) @@ -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)) diff --git a/src/sail_latex_backend/dune b/src/sail_latex_backend/dune index 9a518cbd3..ec6bc6809 100644 --- a/src/sail_latex_backend/dune +++ b/src/sail_latex_backend/dune @@ -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)) @@ -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)) diff --git a/src/sail_lean_backend/dune b/src/sail_lean_backend/dune index fbd1c131b..f689c3d0f 100644 --- a/src/sail_lean_backend/dune +++ b/src/sail_lean_backend/dune @@ -9,7 +9,8 @@ (executable (name sail_plugin_lean) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (install @@ -17,4 +18,4 @@ (site (libsail plugins))) (package sail_lean_backend) - (files sail_plugin_lean.cmxs)) + (files sail_plugin_lean.cmxs sail_plugin_lean.cma)) diff --git a/src/sail_lem_backend/dune b/src/sail_lem_backend/dune index 28907ec9a..1ef089031 100644 --- a/src/sail_lem_backend/dune +++ b/src/sail_lem_backend/dune @@ -9,7 +9,8 @@ (executable (name sail_plugin_lem) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (install @@ -17,4 +18,4 @@ (site (libsail plugins))) (package sail_lem_backend) - (files sail_plugin_lem.cmxs)) + (files sail_plugin_lem.cmxs sail_plugin_lem.cma)) diff --git a/src/sail_ocaml_backend/dune b/src/sail_ocaml_backend/dune index 251d7d0f2..9f0d7b866 100644 --- a/src/sail_ocaml_backend/dune +++ b/src/sail_ocaml_backend/dune @@ -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)) @@ -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)) diff --git a/src/sail_output/dune b/src/sail_output/dune index 4a0fa1a5e..b2ec82901 100644 --- a/src/sail_output/dune +++ b/src/sail_output/dune @@ -1,7 +1,8 @@ (executable (name sail_plugin_output) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (install @@ -9,4 +10,4 @@ (site (libsail plugins))) (package sail_output) - (files sail_plugin_output.cmxs)) + (files sail_plugin_output.cmxs sail_plugin_output.cma)) diff --git a/src/sail_smt_backend/dune b/src/sail_smt_backend/dune index 7a0128ab8..5bbd2e264 100644 --- a/src/sail_smt_backend/dune +++ b/src/sail_smt_backend/dune @@ -9,7 +9,8 @@ (executable (name sail_plugin_smt) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (install @@ -17,4 +18,4 @@ (site (libsail plugins))) (package sail_smt_backend) - (files sail_plugin_smt.cmxs)) + (files sail_plugin_smt.cmxs sail_plugin_smt.cma)) diff --git a/src/sail_sv_backend/dune b/src/sail_sv_backend/dune index ff1092a0a..a0870202a 100644 --- a/src/sail_sv_backend/dune +++ b/src/sail_sv_backend/dune @@ -9,7 +9,8 @@ (executable (name sail_plugin_sv) (modes - (native plugin)) + (native plugin) + (byte plugin)) (libraries libsail)) (menhir @@ -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))