ELF loading for C backend

Add a flag to Sail that allows for an image of an elf file to be
dumped in a simple format using linksem, used as

sail -elf test.elf -o test.bin

This image file can then be used by a compiled C version of a sail
spec as with ocaml simply by

./a.out test.bin

5 files changed, 43 insertions, 13 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 20cdb4ac..d7d9b27f 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2069,7 +2069,7 @@ let fix_exception ctx instrs =
 let letdef_count = ref 0
 
 (** Compile a Sail toplevel definition into an IR definition **)
-let compile_def ctx = function
+let rec compile_def ctx = function
   | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) ->
      [CDEF_reg_dec (id, ctyp_of_typ ctx typ)], ctx
   | DEF_reg_dec _ -> failwith "Unsupported register declaration" (* FIXME *)
@@ -2166,6 +2166,10 @@ let compile_def ctx = function
   (* Only the parser and sail pretty printer care about this. *)
   | DEF_fixity _ -> [], ctx
 
+  | DEF_internal_mutrec fundefs ->
+     let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in
+     List.fold_left (fun (cdefs, ctx) def -> let cdefs', ctx = compile_def ctx def in (cdefs @ cdefs', ctx)) ([], ctx) defs
+
   | def ->
      c_error ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))
 
@@ -3280,8 +3284,9 @@ let compile_ast ctx (Defs defs) =
     in
 
     let postamble = separate hardline (List.map string
-       ( [ "int main(void)";
+       ( [ "int main(int argc, char *argv[])";
            "{";
+           "  if (argc > 1) { load_image(argv[1]); }";
            "  setup_library();" ]
        @ fst exn_boilerplate
        @ startup cdefs
@@ -3294,7 +3299,7 @@ let compile_ast ctx (Defs defs) =
        @ finish cdefs
        @ snd exn_boilerplate
        @ [ "  cleanup_library();";
-           "  return 0;";
+           "  return EXIT_SUCCESS;";
            "}" ] ))
     in
 
diff --git a/src/elf_loader.ml b/src/elf_loader.ml
index 1be3b1d1..89987647 100644
--- a/src/elf_loader.ml
+++ b/src/elf_loader.ml
@@ -103,7 +103,14 @@ let read name =
   in
   (segments, e_entry, symbol_map)
 
-let load_segment seg =
+let write_sail_lib paddr i byte =
+  Sail_lib.wram (Big_int.add paddr (Big_int.of_int i)) byte
+
+let write_file chan paddr i byte =
+  output_string chan (Big_int.to_string (Big_int.add paddr (Big_int.of_int i)) ^ "\n");
+  output_string chan (string_of_int byte ^ "\n")
+
+let load_segment ?writer:(writer=write_sail_lib) seg =
   let open Elf_interpreted_segment in
   let (Byte_sequence.Sequence bs) = seg.elf64_segment_body in
   let paddr = seg.elf64_segment_paddr in
@@ -114,15 +121,15 @@ let load_segment seg =
   prerr_endline ("Segment base address: " ^ Big_int.to_string base);
   prerr_endline ("Segment physical address: " ^ Big_int.to_string paddr);
   print_segment seg;
-  List.iteri (fun i byte -> Sail_lib.wram (Big_int.add paddr (Big_int.of_int i)) byte) (List.map int_of_char bs)
+  List.iteri (writer paddr) (List.map int_of_char bs)
 
-let load_elf name =
+let load_elf ?writer:(writer=write_sail_lib) name =
   let segments, e_entry, symbol_map = read name in
   opt_elf_entry := e_entry;
   (if List.mem_assoc "tohost" symbol_map then
      let (_, _, tohost_addr, _, _) = List.assoc "tohost" symbol_map in
      opt_elf_tohost := tohost_addr);
-  List.iter load_segment segments
+  List.iter (load_segment ~writer:writer) segments
 
 (* The sail model can access this by externing a unit -> int function
    as Elf_loader.elf_entry. *)
diff --git a/src/sail.ml b/src/sail.ml
index 2e13bc01..888e8eb6 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -66,6 +66,7 @@ let opt_sanity = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_file_arguments = ref ([]:string list)
 let opt_mono_split = ref ([]:((string * int) * string) list)
+let opt_process_elf : string option ref = ref None
 
 let options = Arg.align ([
   ( "-o",
@@ -90,6 +91,9 @@ let options = Arg.align ([
   ( "-c",
     Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen],
     " output a C translated version of the input");
+  ( "-elf",
+    Arg.String (fun elf -> opt_process_elf := Some elf),
+    " process an elf file so that it can be executed by compiled C code");
   ( "-O",
     Arg.Tuple [Arg.Set C_backend.optimize_primops;
                Arg.Set C_backend.optimize_hoist_allocations;
@@ -244,6 +248,21 @@ let main() =
     let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
     Util.opt_warnings := false; (* Don't show warnings during re-writing for now *)
 
+    begin match !opt_process_elf, !opt_file_out with
+    | Some elf, Some out ->
+       begin
+         let open Elf_loader in
+         let chan = open_out out in
+         load_elf ~writer:(write_file chan) elf;
+         close_out chan;
+         exit 0
+       end
+    | Some _, None ->
+       prerr_endline "Failure: No output file given for processed ELF (option -o).";
+       exit 1
+    | None, _ -> ()
+    end;
+
     (*let _ = Printf.eprintf "Type checked, next to pretty print" in*)
     begin
       (if !(opt_interactive)
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 252d815d..8b3e2313 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -556,7 +556,6 @@ let zero_extend (vec, n) =
   then take m vec
   else replicate_bits ([B0], Big_int.of_int (m - List.length vec)) @ vec
 
-
 let sign_extend (vec, n) =
   let m = Big_int.to_int n in
   match vec with
@@ -576,7 +575,7 @@ let shiftr (x, y) =
   let zeros = zeros y in
   let rbits = zeros @ x in
   take (List.length x) rbits
-  
+
 let shift_bits_right (x, y) =
   shiftr (x, uint(y))
 
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 74312d9b..97b634da 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -568,14 +568,14 @@ let add_def_to_graph (prelude, original_order, defset, graph) d =
 let print_dot graph component : unit =
   match component with
   | root :: _ ->
-     print_endline ("// Dependency cycle including " ^ root);
-     print_endline ("digraph cycle_" ^ root ^ " {");
+     prerr_endline ("// Dependency cycle including " ^ root);
+     prerr_endline ("digraph cycle_" ^ root ^ " {");
      List.iter (fun caller ->
-       let print_edge callee = print_endline ("  \"" ^ caller ^ "\" -> \"" ^ callee ^ "\";") in
+       let print_edge callee = prerr_endline ("  \"" ^ caller ^ "\" -> \"" ^ callee ^ "\";") in
        Namemap.find caller graph
        |> Nameset.filter (fun id -> List.mem id component)
        |> Nameset.iter print_edge) component;
-     print_endline "}"
+     prerr_endline "}"
   | [] -> ()
 
 let def_of_component graph defset comp =