From 89c0c1c451a2adac9a5b57b38c1fac97f5a0fe02 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 6 Feb 2025 01:17:35 +0000 Subject: [PATCH 1/2] C: Refactor some C backend options --- src/sail_c_backend/c_backend.ml | 33 ++++++++++++------------ src/sail_c_backend/c_backend.mli | 39 ++++++++++++++++++----------- src/sail_c_backend/sail_plugin_c.ml | 28 ++++++++++++++++----- 3 files changed, 63 insertions(+), 37 deletions(-) diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index d34a573a9..8bba4e727 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -63,13 +63,10 @@ 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 let opt_prefix = ref "z" let opt_extra_params = ref None let opt_extra_arguments = ref None -let opt_branch_coverage = ref None let extra_params () = match !opt_extra_params with Some str -> str ^ ", " | _ -> "" @@ -78,7 +75,6 @@ let extra_arguments is_extern = match !opt_extra_arguments with Some str when no (* Optimization flags *) let optimize_primops = ref false let optimize_hoist_allocations = ref false -let optimize_struct_updates = ref false let optimize_alias = ref false let optimize_fixed_int = ref false let optimize_fixed_bits = ref false @@ -872,14 +868,13 @@ let combine_variables = visit_cdefs (new Combine_variables.visitor) let concatMap f xs = List.concat (List.map f xs) -let optimize recursive_functions cdefs = +let optimize ~have_rts recursive_functions cdefs = let nothing cdefs = cdefs in cdefs |> (if !optimize_alias then concatMap remove_alias else nothing) |> (if !optimize_alias then combine_variables else nothing) (* We need the runtime to initialize hoisted allocations *) - |> - if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations recursive_functions) else nothing + |> if !optimize_hoist_allocations && have_rts then concatMap (hoist_allocations recursive_functions) else nothing (**************************************************************************) (* 6. Code generation *) @@ -2129,6 +2124,10 @@ module type CODEGEN_CONFIG = sig val generate_header : bool val includes : string list val header_includes : string list + val no_main : bool + val no_lib : bool + val no_rts : bool + val branch_coverage : out_channel option end module Codegen (Config : CODEGEN_CONFIG) = struct @@ -2152,7 +2151,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct let jib_of_ast env effect_info ast = let module Jibc = Make (C_config (struct - let branch_coverage = !opt_branch_coverage + let branch_coverage = Config.branch_coverage end)) in let env, effect_info = add_special_functions env effect_info in let ctx = initial_ctx env effect_info in @@ -2165,7 +2164,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct let cdefs = insert_heap_returns Bindings.empty cdefs in let recursive_functions = get_recursive_functions cdefs in - let cdefs = optimize recursive_functions cdefs in + let cdefs = optimize ~have_rts:(not Config.no_rts) recursive_functions cdefs in let header_doc_opt, docs = List.map (codegen_def ctx) cdefs |> List.concat |> merge_file_docs in @@ -2175,15 +2174,15 @@ module Codegen (Config : CODEGEN_CONFIG) = struct enabled, so it can set the output file with an option. *) let coverage_hook = string "void (*sail_rts_set_coverage_file)(const char *) = &sail_set_coverage_file;" in let no_coverage_hook = string "void (*sail_rts_set_coverage_file)(const char *) = NULL;" in - match !opt_branch_coverage with - | Some _ -> if !opt_no_rts then ([header], []) else ([header], [coverage_hook]) - | None -> if !opt_no_rts then ([], []) else ([], [no_coverage_hook]) + match Config.branch_coverage with + | Some _ -> if Config.no_rts then ([header], []) else ([header], [coverage_hook]) + | None -> if Config.no_rts then ([], []) else ([], [no_coverage_hook]) in let preamble in_header = separate hardline - ((if !opt_no_lib then [] else [string "#include \"sail.h\""]) - @ (if !opt_no_rts then [] else [string "#include \"rts.h\""; string "#include \"elf.h\""]) + ((if Config.no_lib then [] else [string "#include \"sail.h\""]) + @ (if Config.no_rts then [] else [string "#include \"rts.h\""; string "#include \"elf.h\""]) @ coverage_include @ ( if in_header then List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) Config.header_includes else List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) Config.includes @@ -2265,7 +2264,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct let model_pre_exit = (["void model_pre_exit()"; "{"] @ - if Option.is_some !opt_branch_coverage then + if Option.is_some Config.branch_coverage then [ " if (sail_coverage_exit() != 0) {"; " fprintf(stderr, \"Could not write coverage information\\n\");"; @@ -2300,7 +2299,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct cdefs in separate hardline - ( if !opt_no_main then [] + ( if Config.no_main then [] else List.map string (["int main(int argc, char *argv[])"; "{"] @ extra @ [" return model_main(argc, argv);"; "}"]) @@ -2319,7 +2318,7 @@ module Codegen (Config : CODEGEN_CONFIG) = struct (preamble false ^^ (if Config.generate_header then hardline ^^ Printf.ksprintf string "#include \"%s.h\"" basename else empty) ^^ hlhl ^^ docs ^^ hlhl - ^^ ( if not !opt_no_rts then + ^^ ( if not Config.no_rts then model_init ^^ hlhl ^^ model_fini ^^ hlhl ^^ model_pre_exit ^^ hlhl ^^ model_default_main ^^ hlhl else empty ) diff --git a/src/sail_c_backend/c_backend.mli b/src/sail_c_backend/c_backend.mli index 9899e05fa..b6bb7fd49 100644 --- a/src/sail_c_backend/c_backend.mli +++ b/src/sail_c_backend/c_backend.mli @@ -54,17 +54,6 @@ open Type_check (** Define generated functions as static *) val opt_static : bool ref -(** Do not generate a main function *) -val opt_no_main : bool ref - -(** Do not include rts.h (the runtime), and do not generate code - that requires any setup or teardown routines to be run by a runtime - before executing any instruction semantics. *) -val opt_no_rts : bool ref - -(** Do not include sail.h by default *) -val opt_no_lib : bool ref - (** Ordinarily we use plain z-encoding to name-mangle generated Sail identifiers into a form suitable for C. If opt_prefix is set, then the "z" which is added on the front of each generated C function @@ -87,21 +76,43 @@ val opt_extra_params : string option ref val opt_extra_arguments : string option ref -val opt_branch_coverage : out_channel option ref - (** Optimization flags *) val optimize_primops : bool ref val optimize_hoist_allocations : bool ref -val optimize_struct_updates : bool ref val optimize_alias : bool ref val optimize_fixed_int : bool ref val optimize_fixed_bits : bool ref module type CODEGEN_CONFIG = sig + (** If this is true, then we will generate a separate header file, + otherwise a single C file will be generated without a header + file. *) val generate_header : bool + + (** A list of includes for the generated C file *) val includes : string list + + (** A list of includes for the generated header (if it is + created). *) val header_includes : string list + + (** Do not generate a main function *) + val no_main : bool + + (** Do not include sail.h automatically *) + val no_lib : bool + + (** Do not include rts.h (the runtime), and do not generate code + that requires any setup or teardown routines to be run by a runtime + before executing any instruction semantics. *) + val no_rts : bool + + (** If [Some channel], the generated C code will be instrumented to + track branch coverage information. Information about all the + possible branches will be written to the provided output + channel. *) + val branch_coverage : out_channel option end module Codegen (Config : CODEGEN_CONFIG) : sig diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml index e1e0d5410..56883b405 100644 --- a/src/sail_c_backend/sail_plugin_c.ml +++ b/src/sail_c_backend/sail_plugin_c.ml @@ -48,13 +48,19 @@ open Libsail open Interactive.State +let opt_branch_coverage = ref None +let opt_build = ref false let opt_generate_header = ref false let opt_includes_c : string list ref = ref [] let opt_includes_h : string list ref = ref [] +let opt_no_lib = ref false +let opt_no_main = ref false +let opt_no_rts = ref false let opt_specialize_c = ref false let c_options = [ + (Flag.create ~prefix:["c"] "build", Arg.Set opt_build, "build the generated C output automatically"); ( Flag.create ~prefix:["c"] ~arg:"filename" "include", Arg.String (fun i -> opt_includes_c := i :: !opt_includes_c), "provide additional include for C output" @@ -63,10 +69,10 @@ let c_options = Arg.String (fun i -> opt_includes_c := i :: !opt_includes_h), "provide additional include for C header output" ); - (Flag.create ~prefix:["c"] "no_main", Arg.Set C_backend.opt_no_main, "do not generate the main() function"); - (Flag.create ~prefix:["c"] "no_rts", Arg.Set C_backend.opt_no_rts, "do not include the Sail runtime"); + (Flag.create ~prefix:["c"] "no_main", Arg.Set opt_no_main, "do not generate the main() function"); + (Flag.create ~prefix:["c"] "no_rts", Arg.Set opt_no_rts, "do not include the Sail runtime"); ( Flag.create ~prefix:["c"] "no_lib", - Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts], + Arg.Tuple [Arg.Set opt_no_lib; Arg.Set opt_no_rts], "do not include the Sail runtime or library" ); ( Flag.create ~prefix:["c"] ~arg:"prefix" "prefix", @@ -92,7 +98,7 @@ let c_options = "remove comma separated list of functions from C output, replacing them with unit" ); ( Flag.create ~prefix:["c"] ~arg:"file" "coverage", - Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)), + Arg.String (fun str -> opt_branch_coverage := Some (open_out str)), "Turn on coverage tracking and output information about all branches and functions to a file" ); ( Flag.create ~prefix:["c"] ~hide_prefix:true "O", @@ -101,7 +107,6 @@ let c_options = Arg.Set C_backend.optimize_primops; Arg.Set C_backend.optimize_hoist_allocations; Arg.Set Initial_check.opt_fast_undefined; - Arg.Set C_backend.optimize_struct_updates; Arg.Set C_backend.optimize_alias; ], "turn on optimizations for C compilation" @@ -151,11 +156,15 @@ let c_rewrites = ("constant_fold", [String_arg "c"]); ] -let c_target out_file { ast; effect_info; env; _ } = +let c_target out_file { ast; effect_info; env; default_sail_dir; _ } = let module Codegen = C_backend.Codegen (struct let generate_header = !opt_generate_header let includes = !opt_includes_c let header_includes = !opt_includes_h + let no_main = !opt_no_main + let no_lib = !opt_no_lib + let no_rts = !opt_no_rts + let branch_coverage = !opt_branch_coverage end) in Reporting.opt_warnings := true; let echo_output, basename = match out_file with Some f -> (false, f) | None -> (true, "out") in @@ -182,6 +191,13 @@ let c_target out_file { ast; effect_info; env; _ } = option to specify a file name"; output_string stdout impl; flush stdout + ); + + if !opt_build then ( + let sail_dir = Reporting.get_sail_dir default_sail_dir in + let cmd = Printf.sprintf "%s -lgmp -I '%s'/lib '%s'/lib/*.c %s.c -o %s" "gcc" sail_dir sail_dir basename basename in + let _ = Unix.system cmd in + () ) let _ = Target.register ~name:"c" ~options:c_options ~rewrites:c_rewrites ~supports_abstract_types:true c_target From cf64dc0aa801a2c303b1099a8ceadd4005261d80 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Tue, 11 Feb 2025 15:08:11 +0000 Subject: [PATCH 2/2] Tests: Thread expected_status through step_with_status --- test/sailtest.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/sailtest.py b/test/sailtest.py index cfac22451..e830965ca 100644 --- a/test/sailtest.py +++ b/test/sailtest.py @@ -131,7 +131,7 @@ def step_with_status(string, expected_status=0, cwd=None): return status def step(string, expected_status=0, cwd=None): - if step_with_status(string, cwd=cwd) != expected_status: + if step_with_status(string, expected_status=expected_status, cwd=cwd) != expected_status: sys.exit(1) def banner(string):