Add hopping through declarations on jump into scope

When a goto which jumps into a scope is converted, the declarations
for that scope need to be passed through. It needs to be the same
declaration in both execution paths, so that symex will correctly merge
the two different states when generating the phi functions.

The requirement for executing the same declaration whether entering the
scope through a regular route vs a goto into the middle of the block is
acheived by setting up a chain of hops where -
 * Original goto hops to first declaration.
 * After first declaration we hop to the next declaration if entering
   via a goto.
 * Afer the final declaration we hop to the originally specified label.

The identifiers in the existing `symex_should_filter_value_sets` test
need to be incremented, because the instance being checked is now the
second time the variable is added to the scope.

Author: thomasspriggs

Diff for: regression/cbmc/destructors/compound_literal.desc

@@ -2,21 +2,21 @@ CORE
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*8: END_FUNCTION
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*DEAD .*newAlloc0[\s]*(?P>comment_block)[\s]*DEAD .*pc[\s]*(?P>comment_block)[\s]*DEAD .*literal[\s]*(?P>comment_block)[\s]*9: END_FUNCTION
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-       // 49 file main.c line 44 function main
-       DEAD main::1::newAlloc0
-       // 50 file main.c line 44 function main
-       DEAD main::1::pc
-       // 51 file main.c line 44 function main
-       DEAD main::$tmp::literal
-       // 52 file main.c line 45 function main
-    8: END_FUNCTION
+        // 57 file main.c line 44 function main
+        DEAD main::1::newAlloc0
+        // 58 file main.c line 44 function main
+        DEAD main::1::pc
+        // 59 file main.c line 44 function main
+        DEAD main::$tmp::literal
+        // 60 file main.c line 45 function main
+     9: END_FUNCTION
 
 This asserts that when you've created a compound literal that both temp and real
 variable gets killed.

Diff for: regression/cbmc/destructors/enter_lexical_block.desc

@@ -2,32 +2,34 @@ CORE
 main.c
 --unwind 10 --show-goto-functions
 activate-multi-line-match
-(?P<comment_block>\/\/ [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
+(?P<comment_block>\/\/ [0-9]+ file main\.c line [0-9]+ function main)[\s]*6: .*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]*.*ASSIGN going_to::nested_if := true[\s]*(?P>comment_block)[\s]*.*GOTO 3
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
 Checks for:
 
-       // 37 file main.c line 36 function main
-    5: DECL main::1::2::2::newAlloc4 : struct tag-test
-       // 38 file main.c line 36 function main
+       // 41 file main.c line 36 function main
+    6: DECL main::1::2::2::newAlloc4 : struct tag-test
+       // 42 file main.c line 36 function main
        ASSIGN main::1::2::2::newAlloc4 := { 4 }
-       // 39 file main.c line 37 function main
+       // 43 file main.c line 37 function main
        DECL main::1::2::2::newAlloc6 : struct tag-test
-       // 40 file main.c line 37 function main
+       // 44 file main.c line 37 function main
        ASSIGN main::1::2::2::newAlloc6 := { 6 }
-       // 41 file main.c line 38 function main
+       // 45 file main.c line 38 function main
        DECL main::1::2::2::newAlloc7 : struct tag-test
-       // 42 file main.c line 38 function main
+       // 46 file main.c line 38 function main
        ASSIGN main::1::2::2::newAlloc7 := { 7 }
-       // 43 file main.c line 39 function main
+       // 47 file main.c line 39 function main
        DEAD main::1::2::2::newAlloc7
-       // 44 file main.c line 39 function main
+       // 48 file main.c line 39 function main
        DEAD main::1::2::2::newAlloc6
-       // 45 file main.c line 39 function main
+       // 49 file main.c line 39 function main
        DEAD main::1::2::2::newAlloc4
-       // 46 file main.c line 39 function main
+       // 50 file main.c line 39 function main
+       ASSIGN going_to::nested_if := true
+       // 51 file main.c line 39 function main
        GOTO 3
 
 This asserts that when the GOTO is going into a lexical block that destructors

Diff for: regression/cbmc/symex_should_filter_value_sets/test.desc

@@ -9,8 +9,8 @@ main::1::c3!0@1#. = 1
 main::1::c4!0@1#. = 1
 main::1::c5!0@1#. = 1
 main::1::c6!0@1#. = 1
-main::1::c7!0@1#. = 1
-main::1::c8!0@1#. = 1
+main::1::c7!0@2#. = 1
+main::1::c8!0@2#. = 1
 main::1::c9!0@1#. = 1
 main::1::c10!0@1#. = 1
 main::1::c11!0@1#. = 1

Diff for: src/goto-programs/goto_convert.cpp

@@ -93,6 +93,141 @@ static void finish_catch_push_targets(goto_programt &dest)
   }
 }
 
+struct build_declaration_hops_inputst
+{
+  irep_idt mode;
+  irep_idt label;
+  goto_programt::targett goto_instruction;
+  goto_programt::targett label_instruction;
+  node_indext label_scope_index = 0;
+  node_indext end_scope_index = 0;
+};
+
+void goto_convertt::build_declaration_hops(
+  goto_programt &program,
+  std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
+  const build_declaration_hops_inputst &inputs)
+{
+  // In the case of a goto jumping into a scope, the declarations (but not the
+  // initialisations) need to be executed. This function performs a
+  // transformation from code that looks like -
+  //   {
+  //     statement_block_a();
+  //     if(...)
+  //       goto user_label;
+  //     statement_block_b();
+  //     int x;
+  //     x = 0;
+  //     statement_block_c();
+  //     int y;
+  //     y = 0;
+  //     statement_block_d();
+  //   user_label:
+  //     statement_block_e();
+  //   }
+  // to code which looks like -
+  //   {
+  //     __CPROVER_bool going_to::user_label;
+  //     going_to::user_label = false;
+  //     statement_block_a();
+  //     if(...)
+  //     {
+  //       going_to::user_label = true;
+  //       goto scope_x_label;
+  //     }
+  //     statement_block_b();
+  //   scope_x_label:
+  //     int x;
+  //     if going_to::user_label goto scope_y_label:
+  //     x = 0;
+  //     statement_block_c();
+  //   scope_y_label:
+  //     int y;
+  //     if going_to::user_label goto user_label:
+  //     y = 0;
+  //     statement_block_d();
+  //   user_label:
+  //     going_to::user_label = false;
+  //     statement_block_e();
+  //   }
+
+  PRECONDITION(inputs.label_scope_index != inputs.end_scope_index);
+
+  const auto flag = [&]() -> symbolt {
+    const auto existing_flag = label_flags.find(inputs.label);
+    if(existing_flag != label_flags.end())
+      return existing_flag->second;
+    source_locationt label_location =
+      inputs.label_instruction->source_location();
+    label_location.set_hide();
+    const symbolt &new_flag = get_fresh_aux_symbol(
+      bool_typet{},
+      "going_to",
+      id2string(inputs.label),
+      label_location,
+      inputs.mode,
+      symbol_table);
+    label_flags.emplace(inputs.label, new_flag);
+
+    // Create and initialise flag.
+    goto_programt flag_creation;
+    flag_creation.instructions.push_back(
+      goto_programt::make_decl(new_flag.symbol_expr(), label_location));
+    const auto make_clear_flag = [&]() -> goto_programt::instructiont {
+      return goto_programt::make_assignment(
+        new_flag.symbol_expr(), false_exprt{}, label_location);
+    };
+    flag_creation.instructions.push_back(make_clear_flag());
+    program.destructive_insert(program.instructions.begin(), flag_creation);
+
+    // Clear flag on arrival at label.
+    auto clear_on_arrival = make_clear_flag();
+    program.insert_before_swap(inputs.label_instruction, clear_on_arrival);
+    return new_flag;
+  }();
+
+  auto goto_instruction = inputs.goto_instruction;
+  {
+    // Set flag before the goto.
+    auto goto_location = goto_instruction->source_location();
+    goto_location.set_hide();
+    auto set_flag = goto_programt::make_assignment(
+      flag.symbol_expr(), true_exprt{}, goto_location);
+    program.insert_before_swap(goto_instruction, set_flag);
+    // Keep this iterator referring to the goto instruction, not the assignment.
+    ++goto_instruction;
+  }
+
+  auto target = inputs.label_instruction;
+  targets.scope_stack.set_current_node(inputs.label_scope_index);
+  while(targets.scope_stack.get_current_node() > inputs.end_scope_index)
+  {
+    node_indext current_node = targets.scope_stack.get_current_node();
+    auto &declaration = targets.scope_stack.get_declaration(current_node);
+    targets.scope_stack.descend_tree();
+    if(!declaration)
+      continue;
+
+    bool add_if = declaration->if_conditions_added.find(flag.name) ==
+                  declaration->if_conditions_added.end();
+    if(add_if)
+    {
+      auto declaration_location = declaration->instruction->source_location();
+      declaration_location.set_hide();
+      auto if_goto = goto_programt::make_goto(
+        target, flag.symbol_expr(), declaration_location);
+      program.instructions.insert(
+        std::next(declaration->instruction), std::move(if_goto));
+      declaration->if_conditions_added.insert(flag.name);
+    }
+    target = declaration->instruction;
+  }
+
+  // Update the goto so that it goes to the first declaration rather than its
+  // original/final destination.
+  goto_instruction->set_target(target);
+}
+
 /*******************************************************************	\
 
 Function: goto_convertt::finish_gotos
@@ -107,6 +242,8 @@ Function: goto_convertt::finish_gotos
 
 void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
 {
+  std::unordered_map<irep_idt, symbolt, irep_id_hash> label_flags;
+
   for(const auto &g_it : targets.gotos)
   {
     goto_programt::instructiont &i=*(g_it.first);
@@ -174,17 +311,29 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
         // 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.
+      // Variables *entering* scope on goto, is illegal for C++ non-pod types
+      // and impossible in Java. This is however valid C and should be taken
+      // into account.
       const bool variables_added_to_scope =
         intersection_result.right_depth_below_common_ancestor > 0;
       if(variables_added_to_scope)
       {
+        // If the goto recorded a destructor stack, execute as much as is
+        // appropriate for however many automatic variables leave scope.
         debug().source_location = i.source_location();
         debug() << "encountered goto '" << goto_label
                 << "' that enters one or more lexical blocks; "
-                << "omitting constructors." << eom;
+                << "adding declaration code on jump to '" << goto_label << "'"
+                << eom;
+
+        build_declaration_hops_inputst inputs;
+        inputs.mode = mode;
+        inputs.label = l_it->first;
+        inputs.goto_instruction = g_it.first;
+        inputs.label_instruction = l_it->second.first;
+        inputs.label_scope_index = label_target;
+        inputs.end_scope_index = intersection_result.common_ancestor;
+        build_declaration_hops(dest, label_flags, inputs);
       }
     }
     else

Diff for: src/goto-programs/goto_convert_class.h

@@ -26,6 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include <vector>
 
 class side_effect_expr_overflowt;
+struct build_declaration_hops_inputst;
 
 class goto_convertt:public messaget
 {
@@ -362,6 +363,11 @@ class goto_convertt:public messaget
     optionalt<node_indext> destructor_start_point = {},
     optionalt<node_indext> destructor_end_point = {});
 
+  void build_declaration_hops(
+    goto_programt &dest,
+    std::unordered_map<irep_idt, symbolt, irep_id_hash> &label_flags,
+    const build_declaration_hops_inputst &inputs);
+
   //
   // gotos
   //