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/regression/jbmc/stub_identifiers/Opaque.java

@@ -0,0 +1,16 @@
+public class Opaque extends Exception
+{
+  public static Opaque static_field;
+  public Opaque field;
+
+  public Opaque(Opaque o) {
+  }
+  
+  public static Opaque static_method(Opaque o) {
+    return o;
+  }
+
+  public Opaque[] method(Opaque[] o) {
+    return o;
+  }
+}

jbmc/regression/jbmc/stub_identifiers/Test.class

@@ -0,0 +1,24 @@
+public class Test
+{
+  public static void f00(Opaque z)
+  {
+    try {
+      Opaque x = new Opaque(Opaque.static_field);
+      Opaque[] a = {Opaque.static_method(x.field), z};
+      Opaque[] y = x.method(a);
+      throw y[0];
+    } catch(Opaque o) {
+    }
+  }
+  public Opaque f01(Opaque z)
+  {
+    try {
+      Opaque x = new Opaque(Opaque.static_field);
+      Opaque[] a = {Opaque.static_method(x.field), z};
+      Opaque[] y = x.method(a);
+      throw y[0];
+    } catch(Opaque o) {
+      return o;
+    }
+  }
+}

jbmc/regression/jbmc/stub_identifiers/Test.java

@@ -0,0 +1,23 @@
+CORE symex-driven-lazy-loading-expected-failure
+Test.class
+--show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+^Symbol\.*: java::Opaque\.static_method:\(LOpaque;\)LOpaque;::malloc_site\$[0-3]?$
+^Symbol\.*: java::Opaque\.method:\(\[LOpaque;\)\[LOpaque;::malloc_site\$[0-3]?$
+--
+^Symbol\.*: malloc_site
+^Symbol\.*: to_construct
+^Symbol\.*: to_return
+^Symbol\.*: this
+^Symbol\.*: caught_exception
+^Symbol\.*: anonlocal
+^Symbol\.*: stub_ignored_arg
+^Symbol\.*: #return_value
+^Symbol\.*: return_tmp
+^Symbol\.*: new_tmp
+^Symbol\.*: tmp_new_data_array
+^Symbol\.*: newarray_tmp
+--
+Does not work with symex-driven lazy loading because we want to check the
+symbol table for the entire program.

jbmc/regression/jbmc/stub_identifiers/test.desc

@@ -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,
   message_handlert &message_handler)
 {
   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

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -1488,7 +1488,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)
@@ -1503,6 +1503,7 @@ exprt object_factory(
   main_symbol.base_name=base_name;
   main_symbol.type=type;
   main_symbol.location=loc;
+  parameters.function_id = goto_functionst::entry_point();
 
   exprt object=main_symbol.symbol_expr();
 

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -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/java_object_factory.h

@@ -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,