From f7087d217cc4ced67cb062038fa91e51c11743ee Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Wed, 10 May 2023 11:01:56 +0100 Subject: [PATCH] Improve branch coverage output 1. Distinguish between branches (e.g. and entire `match`) and branch targets (each arm of the `match`). This leads to slightly less naming. `sail_branch_taken` was renamed to `sail_branch_target_taken`. 2. Add integer function IDs and branch target IDs. This speeds up coverage collection since you can just look them up in an array rather than hashing the filenames etc (though I haven't changed the existing Rust library to do that). It also allows logging of the control flow (I have a plan to make a post-execution debugger so you can sort of step through the Sail code). 3. Always call `sail_branch_reached()` even if the source code location could not be determined (e.g. because for mapping it could be spread over multiple files). Ideally the source code location would be known for `scattered` definitions, but I don't know enough about the compiler to do that. --- lib/coverage/src/lib.rs | 28 +++++++++------- lib/sail_coverage.h | 6 ++-- src/lib/jib_compile.ml | 74 ++++++++++++++++++++++++----------------- 3 files changed, 62 insertions(+), 46 deletions(-) diff --git a/lib/coverage/src/lib.rs b/lib/coverage/src/lib.rs index 34261eae4..70cb4805c 100644 --- a/lib/coverage/src/lib.rs +++ b/lib/coverage/src/lib.rs @@ -18,21 +18,21 @@ struct Span { } lazy_static! { - static ref BRANCHES: Mutex> = Mutex::new(HashSet::new()); static ref FUNCTIONS: Mutex> = Mutex::new(HashSet::new()); + static ref BRANCH_TARGETS: Mutex> = Mutex::new(HashSet::new()); static ref OUTPUT_FILE: Mutex = Mutex::new("sail_coverage".to_string()); } -fn function_entry(_function_name: &CStr, span: Span) { +fn function_entry(_function_id: i32, _function_name: &CStr, span: Span) { FUNCTIONS.lock().unwrap().insert(span); } -fn branch_taken(_branch_id: i32, span: Span) { - BRANCHES.lock().unwrap().insert(span); -} - fn branch_reached(_branch_id: i32, _span: Span) {} +fn branch_target_taken(_branch_id: i32, _branch_target_id: i32, span: Span) { + BRANCH_TARGETS.lock().unwrap().insert(span); +} + fn write_locations(file: &mut File, kind: char, spans: &Mutex>) -> bool { for span in spans.lock().unwrap().iter() { let res = writeln!( @@ -59,10 +59,10 @@ pub extern "C" fn sail_coverage_exit() -> c_int { .append(true) .open(&*OUTPUT_FILE.lock().unwrap()) { - if !write_locations(&mut file, 'B', &BRANCHES) { + if !write_locations(&mut file, 'F', &FUNCTIONS) { return 1; } - if !write_locations(&mut file, 'F', &FUNCTIONS) { + if !write_locations(&mut file, 'T', &BRANCH_TARGETS) { return 1; } 0 @@ -78,6 +78,7 @@ pub unsafe extern "C" fn sail_set_coverage_file(output_file: *const c_char) { #[no_mangle] pub unsafe extern "C" fn sail_function_entry( + function_id: c_int, function_name: *const c_char, sail_file: *const c_char, l1: c_int, @@ -86,6 +87,7 @@ pub unsafe extern "C" fn sail_function_entry( c2: c_int, ) { function_entry( + function_id as i32, CStr::from_ptr(function_name), Span { sail_file: CStr::from_ptr(sail_file).into(), @@ -98,7 +100,7 @@ pub unsafe extern "C" fn sail_function_entry( } #[no_mangle] -pub unsafe extern "C" fn sail_branch_taken( +pub unsafe extern "C" fn sail_branch_reached( branch_id: c_int, sail_file: *const c_char, l1: c_int, @@ -106,7 +108,7 @@ pub unsafe extern "C" fn sail_branch_taken( l2: c_int, c2: c_int, ) { - branch_taken( + branch_reached( branch_id as i32, Span { sail_file: CStr::from_ptr(sail_file).into(), @@ -119,16 +121,18 @@ pub unsafe extern "C" fn sail_branch_taken( } #[no_mangle] -pub unsafe extern "C" fn sail_branch_reached( +pub unsafe extern "C" fn sail_branch_target_taken( branch_id: c_int, + branch_target_id: c_int, sail_file: *const c_char, l1: c_int, c1: c_int, l2: c_int, c2: c_int, ) { - branch_reached( + branch_target_taken( branch_id as i32, + branch_target_id as i32, Span { sail_file: CStr::from_ptr(sail_file).into(), line1: l1 as i32, diff --git a/lib/sail_coverage.h b/lib/sail_coverage.h index aeb9c65ae..73dfa26d4 100644 --- a/lib/sail_coverage.h +++ b/lib/sail_coverage.h @@ -76,12 +76,12 @@ int sail_coverage_exit(void); void sail_set_coverage_file(const char *output_file); -void sail_function_entry(const char *function_name, const char *sail_file, int l1, int c1, int l2, int c2); - -void sail_branch_taken(int branch_id, const char *sail_file, int l1, int c1, int l2, int c2); +void sail_function_entry(int function_id, const char *function_name, const char *sail_file, int l1, int c1, int l2, int c2); void sail_branch_reached(int branch_id, const char *sail_file, int l1, int c1, int l2, int c2); +void sail_branch_target_taken(int branch_id, int branch_target_id, const char *sail_file, int l1, int c1, int l2, int c2); + #ifdef __cplusplus } #endif diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 4a4ec9aa0..bfbcb86d2 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -275,29 +275,33 @@ module Make (C : CONFIG) = struct let rec chunkify n xs = match (Util.take n xs, Util.drop n xs) with xs, [] -> [xs] | xs, ys -> xs :: chunkify n ys + (* Counters to provide unique IDs for branches, branch targets and functions. *) let coverage_branch_count = ref 0 + let coverage_branch_target_count = ref 0 + let coverage_function_count = ref 0 let coverage_loc_args l = match Reporting.simp_loc l with - | None -> None + (* Scattered definitions may not have a known location but we still want + to measure coverage of them. *) + | None -> "\"\", 0, 0, 0, 0" | Some (p1, p2) -> - Some - (Printf.sprintf "\"%s\", %d, %d, %d, %d" (String.escaped p1.pos_fname) p1.pos_lnum (p1.pos_cnum - p1.pos_bol) - p2.pos_lnum (p2.pos_cnum - p2.pos_bol) - ) + Printf.sprintf "\"%s\", %d, %d, %d, %d" (String.escaped p1.pos_fname) p1.pos_lnum (p1.pos_cnum - p1.pos_bol) + p2.pos_lnum (p2.pos_cnum - p2.pos_bol) + (* A branch is a `match` (including `mapping`), `if` or short-circuiting and/or. + This returns a new ID for the branch, and the C code to call. It also + writes the static branch info to C.branch_coverage. *) let coverage_branch_reached l = - let branch_id = !coverage_branch_count in - incr coverage_branch_count; - ( branch_id, - 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 - | _ -> [] - ) + match C.branch_coverage with + | Some out -> begin + let branch_id = !coverage_branch_count in + incr coverage_branch_count; + let args = coverage_loc_args l in + Printf.fprintf out "%s\n" ("B " ^ string_of_int branch_id ^ ", " ^ args); + (branch_id, [iraw (Printf.sprintf "sail_branch_reached(%d, %s);" branch_id args)]) + end + | _ -> (0, []) let append_into_block instrs instr = match instrs with [] -> instr | _ -> iblock (instrs @ [instr]) @@ -308,26 +312,33 @@ module Make (C : CONFIG) = struct match e with AE_typ (e', _) -> find_aexp_loc e' | _ -> l ) - let coverage_branch_taken branch_id aexp = + (* This is called when an *arm* of a branch is taken. For example if you + have a `match`, it is called for the match arm that is taken. + For `if` without `else` then it may not be called at all. Same for + short-circuiting boolean expressions. `branch_id` is the ID for the entire + conditional expression (the whole `match` etc.). *) + let coverage_branch_target_taken branch_id aexp = match C.branch_coverage with | None -> [] | Some out -> begin - match coverage_loc_args (find_aexp_loc aexp) with - | None -> [] - | Some args -> - Printf.fprintf out "%s\n" ("B " ^ args); - [iraw (Printf.sprintf "sail_branch_taken(%d, %s);" branch_id args)] + let branch_target_id = !coverage_branch_target_count in + incr coverage_branch_target_count; + let args = coverage_loc_args (find_aexp_loc aexp) in + Printf.fprintf out "%s\n" ("T " ^ string_of_int branch_id ^ ", " ^ string_of_int branch_target_id ^ ", " ^ args); + [iraw (Printf.sprintf "sail_branch_target_taken(%d, %d, %s);" branch_id branch_target_id args)] end + (* Generate code and static branch info for function entry coverage. + `id` is the name of the function. *) let coverage_function_entry id l = 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)] + let function_id = !coverage_function_count in + incr coverage_function_count; + let args = coverage_loc_args l in + Printf.fprintf out "%s\n" ("F " ^ string_of_int function_id ^ ", \"" ^ string_of_id id ^ "\", " ^ args); + [iraw (Printf.sprintf "sail_function_entry(%d, \"%s\", %s);" function_id (string_of_id id) args)] end let rec compile_aval l ctx = function @@ -765,7 +776,7 @@ module Make (C : CONFIG) = struct ] else [] ) - @ (if num_cases > 1 then coverage_branch_taken branch_id body else []) + @ (if num_cases > 1 then coverage_branch_target_taken branch_id body else []) @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @@ -775,6 +786,7 @@ module Make (C : CONFIG) = struct ) in ( aval_setup + @ [icomment ("Case with num_cases: " ^ string_of_int num_cases)] @ (if num_cases > 1 then on_reached else []) @ [idecl l ctyp case_return_id] @ List.concat (List.map compile_case cases) @@ -843,7 +855,7 @@ module Make (C : CONFIG) = struct 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 -> coverage_branch_taken branch_id aexp @ setup @ [call clexp] @ cleanup + fun clexp -> coverage_branch_target_taken branch_id aexp @ setup @ [call clexp] @ cleanup in let setup, cval, cleanup = compile_aval l ctx aval in ( setup, @@ -880,7 +892,7 @@ module Make (C : CONFIG) = struct let branch_id, on_reached = coverage_branch_reached l in let left_setup, cval, left_cleanup = compile_aval l ctx aval in let right_setup, call, right_cleanup = compile_aexp ctx aexp in - let right_coverage = coverage_branch_taken branch_id aexp in + let right_coverage = coverage_branch_target_taken branch_id aexp in let gs = ngensym () in ( left_setup @ on_reached @ [ @@ -898,7 +910,7 @@ module Make (C : CONFIG) = struct let branch_id, on_reached = coverage_branch_reached l in let left_setup, cval, left_cleanup = compile_aval l ctx aval in let right_setup, call, right_cleanup = compile_aexp ctx aexp in - let right_coverage = coverage_branch_taken branch_id aexp in + let right_coverage = coverage_branch_target_taken branch_id aexp in let gs = ngensym () in ( left_setup @ on_reached @ [