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

@@ -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" $*

src/bin/dune

@@ -10,6 +10,7 @@
 
 (executable
  (name sail)
+ (modes native byte)
  (public_name sail)
  (package sail)
  (link_flags -linkall)

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,10 @@ 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 +587,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 +597,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))
         | [] -> ()

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

src/sail_c_backend/dune

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

src/sail_coq_backend/dune

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

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

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

src/sail_lean_backend/dune

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

src/sail_lem_backend/dune

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

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

src/sail_output/dune

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

src/sail_smt_backend/dune

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

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