diff --git a/doc/ADR/README.md b/doc/ADR/README.md index 9420ce20d83..e408e4b7bc5 100644 --- a/doc/ADR/README.md +++ b/doc/ADR/README.md @@ -6,8 +6,8 @@ where taken at the time they were, so that future maintainers can more easily identify constraints that shaped the architecture of the system and the surrounding infrastructure. -## Core goto form -\subpage core-goto +## Symex ready goto form +\subpage symex-ready-goto ## Release & Packaging diff --git a/doc/ADR/core_goto.md b/doc/ADR/symex_ready_goto.md similarity index 72% rename from doc/ADR/core_goto.md rename to doc/ADR/symex_ready_goto.md index 1104942ab8e..bd4efab7b91 100644 --- a/doc/ADR/core_goto.md +++ b/doc/ADR/symex_ready_goto.md @@ -1,13 +1,13 @@ -\page core-goto Core goto definition +\page symex-ready-goto Symex ready goto definition During the analysis of a program CBMC transforms the input program in an intermediate language called extended goto. Then the tool performs a series of simplifications on the obtained goto program until the program is given to the solver. -We say that a program is in the **core goto form** when all the extended goto features have +We say that a program is in the **symex ready goto form** when all the extended goto features have been simplified. -More specifically, a program that is in **core goto form** is one that can be passed to **symex** by +More specifically, a program that is in **symex ready goto form** is one that can be passed to **symex** by using any solver deriving from `goto_verifiert` without requiring any lowering step. At the time of writing, verifiers extending `goto_verifiert` are: diff --git a/doc/architectural/goto-program-transformations.md b/doc/architectural/goto-program-transformations.md index ff9947d0542..cd3572c8f21 100644 --- a/doc/architectural/goto-program-transformations.md +++ b/doc/architectural/goto-program-transformations.md @@ -5,7 +5,7 @@ \section required-transforms Core Transformation Passes This section lists the transformation passes that must have been applied for the -goto model to be in core goto format. +goto model to be in symex ready goto format. Note that the passes are listed below in the order they are currently called in CBMC. While all dependencies on the ordering are not fully documented, the @@ -184,11 +184,11 @@ nondet-transform if it is being used. This transformation removes skip instructions. Note that this transformation is called in many places and may be called as part of other transformations. This -instance here is part of the mandatory transformation to reach core goto format. -If there is a use case where it is desirable to preserve a "no operation" -instruction, a `LOCATION` type instruction may be used in place of a `SKIP` -instruction. The `LOCATION` instruction has the same semantics as the `SKIP` -instruction, but is not removed by the remove skip instructions pass. +instance here is part of the mandatory transformation to reach symex ready goto +format. If there is a use case where it is desirable to preserve a "no +operation" instruction, a `LOCATION` type instruction may be used in place of a +`SKIP` instruction. The `LOCATION` instruction has the same semantics as the +`SKIP` instruction, but is not removed by the remove skip instructions pass. The implementation of this pass is called via \ref remove_skip(goto_modelt &) @@ -215,7 +215,7 @@ coverage-transform if it is being used. The sections lists the optional transformation passes that are optional and will modify a goto model. Note that these are documented here for consistency, but -not required for core goto format. +not required for symex ready goto format. Note for each optional pass there is a listed predeceesor pass. This is the pass currently called before the listed pass in CBMC. While the ordering may not be diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 7a2a54d4d12..b01ddb6edfd 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -525,6 +525,9 @@ give a stack trace only \fB\-\-flush\fR flush every line of output .TP +\fB\-\-export\-symex\-ready\-goto\fR filename +export the symex ready version of the goto-model into the given filename +.TP \fB\-\-verbosity\fR # verbosity level .TP diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt index 138811a009e..b6c03a0a841 100644 --- a/regression/cbmc/CMakeLists.txt +++ b/regression/cbmc/CMakeLists.txt @@ -1,26 +1,32 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC") set(gcc_only -X gcc-only) set(gcc_only_string "-X;gcc-only;") + set(exclude_win_broken_tests -X winbug) + # We add the string at the end of the exclusion list, so it must not + # have the `;` at the end or it bugs out. + set(exclude_win_broken_tests_string "-X;winbug") else() set(gcc_only "") set(gcc_only_string "") + set(exclude_win_broken_tests "") + set(exclude_win_broken_tests_string "") endif() add_test_pl_tests( - "$ --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} + "$ --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests} ) add_test_pl_profile( "cbmc-paths-lifo" "$ --paths lifo" - "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo" + "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}" "CORE" ) add_test_pl_profile( "cbmc-cprover-smt2" "$ --cprover-smt2" - "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2" + "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}" "CORE" ) diff --git a/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc b/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc new file mode 100644 index 00000000000..6decca9ccec --- /dev/null +++ b/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc @@ -0,0 +1,15 @@ +CORE winbug +test.c +--export-symex-ready-goto "" +^ERROR: Please provide a filename to write the goto-binary to.$ +^EXIT=6$ +^SIGNAL=0$ +-- +-- +Ensure that --export-symex-ready-goto exported.symex-ready.goto terminates +with error when incorrectly used. + +The reason why we use `winbug` is that it fails on certain windows system +probably due to different interpretation of "". Not a bug, but we're using +that label to remain consistent with other parts of the codebase, and not +to unnecessarily introduce new ones for simple use cases. diff --git a/regression/cbmc/export-symex-ready-goto/test-correct.desc b/regression/cbmc/export-symex-ready-goto/test-correct.desc new file mode 100644 index 00000000000..e6b592328c7 --- /dev/null +++ b/regression/cbmc/export-symex-ready-goto/test-correct.desc @@ -0,0 +1,15 @@ +CORE +test.c +--export-symex-ready-goto exported.symex.ready.goto +^Parsing test.c$ +^Converting$ +^Type-checking test$ +^Generating GOTO Program$ +^Removal of function pointers and virtual functions$ +^Generic Property Instrumentation$ +Exported goto-program in symex-ready-goto form at exported.symex.ready.goto +^EXIT=0$ +^SIGNAL=0$ +-- +-- +Ensure that --export-symex-ready-goto exported.symex.ready.goto terminates successfully and logs this. diff --git a/regression/cbmc/export-symex-ready-goto/test.c b/regression/cbmc/export-symex-ready-goto/test.c new file mode 100644 index 00000000000..7c995a485d1 --- /dev/null +++ b/regression/cbmc/export-symex-ready-goto/test.c @@ -0,0 +1,6 @@ +int main(int argc, char **argv) +{ + int arr[] = {0, 1, 2, 3, 4}; + __CPROVER_assert(arr[0] == 1, "expected failure: 0 != 1"); + return 0; +} diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index aa1ffe69262..31cf9905f48 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -26,16 +26,24 @@ Author: Daniel Kroening, kroening@kroening.com # include #endif -#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include #include #include #include - #include - #include - #include #include #include @@ -49,29 +57,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - #include #include #include #include - #include - -#include - +#include #include +#include #include "c_test_input_generator.h" @@ -252,6 +245,19 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("trace", true); } + if(cmdline.isset("export-symex-ready-goto")) + { + options.set_option( + "export-symex-ready-goto", cmdline.get_value("export-symex-ready-goto")); + if(options.get_option("export-symex-ready-goto").empty()) + { + log.error() + << "ERROR: Please provide a filename to write the goto-binary to." + << messaget::eom; + exit(CPROVER_EXIT_INTERNAL_ERROR); + } + } + if(cmdline.isset("localize-faults")) options.set_option("localize-faults", true); @@ -553,6 +559,31 @@ int cbmc_parse_optionst::doit() if(set_properties()) return CPROVER_EXIT_SET_PROPERTIES_FAILED; + // At this point, our goto-model should be in symex-ready-goto form (all of + // the transformations have been run and the program is ready to be given + // to the solver). + if(options.is_set("export-symex-ready-goto")) + { + auto symex_ready_goto_filename = + options.get_option("export-symex-ready-goto"); + + bool success = !write_goto_binary( + symex_ready_goto_filename, goto_model, ui_message_handler); + + if(!success) + { + log.error() << "ERROR: Unable to export goto-program in file " + << symex_ready_goto_filename << messaget::eom; + return CPROVER_EXIT_INTERNAL_ERROR; + } + else + { + log.status() << "Exported goto-program in symex-ready-goto form at " + << symex_ready_goto_filename << messaget::eom; + return CPROVER_EXIT_SUCCESS; + } + } + if( options.get_bool_option("program-only") || options.get_bool_option("show-vcc") || @@ -937,6 +968,7 @@ void cbmc_parse_optionst::help() " --show-symbol-table show loaded symbol table\n" HELP_SHOW_GOTO_FUNCTIONS HELP_VALIDATE + " --export-symex-ready-goto f serialise goto-program in symex-ready-goto form in f\n" // NOLINT(*) "\n" "Program instrumentation options:\n" HELP_GOTO_CHECK diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index b1a7abd9f27..8ec5b04ffaa 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -59,6 +59,7 @@ class optionst; "(verbosity):(no-library)" \ "(nondet-static)" \ "(version)" \ + "(export-symex-ready-goto):" \ OPT_COVER \ "(symex-coverage-report):" \ "(mm):" \