Skip to content

[TG-1157] Fix pretty printing routine #1617

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Nov 27, 2017
Merged

[TG-1157] Fix pretty printing routine #1617

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
7d37272
Fix the pretty printing routine to pp types that have java:: as their…
NlightNFotis Nov 23, 2017
0a0fa08
Fixed the pretty printing type function and fix the tests failing, an…
NlightNFotis Nov 24, 2017
8a9aa0f
Move the pretty printing function from generate_java_generic_type to …
NlightNFotis Nov 24, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 13 additions & 6 deletions src/java_bytecode/generate_java_generic_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@

#include "generate_java_generic_type.h"
#include <util/namespace.h>
#include <util/prefix.h>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One more tiny nit that just sprung to mind (sorry!) Now. that the function has been moved out of this file, probably this include is not needed anymore either...

#include <java_bytecode/java_types.h>
#include <java_bytecode/java_utils.h>

Expand All @@ -19,13 +20,19 @@
/// \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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given that this pretty print function doesn't appear to do anything in anyway specific to Java generics, should it perhaps be moved into java_bytecode/java_utils.cpp/.h ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was just done.

{
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(fqn_java_type);
const std::string java_cbmc_string("java::");
// Remove the java internal cbmc identifier
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: This should probably be Remove the CBMC internal java identifier

if(has_prefix(fqn_java_type, java_cbmc_string))
result = fqn_java_type.substr(java_cbmc_string.length());
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

use has_prefix from util here

// 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(
Expand Down
2 changes: 2 additions & 0 deletions src/java_bytecode/generate_java_generic_type.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
42 changes: 37 additions & 5 deletions unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,9 @@

\*******************************************************************/

#include <map>
#include <string>

#include <testing-utils/catch.hpp>
#include <testing-utils/load_java_class.h>
#include <testing-utils/require_type.h>
Expand Down Expand Up @@ -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<java::array[reference]"
"java::generic_field_array_instantiation$generic<array[reference]"
"of_java::java.lang.Float>";

GIVEN("A generic type instantiated with an array type")
Expand Down Expand Up @@ -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<java::array[reference]"
"java::generic_field_array_instantiation$generic<array[reference]"
"of_"
"java::java.lang.Integer>";

const irep_idt test_class_int =
"java::generic_field_array_instantiation$generic<java::array[int]>";
"java::generic_field_array_instantiation$generic<array[int]>";

const irep_idt test_class_float =
"java::generic_field_array_instantiation$generic<java::array[float]>";
"java::generic_field_array_instantiation$generic<array[float]>";

const struct_typet::componentt &component_g =
require_type::require_component(
Expand Down Expand Up @@ -330,7 +333,7 @@ SCENARIO(
"table")
{
const std::string specialised_string =
"<java::array[reference]of_"
"<array[reference]of_"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

should the java:: prefix in the generic type argument disappear, too?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No because if it does, the tests fail.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That doesn't feel like a terribly satisfactory answer :-) Like @mgudemann I'd have expected all the java:: prefixes to need to disappear too - but I assume that making that prefix disappear (if desired) is a different piece of work to this PR?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Due to the change to the pretty print function that is being used, the java:: prefixes are only pruned if they are in the beginning of a string.

These array[reference]of_<something> are being manifest in the goto functions to my understanding, and not in the tests generated, and at the point of their removal, they are just strings. This means that to remove all java:: prefixes in a type, you would do it one of the two ways:

  1. either intercept sooner, when it's still a typet and recursively convert the type, or
  2. some regex magic on the strings, along with some rewriting.

Since these strings are not manifest in the tests we generate, and appear relatively harmless, I think it's outside the scope of this task to investigate exactly how and where to change them.

"java::java.lang.Float>";
const irep_idt specialised_class_name = id2string(harness_class) + "$" +
id2string(inner_class) +
Expand Down Expand Up @@ -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<string, string> types{
// map<Input, Output>
{"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);
}
}
}
}