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: diffblue#2067

Author: tautschnig

src/analyses/goto_check.cpp

@@ -31,6 +31,8 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 #include <langapi/mode.h>
 
+#include <goto-programs/remove_skip.h>
+
 #include "local_bitvector_analysis.h"
 
 class goto_checkt
@@ -1475,6 +1477,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;
 
@@ -1625,13 +1629,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())
@@ -1719,6 +1725,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())
     {
@@ -1727,6 +1734,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
@@ -283,7 +285,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

@@ -204,9 +204,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");
@@ -232,6 +229,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

@@ -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,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

@@ -22,6 +22,8 @@ Date:   December 2014
 
 #include <assembler/assembler_parser.h>
 
+#include "remove_skip.h"
+
 class remove_asmt
 {
 public:
@@ -281,20 +283,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

@@ -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,13 @@ bool remove_returnst::restore_returns(
 
       i_it->make_return();
       i_it->code=return_code;
+      did_something = true;
     }
   }
 
+  if(did_something)
+    remove_skip(goto_program);
+
   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>
@@ -31,7 +31,7 @@ class remove_virtual_functionst
 
   bool remove_virtual_functions(goto_programt &goto_program);
 
-  void remove_virtual_function(
+  goto_programt::targett remove_virtual_function(
     goto_programt &goto_program,
     goto_programt::targett target,
     const dispatch_table_entriest &functions,
@@ -45,7 +45,7 @@ class remove_virtual_functionst
 
   const class_hierarchyt &class_hierarchy;
 
-  void remove_virtual_function(
+  goto_programt::targett remove_virtual_function(
     goto_programt &goto_program,
     goto_programt::targett target);
   typedef std::function<
@@ -73,7 +73,7 @@ remove_virtual_functionst::remove_virtual_functionst(
 {
 }
 
-void remove_virtual_functionst::remove_virtual_function(
+goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   goto_programt &goto_program,
   goto_programt::targett target)
 {
@@ -91,7 +91,7 @@ void remove_virtual_functionst::remove_virtual_function(
   dispatch_table_entriest functions;
   get_functions(function, functions);
 
-  remove_virtual_function(
+  return remove_virtual_function(
     goto_program,
     target,
     functions,
@@ -120,7 +120,7 @@ static void create_static_function_call(
     call.arguments()[0].make_typecast(need_type);
 }
 
-void remove_virtual_functionst::remove_virtual_function(
+goto_programt::targett remove_virtual_functionst::remove_virtual_function(
   goto_programt &goto_program,
   goto_programt::targett target,
   const dispatch_table_entriest &functions,
@@ -132,24 +132,30 @@ void remove_virtual_functionst::remove_virtual_function(
   const code_function_callt &code=
     to_code_function_call(target->code);
 
+  goto_programt::targett next_target = std::next(target);
+
   if(functions.empty())
   {
     target->make_skip();
-    return; // give up
+    remove_skip(goto_program, target, next_target);
+    return next_target; // give up
   }
 
   // only one option?
   if(functions.size()==1 &&
      fallback_action==virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION)
   {
     if(functions.begin()->symbol_expr==symbol_exprt())
+    {
       target->make_skip();
+      remove_skip(goto_program, target, next_target);
+    }
     else
     {
       create_static_function_call(
         to_code_function_call(target->code), functions.front().symbol_expr, ns);
     }
-    return;
+    return next_target;
   }
 
   const auto &vcall_source_loc=target->source_location;
@@ -283,13 +289,14 @@ void remove_virtual_functionst::remove_virtual_function(
       it->source_location.set_comment(comment);
   }
 
-  goto_programt::targett next_target=target;
-  next_target++;
-
   goto_program.destructive_insert(next_target, new_code);
 
   // finally, kill original invocation
   target->make_skip();
+
+  remove_skip(goto_program, target, next_target);
+
+  return next_target;
 }
 
 /// Used by get_functions to track the most-derived parent that provides an
@@ -472,23 +479,29 @@ bool remove_virtual_functionst::remove_virtual_functions(
 {
   bool did_something=false;
 
-  Forall_goto_program_instructions(target, goto_program)
+  for(goto_programt::instructionst::iterator
+      target = goto_program.instructions.begin();
+      target != goto_program.instructions.end();
+      ) // no ++target
+  {
     if(target->is_function_call())
     {
       const code_function_callt &code=
         to_code_function_call(target->code);
 
       if(code.function().id()==ID_virtual_function)
       {
-        remove_virtual_function(goto_program, target);
+        target = remove_virtual_function(goto_program, target);
         did_something=true;
+        continue;
       }
     }
 
+    ++target;
+  }
+
   if(did_something)
-  {
     goto_program.update();
-  }
 
   return did_something;
 }
@@ -536,7 +549,7 @@ void remove_virtual_functions(goto_model_functiont &function)
   rvf.remove_virtual_functions(function.get_goto_function().body);
 }
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   symbol_tablet &symbol_table,
   goto_programt &goto_program,
   goto_programt::targett instruction,
@@ -547,18 +560,22 @@ void remove_virtual_function(
   class_hierarchy(symbol_table);
   remove_virtual_functionst rvf(symbol_table, class_hierarchy);
 
-  rvf.remove_virtual_function(
+  goto_programt::targett next = rvf.remove_virtual_function(
     goto_program, instruction, dispatch_table, fallback_action);
+
+  goto_program.update();
+
+  return next;
 }
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   goto_modelt &goto_model,
   goto_programt &goto_program,
   goto_programt::targett instruction,
   const dispatch_table_entriest &dispatch_table,
   virtual_dispatch_fallback_actiont fallback_action)
 {
-  remove_virtual_function(
+  return remove_virtual_function(
     goto_model.symbol_table,
     goto_program,
     instruction,

src/goto-programs/remove_virtual_functions.h

@@ -59,14 +59,14 @@ class dispatch_table_entryt
 typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
 typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   goto_modelt &goto_model,
   goto_programt &goto_program,
   goto_programt::targett instruction,
   const dispatch_table_entriest &dispatch_table,
   virtual_dispatch_fallback_actiont fallback_action);
 
-void remove_virtual_function(
+goto_programt::targett remove_virtual_function(
   symbol_tablet &symbol_table,
   goto_programt &goto_program,
   goto_programt::targett instruction,

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,7 +267,7 @@ void string_instrumentationt::do_function_call(
     else if(identifier=="fscanf")
       do_fscanf(dest, target, call);
 
-    dest.update();
+    remove_skip(dest);
   }
 }