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::list<std::string> binaries, sources;
75 
76  for(const auto &file : files)
77  {
78  if(is_goto_binary(file, message_handler))
79  binaries.push_back(file);
80  else
81  sources.push_back(file);
82  }
83 
84  language_filest language_files;
85  language_files.set_message_handler(message_handler);
86 
87  goto_modelt goto_model;
88 
89  if(!sources.empty())
90  {
91  for(const auto &filename : sources)
92  {
93  #ifdef _MSC_VER
94  std::ifstream infile(widen(filename));
95  #else
96  std::ifstream infile(filename);
97  #endif
98 
99  if(!infile)
100  {
101  throw system_exceptiont(
102  "Failed to open input file '" + filename + '\'');
103  }
104 
105  language_filet &lf=language_files.add_file(filename);
107 
108  if(lf.language==nullptr)
109  {
111  "Failed to figure out type of file '" + filename + '\'');
112  }
113 
114  languaget &language=*lf.language;
115  language.set_message_handler(message_handler);
116  language.set_language_options(options);
117 
118  msg.status() << "Parsing " << filename << messaget::eom;
119 
120  if(language.parse(infile, filename))
121  {
122  throw invalid_source_file_exceptiont("PARSING ERROR");
123  }
124 
125  lf.get_modules();
126  }
127 
128  msg.status() << "Converting" << messaget::eom;
129 
130  if(language_files.typecheck(goto_model.symbol_table))
131  {
132  throw invalid_source_file_exceptiont("CONVERSION ERROR");
133  }
134  }
135 
136  if(read_objects_and_link(binaries, goto_model, message_handler))
137  {
139  "failed to read object or link in files"};
140  }
141 
142  bool binaries_provided_start=
144 
145  bool entry_point_generation_failed=false;
146 
147  if(binaries_provided_start && options.is_set("function"))
148  {
149  // Get the language annotation of the existing __CPROVER_start function.
150  std::unique_ptr<languaget> language = get_entry_point_language(
151  goto_model.symbol_table, options, message_handler);
152 
153  // To create a new entry point we must first remove the old one
155 
156  // Create the new entry-point
157  entry_point_generation_failed =
158  language->generate_support_functions(goto_model.symbol_table);
159 
160  // Remove the function from the goto functions so it is copied back in
161  // from the symbol table during goto_convert
162  if(!entry_point_generation_failed)
163  goto_model.unload(goto_functionst::entry_point());
164  }
165  else if(!binaries_provided_start)
166  {
167  if(options.is_set("function"))
168  {
169  // no entry point is present; Use the mode of the specified entry function
170  // to generate one
171  entry_point_generation_failed = generate_entry_point_for_function(
172  options.get_option("function"), options, goto_model, message_handler);
173  }
174  if(entry_point_generation_failed || !options.is_set("function"))
175  {
176  // Allow all language front-ends to try to provide the user-specified
177  // (--function) entry-point, or some language-specific default:
178  entry_point_generation_failed =
179  language_files.generate_support_functions(goto_model.symbol_table);
180  }
181  }
182 
183  if(entry_point_generation_failed)
184  {
185  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
186  }
187 
188  if(language_files.final(goto_model.symbol_table))
189  {
190  throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
191  }
192 
193  msg.status() << "Generating GOTO Program" << messaget::eom;
194 
195  goto_convert(
196  goto_model.symbol_table,
197  goto_model.goto_functions,
198  message_handler);
199 
200  if(options.is_set("validate-goto-model"))
201  {
202  goto_model_validation_optionst goto_model_validation_options{
203  goto_model_validation_optionst ::set_optionst::all_false};
204 
205  goto_model.validate(
206  validation_modet::INVARIANT, goto_model_validation_options);
207  }
208 
209  // stupid hack
211  goto_model.symbol_table);
212 
213  return goto_model;
214 }
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1314
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:47
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_objects_and_link(const std::list< std::string > &file_names, goto_modelt &dest, message_handlert &message_handler)
Reads object files and updates the config if any files were read.
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