CBMC
Loading...
Searching...
No Matches
initialize_goto_model.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Get a Goto Program
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
13
14#include <util/arith_tools.h>
15#include <util/c_types.h>
16#include <util/config.h>
18#include <util/message.h>
19#include <util/options.h>
20#include <util/unicode.h>
21
23
25#include <langapi/language.h>
27#include <langapi/mode.h>
29
30#include "read_goto_binary.h"
31
32#include <fstream>
33
37 const optionst &options,
38 symbol_tablet &symbol_table,
39 message_handlert &message_handler)
40{
41 const irep_idt &entry_function_name = options.get_option("function");
43 auto matches = symbol_table.match_name_or_base_name(entry_function_name);
44 // it's ok if this is ambiguous at this point, we just need to get a mode, the
45 // actual entry point generator will take care of resolving (or rejecting)
46 // ambiguity
47 if(matches.empty())
48 {
50 std::string("couldn't find entry with name '") +
51 id2string(entry_function_name) + "' in symbol table",
52 "--function"};
53 }
54 const auto &entry_point_mode = matches.front()->second.mode;
57 CHECK_RETURN(entry_language != nullptr);
58 entry_language->set_language_options(options, message_handler);
59 return entry_language->generate_support_functions(
60 symbol_table, message_handler);
61}
62
64 const std::list<std::string> &sources,
65 const optionst &options,
66 language_filest &language_files,
67 symbol_tablet &symbol_table,
68 message_handlert &message_handler)
69{
70 if(sources.empty())
71 return;
72
73 messaget msg(message_handler);
74
75 for(const auto &filename : sources)
76 {
77 std::ifstream infile(widen_if_needed(filename));
78
79 if(!infile)
80 {
81 throw system_exceptiont("Failed to open input file '" + filename + '\'');
82 }
83
84 language_filet &lf = language_files.add_file(filename);
85 lf.language = get_language_from_filename(filename);
86
87 if(lf.language == nullptr)
88 {
90 "Failed to figure out type of file", filename};
91 }
92
93 languaget &language = *lf.language;
94 language.set_language_options(options, message_handler);
95
96 msg.progress() << "Parsing " << filename << messaget::eom;
97
98 if(language.parse(infile, filename, message_handler))
99 {
100 throw invalid_input_exceptiont("PARSING ERROR");
101 }
102
103 lf.get_modules();
104 }
105
106 msg.progress() << "Converting" << messaget::eom;
107
108 if(language_files.typecheck(symbol_table, message_handler))
109 {
110 throw invalid_input_exceptiont("CONVERSION ERROR");
111 }
112}
113
115 language_filest &language_files,
116 symbol_tablet &symbol_table,
117 const std::function<std::size_t(const irep_idt &)> &unload,
118 const optionst &options,
119 bool try_mode_lookup,
120 message_handlert &message_handler)
121{
124
126
127 if(binaries_provided_start && options.is_set("function"))
128 {
129 // The goto binaries provided already contain a __CPROVER_start
130 // function that may be tied to a different entry point `function`.
131 // Hence, we will rebuild the __CPROVER_start function.
132
133 // Get the language annotation of the existing __CPROVER_start function.
134 std::unique_ptr<languaget> language =
135 get_entry_point_language(symbol_table, options, message_handler);
136
137 // To create a new entry point we must first remove the old one
138 remove_existing_entry_point(symbol_table);
139
140 // Create the new entry-point
142 language->generate_support_functions(symbol_table, message_handler);
143
144 // Remove the function from the goto functions so it is copied back in
145 // from the symbol table during goto_convert
148 }
150 {
151 if(try_mode_lookup && options.is_set("function"))
152 {
153 // no entry point is present; Use the mode of the specified entry function
154 // to generate one
156 options, symbol_table, message_handler);
157 }
158 if(
160 !options.is_set("function"))
161 {
162 // Allow all language front-ends to try to provide the user-specified
163 // (--function) entry-point, or some language-specific default:
165 symbol_table, message_handler);
166 }
167 }
168
170 {
171 throw invalid_input_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
172 }
173}
174
176 const std::vector<std::string> &files,
177 message_handlert &message_handler,
178 const optionst &options)
179{
180 messaget msg(message_handler);
181 if(files.empty())
182 {
184 "missing program argument",
185 "filename",
186 "one or more paths to program files");
187 }
188
189 std::list<std::string> binaries, sources;
190
191 for(const auto &file : files)
192 {
193 if(is_goto_binary(file, message_handler))
194 binaries.push_back(file);
195 else
196 sources.push_back(file);
197 }
198
199 language_filest language_files;
200 goto_modelt goto_model;
202 sources, options, language_files, goto_model.symbol_table, message_handler);
203
204 if(read_objects_and_link(binaries, goto_model, message_handler))
205 throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};
206
208 language_files,
209 goto_model.symbol_table,
210 [&goto_model](const irep_idt &id) { return goto_model.unload(id); },
211 options,
212 true,
213 message_handler);
214
215 if(language_files.final(goto_model.symbol_table))
216 {
217 throw invalid_input_exceptiont("FINAL STAGE CONVERSION ERROR");
218 }
219
220 msg.status() << "Generating GOTO Program" << messaget::eom;
221
223 goto_model.symbol_table,
224 goto_model.goto_functions,
225 message_handler);
226
227 if(options.is_set("validate-goto-model"))
228 {
230 goto_model_validation_optionst ::set_optionst::all_false};
231
232 goto_model.validate(
234 }
235
236 // stupid hack
238 goto_model.symbol_table);
239
240 return goto_model;
241}
242
244 goto_modelt &goto_model,
245 message_handlert &message_handler)
246{
247 if(!goto_model.symbol_table.has_symbol(CPROVER_PREFIX "max_malloc_size"))
248 return;
249
251 goto_model.symbol_table.lookup_ref(CPROVER_PREFIX "max_malloc_size").value);
253
254 if(
255 !previous_max_malloc_size_value.has_value() ||
257 {
259 CPROVER_PREFIX "max_malloc_size");
260 max_malloc_size_sym.value =
263
265 recreate_initialize_function(goto_model, message_handler);
266 }
267}
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1422
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
Definition config.cpp:1603
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void validate(const validation_modet vm=validation_modet::INVARIANT, const goto_model_validation_optionst &goto_model_validation_options=goto_model_validation_optionst{}) const override
Check that the goto model is well-formed.
Definition goto_model.h:105
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition goto_model.h:95
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
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.
bool typecheck(symbol_table_baset &symbol_table, const bool keep_file_local, message_handlert &message_handler)
bool generate_support_functions(symbol_table_baset &symbol_table, message_handlert &message_handler)
language_filet & add_file(const std::string &filename)
bool final(symbol_table_baset &symbol_table)
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
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 std::string get_option(const std::string &option) const
Definition options.cpp:67
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
std::list< symbolst::const_iterator > match_name_or_base_name(const irep_idt &id) const
Collect all symbols the name of which matches id or the base name of which matches id.
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.
The symbol table.
Symbol table entry.
Definition symbol.h:28
Thrown when some external system fails unexpectedly.
#define CPROVER_PREFIX
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
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.
static bool generate_entry_point_for_function(const optionst &options, symbol_tablet &symbol_table, message_handlert &message_handler)
Generate an entry point that calls a function with the given name, based on the functions language mo...
void update_max_malloc_size(goto_modelt &goto_model, message_handlert &message_handler)
Update the initial value of __CPROVER_max_malloc_size in case the number of object bits has changed.
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
Abstract interface to support a programming language.
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
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.
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
#define widen_if_needed(s)
Definition unicode.h:28
#define size_type
Definition unistd.c:186