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

1 files changed, 8 insertions, 3 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