cprover
Loading...
Searching...
No Matches
lazy_goto_model.cpp
Go to the documentation of this file.
1
2
5
6#include "lazy_goto_model.h"
7
9
12
13#include <langapi/mode.h>
14
15#include <util/config.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::list<std::string> binaries, sources;
130
131 for(const auto &file : files)
132 {
134 binaries.push_back(file);
135 else
136 sources.push_back(file);
137 }
138
139 if(sources.empty() && !config.java.main_class.empty())
140 {
141 // We assume it's Java.
142 const std::string filename = "";
143 language_filet &lf = add_language_file(filename);
144 lf.language = get_language_from_mode(ID_java);
145 CHECK_RETURN(lf.language != nullptr);
146
147 languaget &language = *lf.language;
149 language.set_language_options(options);
150
151 msg.status() << "Parsing ..." << messaget::eom;
152
153 if(dynamic_cast<java_bytecode_languaget &>(language).parse())
154 {
155 throw invalid_source_file_exceptiont("PARSING ERROR");
156 }
157
158 msg.status() << "Converting" << messaget::eom;
159
161 {
162 throw invalid_source_file_exceptiont("CONVERSION ERROR");
163 }
164 }
165 else
166 {
167 for(const auto &filename : sources)
168 {
169#ifdef _MSC_VER
170 std::ifstream infile(widen(filename));
171#else
172 std::ifstream infile(filename);
173#endif
174
175 if(!infile)
176 {
177 throw system_exceptiont(
178 "failed to open input file '" + filename + '\'');
179 }
180
181 language_filet &lf = add_language_file(filename);
183
184 if(lf.language == nullptr)
185 {
187 "failed to figure out type of file '" + filename + '\'');
188 }
189
190 languaget &language = *lf.language;
192 language.set_language_options(options);
193
194 msg.status() << "Parsing " << filename << messaget::eom;
195
196 if(language.parse(infile, filename))
197 {
198 throw invalid_source_file_exceptiont("PARSING ERROR");
199 }
200
201 lf.get_modules();
202 }
203
204 msg.status() << "Converting" << messaget::eom;
205
207 {
208 throw invalid_source_file_exceptiont("CONVERSION ERROR");
209 }
210 }
211
213 throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};
214
215 bool binaries_provided_start =
217
218 bool entry_point_generation_failed = false;
219
220 if(binaries_provided_start && options.is_set("function"))
221 {
222 // The goto binaries provided already contain a __CPROVER_start
223 // function that may be tied to a different entry point `function`.
224 // Hence, we will rebuild the __CPROVER_start function.
225
226 // Get the language annotation of the existing __CPROVER_start function.
227 std::unique_ptr<languaget> language =
229
230 // To create a new entry point we must first remove the old one
232
233 // Create the new entry-point
234 entry_point_generation_failed =
235 language->generate_support_functions(symbol_table);
236
237 // Remove the function from the goto functions so it is copied back in
238 // from the symbol table during goto_convert
239 if(!entry_point_generation_failed)
241 }
242 else if(!binaries_provided_start)
243 {
244 // Allow all language front-ends to try to provide the user-specified
245 // (--function) entry-point, or some language-specific default:
246 entry_point_generation_failed =
248 }
249
250 if(entry_point_generation_failed)
251 {
252 throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
253 }
254
255 // stupid hack
257}
258
261{
262 symbol_tablet::symbolst::size_type table_size;
263 symbol_tablet::symbolst::size_type new_table_size =
264 symbol_table.symbols.size();
265 do
266 {
267 table_size = new_table_size;
268
269 // Find symbols that correspond to functions
270 std::vector<irep_idt> fn_ids_to_convert;
271 for(const auto &named_symbol : symbol_table.symbols)
272 {
273 if(named_symbol.second.is_function())
274 fn_ids_to_convert.push_back(named_symbol.first);
275 }
276
277 for(const irep_idt &symbol_name : fn_ids_to_convert)
279
280 // Repeat while new symbols are being added in case any of those are
281 // stubbed functions. Even stubs can create new stubs while being
282 // converted if they are special stubs (e.g. string functions)
283 new_table_size = symbol_table.symbols.size();
284 } while(new_table_size != table_size);
285
286 goto_model->goto_functions.compute_location_numbers();
287}
288
290{
292 journalling_symbol_tablet j_symbol_table =
294 if(language_files.final(j_symbol_table))
295 {
296 msg.error() << "CONVERSION ERROR" << messaget::eom;
297 return true;
298 }
299 for(const irep_idt &updated_symbol_id : j_symbol_table.get_updated())
300 {
301 if(j_symbol_table.lookup_ref(updated_symbol_id).is_function())
302 {
303 // Re-convert any that already exist
304 goto_functions.unload(updated_symbol_id);
305 goto_functions.ensure_function_loaded(updated_symbol_id);
306 }
307 }
308
310
312}
313
315{
317}
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1314
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...
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
const changesett & get_updated() const
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.
language_filet & add_language_file(const std::string &filename)
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.
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
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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 symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
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
STL namespace.
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
irep_idt main_class
Definition: config.h:313
Definition: kdev_t.h:19
std::wstring widen(const char *s)
Definition: unicode.cpp:49