Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[CN-Test-Gen] Coverage, --only and disabling passes #715

Merged
merged 3 commits into from
Nov 12, 2024
Merged

[CN-Test-Gen] Coverage, --only and disabling passes #715

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
da42bd8
[CN-Test-Gen] Coverage support via `lcov`
ZippeyKeys12 Nov 12, 2024
3c0bc9d
[CN-Test-Gen] Support `--only` and `--skip`
ZippeyKeys12 Nov 12, 2024
1d938db
[CN-Test-Gen] Flag for disabling passes
ZippeyKeys12 Nov 12, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
45 changes: 44 additions & 1 deletion backend/cn/bin/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,6 +433,8 @@ let run_tests
without_ownership_checking
(* Test Generation *)
output_dir
only
skip
dont_run
num_samples
max_backtracks
Expand All @@ -446,10 +448,13 @@ let run_tests
exit_fast
max_stack_depth
max_generator_size
coverage
disable_passes
=
(* flags *)
Cerb_debug.debug_level := debug_level;
Pp.print_level := print_level;
Check.skip_and_only := (opt_comma_split skip, opt_comma_split only);
Sym.executable_spec_enabled := true;
let handle_error (e : TypeErrors.type_error) =
let report = TypeErrors.pp_message e.msg in
Expand Down Expand Up @@ -509,7 +514,9 @@ let run_tests
until_timeout;
exit_fast;
max_stack_depth;
max_generator_size
max_generator_size;
coverage;
disable_passes
}
in
TestGeneration.run
Expand Down Expand Up @@ -874,6 +881,16 @@ module Testing_flags = struct
Arg.(required & opt (some string) None & info [ "output-dir" ] ~docv:"FILE" ~doc)


let only =
let doc = "only test this function (or comma-separated names)" in
Arg.(value & opt (some string) None & info [ "only" ] ~doc)


let skip =
let doc = "skip testing of this function (or comma-separated names)" in
Arg.(value & opt (some string) None & info [ "skip" ] ~doc)


let dont_run_tests =
let doc = "Do not run tests, only generate them" in
Arg.(value & flag & info [ "no-run" ] ~doc)
Expand Down Expand Up @@ -969,6 +986,28 @@ module Testing_flags = struct
value
& opt (some int) TestGeneration.default_cfg.max_generator_size
& info [ "max-generator-size" ] ~doc)


let test_coverage =
let doc = "Record coverage of tests" in
Arg.(value & flag & info [ "coverage" ] ~doc)


let disable_passes =
let doc = "skip this optimization pass (or comma-separated names)" in
Arg.(
value
& opt
(list
(enum
[ ("reorder", "reorder");
("picks", "picks");
("flatten", "flatten");
("consistency", "consistency");
("lift_constraints", "lift_constraints")
]))
[]
& info [ "disable" ] ~doc)
end

let testing_cmd =
Expand All @@ -988,6 +1027,8 @@ let testing_cmd =
$ Common_flags.magic_comment_char_dollar
$ Executable_spec_flags.without_ownership_checking
$ Testing_flags.output_test_dir
$ Testing_flags.only
$ Testing_flags.skip
$ Testing_flags.dont_run_tests
$ Testing_flags.gen_num_samples
$ Testing_flags.gen_backtrack_attempts
Expand All @@ -1001,6 +1042,8 @@ let testing_cmd =
$ Testing_flags.test_exit_fast
$ Testing_flags.test_max_stack_depth
$ Testing_flags.test_max_generator_size
$ Testing_flags.test_coverage
$ Testing_flags.disable_passes
in
let doc =
"Generates RapidCheck tests for all functions in [FILE] with CN specifications.\n\
Expand Down
26 changes: 16 additions & 10 deletions backend/cn/lib/check.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2384,24 +2384,27 @@ let c_function_name ((fsym, (_loc, _args_and_body)) : c_function) : string =

(** Filter functions according to [skip_and_only]: first according to "only",
then according to "skip" *)
let select_functions (funs : c_function list) : c_function list =
let select_functions (fsyms : SymSet.t) : SymSet.t =
let matches_str s fsym = String.equal s (Sym.pp_string fsym) in
let str_fsyms s =
match List.filter (matches_str s) (List.map fst funs) with
| [] ->
let ss = SymSet.filter (matches_str s) fsyms in
if SymSet.is_empty ss then (
Pp.warn_noloc (!^"function" ^^^ !^s ^^^ !^"not found");
[]
| ss -> ss
SymSet.empty)
else
ss
in
let strs_fsyms ss =
ss |> List.map str_fsyms |> List.fold_left SymSet.union SymSet.empty
in
let strs_fsyms ss = SymSet.of_list (List.concat_map str_fsyms ss) in
let skip = strs_fsyms (fst !skip_and_only) in
let only = strs_fsyms (snd !skip_and_only) in
let only_funs =
match snd !skip_and_only with
| [] -> funs
| _ss -> List.filter (fun (fsym, _) -> SymSet.mem fsym only) funs
| [] -> fsyms
| _ss -> SymSet.filter (fun fsym -> SymSet.mem fsym only) fsyms
in
List.filter (fun (fsym, _) -> not (SymSet.mem fsym skip)) only_funs
SymSet.filter (fun fsym -> not (SymSet.mem fsym skip)) only_funs


(** Check a single C function. Failure of the check is encoded monadically. *)
Expand Down Expand Up @@ -2464,7 +2467,10 @@ let check_c_functions_all (funs : c_function list) : (string * TypeErrors.t) lis
with the name of the function in which they occurred. When [fail_fast] is
set, the first error encountered will halt checking. *)
let check_c_functions (funs : c_function list) : (string * TypeErrors.t) list m =
let selected_funs = select_functions funs in
let selected_fsyms = select_functions (SymSet.of_list (List.map fst funs)) in
let selected_funs =
List.filter (fun (fsym, _) -> SymSet.mem fsym selected_fsyms) funs
in
match !fail_fast with
| true ->
let@ error_opt = check_c_functions_fast selected_funs in
Expand Down
28 changes: 17 additions & 11 deletions backend/cn/lib/testGeneration/genOptimize.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ module GT = GenTerms
module GS = GenStatements
module GD = GenDefinitions
module GA = GenAnalysis
module Config = TestGenConfig
module SymSet = Set.Make (Sym)
module SymMap = Map.Make (Sym)
module StringSet = Set.Make (String)
Expand Down Expand Up @@ -3453,14 +3454,14 @@ module Specialization = struct
end

let all_passes (prog5 : unit Mucore.file) =
(PartialEvaluation.pass prog5
:: PushPull.pass
:: MemberIndirection.pass
:: Inline.passes)
[ PartialEvaluation.pass prog5 ]
@ (if Config.has_pass "flatten" then [ PushPull.pass ] else [])
@ [ MemberIndirection.pass ]
@ Inline.passes
@ RemoveUnused.passes
@ [ TermSimplification.pass prog5; TermSimplification'.pass; PointerOffsets.pass ]
@ BranchPruning.passes
@ SplitConstraints.passes
@ if Config.has_pass "lift_constraints" then SplitConstraints.passes else []


let optimize_gen (prog5 : unit Mucore.file) (passes : StringSet.t) (gt : GT.t) : GT.t =
Expand Down Expand Up @@ -3496,13 +3497,18 @@ let optimize_gen_def (prog5 : unit Mucore.file) (passes : StringSet.t) (gd : GD.
|> aux
|> Fusion.Each.transform
|> aux
|> FlipIfs.transform
|> (if Config.has_pass "picks" then FlipIfs.transform else fun gd' -> gd')
|> aux
|> Reordering.transform []
|> ConstraintPropagation.transform
|> Specialization.Equality.transform
|> Specialization.Integer.transform
|> Specialization.Pointer.transform
|> (if Config.has_pass "reorder" then Reordering.transform [] else fun gd' -> gd')
|> (if Config.has_pass "consistency" then
fun gd' ->
gd'
|> ConstraintPropagation.transform
|> Specialization.Equality.transform
|> Specialization.Integer.transform
|> Specialization.Pointer.transform
else
fun gd' -> gd')
|> InferAllocationSize.transform
|> aux

Expand Down
131 changes: 96 additions & 35 deletions backend/cn/lib/testGeneration/specTests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,27 +260,27 @@ let compile_assumes
(None, { A.empty_sigma with declarations; function_definitions })


let should_be_unit_test
(sigma : CF.GenTypes.genTypeCategory A.sigma)
(inst : Core_to_mucore.instrumentation)
=
let _, _, decl = List.assoc Sym.equal inst.fn sigma.declarations in
match decl with
| Decl_function (_, _, args, _, _, _) ->
List.is_empty args
&& SymSet.is_empty
(LAT.free_vars (fun _ -> SymSet.empty) (AT.get_lat (Option.get inst.internal)))
| Decl_object _ -> failwith __LOC__


let compile_tests
~(without_ownership_checking : bool)
(filename_base : string)
(sigma : CF.GenTypes.genTypeCategory A.sigma)
(prog5 : unit Mucore.file)
(insts : Core_to_mucore.instrumentation list)
=
let unit_tests, random_tests =
List.partition
(fun (inst : Core_to_mucore.instrumentation) ->
let _, _, decl = List.assoc Sym.equal inst.fn sigma.declarations in
match decl with
| Decl_function (_, _, args, _, _, _) ->
List.is_empty args
&& SymSet.is_empty
(LAT.free_vars
(fun _ -> SymSet.empty)
(AT.get_lat (Option.get inst.internal)))
| Decl_object _ -> failwith __LOC__)
insts
in
let unit_tests, random_tests = List.partition (should_be_unit_test sigma) insts in
let unit_tests_doc = compile_unit_tests unit_tests in
let random_tests_doc = compile_random_tests sigma prog5 random_tests in
let open Pp in
Expand Down Expand Up @@ -366,7 +366,7 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
^^ hardline)
^^ twice hardline
^^ string "TEST_DIR="
^^ string output_dir
^^ string (Filename.dirname (Filename.concat output_dir "junk"))
^^ hardline
^^ twice hardline
^^ string "# Compile"
Expand All @@ -381,7 +381,8 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
"\"-I${RUNTIME_PREFIX}/include/\"";
"-o";
"\"${TEST_DIR}/" ^ Filename.chop_extension test_file ^ ".o\"";
"\"${TEST_DIR}/" ^ test_file ^ "\";";
"\"${TEST_DIR}/" ^ test_file ^ "\"";
(if Config.is_coverage () then "--coverage;" else ";");
"then"
]
^^ nest 4 (hardline ^^ string "echo \"Compiled C files.\"")
Expand All @@ -405,9 +406,11 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
"cc";
"-g";
"\"-I${RUNTIME_PREFIX}/include\"";
"-o \"${TEST_DIR}/tests.out\"";
"-o";
"\"${TEST_DIR}/tests.out\"";
"${TEST_DIR}/" ^ Filename.chop_extension test_file ^ ".o";
"\"${RUNTIME_PREFIX}/libcn.a\";";
"\"${RUNTIME_PREFIX}/libcn.a\"";
(if Config.is_coverage () then "--coverage;" else ";");
"then"
]
^^ nest 4 (hardline ^^ string "echo \"Linked C .o files.\"")
Expand All @@ -429,7 +432,7 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
separate_map
space
string
([ "${TEST_DIR}/tests.out" ]
([ "\"${TEST_DIR}/tests.out\"" ]
@ (Config.has_null_in_every ()
|> Option.map (fun null_in_every ->
[ "--null-in-every"; string_of_int null_in_every ])
Expand Down Expand Up @@ -465,19 +468,68 @@ let compile_script ~(output_dir : string) ~(test_file : string) : Pp.document =
|> Option.to_list
|> List.flatten))
in
string "if"
^^ space
^^ cmd
cmd
^^ semi
^^ space
^^ string "then"
^^ nest 4 (hardline ^^ string "exit 0")
^^ hardline
^^ string "else"
^^ nest 4 (hardline ^^ string "exit 1")
^^ hardline
^^ string "fi"
^^ hardline
^^
if Config.is_coverage () then
string "# Coverage"
^^ hardline
^^ string "test_exit_code=$? # Save tests exit code for later"
^^ twice hardline
^^ string "pushd \"${TEST_DIR}\""
^^ twice hardline
^^ string ("if gcov \"" ^ test_file ^ "\"; then")
^^ nest 4 (hardline ^^ string "echo \"Recorded coverage via gcov.\"")
^^ hardline
^^ string "else"
^^ nest
4
(hardline
^^ string "printf \"Failed to record coverage.\""
^^ hardline
^^ string "exit 1")
^^ hardline
^^ string "fi"
^^ twice hardline
^^ string "if lcov --capture --directory . --output-file coverage.info; then"
^^ nest 4 (hardline ^^ string "echo \"Collected coverage via lcov.\"")
^^ hardline
^^ string "else"
^^ nest
4
(hardline
^^ string "printf \"Failed to collect coverage.\""
^^ hardline
^^ string "exit 1")
^^ hardline
^^ string "fi"
^^ twice hardline
^^ separate_map
space
string
[ "if"; "genhtml"; "--output-directory"; "html"; "\"coverage.info\";"; "then" ]
^^ nest
4
(hardline
^^ string "echo \"Generated HTML report at \\\"${TEST_DIR}/html/\\\".\"")
^^ hardline
^^ string "else"
^^ nest
4
(hardline
^^ string "printf \"Failed to generate HTML report.\""
^^ hardline
^^ string "exit 1")
^^ hardline
^^ string "fi"
^^ twice hardline
^^ string "popd"
^^ twice hardline
^^ string "exit \"$test_exit_code\""
^^ hardline
else
empty


let save ?(perm = 0o666) (output_dir : string) (filename : string) (doc : Pp.document)
Expand Down Expand Up @@ -506,16 +558,25 @@ let generate
:= Some
(let open Stdlib in
open_out "generatorCompilation.log");
let insts = prog5 |> Core_to_mucore.collect_instrumentation |> fst in
let selected_fsyms =
Check.select_functions
(SymSet.of_list
(List.map (fun (inst : Core_to_mucore.instrumentation) -> inst.fn) insts))
in
let insts =
prog5
|> Core_to_mucore.collect_instrumentation
|> fst
insts
|> List.filter (fun (inst : Core_to_mucore.instrumentation) ->
Option.is_some inst.internal)
Option.is_some inst.internal && SymSet.mem inst.fn selected_fsyms)
in
if List.is_empty insts then failwith "No testable functions";
let filename_base = filename |> Filename.basename |> Filename.chop_extension in
let generators_doc = compile_generators sigma prog5 insts in
let generators_doc =
compile_generators
sigma
prog5
(List.filter (fun inst -> not (should_be_unit_test sigma inst)) insts)
in
let generators_fn = filename_base ^ "_gen.h" in
save output_dir generators_fn generators_doc;
let tests_doc =
Expand Down
Loading
Loading