Make string solver functions get converted correctly first time

Previously they were replaced after everything else was done

Author: NathanJPhillips

src/java_bytecode/ci_lazy_methods.cpp

@@ -140,19 +140,17 @@ bool ci_lazy_methodst::operator()(
       {
         if(!methods_already_populated.insert(mname).second)
           continue;
-        method_bytecodet::opt_reft cmb = method_bytecode.get(mname);
-        if(!cmb)
+        debug() << "CI lazy methods: elaborate " << mname << eom;
+        if(
+          method_converter(
+            mname,
+            // Note this wraps *references* to method_worklist2 & needed_classes
+            ci_lazy_methods_neededt(
+              method_worklist2, needed_classes, symbol_table)))
         {
-          debug() << "Skip " << mname << eom;
+          // Couldn't convert this function
           continue;
         }
-        debug() << "CI lazy methods: elaborate " << mname << eom;
-        method_converter(
-          symbol_table.lookup_ref(cmb->get().class_id),
-          cmb->get().method,
-          // Note this wraps *references* to method_worklist2 & needed_classes
-          ci_lazy_methods_neededt(
-            method_worklist2, needed_classes, symbol_table));
         gather_virtual_callsites(
           symbol_table.lookup_ref(mname).value,
           virtual_callsites);
@@ -186,16 +184,23 @@ bool ci_lazy_methodst::operator()(
 
   for(const auto &sym : symbol_table.symbols)
   {
+    // Don't keep global variables (unless they're gathered below from a
+    // function that references them)
     if(sym.second.is_static_lifetime)
       continue;
-    if(
-      method_bytecode.contains_method(sym.first) &&
-      !methods_already_populated.count(sym.first))
-    {
-      continue;
-    }
     if(sym.second.type.id()==ID_code)
+    {
+      // Don't keep functions that belong to this language that we haven't
+      // converted above
+      if(
+        method_bytecode.contains_method(sym.first) &&
+        !methods_already_populated.count(sym.first))
+      {
+        continue;
+      }
+      // If this is a function then add all the things used in it
       gather_needed_globals(sym.second.value, symbol_table, keep_symbols);
+    }
     keep_symbols.add(sym.second);
   }
 

src/java_bytecode/ci_lazy_methods.h

@@ -84,10 +84,9 @@ class method_bytecodet
   }
 };
 
-typedef std::function<void(
-  const symbolt &,
-  const java_bytecode_parse_treet::methodt &,
-  ci_lazy_methods_neededt)> method_convertert;
+typedef std::function<
+  bool(const irep_idt &function_id, ci_lazy_methods_neededt)>
+  method_convertert;
 
 class ci_lazy_methodst:public messaget
 {

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -79,10 +79,10 @@ class patternt
 /// \return Assigns parameter names (side-effects on `ftype`) to function stub
 ///   parameters, which are initially nameless as method conversion hasn't
 ///   happened. Also creates symbols in `symbol_table`.
-void assign_parameter_names(
+static void assign_parameter_names(
   code_typet &ftype,
   const irep_idt &name_prefix,
-  symbol_tablet &symbol_table)
+  symbol_table_baset &symbol_table)
 {
   code_typet::parameterst &parameters=ftype.parameters();
 
@@ -2847,7 +2847,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &method,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,

src/java_bytecode/java_bytecode_convert_method.h

@@ -24,30 +24,12 @@ class class_hierarchyt;
 void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &,
-  symbol_tablet &symbol_table,
+  symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
   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,
-  java_string_library_preprocesst &string_preprocess)
-{
-  java_bytecode_convert_method(
-    class_symbol,
-    method,
-    symbol_table,
-    message_handler,
-    max_array_length,
-    optionalt<ci_lazy_methods_neededt>(),
-    string_preprocess);
-}
-
 void java_bytecode_convert_method_lazy(
   const symbolt &class_symbol,
   const irep_idt &method_identifier,

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -31,13 +31,13 @@ class java_bytecode_convert_methodt:public messaget
 {
 public:
   java_bytecode_convert_methodt(
-    symbol_tablet &_symbol_table,
+    symbol_table_baset &symbol_table,
     message_handlert &_message_handler,
     size_t _max_array_length,
     optionalt<ci_lazy_methods_neededt> needed_lazy_methods,
     java_string_library_preprocesst &_string_preprocess)
     : messaget(_message_handler),
-      symbol_table(_symbol_table),
+      symbol_table(symbol_table),
       max_array_length(_max_array_length),
       needed_lazy_methods(std::move(needed_lazy_methods)),
       string_preprocess(_string_preprocess),
@@ -58,7 +58,7 @@ class java_bytecode_convert_methodt:public messaget
   }
 
 protected:
-  symbol_tablet &symbol_table;
+  symbol_table_baset &symbol_table;
   const size_t max_array_length;
   optionalt<ci_lazy_methods_neededt> needed_lazy_methods;
 

src/java_bytecode/java_bytecode_language.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/suffix.h>
 #include <util/config.h>
 #include <util/cmdline.h>
+#include <util/journalling_symbol_table.h>
 #include <util/string2int.h>
 #include <util/invariant.h>
 #include <json/json_parser.h>
@@ -247,16 +248,20 @@ bool java_bytecode_languaget::typecheck(
   }
   else if(lazy_methods_mode==LAZY_METHODS_MODE_EAGER)
   {
-    // Simply elaborate all methods symbols now.
+    journalling_symbol_tablet journalling_symbol_table =
+      journalling_symbol_tablet::wrap(symbol_table);
+    // Convert all methods for which we have bytecode now
     for(const auto &method_sig : method_bytecode)
     {
-      java_bytecode_convert_method(
-        symbol_table.lookup_ref(method_sig.second.class_id),
-        method_sig.second.method,
-        symbol_table,
-        get_message_handler(),
-        max_user_array_length,
-        string_preprocess);
+      convert_single_method(method_sig.first, journalling_symbol_table);
+    }
+    // Now convert all newly added string methods
+    id_sett string_methods;
+    string_preprocess.get_all_function_names(string_methods);
+    for(const auto &fn_name : journalling_symbol_table.get_inserted())
+    {
+      if(string_methods.count(fn_name) != 0)
+        convert_single_method(fn_name, symbol_table);
     }
   }
   // Otherwise our caller is in charge of elaborating methods on demand.
@@ -310,19 +315,13 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion(
   symbol_tablet &symbol_table,
   method_bytecodet &method_bytecode)
 {
-  const auto method_converter = [&](
-    const symbolt &symbol,
-    const java_bytecode_parse_treet::methodt &method,
-    ci_lazy_methods_neededt new_lazy_methods) {
-    java_bytecode_convert_method(
-      symbol,
-      method,
-      symbol_table,
-      get_message_handler(),
-      max_user_array_length,
-      std::move(new_lazy_methods),
-      string_preprocess);
-  };
+  const method_convertert method_converter =
+    [this, &symbol_table]
+      (const irep_idt &function_id, ci_lazy_methods_neededt lazy_methods_needed)
+    {
+      return convert_single_method(
+        function_id, symbol_table, std::move(lazy_methods_needed));
+    };
 
   ci_lazy_methodst method_gather(
     symbol_table,
@@ -349,9 +348,11 @@ const select_pointer_typet &
 /// \return Populates `methods` with the complete list of lazy methods that are
 ///   available to convert (those which are valid parameters for
 ///   `convert_lazy_method`)
-void java_bytecode_languaget::methods_provided(
-  std::set<irep_idt> &methods) const
+void java_bytecode_languaget::methods_provided(id_sett &methods) const
 {
+  // Add all string solver methods to map
+  string_preprocess.get_all_function_names(methods);
+  // Add all concrete methods to map
   for(const auto &kv : method_bytecode)
     methods.insert(kv.first);
 }
@@ -368,59 +369,60 @@ void java_bytecode_languaget::convert_lazy_method(
   const irep_idt &function_id,
   symbol_tablet &symbol_table)
 {
-  const method_bytecodet::class_method_and_bytecodet &cmb =
-    *method_bytecode.get(function_id);
-  java_bytecode_convert_method(
-    symbol_table.lookup_ref(cmb.class_id),
-    cmb.method,
-    symbol_table,
-    get_message_handler(),
-    max_user_array_length,
-    string_preprocess);
+  convert_single_method(function_id, symbol_table);
 }
 
-/// Replace methods of the String library that are in the symbol table by code
-/// generated by string_preprocess.
-/// \param context: a symbol table
-void java_bytecode_languaget::replace_string_methods(
-  symbol_table_baset &context)
+/// \brief Convert a method (one whose type is known but whose body hasn't
+///   been converted) but don't run typecheck, etc
+/// \remarks Amends the symbol table entry for function `function_id`, which
+///   should be a method provided by this instance of `java_bytecode_languaget`
+///   to have a value representing the method body.
+/// \param function_id: method ID to convert
+/// \param symbol_table: global symbol table
+/// \param needed_lazy_methods: optionally a collection of needed methods to
+///   update with any methods touched during the conversion
+bool java_bytecode_languaget::convert_single_method(
+  const irep_idt &function_id,
+  symbol_table_baset &symbol_table,
+  optionalt<ci_lazy_methods_neededt> needed_lazy_methods)
 {
-  // Symbols that have code type are potentialy to be replaced
-  std::list<symbolt> code_symbols;
-  forall_symbols(symbol, context.symbols)
+  const symbolt &symbol = symbol_table.lookup_ref(function_id);
+
+  // Nothing to do if body is already loaded
+  if(symbol.value.is_not_nil())
+    return false;
+
+  exprt generated_code =
+    string_preprocess.code_for_function(symbol, symbol_table);
+  if(generated_code.is_not_nil())
   {
-    if(symbol->second.type.id()==ID_code)
-      code_symbols.push_back(symbol->second);
+    // Populate body of the function with code generated by string preprocess
+    symbol_table.get_writeable_ref(function_id).value = generated_code;
+    return false;
   }
 
-  for(const auto &symbol : code_symbols)
+  // No string solver implementation, check if have bytecode for it
+  method_bytecodet::opt_reft cmb = method_bytecode.get(function_id);
+  if(cmb)
   {
-    const irep_idt &id=symbol.name;
-    exprt generated_code=string_preprocess.code_for_function(
-      id, to_code_type(symbol.type), symbol.location, context);
-    if(generated_code.is_not_nil())
-    {
-      // Replace body of the function by code generated by string preprocess
-      symbolt &symbol=*context.get_writeable(id);
-      symbol.value=generated_code;
-      // Specifically instrument the new code, since this comes after the
-      // blanket instrumentation pass called before typechecking.
-      java_bytecode_instrument_symbol(
-        context,
-        symbol,
-        throw_runtime_exceptions,
-        get_message_handler());
-    }
+    java_bytecode_convert_method(
+      symbol_table.lookup_ref(cmb->get().class_id),
+      cmb->get().method,
+      symbol_table,
+      get_message_handler(),
+      max_user_array_length,
+      std::move(needed_lazy_methods),
+      string_preprocess);
+    return false;
   }
+
+  return true;
 }
 
 bool java_bytecode_languaget::final(symbol_table_baset &symbol_table)
 {
   PRECONDITION(language_options_initialized);
 
-  // replace code of String methods calls by code we generate
-  replace_string_methods(symbol_table);
-
   return false;
 }
 

src/java_bytecode/java_bytecode_language.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/make_unique.h>
 
 #include "ci_lazy_methods.h"
+#include "ci_lazy_methods_needed.h"
 #include "java_class_loader.h"
 #include "java_string_library_preprocess.h"
 
@@ -103,8 +104,6 @@ class java_bytecode_languaget:public languaget
     symbol_tablet &context,
     const std::string &module) override;
 
-  void replace_string_methods(symbol_table_baset &context);
-
   virtual bool final(symbol_table_baset &context) override;
 
   void show_parse(std::ostream &out) override;
@@ -150,12 +149,24 @@ class java_bytecode_languaget:public languaget
   std::set<std::string> extensions() const override;
 
   void modules_provided(std::set<std::string> &modules) override;
-  virtual void methods_provided(std::set<irep_idt> &methods) const override;
+  virtual void methods_provided(id_sett &methods) const override;
   virtual void convert_lazy_method(
     const irep_idt &function_id,
     symbol_tablet &symbol_table) override;
 
 protected:
+  void convert_single_method(
+    const irep_idt &function_id,
+    symbol_table_baset &symbol_table)
+  {
+    convert_single_method(
+      function_id, symbol_table, optionalt<ci_lazy_methods_neededt>());
+  }
+  bool convert_single_method(
+    const irep_idt &function_id,
+    symbol_table_baset &symbol_table,
+    optionalt<ci_lazy_methods_neededt> needed_lazy_methods);
+
   bool do_ci_lazy_method_conversion(symbol_tablet &, method_bytecodet &);
   const select_pointer_typet &get_pointer_type_selector() const;