Skip to content

Commit

Permalink
Remove the need for the HAVE_COVERAGE check
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Alasdair committed Apr 25, 2024
1 parent 8230bdf commit cf808ff
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 10 deletions.
15 changes: 7 additions & 8 deletions lib/rts.c
Original file line number Diff line number Diff line change
Expand Up @@ -71,16 +71,15 @@
#include <sys/types.h>

#include "sail.h"
#ifdef HAVE_COVERAGE
#include "sail_coverage.h"
#endif
#include "rts.h"
#include "elf.h"

#ifdef __cplusplus
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;
Expand Down Expand Up @@ -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':
Expand Down
15 changes: 14 additions & 1 deletion src/sail_c_backend/c_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
)
Expand Down
2 changes: 1 addition & 1 deletion test/sailcov/run_tests.py
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down

0 comments on commit cf808ff

Please sign in to comment.