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/cbmc_parse_options.cpp

@@ -534,7 +534,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;
@@ -587,25 +588,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?
@@ -622,36 +627,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;
   }
 
@@ -716,7 +721,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
   {
@@ -725,17 +732,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);
 
@@ -751,27 +758,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
@@ -784,21 +790,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.get_bool_option("cover"))
     {
-      if(instrument_cover_goals(options, goto_model, get_message_handler()))
+      if(instrument_cover_goals(options, goto_model, log.get_message_handler()))
         return true;
     }
 
@@ -810,37 +816,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.get_bool_option("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.get_bool_option("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.get_bool_option("property"))
+        property_slicer(goto_model, options.get_list_option("property"));
       else
         full_slicer(goto_model);
     }
@@ -851,25 +859,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();
 };