From 7d37272eec1f9ea536e737f4720d8f5ad48ca74a Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Thu, 23 Nov 2017 14:54:35 +0000 Subject: [PATCH 1/3] Fix the pretty printing routine to pp types that have java:: as their prefix only --- src/java_bytecode/generate_java_generic_type.cpp | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 32164a382cf..706200982a9 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -21,11 +21,17 @@ // qualifiers, or the type as it was passed otherwise. static std::string pretty_print_java_type(const std::string &fqn_java_type) { - const std::string java_lang("java::java.lang."); - const std::string package_name(java_class_to_package(fqn_java_type) + "."); - if(package_name == java_lang) - return fqn_java_type.substr(java_lang.length()); - return fqn_java_type; + std::string result; + const std::string java_cbmc_string("java::"); + // Remove the java internal cbmc identifier + if(fqn_java_type.substr(0, java_cbmc_string.length()) == java_cbmc_string) + result = fqn_java_type.substr(java_cbmc_string.length()); + // If the remaining has the "java.lang." string as well, trim it + const std::string java_lang_string("java.lang."); + const std::string package_name(java_class_to_package(result) + "."); + if(package_name == java_lang_string) + result = result.substr(java_lang_string.length()); + return result; } generate_java_generic_typet::generate_java_generic_typet( From 0a0fa08d16d6ade37f3e8af829739c210502859d Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 24 Nov 2017 14:22:46 +0000 Subject: [PATCH 2/3] Fixed the pretty printing type function and fix the tests failing, and introduce test for the pretty printing function. --- .../generate_java_generic_type.cpp | 13 +++--- .../generate_java_generic_type.h | 2 + .../generate_java_generic_type.cpp | 42 ++++++++++++++++--- 3 files changed, 46 insertions(+), 11 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 706200982a9..fa02cc9c459 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -11,6 +11,7 @@ #include "generate_java_generic_type.h" #include +#include #include #include @@ -19,17 +20,17 @@ /// \param fqn_java_type The java type we want to pretty print. /// \return The pretty printed type if there was a match of the // qualifiers, or the type as it was passed otherwise. -static std::string pretty_print_java_type(const std::string &fqn_java_type) +std::string pretty_print_java_type(const std::string &fqn_java_type) { - std::string result; + std::string result(fqn_java_type); const std::string java_cbmc_string("java::"); // Remove the java internal cbmc identifier - if(fqn_java_type.substr(0, java_cbmc_string.length()) == java_cbmc_string) + if(has_prefix(fqn_java_type, java_cbmc_string)) result = fqn_java_type.substr(java_cbmc_string.length()); - // If the remaining has the "java.lang." string as well, trim it + // If the class is in package java.lang strip + // package name due to default import const std::string java_lang_string("java.lang."); - const std::string package_name(java_class_to_package(result) + "."); - if(package_name == java_lang_string) + if(has_prefix(result, java_lang_string)) result = result.substr(java_lang_string.length()); return result; } diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 5c01756f1b2..6ffe428b6bb 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -43,4 +43,6 @@ class generate_java_generic_typet message_handlert &message_handler; }; +std::string pretty_print_java_type(const std::string &fqn_java_type); + #endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index de216862376..b6e813c39a2 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -7,6 +7,9 @@ \*******************************************************************/ +#include +#include + #include #include #include @@ -179,7 +182,7 @@ SCENARIO( // We want to test that the specialized/instantiated class has it's field // type updated, so find the specialized class, not the generic class. const irep_idt test_class = - "java::generic_field_array_instantiation$generic"; GIVEN("A generic type instantiated with an array type") @@ -224,15 +227,15 @@ SCENARIO( GIVEN("A generic type instantiated with different array types") { const irep_idt test_class_integer = - "java::generic_field_array_instantiation$generic"; const irep_idt test_class_int = - "java::generic_field_array_instantiation$generic"; + "java::generic_field_array_instantiation$generic"; const irep_idt test_class_float = - "java::generic_field_array_instantiation$generic"; + "java::generic_field_array_instantiation$generic"; const struct_typet::componentt &component_g = require_type::require_component( @@ -330,7 +333,7 @@ SCENARIO( "table") { const std::string specialised_string = - ""; const irep_idt specialised_class_name = id2string(harness_class) + "$" + id2string(inner_class) + @@ -389,3 +392,32 @@ SCENARIO( } } } + +SCENARIO( + "Test pretty printing auxiliary function", + "[core][java_bytecode][generate_java_generic_type]") +{ + using std::map; + using std::string; + + WHEN("We have a series of cbmc internal java types") + { + // NOLINTNEXTLINE + const map types{ + // map + {"java::java.lang.Integer", "Integer"}, + {"java::CustomClass", "CustomClass"}, + {"java.lang.String", "String"}, + {"Hashmap", "Hashmap"}, + // We shouldn't prune types not imported in default import + {"java.util.HashSet", "java.util.HashSet"}}; + + THEN("We need to make sure that the types get pruned correctly.") + { + for(const auto &pair : types) + { + REQUIRE(pretty_print_java_type(pair.first) == pair.second); + } + } + } +} From 8a9aa0fb53a33e143cb61534efcefa8beb94fe6f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 24 Nov 2017 16:15:23 +0000 Subject: [PATCH 3/3] Move the pretty printing function from generate_java_generic_type to java_utils. --- .../generate_java_generic_type.cpp | 21 -------------- .../generate_java_generic_type.h | 2 -- src/java_bytecode/java_utils.cpp | 20 +++++++++++++ src/java_bytecode/java_utils.h | 2 ++ .../generate_java_generic_type.cpp | 29 ------------------- unit/java_bytecode/java_utils_test.cpp | 27 +++++++++++++++++ 6 files changed, 49 insertions(+), 52 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index fa02cc9c459..1cc35143fa9 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -11,30 +11,9 @@ #include "generate_java_generic_type.h" #include -#include #include #include -/// Strip the package name from a java type, for the type to be -/// pretty printed (java::java.lang.Integer -> Integer). -/// \param fqn_java_type The java type we want to pretty print. -/// \return The pretty printed type if there was a match of the -// qualifiers, or the type as it was passed otherwise. -std::string pretty_print_java_type(const std::string &fqn_java_type) -{ - std::string result(fqn_java_type); - const std::string java_cbmc_string("java::"); - // Remove the java internal cbmc identifier - if(has_prefix(fqn_java_type, java_cbmc_string)) - result = fqn_java_type.substr(java_cbmc_string.length()); - // If the class is in package java.lang strip - // package name due to default import - const std::string java_lang_string("java.lang."); - if(has_prefix(result, java_lang_string)) - result = result.substr(java_lang_string.length()); - return result; -} - generate_java_generic_typet::generate_java_generic_typet( message_handlert &message_handler): message_handler(message_handler) diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 6ffe428b6bb..5c01756f1b2 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -43,6 +43,4 @@ class generate_java_generic_typet message_handlert &message_handler; }; -std::string pretty_print_java_type(const std::string &fqn_java_type); - #endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index f720d32ada8..0021bff9325 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -305,3 +305,23 @@ irep_idt strip_java_namespace_prefix(const irep_idt &to_strip) PRECONDITION(has_prefix(to_strip_str, prefix)); return to_strip_str.substr(prefix.size(), std::string::npos); } + +/// Strip the package name from a java type, for the type to be +/// pretty printed (java::java.lang.Integer -> Integer). +/// \param fqn_java_type The java type we want to pretty print. +/// \return The pretty printed type if there was a match of the +// qualifiers, or the type as it was passed otherwise. +std::string pretty_print_java_type(const std::string &fqn_java_type) +{ + std::string result(fqn_java_type); + const std::string java_cbmc_string("java::"); + // Remove the CBMC internal java identifier + if(has_prefix(fqn_java_type, java_cbmc_string)) + result = fqn_java_type.substr(java_cbmc_string.length()); + // If the class is in package java.lang strip + // package name due to default import + const std::string java_lang_string("java.lang."); + if(has_prefix(result, java_lang_string)) + result = result.substr(java_lang_string.length()); + return result; +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 6f163df484f..ad4c45f51c0 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -94,4 +94,6 @@ exprt make_function_application( irep_idt strip_java_namespace_prefix(const irep_idt &to_strip); +std::string pretty_print_java_type(const std::string &fqn_java_type); + #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index b6e813c39a2..f4b8625ceec 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -392,32 +392,3 @@ SCENARIO( } } } - -SCENARIO( - "Test pretty printing auxiliary function", - "[core][java_bytecode][generate_java_generic_type]") -{ - using std::map; - using std::string; - - WHEN("We have a series of cbmc internal java types") - { - // NOLINTNEXTLINE - const map types{ - // map - {"java::java.lang.Integer", "Integer"}, - {"java::CustomClass", "CustomClass"}, - {"java.lang.String", "String"}, - {"Hashmap", "Hashmap"}, - // We shouldn't prune types not imported in default import - {"java.util.HashSet", "java.util.HashSet"}}; - - THEN("We need to make sure that the types get pruned correctly.") - { - for(const auto &pair : types) - { - REQUIRE(pretty_print_java_type(pair.first) == pair.second); - } - } - } -} diff --git a/unit/java_bytecode/java_utils_test.cpp b/unit/java_bytecode/java_utils_test.cpp index b568b8c6d01..3f3c7e603a6 100644 --- a/unit/java_bytecode/java_utils_test.cpp +++ b/unit/java_bytecode/java_utils_test.cpp @@ -341,3 +341,30 @@ SCENARIO("find_closing_semi_colon_for_reference_type", "[core][java_util_test]") REQUIRE(find_closing_semi_colon_for_reference_type(descriptor, 10) == 19); } } + +SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]") +{ + using std::map; + using std::string; + + WHEN("We have a series of cbmc internal java types") + { + // NOLINTNEXTLINE + const map types{ + // map + {"java::java.lang.Integer", "Integer"}, + {"java::CustomClass", "CustomClass"}, + {"java.lang.String", "String"}, + {"Hashmap", "Hashmap"}, + // We shouldn't prune types not imported in default import + {"java.util.HashSet", "java.util.HashSet"}}; + + THEN("We need to make sure that the types get pruned correctly.") + { + for(const auto &pair : types) + { + REQUIRE(pretty_print_java_type(pair.first) == pair.second); + } + } + } +}