diff options
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/c_backend.ml | 8 | ||||
| -rw-r--r-- | src/jib/c_backend.mli | 2 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 57 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 2 |
5 files changed, 37 insertions, 34 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 |