From 28b054b28a5dc32bb927e7093690f4fe74d65426 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 28 Jun 2018 14:18:16 +0100
Subject: Add option to build ocaml with bisect_ppx coverage support. Add cheri
 targets using this.

---
 src/ocaml_backend.ml | 11 +++++++++--
 src/sail.ml          |  4 +++-
 2 files changed, 12 insertions(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index 369a325c..5ffb1647 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -60,6 +60,7 @@ module Big_int = Nat_big_num
 let opt_trace_ocaml = ref false
 (* Option to not build generated ocaml by default *)
 let opt_ocaml_nobuild = ref false
+let opt_ocaml_coverage = ref false
 
 type ctx =
   { register_inits : tannot exp list;
@@ -704,8 +705,11 @@ let ocaml_compile spec defs =
   let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/elf_loader.ml .") in
   let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/sail_lib.ml .") in
   let _ = Unix.system ("cp -r " ^ sail_dir ^ "/src/util.ml .") in
-  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/_tags .") in
+  let tags_file = if !opt_ocaml_coverage then "_tags_coverage" else "_tags" in
+  let _ = Unix.system ("cp -r " ^ sail_dir ^ "/lib/" ^ tags_file ^ " _tags") in
   let out_chan = open_out (spec ^ ".ml") in
+  if !opt_ocaml_coverage then 
+    ignore(Unix.system ("cp -r " ^ sail_dir ^ "/lib/myocamlbuild_coverage.ml myocamlbuild.ml"));
   ocaml_pp_defs out_chan defs;
   close_out out_chan;
   if IdSet.mem (mk_id "main") (Initial_check.val_spec_ids defs)
@@ -716,7 +720,10 @@ let ocaml_compile spec defs =
       output_string out_chan (ocaml_main spec sail_dir);
       close_out out_chan;
       if not !opt_ocaml_nobuild then (
-        system_checked "ocamlbuild -use-ocamlfind main.native";
+        if !opt_ocaml_coverage then
+          system_checked "BISECT_COVERAGE=YES ocamlbuild -use-ocamlfind -plugin-tag 'package(bisect_ppx-ocamlbuild)' main.native"
+        else
+          system_checked "ocamlbuild -use-ocamlfind main.native";
         ignore (Unix.system ("cp main.native " ^ cwd ^ "/" ^ spec))
       )
     end
diff --git a/src/sail.ml b/src/sail.ml
index a933ce59..046445d1 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -62,7 +62,6 @@ let opt_print_verbose = ref false
 let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
 let opt_print_ocaml = ref false
-let opt_ocaml_nobuild = ref false
 let opt_print_c = ref false
 let opt_print_latex = ref false
 let opt_print_coq = ref false
@@ -97,6 +96,9 @@ let options = Arg.align ([
   ( "-ocaml_trace",
     Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen; Arg.Set Ocaml_backend.opt_trace_ocaml],
     " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml");
+  ( "-ocaml-coverage",
+    Arg.Set Ocaml_backend.opt_ocaml_coverage,
+    "Build ocaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx).");
   ( "-latex",
     Arg.Set opt_print_latex,
     " pretty print the input to latex");
-- 
cgit v1.2.3