From 3f0b6f6d800ee86721121947566d43466c00cf07 Mon Sep 17 00:00:00 2001
From: Alasdair <alasdair.armstrong@cl.cam.ac.uk>
Date: Wed, 24 Apr 2024 18:31:29 +0100
Subject: [PATCH] Remove the need for the HAVE_COVERAGE check

Have the compiler generate a hook function that is either NULL or
calls the coverage function the runtime wants to use, depending on
whether coverage is enabled or not.
---
 lib/rts.c                       | 15 +++++++--------
 src/sail_c_backend/c_backend.ml | 15 ++++++++++++++-
 test/sailcov/run_tests.py       |  2 +-
 3 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/lib/rts.c b/lib/rts.c
index 7ddc7f2c8..466ff794e 100644
--- a/lib/rts.c
+++ b/lib/rts.c
@@ -71,9 +71,6 @@
 #include <sys/types.h>
 
 #include "sail.h"
-#ifdef HAVE_COVERAGE
-#include "sail_coverage.h"
-#endif
 #include "rts.h"
 #include "elf.h"
 
@@ -81,6 +78,8 @@
 extern "C" {
 #endif
 
+extern void sail_rts_set_coverage_file(char *output_file);
+
 static uint64_t g_elf_entry;
 uint64_t g_cycle_count = 0;
 static uint64_t g_cycle_limit;
@@ -726,11 +725,11 @@ int process_arguments(int argc, char *argv[])
       break;
 
     case 'c':
-#ifdef HAVE_COVERAGE
-      sail_set_coverage_file(optarg);
-#else
-      fprintf(stderr, "Ignoring flag -c %s. Requires sail arg: -c_include sail_coverage.h\n", optarg);
-#endif
+      if (&sail_rts_set_coverage_file) {
+        sail_rts_set_coverage_file(optarg);
+      } else {
+        fprintf(stderr, "Ignoring flag -c %s. Requires the model to be compiled with coverage\n", optarg);
+      }
       break;
 
     case 'v':
diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml
index 7e10f4b59..8b6604fc7 100644
--- a/src/sail_c_backend/c_backend.ml
+++ b/src/sail_c_backend/c_backend.ml
@@ -2005,11 +2005,24 @@ let compile_ast env effect_info output_chan c_includes ast =
 
     let docs = separate_map (hardline ^^ hardline) (codegen_def ctx) cdefs in
 
+    let coverage_include =
+      let header = string "#include \"sail_coverage.h\"" in
+      (* Generate a hook for the RTS to call if we have coverage
+         enabled, so it can set the output file with an option. *)
+      let coverage_hook =
+        string "void sail_rts_set_coverage_file(char *output_file) { sail_set_coverage_file(output_file); }"
+      in
+      let no_coverage_hook = string "void (*sail_rts_set_coverage_file)(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]
+    in
+
     let preamble =
       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 Option.is_some !opt_branch_coverage then [string "#include \"sail_coverage.h\""] else [])
+        @ coverage_include
         @ List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) c_includes
         @ [string "#ifdef __cplusplus"; string "extern \"C\" {"; string "#endif"]
         )
diff --git a/test/sailcov/run_tests.py b/test/sailcov/run_tests.py
index 3fdd98fbf..72c5de42b 100755
--- a/test/sailcov/run_tests.py
+++ b/test/sailcov/run_tests.py
@@ -39,7 +39,7 @@ def test_sailcov():
             tests[filename] = os.fork()
             if tests[filename] == 0:
                 step('{} -no_warn -no_memo_z3 -c -c_include sail_coverage.h -c_coverage {}.branches {} -o {}'.format(sail, basename, filename, basename))
-                step('cc -DHAVE_COVERAGE {}.c {}/lib/*.c {}/lib/coverage/libsail_coverage.a -lgmp -lz -lpthread -ldl -I {}/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename))
+                step('cc {}.c {}/lib/*.c {}/lib/coverage/libsail_coverage.a -lgmp -lz -lpthread -ldl -I {}/lib -o {}.bin'.format(basename, sail_dir, sail_dir, sail_dir, basename))
                 step('./{}.bin -c {}.taken'.format(basename, basename))
                 step('{} --all {}.branches --taken {}.taken {}'.format(sailcov, basename, basename, filename))
                 step('diff {}.html {}.expect'.format(basename, basename))