Skip to content

[TG-1157] New class for specialised generic class types. #1606

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 2 commits into from
Nov 23, 2017
Merged

[TG-1157] New class for specialised generic class types. #1606

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f390795
Add a class to represent specialised generic classes, and change conc…
NlightNFotis Nov 21, 2017
cbb2eff
Changes in the generics concretisation tests to correspond to the new…
NlightNFotis Nov 22, 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
36 changes: 21 additions & 15 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,20 @@
#include <java_bytecode/java_types.h>
#include <java_bytecode/java_utils.h>

/// 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.
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;
}

generate_java_generic_typet::generate_java_generic_typet(
message_handlert &message_handler):
message_handler(message_handler)
Expand Down Expand Up @@ -70,8 +84,8 @@ symbolt generate_java_generic_typet::operator()(
pre_modification_size==after_modification_size,
"All components in the original class should be in the new class");

const java_class_typet &new_java_class = construct_specialised_generic_type(
generic_class_definition, new_tag, replacement_components);
const java_specialized_generic_class_typet new_java_class =
construct_specialised_generic_type(new_tag, replacement_components);
const type_symbolt &class_symbol =
build_symbol_from_specialised_class(new_java_class);

Expand Down Expand Up @@ -193,14 +207,14 @@ irep_idt generate_java_generic_typet::build_generic_tag(
.generic_type_arguments())
{
if(!first)
new_tag_buffer << ",";
new_tag_buffer << ", ";
first=false;

INVARIANT(
!is_java_generic_parameter(type_argument),
"Only create full concretized generic types");
const irep_idt &id(id2string(type_argument.subtype().get(ID_identifier)));
new_tag_buffer << id2string(id);
new_tag_buffer << pretty_print_java_type(id2string(id));
if(is_java_array_tag(id))
{
const typet &element_type =
Expand All @@ -224,25 +238,17 @@ irep_idt generate_java_generic_typet::build_generic_tag(
return new_tag_buffer.str();
}

/// Build the specalised version of the specific class, with the specified
/// Build the specialised version of the specific class, with the specified
/// parameters and name.
/// \param generic_class_definition: The generic class we are specialising
/// \param new_tag: The new name for the class (like Generic<java::Float>)
/// \param new_components: The specialised components
/// \return The newly constructed class.
java_class_typet
java_specialized_generic_class_typet
generate_java_generic_typet::construct_specialised_generic_type(
Copy link
Contributor

Choose a reason for hiding this comment

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

Minor nit (non-blocking): We're getting quite a mix of specialised and specialized now, e.g. both spellings in the same function signature here. Ideally we'd clean this up, but if you don't clean it up in this PR, please raise a technical debt issue to review all the generics work and cleanup the naming in functions/comments/etc.

const java_generic_class_typet &generic_class_definition,
const irep_idt &new_tag,
const struct_typet::componentst &new_components) const
{
java_class_typet specialised_class = generic_class_definition;
// We are specialising the logic - so we don't want to be marked as generic
specialised_class.set(ID_C_java_generics_class_type, false);
specialised_class.set(ID_name, "java::" + id2string(new_tag));
specialised_class.set(ID_base_name, new_tag);
specialised_class.components() = new_components;
return specialised_class;
return java_specialized_generic_class_typet{new_tag, new_components};
}

/// Construct the symbol to be moved into the symbol table
Expand Down
3 changes: 1 addition & 2 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 @@ -33,8 +33,7 @@ class generate_java_generic_typet
const java_generic_class_typet &replacement_type,
const java_generic_typet &generic_reference) const;

java_class_typet construct_specialised_generic_type(
const java_generic_class_typet &generic_class_definition,
java_specialized_generic_class_typet construct_specialised_generic_type(
const irep_idt &new_tag,
const struct_typet::componentst &new_components) const;

Expand Down
51 changes: 51 additions & 0 deletions src/java_bytecode/java_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -374,4 +374,55 @@ void get_dependencies_from_generic_parameters(
const typet &,
std::set<irep_idt> &);

class java_specialized_generic_class_typet : public java_class_typet
{
public:
/// Build the specialised version of the specific class, with the specified
/// parameters and name.
/// \param new_tag: The new name for the class (like Generic<java::Float>)
/// \param new_components: The specialised components
/// \return The newly constructed class.
java_specialized_generic_class_typet(
const irep_idt &new_tag,
const struct_typet::componentst &new_components)
{
set(ID_C_specialized_generic_java_class, true);
// We are specialising the logic - so we don't want to be marked as generic
set(ID_C_java_generics_class_type, false);
set(ID_name, "java::" + id2string(new_tag));
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggest not using name, which is a bit vague. How about ID_java_generic_tag or something?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I think this should be staying like this. The point is it should be creating symbols that look a little bit like this:

  0: struct
      * name: java::reifiedArrayNB<java::java.lang.Float>
      * tag: reifiedArrayNB
      * base_name: reifiedArrayNB<java::java.lang.Float>
      * components:

set(ID_base_name, id2string(new_tag));
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggest not storing this redundant info unless you really need to

Copy link
Contributor Author

Choose a reason for hiding this comment

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

My understanding of the specification (and the implementation of generics thus far) is that all of the base_name, name and tag are needed.

components() = new_components;
const std::string &class_tag = id2string(new_tag);
set_tag(class_tag.substr(0, class_tag.find('<')));
Copy link
Contributor

Choose a reason for hiding this comment

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

Are you sure multiple distinct types with matching tags is okay?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It is my understanding that for a type GenericWrapper<IWrapper> the tag of the class should always be GenericWrapper. That's what I have understood from discussions with @thk123 . I suggest we leave it as it is for now, as I don't have access to the specification and I don't want to make a change against the specification at this point.

Copy link
Contributor

Choose a reason for hiding this comment

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

@smowton this is the case we have currently, I am not aware of any problems, AFAIK the idea is still that the use of generics should be transparent for non-generics aware code

}
};

inline bool is_java_specialized_generic_class_type(const typet &type)
{
return type.get_bool(ID_C_specialized_generic_java_class);
}

inline bool is_java_specialized_generic_class_type(typet &type)
{
return type.get_bool(ID_C_specialized_generic_java_class);
}

inline java_specialized_generic_class_typet
to_java_specialized_generic_class_type(const typet &type)
{
INVARIANT(
is_java_specialized_generic_class_type(type),
"Tried to convert a type that was not a specialised generic java class");
return static_cast<const java_specialized_generic_class_typet &>(type);
}

inline java_specialized_generic_class_typet
to_java_specialized_generic_class_type(typet &type)
{
INVARIANT(
is_java_specialized_generic_class_type(type),
"Tried to convert a type that was not a specialised generic java class");
return static_cast<const java_specialized_generic_class_typet &>(type);
}

#endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H
1 change: 1 addition & 0 deletions src/util/irep_ids.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -830,6 +830,7 @@ IREP_ID_ONE(integer_dereference)
IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter)
IREP_ID_TWO(C_java_generic_type, #java_generic_type)
IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
IREP_ID_TWO(C_specialized_generic_java_class, #specialized_generic_java_class)
IREP_ID_TWO(generic_types, #generic_types)
IREP_ID_TWO(type_variables, #type_variables)
IREP_ID_ONE(havoc_object)
Expand Down
24 changes: 9 additions & 15 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 @@ -40,8 +40,7 @@ SCENARIO(
"generate_java_generic_type_from_file",
"[core][java_bytecode][generate_java_generic_type]")
{
auto expected_symbol=
"java::generic_two_fields$bound_element<java::java.lang.Integer>";
auto expected_symbol = "java::generic_two_fields$bound_element<Integer>";

GIVEN("A generic java type with two generic fields and a concrete "
"substitution")
Expand All @@ -56,8 +55,8 @@ SCENARIO(
REQUIRE(new_symbol_table.has_symbol(expected_symbol));
THEN("The class should contain two instantiated fields.")
{
const auto &class_symbol=new_symbol_table.lookup(
"java::generic_two_fields$bound_element<java::java.lang.Integer>");
const auto &class_symbol = new_symbol_table.lookup(
"java::generic_two_fields$bound_element<Integer>");
const typet &symbol_type=class_symbol->type;

REQUIRE(symbol_type.id()==ID_struct);
Expand Down Expand Up @@ -89,10 +88,8 @@ SCENARIO(
"generate_java_generic_type_from_file_two_params",
"[core][java_bytecode][generate_java_generic_type]")
{
auto expected_symbol=
"java::generic_two_parameters$KeyValuePair"
"<java::java.lang.String,"
"java::java.lang.Integer>";
auto expected_symbol =
"java::generic_two_parameters$KeyValuePair<String, Integer>";

GIVEN("A generic java type with two generic parameters, like a Hashtable")
{
Expand Down Expand Up @@ -133,10 +130,8 @@ SCENARIO(
// After we have loaded the class and converted the generics,
// the presence of these two symbols in the symbol table is
// proof enough that we did the work we needed to do correctly.
auto first_expected_symbol=
"java::generic_two_instances$element<java::java.lang.Boolean>";
auto second_expected_symbol=
"java::generic_two_instances$element<java::java.lang.Integer>";
auto first_expected_symbol = "java::generic_two_instances$element<Boolean>";
auto second_expected_symbol = "java::generic_two_instances$element<Integer>";

GIVEN("A generic java type with a field that refers to another generic with"
" an uninstantiated parameter.")
Expand Down Expand Up @@ -284,9 +279,8 @@ SCENARIO(
"There should be a specialised version of the class in the symbol "
"table")
{
const irep_idt specialised_class_name = id2string(harness_class) + "$" +
id2string(inner_class) +
"<java::java.lang.Float>";
const irep_idt specialised_class_name =
id2string(harness_class) + "$" + id2string(inner_class) + "<Float>";
REQUIRE(new_symbol_table.has_symbol(specialised_class_name));

const symbolt test_class_symbol =
Expand Down