Merge pull request diffblue#1773 from smowton/smowton/feature/string-solver-ensure-class-graph-consistency

Java string solver: ensure base types are loaded

Author: smowton

src/java_bytecode/java_bytecode_language.cpp

@@ -147,6 +147,16 @@ bool java_bytecode_languaget::parse(
   java_class_loader.set_message_handler(get_message_handler());
   java_class_loader.set_java_cp_include_files(java_cp_include_files);
   java_class_loader.add_load_classes(java_load_classes);
+  if(string_refinement_enabled)
+  {
+    string_preprocess.initialize_known_type_table();
+
+    auto get_string_base_classes = [this](const irep_idt &id) { // NOLINT (*)
+      return string_preprocess.get_string_type_base_classes(id);
+    };
+
+    java_class_loader.set_extra_class_refs_function(get_string_base_classes);
+  }
 
   // look at extension
   if(has_suffix(path, ".class"))

src/java_bytecode/java_class_loader.cpp

@@ -72,6 +72,16 @@ java_bytecode_parse_treet &java_class_loadert::operator()(
         it!=parse_tree.class_refs.end();
         it++)
       queue.push(*it);
+
+    // Add any extra dependencies provided by our caller:
+    if(get_extra_class_refs)
+    {
+      std::vector<irep_idt> extra_class_refs =
+        get_extra_class_refs(c);
+
+      for(const irep_idt &id : extra_class_refs)
+        queue.push(id);
+    }
   }
 
   return class_map[class_name];
@@ -83,6 +93,16 @@ void java_class_loadert::set_java_cp_include_files(
   java_cp_include_files=_java_cp_include_files;
 }
 
+/// Sets a function that provides extra dependencies for a particular class.
+/// Currently used by the string preprocessor to note that even if we don't
+/// have a definition of core string types, it will nontheless give them
+/// certain known superclasses and interfaces, such as Serializable.
+void java_class_loadert::set_extra_class_refs_function(
+  java_class_loadert::get_extra_class_refs_functiont func)
+{
+  get_extra_class_refs = func;
+}
+
 /// Retrieves a class file from a jar and loads it into the tree
 bool java_class_loadert::get_class_file(
   java_class_loader_limitt &class_loader_limit,

src/java_bytecode/java_class_loader.h

@@ -34,6 +34,12 @@ class java_class_loadert:public messaget
   void set_java_cp_include_files(std::string &);
   void add_load_classes(const std::vector<irep_idt> &);
 
+  /// A function that yields a list of extra dependencies based on a class name.
+  typedef std::function<std::vector<irep_idt>(const irep_idt &)>
+    get_extra_class_refs_functiont;
+
+  void set_extra_class_refs_function(get_extra_class_refs_functiont func);
+
   static std::string file_to_class_name(const std::string &);
   static std::string class_name_to_file(const irep_idt &);
 
@@ -133,6 +139,7 @@ class java_class_loadert:public messaget
 private:
   std::map<std::string, jar_filet> m_archives;
   std::vector<irep_idt> java_load_classes;
+  get_extra_class_refs_functiont get_extra_class_refs;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H

src/java_bytecode/java_string_library_preprocess.cpp

@@ -186,6 +186,34 @@ typet string_length_type()
   return java_int_type();
 }
 
+/// Gets the base classes for known String and String-related types, or returns
+/// an empty list for other types.
+/// \param class_name: class identifier, without "java::" prefix.
+/// \return a list of base classes, again without "java::" prefix.
+std::vector<irep_idt>
+java_string_library_preprocesst::get_string_type_base_classes(
+  const irep_idt &class_name)
+{
+  if(!is_known_string_type(class_name))
+    return {};
+
+  std::vector<irep_idt> bases;
+  bases.reserve(3);
+  if(class_name != "java.lang.CharSequence")
+  {
+    bases.push_back("java.io.Serializable");
+    bases.push_back("java.lang.CharSequence");
+  }
+  if(class_name == "java.lang.String")
+    bases.push_back("java.lang.Comparable");
+
+  if(class_name == "java.lang.StringBuilder" ||
+     class_name == "java.lang.StringBuffer")
+    bases.push_back("java.lang.AbstractStringBuilder");
+
+  return bases;
+}
+
 /// Add to the symbol table type declaration for a String-like Java class.
 /// \param class_name: a name for the class such as "java.lang.String"
 /// \param symbol_table: symbol table to which the class will be added
@@ -206,17 +234,10 @@ void java_string_library_preprocesst::add_string_type(
   string_type.components()[2].type() = pointer_type(java_char_type());
   string_type.set_access(ID_public);
   string_type.add_base(symbol_typet("java::java.lang.Object"));
-  if(class_name!="java.lang.CharSequence")
-  {
-    string_type.add_base(symbol_typet("java::java.io.Serializable"));
-    string_type.add_base(symbol_typet("java::java.lang.CharSequence"));
-  }
-  if(class_name=="java.lang.String")
-    string_type.add_base(symbol_typet("java::java.lang.Comparable"));
 
-  if(class_name=="java.lang.StringBuilder" ||
-     class_name=="java.lang.StringBuffer")
-    string_type.add_base(symbol_typet("java::java.lang.AbstractStringBuilder"));
+  std::vector<irep_idt> bases = get_string_type_base_classes(class_name);
+  for(const irep_idt &base_name : bases)
+    string_type.add_base(symbol_typet("java::" + id2string(base_name)));
 
   symbolt tmp_string_symbol;
   tmp_string_symbol.name="java::"+id2string(class_name);
@@ -1848,16 +1869,19 @@ bool java_string_library_preprocesst::is_known_string_type(
   return string_types.find(class_name)!=string_types.end();
 }
 
-/// fill maps with correspondence from java method names to conversion functions
-void java_string_library_preprocesst::initialize_conversion_table()
+void java_string_library_preprocesst::initialize_known_type_table()
 {
-  character_preprocess.initialize_conversion_table();
-
   string_types=
     std::unordered_set<irep_idt, irep_id_hash>{"java.lang.String",
                                                "java.lang.StringBuilder",
                                                "java.lang.CharSequence",
                                                "java.lang.StringBuffer"};
+}
+
+/// fill maps with correspondence from java method names to conversion functions
+void java_string_library_preprocesst::initialize_conversion_table()
+{
+  character_preprocess.initialize_conversion_table();
 
   // The following list of function is organized by libraries, with
   // constructors first and then methods in alphabetic order.

src/java_bytecode/java_string_library_preprocess.h

@@ -43,6 +43,7 @@ class java_string_library_preprocesst:public messaget
   {
   }
 
+  void initialize_known_type_table();
   void initialize_conversion_table();
   void initialize_refined_string_type();
 
@@ -56,6 +57,8 @@ class java_string_library_preprocesst:public messaget
   {
     return character_preprocess.replace_character_call(call);
   }
+  std::vector<irep_idt> get_string_type_base_classes(
+    const irep_idt &class_name);
   void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table);
   bool is_known_string_type(irep_idt class_name);