From 2b8a8fcb76f7b338cf3caa2a8085be483dabadf2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 1 Dec 2023 13:23:11 +0000 Subject: [PATCH] Variables leaving scope on jumping should always be marked dead Even if new variables would be introduced to the scope, the existing variables which go out of scope still need to be marked as dead and/or have their destructors called. The placeholder for construction is moved to after the destruction, as destructions should be done first. --- .../cbmc/destructors/enter_lexical_block.desc | 12 +++- src/goto-programs/goto_convert.cpp | 60 +++++++++---------- 2 files changed, 38 insertions(+), 34 deletions(-) diff --git a/regression/cbmc/destructors/enter_lexical_block.desc b/regression/cbmc/destructors/enter_lexical_block.desc index 296188dd84f..dd4f1e34852 100644 --- a/regression/cbmc/destructors/enter_lexical_block.desc +++ b/regression/cbmc/destructors/enter_lexical_block.desc @@ -2,7 +2,7 @@ CORE main.c --unwind 10 --show-goto-functions activate-multi-line-match -(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*GOTO 3 +(?P\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*5: .*newAlloc4 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc4 := \{ 4 \}[\s]*(?P>comment_block)[\s]*.*newAlloc6 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc6 := \{ 6 \}[\s]*(?P>comment_block)[\s]*.*newAlloc7 : struct tag-test[\s]*(?P>comment_block)[\s]*.*newAlloc7 := \{ 7 \}[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc7[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc6[\s]*(?P>comment_block)[\s]*.*DEAD main::1::2::2::newAlloc4[\s]*(?P>comment_block)[\s]*.*GOTO 3 ^EXIT=0$ ^SIGNAL=0$ -- @@ -22,8 +22,14 @@ Checks for: // 42 file main.c line 38 function main ASSIGN main::1::2::2::newAlloc7 := { 7 } // 43 file main.c line 39 function main + DEAD main::1::2::2::newAlloc7 + // 44 file main.c line 39 function main + DEAD main::1::2::2::newAlloc6 + // 45 file main.c line 39 function main + DEAD main::1::2::2::newAlloc4 + // 46 file main.c line 39 function main GOTO 3 This asserts that when the GOTO is going into a lexical block that destructors -are omitted. This used to be a limitation with the previous implementation and should -now be fixable, but for consistency it acts in the same way. +are not omitted. This used to be a limitation with the previous implementation +and has now been fixed. diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 172f1b3f0dc..f1cdce715ed 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -151,42 +151,40 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode) targets.destructor_stack.get_nearest_common_ancestor_info( goto_target, label_target); - bool not_prefix = - intersection_result.right_depth_below_common_ancestor != 0; - // If our goto had no variables of note, just skip if(goto_target != 0) { // 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. - if(not_prefix) - { - debug().source_location = i.source_location(); - debug() << "encountered goto '" << goto_label - << "' that enters one or more lexical blocks; " - << "omitting constructors and destructors" << eom; - } - else - { - debug().source_location = i.source_location(); - debug() << "adding goto-destructor code on jump to '" << goto_label - << "'" << eom; - - node_indext end_destruct = intersection_result.common_ancestor; - goto_programt destructor_code; - unwind_destructor_stack( - i.source_location(), - destructor_code, - mode, - end_destruct, - goto_target); - dest.destructive_insert(g_it.first, destructor_code); - - // This should leave iterators intact, as long as - // goto_programt::instructionst is std::list. - } + debug().source_location = i.source_location(); + debug() << "adding goto-destructor code on jump to '" << goto_label + << "'" << eom; + + node_indext end_destruct = intersection_result.common_ancestor; + goto_programt destructor_code; + unwind_destructor_stack( + i.source_location(), + destructor_code, + mode, + end_destruct, + goto_target); + dest.destructive_insert(g_it.first, destructor_code); + + // This should leave iterators intact, as long as + // goto_programt::instructionst is std::list. + } + + // We don't currently handle variables *entering* scope, which + // is illegal for C++ non-pod types and impossible in Java in any case. + // This is however valid C. + const bool variables_added_to_scope = + intersection_result.right_depth_below_common_ancestor > 0; + if(variables_added_to_scope) + { + debug().source_location = i.source_location(); + debug() << "encountered goto '" << goto_label + << "' that enters one or more lexical blocks; " + << "omitting constructors." << eom; } } else