Name method handles uniformly

smowton · smowton · commit 263089cf2432 · 2020-05-22T14:57:36.000+01:00
They are method handles not references, and their varieties are kinds not types
diff --git a/jbmc/src/java_bytecode/java_bytecode_parse_tree.h b/jbmc/src/java_bytecode/java_bytecode_parse_tree.h
@@ -228,21 +228,21 @@ struct java_bytecode_parse_treet
     typedef std::vector<u2> u2_valuest;
     struct lambda_method_handlet
     {
-      java_class_typet::method_handle_typet handle_type;
+      java_class_typet::method_handle_kindt handle_type;
       optionalt<class_method_descriptor_exprt> method_descriptor;
 
       /// Construct a lambda method handle with parameters \p params.
       lambda_method_handlet(
         const class_method_descriptor_exprt &method_descriptor,
-        java_class_typet::method_handle_typet handle_type)
+        java_class_typet::method_handle_kindt handle_type)
         : handle_type(handle_type), method_descriptor(method_descriptor)
       {
         PRECONDITION(
-          handle_type != java_class_typet::method_handle_typet::UNKNOWN_HANDLE);
+          handle_type != java_class_typet::method_handle_kindt::UNKNOWN_HANDLE);
       }
 
       lambda_method_handlet()
-        : handle_type(java_class_typet::method_handle_typet::UNKNOWN_HANDLE),
+        : handle_type(java_class_typet::method_handle_kindt::UNKNOWN_HANDLE),
           method_descriptor()
       {
       }
@@ -255,7 +255,7 @@ struct java_bytecode_parse_treet
       bool is_unknown_handle() const
       {
         return handle_type ==
-               java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
+               java_class_typet::method_handle_kindt::UNKNOWN_HANDLE;
       }
 
       const class_method_descriptor_exprt &get_method_descriptor() const
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -54,7 +54,7 @@ class java_bytecode_parsert final : public parsert
   using fieldt = java_bytecode_parse_treet::fieldt;
   using instructiont = java_bytecode_parse_treet::instructiont;
   using annotationt = java_bytecode_parse_treet::annotationt;
-  using method_handle_typet = java_class_typet::method_handle_typet;
+  using method_handle_typet = java_class_typet::method_handle_kindt;
   using lambda_method_handlet =
     java_bytecode_parse_treet::classt::lambda_method_handlet;
 
@@ -302,7 +302,7 @@ class base_ref_infot : public structured_pool_entryt
 class method_handle_infot : public structured_pool_entryt
 {
 public:
-  /// Correspond to the different valid values for field reference_kind From
+  /// Correspond to the different valid values for field handle_kind From
   /// Java 8 spec 4.4.8
   /// (https://docs.oracle.com/javase/specs/jvms/se8/html/jvms-4.html)
   enum class method_handle_kindt
@@ -323,21 +323,21 @@ class method_handle_infot : public structured_pool_entryt
   {
     PRECONDITION(entry.tag == CONSTANT_MethodHandle);
     PRECONDITION(entry.ref1 > 0 && entry.ref1 < 10); // Java 8 spec 4.4.8
-    reference_kind = static_cast<method_handle_kindt>(entry.ref1);
+    handle_kind = static_cast<method_handle_kindt>(entry.ref1);
     reference_index = entry.ref2;
   }
 
-  method_handle_kindt get_reference_kind() const
+  method_handle_kindt get_handle_kind() const
   {
-    return reference_kind;
+    return handle_kind;
   }
 
   base_ref_infot get_reference(const pool_entry_lookupt &pool_entry) const
   {
     const base_ref_infot ref_entry{pool_entry(reference_index)};
 
     // validate the correctness of the constant pool entry
-    switch(reference_kind)
+    switch(handle_kind)
     {
     case method_handle_kindt::REF_getField:
     case method_handle_kindt::REF_getStatic:
@@ -373,7 +373,7 @@ class method_handle_infot : public structured_pool_entryt
   }
 
 private:
-  method_handle_kindt reference_kind;
+  method_handle_kindt handle_kind;
   u2 reference_index;
 };
 
@@ -1887,25 +1887,25 @@ void java_bytecode_parsert::parse_local_variable_type_table(methodt &method)
 /// newinvokespecial translates into a special instantiate-and-construct
 /// sequence. The field-manipulation reference kinds appear never to happen in
 /// reality and don't have syntax in the Java language.
-static java_class_typet::method_handle_typet get_method_handle_type(
+static java_class_typet::method_handle_kindt get_method_handle_type(
   method_handle_infot::method_handle_kindt java_handle_kind)
 {
   switch(java_handle_kind)
   {
   case method_handle_infot::method_handle_kindt::REF_newInvokeSpecial:
-    return java_class_typet::method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE;
+    return java_class_typet::method_handle_kindt::LAMBDA_CONSTRUCTOR_HANDLE;
   case method_handle_infot::method_handle_kindt::REF_invokeInterface:
   case method_handle_infot::method_handle_kindt::REF_invokeVirtual:
-    return java_class_typet::method_handle_typet::LAMBDA_VIRTUAL_METHOD_HANDLE;
+    return java_class_typet::method_handle_kindt::LAMBDA_VIRTUAL_METHOD_HANDLE;
   case method_handle_infot::method_handle_kindt::REF_invokeStatic:
   case method_handle_infot::method_handle_kindt::REF_invokeSpecial:
-    return java_class_typet::method_handle_typet::LAMBDA_STATIC_METHOD_HANDLE;
+    return java_class_typet::method_handle_kindt::LAMBDA_STATIC_METHOD_HANDLE;
   case method_handle_infot::method_handle_kindt::REF_getField:
   case method_handle_infot::method_handle_kindt::REF_getStatic:
   case method_handle_infot::method_handle_kindt::REF_putField:
   case method_handle_infot::method_handle_kindt::REF_putStatic:
   default:
-    return java_class_typet::method_handle_typet::UNKNOWN_HANDLE;
+    return java_class_typet::method_handle_kindt::UNKNOWN_HANDLE;
   }
 }
 
@@ -1937,13 +1937,13 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
   // they ever turn up this is where to fix them.
 
   if(
-    entry.get_reference_kind() ==
+    entry.get_handle_kind() ==
       method_handle_infot::method_handle_kindt::REF_getField ||
-    entry.get_reference_kind() ==
+    entry.get_handle_kind() ==
       method_handle_infot::method_handle_kindt::REF_putField ||
-    entry.get_reference_kind() ==
+    entry.get_handle_kind() ==
       method_handle_infot::method_handle_kindt::REF_getStatic ||
-    entry.get_reference_kind() ==
+    entry.get_handle_kind() ==
       method_handle_infot::method_handle_kindt::REF_putStatic)
   {
     return {};
@@ -1958,7 +1958,7 @@ java_bytecode_parsert::parse_method_handle(const method_handle_infot &entry)
   typet method_type = *java_type_from_string(descriptor);
 
   method_handle_typet handle_type =
-    get_method_handle_type(entry.get_reference_kind());
+    get_method_handle_type(entry.get_handle_kind());
 
   class_method_descriptor_exprt method_descriptor{
     method_type, mangled_method_name, class_name, method_name};
diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h
@@ -451,7 +451,7 @@ class java_class_typet:public class_typet
   }
 
   /// Indicates what sort of code should be synthesised for a lambda call:
-  enum class method_handle_typet
+  enum class method_handle_kindt
   {
     /// Direct call to the given method
     LAMBDA_STATIC_METHOD_HANDLE,
@@ -466,23 +466,23 @@ class java_class_typet:public class_typet
   /// Represents a lambda call to a method. We store the method being called in
   /// the same class_method_descriptor_exprt as java_bytecode_convert_method
   /// uses to translate virtual method calls to denote the method targeted, and
-  /// use method_handle_typet above to indicate what kind of dispatch should be
+  /// use method_handle_kindt above to indicate what kind of dispatch should be
   /// used.
   class java_lambda_method_handlet : public irept
   {
   public:
     java_lambda_method_handlet(
       const class_method_descriptor_exprt &method_descriptor,
-      method_handle_typet handle_type)
+      method_handle_kindt handle_kind)
     {
       set(ID_object_descriptor, method_descriptor);
-      set(ID_handle_type, static_cast<int>(handle_type));
+      set(ID_handle_type, static_cast<int>(handle_kind));
     }
 
     java_lambda_method_handlet()
     {
       set(
-        ID_handle_type, static_cast<int>(method_handle_typet::UNKNOWN_HANDLE));
+        ID_handle_type, static_cast<int>(method_handle_kindt::UNKNOWN_HANDLE));
     }
 
     const class_method_descriptor_exprt &get_lambda_method_descriptor() const
@@ -496,9 +496,9 @@ class java_class_typet:public class_typet
       return get_lambda_method_descriptor().get_identifier();
     }
 
-    method_handle_typet get_handle_type() const
+    method_handle_kindt get_handle_kind() const
     {
-      return (method_handle_typet)get_int(ID_handle_type);
+      return (method_handle_kindt)get_int(ID_handle_type);
     }
   };
 
@@ -519,10 +519,10 @@ class java_class_typet:public class_typet
 
   void add_lambda_method_handle(
     const class_method_descriptor_exprt &method_descriptor,
-    method_handle_typet handle_type)
+    method_handle_kindt handle_kind)
   {
     // creates a symbol_exprt for the identifier and pushes it in the vector
-    lambda_method_handles().emplace_back(method_descriptor, handle_type);
+    lambda_method_handles().emplace_back(method_descriptor, handle_kind);
   }
   void add_unknown_lambda_method_handle()
   {
diff --git a/jbmc/src/java_bytecode/lambda_synthesis.cpp b/jbmc/src/java_bytecode/lambda_synthesis.cpp
@@ -67,8 +67,8 @@ get_lambda_method_handle(
   // If the lambda method handle has an unknown type, it does not refer to
   // any symbol (it has an empty identifier)
   if(
-    lambda_method_handle.get_handle_type() !=
-    java_class_typet::method_handle_typet::UNKNOWN_HANDLE)
+    lambda_method_handle.get_handle_kind() !=
+    java_class_typet::method_handle_kindt::UNKNOWN_HANDLE)
     return lambda_method_handle;
   return {};
 }
@@ -656,13 +656,13 @@ codet invokedynamic_synthetic_method(
 
   const auto &lambda_method_symbol =
     ns.lookup(lambda_method_handle.get_lambda_method_identifier());
-  const auto handle_type = lambda_method_handle.get_handle_type();
+  const auto handle_type = lambda_method_handle.get_handle_kind();
   const auto is_constructor_lambda =
     handle_type ==
-    java_class_typet::method_handle_typet::LAMBDA_CONSTRUCTOR_HANDLE;
+    java_class_typet::method_handle_kindt::LAMBDA_CONSTRUCTOR_HANDLE;
   const auto use_virtual_dispatch =
     handle_type ==
-    java_class_typet::method_handle_typet::LAMBDA_VIRTUAL_METHOD_HANDLE;
+    java_class_typet::method_handle_kindt::LAMBDA_VIRTUAL_METHOD_HANDLE;
 
   if(is_constructor_lambda)
   {

Original file line number	Diff line number	Diff line change
`@@ -228,21 +228,21 @@ struct java_bytecode_parse_treet`
`228`	`228`	`typedef std::vector<u2> u2_valuest;`
`229`	`229`	`struct lambda_method_handlet`
`230`	`230`	`{`
`231`		`- java_class_typet::method_handle_typet handle_type;`
	`231`	`+ java_class_typet::method_handle_kindt handle_type;`
`232`	`232`	`optionalt<class_method_descriptor_exprt> method_descriptor;`
`233`	`233`
`234`	`234`	`/// Construct a lambda method handle with parameters \p params.`
`235`	`235`	`lambda_method_handlet(`
`236`	`236`	`const class_method_descriptor_exprt &method_descriptor,`
`237`		`- java_class_typet::method_handle_typet handle_type)`
	`237`	`+ java_class_typet::method_handle_kindt handle_type)`
`238`	`238`	`: handle_type(handle_type), method_descriptor(method_descriptor)`
`239`	`239`	`{`
`240`	`240`	`PRECONDITION(`
`241`		`- handle_type != java_class_typet::method_handle_typet::UNKNOWN_HANDLE);`
	`241`	`+ handle_type != java_class_typet::method_handle_kindt::UNKNOWN_HANDLE);`
`242`	`242`	`}`
`243`	`243`
`244`	`244`	`lambda_method_handlet()`
`245`		`- : handle_type(java_class_typet::method_handle_typet::UNKNOWN_HANDLE),`
	`245`	`+ : handle_type(java_class_typet::method_handle_kindt::UNKNOWN_HANDLE),`
`246`	`246`	`method_descriptor()`
`247`	`247`	`{`
`248`	`248`	`}`
`@@ -255,7 +255,7 @@ struct java_bytecode_parse_treet`
`255`	`255`	`bool is_unknown_handle() const`
`256`	`256`	`{`
`257`	`257`	`return handle_type ==`
`258`		`- java_class_typet::method_handle_typet::UNKNOWN_HANDLE;`
	`258`	`+ java_class_typet::method_handle_kindt::UNKNOWN_HANDLE;`
`259`	`259`	`}`
`260`	`260`
`261`	`261`	`const class_method_descriptor_exprt &get_method_descriptor() const`
Original file line number	Diff line number	Diff line change
`@@ -451,7 +451,7 @@ class java_class_typet:public class_typet`
`451`	`451`	`}`
`452`	`452`
`453`	`453`	`/// Indicates what sort of code should be synthesised for a lambda call:`
`454`		`- enum class method_handle_typet`
	`454`	`+ enum class method_handle_kindt`
`455`	`455`	`{`
`456`	`456`	`/// Direct call to the given method`
`457`	`457`	`LAMBDA_STATIC_METHOD_HANDLE,`
`@@ -466,23 +466,23 @@ class java_class_typet:public class_typet`
`466`	`466`	`/// Represents a lambda call to a method. We store the method being called in`
`467`	`467`	`/// the same class_method_descriptor_exprt as java_bytecode_convert_method`
`468`	`468`	`/// uses to translate virtual method calls to denote the method targeted, and`
`469`		`- /// use method_handle_typet above to indicate what kind of dispatch should be`
	`469`	`+ /// use method_handle_kindt above to indicate what kind of dispatch should be`
`470`	`470`	`/// used.`
`471`	`471`	`class java_lambda_method_handlet : public irept`
`472`	`472`	`{`
`473`	`473`	`public:`
`474`	`474`	`java_lambda_method_handlet(`
`475`	`475`	`const class_method_descriptor_exprt &method_descriptor,`
`476`		`- method_handle_typet handle_type)`
	`476`	`+ method_handle_kindt handle_kind)`
`477`	`477`	`{`
`478`	`478`	`set(ID_object_descriptor, method_descriptor);`
`479`		`- set(ID_handle_type, static_cast<int>(handle_type));`
	`479`	`+ set(ID_handle_type, static_cast<int>(handle_kind));`
`480`	`480`	`}`
`481`	`481`
`482`	`482`	`java_lambda_method_handlet()`
`483`	`483`	`{`
`484`	`484`	`set(`
`485`		`- ID_handle_type, static_cast<int>(method_handle_typet::UNKNOWN_HANDLE));`
	`485`	`+ ID_handle_type, static_cast<int>(method_handle_kindt::UNKNOWN_HANDLE));`
`486`	`486`	`}`
`487`	`487`
`488`	`488`	`const class_method_descriptor_exprt &get_lambda_method_descriptor() const`
`@@ -496,9 +496,9 @@ class java_class_typet:public class_typet`
`496`	`496`	`return get_lambda_method_descriptor().get_identifier();`
`497`	`497`	`}`
`498`	`498`
`499`		`- method_handle_typet get_handle_type() const`
	`499`	`+ method_handle_kindt get_handle_kind() const`
`500`	`500`	`{`
`501`		`- return (method_handle_typet)get_int(ID_handle_type);`
	`501`	`+ return (method_handle_kindt)get_int(ID_handle_type);`
`502`	`502`	`}`
`503`	`503`	`};`
`504`	`504`
`@@ -519,10 +519,10 @@ class java_class_typet:public class_typet`
`519`	`519`
`520`	`520`	`void add_lambda_method_handle(`
`521`	`521`	`const class_method_descriptor_exprt &method_descriptor,`
`522`		`- method_handle_typet handle_type)`
	`522`	`+ method_handle_kindt handle_kind)`
`523`	`523`	`{`
`524`	`524`	`// creates a symbol_exprt for the identifier and pushes it in the vector`
`525`		`- lambda_method_handles().emplace_back(method_descriptor, handle_type);`
	`525`	`+ lambda_method_handles().emplace_back(method_descriptor, handle_kind);`
`526`	`526`	`}`
`527`	`527`	`void add_unknown_lambda_method_handle()`
`528`	`528`	`{`