Change code_typet to java_method_typet in JBMC

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -376,7 +376,7 @@ void ci_lazy_methodst::initialize_instantiated_classes(
   for(const auto &mname : entry_points)
   {
     const auto &symbol=ns.lookup(mname);
-    const auto &mtype=to_code_type(symbol.type);
+    const auto &mtype = to_java_method_type(symbol.type);
     for(const auto &param : mtype.parameters())
     {
       if(param.type().id()==ID_pointer)

jbmc/src/java_bytecode/expr2java.cpp

@@ -56,11 +56,10 @@ std::string expr2javat::convert_code_function_call(
     dest+='=';
   }
 
-  const code_typet &code_type=
-    to_code_type(src.function().type());
+  const java_method_typet &method_type =
+    to_java_method_type(src.function().type());
 
-  bool has_this=code_type.has_this() &&
-                !src.arguments().empty();
+  bool has_this = method_type.has_this() && !src.arguments().empty();
 
   if(has_this)
   {
@@ -284,7 +283,7 @@ std::string expr2javat::convert_rec(
     return q+"byte"+d;
   else if(src.id()==ID_code)
   {
-    const code_typet &code_type=to_code_type(src);
+    const java_method_typet &method_type = to_java_method_type(src);
 
     // Java doesn't really have syntax for function types,
     // so we make one up, loosely inspired by the syntax
@@ -293,11 +292,10 @@ std::string expr2javat::convert_rec(
     std::string dest="";
 
     dest+='(';
-    const code_typet::parameterst &parameters=code_type.parameters();
+    const java_method_typet::parameterst &parameters = method_type.parameters();
 
-    for(code_typet::parameterst::const_iterator
-        it=parameters.begin();
-        it!=parameters.end();
+    for(java_method_typet::parameterst::const_iterator it = parameters.begin();
+        it != parameters.end();
         it++)
     {
       if(it!=parameters.begin())
@@ -306,7 +304,7 @@ std::string expr2javat::convert_rec(
       dest+=convert(it->type());
     }
 
-    if(code_type.has_ellipsis())
+    if(method_type.has_ellipsis())
     {
       if(!parameters.empty())
         dest+=", ";
@@ -315,7 +313,7 @@ std::string expr2javat::convert_rec(
 
     dest+=')';
 
-    const typet &return_type=code_type.return_type();
+    const typet &return_type = method_type.return_type();
     dest+=" -> "+convert(return_type);
 
     return q + dest;

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -781,12 +781,12 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
 
     const irep_idt clone_name=
       id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
-    code_typet::parametert this_param;
+    java_method_typet::parametert this_param;
     this_param.set_identifier(id2string(clone_name)+"::this");
     this_param.set_base_name("this");
     this_param.set_this();
     this_param.type()=java_reference_type(symbol_type);
-    const code_typet clone_type({this_param}, java_lang_object_type());
+    const java_method_typet clone_type({this_param}, java_lang_object_type());
 
     parameter_symbolt this_symbol;
     this_symbol.name=this_param.get_identifier();

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -87,11 +87,11 @@ class patternt
 ///   parameters, which are initially nameless as method conversion hasn't
 ///   happened. Also creates symbols in `symbol_table`.
 static void assign_parameter_names(
-  code_typet &ftype,
+  java_method_typet &ftype,
   const irep_idt &name_prefix,
   symbol_table_baset &symbol_table)
 {
-  code_typet::parameterst &parameters=ftype.parameters();
+  java_method_typet::parameterst &parameters = ftype.parameters();
 
   // Mostly borrowed from java_bytecode_convert.cpp; maybe factor this out.
   // assign names to parameters
@@ -255,7 +255,7 @@ const exprt java_bytecode_convert_methodt::variable(
 ///   message handler to collect warnings
 /// \return
 ///   the constructed member type
-code_typet member_type_lazy(
+java_method_typet member_type_lazy(
   const std::string &descriptor,
   const optionalt<std::string> &signature,
   const std::string &class_name,
@@ -282,10 +282,11 @@ code_typet member_type_lazy(
         signature.value(),
         class_name);
       INVARIANT(member_type_from_signature.id()==ID_code, "Must be code type");
-      if(to_code_type(member_type_from_signature).parameters().size()==
-         to_code_type(member_type_from_descriptor).parameters().size())
+      if(
+        to_java_method_type(member_type_from_signature).parameters().size() ==
+        to_java_method_type(member_type_from_descriptor).parameters().size())
       {
-        return to_code_type(member_type_from_signature);
+        return to_java_method_type(member_type_from_signature);
       }
       else
       {
@@ -306,7 +307,7 @@ code_typet member_type_lazy(
                         << message.eom;
     }
   }
-  return to_code_type(member_type_from_descriptor);
+  return to_java_method_type(member_type_from_descriptor);
 }
 
 /// Retrieves the symbol of the lambda method associated with the given
@@ -345,7 +346,7 @@ void java_bytecode_convert_method_lazy(
 {
   symbolt method_symbol;
 
-  code_typet member_type = member_type_lazy(
+  java_method_typet member_type = member_type_lazy(
     m.descriptor,
     m.signature,
     id2string(class_symbol.name),
@@ -378,8 +379,8 @@ void java_bytecode_convert_method_lazy(
   // do we need to add 'this' as a parameter?
   if(!m.is_static)
   {
-    code_typet::parameterst &parameters = member_type.parameters();
-    code_typet::parametert this_p;
+    java_method_typet::parameterst &parameters = member_type.parameters();
+    java_method_typet::parametert this_p;
     const reference_typet object_ref_type=
       java_reference_type(symbol_typet(class_symbol.name));
     this_p.type()=object_ref_type;
@@ -442,12 +443,12 @@ void java_bytecode_convert_methodt::convert(
 
   symbolt &method_symbol=*symbol_table.get_writeable(method_identifier);
 
-  // Obtain a std::vector of code_typet::parametert objects from the
+  // Obtain a std::vector of java_method_typet::parametert objects from the
   // (function) type of the symbol
   java_method_typet method_type = to_java_method_type(method_symbol.type);
   method_type.set(ID_C_class, class_symbol.name);
   method_return_type = method_type.return_type();
-  code_typet::parameterst &parameters = method_type.parameters();
+  java_method_typet::parameterst &parameters = method_type.parameters();
 
   // Determine the number of local variable slots used by the JVM to maintain
   // the formal parameters
@@ -1250,9 +1251,10 @@ codet java_bytecode_convert_methodt::convert_instructions(
             id2string(arg0.get(ID_identifier))==
             "java::org.cprover.CProver.assume:(Z)V")
     {
-      const code_typet &code_type=to_code_type(arg0.type());
-      INVARIANT(code_type.parameters().size()==1,
-                "function expected to have exactly one parameter");
+      const java_method_typet &method_type = to_java_method_type(arg0.type());
+      INVARIANT(
+        method_type.parameters().size() == 1,
+        "function expected to have exactly one parameter");
       c = replace_call_to_cprover_assume(i_it->source_location, c);
     }
     // replace calls to CProver.atomicBegin
@@ -1995,8 +1997,8 @@ codet java_bytecode_convert_methodt::convert_monitorenterexit(
     return code_skipt();
 
   // becomes a function call
-  code_typet type(
-    {code_typet::parametert(java_reference_type(void_typet()))},
+  java_method_typet type(
+    {java_method_typet::parametert(java_reference_type(void_typet()))},
     void_typet());
   code_function_callt call;
   call.function() = symbol_exprt(descriptor, type);
@@ -2105,8 +2107,8 @@ void java_bytecode_convert_methodt::convert_invoke(
   const bool is_virtual(
     statement == "invokevirtual" || statement == "invokeinterface");
 
-  code_typet &code_type = to_code_type(arg0.type());
-  code_typet::parameterst &parameters(code_type.parameters());
+  java_method_typet &method_type = to_java_method_type(arg0.type());
+  java_method_typet::parameterst &parameters(method_type.parameters());
 
   if(use_this)
   {
@@ -2122,13 +2124,13 @@ void java_bytecode_convert_methodt::convert_invoke(
         {
           if(needed_lazy_methods)
             needed_lazy_methods->add_needed_class(classname);
-          code_type.set_is_constructor();
+          method_type.set_is_constructor();
         }
         else
-          code_type.set(ID_java_super_method_call, true);
+          method_type.set(ID_java_super_method_call, true);
       }
       reference_typet object_ref_type = java_reference_type(thistype);
-      code_typet::parametert this_p(object_ref_type);
+      java_method_typet::parametert this_p(object_ref_type);
       this_p.set_this();
       this_p.set_base_name("this");
       parameters.insert(parameters.begin(), this_p);
@@ -2170,7 +2172,7 @@ void java_bytecode_convert_methodt::convert_invoke(
 
   // do some type adjustment for return values
 
-  const typet &return_type = code_type.return_type();
+  const typet &return_type = method_type.return_type();
 
   if(return_type.id() != ID_empty)
   {
@@ -2215,7 +2217,7 @@ void java_bytecode_convert_methodt::convert_invoke(
     symbol.value.make_nil();
     symbol.mode = ID_java;
     assign_parameter_names(
-      to_code_type(symbol.type), symbol.name, symbol_table);
+      to_java_method_type(symbol.type), symbol.name, symbol_table);
 
     debug() << "Generating codet:  new opaque symbol: method '" << symbol.name
             << "'" << eom;
@@ -2945,11 +2947,11 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
   const source_locationt &location,
   const exprt &arg0)
 {
-  const code_typet &code_type = to_code_type(arg0.type());
+  const java_method_typet &method_type = to_java_method_type(arg0.type());
 
   const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
     lambda_method_handles,
-    code_type.get_int(ID_java_lambda_method_handle_index));
+    method_type.get_int(ID_java_lambda_method_handle_index));
   if(lambda_method_symbol.has_value())
     debug() << "Converting invokedynamic for lambda: "
             << lambda_method_symbol.value().name << eom;
@@ -2958,11 +2960,11 @@ optionalt<exprt> java_bytecode_convert_methodt::convert_invoke_dynamic(
                "type"
             << eom;
 
-  const code_typet::parameterst &parameters(code_type.parameters());
+  const java_method_typet::parameterst &parameters(method_type.parameters());
 
   pop(parameters.size());
 
-  const typet &return_type = code_type.return_type();
+  const typet &return_type = method_type.return_type();
 
   if(return_type.id() == ID_empty)
     return {};
@@ -3019,13 +3021,13 @@ void java_bytecode_initialize_parameter_names(
     &local_variable_table,
   symbol_table_baset &symbol_table)
 {
-  // Obtain a std::vector of code_typet::parametert objects from the
+  // Obtain a std::vector of java_method_typet::parametert objects from the
   // (function) type of the symbol
-  code_typet &code_type = to_code_type(method_symbol.type);
-  code_typet::parameterst &parameters = code_type.parameters();
+  java_method_typet &method_type = to_java_method_type(method_symbol.type);
+  java_method_typet::parameterst &parameters = method_type.parameters();
 
   // Find number of parameters
-  unsigned slots_for_parameters = java_method_parameter_slots(code_type);
+  unsigned slots_for_parameters = java_method_parameter_slots(method_type);
 
   // Find parameter names in the local variable table:
   typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;

jbmc/src/java_bytecode/java_bytecode_instrument.cpp

@@ -446,8 +446,8 @@ void java_bytecode_instrumentt::instrument_code(codet &code)
     add_expr_instrumentation(block, code_function_call.lhs());
     add_expr_instrumentation(block, code_function_call.function());
 
-    const code_typet &function_type=
-      to_code_type(code_function_call.function().type());
+    const java_method_typet &function_type =
+      to_java_method_type(code_function_call.function().type());
 
     // Check for a null this-argument of a virtual call:
     if(function_type.has_this())

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1068,7 +1068,7 @@ bool java_bytecode_languaget::convert_single_method(
 
   // The return of an opaque function is a source of an otherwise invisible
   // instantiation, so here we ensure we've loaded the appropriate classes.
-  const code_typet function_type = to_code_type(symbol.type);
+  const java_method_typet function_type = to_java_method_type(symbol.type);
   if(
     const pointer_typet *pointer_return_type =
       type_try_dynamic_cast<pointer_typet>(function_type.return_type()))

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -610,7 +610,7 @@ void java_bytecode_parsert::get_class_refs_rec(const typet &src)
 {
   if(src.id()==ID_code)
   {
-    const code_typet &ct=to_code_type(src);
+    const java_method_typet &ct = to_java_method_type(src);
     const typet &rt=ct.return_type();
     get_class_refs_rec(rt);
     for(const auto &p : ct.parameters())

jbmc/src/java_bytecode/java_bytecode_typecheck.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H
 
+#include "java_types.h"
+
 #include <set>
 #include <map>
 

jbmc/src/java_bytecode/java_bytecode_typecheck_type.cpp

@@ -38,13 +38,14 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
   }
   else if(type.id()==ID_code)
   {
-    code_typet &code_type=to_code_type(type);
-    typecheck_type(code_type.return_type());
+    java_method_typet &method_type = to_java_method_type(type);
+    typecheck_type(method_type.return_type());
 
-    code_typet::parameterst &parameters=code_type.parameters();
+    java_method_typet::parameterst &parameters = method_type.parameters();
 
-    for(code_typet::parameterst::iterator
-        it=parameters.begin(); it!=parameters.end(); it++)
+    for(java_method_typet::parameterst::iterator it = parameters.begin();
+        it != parameters.end();
+        it++)
       typecheck_type(it->type());
   }
 }