From 309d20704ed4a4a47cddb534f22349db0793e085 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 13 Jun 2018 15:49:00 +0100 Subject: [PATCH 1/2] remove conversion for non-deterministic-goto --- src/goto-programs/goto_convert.cpp | 23 +---------------------- 1 file changed, 1 insertion(+), 22 deletions(-) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 34384f590e5..14e5dc3dc57 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -109,28 +109,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) { goto_programt::instructiont &i=*(g_it.first); - if(i.code.get_statement()=="non-deterministic-goto") - { - const irept &destinations=i.code.find("destinations"); - - i.make_goto(); - - forall_irep(it, destinations.get_sub()) - { - labelst::const_iterator l_it= - targets.labels.find(it->id_string()); - - if(l_it==targets.labels.end()) - { - error().source_location=i.code.find_source_location(); - error() << "goto label `" << it->id() << "' not found" << eom; - throw 0; - } - - i.targets.push_back(l_it->second.first); - } - } - else if(i.is_start_thread()) + if(i.is_start_thread()) { const irep_idt &goto_label=i.code.get(ID_destination); From 199d4cc841de1eb83e1afe2d741924bd741810dc Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 13 Jun 2018 15:49:41 +0100 Subject: [PATCH 2/2] prevent half-constructed GOTO instructions --- jbmc/regression/jbmc/generic_class_bound1/test.desc | 8 ++++---- jbmc/regression/jbmc/reachability-slice/test2.desc | 2 +- jbmc/src/java_bytecode/remove_exceptions.cpp | 7 +++---- src/goto-instrument/accelerate/accelerate.cpp | 8 ++------ src/goto-instrument/branch.cpp | 3 +-- src/goto-programs/goto_convert.cpp | 11 ++++++----- src/goto-programs/goto_program.h | 3 +-- 7 files changed, 18 insertions(+), 24 deletions(-) diff --git a/jbmc/regression/jbmc/generic_class_bound1/test.desc b/jbmc/regression/jbmc/generic_class_bound1/test.desc index 92f3f36c32f..d4d425ec194 100644 --- a/jbmc/regression/jbmc/generic_class_bound1/test.desc +++ b/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.\:\(\)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.\:\(\)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 diff --git a/jbmc/regression/jbmc/reachability-slice/test2.desc b/jbmc/regression/jbmc/reachability-slice/test2.desc index d8eea80d626..2e95cfa5107 100644 --- a/jbmc/regression/jbmc/reachability-slice/test2.desc +++ b/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 diff --git a/jbmc/src/java_bytecode/remove_exceptions.cpp b/jbmc/src/java_bytecode/remove_exceptions.cpp index 25ee5b2985c..b5082e4def1 100644 --- a/jbmc/src/java_bytecode/remove_exceptions.cpp +++ b/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) diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 0359d926e2a..50cff3f5b35 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/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; diff --git a/src/goto-instrument/branch.cpp b/src/goto-instrument/branch.cpp index 54abd3ed07e..913bf526b31 100644 --- a/src/goto-instrument/branch.cpp +++ b/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( diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 14e5dc3dc57..298f61aefb5 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/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,12 +1460,12 @@ 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)); } @@ -1472,8 +1473,8 @@ 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; diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index a630acafdb6..c4c7361cfa8 100644 --- a/src/goto-programs/goto_program.h +++ b/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); }