Skip to content

Use irept instead of symbol_exprt in java_lambda_method_handlest [blocks: #2310] #3286

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 10, 2018
Merged

Use irept instead of symbol_exprt in java_lambda_method_handlest [blocks: #2310] #3286

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
bd5b18f
Use irept instead of symbol_exprt in java_lambda_method_handlest
tautschnig Nov 6, 2018
68d7791
clang-format compatible line breaks
tautschnig Nov 7, 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
8 changes: 4 additions & 4 deletions jbmc/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 @@ -316,11 +316,11 @@ 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)
{
const symbol_exprt &lambda_method_handle = lambda_method_handles.at(index);
const irept &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());
// any symbol (it has an empty identifier)
if(!lambda_method_handle.id().empty())
return symbol_table.lookup_ref(lambda_method_handle.id());
return {};
}

Expand Down
21 changes: 15 additions & 6 deletions jbmc/src/java_bytecode/java_types.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -171,19 +171,28 @@ class java_class_typet:public class_typet
set(ID_final, is_final);
}

typedef std::vector<symbol_exprt> java_lambda_method_handlest;
// it may be better to introduce a class like
// class java_lambda_method_handlet : private irept
// {
// java_lambda_method_handlet(const irep_idt &id) : irept(id)
// {
// }
//
// const irep_idt &get_lambda_method_handle() const
// {
// return id();
// }
// };
using java_lambda_method_handlest = irept::subt;

const java_lambda_method_handlest &lambda_method_handles() const
{
return (const java_lambda_method_handlest &)find(
ID_java_lambda_method_handles)
.get_sub();
return 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();
return add(ID_java_lambda_method_handles).get_sub();
}

void add_lambda_method_handle(const irep_idt &identifier)
Expand Down
19 changes: 9 additions & 10 deletions jbmc/unit/java-testing-utils/require_type.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -521,15 +521,14 @@ require_type::require_lambda_method_handles(
class_type.lambda_method_handles();
REQUIRE(lambda_method_handles.size() == expected_identifiers.size());

REQUIRE(
std::equal(
lambda_method_handles.begin(),
lambda_method_handles.end(),
expected_identifiers.begin(),
[](
const symbol_exprt &lambda_method_handle,
const std::string &expected_identifier) { //NOLINT
return lambda_method_handle.get_identifier() == expected_identifier;
}));
REQUIRE(std::equal(
lambda_method_handles.begin(),
lambda_method_handles.end(),
expected_identifiers.begin(),
[](
const irept &lambda_method_handle,
const std::string &expected_identifier) { //NOLINT
return lambda_method_handle.id() == expected_identifier;
}));
return lambda_method_handles;
}