From 476107021f8656094762c2528fdc9a48b8f56eb3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Thu, 28 Mar 2019 14:13:03 +0000 Subject: [PATCH 1/6] Add owning class functions as interface to the owner of a symbol Without the functions added by this commit, the only way to access the owner of a symbol for static fields and java methods is through `symbol.type.get(ID_C_class)`. When this technique is used by downstream repositories, they are vulnerable to being broken by upstream changes to how this information is stored in JBMC. The intension of this commit is that the two new functions added will be the standard interface to this symbol -> owner link. This means that future changes to how this information is stored can be made without breaking downstream repositories by changing these two functions. --- jbmc/src/java_bytecode/java_utils.cpp | 11 +++++++++ jbmc/src/java_bytecode/java_utils.h | 11 +++++++++ jbmc/unit/java_bytecode/java_utils_test.cpp | 25 +++++++++++++++++++++ 3 files changed, 47 insertions(+) diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 1dfdfb878df..950d704b1c9 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -464,3 +464,14 @@ symbolt &fresh_java_symbol( return get_fresh_aux_symbol( type, name_prefix, basename_prefix, source_location, ID_java, symbol_table); } + +optionalt owning_class(const symbolt &symbol) +{ + const irep_idt &class_id = symbol.type.get(ID_C_class); + return class_id.empty() ? optionalt{} : class_id; +} + +void set_owning_class(symbolt &symbol, const irep_idt &owning_class) +{ + symbol.type.set(ID_C_class, owning_class); +} diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 0f4b38a9623..a3db247e3ba 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -115,4 +116,14 @@ symbolt &fresh_java_symbol( const irep_idt &function_name, symbol_table_baset &symbol_table); +/// Gets the identifier of the class which owns a given \p symbol. If the symbol +/// is not owned by a class the an empty optional is returned. This is used for +/// method symbols and static field symbols to link them back to the class which +/// owns them. +optionalt owning_class(const symbolt &symbol); + +/// Sets the identifier of the class which owns a given \p symbol to \p +/// owning_class. +void set_owning_class(symbolt &symbol, const irep_idt &owning_class); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/jbmc/unit/java_bytecode/java_utils_test.cpp b/jbmc/unit/java_bytecode/java_utils_test.cpp index d56a08323fd..f5acb56a5b4 100644 --- a/jbmc/unit/java_bytecode/java_utils_test.cpp +++ b/jbmc/unit/java_bytecode/java_utils_test.cpp @@ -368,3 +368,28 @@ SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]") } } } + +SCENARIO("Test symbol ownership.", "[core][java_util_test]") +{ + WHEN("We have a new symbol.") + { + symbolt symbol; + + THEN("The symbol has no owner.") + { + REQUIRE(!owning_class(symbol).has_value()); + } + } + + WHEN("The owning class of a symbol is set.") + { + const auto owning_class = "java::java.lang.object"; + symbolt symbol; + set_owning_class(symbol, owning_class); + + THEN("Getting the owning class of a symbol returns the class set.") + { + REQUIRE(id2string(*::owning_class(symbol)) == owning_class); + } + } +} From bd2bacd2e13387adb0658ea0c9ae7d83b4311540 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Mar 2019 09:08:37 +0000 Subject: [PATCH 2/6] Use owning class functions as interface to the owner of a symbol This commit replaces access to `symbol.type.get(ID_C_class)`. With calls to the `owning_class` function and access to `symbol.type.set(ID_C_class, class_id)` with calls to `set_owning_class`. This allows for changes to how the owner of a symbol is stored by changing these two functions only, rather than by changing all the places where `ID_C_class` was previously accessed directly. This is preparatory work for moving this link from being stored in a comment on a symbols type, to the symbol itself. --- .../java_bytecode_convert_class.cpp | 7 ++- .../java_bytecode_convert_method.cpp | 3 +- .../java_bytecode/java_bytecode_language.cpp | 2 +- .../java_enum_static_init_unwind_handler.cpp | 8 +-- .../java_static_initializers.cpp | 54 ++++++++----------- jbmc/src/jdiff/java_syntactic_diff.cpp | 9 ++-- 6 files changed, 38 insertions(+), 45 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 3241a20fbb7..9094d304c0f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -689,10 +689,9 @@ void java_bytecode_convert_classt::convert( new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name); new_symbol.base_name=f.name; new_symbol.type=field_type; - // Annotating the type with ID_C_class to provide a static field -> class - // link matches the method used by java_bytecode_convert_method::convert - // for methods. - new_symbol.type.set(ID_C_class, class_symbol.name); + // Provide a static field -> class link, like + // java_bytecode_convert_method::convert does for method -> class. + set_owning_class(new_symbol, class_symbol.name); new_symbol.type.set(ID_C_field, f.name); new_symbol.type.set(ID_C_constant, f.is_final); new_symbol.pretty_name=id2string(class_symbol.pretty_name)+ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 9aae017a6e7..ccd724c1a9f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -419,6 +419,8 @@ void java_bytecode_convert_methodt::convert( get_method_identifier(class_symbol.name, m); method_id=method_identifier; + set_owning_class( + symbol_table.get_writeable_ref(method_identifier), class_symbol.name); // Obtain a std::vector of java_method_typet::parametert objects from the // (function) type of the symbol @@ -428,7 +430,6 @@ void java_bytecode_convert_methodt::convert( // to the symbol later. java_method_typet method_type = to_java_method_type(symbol_table.lookup_ref(method_identifier).type); - method_type.set(ID_C_class, class_symbol.name); method_type.set_is_final(m.is_final); method_return_type = method_type.return_type(); java_method_typet::parameterst ¶meters = method_type.parameters(); diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 4c895d2a3da..173a119087d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -496,7 +496,7 @@ static void create_stub_global_symbol( new_symbol.name = symbol_id; new_symbol.base_name = symbol_basename; new_symbol.type = symbol_type; - new_symbol.type.set(ID_C_class, class_id); + set_owning_class(new_symbol, class_id); // Public access is a guess; it encourages merging like-typed static fields, // whereas a more restricted visbility would encourage separating them. // Neither is correct, as without the class file we can't know the truth. diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp index bbdc9c92532..f099cbc66d0 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp +++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp @@ -10,6 +10,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com /// Unwind loops in static initializers #include "java_enum_static_init_unwind_handler.h" +#include "java_utils.h" #include #include @@ -76,11 +77,10 @@ tvt java_enum_static_init_unwind_handler( return tvt::unknown(); const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id); - irep_idt class_id = function_symbol.type.get(ID_C_class); - INVARIANT( - !class_id.empty(), "functions should have their defining class annotated"); + const auto class_id = owning_class(function_symbol); + INVARIANT(class_id, "Java methods should have a defining class."); - const typet &class_type = symbol_table.lookup_ref(class_id).type; + const typet &class_type = symbol_table.lookup_ref(*class_id).type; size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind); if(unwinds != 0 && unwind_count < unwinds) { diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 051ad245b4d..99df9dab8d9 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -232,7 +232,7 @@ static void clinit_wrapper_do_recursive_calls( symbol_table.symbols.end(), [&](const std::pair &symbol) { if( - symbol.second.type.get(ID_C_class) == class_name && + owning_class(symbol.second) == class_name && symbol.second.is_static_lifetime && !symbol.second.type.get_bool(ID_C_constant)) { @@ -352,10 +352,9 @@ static void create_clinit_wrapper_symbols( wrapper_method_symbol.pretty_name = wrapper_method_symbol.name; wrapper_method_symbol.base_name = "clinit_wrapper"; wrapper_method_symbol.type = wrapper_method_type; - // Note this use of a type-comment to provide a back-link from a method - // to its associated class is the same one used in - // java_bytecode_convert_methodt::convert - wrapper_method_symbol.type.set(ID_C_class, class_name); + // This provides a back-link from a method to its associated class, as is done + // for java_bytecode_convert_methodt::convert. + set_owning_class(wrapper_method_symbol, class_name); wrapper_method_symbol.mode = ID_java; bool failed = symbol_table.add(wrapper_method_symbol); INVARIANT(!failed, "clinit-wrapper symbol should be fresh"); @@ -453,21 +452,20 @@ code_blockt get_thread_safe_clinit_wrapper_body( message_handlert &message_handler) { const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id); - irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class); - INVARIANT( - !class_name.empty(), "wrapper function should be annotated with its class"); + const auto class_name = owning_class(wrapper_method_symbol); + INVARIANT(class_name, "Wrapper function should have an owning class."); const symbolt &clinit_state_sym = - symbol_table.lookup_ref(clinit_state_var_name(class_name)); + symbol_table.lookup_ref(clinit_state_var_name(*class_name)); const symbolt &clinit_thread_local_state_sym = - symbol_table.lookup_ref(clinit_thread_local_state_var_name(class_name)); + symbol_table.lookup_ref(clinit_thread_local_state_var_name(*class_name)); // Create a function-local variable "init_complete". This variable is used to // avoid inspecting the global state (clinit_state_sym) outside of // the critical-section. const symbolt &init_complete = add_new_variable_symbol( symbol_table, - clinit_local_init_complete_var_name(class_name), + clinit_local_init_complete_var_name(*class_name), bool_typet(), nil_exprt(), true, @@ -598,7 +596,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( code_blockt init_body; clinit_wrapper_do_recursive_calls( symbol_table, - class_name, + *class_name, init_body, nondet_static, object_factory_parameters, @@ -666,12 +664,11 @@ code_ifthenelset get_clinit_wrapper_body( // } // } const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id); - irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class); - INVARIANT( - !class_name.empty(), "wrapper function should be annotated with its class"); + const auto class_name = owning_class(wrapper_method_symbol); + INVARIANT(class_name, "Wrapper function should have an owning class."); const symbolt &already_run_symbol = - symbol_table.lookup_ref(clinit_already_run_variable_name(class_name)); + symbol_table.lookup_ref(clinit_already_run_variable_name(*class_name)); equal_exprt check_already_run( already_run_symbol.symbol_expr(), @@ -683,7 +680,7 @@ code_ifthenelset get_clinit_wrapper_body( clinit_wrapper_do_recursive_calls( symbol_table, - class_name, + *class_name, init_body, nondet_static, object_factory_parameters, @@ -766,12 +763,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( continue; } - const irep_idt class_id = - global_symbol.type.get(ID_C_class); - INVARIANT( - !class_id.empty(), - "static field should be annotated with its defining class"); - stub_globals_by_class.insert({class_id, stub_global}); + const auto class_id = owning_class(global_symbol); + INVARIANT(class_id, "Static field should have a defining class."); + stub_globals_by_class.insert({*class_id, stub_global}); } // For each distinct class that has stub globals, create a clinit symbol: @@ -799,10 +793,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( static_init_symbol.base_name = "clinit():V"; static_init_symbol.mode = ID_java; static_init_symbol.type = thunk_type; - // Note this use of a type-comment to provide a back-link from a method - // to its associated class is the same one used in - // java_bytecode_convert_methodt::convert - static_init_symbol.type.set(ID_C_class, it->first); + // This provides a back-link from a method to its associated class, as is + // done for java_bytecode_convert_methodt::convert. + set_owning_class(static_init_symbol, it->first); bool failed = symbol_table.add(static_init_symbol); INVARIANT(!failed, "symbol should not already exist"); @@ -839,17 +832,16 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body( message_handlert &message_handler) { const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id); - irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class); + const auto class_id = owning_class(stub_initializer_symbol); INVARIANT( - !class_id.empty(), - "synthetic static initializer should be annotated with its class"); + class_id, "Synthetic static initializer should have an owning class."); code_blockt static_init_body; // Add a standard nondet initialisation for each global declared on this // class. Note this is the same invocation used in // java_static_lifetime_init. - auto class_globals = stub_globals_by_class.equal_range(class_id); + auto class_globals = stub_globals_by_class.equal_range(*class_id); INVARIANT( class_globals.first != class_globals.second, "class with synthetic clinit should have at least one global to init"); diff --git a/jbmc/src/jdiff/java_syntactic_diff.cpp b/jbmc/src/jdiff/java_syntactic_diff.cpp index b99707a1f4c..2296ab67c55 100644 --- a/jbmc/src/jdiff/java_syntactic_diff.cpp +++ b/jbmc/src/jdiff/java_syntactic_diff.cpp @@ -12,6 +12,7 @@ Author: Peter Schrammel #include "java_syntactic_diff.h" #include +#include bool java_syntactic_difft::operator()() { @@ -35,16 +36,16 @@ bool java_syntactic_difft::operator()() CHECK_RETURN(fun1 != nullptr); const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first); CHECK_RETURN(fun2 != nullptr); - const irep_idt &class_name = fun1->type.get(ID_C_class); + const optionalt class_name = owning_class(*fun1); bool function_access_changed = fun1->type.get(ID_access) != fun2->type.get(ID_access); bool class_access_changed = false; bool field_access_changed = false; - if(!class_name.empty()) + if(class_name) { - const symbolt *class1 = goto_model1.symbol_table.lookup(class_name); + const symbolt *class1 = goto_model1.symbol_table.lookup(*class_name); CHECK_RETURN(class1 != nullptr); - const symbolt *class2 = goto_model2.symbol_table.lookup(class_name); + const symbolt *class2 = goto_model2.symbol_table.lookup(*class_name); CHECK_RETURN(class2 != nullptr); class_access_changed = class1->type.get(ID_access) != class2->type.get(ID_access); From 242bb0feb9e8e4a0407321aee646515ae1c28871 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Mar 2019 11:30:17 +0000 Subject: [PATCH 3/6] Rename `owning_class` to `declaring_class` --- .../java_bytecode_convert_class.cpp | 2 +- .../java_bytecode_convert_method.cpp | 2 +- .../java_bytecode/java_bytecode_language.cpp | 2 +- .../java_enum_static_init_unwind_handler.cpp | 2 +- .../java_bytecode/java_static_initializers.cpp | 14 +++++++------- jbmc/src/java_bytecode/java_utils.cpp | 6 +++--- jbmc/src/java_bytecode/java_utils.h | 18 +++++++++--------- jbmc/src/jdiff/java_syntactic_diff.cpp | 2 +- jbmc/unit/java_bytecode/java_utils_test.cpp | 16 ++++++++-------- 9 files changed, 32 insertions(+), 32 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 9094d304c0f..5580caa8862 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -691,7 +691,7 @@ void java_bytecode_convert_classt::convert( new_symbol.type=field_type; // Provide a static field -> class link, like // java_bytecode_convert_method::convert does for method -> class. - set_owning_class(new_symbol, class_symbol.name); + set_declaring_class(new_symbol, class_symbol.name); new_symbol.type.set(ID_C_field, f.name); new_symbol.type.set(ID_C_constant, f.is_final); new_symbol.pretty_name=id2string(class_symbol.pretty_name)+ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index ccd724c1a9f..5c5824408a1 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -419,7 +419,7 @@ void java_bytecode_convert_methodt::convert( get_method_identifier(class_symbol.name, m); method_id=method_identifier; - set_owning_class( + set_declaring_class( symbol_table.get_writeable_ref(method_identifier), class_symbol.name); // Obtain a std::vector of java_method_typet::parametert objects from the diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 173a119087d..a1450e0e7ba 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -496,7 +496,7 @@ static void create_stub_global_symbol( new_symbol.name = symbol_id; new_symbol.base_name = symbol_basename; new_symbol.type = symbol_type; - set_owning_class(new_symbol, class_id); + set_declaring_class(new_symbol, class_id); // Public access is a guess; it encourages merging like-typed static fields, // whereas a more restricted visbility would encourage separating them. // Neither is correct, as without the class file we can't know the truth. diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp index f099cbc66d0..904e2785bbd 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp +++ b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp @@ -77,7 +77,7 @@ tvt java_enum_static_init_unwind_handler( return tvt::unknown(); const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id); - const auto class_id = owning_class(function_symbol); + const auto class_id = declaring_class(function_symbol); INVARIANT(class_id, "Java methods should have a defining class."); const typet &class_type = symbol_table.lookup_ref(*class_id).type; diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 99df9dab8d9..0c8c8221901 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/jbmc/src/java_bytecode/java_static_initializers.cpp @@ -232,7 +232,7 @@ static void clinit_wrapper_do_recursive_calls( symbol_table.symbols.end(), [&](const std::pair &symbol) { if( - owning_class(symbol.second) == class_name && + declaring_class(symbol.second) == class_name && symbol.second.is_static_lifetime && !symbol.second.type.get_bool(ID_C_constant)) { @@ -354,7 +354,7 @@ static void create_clinit_wrapper_symbols( wrapper_method_symbol.type = wrapper_method_type; // This provides a back-link from a method to its associated class, as is done // for java_bytecode_convert_methodt::convert. - set_owning_class(wrapper_method_symbol, class_name); + set_declaring_class(wrapper_method_symbol, class_name); wrapper_method_symbol.mode = ID_java; bool failed = symbol_table.add(wrapper_method_symbol); INVARIANT(!failed, "clinit-wrapper symbol should be fresh"); @@ -452,7 +452,7 @@ code_blockt get_thread_safe_clinit_wrapper_body( message_handlert &message_handler) { const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id); - const auto class_name = owning_class(wrapper_method_symbol); + const auto class_name = declaring_class(wrapper_method_symbol); INVARIANT(class_name, "Wrapper function should have an owning class."); const symbolt &clinit_state_sym = @@ -664,7 +664,7 @@ code_ifthenelset get_clinit_wrapper_body( // } // } const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id); - const auto class_name = owning_class(wrapper_method_symbol); + const auto class_name = declaring_class(wrapper_method_symbol); INVARIANT(class_name, "Wrapper function should have an owning class."); const symbolt &already_run_symbol = @@ -763,7 +763,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( continue; } - const auto class_id = owning_class(global_symbol); + const auto class_id = declaring_class(global_symbol); INVARIANT(class_id, "Static field should have a defining class."); stub_globals_by_class.insert({*class_id, stub_global}); } @@ -795,7 +795,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( static_init_symbol.type = thunk_type; // This provides a back-link from a method to its associated class, as is // done for java_bytecode_convert_methodt::convert. - set_owning_class(static_init_symbol, it->first); + set_declaring_class(static_init_symbol, it->first); bool failed = symbol_table.add(static_init_symbol); INVARIANT(!failed, "symbol should not already exist"); @@ -832,7 +832,7 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body( message_handlert &message_handler) { const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id); - const auto class_id = owning_class(stub_initializer_symbol); + const auto class_id = declaring_class(stub_initializer_symbol); INVARIANT( class_id, "Synthetic static initializer should have an owning class."); code_blockt static_init_body; diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 950d704b1c9..91f9e2a4dbb 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/jbmc/src/java_bytecode/java_utils.cpp @@ -465,13 +465,13 @@ symbolt &fresh_java_symbol( type, name_prefix, basename_prefix, source_location, ID_java, symbol_table); } -optionalt owning_class(const symbolt &symbol) +optionalt declaring_class(const symbolt &symbol) { const irep_idt &class_id = symbol.type.get(ID_C_class); return class_id.empty() ? optionalt{} : class_id; } -void set_owning_class(symbolt &symbol, const irep_idt &owning_class) +void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class) { - symbol.type.set(ID_C_class, owning_class); + symbol.type.set(ID_C_class, declaring_class); } diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index a3db247e3ba..d2eddf81a10 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -116,14 +116,14 @@ symbolt &fresh_java_symbol( const irep_idt &function_name, symbol_table_baset &symbol_table); -/// Gets the identifier of the class which owns a given \p symbol. If the symbol -/// is not owned by a class the an empty optional is returned. This is used for -/// method symbols and static field symbols to link them back to the class which -/// owns them. -optionalt owning_class(const symbolt &symbol); - -/// Sets the identifier of the class which owns a given \p symbol to \p -/// owning_class. -void set_owning_class(symbolt &symbol, const irep_idt &owning_class); +/// Gets the identifier of the class which declared a given \p symbol. If the +/// symbol is not declared by a class then an empty optional is returned. This +/// is used for method symbols and static field symbols to link them back to the +/// class which declared them. +optionalt declaring_class(const symbolt &symbol); + +/// Sets the identifier of the class which declared a given \p symbol to \p +/// declaring_class. +void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class); #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/jbmc/src/jdiff/java_syntactic_diff.cpp b/jbmc/src/jdiff/java_syntactic_diff.cpp index 2296ab67c55..bc436f691a7 100644 --- a/jbmc/src/jdiff/java_syntactic_diff.cpp +++ b/jbmc/src/jdiff/java_syntactic_diff.cpp @@ -36,7 +36,7 @@ bool java_syntactic_difft::operator()() CHECK_RETURN(fun1 != nullptr); const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first); CHECK_RETURN(fun2 != nullptr); - const optionalt class_name = owning_class(*fun1); + const optionalt class_name = declaring_class(*fun1); bool function_access_changed = fun1->type.get(ID_access) != fun2->type.get(ID_access); bool class_access_changed = false; diff --git a/jbmc/unit/java_bytecode/java_utils_test.cpp b/jbmc/unit/java_bytecode/java_utils_test.cpp index f5acb56a5b4..3bee7b0c05d 100644 --- a/jbmc/unit/java_bytecode/java_utils_test.cpp +++ b/jbmc/unit/java_bytecode/java_utils_test.cpp @@ -369,27 +369,27 @@ SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]") } } -SCENARIO("Test symbol ownership.", "[core][java_util_test]") +SCENARIO("Test symbol declarers.", "[core][java_util_test]") { WHEN("We have a new symbol.") { symbolt symbol; - THEN("The symbol has no owner.") + THEN("The symbol has no declarer.") { - REQUIRE(!owning_class(symbol).has_value()); + REQUIRE(!declaring_class(symbol).has_value()); } } - WHEN("The owning class of a symbol is set.") + WHEN("The declaring class of a symbol is set.") { - const auto owning_class = "java::java.lang.object"; + const auto declaring_class = "java::java.lang.object"; symbolt symbol; - set_owning_class(symbol, owning_class); + set_declaring_class(symbol, declaring_class); - THEN("Getting the owning class of a symbol returns the class set.") + THEN("Getting the declaring class of a symbol returns the class set.") { - REQUIRE(id2string(*::owning_class(symbol)) == owning_class); + REQUIRE(id2string(*::declaring_class(symbol)) == declaring_class); } } } From ba971c0a61cab128cee5c952e63bfdb6d77ed766 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Mar 2019 12:29:11 +0000 Subject: [PATCH 4/6] Fix missing declaring class of opaque methods --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 1 + .../java_bytecode_convert_method/convert_method.cpp | 8 ++++++++ 2 files changed, 9 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 5c5824408a1..f1b5fe03e2d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2207,6 +2207,7 @@ void java_bytecode_convert_methodt::convert_invoke( symbol.mode = ID_java; assign_parameter_names( to_java_method_type(symbol.type), symbol.name, symbol_table); + set_declaring_class(symbol, arg0.get(ID_C_class)); debug() << "Generating codet: new opaque symbol: method '" << symbol.name << "'" << eom; diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index b4539c8f0e1..d74c926e92b 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -8,11 +8,14 @@ Author: Diffblue Limited. #include +#include #include #include #include +#include + SCENARIO( "java_bytecode_convert_bridge_method", "[core][java_bytecode][java_bytecode_convert_method]") @@ -138,6 +141,11 @@ SCENARIO( { REQUIRE(function_type.get_is_final()); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == "java::OpaqueClass"); + } } } } From 115417a332ae7825b120f896c67c397ad3d2ab6c Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Mar 2019 13:28:00 +0000 Subject: [PATCH 5/6] Add unit tests covering method parsing setting `declaring_class` --- .../ClassWithStaticMethod.class | Bin 0 -> 347 bytes .../ClassWithStaticMethod.java | 5 + .../convert_method.cpp | 106 ++++++++++++++---- 3 files changed, 91 insertions(+), 20 deletions(-) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.class b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.class new file mode 100644 index 0000000000000000000000000000000000000000..93e79e8b5dccd4c7ca31b06c4a91042c981d294f GIT binary patch literal 347 zcmZvXze)o^5XQf`zvhf421H0_rxspgr`QAn!o?JkSnq8XZ^L;9cY8jSja9(H2gpMO zXE%aPwwRgkH{Z-M+uipMfIEy5_!z_(#yBHH54zIkk>FolFA2e#pofH2566z!;j!!RO8=7;;eXO+b;8WU=`RXiM9=^L literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java new file mode 100644 index 00000000000..e70df5f7e10 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java @@ -0,0 +1,5 @@ +public class ClassWithStaticMethod { + public static int staticFunc() { + return 0; + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index d74c926e92b..dbe50f0523f 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -42,20 +42,29 @@ SCENARIO( { REQUIRE(function_type.get_bool(ID_is_bridge_method)); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == + "java::ClassWithBridgeMethod"); + } } WHEN("When parsing a non-bridge method") { - THEN("THe method should not be marked as a bridge method") - { - const symbolt function_symbol = - symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I"); + const symbolt function_symbol = + symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I"); - const java_method_typet &function_type = - require_type::require_java_method(function_symbol.type); - THEN("The method should be marked as a bridge method") - { - REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method)); - } + const java_method_typet &function_type = + require_type::require_java_method(function_symbol.type); + THEN("The method should not be marked as a bridge method.") + { + REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method)); + } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == + "java::ClassWithBridgeMethod"); } } } @@ -81,20 +90,29 @@ SCENARIO( { REQUIRE(to_java_method_type(function_type).get_native()); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == + "java::ClassWithNativeMethod"); + } } WHEN("When parsing a non-native method") { - THEN("THe method should not be marked as a native method") - { - const symbolt function_symbol = - symbol_table.lookup_ref(method_name + ":(I)Z"); + const symbolt function_symbol = + symbol_table.lookup_ref(method_name + ":(I)Z"); - const java_method_typet &function_type = - require_type::require_java_method(function_symbol.type); - THEN("The method should be marked as a native method") - { - REQUIRE_FALSE(to_java_method_type(function_type).get_native()); - } + const java_method_typet &function_type = + require_type::require_java_method(function_symbol.type); + THEN("The method should not be marked as a native method.") + { + REQUIRE_FALSE(to_java_method_type(function_type).get_native()); + } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == + "java::ClassWithNativeMethod"); } } } @@ -119,6 +137,12 @@ SCENARIO( { REQUIRE(function_type.get_is_final()); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == + "java::ClassWithFinalMethod"); + } } WHEN("When parsing a non-final method") { @@ -130,6 +154,12 @@ SCENARIO( { REQUIRE(!function_type.get_is_final()); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(function_symbol)) == + "java::ClassWithFinalMethod"); + } } WHEN("When parsing an opaque method") { @@ -169,6 +199,12 @@ SCENARIO( { REQUIRE(method_type.get_is_varargs()); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(method_symbol)) == + "java::ClassWithVarArgsMethod"); + } } WHEN("When parsing a method with constant number of arguments") { @@ -180,6 +216,36 @@ SCENARIO( { REQUIRE_FALSE(method_type.get_is_varargs()); } + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(method_symbol)) == + "java::ClassWithVarArgsMethod"); + } + } + } +} + +SCENARIO( + "java_bytecode_convert_static_method", + "[core][java_bytecode][java_bytecode_convert_method]") +{ + GIVEN("A class with a static method.") + { + const symbol_tablet symbol_table = load_java_class( + "ClassWithStaticMethod", "./java_bytecode/java_bytecode_convert_method"); + + WHEN("Parsing a static method.") + { + const symbolt method_symbol = + symbol_table.lookup_ref("java::ClassWithStaticMethod.staticFunc:()I"); + + THEN("The method should be marked as declared by its class") + { + REQUIRE( + id2string(*declaring_class(method_symbol)) == + "java::ClassWithStaticMethod"); + } } } } From 65e3d31a79aa9c439b7bad473509a93d48092783 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 29 Mar 2019 14:23:26 +0000 Subject: [PATCH 6/6] Test that parsed static fields have correct `declaring_class` --- .../inherited_static_fields.cpp | 71 +++++++++++++++++++ 1 file changed, 71 insertions(+) diff --git a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp index fe32f90b8bf..a505fed318e 100644 --- a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp +++ b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp @@ -12,6 +12,7 @@ Author: Diffblue Ltd. #include #include +#include #include /// Check the full tree of expr for any symbol_exprts that have an identifier id @@ -37,6 +38,12 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::Parent1.x")); } + THEN("Static field 'Parent1.x' should be declared by class Parent1") + { + REQUIRE( + id2string(*declaring_class( + symbol_table.lookup_ref("java::Parent1.x"))) == "java::Parent1"); + } THEN("No static field 'Test1.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test1.x")); @@ -62,6 +69,14 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::StaticInterface2.x")); } + THEN( + "Static field 'java::StaticInterface2.x' should be declared by " + "StaticInterface2") + { + REQUIRE( + id2string(*declaring_class(symbol_table.lookup_ref( + "java::StaticInterface2.x"))) == "java::StaticInterface2"); + } THEN("No static field 'Test2.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test2.x")); @@ -93,6 +108,14 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::OpaqueParent3.x")); } + THEN( + "Static field 'OpaqueParent3.x' should be declared by class " + "OpaqueParent3") + { + REQUIRE( + id2string(*declaring_class(symbol_table.lookup_ref( + "java::OpaqueParent3.x"))) == "java::OpaqueParent3"); + } THEN("No static field 'Test3.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test3.x")); @@ -124,6 +147,14 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::OpaqueInterface4.x")); } + THEN( + "Static field 'OpaqueInterface4.x' should be declared by class " + "OpaqueInterface4") + { + REQUIRE( + id2string(*declaring_class(symbol_table.lookup_ref( + "java::OpaqueInterface4.x"))) == "java::OpaqueInterface4"); + } THEN("No static field 'Test4.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test4.x")); @@ -191,6 +222,12 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::Parent6.x")); } + THEN("Static field 'Parent6.x' should be declared by class Parent6") + { + REQUIRE( + id2string(*declaring_class( + symbol_table.lookup_ref("java::Parent6.x"))) == "java::Parent6"); + } THEN("No static field 'Test6.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test6.x")); @@ -217,10 +254,26 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::otherpackage.Parent7.x")); } + THEN( + "Static field 'otherpackage.Parent7.x' should be declared by class " + "otherpackage.Parent7") + { + REQUIRE( + id2string(*declaring_class(symbol_table.lookup_ref( + "java::otherpackage.Parent7.x"))) == "java::otherpackage.Parent7"); + } THEN("A static field StaticInterface7.x should exist") { REQUIRE(symbol_table.has_symbol("java::StaticInterface7.x")); } + THEN( + "Static field 'StaticInterface7.x' should be declared by class " + "StaticInterface7") + { + REQUIRE( + id2string(*declaring_class(symbol_table.lookup_ref( + "java::StaticInterface7.x"))) == "java::StaticInterface7"); + } THEN("No static field 'Test7.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test7.x")); @@ -253,6 +306,12 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::Parent8.x")); } + THEN("Static field 'Parent8.x' should be declared by class Parent8") + { + REQUIRE( + id2string(*declaring_class( + symbol_table.lookup_ref("java::Parent8.x"))) == "java::Parent8"); + } THEN("No static field 'Test8.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test8.x")); @@ -279,10 +338,22 @@ SCENARIO( { REQUIRE(symbol_table.has_symbol("java::Parent9.x")); } + THEN("Static field 'Parent9.x' should be declared by class Parent9") + { + REQUIRE( + id2string(*declaring_class( + symbol_table.lookup_ref("java::Parent9.x"))) == "java::Parent9"); + } THEN("A static field StaticInterface9.x should exist") { REQUIRE(symbol_table.has_symbol("java::StaticInterface9.x")); } + THEN("Static field 'Parent8.x' should be declared by StaticInterface9") + { + REQUIRE( + id2string(*declaring_class(symbol_table.lookup_ref( + "java::StaticInterface9.x"))) == "java::StaticInterface9"); + } THEN("No static field 'Test9.x' should be created") { REQUIRE(!symbol_table.has_symbol("java::Test9.x"));