Skip to content

[TG-2478] Make Bootstrap methods available in method/instruction conversion #1937

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 12 commits into from
Mar 27, 2018
Merged

[TG-2478] Make Bootstrap methods available in method/instruction conversion #1937

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
0a49697
Store bootstrap method index for invokedynamic instructions
Mar 13, 2018
37afd9a
Store the full method reference of lambda method handles
Mar 13, 2018
a518393
Introduce lambda method handles in java class type
Mar 12, 2018
bf04c93
Add lambda method handles during class conversion
Mar 12, 2018
a8ac3d4
Pass lambda method handles to method instruction conversion
Mar 12, 2018
078dc0f
Updating a utility function
Mar 19, 2018
3585f73
Updating unit tests for parsing lambda method table
Mar 19, 2018
844bb20
Pulling out a utility function to a separate file
Mar 19, 2018
8b172b4
Adding a utility function for lambda method handles in struct
Mar 19, 2018
823f2a7
Adding a unit test for lambda method handles in class symbol
Mar 19, 2018
d57fe53
Renaming the folder with lambda unit tests
Mar 26, 2018
212da75
Making members of a test utility class non-const
Mar 26, 2018
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
12 changes: 12 additions & 0 deletions src/java_bytecode/java_bytecode_convert_class.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -310,6 +310,18 @@ void java_bytecode_convert_classt::convert(const classt &c)
}
}

// now do lambda method handles (bootstrap methods)
for(const auto &lambda_entry : c.lambda_method_handle_map)
{
// if the handle is of unknown type, we still need to store it to preserve
// the correct indexing (invokedynamic instructions will retrieve
// method handles by index)
lambda_entry.second.is_unknown_handle()
? class_type.add_unknown_lambda_method_handle()
: class_type.add_lambda_method_handle(
"java::" + id2string(lambda_entry.second.lambda_method_ref));
}

// produce class symbol
symbolt new_symbol;
new_symbol.base_name=c.name;
Expand Down
42 changes: 39 additions & 3 deletions src/java_bytecode/java_bytecode_convert_method.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,25 @@ code_typet member_type_lazy(
return to_code_type(member_type_from_descriptor);
}

/// Retrieves the symbol of the lambda method associated with the given
/// lambda method handle (bootstrap method).
/// \param lambda_method_handles Vector of lambda method handles (bootstrap
/// methods) of the class where the lambda is called
/// \param index Index of the lambda method handle in the vector
/// \return Symbol of the lambda method if the method handle does not have an
Copy link
Contributor

Choose a reason for hiding this comment

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

"... does not have an unknown ..." maybe better "... have a known ..." ?

/// unknown type
optionalt<symbolt> java_bytecode_convert_methodt::get_lambda_method_symbol(
const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
const size_t &index)
Copy link
Contributor

Choose a reason for hiding this comment

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

index should be passed by value

{
const symbol_exprt &lambda_method_handle = lambda_method_handles.at(index);
// If the lambda method handle has an unknown type, it does not refer to
// any symbol (it is a symbol expression with empty identifier)
if(!lambda_method_handle.get_identifier().empty())
return symbol_table.lookup_ref(lambda_method_handle.get_identifier());
return {};
}

/// This creates a method symbol in the symtab, but doesn't actually perform
/// method conversion just yet. The caller should call
/// java_bytecode_convert_method later to give the symbol/method a body.
Expand Down Expand Up @@ -555,7 +574,11 @@ void java_bytecode_convert_methodt::convert(
current_method=method_symbol.name;
method_has_this=code_type.has_this();
if((!m.is_abstract) && (!m.is_native))
method_symbol.value=convert_instructions(m, code_type, method_symbol.name);
method_symbol.value = convert_instructions(
m,
code_type,
method_symbol.name,
to_java_class_type(class_symbol.type).lambda_method_handles());
}

const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info(
Expand Down Expand Up @@ -926,7 +949,8 @@ static unsigned get_bytecode_type_width(const typet &ty)
codet java_bytecode_convert_methodt::convert_instructions(
const methodt &method,
const code_typet &method_type,
const irep_idt &method_name)
const irep_idt &method_name,
const java_class_typet::java_lambda_method_handlest &lambda_method_handles)
{
const instructionst &instructions=method.instructions;

Expand Down Expand Up @@ -1211,7 +1235,19 @@ codet java_bytecode_convert_methodt::convert_instructions(
else if(statement=="invokedynamic")
{
// not used in Java
code_typet &code_type=to_code_type(arg0.type());
code_typet &code_type = to_code_type(arg0.type());

const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
lambda_method_handles,
code_type.get_int(ID_java_lambda_method_handle_index));
if(lambda_method_symbol.has_value())
debug() << "Converting invokedynamic for lambda: "
<< lambda_method_symbol.value().name << eom;
else
debug() << "Converting invokedynamic for lambda with unknown handle "
"type"
<< eom;

const code_typet::parameterst &parameters(code_type.parameters());

pop(parameters.size());
Expand Down
7 changes: 6 additions & 1 deletion src/java_bytecode/java_bytecode_convert_method_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -235,13 +235,18 @@ class java_bytecode_convert_methodt:public messaget
const address_mapt &amap,
bool allow_merge=true);

optionalt<symbolt> get_lambda_method_symbol(
const java_class_typet::java_lambda_method_handlest &lambda_method_handles,
const size_t &index);

// conversion
void convert(const symbolt &class_symbol, const methodt &);

codet convert_instructions(
const methodt &,
const code_typet &,
const irep_idt &);
const irep_idt &,
const java_class_typet::java_lambda_method_handlest &);

const bytecode_infot &get_bytecode_info(const irep_idt &statement);

Expand Down
6 changes: 6 additions & 0 deletions src/java_bytecode/java_bytecode_parse_tree.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,7 @@ class java_bytecode_parse_treet
public:
method_handle_typet handle_type;
irep_idt lambda_method_name;
irep_idt lambda_method_ref;
irep_idt interface_type;
irep_idt method_type;
u2_valuest u2_values;
Expand All @@ -204,6 +205,11 @@ class java_bytecode_parse_treet
lambda_method_handle.u2_values = std::move(params);
return lambda_method_handle;
}

bool is_unknown_handle() const
{
return handle_type == method_handle_typet::UNKNOWN_HANDLE;
}
};

// TODO(tkiley): This map shouldn't be interacted with directly (instead
Expand Down
6 changes: 4 additions & 2 deletions src/java_bytecode/java_bytecode_parser.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -843,6 +843,7 @@ void java_bytecode_parsert::rconstant_pool()
it->expr.id("invokedynamic");
const pool_entryt &nameandtype_entry=pool_entry(it->ref2);
typet type=type_entry(nameandtype_entry.ref2);
type.set(ID_java_lambda_method_handle_index, it->ref1);
it->expr.type()=type;
}
break;
Expand Down Expand Up @@ -1776,9 +1777,9 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
const name_and_type_infot &name_and_type =
ref_entry.get_name_and_type(pool_entry_lambda);

const std::string method_name =
const std::string method_ref =
class_entry.get_name(pool_entry_lambda) + "." +
name_and_type.get_name(pool_entry_lambda) +
name_and_type.get_name(pool_entry_lambda) + ':' +
name_and_type.get_descriptor(pool_entry_lambda);

lambda_method_handlet lambda_method_handle;
Expand All @@ -1791,6 +1792,7 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
// "new" when it is a class variable, instantiated in <init>
lambda_method_handle.lambda_method_name =
name_and_type.get_name(pool_entry_lambda);
lambda_method_handle.lambda_method_ref = method_ref;
Copy link
Contributor

Choose a reason for hiding this comment

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

could be a std::move

lambda_method_handle.handle_type =
method_handle_typet::LAMBDA_METHOD_HANDLE;

Expand Down
25 changes: 25 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 @@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
#include <util/std_types.h>
#include <util/c_types.h>
#include <util/optional.h>
#include <util/std_expr.h>

class java_class_typet:public class_typet
{
Expand All @@ -30,6 +31,30 @@ class java_class_typet:public class_typet
{
return set(ID_access, access);
}

typedef std::vector<symbol_exprt> java_lambda_method_handlest;

const java_lambda_method_handlest &lambda_method_handles() const
{
return (const java_lambda_method_handlest &)find(
ID_java_lambda_method_handles)
.get_sub();
}

java_lambda_method_handlest &lambda_method_handles()
{
return (java_lambda_method_handlest &)add(ID_java_lambda_method_handles)
.get_sub();
}

void add_lambda_method_handle(const irep_idt &identifier)
{
lambda_method_handles().emplace_back(identifier);
Copy link
Contributor

@thomasspriggs thomasspriggs Mar 22, 2018 •
edited
Loading

Choose a reason for hiding this comment

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

This doesn't appear to be quite right, due to the mix an match of move semantics and const references. My understanding is that emplace_back will move its parameter into the vector, leaving the original copy it was passed in, in an invalid/undefined state. However the type of identifier is const reference, which means we are promising not to update it.

Copy link
Author

Choose a reason for hiding this comment

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

emplace_back takes arguments to pass to the constructor of the vector type (in this case const irep_idt &identifier as an input to symbol_exprt constructor):
http://en.cppreference.com/w/cpp/container/vector/emplace_back
I don't think the identifier is left in an invalid/undefined state, maybe the original copy of symbol_exprt that is moved to the vector? Although the above source says that the new element is constructed 'in-place at the location provided by the container'

Copy link
Contributor

Choose a reason for hiding this comment

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

Ok, thank you for explaining how this works, I was wondering where the conversion from irep_idt to symbol_exprt was happening. I had previously been reading about && as part of move semantics. Why is the type of the identifier parameter not irep_idt &&identifier to match the type needed by emplace_back?

Copy link
Contributor

Choose a reason for hiding this comment

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

emplace_back and std::move are different things, with similar aims. emplace_back just tries to avoid constructing a temporary object to pass as an argument, copy-constructing an object to go in the collection, and then destructing the original temporary. It can only be used to create a new object, but it does it directly in the place it's needed.

}
void add_unknown_lambda_method_handle()
{
lambda_method_handles().emplace_back();
Copy link
Contributor

Choose a reason for hiding this comment

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

could you please add a comment that explains why this works? I imagine it is because UNKNOWN is the default

}
};

inline const java_class_typet &to_java_class_type(const typet &type)
Expand Down
2 changes: 2 additions & 0 deletions src/util/irep_ids.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -836,6 +836,8 @@ IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol)
IREP_ID_TWO(generic_types, #generic_types)
IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
IREP_ID_TWO(type_variables, #type_variables)
IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)
IREP_ID_TWO(java_lambda_method_handles, lambda_method_handles)
IREP_ID_ONE(havoc_object)
IREP_ID_TWO(overflow_shl, overflow-shl)
IREP_ID_TWO(C_no_initialization_required, #no_initialization_required)
Expand Down
2 changes: 2 additions & 0 deletions unit/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,8 @@ SRC += unit_tests.cpp \
java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \
java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \
java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \
miniBDD_new.cpp \
java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
java_bytecode/java_utils_test.cpp \
Expand Down
10 changes: 5 additions & 5 deletions unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ SCENARIO(
{
const symbol_tablet symbol_table = load_java_class_lazy(
"LocalLambdas",
"./java_bytecode/java_bytecode_parser/lambda_examples/",
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
"LocalLambdas.test");

THEN("Then the lambdas should be loaded")
Expand Down Expand Up @@ -68,7 +68,7 @@ SCENARIO(
{
const symbol_tablet symbol_table = load_java_class_lazy(
"MemberLambdas",
"./java_bytecode/java_bytecode_parser/lambda_examples/",
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
"MemberLambdas.test");

THEN("Then the lambdas should be loaded")
Expand Down Expand Up @@ -117,7 +117,7 @@ SCENARIO(
{
const symbol_tablet symbol_table = load_java_class_lazy(
"StaticLambdas",
"./java_bytecode/java_bytecode_parser/lambda_examples/",
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
"StaticLambdas.test");

THEN("Then the lambdas should be loaded")
Expand Down Expand Up @@ -166,7 +166,7 @@ SCENARIO(
{
const symbol_tablet symbol_table = load_java_class_lazy(
"OuterMemberLambdas$Inner",
"./java_bytecode/java_bytecode_parser/lambda_examples/",
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
"OuterMemberLambdas$Inner.test");

THEN("Then the lambdas should be loaded")
Expand All @@ -192,7 +192,7 @@ SCENARIO(
{
const symbol_tablet symbol_table = load_java_class_lazy(
"ExternalLambdaAccessor",
"./java_bytecode/java_bytecode_parser/lambda_examples/",
"./java_bytecode/java_bytecode_parse_lambdas/lambda_examples/",
"ExternalLambdaAccessor.test");

THEN("Then the lambdas should be loaded")
Expand Down
Loading