diff options
| -rw-r--r-- | opam | 2 | ||||
| -rw-r--r-- | src/jib/anf.ml | 2 | ||||
| -rw-r--r-- | src/jib/anf.mli | 4 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 12 | ||||
| -rw-r--r-- | src/jib/jib_compile.ml | 60 | ||||
| -rw-r--r-- | src/jib/jib_compile.mli | 2 | ||||
| -rw-r--r-- | src/jib/jib_smt.ml | 1 | ||||
| -rw-r--r-- | src/reporting.ml | 5 |
8 files changed, 74 insertions, 14 deletions
@@ -36,7 +36,7 @@ depends: [ "conf-gmp" "conf-zlib" "base64" {< "3.0.0"} - "yojson" + "yojson" {>= "1.7.0"} "pprint" ] available: [ocaml-version >= "4.06.1"] diff --git a/src/jib/anf.ml b/src/jib/anf.ml index 6bc447c0..7757cd9a 100644 --- a/src/jib/anf.ml +++ b/src/jib/anf.ml @@ -106,6 +106,8 @@ and 'a aval = | AV_record of ('a aval) Bindings.t * 'a | AV_cval of cval * 'a +let aexp_loc (AE_aux (_, _, l)) = l + (* Renaming variables in ANF expressions *) let rec apat_bindings (AP_aux (apat_aux, _, _)) = diff --git a/src/jib/anf.mli b/src/jib/anf.mli index d01fe146..b96766da 100644 --- a/src/jib/anf.mli +++ b/src/jib/anf.mli @@ -133,8 +133,10 @@ and 'a aval = counter to ensure uniqueness. This function resets that counter. *) val reset_anf_counter : unit -> unit +val aexp_loc : 'a aexp -> Parse_ast.l + (** {2 Functions for transforming ANF expressions} *) - + val aval_typ : typ aval -> typ val aexp_typ : typ aexp -> typ diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 829f4d37..c38749f3 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -165,11 +165,11 @@ let literal_to_fragment (L_aux (l_aux, _) as lit) = | _ -> None module C_config : 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 - types and attempts to fit them into the smallest possible C - types, provided ctx.optimize_smt is true (default) **) + + (** 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 + types and attempts to fit them into the smallest possible C + types, provided ctx.optimize_smt is true (default) **) let rec convert_typ ctx typ = let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in match typ_aux with @@ -562,6 +562,7 @@ module C_config : Config = struct let ignore_64 = false let struct_value = false let use_real = false + let branch_coverage = false end (* When compiling to a C library, we want to do things slightly @@ -656,6 +657,7 @@ module Clib_config : Config = struct let ignore_64 = false let struct_value = false let use_real = false + let branch_coverage = false end (** Functions that have heap-allocated return types are implemented by diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index 1cd7d82a..cd86840b 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -179,6 +179,7 @@ module type Config = sig val ignore_64 : bool val struct_value : bool val use_real : bool + val branch_coverage : bool end module Make(C: Config) = struct @@ -195,6 +196,45 @@ let name_or_global ctx id = global id else name id + +let coverage_branch_count = ref 0 + +let coverage_loc_args l = + match Reporting.simp_loc l with + | None -> + Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation"; + None + | Some (p1, p2) -> + Some (Printf.sprintf "\"%s\", %d, %d, %d, %d" + p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)) + +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 -> + Reporting.simple_warn "Branch found with no location info when inserting coverage instrumentation"; + [] + | Some args -> + [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)] + end + else + [] + +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 -> [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)] let rec compile_aval l ctx = function | AV_cval (cval, typ) -> @@ -628,6 +668,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | AE_case (aval, cases, typ) -> let ctyp = ctyp_of_typ ctx typ in let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in + let branch_id, on_reached = coverage_branch_reached l in let case_return_id = ngensym () in let finish_match_label = label "finish_match_" in let compile_case (apat, guard, body) = @@ -647,7 +688,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) - @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup + @ body_setup + @ coverage_branch_taken branch_id body + @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in if is_dead_aexp body then @@ -655,7 +698,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = else [iblock case_instrs; ilabel case_label] in - aval_setup @ [idecl ctyp case_return_id] + aval_setup @ on_reached @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], @@ -713,16 +756,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = compile_aexp ctx then_aexp else let if_ctyp = ctyp_of_typ ctx if_typ in + let branch_id, on_reached = coverage_branch_reached l in let compile_branch aexp = let setup, call, cleanup = compile_aexp ctx aexp in - fun clexp -> setup @ [call clexp] @ cleanup + fun clexp -> coverage_branch_taken branch_id aexp @ setup @ [call clexp] @ cleanup in let setup, cval, cleanup = compile_aval l ctx aval in setup, - (fun clexp -> iif l cval - (compile_branch then_aexp clexp) - (compile_branch else_aexp clexp) - if_ctyp), + (fun clexp -> + append_into_block on_reached + (iif l cval + (compile_branch then_aexp clexp) + (compile_branch else_aexp clexp) + if_ctyp)), cleanup (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli index a642f29e..98ab44de 100644 --- a/src/jib/jib_compile.mli +++ b/src/jib/jib_compile.mli @@ -117,6 +117,8 @@ module type Config = sig val struct_value : bool (** Allow real literals *) val use_real : bool + (** Insert branch coverage operations *) + val branch_coverage : bool end module Make(C: Config) : sig diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index b662ef41..734f3fe4 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1563,6 +1563,7 @@ let unroll_static_foreach ctx = function let unroll_loops () = Some !opt_unroll_limit let struct_value = true let use_real = true + let branch_coverage = false end diff --git a/src/reporting.ml b/src/reporting.ml index 0029b902..603bc84f 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -127,6 +127,11 @@ let short_loc_to_string l = Printf.sprintf "%s %d:%d - %d:%d" p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol) +let loc_to_coverage l = + match simp_loc l with + | None -> None + | Some (p1, p2) -> Some (p1.pos_fname, p1.pos_cnum - p1.pos_bol, p2.pos_lnum, p2.pos_cnum - p2.pos_bol) + let print_err l m1 m2 = print_err_internal (Loc l) m1 m2 |