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/mode.h>
24 #include <langapi/language.h>
25 
27 #include <util/exception_utils.h>
28 
29 #include "goto_convert_functions.h"
30 #include "read_goto_binary.h"
31 
33  const std::vector<std::string> &files,
34  message_handlert &message_handler,
35  const optionst &options)
36 {
37  messaget msg(message_handler);
38  if(files.empty())
39  {
41  "missing program argument",
42  "filename",
43  "one or more paths to program files");
44  }
45 
46  std::vector<std::string> binaries, sources;
47  binaries.reserve(files.size());
48  sources.reserve(files.size());
49 
50  for(const auto &file : files)
51  {
52  if(is_goto_binary(file))
53  binaries.push_back(file);
54  else
55  sources.push_back(file);
56  }
57 
58  language_filest language_files;
59  language_files.set_message_handler(message_handler);
60 
61  goto_modelt goto_model;
62 
63  if(!sources.empty())
64  {
65  for(const auto &filename : sources)
66  {
67  #ifdef _MSC_VER
68  std::ifstream infile(widen(filename));
69  #else
70  std::ifstream infile(filename);
71  #endif
72 
73  if(!infile)
74  {
75  throw system_exceptiont(
76  "Failed to open input file `" + filename + '\'');
77  }
78 
79  language_filet &lf=language_files.add_file(filename);
81 
82  if(lf.language==nullptr)
83  {
85  "Failed to figure out type of file `" + filename + '\'');
86  }
87 
88  languaget &language=*lf.language;
89  language.set_message_handler(message_handler);
90  language.set_language_options(options);
91 
92  msg.status() << "Parsing " << filename << messaget::eom;
93 
94  if(language.parse(infile, filename))
95  {
96  throw invalid_source_file_exceptiont("PARSING ERROR");
97  }
98 
99  lf.get_modules();
100  }
101 
102  msg.status() << "Converting" << messaget::eom;
103 
104  if(language_files.typecheck(goto_model.symbol_table))
105  {
106  throw invalid_source_file_exceptiont("CONVERSION ERROR");
107  }
108  }
109 
110  for(const auto &file : binaries)
111  {
112  msg.status() << "Reading GOTO program from file" << messaget::eom;
113 
114  if(read_object_and_link(file, goto_model, message_handler))
115  {
117  "failed to read object or link in file `" + file + '\'');
118  }
119  }
120 
121  bool binaries_provided_start=
123 
124  bool entry_point_generation_failed=false;
125 
126  if(binaries_provided_start && options.is_set("function"))
127  {
128  // Rebuild the entry-point, using the language annotation of the
129  // existing __CPROVER_start function:
130  rebuild_goto_start_functiont rebuild_existing_start(
131  options, goto_model, msg.get_message_handler());
132  entry_point_generation_failed=rebuild_existing_start();
133  }
134  else if(!binaries_provided_start)
135  {
136  // Allow all language front-ends to try to provide the user-specified
137  // (--function) entry-point, or some language-specific default:
138  entry_point_generation_failed=
139  language_files.generate_support_functions(goto_model.symbol_table);
140  }
141 
142  if(entry_point_generation_failed)
143  {
144  throw invalid_source_file_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
145  }
146 
147  if(language_files.final(goto_model.symbol_table))
148  {
149  throw invalid_source_file_exceptiont("FINAL STAGE CONVERSION ERROR");
150  }
151 
152  msg.status() << "Generating GOTO Program" << messaget::eom;
153 
154  goto_convert(
155  goto_model.symbol_table,
156  goto_model.goto_functions,
157  message_handler);
158 
159  if(options.is_set("validate-goto-model"))
160  {
162  }
163 
164  // stupid hack
166  goto_model.symbol_table);
167 
168  return goto_model;
169 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
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:78
exception_utils.h
is_goto_binary
bool is_goto_binary(const std::string &filename)
Definition: read_goto_binary.cpp:168
language_filet::get_modules
void get_modules()
Definition: language_file.cpp:35
optionst
Definition: options.h:22
language_filest::typecheck
bool typecheck(symbol_tablet &symbol_table)
Definition: language_file.cpp:85
messaget::status
mstreamt & status() const
Definition: message.h:401
language_filet
Definition: language_file.h:40
file
Definition: kdev_t.h:19
goto_modelt
Definition: goto_model.h:24
mode.h
invalid_source_file_exceptiont
Thrown when we can't handle something in an input source file.
Definition: exception_utils.h:170
options.h
messaget::eom
static eomt eom
Definition: message.h:284
language_filest::generate_support_functions
bool generate_support_functions(symbol_tablet &symbol_table)
Definition: language_file.cpp:155
goto_modelt::validate
void validate(const validation_modet vm) const
Check that the goto model is well-formed.
Definition: goto_model.h:97
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:1931
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
rebuild_goto_start_function.h
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:60
system_exceptiont
Thrown when some external system fails unexpectedly.
Definition: exception_utils.h:60
languaget::parse
virtual bool parse(std::istream &instream, const std::string &path)=0
language.h
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
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:24
language_filet::language
std::unique_ptr< languaget > language
Definition: language_file.h:46
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
read_goto_binary.h
config
configt config
Definition: config.cpp:24
language_filest::final
bool final(symbol_table_baset &symbol_table)
Definition: language_file.cpp:170
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
validation_modet::EXCEPTION
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:234
unicode.h
languaget
Definition: language.h:39
config.h
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
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:32
goto_convert_functions.h
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:37
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:1232
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
rebuild_goto_start_function_baset
Definition: rebuild_goto_start_function.h:28
language_filest
Definition: language_file.h:61