Merge pull request #7697 from NlightNFotis/extract_core_goto

Add capability to export goto-program in symex-ready-goto form to CBMC.

Author: Enrico Steffinlongo

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
 

doc/ADR/core_goto.md renamed to 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:

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.</em>
 
 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.</em>
 
 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

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

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(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "cbmc-paths-lifo"
     "$<TARGET_FILE:cbmc> --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"
     "$<TARGET_FILE:cbmc> --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"
 )
 

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.

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.

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;
+}

src/cbmc/cbmc_parse_options.cpp

@@ -26,16 +26,24 @@ Author: Daniel Kroening, [email protected]
 #  include <util/unicode.h>
 #endif
 
-#include <langapi/language.h>
+#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
+#include <goto-programs/process_goto_program.h>
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/set_properties.h>
+#include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
+#include <goto-programs/show_symbol_table.h>
+#include <goto-programs/write_goto_binary.h>
 
 #include <ansi-c/c_preprocess.h>
 #include <ansi-c/cprover_library.h>
 #include <ansi-c/gcc_version.h>
-
 #include <assembler/remove_asm.h>
-
 #include <cpp/cprover_library.h>
-
 #include <goto-checker/all_properties_verifier.h>
 #include <goto-checker/all_properties_verifier_with_fault_localization.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
@@ -49,29 +57,14 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/single_path_symex_only_checker.h>
 #include <goto-checker/stop_on_fail_verifier.h>
 #include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
-
-#include <goto-programs/initialize_goto_model.h>
-#include <goto-programs/link_to_library.h>
-#include <goto-programs/loop_ids.h>
-#include <goto-programs/process_goto_program.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/remove_skip.h>
-#include <goto-programs/remove_unused_functions.h>
-#include <goto-programs/set_properties.h>
-#include <goto-programs/show_goto_functions.h>
-#include <goto-programs/show_properties.h>
-#include <goto-programs/show_symbol_table.h>
-
 #include <goto-instrument/cover.h>
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/reachability_slicer.h>
-
 #include <goto-symex/path_storage.h>
-
-#include <pointer-analysis/add_failed_symbols.h>
-
+#include <langapi/language.h>
 #include <langapi/mode.h>
+#include <pointer-analysis/add_failed_symbols.h>
 
 #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

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):" \