Merge pull request #6569 from tautschnig/bugfixes/6566

C nondet factory: Ensure parameter initialisers use unique symbol names

Author: tautschnig

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/array_element_from_pointer.h>
 #include <util/expr_initializer.h>
+#include <util/fresh_symbol.h>
 #include <util/message.h>
 #include <util/nondet_bool.h>
 #include <util/prefix.h>
@@ -103,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);
 
@@ -1110,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)
@@ -1551,24 +1552,18 @@ exprt object_factory(
   const select_pointer_typet &pointer_type_selector,
   message_handlert &log)
 {
-  irep_idt identifier=id2string(goto_functionst::entry_point())+
-    "::"+id2string(base_name);
-
-  auxiliary_symbolt main_symbol;
-  main_symbol.mode=ID_java;
-  main_symbol.is_static_lifetime=false;
-  main_symbol.name=identifier;
-  main_symbol.base_name=base_name;
-  main_symbol.type=type;
-  main_symbol.location=loc;
+  const symbolt &main_symbol = get_fresh_aux_symbol(
+    type,
+    id2string(goto_functionst::entry_point()),
+    id2string(base_name),
+    loc,
+    ID_java,
+    symbol_table);
+
   parameters.function_id = goto_functionst::entry_point();
 
   exprt object=main_symbol.symbol_expr();
 
-  symbolt *main_symbol_ptr;
-  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
-  CHECK_RETURN(!moving_symbol_failed);
-
   java_object_factoryt state(
     loc, parameters, symbol_table, pointer_type_selector, log);
   code_blockt assignments;
@@ -1583,7 +1578,7 @@ exprt object_factory(
     update_in_placet::NO_UPDATE_IN_PLACE,
     loc);
 
-  state.add_created_symbol(main_symbol_ptr);
+  state.add_created_symbol(main_symbol);
   state.declare_created_symbols(init_code);
 
   assert_type_consistency(assignments);

regression/cbmc/pointer-function-parameters/main.c

@@ -0,0 +1,3 @@
+void f(int *b, int tmp)
+{
+}

regression/cbmc/pointer-function-parameters/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--function f
+^EXIT=0$
+^SIGNAL=0$
+VERIFICATION SUCCESSFUL
+--
+^warning: ignoring

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -15,6 +15,7 @@ Author: Diffblue Ltd.
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/fresh_symbol.h>
 #include <util/namespace.h>
 #include <util/nondet_bool.h>
 #include <util/pointer_expr.h>
@@ -204,23 +205,15 @@ symbol_exprt c_nondet_symbol_factory(
   const c_object_factory_parameterst &object_factory_parameters,
   const lifetimet lifetime)
 {
-  irep_idt identifier=id2string(goto_functionst::entry_point())+
-    "::"+id2string(base_name);
-
-  auxiliary_symbolt main_symbol;
-  main_symbol.mode=ID_C;
-  main_symbol.is_static_lifetime=false;
-  main_symbol.name=identifier;
-  main_symbol.base_name=base_name;
-  main_symbol.type=type;
-  main_symbol.location=loc;
-
+  const symbolt &main_symbol = get_fresh_aux_symbol(
+    type,
+    id2string(goto_functionst::entry_point()),
+    id2string(base_name),
+    loc,
+    ID_C,
+    symbol_table);
   symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
 
-  symbolt *main_symbol_ptr;
-  bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
-  CHECK_RETURN(!moving_symbol_failed);
-
   symbol_factoryt state(
     symbol_table,
     loc,
@@ -231,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_ptr);
+  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,11 +228,12 @@ 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());
+      code_declt decl{symbol.symbol_expr()};
       decl.add_source_location() = source_location;
       init_code.add(decl);
     }
@@ -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,