Run remove_skip in passes that may introduce skips

The only passes left out are set_properties and remove_unreachable as the caller
may still find value in those instructions replaced by a skip. (This need not be
true and it may as well be safe to run remove_skip for those as well.)

Fixes: #2067

Author: tautschnig

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -26,6 +26,8 @@ Date:   December 2016
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include <analyses/uncaught_exceptions_analysis.h>
 
 /// Lowers high-level exception descriptions into low-level operations suitable
@@ -122,13 +124,13 @@ class remove_exceptionst
     const stack_catcht &stack_catch,
     const std::vector<exprt> &locals);
 
-  void instrument_throw(
+  bool instrument_throw(
     goto_programt &goto_program,
     const goto_programt::targett &,
     const stack_catcht &,
     const std::vector<exprt> &);
 
-  void instrument_function_call(
+  bool instrument_function_call(
     goto_programt &goto_program,
     const goto_programt::targett &,
     const stack_catcht &,
@@ -369,7 +371,7 @@ void remove_exceptionst::add_exception_dispatch_sequence(
 
 /// instruments each throw with conditional GOTOS to the corresponding
 /// exception handlers
-void remove_exceptionst::instrument_throw(
+bool remove_exceptionst::instrument_throw(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const remove_exceptionst::stack_catcht &stack_catch,
@@ -387,7 +389,7 @@ void remove_exceptionst::instrument_throw(
   // and this may reduce the instrumentation considerably if the programmer
   // used assertions)
   if(assertion_error)
-    return;
+    return false;
 
   add_exception_dispatch_sequence(
     goto_program, instr_it, stack_catch, locals);
@@ -403,11 +405,13 @@ void remove_exceptionst::instrument_throw(
   // now turn the `throw' into `assignment'
   instr_it->type=ASSIGN;
   instr_it->code=assignment;
+
+  return true;
 }
 
 /// instruments each function call that may escape exceptions with conditional
 /// GOTOS to the corresponding exception handlers
-void remove_exceptionst::instrument_function_call(
+bool remove_exceptionst::instrument_function_call(
   goto_programt &goto_program,
   const goto_programt::targett &instr_it,
   const stack_catcht &stack_catch,
@@ -441,7 +445,11 @@ void remove_exceptionst::instrument_function_call(
     t_null->source_location=instr_it->source_location;
     t_null->function=instr_it->function;
     t_null->guard=eq_null;
+
+    return true;
   }
+
+  return false;
 }
 
 /// instruments throws, function calls that may escape exceptions and exception
@@ -460,6 +468,8 @@ void remove_exceptionst::instrument_exceptions(
   bool program_or_callees_may_throw =
     function_or_callees_may_throw(goto_program);
 
+  bool did_something = false;
+
   Forall_goto_program_instructions(instr_it, goto_program)
   {
     if(instr_it->is_decl())
@@ -537,18 +547,22 @@ void remove_exceptionst::instrument_exceptions(
           "CATCH opcode should be one of push-catch, pop-catch, landingpad");
       }
       instr_it->make_skip();
+      did_something = true;
     }
     else if(instr_it->type==THROW)
     {
-      instrument_throw(
-        goto_program, instr_it, stack_catch, locals);
+      did_something |=
+        instrument_throw(goto_program, instr_it, stack_catch, locals);
     }
     else if(instr_it->type==FUNCTION_CALL)
     {
-      instrument_function_call(
-        goto_program, instr_it, stack_catch, locals);
+      did_something |=
+        instrument_function_call(goto_program, instr_it, stack_catch, locals);
     }
   }
+
+  if(did_something)
+    remove_skip(goto_program);
 }
 
 void remove_exceptionst::operator()(goto_functionst &goto_functions)

src/analyses/goto_check.cpp

@@ -31,6 +31,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include "local_bitvector_analysis.h"
 
 class goto_checkt
@@ -1501,6 +1503,8 @@ void goto_checkt::goto_check(
   assertions.clear();
   mode = _mode;
 
+  bool did_something = false;
+
   local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
   local_bitvector_analysis=&local_bitvector_analysis_obj;
 
@@ -1651,13 +1655,15 @@ void goto_checkt::goto_check(
          (!is_user_provided && !enable_built_in_assertions))
       {
         i.make_skip();
+        did_something = true;
       }
     }
     else if(i.is_assume())
     {
       if(!enable_assumptions)
       {
         i.make_skip();
+        did_something = true;
       }
     }
     else if(i.is_dead())
@@ -1745,6 +1751,7 @@ void goto_checkt::goto_check(
     }
 
     // insert new instructions -- make sure targets are not moved
+    did_something |= !new_code.instructions.empty();
 
     while(!new_code.instructions.empty())
     {
@@ -1753,6 +1760,9 @@ void goto_checkt::goto_check(
       it++;
     }
   }
+
+  if(did_something)
+    remove_skip(goto_program);
 }
 
 void goto_check(

src/goto-instrument/cover.cpp

@@ -20,6 +20,8 @@ Date: May 2016
 #include <util/options.h>
 #include <util/deprecate.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include "cover_basic_blocks.h"
 
 /// Applies instrumenters to given goto program
@@ -293,7 +295,7 @@ static void instrument_cover_goals(
   }
 
   if(changed)
-    function.body.update();
+    remove_skip(function.body);
 }
 
 /// Instruments a single goto program based on the given configuration

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -174,9 +174,6 @@ int goto_instrument_parse_optionst::doit()
         goto_unwindt goto_unwind;
         goto_unwind(goto_model, unwindset, unwind_strategy);
 
-        goto_model.goto_functions.update();
-        goto_model.goto_functions.compute_loop_numbers();
-
         if(cmdline.isset("log"))
         {
           std::string filename=cmdline.get_value("log");
@@ -202,6 +199,10 @@ int goto_instrument_parse_optionst::doit()
             std::cout << result << '\n';
           }
         }
+
+        // goto_unwind holds references to instructions, only do remove_skip
+        // after having generated the log above
+        remove_skip(goto_model);
       }
     }
 

src/goto-programs/generate_function_bodies.cpp

@@ -13,6 +13,8 @@ Author: Diffblue Ltd.
 #include <util/make_unique.h>
 #include <util/string_utils.h>
 
+#include "remove_skip.h"
+
 void generate_function_bodiest::generate_function_body(
   goto_functiont &function,
   symbol_tablet &symbol_table,
@@ -307,6 +309,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     }
     auto end_function_instruction = add_instruction();
     end_function_instruction->make_end_function();
+
+    remove_skip(function.body);
   }
 
 private:

src/goto-programs/remove_asm.cpp

@@ -20,6 +20,7 @@ Date:   December 2014
 #include <assembler/assembler_parser.h>
 
 #include "goto_model.h"
+#include "remove_skip.h"
 
 class remove_asmt
 {
@@ -280,20 +281,26 @@ void remove_asmt::process_instruction(
 void remove_asmt::process_function(
   goto_functionst::goto_functiont &goto_function)
 {
+  bool did_something = false;
+
   Forall_goto_program_instructions(it, goto_function.body)
   {
     if(it->is_other() && it->code.get_statement()==ID_asm)
     {
       goto_programt tmp_dest;
       process_instruction(*it, tmp_dest);
       it->make_skip();
+      did_something = true;
 
       goto_programt::targett next=it;
       next++;
 
       goto_function.body.destructive_insert(next, tmp_dest);
     }
   }
+
+  if(did_something)
+    remove_skip(goto_function.body);
 }
 
 /// removes assembler

src/goto-programs/remove_returns.cpp

@@ -17,6 +17,8 @@ Date:   September 2009
 
 #include "goto_model.h"
 
+#include "remove_skip.h"
+
 class remove_returnst
 {
 public:
@@ -342,6 +344,8 @@ bool remove_returnst::restore_returns(
 
   goto_programt &goto_program=f_it->second.body;
 
+  bool did_something = false;
+
   Forall_goto_program_instructions(i_it, goto_program)
   {
     if(i_it->is_assign())
@@ -355,9 +359,13 @@ bool remove_returnst::restore_returns(
       const exprt rhs = assign.rhs();
       i_it->make_return();
       i_it->code = code_returnt(rhs);
+      did_something = true;
     }
   }
 
+  if(did_something)
+    remove_skip(goto_program);
+
   return false;
 }