cprover
initialize_goto_model.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Get a Goto Program
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "initialize_goto_model.h"
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>
25 #include <langapi/language_file.h>
26 #include <langapi/mode.h>
27 
29 #include <util/exception_utils.h>
30 
31 #include "goto_convert_functions.h"
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::vector<std::string> binaries, sources;
75  binaries.reserve(files.size());
76  sources.reserve(files.size());
77 
78  for(const auto &file : files)
79  {
80  if(is_goto_binary(file, message_handler))
81  binaries.push_back(file);
82  else
83  sources.push_back(file);
84  }
85 
86  language_filest language_files;
87  language_files.set_message_handler(message_handler);
88 
89  goto_modelt goto_model;
90 
91  if(!sources.empty())
92  {
93  for(const auto &filename : sources)
94  {
95  #ifdef _MSC_VER
96  std::ifstream infile(widen(filename));
97  #else
98  std::ifstream infile(filename);
99  #endif
100 
101  if(!infile)
102  {
103  throw system_exceptiont(
104  "Failed to open input file '" + filename + '\'');
105  }
106 
107  language_filet &lf=language_files.add_file(filename);
109 
110  if(lf.language==nullptr)
111  {
113  "Failed to figure out type of file '" + filename + '\'');
114  }
115 
116  languaget &language=*lf.language;
117  language.set_message_handler(message_handler);
118  language.set_language_options(options);
119 
120  msg.status() << "Parsing " << filename << messaget::eom;
121 
122  if(language.parse(infile, filename))
123  {
124  throw invalid_source_file_exceptiont("PARSING ERROR");
125  }
126 
127  lf.get_modules();
128  }
129 
130  msg.status() << "Converting" << messaget::eom;
131 
132  if(language_files.typecheck(goto_model.symbol_table))
133  {
134  throw invalid_source_file_exceptiont("CONVERSION ERROR");
135  }
136  }
137 
138  for(const auto &file : binaries)
139  {
140  msg.status() << "Reading GOTO program from file" << messaget::eom;
141 
142  if(read_object_and_link(file, goto_model, message_handler))
143  {
145  "failed to read object or link in file '" + file + '\'');
146  }
147  }
148 
149  bool binaries_provided_start=
151 
152  bool entry_point_generation_failed=false;
153 
154  if(binaries_provided_start && options.is_set("function"))
155  {
156  // Get the language annotation of the existing __CPROVER_start function.
157  std::unique_ptr<languaget> language = get_entry_point_language(
158  goto_model.symbol_table, options, message_handler);
159 
160  // To create a new entry point we must first remove the old one
162 
163  // Create the new entry-point
164  entry_point_generation_failed =
165  language->generate_support_functions(goto_model.symbol_table);
166 
167  // Remove the function from the goto functions so it is copied back in
168  // from the symbol table during goto_convert
169  if(!entry_point_generation_failed)
170  goto_model.unload(goto_functionst::entry_point());
171  }
172  else if(!binaries_provided_start)
173  {
174  if(options.is_set("function"))
175  {
176  // no entry point is present; Use the mode of the specified entry function
177  // to generate one
178  entry_point_generation_failed = generate_entry_point_for_function(
179  options.get_option("function"), options, goto_model, message_handler);
180  }
181  if(entry_point_generation_failed || !options.is_set("function"))
182  {
183  // Allow all language front-ends to try to provide the user-specified
184  // (--function) entry-point, or some language-specific default:
185  entry_point_generation_failed =
186  language_files.generate_support_functions(goto_model.symbol_table);
187  }
188  }
189 
190  if(entry_point_generation_failed)
191  {
192  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
193  }
194 
195  if(language_files.final(goto_model.symbol_table))
196  {
197  throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
198  }
199 
200  msg.status() << "Generating GOTO Program" << messaget::eom;
201 
202  goto_convert(
203  goto_model.symbol_table,
204  goto_model.goto_functions,
205  message_handler);
206 
207  if(options.is_set("validate-goto-model"))
208  {
209  goto_model_validation_optionst goto_model_validation_options{
210  goto_model_validation_optionst ::set_optionst::all_false};
211 
212  goto_model.validate(
213  validation_modet::INVARIANT, goto_model_validation_options);
214  }
215 
216  // stupid hack
218  goto_model.symbol_table);
219 
220  return goto_model;
221 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
goto_modelt::unload
void unload(const irep_idt &name)
Definition: goto_model.h:68
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:33
get_entry_point_language
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.
Definition: rebuild_goto_start_function.cpp:24
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:83
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::status
mstreamt & status() const
Definition: message.h:414
language_filet
Definition: language_file.h:42
get_language_from_mode
std::unique_ptr< languaget > get_language_from_mode(const irep_idt &mode)
Get the language corresponding to the given mode.
Definition: mode.cpp:51
file
Definition: kdev_t.h:19
goto_model_validation_optionst
Definition: validate_goto_model.h:16
goto_modelt
Definition: goto_model.h:26
mode.h
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:171
options.h
Options.
messaget::eom
static eomt eom
Definition: message.h:297
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:163
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:41
goto_convert
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Definition: goto_convert.cpp:1876
generate_entry_point_for_function
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...
Definition: initialize_goto_model.cpp:36
get_language_from_filename
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
initialize_goto_model.h
Initialize a Goto Program.
rebuild_goto_start_function.h
Goto Programs Author: Thomas Kiley, thomas@diffblue.com.
remove_existing_entry_point
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...
Definition: rebuild_goto_start_function.cpp:47
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
languaget::generate_support_functions
virtual bool generate_support_functions(symbol_tablet &symbol_table)=0
Create language-specific support functions, such as __CPROVER_start, __CPROVER_initialize and languag...
optionst::is_set
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:61
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
language.h
Abstract interface to support a programming language.
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
language_filest::add_file
language_filet & add_file(const std::string &filename)
Definition: language_file.h:77
message_handlert
Definition: message.h:28
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:47
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:48
read_goto_binary.h
Read Goto Programs.
config
configt config
Definition: config.cpp:25
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:178
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
read_object_and_link
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file, and also updates config
Definition: read_goto_binary.cpp:274
unicode.h
languaget
Definition: language.h:38
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:191
config.h
goto_modelt::validate
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_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
initialize_goto_model
goto_modelt initialize_goto_model(const std::vector< std::string > &files, message_handlert &message_handler, const optionst &options)
Definition: initialize_goto_model.cpp:60
goto_convert_functions.h
Goto Programs with Functions.
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
message.h
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
configt::set_object_bits_from_symbol_table
void set_object_bits_from_symbol_table(const symbol_tablet &)
Sets the number of bits used for object addresses.
Definition: config.cpp:1291
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
language_file.h
language_filest
Definition: language_file.h:63