Merge pull request #5007 from owen-mc-diffblue/virtual-function-expr

Create class_method_descriptor_exprt for ID_virtual_function

Author: owen-mc-diffblue

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -130,7 +130,8 @@ bool ci_lazy_methodst::operator()(
   }
 
   std::unordered_set<irep_idt> methods_already_populated;
-  std::unordered_set<exprt, irep_hash> virtual_function_calls;
+  std::unordered_set<class_method_descriptor_exprt, irep_hash>
+    called_virtual_functions;
   bool class_initializer_seen = false;
 
   bool any_new_classes = true;
@@ -154,7 +155,7 @@ bool ci_lazy_methodst::operator()(
             symbol_table,
             methods_to_convert_later,
             instantiated_classes,
-            virtual_function_calls);
+            called_virtual_functions);
           any_new_methods |= conversion_result.new_method_seen;
           class_initializer_seen |= conversion_result.class_initializer_seen;
         }
@@ -164,12 +165,13 @@ bool ci_lazy_methodst::operator()(
       // possible virtual function call targets:
 
       debug() << "CI lazy methods: add virtual method targets ("
-              << virtual_function_calls.size() << " callsites)" << eom;
+              << called_virtual_functions.size() << " callsites)" << eom;
 
-      for(const exprt &function : virtual_function_calls)
+      for(const class_method_descriptor_exprt &called_virtual_function :
+          called_virtual_functions)
       {
         get_virtual_method_targets(
-          function,
+          called_virtual_function,
           instantiated_classes,
           methods_to_convert_later,
           symbol_table);
@@ -179,7 +181,7 @@ bool ci_lazy_methodst::operator()(
     any_new_classes = handle_virtual_methods_with_no_callees(
       methods_to_convert_later,
       instantiated_classes,
-      virtual_function_calls,
+      called_virtual_functions,
       symbol_table);
   }
 
@@ -231,7 +233,8 @@ bool ci_lazy_methodst::operator()(
 bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
   std::unordered_set<irep_idt> &methods_to_convert_later,
   std::unordered_set<irep_idt> &instantiated_classes,
-  const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
+  const std::unordered_set<class_method_descriptor_exprt, irep_hash>
+    &virtual_functions,
   symbol_tablet &symbol_table)
 {
   ci_lazy_methods_neededt lazy_methods_loader(
@@ -241,11 +244,11 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
     pointer_type_selector);
 
   bool any_new_classes = false;
-  for(const exprt &virtual_function_call : virtual_function_calls)
+  for(const class_method_descriptor_exprt &virtual_function : virtual_functions)
   {
     std::unordered_set<irep_idt> candidate_target_methods;
     get_virtual_method_targets(
-      virtual_function_call,
+      virtual_function,
       instantiated_classes,
       candidate_target_methods,
       symbol_table);
@@ -254,13 +257,13 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
       continue;
 
     const java_method_typet &java_method_type =
-      to_java_method_type(virtual_function_call.type());
+      to_java_method_type(virtual_function.type());
 
     // Add the call class to instantiated_classes and assert that it
     // didn't already exist. It can't be instantiated already, otherwise it
     // would give a concrete definition of the called method, and
     // candidate_target_methods would be non-empty.
-    const irep_idt &call_class = virtual_function_call.get(ID_C_class);
+    const irep_idt &call_class = virtual_function.get_class_name();
     bool was_missing = instantiated_classes.count(call_class) == 0;
     CHECK_RETURN(was_missing);
     any_new_classes = true;
@@ -289,8 +292,7 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
     }
 
     // Check that `get_virtual_method_target` returns a method now
-    const irep_idt &call_basename =
-      virtual_function_call.get(ID_component_name);
+    const irep_idt &call_basename = virtual_function.get_component_name();
     const irep_idt method_name = get_virtual_method_target(
       instantiated_classes, call_basename, call_class, symbol_table);
     CHECK_RETURN(!method_name.empty());
@@ -303,7 +305,7 @@ bool ci_lazy_methodst::handle_virtual_methods_with_no_callees(
 
 /// Convert a method, add it to the populated set, add needed methods to
 /// methods_to_convert_later and add virtual calls from the method to
-/// virtual_function_calls
+/// virtual_functions
 /// \return structure containing two Booleans:
 ///     * class_initializer_seen which is true if the class_initializer_seen
 ///       argument was false and the class_model is referenced in
@@ -319,7 +321,8 @@ ci_lazy_methodst::convert_and_analyze_method(
   symbol_tablet &symbol_table,
   std::unordered_set<irep_idt> &methods_to_convert_later,
   std::unordered_set<irep_idt> &instantiated_classes,
-  std::unordered_set<exprt, irep_hash> &virtual_function_calls)
+  std::unordered_set<class_method_descriptor_exprt, irep_hash>
+    &called_virtual_functions)
 {
   convert_method_resultt result;
   if(!methods_already_populated.insert(method_name).second)
@@ -339,7 +342,7 @@ ci_lazy_methodst::convert_and_analyze_method(
     return result;
 
   const exprt &method_body = symbol_table.lookup_ref(method_name).value;
-  gather_virtual_callsites(method_body, virtual_function_calls);
+  gather_virtual_callsites(method_body, called_virtual_functions);
 
   if(!class_initializer_already_seen && references_class_model(method_body))
   {
@@ -438,15 +441,18 @@ void ci_lazy_methodst::initialize_instantiated_classes(
 ///   e that calls a virtual function.
 void ci_lazy_methodst::gather_virtual_callsites(
   const exprt &e,
-  std::unordered_set<exprt, irep_hash> &result)
+  std::unordered_set<class_method_descriptor_exprt, irep_hash> &result)
 {
   if(e.id()!=ID_code)
     return;
   const codet &c=to_code(e);
-  if(c.get_statement()==ID_function_call &&
-     to_code_function_call(c).function().id()==ID_virtual_function)
+  if(
+    c.get_statement() == ID_function_call &&
+    can_cast_expr<class_method_descriptor_exprt>(
+      to_code_function_call(c).function()))
   {
-    result.insert(to_code_function_call(c).function());
+    result.insert(
+      to_class_method_descriptor_expr(to_code_function_call(c).function()));
   }
   else
   {
@@ -466,17 +472,15 @@ void ci_lazy_methodst::gather_virtual_callsites(
 ///   defined on classes that are not 'needed' are ignored)
 /// \param symbol_table: global symbol table
 void ci_lazy_methodst::get_virtual_method_targets(
-  const exprt &called_function,
+  const class_method_descriptor_exprt &called_function,
   const std::unordered_set<irep_idt> &instantiated_classes,
   std::unordered_set<irep_idt> &callable_methods,
   symbol_tablet &symbol_table)
 {
-  PRECONDITION(called_function.id()==ID_virtual_function);
-
-  const auto &call_class=called_function.get(ID_C_class);
+  const auto &call_class = called_function.get_class_name();
   INVARIANT(
     !call_class.empty(), "All virtual calls should be aimed at a class");
-  const auto &call_basename=called_function.get(ID_component_name);
+  const auto &call_basename = called_function.get_component_name();
   INVARIANT(
     !call_basename.empty(),
     "Virtual function must have a reasonable name after removing class");

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -122,10 +122,10 @@ class ci_lazy_methodst:public messaget
 
   void gather_virtual_callsites(
     const exprt &e,
-    std::unordered_set<exprt, irep_hash> &result);
+    std::unordered_set<class_method_descriptor_exprt, irep_hash> &result);
 
   void get_virtual_method_targets(
-    const exprt &called_function,
+    const class_method_descriptor_exprt &called_function,
     const std::unordered_set<irep_idt> &instantiated_classes,
     std::unordered_set<irep_idt> &callable_methods,
     symbol_tablet &symbol_table);
@@ -171,12 +171,14 @@ class ci_lazy_methodst:public messaget
     symbol_tablet &symbol_table,
     std::unordered_set<irep_idt> &methods_to_convert_later,
     std::unordered_set<irep_idt> &instantiated_classes,
-    std::unordered_set<exprt, irep_hash> &virtual_function_calls);
+    std::unordered_set<class_method_descriptor_exprt, irep_hash>
+      &called_virtual_functions);
 
   bool handle_virtual_methods_with_no_callees(
     std::unordered_set<irep_idt> &methods_to_convert_later,
     std::unordered_set<irep_idt> &instantiated_classes,
-    const std::unordered_set<exprt, irep_hash> &virtual_function_calls,
+    const std::unordered_set<class_method_descriptor_exprt, irep_hash>
+      &virtual_functions,
     symbol_tablet &symbol_table);
 };
 

jbmc/src/java_bytecode/expr2java.cpp

@@ -420,11 +420,11 @@ std::string expr2javat::convert_with_precedence(
     return "pod_constructor";
   else if(src.id()==ID_virtual_function)
   {
-    return "VIRTUAL_FUNCTION(" +
-      id2string(src.get(ID_C_class)) +
-      "." +
-      id2string(src.get(ID_component_name)) +
-      ")";
+    const class_method_descriptor_exprt &virtual_function =
+      to_class_method_descriptor_expr(src);
+    return "CLASS_METHOD_DESCRIPTOR(" +
+           id2string(virtual_function.get_class_name()) + "." +
+           id2string(virtual_function.get_component_name()) + ")";
   }
   else if(
     const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1330,7 +1330,16 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       bytecode == BC_invokeinterface || bytecode == BC_invokespecial ||
       bytecode == BC_invokevirtual || bytecode == BC_invokestatic)
     {
-      convert_invoke(i_it->source_location, statement, arg0, c, results);
+      class_method_descriptor_exprt *class_method_descriptor =
+        expr_try_dynamic_cast<class_method_descriptor_exprt>(arg0);
+
+      INVARIANT(
+        class_method_descriptor,
+        "invokeinterface, invokespecial, invokevirtual and invokestatic should "
+        "be called with a class method descriptor expression as arg0");
+
+      convert_invoke(
+        i_it->source_location, statement, *class_method_descriptor, c, results);
     }
     else if(bytecode == BC_return)
     {
@@ -2153,15 +2162,15 @@ static void adjust_invoke_argument_types(
 void java_bytecode_convert_methodt::convert_invoke(
   source_locationt location,
   const irep_idt &statement,
-  exprt &arg0,
+  class_method_descriptor_exprt &class_method_descriptor,
   codet &c,
   exprt::operandst &results)
 {
   const bool use_this(statement != "invokestatic");
   const bool is_virtual(
     statement == "invokevirtual" || statement == "invokeinterface");
 
-  const irep_idt &invoked_method_id = arg0.get(ID_identifier);
+  const irep_idt &invoked_method_id = class_method_descriptor.get_identifier();
   INVARIANT(
     !invoked_method_id.empty(),
     "invoke statement arg0 must have an identifier");
@@ -2177,21 +2186,22 @@ void java_bytecode_convert_methodt::convert_invoke(
     // invokespecial will have zero arguments (the `this` is added below)
     // but the symbol for the <init> will have the this parameter.
     INVARIANT(
-      to_java_method_type(arg0.type()).return_type().id() ==
+      to_java_method_type(class_method_descriptor.type()).return_type().id() ==
         to_code_type(method_symbol->second.type).return_type().id(),
       "Function return type must not change in kind");
-    arg0.type() = method_symbol->second.type;
+    class_method_descriptor.type() = method_symbol->second.type;
   }
 
   // Note arg0 and arg0.type() are subject to many side-effects in this method,
   // then finally used to populate the call instruction.
-  java_method_typet &method_type = to_java_method_type(arg0.type());
+  java_method_typet &method_type =
+    to_java_method_type(class_method_descriptor.type());
 
   java_method_typet::parameterst &parameters(method_type.parameters());
 
   if(use_this)
   {
-    irep_idt classname = arg0.get(ID_C_class);
+    irep_idt classname = class_method_descriptor.get(ID_C_class);
 
     if(parameters.empty() || !parameters[0].get_this())
     {
@@ -2242,8 +2252,6 @@ void java_bytecode_convert_methodt::convert_invoke(
     results[0] = promoted;
   }
 
-  assert(arg0.id() == ID_virtual_function);
-
   // If we don't have a definition for the called symbol, and we won't
   // inherit a definition from a super-class, we create a new symbol and
   // insert it in the symbol table. The name and type of the method are
@@ -2258,16 +2266,17 @@ void java_bytecode_convert_methodt::convert_invoke(
   // We set opaque methods as final to avoid assuming they can be overridden.
   if(
     method_symbol == symbol_table.symbols.end() &&
-    !(is_virtual &&
-      is_method_inherited(arg0.get(ID_C_class), arg0.get(ID_component_name))))
+    !(is_virtual && is_method_inherited(
+                      class_method_descriptor.get_class_name(),
+                      class_method_descriptor.get_component_name())))
   {
     create_method_stub_symbol(
       invoked_method_id,
-      arg0.get(ID_C_base_name),
-      id2string(arg0.get(ID_C_class)).substr(6) + "." +
-        id2string(arg0.get(ID_C_base_name)) + "()",
+      class_method_descriptor.get_base_name(),
+      id2string(class_method_descriptor.get_class_name()).substr(6) + "." +
+        id2string(class_method_descriptor.get_base_name()) + "()",
       method_type,
-      arg0.get(ID_C_class),
+      class_method_descriptor.get_class_name(),
       symbol_table,
       get_message_handler());
   }
@@ -2278,7 +2287,7 @@ void java_bytecode_convert_methodt::convert_invoke(
     // dynamic binding
     PRECONDITION(use_this);
     PRECONDITION(!arguments.empty());
-    function = arg0;
+    function = class_method_descriptor;
     // Populate needed methods later,
     // once we know what object types can exist.
   }
@@ -2290,7 +2299,8 @@ void java_bytecode_convert_methodt::convert_invoke(
     {
       needed_lazy_methods->add_needed_method(invoked_method_id);
       // Calling a static method causes static initialization:
-      needed_lazy_methods->add_needed_class(arg0.get(ID_C_class));
+      needed_lazy_methods->add_needed_class(
+        class_method_descriptor.get_class_name());
     }
   }
 
@@ -2305,7 +2315,8 @@ void java_bytecode_convert_methodt::convert_invoke(
 
   if(!use_this)
   {
-    codet clinit_call = get_clinit_call(arg0.get(ID_C_class));
+    codet clinit_call =
+      get_clinit_call(class_method_descriptor.get_class_name());
     if(clinit_call.get_statement() != ID_skip)
       c = code_blockt({clinit_call, c});
   }

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -494,7 +494,7 @@ class java_bytecode_convert_methodt:public messaget
   void convert_invoke(
     source_locationt location,
     const irep_idt &statement,
-    exprt &arg0,
+    class_method_descriptor_exprt &class_method_descriptor,
     codet &c,
     exprt::operandst &results);
 

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -763,13 +763,8 @@ void java_bytecode_parsert::rconstant_pool()
         irep_idt identifier=
           id2string(class_name)+"."+id2string(component_name);
 
-        exprt virtual_function(ID_virtual_function, type);
-        virtual_function.set(ID_component_name, component_name);
-        virtual_function.set(ID_C_class, class_name);
-        virtual_function.set(ID_C_base_name, name_entry.s);
-        virtual_function.set(ID_identifier, identifier);
-
-        entry.expr = virtual_function;
+        entry.expr = class_method_descriptor_exprt{
+          type, component_name, class_name, name_entry.s, identifier};
       }
       break;
 

jbmc/unit/java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp

@@ -133,10 +133,11 @@ SCENARIO(
   const symbolt &callee_symbol =
     symbol_table.lookup_ref("java::VirtualFunctionsTestParent.f:()V");
 
-  exprt callee(ID_virtual_function, callee_symbol.type);
-  callee.set(ID_identifier, callee_symbol.name);
-  callee.set(ID_C_class, "java::VirtualFunctionsTestParent");
-  callee.set(ID_component_name, "f:()V");
+  class_method_descriptor_exprt callee{callee_symbol.type,
+                                       "f:()V",
+                                       "java::VirtualFunctionsTestParent",
+                                       "f",
+                                       callee_symbol.name};
 
   const code_function_callt call(
     callee,

jbmc/unit/java_bytecode/java_bytecode_instrument/virtual_call_null_checks.cpp

@@ -24,7 +24,7 @@ static bool is_expected_virtualmethod_call(
     return false;
   const auto &virtual_call = to_code_function_call(instruction.code);
   const auto &called_function = virtual_call.function();
-  if(called_function.id() != ID_virtual_function)
+  if(!can_cast_expr<class_method_descriptor_exprt>(called_function))
     return false;
   if(called_function.get(ID_identifier) != "java::B.virtualmethod:()V")
     return false;