From 9e9f251d122bf73db2bbaac9d364336f6231fdd8 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Thu, 31 May 2018 17:14:00 +0100 Subject: [PATCH] Prefix identifiers in stubs with function name The name of an auxiliary variable must not depend on other functions in the symbol table. --- .../jbmc/stub_identifiers/Opaque.java | 16 ++++++++++++ .../jbmc/stub_identifiers/Test.class | Bin 0 -> 635 bytes .../jbmc/stub_identifiers/Test.java | 24 ++++++++++++++++++ .../jbmc/stub_identifiers/test.desc | 23 +++++++++++++++++ jbmc/src/java_bytecode/java_entry_point.cpp | 3 ++- .../src/java_bytecode/java_object_factory.cpp | 3 ++- jbmc/src/java_bytecode/java_object_factory.h | 2 +- .../java_bytecode/simple_method_stubbing.cpp | 9 +++++-- 8 files changed, 75 insertions(+), 5 deletions(-) create mode 100644 jbmc/regression/jbmc/stub_identifiers/Opaque.java create mode 100644 jbmc/regression/jbmc/stub_identifiers/Test.class create mode 100644 jbmc/regression/jbmc/stub_identifiers/Test.java create mode 100644 jbmc/regression/jbmc/stub_identifiers/test.desc 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 0000000000000000000000000000000000000000..7b746ad8df2835f189ef31cf7c2e82ee40b0342e GIT binary patch literal 635 zcmZ9J-A~g{7{;How(CBM8)H*IhoF#jZRfynCB_>Qul8|KLPEGO-F7CO`vN-tE-^-o zM7{TqB0i_vSYn&J=jnT%_x-&+=kNW`-vAD=mq8kjO*}~>f%Oc-hEkhKJyqeEiL!|; zf#ln86h`j^G`n&lpuZn?r9iG8j%0H>Y|G2zpgmwl>+SCgWbJxu5?oB>kutCNQPBC^ z2qv+IwAgkaP*~a)eu0cXo?dq3hfuXkAIq!gRX?~6EM$=79J9U_o?~03au#-!dVw_y zFR{zfREa=d71aj8=u@rL?#m8S)>RZlVdrBnl!LB7YRNR_sg=27D5LW+Ey;x_+Gh)Q z>7^_#eh4V%}Ki2H7`v+AA&uZkn>l3;V33JLic_uRxP z>k3$#bBClF+^a6RjTzT_;JSX(tCIUh-_S{Jcwb_)1Lr?m JE)teN=^tUOX&nFn literal 0 HcmV?d00001 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,