remove_calls_no_body: generate status output

Use of this functionality will make symex warnings about functions
without body go away. To make up for this, at least status output should
be produced to ensure that this possible soundness issue of the
verification result can be caught.

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -962,18 +962,24 @@ bool jbmc_parse_optionst::process_goto_functions(
     log.status() << "Performing a forwards-backwards reachability slice"
                  << messaget::eom;
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"), true);
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), true, ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model, true);
+      reachability_slicer(goto_model, true, ui_message_handler);
   }
 
   if(cmdline.isset("reachability-slice"))
   {
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"));
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, ui_message_handler);
   }
 
   // full slice?

regression/goto-instrument/reachability-slice/test.desc

@@ -1,6 +1,7 @@
 CORE
 main.c
 --reachability-slice
+Removing call to undefined_function, which has no body
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

src/cbmc/cbmc_parse_options.cpp

@@ -944,19 +944,29 @@ bool cbmc_parse_optionst::process_goto_program(
     log.status() << "Performing a forwards-backwards reachability slice"
                  << messaget::eom;
     if(options.is_set("property"))
+    {
       reachability_slicer(
-        goto_model, options.get_list_option("property"), true);
+        goto_model,
+        options.get_list_option("property"),
+        true,
+        log.get_message_handler());
+    }
     else
-      reachability_slicer(goto_model, true);
+      reachability_slicer(goto_model, true, log.get_message_handler());
   }
 
   if(options.get_bool_option("reachability-slice"))
   {
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(options.is_set("property"))
-      reachability_slicer(goto_model, options.get_list_option("property"));
+    {
+      reachability_slicer(
+        goto_model,
+        options.get_list_option("property"),
+        log.get_message_handler());
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, log.get_message_handler());
   }
 
   // full slice?

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -841,7 +841,7 @@ int goto_instrument_parse_optionst::doit()
       log.status() << "Removing calls to functions without a body"
                    << messaget::eom;
       remove_calls_no_bodyt remove_calls_no_body;
-      remove_calls_no_body(goto_model.goto_functions);
+      remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
 
       log.status() << "Accelerating" << messaget::eom;
       guard_managert guard_manager;
@@ -1248,7 +1248,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
                  << messaget::eom;
 
     remove_calls_no_bodyt remove_calls_no_body;
-    remove_calls_no_body(goto_model.goto_functions);
+    remove_calls_no_body(goto_model.goto_functions, ui_message_handler);
 
     goto_model.goto_functions.update();
     goto_model.goto_functions.compute_loop_numbers();
@@ -1605,9 +1605,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
 
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"));
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, ui_message_handler);
   }
 
   if(cmdline.isset("fp-reachability-slice"))
@@ -1617,7 +1620,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     log.status() << "Performing a function pointer reachability slice"
                  << messaget::eom;
     function_path_reachability_slicer(
-      goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
+      goto_model,
+      cmdline.get_comma_separated_values("fp-reachability-slice"),
+      ui_message_handler);
   }
 
   // full slice?
@@ -1690,9 +1695,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(cmdline.isset("property"))
-      reachability_slicer(goto_model, cmdline.get_values("property"));
+    {
+      reachability_slicer(
+        goto_model, cmdline.get_values("property"), ui_message_handler);
+    }
     else
-      reachability_slicer(goto_model);
+      reachability_slicer(goto_model, ui_message_handler);
   }
 
   if(cmdline.isset("ensure-one-backedge-per-target"))

src/goto-instrument/reachability_slicer.cpp

@@ -30,13 +30,14 @@ Author: Daniel Kroening, kroening@kroening.com
 void reachability_slicert::operator()(
   goto_functionst &goto_functions,
   const slicing_criteriont &criterion,
-  bool include_forward_reachability)
+  bool include_forward_reachability,
+  message_handlert &message_handler)
 {
   // Replace function calls without body by non-deterministic return values to
   // ensure the CFG does not consider instructions after such a call to be
   // unreachable.
   remove_calls_no_bodyt remove_calls_no_body;
-  remove_calls_no_body(goto_functions);
+  remove_calls_no_body(goto_functions, message_handler);
   goto_functions.update();
 
   cfg(goto_functions);
@@ -392,13 +393,18 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
 /// \param include_forward_reachability: Determines if only instructions
 ///   from which the criterion is reachable should be kept (false) or also
 ///   those reachable from the criterion (true)
+/// \param message_handler: message handler
 void reachability_slicer(
   goto_modelt &goto_model,
-  const bool include_forward_reachability)
+  const bool include_forward_reachability,
+  message_handlert &message_handler)
 {
   reachability_slicert s;
   assert_criteriont a;
-  s(goto_model.goto_functions, a, include_forward_reachability);
+  s(goto_model.goto_functions,
+    a,
+    include_forward_reachability,
+    message_handler);
 }
 
 /// Perform reachability slicing on goto_model for selected properties.
@@ -408,34 +414,42 @@ void reachability_slicer(
 /// \param include_forward_reachability: Determines if only instructions
 ///   from which the criterion is reachable should be kept (false) or also
 ///   those reachable from the criterion (true)
+/// \param message_handler: message handler
 void reachability_slicer(
   goto_modelt &goto_model,
   const std::list<std::string> &properties,
-  const bool include_forward_reachability)
+  const bool include_forward_reachability,
+  message_handlert &message_handler)
 {
   reachability_slicert s;
   properties_criteriont p(properties);
-  s(goto_model.goto_functions, p, include_forward_reachability);
+  s(goto_model.goto_functions,
+    p,
+    include_forward_reachability,
+    message_handler);
 }
 
 /// Perform reachability slicing on goto_model for selected functions.
 /// \param goto_model: Goto program to slice
 /// \param functions_list: The functions relevant for the slicing (i.e. starting
 ///   point for the search in the CFG). Anything that is reachable in the CFG
 ///   starting from these functions will be kept.
+/// \param message_handler: message handler
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &functions_list)
+  const std::list<std::string> &functions_list,
+  message_handlert &message_handler)
 {
   for(const auto &function : functions_list)
   {
     in_function_criteriont matching_criterion(function);
     reachability_slicert slicer;
-    slicer(goto_model.goto_functions, matching_criterion, true);
+    slicer(
+      goto_model.goto_functions, matching_criterion, true, message_handler);
   }
 
   remove_calls_no_bodyt remove_calls_no_body;
-  remove_calls_no_body(goto_model.goto_functions);
+  remove_calls_no_body(goto_model.goto_functions, message_handler);
 
   goto_model.goto_functions.update();
   goto_model.goto_functions.compute_loop_numbers();
@@ -445,19 +459,24 @@ void function_path_reachability_slicer(
 /// comprising all properties. Only instructions from which the criterion
 /// is reachable will be kept.
 /// \param goto_model: Goto program to slice
-void reachability_slicer(goto_modelt &goto_model)
+/// \param message_handler: message handler
+void reachability_slicer(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
 {
-  reachability_slicer(goto_model, false);
+  reachability_slicer(goto_model, false, message_handler);
 }
 
 /// Perform reachability slicing on goto_model for selected properties. Only
 /// instructions from which the criterion is reachable will be kept.
 /// \param goto_model: Goto program to slice
 /// \param properties: The properties relevant for the slicing (i.e. starting
 ///   point for the search in the cfg)
+/// \param message_handler: message handler
 void reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &properties)
+  const std::list<std::string> &properties,
+  message_handlert &message_handler)
 {
-  reachability_slicer(goto_model, properties, false);
+  reachability_slicer(goto_model, properties, false, message_handler);
 }

src/goto-instrument/reachability_slicer.h

@@ -16,25 +16,30 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <string>
 
 class goto_modelt;
+class message_handlert;
 
-void reachability_slicer(goto_modelt &);
+void reachability_slicer(goto_modelt &, message_handlert &);
 
 void reachability_slicer(
   goto_modelt &,
-  const std::list<std::string> &properties);
+  const std::list<std::string> &properties,
+  message_handlert &);
 
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::list<std::string> &functions_list);
+  const std::list<std::string> &functions_list,
+  message_handlert &);
 
 void reachability_slicer(
   goto_modelt &,
-  const bool include_forward_reachability);
+  const bool include_forward_reachability,
+  message_handlert &);
 
 void reachability_slicer(
   goto_modelt &,
   const std::list<std::string> &properties,
-  const bool include_forward_reachability);
+  const bool include_forward_reachability,
+  message_handlert &);
 
 // clang-format off
 #define OPT_REACHABILITY_SLICER                                                \

src/goto-instrument/reachability_slicer_class.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/goto_program.h>
 
 class goto_functionst;
+class message_handlert;
 class slicing_criteriont;
 
 class reachability_slicert
@@ -23,7 +24,8 @@ class reachability_slicert
   void operator()(
     goto_functionst &goto_functions,
     const slicing_criteriont &criterion,
-    bool include_forward_reachability);
+    bool include_forward_reachability,
+    message_handlert &);
 
 protected:
   struct slicer_entryt

src/goto-programs/remove_calls_no_body.cpp

@@ -12,6 +12,7 @@ Author: Daniel Poetzl
 #include "remove_calls_no_body.h"
 
 #include <util/invariant.h>
+#include <util/message.h>
 #include <util/std_code.h>
 
 #include "goto_functions.h"
@@ -94,14 +95,21 @@ bool remove_calls_no_bodyt::is_opaque_function_call(
 /// \param goto_program: goto program to operate on
 /// \param goto_functions: all goto functions; for looking up functions which
 ///   the goto program may call
-void remove_calls_no_bodyt::
-operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
+/// \param message_handler: message handler
+void remove_calls_no_bodyt::operator()(
+  goto_programt &goto_program,
+  const goto_functionst &goto_functions,
+  message_handlert &message_handler)
 {
   for(goto_programt::targett it = goto_program.instructions.begin();
       it != goto_program.instructions.end();) // no it++
   {
     if(is_opaque_function_call(it, goto_functions))
     {
+      messaget log{message_handler};
+      log.status() << "Removing call to "
+                   << to_symbol_expr(it->call_function()).get_identifier()
+                   << ", which has no body" << messaget::eom;
       remove_call_no_body(
         goto_program, it, it->call_lhs(), it->call_arguments());
     }
@@ -116,10 +124,13 @@ operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
 /// of the arguments of the call and a nondet assignment to the variable taking
 /// the return value.
 /// \param goto_functions: goto functions to operate on
-void remove_calls_no_bodyt::operator()(goto_functionst &goto_functions)
+/// \param message_handler: message handler
+void remove_calls_no_bodyt::operator()(
+  goto_functionst &goto_functions,
+  message_handlert &message_handler)
 {
   for(auto &gf_entry : goto_functions.function_map)
   {
-    (*this)(gf_entry.second.body, goto_functions);
+    (*this)(gf_entry.second.body, goto_functions, message_handler);
   }
 }

src/goto-programs/remove_calls_no_body.h

@@ -15,6 +15,7 @@ Author: Daniel Poetzl
 #include "goto_program.h"
 
 class goto_functionst;
+class message_handlert;
 
 class remove_calls_no_bodyt
 {
@@ -32,9 +33,10 @@ class remove_calls_no_bodyt
 public:
   void operator()(
     goto_programt &goto_program,
-    const goto_functionst &goto_functions);
+    const goto_functionst &goto_functions,
+    message_handlert &);
 
-  void operator()(goto_functionst &goto_functions);
+  void operator()(goto_functionst &goto_functions, message_handlert &);
 };
 
 #define OPT_REMOVE_CALLS_NO_BODY "(remove-calls-no-body)"