cprover
lazy_goto_model.cpp
Go to the documentation of this file.
1 
5 
6 #include "lazy_goto_model.h"
7 
9 
12 
13 #include <langapi/mode.h>
14 
15 #include <util/config.h>
16 #include <util/exception_utils.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 
26 #include <fstream>
27 
30  post_process_functiont post_process_function,
31  post_process_functionst post_process_functions,
32  can_generate_function_bodyt driver_program_can_generate_function_body,
33  generate_function_bodyt driver_program_generate_function_body,
34  message_handlert &message_handler)
35  : goto_model(new goto_modelt()),
36  symbol_table(goto_model->symbol_table),
37  goto_functions(
38  goto_model->goto_functions.function_map,
39  language_files,
40  symbol_table,
41  [this](
42  const irep_idt &function_name,
44  journalling_symbol_tablet &journalling_symbol_table) -> void {
45  goto_model_functiont model_function(
46  journalling_symbol_table,
47  goto_model->goto_functions,
48  function_name,
49  function);
50  this->post_process_function(model_function, *this);
51  },
52  driver_program_can_generate_function_body,
53  driver_program_generate_function_body,
54  message_handler),
55  post_process_function(post_process_function),
56  post_process_functions(post_process_functions),
57  driver_program_can_generate_function_body(
58  driver_program_can_generate_function_body),
59  driver_program_generate_function_body(
60  driver_program_generate_function_body),
61  message_handler(message_handler)
62 {
63  language_files.set_message_handler(message_handler);
64 }
65 
67  : goto_model(std::move(other.goto_model)),
68  symbol_table(goto_model->symbol_table),
69  goto_functions(
70  goto_model->goto_functions.function_map,
71  language_files,
72  symbol_table,
73  [this](
74  const irep_idt &function_name,
76  journalling_symbol_tablet &journalling_symbol_table) -> void {
77  goto_model_functiont model_function(
78  journalling_symbol_table,
79  goto_model->goto_functions,
80  function_name,
81  function);
82  this->post_process_function(model_function, *this);
83  },
84  other.driver_program_can_generate_function_body,
85  other.driver_program_generate_function_body,
86  other.message_handler),
87  language_files(std::move(other.language_files)),
88  post_process_function(other.post_process_function),
89  post_process_functions(other.post_process_functions),
90  message_handler(other.message_handler)
91 {
92 }
94 
115  const std::vector<std::string> &files,
116  const optionst &options)
117 {
119 
120  if(files.empty() && config.java.main_class.empty())
121  {
123  "no program provided",
124  "source file names",
125  "one or more paths to a goto binary or a source file in a supported "
126  "language");
127  }
128 
129  std::vector<std::string> binaries, sources;
130  binaries.reserve(files.size());
131  sources.reserve(files.size());
132 
133  for(const auto &file : files)
134  {
136  binaries.push_back(file);
137  else
138  sources.push_back(file);
139  }
140 
141  if(sources.empty() && !config.java.main_class.empty())
142  {
143  // We assume it's Java.
144  const std::string filename = "";
145  language_filet &lf = add_language_file(filename);
146  lf.language = get_language_from_mode(ID_java);
147  CHECK_RETURN(lf.language != nullptr);
148 
149  languaget &language = *lf.language;
151  language.set_language_options(options);
152 
153  msg.status() << "Parsing ..." << messaget::eom;
154 
155  if(dynamic_cast<java_bytecode_languaget &>(language).parse())
156  {
157  throw invalid_source_file_exceptiont("PARSING ERROR");
158  }
159 
160  msg.status() << "Converting" << messaget::eom;
161 
163  {
164  throw invalid_source_file_exceptiont("CONVERSION ERROR");
165  }
166  }
167  else
168  {
169  for(const auto &filename : sources)
170  {
171 #ifdef _MSC_VER
172  std::ifstream infile(widen(filename));
173 #else
174  std::ifstream infile(filename);
175 #endif
176 
177  if(!infile)
178  {
179  throw system_exceptiont(
180  "failed to open input file '" + filename + '\'');
181  }
182 
183  language_filet &lf = add_language_file(filename);
184  lf.language = get_language_from_filename(filename);
185 
186  if(lf.language == nullptr)
187  {
189  "failed to figure out type of file '" + filename + '\'');
190  }
191 
192  languaget &language = *lf.language;
194  language.set_language_options(options);
195 
196  msg.status() << "Parsing " << filename << messaget::eom;
197 
198  if(language.parse(infile, filename))
199  {
200  throw invalid_source_file_exceptiont("PARSING ERROR");
201  }
202 
203  lf.get_modules();
204  }
205 
206  msg.status() << "Converting" << messaget::eom;
207 
209  {
210  throw invalid_source_file_exceptiont("CONVERSION ERROR");
211  }
212  }
213 
214  for(const std::string &file : binaries)
215  {
216  msg.status() << "Reading GOTO program from file" << messaget::eom;
217 
219  {
220  source_locationt source_location;
221  source_location.set_file(file);
223  "failed to read/link goto model", source_location);
224  }
225  }
226 
227  bool binaries_provided_start =
229 
230  bool entry_point_generation_failed = false;
231 
232  if(binaries_provided_start && options.is_set("function"))
233  {
234  // The goto binaries provided already contain a __CPROVER_start
235  // function that may be tied to a different entry point `function`.
236  // Hence, we will rebuild the __CPROVER_start function.
237 
238  // Get the language annotation of the existing __CPROVER_start function.
239  std::unique_ptr<languaget> language =
241 
242  // To create a new entry point we must first remove the old one
244 
245  // Create the new entry-point
246  entry_point_generation_failed =
247  language->generate_support_functions(symbol_table);
248 
249  // Remove the function from the goto functions so it is copied back in
250  // from the symbol table during goto_convert
251  if(!entry_point_generation_failed)
253  }
254  else if(!binaries_provided_start)
255  {
256  // Allow all language front-ends to try to provide the user-specified
257  // (--function) entry-point, or some language-specific default:
258  entry_point_generation_failed =
260  }
261 
262  if(entry_point_generation_failed)
263  {
264  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
265  }
266 
267  // stupid hack
269 }
270 
273 {
275  symbol_tablet::symbolst::size_type new_table_size =
276  symbol_table.symbols.size();
277  do
278  {
279  table_size = new_table_size;
280 
281  // Find symbols that correspond to functions
282  std::vector<irep_idt> fn_ids_to_convert;
283  for(const auto &named_symbol : symbol_table.symbols)
284  {
285  if(named_symbol.second.is_function())
286  fn_ids_to_convert.push_back(named_symbol.first);
287  }
288 
289  for(const irep_idt &symbol_name : fn_ids_to_convert)
291 
292  // Repeat while new symbols are being added in case any of those are
293  // stubbed functions. Even stubs can create new stubs while being
294  // converted if they are special stubs (e.g. string functions)
295  new_table_size = symbol_table.symbols.size();
296  } while(new_table_size != table_size);
297 
298  goto_model->goto_functions.compute_location_numbers();
299 }
300 
302 {
304  journalling_symbol_tablet j_symbol_table =
306  if(language_files.final(j_symbol_table))
307  {
308  msg.error() << "CONVERSION ERROR" << messaget::eom;
309  return true;
310  }
311  for(const irep_idt &updated_symbol_id : j_symbol_table.get_updated())
312  {
313  if(j_symbol_table.lookup_ref(updated_symbol_id).is_function())
314  {
315  // Re-convert any that already exist
316  goto_functions.unload(updated_symbol_id);
317  goto_functions.ensure_function_loaded(updated_symbol_id);
318  }
319  }
320 
322 
324 }
325 
327 {
329 }
unsignedbv_typet size_type()
Definition: c_types.cpp:58
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1291
struct configt::javat java
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
A collection of goto functions.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
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.
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
const changesett & get_updated() const
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
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
void ensure_function_loaded(const key_type &name) const
void unload(const key_type &name) const
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
A GOTO model that produces function bodies on demand.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
std::unique_ptr< goto_modelt > goto_model
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
const lazy_goto_functions_mapt goto_functions
language_filest language_files
const post_process_functionst post_process_functions
void unload(const irep_idt &name) const
lazy_goto_modelt(post_process_functiont post_process_function, post_process_functionst post_process_functions, can_generate_function_bodyt driver_program_can_generate_function_body, generate_function_bodyt driver_program_generate_function_body, message_handlert &message_handler)
Construct a lazy GOTO model, supplying callbacks that customise its behaviour.
message_handlert & message_handler
Logging helper field.
language_filet & add_language_file(const std::string &filename)
void initialize(const std::vector< std::string > &files, const optionst &options)
Performs initial symbol table and language_filest initialization from a given commandline and parsed ...
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
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
void set_file(const irep_idt &file)
const symbolst & symbols
Read-only field, used to look up symbols given their names.
const symbolt & lookup_ref(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.
bool is_function() const
Definition: symbol.h:100
Thrown when some external system fails unexpectedly.
configt config
Definition: config.cpp:25
Author: Diffblue Ltd.
Abstract interface to support a programming language.
Author: Diffblue Ltd.
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
irep_idt main_class
Definition: config.h:247
Definition: kdev_t.h:19
std::wstring widen(const char *s)
Definition: unicode.cpp:48