Add build_declaration_hops

Author: thomasspriggs

src/goto-programs/goto_convert.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 /// Program Transformation
 
 #include "goto_convert.h"
+#include "goto_convert_class.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -24,10 +25,14 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 #include <util/symbol_table_builder.h>
 
-#include "goto_convert_class.h"
 #include "destructor.h"
 #include "remove_skip.h"
 
+#include <iostream>
+#define WATCHVAR(var)                                                          \
+  std::cerr << "DBG: " << __FILE__ << "(" << __LINE__ << ") " << #var          \
+            << " = [" << (var) << "]" << std::endl
+
 static bool is_empty(const goto_programt &goto_program)
 {
   forall_goto_program_instructions(it, goto_program)
@@ -134,6 +139,136 @@ goto_programt goto_convertt::build_declaration_stack(
   return declarations;
 }
 
+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 label;
+  //     statement_block_b();
+  //   user_label:
+  //   x_label:
+  //     int x;
+  //     x = 0;
+  //     statement_block_c();
+  //     int y;
+  //     y = 0;
+  //     statement_block_d();
+  //   label:
+  //     statement_block_e();
+  //   }
+  // to code which looks like -
+  //   {
+  //     __CPROVER_bool going_to_label;
+  //     going_to_label = false;
+  //     statement_block_a();
+  //     if(...)
+  //       going_to_label = true;
+  //       goto scope_x_label;
+  //     statement_block_b();
+  //   scope_x_label:
+  //     int x;
+  //     if going_to_label goto scope_y_label:
+  //     x = 0;
+  //     statement_block_c();
+  //   scope_y_label:
+  //     int y;
+  //     if going_to_label goto label:
+  //     y = 0;
+  //     statement_block_d();
+  //   label:
+  //     going_to_label = false;
+  //     statement_block_e();
+  //   }
+
+  PRECONDITION(inputs.label_scope_index != inputs.end_scope_index);
+
+  source_locationt hidden{};
+  hidden.set_hide();
+  const auto flag = [&]() -> symbolt {
+    const auto existing_flag = label_flags.find(inputs.label);
+    if(existing_flag != label_flags.end())
+      return existing_flag->second;
+    const symbolt &new_flag = get_fresh_aux_symbol(
+      bool_typet{},
+      id2string(inputs.label),
+      "going_to",
+      hidden,
+      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(), hidden));
+    const auto make_clear_flag = [&]() -> goto_programt::instructiont {
+      return goto_programt::make_assignment(
+        new_flag.symbol_expr(), false_exprt{}, hidden);
+    };
+    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;
+  }();
+
+  {
+    // Set flag before the goto.
+    auto set_flag =
+      goto_programt::make_assignment(flag.symbol_expr(), true_exprt{}, hidden);
+    program.insert_before_swap(inputs.goto_instruction, set_flag);
+  }
+
+  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;
+
+    // TODO - TYPE CHECK FOR VAR ARRAYS!
+
+    WATCHVAR(declaration->instruction->to_string());
+    bool add_if = declaration->if_conditions_added.find(flag.name) ==
+                  declaration->if_conditions_added.end();
+    if(add_if)
+    {
+      auto if_goto =
+        goto_programt::make_goto(target, flag.symbol_expr(), hidden);
+      program.instructions.insert(
+        std::next(declaration->instruction), std::move(if_goto));
+      declaration->if_conditions_added.insert(flag.name);
+    }
+    target = declaration->instruction;
+  }
+
+  // We need to look at the list node after goto_instruction because this
+  // iterator now refers to the flag assignment.
+  std::next(inputs.goto_instruction)->set_target(target);
+}
+
 /*******************************************************************	\
 
 Function: goto_convertt::finish_gotos
@@ -148,6 +283,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);
@@ -179,6 +316,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
       }
 
       i.complete_goto(l_it->second.first);
+      WATCHVAR(i.get_target()->to_string());
 
       node_indext label_target = l_it->second.second;
       node_indext goto_target = g_it.second;
@@ -222,9 +360,15 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
         debug() << "adding declaration code on jump to '" << goto_label << "'"
                 << eom;
 
-        auto declaration_code = build_declaration_stack(
-          mode, label_target, intersection_result.common_ancestor);
-        dest.destructive_insert(g_it.first, declaration_code);
+        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);
+        //WATCHVAR(i.get_target()->to_string());
       }
     }
     else
@@ -660,7 +804,7 @@ void goto_convertt::convert_frontend_decl(
     if(code.operands().size() == 1)
     {
       copy(code, DECL, dest);
-      return dest.instructions.end()--;
+      return std::prev(dest.instructions.end());
     }
 
     exprt initializer = code.op1();
@@ -673,7 +817,7 @@ void goto_convertt::convert_frontend_decl(
     // Break up into decl and assignment.
     // Decl must be visible before initializer.
     copy(tmp, DECL, dest);
-    const auto declaration_iterator = dest.instructions.end()--;
+    const auto declaration_iterator = std::prev(dest.instructions.end());
 
     auto initializer_location = initializer.find_source_location();
     clean_expr(initializer, dest, mode);
@@ -696,7 +840,6 @@ void goto_convertt::convert_frontend_decl(
 
   {
     code_deadt code_dead(symbol_expr);
-
     targets.scope_stack.add(code_dead, {declaration_iterator});
   }
 

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
 {
@@ -367,6 +368,11 @@ class goto_convertt:public messaget
     node_indext declaration_start_point,
     node_indext declaration_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
   //