Merge pull request #5195 from peterschrammel/move-lazy-goto-model

Move lazy goto model to JBMC [TG-9888] [blocks: 4753]

Author: peterschrammel

jbmc/src/java_bytecode/Makefile

@@ -43,8 +43,9 @@ SRC = assignments_from_json.cpp \
       java_trace_validation.cpp \
       java_types.cpp \
       java_utils.cpp \
-      lift_clinit_calls.cpp \
       lambda_synthesis.cpp \
+      lazy_goto_model.cpp \
+      lift_clinit_calls.cpp \
       load_method_by_regex.cpp \
       mz_zip_archive.cpp \
       remove_exceptions.cpp \

src/goto-programs/lazy_goto_functions_map.h renamed to jbmc/src/java_bytecode/lazy_goto_functions_map.h

@@ -8,8 +8,8 @@
 
 #include <unordered_set>
 
-#include "goto_functions.h"
-#include "goto_convert_functions.h"
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_functions.h>
 
 #include <langapi/language_file.h>
 #include <util/journalling_symbol_table.h>
@@ -49,20 +49,17 @@ class lazy_goto_functions_mapt final
   // NOLINTNEXTLINE(readability/identifiers)  - name matches those used in STL
   typedef std::size_t size_type;
 
-  typedef
-    std::function<void(
-      const irep_idt &name,
-      goto_functionst::goto_functiont &function,
-      journalling_symbol_tablet &function_symbols)>
+  typedef std::function<void(
+    const irep_idt &name,
+    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)>
+  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:
@@ -90,15 +87,15 @@ class lazy_goto_functions_mapt final
     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(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)
+    : goto_functions(goto_functions),
+      language_files(language_files),
+      symbol_table(symbol_table),
+      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)
   {
   }
 
@@ -125,12 +122,14 @@ 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) ||
-      driver_program_can_generate_function_body(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); }
+  void unload(const key_type &name) const
+  {
+    goto_functions.erase(name);
+  }
 
   void ensure_function_loaded(const key_type &name) const
   {
@@ -148,9 +147,9 @@ class lazy_goto_functions_mapt final
 
     journalling_symbol_tablet journalling_table =
       journalling_symbol_tablet::wrap(symbol_table_builder);
-    reference named_function=ensure_entry_converted(name, journalling_table);
-    mapped_type function=named_function.second;
-    if(processed_functions.count(name)==0)
+    reference named_function = ensure_entry_converted(name, journalling_table);
+    mapped_type function = named_function.second;
+    if(processed_functions.count(name) == 0)
     {
       // Run function-pass conversions
       post_process_function(name, function, journalling_table);
@@ -176,19 +175,18 @@ class lazy_goto_functions_mapt final
     // Fill in symbol table entry body if not already done
     language_files.convert_lazy_method(name, function_symbol_table);
 
-    underlying_mapt::iterator it=goto_functions.find(name);
-    if(it!=goto_functions.end())
+    underlying_mapt::iterator it = goto_functions.find(name);
+    if(it != goto_functions.end())
       return *it;
 
     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));
+    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)
@@ -204,4 +202,4 @@ class lazy_goto_functions_mapt final
   }
 };
 
-#endif  // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H
+#endif // CPROVER_GOTO_PROGRAMS_LAZY_GOTO_FUNCTIONS_MAP_H

src/goto-programs/lazy_goto_model.cpp renamed to jbmc/src/java_bytecode/lazy_goto_model.cpp

@@ -4,8 +4,9 @@
 /// Model for lazy loading of functions
 
 #include "lazy_goto_model.h"
-#include "read_goto_binary.h"
-#include "rebuild_goto_start_function.h"
+
+#include <goto-programs/read_goto_binary.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <langapi/mode.h>
 
@@ -32,11 +33,10 @@ lazy_goto_modelt::lazy_goto_modelt(
       goto_model->goto_functions.function_map,
       language_files,
       symbol_table,
-      [this] (
+      [this](
         const irep_idt &function_name,
         goto_functionst::goto_functiont &function,
-        journalling_symbol_tablet &journalling_symbol_table) -> void
-      {
+        journalling_symbol_tablet &journalling_symbol_table) -> void {
         goto_model_functiont model_function(
           journalling_symbol_table,
           goto_model->goto_functions,
@@ -65,11 +65,10 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
       goto_model->goto_functions.function_map,
       language_files,
       symbol_table,
-      [this] (
+      [this](
         const irep_idt &function_name,
         goto_functionst::goto_functiont &function,
-        journalling_symbol_tablet &journalling_symbol_table) -> void
-      {
+        journalling_symbol_tablet &journalling_symbol_table) -> void {
         goto_model_functiont model_function(
           journalling_symbol_table,
           goto_model->goto_functions,
@@ -150,16 +149,16 @@ void lazy_goto_modelt::initialize(
           "failed to open input file '" + filename + '\'');
       }
 
-      language_filet &lf=add_language_file(filename);
-      lf.language=get_language_from_filename(filename);
+      language_filet &lf = add_language_file(filename);
+      lf.language = get_language_from_filename(filename);
 
-      if(lf.language==nullptr)
+      if(lf.language == nullptr)
       {
         throw invalid_source_file_exceptiont(
           "failed to figure out type of file '" + filename + '\'');
       }
 
-      languaget &language=*lf.language;
+      languaget &language = *lf.language;
       language.set_message_handler(message_handler);
       language.set_language_options(options);
 
@@ -197,21 +196,35 @@ void lazy_goto_modelt::initialize(
   bool binaries_provided_start =
     symbol_table.has_symbol(goto_functionst::entry_point());
 
-  bool entry_point_generation_failed=false;
+  bool entry_point_generation_failed = false;
 
   if(binaries_provided_start && options.is_set("function"))
   {
-    // Rebuild the entry-point, using the language annotation of the
-    // existing __CPROVER_start function:
-    rebuild_lazy_goto_start_functiont rebuild_existing_start(
-      options, *this, message_handler);
-    entry_point_generation_failed=rebuild_existing_start();
+    // The goto binaries provided already contain a __CPROVER_start
+    // function that may be tied to a different entry point `function`.
+    // Hence, we will rebuild the __CPROVER_start function.
+
+    // Get the language annotation of the existing __CPROVER_start function.
+    std::unique_ptr<languaget> language =
+      get_entry_point_language(symbol_table, options, message_handler);
+
+    // To create a new entry point we must first remove the old one
+    remove_existing_entry_point(symbol_table);
+
+    // Create the new entry-point
+    entry_point_generation_failed =
+      language->generate_support_functions(symbol_table);
+
+    // Remove the function from the goto functions so it is copied back in
+    // from the symbol table during goto_convert
+    if(!entry_point_generation_failed)
+      unload(goto_functionst::entry_point());
   }
   else if(!binaries_provided_start)
   {
     // Allow all language front-ends to try to provide the user-specified
     // (--function) entry-point, or some language-specific default:
-    entry_point_generation_failed=
+    entry_point_generation_failed =
       language_files.generate_support_functions(symbol_table);
   }
 
@@ -228,10 +241,11 @@ void lazy_goto_modelt::initialize(
 void lazy_goto_modelt::load_all_functions() const
 {
   symbol_tablet::symbolst::size_type table_size;
-  symbol_tablet::symbolst::size_type new_table_size=symbol_table.symbols.size();
+  symbol_tablet::symbolst::size_type new_table_size =
+    symbol_table.symbols.size();
   do
   {
-    table_size=new_table_size;
+    table_size = new_table_size;
 
     // Find symbols that correspond to functions
     std::vector<irep_idt> fn_ids_to_convert;
@@ -247,8 +261,8 @@ void lazy_goto_modelt::load_all_functions() const
     // Repeat while new symbols are being added in case any of those are
     // stubbed functions. Even stubs can create new stubs while being
     // converted if they are special stubs (e.g. string functions)
-    new_table_size=symbol_table.symbols.size();
-  } while(new_table_size!=table_size);
+    new_table_size = symbol_table.symbols.size();
+  } while(new_table_size != table_size);
 
   goto_model->goto_functions.compute_location_numbers();
 }

src/goto-programs/lazy_goto_model.h renamed to jbmc/src/java_bytecode/lazy_goto_model.h

@@ -8,10 +8,11 @@
 
 #include <langapi/language_file.h>
 
-#include "abstract_goto_model.h"
-#include "goto_model.h"
+#include <goto-programs/abstract_goto_model.h>
+#include <goto-programs/goto_convert_functions.h>
+#include <goto-programs/goto_model.h>
+
 #include "lazy_goto_functions_map.h"
-#include "goto_convert_functions.h"
 
 class optionst;
 
@@ -148,7 +149,7 @@ class lazy_goto_modelt : public abstract_goto_modelt
   /// \param message_handler: The message_handler to use for logging
   /// \tparam THandler: a type that defines methods process_goto_function and
   /// process_goto_functions
-  template<typename THandler>
+  template <typename THandler>
   static lazy_goto_modelt from_handler_object(
     THandler &handler,
     const optionst &options,
@@ -165,15 +166,13 @@ class lazy_goto_modelt : public abstract_goto_modelt
       [&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);
+      [&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);
   }
@@ -184,7 +183,10 @@ class lazy_goto_modelt : public abstract_goto_modelt
   /// Eagerly loads all functions from the symbol table.
   void load_all_functions() const;
 
-  void unload(const irep_idt &name) const { goto_functions.unload(name); }
+  void unload(const irep_idt &name) const
+  {
+    goto_functions.unload(name);
+  }
 
   language_filet &add_language_file(const std::string &filename)
   {
@@ -197,8 +199,8 @@ class lazy_goto_modelt : public abstract_goto_modelt
   /// Before freezing the functions all module-level passes are run
   /// \param model: The lazy_goto_modelt to freeze
   /// \return The frozen goto_modelt or an empty optional if freezing fails
-  static std::unique_ptr<goto_modelt> process_whole_model_and_freeze(
-    lazy_goto_modelt &&model)
+  static std::unique_ptr<goto_modelt>
+  process_whole_model_and_freeze(lazy_goto_modelt &&model)
   {
     if(model.finalize())
       return nullptr;
@@ -237,8 +239,8 @@ class lazy_goto_modelt : public abstract_goto_modelt
   ///    `languaget::convert_lazy_method` function. If that results in a `codet`
   ///    representation of the function stored in the symbol table, convert it
   ///    to GOTO and return it as in step (3).
-  const goto_functionst::goto_functiont &get_goto_function(const irep_idt &id)
-    override
+  const goto_functionst::goto_functiont &
+  get_goto_function(const irep_idt &id) override
   {
     return goto_functions.at(id);
   }

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -35,23 +35,22 @@ Author: Daniel Kroening, [email protected]
 #include <goto-checker/stop_on_fail_verifier_with_fault_localization.h>
 
 #include <goto-programs/adjust_float_expressions.h>
-#include <goto-programs/lazy_goto_model.h>
-#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
+#include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/loop_ids.h>
-#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/remove_returns.h>
-#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/remove_virtual_functions.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
-#include <goto-programs/show_symbol_table.h>
 #include <goto-programs/show_properties.h>
+#include <goto-programs/show_symbol_table.h>
 
 #include <goto-instrument/full_slicer.h>
-#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>
+#include <goto-instrument/reachability_slicer.h>
 
 #include <goto-symex/path_storage.h>
 
@@ -68,6 +67,7 @@ Author: Daniel Kroening, [email protected]
 #include <java_bytecode/java_multi_path_symex_only_checker.h>
 #include <java_bytecode/java_single_path_symex_checker.h>
 #include <java_bytecode/java_single_path_symex_only_checker.h>
+#include <java_bytecode/lazy_goto_model.h>
 #include <java_bytecode/remove_exceptions.h>
 #include <java_bytecode/remove_instanceof.h>
 #include <java_bytecode/remove_java_new.h>

jbmc/src/jbmc/jbmc_parse_options.h

@@ -25,8 +25,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/class_hierarchy.h>
 #include <goto-programs/goto_trace.h>
-#include <goto-programs/lazy_goto_model.h>
 #include <goto-programs/show_properties.h>
+#include <java_bytecode/lazy_goto_model.h>
 
 #include <goto-symex/path_storage.h>