Reachability slice requires function bodies

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/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+void undefined_function();
+
+void a()
+{
+  undefined_function();
+}
+
+void b()
+{
+  int should_be_sliced_away;
+}
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  a();
+  __CPROVER_assert(0, "reach me");
+  b();
+}

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

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

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;
@@ -1066,8 +1066,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // we add the library in some cases, as some analyses benefit
 
-  if(cmdline.isset("add-library") ||
-     cmdline.isset("mm"))
+  if(
+    cmdline.isset("add-library") || cmdline.isset("mm") ||
+    cmdline.isset("reachability-slice") ||
+    cmdline.isset("reachability-slice-fb") ||
+    cmdline.isset("fp-reachability-slice"))
   {
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))
@@ -1245,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();
@@ -1602,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"))
@@ -1614,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?
@@ -1687,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

@@ -13,17 +13,46 @@ Author: Daniel Kroening, [email protected]
 /// (and possibly, depending on the parameters, keep those that can be reached
 /// from the criterion).
 
-#include "reachability_slicer.h"
+#include "full_slicer_class.h"
+#include "reachability_slicer_class.h"
+
+#include <util/exception_utils.h>
 
 #include <goto-programs/cfg.h>
 #include <goto-programs/remove_calls_no_body.h>
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/remove_unreachable.h>
 
-#include <util/exception_utils.h>
+#include <analyses/is_threaded.h>
 
-#include "full_slicer_class.h"
-#include "reachability_slicer_class.h"
+#include "reachability_slicer.h"
+
+void reachability_slicert::operator()(
+  goto_functionst &goto_functions,
+  const slicing_criteriont &criterion,
+  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, message_handler);
+  goto_functions.update();
+
+  cfg(goto_functions);
+  for(const auto &gf_entry : goto_functions.function_map)
+  {
+    forall_goto_program_instructions(i_it, gf_entry.second.body)
+      cfg[cfg.entry_map[i_it]].function_id = gf_entry.first;
+  }
+
+  is_threadedt is_threaded(goto_functions);
+  fixedpoint_to_assertions(is_threaded, criterion);
+  if(include_forward_reachability)
+    fixedpoint_from_assertions(is_threaded, criterion);
+  slice(goto_functions);
+}
 
 /// Get the set of nodes that correspond to the given criterion, or that can
 /// appear in concurrent execution. None of these should be sliced away so
@@ -364,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.
@@ -380,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();
@@ -417,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, [email protected]
 #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

@@ -12,11 +12,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
 #define CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H
 
-#include <goto-programs/goto_functions.h>
-#include <goto-programs/cfg.h>
-
-#include <analyses/is_threaded.h>
+#include <goto-programs/goto_program.h>
 
+class goto_functionst;
+class message_handlert;
 class slicing_criteriont;
 
 class reachability_slicert
@@ -25,21 +24,8 @@ class reachability_slicert
   void operator()(
     goto_functionst &goto_functions,
     const slicing_criteriont &criterion,
-    bool include_forward_reachability)
-  {
-    cfg(goto_functions);
-    for(const auto &gf_entry : goto_functions.function_map)
-    {
-      forall_goto_program_instructions(i_it, gf_entry.second.body)
-        cfg[cfg.entry_map[i_it]].function_id = gf_entry.first;
-    }
-
-    is_threadedt is_threaded(goto_functions);
-    fixedpoint_to_assertions(is_threaded, criterion);
-    if(include_forward_reachability)
-      fixedpoint_from_assertions(is_threaded, criterion);
-    slice(goto_functions);
-  }
+    bool include_forward_reachability,
+    message_handlert &);
 
 protected:
   struct slicer_entryt