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 #include <iostream>
16 
17 #include <util/config.h>
18 #include <util/message.h>
20 #include <util/options.h>
21 #include <util/unicode.h>
22 
23 #include <langapi/language.h>
24 #include <langapi/language_file.h>
25 #include <langapi/mode.h>
26 
28 #include <util/exception_utils.h>
29 
30 #include "goto_convert_functions.h"
31 #include "read_goto_binary.h"
32 
36  const irep_idt &entry_function_name,
37  const optionst &options,
38  goto_modelt &goto_model,
39  message_handlert &message_handler)
40 {
41  auto const entry_function_sym =
42  goto_model.symbol_table.lookup(entry_function_name);
43  if(entry_function_sym == nullptr)
44  {
46  // NOLINTNEXTLINE(whitespace/braces)
47  std::string{"couldn't find function with name '"} +
48  id2string(entry_function_name) + "' in symbol table",
49  "--function"};
50  }
51  PRECONDITION(!entry_function_sym->mode.empty());
52  auto const entry_language = get_language_from_mode(entry_function_sym->mode);
53  CHECK_RETURN(entry_language != nullptr);
54  entry_language->set_message_handler(message_handler);
55  entry_language->set_language_options(options);
56  return entry_language->generate_support_functions(goto_model.symbol_table);
57 }
58 
60  const std::vector<std::string> &files,
61  message_handlert &message_handler,
62  const optionst &options)
63 {
64  messaget msg(message_handler);
65  if(files.empty())
66  {
68  "missing program argument",
69  "filename",
70  "one or more paths to program files");
71  }
72 
73  std::vector<std::string> binaries, sources;
74  binaries.reserve(files.size());
75  sources.reserve(files.size());
76 
77  for(const auto &file : files)
78  {
79  if(is_goto_binary(file, message_handler))
80  binaries.push_back(file);
81  else
82  sources.push_back(file);
83  }
84 
85  language_filest language_files;
86  language_files.set_message_handler(message_handler);
87 
88  goto_modelt goto_model;
89 
90  if(!sources.empty())
91  {
92  for(const auto &filename : sources)
93  {
94  #ifdef _MSC_VER
95  std::ifstream infile(widen(filename));
96  #else
97  std::ifstream infile(filename);
98  #endif
99 
100  if(!infile)
101  {
102  throw system_exceptiont(
103  "Failed to open input file '" + filename + '\'');
104  }
105 
106  language_filet &lf=language_files.add_file(filename);
108 
109  if(lf.language==nullptr)
110  {
112  "Failed to figure out type of file '" + filename + '\'');
113  }
114 
115  languaget &language=*lf.language;
116  language.set_message_handler(message_handler);
117  language.set_language_options(options);
118 
119  msg.status() << "Parsing " << filename << messaget::eom;
120 
121  if(language.parse(infile, filename))
122  {
123  throw invalid_source_file_exceptiont("PARSING ERROR");
124  }
125 
126  lf.get_modules();
127  }
128 
129  msg.status() << "Converting" << messaget::eom;
130 
131  if(language_files.typecheck(goto_model.symbol_table))
132  {
133  throw invalid_source_file_exceptiont("CONVERSION ERROR");
134  }
135  }
136 
137  for(const auto &file : binaries)
138  {
139  msg.status() << "Reading GOTO program from file" << messaget::eom;
140 
141  if(read_object_and_link(file, goto_model, message_handler))
142  {
144  "failed to read object or link in file '" + file + '\'');
145  }
146  }
147 
148  bool binaries_provided_start=
150 
151  bool entry_point_generation_failed=false;
152 
153  if(binaries_provided_start && options.is_set("function"))
154  {
155  // Get the language annotation of the existing __CPROVER_start function.
156  std::unique_ptr<languaget> language = get_entry_point_language(
157  goto_model.symbol_table, options, message_handler);
158 
159  // To create a new entry point we must first remove the old one
161 
162  // Create the new entry-point
163  entry_point_generation_failed =
164  language->generate_support_functions(goto_model.symbol_table);
165 
166  // Remove the function from the goto functions so it is copied back in
167  // from the symbol table during goto_convert
168  if(!entry_point_generation_failed)
169  goto_model.unload(goto_functionst::entry_point());
170  }
171  else if(!binaries_provided_start)
172  {
173  if(options.is_set("function"))
174  {
175  // no entry point is present; Use the mode of the specified entry function
176  // to generate one
177  entry_point_generation_failed = generate_entry_point_for_function(
178  options.get_option("function"), options, goto_model, message_handler);
179  }
180  if(entry_point_generation_failed || !options.is_set("function"))
181  {
182  // Allow all language front-ends to try to provide the user-specified
183  // (--function) entry-point, or some language-specific default:
184  entry_point_generation_failed =
185  language_files.generate_support_functions(goto_model.symbol_table);
186  }
187  }
188 
189  if(entry_point_generation_failed)
190  {
191  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
192  }
193 
194  if(language_files.final(goto_model.symbol_table))
195  {
196  throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
197  }
198 
199  msg.status() << "Generating GOTO Program" << messaget::eom;
200 
201  goto_convert(
202  goto_model.symbol_table,
203  goto_model.goto_functions,
204  message_handler);
205 
206  if(options.is_set("validate-goto-model"))
207  {
208  goto_model_validation_optionst goto_model_validation_options{
209  goto_model_validation_optionst ::set_optionst::all_false};
210 
211  goto_model.validate(
212  validation_modet::INVARIANT, goto_model_validation_options);
213  }
214 
215  // stupid hack
217  goto_model.symbol_table);
218 
219  return goto_model;
220 }
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:35
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:26
optionst
Definition: options.h:23
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table, const bool keep_file_local=false)
Definition: language_file.cpp:85
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:41
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:50
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:165
languaget::set_language_options
virtual void set_language_options(const optionst &)
Set language-specific options.
Definition: language.h:43
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:1846
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:35
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:101
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:49
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:464
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
object_factory_parameters.h
language_filest::add_file
language_filet & add_file(const std::string &filename)
Definition: language_file.h:76
message_handlert
Definition: message.h:28
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
read_goto_binary.h
Read Goto Programs.
config
configt config
Definition: config.cpp:24
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:180
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:273
unicode.h
languaget
Definition: language.h:40
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:190
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:90
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:59
goto_convert_functions.h
Goto Programs with Functions.
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:1266
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
validation_modet::INVARIANT
@ INVARIANT
language_file.h
language_filest
Definition: language_file.h:62