diff --git a/regression/cbmc-java/destructor1/Break.class b/regression/cbmc-java/destructor1/Break.class new file mode 100644 index 00000000000..5b848534cc0 Binary files /dev/null and b/regression/cbmc-java/destructor1/Break.class differ diff --git a/regression/cbmc-java/destructor1/Break.java b/regression/cbmc-java/destructor1/Break.java new file mode 100644 index 00000000000..52ab6048bd4 --- /dev/null +++ b/regression/cbmc-java/destructor1/Break.java @@ -0,0 +1,14 @@ + +public class Break { + + public static void main() { + + int j = 0; + ++j; + for(int i = 0; i < 10; ++i) + if(i == 5) break; + for(j = 0; j < 10; ++j) + if(j == 5) break; + } + +} diff --git a/regression/cbmc-java/destructor1/test.desc b/regression/cbmc-java/destructor1/test.desc new file mode 100644 index 00000000000..53856821b22 --- /dev/null +++ b/regression/cbmc-java/destructor1/test.desc @@ -0,0 +1,8 @@ +CORE +Break.class +--show-goto-functions +^EXIT=0$ +^SIGNAL=0$ +dead i; +-- +GOTO 10 diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index e161fe0a5bc..b4f4385a314 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -57,11 +57,11 @@ Function: goto_convertt::finish_gotos \*******************************************************************/ -void goto_convertt::finish_gotos() +void goto_convertt::finish_gotos(goto_programt &dest) { for(const auto &g_it : targets.gotos) { - goto_programt::instructiont &i=*g_it; + goto_programt::instructiont &i=*(g_it.first); if(i.code.get_statement()=="non-deterministic-goto") { @@ -81,7 +81,7 @@ void goto_convertt::finish_gotos() throw 0; } - i.targets.push_back(l_it->second); + i.targets.push_back(l_it->second.first); } } else if(i.is_start_thread()) @@ -98,7 +98,7 @@ void goto_convertt::finish_gotos() throw 0; } - i.targets.push_back(l_it->second); + i.targets.push_back(l_it->second.first); } else if(i.code.get_statement()==ID_goto) { @@ -114,7 +114,49 @@ void goto_convertt::finish_gotos() } i.targets.clear(); - i.targets.push_back(l_it->second); + i.targets.push_back(l_it->second.first); + + // If the goto recorded a destructor stack, execute as much as is + // appropriate for however many automatic variables leave scope. + // We don't currently handle variables *entering* scope, which is illegal + // for C++ non-pod types and impossible in Java in any case. + auto goto_stack=g_it.second; + const auto& label_stack=l_it->second.second; + bool stack_is_prefix=true; + if(label_stack.size()>goto_stack.size()) + stack_is_prefix=false; + for(unsigned i=0, ilim=label_stack.size(); + i!=ilim && stack_is_prefix; + ++i) + { + if(goto_stack[i]!=label_stack[i]) + stack_is_prefix=false; + } + + if(!stack_is_prefix) + { + warning() << "Encountered goto (" << goto_label << + ") that enters one or more lexical blocks;" << + "omitting constructors and destructors." << eom; + } + else + { + auto unwind_to_size=label_stack.size(); + if(unwind_to_sizemake_goto(label.second); + t->make_goto(label.second.first); t->source_location=i.source_location; t->guard=guard; } @@ -180,6 +222,50 @@ void goto_convertt::finish_computed_gotos(goto_programt &goto_program) /*******************************************************************\ +Function: goto_convertt::finish_guarded_gotos + + Inputs: Destination goto program + + Outputs: + + Purpose: 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; + +\*******************************************************************/ + +void goto_convertt::finish_guarded_gotos(goto_programt &dest) +{ + for(auto& gg : guarded_gotos) + { + // 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 so, can't simplify. + if(destructor_present) + continue; + + // Simplify: remove whatever code was generated for the condition + // and attach the original guard to the goto instruction. + gg.gotoiter->guard=gg.guard; + // goto_programt doesn't provide an erase operation, + // perhaps for a good reason, so let's be cautious and just + // flatten the un-needed instructions into skips. + for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it) + it->make_skip(); + } +} + +/*******************************************************************\ + Function: goto_convertt::goto_convert Inputs: @@ -213,8 +299,9 @@ void goto_convertt::goto_convert_rec( { convert(code, dest); - finish_gotos(); + finish_gotos(dest); finish_computed_gotos(dest); + finish_guarded_gotos(dest); } /*******************************************************************\ @@ -282,8 +369,7 @@ void goto_convertt::convert_label( goto_programt::targett target=tmp.instructions.begin(); dest.destructive_append(tmp); - targets.labels.insert(std::pair - (label, target)); + targets.labels.insert({label, {target, targets.destructor_stack}}); target->labels.push_front(label); } @@ -1628,7 +1714,7 @@ void goto_convertt::convert_goto( t->code=code; // remember it to do target later - targets.gotos.push_back(t); + targets.gotos.push_back(std::make_pair(t,targets.destructor_stack)); } /*******************************************************************\ @@ -2130,6 +2216,24 @@ void goto_convertt::collect_operands( /*******************************************************************\ +Function: is_size_one + + Inputs: Goto program 'g' + + Outputs: True if 'g' has one instruction + + Purpose: This is (believed to be) faster than using std::list.size + +\*******************************************************************/ + +static inline bool is_size_one(const goto_programt &g) +{ + return (!g.instructions.empty()) && + ++g.instructions.begin()==g.instructions.end(); +} + +/*******************************************************************\ + Function: goto_convertt::generate_ifthenelse Inputs: @@ -2161,24 +2265,24 @@ void goto_convertt::generate_ifthenelse( return; } + bool is_guarded_goto=false; + // do guarded gotos directly if(is_empty(false_case) && - // true_case.instructions.size()==1 optimised - !true_case.instructions.empty() && - ++true_case.instructions.begin()==true_case.instructions.end() && + 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; } - true_case.instructions.back().guard=guard; - dest.destructive_append(true_case); - return; + // 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 - if(true_case.instructions.size()==1 && + if(is_size_one(true_case) && true_case.instructions.back().is_assert() && true_case.instructions.back().guard.is_false() && true_case.instructions.back().labels.empty()) @@ -2191,7 +2295,7 @@ void goto_convertt::generate_ifthenelse( } // similarly, do guarded assertions directly - if(false_case.instructions.size()==1 && + if(is_size_one(false_case) && false_case.instructions.back().is_assert() && false_case.instructions.back().guard.is_false() && false_case.instructions.back().labels.empty()) @@ -2258,6 +2362,15 @@ 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 daea6f6571f..a0e3ac1fe16 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -216,22 +216,29 @@ class goto_convertt:public messaget // exceptions // + typedef std::vector destructor_stackt; + symbol_exprt exception_flag(); void unwind_destructor_stack( const source_locationt &, std::size_t stack_size, goto_programt &dest); + void unwind_destructor_stack( + const source_locationt &, + std::size_t stack_size, + goto_programt &dest, + destructor_stackt &stack); // // gotos // - void finish_gotos(); + void finish_gotos(goto_programt &dest); void finish_computed_gotos(goto_programt &dest); + void finish_guarded_gotos(goto_programt &dest); - typedef std::vector destructor_stackt; - typedef std::map labelst; - typedef std::list gotost; + typedef std::map > labelst; + typedef std::list > gotost; typedef std::list computed_gotost; typedef exprt::operandst caset; typedef std::list > casest; @@ -412,6 +419,14 @@ 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_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp index 75dcffe1552..54d72f9c224 100644 --- a/src/goto-programs/goto_convert_exceptions.cpp +++ b/src/goto-programs/goto_convert_exceptions.cpp @@ -374,23 +374,36 @@ void goto_convertt::unwind_destructor_stack( const source_locationt &source_location, std::size_t final_stack_size, goto_programt &dest) +{ + unwind_destructor_stack( + source_location, + final_stack_size, + dest, + targets.destructor_stack); +} + +void goto_convertt::unwind_destructor_stack( + const source_locationt &source_location, + std::size_t final_stack_size, + goto_programt &dest, + destructor_stackt &destructor_stack) { // There might be exceptions happening in the exception // handler. We thus pop off the stack, and then later // one restore the original stack. - destructor_stackt old_stack=targets.destructor_stack; + destructor_stackt old_stack=destructor_stack; - while(targets.destructor_stack.size()>final_stack_size) + while(destructor_stack.size()>final_stack_size) { - codet d_code=targets.destructor_stack.back(); + codet d_code=destructor_stack.back(); d_code.add_source_location()=source_location; // pop now to avoid doing this again - targets.destructor_stack.pop_back(); + destructor_stack.pop_back(); convert(d_code, dest); } // Now restore old stack. - old_stack.swap(targets.destructor_stack); + old_stack.swap(destructor_stack); }