cprover
initialize_goto_model.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Get a Goto Program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "initialize_goto_model.h"
13 
14 #include <fstream>
15 #include <iostream>
16 
17 #include <util/config.h>
18 #include <util/unicode.h>
19 
20 #include <langapi/mode.h>
21 #include <langapi/language_ui.h>
22 #include <langapi/language.h>
23 
25 
26 #include "goto_convert_functions.h"
27 #include "read_goto_binary.h"
28 
30  const cmdlinet &cmdline,
32 {
34  const std::vector<std::string> &files=cmdline.args;
35  if(files.empty())
36  {
37  msg.error() << "Please provide a program" << messaget::eom;
38  throw 0;
39  }
40 
41  std::vector<std::string> binaries, sources;
42  binaries.reserve(files.size());
43  sources.reserve(files.size());
44 
45  for(const auto &file : files)
46  {
47  if(is_goto_binary(file))
48  binaries.push_back(file);
49  else
50  sources.push_back(file);
51  }
52 
53  language_filest language_files;
54  language_files.set_message_handler(message_handler);
55 
56  goto_modelt goto_model;
57 
58  if(!sources.empty())
59  {
60  for(const auto &filename : sources)
61  {
62  #ifdef _MSC_VER
63  std::ifstream infile(widen(filename));
64  #else
65  std::ifstream infile(filename);
66  #endif
67 
68  if(!infile)
69  {
70  msg.error() << "failed to open input file `" << filename
71  << '\'' << messaget::eom;
72  throw 0;
73  }
74 
75  language_filet &lf=language_files.add_file(filename);
77 
78  if(lf.language==nullptr)
79  {
80  source_locationt location;
81  location.set_file(filename);
82  msg.error().source_location=location;
83  msg.error() << "failed to figure out type of file" << messaget::eom;
84  throw 0;
85  }
86 
87  languaget &language=*lf.language;
89  language.get_language_options(cmdline);
90 
91  msg.status() << "Parsing " << filename << messaget::eom;
92 
93  if(language.parse(infile, filename))
94  {
95  msg.error() << "PARSING ERROR" << messaget::eom;
96  throw 0;
97  }
98 
99  lf.get_modules();
100  }
101 
102  msg.status() << "Converting" << messaget::eom;
103 
104  if(language_files.typecheck(goto_model.symbol_table))
105  {
106  msg.error() << "CONVERSION ERROR" << messaget::eom;
107  throw 0;
108  }
109  }
110 
111  for(const auto &file : binaries)
112  {
113  msg.status() << "Reading GOTO program from file" << messaget::eom;
114 
115  if(read_object_and_link(file, goto_model, message_handler))
116  throw 0;
117  }
118 
119  bool binaries_provided_start=
121 
122  bool entry_point_generation_failed=false;
123 
124  if(binaries_provided_start && cmdline.isset("function"))
125  {
126  // Rebuild the entry-point, using the language annotation of the
127  // existing __CPROVER_start function:
128  rebuild_goto_start_functiont rebuild_existing_start(
129  cmdline,
130  goto_model,
131  msg.get_message_handler());
132  entry_point_generation_failed=rebuild_existing_start();
133  }
134  else if(!binaries_provided_start)
135  {
136  // Unsure of the rationale for only generating stubs when there are no
137  // GOTO binaries in play; simply mirroring old code in language_uit here.
138  if(binaries.empty())
139  {
140  // Enable/disable stub generation for opaque methods
141  bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
142  language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
143  }
144 
145  // Allow all language front-ends to try to provide the user-specified
146  // (--function) entry-point, or some language-specific default:
147  entry_point_generation_failed=
148  language_files.generate_support_functions(goto_model.symbol_table);
149  }
150 
151  if(entry_point_generation_failed)
152  {
153  msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
154  throw 0;
155  }
156 
157  if(language_files.final(goto_model.symbol_table))
158  {
159  msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
160  throw 0;
161  }
162 
163  msg.status() << "Generating GOTO Program" << messaget::eom;
164 
165  goto_convert(
166  goto_model.symbol_table,
167  goto_model.goto_functions,
169 
170  // stupid hack
172  goto_model.symbol_table);
173 
174  return goto_model;
175 }
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
bool final(symbol_table_baset &symbol_table)
std::wstring widen(const char *s)
Definition: unicode.cpp:56
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
std::unique_ptr< languaget > get_language_from_filename(const std::string &filename)
Get the language corresponding to the registered file name extensions.
Definition: mode.cpp:101
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
std::unique_ptr< languaget > language
Definition: language_file.h:46
argst args
Definition: cmdline.h:37
virtual bool isset(char option) const
Definition: cmdline.cpp:27
Initialize a Goto Program.
source_locationt source_location
Definition: message.h:214
void set_file(const irep_idt &file)
mstreamt & error() const
Definition: message.h:302
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
void set_should_generate_opaque_method_stubs(bool stubs_enabled)
Turn on or off stub generation for all the languages.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
message_handlert & get_message_handler()
Definition: message.h:153
Goto Programs with Functions.
static irep_idt entry_point()
mstreamt & status() const
Definition: message.h:317
goto_modelt initialize_goto_model(const cmdlinet &cmdline, message_handlert &message_handler)
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
virtual bool parse(std::istream &instream, const std::string &path)=0
bool generate_support_functions(symbol_tablet &symbol_table)
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1177
Definition: kdev_t.h:19