Merge pull request #3286 from tautschnig/lambda_method_handles

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

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -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 {};
 }
 

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<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)

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