From 331e0bc95ae50007e3923e3d25dc348054be4d8c Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Tue, 17 Sep 2019 18:01:56 +0100 Subject: [PATCH] Add unit tests for preserving meta-information of excluded methods These unit tests complement the regression tests in jbmc/regression/jbmc/context-include-exclude that were added in a previous commit to check for properties of excluded methods. Some properties, like information about accessibility and final and static status, is easier to check in unit-style tests. --- jbmc/unit/Makefile | 1 + .../ClassWithDifferentModifiers.class | Bin 0 -> 977 bytes .../ClassWithDifferentModifiers.java | 18 ++++ .../context_excluded.cpp | 98 ++++++++++++++++++ 4 files changed, 117 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_language/context_excluded.cpp diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 5a9966ece1..4d9cc0dba9 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -22,6 +22,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_convert_method/convert_method.cpp \ java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp \ java_bytecode/java_bytecode_language/language.cpp \ + java_bytecode/java_bytecode_language/context_excluded.cpp \ java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \ java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class b/jbmc/unit/java_bytecode/java_bytecode_language/ClassWithDifferentModifiers.class new file mode 100644 index 0000000000000000000000000000000000000000..47961b187b575aec3a03fcb564fabe92406308eb GIT binary patch literal 977 zcmaJ;O>fgc5Pj>|apJf%UkxUuNeczi2I!@ns1T^3Qbh_#K~$8JV{gh9*GBfHKc*MB zap3|;Eus?K`ArBhYnmp?0Uu`Pip7yDIWqpsYB z7o01wdeJcU_?A$77dHcvyes6Jju;Gh%tN^o`C=e=oZM9kY|Ns_F#jK%jTv0BaTyMS zGgkd*w93bE9K|-Sz_C$RW*&}-RU2*GW+;w3p7jq%6s>ifN`FiH^m!s;?qAGQx`s)* zr#&pu6>YjaD>{k_c_wHIieyU^Ezry8HC9i-J}V%~WV30KA&&~G + +#include + +#include +#include + +SCENARIO( + "Exclude a method using context-include/exclude", + "[core][java_bytecode][java_bytecode_language]") +{ + GIVEN("A class with all methods excluded except for main") + { + const symbol_tablet symbol_table = + load_goto_model_from_java_class( + "ClassWithDifferentModifiers", + "./java_bytecode/java_bytecode_language", + {}, + {{"context-include", "ClassWithDifferentModifiers.main"}}) + .get_symbol_table(); + + WHEN("Converting the methods of this class") + { + const auto public_instance_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testPublicInstance:()I"); + REQUIRE(public_instance_symbol); + const auto public_instance_type = + type_try_dynamic_cast(public_instance_symbol->type); + + const auto private_static_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testPrivateStatic:()I"); + REQUIRE(private_static_symbol); + const auto private_static_type = + type_try_dynamic_cast(private_static_symbol->type); + + const auto protected_final_instance_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testProtectedFinalInstance:()I"); + REQUIRE(protected_final_instance_symbol); + const auto protected_final_instance_type = + type_try_dynamic_cast( + protected_final_instance_symbol->type); + + const auto default_final_static_symbol = symbol_table.lookup( + "java::ClassWithDifferentModifiers.testDefaultFinalStatic:()I"); + REQUIRE(default_final_static_symbol); + const auto default_final_static_type = + type_try_dynamic_cast( + default_final_static_symbol->type); + THEN( + "Symbol values for excluded methods are nil as the lazy_goto_modelt " + "for unit tests does not generate stub/exclude bodies.") + { + REQUIRE(public_instance_symbol->value.is_nil()); + REQUIRE(private_static_symbol->value.is_nil()); + REQUIRE(protected_final_instance_symbol->value.is_nil()); + REQUIRE(default_final_static_symbol->value.is_nil()); + } + THEN( + "Types of excluded methods are stored as java_method_typets in the " + "symbol table.") + { + REQUIRE(public_instance_type); + REQUIRE(private_static_type); + REQUIRE(protected_final_instance_type); + REQUIRE(default_final_static_type); + } + THEN("Access modifiers of excluded methods are preserved.") + { + REQUIRE(public_instance_type->get_access() == ID_public); + REQUIRE(private_static_type->get_access() == ID_private); + REQUIRE(protected_final_instance_type->get_access() == ID_protected); + REQUIRE(default_final_static_type->get_access() == ID_default); + } + THEN("Static/Instance meta-information of excluded methods is preserved.") + { + REQUIRE_FALSE(public_instance_type->get_bool(ID_is_static)); + REQUIRE(private_static_type->get_bool(ID_is_static)); + REQUIRE_FALSE(protected_final_instance_type->get_bool(ID_is_static)); + REQUIRE(default_final_static_type->get_bool(ID_is_static)); + } + THEN("Final/Non-final meta-information of excluded methods is preserved.") + { + REQUIRE_FALSE(public_instance_type->get_is_final()); + REQUIRE_FALSE(private_static_type->get_is_final()); + REQUIRE(protected_final_instance_type->get_is_final()); + REQUIRE(default_final_static_type->get_is_final()); + } + } + } +}