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/language.h>
18 #include <util/config.h>
19 #include <util/unicode.h>
20 
21 #include <langapi/mode.h>
22 #include <langapi/language_ui.h>
23 
24 #include "goto_convert_functions.h"
25 #include "read_goto_binary.h"
26 
28  goto_modelt &goto_model,
29  const cmdlinet &cmdline,
30  message_handlert &message_handler)
31 {
32  messaget msg(message_handler);
33  const std::vector<std::string> &files=cmdline.args;
34  if(files.empty())
35  {
36  msg.error() << "Please provide a program" << messaget::eom;
37  return true;
38  }
39 
40  try
41  {
42  std::vector<std::string> binaries, sources;
43  binaries.reserve(files.size());
44  sources.reserve(files.size());
45 
46  for(const auto &file : files)
47  {
48  if(is_goto_binary(file))
49  binaries.push_back(file);
50  else
51  sources.push_back(file);
52  }
53 
54  if(!sources.empty())
55  {
56  language_filest language_files;
57 
58  language_files.set_message_handler(message_handler);
59 
60  for(const auto &filename : sources)
61  {
62  #ifdef _MSC_VER
63  std::ifstream infile(widen(filename));
64  #else
65  std::ifstream infile(filename);
66  #endif
67 
68  if(!infile)
69  {
70  msg.error() << "failed to open input file `" << filename
71  << '\'' << messaget::eom;
72  return true;
73  }
74 
75  std::pair<language_filest::file_mapt::iterator, bool>
76  result=language_files.file_map.insert(
77  std::pair<std::string, language_filet>(filename, language_filet()));
78 
79  language_filet &lf=result.first->second;
80 
81  lf.filename=filename;
83 
84  if(lf.language==nullptr)
85  {
86  source_locationt location;
87  location.set_file(filename);
88  msg.error().source_location=location;
89  msg.error() << "failed to figure out type of file" << messaget::eom;
90  return true;
91  }
92 
93  languaget &language=*lf.language;
94  language.set_message_handler(message_handler);
95  language.get_language_options(cmdline);
96 
97  msg.status() << "Parsing " << filename << messaget::eom;
98 
99  if(language.parse(infile, filename))
100  {
101  msg.error() << "PARSING ERROR" << messaget::eom;
102  return true;
103  }
104 
105  lf.get_modules();
106  }
107 
108  msg.status() << "Converting" << messaget::eom;
109 
110  if(language_files.typecheck(goto_model.symbol_table))
111  {
112  msg.error() << "CONVERSION ERROR" << messaget::eom;
113  return true;
114  }
115 
116  if(binaries.empty())
117  {
118  if(language_files.final(goto_model.symbol_table))
119  {
120  msg.error() << "CONVERSION ERROR" << messaget::eom;
121  return true;
122  }
123  }
124  }
125 
126  for(const auto &file : binaries)
127  {
128  msg.status() << "Reading GOTO program from file" << messaget::eom;
129 
130  if(read_object_and_link(file, goto_model, message_handler))
131  return true;
132  }
133 
134  if(!binaries.empty())
136 
137  msg.status() << "Generating GOTO Program" << messaget::eom;
138 
139  goto_convert(
140  goto_model.symbol_table,
141  goto_model.goto_functions,
142  message_handler);
143  }
144  catch(const char *e)
145  {
146  msg.error() << e << messaget::eom;
147  return true;
148  }
149  catch(const std::string e)
150  {
151  msg.error() << e << messaget::eom;
152  return true;
153  }
154  catch(int)
155  {
156  return true;
157  }
158  catch(std::bad_alloc)
159  {
160  msg.error() << "Out of memory" << messaget::eom;
161  return true;
162  }
163 
164  return false; // no error
165 }
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
std::wstring widen(const char *s)
Definition: unicode.cpp:56
languaget * language
Definition: language_file.h:41
mstreamt & status()
Definition: message.h:238
virtual void get_language_options(const cmdlinet &)
Definition: language.h:31
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
symbol_tablet symbol_table
Definition: goto_model.h:25
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
argst args
Definition: cmdline.h:35
Initialize a Goto Program.
source_locationt source_location
Definition: message.h:175
void set_file(const irep_idt &file)
Abstract interface to support a programming language.
bool typecheck(symbol_tablet &symbol_table)
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
bool read_object_and_link(const std::string &file_name, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads an object file
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1091
bool final(symbol_tablet &symbol_table)
Goto Programs with Functions.
languaget * get_language_from_filename(const std::string &filename)
Definition: mode.cpp:51
file_mapt file_map
Definition: language_file.h:63
std::string filename
Definition: language_file.h:42
mstreamt & error()
Definition: message.h:223
virtual bool parse(std::istream &instream, const std::string &path)=0
bool initialize_goto_model(goto_modelt &goto_model, const cmdlinet &cmdline, message_handlert &message_handler)
goto_functionst goto_functions
Definition: goto_model.h:26
Definition: kdev_t.h:19