Pass object factory parameters through to object factories

Author: danpoe

jbmc/src/java_bytecode/java_object_factory_parameters.h

@@ -18,7 +18,7 @@ struct java_object_factory_parameterst final : public object_factory_parameterst
   }
 
   java_object_factory_parameterst(const optionst &options)
-    : object_factory_paramterst(options)
+    : object_factory_parameterst(options)
   {
   }
 };

src/ansi-c/ansi_c_entry_point.cpp

@@ -22,7 +22,8 @@ Author: Daniel Kroening, [email protected]
 exprt::operandst build_function_environment(
   const code_typet::parameterst &parameters,
   code_blockt &init_code,
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   exprt::operandst main_arguments;
   main_arguments.resize(parameters.size());
@@ -35,14 +36,14 @@ exprt::operandst build_function_environment(
     const irep_idt base_name=p.get_base_name().empty()?
       ("argument#"+std::to_string(param_number)):p.get_base_name();
 
-    main_arguments[param_number]=
-      c_nondet_symbol_factory(
-        init_code,
-        symbol_table,
-        base_name,
-        p.type(),
-        p.source_location(),
-        true);
+    main_arguments[param_number] = c_nondet_symbol_factory(
+      init_code,
+      symbol_table,
+      base_name,
+      p.type(),
+      p.source_location(),
+      true,
+      object_factory_parameters);
   }
 
   return main_arguments;
@@ -111,7 +112,8 @@ void record_function_outputs(
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   // check if entry point is already there
   if(symbol_table.symbols.find(goto_functionst::entry_point())!=
@@ -179,7 +181,8 @@ bool ansi_c_entry_point(
 
   static_lifetime_init(symbol_table, symbol.location, message_handler);
 
-  return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
+  return generate_ansi_c_start_function(
+    symbol, symbol_table, message_handler, object_factory_parameters);
 }
 
 
@@ -193,7 +196,8 @@ bool ansi_c_entry_point(
 bool generate_ansi_c_start_function(
   const symbolt &symbol,
   symbol_tablet &symbol_table,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   PRECONDITION(!symbol.value.is_nil());
   code_blockt init_code;
@@ -423,11 +427,8 @@ bool generate_ansi_c_start_function(
   else
   {
     // produce nondet arguments
-    call_main.arguments()=
-      build_function_environment(
-        parameters,
-        init_code,
-        symbol_table);
+    call_main.arguments() = build_function_environment(
+      parameters, init_code, symbol_table, object_factory_parameters);
   }
 
   init_code.move(call_main);

src/ansi-c/ansi_c_entry_point.h

@@ -10,16 +10,19 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
 #define CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H
 
-#include <util/symbol_table.h>
+#include <ansi-c/c_object_factory_parameters.h>
 #include <util/message.h>
+#include <util/symbol_table.h>
 
 bool ansi_c_entry_point(
   symbol_tablet &symbol_table,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters);
 
 bool generate_ansi_c_start_function(
   const symbolt &symbol,
   symbol_tablet &symbol_table,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  const c_object_factory_parameterst &object_factory_parameters);
 
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H

src/ansi-c/ansi_c_language.cpp

@@ -137,8 +137,10 @@ bool ansi_c_languaget::generate_support_functions(
   // function body parsing, or else generate-stubs moved to the
   // final phase.
   generate_opaque_method_stubs(symbol_table);
+
   // This creates __CPROVER_start and __CPROVER_initialize:
-  return ansi_c_entry_point(symbol_table, get_message_handler());
+  return ansi_c_entry_point(
+    symbol_table, get_message_handler(), object_factory_params);
 }
 
 void ansi_c_languaget::show_parse(std::ostream &out)

src/ansi-c/ansi_c_language.h

@@ -17,10 +17,16 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #include "ansi_c_parse_tree.h"
+#include "c_object_factory_parameters.h"
 
 class ansi_c_languaget:public languaget
 {
 public:
+  void set_language_options(const optionst &options)
+  {
+    object_factory_params.set(options);
+  }
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -75,6 +81,8 @@ class ansi_c_languaget:public languaget
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
+
+  c_object_factory_parameterst object_factory_params;
 };
 
 std::unique_ptr<languaget> new_ansi_c_language();

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -29,6 +29,7 @@ class symbol_factoryt
   const source_locationt &loc;
   const bool assume_non_null;
   namespacet ns;
+  const c_object_factory_parameterst &object_factory_params;
 
   const symbolt &c_new_tmp_symbol(
     //symbol_tablet &symbol_table,
@@ -42,12 +43,14 @@ class symbol_factoryt
     std::vector<const symbolt *> &_symbols_created,
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
-    const bool _assume_non_null):
-      symbols_created(_symbols_created),
+    const bool _assume_non_null,
+    const c_object_factory_parameterst &object_factory_params)
+    : symbols_created(_symbols_created),
       symbol_table(_symbol_table),
       loc(loc),
       assume_non_null(_assume_non_null),
-      ns(_symbol_table)
+      ns(_symbol_table),
+      object_factory_params(object_factory_params)
   {}
 
   exprt allocate_object(
@@ -210,7 +213,8 @@ exprt c_nondet_symbol_factory(
   const irep_idt base_name,
   const typet &type,
   const source_locationt &loc,
-  bool allow_null)
+  bool allow_null,
+  const c_object_factory_parameterst &object_factory_parameters)
 {
   irep_idt identifier=id2string(goto_functionst::entry_point())+
     "::"+id2string(base_name);
@@ -233,10 +237,7 @@ exprt c_nondet_symbol_factory(
   symbols_created.push_back(main_symbol_ptr);
 
   symbol_factoryt state(
-    symbols_created,
-    symbol_table,
-    loc,
-    !allow_null);
+    symbols_created, symbol_table, loc, !allow_null, object_factory_parameters);
   code_blockt assignments;
   state.gen_nondet_init(assignments, main_symbol_expr);
 

src/ansi-c/c_nondet_symbol_factory.h

@@ -15,12 +15,15 @@ Author: Diffblue Ltd.
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
+class c_object_factory_parameterst;
+
 exprt c_nondet_symbol_factory(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   const irep_idt base_name,
   const typet &type,
   const source_locationt &,
-  bool allow_null);
+  bool allow_null,
+  const c_object_factory_parameterst &object_factory_parameters);
 
 #endif // CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H

src/cpp/cpp_language.cpp

@@ -137,7 +137,8 @@ bool cpp_languaget::typecheck(
 bool cpp_languaget::generate_support_functions(
   symbol_tablet &symbol_table)
 {
-  return ansi_c_entry_point(symbol_table, get_message_handler());
+  return ansi_c_entry_point(
+    symbol_table, get_message_handler(), object_factory_params);
 }
 
 void cpp_languaget::show_parse(std::ostream &out)

src/cpp/cpp_language.h

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <memory>
 
+#include <ansi-c/c_object_factory_parameters.h>
+
 #include <util/make_unique.h> // unique_ptr
 
 #include <langapi/language.h>
@@ -23,6 +25,11 @@ Author: Daniel Kroening, [email protected]
 class cpp_languaget:public languaget
 {
 public:
+  void set_language_options(const optionst &options)
+  {
+    object_factory_params.set(options);
+  }
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -88,6 +95,8 @@ class cpp_languaget:public languaget
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;
 
+  c_object_factory_parameterst object_factory_params;
+
   void show_parse(std::ostream &out, const cpp_itemt &item);
 
   std::string main_symbol()

src/goto-cc/compile.cpp

@@ -368,7 +368,12 @@ bool compilet::link()
     goto_model.goto_functions.function_map.erase(
       goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(goto_model.symbol_table, get_message_handler()))
+    const bool error = ansi_c_entry_point(
+      goto_model.symbol_table,
+      get_message_handler(),
+      c_object_factory_parameterst());
+
+    if(error)
       return true;
 
     // entry_point may (should) add some more functions.

src/goto-programs/initialize_goto_model.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/cmdline.h>
 #include <util/config.h>
 #include <util/message.h>
+#include <util/object_factory_parameters.h>
 #include <util/unicode.h>
 
 #include <langapi/mode.h>

src/goto-programs/initialize_goto_model.h

@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
 
 class cmdlinet;
 class message_handlert;
+class object_factory_parameterst;
 class optionst;
 
 goto_modelt initialize_goto_model(

src/goto-programs/rebuild_goto_start_function.cpp

@@ -8,10 +8,13 @@
 
 #include "rebuild_goto_start_function.h"
 
+#include <ansi-c/c_object_factory_parameters.h>
+
+#include <util/cmdline.h>
+#include <util/object_factory_parameters.h>
+#include <util/prefix.h>
 #include <util/symbol.h>
 #include <util/symbol_table.h>
-#include <util/prefix.h>
-#include <util/cmdline.h>
 
 #include <langapi/mode.h>
 #include <langapi/language.h>

src/langapi/language.h

@@ -17,9 +17,10 @@ Author: Daniel Kroening, [email protected]
 #include <string>
 #include <memory> // unique_ptr
 
-#include <util/symbol.h>
-#include <util/std_types.h>
 #include <util/message.h>
+#include <util/object_factory_parameters.h>
+#include <util/std_types.h>
+#include <util/symbol.h>
 
 #include <goto-programs/system_library_symbols.h>
 
@@ -63,8 +64,7 @@ class languaget:public messaget
   /// complete. Functions introduced here are visible to lazy loading and
   /// can influence its decisions (e.g. picking the types of input parameters
   /// and globals), whereas anything introduced during `final` cannot.
-  virtual bool generate_support_functions(
-    symbol_tablet &symbol_table)=0;
+  virtual bool generate_support_functions(symbol_tablet &symbol_table) = 0;
 
   // add external dependencies of a given module to set
 

src/langapi/language_file.cpp

@@ -10,6 +10,10 @@ Author: Daniel Kroening, [email protected]
 
 #include <fstream>
 
+#include <ansi-c/c_object_factory_parameters.h>
+
+#include <util/object_factory_parameters.h>
+
 #include "language.h"
 
 language_filet::language_filet(const language_filet &rhs):
@@ -169,14 +173,19 @@ bool language_filest::generate_support_functions(
 
   for(auto &file : file_map)
   {
-    if(languages.insert(file.second.language->id()).second)
-      if(file.second.language->generate_support_functions(symbol_table))
+    auto &language = *file.second.language;
+
+    if(languages.insert(language.id()).second)
+    {
+      bool error = language.generate_support_functions(symbol_table);
+
+      if(error)
         return true;
+    }
   }
 
   return false;
 }
-
 bool language_filest::final(symbol_table_baset &symbol_table)
 {
   std::set<std::string> languages;