C: Refactor some option handling

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
              )

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

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

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