cprover
lazy_goto_model.cpp
Go to the documentation of this file.
1 
5 
6 #include "lazy_goto_model.h"
7 #include "read_goto_binary.h"
9 
10 #include <langapi/mode.h>
11 
12 #include <util/config.h>
13 #include <util/exception_utils.h>
15 #include <util/options.h>
16 #include <util/unicode.h>
17 
18 #include <langapi/language.h>
19 
20 #include <fstream>
21 
24  post_process_functiont post_process_function,
25  post_process_functionst post_process_functions,
26  can_generate_function_bodyt driver_program_can_generate_function_body,
27  generate_function_bodyt driver_program_generate_function_body,
28  message_handlert &message_handler)
29  : goto_model(new goto_modelt()),
30  symbol_table(goto_model->symbol_table),
31  goto_functions(
32  goto_model->goto_functions.function_map,
33  language_files,
34  symbol_table,
35  [this] (
36  const irep_idt &function_name,
38  journalling_symbol_tablet &journalling_symbol_table) -> void
39  {
40  goto_model_functiont model_function(
41  journalling_symbol_table,
42  goto_model->goto_functions,
43  function_name,
44  function);
45  this->post_process_function(model_function, *this);
46  },
47  driver_program_can_generate_function_body,
48  driver_program_generate_function_body,
49  message_handler),
50  post_process_function(post_process_function),
51  post_process_functions(post_process_functions),
52  driver_program_can_generate_function_body(
53  driver_program_can_generate_function_body),
54  driver_program_generate_function_body(
55  driver_program_generate_function_body),
56  message_handler(message_handler)
57 {
58  language_files.set_message_handler(message_handler);
59 }
60 
62  : goto_model(std::move(other.goto_model)),
63  symbol_table(goto_model->symbol_table),
64  goto_functions(
65  goto_model->goto_functions.function_map,
66  language_files,
67  symbol_table,
68  [this] (
69  const irep_idt &function_name,
71  journalling_symbol_tablet &journalling_symbol_table) -> void
72  {
73  goto_model_functiont model_function(
74  journalling_symbol_table,
75  goto_model->goto_functions,
76  function_name,
77  function);
78  this->post_process_function(model_function, *this);
79  },
80  other.driver_program_can_generate_function_body,
81  other.driver_program_generate_function_body,
82  other.message_handler),
83  language_files(std::move(other.language_files)),
84  post_process_function(other.post_process_function),
85  post_process_functions(other.post_process_functions),
86  message_handler(other.message_handler)
87 {
88 }
90 
111  const std::vector<std::string> &files,
112  const optionst &options)
113 {
115 
116  if(files.empty())
117  {
119  "no program provided",
120  "source file names",
121  "one or more paths to a goto binary or a source file in a supported "
122  "language");
123  }
124 
125  std::vector<std::string> binaries, sources;
126  binaries.reserve(files.size());
127  sources.reserve(files.size());
128 
129  for(const auto &file : files)
130  {
131  if(is_goto_binary(file))
132  binaries.push_back(file);
133  else
134  sources.push_back(file);
135  }
136 
137  if(!sources.empty())
138  {
139  for(const auto &filename : sources)
140  {
141 #ifdef _MSC_VER
142  std::ifstream infile(widen(filename));
143 #else
144  std::ifstream infile(filename);
145 #endif
146 
147  if(!infile)
148  {
149  throw system_exceptiont(
150  "failed to open input file `" + filename + '\'');
151  }
152 
153  language_filet &lf=add_language_file(filename);
155 
156  if(lf.language==nullptr)
157  {
159  "failed to figure out type of file `" + filename + '\'');
160  }
161 
162  languaget &language=*lf.language;
164  language.set_language_options(options);
165 
166  msg.status() << "Parsing " << filename << messaget::eom;
167 
168  if(language.parse(infile, filename))
169  {
170  throw invalid_source_file_exceptiont("PARSING ERROR");
171  }
172 
173  lf.get_modules();
174  }
175 
176  msg.status() << "Converting" << messaget::eom;
177 
179  {
180  throw invalid_source_file_exceptiont("CONVERSION ERROR");
181  }
182  }
183 
184  for(const std::string &file : binaries)
185  {
186  msg.status() << "Reading GOTO program from file" << messaget::eom;
187 
189  {
190  source_locationt source_location;
191  source_location.set_file(file);
193  "failed to read/link goto model", source_location);
194  }
195  }
196 
197  bool binaries_provided_start =
199 
200  bool entry_point_generation_failed=false;
201 
202  if(binaries_provided_start && options.is_set("function"))
203  {
204  // Rebuild the entry-point, using the language annotation of the
205  // existing __CPROVER_start function:
206  rebuild_lazy_goto_start_functiont rebuild_existing_start(
207  options, *this, message_handler);
208  entry_point_generation_failed=rebuild_existing_start();
209  }
210  else if(!binaries_provided_start)
211  {
212  // Allow all language front-ends to try to provide the user-specified
213  // (--function) entry-point, or some language-specific default:
214  entry_point_generation_failed=
216  }
217 
218  if(entry_point_generation_failed)
219  {
220  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
221  }
222 
223  // stupid hack
225 }
226 
229 {
232  do
233  {
234  table_size=new_table_size;
235 
236  // Find symbols that correspond to functions
237  std::vector<irep_idt> fn_ids_to_convert;
238  for(const auto &named_symbol : symbol_table.symbols)
239  {
240  if(named_symbol.second.is_function())
241  fn_ids_to_convert.push_back(named_symbol.first);
242  }
243 
244  for(const irep_idt &symbol_name : fn_ids_to_convert)
246 
247  // Repeat while new symbols are being added in case any of those are
248  // stubbed functions. Even stubs can create new stubs while being
249  // converted if they are special stubs (e.g. string functions)
250  new_table_size=symbol_table.symbols.size();
251  } while(new_table_size!=table_size);
252 
253  goto_model->goto_functions.compute_location_numbers();
254 }
255 
257 {
259  journalling_symbol_tablet j_symbol_table =
261  if(language_files.final(j_symbol_table))
262  {
263  msg.error() << "CONVERSION ERROR" << messaget::eom;
264  return true;
265  }
266  for(const irep_idt &updated_symbol_id : j_symbol_table.get_updated())
267  {
268  if(j_symbol_table.lookup_ref(updated_symbol_id).is_function())
269  {
270  // Re-convert any that already exist
271  goto_functions.unload(updated_symbol_id);
272  goto_functions.ensure_function_loaded(updated_symbol_id);
273  }
274  }
275 
277 
279 }
280 
282 {
284 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
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:78
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:35
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:126
lazy_goto_modelt::symbol_table
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
Definition: lazy_goto_model.h:251
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:96
is_goto_binary
bool is_goto_binary(const std::string &filename)
Definition: read_goto_binary.cpp:168
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:35
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:78
optionst
Definition: options.h:22
lazy_goto_modelt::goto_functions
const lazy_goto_functions_mapt goto_functions
Definition: lazy_goto_model.h:254
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table)
Definition: language_file.cpp:85
messaget::status
mstreamt & status() const
Definition: message.h:401
lazy_goto_modelt::add_language_file
language_filet & add_language_file(const std::string &filename)
Definition: lazy_goto_model.h:189
lazy_goto_modelt::language_files
language_filest language_files
Definition: lazy_goto_model.h:255
language_filet
Definition: language_file.h:40
file
Definition: kdev_t.h:19
journalling_symbol_tablet::get_updated
const changesett & get_updated() const
Definition: journalling_symbol_table.h:147
goto_modelt
Definition: goto_model.h:24
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:133
mode.h
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:170
options.h
messaget::eom
static eomt eom
Definition: message.h:284
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:155
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:281
lazy_goto_modelt::message_handler
message_handlert & message_handler
Logging helper field.
Definition: lazy_goto_model.h:264
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:43
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:89
lazy_goto_modelt::finalize
bool finalize()
Definition: lazy_goto_model.cpp:256
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:101
messaget::error
mstreamt & error() const
Definition: message.h:386
rebuild_goto_start_function.h
lazy_goto_modelt
A GOTO model that produces function bodies on demand.
Definition: lazy_goto_model.h:41
symbolt::is_function
bool is_function() const
Definition: symbol.h:105
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:60
source_locationt::set_file
void set_file(const irep_idt &file)
Definition: source_location.h:92
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:60
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
language.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
lazy_goto_modelt::goto_model
std::unique_ptr< goto_modelt > goto_model
Definition: lazy_goto_model.h:247
message_handlert
Definition: message.h:24
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:26
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:110
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
read_goto_binary.h
lazy_goto_modelt::post_process_functions
const post_process_functionst post_process_functions
Definition: lazy_goto_model.h:259
config
configt config
Definition: config.cpp:24
source_locationt
Definition: source_location.h:20
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:170
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
language_filest::clear
void clear()
Definition: language_file.h:134
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
lazy_goto_functions_mapt::ensure_function_loaded
void ensure_function_loaded(const key_type &name) const
Definition: lazy_goto_functions_map.h:135
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:234
unicode.h
languaget
Definition: language.h:39
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:228
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
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:37
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:1232
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removed.
Definition: journalling_symbol_table.h:35
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:153
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.
rebuild_goto_start_function_baset
Definition: rebuild_goto_start_function.h:28