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] Expose static hack via CLI flag #808

Merged
merged 1 commit into from
Jan 2, 2025
Merged

[CN-Test-Gen] Expose static hack via CLI flag #808

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
106 changes: 58 additions & 48 deletions backend/cn/bin/main.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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@ () =
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -132,14 +133,15 @@ 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 ->
paused:_ Typing.pause ->
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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -457,6 +460,7 @@ let run_tests
max_backtracks
max_unfolds
max_array_length
with_static_hack
input_timeout
null_in_every
seed
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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.(
Expand Down Expand Up @@ -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
Expand Down
79 changes: 65 additions & 14 deletions backend/cn/lib/testGeneration/buildScript.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ let attempt cmd success failure =
^^ string "fi"


let compile ~test_file =
let compile ~filename_base =
string "# Compile"
^^ hardline
^^ attempt
Expand All @@ -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
" "
Expand All @@ -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\""
]
@
Expand Down Expand Up @@ -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
Expand All @@ -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"
Expand Down
2 changes: 1 addition & 1 deletion backend/cn/lib/testGeneration/buildScript.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
val generate : output_dir:string -> test_file:string -> Pp.document
val generate : output_dir:string -> filename_base:string -> Pp.document
Loading