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 
16 #include <util/config.h>
17 #include <util/message.h>
18 #include <util/options.h>
19 
20 #ifdef _MSC_VER
21 # include <util/unicode.h>
22 #endif
23 
24 #include <langapi/language.h>
25 #include <langapi/language_file.h>
26 #include <langapi/mode.h>
27 
29 #include <util/exception_utils.h>
30 
31 #include "goto_convert_functions.h"
32 #include "read_goto_binary.h"
33 
37  const irep_idt &entry_function_name,
38  const optionst &options,
39  goto_modelt &goto_model,
40  message_handlert &message_handler)
41 {
42  auto const entry_function_sym =
43  goto_model.symbol_table.lookup(entry_function_name);
44  if(entry_function_sym == nullptr)
45  {
47  // NOLINTNEXTLINE(whitespace/braces)
48  std::string{"couldn't find function with name '"} +
49  id2string(entry_function_name) + "' in symbol table",
50  "--function"};
51  }
52  PRECONDITION(!entry_function_sym->mode.empty());
53  auto const entry_language = get_language_from_mode(entry_function_sym->mode);
54  CHECK_RETURN(entry_language != nullptr);
55  entry_language->set_message_handler(message_handler);
56  entry_language->set_language_options(options);
57  return entry_language->generate_support_functions(goto_model.symbol_table);
58 }
59 
61  const std::vector<std::string> &files,
62  message_handlert &message_handler,
63  const optionst &options)
64 {
65  messaget msg(message_handler);
66  if(files.empty())
67  {
69  "missing program argument",
70  "filename",
71  "one or more paths to program files");
72  }
73 
74  std::vector<std::string> binaries, sources;
75  binaries.reserve(files.size());
76  sources.reserve(files.size());
77 
78  for(const auto &file : files)
79  {
80  if(is_goto_binary(file, message_handler))
81  binaries.push_back(file);
82  else
83  sources.push_back(file);
84  }
85 
86  language_filest language_files;
87  language_files.set_message_handler(message_handler);
88 
89  goto_modelt goto_model;
90 
91  if(!sources.empty())
92  {
93  for(const auto &filename : sources)
94  {
95  #ifdef _MSC_VER
96  std::ifstream infile(widen(filename));
97  #else
98  std::ifstream infile(filename);
99  #endif
100 
101  if(!infile)
102  {
103  throw system_exceptiont(
104  "Failed to open input file '" + filename + '\'');
105  }
106 
107  language_filet &lf=language_files.add_file(filename);
109 
110  if(lf.language==nullptr)
111  {
113  "Failed to figure out type of file '" + filename + '\'');
114  }
115 
116  languaget &language=*lf.language;
117  language.set_message_handler(message_handler);
118  language.set_language_options(options);
119 
120  msg.status() << "Parsing " << filename << messaget::eom;
121 
122  if(language.parse(infile, filename))
123  {
124  throw invalid_source_file_exceptiont("PARSING ERROR");
125  }
126 
127  lf.get_modules();
128  }
129 
130  msg.status() << "Converting" << messaget::eom;
131 
132  if(language_files.typecheck(goto_model.symbol_table))
133  {
134  throw invalid_source_file_exceptiont("CONVERSION ERROR");
135  }
136  }
137 
138  for(const auto &file : binaries)
139  {
140  msg.status() << "Reading GOTO program from file" << messaget::eom;
141 
142  if(read_object_and_link(file, goto_model, message_handler))
143  {
145  "failed to read object or link in file '" + file + '\'');
146  }
147  }
148 
149  bool binaries_provided_start=
151 
152  bool entry_point_generation_failed=false;
153 
154  if(binaries_provided_start && options.is_set("function"))
155  {
156  // Get the language annotation of the existing __CPROVER_start function.
157  std::unique_ptr<languaget> language = get_entry_point_language(
158  goto_model.symbol_table, options, message_handler);
159 
160  // To create a new entry point we must first remove the old one
162 
163  // Create the new entry-point
164  entry_point_generation_failed =
165  language->generate_support_functions(goto_model.symbol_table);
166 
167  // Remove the function from the goto functions so it is copied back in
168  // from the symbol table during goto_convert
169  if(!entry_point_generation_failed)
170  goto_model.unload(goto_functionst::entry_point());
171  }
172  else if(!binaries_provided_start)
173  {
174  if(options.is_set("function"))
175  {
176  // no entry point is present; Use the mode of the specified entry function
177  // to generate one
178  entry_point_generation_failed = generate_entry_point_for_function(
179  options.get_option("function"), options, goto_model, message_handler);
180  }
181  if(entry_point_generation_failed || !options.is_set("function"))
182  {
183  // Allow all language front-ends to try to provide the user-specified
184  // (--function) entry-point, or some language-specific default:
185  entry_point_generation_failed =
186  language_files.generate_support_functions(goto_model.symbol_table);
187  }
188  }
189 
190  if(entry_point_generation_failed)
191  {
192  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
193  }
194 
195  if(language_files.final(goto_model.symbol_table))
196  {
197  throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
198  }
199 
200  msg.status() << "Generating GOTO Program" << messaget::eom;
201 
202  goto_convert(
203  goto_model.symbol_table,
204  goto_model.goto_functions,
205  message_handler);
206 
207  if(options.is_set("validate-goto-model"))
208  {
209  goto_model_validation_optionst goto_model_validation_options{
210  goto_model_validation_optionst ::set_optionst::all_false};
211 
212  goto_model.validate(
213  validation_modet::INVARIANT, goto_model_validation_options);
214  }
215 
216  // stupid hack
218  goto_model.symbol_table);
219 
220  return goto_model;
221 }
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1291
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void unload(const irep_idt &name)
Definition: goto_model.h:68
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition: goto_model.h:98
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Thrown when we can't handle something in an input source file.
language_filet & add_file(const std::string &filename)
Definition: language_file.h:77
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
bool generate_support_functions(symbol_tablet &symbol_table)
bool final(symbol_table_baset &symbol_table)
std::unique_ptr< languaget > language
Definition: language_file.h:47
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
virtual bool parse(std::istream &instream, const std::string &path)=0
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & status() const
Definition: message.h:414
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
static eomt eom
Definition: message.h:297
bool is_set(const std::string &option) const
N.B. opts.is_set("foo") does not imply opts.get_bool_option("foo")
Definition: options.cpp:62
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Thrown when some external system fails unexpectedly.
configt config
Definition: config.cpp:25
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
static bool generate_entry_point_for_function(const irep_idt &entry_function_name, const optionst &options, goto_modelt &goto_model, message_handlert &message_handler)
Generate an entry point that calls a function with the given name, based on the functions language mo...
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
Abstract interface to support a programming language.
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:102
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
Options.
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file, and also updates config
Read Goto Programs.
void remove_existing_entry_point(symbol_table_baset &symbol_table)
Eliminate the existing entry point function symbol and any symbols created in that scope from the sym...
std::unique_ptr< languaget > get_entry_point_language(const symbol_table_baset &symbol_table, const optionst &options, message_handlert &message_handler)
Find the language corresponding to the __CPROVER_start function.
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Definition: kdev_t.h:19
std::wstring widen(const char *s)
Definition: unicode.cpp:48