Prefix identifiers in stubs with function name

peterschrammel · peterschrammel · commit 9e9f251d122b · 2018-06-10T23:52:23.000+01:00
The name of an auxiliary variable must not depend
on other functions in the symbol table.
diff --git a/jbmc/regression/jbmc/stub_identifiers/Opaque.java b/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;
+  }
+}
diff --git a/jbmc/regression/jbmc/stub_identifiers/Test.class b/jbmc/regression/jbmc/stub_identifiers/Test.class
diff --git a/jbmc/regression/jbmc/stub_identifiers/Test.java b/jbmc/regression/jbmc/stub_identifiers/Test.java
@@ -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;
+    }
+  }
+}
diff --git a/jbmc/regression/jbmc/stub_identifiers/test.desc b/jbmc/regression/jbmc/stub_identifiers/test.desc
@@ -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.
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -119,13 +119,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
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -1471,7 +1471,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   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)
@@ -1486,6 +1486,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();
 
diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h
@@ -91,7 +91,7 @@ exprt object_factory(
   const irep_idt base_name,
   code_blockt &init_code,
   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);
diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/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,
@@ -112,6 +114,7 @@ void java_simple_method_stubst::create_method_stub_at(
 
   // Generate new instructions.
   code_blockt new_instructions;
+  parameters.function_id = function_id;
   gen_nondet_init(
     to_init,
     new_instructions,
@@ -158,7 +161,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,
@@ -172,6 +175,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,
@@ -184,7 +188,7 @@ 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,
@@ -211,6 +215,7 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol)
           required_return_type,
           to_return,
           synthesized_source_location,
+          symbol.name,
           new_instructions,
           0,
           false,
