Run remove_skip and goto_program.update() 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: diffblue#2067

Author: tautschnig

src/analyses/goto_check.cpp

@@ -28,6 +28,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/options.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include <langapi/language_util.h>
 
 #include "local_bitvector_analysis.h"
@@ -1477,6 +1479,7 @@ void goto_checkt::goto_check(
   const irep_idt &mode)
 {
   assertions.clear();
+  bool did_something = false;
 
   local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
   local_bitvector_analysis=&local_bitvector_analysis_obj;
@@ -1628,13 +1631,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())
@@ -1722,6 +1727,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())
     {
@@ -1730,6 +1736,12 @@ void goto_checkt::goto_check(
       it++;
     }
   }
+
+  if(did_something)
+  {
+    remove_skip(goto_program);
+    goto_program.update();
+  }
 }
 
 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
@@ -283,7 +285,10 @@ static void instrument_cover_goals(
   }
 
   if(changed)
+  {
+    remove_skip(function.body);
     function.body.update();
+  }
 }
 
 /// Instruments a single goto program based on the given configuration

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -207,9 +207,6 @@ int goto_instrument_parse_optionst::doit()
         goto_unwindt goto_unwind;
         goto_unwind(goto_model, unwind_set, k, 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");
@@ -235,6 +232,12 @@ 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);
+        goto_model.goto_functions.update();
+        goto_model.goto_functions.compute_loop_numbers();
       }
     }
 

src/goto-programs/generate_function_bodies.cpp

@@ -20,6 +20,8 @@ Author: Diffblue Ltd.
 #include <util/pointer_offset_size.h>
 #include <util/arith_tools.h>
 
+#include "remove_skip.h"
+
 void generate_function_bodiest::generate_function_body(
   goto_functiont &function,
   symbol_tablet &symbol_table,
@@ -314,6 +316,9 @@ 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);
+    function.body.update();
   }
 
 private:

src/goto-programs/remove_asm.cpp

@@ -22,6 +22,8 @@ Date:   December 2014
 
 #include <assembler/assembler_parser.h>
 
+#include "remove_skip.h"
+
 class remove_asmt
 {
 public:
@@ -281,20 +283,29 @@ 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);
+    goto_function.body.update();
+  }
 }
 
 /// removes assembler

src/goto-programs/remove_returns.cpp

@@ -16,6 +16,8 @@ Date:   September 2009
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
+#include "remove_skip.h"
+
 class remove_returnst
 {
 public:
@@ -341,6 +343,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())
@@ -383,9 +387,16 @@ bool remove_returnst::restore_returns(
 
       i_it->make_return();
       i_it->code=return_code;
+      did_something = true;
     }
   }
 
+  if(did_something)
+  {
+    remove_skip(goto_program);
+    goto_program.update();
+  }
+
   return false;
 }
 

src/goto-programs/remove_virtual_functions.cpp

@@ -13,8 +13,8 @@ Author: Daniel Kroening, [email protected]
 #include "remove_virtual_functions.h"
 #include "class_hierarchy.h"
 #include "class_identifier.h"
-
-#include <goto-programs/resolve_inherited_component.h>
+#include "remove_skip.h"
+#include "resolve_inherited_component.h"
 
 #include <util/c_types.h>
 #include <util/prefix.h>
@@ -487,6 +487,7 @@ bool remove_virtual_functionst::remove_virtual_functions(
 
   if(did_something)
   {
+    remove_skip(goto_program);
     goto_program.update();
   }
 
@@ -549,6 +550,9 @@ void remove_virtual_function(
 
   rvf.remove_virtual_function(
     goto_program, instruction, dispatch_table, fallback_action);
+
+  remove_skip(goto_program);
+  goto_program.update();
 }
 
 void remove_virtual_function(

src/goto-programs/string_instrumentation.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/format_strings.h>
 #include <goto-programs/goto_model.h>
+#include <goto-programs/remove_skip.h>
 
 
 exprt is_zero_string(
@@ -266,6 +267,7 @@ void string_instrumentationt::do_function_call(
     else if(identifier=="fscanf")
       do_fscanf(dest, target, call);
 
+    remove_skip(dest);
     dest.update();
   }
 }

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,25 @@ 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(
+      did_something |= instrument_throw(
         goto_program, instr_it, stack_catch, locals);
     }
     else if(instr_it->type==FUNCTION_CALL)
     {
-      instrument_function_call(
+      did_something |= instrument_function_call(
         goto_program, instr_it, stack_catch, locals);
     }
   }
+
+  if(did_something)
+  {
+    remove_skip(goto_program);
+    goto_program.update();
+  }
 }
 
 void remove_exceptionst::operator()(goto_functionst &goto_functions)