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 =
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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
lazy_goto_functions_mapt::can_produce_function
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
Definition: lazy_goto_functions_map.h:123
lazy_goto_modelt::symbol_table
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Definition: lazy_goto_model.h:265
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
configt::javat::main_class
irep_idt main_class
Definition: config.h:247
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:33
java_bytecode_language.h
journalling_symbol_tablet::wrap
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
Definition: journalling_symbol_table.h:80
lazy_goto_functions_mapt::post_process_function
const post_process_functiont post_process_function
Definition: lazy_goto_functions_map.h:75
get_entry_point_language
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.
Definition: rebuild_goto_start_function.cpp:24
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:83
lazy_goto_modelt::goto_functions
const lazy_goto_functions_mapt goto_functions
Definition: lazy_goto_model.h:268
messaget::status
mstreamt & status() const
Definition: message.h:414
lazy_goto_modelt::add_language_file
language_filet & add_language_file(const std::string &filename)
Definition: lazy_goto_model.h:191
lazy_goto_modelt::language_files
language_filest language_files
Definition: lazy_goto_model.h:269
language_filet
Definition: language_file.h:42
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
file
Definition: kdev_t.h:19
journalling_symbol_tablet::get_updated
const changesett & get_updated() const
Definition: journalling_symbol_table.h:150
goto_modelt
Definition: goto_model.h:26
journalling_symbol_table.h
Author: Diffblue Ltd.
lazy_goto_functions_mapt::unload
void unload(const key_type &name) const
Definition: lazy_goto_functions_map.h:129
mode.h
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
options.h
Options.
messaget::eom
static eomt eom
Definition: message.h:297
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:163
lazy_goto_modelt::can_produce_function
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition: lazy_goto_model.cpp:326
lazy_goto_modelt::message_handler
message_handlert & message_handler
Logging helper field.
Definition: lazy_goto_model.h:278
lazy_goto_model.h
Author: Diffblue Ltd.
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
incorrect_goto_program_exceptiont
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Definition: exception_utils.h:90
lazy_goto_modelt::finalize
bool finalize()
Definition: lazy_goto_model.cpp:301
get_language_from_filename
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
messaget::error
mstreamt & error() const
Definition: message.h:399
rebuild_goto_start_function.h
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
remove_existing_entry_point
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...
Definition: rebuild_goto_start_function.cpp:47
languaget::generate_support_functions
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:43
symbolt::is_function
bool is_function() const
Definition: symbol.h:100
optionst::is_set
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
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:95
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:61
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
lazy_goto_modelt::goto_model
std::unique_ptr< goto_modelt > goto_model
Definition: lazy_goto_model.h:261
lazy_goto_modelt::unload
void unload(const irep_idt &name) const
Definition: lazy_goto_model.h:186
message_handlert
Definition: message.h:28
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
lazy_goto_modelt::initialize
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 ...
Definition: lazy_goto_model.cpp:114
dstringt::empty
bool empty() const
Definition: dstring.h:88
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:47
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:48
read_goto_binary.h
Read Goto Programs.
lazy_goto_modelt::post_process_functions
const post_process_functionst post_process_functions
Definition: lazy_goto_model.h:273
config
configt config
Definition: config.cpp:25
source_locationt
Definition: source_location.h:19
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:178
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
language_filest::clear
void clear()
Definition: language_file.h:136
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
lazy_goto_functions_mapt::ensure_function_loaded
void ensure_function_loaded(const key_type &name) const
Definition: lazy_goto_functions_map.h:134
configt::java
struct configt::javat java
read_object_and_link
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
Definition: read_goto_binary.cpp:274
unicode.h
languaget
Definition: language.h:38
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:191
config.h
lazy_goto_modelt::load_all_functions
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Definition: lazy_goto_model.cpp:272
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
java_bytecode_languaget
Definition: java_bytecode_language.h:273
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
configt::set_object_bits_from_symbol_table
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1291
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
lazy_goto_modelt::lazy_goto_modelt
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.