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 #if defined(__linux__) || \
15  defined(__FreeBSD_kernel__) || \
16  defined(__GNU__) || \
17  defined(__unix__) || \
18  defined(__CYGWIN__) || \
19  defined(__MACH__)
20 #include <unistd.h>
21 #endif
22 
23 #include <fstream>
24 #include <unordered_set>
25 
26 #include <util/message.h>
27 #include <util/unicode.h>
28 #include <util/tempfile.h>
29 #include <util/rename_symbol.h>
30 #include <util/base_type.h>
31 
32 #include <langapi/language_ui.h>
33 
34 #include <linking/linking_class.h>
35 
36 #include "goto_model.h"
37 #include "read_bin_goto_object.h"
38 #include "elf_reader.h"
39 #include "osx_fat_reader.h"
40 
42  const std::string &filename,
43  goto_modelt &dest,
44  message_handlert &message_handler)
45 {
46  return read_goto_binary(
47  filename, dest.symbol_table, dest.goto_functions, message_handler);
48 }
49 
51  const std::string &filename,
52  symbol_tablet &symbol_table,
53  goto_functionst &goto_functions,
54  message_handlert &message_handler)
55 {
56  #ifdef _MSC_VER
57  std::ifstream in(widen(filename), std::ios::binary);
58  #else
59  std::ifstream in(filename, std::ios::binary);
60  #endif
61 
62  if(!in)
63  {
64  messaget message(message_handler);
65  message.error() << "Failed to open `" << filename << "'"
66  << messaget::eom;
67  return true;
68  }
69 
70  char hdr[4];
71  hdr[0]=in.get();
72  hdr[1]=in.get();
73  hdr[2]=in.get();
74  hdr[3]=in.get();
75  in.seekg(0);
76 
77  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
78  {
79  return read_bin_goto_object(
80  in, filename, symbol_table, goto_functions, message_handler);
81  }
82  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
83  {
84  // ELF binary.
85  // This _may_ have a goto-cc section.
86  try
87  {
88  elf_readert elf_reader(in);
89 
90  for(unsigned i=0; i<elf_reader.number_of_sections; i++)
91  if(elf_reader.section_name(i)=="goto-cc")
92  {
93  in.seekg(elf_reader.section_offset(i));
94  return read_bin_goto_object(
95  in, filename, symbol_table, goto_functions, message_handler);
96  }
97 
98  // section not found
99  messaget(message_handler).error() <<
100  "failed to find goto-cc section in ELF binary" << messaget::eom;
101  }
102 
103  catch(const char *s)
104  {
105  messaget(message_handler).error() << s << messaget::eom;
106  }
107  }
108  else if(is_osx_fat_magic(hdr))
109  {
110  std::string tempname;
111  // Mach-O universal binary
112  // This _may_ have a goto binary as hppa7100LC architecture
113  try
114  {
115  osx_fat_readert osx_fat_reader(in);
116 
117  if(osx_fat_reader.has_gb())
118  {
119  tempname=get_temporary_file("tmp.goto-binary", ".gb");
120  osx_fat_reader.extract_gb(filename, tempname);
121 
122  std::ifstream temp_in(tempname, std::ios::binary);
123  if(!temp_in)
124  messaget(message_handler).error() << "failed to read temp binary"
125  << messaget::eom;
126  const bool read_err=read_bin_goto_object(
127  temp_in, filename, symbol_table, goto_functions, message_handler);
128  temp_in.close();
129 
130  unlink(tempname.c_str());
131  return read_err;
132  }
133 
134  // architecture not found
135  messaget(message_handler).error() <<
136  "failed to find goto binary in Mach-O file" << messaget::eom;
137  }
138 
139  catch(const char *s)
140  {
141  if(!tempname.empty())
142  unlink(tempname.c_str());
143  messaget(message_handler).error() << s << messaget::eom;
144  }
145  }
146  else
147  {
148  messaget(message_handler).error() <<
149  "not a goto binary" << messaget::eom;
150  }
151 
152  return true;
153 }
154 
155 bool is_goto_binary(const std::string &filename)
156 {
157  #ifdef _MSC_VER
158  std::ifstream in(widen(filename), std::ios::binary);
159  #else
160  std::ifstream in(filename, std::ios::binary);
161  #endif
162 
163  if(!in)
164  return false;
165 
166  // We accept two forms:
167  // 1. goto binaries, marked with 0x7f GBF
168  // 2. ELF binaries, marked with 0x7f ELF
169 
170  char hdr[4];
171  hdr[0]=in.get();
172  hdr[1]=in.get();
173  hdr[2]=in.get();
174  hdr[3]=in.get();
175 
176  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
177  {
178  return true; // yes, this is a goto binary
179  }
180  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
181  {
182  // this _may_ have a goto-cc section
183  try
184  {
185  in.seekg(0);
186  elf_readert elf_reader(in);
187  if(elf_reader.has_section("goto-cc"))
188  return true;
189  }
190 
191  catch(...)
192  {
193  // ignore any errors
194  }
195  }
196  else if(is_osx_fat_magic(hdr))
197  {
198  // this _may_ have a goto binary as hppa7100LC architecture
199  try
200  {
201  in.seekg(0);
202  osx_fat_readert osx_fat_reader(in);
203  if(osx_fat_reader.has_gb())
204  return true;
205  }
206 
207  catch(...)
208  {
209  // ignore any errors
210  }
211  }
212 
213  return false;
214 }
215 
218  const rename_symbolt &rename_symbol)
219 {
220  goto_programt &program=function.body;
221  rename_symbol(function.type);
222 
224  {
225  rename_symbol(iit->code);
226  rename_symbol(iit->guard);
227  }
228 }
229 
230 static bool link_functions(
231  symbol_tablet &dest_symbol_table,
232  goto_functionst &dest_functions,
233  const symbol_tablet &src_symbol_table,
234  goto_functionst &src_functions,
235  const rename_symbolt &rename_symbol,
236  const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols,
237  const replace_symbolt &object_type_updates)
238 {
239  namespacet ns(dest_symbol_table);
240  namespacet src_ns(src_symbol_table);
241 
242  // merge functions
243  Forall_goto_functions(src_it, src_functions)
244  {
245  // the function might have been renamed
246  rename_symbolt::expr_mapt::const_iterator e_it=
247  rename_symbol.expr_map.find(src_it->first);
248 
249  irep_idt final_id=src_it->first;
250 
251  if(e_it!=rename_symbol.expr_map.end())
252  final_id=e_it->second;
253 
254  // already there?
255  goto_functionst::function_mapt::iterator dest_f_it=
256  dest_functions.function_map.find(final_id);
257 
258  if(dest_f_it==dest_functions.function_map.end()) // not there yet
259  {
260  rename_symbols_in_function(src_it->second, rename_symbol);
261 
262  goto_functionst::goto_functiont &in_dest_symbol_table=
263  dest_functions.function_map[final_id];
264 
265  in_dest_symbol_table.body.swap(src_it->second.body);
266  in_dest_symbol_table.type=src_it->second.type;
267  }
268  else // collision!
269  {
270  goto_functionst::goto_functiont &in_dest_symbol_table=
271  dest_functions.function_map[final_id];
272 
273  goto_functionst::goto_functiont &src_func=src_it->second;
274 
275  if(in_dest_symbol_table.body.instructions.empty() ||
276  weak_symbols.find(final_id)!=weak_symbols.end())
277  {
278  // the one with body wins!
279  rename_symbols_in_function(src_func, rename_symbol);
280 
281  in_dest_symbol_table.body.swap(src_func.body);
282  in_dest_symbol_table.type=src_func.type;
283  }
284  else if(src_func.body.instructions.empty() ||
285  src_ns.lookup(src_it->first).is_weak)
286  {
287  // just keep the old one in dest
288  }
289  else if(in_dest_symbol_table.type.get_bool(ID_C_inlined))
290  {
291  // ok, we silently ignore
292  }
293  else
294  {
295  // the linking code will have ensured that types match
296  rename_symbol(src_func.type);
297  assert(base_type_eq(in_dest_symbol_table.type, src_func.type, ns));
298  }
299  }
300  }
301 
302  // apply macros
303  rename_symbolt macro_application;
304 
305  forall_symbols(it, dest_symbol_table.symbols)
306  if(it->second.is_macro && !it->second.is_type)
307  {
308  const symbolt &symbol=it->second;
309 
310  assert(symbol.value.id()==ID_symbol);
311  const irep_idt &id=to_symbol_expr(symbol.value).get_identifier();
312 
313  #if 0
314  if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
315  {
316  std::cerr << symbol << '\n';
317  std::cerr << ns.lookup(id) << '\n';
318  }
319  assert(base_type_eq(symbol.type, ns.lookup(id).type, ns));
320  #endif
321 
322  macro_application.insert_expr(symbol.name, id);
323  }
324 
325  if(!macro_application.expr_map.empty())
326  Forall_goto_functions(dest_it, dest_functions)
327  rename_symbols_in_function(dest_it->second, macro_application);
328 
329  if(!object_type_updates.expr_map.empty())
330  {
331  Forall_goto_functions(dest_it, dest_functions)
332  Forall_goto_program_instructions(iit, dest_it->second.body)
333  {
334  object_type_updates(iit->code);
335  object_type_updates(iit->guard);
336  }
337  }
338 
339  return false;
340 }
341 
346  const std::string &file_name,
347  symbol_tablet &symbol_table,
348  goto_functionst &functions,
349  message_handlert &message_handler)
350 {
351  messaget(message_handler).statistics() << "Reading: "
352  << file_name << messaget::eom;
353 
354  // we read into a temporary model
355  goto_modelt temp_model;
356 
357  if(read_goto_binary(
358  file_name,
359  temp_model,
360  message_handler))
361  return true;
362 
363  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
364  id_sett weak_symbols;
365  forall_symbols(it, symbol_table.symbols)
366  if(it->second.is_weak)
367  weak_symbols.insert(it->first);
368 
369  linkingt linking(symbol_table,
370  temp_model.symbol_table,
371  message_handler);
372 
373  if(linking.typecheck_main())
374  return true;
375 
376  if(link_functions(
377  symbol_table,
378  functions,
379  temp_model.symbol_table,
380  temp_model.goto_functions,
381  linking.rename_symbol,
382  weak_symbols,
383  linking.object_type_updates))
384  return true;
385 
386  return false;
387 }
388 
393  const std::string &file_name,
394  goto_modelt &goto_model,
395  message_handlert &message_handler)
396 {
397  return read_object_and_link(
398  file_name,
399  goto_model.symbol_table,
400  goto_model.goto_functions,
401  message_handler);
402 }
bool has_section(const std::string &name) const
Definition: elf_reader.cpp:142
irep_idt name
The unique identifier.
Definition: symbol.h:46
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
std::wstring widen(const char *s)
Definition: unicode.cpp:56
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:270
Read goto object files.
const irep_idt & get_identifier() const
Definition: std_expr.h:120
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
std::string section_name(unsigned index) const
Definition: elf_reader.h:137
exprt value
Initial value of symbol.
Definition: symbol.h:40
bool linking(symbol_tablet &dest_symbol_table, symbol_tablet &new_symbol_table, message_handlert &message_handler)
Definition: linking.cpp:1336
symbol_tablet symbol_table
Definition: goto_model.h:25
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
expr_mapt expr_map
Definition: rename_symbol.h:59
static void rename_symbols_in_function(goto_functionst::goto_functiont &function, const rename_symbolt &rename_symbol)
Read OS X Fat Binaries.
Read ELF.
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
const irep_idt & id() const
Definition: irep.h:189
Symbol Table + CFG.
symbolst symbols
Definition: symbol_table.h:57
bool extract_gb(const std::string &source, const std::string &dest) const
bool has_gb() const
unsigned number_of_sections
Definition: elf_reader.h:135
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
static bool link_functions(symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, const symbol_tablet &src_symbol_table, goto_functionst &src_functions, const rename_symbolt &rename_symbol, const std::unordered_set< irep_idt, irep_id_hash > &weak_symbols, const replace_symbolt &object_type_updates)
goto_function_templatet< goto_programt > goto_functiont
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
mstreamt & statistics()
Definition: message.h:243
replace_symbolt object_type_updates
Definition: linking_class.h:38
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
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
bool is_osx_fat_magic(char hdr[4])
typet type
Type of symbol.
Definition: symbol.h:37
void insert_expr(const irep_idt &old_id, const irep_idt &new_id)
Definition: rename_symbol.h:31
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
Definition: tempfile.cpp:87
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
ANSI-C Linking.
#define Forall_goto_functions(it, functions)
rename_symbolt rename_symbol
Definition: linking_class.h:37
mstreamt & error()
Definition: message.h:223
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Base Type Computation.
expr_mapt expr_map
std::streampos section_offset(unsigned index) const
Definition: elf_reader.h:144
virtual bool typecheck_main()
Definition: typecheck.cpp:12
goto_functionst goto_functions
Definition: goto_model.h:26