diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml index 0ffdb0d56..816fe8743 100644 --- a/backend/cn/bin/main.ml +++ b/backend/cn/bin/main.ml @@ -73,7 +73,7 @@ let frontend ~macros ~incl_dirs ~incl_files astprints ~filename ~magic_comment_c idents = [ Alloc.History.(str, sym, None) ] } in - let@ _, ail_prog_opt, prog0 = + let@ cabs_tunit_opt, ail_prog_opt, prog0 = c_frontend_and_elaboration ~cn_init_scope (conf, io) (stdlib, impl) ~filename in let@ () = @@ -83,6 +83,7 @@ let frontend ~macros ~incl_dirs ~incl_files astprints ~filename ~magic_comment_c else return () in + let cabs_tunit = Option.get cabs_tunit_opt in let markers_env, ail_prog = Option.get ail_prog_opt in Tags.set_tagDefs prog0.Core.tagDefs; let prog1 = Remove_unspecs.rewrite_file prog0 in @@ -91,7 +92,7 @@ let frontend ~macros ~incl_dirs ~incl_files astprints ~filename ~magic_comment_c let statement_locs = CStatements.search (snd ail_prog) in print_log_file ("original", CORE prog0); print_log_file ("without_unspec", CORE prog1); - return (prog3, (markers_env, ail_prog), statement_locs) + return (cabs_tunit, prog3, (markers_env, ail_prog), statement_locs) let handle_frontend_error = function @@ -132,6 +133,7 @@ let with_well_formedness_check ~(* Callbacks *) handle_error ~(f : + cabs_tunit:CF.Cabs.translation_unit -> prog5:unit Mucore.file -> ail_prog:CF.GenTypes.genTypeCategory A.ail_program -> statement_locs:Cerb_location.t CStatements.LocMap.t -> @@ -139,7 +141,7 @@ let with_well_formedness_check unit Or_TypeError.t) = check_input_file filename; - let prog, (markers_env, ail_prog), statement_locs = + let cabs_tunit, prog, (markers_env, ail_prog), statement_locs = handle_frontend_error (frontend ~macros @@ -169,7 +171,7 @@ let with_well_formedness_check Typing.run_to_pause Context.empty (Check.check_decls_lemmata_fun_specs prog5) in Result.iter_error handle_error (Typing.pause_to_result paused); - f ~prog5 ~ail_prog ~statement_locs ~paused + f ~cabs_tunit ~prog5 ~ail_prog ~statement_locs ~paused in Pp.maybe_close_times_channel (); Result.fold ~ok:(fun () -> exit 0) ~error:handle_error result @@ -250,7 +252,8 @@ let well_formed ~no_inherit_loc ~magic_comment_char_dollar ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace) - ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused:_ -> Or_TypeError.return ()) + ~f:(fun ~cabs_tunit:_ ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused:_ -> + Or_TypeError.return ()) let verify @@ -321,7 +324,7 @@ let verify ~no_inherit_loc ~magic_comment_char_dollar (* Callbacks *) ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace) - ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused -> + ~f:(fun ~cabs_tunit:_ ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused -> let check (functions, global_var_constraints, lemmas) = let open Typing in let@ errors = Check.time_check_c_functions (global_var_constraints, functions) in @@ -413,7 +416,7 @@ let generate_executable_specs ~no_inherit_loc ~magic_comment_char_dollar (* Callbacks *) ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace) - ~f:(fun ~prog5 ~ail_prog ~statement_locs ~paused:_ -> + ~f:(fun ~cabs_tunit:_ ~prog5 ~ail_prog ~statement_locs ~paused:_ -> Cerb_colour.without_colour (fun () -> (try @@ -457,6 +460,7 @@ let run_tests max_backtracks max_unfolds max_array_length + with_static_hack input_timeout null_in_every seed @@ -495,25 +499,45 @@ let run_tests ~no_inherit_loc ~magic_comment_char_dollar (* Callbacks *) ~handle_error - ~f:(fun ~prog5 ~ail_prog ~statement_locs ~paused:_ -> + ~f:(fun ~cabs_tunit ~prog5 ~ail_prog ~statement_locs ~paused:_ -> + let config : TestGeneration.config = + { num_samples; + max_backtracks; + max_unfolds; + max_array_length; + with_static_hack; + input_timeout; + null_in_every; + seed; + logging_level; + progress_level; + interactive; + until_timeout; + exit_fast; + max_stack_depth; + allowed_depth_failures; + max_generator_size; + random_size_splits; + allowed_size_split_backtracks; + sized_null; + coverage; + disable_passes + } + in + TestGeneration.set_config config; + let _, sigma = ail_prog in + if + List.is_empty + (TestGeneration.functions_under_test ~with_warning:true cabs_tunit sigma prog5) + then ( + print_endline "No testable functions, trivially passing"; + exit 0); + if not (Sys.file_exists output_dir) then ( + print_endline ("Directory \"" ^ output_dir ^ "\" does not exist."); + Sys.mkdir output_dir 0o777; + print_endline ("Created directory \"" ^ output_dir ^ "\" with full permissions.")); Cerb_colour.without_colour (fun () -> - if - prog5 - |> Executable_spec_extract.collect_instrumentation - |> fst - |> List.filter (fun (inst : Executable_spec_extract.instrumentation) -> - Option.is_some inst.internal) - |> List.is_empty - then ( - print_endline "No testable functions, trivially passing"; - exit 0); - if not (Sys.file_exists output_dir) then ( - print_endline ("Directory \"" ^ output_dir ^ "\" does not exist."); - Sys.mkdir output_dir 0o777; - print_endline - ("Created directory \"" ^ output_dir ^ "\" with full permissions.")); - let _, sigma = ail_prog in Cn_internal_to_ail.augment_record_map (BaseTypes.Record []); (try Executable_spec.main @@ -528,35 +552,12 @@ let run_tests statement_locs with | e -> handle_error_with_user_guidance ~label:"CN-Exec" e); - let config : TestGeneration.config = - { num_samples; - max_backtracks; - max_unfolds; - max_array_length; - input_timeout; - null_in_every; - seed; - logging_level; - progress_level; - interactive; - until_timeout; - exit_fast; - max_stack_depth; - allowed_depth_failures; - max_generator_size; - random_size_splits; - allowed_size_split_backtracks; - sized_null; - coverage; - disable_passes - } - in (try TestGeneration.run ~output_dir ~filename ~without_ownership_checking - config + cabs_tunit sigma prog5 with @@ -949,6 +950,14 @@ module Testing_flags = struct & info [ "max-array-length" ] ~doc) + let with_static_hack = + let doc = + "(HACK) Use an `#include` instead of linking to build testing. Necessary until \ + https://github.com/rems-project/cerberus/issues/784 or equivalent." + in + Arg.(value & flag & info [ "with-static-hack" ] ~doc) + + let input_timeout = let doc = "Timeout for discarding a generation attempt (ms)" in Arg.( @@ -1104,6 +1113,7 @@ let testing_cmd = $ Testing_flags.gen_backtrack_attempts $ Testing_flags.gen_max_unfolds $ Testing_flags.max_array_length + $ Testing_flags.with_static_hack $ Testing_flags.input_timeout $ Testing_flags.null_in_every $ Testing_flags.seed diff --git a/backend/cn/lib/testGeneration/buildScript.ml b/backend/cn/lib/testGeneration/buildScript.ml index 3aec09b0e..97685cc43 100644 --- a/backend/cn/lib/testGeneration/buildScript.ml +++ b/backend/cn/lib/testGeneration/buildScript.ml @@ -41,7 +41,7 @@ let attempt cmd success failure = ^^ string "fi" -let compile ~test_file = +let compile ~filename_base = string "# Compile" ^^ hardline ^^ attempt @@ -52,22 +52,65 @@ let compile ~test_file = "-c"; "\"-I${RUNTIME_PREFIX}/include/\""; "-o"; - "\"./" ^ Filename.chop_extension test_file ^ ".o\""; - "\"./" ^ test_file ^ "\"" + "\"./" ^ filename_base ^ "_test.o\""; + "\"./" ^ filename_base ^ "_test.c\"" ] @ if Config.is_coverage () then [ "--coverage" ] else [])) - "Compiled C files." - "Failed to compile C files in ${TEST_DIR}." + ("Compiled '" ^ filename_base ^ "_test.c'.") + ("Failed to compile '" ^ filename_base ^ "_test.c' in ${TEST_DIR}.") + ^^ (if Config.with_static_hack () then + empty + else + twice hardline + ^^ attempt + (String.concat + " " + ([ "cc"; + "-g"; + "-c"; + "\"-I${RUNTIME_PREFIX}/include/\""; + "-o"; + "\"./" ^ filename_base ^ "-exec.o\""; + "\"./" ^ filename_base ^ "-exec.c\"" + ] + @ + if Config.is_coverage () then + [ "--coverage" ] + else + [])) + ("Compiled '" ^ filename_base ^ "-exec.c'.") + ("Failed to compile '" ^ filename_base ^ "-exec.c' in ${TEST_DIR}.") + ^^ twice hardline + ^^ attempt + (String.concat + " " + ([ "cc"; + "-g"; + "-c"; + "\"-I${RUNTIME_PREFIX}/include/\""; + "-o"; + "\"./cn.o\""; + "\"./cn.c\"" + ] + @ + if Config.is_coverage () then + [ "--coverage" ] + else + [])) + "Compiled 'cn.c'." + "Failed to compile 'cn.c' in ${TEST_DIR}.") ^^ hardline -let link ~test_file = +let link ~filename_base = string "# Link" ^^ hardline + ^^ string "echo" + ^^ twice hardline ^^ attempt (String.concat " " @@ -76,7 +119,13 @@ let link ~test_file = "\"-I${RUNTIME_PREFIX}/include\""; "-o"; "\"./tests.out\""; - Filename.chop_extension test_file ^ ".o"; + (filename_base + ^ "_test.o" + ^ + if Config.with_static_hack () then + "" + else + " " ^ filename_base ^ "-exec.o cn.o"); "\"${RUNTIME_PREFIX}/libcn.a\"" ] @ @@ -157,17 +206,19 @@ let run () = in string "# Run" ^^ hardline + ^^ string "echo" + ^^ twice hardline ^^ cmd ^^ hardline ^^ string "test_exit_code=$? # Save tests exit code for later" ^^ hardline -let coverage ~test_file = +let coverage ~filename_base = string "# Coverage" ^^ hardline ^^ attempt - ("gcov \"" ^ test_file ^ "\"") + ("gcov \"" ^ filename_base ^ "_test.c\"") "Recorded coverage via gcov." "Failed to record coverage." ^^ twice hardline @@ -178,22 +229,22 @@ let coverage ~test_file = ^^ twice hardline ^^ attempt "genhtml --output-directory html \"coverage.info\"" - "Generated HTML report at \\\"${TEST_DIR}/html/\\\"." + "Generated HTML report at '${TEST_DIR}/html/'." "Failed to generate HTML report." ^^ hardline -let generate ~(output_dir : string) ~(test_file : string) : Pp.document = +let generate ~(output_dir : string) ~(filename_base : string) : Pp.document = setup ~output_dir ^^ hardline - ^^ compile ~test_file + ^^ compile ~filename_base ^^ hardline - ^^ link ~test_file + ^^ link ~filename_base ^^ hardline ^^ run () ^^ hardline ^^ (if Config.is_coverage () then - coverage ~test_file ^^ hardline + coverage ~filename_base ^^ hardline else empty) ^^ string "popd > /dev/null" diff --git a/backend/cn/lib/testGeneration/buildScript.mli b/backend/cn/lib/testGeneration/buildScript.mli index 45de35f3d..9d2928de2 100644 --- a/backend/cn/lib/testGeneration/buildScript.mli +++ b/backend/cn/lib/testGeneration/buildScript.mli @@ -1 +1 @@ -val generate : output_dir:string -> test_file:string -> Pp.document +val generate : output_dir:string -> filename_base:string -> Pp.document diff --git a/backend/cn/lib/testGeneration/specTests.ml b/backend/cn/lib/testGeneration/specTests.ml index d261bb501..963445f79 100644 --- a/backend/cn/lib/testGeneration/specTests.ml +++ b/backend/cn/lib/testGeneration/specTests.ml @@ -31,7 +31,9 @@ let debug_stage (stage : string) (str : string) : unit = debug_log (str ^ "\n\n") -let compile_constant_tests (insts : Executable_spec_extract.instrumentation list) +let compile_constant_tests + (sigma : CF.GenTypes.genTypeCategory A.sigma) + (insts : Executable_spec_extract.instrumentation list) : Test.t list * Pp.document = let test_names, docs = @@ -48,18 +50,29 @@ let compile_constant_tests (insts : Executable_spec_extract.instrumentation list |> List.hd; test = Sym.pp_string inst.fn }, - CF.Pp_ail.pp_statement - A.( - Utils.mk_stmt - (AilSexpr - (Utils.mk_expr - (AilEcall - ( Utils.mk_expr (AilEident (Sym.fresh_named "CN_UNIT_TEST_CASE")), - [ Utils.mk_expr (AilEident inst.fn) ] ))))) )) + let open Pp in + (if not (Config.with_static_hack ()) then + CF.Pp_ail.pp_function_prototype + ~executable_spec:true + inst.fn + (let _, _, decl = List.assoc Sym.equal inst.fn sigma.declarations in + decl) + ^^ hardline + else + empty) + ^^ CF.Pp_ail.pp_statement + A.( + Utils.mk_stmt + (AilSexpr + (Utils.mk_expr + (AilEcall + ( Utils.mk_expr + (AilEident (Sym.fresh_named "CN_UNIT_TEST_CASE")), + [ Utils.mk_expr (AilEident inst.fn) ] ))))) )) insts in let open Pp in - (test_names, separate (semi ^^ twice hardline) docs ^^ twice hardline) + (test_names, separate (twice hardline) docs ^^ twice hardline) let compile_generators @@ -84,6 +97,7 @@ let compile_generators let compile_random_test_case + (sigma : CF.GenTypes.genTypeCategory A.sigma) (prog5 : unit Mucore.file) (args_map : (Sym.t * (Sym.t * C.ctype) list) list) (convert_from : Sym.t * C.ctype -> Pp.document) @@ -112,59 +126,68 @@ let compile_random_test_case | GlobalDef (sct, _) -> (sym, sct)) global_syms in - (if List.is_empty globals then - string "CN_RANDOM_TEST_CASE" - else ( - let init_name = string "cn_test_gen_" ^^ Sym.pp inst.fn ^^ string "_init" in - string "void" - ^^ space - ^^ init_name - ^^ parens - (string "struct" - ^^ space - ^^ string (String.concat "_" [ "cn_gen"; Sym.pp_string inst.fn; "record" ]) - ^^ star - ^^ space - ^^ string "res") - ^^ space - ^^ braces - (nest - 2 - (hardline - ^^ separate_map - hardline - (fun (sym, sct) -> - let ty = - CF.Pp_ail.pp_ctype - ~executable_spec:true - ~is_human:false - C.no_qualifiers - (Sctypes.to_ctype sct) - in - Sym.pp sym - ^^ space - ^^ equals - ^^ space - ^^ star - ^^ parens (ty ^^ star) - ^^ string "convert_from_cn_pointer" - ^^ parens - (string "res->" ^^ Sym.pp (GenUtils.get_mangled_name [ sym ])) - ^^ semi - ^^ hardline - ^^ string "cn_assume_ownership" - ^^ parens - (separate - (comma ^^ space) - [ ampersand ^^ Sym.pp sym; - string "sizeof" ^^ parens ty; - string "(char*)" ^^ dquotes init_name - ]) - ^^ semi) - globals) - ^^ hardline) - ^^ twice hardline - ^^ string "CN_RANDOM_TEST_CASE_WITH_INIT")) + (if not (Config.with_static_hack ()) then + CF.Pp_ail.pp_function_prototype + ~executable_spec:true + inst.fn + (let _, _, decl = List.assoc Sym.equal inst.fn sigma.declarations in + decl) + ^^ hardline + else + empty) + ^^ (if List.is_empty globals then + string "CN_RANDOM_TEST_CASE" + else ( + let init_name = string "cn_test_gen_" ^^ Sym.pp inst.fn ^^ string "_init" in + string "void" + ^^ space + ^^ init_name + ^^ parens + (string "struct" + ^^ space + ^^ string (String.concat "_" [ "cn_gen"; Sym.pp_string inst.fn; "record" ]) + ^^ star + ^^ space + ^^ string "res") + ^^ space + ^^ braces + (nest + 2 + (hardline + ^^ separate_map + hardline + (fun (sym, sct) -> + let ty = + CF.Pp_ail.pp_ctype + ~executable_spec:true + ~is_human:false + C.no_qualifiers + (Sctypes.to_ctype sct) + in + Sym.pp sym + ^^ space + ^^ equals + ^^ space + ^^ star + ^^ parens (ty ^^ star) + ^^ string "convert_from_cn_pointer" + ^^ parens + (string "res->" ^^ Sym.pp (GenUtils.get_mangled_name [ sym ])) + ^^ semi + ^^ hardline + ^^ string "cn_assume_ownership" + ^^ parens + (separate + (comma ^^ space) + [ ampersand ^^ Sym.pp sym; + string "sizeof" ^^ parens ty; + string "(char*)" ^^ dquotes init_name + ]) + ^^ semi) + globals) + ^^ hardline) + ^^ twice hardline + ^^ string "CN_RANDOM_TEST_CASE_WITH_INIT")) ^^ parens (separate (comma ^^ space) @@ -173,6 +196,7 @@ let compile_random_test_case int (Config.get_num_samples ()); separate_map (comma ^^ space) convert_from args ]) + ^^ semi ^^ twice hardline @@ -237,5 +261,5 @@ let compile_generator_tests let open Pp in ( tests, concat_map - (compile_random_test_case prog5 args_map convert_from) + (compile_random_test_case sigma prog5 args_map convert_from) (List.combine tests insts) ) diff --git a/backend/cn/lib/testGeneration/specTests.mli b/backend/cn/lib/testGeneration/specTests.mli index 6e9915cdb..b64eb23c1 100644 --- a/backend/cn/lib/testGeneration/specTests.mli +++ b/backend/cn/lib/testGeneration/specTests.mli @@ -2,7 +2,8 @@ module CF = Cerb_frontend module A = CF.AilSyntax val compile_constant_tests - : Executable_spec_extract.instrumentation list -> + : CF.GenTypes.genTypeCategory A.sigma -> + Executable_spec_extract.instrumentation list -> Test.t list * Pp.document val compile_generators diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/backend/cn/lib/testGeneration/testGenConfig.ml index 6c0746240..8a43a1223 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.ml +++ b/backend/cn/lib/testGeneration/testGenConfig.ml @@ -4,8 +4,9 @@ type t = max_backtracks : int; max_unfolds : int option; max_array_length : int; - input_timeout : int option; + with_static_hack : bool; (* Run time *) + input_timeout : int option; null_in_every : int option; seed : string option; logging_level : int option; @@ -28,6 +29,7 @@ let default = max_backtracks = 25; max_unfolds = None; max_array_length = 50; + with_static_hack = false; input_timeout = None; null_in_every = None; seed = None; @@ -59,6 +61,8 @@ let get_max_unfolds () = !instance.max_unfolds let get_max_array_length () = !instance.max_array_length +let with_static_hack () = !instance.with_static_hack + let has_input_timeout () = !instance.input_timeout let has_null_in_every () = !instance.null_in_every diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/backend/cn/lib/testGeneration/testGenConfig.mli index b5dd0a8d2..e1c9acbce 100644 --- a/backend/cn/lib/testGeneration/testGenConfig.mli +++ b/backend/cn/lib/testGeneration/testGenConfig.mli @@ -4,6 +4,7 @@ type t = max_backtracks : int; max_unfolds : int option; max_array_length : int; + with_static_hack : bool; (* Run time *) input_timeout : int option; null_in_every : int option; @@ -35,6 +36,8 @@ val get_max_unfolds : unit -> int option val get_max_array_length : unit -> int +val with_static_hack : unit -> bool + val has_input_timeout : unit -> int option val has_null_in_every : unit -> int option diff --git a/backend/cn/lib/testGeneration/testGeneration.ml b/backend/cn/lib/testGeneration/testGeneration.ml index 4f994b3a1..52837d782 100644 --- a/backend/cn/lib/testGeneration/testGeneration.ml +++ b/backend/cn/lib/testGeneration/testGeneration.ml @@ -11,6 +11,8 @@ type config = Config.t let default_cfg : config = Config.default +let set_config = Config.initialize + let is_constant_function (sigma : CF.GenTypes.genTypeCategory A.sigma) (inst : Executable_spec_extract.instrumentation) @@ -92,6 +94,28 @@ let pp_label ?(width : int = 30) (label : string) (doc : Pp.document) : Pp.docum ^^ doc +let compile_includes ~filename_base = + let open Pp in + string "#include " + ^^ dquotes (string (filename_base ^ "_gen.h")) + ^^ hardline + ^^ + if Config.with_static_hack () then + string "#include " + ^^ dquotes (string (filename_base ^ "-exec.c")) + ^^ hardline + ^^ string "#include " + ^^ dquotes (string "cn.c") + else + string "#include " ^^ dquotes (string "cn.h") + + +let compile_test test = + let open Pp in + let macro = Test.registration_macro test in + string macro ^^ parens (string test.suite ^^ comma ^^ space ^^ string test.test) ^^ semi + + let compile_test_file ~(without_ownership_checking : bool) (filename_base : string) @@ -101,21 +125,14 @@ let compile_test_file = let for_constant, for_generator = List.partition (is_constant_function sigma) insts in let constant_tests, constant_tests_defs = - SpecTests.compile_constant_tests for_constant + SpecTests.compile_constant_tests sigma for_constant in let generator_tests, generator_tests_defs = SpecTests.compile_generator_tests sigma prog5 for_generator in let tests = [ constant_tests; generator_tests ] in let open Pp in - string "#include " - ^^ dquotes (string (filename_base ^ "_gen.h")) - ^^ hardline - ^^ string "#include " - ^^ dquotes (string (filename_base ^ "-exec.c")) - ^^ hardline - ^^ string "#include " - ^^ dquotes (string "cn.c") + compile_includes ~filename_base ^^ twice hardline ^^ pp_label "Assume Ownership Functions" @@ -133,12 +150,7 @@ let compile_test_file (hardline ^^ separate_map (twice hardline) - (separate_map hardline (fun test -> - let macro = Test.registration_macro test in - string macro - ^^ parens - (string test.suite ^^ comma ^^ space ^^ string test.test) - ^^ semi)) + (separate_map hardline compile_test) tests ^^ twice hardline ^^ string "return cn_test_main(argc, argv);") @@ -184,32 +196,110 @@ let save_tests (sigma : CF.GenTypes.genTypeCategory A.sigma) (prog5 : unit Mucore.file) (insts : Executable_spec_extract.instrumentation list) - : string + : unit = let tests_doc = compile_test_file ~without_ownership_checking filename_base sigma prog5 insts in - let test_file = filename_base ^ "_test.c" in - save output_dir test_file tests_doc; - test_file + save output_dir (filename_base ^ "_test.c") tests_doc -let save_build_script ~output_dir ~test_file = - let script_doc = BuildScript.generate ~output_dir ~test_file in +let save_build_script ~output_dir ~filename_base = + let script_doc = BuildScript.generate ~output_dir ~filename_base in save ~perm:0o777 output_dir "run_tests.sh" script_doc -let run - ~output_dir - ~filename - ~without_ownership_checking - (cfg : config) +let needs_static_hack + ~(with_warning : bool) + (cabs_tunit : CF.Cabs.translation_unit) + (sigma : CF.GenTypes.genTypeCategory A.sigma) + (inst : Executable_spec_extract.instrumentation) + = + let (TUnit decls) = cabs_tunit in + let is_static_func () = + List.exists + (fun decl -> + match decl with + | CF.Cabs.EDecl_func + (FunDef + ( loc, + _, + { storage_classes; _ }, + Declarator + (_, DDecl_function (DDecl_identifier (_, Identifier (_, fn')), _)), + _ )) + when String.equal (Sym.pp_string inst.fn) fn' + && List.exists + (fun scs -> match scs with CF.Cabs.SC_static -> true | _ -> false) + storage_classes -> + if with_warning then + Cerb_colour.with_colour + (fun () -> + Pp.( + warn + loc + (string "Static function" + ^^^ squotes (Sym.pp inst.fn) + ^^^ string "could not be tested." + ^/^ string "You can try again with '--with-static-hack'"))) + (); + true + | _ -> false) + decls + in + let _, _, _, args, _ = List.assoc Sym.equal inst.fn sigma.function_definitions in + let depends_on_static_glob () = + let global_syms = + inst.internal + |> Option.get + |> AT.get_lat + |> LAT.free_vars (fun _ -> Sym.Set.empty) + |> Sym.Set.to_seq + |> List.of_seq + |> List.filter (fun x -> + not + (List.mem (fun x y -> String.equal (Sym.pp_string x) (Sym.pp_string y)) x args)) + in + let static_globs = + List.filter_map + (fun sym -> + match List.assoc Sym.equal sym sigma.declarations with + | loc, _, Decl_object ((Static, _), _, _, _) -> Some (sym, loc) + | _ -> None) + global_syms + in + if List.is_empty static_globs then + false + else ( + if with_warning then + Cerb_colour.with_colour + (fun () -> + List.iter + (fun (sym, loc) -> + Pp.( + warn + loc + (string "Function" + ^^^ squotes (Sym.pp inst.fn) + ^^^ string "relies on static global" + ^^^ squotes (Sym.pp sym) + ^^ comma + ^^^ string "so could not be tested." + ^^^ string "You can try again with '--with-static-hack'."))) + static_globs) + (); + true) + in + is_static_func () || depends_on_static_glob () + + +let functions_under_test + ~(with_warning : bool) + (cabs_tunit : CF.Cabs.translation_unit) (sigma : CF.GenTypes.genTypeCategory A.sigma) (prog5 : unit Mucore.file) - : unit + : Executable_spec_extract.instrumentation list = - Config.initialize cfg; - Cerb_debug.begin_csv_timing (); let insts = prog5 |> Executable_spec_extract.collect_instrumentation |> fst in let selected_fsyms = Check.select_functions @@ -218,15 +308,27 @@ let run (fun (inst : Executable_spec_extract.instrumentation) -> inst.fn) insts)) in - let insts = - insts - |> List.filter (fun (inst : Executable_spec_extract.instrumentation) -> - Option.is_some inst.internal && Sym.Set.mem inst.fn selected_fsyms) - in + insts + |> List.filter (fun (inst : Executable_spec_extract.instrumentation) -> + Option.is_some inst.internal + && Sym.Set.mem inst.fn selected_fsyms + && (Config.with_static_hack () + || not (needs_static_hack ~with_warning cabs_tunit sigma inst))) + + +let run + ~output_dir + ~filename + ~without_ownership_checking + (cabs_tunit : CF.Cabs.translation_unit) + (sigma : CF.GenTypes.genTypeCategory A.sigma) + (prog5 : unit Mucore.file) + : unit + = + Cerb_debug.begin_csv_timing (); + let insts = functions_under_test ~with_warning:false cabs_tunit sigma prog5 in let filename_base = filename |> Filename.basename |> Filename.chop_extension in save_generators ~output_dir ~filename_base sigma prog5 insts; - let test_file = - save_tests ~output_dir ~filename_base ~without_ownership_checking sigma prog5 insts - in - save_build_script ~output_dir ~test_file; + save_tests ~output_dir ~filename_base ~without_ownership_checking sigma prog5 insts; + save_build_script ~output_dir ~filename_base; Cerb_debug.end_csv_timing "specification test generation" diff --git a/backend/cn/lib/testGeneration/testGeneration.mli b/backend/cn/lib/testGeneration/testGeneration.mli index d20712e81..2e7b60dea 100644 --- a/backend/cn/lib/testGeneration/testGeneration.mli +++ b/backend/cn/lib/testGeneration/testGeneration.mli @@ -2,11 +2,20 @@ type config = TestGenConfig.t val default_cfg : config +val set_config : config -> unit + +val functions_under_test + : with_warning:bool -> + Cerb_frontend.Cabs.translation_unit -> + Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.sigma -> + unit Mucore.file -> + Executable_spec_extract.instrumentation list + val run : output_dir:string -> filename:string -> without_ownership_checking:bool -> - config -> + Cerb_frontend.Cabs.translation_unit -> Cerb_frontend.GenTypes.genTypeCategory Cerb_frontend.AilSyntax.sigma -> unit Mucore.file -> unit diff --git a/tests/run-cn-test-gen.sh b/tests/run-cn-test-gen.sh index 2524271f0..bfb477a1e 100755 --- a/tests/run-cn-test-gen.sh +++ b/tests/run-cn-test-gen.sh @@ -27,7 +27,7 @@ function separator() { printf '\n\n' } -CONFIGS=("--coverage" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") +CONFIGS=("--coverage" "--with-static-hack --coverage" "--sized-null" "--random-size-splits" "--random-size-splits --allowed-size-split-backtracks=10") # For each configuration for CONFIG in "${CONFIGS[@]}"; do