Merging string and character preprocess as one argument of bytecode conversion

Removing add_string_type declaration, not used anymore

Author: romainbrenguier

src/java_bytecode/Makefile

@@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \
       java_object_factory.cpp \
       java_pointer_casts.cpp \
       java_root_class.cpp \
+      java_string_library_preprocess.cpp \
       java_types.cpp \
       java_utils.cpp \
       # Empty last line

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -31,13 +31,13 @@ class java_bytecode_convert_classt:public messaget
     size_t _max_array_length,
     lazy_methodst& _lazy_methods,
     lazy_methods_modet _lazy_methods_mode,
-    bool _string_refinement_enabled):
+    const java_string_library_preprocesst &_string_preprocess):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     max_array_length(_max_array_length),
     lazy_methods(_lazy_methods),
     lazy_methods_mode(_lazy_methods_mode),
-    string_refinement_enabled(_string_refinement_enabled)
+    string_preprocess(_string_preprocess)
   {
   }
 
@@ -47,18 +47,10 @@ class java_bytecode_convert_classt:public messaget
 
     if(parse_tree.loading_successful)
       convert(parse_tree.parsed_class);
-    else if(string_refinement_enabled &&
-            parse_tree.parsed_class.name=="java.lang.String")
-      add_string_type("java.lang.String");
-    else if(string_refinement_enabled &&
-            parse_tree.parsed_class.name=="java.lang.StringBuilder")
-      add_string_type("java.lang.StringBuilder");
-    else if(string_refinement_enabled &&
-            parse_tree.parsed_class.name=="java.lang.CharSequence")
-      add_string_type("java.lang.CharSequence");
-    else if(string_refinement_enabled &&
-            parse_tree.parsed_class.name=="java.lang.StringBuffer")
-      add_string_type("java.lang.StringBuffer");
+    else if(string_preprocess.is_known_string_type(
+              parse_tree.parsed_class.name))
+      string_preprocess.add_string_type(
+        parse_tree.parsed_class.name, symbol_table);
     else
       generate_class_stub(parse_tree.parsed_class.name);
   }
@@ -71,15 +63,14 @@ class java_bytecode_convert_classt:public messaget
   const size_t max_array_length;
   lazy_methodst &lazy_methods;
   lazy_methods_modet lazy_methods_mode;
-  bool string_refinement_enabled;
+  java_string_library_preprocesst string_preprocess;
 
   // conversion
   void convert(const classt &c);
   void convert(symbolt &class_symbol, const fieldt &f);
 
   void generate_class_stub(const irep_idt &class_name);
   void add_array_types();
-  void add_string_type(const irep_idt &class_name);
 };
 
 /*******************************************************************\
@@ -486,15 +477,15 @@ bool java_bytecode_convert_class(
   size_t max_array_length,
   lazy_methodst &lazy_methods,
   lazy_methods_modet lazy_methods_mode,
-  bool string_refinement_enabled)
+  const java_string_library_preprocesst &string_preprocess)
 {
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,
     message_handler,
     max_array_length,
     lazy_methods,
     lazy_methods_mode,
-    string_refinement_enabled);
+    string_preprocess);
 
   try
   {
@@ -518,66 +509,3 @@ bool java_bytecode_convert_class(
 
   return true;
 }
-
-/*******************************************************************\
-
-Function: java_bytecode_convert_classt::add_string_type
-
-  Inputs: a name for the class such as "java.lang.String"
-
- Purpose: Implements the java.lang.String type in the case that
-          we provide an internal implementation.
-
-\*******************************************************************/
-
-void java_bytecode_convert_classt::add_string_type(const irep_idt &class_name)
-{
-  class_typet string_type;
-  string_type.set_tag(class_name);
-  string_type.components().resize(3);
-  string_type.components()[0].set_name("@java.lang.Object");
-  string_type.components()[0].set_pretty_name("@java.lang.Object");
-  string_type.components()[0].type()=symbol_typet("java::java.lang.Object");
-  string_type.components()[1].set_name("length");
-  string_type.components()[1].set_pretty_name("length");
-  string_type.components()[1].type()=java_int_type();
-  string_type.components()[2].set_name("data");
-  string_type.components()[2].set_pretty_name("data");
-  // Use a pointer-to-unbounded-array instead of a pointer-to-char.
-  // Saves some casting in the string refinement algorithm but may
-  // be unnecessary.
-  string_type.components()[2].type()=pointer_typet(
-    array_typet(java_char_type(), infinity_exprt(java_int_type())));
-  string_type.add_base(symbol_typet("java::java.lang.Object"));
-
-  symbolt string_symbol;
-  string_symbol.name="java::"+id2string(class_name);
-  string_symbol.base_name=id2string(class_name);
-  string_symbol.type=string_type;
-  string_symbol.is_type=true;
-
-  symbol_table.add(string_symbol);
-
-  // Also add a stub of `String.equals` so that remove-virtual-functions
-  // generates a check for Object.equals vs. String.equals.
-  // No need to fill it in, as pass_preprocess will replace the calls again.
-  symbolt string_equals_symbol;
-  string_equals_symbol.name=
-    "java::java.lang.String.equals:(Ljava/lang/Object;)Z";
-  string_equals_symbol.base_name=id2string(class_name)+".equals";
-  string_equals_symbol.pretty_name=id2string(class_name)+".equals";
-  string_equals_symbol.mode=ID_java;
-
-  code_typet string_equals_type;
-  string_equals_type.return_type()=java_boolean_type();
-  code_typet::parametert thisparam;
-  thisparam.set_this();
-  thisparam.type()=pointer_typet(symbol_typet(string_symbol.name));
-  code_typet::parametert otherparam;
-  otherparam.type()=pointer_typet(symbol_typet("java::java.lang.Object"));
-  string_equals_type.parameters().push_back(thisparam);
-  string_equals_type.parameters().push_back(otherparam);
-  string_equals_symbol.type=std::move(string_equals_type);
-
-  symbol_table.add(string_equals_symbol);
-}

src/java_bytecode/java_bytecode_convert_class.h

@@ -22,6 +22,6 @@ bool java_bytecode_convert_class(
   size_t max_array_length,
   lazy_methodst &,
   lazy_methods_modet,
-  bool string_refinement_enabled);
+  const java_string_library_preprocesst &string_preprocess);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -1556,8 +1556,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
           symbol.name,
           symbol_table);
 
-        // functions of the String libraries can have code
-        // generated for them
+        // The string refinement module may provide a definition for this
+        // function.
         symbol.value=string_preprocess.code_for_function(
           id, to_code_type(symbol.type), loc, symbol_table);
 

src/java_bytecode/java_bytecode_convert_method.h

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 #include <util/message.h>
 #include <util/safe_pointer.h>
+#include "java_string_library_preprocess.h"
 
 #include "java_bytecode_parse_tree.h"
 #include "ci_lazy_methods.h"
@@ -24,22 +25,25 @@ void java_bytecode_convert_method(
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
-  safe_pointer<ci_lazy_methodst> lazy_methods);
+  safe_pointer<ci_lazy_methodst> lazy_methods,
+  const java_string_library_preprocesst &string_preprocess);
 
 inline void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
-  size_t max_array_length)
+  size_t max_array_length,
+  const java_string_library_preprocesst &string_preprocess)
 {
   java_bytecode_convert_method(
     class_symbol,
     method,
     symbol_table,
     message_handler,
     max_array_length,
-    safe_pointer<ci_lazy_methodst>::create_null());
+    safe_pointer<ci_lazy_methodst>::create_null(),
+    string_preprocess);
 }
 
 void java_bytecode_convert_method_lazy(

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -32,11 +32,13 @@ class java_bytecode_convert_methodt:public messaget
     symbol_tablet &_symbol_table,
     message_handlert &_message_handler,
     size_t _max_array_length,
-    safe_pointer<ci_lazy_methodst> _lazy_methods):
+    safe_pointer<ci_lazy_methodst> _lazy_methods,
+    const java_string_library_preprocesst &_string_preprocess):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     max_array_length(_max_array_length),
-    lazy_methods(_lazy_methods)
+    lazy_methods(_lazy_methods),
+    string_preprocess(_string_preprocess)
   {
   }
 
@@ -59,6 +61,7 @@ class java_bytecode_convert_methodt:public messaget
   irep_idt method_id;
   irep_idt current_method;
   typet method_return_type;
+  java_string_library_preprocesst string_preprocess;
 
 public:
   struct holet

src/java_bytecode/java_bytecode_language.cpp

@@ -511,6 +511,9 @@ bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
+  if(string_refinement_enabled)
+    string_preprocess.initialize_conversion_table();
+
   // first convert all
   for(java_class_loadert::class_mapt::const_iterator
       c_it=java_class_loader.class_map.begin();
@@ -529,7 +532,7 @@ bool java_bytecode_languaget::typecheck(
          max_user_array_length,
          lazy_methods,
          lazy_methods_mode,
-         string_refinement_enabled))
+         string_preprocess))
       return true;
   }
 
@@ -551,7 +554,8 @@ bool java_bytecode_languaget::typecheck(
         *method_sig.second.second,
         symbol_table,
         get_message_handler(),
-        max_user_array_length);
+        max_user_array_length,
+        string_preprocess);
     }
   }
   // Otherwise our caller is in charge of elaborating methods on demand.
@@ -678,7 +682,8 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
           symbol_table,
           get_message_handler(),
           max_user_array_length,
-          safe_pointer<ci_lazy_methodst>::create_non_null(&lazy_methods));
+          safe_pointer<ci_lazy_methodst>::create_non_null(&lazy_methods),
+          string_preprocess);
         gather_virtual_callsites(
           symbol_table.lookup(mname).value,
           virtual_callsites);
@@ -788,7 +793,8 @@ void java_bytecode_languaget::convert_lazy_method(
     *lazy_method_entry.second,
     symtab,
     get_message_handler(),
-    max_user_array_length);
+    max_user_array_length,
+    string_preprocess);
 }
 
 /*******************************************************************\

src/java_bytecode/java_bytecode_language.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cmdline.h>
 
 #include "java_class_loader.h"
+#include "java_string_library_preprocess.h"
 
 #define MAX_NONDET_ARRAY_LENGTH_DEFAULT 5
 
@@ -99,6 +100,7 @@ class java_bytecode_languaget:public languaget
   lazy_methodst lazy_methods;
   lazy_methods_modet lazy_methods_mode;
   bool string_refinement_enabled;
+  java_string_library_preprocesst string_preprocess;
   std::string java_cp_include_files;
 };