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))