From 8e98eaacd724aa3abb3c8486b1f56d1c41adcc6f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 31 Aug 2016 15:59:43 +0100 Subject: [PATCH 1/3] Execute destructors on goto exiting block statement The case where it enters a scope is not handled at present, as I don't know how to phrase that in terms of goto-program decl statements. It's also illegal in C++ if a nontrivial constructor would be needed, and can't be constructed in Java source AFAIK. --- src/goto-programs/goto_convert.cpp | 68 ++++++++++++++++--- src/goto-programs/goto_convert_class.h | 14 ++-- src/goto-programs/goto_convert_exceptions.cpp | 23 +++++-- 3 files changed, 86 insertions(+), 19 deletions(-) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index e161fe0a5bc..1ee618acd68 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,48 @@ 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. + 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; } @@ -213,7 +254,7 @@ void goto_convertt::goto_convert_rec( { convert(code, dest); - finish_gotos(); + finish_gotos(dest); finish_computed_gotos(dest); } @@ -282,8 +323,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); } @@ -1622,13 +1662,21 @@ void goto_convertt::convert_goto( const codet &code, goto_programt &dest) { + // Precede with a 'skip', which will be replaced by any pre-departure + // destructor code if appropriate. Without this the goto can be amalgamated + // into a control-flow structure, such as IF x THEN GOTO 1;, leaving + // nowhere for the destructors to go. + goto_programt::targett skip=dest.add_instruction(SKIP); + skip->source_location=code.source_location(); + skip->code=code_skipt(); + goto_programt::targett t=dest.add_instruction(); t->make_goto(); t->source_location=code.source_location(); 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)); } /*******************************************************************\ diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index daea6f6571f..bdb48028ce3 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -216,22 +216,28 @@ 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); - 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; 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); } From ea16fd4228f482d596a96a8de9197871d2a84a6d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 1 Sep 2016 16:24:29 +0100 Subject: [PATCH 2/3] Restore the guarded-goto construct Instead of building it in the first pass, make a pessimistic multi-instruction branch and then promote it in the post-pass if no destructors got added. --- src/goto-programs/goto_convert.cpp | 99 +++++++++++++++++++++----- src/goto-programs/goto_convert_class.h | 9 +++ 2 files changed, 91 insertions(+), 17 deletions(-) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 1ee618acd68..b4f4385a314 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -118,7 +118,8 @@ void goto_convertt::finish_gotos(goto_programt &dest) // 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. + // 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; @@ -221,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: @@ -256,6 +301,7 @@ void goto_convertt::goto_convert_rec( finish_gotos(dest); finish_computed_gotos(dest); + finish_guarded_gotos(dest); } /*******************************************************************\ @@ -1662,14 +1708,6 @@ void goto_convertt::convert_goto( const codet &code, goto_programt &dest) { - // Precede with a 'skip', which will be replaced by any pre-departure - // destructor code if appropriate. Without this the goto can be amalgamated - // into a control-flow structure, such as IF x THEN GOTO 1;, leaving - // nowhere for the destructors to go. - goto_programt::targett skip=dest.add_instruction(SKIP); - skip->source_location=code.source_location(); - skip->code=code_skipt(); - goto_programt::targett t=dest.add_instruction(); t->make_goto(); t->source_location=code.source_location(); @@ -2178,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: @@ -2209,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()) @@ -2239,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()) @@ -2306,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 bdb48028ce3..a0e3ac1fe16 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -235,6 +235,7 @@ class goto_convertt:public messaget void finish_gotos(goto_programt &dest); void finish_computed_gotos(goto_programt &dest); + void finish_guarded_gotos(goto_programt &dest); typedef std::map > labelst; typedef std::list > gotost; @@ -418,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); From cfbe2ac5bfd01f54c9661bfda7cb7e0bb7bcf0f0 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 18 Jan 2017 10:03:54 +0000 Subject: [PATCH 3/3] Add goto-destructor test This checks that (a) the loop iterator 'i' gets killed before function exit and (b) there aren't too may basic blocks (indicated by 'GOTO 10' appearing, which would indicate the second loop's guarded goto statements are being unnecessarily disrupted. (For example, producing 'if(j==5) goto 2; goto end; 2: ...' instead of the simpler 'if(j==5) goto end; ...', which is necessary for the i-loop to accomodate the 'dead i;' statement, but not for the j-loop) --- regression/cbmc-java/destructor1/Break.class | Bin 0 -> 443 bytes regression/cbmc-java/destructor1/Break.java | 14 ++++++++++++++ regression/cbmc-java/destructor1/test.desc | 8 ++++++++ 3 files changed, 22 insertions(+) create mode 100644 regression/cbmc-java/destructor1/Break.class create mode 100644 regression/cbmc-java/destructor1/Break.java create mode 100644 regression/cbmc-java/destructor1/test.desc diff --git a/regression/cbmc-java/destructor1/Break.class b/regression/cbmc-java/destructor1/Break.class new file mode 100644 index 0000000000000000000000000000000000000000..5b848534cc0ba2eda064fd67810ffe3234f71e18 GIT binary patch literal 443 zcmX|-%SyvQ6o&tkG)Wtq-fUg8D-pyCSQU3IE))cz>Y~#9GzLvCsl?PL=u@~7H(k3D zT=)RKjC;Y$Kk+hf=FI#z5e86Xg$2 z)b($T+nr2fKR60?S2r!(8mL>9M+TO_N{OJPS#zYK%jQ{s5cmm}VQ_H04A2P{cblro zEX>x%6XY@d>~ObJXdugT{^tU6aH(=w_%FU=GlOi`Y|S8MyHRo