From f3160e12b17d6afaf5c0c2d53b40e0f3e0a53878 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 15:01:24 +0000 Subject: [PATCH 01/14] resolve_concrete_function_callt -> resolve_inherited_componentt This actually doesn't have any logic specific to function calls, and can be used to resolve inherited fields too. --- src/goto-programs/Makefile | 2 +- .../remove_virtual_functions.cpp | 17 +-- .../resolve_concrete_function_call.cpp | 102 ------------------ .../resolve_concrete_function_call.h | 75 ------------- .../resolve_inherited_component.cpp | 102 ++++++++++++++++++ .../resolve_inherited_component.h | 75 +++++++++++++ src/java_bytecode/ci_lazy_methods.cpp | 10 +- .../java_bytecode_convert_method.cpp | 10 +- 8 files changed, 197 insertions(+), 196 deletions(-) delete mode 100644 src/goto-programs/resolve_concrete_function_call.cpp delete mode 100644 src/goto-programs/resolve_concrete_function_call.h create mode 100644 src/goto-programs/resolve_inherited_component.cpp create mode 100644 src/goto-programs/resolve_inherited_component.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index e12c9e5f145..e01482d883a 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -52,7 +52,7 @@ SRC = basic_blocks.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ replace_java_nondet.cpp \ - resolve_concrete_function_call.cpp \ + resolve_inherited_component.cpp \ safety_checker.cpp \ set_properties.cpp \ show_goto_functions.cpp \ diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 3372e390a42..041f8382f1c 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "class_hierarchy.h" #include "class_identifier.h" -#include +#include #include #include @@ -48,7 +48,7 @@ class remove_virtual_functionst void get_functions(const exprt &, dispatch_table_entriest &); typedef std::function< - resolve_concrete_function_callt::concrete_function_callt( + resolve_inherited_componentt::inherited_componentt( const irep_idt &, const irep_idt &)> function_call_resolvert; @@ -343,13 +343,14 @@ void remove_virtual_functionst::get_child_functions_rec( } if(function.symbol_expr == symbol_exprt()) { - const resolve_concrete_function_callt::concrete_function_callt + const resolve_inherited_componentt::inherited_componentt &resolved_call = resolve_function_call(child, component_name); if(resolved_call.is_valid()) { function.class_id = resolved_call.get_class_identifier(); const symbolt &called_symbol = - symbol_table.lookup_ref(resolved_call.get_virtual_method_name()); + symbol_table.lookup_ref( + resolved_call.get_full_component_identifier()); function.symbol_expr = called_symbol.symbol_expr(); function.symbol_expr.set( @@ -384,7 +385,7 @@ void remove_virtual_functionst::get_functions( const std::string function_name_string(id2string(function_name)); INVARIANT(!class_id.empty(), "All virtual functions must have a class"); - resolve_concrete_function_callt get_virtual_call_target( + resolve_inherited_componentt get_virtual_call_target( symbol_table, class_hierarchy); const function_call_resolvert resolve_function_call = [&get_virtual_call_target]( @@ -392,7 +393,7 @@ void remove_virtual_functionst::get_functions( return get_virtual_call_target(class_id, function_name); }; - const resolve_concrete_function_callt::concrete_function_callt + const resolve_inherited_componentt::inherited_componentt &resolved_call = get_virtual_call_target(class_id, function_name); dispatch_table_entryt root_function; @@ -402,7 +403,7 @@ void remove_virtual_functionst::get_functions( root_function.class_id=resolved_call.get_class_identifier(); const symbolt &called_symbol = - symbol_table.lookup_ref(resolved_call.get_virtual_method_name()); + symbol_table.lookup_ref(resolved_call.get_full_component_identifier()); root_function.symbol_expr=called_symbol.symbol_expr(); root_function.symbol_expr.set( @@ -454,7 +455,7 @@ exprt remove_virtual_functionst::get_method( const irep_idt &component_name) const { const irep_idt &id= - resolve_concrete_function_callt::build_virtual_method_name( + resolve_inherited_componentt::build_full_component_identifier( class_id, component_name); const symbolt *symbol; diff --git a/src/goto-programs/resolve_concrete_function_call.cpp b/src/goto-programs/resolve_concrete_function_call.cpp deleted file mode 100644 index 117ebfb5963..00000000000 --- a/src/goto-programs/resolve_concrete_function_call.cpp +++ /dev/null @@ -1,102 +0,0 @@ -/*******************************************************************\ - - Module: GOTO Program Utilities - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include - -#include "resolve_concrete_function_call.h" - -/// See the operator() method comment. -/// \param symbol_table: The symbol table to resolve the function call in -resolve_concrete_function_callt::resolve_concrete_function_callt( - const symbol_tablet &symbol_table): - symbol_table(symbol_table) -{ - class_hierarchy(symbol_table); -} - -/// See the operator() method comment -/// \param symbol_table: The symbol table to resolve the function call in -/// \param class_hierarchy: A prebuilt class_hierachy based on the symbol_table -/// -resolve_concrete_function_callt::resolve_concrete_function_callt( - const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy): - class_hierarchy(class_hierarchy), - symbol_table(symbol_table) -{ - // We require the class_hierarchy to be already populated if we are being - // supplied it. - PRECONDITION(!class_hierarchy.class_map.empty()); -} - -/// Given a virtual function call, identify what concrete call this would be -/// resolved to. For example, calling a method on a class will call its -/// implementions if it exists, else will call the first parent that provides an -/// implementation. If none are found, an empty string will be returned. -/// \param class_id: The name of the class the function is being called on -/// \param component_name: The base name of the function (e.g. without the -/// class specifier -/// \return The concrete call that has been resolved -resolve_concrete_function_callt::concrete_function_callt - resolve_concrete_function_callt::operator()( - const irep_idt &class_id, const irep_idt &component_name) -{ - PRECONDITION(!class_id.empty()); - PRECONDITION(!component_name.empty()); - - irep_idt current_class=class_id; - while(!current_class.empty()) - { - const irep_idt &virtual_method_name= - build_virtual_method_name(current_class, component_name); - - if(symbol_table.has_symbol(virtual_method_name)) - { - return concrete_function_callt(current_class, component_name); - } - - const class_hierarchyt::idst &parents= - class_hierarchy.class_map[current_class].parents; - - if(parents.empty()) - break; - current_class=parents.front(); - } - - return concrete_function_callt(); -} - -/// Build a method name as found in a GOTO symbol table equivalent to the name -/// of a concrete call of method component_method_name on class class_name -/// \param component_method_name: The name of the function -/// \param class_name: The class the implementation would be found on. -/// \return A name for looking up in the symbol table for classes `class_name`'s -/// implementation of `component_name` -irep_idt resolve_concrete_function_callt::build_virtual_method_name( - const irep_idt &class_name, const irep_idt &component_method_name) -{ - // Verify the parameters are called in the correct order. - PRECONDITION(id2string(class_name).find("::")!=std::string::npos); - PRECONDITION(id2string(component_method_name).find("(")!=std::string::npos); - return id2string(class_name)+'.'+id2string(component_method_name); -} - -/// Get the full name of this function -/// \return The symbol name for this function call -irep_idt resolve_concrete_function_callt::concrete_function_callt:: - get_virtual_method_name() const -{ - return resolve_concrete_function_callt::build_virtual_method_name( - class_identifier, function_identifier); -} - -/// Use to check if this concrete_function_callt has been fully constructed. -/// \return True if this represents a real concrete function call -bool resolve_concrete_function_callt::concrete_function_callt::is_valid() const -{ - return !class_identifier.empty(); -} diff --git a/src/goto-programs/resolve_concrete_function_call.h b/src/goto-programs/resolve_concrete_function_call.h deleted file mode 100644 index c739e9b7393..00000000000 --- a/src/goto-programs/resolve_concrete_function_call.h +++ /dev/null @@ -1,75 +0,0 @@ -/*******************************************************************\ - - Module: GOTO Program Utilities - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -/// \file -/// Given a virtual function call on a specific class, find which implementation -/// needs to be used. - -#ifndef CPROVER_GOTO_PROGRAMS_RESOLVE_CONCRETE_FUNCTION_CALL_H -#define CPROVER_GOTO_PROGRAMS_RESOLVE_CONCRETE_FUNCTION_CALL_H - -#include -#include -#include -#include - -class resolve_concrete_function_callt -{ -public: - explicit resolve_concrete_function_callt(const symbol_tablet &symbol_table); - resolve_concrete_function_callt( - const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy); - - class concrete_function_callt - { - public: - concrete_function_callt() - {} - - concrete_function_callt( - const irep_idt &class_id, const irep_idt &method_id): - class_identifier(class_id), - function_identifier(method_id) - {} - - irep_idt get_virtual_method_name() const; - - irep_idt get_class_identifier() const - { - return class_identifier; - } - - irep_idt get_function_identifier() const - { - return function_identifier; - } - - bool is_valid() const; - - private: - irep_idt class_identifier; - irep_idt function_identifier; - }; - - concrete_function_callt operator()( - const irep_idt &class_id, const irep_idt &component_name); - - static irep_idt build_virtual_method_name( - const irep_idt &class_name, const irep_idt &component_method_name); - -private: - bool does_implementation_exist( - const irep_idt &class_name, - const irep_idt &component_method_name, - const irep_idt &calling_class_name); - - class_hierarchyt class_hierarchy; - const symbol_tablet &symbol_table; -}; - -#endif // CPROVER_GOTO_PROGRAMS_RESOLVE_CONCRETE_FUNCTION_CALL_H diff --git a/src/goto-programs/resolve_inherited_component.cpp b/src/goto-programs/resolve_inherited_component.cpp new file mode 100644 index 00000000000..c06e7d20bcf --- /dev/null +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -0,0 +1,102 @@ +/*******************************************************************\ + + Module: GOTO Program Utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include "resolve_inherited_component.h" + +/// See the operator() method comment. +/// \param symbol_table: The symbol table to resolve the component against +resolve_inherited_componentt::resolve_inherited_componentt( + const symbol_tablet &symbol_table): + symbol_table(symbol_table) +{ + class_hierarchy(symbol_table); +} + +/// See the operator() method comment +/// \param symbol_table: The symbol table to resolve the component against +/// \param class_hierarchy: A prebuilt class_hierachy based on the symbol_table +/// +resolve_inherited_componentt::resolve_inherited_componentt( + const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy): + class_hierarchy(class_hierarchy), + symbol_table(symbol_table) +{ + // We require the class_hierarchy to be already populated if we are being + // supplied it. + PRECONDITION(!class_hierarchy.class_map.empty()); +} + +/// Given a class and a component, identify the concrete field or method it is +/// resolved to. For example, a reference Child.abc refers to Child's method or +/// field if it exists, or else Parent.abc, and so on regarding Parent's +/// ancestors. If none are found, an empty string will be returned. +/// \param class_id: The name of the class the function is being called on +/// \param component_name: The base name of the component (i.e. without the +/// class specifier) +/// \return The concrete component that has been resolved +resolve_inherited_componentt::inherited_componentt + resolve_inherited_componentt::operator()( + const irep_idt &class_id, const irep_idt &component_name) +{ + PRECONDITION(!class_id.empty()); + PRECONDITION(!component_name.empty()); + + irep_idt current_class=class_id; + while(!current_class.empty()) + { + const irep_idt &full_component_identifier= + build_full_component_identifier(current_class, component_name); + + if(symbol_table.has_symbol(full_component_identifier)) + { + return inherited_componentt(current_class, component_name); + } + + const class_hierarchyt::idst &parents= + class_hierarchy.class_map[current_class].parents; + + if(parents.empty()) + break; + current_class=parents.front(); + } + + return inherited_componentt(); +} + +/// Build a component name as found in a GOTO symbol table equivalent to the +/// name of a concrete component component_name on class class_name +/// \param component_name: The name of the component +/// \param class_name: The class the implementation would be found on. +/// \return A name for looking up in the symbol table for classes `class_name`'s +/// component `component_name` +irep_idt resolve_inherited_componentt::build_full_component_identifier( + const irep_idt &class_name, const irep_idt &component_name) +{ + // Verify the parameters are called in the correct order. + PRECONDITION(id2string(class_name).find("::")!=std::string::npos); + PRECONDITION(id2string(component_name).find("::")==std::string::npos); + return id2string(class_name)+'.'+id2string(component_name); +} + +/// Get the full name of this function +/// \return The symbol name for this function call +irep_idt resolve_inherited_componentt::inherited_componentt:: + get_full_component_identifier() const +{ + return resolve_inherited_componentt::build_full_component_identifier( + class_identifier, component_identifier); +} + +/// Use to check if this inherited_componentt has been fully constructed. +/// \return True if this represents a real concrete component +bool resolve_inherited_componentt::inherited_componentt::is_valid() const +{ + return !class_identifier.empty(); +} diff --git a/src/goto-programs/resolve_inherited_component.h b/src/goto-programs/resolve_inherited_component.h new file mode 100644 index 00000000000..c87fed6933b --- /dev/null +++ b/src/goto-programs/resolve_inherited_component.h @@ -0,0 +1,75 @@ +/*******************************************************************\ + + Module: GOTO Program Utilities + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Given a class and a component (either field or method), find the closest +/// parent that defines that component. + +#ifndef CPROVER_GOTO_PROGRAMS_RESOLVE_INHERITED_COMPONENT_H +#define CPROVER_GOTO_PROGRAMS_RESOLVE_INHERITED_COMPONENT_H + +#include +#include +#include +#include + +class resolve_inherited_componentt +{ +public: + explicit resolve_inherited_componentt(const symbol_tablet &symbol_table); + resolve_inherited_componentt( + const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy); + + class inherited_componentt + { + public: + inherited_componentt() + {} + + inherited_componentt( + const irep_idt &class_id, const irep_idt &component_id): + class_identifier(class_id), + component_identifier(component_id) + {} + + irep_idt get_full_component_identifier() const; + + irep_idt get_class_identifier() const + { + return class_identifier; + } + + irep_idt get_component_basename() const + { + return component_identifier; + } + + bool is_valid() const; + + private: + irep_idt class_identifier; + irep_idt component_identifier; + }; + + inherited_componentt operator()( + const irep_idt &class_id, const irep_idt &component_name); + + static irep_idt build_full_component_identifier( + const irep_idt &class_name, const irep_idt &component_name); + +private: + bool does_implementation_exist( + const irep_idt &class_name, + const irep_idt &component_name, + const irep_idt &user_class_name); + + class_hierarchyt class_hierarchy; + const symbol_tablet &symbol_table; +}; + +#endif // CPROVER_GOTO_PROGRAMS_RESOLVE_INHERITED_COMPONENT_H diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 8ce9b93dd35..a8e21ee52bf 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -13,7 +13,7 @@ #include #include -#include +#include #include /// Constructor for lazy-method loading @@ -568,12 +568,12 @@ irep_idt ci_lazy_methodst::get_virtual_method_target( if(!needed_classes.count(classname)) return irep_idt(); - resolve_concrete_function_callt call_resolver(symbol_table, class_hierarchy); - const resolve_concrete_function_callt ::concrete_function_callt & - resolved_call=call_resolver(classname, call_basename); + resolve_inherited_componentt call_resolver(symbol_table, class_hierarchy); + const resolve_inherited_componentt::inherited_componentt resolved_call = + call_resolver(classname, call_basename); if(resolved_call.is_valid()) - return resolved_call.get_virtual_method_name(); + return resolved_call.get_full_component_identifier(); else return irep_idt(); } diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index ec771081f2f..de35b4e066c 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -36,7 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include +#include #include #include @@ -2806,9 +2806,9 @@ void java_bytecode_convert_method( bool java_bytecode_convert_methodt::is_method_inherited( const irep_idt &classname, const irep_idt &methodid) const { - resolve_concrete_function_callt call_resolver(symbol_table); - const resolve_concrete_function_callt ::concrete_function_callt & - resolved_call=call_resolver(classname, methodid); + resolve_inherited_componentt call_resolver(symbol_table); + const resolve_inherited_componentt::inherited_componentt resolved_call = + call_resolver(classname, methodid); // resolved_call is a pair (class-name, method-name) found by walking the // chain of class inheritance (not interfaces!) and stopping on the first @@ -2817,7 +2817,7 @@ bool java_bytecode_convert_methodt::is_method_inherited( if(resolved_call.is_valid()) { const symbolt &function_symbol= - *symbol_table.lookup(resolved_call.get_virtual_method_name()); + *symbol_table.lookup(resolved_call.get_full_component_identifier()); INVARIANT(function_symbol.type.id()==ID_code, "Function must be code"); From 168c2a896641fa48d4e3833a4db273eed505cdb5 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 15:26:43 +0000 Subject: [PATCH 02/14] Generalise get_inherited_method This can now resolve fields too, and is moved into java_utils so it can be used more widely. --- .../java_bytecode_convert_method.cpp | 52 +----------- src/java_bytecode/java_utils.cpp | 79 +++++++++++++++++++ src/java_bytecode/java_utils.h | 8 ++ 3 files changed, 90 insertions(+), 49 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index de35b4e066c..0868c1739a8 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2806,55 +2806,9 @@ void java_bytecode_convert_method( bool java_bytecode_convert_methodt::is_method_inherited( const irep_idt &classname, const irep_idt &methodid) const { - resolve_inherited_componentt call_resolver(symbol_table); - const resolve_inherited_componentt::inherited_componentt resolved_call = - call_resolver(classname, methodid); - - // resolved_call is a pair (class-name, method-name) found by walking the - // chain of class inheritance (not interfaces!) and stopping on the first - // class that contains a method of equal name and type to `methodid` - - if(resolved_call.is_valid()) - { - const symbolt &function_symbol= - *symbol_table.lookup(resolved_call.get_full_component_identifier()); - - INVARIANT(function_symbol.type.id()==ID_code, "Function must be code"); - - const auto &access=function_symbol.type.get(ID_access); - if(access==ID_public || access==ID_protected) - { - // since the method is public, it is a public method of `classname`, it is - // inherited - return true; - } - - // methods with the default access modifier are only - // accessible within the same package. - if(access==ID_default) - { - const std::string &class_package= - java_class_to_package(id2string(classname)); - const std::string &method_package= - java_class_to_package(id2string(resolved_call.get_class_identifier())); - return method_package==class_package; - } - - if(access==ID_private) - { - // We return false because the method found by the call_resolver above - // proves that `methodid` cannot be inherited (assuming that the original - // Java code compiles). This is because, as we walk the inheritance chain - // for `classname` from Object to `classname`, a method can only become - // "more accessible". So, if the last occurrence is private, all others - // before must be private as well, and none is inherited in `classname`. - return false; - } - - INVARIANT(false, "Unexpected access modifier."); - } - - return false; + resolve_inherited_componentt::inherited_componentt inherited_method = + get_inherited_component(classname, methodid, classname, symbol_table); + return inherited_method.is_valid(); } /// create temporary variables if a write instruction can have undesired side- diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 0021bff9325..1f95509ac68 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -325,3 +325,82 @@ std::string pretty_print_java_type(const std::string &fqn_java_type) result = result.substr(java_lang_string.length()); return result; } + +/// Finds an inherited component (method or field), taking component visibility +/// into account. +/// \param component_class_id: class to start searching from. For example, if +/// trying to resolve a reference to A.b, component_class_id is "A". +/// \param component_name: component basename to search for. If searching for +/// A.b, this is "b". +/// \param user_class_id: class identifier making reference to the sought +/// component. The user class is relevant when determining whether package- +/// scoped components are visible from a particular use site. +/// \param symbol_table: global symbol table. +/// \return the concrete component referred to if any is found, or an invalid +/// resolve_inherited_componentt::inherited_componentt otherwise. +resolve_inherited_componentt::inherited_componentt get_inherited_component( + const irep_idt &component_class_id, + const irep_idt &component_name, + const irep_idt &user_class_id, + const symbol_tablet &symbol_table) +{ + resolve_inherited_componentt component_resolver(symbol_table); + const resolve_inherited_componentt::inherited_componentt resolved_component = + component_resolver(component_class_id, component_name); + + // resolved_component is a pair (class-name, component-name) found by walking + // the chain of class inheritance (not interfaces!) and stopping on the first + // class that contains a component of equal name and type to `component_name` + + if(resolved_component.is_valid()) + { + // Directly defined on the class referred to? + if(component_class_id == resolved_component.get_class_identifier()) + return resolved_component; + + // No, may be inherited from some parent class; check it is visible: + const symbolt &component_symbol= + *symbol_table.lookup(resolved_component.get_full_component_identifier()); + + const auto &access=component_symbol.type.get(ID_access); + if(access==ID_public || access==ID_protected) + { + // since the component is public, it is inherited + return resolved_component; + } + + // components with the default access modifier are only + // accessible within the same package. + if(access==ID_default) + { + const std::string &class_package= + java_class_to_package(id2string(component_class_id)); + const std::string &component_package= + java_class_to_package( + id2string( + resolved_component.get_class_identifier())); + if(component_package == class_package) + return resolved_component; + else + return resolve_inherited_componentt::inherited_componentt(); + } + + if(access==ID_private) + { + // We return not-found because the component found by the + // component_resolver above proves that `component_name` cannot be + // inherited (assuming that the original Java code compiles). This is + // because, as we walk the inheritance chain for `classname` from Object + // to `classname`, a component can only become "more accessible". So, if + // the last occurrence is private, all others before must be private as + // well, and none is inherited in `classname`. + return resolve_inherited_componentt::inherited_componentt(); + } + + UNREACHABLE; // Unexpected access modifier + } + else + { + return resolve_inherited_componentt::inherited_componentt(); + } +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index ad4c45f51c0..e30618f57b8 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + bool java_is_array_type(const typet &type); void generate_class_stub( @@ -96,4 +98,10 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip); std::string pretty_print_java_type(const std::string &fqn_java_type); +resolve_inherited_componentt::inherited_componentt get_inherited_component( + const irep_idt &component_class_id, + const irep_idt &component_name, + const irep_idt &user_class_id, + const symbol_tablet &symbol_table); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H From bea6371d3657a466daefbbd016869d8b40ce02fc Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 15:58:20 +0000 Subject: [PATCH 03/14] Annotate static fields with accessibility This mirrors the annotation already present on methods, and is needed to resolve indirect reference to an inherited static field, similar to virtual call resolution. The access attribute is set as a comment so that in an assignment some_static_field = some_constant we don't need to attach spurious access tags to the constant, or scrub them from the field, for their types to be considered matching. --- src/java_bytecode/java_bytecode_convert_class.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 12b87375e77..16126efb32f 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -391,6 +391,20 @@ void java_bytecode_convert_classt::convert( "."+id2string(f.name); new_symbol.mode=ID_java; new_symbol.is_type=false; + + // These annotations use `ID_C_access` instead of `ID_access` like methods + // to avoid type clashes in expressions like `some_static_field = 0`, where + // with ID_access the constant '0' would need to have an access modifier + // too, or else appear to have incompatible type. + if(f.is_public) + new_symbol.type.set(ID_C_access, ID_public); + else if(f.is_protected) + new_symbol.type.set(ID_C_access, ID_protected); + else if(f.is_private) + new_symbol.type.set(ID_C_access, ID_private); + else + new_symbol.type.set(ID_C_access, ID_default); + const namespacet ns(symbol_table); new_symbol.value= zero_initializer( From e73e756f122c77376999a04a68ed35638e8f1855 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 15:43:14 +0000 Subject: [PATCH 04/14] Create stub globals: check for inherited globals Bytecode can refer to a static field via a child class; for example, referring to B.f when the actual referee field is A.f, where B extends A. By missing this case we could previously accidentally create a stub global for (in this example) B.f. --- src/java_bytecode/java_bytecode_language.cpp | 12 ++++++++++-- src/java_bytecode/java_utils.cpp | 5 ++++- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index b63d5923e5f..e96433104e5 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -448,10 +448,18 @@ static void create_stub_global_symbols( irep_idt class_id = instruction.args[0].get_string(ID_class); INVARIANT( !class_id.empty(), "get/putstatic should specify a class"); - irep_idt identifier = id2string(class_id) + "." + id2string(component); - if(!symbol_table.has_symbol(identifier)) + resolve_inherited_componentt::inherited_componentt referred_component = + get_inherited_component( + class_id, + component, + "java::" + id2string(parse_tree.parsed_class.name), + symbol_table); + if(!referred_component.is_valid()) { + irep_idt identifier = + id2string(class_id) + "." + id2string(component); + create_stub_global_symbol( symbol_table, identifier, diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 1f95509ac68..a8c94480558 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -362,7 +362,10 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( const symbolt &component_symbol= *symbol_table.lookup(resolved_component.get_full_component_identifier()); - const auto &access=component_symbol.type.get(ID_access); + irep_idt access = component_symbol.type.get(ID_access); + if(access.empty()) + access = component_symbol.type.get(ID_C_access); + if(access==ID_public || access==ID_protected) { // since the component is public, it is inherited From 5b3cde578fda4068f36cf793c25e3ebd6dc23211 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 16:28:19 +0000 Subject: [PATCH 05/14] Use a common instance of class_hierarchyt in get_inherited_component This avoids constructing a fresh class_hierarchyt with a consequent sweep of the complete symbol table every time inheritence is queried. --- .../java_bytecode_convert_method.cpp | 18 ++++++++++++++---- .../java_bytecode_convert_method.h | 3 ++- .../java_bytecode_convert_method_class.h | 7 +++++-- src/java_bytecode/java_bytecode_language.cpp | 17 +++++++++++++---- src/java_bytecode/java_bytecode_language.h | 1 + src/java_bytecode/java_utils.cpp | 7 +++++-- src/java_bytecode/java_utils.h | 3 ++- 7 files changed, 42 insertions(+), 14 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 0868c1739a8..81911e46425 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2764,7 +2764,8 @@ void java_bytecode_convert_method( message_handlert &message_handler, size_t max_array_length, optionalt needed_lazy_methods, - java_string_library_preprocesst &string_preprocess) + java_string_library_preprocesst &string_preprocess, + const class_hierarchyt &class_hierarchy) { static const std::unordered_set methods_to_ignore { @@ -2795,7 +2796,8 @@ void java_bytecode_convert_method( message_handler, max_array_length, needed_lazy_methods, - string_preprocess); + string_preprocess, + class_hierarchy); java_bytecode_convert_method(class_symbol, method); } @@ -2803,11 +2805,19 @@ void java_bytecode_convert_method( /// Returns true iff method \p methodid from class \p classname is /// a method inherited from a class (and not an interface!) from which /// \p classname inherits, either directly or indirectly. +/// \param classname: class whose method is referenced +/// \param methodid: method basename bool java_bytecode_convert_methodt::is_method_inherited( - const irep_idt &classname, const irep_idt &methodid) const + const irep_idt &classname, + const irep_idt &methodid) const { resolve_inherited_componentt::inherited_componentt inherited_method = - get_inherited_component(classname, methodid, classname, symbol_table); + get_inherited_component( + classname, + methodid, + classname, + symbol_table, + class_hierarchy); return inherited_method.is_valid(); } diff --git a/src/java_bytecode/java_bytecode_convert_method.h b/src/java_bytecode/java_bytecode_convert_method.h index b27fd1cf898..90e76f501f9 100644 --- a/src/java_bytecode/java_bytecode_convert_method.h +++ b/src/java_bytecode/java_bytecode_convert_method.h @@ -34,7 +34,8 @@ void java_bytecode_convert_method( message_handlert &message_handler, size_t max_array_length, optionalt needed_lazy_methods, - java_string_library_preprocesst &string_preprocess); + java_string_library_preprocesst &string_preprocess, + const class_hierarchyt &class_hierarchy); void java_bytecode_convert_method_lazy( const symbolt &class_symbol, diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index fbcf46cedb8..d0547d98617 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -35,14 +35,16 @@ class java_bytecode_convert_methodt:public messaget message_handlert &_message_handler, size_t _max_array_length, optionalt needed_lazy_methods, - java_string_library_preprocesst &_string_preprocess) + java_string_library_preprocesst &_string_preprocess, + const class_hierarchyt &class_hierarchy) : messaget(_message_handler), symbol_table(symbol_table), max_array_length(_max_array_length), needed_lazy_methods(std::move(needed_lazy_methods)), string_preprocess(_string_preprocess), slots_for_parameters(0), - method_has_this(false) + method_has_this(false), + class_hierarchy(class_hierarchy) { } @@ -116,6 +118,7 @@ class java_bytecode_convert_methodt:public messaget bool method_has_this; std::map class_has_clinit_method; std::map any_superclass_has_clinit_method; + class_hierarchyt class_hierarchy; enum instruction_sizet { diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index e96433104e5..2ab522d4e3b 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -426,9 +426,11 @@ static void create_stub_global_symbol( /// static fields, and nondet-initialised for primitives. /// \param parse_tree: class bytecode /// \param symbol_table: symbol table; may gain new symbols +/// \param class_hierarchy: global class hierarchy static void create_stub_global_symbols( const java_bytecode_parse_treet &parse_tree, - symbol_table_baset &symbol_table) + symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy) { namespacet ns(symbol_table); for(const auto &method : parse_tree.parsed_class.methods) @@ -454,7 +456,8 @@ static void create_stub_global_symbols( class_id, component, "java::" + id2string(parse_tree.parsed_class.name), - symbol_table); + symbol_table, + class_hierarchy); if(!referred_component.is_valid()) { irep_idt identifier = @@ -523,6 +526,10 @@ bool java_bytecode_languaget::typecheck( return true; } + // Now that all classes have been created in the symbol table we can populate + // the class hierarchy: + class_hierarchy(symbol_table); + // find and mark all implicitly generic class types // this can only be done once all the class symbols have been created for(const auto &c : java_class_loader.class_map) @@ -582,7 +589,8 @@ bool java_bytecode_languaget::typecheck( journalling_symbol_tablet::wrap(symbol_table); for(const auto &c : java_class_loader.class_map) { - create_stub_global_symbols(c.second, symbol_table_journal); + create_stub_global_symbols( + c.second, symbol_table_journal, class_hierarchy); } stub_global_initializer_factory.create_stub_global_initializer_symbols( @@ -875,7 +883,8 @@ bool java_bytecode_languaget::convert_single_method( get_message_handler(), max_user_array_length, std::move(needed_lazy_methods), - string_preprocess); + string_preprocess, + class_hierarchy); return false; } diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index e75fb39dc31..dc708eef744 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -174,6 +174,7 @@ class java_bytecode_languaget:public languaget const std::unique_ptr pointer_type_selector; synthetic_methods_mapt synthetic_methods; stub_global_initializer_factoryt stub_global_initializer_factory; + class_hierarchyt class_hierarchy; }; std::unique_ptr new_java_bytecode_language(); diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index a8c94480558..ad18ed4caea 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -336,15 +336,18 @@ std::string pretty_print_java_type(const std::string &fqn_java_type) /// component. The user class is relevant when determining whether package- /// scoped components are visible from a particular use site. /// \param symbol_table: global symbol table. +/// \param class_hierarchy: global class hierarchy. /// \return the concrete component referred to if any is found, or an invalid /// resolve_inherited_componentt::inherited_componentt otherwise. resolve_inherited_componentt::inherited_componentt get_inherited_component( const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, - const symbol_tablet &symbol_table) + const symbol_tablet &symbol_table, + const class_hierarchyt &class_hierarchy) { - resolve_inherited_componentt component_resolver(symbol_table); + resolve_inherited_componentt component_resolver( + symbol_table, class_hierarchy); const resolve_inherited_componentt::inherited_componentt resolved_component = component_resolver(component_class_id, component_name); diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index e30618f57b8..6b069f83475 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -102,6 +102,7 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, - const symbol_tablet &symbol_table); + const symbol_tablet &symbol_table, + const class_hierarchyt &class_hierarchy); #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H From 045ac0538fda1b02b783521d761bdc76bb50a0c3 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 16:38:46 +0000 Subject: [PATCH 06/14] Create stub globals on the first parent incomplete class Previously if a reference to static field A.x did not resolve, then A.x would be created as a stub, but this is inappropriate if A is a complete (non-stub) class. Instead, create the field on A's first ancestor that is incomplete. --- src/java_bytecode/java_bytecode_language.cpp | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 2ab522d4e3b..8e7a678ad0c 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -460,15 +460,29 @@ static void create_stub_global_symbols( class_hierarchy); if(!referred_component.is_valid()) { + // Create a new stub global on the first incomplete (stub) parent of + // the class that was referred to: + irep_idt add_to_class_id = class_id; + while(!symbol_table.lookup_ref(add_to_class_id).type.get_bool( + ID_incomplete_class)) + { + const class_hierarchyt::idst &parents = + class_hierarchy.class_map.at(add_to_class_id).parents; + INVARIANT( + !parents.empty(), + "unresolved global reference should come from incomplete class"); + add_to_class_id = parents[0]; + } + irep_idt identifier = - id2string(class_id) + "." + id2string(component); + id2string(add_to_class_id) + "." + id2string(component); create_stub_global_symbol( symbol_table, identifier, component, instruction.args[0].type(), - class_id); + add_to_class_id); } } } From b2d3d61f7b61845305bc67c9b417d68dee1c0fbf Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 17:00:17 +0000 Subject: [PATCH 07/14] Search static fields inherited from interfaces Previously we assumed that static fields, like regular fields, could only be inherited from ordinary classes, but in fact they can also come from interfaces. We therefore augment resolve-inherited-component to optionally search in all ancestors including interfaces, and use that facility when searching for inherited static fields. --- .../remove_virtual_functions.cpp | 4 +-- .../resolve_inherited_component.cpp | 27 ++++++++++++++----- .../resolve_inherited_component.h | 4 ++- src/java_bytecode/ci_lazy_methods.cpp | 2 +- .../java_bytecode_convert_method.cpp | 3 ++- src/java_bytecode/java_bytecode_language.cpp | 5 +++- src/java_bytecode/java_utils.cpp | 7 +++-- src/java_bytecode/java_utils.h | 3 ++- 8 files changed, 40 insertions(+), 15 deletions(-) diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index 041f8382f1c..7028d0550ce 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -390,11 +390,11 @@ void remove_virtual_functionst::get_functions( const function_call_resolvert resolve_function_call = [&get_virtual_call_target]( const irep_idt &class_id, const irep_idt &function_name) { - return get_virtual_call_target(class_id, function_name); + return get_virtual_call_target(class_id, function_name, false); }; const resolve_inherited_componentt::inherited_componentt - &resolved_call = get_virtual_call_target(class_id, function_name); + &resolved_call = get_virtual_call_target(class_id, function_name, false); dispatch_table_entryt root_function; diff --git a/src/goto-programs/resolve_inherited_component.cpp b/src/goto-programs/resolve_inherited_component.cpp index c06e7d20bcf..f408c112735 100644 --- a/src/goto-programs/resolve_inherited_component.cpp +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -40,17 +40,25 @@ resolve_inherited_componentt::resolve_inherited_componentt( /// \param class_id: The name of the class the function is being called on /// \param component_name: The base name of the component (i.e. without the /// class specifier) +/// \param include_interfaces: If true, consider inheritence from interfaces +/// (parent types other than the first listed) /// \return The concrete component that has been resolved resolve_inherited_componentt::inherited_componentt resolve_inherited_componentt::operator()( - const irep_idt &class_id, const irep_idt &component_name) + const irep_idt &class_id, + const irep_idt &component_name, + bool include_interfaces) { PRECONDITION(!class_id.empty()); PRECONDITION(!component_name.empty()); - irep_idt current_class=class_id; - while(!current_class.empty()) + std::vector classes_to_visit; + classes_to_visit.push_back(class_id); + while(!classes_to_visit.empty()) { + irep_idt current_class = classes_to_visit.back(); + classes_to_visit.pop_back(); + const irep_idt &full_component_identifier= build_full_component_identifier(current_class, component_name); @@ -62,9 +70,16 @@ resolve_inherited_componentt::inherited_componentt const class_hierarchyt::idst &parents= class_hierarchy.class_map[current_class].parents; - if(parents.empty()) - break; - current_class=parents.front(); + if(include_interfaces) + { + classes_to_visit.insert( + classes_to_visit.end(), parents.begin(), parents.end()); + } + else + { + if(!parents.empty()) + classes_to_visit.push_back(parents.front()); + } } return inherited_componentt(); diff --git a/src/goto-programs/resolve_inherited_component.h b/src/goto-programs/resolve_inherited_component.h index c87fed6933b..a6ac3b1eca0 100644 --- a/src/goto-programs/resolve_inherited_component.h +++ b/src/goto-programs/resolve_inherited_component.h @@ -57,7 +57,9 @@ class resolve_inherited_componentt }; inherited_componentt operator()( - const irep_idt &class_id, const irep_idt &component_name); + const irep_idt &class_id, + const irep_idt &component_name, + bool include_interfaces); static irep_idt build_full_component_identifier( const irep_idt &class_name, const irep_idt &component_name); diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index a8e21ee52bf..51f746a286b 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -570,7 +570,7 @@ irep_idt ci_lazy_methodst::get_virtual_method_target( resolve_inherited_componentt call_resolver(symbol_table, class_hierarchy); const resolve_inherited_componentt::inherited_componentt resolved_call = - call_resolver(classname, call_basename); + call_resolver(classname, call_basename, false); if(resolved_call.is_valid()) return resolved_call.get_full_component_identifier(); diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 81911e46425..81080b68e69 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2817,7 +2817,8 @@ bool java_bytecode_convert_methodt::is_method_inherited( methodid, classname, symbol_table, - class_hierarchy); + class_hierarchy, + false); return inherited_method.is_valid(); } diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 8e7a678ad0c..014344c9c71 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -451,13 +451,16 @@ static void create_stub_global_symbols( INVARIANT( !class_id.empty(), "get/putstatic should specify a class"); + // The final 'true' parameter here includes interfaces, as they can + // define static fields. resolve_inherited_componentt::inherited_componentt referred_component = get_inherited_component( class_id, component, "java::" + id2string(parse_tree.parsed_class.name), symbol_table, - class_hierarchy); + class_hierarchy, + true); if(!referred_component.is_valid()) { // Create a new stub global on the first incomplete (stub) parent of diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index ad18ed4caea..ada0934367c 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -337,6 +337,8 @@ std::string pretty_print_java_type(const std::string &fqn_java_type) /// scoped components are visible from a particular use site. /// \param symbol_table: global symbol table. /// \param class_hierarchy: global class hierarchy. +/// \param include_interfaces: if true, search for the given component in all +/// ancestors including interfaces, rather than just parents. /// \return the concrete component referred to if any is found, or an invalid /// resolve_inherited_componentt::inherited_componentt otherwise. resolve_inherited_componentt::inherited_componentt get_inherited_component( @@ -344,12 +346,13 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( const irep_idt &component_name, const irep_idt &user_class_id, const symbol_tablet &symbol_table, - const class_hierarchyt &class_hierarchy) + const class_hierarchyt &class_hierarchy, + bool include_interfaces) { resolve_inherited_componentt component_resolver( symbol_table, class_hierarchy); const resolve_inherited_componentt::inherited_componentt resolved_component = - component_resolver(component_class_id, component_name); + component_resolver(component_class_id, component_name, include_interfaces); // resolved_component is a pair (class-name, component-name) found by walking // the chain of class inheritance (not interfaces!) and stopping on the first diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 6b069f83475..93ec538dda4 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -103,6 +103,7 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( const irep_idt &component_name, const irep_idt &user_class_id, const symbol_tablet &symbol_table, - const class_hierarchyt &class_hierarchy); + const class_hierarchyt &class_hierarchy, + bool include_interfaces); #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H From 32cc538a6fa23cc2c46d7bd50979f9d5c80c70f6 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 17:11:58 +0000 Subject: [PATCH 08/14] Insert stub static globals onto any incomplete ancestor class Previously they were always created on either the class that was referred to, or on some parent or grandparent; however, this was inappropriate if all those classes were concrete (non-stub) types but some interface *was* a stub. In that case an interface will be arbitrarily picked and given a stub field. --- src/java_bytecode/java_bytecode_language.cpp | 52 +++++++++++++++----- 1 file changed, 39 insertions(+), 13 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 014344c9c71..3e4ec399cfc 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -420,6 +420,39 @@ static void create_stub_global_symbol( !add_failed, "caller should have checked symbol not already in table"); } +/// Find any incomplete ancestor of a given class +/// \param start_class_id: class to start searching from +/// \param symbol_table: global symbol table +/// \param class_hierarchy: global class hierarchy +/// \return first incomplete ancestor encountered, +/// including start_class_id itself. +static irep_idt get_any_incomplete_ancestor( + const irep_idt &start_class_id, + const symbol_tablet &symbol_table, + const class_hierarchyt &class_hierarchy) +{ + // Depth-first search: return the first ancestor with ID_incomplete_class, or + // irep_idt() if none found. + std::vector classes_to_check; + classes_to_check.push_back(start_class_id); + + while(!classes_to_check.empty()) + { + irep_idt to_check = classes_to_check.back(); + classes_to_check.pop_back(); + + if(symbol_table.lookup_ref(to_check).type.get_bool(ID_incomplete_class)) + return to_check; + + const class_hierarchyt::idst &parents = + class_hierarchy.class_map.at(to_check).parents; + classes_to_check.insert( + classes_to_check.end(), parents.begin(), parents.end()); + } + + INVARIANT(false, "input class id should have some incomplete ancestor"); +} + /// Search for getstatic and putstatic instructions in a class' bytecode and /// create stub symbols for any static fields that aren't already in the symbol /// table. The new symbols are null-initialised for reference-typed globals / @@ -463,19 +496,12 @@ static void create_stub_global_symbols( true); if(!referred_component.is_valid()) { - // Create a new stub global on the first incomplete (stub) parent of - // the class that was referred to: - irep_idt add_to_class_id = class_id; - while(!symbol_table.lookup_ref(add_to_class_id).type.get_bool( - ID_incomplete_class)) - { - const class_hierarchyt::idst &parents = - class_hierarchy.class_map.at(add_to_class_id).parents; - INVARIANT( - !parents.empty(), - "unresolved global reference should come from incomplete class"); - add_to_class_id = parents[0]; - } + // Create a new stub global on an arbitrary incomplete ancestor of the + // class that was referred to. This is just a guess, but we have no + // better information to go on. + irep_idt add_to_class_id = + get_any_incomplete_ancestor( + class_id, symbol_table, class_hierarchy); irep_idt identifier = id2string(add_to_class_id) + "." + id2string(component); From d6783d85cbde396dd395b72815edaaca331daf49 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 17:45:41 +0000 Subject: [PATCH 09/14] Java method converter: look for inherited static fields Previously it assumed that static field references were resolved in the bytecode (e.g. that a reference to A.somefield meant that A defines somefield). However in fact they can be inherited, and especially now that stub fields can be created on parent classes they are likely to appear there. As such the "get/putstatic" instructions now search the class hierarchy for the field they actually refer to. --- .../java_bytecode_convert_method.cpp | 37 ++++++++++++++++++- .../java_bytecode_convert_method_class.h | 3 ++ 2 files changed, 38 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 81080b68e69..1af1c53260c 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1996,7 +1996,9 @@ codet java_bytecode_convert_methodt::convert_instructions( const auto &field_name=arg0.get_string(ID_component_name); const bool is_assertions_disabled_field= field_name.find("$assertionsDisabled")!=std::string::npos; - symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name); + + symbol_expr.set_identifier( + get_static_field(arg0.get_string(ID_class), field_name)); INVARIANT( symbol_table.has_symbol(symbol_expr.get_identifier()), @@ -2025,6 +2027,9 @@ codet java_bytecode_convert_methodt::convert_instructions( } results[0]=java_bytecode_promotion(symbol_expr); + // Note this initialiser call deliberately inits the class used to make + // the reference, which may be a child of the class that actually defines + // the field. codet clinit_call=get_clinit_call(arg0.get_string(ID_class)); if(clinit_call.get_statement()!=ID_skip) c=clinit_call; @@ -2052,7 +2057,8 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(op.size()==1 && results.empty()); symbol_exprt symbol_expr(arg0.type()); const auto &field_name=arg0.get_string(ID_component_name); - symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+field_name); + symbol_expr.set_identifier( + get_static_field(arg0.get_string(ID_class), field_name)); INVARIANT( symbol_table.has_symbol(symbol_expr.get_identifier()), @@ -2067,6 +2073,9 @@ codet java_bytecode_convert_methodt::convert_instructions( code_blockt block; block.add_source_location()=i_it->source_location; + // Note this initialiser call deliberately inits the class used to make + // the reference, which may be a child of the class that actually defines + // the field. codet clinit_call=get_clinit_call(arg0.get_string(ID_class)); if(clinit_call.get_statement()!=ID_skip) block.move_to_operands(clinit_call); @@ -2822,6 +2831,30 @@ bool java_bytecode_convert_methodt::is_method_inherited( return inherited_method.is_valid(); } +/// Get static field identifier referred to by `class_identifier.component_name` +/// Note this may be inherited from either a parent or an interface. +/// \param class_identifier: class used to refer to the field +/// \param component_name: component (static field) name +/// \return identifier of the actual concrete field referred to +irep_idt java_bytecode_convert_methodt::get_static_field( + const irep_idt &class_identifier, + const irep_idt &component_name) const +{ + resolve_inherited_componentt::inherited_componentt inherited_method = + get_inherited_component( + class_identifier, + component_name, + symbol_table.lookup_ref(current_method).type.get(ID_C_class), + symbol_table, + class_hierarchy, + true); + + INVARIANT( + inherited_method.is_valid(), "static field should be in symbol table"); + + return inherited_method.get_full_component_identifier(); +} + /// create temporary variables if a write instruction can have undesired side- /// effects void java_bytecode_convert_methodt::save_stack_entries( diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index d0547d98617..b7ea7d0748e 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -257,6 +257,9 @@ class java_bytecode_convert_methodt:public messaget const irep_idt &classname, const irep_idt &methodid) const; + irep_idt get_static_field( + const irep_idt &class_identifier, const irep_idt &component_name) const; + enum class bytecode_write_typet { VARIABLE, ARRAY_REF, STATIC_FIELD, FIELD}; void save_stack_entries( const std::string &, From 873e1f66780d85c49fa1bc156b4f128421e2a073 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 18:11:16 +0000 Subject: [PATCH 10/14] Guess public access for stub globals Any choice here is wrong (we can't know the global's actual visibility because we don't have the bytecode). I guess at public visibility on the hunch that actually- shared globals are somewhat more common than private ones with the same name and type. --- src/java_bytecode/java_bytecode_language.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 3e4ec399cfc..3e0424bbcc7 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -405,6 +405,10 @@ static void create_stub_global_symbol( new_symbol.base_name = symbol_basename; new_symbol.type = symbol_type; new_symbol.type.set(ID_C_class, 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. + new_symbol.type.set(ID_C_access, ID_public); new_symbol.pretty_name = new_symbol.name; new_symbol.mode = ID_java; new_symbol.is_type = false; From d4d4a9aa634ea4716e71f9474b8348bbfffa5685 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 13 Feb 2018 09:57:29 +0000 Subject: [PATCH 11/14] Tolerate stub static fields defined on non-stub types Normally this situation (a reference to static field A.x, when neither A nor any of its ancestors either define a field x or are opaque stubs) would be an error, probably indicating a class version mismatch, but at present some of our library models intentionally exploit this behaviour to obtain a nondet- initialised field. Therefore for the time being we tolerate the situation, initialising such fields in __CPROVER_initialize, as we cannot attach a synthetic clinit method to a non-stub type. --- src/java_bytecode/java_bytecode_language.cpp | 43 ++++++++++++++++--- src/java_bytecode/java_entry_point.cpp | 2 + .../java_static_initializers.cpp | 32 +++++++------- src/java_bytecode/java_static_initializers.h | 5 ++- src/java_bytecode/java_utils.cpp | 15 +++++++ src/java_bytecode/java_utils.h | 2 + 6 files changed, 76 insertions(+), 23 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 3e0424bbcc7..924df1aca6c 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -390,12 +390,17 @@ static void generate_constant_global_variables( /// \param symbol_basename: new symbol basename /// \param symbol_type: new symbol type /// \param class_id: class id that directly encloses this static field +/// \param force_nondet_init: if true, always leave the symbol's value nil so it +/// gets nondet initialised during __CPROVER_initialize. Otherwise, pointer- +/// typed globals are initialised null and we expect a synthetic clinit method +/// to be created later. static void create_stub_global_symbol( symbol_table_baset &symbol_table, const irep_idt &symbol_id, const irep_idt &symbol_basename, const typet &symbol_type, - const irep_idt &class_id) + const irep_idt &class_id, + bool force_nondet_init) { symbolt new_symbol; new_symbol.is_static_lifetime = true; @@ -415,7 +420,7 @@ static void create_stub_global_symbol( // If pointer-typed, initialise to null and a static initialiser will be // created to initialise on first reference. If primitive-typed, specify // nondeterministic initialisation by setting a nil value. - if(symbol_type.id() == ID_pointer) + if(symbol_type.id() == ID_pointer && !force_nondet_init) new_symbol.value = null_pointer_exprt(to_pointer_type(symbol_type)); else new_symbol.value.make_nil(); @@ -454,7 +459,7 @@ static irep_idt get_any_incomplete_ancestor( classes_to_check.end(), parents.begin(), parents.end()); } - INVARIANT(false, "input class id should have some incomplete ancestor"); + return irep_idt(); } /// Search for getstatic and putstatic instructions in a class' bytecode and @@ -464,10 +469,13 @@ static irep_idt get_any_incomplete_ancestor( /// \param parse_tree: class bytecode /// \param symbol_table: symbol table; may gain new symbols /// \param class_hierarchy: global class hierarchy +/// \param log: message handler used to log warnings when stub static fields are +/// found belonging to non-stub classes. static void create_stub_global_symbols( const java_bytecode_parse_treet &parse_tree, symbol_table_baset &symbol_table, - const class_hierarchyt &class_hierarchy) + const class_hierarchyt &class_hierarchy, + messaget &log) { namespacet ns(symbol_table); for(const auto &method : parse_tree.parsed_class.methods) @@ -507,6 +515,28 @@ static void create_stub_global_symbols( get_any_incomplete_ancestor( class_id, symbol_table, class_hierarchy); + // If there are no incomplete ancestors to ascribe the missing field + // to, we must have an incomplete model of a class or simply a + // version mismatch of some kind. Normally this would be an error, but + // our models library currently triggers this error in some cases + // (notably java.lang.System, which is missing System.in/out/err). + // Therefore for this case we ascribe the missing field to the class + // it was directly referenced from, and fall back to initialising the + // field in __CPROVER_initialize, rather than try to create or augment + // a clinit method for a non-stub class. + + bool no_incomplete_ancestors = add_to_class_id.empty(); + if(no_incomplete_ancestors) + { + add_to_class_id = class_id; + + // TODO forbid this again once the models library has been checked + // for missing static fields. + log.warning() << "Stub static field " << component << " found for " + << "non-stub type " << class_id << ". In future this " + << "will be a fatal error." << messaget::eom; + } + irep_idt identifier = id2string(add_to_class_id) + "." + id2string(component); @@ -515,7 +545,8 @@ static void create_stub_global_symbols( identifier, component, instruction.args[0].type(), - add_to_class_id); + add_to_class_id, + no_incomplete_ancestors); } } } @@ -637,7 +668,7 @@ bool java_bytecode_languaget::typecheck( for(const auto &c : java_class_loader.class_map) { create_stub_global_symbols( - c.second, symbol_table_journal, class_hierarchy); + c.second, symbol_table_journal, class_hierarchy, *this); } stub_global_initializer_factory.create_stub_global_initializer_symbols( diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 2f2242c4424..2bf4e8ec9e6 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -118,6 +118,8 @@ static void java_static_lifetime_init( allow_null=false; if(allow_null && is_java_string_literal_id(nameid)) allow_null=false; + if(allow_null && is_non_null_library_global(nameid)) + allow_null = false; } gen_nondet_init( sym.symbol_expr(), diff --git a/src/java_bytecode/java_static_initializers.cpp b/src/java_bytecode/java_static_initializers.cpp index 9246ef4cba5..b77ffc7bf61 100644 --- a/src/java_bytecode/java_static_initializers.cpp +++ b/src/java_bytecode/java_static_initializers.cpp @@ -8,6 +8,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com #include "java_static_initializers.h" #include "java_object_factory.h" +#include "java_utils.h" #include #include #include @@ -266,8 +267,20 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( // Populate map from class id -> stub globals: for(const irep_idt &stub_global : stub_globals_set) { + const symbolt &global_symbol = symbol_table.lookup_ref(stub_global); + if(global_symbol.value.is_nil()) + { + // This symbol is already nondet-initialised during __CPROVER_initialize + // (generated in java_static_lifetime_init). In future this will only + // be the case for primitive-typed fields, but for now reference-typed + // fields can also be treated this way in the exceptional case that they + // belong to a non-stub class. Skip the field, as it does not need a + // synthetic static initializer. + continue; + } + const irep_idt class_id = - symbol_table.lookup_ref(stub_global).type.get(ID_C_class); + global_symbol.type.get(ID_C_class); INVARIANT( !class_id.empty(), "static field should be annotated with its defining class"); @@ -283,6 +296,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( { const irep_idt static_init_name = clinit_function_name(it->first); + INVARIANT( + symbol_table.lookup_ref(it->first).type.get_bool(ID_incomplete_class), + "only incomplete classes should be given synthetic static initialisers"); INVARIANT( !symbol_table.has_symbol(static_init_name), "a class cannot be both incomplete, and so have stub static fields, and " @@ -315,20 +331,6 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols( } } -/// Check if a symbol is a well-known non-null global -/// \param symbolid: symbol id to check -/// \return true if this static field is known never to be null -static bool is_non_null_library_global(const irep_idt &symbolid) -{ - static const std::unordered_set non_null_globals = - { - "java::java.lang.System.out", - "java::java.lang.System.err", - "java::java.lang.System.in" - }; - return non_null_globals.count(symbolid); -} - /// Create the body of a synthetic static initializer (clinit method), /// which initialise stub globals in the same manner as /// java_static_lifetime_init, only delayed until first reference by virtue of diff --git a/src/java_bytecode/java_static_initializers.h b/src/java_bytecode/java_static_initializers.h index 3c8b1a6e898..447cbfa5a7e 100644 --- a/src/java_bytecode/java_static_initializers.h +++ b/src/java_bytecode/java_static_initializers.h @@ -31,8 +31,9 @@ codet get_clinit_wrapper_body( class stub_global_initializer_factoryt { /// Maps class symbols onto the stub globals that belong to them - std::unordered_multimap - stub_globals_by_class; + typedef std::unordered_multimap + stub_globals_by_classt; + stub_globals_by_classt stub_globals_by_class; public: void create_stub_global_initializer_symbols( diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index ada0934367c..ae4839f52f7 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include bool java_is_array_type(const typet &type) { @@ -413,3 +414,17 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( return resolve_inherited_componentt::inherited_componentt(); } } + +/// Check if a symbol is a well-known non-null global +/// \param symbolid: symbol id to check +/// \return true if this static field is known never to be null +bool is_non_null_library_global(const irep_idt &symbolid) +{ + static const std::unordered_set non_null_globals = + { + "java::java.lang.System.out", + "java::java.lang.System.err", + "java::java.lang.System.in" + }; + return non_null_globals.count(symbolid); +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 93ec538dda4..d2ceb0442dd 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -106,4 +106,6 @@ resolve_inherited_componentt::inherited_componentt get_inherited_component( const class_hierarchyt &class_hierarchy, bool include_interfaces); +bool is_non_null_library_global(const irep_idt &); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H From afa443c6fa0468292ff73d1aa14c931bda5efc38 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Feb 2018 09:00:49 +0000 Subject: [PATCH 12/14] US spelling of initialize No functional changes. --- src/java_bytecode/java_bytecode_convert_method.cpp | 4 ++-- src/java_bytecode/java_bytecode_language.cpp | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 1af1c53260c..191d2f997db 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -2027,7 +2027,7 @@ codet java_bytecode_convert_methodt::convert_instructions( } results[0]=java_bytecode_promotion(symbol_expr); - // Note this initialiser call deliberately inits the class used to make + // Note this initializer call deliberately inits the class used to make // the reference, which may be a child of the class that actually defines // the field. codet clinit_call=get_clinit_call(arg0.get_string(ID_class)); @@ -2073,7 +2073,7 @@ codet java_bytecode_convert_methodt::convert_instructions( code_blockt block; block.add_source_location()=i_it->source_location; - // Note this initialiser call deliberately inits the class used to make + // Note this initializer call deliberately inits the class used to make // the reference, which may be a child of the class that actually defines // the field. codet clinit_call=get_clinit_call(arg0.get_string(ID_class)); diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 924df1aca6c..6d5f3318a5f 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -391,8 +391,8 @@ static void generate_constant_global_variables( /// \param symbol_type: new symbol type /// \param class_id: class id that directly encloses this static field /// \param force_nondet_init: if true, always leave the symbol's value nil so it -/// gets nondet initialised during __CPROVER_initialize. Otherwise, pointer- -/// typed globals are initialised null and we expect a synthetic clinit method +/// gets nondet initialized during __CPROVER_initialize. Otherwise, pointer- +/// typed globals are initialized null and we expect a synthetic clinit method /// to be created later. static void create_stub_global_symbol( symbol_table_baset &symbol_table, @@ -464,8 +464,8 @@ static irep_idt get_any_incomplete_ancestor( /// Search for getstatic and putstatic instructions in a class' bytecode and /// create stub symbols for any static fields that aren't already in the symbol -/// table. The new symbols are null-initialised for reference-typed globals / -/// static fields, and nondet-initialised for primitives. +/// table. The new symbols are null-initialized for reference-typed globals / +/// static fields, and nondet-initialized for primitives. /// \param parse_tree: class bytecode /// \param symbol_table: symbol table; may gain new symbols /// \param class_hierarchy: global class hierarchy From f15c3128700b39995a5753ffc4bb0b0d47e8107c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Feb 2018 10:34:15 +0000 Subject: [PATCH 13/14] Exclude j.l.O from possible static field hosts. --- src/java_bytecode/java_bytecode_language.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 6d5f3318a5f..2e9ff41c560 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -429,13 +429,15 @@ static void create_stub_global_symbol( !add_failed, "caller should have checked symbol not already in table"); } -/// Find any incomplete ancestor of a given class +/// Find any incomplete ancestor of a given class that can have a stub static +/// field attached to it. This specifically excludes java.lang.Object, which we +/// know cannot have static fields. /// \param start_class_id: class to start searching from /// \param symbol_table: global symbol table /// \param class_hierarchy: global class hierarchy /// \return first incomplete ancestor encountered, /// including start_class_id itself. -static irep_idt get_any_incomplete_ancestor( +static irep_idt get_any_incomplete_ancestor_for_stub_static_field( const irep_idt &start_class_id, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy) @@ -450,8 +452,12 @@ static irep_idt get_any_incomplete_ancestor( irep_idt to_check = classes_to_check.back(); classes_to_check.pop_back(); - if(symbol_table.lookup_ref(to_check).type.get_bool(ID_incomplete_class)) + // Exclude java.lang.Object because it can + if(symbol_table.lookup_ref(to_check).type.get_bool(ID_incomplete_class) && + to_check != "java::java.lang.Object") + { return to_check; + } const class_hierarchyt::idst &parents = class_hierarchy.class_map.at(to_check).parents; @@ -512,7 +518,7 @@ static void create_stub_global_symbols( // class that was referred to. This is just a guess, but we have no // better information to go on. irep_idt add_to_class_id = - get_any_incomplete_ancestor( + get_any_incomplete_ancestor_for_stub_static_field( class_id, symbol_table, class_hierarchy); // If there are no incomplete ancestors to ascribe the missing field From 1da5be1abc39b3ceef2e1b46c27e96b6269d4331 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 12 Feb 2018 18:37:27 +0000 Subject: [PATCH 14/14] Add tests for inherited static fields These cover various permutations of static fields defined on parents, on interfaces, and those parents and/or interfaces being opaque (stubs). They check both that jbmc doesn't outright crash, and in some cases that jbmc correctly determines that two static fields must be the same one, and therefore cannot differ. --- .../inherited_static_field1/Parent.class | Bin 0 -> 200 bytes .../inherited_static_field1/Test.class | Bin 0 -> 526 bytes .../inherited_static_field1/Test.java | 16 + .../inherited_static_field1/test.desc | 8 + .../inherited_static_field10/Parent.class | Bin 0 -> 202 bytes .../inherited_static_field10/Parent.java | 9 + .../inherited_static_field10/Test.class | Bin 0 -> 526 bytes .../inherited_static_field10/Test.java | 10 + .../compile_against/Parent.class | Bin 0 -> 202 bytes .../compile_against/Parent.java | 8 + .../inherited_static_field10/test.desc | 11 + .../InterfaceWithStatic.class | Bin 0 -> 428 bytes .../InterfaceWithStatic.java | 12 + .../inherited_static_field2/Parent.class | Bin 0 -> 184 bytes .../inherited_static_field2/Test.class | Bin 0 -> 554 bytes .../inherited_static_field2/Test.java | 16 + .../inherited_static_field2/test.desc | 8 + .../inherited_static_field3/Test.class | Bin 0 -> 517 bytes .../inherited_static_field3/Test.java | 15 + .../inherited_static_field3/test.desc | 7 + .../inherited_static_field4/Grandparent.class | Bin 0 -> 205 bytes .../inherited_static_field4/Parent.class | Bin 0 -> 195 bytes .../inherited_static_field4/Test.class | Bin 0 -> 543 bytes .../inherited_static_field4/Test.java | 22 ++ .../inherited_static_field4/test.desc | 9 + .../InterfaceWithStatic.class | Bin 0 -> 428 bytes .../InterfaceWithStatic.java | 12 + .../inherited_static_field5/Test.class | Bin 0 -> 560 bytes .../inherited_static_field5/Test.java | 16 + .../inherited_static_field5/test.desc | 8 + .../inherited_static_field6/Grandparent.class | Bin 0 -> 205 bytes .../inherited_static_field6/Test.class | Bin 0 -> 549 bytes .../inherited_static_field6/Test.java | 22 ++ .../inherited_static_field6/test.desc | 10 + .../OpaqueInterfaceWithStatic.java | 12 + .../inherited_static_field7/Test.class | Bin 0 -> 570 bytes .../inherited_static_field7/Test.java | 12 + .../inherited_static_field7/test.desc | 9 + .../inherited_static_field8/Parent.class | Bin 0 -> 201 bytes .../inherited_static_field8/Test.class | Bin 0 -> 582 bytes .../inherited_static_field8/Test.java | 23 ++ .../inherited_static_field8/test.desc | 11 + .../inherited_static_field9/Parent.class | Bin 0 -> 186 bytes .../inherited_static_field9/Parent.java | 7 + .../inherited_static_field9/Test.class | Bin 0 -> 526 bytes .../inherited_static_field9/Test.java | 10 + .../compile_against/Parent.class | Bin 0 -> 202 bytes .../compile_against/Parent.java | 8 + .../inherited_static_field9/test.desc | 13 + unit/Makefile | 1 + .../inherited_static_fields/Parent1.class | Bin 0 -> 202 bytes .../inherited_static_fields/Parent6.class | Bin 0 -> 202 bytes .../inherited_static_fields/Parent8.class | Bin 0 -> 202 bytes .../inherited_static_fields/Parent9.class | Bin 0 -> 202 bytes .../StaticInterface2.class | Bin 0 -> 411 bytes .../StaticInterface7.class | Bin 0 -> 411 bytes .../StaticInterface9.class | Bin 0 -> 411 bytes .../inherited_static_fields/Test1.class | Bin 0 -> 248 bytes .../inherited_static_fields/Test1.java | 12 + .../inherited_static_fields/Test2.class | Bin 0 -> 281 bytes .../inherited_static_fields/Test2.java | 18 + .../inherited_static_fields/Test3.class | Bin 0 -> 254 bytes .../inherited_static_fields/Test3.java | 12 + .../inherited_static_fields/Test4.class | Bin 0 -> 281 bytes .../inherited_static_fields/Test4.java | 18 + .../inherited_static_fields/Test5.class | Bin 0 -> 278 bytes .../inherited_static_fields/Test5.java | 22 ++ .../inherited_static_fields/Test6.class | Bin 0 -> 248 bytes .../inherited_static_fields/Test6.java | 12 + .../inherited_static_fields/Test7.class | Bin 0 -> 285 bytes .../inherited_static_fields/Test7.java | 18 + .../inherited_static_fields/Test8.class | Bin 0 -> 248 bytes .../inherited_static_fields/Test8.java | 12 + .../inherited_static_fields/Test9.class | Bin 0 -> 272 bytes .../inherited_static_fields/Test9.java | 22 ++ .../inherited_static_fields.cpp | 311 ++++++++++++++++++ .../otherpackage/Parent7.class | Bin 0 -> 217 bytes .../otherpackage/Parent7.java | 5 + 78 files changed, 787 insertions(+) create mode 100644 regression/cbmc-java/inherited_static_field1/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field1/Test.class create mode 100644 regression/cbmc-java/inherited_static_field1/Test.java create mode 100644 regression/cbmc-java/inherited_static_field1/test.desc create mode 100644 regression/cbmc-java/inherited_static_field10/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field10/Parent.java create mode 100644 regression/cbmc-java/inherited_static_field10/Test.class create mode 100644 regression/cbmc-java/inherited_static_field10/Test.java create mode 100644 regression/cbmc-java/inherited_static_field10/compile_against/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field10/compile_against/Parent.java create mode 100644 regression/cbmc-java/inherited_static_field10/test.desc create mode 100644 regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.class create mode 100644 regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.java create mode 100644 regression/cbmc-java/inherited_static_field2/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field2/Test.class create mode 100644 regression/cbmc-java/inherited_static_field2/Test.java create mode 100644 regression/cbmc-java/inherited_static_field2/test.desc create mode 100644 regression/cbmc-java/inherited_static_field3/Test.class create mode 100644 regression/cbmc-java/inherited_static_field3/Test.java create mode 100644 regression/cbmc-java/inherited_static_field3/test.desc create mode 100644 regression/cbmc-java/inherited_static_field4/Grandparent.class create mode 100644 regression/cbmc-java/inherited_static_field4/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field4/Test.class create mode 100644 regression/cbmc-java/inherited_static_field4/Test.java create mode 100644 regression/cbmc-java/inherited_static_field4/test.desc create mode 100644 regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.class create mode 100644 regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.java create mode 100644 regression/cbmc-java/inherited_static_field5/Test.class create mode 100644 regression/cbmc-java/inherited_static_field5/Test.java create mode 100644 regression/cbmc-java/inherited_static_field5/test.desc create mode 100644 regression/cbmc-java/inherited_static_field6/Grandparent.class create mode 100644 regression/cbmc-java/inherited_static_field6/Test.class create mode 100644 regression/cbmc-java/inherited_static_field6/Test.java create mode 100644 regression/cbmc-java/inherited_static_field6/test.desc create mode 100644 regression/cbmc-java/inherited_static_field7/OpaqueInterfaceWithStatic.java create mode 100644 regression/cbmc-java/inherited_static_field7/Test.class create mode 100644 regression/cbmc-java/inherited_static_field7/Test.java create mode 100644 regression/cbmc-java/inherited_static_field7/test.desc create mode 100644 regression/cbmc-java/inherited_static_field8/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field8/Test.class create mode 100644 regression/cbmc-java/inherited_static_field8/Test.java create mode 100644 regression/cbmc-java/inherited_static_field8/test.desc create mode 100644 regression/cbmc-java/inherited_static_field9/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field9/Parent.java create mode 100644 regression/cbmc-java/inherited_static_field9/Test.class create mode 100644 regression/cbmc-java/inherited_static_field9/Test.java create mode 100644 regression/cbmc-java/inherited_static_field9/compile_against/Parent.class create mode 100644 regression/cbmc-java/inherited_static_field9/compile_against/Parent.java create mode 100644 regression/cbmc-java/inherited_static_field9/test.desc create mode 100644 unit/java_bytecode/inherited_static_fields/Parent1.class create mode 100644 unit/java_bytecode/inherited_static_fields/Parent6.class create mode 100644 unit/java_bytecode/inherited_static_fields/Parent8.class create mode 100644 unit/java_bytecode/inherited_static_fields/Parent9.class create mode 100644 unit/java_bytecode/inherited_static_fields/StaticInterface2.class create mode 100644 unit/java_bytecode/inherited_static_fields/StaticInterface7.class create mode 100644 unit/java_bytecode/inherited_static_fields/StaticInterface9.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test1.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test1.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test2.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test2.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test3.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test3.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test4.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test4.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test5.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test5.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test6.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test6.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test7.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test7.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test8.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test8.java create mode 100644 unit/java_bytecode/inherited_static_fields/Test9.class create mode 100644 unit/java_bytecode/inherited_static_fields/Test9.java create mode 100644 unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp create mode 100644 unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.class create mode 100644 unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.java diff --git a/regression/cbmc-java/inherited_static_field1/Parent.class b/regression/cbmc-java/inherited_static_field1/Parent.class new file mode 100644 index 0000000000000000000000000000000000000000..04f63e0aac09ef3cd401a93af03b5092d8b69c69 GIT binary patch literal 200 zcmXYqJqp4=5QX2EKaJ6N0l`u&Ok*iFf*^fN zEa%*Gcy}QB46MTtsF{}Oo-ioo!&?TmKI#jG*rjQS>+!HF?6w@H#*mv9xpGsEMOrTJ zJznvrMK@UM4Hh_hYc#fd;=+_$p|)_`;|KoC4H$?R*uu5}9btx?tX2lxy04rqwKZ&e zWD|+p(y(J-7keb}hTFn&N$(52CaGJm)(3PLL#8hr(-!>|66tft)S#<6grd>U04$!9 z+!QHbQV-cEWhL^Ay#Htp_AUnzBOCCFbOho^P%K9q@Ojl@eg@wZ$^_}D4AfVIzu>={ zBk&^;d>%rShzJ%cVHFTWk}{%}VQR%*^#FlHQu{z~0!@8`s?4CQah6Ktz8^m0RO(H8 GG#me6nphzK literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field1/Test.java b/regression/cbmc-java/inherited_static_field1/Test.java new file mode 100644 index 00000000000..c90b2f72366 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field1/Test.java @@ -0,0 +1,16 @@ +public class Test extends Parent { + + public static void main(int nondet) { + + x = nondet; + assert x == Parent.x; + + } + +} + +class Parent { + + public static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field1/test.desc b/regression/cbmc-java/inherited_static_field1/test.desc new file mode 100644 index 00000000000..2907dba48a4 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field1/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ +-- +-- +This checks that jbmc knows that test.x and parent.x refer to the same field. +Both test and parent are concrete (available) classes. diff --git a/regression/cbmc-java/inherited_static_field10/Parent.class b/regression/cbmc-java/inherited_static_field10/Parent.class new file mode 100644 index 0000000000000000000000000000000000000000..787201859b0dd94ca3b90143e91f1b7600d61335 GIT binary patch literal 202 zcmXAiJqp4=5QX35Z#9X=3s~5xg=s9sMi2y1L9yS&MK;6@ghafSm0;lkJd`-bV&2UA zhI#Y;JYN8&hobyM7-VesPH0OAmWGbyNfW@By4uJ!=nfL&LNsC>dJ8^f% S5750?w^_XgTC6@h3&9t6G$Gyq literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field10/Parent.java b/regression/cbmc-java/inherited_static_field10/Parent.java new file mode 100644 index 00000000000..6c2ec6f56d4 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field10/Parent.java @@ -0,0 +1,9 @@ + +public class Parent { + + // This is the version of Parent we will run jbmc against, which has + // a static field 'x', but that field is private and cannot correspond + // to the reference 'Test.x'. + private static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field10/Test.class b/regression/cbmc-java/inherited_static_field10/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..84525e68f472c99f642bdf978b41e8ef2ea58f6d GIT binary patch literal 526 zcmYLFOG^S#7(Le+9UaHFsrl%=uok&-DN&e#P!T9W?yh=?DIH^GjDCxomaS7rD5!lu zD*Eo=V{yOtch33l@89P)fGYNNgpdhALsptxh|;WvO&xw@G~{&@P}ERjNF8v;5w>fN zEa%*Gcy}QB46MTtsF{}Oo-ioo!&?TmKI#jG*rjQS>+!HF?6w@H#*mv9xpGsEMOrTJ zJznvrMK@UM4Hh_hYc#fd;=+_$p|)_`;|KoC4H$?R*uu5}9btx?tX2lxy04rqwKZ&e zWD|+p(y(J-7keb}hTFn&N$(52CaGJm)(3PLL#8hr(-!>|66tft)S#<6grd>U04$!9 z+!QHbQV-cEWhL^Ay#Htp_AUnzBOCCFbOho^P%K9q@Ojl@eg@wZ$^_}D4AfVIzu>={ zBk&^;d>%rShzJ%cVHFTWk}{%}VQR%*^#FlHQu{z~0!@8`s?4CQah6Ktz8^m0RO(H8 GG#me6nphzK literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field10/Test.java b/regression/cbmc-java/inherited_static_field10/Test.java new file mode 100644 index 00000000000..0826320a970 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field10/Test.java @@ -0,0 +1,10 @@ +public class Test extends Parent { + + public static void main(int nondet) { + + x = nondet; + assert x == Parent.x; + + } + +} diff --git a/regression/cbmc-java/inherited_static_field10/compile_against/Parent.class b/regression/cbmc-java/inherited_static_field10/compile_against/Parent.class new file mode 100644 index 0000000000000000000000000000000000000000..281a2d673259caf49872c6156b0902136c405046 GIT binary patch literal 202 zcmXYqJqp4=5QX35Z#9X=3s~5xg=s9sMi2y1L9yS&MH1o$LLy$vO0e(%9!i`9A~ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field10/compile_against/Parent.java b/regression/cbmc-java/inherited_static_field10/compile_against/Parent.java new file mode 100644 index 00000000000..70a93b432bf --- /dev/null +++ b/regression/cbmc-java/inherited_static_field10/compile_against/Parent.java @@ -0,0 +1,8 @@ + +public class Parent { + + // This is the version of Parent we compile Test.java against, which does + // have a static field 'x'. + public static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field10/test.desc b/regression/cbmc-java/inherited_static_field10/test.desc new file mode 100644 index 00000000000..21b4aa8958f --- /dev/null +++ b/regression/cbmc-java/inherited_static_field10/test.desc @@ -0,0 +1,11 @@ +CORE +Test.class + +Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\. +assertion at file Test\.java line 6 .* FAILURE +^VERIFICATION FAILED$ +-- +Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\. +-- +This test is the same as inherited_static_field9, except that the version of Parent we run against +has a private static field that Test's 'x' cannot be referring to. diff --git a/regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.class b/regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.class new file mode 100644 index 0000000000000000000000000000000000000000..b21da732e3d9f4005304f170b067ee1f3837d186 GIT binary patch literal 428 zcmZutO-sW-5Pg%@q>a&3TebD;tR9R9Z!HB8ghJ6nMe(?eYu%Eju-%CIue6|`;1BRe ziL=pT7ItUe?3=f5=lkd53&1gUJv4j})~ax^ZnF)WH9fREY!V!i@MV829z>KGl|(06 zi>JPtnKq$1P@`0sOiRK+5vTK4Ohh`0da02ksoPy{q(|O8LZuTYDpjUSDDCZE5z432 zTNVrZDwXHiWGMBe7$#it2h&W)@=RIKv|9R3#PV91`+*Tg#fR1+pC1w_g5NdgUZunw2ma!qYoqvnvnR@2e*=f%O56R;RI%rv8o|~VeMaC@8IsXpJ r2szdm9Wm3c#wY0J9nKu3SCrmRo@3#K>x30P{hU?dXcbqv;-LNuh2mQW literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.java b/regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.java new file mode 100644 index 00000000000..b09e6de019e --- /dev/null +++ b/regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.java @@ -0,0 +1,12 @@ +import java.util.ArrayList; + +interface InterfaceWithStatic { + + // The ArrayList is only here to define a constant x that + // is complicated enough for javac to generate a static init + // rather than just propagate the constant to all users. + static ArrayList al = new ArrayList(); + static int x = al.size(); + +} + diff --git a/regression/cbmc-java/inherited_static_field2/Parent.class b/regression/cbmc-java/inherited_static_field2/Parent.class new file mode 100644 index 0000000000000000000000000000000000000000..1c26d41b5f622b6ca4dc5bea7eabc5331ae164b8 GIT binary patch literal 184 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!oUhNB_OdVHLrw`K>#GE zpOcuEuJ50em6}|_puoTcv=0Orff%S7NV5T1vOpRn!m72MfpH^PnjJ{8fdzSiBnObk H#J~vvQDz`2 literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field2/Test.class b/regression/cbmc-java/inherited_static_field2/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..d495fed0e6dada68b9609afaaea0af518dfd89ff GIT binary patch literal 554 zcmYL_&o2W(6vw}>-R*SOqKYc@n*$D9+%!V`NF<1a5N=~T7-}oCTk*HJI6A9@goL~Q ziFi{~Hv4AgJ8!=4^WMkT%Nu}sO#1Lp@Zh7*gZK$Wfqow@3IYQ@N*ELv5*Q|QPs%t} zCegJhUe&QYuBr-wjtH5uj&!m}NKZ}g6P%S=MG-nTb)>fIm&eNN*<`-BlsY1`?V+**tm2pCX#5P zdq2uJw*g$-nL9IQ&YYQ_-;XZR=V7|tsKro9lLJd zr6ICQ!0m5blrrcS0+Az5c7dW2c}8B{nSi}YAQEIFL6TNMat_^tLKUDmhB88SjL;b2XT(0C z-b@hrmfcFwZ3IXa1sa~BER8H6iu9bS8qfo&wDykZ2wM0B;m{kDe~y^~*{?z|52Vga HFe3X06nt2a literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field3/Test.java b/regression/cbmc-java/inherited_static_field3/Test.java new file mode 100644 index 00000000000..b6dd107bd7c --- /dev/null +++ b/regression/cbmc-java/inherited_static_field3/Test.java @@ -0,0 +1,15 @@ +public class Test extends OpaqueParent { + + public static void main() { + + assert x == OpaqueParent.x; + + } + +} + +class OpaqueParent { + + public static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field3/test.desc b/regression/cbmc-java/inherited_static_field3/test.desc new file mode 100644 index 00000000000..7c103f56c23 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field3/test.desc @@ -0,0 +1,7 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ +-- +-- +This is the same as test inherited_static_field1, except Test's parent is opaque. diff --git a/regression/cbmc-java/inherited_static_field4/Grandparent.class b/regression/cbmc-java/inherited_static_field4/Grandparent.class new file mode 100644 index 0000000000000000000000000000000000000000..8c01226bd0557f1b70e0d53965e7811df1d36f68 GIT binary patch literal 205 zcmXX6rD!BXA`~wAy}OO>eaw5A z_viTnFhV0l5!C>-0CfW0cou}xSZQS^gkrb1C3w?gCJBwD(sFew*ta`UETjIo3TV_M}!R|eOc9QLILf5echH#dk#B zpbe0HQ-S`B#22DBL&Sa*LL@|(AtHi>PFRbGBTX4mt1vTRuY`cWT-x|Rd;mj#fv&wn Uo8pX>sQoA+_JPuy4Qb~80Z9m4>Hq)$ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field4/Test.java b/regression/cbmc-java/inherited_static_field4/Test.java new file mode 100644 index 00000000000..75baf498b48 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field4/Test.java @@ -0,0 +1,22 @@ +public class Test extends Parent { + + public static void main(int nondet) { + + x = nondet; + assert x == Grandparent.x; + + } + +} + +class Parent extends Grandparent { + + public static int x; + +} + +class Grandparent { + + public static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field4/test.desc b/regression/cbmc-java/inherited_static_field4/test.desc new file mode 100644 index 00000000000..7654d272915 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field4/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class + +assertion at file Test\.java line 6 .* FAILURE +^VERIFICATION FAILED$ +-- +-- +This checks that jbmc knows that the hidden field Grandparent.x is not the same +as Test.x, which resolves to Parent.x. diff --git a/regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.class b/regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.class new file mode 100644 index 0000000000000000000000000000000000000000..b21da732e3d9f4005304f170b067ee1f3837d186 GIT binary patch literal 428 zcmZutO-sW-5Pg%@q>a&3TebD;tR9R9Z!HB8ghJ6nMe(?eYu%Eju-%CIue6|`;1BRe ziL=pT7ItUe?3=f5=lkd53&1gUJv4j})~ax^ZnF)WH9fREY!V!i@MV829z>KGl|(06 zi>JPtnKq$1P@`0sOiRK+5vTK4Ohh`0da02ksoPy{q(|O8LZuTYDpjUSDDCZE5z432 zTNVrZDwXHiWGMBe7$#it2h&W)@=RIKv|9R3#PV91`+*Tg#fR1+pC1w_g5NdgUZunw2ma!qYoqvnvnR@2e*=f%O56R;RI%rv8o|~VeMaC@8IsXpJ r2szdm9Wm3c#wY0J9nKu3SCrmRo@3#K>x30P{hU?dXcbqv;-LNuh2mQW literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.java b/regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.java new file mode 100644 index 00000000000..b09e6de019e --- /dev/null +++ b/regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.java @@ -0,0 +1,12 @@ +import java.util.ArrayList; + +interface InterfaceWithStatic { + + // The ArrayList is only here to define a constant x that + // is complicated enough for javac to generate a static init + // rather than just propagate the constant to all users. + static ArrayList al = new ArrayList(); + static int x = al.size(); + +} + diff --git a/regression/cbmc-java/inherited_static_field5/Test.class b/regression/cbmc-java/inherited_static_field5/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..c10309d1e79a79a5ae008fee2d17f8a3ea3df047 GIT binary patch literal 560 zcmYLFO-~y!5Pg&E#@Wq=giu0C_$(ZN16;T@Lajn8MJgXs5D0G0#uT?<1KthlZ{gA- zXMzM$E46q26NqsXf-H~iH{&<&&ExZ*e*iYI?88IZgTRyr-v)t-z^Req*qoC2~NG+R)oSg9jV>kc}tlCTg-`b zsUt$ZnaJ?xj=UJc*;?2c68Oz-&xGo$w&mV|ij(yp@=6BCV=TZt76RlD5Goek=*Z~% z#^+a2UySJ*Zeo84EC%?1B|@-wAuoGsUm6u9Y@!h*%ACqj9qHtZg(Ny;6Tf&jSn?Zf zy~Az^<+h5oQSDI|`=!STwt9j^o|gyW(NVEtmGM;5{ARTr3;depllXMk9zeHzArv`g z1|VC+_^5OTDPF)#AE}Rhq-%XR*C_Cy@qgZ;H2;1yz#v%vK%f_!6&Qx-Jsp%3lunFg#Z8m literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/inherited_static_field5/Test.java b/regression/cbmc-java/inherited_static_field5/Test.java new file mode 100644 index 00000000000..be37ca3a27e --- /dev/null +++ b/regression/cbmc-java/inherited_static_field5/Test.java @@ -0,0 +1,16 @@ +public class Test extends OpaqueParent implements InterfaceWithStatic { + + public static void main() { + + int val1 = x; + int val2 = InterfaceWithStatic.x; + assert val1 == val2; + + } + +} + +class OpaqueParent { + +} + diff --git a/regression/cbmc-java/inherited_static_field5/test.desc b/regression/cbmc-java/inherited_static_field5/test.desc new file mode 100644 index 00000000000..648ed211410 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field5/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ +-- +-- +This is the same as inherited_static_field2, except that Test's parent is opaque. It must pass because +the field 'x' should be found on InterfaceWithStatic, and so not created as a stub on OpaqueParent. diff --git a/regression/cbmc-java/inherited_static_field6/Grandparent.class b/regression/cbmc-java/inherited_static_field6/Grandparent.class new file mode 100644 index 0000000000000000000000000000000000000000..8c01226bd0557f1b70e0d53965e7811df1d36f68 GIT binary patch literal 205 zcmXX6rD!BXA`~wAy}OO>eaw5A z_viTnFhV0l5!C>-0CfW0cou}xSZQS^gkrb1C3w?gCJBwD(sFe6_VPHm?yop)N7?`sVMb5yyg#wBO78o*R?)yRp zZrAhoT%R}F!eL+yhS-+txxqGrwzhuBpx3&NU`QXio;c}unnGTvVQO@^>ycYKRAb5W zfVXasd2iH>Z?)PZ9P7N>mo2gHsx9+E_`&84zvnh=ByB8W$%ci5ff7SrH7afHT~~Jh z4NbWhkQ8oP!S8LO~3^_;mt`yD~ zon!}nYS6I_l<3b)`bajBSCS~wKvYPQO;J`P&&WqN-oT#KAkt)GVUcdb1STm~qjf~W zYGLjLks-7JvO^W