diff --git a/jbmc/regression/jbmc/stub_identifiers/Opaque.java b/jbmc/regression/jbmc/stub_identifiers/Opaque.java new file mode 100644 index 00000000000..eaf64d7facd --- /dev/null +++ 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 new file mode 100644 index 00000000000..7b746ad8df2 Binary files /dev/null and b/jbmc/regression/jbmc/stub_identifiers/Test.class differ diff --git a/jbmc/regression/jbmc/stub_identifiers/Test.java b/jbmc/regression/jbmc/stub_identifiers/Test.java new file mode 100644 index 00000000000..e8463fb8f57 --- /dev/null +++ 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 new file mode 100644 index 00000000000..e3bd2c638d6 --- /dev/null +++ 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 index a6fc3018f7e..17ff96f84a6 100644 --- 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 index 29935ebedfc..d4af87e9637 100644 --- 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 ¶meters, + 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 index 4c69f282bea..a1ce6bb51d6 100644 --- 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 ¶meters, + 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 index 16a52370fee..099b956e442 100644 --- 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,