compilet can now use a goto_modelt

Author: Daniel Kroening

src/goto-cc/compile.cpp

@@ -76,7 +76,7 @@ Date: June 2006
 /// \return true on error, false otherwise
 bool compilet::doit()
 {
-  compiled_functions.clear();
+  goto_model.goto_functions.clear();
 
   add_compiler_specific_defines(config);
 
@@ -346,13 +346,12 @@ bool compilet::link()
 {
   // "compile" hitherto uncompiled functions
   statistics() << "Compiling functions" << eom;
-  convert_symbols(compiled_functions);
+  convert_symbols(goto_model.goto_functions);
 
   // parse object files
   for(const auto &file_name : object_files)
   {
-    if(read_object_and_link(file_name, symbol_table,
-                            compiled_functions, get_message_handler()))
+    if(read_object_and_link(file_name, goto_model, get_message_handler()))
       return true;
   }
 
@@ -363,23 +362,23 @@ bool compilet::link()
     // new symbols may have been added to a previously linked file
     // make sure a new entry point is created that contains all
     // static initializers
-    compiled_functions.function_map.erase(INITIALIZE_FUNCTION);
+    goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION);
 
-    symbol_table.remove(goto_functionst::entry_point());
-    compiled_functions.function_map.erase(goto_functionst::entry_point());
+    goto_model.symbol_table.remove(goto_functionst::entry_point());
+    goto_model.goto_functions.function_map.erase(
+      goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, get_message_handler()))
+    if(ansi_c_entry_point(goto_model.symbol_table, get_message_handler()))
       return true;
 
     // entry_point may (should) add some more functions.
-    convert_symbols(compiled_functions);
+    convert_symbols(goto_model.goto_functions);
   }
 
-  if(write_object_file(
-      output_file_executable, symbol_table, compiled_functions))
+  if(write_object_file(output_file_executable, goto_model))
     return true;
 
-  return add_written_cprover_symbols(symbol_table);
+  return add_written_cprover_symbols(goto_model.symbol_table);
 }
 
 /// parses source files and writes object files, or keeps the symbols in the
@@ -419,7 +418,7 @@ bool compilet::compile()
       // output an object file for every source file
 
       // "compile" functions
-      convert_symbols(compiled_functions);
+      convert_symbols(goto_model.goto_functions);
 
       std::string cfn;
 
@@ -436,14 +435,13 @@ bool compilet::compile()
       else
         cfn = output_file_object;
 
-      if(write_object_file(cfn, symbol_table, compiled_functions))
+      if(write_object_file(cfn, goto_model))
         return true;
 
-      if(add_written_cprover_symbols(symbol_table))
+      if(add_written_cprover_symbols(goto_model.symbol_table))
         return true;
 
-      symbol_table.clear(); // clean symbol table for next source file.
-      compiled_functions.clear();
+      goto_model.clear(); // clean symbol table for next source file.
     }
   }
 
@@ -582,10 +580,9 @@ bool compilet::parse_stdin()
 /// \return true on error, false otherwise
 bool compilet::write_object_file(
   const std::string &file_name,
-  const symbol_tablet &lsymbol_table,
-  goto_functionst &functions)
+  const goto_modelt &goto_model)
 {
-  return write_bin_object_file(file_name, lsymbol_table, functions);
+  return write_bin_object_file(file_name, goto_model);
 }
 
 /// writes the goto functions in the function table to a binary format object
@@ -594,15 +591,14 @@ bool compilet::write_object_file(
 /// \return true on error, false otherwise
 bool compilet::write_bin_object_file(
   const std::string &file_name,
-  const symbol_tablet &lsymbol_table,
-  goto_functionst &functions)
+  const goto_modelt &goto_model)
 {
   statistics() << "Writing binary format object `"
                << file_name << "'" << eom;
 
   // symbols
-  statistics() << "Symbols in table: "
-               << lsymbol_table.symbols.size() << eom;
+  statistics() << "Symbols in table: " << goto_model.symbol_table.symbols.size()
+               << eom;
 
   std::ofstream outfile(file_name, std::ios::binary);
 
@@ -612,12 +608,12 @@ bool compilet::write_bin_object_file(
     return true;
   }
 
-  if(write_goto_binary(outfile, lsymbol_table, functions))
+  if(write_goto_binary(outfile, goto_model))
     return true;
 
-  const auto cnt = function_body_count(functions);
+  const auto cnt = function_body_count(goto_model.goto_functions);
 
-  statistics() << "Functions: " << functions.function_map.size()
+  statistics() << "Functions: " << goto_model.goto_functions.function_map.size()
                << "; " << cnt << " have a body." << eom;
 
   outfile.close();
@@ -637,13 +633,13 @@ bool compilet::parse_source(const std::string &file_name)
     return true;
 
   // we just typecheck one file here
-  if(language_files.typecheck(symbol_table))
+  if(language_files.typecheck(goto_model.symbol_table))
   {
     error() << "CONVERSION ERROR" << eom;
     return true;
   }
 
-  if(language_files.final(symbol_table))
+  if(language_files.final(goto_model.symbol_table))
   {
     error() << "CONVERSION ERROR" << eom;
     return true;
@@ -655,7 +651,10 @@ bool compilet::parse_source(const std::string &file_name)
 /// constructor
 /// \return nothing
 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
-  : messaget(mh), ns(symbol_table), cmdline(_cmdline), warning_is_fatal(Werror)
+  : messaget(mh),
+    ns(goto_model.symbol_table),
+    cmdline(_cmdline),
+    warning_is_fatal(Werror)
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
@@ -693,28 +692,29 @@ void compilet::add_compiler_specific_defines(configt &config) const
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
-  goto_convert_functionst converter(symbol_table, get_message_handler());
+  goto_convert_functionst converter(
+    goto_model.symbol_table, get_message_handler());
 
   // the compilation may add symbols!
 
   symbol_tablet::symbolst::size_type before=0;
 
-  while(before!=symbol_table.symbols.size())
+  while(before != goto_model.symbol_table.symbols.size())
   {
-    before=symbol_table.symbols.size();
+    before = goto_model.symbol_table.symbols.size();
 
     typedef std::set<irep_idt> symbols_sett;
     symbols_sett symbols;
 
-    for(const auto &named_symbol : symbol_table.symbols)
+    for(const auto &named_symbol : goto_model.symbol_table.symbols)
       symbols.insert(named_symbol.first);
 
     // the symbol table iterators aren't stable
     for(const auto &symbol : symbols)
     {
       symbol_tablet::symbolst::const_iterator s_it =
-        symbol_table.symbols.find(symbol);
-      CHECK_RETURN(s_it != symbol_table.symbols.end());
+        goto_model.symbol_table.symbols.find(symbol);
+      CHECK_RETURN(s_it != goto_model.symbol_table.symbols.end());
 
       if(s_it->second.type.id()==ID_code &&
          !s_it->second.is_macro &&
@@ -724,7 +724,8 @@ void compilet::convert_symbols(goto_functionst &dest)
       {
         debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first, dest.function_map[s_it->first]);
-        symbol_table.get_writeable_ref(symbol).value = exprt("compiled");
+        goto_model.symbol_table.get_writeable_ref(symbol).value =
+          exprt("compiled");
       }
     }
   }

src/goto-cc/compile.h

@@ -17,7 +17,6 @@ Date: June 2006
 #include <util/cmdline.h>
 #include <util/message.h>
 #include <util/rename_symbol.h>
-#include <util/symbol_table.h>
 
 #include <goto-programs/goto_model.h>
 
@@ -28,8 +27,7 @@ class compilet : public messaget
 public:
   // compilation results
   namespacet ns;
-  symbol_tablet symbol_table;
-  goto_functionst compiled_functions;
+  goto_modelt goto_model;
 
   // configuration
   bool echo_file_name;
@@ -73,15 +71,9 @@ class compilet : public messaget
 
   bool parse_source(const std::string &);
 
-  bool write_object_file(
-    const std::string &,
-    const symbol_tablet &,
-    goto_functionst &);
+  bool write_object_file(const std::string &, const goto_modelt &);
 
-  bool write_bin_object_file(
-    const std::string &,
-    const symbol_tablet &,
-    goto_functionst &);
+  bool write_bin_object_file(const std::string &, const goto_modelt &);
 
   /// \brief Has this compiler written any object files?
   bool wrote_object_files() const { return wrote_object; }

src/goto-cc/linker_script_merge.cpp

@@ -32,12 +32,11 @@ int linker_script_merget::add_linker_script_definitions()
 
   temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
   std::list<irep_idt> linker_defined_symbols;
-  int fail=
-    get_linker_script_data(
-      linker_defined_symbols,
-      compiler.symbol_table,
-      elf_binary,
-      linker_def_outfile());
+  int fail = get_linker_script_data(
+    linker_defined_symbols,
+    compiler.goto_model.symbol_table,
+    elf_binary,
+    linker_def_outfile());
   // ignore linker script parsing failures until the code is tested more widely
   if(fail!=0)
     return 0;
@@ -58,11 +57,10 @@ int linker_script_merget::add_linker_script_definitions()
     return fail;
   }
 
-  symbol_tablet original_st;
-  goto_functionst original_gf;
+  goto_modelt original_goto_model;
 
-  fail=read_goto_binary(goto_binary, original_st, original_gf,
-      get_message_handler());
+  fail =
+    read_goto_binary(goto_binary, original_goto_model, get_message_handler());
 
   if(fail!=0)
   {
@@ -72,19 +70,20 @@ int linker_script_merget::add_linker_script_definitions()
 
   fail=1;
   linker_valuest linker_values;
-  const auto &pair=original_gf.function_map.find(INITIALIZE_FUNCTION);
-  if(pair==original_gf.function_map.end())
+  const auto &pair =
+    original_goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION);
+  if(pair == original_goto_model.goto_functions.function_map.end())
   {
     error() << "No " << INITIALIZE_FUNCTION << " found in goto_functions"
             << eom;
     return fail;
   }
-  fail=ls_data2instructions(
-      data,
-      cmdline.get_value('T'),
-      pair->second.body,
-      original_st,
-      linker_values);
+  fail = ls_data2instructions(
+    data,
+    cmdline.get_value('T'),
+    pair->second.body,
+    original_goto_model.symbol_table,
+    linker_values);
   if(fail!=0)
   {
     error() << "Could not add linkerscript defs to " INITIALIZE_FUNCTION << eom;
@@ -98,16 +97,15 @@ int linker_script_merget::add_linker_script_definitions()
   // The keys of linker_values are exactly the elements of
   // linker_defined_symbols, so iterate over linker_values from now on.
 
-  fail=pointerize_linker_defined_symbols(original_gf, original_st,
-      linker_values);
+  fail = pointerize_linker_defined_symbols(original_goto_model, linker_values);
 
   if(fail!=0)
   {
     error() << "Could not pointerize all linker-defined expressions" << eom;
     return fail;
   }
 
-  fail=compiler.write_object_file(goto_binary, original_st, original_gf);
+  fail = compiler.write_object_file(goto_binary, original_goto_model);
 
   if(fail!=0)
     error() << "Could not write linkerscript-augmented binary" << eom;
@@ -185,17 +183,16 @@ linker_script_merget::linker_script_merget(
 {}
 
 int linker_script_merget::pointerize_linker_defined_symbols(
-      goto_functionst &goto_functions,
-      symbol_tablet &symbol_table,
-      const linker_valuest &linker_values)
+  goto_modelt &goto_model,
+  const linker_valuest &linker_values)
 {
-  const namespacet ns(symbol_table);
+  const namespacet ns(goto_model.symbol_table);
 
   int ret=0;
   // First, pointerize the actual linker-defined symbols
   for(const auto &pair : linker_values)
   {
-    const auto maybe_symbol=symbol_table.get_writeable(pair.first);
+    const auto maybe_symbol = goto_model.symbol_table.get_writeable(pair.first);
     if(!maybe_symbol)
       continue;
     symbolt &entry=*maybe_symbol;
@@ -206,7 +203,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
 
   // Next, find all occurrences of linker-defined symbols that are _values_
   // of some symbol in the symbol table, and pointerize them too
-  for(const auto &pair : symbol_table.symbols)
+  for(const auto &pair : goto_model.symbol_table.symbols)
   {
     std::list<symbol_exprt> to_pointerize;
     symbols_to_pointerize(linker_values, pair.second.value, to_pointerize);
@@ -215,8 +212,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
       continue;
     debug() << "Pointerizing the symbol-table value of symbol " << pair.first
             << eom;
-    int fail=pointerize_subexprs_of(
-      symbol_table.get_writeable_ref(pair.first).value,
+    int fail = pointerize_subexprs_of(
+      goto_model.symbol_table.get_writeable_ref(pair.first).value,
       to_pointerize,
       linker_values,
       ns);
@@ -232,7 +229,7 @@ int linker_script_merget::pointerize_linker_defined_symbols(
 
   // Finally, pointerize all occurrences of linker-defined symbols in the
   // goto program
-  for(auto &gf : goto_functions.function_map)
+  for(auto &gf : goto_model.goto_functions.function_map)
   {
     goto_programt &program=gf.second.body;
     Forall_goto_program_instructions(iit, program)

src/goto-cc/linker_script_merge.h

@@ -156,10 +156,7 @@ class linker_script_merget:public messaget
   /// \post Expressions of the shape `&foo[0]`, `&foo`, and `foo`, where `foo`
   ///       is a linker-script defined symbol with type array, have been
   ///       converted to `foo` whose type is `char*`.
-  int pointerize_linker_defined_symbols(
-      goto_functionst &goto_functions,
-      symbol_tablet &symbol_table,
-      const linker_valuest &linker_values);
+  int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &);
 
   /// \param expr an expr whose subexpressions may need to be pointerized
   /// \param to_pointerize  The symbols that are contained in the subexpressions