cprover
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/config.h>
16#include <util/message.h>
17#include <util/options.h>
18#include <util/unicode.h>
19
21
22#include <langapi/language.h>
24#include <langapi/mode.h>
25
27#include "read_goto_binary.h"
28
29#include <fstream>
30
34 const optionst &options,
35 symbol_tablet &symbol_table,
36 message_handlert &message_handler)
37{
38 const irep_idt &entry_function_name = options.get_option("function");
40 auto matches = symbol_table.match_name_or_base_name(entry_function_name);
41 // it's ok if this is ambiguous at this point, we just need to get a mode, the
42 // actual entry point generator will take care of resolving (or rejecting)
43 // ambiguity
44 if(matches.empty())
45 {
47 std::string("couldn't find entry with name '") +
48 id2string(entry_function_name) + "' in symbol table",
49 "--function"};
50 }
51 const auto &entry_point_mode = matches.front()->second.mode;
54 CHECK_RETURN(entry_language != nullptr);
55 entry_language->set_message_handler(message_handler);
56 entry_language->set_language_options(options);
57 return entry_language->generate_support_functions(symbol_table);
58}
59
61 const std::list<std::string> &sources,
62 const optionst &options,
63 language_filest &language_files,
64 symbol_tablet &symbol_table,
65 message_handlert &message_handler)
66{
67 if(sources.empty())
68 return;
69
70 messaget msg(message_handler);
71
72 for(const auto &filename : sources)
73 {
74 std::ifstream infile(widen_if_needed(filename));
75
76 if(!infile)
77 {
78 throw system_exceptiont("Failed to open input file '" + filename + '\'');
79 }
80
81 language_filet &lf = language_files.add_file(filename);
82 lf.language = get_language_from_filename(filename);
83
84 if(lf.language == nullptr)
85 {
87 "Failed to figure out type of file", filename};
88 }
89
90 languaget &language = *lf.language;
91 language.set_message_handler(message_handler);
92 language.set_language_options(options);
93
94 msg.status() << "Parsing " << filename << messaget::eom;
95
96 if(language.parse(infile, filename))
97 {
98 throw invalid_input_exceptiont("PARSING ERROR");
99 }
100
101 lf.get_modules();
102 }
103
104 msg.status() << "Converting" << messaget::eom;
105
106 if(language_files.typecheck(symbol_table, message_handler))
107 {
108 throw invalid_input_exceptiont("CONVERSION ERROR");
109 }
110}
111
113 language_filest &language_files,
114 symbol_tablet &symbol_table,
115 const std::function<std::size_t(const irep_idt &)> &unload,
116 const optionst &options,
117 bool try_mode_lookup,
118 message_handlert &message_handler)
119{
122
124
125 if(binaries_provided_start && options.is_set("function"))
126 {
127 // The goto binaries provided already contain a __CPROVER_start
128 // function that may be tied to a different entry point `function`.
129 // Hence, we will rebuild the __CPROVER_start function.
130
131 // Get the language annotation of the existing __CPROVER_start function.
132 std::unique_ptr<languaget> language =
133 get_entry_point_language(symbol_table, options, message_handler);
134
135 // To create a new entry point we must first remove the old one
136 remove_existing_entry_point(symbol_table);
137
138 // Create the new entry-point
140 language->generate_support_functions(symbol_table);
141
142 // Remove the function from the goto functions so it is copied back in
143 // from the symbol table during goto_convert
146 }
148 {
149 if(try_mode_lookup && options.is_set("function"))
150 {
151 // no entry point is present; Use the mode of the specified entry function
152 // to generate one
154 options, symbol_table, message_handler);
155 }
156 if(
158 !options.is_set("function"))
159 {
160 // Allow all language front-ends to try to provide the user-specified
161 // (--function) entry-point, or some language-specific default:
163 language_files.generate_support_functions(symbol_table);
164 }
165 }
166
168 {
169 throw invalid_input_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
170 }
171}
172
174 const std::vector<std::string> &files,
175 message_handlert &message_handler,
176 const optionst &options)
177{
178 messaget msg(message_handler);
179 if(files.empty())
180 {
182 "missing program argument",
183 "filename",
184 "one or more paths to program files");
185 }
186
187 std::list<std::string> binaries, sources;
188
189 for(const auto &file : files)
190 {
191 if(is_goto_binary(file, message_handler))
192 binaries.push_back(file);
193 else
194 sources.push_back(file);
195 }
196
197 language_filest language_files;
198 goto_modelt goto_model;
200 sources, options, language_files, goto_model.symbol_table, message_handler);
201
202 if(read_objects_and_link(binaries, goto_model, message_handler))
203 throw incorrect_goto_program_exceptiont{"failed to read/link goto model"};
204
206 language_files,
207 goto_model.symbol_table,
208 [&goto_model](const irep_idt &id) { return goto_model.unload(id); },
209 options,
210 true,
211 message_handler);
212
213 if(language_files.final(goto_model.symbol_table))
214 {
215 throw invalid_input_exceptiont("FINAL STAGE CONVERSION ERROR");
216 }
217
218 msg.status() << "Generating GOTO Program" << messaget::eom;
219
221 goto_model.symbol_table,
222 goto_model.goto_functions,
223 message_handler);
224
225 if(options.is_set("validate-goto-model"))
226 {
228 goto_model_validation_optionst ::set_optionst::all_false};
229
230 goto_model.validate(
232 }
233
234 // stupid hack
236 goto_model.symbol_table);
237
238 return goto_model;
239}
configt config
Definition config.cpp:25
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
void set_object_bits_from_symbol_table(const symbol_table_baset &)
Sets the number of bits used for object addresses.
Definition config.cpp:1315
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
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
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)
language_filet & add_file(const std::string &filename)
bool generate_support_functions(symbol_table_baset &symbol_table)
bool final(symbol_table_baset &symbol_table)
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition language.h:39
virtual bool parse(std::istream &instream, const std::string &path)=0
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
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 std::string get_option(const std::string &option) const
Definition options.cpp:67
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.
The symbol table.
Thrown when some external system fails unexpectedly.
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...
Initialize a Goto Program.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Definition kdev_t.h:19
#define widen_if_needed(s)
Definition unicode.h:28