From 3c5e993e6e9de76393cea54215ec21c5fdb73c1d 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. sail can now load bytecode plugins, and will do so when the main sail program is running from bytecode 3. adds a wrapper called debug_sail which runs ocamldebug with the right environment --- debug_sail | 12 ++++++++++++ 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, 48 insertions(+), 22 deletions(-) create mode 100755 debug_sail diff --git a/debug_sail b/debug_sail new file mode 100755 index 000000000..b72c2be81 --- /dev/null +++ b/debug_sail @@ -0,0 +1,12 @@ +#!/usr/bin/env bash + +SAIL_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" +SAIL_BC="$SAIL_DIR/_build/default/src/bin/sail.bc" +if [ ! -f "$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_BC" $* diff --git a/src/bin/dune b/src/bin/dune index 59d9f36af..7d7b1d106 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..07fec203b 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -76,6 +76,7 @@ let opt_format_backup : string option ref = ref None let opt_format_only : string list ref = ref [] let opt_format_skip : string list ref = ref [] let opt_slice_instantiation_types : bool ref = ref false +let is_bytecode = Sys.backend_type = Bytecode (* Allow calling all options as either -foo_bar, -foo-bar, or --foo-bar (for long options). The standard long-opt version @@ -147,7 +148,7 @@ let add_target_header plugin opts = let load_plugin opts plugin = try - Dynlink.loadfile_private plugin; + if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private 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 +584,7 @@ let main () = options := Arg.align (fix_options !options); + 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))