prevent half-constructed GOTO instructions

Author: Daniel Kroening

jbmc/regression/jbmc/generic_class_bound1/test.desc

@@ -3,10 +3,10 @@ Gn.class
 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-.*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 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
+.*file Gn.java line 6 function java::Gn.\<init\>:\(\)V bytecode-index 1 block .: FAILED
+.*file Gn.java line 9 function java::Gn.foo1:\(LGn;\)V bytecode-index 1 block .: FAILED
+.*file Gn.java line 10 function java::Gn.foo1:\(LGn;\)V bytecode-index 4 block .: FAILED
+.*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block .: SATISFIED
 --
 --
 This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable

jbmc/regression/jbmc/reachability-slice/test2.desc

@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 A.class
---reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.3' --cover location
+--reachability-slice-fb --show-goto-functions --property 'java::A.foo:(I)V.coverage.4' --cover location
 1001
 1002
 1003

jbmc/src/java_bytecode/remove_exceptions.cpp

@@ -306,9 +306,6 @@ void remove_exceptionst::add_exception_dispatch_sequence(
   // Jump to the universal handler or function end, as appropriate.
   // This will appear after the GOTO-based dynamic dispatch below
   goto_programt::targett default_dispatch=goto_program.insert_after(instr_it);
-  default_dispatch->make_goto();
-  default_dispatch->source_location=instr_it->source_location;
-  default_dispatch->function=instr_it->function;
 
   // find the symbol corresponding to the caught exceptions
   symbol_exprt exc_thrown =
@@ -356,7 +353,9 @@ void remove_exceptionst::add_exception_dispatch_sequence(
     }
   }
 
-  default_dispatch->set_target(default_target);
+  default_dispatch->make_goto(default_target);
+  default_dispatch->source_location=instr_it->source_location;
+  default_dispatch->function=instr_it->function;
 
   // add dead instructions
   for(const auto &local : locals)

src/goto-instrument/accelerate/accelerate.cpp

@@ -212,16 +212,12 @@ void acceleratet::insert_looping_path(
   ++loop_body;
 
   goto_programt::targett jump=program.insert_before(loop_body);
-  jump->make_goto();
-  jump->guard=side_effect_expr_nondett(bool_typet());
-  jump->targets.push_back(loop_body);
+  jump->make_goto(loop_body, side_effect_expr_nondett(bool_typet()));
 
   program.destructive_insert(loop_body, looping_path);
 
   jump=program.insert_before(loop_body);
-  jump->make_goto();
-  jump->guard=true_exprt();
-  jump->targets.push_back(back_jump);
+  jump->make_goto(back_jump, true_exprt());
 
   for(goto_programt::targett t=loop_header;
       t!=loop_body;

src/goto-instrument/branch.cpp

@@ -56,8 +56,7 @@ void branch(
         t1->function=f_it->first;
 
         goto_programt::targett t2=body.insert_after(t1);
-        t2->make_goto();
-        t2->targets=i_it->targets;
+        t2->make_goto(i_it->get_target());
 
         goto_programt::targett t3=body.insert_after(t2);
         t3->make_function_call(

src/goto-programs/goto_convert.cpp

@@ -138,6 +138,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
         throw 0;
       }
 
+      i.type=GOTO;
       i.targets.clear();
       i.targets.push_back(l_it->second.first);
 
@@ -1459,21 +1460,21 @@ void goto_convertt::convert_goto(
   const codet &code,
   goto_programt &dest)
 {
-  goto_programt::targett t=dest.add_instruction();
-  t->make_goto();
+  // this instruction will turn into a goto during post-processing
+  goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
   t->source_location=code.source_location();
   t->code=code;
 
-  // remember it to do target later
+  // remember it to do the target later
   targets.gotos.push_back(std::make_pair(t, targets.destructor_stack));
 }
 
 void goto_convertt::convert_gcc_computed_goto(
   const codet &code,
   goto_programt &dest)
 {
-  goto_programt::targett t=dest.add_instruction();
-  t->make_skip();
+  // this instruction will turn into OTHER during post-processing
+  goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
   t->source_location=code.source_location();
   t->code=code;
 

src/goto-programs/goto_program.h

@@ -237,7 +237,6 @@ class goto_programt
       code.make_nil();
     }
 
-    void make_goto() { clear(GOTO); }
     void make_return() { clear(RETURN); }
     void make_skip() { clear(SKIP); }
     void make_location(const source_locationt &l)
@@ -256,7 +255,7 @@ class goto_programt
 
     void make_goto(targett _target)
     {
-      make_goto();
+      clear(GOTO);
       targets.push_back(_target);
     }