Skip to content

Commit 0fb0063

Browse files
smowtonsmowton
committed
Add support for invoke-virtual and invoke-interface lambdas
To support these we store lambda descriptors in the same form as virtual method references, using class_method_descriptor_exprt, lowering it to a symbol_exprt if we have a known callee. This is also the first form of synthetic method to produce a virtual method call, hence the alteration of notify_static_method_calls to tolerate them.
1 parent 68222b0 commit 0fb0063

File tree

11 files changed

+260
-173
lines changed

11 files changed

+260
-173
lines changed

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -426,7 +426,7 @@ void java_bytecode_convert_classt::convert(
426426
lambda_entry.second.is_unknown_handle()
427427
? class_type.add_unknown_lambda_method_handle()
428428
: class_type.add_lambda_method_handle(
429-
"java::" + id2string(lambda_entry.second.lambda_method_ref),
429+
lambda_entry.second.get_method_descriptor(),
430430
lambda_entry.second.handle_type);
431431
}
432432

‎jbmc/src/java_bytecode/java_bytecode_language.cpp‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1228,18 +1228,20 @@ static void notify_static_method_calls(
12281228
// starts to introduce virtual function calls then we will need to
12291229
// duplicate the behavior of java_bytecode_convert_method where it
12301230
// handles the invokevirtual instruction
1231-
const symbol_exprt &fn_sym =
1232-
expr_dynamic_cast<symbol_exprt>(fn_call->function());
1233-
needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
1231+
const symbol_exprt *fn_sym =
1232+
expr_try_dynamic_cast<symbol_exprt>(fn_call->function());
1233+
if(fn_sym)
1234+
needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
12341235
}
12351236
else if(
12361237
it->id() == ID_side_effect &&
12371238
to_side_effect_expr(*it).get_statement() == ID_function_call)
12381239
{
12391240
const auto &call_expr = to_side_effect_expr_function_call(*it);
1240-
const symbol_exprt &fn_sym =
1241-
expr_dynamic_cast<symbol_exprt>(call_expr.function());
1242-
needed_lazy_methods->add_needed_method(fn_sym.get_identifier());
1241+
const symbol_exprt *fn_sym =
1242+
expr_try_dynamic_cast<symbol_exprt>(call_expr.function());
1243+
if(fn_sym)
1244+
needed_lazy_methods->add_needed_method(fn_sym->get_identifier());
12431245
}
12441246
}
12451247
}

‎jbmc/src/java_bytecode/java_bytecode_parse_tree.h‎

Lines changed: 22 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -228,32 +228,41 @@ struct java_bytecode_parse_treet
228228
typedef std::vector<u2> u2_valuest;
229229
struct lambda_method_handlet
230230
{
231-
java_class_typet::method_handle_typet handle_type =
232-
java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
233-
irep_idt lambda_method_name;
234-
irep_idt lambda_method_ref;
235-
irep_idt interface_type;
236-
irep_idt method_type;
237-
u2_valuest u2_values;
238-
lambda_method_handlet() = default;
231+
java_class_typet::method_handle_typet handle_type;
232+
optionalt<class_method_descriptor_exprt> method_descriptor;
239233

240234
/// Construct a lambda method handle with parameters \p params.
241-
explicit lambda_method_handlet(const u2_valuest &params)
242-
: u2_values(params)
235+
lambda_method_handlet(
236+
const class_method_descriptor_exprt &method_descriptor,
237+
java_class_typet::method_handle_typet handle_type)
238+
: handle_type(handle_type), method_descriptor(method_descriptor)
243239
{
240+
PRECONDITION(
241+
handle_type != java_class_typet::method_handle_typet::UNKNOWN_HANDLE);
244242
}
245243

246-
/// Construct a lambda method handle with parameters \p params.
247-
explicit lambda_method_handlet(u2_valuest &&params)
248-
: u2_values(std::move(params))
244+
lambda_method_handlet()
245+
: handle_type(java_class_typet::method_handle_typet::UNKNOWN_HANDLE),
246+
method_descriptor()
247+
{
248+
}
249+
250+
static lambda_method_handlet get_unknown_handle()
249251
{
252+
return lambda_method_handlet{};
250253
}
251254

252255
bool is_unknown_handle() const
253256
{
254257
return handle_type ==
255258
java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
256259
}
260+
261+
const class_method_descriptor_exprt &get_method_descriptor() const
262+
{
263+
PRECONDITION(!is_unknown_handle());
264+
return *method_descriptor;
265+
}
257266
};
258267

259268
// TODO(tkiley): This map shouldn't be interacted with directly (instead

‎jbmc/src/java_bytecode/java_bytecode_parser.cpp‎

Lines changed: 44 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -146,9 +146,7 @@ class java_bytecode_parsert final : public parsert
146146
return narrow_cast<T>(result);
147147
}
148148

149-
void store_unknown_method_handle(
150-
size_t bootstrap_method_index,
151-
std::vector<u2> u2_values);
149+
void store_unknown_method_handle(size_t bootstrap_method_index);
152150
};
153151

154152
#define CONSTANT_Class 7
@@ -1883,6 +1881,28 @@ void java_bytecode_parsert::parse_local_variable_type_table(methodt &method)
18831881
}
18841882
}
18851883

1884+
static java_class_typet::method_handle_typet get_method_handle_type(
1885+
method_handle_infot::method_handle_kindt java_handle_kind)
1886+
{
1887+
switch(java_handle_kind)
1888+
{
1889+
case method_handle_infot::method_handle_kindt::REF_newInvokeSpecial:
1890+
return java_class_typet::method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE;
1891+
case method_handle_infot::method_handle_kindt::REF_invokeInterface:
1892+
case method_handle_infot::method_handle_kindt::REF_invokeVirtual:
1893+
return java_class_typet::method_handle_typet::LAMBDA_VIRTUAL_METHOD_HANDLE;
1894+
case method_handle_infot::method_handle_kindt::REF_invokeStatic:
1895+
case method_handle_infot::method_handle_kindt::REF_invokeSpecial:
1896+
return java_class_typet::method_handle_typet::LAMBDA_STATIC_METHOD_HANDLE;
1897+
case method_handle_infot::method_handle_kindt::REF_getField:
1898+
case method_handle_infot::method_handle_kindt::REF_getStatic:
1899+
case method_handle_infot::method_handle_kindt::REF_putField:
1900+
case method_handle_infot::method_handle_kindt::REF_putStatic:
1901+
default:
1902+
return java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
1903+
}
1904+
}
1905+
18861906
/// Read method handle pointed to from constant pool entry at index, return type
18871907
/// of method handle and name if lambda function is found.
18881908
/// \param entry: the constant pool entry of the methodhandle_info structure
@@ -1900,12 +1920,6 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
19001920
const name_and_type_infot &name_and_type =
19011921
ref_entry.get_name_and_type(pool_entry_lambda);
19021922

1903-
std::string class_name = class_entry.get_name(pool_entry_lambda);
1904-
// replace '.' for '$' (inner classes)
1905-
std::replace(class_name.begin(), class_name.end(), '.', '$');
1906-
// replace '/' for '.' (package)
1907-
std::replace(class_name.begin(), class_name.end(), '/', '.');
1908-
19091923
// The following lambda kinds specified in the JVMS (see for example
19101924
// https://docs.oracle.com/javase/specs/jvms/se7/html/jvms-5.html#jvms-5.4.3.5
19111925
// but which aren't actually created by javac. Java has no syntax for a field-
@@ -1929,20 +1943,20 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
19291943
return {};
19301944
}
19311945

1932-
const std::string method_ref =
1933-
class_name + "." + name_and_type.get_name(pool_entry_lambda) + ':' +
1934-
name_and_type.get_descriptor(pool_entry_lambda);
1946+
irep_idt class_name =
1947+
java_classname(class_entry.get_name(pool_entry_lambda)).get_identifier();
19351948

1936-
lambda_method_handlet lambda_method_handle;
1949+
irep_idt method_name = name_and_type.get_name(pool_entry_lambda);
1950+
std::string descriptor = name_and_type.get_descriptor(pool_entry_lambda);
1951+
irep_idt mangled_method_name = id2string(method_name) + ":" + descriptor;
1952+
typet method_type = *java_type_from_string(descriptor);
19371953

1938-
lambda_method_handle.lambda_method_name =
1939-
name_and_type.get_name(pool_entry_lambda);
1940-
lambda_method_handle.lambda_method_ref = method_ref;
1941-
lambda_method_handle.handle_type =
1942-
entry.get_reference_kind() ==
1943-
method_handle_infot::method_handle_kindt::REF_newInvokeSpecial
1944-
? method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE
1945-
: method_handle_typet::LAMBDA_METHOD_HANDLE;
1954+
method_handle_typet handle_type =
1955+
get_method_handle_type(entry.get_reference_kind());
1956+
1957+
class_method_descriptor_exprt method_descriptor{
1958+
method_type, mangled_method_name, class_name, method_name};
1959+
lambda_method_handlet lambda_method_handle{method_descriptor, handle_type};
19461960

19471961
return lambda_method_handle;
19481962
}
@@ -2001,7 +2015,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
20012015
// understand
20022016
if(num_bootstrap_arguments < 3)
20032017
{
2004-
store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2018+
store_unknown_method_handle(bootstrap_method_index);
20052019
debug()
20062020
<< "format of BootstrapMethods entry not recognized: too few arguments"
20072021
<< eom;
@@ -2028,7 +2042,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
20282042
debug() << "format of BootstrapMethods entry not recognized: extra "
20292043
"arguments of wrong type"
20302044
<< eom;
2031-
store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2045+
store_unknown_method_handle(bootstrap_method_index);
20322046
continue;
20332047
}
20342048

@@ -2045,7 +2059,7 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
20452059
debug() << "format of BootstrapMethods entry not recognized: arguments "
20462060
"wrong type"
20472061
<< eom;
2048-
store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2062+
store_unknown_method_handle(bootstrap_method_index);
20492063
continue;
20502064
}
20512065

@@ -2058,20 +2072,17 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
20582072
debug() << "format of BootstrapMethods entry not recognized: method "
20592073
"handle not recognised"
20602074
<< eom;
2061-
store_unknown_method_handle(bootstrap_method_index, std::move(u2_values));
2075+
store_unknown_method_handle(bootstrap_method_index);
20622076
continue;
20632077
}
20642078

20652079
// If parse_method_handle can't parse the lambda method, it should return {}
20662080
POSTCONDITION(
20672081
lambda_method_handle->handle_type != method_handle_typet::UNKNOWN_HANDLE);
20682082

2069-
lambda_method_handle->interface_type =
2070-
pool_entry(interface_type_argument.ref1).s;
2071-
lambda_method_handle->method_type = pool_entry(method_type_argument.ref1).s;
2072-
lambda_method_handle->u2_values = std::move(u2_values);
20732083
debug() << "lambda function reference "
2074-
<< id2string(lambda_method_handle->lambda_method_name)
2084+
<< id2string(lambda_method_handle->get_method_descriptor()
2085+
.base_method_name())
20752086
<< " in class \"" << parse_tree.parsed_class.name << "\""
20762087
<< "\n interface type is "
20772088
<< id2string(pool_entry(interface_type_argument.ref1).s)
@@ -2085,12 +2096,11 @@ void java_bytecode_parsert::read_bootstrapmethods_entry()
20852096
/// Creates an unknown method handle and puts it into the parsed_class
20862097
/// \param bootstrap_method_index: The current index in the bootstrap entry
20872098
/// table
2088-
/// \param u2_values: The indices of the arguments for the call
20892099
void java_bytecode_parsert::store_unknown_method_handle(
2090-
size_t bootstrap_method_index,
2091-
std::vector<u2> u2_values)
2100+
size_t bootstrap_method_index)
20922101
{
2093-
const lambda_method_handlet lambda_method_handle(std::move(u2_values));
2102+
const lambda_method_handlet lambda_method_handle =
2103+
lambda_method_handlet::get_unknown_handle();
20942104
parse_tree.parsed_class.add_method_handle(
20952105
bootstrap_method_index, lambda_method_handle);
20962106
}

‎jbmc/src/java_bytecode/java_types.h‎

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -452,7 +452,8 @@ class java_class_typet:public class_typet
452452

453453
enum class method_handle_typet
454454
{
455-
LAMBDA_METHOD_HANDLE,
455+
LAMBDA_STATIC_METHOD_HANDLE,
456+
LAMBDA_VIRTUAL_METHOD_HANDLE,
456457
LAMBDA_CONSTRUCTOR_HANDLE,
457458
UNKNOWN_HANDLE
458459
};
@@ -461,10 +462,10 @@ class java_class_typet:public class_typet
461462
{
462463
public:
463464
java_lambda_method_handlet(
464-
const irep_idt &id,
465+
const class_method_descriptor_exprt &method_descriptor,
465466
method_handle_typet handle_type)
466-
: irept(id)
467467
{
468+
set(ID_object_descriptor, method_descriptor);
468469
set(ID_handle_type, static_cast<int>(handle_type));
469470
}
470471

@@ -474,9 +475,15 @@ class java_class_typet:public class_typet
474475
ID_handle_type, static_cast<int>(method_handle_typet::UNKNOWN_HANDLE));
475476
}
476477

478+
const class_method_descriptor_exprt &get_lambda_method_descriptor() const
479+
{
480+
return static_cast<const class_method_descriptor_exprt &>(
481+
find(ID_object_descriptor));
482+
}
483+
477484
const irep_idt &get_lambda_method_identifier() const
478485
{
479-
return id();
486+
return get_lambda_method_descriptor().get_identifier();
480487
}
481488

482489
method_handle_typet get_handle_type() const
@@ -501,11 +508,11 @@ class java_class_typet:public class_typet
501508
}
502509

503510
void add_lambda_method_handle(
504-
const irep_idt &identifier,
511+
const class_method_descriptor_exprt &method_descriptor,
505512
method_handle_typet handle_type)
506513
{
507514
// creates a symbol_exprt for the identifier and pushes it in the vector
508-
lambda_method_handles().emplace_back(identifier, handle_type);
515+
lambda_method_handles().emplace_back(method_descriptor, handle_type);
509516
}
510517
void add_unknown_lambda_method_handle()
511518
{

‎jbmc/src/java_bytecode/lambda_synthesis.cpp‎

Lines changed: 43 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -508,6 +508,27 @@ codet invokedynamic_synthetic_constructor(
508508
return std::move(result);
509509
}
510510

511+
static symbol_exprt create_and_declare_local(
512+
const irep_idt &function_id,
513+
const irep_idt &basename,
514+
const typet &type,
515+
symbol_table_baset &symbol_table,
516+
code_blockt &method)
517+
{
518+
irep_idt new_var_name = id2string(function_id) + "::" + id2string(basename);
519+
auxiliary_symbolt new_instance_var_symbol;
520+
new_instance_var_symbol.name = new_var_name;
521+
new_instance_var_symbol.base_name = basename;
522+
new_instance_var_symbol.mode = ID_java;
523+
new_instance_var_symbol.type = type;
524+
bool add_failed = symbol_table.add(new_instance_var_symbol);
525+
POSTCONDITION(!add_failed);
526+
symbol_exprt new_instance_var = new_instance_var_symbol.symbol_expr();
527+
method.add(code_declt{new_instance_var});
528+
529+
return new_instance_var;
530+
}
531+
511532
static symbol_exprt instantiate_new_object(
512533
const irep_idt &function_id,
513534
const symbolt &lambda_method_symbol,
@@ -531,18 +552,12 @@ static symbol_exprt instantiate_new_object(
531552
}
532553

533554
// Make a local to hold the new instance:
534-
irep_idt new_instance_var_basename = "newinvokespecial_instance";
535-
irep_idt new_instance_var_name =
536-
id2string(function_id) + "::" + id2string(new_instance_var_basename);
537-
auxiliary_symbolt new_instance_var_symbol;
538-
new_instance_var_symbol.name = new_instance_var_name;
539-
new_instance_var_symbol.base_name = new_instance_var_basename;
540-
new_instance_var_symbol.mode = ID_java;
541-
new_instance_var_symbol.type = created_type;
542-
bool add_failed = symbol_table.add(new_instance_var_symbol);
543-
POSTCONDITION(!add_failed);
544-
symbol_exprt new_instance_var = new_instance_var_symbol.symbol_expr();
545-
result.add(code_declt{new_instance_var});
555+
symbol_exprt new_instance_var = create_and_declare_local(
556+
function_id,
557+
"newinvokespecial_instance",
558+
created_type,
559+
symbol_table,
560+
result);
546561

547562
// Instantiate the object:
548563
side_effect_exprt java_new_expr(ID_java_new, created_type, {});
@@ -611,6 +626,9 @@ codet invokedynamic_synthetic_method(
611626
const auto is_constructor_lambda =
612627
handle_type ==
613628
java_class_typet::method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE;
629+
const auto use_virtual_dispatch =
630+
handle_type ==
631+
java_class_typet::method_handle_typet::LAMBDA_VIRTUAL_METHOD_HANDLE;
614632

615633
if(is_constructor_lambda)
616634
{
@@ -621,18 +639,24 @@ codet invokedynamic_synthetic_method(
621639
lambda_method_args.insert(lambda_method_args.begin(), new_instance_var);
622640
}
623641

642+
const auto &lambda_method_descriptor =
643+
lambda_method_handle.get_lambda_method_descriptor();
644+
exprt callee;
645+
if(use_virtual_dispatch)
646+
callee = lambda_method_descriptor;
647+
else
648+
callee = lambda_method_symbol.symbol_expr();
649+
624650
if(return_type != empty_typet() && !is_constructor_lambda)
625651
{
626-
result.add(code_returnt(side_effect_expr_function_callt(
627-
lambda_method_symbol.symbol_expr(),
628-
lambda_method_args,
629-
return_type,
630-
source_locationt())));
652+
symbol_exprt result_local = create_and_declare_local(
653+
function_id, "return_value", return_type, symbol_table, result);
654+
result.add(code_function_callt(result_local, callee, lambda_method_args));
655+
result.add(code_returnt{result_local});
631656
}
632657
else
633658
{
634-
result.add(code_function_callt(
635-
lambda_method_symbol.symbol_expr(), lambda_method_args));
659+
result.add(code_function_callt(callee, lambda_method_args));
636660
}
637661

638662
if(is_constructor_lambda)

0 commit comments

Comments
 (0)