From da42bd86473576d26ed018d2ac5cfae6f0f7e45c Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Tue, 12 Nov 2024 02:44:23 -0500 Subject: [PATCH 1/3] [CN-Test-Gen] Coverage support via `lcov` --- backend/cn/bin/main.ml | 10 +- backend/cn/lib/testGeneration/specTests.ml | 119 +++++++++++++----- .../cn/lib/testGeneration/testGenConfig.ml | 8 +- .../cn/lib/testGeneration/testGenConfig.mli | 5 +- 4 files changed, 107 insertions(+), 35 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 60fb8a3c1..5b7cf3094 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -446,6 +446,7 @@ let run_tests exit_fast max_stack_depth max_generator_size + coverage = (* flags *) Cerb_debug.debug_level := debug_level; @@ -509,7 +510,8 @@ let run_tests until_timeout; exit_fast; max_stack_depth; - max_generator_size + max_generator_size; + coverage } in TestGeneration.run @@ -969,6 +971,11 @@ 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) end let testing_cmd = @@ -1001,6 +1008,7 @@ let testing_cmd = $ Testing_flags.test_exit_fast $ Testing_flags.test_max_stack_depth $ Testing_flags.test_max_generator_size + $ Testing_flags.test_coverage in let doc = "Generates RapidCheck tests for all functions in [FILE] with CN specifications.\n\ diff --git a/backend/cn/lib/testGeneration/specTests.ml b/backend/cn/lib/testGeneration/specTests.ml index 78127e685..c4a16bbef 100644 --- a/backend/cn/lib/testGeneration/specTests.ml +++ b/backend/cn/lib/testGeneration/specTests.ml @@ -260,6 +260,19 @@ 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) @@ -267,20 +280,7 @@ let compile_tests (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 @@ -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" @@ -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.\"") @@ -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.\"") @@ -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 ]) @@ -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) @@ -515,7 +567,12 @@ let generate 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 = diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/backend/cn/lib/testGeneration/testGenConfig.ml index 94521760b..fbe7b614e 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.ml +++ b/backend/cn/lib/testGeneration/testGenConfig.ml @@ -12,7 +12,8 @@ type t = until_timeout : int option; exit_fast : bool; max_stack_depth : int option; - max_generator_size : int option + max_generator_size : int option; + coverage : bool } let default = @@ -27,7 +28,8 @@ let default = until_timeout = None; exit_fast = false; max_stack_depth = None; - max_generator_size = None + max_generator_size = None; + coverage = false } @@ -58,3 +60,5 @@ let is_exit_fast () = !instance.exit_fast let has_max_stack_depth () = !instance.max_stack_depth let has_max_generator_size () = !instance.max_generator_size + +let is_coverage () = !instance.coverage diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/backend/cn/lib/testGeneration/testGenConfig.mli index e5a52341e..4981fa1c6 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.mli +++ b/backend/cn/lib/testGeneration/testGenConfig.mli @@ -12,7 +12,8 @@ type t = until_timeout : int option; exit_fast : bool; max_stack_depth : int option; - max_generator_size : int option + max_generator_size : int option; + coverage : bool } val default : t @@ -42,3 +43,5 @@ val is_exit_fast : unit -> bool val has_max_stack_depth : unit -> int option val has_max_generator_size : unit -> int option + +val is_coverage : unit -> bool From 3c0bc9d6d55cd74385f10db603347be109819610 Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Tue, 12 Nov 2024 03:42:27 -0500 Subject: [PATCH 2/3] [CN-Test-Gen] Support `--only` and `--skip` --- backend/cn/bin/main.ml | 15 +++++++++++++ backend/cn/lib/check.ml | 26 +++++++++++++--------- backend/cn/lib/testGeneration/specTests.ml | 12 ++++++---- 3 files changed, 39 insertions(+), 14 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 5b7cf3094..beee98df6 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -433,6 +433,8 @@ let run_tests without_ownership_checking (* Test Generation *) output_dir + only + skip dont_run num_samples max_backtracks @@ -451,6 +453,7 @@ let run_tests (* 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 @@ -876,6 +879,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) @@ -995,6 +1008,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 diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml index c9fde5226..d84538a3f 100644 --- a/backend/cn/lib/check.ml +++ b/backend/cn/lib/check.ml @@ -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. *) @@ -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 diff --git a/backend/cn/lib/testGeneration/specTests.ml b/backend/cn/lib/testGeneration/specTests.ml index c4a16bbef..b62bb2487 100644 --- a/backend/cn/lib/testGeneration/specTests.ml +++ b/backend/cn/lib/testGeneration/specTests.ml @@ -558,12 +558,16 @@ 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 From 1d938db989ee2bdaf875899445aa3834b3b46ea3 Mon Sep 17 00:00:00 2001 From: Zain K Aamer Date: Tue, 12 Nov 2024 06:01:44 -0500 Subject: [PATCH 3/3] [CN-Test-Gen] Flag for disabling passes --- backend/cn/bin/main.ml | 22 ++++++++++++++- backend/cn/lib/testGeneration/genOptimize.ml | 28 +++++++++++-------- .../cn/lib/testGeneration/testGenConfig.ml | 8 ++++-- .../cn/lib/testGeneration/testGenConfig.mli | 5 +++- 4 files changed, 48 insertions(+), 15 deletions(-) diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index beee98df6..8bf5f3d13 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -449,6 +449,7 @@ let run_tests max_stack_depth max_generator_size coverage + disable_passes = (* flags *) Cerb_debug.debug_level := debug_level; @@ -514,7 +515,8 @@ let run_tests exit_fast; max_stack_depth; max_generator_size; - coverage + coverage; + disable_passes } in TestGeneration.run @@ -989,6 +991,23 @@ module Testing_flags = struct 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 = @@ -1024,6 +1043,7 @@ let testing_cmd = $ 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\ diff --git a/backend/cn/lib/testGeneration/genOptimize.ml b/backend/cn/lib/testGeneration/genOptimize.ml index f224db9f3..8d9bb4183 100644 --- a/backend/cn/lib/testGeneration/genOptimize.ml +++ b/backend/cn/lib/testGeneration/genOptimize.ml @@ -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) @@ -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 = @@ -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 diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/backend/cn/lib/testGeneration/testGenConfig.ml index fbe7b614e..642d20273 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.ml +++ b/backend/cn/lib/testGeneration/testGenConfig.ml @@ -13,7 +13,8 @@ type t = exit_fast : bool; max_stack_depth : int option; max_generator_size : int option; - coverage : bool + coverage : bool; + disable_passes : string list } let default = @@ -29,7 +30,8 @@ let default = exit_fast = false; max_stack_depth = None; max_generator_size = None; - coverage = false + coverage = false; + disable_passes = [] } @@ -62,3 +64,5 @@ let has_max_stack_depth () = !instance.max_stack_depth let has_max_generator_size () = !instance.max_generator_size let is_coverage () = !instance.coverage + +let has_pass s = not (List.mem String.equal s !instance.disable_passes) diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/backend/cn/lib/testGeneration/testGenConfig.mli index 4981fa1c6..b09ecf0b6 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.mli +++ b/backend/cn/lib/testGeneration/testGenConfig.mli @@ -13,7 +13,8 @@ type t = exit_fast : bool; max_stack_depth : int option; max_generator_size : int option; - coverage : bool + coverage : bool; + disable_passes : string list } val default : t @@ -45,3 +46,5 @@ val has_max_stack_depth : unit -> int option val has_max_generator_size : unit -> int option val is_coverage : unit -> bool + +val has_pass : string -> bool