Pass object factory parameters through to object factories

Author: danpoe

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,21 +181,24 @@ bool ansi_c_entry_point(
 
   static_lifetime_init(symbol_table, symbol.location);
 
-  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);
 }
 
-
 /// Generate a _start function for a specific function
 /// \param symbol: The symbol for the function that should be
 ///   used as the entry point
 /// \param symbol_table: The symbol table for the program. The new _start
 ///   function symbol will be added to this table
 /// \param message_handler: The message handler
+/// \param object_factory_parameters configuration parameters for the object
+///   factory
 /// \return Returns false if the _start method was generated correctly
 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 +428,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.add(std::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,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language.h>
 
 #include "ansi_c_parse_tree.h"
+#include "c_object_factory_parameters.h"
 
 // clang-format off
 #define OPT_ANSI_C_LANGUAGE \
@@ -33,6 +34,11 @@ Author: Daniel Kroening, [email protected]
 class ansi_c_languaget:public languaget
 {
 public:
+  void set_language_options(const optionst &options) override
+  {
+    object_factory_params.set(options);
+  }
+
   bool preprocess(
     std::istream &instream,
     const std::string &path,
@@ -87,6 +93,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,18 +29,21 @@ class symbol_factoryt
   const source_locationt &loc;
   const bool assume_non_null;
   namespacet ns;
+  const c_object_factory_parameterst &object_factory_params;
 
 public:
   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(
@@ -179,14 +182,17 @@ void symbol_factoryt::gen_nondet_init(
 /// \param type: The type for the symbol created
 /// \param loc: The location to assign to generated code
 /// \param allow_null: Whether to allow a null value when type is a pointer
+/// \param object_factory_parameters configuration parameters for the object
+///   factory
 /// \return Returns the symbol_exprt for the symbol created
 symbol_exprt c_nondet_symbol_factory(
   code_blockt &init_code,
   symbol_tablet &symbol_table,
   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);
@@ -209,10 +215,7 @@ symbol_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

@@ -12,6 +12,8 @@ Author: Diffblue Ltd.
 #ifndef CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
 #define CPROVER_ANSI_C_C_NONDET_SYMBOL_FACTORY_H
 
+#include "c_object_factory_parameters.h"
+
 #include <util/std_code.h>
 #include <util/symbol_table.h>
 
@@ -21,6 +23,7 @@ symbol_exprt c_nondet_symbol_factory(
   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) override
+  {
+    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/langapi/language_file.cpp

@@ -10,6 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <fstream>
 
+#include <util/object_factory_parameters.h>
+
 #include "language.h"
 
 language_filet::language_filet(const language_filet &rhs):