Lazy methods: allow driver program to provide stubs

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(
+      const irep_idt &function_name,
+      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)),
+    post_process_function(post_process_function),
+    driver_program_can_generate_function_body(
+      driver_program_can_generate_function_body),
+    driver_program_generate_function_body(
+      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,30 @@ 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);
+
+    goto_functiont function;
+
+    // First chance: see if the driver program wants to provide a replacement:
+    bool body_provided =
+      driver_program_generate_function_body(
+        name,
+        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_table.lookup_ref(name).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);
       },
+      driver_program_can_generate_function_body,
+      driver_program_generate_function_body,
       message_handler),
-    post_process_function(std::move(post_process_function)),
-    post_process_functions(std::move(post_process_functions)),
+    post_process_function(post_process_function),
+    post_process_functions(post_process_functions),
+    driver_program_can_generate_function_body(
+      driver_program_can_generate_function_body),
+    driver_program_generate_function_body(
+      driver_program_generate_function_body),
     message_handler(message_handler)
 {
   language_files.set_message_handler(message_handler);
@@ -68,10 +76,12 @@ 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)),
-    post_process_functions(std::move(other.post_process_functions)),
+    post_process_function(other.post_process_function),
+    post_process_functions(other.post_process_functions),
     message_handler(other.message_handler)
 {
 }

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]
+      (const irep_idt &function_name,
+       symbol_table_baset &symbol_table,
+       goto_functiont &function,
+       bool is_first_chance)
+      {
+        return
+          handler.generate_function_body(
+            function_name, 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/java_bytecode/Makefile

@@ -37,6 +37,7 @@ SRC = bytecode_info.cpp \
       remove_java_new.cpp \
       replace_java_nondet.cpp \
       select_pointer_type.cpp \
+      simple_method_stubbing.cpp \
       # Empty last line
 
 INCLUDES= -I ..