From bd5b18ffdd3cc9ef0ecc53843dcf4d75a9e0f995 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 6 Nov 2018 23:28:11 +0000 Subject: [PATCH 1/2] Use irept instead of symbol_exprt in java_lambda_method_handlest A java_lambda_method_handlest really is just a collection of identifiers - there is no need to put them into a symbol_exprt, instead the identifier can directly be used as the id of an irept. This reduces the memory footprint, but more importantly avoids a warning of using a deprecated symbol_exprt constructor. This warning is well placed, because those symbol_exprt would never have a type set, which makes them invalid symbol_exprt anyway. --- .../java_bytecode_convert_method.cpp | 8 +++---- jbmc/src/java_bytecode/java_types.h | 21 +++++++++++++------ jbmc/unit/java-testing-utils/require_type.cpp | 4 ++-- 3 files changed, 21 insertions(+), 12 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 18dac837fb..261a4037fb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -316,11 +316,11 @@ optionalt 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 {}; } diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 81eeae4bdb..8e7fea4b7c 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -171,19 +171,28 @@ class java_class_typet:public class_typet set(ID_final, is_final); } - typedef std::vector 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) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index e6c2820bb4..68cba20e96 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -527,9 +527,9 @@ require_type::require_lambda_method_handles( lambda_method_handles.end(), expected_identifiers.begin(), []( - const symbol_exprt &lambda_method_handle, + const irept &lambda_method_handle, const std::string &expected_identifier) { //NOLINT - return lambda_method_handle.get_identifier() == expected_identifier; + return lambda_method_handle.id() == expected_identifier; })); return lambda_method_handles; } From 68d77913ce410f4ead9103c433cf6ccb3910bbf6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Nov 2018 07:38:26 +0000 Subject: [PATCH 2/2] clang-format compatible line breaks --- jbmc/unit/java-testing-utils/require_type.cpp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 68cba20e96..c6240190f2 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -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 irept &lambda_method_handle, - const std::string &expected_identifier) { //NOLINT - return lambda_method_handle.id() == 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; }