Lazy goto model: hook for driver program to replace or stub functions

This provides a hook for the driver program to either replace a method outright, or to provide a
stub implementation when a function body cannot be provided by the language frontend (language_filest).

Author: smowton

src/goto-programs/lazy_goto_functions_map.h

@@ -54,6 +54,15 @@ class lazy_goto_functions_mapt final
       goto_functionst::goto_functiont &function,
       journalling_symbol_tablet &function_symbols)>
     post_process_functiont;
+  typedef std::function<bool(const irep_idt &name)>
+    can_generate_function_bodyt;
+  typedef std::function<
+    bool(
+      symbolt &symbol,
+      symbol_table_baset &symbol_table,
+      goto_functiont &function,
+      bool body_available)>
+    generate_function_bodyt;
 
 private:
   typedef std::map<key_type, goto_functiont> underlying_mapt;
@@ -66,6 +75,8 @@ class lazy_goto_functions_mapt final
   language_filest &language_files;
   symbol_tablet &symbol_table;
   const post_process_functiont post_process_function;
+  const can_generate_function_bodyt driver_program_can_generate_function_body;
+  const generate_function_bodyt driver_program_generate_function_body;
   message_handlert &message_handler;
 
 public:
@@ -75,11 +86,17 @@ class lazy_goto_functions_mapt final
     language_filest &language_files,
     symbol_tablet &symbol_table,
     post_process_functiont post_process_function,
+    can_generate_function_bodyt driver_program_can_generate_function_body,
+    generate_function_bodyt driver_program_generate_function_body,
     message_handlert &message_handler)
   : goto_functions(goto_functions),
     language_files(language_files),
     symbol_table(symbol_table),
     post_process_function(std::move(post_process_function)),
+    driver_program_can_generate_function_body(
+      std::move(driver_program_can_generate_function_body)),
+    driver_program_generate_function_body(
+      std::move(driver_program_generate_function_body)),
     message_handler(message_handler)
   {
   }
@@ -107,7 +124,9 @@ class lazy_goto_functions_mapt final
   ///   it a bodyless stub.
   bool can_produce_function(const key_type &name) const
   {
-    return language_files.can_convert_lazy_method(name);
+    return
+      language_files.can_convert_lazy_method(name) ||
+      driver_program_can_generate_function_body(name);
   }
 
   void unload(const key_type &name) const { goto_functions.erase(name); }
@@ -153,14 +172,31 @@ class lazy_goto_functions_mapt final
     underlying_mapt::iterator it=goto_functions.find(name);
     if(it!=goto_functions.end())
       return *it;
-    // Fill in symbol table entry body if not already done
-    // If this returns false then it's a stub
-    language_files.convert_lazy_method(name, function_symbol_table);
-    // Create goto_functiont
-    goto_functionst::goto_functiont function;
-    goto_convert_functionst convert_functions(
-      function_symbol_table, message_handler);
-    convert_functions.convert_function(name, function);
+
+    symbolt &function_symbol = function_symbol_table.get_writeable_ref(name);
+    goto_functiont function;
+
+    // First chance: see if the driver program wants to provide a replacement:
+    bool body_provided =
+      driver_program_generate_function_body(
+        function_symbol,
+        function_symbol_table,
+        function,
+        language_files.can_convert_lazy_method(name));
+
+    // Second chance: see if language_filest can provide a body:
+    if(!body_provided)
+    {
+      // Fill in symbol table entry body if not already done
+      language_files.convert_lazy_method(name, function_symbol_table);
+      body_provided = function_symbol.value.is_not_nil();
+
+      // Create goto_functiont
+      goto_convert_functionst convert_functions(
+        function_symbol_table, message_handler);
+      convert_functions.convert_function(name, function);
+    }
+
     // Add to map
     return *goto_functions.emplace(name, std::move(function)).first;
   }

src/goto-programs/lazy_goto_model.cpp

@@ -22,6 +22,8 @@
 lazy_goto_modelt::lazy_goto_modelt(
   post_process_functiont post_process_function,
   post_process_functionst post_process_functions,
+  can_generate_function_bodyt driver_program_can_generate_function_body,
+  generate_function_bodyt driver_program_generate_function_body,
   message_handlert &message_handler)
   : goto_model(new goto_modelt()),
     symbol_table(goto_model->symbol_table),
@@ -41,9 +43,15 @@ lazy_goto_modelt::lazy_goto_modelt(
           function);
         this->post_process_function(model_function, *this);
       },
+      std::move(driver_program_can_generate_function_body),
+      std::move(driver_program_generate_function_body),
       message_handler),
     post_process_function(std::move(post_process_function)),
     post_process_functions(std::move(post_process_functions)),
+    driver_program_can_generate_function_body(
+      std::move(driver_program_can_generate_function_body)),
+    driver_program_generate_function_body(
+      std::move(driver_program_generate_function_body)),
     message_handler(message_handler)
 {
   language_files.set_message_handler(message_handler);
@@ -68,6 +76,8 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
           function);
         this->post_process_function(model_function, *this);
       },
+      other.driver_program_can_generate_function_body,
+      other.driver_program_generate_function_body,
       other.message_handler),
     language_files(std::move(other.language_files)),
     post_process_function(std::move(other.post_process_function)),

src/goto-programs/lazy_goto_model.h

@@ -24,10 +24,16 @@ class lazy_goto_modelt : public abstract_goto_modelt
     void(goto_model_functiont &function, const abstract_goto_modelt &)>
     post_process_functiont;
   typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
+  typedef lazy_goto_functions_mapt::can_generate_function_bodyt
+    can_generate_function_bodyt;
+  typedef lazy_goto_functions_mapt::generate_function_bodyt
+    generate_function_bodyt;
 
   explicit lazy_goto_modelt(
     post_process_functiont post_process_function,
     post_process_functionst post_process_functions,
+    can_generate_function_bodyt driver_program_can_generate_function_body,
+    generate_function_bodyt driver_program_generate_function_body,
     message_handlert &message_handler);
 
   lazy_goto_modelt(lazy_goto_modelt &&other);
@@ -60,6 +66,19 @@ class lazy_goto_modelt : public abstract_goto_modelt
       [&handler, &options](goto_modelt &goto_model) -> bool {
         return handler.process_goto_functions(goto_model, options);
       },
+      [&handler](const irep_idt &name) -> bool {
+        return handler.can_generate_function_body(name);
+      },
+      [&handler]
+      (symbolt &symbol,
+       symbol_table_baset &symbol_table,
+       goto_functiont &function,
+       bool is_first_chance)
+      {
+        return
+          handler.generate_function_body(
+            symbol, symbol_table, function, is_first_chance);
+      },
       message_handler);
   }
 
@@ -127,6 +146,8 @@ class lazy_goto_modelt : public abstract_goto_modelt
   // Function/module processing functions
   const post_process_functiont post_process_function;
   const post_process_functionst post_process_functions;
+  const can_generate_function_bodyt driver_program_can_generate_function_body;
+  const generate_function_bodyt driver_program_generate_function_body;
 
   /// Logging helper field
   message_handlert &message_handler;

src/jbmc/jbmc_parse_options.cpp

@@ -994,6 +994,20 @@ bool jbmc_parse_optionst::process_goto_functions(
   return false;
 }
 
+bool jbmc_parse_optionst::can_generate_function_body(const irep_idt &name)
+{
+  return false;
+}
+
+bool jbmc_parse_optionst::generate_function_body(
+  symbolt &symbol,
+  symbol_table_baset &symbol_table,
+  goto_functiont &function,
+  bool body_available)
+{
+  return false;
+}
+
 /// display command line help
 void jbmc_parse_optionst::help()
 {

src/jbmc/jbmc_parse_options.h

@@ -98,6 +98,14 @@ class jbmc_parse_optionst:
     const optionst &);
   bool process_goto_functions(goto_modelt &goto_model, const optionst &options);
 
+  bool can_generate_function_body(const irep_idt &name);
+
+  bool generate_function_body(
+    symbolt &symbol,
+    symbol_table_baset &symbol_table,
+    goto_functiont &function,
+    bool body_available);
+
 protected:
   ui_message_handlert ui_message_handler;
   std::unique_ptr<cover_configt> cover_config;

unit/testing-utils/load_java_class.cpp

@@ -97,6 +97,8 @@ symbol_tablet load_java_class(
   lazy_goto_modelt lazy_goto_model(
     [] (goto_model_functiont &function, const abstract_goto_modelt &model) { }, // NOLINT (*)
     [] (goto_modelt &goto_model) { return false; }, // NOLINT (*)
+    [] (const irep_idt &name) { return false; },
+    [] (symbolt &symbol, symbol_table_baset &symbol_table, goto_functiont &function, bool body_available) { return false; }, // NOLINT (*)
     message_handler);
 
   // Configure the path loading