Rename "destructor tree" classes to "scope tree"

This data structure is going to be used for declarations as well as
destructors. So it needs to be renamed to match the expanded use case.

Author: thomasspriggs

src/goto-programs/destructor_tree.cpp

@@ -1,30 +1,30 @@
 /*******************************************************************\
 
- Module: Destructor Tree
+ Module: Scope Tree
 
  Author: John Dumbell, [email protected]
 
 \*******************************************************************/
 
 #include "destructor_tree.h"
 
-void destructor_treet::add(
+void scope_treet::add(
   const codet &destructor,
   std::optional<goto_programt::targett> declaration)
 {
   auto previous_node = get_current_node();
-  auto new_node = destruction_graph.add_node(destructor);
-  destruction_graph.add_edge(previous_node, new_node);
+  auto new_node = scope_graph.add_node(destructor);
+  scope_graph.add_edge(previous_node, new_node);
   current_node = new_node;
 }
 
-optionalt<codet> &destructor_treet::get_destructor(node_indext index)
+optionalt<codet> &scope_treet::get_destructor(node_indext index)
 {
-  PRECONDITION(index < destruction_graph.size());
-  return destruction_graph[index].destructor_value;
+  PRECONDITION(index < scope_graph.size());
+  return scope_graph[index].destructor_value;
 }
 
-const ancestry_resultt destructor_treet::get_nearest_common_ancestor_info(
+const ancestry_resultt scope_treet::get_nearest_common_ancestor_info(
   node_indext left_index,
   node_indext right_index)
 {
@@ -33,7 +33,7 @@ const ancestry_resultt destructor_treet::get_nearest_common_ancestor_info(
   {
     if(right_index > left_index)
     {
-      auto edge_map = destruction_graph[right_index].in;
+      auto edge_map = scope_graph[right_index].in;
       INVARIANT(
         !edge_map.empty(),
         "Node at index " + std::to_string(right_index) +
@@ -42,7 +42,7 @@ const ancestry_resultt destructor_treet::get_nearest_common_ancestor_info(
     }
     else
     {
-      auto edge_map = destruction_graph[left_index].in;
+      auto edge_map = scope_graph[left_index].in;
       INVARIANT(
         !edge_map.empty(),
         "Node at index " + std::to_string(left_index) +
@@ -55,7 +55,7 @@ const ancestry_resultt destructor_treet::get_nearest_common_ancestor_info(
   return {right_index, left_unique_count, right_unique_count};
 }
 
-const std::vector<destructor_and_idt> destructor_treet::get_destructors(
+const std::vector<destructor_and_idt> scope_treet::get_destructors(
   optionalt<node_indext> end_index,
   optionalt<node_indext> starting_index)
 {
@@ -65,7 +65,7 @@ const std::vector<destructor_and_idt> destructor_treet::get_destructors(
   std::vector<destructor_and_idt> codes;
   while(next_id > end_id)
   {
-    auto node = destruction_graph[next_id];
+    auto node = scope_graph[next_id];
     auto &destructor = node.destructor_value;
     if(destructor)
       codes.emplace_back(destructor_and_idt(*destructor, next_id));
@@ -76,27 +76,27 @@ const std::vector<destructor_and_idt> destructor_treet::get_destructors(
   return codes;
 }
 
-void destructor_treet::set_current_node(optionalt<node_indext> val)
+void scope_treet::set_current_node(optionalt<node_indext> val)
 {
   if(val)
     set_current_node(*val);
 }
 
-void destructor_treet::set_current_node(node_indext val)
+void scope_treet::set_current_node(node_indext val)
 {
   current_node = val;
 }
 
-void destructor_treet::descend_tree()
+void scope_treet::descend_tree()
 {
   node_indext current_node = get_current_node();
   if(current_node != 0)
   {
-    set_current_node(destruction_graph[current_node].in.begin()->first);
+    set_current_node(scope_graph[current_node].in.begin()->first);
   }
 }
 
-node_indext destructor_treet::get_current_node() const
+node_indext scope_treet::get_current_node() const
 {
   return current_node;
 }

src/goto-programs/destructor_tree.h

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
- Module: Destructor Tree
+ Module: Scope Tree
 
  Author: John Dumbell, [email protected]
 
@@ -87,13 +87,13 @@ class destructor_and_idt
 /// required to get there from 'c' was 2 and 'e' was 1, which also tells
 /// you if a certain branch is a prefix or not. In this case neither are a
 /// prefix of the other.
-class destructor_treet
+class scope_treet
 {
 public:
-  destructor_treet()
+  scope_treet()
   {
     // We add a default node to the graph to act as a root for path traversal.
-    this->destruction_graph.add_node();
+    this->scope_graph.add_node();
   }
 
   /// Adds a destructor/declaration pair to the current stack, attaching it to
@@ -142,19 +142,19 @@ class destructor_treet
   void descend_tree();
 
 private:
-  class destructor_nodet : public graph_nodet<empty_edget>
+  class scope_nodet : public graph_nodet<empty_edget>
   {
   public:
-    destructor_nodet() = default;
+    scope_nodet() = default;
 
-    explicit destructor_nodet(codet destructor)
+    explicit scope_nodet(codet destructor)
       : destructor_value(std::move(destructor))
     {
     }
     optionalt<codet> destructor_value;
   };
 
-  grapht<destructor_nodet> destruction_graph;
+  grapht<scope_nodet> scope_graph;
   node_indext current_node = 0;
 };
 

src/goto-programs/goto_clean_expr.cpp

@@ -53,7 +53,7 @@ symbol_exprt goto_convertt::make_compound_literal(
   if(!new_symbol.is_static_lifetime)
   {
     code_deadt code_dead(result);
-    targets.destructor_stack.add(std::move(code_dead), {});
+    targets.scope_stack.add(std::move(code_dead), {});
   }
 
   return result;

src/goto-programs/goto_convert.cpp

@@ -148,7 +148,7 @@ void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
       // Compare the currently-live variables on the path of the GOTO and label.
       // We want to work out what variables should die during the jump.
       ancestry_resultt intersection_result =
-        targets.destructor_stack.get_nearest_common_ancestor_info(
+        targets.scope_stack.get_nearest_common_ancestor_info(
           goto_target, label_target);
 
       // If our goto had no variables of note, just skip
@@ -339,7 +339,7 @@ void goto_convertt::convert_label(
     dest.destructive_append(tmp);
 
     targets.labels.insert(
-      {label, {target, targets.destructor_stack.get_current_node()}});
+      {label, {target, targets.scope_stack.get_current_node()}});
     target->labels.push_front(label);
   }
 }
@@ -545,8 +545,7 @@ void goto_convertt::convert_block(
   const source_locationt &end_location=code.end_location();
 
   // this saves the index of the destructor stack
-  node_indext old_stack_top =
-    targets.destructor_stack.get_current_node();
+  node_indext old_stack_top = targets.scope_stack.get_current_node();
 
   // now convert block
   for(const auto &b_code : code.statements())
@@ -564,7 +563,7 @@ void goto_convertt::convert_block(
     unwind_destructor_stack(end_location, dest, mode, old_stack_top);
 
   // Set the current node of our destructor stack back to before the block.
-  targets.destructor_stack.set_current_node(old_stack_top);
+  targets.scope_stack.set_current_node(old_stack_top);
 }
 
 void goto_convertt::convert_expression(
@@ -653,7 +652,7 @@ void goto_convertt::convert_frontend_decl(
 
   {
     code_deadt code_dead(symbol_expr);
-    targets.destructor_stack.add(code_dead, {});
+    targets.scope_stack.add(code_dead, {});
   }
 
   // do destructor
@@ -665,7 +664,7 @@ void goto_convertt::convert_frontend_decl(
     address_of_exprt this_expr(symbol_expr, pointer_type(symbol.type));
     destructor.arguments().push_back(this_expr);
 
-    targets.destructor_stack.add(destructor, {});
+    targets.scope_stack.add(destructor, {});
   }
 }
 
@@ -1367,7 +1366,7 @@ void goto_convertt::convert_goto(const code_gotot &code, goto_programt &dest)
     dest.add(goto_programt::make_incomplete_goto(code, code.source_location()));
 
   // remember it to do the target later
-  targets.gotos.emplace_back(t, targets.destructor_stack.get_current_node());
+  targets.gotos.emplace_back(t, targets.scope_stack.get_current_node());
 }
 
 void goto_convertt::convert_gcc_computed_goto(
@@ -1391,7 +1390,7 @@ void goto_convertt::convert_start_thread(
 
   // remember it to do target later
   targets.gotos.emplace_back(
-    start_thread, targets.destructor_stack.get_current_node());
+    start_thread, targets.scope_stack.get_current_node());
 }
 
 void goto_convertt::convert_end_thread(

src/goto-programs/goto_convert_class.h

@@ -395,7 +395,7 @@ class goto_convertt:public messaget
     labelst labels;
     gotost gotos;
     computed_gotost computed_gotos;
-    destructor_treet destructor_stack;
+    scope_treet scope_stack;
 
     casest cases;
     cases_mapt cases_map;
@@ -425,14 +425,14 @@ class goto_convertt:public messaget
     {
       break_set=true;
       break_target=_break_target;
-      break_stack_node=destructor_stack.get_current_node();
+      break_stack_node = scope_stack.get_current_node();
     }
 
     void set_continue(goto_programt::targett _continue_target)
     {
       continue_set=true;
       continue_target=_continue_target;
-      continue_stack_node=destructor_stack.get_current_node();
+      continue_stack_node = scope_stack.get_current_node();
     }
 
     void set_default(goto_programt::targett _default_target)
@@ -451,14 +451,14 @@ class goto_convertt:public messaget
     {
       throw_set=true;
       throw_target=_throw_target;
-      throw_stack_node=destructor_stack.get_current_node();
+      throw_stack_node = scope_stack.get_current_node();
     }
 
     void set_leave(goto_programt::targett _leave_target)
     {
       leave_set=true;
       leave_target=_leave_target;
-      leave_stack_node=destructor_stack.get_current_node();
+      leave_stack_node = scope_stack.get_current_node();
     }
   } targets;
 
@@ -497,7 +497,7 @@ class goto_convertt:public messaget
       default_set=targets.default_set;
       break_target=targets.break_target;
       default_target=targets.default_target;
-      break_stack_node=targets.destructor_stack.get_current_node();
+      break_stack_node = targets.scope_stack.get_current_node();
       cases=targets.cases;
       cases_map=targets.cases_map;
     }
@@ -529,7 +529,7 @@ class goto_convertt:public messaget
     {
       throw_set=targets.throw_set;
       throw_target=targets.throw_target;
-      throw_stack_node=targets.destructor_stack.get_current_node();
+      throw_stack_node = targets.scope_stack.get_current_node();
     }
 
     void restore(targetst &targets)
@@ -551,7 +551,7 @@ class goto_convertt:public messaget
     {
       leave_set=targets.leave_set;
       leave_target=targets.leave_target;
-      leave_stack_node=targets.destructor_stack.get_current_node();
+      leave_stack_node = targets.scope_stack.get_current_node();
     }
 
     void restore(targetst &targets)