Change code_typet to java_method_typet in jbmc

Author: jeannielynnmoulton

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 &code_type =
+    to_java_method_type(src.function().type());
 
-  bool has_this=code_type.has_this() &&
-                !src.arguments().empty();
+  bool has_this = code_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 &code_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 = code_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())
@@ -315,7 +313,7 @@ std::string expr2javat::convert_rec(
 
     dest+=')';
 
-    const typet &return_type=code_type.return_type();
+    const typet &return_type = code_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 &code_type = to_java_method_type(arg0.type());
+      INVARIANT(
+        code_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 &code_type = to_java_method_type(arg0.type());
+  java_method_typet::parameterst &parameters(code_type.parameters());
 
   if(use_this)
   {
@@ -2128,7 +2130,7 @@ void java_bytecode_convert_methodt::convert_invoke(
           code_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);
@@ -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,7 +2947,7 @@ 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 &code_type = to_java_method_type(arg0.type());
 
   const optionalt<symbolt> &lambda_method_symbol = get_lambda_method_symbol(
     lambda_method_handles,
@@ -2958,7 +2960,7 @@ 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(code_type.parameters());
 
   pop(parameters.size());
 
@@ -3019,10 +3021,10 @@ 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 &code_type = to_java_method_type(method_symbol.type);
+  java_method_typet::parameterst &parameters = code_type.parameters();
 
   // Find number of parameters
   unsigned slots_for_parameters = java_method_parameter_slots(code_type);

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);
+    java_method_typet &code_type = to_java_method_type(type);
     typecheck_type(code_type.return_type());
 
-    code_typet::parameterst &parameters=code_type.parameters();
+    java_method_typet::parameterst &parameters = code_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());
   }
 }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -36,7 +36,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
   initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
-  initialize.type = code_typet({}, empty_typet());
+  initialize.type = java_method_typet({}, empty_typet());
 
   code_blockt init_code;
 
@@ -251,12 +251,12 @@ static void java_static_lifetime_init(
 bool is_java_main(const symbolt &function)
 {
   bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
-  const code_typet &function_type = to_code_type(function.type);
+  const java_method_typet &function_type = to_java_method_type(function.type);
   const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
   // checks whether the function is static and has a single String[] parameter
   bool is_static = !function_type.has_this();
   // this should be implied by the signature
-  const code_typet::parameterst &parameters = function_type.parameters();
+  const java_method_typet::parameterst &parameters = function_type.parameters();
   bool has_correct_type = function_type.return_type().id() == ID_empty &&
                           parameters.size() == 1 &&
                           parameters[0].type().full_eq(string_array_type);
@@ -281,8 +281,8 @@ exprt::operandst java_build_arguments(
   object_factory_parameterst object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
-  const code_typet::parameterst &parameters=
-    to_code_type(function.type).parameters();
+  const java_method_typet::parameterst &parameters =
+    to_java_method_type(function.type).parameters();
 
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
@@ -299,7 +299,7 @@ exprt::operandst java_build_arguments(
       param_number<parameters.size();
       param_number++)
   {
-    const code_typet::parametert &p=parameters[param_number];
+    const java_method_typet::parametert &p = parameters[param_number];
     const irep_idt base_name=p.get_base_name().empty()?
       ("argument#"+std::to_string(param_number)):p.get_base_name();
 
@@ -352,14 +352,14 @@ void java_record_outputs(
   code_blockt &init_code,
   symbol_table_baset &symbol_table)
 {
-  const code_typet::parameterst &parameters=
-    to_code_type(function.type).parameters();
+  const java_method_typet::parameterst &parameters =
+    to_java_method_type(function.type).parameters();
 
   exprt::operandst result;
   result.reserve(parameters.size()+1);
 
-  bool has_return_value=
-    to_code_type(function.type).return_type()!=empty_typet();
+  bool has_return_value =
+    to_java_method_type(function.type).return_type() != empty_typet();
 
   if(has_return_value)
   {
@@ -624,14 +624,14 @@ bool generate_java_start_function(
 
   // if the method return type is not void, store return value in a new variable
   // named 'return'
-  if(to_code_type(symbol.type).return_type()!=empty_typet())
+  if(to_java_method_type(symbol.type).return_type() != empty_typet())
   {
     auxiliary_symbolt return_symbol;
     return_symbol.mode=ID_java;
     return_symbol.is_static_lifetime=false;
     return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
     return_symbol.base_name="return";
-    return_symbol.type=to_code_type(symbol.type).return_type();
+    return_symbol.type = to_java_method_type(symbol.type).return_type();
 
     symbol_table.add(return_symbol);
     call_main.lhs()=return_symbol.symbol_expr();
@@ -715,7 +715,7 @@ bool generate_java_start_function(
   symbolt new_symbol;
 
   new_symbol.name=goto_functionst::entry_point();
-  new_symbol.type = code_typet({}, empty_typet());
+  new_symbol.type = java_method_typet({}, empty_typet());
   new_symbol.value.swap(init_code);
   new_symbol.mode=ID_java;
 

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1084,7 +1084,7 @@ void java_object_factoryt::gen_nondet_struct_init(
 
   if(const auto func = symbol_table.lookup(init_method_name))
   {
-    const code_typet &type = to_code_type(func->type);
+    const java_method_typet &type = to_java_method_type(func->type);
     code_function_callt fun_call;
     fun_call.function() = func->symbol_expr();
     if(type.has_this())