cprover
read_goto_binary.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Read Goto Programs
4 
5 Author:
6 
7 \*******************************************************************/
8 
11 
12 #include "read_goto_binary.h"
13 
14 #include <fstream>
15 #include <unordered_set>
16 
17 #include <util/message.h>
18 #include <util/unicode.h>
19 #include <util/tempfile.h>
20 #include <util/rename_symbol.h>
21 #include <util/config.h>
22 
23 #include "goto_model.h"
24 #include "link_goto_model.h"
25 #include "read_bin_goto_object.h"
26 #include "elf_reader.h"
27 #include "osx_fat_reader.h"
28 
29 static bool read_goto_binary(
30  const std::string &filename,
31  symbol_tablet &,
34 
40 read_goto_binary(const std::string &filename, message_handlert &message_handler)
41 {
42  goto_modelt dest;
43 
45  filename, dest.symbol_table, dest.goto_functions, message_handler))
46  {
47  return {};
48  }
49  else
50  return std::move(dest);
51 }
52 
59 static bool read_goto_binary(
60  const std::string &filename,
61  symbol_tablet &symbol_table,
62  goto_functionst &goto_functions,
63  message_handlert &message_handler)
64 {
65  #ifdef _MSC_VER
66  std::ifstream in(widen(filename), std::ios::binary);
67  #else
68  std::ifstream in(filename, std::ios::binary);
69  #endif
70 
71  messaget message(message_handler);
72 
73  if(!in)
74  {
75  message.error() << "Failed to open '" << filename << "'" << messaget::eom;
76  return true;
77  }
78 
79  char hdr[8];
80  in.read(hdr, 8);
81  if(!in)
82  {
83  message.error() << "Failed to read header from '" << filename << "'"
84  << messaget::eom;
85  return true;
86  }
87 
88  in.seekg(0);
89 
90  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
91  {
92  return read_bin_goto_object(
93  in, filename, symbol_table, goto_functions, message_handler);
94  }
95  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
96  {
97  // ELF binary.
98  // This _may_ have a goto-cc section.
99  try
100  {
101  elf_readert elf_reader(in);
102 
103  for(unsigned i=0; i<elf_reader.number_of_sections; i++)
104  if(elf_reader.section_name(i)=="goto-cc")
105  {
106  in.seekg(elf_reader.section_offset(i));
107  return read_bin_goto_object(
108  in, filename, symbol_table, goto_functions, message_handler);
109  }
110 
111  // section not found
112  messaget(message_handler).error() <<
113  "failed to find goto-cc section in ELF binary" << messaget::eom;
114  }
115 
116  catch(const char *s)
117  {
118  messaget(message_handler).error() << s << messaget::eom;
119  }
120  }
121  else if(is_osx_fat_header(hdr))
122  {
123  messaget message(message_handler);
124 
125  // Mach-O universal binary
126  // This _may_ have a goto binary as hppa7100LC architecture
127  osx_fat_readert osx_fat_reader(in, message_handler);
128 
129  if(osx_fat_reader.has_gb())
130  {
131  temporary_filet tempname("tmp.goto-binary", ".gb");
132  if(osx_fat_reader.extract_gb(filename, tempname()))
133  {
134  message.error() << "failed to extract goto binary" << messaget::eom;
135  return true;
136  }
137 
138  std::ifstream temp_in(tempname(), std::ios::binary);
139  if(!temp_in)
140  message.error() << "failed to read temp binary" << messaget::eom;
141 
142  const bool read_err = read_bin_goto_object(
143  temp_in, filename, symbol_table, goto_functions, message_handler);
144  temp_in.close();
145 
146  return read_err;
147  }
148 
149  // architecture not found
150  message.error() << "failed to find goto binary in Mach-O file"
151  << messaget::eom;
152  }
153  else if(is_osx_mach_object(hdr))
154  {
155  messaget message(message_handler);
156 
157  // Mach-O object file, may contain a goto-cc section
158  try
159  {
160  osx_mach_o_readert mach_o_reader(in, message_handler);
161 
162  osx_mach_o_readert::sectionst::const_iterator entry =
163  mach_o_reader.sections.find("goto-cc");
164  if(entry != mach_o_reader.sections.end())
165  {
166  in.seekg(entry->second.offset);
167  return read_bin_goto_object(
168  in, filename, symbol_table, goto_functions, message_handler);
169  }
170 
171  // section not found
172  messaget(message_handler).error()
173  << "failed to find goto-cc section in Mach-O binary" << messaget::eom;
174  }
175 
176  catch(const deserialization_exceptiont &e)
177  {
178  messaget(message_handler).error() << e.what() << messaget::eom;
179  }
180  }
181  else
182  {
183  messaget(message_handler).error() <<
184  "not a goto binary" << messaget::eom;
185  }
186 
187  return true;
188 }
189 
191  const std::string &filename,
192  message_handlert &message_handler)
193 {
194  #ifdef _MSC_VER
195  std::ifstream in(widen(filename), std::ios::binary);
196  #else
197  std::ifstream in(filename, std::ios::binary);
198  #endif
199 
200  if(!in)
201  return false;
202 
203  // We accept two forms:
204  // 1. goto binaries, marked with 0x7f GBF
205  // 2. ELF binaries, marked with 0x7f ELF
206 
207  char hdr[8];
208  in.read(hdr, 8);
209  if(!in)
210  return false;
211 
212  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
213  {
214  return true; // yes, this is a goto binary
215  }
216  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
217  {
218  // this _may_ have a goto-cc section
219  try
220  {
221  in.seekg(0);
222  elf_readert elf_reader(in);
223  if(elf_reader.has_section("goto-cc"))
224  return true;
225  }
226 
227  catch(...)
228  {
229  // ignore any errors
230  }
231  }
232  else if(is_osx_fat_header(hdr))
233  {
234  // this _may_ have a goto binary as hppa7100LC architecture
235  try
236  {
237  in.seekg(0);
238  osx_fat_readert osx_fat_reader(in, message_handler);
239  if(osx_fat_reader.has_gb())
240  return true;
241  }
242 
243  catch(...)
244  {
245  // ignore any errors
246  }
247  }
248  else if(is_osx_mach_object(hdr))
249  {
250  // this _may_ have a goto-cc section
251  try
252  {
253  in.seekg(0);
254  osx_mach_o_readert mach_o_reader(in, message_handler);
255  if(mach_o_reader.has_section("goto-cc"))
256  return true;
257  }
258 
259  catch(...)
260  {
261  // ignore any errors
262  }
263  }
264 
265  return false;
266 }
267 
274  const std::string &file_name,
275  goto_modelt &dest,
276  message_handlert &message_handler)
277 {
278  messaget(message_handler).statistics() << "Reading: "
279  << file_name << messaget::eom;
280 
281  // we read into a temporary model
282  auto temp_model = read_goto_binary(file_name, message_handler);
283  if(!temp_model.has_value())
284  return true;
285 
286  try
287  {
288  link_goto_model(dest, *temp_model, message_handler);
289  }
290  catch(...)
291  {
292  return true;
293  }
294 
295  // reading successful, let's update config
297 
298  return false;
299 }
300 
308  const std::string &file_name,
309  symbol_tablet &dest_symbol_table,
310  goto_functionst &dest_functions,
311  message_handlert &message_handler)
312 {
313  goto_modelt goto_model;
314 
315  goto_model.symbol_table.swap(dest_symbol_table);
316  goto_model.goto_functions.swap(dest_functions);
317 
318  bool result=read_object_and_link(
319  file_name,
320  goto_model,
321  message_handler);
322 
323  goto_model.symbol_table.swap(dest_symbol_table);
324  goto_model.goto_functions.swap(dest_functions);
325 
326  return result;
327 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
tempfile.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
osx_mach_o_readert
Definition: osx_fat_reader.h:43
read_bin_goto_object.h
Read goto object files.
read_bin_goto_object
static bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
Definition: read_bin_goto_object.cpp:27
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:73
elf_reader.h
Read ELF.
osx_fat_reader.h
Read OS X Fat Binaries.
elf_readert::has_section
bool has_section(const std::string &name) const
Definition: elf_reader.cpp:143
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
messaget::eom
static eomt eom
Definition: message.h:297
rename_symbol.h
is_osx_mach_object
bool is_osx_mach_object(char hdr[4])
Definition: osx_fat_reader.cpp:135
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
elf_readert::number_of_sections
std::size_t number_of_sections
Definition: elf_reader.h:135
osx_fat_readert::has_gb
bool has_gb() const
Definition: osx_fat_reader.h:29
messaget::error
mstreamt & error() const
Definition: message.h:399
osx_fat_readert
Definition: osx_fat_reader.h:25
elf_readert
Definition: elf_reader.h:101
elf_readert::section_name
std::string section_name(std::size_t index) const
Definition: elf_reader.h:137
osx_mach_o_readert::sections
sectionst sections
Definition: osx_fat_reader.h:60
message_handlert
Definition: message.h:28
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1205
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:50
read_goto_binary.h
Read Goto Programs.
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
config
configt config
Definition: config.cpp:24
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
osx_fat_readert::extract_gb
bool extract_gb(const std::string &source, const std::string &dest) const
Definition: osx_fat_reader.cpp:123
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
symbol_tablet::swap
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
Definition: symbol_table.h:80
osx_mach_o_readert::has_section
bool has_section(const std::string &name) const
Definition: osx_fat_reader.h:62
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
goto_functionst::swap
void swap(goto_functionst &other)
Definition: goto_functions.h:96
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
is_goto_binary
bool is_goto_binary(const std::string &filename, message_handlert &message_handler)
Definition: read_goto_binary.cpp:190
config.h
read_goto_binary
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
Definition: read_goto_binary.cpp:59
is_osx_fat_header
bool is_osx_fat_header(char header_bytes[8])
Definition: osx_fat_reader.cpp:58
message.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
temporary_filet
Definition: tempfile.h:24
elf_readert::section_offset
std::streampos section_offset(std::size_t index) const
Definition: elf_reader.h:144
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
deserialization_exceptiont::what
std::string what() const override
A human readable description of what went wrong.
Definition: exception_utils.cpp:52