Add utility function for remove_unreachable.

Author: martin

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -233,6 +233,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show", true);
   }
 
+  // For development allow slicing to be disabled in the simplify task
+  options.set_option("simplify-slicing", !(cmdline.isset("no-simplify-slicing")));
 
   // Abstract interpreter choice
   options.set_option("flow-sensitive", false);

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -39,8 +39,9 @@ class optionst;
   "(non-null)(show-non-null)" \
   "(constants)" \
   "(dependence-graph)" \
-  "(show)(verify)(simplify):"			\
-  "(flow-sensitive)(concurrent)"
+  "(show)(verify)(simplify):" \
+  "(flow-sensitive)(concurrent)" \
+  "(no-simplify-slicing)"
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,

src/goto-analyzer/static_simplifier.cpp

@@ -19,6 +19,9 @@ Author: Lucas Cordeiro, [email protected]
 #include <analyses/interval_domain.h>
 #include <analyses/constant_propagator.h>
 
+#include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unreachable.h>
+
 #include "static_simplifier.h"
 
 template<class analyzerT>
@@ -74,6 +77,21 @@ bool static_simplifiert<analyzerT>::operator()(void)
   status() << "Simplifying program" << eom;
   simplify_program();
 
+  // Remove obviously unreachable things and (now) unconditional branches
+  if (options.get_bool_option("simplify-slicing"))
+  {
+    status() << "Removing unreachable instructions" << eom;
+
+    remove_skip(goto_functions);  // Removes goto false
+    goto_functions.update();
+
+    remove_unreachable(goto_functions);  // Convert unreachable to skips
+    goto_functions.update();
+
+    remove_skip(goto_functions);  // Remove all of the new skips
+    goto_functions.update();
+  }
+
   status() << "Writing goto binary" << eom;
   return write_goto_binary(out, ns.get_symbol_table(), goto_functions);
 }

src/goto-programs/remove_unreachable.cpp

@@ -57,3 +57,10 @@ void remove_unreachable(goto_programt &goto_program)
       it->make_skip();
   }
 }
+
+void remove_unreachable(goto_functionst &goto_functions)
+{
+  Forall_goto_functions(f_it, goto_functions)
+    remove_unreachable(f_it->second.body);
+}
+

src/goto-programs/remove_unreachable.h

@@ -12,5 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "goto_functions.h"
 
 void remove_unreachable(goto_programt &goto_program);
+void remove_unreachable(goto_functionst &goto_functions);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H