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/cmdline.h>
13 #include <util/config.h>
15 #include <util/unicode.h>
16 
17 #include <langapi/language.h>
18 
19 #include <fstream>
20 
23  post_process_functiont post_process_function,
24  post_process_functionst post_process_functions,
25  can_generate_function_bodyt driver_program_can_generate_function_body,
26  generate_function_bodyt driver_program_generate_function_body,
28  : goto_model(new goto_modelt()),
29  symbol_table(goto_model->symbol_table),
30  goto_functions(
31  goto_model->goto_functions.function_map,
32  language_files,
33  symbol_table,
34  [this] (
35  const irep_idt &function_name,
37  journalling_symbol_tablet &journalling_symbol_table) -> void
38  {
39  goto_model_functiont model_function(
40  journalling_symbol_table,
41  goto_model->goto_functions,
42  function_name,
43  function);
44  this->post_process_function(model_function, *this);
45  },
46  driver_program_can_generate_function_body,
47  driver_program_generate_function_body,
49  post_process_function(post_process_function),
50  post_process_functions(post_process_functions),
51  driver_program_can_generate_function_body(
52  driver_program_can_generate_function_body),
53  driver_program_generate_function_body(
54  driver_program_generate_function_body),
56 {
57  language_files.set_message_handler(message_handler);
58 }
59 
61  : goto_model(std::move(other.goto_model)),
62  symbol_table(goto_model->symbol_table),
63  goto_functions(
64  goto_model->goto_functions.function_map,
65  language_files,
66  symbol_table,
67  [this] (
68  const irep_idt &function_name,
70  journalling_symbol_tablet &journalling_symbol_table) -> void
71  {
72  goto_model_functiont model_function(
73  journalling_symbol_table,
74  goto_model->goto_functions,
75  function_name,
76  function);
77  this->post_process_function(model_function, *this);
78  },
79  other.driver_program_can_generate_function_body,
80  other.driver_program_generate_function_body,
81  other.message_handler),
82  language_files(std::move(other.language_files)),
83  post_process_function(other.post_process_function),
84  post_process_functions(other.post_process_functions),
85  message_handler(other.message_handler)
86 {
87 }
89 
91 {
93 
94  const std::vector<std::string> &files=cmdline.args;
95  if(files.empty())
96  {
97  msg.error() << "Please provide a program" << messaget::eom;
98  throw 0;
99  }
100 
101  std::vector<std::string> binaries, sources;
102  binaries.reserve(files.size());
103  sources.reserve(files.size());
104 
105  for(const auto &file : files)
106  {
107  if(is_goto_binary(file))
108  binaries.push_back(file);
109  else
110  sources.push_back(file);
111  }
112 
113  if(!sources.empty())
114  {
115  for(const auto &filename : sources)
116  {
117 #ifdef _MSC_VER
118  std::ifstream infile(widen(filename));
119 #else
120  std::ifstream infile(filename);
121 #endif
122 
123  if(!infile)
124  {
125  msg.error() << "failed to open input file `" << filename
126  << '\'' << messaget::eom;
127  throw 0;
128  }
129 
130  language_filet &lf=add_language_file(filename);
132 
133  if(lf.language==nullptr)
134  {
135  source_locationt location;
136  location.set_file(filename);
137  msg.error().source_location=location;
138  msg.error() << "failed to figure out type of file" << messaget::eom;
139  throw 0;
140  }
141 
142  languaget &language=*lf.language;
144  language.get_language_options(cmdline);
145 
146  msg.status() << "Parsing " << filename << messaget::eom;
147 
148  if(language.parse(infile, filename))
149  {
150  msg.error() << "PARSING ERROR" << messaget::eom;
151  throw 0;
152  }
153 
154  lf.get_modules();
155  }
156 
157  msg.status() << "Converting" << messaget::eom;
158 
160  {
161  msg.error() << "CONVERSION ERROR" << messaget::eom;
162  throw 0;
163  }
164  }
165 
166  for(const std::string &file : binaries)
167  {
168  msg.status() << "Reading GOTO program from file" << messaget::eom;
169 
171  throw 0;
172  }
173 
174  bool binaries_provided_start =
176 
177  bool entry_point_generation_failed=false;
178 
179  if(binaries_provided_start && cmdline.isset("function"))
180  {
181  // Rebuild the entry-point, using the language annotation of the
182  // existing __CPROVER_start function:
183  rebuild_lazy_goto_start_functiont rebuild_existing_start(
184  cmdline, *this, message_handler);
185  entry_point_generation_failed=rebuild_existing_start();
186  }
187  else if(!binaries_provided_start)
188  {
189  // Unsure of the rationale for only generating stubs when there are no
190  // GOTO binaries in play; simply mirroring old code in language_uit here.
191  if(binaries.empty())
192  {
193  // Enable/disable stub generation for opaque methods
194  bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
196  }
197 
198  // Allow all language front-ends to try to provide the user-specified
199  // (--function) entry-point, or some language-specific default:
200  entry_point_generation_failed=
202  }
203 
204  if(entry_point_generation_failed)
205  {
206  msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
207  throw 0;
208  }
209 
210  // stupid hack
212 }
213 
216 {
219  do
220  {
221  table_size=new_table_size;
222 
223  // Find symbols that correspond to functions
224  std::vector<irep_idt> fn_ids_to_convert;
225  for(const auto &named_symbol : symbol_table.symbols)
226  {
227  if(named_symbol.second.is_function())
228  fn_ids_to_convert.push_back(named_symbol.first);
229  }
230 
231  for(const irep_idt &symbol_name : fn_ids_to_convert)
233 
234  // Repeat while new symbols are being added in case any of those are
235  // stubbed functions. Even stubs can create new stubs while being
236  // converted if they are special stubs (e.g. string functions)
237  new_table_size=symbol_table.symbols.size();
238  } while(new_table_size!=table_size);
239 
240  goto_model->goto_functions.compute_location_numbers();
241 }
242 
244 {
246  journalling_symbol_tablet symbol_table=
247  journalling_symbol_tablet::wrap(this->symbol_table);
249  {
250  msg.error() << "CONVERSION ERROR" << messaget::eom;
251  return true;
252  }
253  for(const irep_idt &updated_symbol_id : symbol_table.get_updated())
254  {
255  if(symbol_table.lookup_ref(updated_symbol_id).is_function())
256  {
257  // Re-convert any that already exist
258  goto_functions.unload(updated_symbol_id);
259  goto_functions.ensure_function_loaded(updated_symbol_id);
260  }
261  }
262 
264 
266 }
267 
269 {
271 }
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool final(symbol_table_baset &symbol_table)
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
std::wstring widen(const char *s)
Definition: unicode.cpp:46
const post_process_functionst post_process_functions
virtual void get_language_options(const cmdlinet &)
Definition: language.h:43
const lazy_goto_functions_mapt goto_functions
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
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)
unsignedbv_typet size_type()
Definition: c_types.cpp:58
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
STL namespace.
Model that holds partially loaded map of functions.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
void unload(const key_type &name) const
std::unique_ptr< languaget > language
Definition: language_file.h:46
message_handlert & message_handler
Logging helper field.
language_filest language_files
argst args
Definition: cmdline.h:37
virtual bool isset(char option) const
Definition: cmdline.cpp:27
source_locationt source_location
Definition: message.h:214
void set_file(const irep_idt &file)
void initialize(const cmdlinet &cmdline)
mstreamt & error() const
Definition: message.h:302
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
void set_should_generate_opaque_method_stubs(bool stubs_enabled)
Turn on or off stub generation for all the languages.
const symbolst & symbols
bool is_function() const
Definition: symbol.h:106
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
void load_all_functions() const
Eagerly loads all functions from the symbol table.
Author: Diffblue Ltd.
bool can_produce_function(const key_type &name) const
Determines if this lazy GOTO functions map can produce a body for the given function.
void ensure_function_loaded(const key_type &name) const
static irep_idt entry_point()
mstreamt & status() const
Definition: message.h:317
std::unique_ptr< goto_modelt > goto_model
const post_process_functiont post_process_function
symbol_tablet & symbol_table
Reference to symbol_table in the internal goto_model.
language_filet & add_language_file(const std::string &filename)
Author: Diffblue Ltd.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
virtual bool parse(std::istream &instream, const std::string &path)=0
bool generate_support_functions(symbol_tablet &symbol_table)
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1178
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:147
Definition: kdev_t.h:19