Prefix identifiers in stubs with function name

The name of an auxiliary variable must not depend
on other functions in the symbol table.

Author: peterschrammel

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -117,13 +117,14 @@ static void java_static_lifetime_init(
   symbol_table_baset &symbol_table,
   const source_locationt &source_location,
   bool assume_init_pointers_not_null,
-  const object_factory_parameterst &object_factory_parameters,
+  object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector,
   bool string_refinement_enabled)
 {
   symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION);
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
-
+  object_factory_parameters.function_id = initialize_symbol.name;
+  
   // We need to zero out all static variables, or nondet-initialize if they're
   // external. Iterate over a copy of the symtab, as its iterators are
   // invalidated by object_factory:

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1489,7 +1489,7 @@ exprt object_factory(
   code_blockt &init_code,
   bool allow_null,
   symbol_table_baset &symbol_table,
-  const object_factory_parameterst &parameters,
+  object_factory_parameterst parameters,
   allocation_typet alloc_type,
   const source_locationt &loc,
   const select_pointer_typet &pointer_type_selector)
@@ -1504,7 +1504,8 @@ exprt object_factory(
   main_symbol.base_name=base_name;
   main_symbol.type=type;
   main_symbol.location=loc;
-
+  parameters.function_id = identifier;
+ 
   exprt object=main_symbol.symbol_expr();
 
   symbolt *main_symbol_ptr;

jbmc/src/java_bytecode/java_object_factory.h

@@ -92,7 +92,7 @@ exprt object_factory(
   code_blockt &init_code,
   bool allow_null,
   symbol_table_baset &symbol_table,
-  const object_factory_parameterst &parameters,
+  object_factory_parameterst parameters,
   allocation_typet alloc_type,
   const source_locationt &location,
   const select_pointer_typet &pointer_type_selector);

jbmc/src/java_bytecode/simple_method_stubbing.cpp

@@ -39,6 +39,7 @@ class java_simple_method_stubst
     const typet &expected_type,
     const exprt &ptr,
     const source_locationt &loc,
+    const irep_idt &function_id,
     code_blockt &parent_block,
     unsigned insert_before_index,
     bool is_constructor,
@@ -77,6 +78,7 @@ void java_simple_method_stubst::create_method_stub_at(
   const typet &expected_type,
   const exprt &ptr,
   const source_locationt &loc,
+  const irep_idt &function_id,
   code_blockt &parent_block,
   const unsigned insert_before_index,
   const bool is_constructor,
@@ -108,6 +110,8 @@ void java_simple_method_stubst::create_method_stub_at(
 
   // Generate new instructions.
   code_blockt new_instructions;
+  object_factory_parameterst parameters = object_factory_parameters;
+  parameters.function_id = function_id;
   gen_nondet_init(
     to_init,
     new_instructions,
@@ -116,7 +120,7 @@ void java_simple_method_stubst::create_method_stub_at(
     is_constructor,
     allocation_typet::DYNAMIC,
     !assume_non_null,
-    object_factory_parameters,
+    parameters,
     update_in_place ? update_in_placet::MUST_UPDATE_IN_PLACE
                     : update_in_placet::NO_UPDATE_IN_PLACE);
 
@@ -155,7 +159,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
     const typet &this_type = this_argument.type();
     symbolt &init_symbol = get_fresh_aux_symbol(
       this_type,
-      "to_construct",
+      id2string(symbol.name),
       "to_construct",
       synthesized_source_location,
       ID_java,
@@ -169,6 +173,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
       this_type,
       init_symbol_expression,
       synthesized_source_location,
+      symbol.name,
       new_instructions,
       1,
       true,
@@ -181,14 +186,16 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
     {
       symbolt &to_return_symbol = get_fresh_aux_symbol(
         required_return_type,
-        "to_return",
+        id2string(symbol.name),
         "to_return",
         synthesized_source_location,
         ID_java,
         symbol_table);
       const exprt &to_return = to_return_symbol.symbol_expr();
       if(to_return_symbol.type.id() != ID_pointer)
       {
+        object_factory_parameterst parameters = object_factory_parameters;
+        parameters.function_id = symbol.name;
         gen_nondet_init(
           to_return,
           new_instructions,
@@ -197,14 +204,15 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
           false,
           allocation_typet::LOCAL, // Irrelevant as type is primitive
           !assume_non_null,
-          object_factory_parameters,
+          parameters,
           update_in_placet::NO_UPDATE_IN_PLACE);
       }
       else
         create_method_stub_at(
           required_return_type,
           to_return,
           synthesized_source_location,
+          symbol.name,
           new_instructions,
           0,
           false,