Skip to content

Commit

Permalink
[CN-Test-Gen] Expose static hack via CLI flag (#808)
Browse files Browse the repository at this point in the history
  • Loading branch information
@ZippeyKeys12
ZippeyKeys12 authored Jan 2, 2025
1 parent 6fc4ec4 commit 6d4b486
Show file tree
Hide file tree
Showing 10 changed files with 373 additions and 169 deletions.
106 changes: 58 additions & 48 deletions backend/cn/bin/main.ml
View file
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
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
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

0 comments on commit 6d4b486

Please sign in to comment.