Use output file for generated branch information.

6 files changed, 39 insertions, 36 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 823925a2..9dedb830 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -69,7 +69,7 @@ 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 false
+let opt_branch_coverage = ref None
                         
 let extra_params () =
   match !opt_extra_params with
@@ -166,7 +166,7 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) =
   | L_false -> Some (V_lit (VL_bool false, CT_bool))
   | _ -> None
  
-module C_config(Opts : sig val branch_coverage : bool end) : Config = struct
+module C_config(Opts : sig val branch_coverage : out_channel option end) : Config = struct
   
   (** Convert a sail type into a C-type. This function can be quite
      slow, because it uses ctx.local_env and SMT to analyse the Sail
@@ -2244,7 +2244,7 @@ let compile_ast env output_chan c_includes ast =
                       @ (if !opt_no_rts then [] else
                            [ string "#include \"rts.h\"";
                              string "#include \"elf.h\"" ])
-                      @ (if !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else [])
+                      @ (if Util.is_some !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else [])
                       @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes))
     in
 
@@ -2316,7 +2316,7 @@ let compile_ast env output_chan c_includes ast =
          "  if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
          Printf.sprintf "  %s(UNIT);" (sgen_function_id (mk_id "main"));
          "  model_fini();" ]
-       @ (if !opt_branch_coverage then
+       @ (if Util.is_some !opt_branch_coverage then
             [ "  if (sail_coverage_exit() != 0) {";
               "    fprintf(stderr, \"Could not write coverage information\\n\");";
               "    exit(EXIT_FAILURE);";
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index b10e53d3..5f2d5211 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -88,7 +88,7 @@ val opt_prefix : string ref
 val opt_extra_params : string option ref
 val opt_extra_arguments : string option ref
 
-val opt_branch_coverage : bool ref
+val opt_branch_coverage : out_channel option ref
   
 (** Optimization flags *)
 
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 9a07d365..5e234eae 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -178,7 +178,7 @@ module type Config = sig
   val ignore_64 : bool
   val struct_value : bool
   val use_real : bool
-  val branch_coverage : bool
+  val branch_coverage : out_channel option
   val track_throw : bool
 end
 
@@ -210,40 +210,43 @@ let coverage_branch_reached l =
   let branch_id = !coverage_branch_count in
   incr coverage_branch_count;
   branch_id,
-  if C.branch_coverage then
-    begin match coverage_loc_args l with
-    | None -> []
-    | Some args ->
-       [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)]
-    end
-  else
-    []
+  (match C.branch_coverage with
+   | Some _ ->
+      begin match coverage_loc_args l with
+      | None -> []
+      | Some args ->
+         [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)]
+      end
+   | _ -> []
+  )
 
 let append_into_block instrs instr =
   match instrs with
   | [] -> instr
   | _ -> iblock (instrs @ [instr])
-  
+
 let coverage_branch_taken branch_id (AE_aux (_, _, l)) =
-  if not C.branch_coverage then
-    []
-  else
-    match coverage_loc_args l with
-    | None -> []
-    | Some args ->
-       print_endline ("B " ^ args);
-       [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)]
+  match C.branch_coverage with
+  | None -> []
+  | Some out -> begin
+     match coverage_loc_args l with
+     | None -> []
+     | Some args ->
+        Printf.fprintf out "%s\n" ("B " ^ args);
+        [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)]
+    end
 
 let coverage_function_entry id l =
-  if not C.branch_coverage then
-    []
-  else
-    match coverage_loc_args l with
-    | None -> []
-    | Some args ->
-       print_endline ("F " ^ args);
-       [iraw (Printf.sprintf "sail_function_entry(\"%s\", %s);" (string_of_id id) args)]
-       
+  match C.branch_coverage with
+  | None -> []
+  | Some out -> begin
+     match coverage_loc_args l with
+     | None -> []
+     | Some args ->
+        Printf.fprintf out "%s\n" ("F " ^ args);
+        [iraw (Printf.sprintf "sail_function_entry(\"%s\", %s);" (string_of_id id) args)]
+    end
+
 let rec compile_aval l ctx = function
   | AV_cval (cval, typ) ->
      let ctyp = cval_ctyp cval in
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 47ca6962..3756e58a 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -113,7 +113,7 @@ module type Config = sig
   (** Allow real literals *)
   val use_real : bool
   (** Insert branch coverage operations *)
-  val branch_coverage : bool
+  val branch_coverage : out_channel option
   (** If true track the location of the last exception thrown, useful
      for debugging C but we want to turn it off for SMT generation
      where we can't use strings *)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 26509a69..359704b0 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1584,7 +1584,7 @@ let unroll_static_foreach ctx = function
   let unroll_loops = Some Opts.unroll_limit
   let struct_value = true
   let use_real = true
-  let branch_coverage = false
+  let branch_coverage = None
   let track_throw = false
 end
 
diff --git a/src/sail.ml b/src/sail.ml
index 75adcd9c..b537705c 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -233,8 +233,8 @@ let options = Arg.align ([
     Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str),
     " remove comma separated list of functions from C output, replacing them with unit");
   ( "-c_coverage",
-    Arg.Set C_backend.opt_branch_coverage,
-    " instrument C code to track branch coverage");
+    Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)),
+    " output file for C code instrumention to track branch coverage");
   ( "-elf",
     Arg.String (fun elf -> opt_process_elf := Some elf),
     " process an ELF file so that it can be executed by compiled C code");