From e6354d8ceea7217e1544606c3c2b79bca4e582fe Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Thu, 14 May 2020 18:01:16 +0100 Subject: Add static to more C functions This allows me to compile sail-riscv64 and sail-riscv128 code in the same static library. --- src/jib/c_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index fa4fa802..e5486645 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -1592,7 +1592,7 @@ let codegen_type_def ctx = function in let codegen_undefined = let name = sgen_id id in - string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) + string (Printf.sprintf "static enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id)) in string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi] -- cgit v1.2.3 From 363cf77a75cb8237fb13b028c0046b7817dbe734 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 13:43:07 +0100 Subject: Also allow adding static to model_{init,fini,main}() Without this I get the following linker error when trying to include both 64 and 128 bit sail-riscv code in the same binary: duplicate symbol '_model_init' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) duplicate symbol '_model_main' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) duplicate symbol '_model_fini' in: libsail_wrapper128.a(sail_wrapper_128.c.o) libsail_wrapper128.a(sail_wrapper_64.c.o) # Conflicts: # src/jib/c_backend.ml --- src/jib/c_backend.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index e5486645..e6610e93 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2291,7 +2291,7 @@ let compile_ast env output_chan c_includes ast = in let model_init = separate hardline (List.map string - ( [ "void model_init(void)"; + ( [ "static void model_init(void)"; "{"; " setup_rts();" ] @ fst exn_boilerplate @@ -2303,7 +2303,7 @@ let compile_ast env output_chan c_includes ast = in let model_fini = separate hardline (List.map string - ( [ "void model_fini(void)"; + ( [ "static void model_fini(void)"; "{" ] @ letbind_finalizers @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) @@ -2313,8 +2313,8 @@ let compile_ast env output_chan c_includes ast = @ [ "}" ] )) in - let model_default_main = - ([ "int model_main(int argc, char *argv[])"; + let model_default_main = + ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (if !opt_static then "static " else ""); "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; -- cgit v1.2.3 From dc5a39649116c7fd76a024d069707f8b3aa7e201 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 09:43:12 +0100 Subject: Also make the letbinding C variables static I was getting run-time failures when code generate from cheri128 and cheri64 in the same process. This was caused because my compiler defaults to -fcommon so it merged multiple variables (with conflicting types!). When initializing the second set of letbindings, the first one was overwritten (first variable was lbits, the other was uint64_t). Compiling with -fno-common exposes this problem. --- src/jib/c_backend.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index e6610e93..080be248 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2127,7 +2127,8 @@ let codegen_def' ctx = function let cleanup = List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings) in - separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings + let static = if !opt_static then "static " else "" in + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" static (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) ^^ string "{" ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline -- cgit v1.2.3 From 402fe1f632f7e6075e0810dcff2d8432b65352d2 Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 13:51:32 +0100 Subject: Add static to registers if -static is passed This was the final missing step for me to link two almost identical C files generated from sail into the same library. --- src/jib/c_backend.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 080be248..40d784ca 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2050,7 +2050,7 @@ let codegen_alloc = function let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline - ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf "%s%s %s;" (if !opt_static then "static " else "") (sgen_ctyp ctyp) (sgen_id id)) | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> let static = if !opt_static then "static " else "" in -- cgit v1.2.3 From 4d50c7b8601907774da137f4f3609f644f5df20a Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 16:26:00 +0100 Subject: C backend: Add a static () helper This simplifies some of the code. --- src/jib/c_backend.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 40d784ca..4527aaa1 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -62,6 +62,7 @@ open Anf module Big_int = Nat_big_num let opt_static = ref false +let static () = if !opt_static then "static " else "" let opt_no_main = ref false let opt_no_lib = ref false let opt_no_rts = ref false @@ -2050,16 +2051,15 @@ let codegen_alloc = function let codegen_def' ctx = function | CDEF_reg_dec (id, ctyp, _) -> string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline - ^^ string (Printf.sprintf "%s%s %s;" (if !opt_static then "static " else "") (sgen_ctyp ctyp) (sgen_id id)) + ^^ string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id)) | CDEF_spec (id, _, arg_ctyps, ret_ctyp) -> - let static = if !opt_static then "static " else "" in if Env.is_extern id ctx.tc_env "c" then empty else if is_stack_ctyp ret_ctyp then - string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%s%s %s(%s%s);" (static ()) (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) else - string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) + string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" (static ()) (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)) | CDEF_fundef (id, ret_arg, args, instrs) as def -> let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with @@ -2100,8 +2100,7 @@ let codegen_def' ctx = function codegen_type_def ctx ctype_def | CDEF_startup (id, instrs) -> - let static = if !opt_static then "static " else "" in - let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" static (sgen_function_id id)) in + let startup_header = string (Printf.sprintf "%svoid startup_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl instrs ^^ twice hardline ^^ startup_header ^^ hardline @@ -2110,8 +2109,7 @@ let codegen_def' ctx = function ^^ string "}" | CDEF_finish (id, instrs) -> - let static = if !opt_static then "static " else "" in - let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" static (sgen_function_id id)) in + let finish_header = string (Printf.sprintf "%svoid finish_%s(void)" (static ()) (sgen_function_id id)) in separate_map hardline codegen_decl (List.filter is_decl instrs) ^^ twice hardline ^^ finish_header ^^ hardline @@ -2127,8 +2125,7 @@ let codegen_def' ctx = function let cleanup = List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings) in - let static = if !opt_static then "static " else "" in - separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" static (sgen_ctyp ctyp) (sgen_id id))) bindings + separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id))) bindings ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number) ^^ string "{" ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline @@ -2315,7 +2312,7 @@ let compile_ast env output_chan c_includes ast = in let model_default_main = - ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (if !opt_static then "static " else ""); + ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (static ()); "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; -- cgit v1.2.3 From a2ddd7d0fb1f1c3b6ac0d7bd360ff9a6f9d728dc Mon Sep 17 00:00:00 2001 From: Alex Richardson Date: Fri, 15 May 2020 16:26:37 +0100 Subject: C backend: Only add static to model_{init,fini} if -static is passed Otherwise the C emulator doesn't build. --- src/jib/c_backend.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 4527aaa1..b1d6cc40 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2289,7 +2289,7 @@ let compile_ast env output_chan c_includes ast = in let model_init = separate hardline (List.map string - ( [ "static void model_init(void)"; + ( [ Printf.sprintf "%svoid model_init(void)" (static ()); "{"; " setup_rts();" ] @ fst exn_boilerplate @@ -2301,7 +2301,7 @@ let compile_ast env output_chan c_includes ast = in let model_fini = separate hardline (List.map string - ( [ "static void model_fini(void)"; + ( [ Printf.sprintf "%svoid model_fini(void)" (static ()); "{" ] @ letbind_finalizers @ List.concat (List.map (fun r -> snd (register_init_clear r)) regs) -- cgit v1.2.3