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
8#include <util/config.h>
11
14
15#include <langapi/mode.h>
16
18
19#ifdef _MSC_VER
20# include <util/unicode.h>
21#endif
22
23#include <langapi/language.h>
24
27 post_process_functiont post_process_function,
28 post_process_functionst post_process_functions,
29 can_generate_function_bodyt driver_program_can_generate_function_body,
30 generate_function_bodyt driver_program_generate_function_body,
31 message_handlert &message_handler)
32 : goto_model(new goto_modelt()),
33 symbol_table(goto_model->symbol_table),
34 goto_functions(
35 goto_model->goto_functions.function_map,
36 language_files,
37 symbol_table,
38 [this](
39 const irep_idt &function_name,
41 journalling_symbol_tablet &journalling_symbol_table) -> void {
42 goto_model_functiont model_function(
43 journalling_symbol_table,
44 goto_model->goto_functions,
45 function_name,
46 function);
47 this->post_process_function(model_function, *this);
48 },
49 driver_program_can_generate_function_body,
50 driver_program_generate_function_body,
51 message_handler),
52 post_process_function(post_process_function),
53 post_process_functions(post_process_functions),
54 driver_program_can_generate_function_body(
55 driver_program_can_generate_function_body),
56 driver_program_generate_function_body(
57 driver_program_generate_function_body),
58 message_handler(message_handler)
59{
60}
61
63 : goto_model(std::move(other.goto_model)),
64 symbol_table(goto_model->symbol_table),
65 goto_functions(
66 goto_model->goto_functions.function_map,
67 language_files,
68 symbol_table,
69 [this](
70 const irep_idt &function_name,
72 journalling_symbol_tablet &journalling_symbol_table) -> void {
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() && config.java.main_class.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::list<std::string> binaries, sources;
126
127 for(const auto &file : files)
128 {
130 binaries.push_back(file);
131 else
132 sources.push_back(file);
133 }
134
135 if(sources.empty() && !config.java.main_class.empty())
136 {
137 // We assume it's Java.
138 const std::string filename = "";
139 language_filet &lf = add_language_file(filename);
140 lf.language = get_language_from_mode(ID_java);
141 CHECK_RETURN(lf.language != nullptr);
142
143 languaget &language = *lf.language;
145 language.set_language_options(options);
146
147 msg.status() << "Parsing ..." << messaget::eom;
148
149 if(dynamic_cast<java_bytecode_languaget &>(language).parse())
150 {
151 throw invalid_input_exceptiont("PARSING ERROR");
152 }
153
154 msg.status() << "Converting" << messaget::eom;
155
157 {
158 throw invalid_input_exceptiont("CONVERSION ERROR");
159 }
160 }
161 else
162 {
164 sources, options, language_files, symbol_table, message_handler);
165 }
166
168 throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};
169
173 [this](const irep_idt &id) { return goto_functions.unload(id); },
174 options,
175 false,
177
178 // stupid hack
180}
181
184{
185 symbol_tablet::symbolst::size_type table_size;
186 symbol_tablet::symbolst::size_type new_table_size =
187 symbol_table.symbols.size();
188 do
189 {
190 table_size = new_table_size;
191
192 // Find symbols that correspond to functions
193 std::vector<irep_idt> fn_ids_to_convert;
194 for(const auto &named_symbol : symbol_table.symbols)
195 {
196 if(named_symbol.second.is_function())
197 fn_ids_to_convert.push_back(named_symbol.first);
198 }
199
200 for(const irep_idt &symbol_name : fn_ids_to_convert)
202
203 // Repeat while new symbols are being added in case any of those are
204 // stubbed functions. Even stubs can create new stubs while being
205 // converted if they are special stubs (e.g. string functions)
206 new_table_size = symbol_table.symbols.size();
207 } while(new_table_size != table_size);
208
210}
211
213{
215 journalling_symbol_tablet j_symbol_table =
217 if(language_files.final(j_symbol_table))
218 {
219 msg.error() << "CONVERSION ERROR" << messaget::eom;
220 return true;
221 }
222 for(const irep_idt &updated_symbol_id : j_symbol_table.get_updated())
223 {
224 if(j_symbol_table.lookup_ref(updated_symbol_id).is_function())
225 {
226 // Re-convert any that already exist
227 goto_functions.unload(updated_symbol_id);
228 goto_functions.ensure_function_loaded(updated_symbol_id);
229 }
230 }
231
233
235}
236
configt config
Definition config.cpp:25
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1317
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:39
bool empty() const
Definition dstring.h:90
A collection of goto functions.
void compute_location_numbers()
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:190
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
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 user-provided input cannot be processed.
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_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
bool final(symbol_table_baset &symbol_table)
std::unique_ptr< languaget > language
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition language.h:39
std::size_t unload(const key_type &name) const
Remove the function named name from the function map, if it exists.
void ensure_function_loaded(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
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
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 is_function() const
Definition symbol.h:106
void initialize_from_source_files(const std::list< std::string > &sources, const optionst &options, language_filest &language_files, symbol_tablet &symbol_table, message_handlert &message_handler)
Populate symbol_table from sources by parsing and type checking via language_files.
void set_up_custom_entry_point(language_filest &language_files, symbol_tablet &symbol_table, const std::function< std::size_t(const irep_idt &)> &unload, const optionst &options, bool try_mode_lookup, message_handlert &message_handler)
Process the "function" option in options to prepare a custom entry point to replace __CPROVER_start.
Initialize a Goto Program.
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
STL namespace.
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.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
irep_idt main_class
Definition config.h:340
Definition kdev_t.h:19