diff --git a/backend/cn/TESTING.md b/backend/cn/TESTING.md index 7d5971594..ef2078ac2 100644 --- a/backend/cn/TESTING.md +++ b/backend/cn/TESTING.md @@ -12,6 +12,9 @@ This script compiles the C files and runs the tests. By default, running `cn test` will automatically run `run_tests.sh`, which produces a test executable `tests.out`. This can be disabled by using the `--no-run` flag. +The default behavior of testing is to rely on Fulminate for checking, which does not detect undefined behavior. +If you would like to also check for undefined behavior, you can use a sanitizer via `--sanitize=undefined`. + The output directory for these files can be set by using `--output-dir=`. If the directory does not already exist, it is created. diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 7e5a85352..d8e65a41d 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -469,6 +469,7 @@ let run_tests max_unfolds max_array_length with_static_hack + build_tool sanitizers input_timeout null_in_every @@ -518,6 +519,7 @@ let run_tests max_unfolds; max_array_length; with_static_hack; + build_tool; sanitizers; input_timeout; null_in_every; @@ -980,6 +982,14 @@ module Testing_flags = struct Arg.(value & flag & info [ "with-static-hack" ] ~doc) + let build_tool = + let doc = "Set which build tool to use." in + Arg.( + value + & opt (enum TestGeneration.Options.build_tool) TestGeneration.default_cfg.build_tool + & info [ "build-tool" ] ~doc) + + let sanitize = let doc = "Forwarded to the '-fsanitize' argument of the C compiler" in Arg.( @@ -1021,7 +1031,9 @@ module Testing_flags = struct let doc = "Set the logging level for failing inputs from tests" in Arg.( value - & opt (some int) TestGeneration.default_cfg.logging_level + & opt + (some (enum TestGeneration.Options.logging_level)) + TestGeneration.default_cfg.logging_level & info [ "logging-level" ] ~doc) @@ -1029,18 +1041,19 @@ module Testing_flags = struct let doc = "Set the trace granularity for failing inputs from tests" in Arg.( value - & opt (some int) TestGeneration.default_cfg.trace_granularity + & opt + (some (enum TestGeneration.Options.trace_granularity)) + TestGeneration.default_cfg.trace_granularity & info [ "trace-granularity" ] ~doc) let progress_level = - let doc = - "Set the level of detail for progress updates (0 = Quiet, 1 = Per function, 2 = \ - Per test case)" - in + let doc = "Set the frequency of progress updates." in Arg.( value - & opt (some int) TestGeneration.default_cfg.progress_level + & opt + (some (enum TestGeneration.Options.progress_level)) + TestGeneration.default_cfg.progress_level & info [ "progress-level" ] ~doc) @@ -1084,12 +1097,12 @@ module Testing_flags = struct let sizing_strategy = - let doc = - "Strategy for deciding test case size (0 = Uniform, 1 = Quartile, 2 = QuickCheck)" - in + let doc = "Strategy for deciding test case size." in Arg.( value - & opt (some int) TestGeneration.default_cfg.sizing_strategy + & opt + (some (enum TestGeneration.Options.sizing_strategy)) + TestGeneration.default_cfg.sizing_strategy & info [ "sizing-strategy" ] ~doc) @@ -1168,6 +1181,7 @@ let testing_cmd = $ Testing_flags.gen_max_unfolds $ Testing_flags.max_array_length $ Testing_flags.with_static_hack + $ Testing_flags.build_tool $ Term.product Testing_flags.sanitize Testing_flags.no_sanitize $ Testing_flags.input_timeout $ Testing_flags.null_in_every diff --git a/backend/cn/lib/testGeneration/buildScript.ml b/backend/cn/lib/testGeneration/buildScript.ml index 4da04f378..b32b84add 100644 --- a/backend/cn/lib/testGeneration/buildScript.ml +++ b/backend/cn/lib/testGeneration/buildScript.ml @@ -143,17 +143,16 @@ let run () = |> Option.map (fun seed -> [ "--seed"; seed ]) |> Option.to_list |> List.flatten) - @ (Config.has_logging_level () - |> Option.map (fun level -> [ "--logging-level"; string_of_int level ]) + @ (Config.has_logging_level_str () + |> Option.map (fun level -> [ "--logging-level"; level ]) |> Option.to_list |> List.flatten) - @ (Config.has_trace_granularity () - |> Option.map (fun granularity -> - [ "--trace-granularity"; string_of_int granularity ]) + @ (Config.has_trace_granularity_str () + |> Option.map (fun granularity -> [ "--trace-granularity"; granularity ]) |> Option.to_list |> List.flatten) - @ (Config.has_progress_level () - |> Option.map (fun level -> [ "--progress-level"; string_of_int level ]) + @ (Config.has_progress_level_str () + |> Option.map (fun level -> [ "--progress-level"; level ]) |> Option.to_list |> List.flatten) @ (match Config.is_until_timeout () with @@ -173,9 +172,8 @@ let run () = [ "--max-generator-size"; string_of_int max_generator_size ]) |> Option.to_list |> List.flatten) - @ (Config.has_sizing_strategy () - |> Option.map (fun sizing_strategy -> - [ "--sizing-strategy"; string_of_int sizing_strategy ]) + @ (Config.has_sizing_strategy_str () + |> Option.map (fun sizing_strategy -> [ "--sizing-strategy"; sizing_strategy ]) |> Option.to_list |> List.flatten) @ (if Config.is_sized_null () then diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/backend/cn/lib/testGeneration/testGenConfig.ml index 41881afbd..f77562834 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.ml +++ b/backend/cn/lib/testGeneration/testGenConfig.ml @@ -1,3 +1,25 @@ +type build_tool = Bash + +type logging_level = + | None + | Error + | Info + +type trace_granularity = + | None + | End + | All + +type progress_level = + | Silent + | PerFunc + | PerTestCase + +type sizing_strategy = + | Uniform + | Quartile + | QuickCheck + type t = { (* Compile time *) num_samples : int; @@ -5,20 +27,21 @@ type t = max_unfolds : int option; max_array_length : int; with_static_hack : bool; + build_tool : build_tool; sanitizers : string option * string option; (* Run time *) input_timeout : int option; null_in_every : int option; seed : string option; - logging_level : int option; - trace_granularity : int option; - progress_level : int option; + logging_level : logging_level option; + trace_granularity : trace_granularity option; + progress_level : progress_level option; until_timeout : int option; exit_fast : bool; max_stack_depth : int option; allowed_depth_failures : int option; max_generator_size : int option; - sizing_strategy : int option; + sizing_strategy : sizing_strategy option; random_size_splits : bool; allowed_size_split_backtracks : int option; sized_null : bool; @@ -33,6 +56,7 @@ let default = max_unfolds = None; max_array_length = 50; with_static_hack = false; + build_tool = Bash; sanitizers = (None, None); input_timeout = None; null_in_every = None; @@ -55,6 +79,51 @@ let default = } +let string_of_logging_level (logging_level : logging_level) = + match logging_level with None -> "none" | Error -> "error" | Info -> "info" + + +let string_of_trace_granularity (trace_granularity : trace_granularity) = + match trace_granularity with None -> "none" | End -> "end" | All -> "all" + + +let string_of_progress_level (progress_level : progress_level) = + match progress_level with + | Silent -> "silent" + | PerFunc -> "function" + | PerTestCase -> "testcase" + + +let string_of_sizing_strategy (sizing_strategy : sizing_strategy) = + match sizing_strategy with + | Uniform -> "uniform" + | Quartile -> "quartile" + | QuickCheck -> "quickcheck" + + +module Options = struct + let build_tool = [ ("bash", Bash) ] + + let logging_level : (string * logging_level) list = + List.map (fun lvl -> (string_of_logging_level lvl, lvl)) [ None; Error; Info ] + + + let trace_granularity : (string * trace_granularity) list = + List.map (fun gran -> (string_of_trace_granularity gran, gran)) [ None; End; All ] + + + let progress_level : (string * progress_level) list = + List.map + (fun lvl -> (string_of_progress_level lvl, lvl)) + [ Silent; PerFunc; PerTestCase ] + + + let sizing_strategy : (string * sizing_strategy) list = + List.map + (fun strat -> (string_of_sizing_strategy strat, strat)) + [ Uniform; Quartile; QuickCheck ] +end + let instance = ref default let initialize (cfg : t) = instance := cfg @@ -69,6 +138,8 @@ let get_max_array_length () = !instance.max_array_length let with_static_hack () = !instance.with_static_hack +let get_build_tool () = !instance.build_tool + let has_sanitizers () = !instance.sanitizers let has_input_timeout () = !instance.input_timeout @@ -79,10 +150,20 @@ let has_seed () = !instance.seed let has_logging_level () = !instance.logging_level +let has_logging_level_str () = Option.map string_of_logging_level !instance.logging_level + let has_trace_granularity () = !instance.trace_granularity +let has_trace_granularity_str () = + Option.map string_of_trace_granularity !instance.trace_granularity + + let has_progress_level () = !instance.progress_level +let has_progress_level_str () = + Option.map string_of_progress_level !instance.progress_level + + let is_until_timeout () = !instance.until_timeout let is_exit_fast () = !instance.exit_fast @@ -95,6 +176,10 @@ let has_max_generator_size () = !instance.max_generator_size let has_sizing_strategy () = !instance.sizing_strategy +let has_sizing_strategy_str () = + Option.map string_of_sizing_strategy !instance.sizing_strategy + + let is_random_size_splits () = !instance.random_size_splits let has_allowed_size_split_backtracks () = !instance.allowed_size_split_backtracks diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/backend/cn/lib/testGeneration/testGenConfig.mli index f7507aa37..c4873b2fb 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.mli +++ b/backend/cn/lib/testGeneration/testGenConfig.mli @@ -1,3 +1,25 @@ +type build_tool = Bash + +type logging_level = + | None + | Error + | Info + +type trace_granularity = + | None + | End + | All + +type progress_level = + | Silent + | PerFunc + | PerTestCase + +type sizing_strategy = + | Uniform + | Quartile + | QuickCheck + type t = { (* Compile time *) num_samples : int; @@ -5,20 +27,21 @@ type t = max_unfolds : int option; max_array_length : int; with_static_hack : bool; + build_tool : build_tool; sanitizers : string option * string option; (* Run time *) input_timeout : int option; null_in_every : int option; seed : string option; - logging_level : int option; - trace_granularity : int option; - progress_level : int option; + logging_level : logging_level option; + trace_granularity : trace_granularity option; + progress_level : progress_level option; until_timeout : int option; exit_fast : bool; max_stack_depth : int option; allowed_depth_failures : int option; max_generator_size : int option; - sizing_strategy : int option; + sizing_strategy : sizing_strategy option; random_size_splits : bool; allowed_size_split_backtracks : int option; sized_null : bool; @@ -29,6 +52,18 @@ type t = val default : t +module Options : sig + val build_tool : (string * build_tool) list + + val logging_level : (string * logging_level) list + + val trace_granularity : (string * trace_granularity) list + + val progress_level : (string * progress_level) list + + val sizing_strategy : (string * sizing_strategy) list +end + val initialize : t -> unit val get_num_samples : unit -> int @@ -41,6 +76,8 @@ val get_max_array_length : unit -> int val with_static_hack : unit -> bool +val get_build_tool : unit -> build_tool + val has_sanitizers : unit -> string option * string option val has_input_timeout : unit -> int option @@ -49,11 +86,17 @@ val has_null_in_every : unit -> int option val has_seed : unit -> string option -val has_logging_level : unit -> int option +val has_logging_level : unit -> logging_level option + +val has_logging_level_str : unit -> string option -val has_trace_granularity : unit -> int option +val has_trace_granularity : unit -> trace_granularity option -val has_progress_level : unit -> int option +val has_trace_granularity_str : unit -> string option + +val has_progress_level : unit -> progress_level option + +val has_progress_level_str : unit -> string option val is_until_timeout : unit -> int option @@ -65,7 +108,9 @@ val has_allowed_depth_failures : unit -> int option val has_max_generator_size : unit -> int option -val has_sizing_strategy : unit -> int option +val has_sizing_strategy : unit -> sizing_strategy option + +val has_sizing_strategy_str : unit -> string option val is_random_size_splits : unit -> bool diff --git a/backend/cn/lib/testGeneration/testGeneration.ml b/backend/cn/lib/testGeneration/testGeneration.ml index abe4ac061..1760f6987 100644 --- a/backend/cn/lib/testGeneration/testGeneration.ml +++ b/backend/cn/lib/testGeneration/testGeneration.ml @@ -6,6 +6,7 @@ module LAT = LogicalArgumentTypes module CtA = Cn_internal_to_ail module ESpecInternal = Executable_spec_internal module Config = TestGenConfig +module Options = Config.Options type config = Config.t diff --git a/backend/cn/lib/testGeneration/testGeneration.mli b/backend/cn/lib/testGeneration/testGeneration.mli index 2e7b60dea..76c0e481f 100644 --- a/backend/cn/lib/testGeneration/testGeneration.mli +++ b/backend/cn/lib/testGeneration/testGeneration.mli @@ -4,6 +4,8 @@ val default_cfg : config val set_config : config -> unit +module Options = TestGenConfig.Options + val functions_under_test : with_warning:bool -> Cerb_frontend.Cabs.translation_unit -> diff --git a/runtime/libcn/include/cn-testing/test.h b/runtime/libcn/include/cn-testing/test.h index 3a9f8bc64..f11121aea 100644 --- a/runtime/libcn/include/cn-testing/test.h +++ b/runtime/libcn/include/cn-testing/test.h @@ -13,13 +13,13 @@ enum cn_test_gen_progress { CN_TEST_GEN_PROGRESS_ALL = 2 }; -enum cn_gen_size_strategy { +enum cn_gen_sizing_strategy { CN_GEN_SIZE_UNIFORM = 0, CN_GEN_SIZE_QUARTILE = 1, CN_GEN_SIZE_QUICKCHECK = 2 }; -typedef enum cn_test_result cn_test_case_fn(bool replay, enum cn_test_gen_progress, enum cn_gen_size_strategy, bool trap); +typedef enum cn_test_result cn_test_case_fn(bool replay, enum cn_test_gen_progress, enum cn_gen_sizing_strategy, bool trap); void cn_register_test_case(const char* suite, const char* name, cn_test_case_fn* func); @@ -28,7 +28,7 @@ void print_test_info(const char* suite, const char* name, int tests, int discard /** This function is called right before rerunning a failing test case. */ void cn_trap(void); -size_t cn_gen_compute_size(enum cn_gen_size_strategy strategy, int max_tests, size_t max_size, int max_discard_ratio, int successes, int recent_discards); +size_t cn_gen_compute_size(enum cn_gen_sizing_strategy strategy, int max_tests, size_t max_size, int max_discard_ratio, int successes, int recent_discards); #define CN_UNIT_TEST_CASE_NAME(FuncName) cn_test_const_##FuncName @@ -42,7 +42,7 @@ size_t cn_gen_compute_size(enum cn_gen_size_strategy strategy, int max_tests, si enum cn_test_result cn_test_const_##FuncName ( \ bool replay, \ enum cn_test_gen_progress progress_level, \ - enum cn_gen_size_strategy size_strategy, \ + enum cn_gen_sizing_strategy sizing_strategy, \ bool trap \ ) { \ if (setjmp(buf_##FuncName)) { \ @@ -72,7 +72,7 @@ size_t cn_gen_compute_size(enum cn_gen_size_strategy strategy, int max_tests, si enum cn_test_result cn_test_gen_##Name ( \ bool replay, \ enum cn_test_gen_progress progress_level, \ - enum cn_gen_size_strategy size_strategy, \ + enum cn_gen_sizing_strategy sizing_strategy, \ bool trap \ ) { \ cn_gen_rand_checkpoint checkpoint = cn_gen_rand_save(); \ @@ -105,7 +105,7 @@ size_t cn_gen_compute_size(enum cn_gen_size_strategy strategy, int max_tests, si } \ if (!replay) { \ cn_gen_set_size(cn_gen_compute_size( \ - size_strategy, \ + sizing_strategy, \ Samples, \ cn_gen_get_max_size(), \ 10, \ diff --git a/runtime/libcn/src/cn-testing/test.c b/runtime/libcn/src/cn-testing/test.c index eb3df3413..f2a170399 100644 --- a/runtime/libcn/src/cn-testing/test.c +++ b/runtime/libcn/src/cn-testing/test.c @@ -112,7 +112,7 @@ static inline void _cn_trap(void) { __asm__ __volatile__("NOP\n .word 0x10000000 void cn_trap(void) { _cn_trap(); } -size_t cn_gen_compute_size(enum cn_gen_size_strategy strategy, int max_tests, size_t max_size, int max_discard_ratio, int successes, int recent_discards) { +size_t cn_gen_compute_size(enum cn_gen_sizing_strategy strategy, int max_tests, size_t max_size, int max_discard_ratio, int successes, int recent_discards) { switch (strategy) { case CN_GEN_SIZE_QUARTILE: if (successes < max_tests / 4) { @@ -188,7 +188,7 @@ int cn_test_main(int argc, char* argv[]) { int input_timeout = 5000; int exit_fast = 0; int trap = 0; - enum cn_gen_size_strategy sizing_strategy = 0; + enum cn_gen_sizing_strategy sizing_strategy = CN_GEN_SIZE_QUICKCHECK; for (int i = 0; i < argc; i++) { char* arg = argv[i]; @@ -197,15 +197,60 @@ int cn_test_main(int argc, char* argv[]) { i++; } else if (strcmp("--logging-level", arg) == 0) { - logging_level = strtol(argv[i + 1], NULL, 10); + char* next = argv[i + 1]; + if (strcmp("none", next) == 0) { + logging_level = CN_LOGGING_NONE; + } + else if (strcmp("error", next) == 0) { + logging_level = CN_LOGGING_ERROR; + } + else if (strcmp("info", next) == 0) { + logging_level = CN_LOGGING_INFO; + } + else + { + logging_level = strtol(next, NULL, 10); + } + i++; } else if (strcmp("--trace-granularity", arg) == 0) { - set_cn_trace_granularity(strtol(argv[i + 1], NULL, 10)); + enum cn_trace_granularity granularity; + + char* next = argv[i + 1]; + if (strcmp("none", next) == 0) { + granularity = CN_TRACE_NONE; + } + else if (strcmp("ends", next) == 0) { + granularity = CN_TRACE_ENDS; + } + else if (strcmp("all", next) == 0) { + granularity = CN_TRACE_ALL; + } + else + { + granularity = strtol(next, NULL, 10); + } + + set_cn_trace_granularity(granularity); i++; } else if (strcmp("--progress-level", arg) == 0) { - progress_level = strtol(argv[i + 1], NULL, 10); + char* next = argv[i + 1]; + if (strcmp("silent", next) == 0) { + progress_level = CN_TEST_GEN_PROGRESS_NONE; + } + else if (strcmp("function", next) == 0) { + progress_level = CN_TEST_GEN_PROGRESS_FINAL; + } + else if (strcmp("testcase", next) == 0) { + progress_level = CN_TEST_GEN_PROGRESS_ALL; + } + else + { + progress_level = strtol(next, NULL, 10); + } + i++; } else if (strcmp("--input-timeout", arg) == 0) { @@ -248,7 +293,21 @@ int cn_test_main(int argc, char* argv[]) { trap = 1; } else if (strcmp("--sizing-strategy", arg) == 0) { - sizing_strategy = strtoul(argv[i + 1], NULL, 10); + char* next = argv[i + 1]; + if (strcmp("uniform", next) == 0) { + sizing_strategy = CN_GEN_SIZE_UNIFORM; + } + else if (strcmp("quartile", next) == 0) { + sizing_strategy = CN_GEN_SIZE_QUARTILE; + } + else if (strcmp("quickcheck", next) == 0) { + sizing_strategy = CN_GEN_SIZE_QUICKCHECK; + } + else + { + sizing_strategy = strtoul(next, NULL, 10); + } + i++; } } diff --git a/tests/cn-test-gen/.gitignore b/tests/cn-test-gen/.gitignore index bff9cebc8..a1ddebefa 100644 --- a/tests/cn-test-gen/.gitignore +++ b/tests/cn-test-gen/.gitignore @@ -1,3 +1,5 @@ build/ decorated/ test/ +passing-* +failing-* diff --git a/tests/cn-test-gen/run-single-test.sh b/tests/cn-test-gen/run-single-test.sh index 703cb091f..fc0545694 100755 --- a/tests/cn-test-gen/run-single-test.sh +++ b/tests/cn-test-gen/run-single-test.sh @@ -29,7 +29,7 @@ function separator() { OUTPUT="${OUTPUT}\n\n" } -CONFIGS=("--sized-null --sizing-strategy 0" "--coverage --sizing-strategy 1" "--with-static-hack --coverage --sizing-strategy 2" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") +CONFIGS=("--sized-null --sizing-strategy=uniform" "--coverage --sizing-strategy=quartile" "--with-static-hack --coverage --sizing-strategy=quickcheck" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") OUTPUT="" @@ -39,7 +39,7 @@ for CONFIG in "${CONFIGS[@]}"; do OUTPUT="${OUTPUT}Running CI with CLI config \"$CONFIG\"\n" separator - FULL_CONFIG="$CONFIG --input-timeout=1000 --progress-level=1 --sanitize=undefined" + FULL_CONFIG="$CONFIG --input-timeout=1000 --progress-level=function --sanitize=undefined" if [[ $TEST == *.pass.c ]]; then CLEANUP="rm -rf ${DIR} run_tests.sh;separator"