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/base_type.h>
22 #include <util/config.h>
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 
37  const std::string &filename,
38  goto_modelt &dest,
39  message_handlert &message_handler)
40 {
41  return read_goto_binary(
42  filename, dest.symbol_table, dest.goto_functions, message_handler);
43 }
44 
50 read_goto_binary(const std::string &filename, message_handlert &message_handler)
51 {
52  goto_modelt dest;
53 
55  filename, dest.symbol_table, dest.goto_functions, message_handler))
56  {
57  return {};
58  }
59  else
60  return std::move(dest);
61 }
62 
70  const std::string &filename,
71  symbol_tablet &symbol_table,
72  goto_functionst &goto_functions,
73  message_handlert &message_handler)
74 {
75  #ifdef _MSC_VER
76  std::ifstream in(widen(filename), std::ios::binary);
77  #else
78  std::ifstream in(filename, std::ios::binary);
79  #endif
80 
81  if(!in)
82  {
83  messaget message(message_handler);
84  message.error() << "Failed to open `" << filename << "'"
85  << messaget::eom;
86  return true;
87  }
88 
89  char hdr[4];
90  hdr[0]=in.get();
91  hdr[1]=in.get();
92  hdr[2]=in.get();
93  hdr[3]=in.get();
94  in.seekg(0);
95 
96  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
97  {
98  return read_bin_goto_object(
99  in, filename, symbol_table, goto_functions, message_handler);
100  }
101  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
102  {
103  // ELF binary.
104  // This _may_ have a goto-cc section.
105  try
106  {
107  elf_readert elf_reader(in);
108 
109  for(unsigned i=0; i<elf_reader.number_of_sections; i++)
110  if(elf_reader.section_name(i)=="goto-cc")
111  {
112  in.seekg(elf_reader.section_offset(i));
113  return read_bin_goto_object(
114  in, filename, symbol_table, goto_functions, message_handler);
115  }
116 
117  // section not found
118  messaget(message_handler).error() <<
119  "failed to find goto-cc section in ELF binary" << messaget::eom;
120  }
121 
122  catch(const char *s)
123  {
124  messaget(message_handler).error() << s << messaget::eom;
125  }
126  }
127  else if(is_osx_fat_magic(hdr))
128  {
129  messaget message(message_handler);
130 
131  // Mach-O universal binary
132  // This _may_ have a goto binary as hppa7100LC architecture
133  osx_fat_readert osx_fat_reader(in);
134 
135  if(osx_fat_reader.has_gb())
136  {
137  temporary_filet tempname("tmp.goto-binary", ".gb");
138  if(osx_fat_reader.extract_gb(filename, tempname()))
139  {
140  message.error() << "failed to extract goto binary" << messaget::eom;
141  return true;
142  }
143 
144  std::ifstream temp_in(tempname(), std::ios::binary);
145  if(!temp_in)
146  message.error() << "failed to read temp binary" << messaget::eom;
147 
148  const bool read_err = read_bin_goto_object(
149  temp_in, filename, symbol_table, goto_functions, message_handler);
150  temp_in.close();
151 
152  return read_err;
153  }
154 
155  // architecture not found
156  message.error() << "failed to find goto binary in Mach-O file"
157  << messaget::eom;
158  }
159  else
160  {
161  messaget(message_handler).error() <<
162  "not a goto binary" << messaget::eom;
163  }
164 
165  return true;
166 }
167 
168 bool is_goto_binary(const std::string &filename)
169 {
170  #ifdef _MSC_VER
171  std::ifstream in(widen(filename), std::ios::binary);
172  #else
173  std::ifstream in(filename, std::ios::binary);
174  #endif
175 
176  if(!in)
177  return false;
178 
179  // We accept two forms:
180  // 1. goto binaries, marked with 0x7f GBF
181  // 2. ELF binaries, marked with 0x7f ELF
182 
183  char hdr[4];
184  hdr[0]=in.get();
185  hdr[1]=in.get();
186  hdr[2]=in.get();
187  hdr[3]=in.get();
188 
189  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
190  {
191  return true; // yes, this is a goto binary
192  }
193  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
194  {
195  // this _may_ have a goto-cc section
196  try
197  {
198  in.seekg(0);
199  elf_readert elf_reader(in);
200  if(elf_reader.has_section("goto-cc"))
201  return true;
202  }
203 
204  catch(...)
205  {
206  // ignore any errors
207  }
208  }
209  else if(is_osx_fat_magic(hdr))
210  {
211  // this _may_ have a goto binary as hppa7100LC architecture
212  try
213  {
214  in.seekg(0);
215  osx_fat_readert osx_fat_reader(in);
216  if(osx_fat_reader.has_gb())
217  return true;
218  }
219 
220  catch(...)
221  {
222  // ignore any errors
223  }
224  }
225 
226  return false;
227 }
228 
235  const std::string &file_name,
236  goto_modelt &dest,
237  message_handlert &message_handler)
238 {
239  messaget(message_handler).statistics() << "Reading: "
240  << file_name << messaget::eom;
241 
242  // we read into a temporary model
243  goto_modelt temp_model;
244 
245  if(read_goto_binary(
246  file_name,
247  temp_model,
248  message_handler))
249  return true;
250 
251  try
252  {
253  link_goto_model(dest, temp_model, message_handler);
254  }
255  catch(...)
256  {
257  return true;
258  }
259 
260  // reading successful, let's update config
262 
263  return false;
264 }
265 
273  const std::string &file_name,
274  symbol_tablet &dest_symbol_table,
275  goto_functionst &dest_functions,
276  message_handlert &message_handler)
277 {
278  goto_modelt goto_model;
279 
280  goto_model.symbol_table.swap(dest_symbol_table);
281  goto_model.goto_functions.swap(dest_functions);
282 
283  bool result=read_object_and_link(
284  file_name,
285  goto_model,
286  message_handler);
287 
288  goto_model.symbol_table.swap(dest_symbol_table);
289  goto_model.goto_functions.swap(dest_functions);
290 
291  return result;
292 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
tempfile.h
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
read_bin_goto_object.h
is_goto_binary
bool is_goto_binary(const std::string &filename)
Definition: read_goto_binary.cpp:168
read_goto_binary
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Read a goto binary from a file, but do not update config.
Definition: read_goto_binary.cpp:36
elf_reader.h
osx_fat_reader.h
elf_readert::has_section
bool has_section(const std::string &name) const
Definition: elf_reader.cpp:143
goto_model.h
goto_modelt
Definition: goto_model.h:24
messaget::eom
static eomt eom
Definition: message.h:284
rename_symbol.h
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:26
messaget::error
mstreamt & error() const
Definition: message.h:386
osx_fat_readert
Definition: osx_fat_reader.h:21
base_type.h
elf_readert
Definition: elf_reader.h:100
elf_readert::section_name
std::string section_name(std::size_t index) const
Definition: elf_reader.h:137
message_handlert
Definition: message.h:24
configt::set_from_symbol_table
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1171
widen
std::wstring widen(const char *s)
Definition: unicode.cpp:52
read_goto_binary.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
config
configt config
Definition: config.cpp:24
read_bin_goto_object
bool read_bin_goto_object(std::istream &in, const std::string &filename, symbol_tablet &symbol_table, goto_functionst &functions, message_handlert &message_handler)
reads a goto binary file back into a symbol and a function table
Definition: read_bin_goto_object.cpp:170
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
osx_fat_readert::extract_gb
bool extract_gb(const std::string &source, const std::string &dest) const
Definition: osx_fat_reader.cpp:85
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
symbol_tablet::swap
void swap(symbol_tablet &other)
Swap symbol maps between two symbol tables.
Definition: symbol_table.h:77
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
goto_functionst::swap
void swap(goto_functionst &other)
Definition: goto_functions.h:107
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
config.h
is_osx_fat_magic
bool is_osx_fat_magic(char hdr[4])
Definition: osx_fat_reader.cpp:24
message.h
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
temporary_filet
Definition: tempfile.h:23
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:406