allocate_objectst::add_created_symbol: do not use pointers

Use references and symbol names to track created symbols rather than
pointers. This avoids the risk of dereferencing pointers to objects that
have been deallocated by the time dereferencing takes place.

This is just defensive programming, no known bugs fixes or changes in
behaviour intended.

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -104,7 +104,7 @@ class java_object_factoryt
     update_in_placet,
     const source_locationt &location);
 
-  void add_created_symbol(const symbolt *symbol);
+  void add_created_symbol(const symbolt &symbol);
 
   void declare_created_symbols(code_blockt &init_code);
 
@@ -1111,9 +1111,9 @@ void java_object_factoryt::gen_nondet_init(
   }
 }
 
-void java_object_factoryt::add_created_symbol(const symbolt *symbol_ptr)
+void java_object_factoryt::add_created_symbol(const symbolt &symbol)
 {
-  allocate_objects.add_created_symbol(symbol_ptr);
+  allocate_objects.add_created_symbol(symbol);
 }
 
 void java_object_factoryt::declare_created_symbols(code_blockt &init_code)
@@ -1578,7 +1578,7 @@ exprt object_factory(
     update_in_placet::NO_UPDATE_IN_PLACE,
     loc);
 
-  state.add_created_symbol(&main_symbol);
+  state.add_created_symbol(main_symbol);
   state.declare_created_symbols(init_code);
 
   assert_type_consistency(assignments);

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -224,7 +224,7 @@ symbol_exprt c_nondet_symbol_factory(
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 
-  state.add_created_symbol(&main_symbol);
+  state.add_created_symbol(main_symbol);
   state.declare_created_symbols(init_code);
 
   init_code.append(assignments);

src/ansi-c/c_nondet_symbol_factory.h

@@ -56,9 +56,9 @@ class symbol_factoryt
     recursion_sett recursion_set = recursion_sett(),
     const bool assign_const = true);
 
-  void add_created_symbol(const symbolt *symbol_ptr)
+  void add_created_symbol(const symbolt &symbol)
   {
-    allocate_objects.add_created_symbol(symbol_ptr);
+    allocate_objects.add_created_symbol(symbol);
   }
 
   void declare_created_symbols(code_blockt &init_code)

src/goto-programs/allocate_objects.cpp

@@ -116,7 +116,7 @@ symbol_exprt allocate_objectst::allocate_automatic_local_object(
     symbol_mode,
     symbol_table);
 
-  symbols_created.push_back(&aux_symbol);
+  add_created_symbol(aux_symbol);
 
   return aux_symbol.symbol_expr();
 }
@@ -153,7 +153,7 @@ exprt allocate_objectst::allocate_dynamic_object_symbol(
     symbol_mode,
     symbol_table);
 
-  symbols_created.push_back(&malloc_sym);
+  add_created_symbol(malloc_sym);
 
   code_frontend_assignt assign =
     make_allocate_code(malloc_sym.symbol_expr(), object_size.value());
@@ -194,7 +194,7 @@ exprt allocate_objectst::allocate_non_dynamic_object(
     symbol_table);
 
   aux_symbol.is_static_lifetime = static_lifetime;
-  symbols_created.push_back(&aux_symbol);
+  add_created_symbol(aux_symbol);
 
   exprt aoe = typecast_exprt::conditional_cast(
     address_of_exprt(aux_symbol.symbol_expr()), target_expr.type());
@@ -215,10 +215,10 @@ exprt allocate_objectst::allocate_non_dynamic_object(
 
 /// Add a pointer to a symbol to the list of pointers to symbols created so far
 ///
-/// \param symbol_ptr: pointer to a symbol in the symbol table
-void allocate_objectst::add_created_symbol(const symbolt *symbol_ptr)
+/// \param symbol: symbol in the symbol table
+void allocate_objectst::add_created_symbol(const symbolt &symbol)
 {
-  symbols_created.push_back(symbol_ptr);
+  symbols_created.push_back(symbol.name);
 }
 
 /// Adds declarations for all non-static symbols created
@@ -228,9 +228,10 @@ void allocate_objectst::declare_created_symbols(code_blockt &init_code)
 {
   // Add the following code to init_code for each symbol that's been created:
   //   <type> <identifier>;
-  for(const symbolt *const symbol_ptr : symbols_created)
+  for(const auto &symbol_id : symbols_created)
   {
-    if(!symbol_ptr->is_static_lifetime)
+    const symbolt &symbol = ns.lookup(symbol_id);
+    if(!symbol.is_static_lifetime)
     {
       code_declt decl(symbol_ptr->symbol_expr());
       decl.add_source_location() = source_location;
@@ -246,10 +247,11 @@ void allocate_objectst::mark_created_symbols_as_input(code_blockt &init_code)
 {
   // Add the following code to init_code for each symbol that's been created:
   //   INPUT("<identifier>", <identifier>);
-  for(symbolt const *symbol_ptr : symbols_created)
+  for(const auto &symbol_id : symbols_created)
   {
-    init_code.add(code_inputt{
-      symbol_ptr->base_name, symbol_ptr->symbol_expr(), source_location});
+    const symbolt &symbol = ns.lookup(symbol_id);
+    init_code.add(
+      code_inputt{symbol.base_name, symbol.symbol_expr(), source_location});
   }
 }
 

src/goto-programs/allocate_objects.h

@@ -93,7 +93,7 @@ class allocate_objectst
     const typet &allocate_type,
     const irep_idt &basename_prefix = "tmp");
 
-  void add_created_symbol(const symbolt *symbol_ptr);
+  void add_created_symbol(const symbolt &symbol);
 
   void declare_created_symbols(code_blockt &init_code);
 
@@ -107,7 +107,7 @@ class allocate_objectst
   symbol_table_baset &symbol_table;
   const namespacet ns;
 
-  std::vector<const symbolt *> symbols_created;
+  std::vector<irep_idt> symbols_created;
 
   exprt allocate_non_dynamic_object(
     code_blockt &assignments,