diff --git a/regression/cbmc/goto5/main.c b/regression/cbmc/goto5/main.c new file mode 100644 index 00000000000..f4e45d2330e --- /dev/null +++ b/regression/cbmc/goto5/main.c @@ -0,0 +1,15 @@ +#include + +int main(void) +{ + int r = 0; + + if(r == 0) + { + goto l1; + r = 1; + } + +l1: + assert(r != 0); // expected to fail +} diff --git a/regression/cbmc/goto5/test.desc b/regression/cbmc/goto5/test.desc new file mode 100644 index 00000000000..6de79559914 --- /dev/null +++ b/regression/cbmc/goto5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index d02afd0ae6c..55236145ab8 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -719,6 +719,7 @@ void goto_rw(goto_programt::const_targett target, switch(target->type) { case NO_INSTRUCTION_TYPE: + case INCOMPLETE_GOTO: UNREACHABLE; break; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 2480dea2729..aa1b96bab13 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -245,6 +245,7 @@ goto_programt::const_targett goto_program2codet::convert_instruction( return convert_catch(target, upper_bound, dest); case NO_INSTRUCTION_TYPE: + case INCOMPLETE_GOTO: UNREACHABLE; } diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index da7bec886b9..ee77dd6ce37 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -418,6 +418,7 @@ void cfg_baset::compute_edges( break; case NO_INSTRUCTION_TYPE: + case INCOMPLETE_GOTO: UNREACHABLE; break; } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 9833cc07775..0dbe67d20b5 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -138,9 +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); + i.complete_goto(l_it->second.first); // If the goto recorded a destructor stack, execute as much as is // appropriate for however many automatic variables leave scope. @@ -234,45 +232,49 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) targets.computed_gotos.clear(); } -/// For each if(x) goto z; goto y; z: emitted, see if any destructor statements -/// were inserted between goto z and z, and if not, simplify into if(!x) goto y; +/// Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" +/// This only works if the "goto y" is not a branch target. /// \par parameters: Destination goto program -void goto_convertt::finish_guarded_gotos(goto_programt &dest) +void goto_convertt::optimize_guarded_gotos(goto_programt &dest) { - for(auto &gg : guarded_gotos) + // We cannot use a set of targets, as target iterators + // cannot be compared at this stage. + + // collect targets: reset marking + for(auto &i : dest.instructions) + i.target_number = goto_programt::instructiont::nil_target; + + // mark the goto targets + unsigned cnt = 0; + for(const auto &i : dest.instructions) + if(i.is_goto()) + i.get_target()->target_number = (++cnt); + + for(auto it = dest.instructions.begin(); it != dest.instructions.end(); it++) { - // Check if any destructor code has been inserted: - bool destructor_present=false; - for(auto it=gg.ifiter; - it!=gg.gotoiter && !destructor_present; - ++it) - { - if(!(it->is_goto() || it->is_skip())) - destructor_present=true; - } + if(!it->is_goto()) + continue; + + auto it_goto_y = std::next(it); - // If so, can't simplify. - if(destructor_present) + if( + it_goto_y == dest.instructions.end() || !it_goto_y->is_goto() || + !it_goto_y->guard.is_true() || it_goto_y->is_target()) continue; - // Simplify: remove whatever code was generated for the condition - // and attach the original guard to the goto instruction. - gg.gotoiter->guard=gg.guard; - // inherit the source location (otherwise the guarded goto will - // have the source location of the else branch) - gg.gotoiter->source_location=gg.ifiter->source_location; - // goto_programt doesn't provide an erase operation, - // perhaps for a good reason, so let's be cautious and just - // flatten the unneeded instructions into skips. - for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it) - it->make_skip(); - } + auto it_z = std::next(it_goto_y); - // Must clear this, as future functions may be converted - // using the same instance of goto_convertt, typically via - // goto_convert_functions. + if(it_z == dest.instructions.end()) + continue; - guarded_gotos.clear(); + // cannot compare iterators, so compare target number instead + if(it->get_target()->target_number == it_z->target_number) + { + it->set_target(it_goto_y->get_target()); + it->guard = boolean_negate(it->guard); + it_goto_y->make_skip(); + } + } } void goto_convertt::goto_convert( @@ -288,14 +290,11 @@ void goto_convertt::goto_convert_rec( goto_programt &dest, const irep_idt &mode) { - // Check that guarded_gotos was cleared after any previous use of this - // converter instance: - PRECONDITION(guarded_gotos.empty()); convert(code, dest, mode); finish_gotos(dest, mode); finish_computed_gotos(dest); - finish_guarded_gotos(dest); + optimize_guarded_gotos(dest); finish_catch_push_targets(dest); } @@ -493,13 +492,11 @@ void goto_convertt::convert( else if(statement==ID_continue) convert_continue(to_code_continue(code), dest, mode); else if(statement==ID_goto) - convert_goto(code, dest); + convert_goto(to_code_goto(code), dest); else if(statement==ID_gcc_computed_goto) convert_gcc_computed_goto(code, dest); else if(statement==ID_skip) convert_skip(code, dest); - else if(statement=="non-deterministic-goto") - convert_non_deterministic_goto(code, dest); else if(statement==ID_ifthenelse) convert_ifthenelse(to_code_ifthenelse(code), dest, mode); else if(statement==ID_start_thread) @@ -1456,16 +1453,12 @@ void goto_convertt::convert_continue( t->source_location=code.source_location(); } -void goto_convertt::convert_goto( - const codet &code, - goto_programt &dest) +void goto_convertt::convert_goto(const code_gotot &code, goto_programt &dest) { // this instruction will be completed during post-processing - // it is required to mark this as GOTO in order to enable - // simplifications in generate_ifthenelse - goto_programt::targett t = dest.add_instruction(GOTO); + goto_programt::targett t = dest.add_instruction(); + t->make_incomplete_goto(code); t->source_location=code.source_location(); - t->code=code; // remember it to do the target later targets.gotos.push_back(std::make_pair(t, targets.destructor_stack)); @@ -1484,13 +1477,6 @@ void goto_convertt::convert_gcc_computed_goto( targets.computed_gotos.push_back(t); } -void goto_convertt::convert_non_deterministic_goto( - const codet &code, - goto_programt &dest) -{ - convert_goto(code, dest); -} - void goto_convertt::convert_start_thread( const codet &code, goto_programt &dest) @@ -1649,24 +1635,7 @@ void goto_convertt::generate_ifthenelse( return; } - bool is_guarded_goto=false; - - // do guarded gotos directly - if(is_empty(false_case) && - is_size_one(true_case) && - true_case.instructions.back().is_goto() && - true_case.instructions.back().guard.is_true() && - true_case.instructions.back().labels.empty()) - { - // The above conjunction deliberately excludes the instance - // if(some) { label: goto somewhere; } - // Don't perform the transformation here, as code might get inserted into - // the true case to perform destructors. - // This will be attempted in finish_guarded_gotos. - is_guarded_goto=true; - } - - // similarly, do guarded assertions directly + // do guarded assertions directly if(is_size_one(true_case) && true_case.instructions.back().is_assert() && true_case.instructions.back().guard.is_false() && @@ -1779,13 +1748,6 @@ void goto_convertt::generate_ifthenelse( assert(!tmp_w.instructions.empty()); x->source_location=tmp_w.instructions.back().source_location; - // See if we can simplify this guarded goto later. - // Note this depends on the fact that `instructions` is a std::list - // and so goto-program-destructive-append preserves iterator validity. - if(is_guarded_goto) - guarded_gotos.push_back( - {tmp_v.instructions.begin(), tmp_w.instructions.begin(), guard}); - dest.destructive_append(tmp_v); dest.destructive_append(tmp_w); diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 273bf099da9..2648f43670b 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -268,10 +268,9 @@ class goto_convertt:public messaget const irep_idt &mode); void convert_init(const codet &code, goto_programt &dest, const irep_idt &mode); - void convert_goto(const codet &code, goto_programt &dest); + void convert_goto(const code_gotot &code, goto_programt &dest); void convert_gcc_computed_goto(const codet &code, goto_programt &dest); void convert_skip(const codet &code, goto_programt &dest); - void convert_non_deterministic_goto(const codet &code, goto_programt &dest); void convert_label( const code_labelt &code, goto_programt &dest, @@ -355,7 +354,7 @@ class goto_convertt:public messaget void finish_gotos(goto_programt &dest, const irep_idt &mode); void finish_computed_gotos(goto_programt &dest); - void finish_guarded_gotos(goto_programt &dest); + void optimize_guarded_gotos(goto_programt &dest); typedef std::map> @@ -545,15 +544,6 @@ class goto_convertt:public messaget std::size_t leave_stack_size; }; - struct guarded_gotot - { - goto_programt::targett ifiter; - goto_programt::targett gotoiter; - exprt guard; - }; - typedef std::list guarded_gotost; - guarded_gotost guarded_gotos; - exprt case_guard( const exprt &value, const caset &case_op); diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index c4c7361cfa8..3232f467672 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -28,25 +28,26 @@ Author: Daniel Kroening, kroening@kroening.com /// The type of an instruction in a GOTO program. enum goto_program_instruction_typet { - NO_INSTRUCTION_TYPE=0, - GOTO=1, // branch, possibly guarded - ASSUME=2, // non-failing guarded self loop - ASSERT=3, // assertions - OTHER=4, // anything else - SKIP=5, // just advance the PC - START_THREAD=6, // spawns an asynchronous thread - END_THREAD=7, // end the current thread - LOCATION=8, // semantically like SKIP - END_FUNCTION=9, // exit point of a function - ATOMIC_BEGIN=10, // marks a block without interleavings - ATOMIC_END=11, // end of a block without interleavings - RETURN=12, // set function return value (no control-flow change) - ASSIGN=13, // assignment lhs:=rhs - DECL=14, // declare a local variable - DEAD=15, // marks the end-of-live of a local variable - FUNCTION_CALL=16, // call a function - THROW=17, // throw an exception - CATCH=18 // push, pop or enter an exception handler + NO_INSTRUCTION_TYPE = 0, + GOTO = 1, // branch, possibly guarded + ASSUME = 2, // non-failing guarded self loop + ASSERT = 3, // assertions + OTHER = 4, // anything else + SKIP = 5, // just advance the PC + START_THREAD = 6, // spawns an asynchronous thread + END_THREAD = 7, // end the current thread + LOCATION = 8, // semantically like SKIP + END_FUNCTION = 9, // exit point of a function + ATOMIC_BEGIN = 10, // marks a block without interleavings + ATOMIC_END = 11, // end of a block without interleavings + RETURN = 12, // set function return value (no control-flow change) + ASSIGN = 13, // assignment lhs:=rhs + DECL = 14, // declare a local variable + DEAD = 15, // marks the end-of-live of a local variable + FUNCTION_CALL = 16, // call a function + THROW = 17, // throw an exception + CATCH = 18, // push, pop or enter an exception handler + INCOMPLETE_GOTO = 19 // goto where target is yet to be determined }; std::ostream &operator<<(std::ostream &, goto_program_instruction_typet); @@ -253,6 +254,12 @@ class goto_programt void make_atomic_end() { clear(ATOMIC_END); } void make_end_function() { clear(END_FUNCTION); } + void make_incomplete_goto(const code_gotot &_code) + { + clear(INCOMPLETE_GOTO); + code = _code; + } + void make_goto(targett _target) { clear(GOTO); @@ -265,6 +272,13 @@ class goto_programt guard=g; } + void complete_goto(targett _target) + { + PRECONDITION(type == INCOMPLETE_GOTO); + targets.push_back(_target); + type = GOTO; + } + void make_assignment(const codet &_code) { clear(ASSIGN); @@ -301,6 +315,10 @@ class goto_programt bool is_start_thread () const { return type==START_THREAD; } bool is_end_thread () const { return type==END_THREAD; } bool is_end_function () const { return type==END_FUNCTION; } + bool is_incomplete_goto() const + { + return type == INCOMPLETE_GOTO; + } instructiont(): instructiont(NO_INSTRUCTION_TYPE) // NOLINT(runtime/explicit) diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 5a9043cff2b..f806d403177 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -490,6 +490,8 @@ goto_programt::targett string_abstractiont::abstract( case OTHER: case LOCATION: break; + + case INCOMPLETE_GOTO: case NO_INSTRUCTION_TYPE: UNREACHABLE; break;