Factor out getting & processing goto-model

CBMC's methods for getting a goto-model from a source file, and
processing that goto-model to be ready for bounded model checking, are
now static so that they can be called from clients that wish to set up a
goto-model the same way that CBMC does.

Author: karkhaz

src/cbmc/bmc.h

@@ -321,7 +321,8 @@ class path_explorert : public bmct
   "                              (use --show-loops to get the loop IDs)\n"     \
   " --show-vcc                   show the verification conditions\n"           \
   " --slice-formula              remove assignments unrelated to property\n"   \
-  " --unwinding-assertions       generate unwinding assertions\n"              \
+  " --unwinding-assertions       generate unwinding assertions (cannot be\n"   \
+  "                              used with --cover or --partial-loops)\n"      \
   " --partial-loops              permit paths with partial loops\n"            \
   " --no-pretty-names            do not simplify identifiers\n"                \
   " --graphml-witness filename   write the witness in GraphML format to "      \

src/cbmc/cbmc_parse_options.cpp

@@ -132,6 +132,28 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
 
   cbmc_parse_optionst::set_default_options(options);
 
+  if(cmdline.isset("cover") && cmdline.isset("unwinding-assertions"))
+  {
+    error() << "--cover and --unwinding-assertions must not be given together"
+            << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
+
+  if(cmdline.isset("partial-loops") && cmdline.isset("unwinding-assertions"))
+  {
+    error() << "--partial-loops and --unwinding-assertions must not be given "
+            << "together" << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
+
+  if(cmdline.isset("reachability-slice") &&
+     cmdline.isset("reachability-slice-fb"))
+  {
+    error() << "--reachability-slice and --reachability-slice-fb must not be "
+            << "given together" << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
+
   if(cmdline.isset("paths"))
     options.set_option("paths", true);
 
@@ -165,6 +187,24 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cpp11"))
     config.cpp.set_cpp11();
 
+  if(cmdline.isset("property"))
+    options.set_option("property", cmdline.get_values("property"));
+
+  if(cmdline.isset("drop-unused-functions"))
+    options.set_option("drop-unused-functions", true);
+
+  if(cmdline.isset("string-abstraction"))
+    options.set_option("string-abstraction", true);
+
+  if(cmdline.isset("reachability-slice-fb"))
+    options.set_option("reachability-slice-fb", true);
+
+  if(cmdline.isset("reachability-slice"))
+    options.set_option("reachability-slice", true);
+
+  if(cmdline.isset("nondet-static"))
+    options.set_option("nondet-static", true);
+
   if(cmdline.isset("no-simplify"))
     options.set_option("simplify", false);
 
@@ -227,21 +267,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("partial-loops"))
     options.set_option("partial-loops", true);
 
-  if(options.is_set("cover") && options.get_bool_option("unwinding-assertions"))
-  {
-    error() << "--cover and --unwinding-assertions "
-            << "must not be given together" << eom;
-    exit(CPROVER_EXIT_USAGE_ERROR);
-  }
-
-  if(options.get_bool_option("partial-loops") &&
-     options.get_bool_option("unwinding-assertions"))
-  {
-    error() << "--partial-loops and --unwinding-assertions "
-            << "must not be given together" << eom;
-    exit(CPROVER_EXIT_USAGE_ERROR);
-  }
-
   // remove unused equations
   if(cmdline.isset("slice-formula"))
     options.set_option("slice-formula", true);
@@ -532,7 +557,8 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_SUCCESS;
   }
 
-  int get_goto_program_ret=get_goto_program(options);
+  int get_goto_program_ret =
+    get_goto_program(goto_model, options, cmdline, *this, ui_message_handler);
 
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
@@ -585,25 +611,29 @@ bool cbmc_parse_optionst::set_properties()
 }
 
 int cbmc_parse_optionst::get_goto_program(
-  const optionst &options)
+  goto_modelt &goto_model,
+  const optionst &options,
+  const cmdlinet &cmdline,
+  messaget &log,
+  ui_message_handlert &ui_message_handler)
 {
   if(cmdline.args.empty())
   {
-    error() << "Please provide a program to verify" << eom;
+    log.error() << "Please provide a program to verify" << log.eom;
     return CPROVER_EXIT_INCORRECT_TASK;
   }
 
   try
   {
-    goto_model=initialize_goto_model(cmdline, get_message_handler());
+    goto_model = initialize_goto_model(cmdline, ui_message_handler);
 
     if(cmdline.isset("show-symbol-table"))
     {
       show_symbol_table(goto_model, ui_message_handler.get_ui());
       return CPROVER_EXIT_SUCCESS;
     }
 
-    if(process_goto_program(options))
+    if(cbmc_parse_optionst::process_goto_program(goto_model, options, log))
       return CPROVER_EXIT_INTERNAL_ERROR;
 
     // show it?
@@ -620,36 +650,36 @@ int cbmc_parse_optionst::get_goto_program(
     {
       show_goto_functions(
         goto_model,
-        get_message_handler(),
+        ui_message_handler,
         ui_message_handler.get_ui(),
         cmdline.isset("list-goto-functions"));
       return CPROVER_EXIT_SUCCESS;
     }
 
-    status() << config.object_bits_info() << eom;
+    log.status() << config.object_bits_info() << log.eom;
   }
 
   catch(const char *e)
   {
-    error() << e << eom;
+    log.error() << e << log.eom;
     return CPROVER_EXIT_EXCEPTION;
   }
 
   catch(const std::string &e)
   {
-    error() << e << eom;
+    log.error() << e << log.eom;
     return CPROVER_EXIT_EXCEPTION;
   }
 
   catch(int e)
   {
-    error() << "Numeric exception : " << e << eom;
+    log.error() << "Numeric exception : " << e << log.eom;
     return CPROVER_EXIT_EXCEPTION;
   }
 
   catch(const std::bad_alloc &)
   {
-    error() << "Out of memory" << eom;
+    log.error() << "Out of memory" << log.eom;
     return CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY;
   }
 
@@ -714,7 +744,9 @@ void cbmc_parse_optionst::preprocessing()
 }
 
 bool cbmc_parse_optionst::process_goto_program(
-  const optionst &options)
+  goto_modelt &goto_model,
+  const optionst &options,
+  messaget &log)
 {
   try
   {
@@ -723,17 +755,17 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
-    link_to_library(goto_model, get_message_handler());
+    link_to_library(goto_model, log.get_message_handler());
 
-    if(cmdline.isset("string-abstraction"))
-      string_instrumentation(goto_model, get_message_handler());
+    if(options.get_bool_option("string-abstraction"))
+      string_instrumentation(goto_model, log.get_message_handler());
 
     // remove function pointers
-    status() << "Removal of function pointers and virtual functions" << eom;
+    log.status() << "Removal of function pointers and virtual functions" << eom;
     remove_function_pointers(
-      get_message_handler(),
+      log.get_message_handler(),
       goto_model,
-      cmdline.isset("pointer-check"));
+      options.get_bool_option("pointer-check"));
     // remove catch and throw (introduces instanceof)
     remove_exceptions(goto_model);
 
@@ -749,27 +781,26 @@ bool cbmc_parse_optionst::process_goto_program(
     rewrite_union(goto_model);
 
     // add generic checks
-    status() << "Generic Property Instrumentation" << eom;
+    log.status() << "Generic Property Instrumentation" << eom;
     goto_check(options, goto_model);
 
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_model);
 
     // ignore default/user-specified initialization
     // of variables with static lifetime
-    if(cmdline.isset("nondet-static"))
+    if(options.get_bool_option("nondet-static"))
     {
-      status() << "Adding nondeterministic initialization "
-                  "of static/global variables" << eom;
+      log.status() << "Adding nondeterministic initialization "
+                      "of static/global variables"
+                   << eom;
       nondet_static(goto_model);
     }
 
-    if(cmdline.isset("string-abstraction"))
+    if(options.get_bool_option("string-abstraction"))
     {
-      status() << "String Abstraction" << eom;
-      string_abstraction(
-        goto_model,
-        get_message_handler());
+      log.status() << "String Abstraction" << eom;
+      string_abstraction(goto_model, log.get_message_handler());
     }
 
     // add failed symbols
@@ -782,21 +813,21 @@ bool cbmc_parse_optionst::process_goto_program(
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
 
-    if(cmdline.isset("drop-unused-functions"))
+    if(options.get_bool_option("drop-unused-functions"))
     {
       // Entry point will have been set before and function pointers removed
-      status() << "Removing unused functions" << eom;
-      remove_unused_functions(goto_model, get_message_handler());
+      log.status() << "Removing unused functions" << eom;
+      remove_unused_functions(goto_model, log.get_message_handler());
     }
 
     // remove skips such that trivial GOTOs are deleted and not considered
     // for coverage annotation:
     remove_skip(goto_model);
 
     // instrument cover goals
-    if(cmdline.isset("cover"))
+    if(options.is_set("cover"))
     {
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
+      if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
         return true;
     }
 
@@ -808,37 +839,39 @@ bool cbmc_parse_optionst::process_goto_program(
     label_properties(goto_model);
 
     // reachability slice?
-    if(cmdline.isset("reachability-slice-fb"))
+    if(options.get_bool_option("reachability-slice-fb"))
     {
-      if(cmdline.isset("reachability-slice"))
+      if(options.get_bool_option("reachability-slice"))
       {
-        error() << "--reachability-slice and --reachability-slice-fb "
-                << "must not be given together" << eom;
+        log.error() << "--reachability-slice and --reachability-slice-fb "
+                    << "must not be given together" << eom;
         return true;
       }
 
-      status() << "Performing a forwards-backwards reachability slice" << eom;
-      if(cmdline.isset("property"))
-        reachability_slicer(goto_model, cmdline.get_values("property"), true);
+      log.status() << "Performing a forwards-backwards reachability slice"
+                   << eom;
+      if(options.is_set("property"))
+        reachability_slicer(
+          goto_model, options.get_list_option("property"), true);
       else
         reachability_slicer(goto_model, true);
     }
 
-    if(cmdline.isset("reachability-slice"))
+    if(options.get_bool_option("reachability-slice"))
     {
-      status() << "Performing a reachability slice" << eom;
-      if(cmdline.isset("property"))
-        reachability_slicer(goto_model, cmdline.get_values("property"));
+      log.status() << "Performing a reachability slice" << eom;
+      if(options.is_set("property"))
+        reachability_slicer(goto_model, options.get_list_option("property"));
       else
         reachability_slicer(goto_model);
     }
 
     // full slice?
-    if(cmdline.isset("full-slice"))
+    if(options.get_bool_option("full-slice"))
     {
-      status() << "Performing a full slice" << eom;
-      if(cmdline.isset("property"))
-        property_slicer(goto_model, cmdline.get_values("property"));
+      log.status() << "Performing a full slice" << eom;
+      if(options.is_set("property"))
+        property_slicer(goto_model, options.get_list_option("property"));
       else
         full_slicer(goto_model);
     }
@@ -849,25 +882,25 @@ bool cbmc_parse_optionst::process_goto_program(
 
   catch(const char *e)
   {
-    error() << e << eom;
+    log.error() << e << eom;
     return true;
   }
 
   catch(const std::string &e)
   {
-    error() << e << eom;
+    log.error() << e << eom;
     return true;
   }
 
   catch(int e)
   {
-    error() << "Numeric exception : " << e << eom;
+    log.error() << "Numeric exception : " << e << eom;
     return true;
   }
 
   catch(const std::bad_alloc &)
   {
-    error() << "Out of memory" << eom;
+    log.error() << "Out of memory" << eom;
     exit(CPROVER_EXIT_INTERNAL_OUT_OF_MEMORY);
     return true;
   }

src/cbmc/cbmc_parse_options.h

@@ -97,6 +97,15 @@ class cbmc_parse_optionst:
   /// default behaviour, for example unit tests.
   static void set_default_options(optionst &);
 
+  static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
+
+  static int get_goto_program(
+    goto_modelt &,
+    const optionst &,
+    const cmdlinet &,
+    messaget &,
+    ui_message_handlert &);
+
 protected:
   goto_modelt goto_model;
   ui_message_handlert ui_message_handler;
@@ -105,8 +114,6 @@ class cbmc_parse_optionst:
   void register_languages();
   void get_command_line_options(optionst &);
   void preprocessing();
-  int get_goto_program(const optionst &);
-  bool process_goto_program(const optionst &);
   bool set_properties();
 };