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