Merge pull request #2089 from tautschnig/remove-skip-cleanup

Run remove_skip and goto_program.update() in passes that may introduce skips

Author: tautschnig

jbmc/regression/jbmc/generic_class_bound1/test.desc

@@ -6,7 +6,6 @@ Gn.class
 .*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block 1: FAILED
 .*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block 1: FAILED
 .*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block 2: FAILED
-.*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED
 .*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
 --
 --

jbmc/regression/jbmc/virtual8/A.class

@@ -10,16 +10,16 @@ public static void main() {
 }
 
 class A {
-  void f() { }
+  int f() { return 0; }
 }
 
 
 class B extends A {
-  void f() { }
+  int f() { return 0; }
 }
 
 class C extends A {
-  void f() { }
+  int f() { return 0; }
 }
 
 class D extends C {

jbmc/regression/jbmc/virtual8/B.class

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

jbmc/regression/jbmc/virtual8/C.class

@@ -288,8 +288,6 @@ void replace_java_nondet(goto_model_functiont &function)
   goto_programt &program = function.get_goto_function().body;
   replace_java_nondet(program);
 
-  function.compute_location_numbers();
-
   remove_skip(program);
 }
 
@@ -300,8 +298,6 @@ void replace_java_nondet(goto_functionst &goto_functions)
     replace_java_nondet(goto_program.second.body);
   }
 
-  goto_functions.compute_location_numbers();
-
   remove_skip(goto_functions);
 }
 

jbmc/regression/jbmc/virtual8/D.class

@@ -988,7 +988,6 @@ bool jbmc_parse_optionst::process_goto_functions(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   catch(const char *e)

jbmc/regression/jbmc/virtual8/E.class

@@ -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
@@ -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;
 
@@ -1649,12 +1653,18 @@ void goto_checkt::goto_check(
       if((is_user_provided && !enable_assertions &&
           i.source_location.get_property_class()!="error label") ||
          (!is_user_provided && !enable_built_in_assertions))
-        i.type=SKIP;
+      {
+        i.make_skip();
+        did_something = true;
+      }
     }
     else if(i.is_assume())
     {
       if(!enable_assumptions)
-        i.type=SKIP;
+      {
+        i.make_skip();
+        did_something = true;
+      }
     }
     else if(i.is_dead())
     {
@@ -1741,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())
     {
@@ -1749,6 +1760,9 @@ void goto_checkt::goto_check(
       it++;
     }
   }
+
+  if(did_something)
+    remove_skip(goto_program);
 }
 
 void goto_check(

jbmc/regression/jbmc/virtual8/Test.class

@@ -158,16 +158,13 @@ bool static_simplifier(
     m.status() << "Removing unreachable instructions" << messaget::eom;
 
     // Removes goto false
-    remove_skip(goto_model.goto_functions);
-    goto_model.goto_functions.update();
+    remove_skip(goto_model);
 
     // Convert unreachable to skips
     remove_unreachable(goto_model.goto_functions);
-    goto_model.goto_functions.update();
 
     // Remove all of the new skips
-    remove_skip(goto_model.goto_functions);
-    goto_model.goto_functions.update();
+    remove_skip(goto_model);
   }
 
   // restore return types before writing the binary

jbmc/regression/jbmc/virtual8/Test.java

@@ -132,7 +132,6 @@ void full_slicert::operator()(
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -425,13 +425,13 @@ bool goto_diff_parse_optionst::process_goto_program(
     // add loop ids
     goto_model.goto_functions.compute_loop_numbers();
 
-    // remove skips such that trivial GOTOs are deleted and not considered
-    // for coverage annotation:
-    remove_skip(goto_model);
-
     // instrument cover goals
     if(cmdline.isset("cover"))
     {
+      // remove skips such that trivial GOTOs are deleted and not considered
+      // for coverage annotation:
+      remove_skip(goto_model);
+
       if(instrument_cover_goals(options, goto_model, get_message_handler()))
         return true;
     }
@@ -445,7 +445,6 @@ bool goto_diff_parse_optionst::process_goto_program(
 
     // remove any skips introduced since coverage instrumentation
     remove_skip(goto_model);
-    goto_model.goto_functions.update();
   }
 
   catch(const char *e)

jbmc/src/java_bytecode/replace_java_nondet.cpp

@@ -21,7 +21,6 @@ Author: Matt Lewis
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/wp.h>
-#include <goto-programs/remove_skip.h>
 #include <goto-programs/goto_functions.h>
 
 #include <goto-symex/goto_symex.h>

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -29,7 +29,6 @@ bool scratch_programt::check_sat(bool do_slice)
   add_instruction(END_FUNCTION);
 
   remove_skip(*this);
-  update();
 
 #ifdef DEBUG
   std::cout << "Checking following program for satness:\n";

src/analyses/goto_check.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-analyzer/static_simplifier.cpp

@@ -364,7 +364,6 @@ void full_slicert::operator()(
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 void full_slicer(

src/goto-diff/change_impact.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);
       }
     }
 
@@ -707,7 +708,6 @@ int goto_instrument_parse_optionst::doit()
       accelerate_functions(
         goto_model, get_message_handler(), cmdline.isset("z3"));
       remove_skip(goto_model);
-      goto_model.goto_functions.update();
     }
 
     if(cmdline.isset("horn-encoding"))

src/goto-diff/goto_diff_parse_options.cpp

@@ -182,8 +182,6 @@ bool model_argc_argv(
 
   // update counters etc.
   remove_skip(start);
-  start.compute_loop_numbers();
-  goto_model.goto_functions.update();
 
   return false;
 }

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -206,7 +206,6 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
 
   // remove the skips
   remove_skip(goto_functions);
-  goto_functions.update();
 }
 
 /// Perform reachability slicing on goto_model, with respect to the

src/goto-instrument/accelerate/scratch_program.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-instrument/cover.cpp

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
-#include "remove_skip.h"
 #include "goto_inline_class.h"
 
 void goto_inline(