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 00000000000..04f63e0aac0 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field1/Parent.class differ diff --git a/regression/cbmc-java/inherited_static_field1/Test.class b/regression/cbmc-java/inherited_static_field1/Test.class new file mode 100644 index 00000000000..84525e68f47 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field1/Test.class differ 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 00000000000..787201859b0 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field10/Parent.class differ 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 00000000000..84525e68f47 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field10/Test.class differ 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 00000000000..281a2d67325 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field10/compile_against/Parent.class differ 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 00000000000..b21da732e3d Binary files /dev/null and b/regression/cbmc-java/inherited_static_field2/InterfaceWithStatic.class differ 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 00000000000..1c26d41b5f6 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field2/Parent.class differ 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 00000000000..d495fed0e6d Binary files /dev/null and b/regression/cbmc-java/inherited_static_field2/Test.class differ diff --git a/regression/cbmc-java/inherited_static_field2/Test.java b/regression/cbmc-java/inherited_static_field2/Test.java new file mode 100644 index 00000000000..f6f558bcfe9 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field2/Test.java @@ -0,0 +1,16 @@ +public class Test extends Parent implements InterfaceWithStatic { + + public static void main() { + + int val1 = InterfaceWithStatic.x; + int val2 = x; + assert val1 == val2; + + } + +} + +class Parent { + +} + diff --git a/regression/cbmc-java/inherited_static_field2/test.desc b/regression/cbmc-java/inherited_static_field2/test.desc new file mode 100644 index 00000000000..03cdd9bf210 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field2/test.desc @@ -0,0 +1,8 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ +-- +-- +This checks that jbmc knows that Test.x and InterfaceWithStatic.x are the same field. +All types are concrete (not stubs). diff --git a/regression/cbmc-java/inherited_static_field3/Test.class b/regression/cbmc-java/inherited_static_field3/Test.class new file mode 100644 index 00000000000..bbc4cd29420 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field3/Test.class differ 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 00000000000..8c01226bd05 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field4/Grandparent.class differ diff --git a/regression/cbmc-java/inherited_static_field4/Parent.class b/regression/cbmc-java/inherited_static_field4/Parent.class new file mode 100644 index 00000000000..4e5005f251f Binary files /dev/null and b/regression/cbmc-java/inherited_static_field4/Parent.class differ diff --git a/regression/cbmc-java/inherited_static_field4/Test.class b/regression/cbmc-java/inherited_static_field4/Test.class new file mode 100644 index 00000000000..267697d1a1f Binary files /dev/null and b/regression/cbmc-java/inherited_static_field4/Test.class differ 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 00000000000..b21da732e3d Binary files /dev/null and b/regression/cbmc-java/inherited_static_field5/InterfaceWithStatic.class differ 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 00000000000..c10309d1e79 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field5/Test.class differ 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 00000000000..8c01226bd05 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field6/Grandparent.class differ diff --git a/regression/cbmc-java/inherited_static_field6/Test.class b/regression/cbmc-java/inherited_static_field6/Test.class new file mode 100644 index 00000000000..b31bf4ccfd0 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field6/Test.class differ diff --git a/regression/cbmc-java/inherited_static_field6/Test.java b/regression/cbmc-java/inherited_static_field6/Test.java new file mode 100644 index 00000000000..251eeb2c73a --- /dev/null +++ b/regression/cbmc-java/inherited_static_field6/Test.java @@ -0,0 +1,22 @@ +public class Test extends OpaqueParent { + + public static void main(int nondet) { + + x = nondet; + assert x == Grandparent.x; + + } + +} + +class OpaqueParent extends Grandparent { + + public static int x; + +} + +class Grandparent { + + public static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field6/test.desc b/regression/cbmc-java/inherited_static_field6/test.desc new file mode 100644 index 00000000000..37e554af6ca --- /dev/null +++ b/regression/cbmc-java/inherited_static_field6/test.desc @@ -0,0 +1,10 @@ +CORE +Test.class + +assertion at file Test\.java line 6 .* FAILURE +^VERIFICATION FAILED$ +-- +-- +This test is the same as inherited_static_field4, except that Test's parent is opaque. +This checks that jbmc guesses that the hidden field Grandparent.x is not the same +as Test.x, which may resolve to the (unseen) Parent.x. diff --git a/regression/cbmc-java/inherited_static_field7/OpaqueInterfaceWithStatic.java b/regression/cbmc-java/inherited_static_field7/OpaqueInterfaceWithStatic.java new file mode 100644 index 00000000000..42770560db9 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field7/OpaqueInterfaceWithStatic.java @@ -0,0 +1,12 @@ +import java.util.ArrayList; + +interface OpaqueInterfaceWithStatic { + + // 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_field7/Test.class b/regression/cbmc-java/inherited_static_field7/Test.class new file mode 100644 index 00000000000..655f2554cbe Binary files /dev/null and b/regression/cbmc-java/inherited_static_field7/Test.class differ diff --git a/regression/cbmc-java/inherited_static_field7/Test.java b/regression/cbmc-java/inherited_static_field7/Test.java new file mode 100644 index 00000000000..313ce341c39 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field7/Test.java @@ -0,0 +1,12 @@ +public class Test implements OpaqueInterfaceWithStatic { + + public static void main() { + + int val1 = x; + int val2 = OpaqueInterfaceWithStatic.x; + assert val1 == val2; + + } + +} + diff --git a/regression/cbmc-java/inherited_static_field7/test.desc b/regression/cbmc-java/inherited_static_field7/test.desc new file mode 100644 index 00000000000..f008fcef51b --- /dev/null +++ b/regression/cbmc-java/inherited_static_field7/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ +-- +-- +This test must pass, as there is only one opaque parent (interface_with_static). +In particular this one makes sure we don't identify Object as opaque and guess that +java.lang.Object.x exists (since we know Object doesn't have static fields). diff --git a/regression/cbmc-java/inherited_static_field8/Parent.class b/regression/cbmc-java/inherited_static_field8/Parent.class new file mode 100644 index 00000000000..2a9c67b65e1 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field8/Parent.class differ diff --git a/regression/cbmc-java/inherited_static_field8/Test.class b/regression/cbmc-java/inherited_static_field8/Test.class new file mode 100644 index 00000000000..cd9c0634227 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field8/Test.class differ diff --git a/regression/cbmc-java/inherited_static_field8/Test.java b/regression/cbmc-java/inherited_static_field8/Test.java new file mode 100644 index 00000000000..035f3116106 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field8/Test.java @@ -0,0 +1,23 @@ +public class Test extends Parent { + + public static void main(int nondet) { + + x = nondet; + assert x == Parent.x; + assert x == OpaqueGrandparent.x; + + } + +} + +class Parent extends OpaqueGrandparent { + + public static int x; + +} + +class OpaqueGrandparent { + + public static int x; + +} diff --git a/regression/cbmc-java/inherited_static_field8/test.desc b/regression/cbmc-java/inherited_static_field8/test.desc new file mode 100644 index 00000000000..2a8234f4dc3 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field8/test.desc @@ -0,0 +1,11 @@ +CORE +Test.class + +assertion at file Test\.java line 6 .* SUCCESS +assertion at file Test\.java line 7 .* FAILURE +^VERIFICATION FAILED$ +-- +-- +This test is the same as inherited_static_field4, except that Test's grandparent is opaque. +This checks that jbmc infers that the hidden field Grandparent.x is not the same +as Test.x, which is known to resolve to Parent.x. diff --git a/regression/cbmc-java/inherited_static_field9/Parent.class b/regression/cbmc-java/inherited_static_field9/Parent.class new file mode 100644 index 00000000000..26fd370b066 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field9/Parent.class differ diff --git a/regression/cbmc-java/inherited_static_field9/Parent.java b/regression/cbmc-java/inherited_static_field9/Parent.java new file mode 100644 index 00000000000..4b6048d9bb4 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field9/Parent.java @@ -0,0 +1,7 @@ + +public class Parent { + + // This is the version of Parent we will run jbmc against, which does + // not have a static field 'x'. + +} diff --git a/regression/cbmc-java/inherited_static_field9/Test.class b/regression/cbmc-java/inherited_static_field9/Test.class new file mode 100644 index 00000000000..84525e68f47 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field9/Test.class differ diff --git a/regression/cbmc-java/inherited_static_field9/Test.java b/regression/cbmc-java/inherited_static_field9/Test.java new file mode 100644 index 00000000000..0826320a970 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field9/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_field9/compile_against/Parent.class b/regression/cbmc-java/inherited_static_field9/compile_against/Parent.class new file mode 100644 index 00000000000..281a2d67325 Binary files /dev/null and b/regression/cbmc-java/inherited_static_field9/compile_against/Parent.class differ diff --git a/regression/cbmc-java/inherited_static_field9/compile_against/Parent.java b/regression/cbmc-java/inherited_static_field9/compile_against/Parent.java new file mode 100644 index 00000000000..70a93b432bf --- /dev/null +++ b/regression/cbmc-java/inherited_static_field9/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_field9/test.desc b/regression/cbmc-java/inherited_static_field9/test.desc new file mode 100644 index 00000000000..91444da43c2 --- /dev/null +++ b/regression/cbmc-java/inherited_static_field9/test.desc @@ -0,0 +1,13 @@ +CORE +Test.class + +Stub static field x found for non-stub type java::Test\. In future this will be a fatal error\. +Stub static field x found for non-stub type java::Parent\. In future this will be a fatal error\. +assertion at file Test\.java line 6 .* FAILURE +^VERIFICATION FAILED$ +-- +-- +This tests the corner case where static fields are found on non-stub types, here caused +by compiling Test.class against a version of Parent.class (in directory compile_against) +that has a static field but then analysing it with one that doesn't have that field. +In future, as the warning messages we check for note, this will be a fatal error. 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..7028d0550ce 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,16 +385,16 @@ 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]( 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_concrete_function_callt::concrete_function_callt - &resolved_call = get_virtual_call_target(class_id, function_name); + const resolve_inherited_componentt::inherited_componentt + &resolved_call = get_virtual_call_target(class_id, function_name, false); 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..f408c112735 --- /dev/null +++ b/src/goto-programs/resolve_inherited_component.cpp @@ -0,0 +1,117 @@ +/*******************************************************************\ + + 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) +/// \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, + bool include_interfaces) +{ + PRECONDITION(!class_id.empty()); + PRECONDITION(!component_name.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); + + 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(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(); +} + +/// 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..a6ac3b1eca0 --- /dev/null +++ b/src/goto-programs/resolve_inherited_component.h @@ -0,0 +1,77 @@ +/*******************************************************************\ + + 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, + bool include_interfaces); + + 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..51f746a286b 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, false); 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_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( diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index ec771081f2f..191d2f997db 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 @@ -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 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)); 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 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)); if(clinit_call.get_statement()!=ID_skip) block.move_to_operands(clinit_call); @@ -2764,7 +2773,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 +2805,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,58 +2814,45 @@ 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_concrete_function_callt call_resolver(symbol_table); - const resolve_concrete_function_callt ::concrete_function_callt & - 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_virtual_method_name()); - - 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; - } + resolve_inherited_componentt::inherited_componentt inherited_method = + get_inherited_component( + classname, + methodid, + classname, + symbol_table, + class_hierarchy, + false); + return inherited_method.is_valid(); +} - 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; - } +/// 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(false, "Unexpected access modifier."); - } + INVARIANT( + inherited_method.is_valid(), "static field should be in symbol table"); - return false; + return inherited_method.get_full_component_identifier(); } /// create temporary variables if a write instruction can have undesired side- 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..b7ea7d0748e 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 { @@ -254,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 &, diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index b63d5923e5f..2e9ff41c560 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 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, 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; @@ -405,13 +410,17 @@ 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; // 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(); @@ -420,15 +429,59 @@ 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 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_for_stub_static_field( + 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(); + + // 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; + classes_to_check.insert( + classes_to_check.end(), parents.begin(), parents.end()); + } + + return irep_idt(); +} + /// 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 +/// \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) + symbol_table_baset &symbol_table, + const class_hierarchyt &class_hierarchy, + messaget &log) { namespacet ns(symbol_table); for(const auto &method : parse_tree.parsed_class.methods) @@ -448,16 +501,58 @@ 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)) + // 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, + true); + if(!referred_component.is_valid()) { + // 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_for_stub_static_field( + 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); + create_stub_global_symbol( symbol_table, identifier, component, instruction.args[0].type(), - class_id); + add_to_class_id, + no_incomplete_ancestors); } } } @@ -515,6 +610,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) @@ -574,7 +673,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, *this); } stub_global_initializer_factory.create_stub_global_initializer_symbols( @@ -867,7 +967,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_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 0021bff9325..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) { @@ -325,3 +326,105 @@ 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. +/// \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( + const irep_idt &component_class_id, + const irep_idt &component_name, + const irep_idt &user_class_id, + const symbol_tablet &symbol_table, + 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, 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 + // 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()); + + 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 + 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(); + } +} + +/// 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 ad4c45f51c0..d2ceb0442dd 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,14 @@ 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, + const class_hierarchyt &class_hierarchy, + bool include_interfaces); + +bool is_non_null_library_global(const irep_idt &); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/unit/Makefile b/unit/Makefile index 91dc62345cf..16f985fa47a 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -25,6 +25,7 @@ SRC += unit_tests.cpp \ miniBDD_new.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_utils_test.cpp \ + java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ pointer-analysis/custom_value_set_analysis.cpp \ sharing_node.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ diff --git a/unit/java_bytecode/inherited_static_fields/Parent1.class b/unit/java_bytecode/inherited_static_fields/Parent1.class new file mode 100644 index 00000000000..51190559ff4 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Parent1.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Parent6.class b/unit/java_bytecode/inherited_static_fields/Parent6.class new file mode 100644 index 00000000000..7c953e25133 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Parent6.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Parent8.class b/unit/java_bytecode/inherited_static_fields/Parent8.class new file mode 100644 index 00000000000..f7d8c16af7a Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Parent8.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Parent9.class b/unit/java_bytecode/inherited_static_fields/Parent9.class new file mode 100644 index 00000000000..6dcb3a97bcc Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Parent9.class differ diff --git a/unit/java_bytecode/inherited_static_fields/StaticInterface2.class b/unit/java_bytecode/inherited_static_fields/StaticInterface2.class new file mode 100644 index 00000000000..911c2b52061 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/StaticInterface2.class differ diff --git a/unit/java_bytecode/inherited_static_fields/StaticInterface7.class b/unit/java_bytecode/inherited_static_fields/StaticInterface7.class new file mode 100644 index 00000000000..7b33d219ded Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/StaticInterface7.class differ diff --git a/unit/java_bytecode/inherited_static_fields/StaticInterface9.class b/unit/java_bytecode/inherited_static_fields/StaticInterface9.class new file mode 100644 index 00000000000..e9469a7415e Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/StaticInterface9.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test1.class b/unit/java_bytecode/inherited_static_fields/Test1.class new file mode 100644 index 00000000000..d602ddd23af Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test1.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test1.java b/unit/java_bytecode/inherited_static_fields/Test1.java new file mode 100644 index 00000000000..f7675ad8cda --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test1.java @@ -0,0 +1,12 @@ + +public class Test1 extends Parent1 { + + public static int main() { + return x; + } + +} + +class Parent1 { + public static int x; +} diff --git a/unit/java_bytecode/inherited_static_fields/Test2.class b/unit/java_bytecode/inherited_static_fields/Test2.class new file mode 100644 index 00000000000..56a4ae54105 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test2.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test2.java b/unit/java_bytecode/inherited_static_fields/Test2.java new file mode 100644 index 00000000000..f1fc7f5aa20 --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test2.java @@ -0,0 +1,18 @@ + +import java.util.ArrayList; + +public class Test2 implements StaticInterface2 { + + public static int main() { + return x; + } + +} + +interface StaticInterface2 { + // 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/unit/java_bytecode/inherited_static_fields/Test3.class b/unit/java_bytecode/inherited_static_fields/Test3.class new file mode 100644 index 00000000000..5f79a32deea Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test3.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test3.java b/unit/java_bytecode/inherited_static_fields/Test3.java new file mode 100644 index 00000000000..9d9c0fa99cd --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test3.java @@ -0,0 +1,12 @@ + +public class Test3 extends OpaqueParent3 { + + public static int main() { + return x; + } + +} + +class OpaqueParent3 { + public static int x; +} diff --git a/unit/java_bytecode/inherited_static_fields/Test4.class b/unit/java_bytecode/inherited_static_fields/Test4.class new file mode 100644 index 00000000000..730aecc0c79 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test4.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test4.java b/unit/java_bytecode/inherited_static_fields/Test4.java new file mode 100644 index 00000000000..bfabf903b5c --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test4.java @@ -0,0 +1,18 @@ + +import java.util.ArrayList; + +public class Test4 implements OpaqueInterface4 { + + public static int main() { + return x; + } + +} + +interface OpaqueInterface4 { + // 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/unit/java_bytecode/inherited_static_fields/Test5.class b/unit/java_bytecode/inherited_static_fields/Test5.class new file mode 100644 index 00000000000..c09deec2f3f Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test5.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test5.java b/unit/java_bytecode/inherited_static_fields/Test5.java new file mode 100644 index 00000000000..708b57032fd --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test5.java @@ -0,0 +1,22 @@ + +import java.util.ArrayList; + +public class Test5 extends OpaqueParent5 implements OpaqueInterface5 { + + public static int main() { + return x; + } + +} + +class OpaqueParent5 { + +} + +interface OpaqueInterface5 { + // 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/unit/java_bytecode/inherited_static_fields/Test6.class b/unit/java_bytecode/inherited_static_fields/Test6.class new file mode 100644 index 00000000000..ff8db032d23 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test6.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test6.java b/unit/java_bytecode/inherited_static_fields/Test6.java new file mode 100644 index 00000000000..19b45cf3bae --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test6.java @@ -0,0 +1,12 @@ + +public class Test6 extends Parent6 { + + public static int main() { + return x; + } + +} + +class Parent6 { + protected static int x; +} diff --git a/unit/java_bytecode/inherited_static_fields/Test7.class b/unit/java_bytecode/inherited_static_fields/Test7.class new file mode 100644 index 00000000000..16f4a835311 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test7.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test7.java b/unit/java_bytecode/inherited_static_fields/Test7.java new file mode 100644 index 00000000000..a86bc8e4836 --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test7.java @@ -0,0 +1,18 @@ + +import java.util.ArrayList; + +public class Test7 extends otherpackage.Parent7 implements StaticInterface7 { + + public static int main() { + return x; + } + +} + +interface StaticInterface7 { + // 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/unit/java_bytecode/inherited_static_fields/Test8.class b/unit/java_bytecode/inherited_static_fields/Test8.class new file mode 100644 index 00000000000..16bd0174dd2 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test8.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test8.java b/unit/java_bytecode/inherited_static_fields/Test8.java new file mode 100644 index 00000000000..3e5049b68b4 --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test8.java @@ -0,0 +1,12 @@ + +public class Test8 extends Parent8 { + + public static int main() { + return x; + } + +} + +class Parent8 { + static int x; // package visibility, should be visible to Test8 +} diff --git a/unit/java_bytecode/inherited_static_fields/Test9.class b/unit/java_bytecode/inherited_static_fields/Test9.class new file mode 100644 index 00000000000..c62cc74e256 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/Test9.class differ diff --git a/unit/java_bytecode/inherited_static_fields/Test9.java b/unit/java_bytecode/inherited_static_fields/Test9.java new file mode 100644 index 00000000000..a1d8e6bac95 --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/Test9.java @@ -0,0 +1,22 @@ + +import java.util.ArrayList; + +public class Test9 extends Parent9 implements StaticInterface9 { + + public static int main() { + return x; + } + +} + +class Parent9 { + private static int x; // should be invisible to Test9 +} + +interface StaticInterface9 { + // 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/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp b/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp new file mode 100644 index 00000000000..079cc3fa343 --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp @@ -0,0 +1,311 @@ +/*******************************************************************\ + + Module: Unit tests for inherited static fields + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include + +#include + +#include + +/// Check the full tree of expr for any symbol_exprts that have an identifier id +/// \param expr: expr to check +/// \param id: symbol id to look for +/// \return true if a suitable symbol_exprt is found +static bool contains_symbol_reference(const exprt &expr, const irep_idt &id) +{ + return + std::any_of( + expr.depth_begin(), + expr.depth_end(), + [id](const exprt &e) { // NOLINT (*) + return e.id() == ID_symbol && to_symbol_expr(e).get_identifier() == id; + }); +} + +SCENARIO( + "inherited_static_types", "[core][java_bytecode][inherited_static_types]") +{ + WHEN("A class uses an inherited static field 'x'") + { + symbol_tablet symbol_table= + load_java_class("Test1", "./java_bytecode/inherited_static_fields"); + THEN("A static field 'Parent1.x' should exist") + { + REQUIRE(symbol_table.has_symbol("java::Parent1.x")); + } + THEN("No static field 'Test1.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test1.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test1.main should refer to Parent1.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test1.main:()I").value, + "java::Parent1.x")); + } + } + + WHEN("A class uses an interface static field 'x'") + { + symbol_tablet symbol_table= + load_java_class("Test2", "./java_bytecode/inherited_static_fields"); + THEN("A static field 'StaticInterface2.x' should exist") + { + REQUIRE(symbol_table.has_symbol("java::StaticInterface2.x")); + } + THEN("No static field 'Test2.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test2.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test2.main should refer to StaticInterface2.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test2.main:()I").value, + "java::StaticInterface2.x")); + } + } + + WHEN("A class with an opaque parent uses an inherited static field 'x'") + { + symbol_tablet symbol_table= + load_java_class("Test3", "./java_bytecode/inherited_static_fields"); + THEN("Type OpaqueParent3 should be opaque") + { + REQUIRE( + symbol_table.lookup_ref("java::OpaqueParent3").type.get_bool( + ID_incomplete_class)); + } + THEN("A static field 'OpaqueParent3.x' should exist") + { + REQUIRE(symbol_table.has_symbol("java::OpaqueParent3.x")); + } + THEN("No static field 'Test3.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test3.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test3.main should refer to OpaqueParent3.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test3.main:()I").value, + "java::OpaqueParent3.x")); + } + } + + WHEN("A class with an opaque interface uses an inherited static field 'x'") + { + symbol_tablet symbol_table= + load_java_class("Test4", "./java_bytecode/inherited_static_fields"); + THEN("Type OpaqueInterface4 should be opaque") + { + REQUIRE( + symbol_table.lookup_ref("java::OpaqueInterface4").type.get_bool( + ID_incomplete_class)); + } + THEN("A static field 'OpaqueInterface4.x' should exist") + { + REQUIRE(symbol_table.has_symbol("java::OpaqueInterface4.x")); + } + THEN("No static field 'Test4.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test4.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test4.main should refer to OpaqueInterface4.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test4.main:()I").value, + "java::OpaqueInterface4.x")); + } + } + + WHEN("A class with two opaque parents uses an inherited static field 'x'") + { + symbol_tablet symbol_table= + load_java_class("Test5", "./java_bytecode/inherited_static_fields"); + THEN("Type OpaqueParent5 should be opaque") + { + REQUIRE( + symbol_table.lookup_ref("java::OpaqueParent5").type.get_bool( + ID_incomplete_class)); + } + THEN("Type OpaqueInterface5 should be opaque") + { + REQUIRE( + symbol_table.lookup_ref("java::OpaqueInterface5").type.get_bool( + ID_incomplete_class)); + } + THEN("One or other parent (not both) should gain a static field 'x'") + { + REQUIRE( + symbol_table.has_symbol("java::OpaqueInterface5.x") != + symbol_table.has_symbol("java::OpaqueParent5.x")); + } + THEN("No static field 'Test5.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test5.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test5.main should use either OpaqueParent5.x or OpaqueInterface5.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test5.main:()I").value, + "java::OpaqueInterface5.x") != + contains_symbol_reference( + symbol_table.lookup_ref("java::Test5.main:()I").value, + "java::OpaqueParent5.x")); + } + } + + WHEN("A class refers to a parent's protected static field") + { + symbol_tablet symbol_table= + load_java_class("Test6", "./java_bytecode/inherited_static_fields"); + THEN("A static field Parent6.x should exist") + { + REQUIRE(symbol_table.has_symbol("java::Parent6.x")); + } + THEN("No static field 'Test6.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test6.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test6.main should use Parent6.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test6.main:()I").value, + "java::Parent6.x")); + } + } + + WHEN("A class refers to an interface field " + "and its parent has an invisible package-private field of the same name") + { + symbol_tablet symbol_table= + load_java_class("Test7", "./java_bytecode/inherited_static_fields"); + THEN("A static field otherpackage.Parent7.x should exist") + { + REQUIRE(symbol_table.has_symbol("java::otherpackage.Parent7.x")); + } + THEN("A static field StaticInterface7.x should exist") + { + REQUIRE(symbol_table.has_symbol("java::StaticInterface7.x")); + } + THEN("No static field 'Test7.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test7.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test7.main should use StaticInterface7.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test7.main:()I").value, + "java::StaticInterface7.x")); + } + THEN("Test7.main should not use otherpackage.Parent7.x") + { + REQUIRE( + !contains_symbol_reference( + symbol_table.lookup_ref("java::Test7.main:()I").value, + "java::otherpackage.Parent7.x")); + } + } + + WHEN("A class refers to a parent's visible package-visibility field") + { + symbol_tablet symbol_table= + load_java_class("Test8", "./java_bytecode/inherited_static_fields"); + THEN("A static field Parent8.x should exist") + { + REQUIRE(symbol_table.has_symbol("java::Parent8.x")); + } + THEN("No static field 'Test8.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test8.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test8.main should use Parent8.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test8.main:()I").value, + "java::Parent8.x")); + } + } + + WHEN("A class refers to an interface field " + "and its parent has an invisible private field of the same name") + { + symbol_tablet symbol_table= + load_java_class("Test9", "./java_bytecode/inherited_static_fields"); + THEN("A static field Parent9.x should exist") + { + REQUIRE(symbol_table.has_symbol("java::Parent9.x")); + } + THEN("A static field StaticInterface9.x should exist") + { + REQUIRE(symbol_table.has_symbol("java::StaticInterface9.x")); + } + THEN("No static field 'Test9.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::Test9.x")); + } + THEN("No static field 'java.lang.Object.x' should be created") + { + REQUIRE(!symbol_table.has_symbol("java::java.lang.Object.x")); + } + THEN("Test9.main should use StaticInterface9.x") + { + REQUIRE( + contains_symbol_reference( + symbol_table.lookup_ref("java::Test9.main:()I").value, + "java::StaticInterface9.x")); + } + THEN("Test9.main should not use Parent9.x") + { + REQUIRE( + !contains_symbol_reference( + symbol_table.lookup_ref("java::Test9.main:()I").value, + "java::Parent9.x")); + } + } +} diff --git a/unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.class b/unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.class new file mode 100644 index 00000000000..2a6f3f58809 Binary files /dev/null and b/unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.class differ diff --git a/unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.java b/unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.java new file mode 100644 index 00000000000..6797032e006 --- /dev/null +++ b/unit/java_bytecode/inherited_static_fields/otherpackage/Parent7.java @@ -0,0 +1,5 @@ +package otherpackage; + +public class Parent7 { + static int x; // package visibility, should be invisible to Test7 +}