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;
144 language.set_language_options(options, message_handler);
145
146 msg.status() << "Parsing ..." << messaget::eom;
147
148 std::istringstream unused;
149 if(language.parse(unused, "", message_handler))
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
179 config.set_object_bits_from_symbol_table(symbol_table);
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)
201 goto_functions.ensure_function_loaded(symbol_name);
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
209 goto_model->goto_functions.compute_location_numbers();
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
232 language_files.clear();
233
235}
236
238{
239 return goto_functions.can_produce_function(id);
240}
configt config
Definition config.cpp:25
A collection of goto functions.
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
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
std::unique_ptr< languaget > language
virtual bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler)=0
virtual void set_language_options(const optionst &, message_handlert &)
Set language-specific options.
Definition language.h:40
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:154
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
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
Definition kdev_t.h:19
dstringt irep_idt