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 <fstream>
15
16#include <util/config.h>
17#include <util/message.h>
18#include <util/options.h>
19
20#ifdef _MSC_VER
21# include <util/unicode.h>
22#endif
23
24#include <langapi/language.h>
26#include <langapi/mode.h>
27
30
32#include "read_goto_binary.h"
33
37 const irep_idt &entry_function_name,
38 const optionst &options,
39 goto_modelt &goto_model,
40 message_handlert &message_handler)
41{
42 auto const entry_function_sym =
43 goto_model.symbol_table.lookup(entry_function_name);
44 if(entry_function_sym == nullptr)
45 {
47 // NOLINTNEXTLINE(whitespace/braces)
48 std::string{"couldn't find function with name '"} +
49 id2string(entry_function_name) + "' in symbol table",
50 "--function"};
51 }
52 PRECONDITION(!entry_function_sym->mode.empty());
53 auto const entry_language = get_language_from_mode(entry_function_sym->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(goto_model.symbol_table);
58}
59
61 const std::vector<std::string> &files,
62 message_handlert &message_handler,
63 const optionst &options)
64{
65 messaget msg(message_handler);
66 if(files.empty())
67 {
69 "missing program argument",
70 "filename",
71 "one or more paths to program files");
72 }
73
74 std::list<std::string> binaries, sources;
75
76 for(const auto &file : files)
77 {
78 if(is_goto_binary(file, message_handler))
79 binaries.push_back(file);
80 else
81 sources.push_back(file);
82 }
83
84 language_filest language_files;
85 language_files.set_message_handler(message_handler);
86
87 goto_modelt goto_model;
88
89 if(!sources.empty())
90 {
91 for(const auto &filename : sources)
92 {
93 #ifdef _MSC_VER
94 std::ifstream infile(widen(filename));
95 #else
96 std::ifstream infile(filename);
97 #endif
98
99 if(!infile)
100 {
101 throw system_exceptiont(
102 "Failed to open input file '" + filename + '\'');
103 }
104
105 language_filet &lf=language_files.add_file(filename);
107
108 if(lf.language==nullptr)
109 {
111 "Failed to figure out type of file '" + filename + '\'');
112 }
113
114 languaget &language=*lf.language;
115 language.set_message_handler(message_handler);
116 language.set_language_options(options);
117
118 msg.status() << "Parsing " << filename << messaget::eom;
119
120 if(language.parse(infile, filename))
121 {
122 throw invalid_source_file_exceptiont("PARSING ERROR");
123 }
124
125 lf.get_modules();
126 }
127
128 msg.status() << "Converting" << messaget::eom;
129
130 if(language_files.typecheck(goto_model.symbol_table))
131 {
132 throw invalid_source_file_exceptiont("CONVERSION ERROR");
133 }
134 }
135
136 if(read_objects_and_link(binaries, goto_model, message_handler))
137 {
139 "failed to read object or link in files"};
140 }
141
142 bool binaries_provided_start=
144
145 bool entry_point_generation_failed=false;
146
147 if(binaries_provided_start && options.is_set("function"))
148 {
149 // Get the language annotation of the existing __CPROVER_start function.
150 std::unique_ptr<languaget> language = get_entry_point_language(
151 goto_model.symbol_table, options, message_handler);
152
153 // To create a new entry point we must first remove the old one
155
156 // Create the new entry-point
157 entry_point_generation_failed =
158 language->generate_support_functions(goto_model.symbol_table);
159
160 // Remove the function from the goto functions so it is copied back in
161 // from the symbol table during goto_convert
162 if(!entry_point_generation_failed)
164 }
165 else if(!binaries_provided_start)
166 {
167 if(options.is_set("function"))
168 {
169 // no entry point is present; Use the mode of the specified entry function
170 // to generate one
171 entry_point_generation_failed = generate_entry_point_for_function(
172 options.get_option("function"), options, goto_model, message_handler);
173 }
174 if(entry_point_generation_failed || !options.is_set("function"))
175 {
176 // Allow all language front-ends to try to provide the user-specified
177 // (--function) entry-point, or some language-specific default:
178 entry_point_generation_failed =
179 language_files.generate_support_functions(goto_model.symbol_table);
180 }
181 }
182
183 if(entry_point_generation_failed)
184 {
185 throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
186 }
187
188 if(language_files.final(goto_model.symbol_table))
189 {
190 throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
191 }
192
193 msg.status() << "Generating GOTO Program" << messaget::eom;
194
196 goto_model.symbol_table,
197 goto_model.goto_functions,
198 message_handler);
199
200 if(options.is_set("validate-goto-model"))
201 {
202 goto_model_validation_optionst goto_model_validation_options{
203 goto_model_validation_optionst ::set_optionst::all_false};
204
205 goto_model.validate(
206 validation_modet::INVARIANT, goto_model_validation_options);
207 }
208
209 // stupid hack
211 goto_model.symbol_table);
212
213 return goto_model;
214}
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition config.cpp:1314
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void unload(const irep_idt &name)
Definition goto_model.h:68
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:98
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:33
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.
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
language_filet & add_file(const std::string &filename)
bool generate_support_functions(symbol_tablet &symbol_table)
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:41
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
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Thrown when some external system fails unexpectedly.
configt config
Definition config.cpp:25
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)
static bool generate_entry_point_for_function(const irep_idt &entry_function_name, const optionst &options, goto_modelt &goto_model, 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
std::wstring widen(const char *s)
Definition unicode.cpp:49