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 
31  const std::string &filename,
32  goto_modelt &dest,
34 {
35  return read_goto_binary(
36  filename, dest.symbol_table, dest.goto_functions, message_handler);
37 }
38 
40  const std::string &filename,
41  symbol_tablet &symbol_table,
42  goto_functionst &goto_functions,
44 {
45  #ifdef _MSC_VER
46  std::ifstream in(widen(filename), std::ios::binary);
47  #else
48  std::ifstream in(filename, std::ios::binary);
49  #endif
50 
51  if(!in)
52  {
53  messaget message(message_handler);
54  message.error() << "Failed to open `" << filename << "'"
55  << messaget::eom;
56  return true;
57  }
58 
59  char hdr[4];
60  hdr[0]=in.get();
61  hdr[1]=in.get();
62  hdr[2]=in.get();
63  hdr[3]=in.get();
64  in.seekg(0);
65 
66  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
67  {
68  return read_bin_goto_object(
69  in, filename, symbol_table, goto_functions, message_handler);
70  }
71  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
72  {
73  // ELF binary.
74  // This _may_ have a goto-cc section.
75  try
76  {
77  elf_readert elf_reader(in);
78 
79  for(unsigned i=0; i<elf_reader.number_of_sections; i++)
80  if(elf_reader.section_name(i)=="goto-cc")
81  {
82  in.seekg(elf_reader.section_offset(i));
83  return read_bin_goto_object(
84  in, filename, symbol_table, goto_functions, message_handler);
85  }
86 
87  // section not found
89  "failed to find goto-cc section in ELF binary" << messaget::eom;
90  }
91 
92  catch(const char *s)
93  {
95  }
96  }
97  else if(is_osx_fat_magic(hdr))
98  {
99  messaget message(message_handler);
100 
101  // Mach-O universal binary
102  // This _may_ have a goto binary as hppa7100LC architecture
103  osx_fat_readert osx_fat_reader(in);
104 
105  if(osx_fat_reader.has_gb())
106  {
107  temporary_filet tempname("tmp.goto-binary", ".gb");
108  osx_fat_reader.extract_gb(filename, tempname());
109 
110  std::ifstream temp_in(tempname(), std::ios::binary);
111  if(!temp_in)
112  message.error() << "failed to read temp binary" << messaget::eom;
113 
114  const bool read_err = read_bin_goto_object(
115  temp_in, filename, symbol_table, goto_functions, message_handler);
116  temp_in.close();
117 
118  return read_err;
119  }
120 
121  // architecture not found
122  message.error() << "failed to find goto binary in Mach-O file"
123  << messaget::eom;
124  }
125  else
126  {
128  "not a goto binary" << messaget::eom;
129  }
130 
131  return true;
132 }
133 
134 bool is_goto_binary(const std::string &filename)
135 {
136  #ifdef _MSC_VER
137  std::ifstream in(widen(filename), std::ios::binary);
138  #else
139  std::ifstream in(filename, std::ios::binary);
140  #endif
141 
142  if(!in)
143  return false;
144 
145  // We accept two forms:
146  // 1. goto binaries, marked with 0x7f GBF
147  // 2. ELF binaries, marked with 0x7f ELF
148 
149  char hdr[4];
150  hdr[0]=in.get();
151  hdr[1]=in.get();
152  hdr[2]=in.get();
153  hdr[3]=in.get();
154 
155  if(hdr[0]==0x7f && hdr[1]=='G' && hdr[2]=='B' && hdr[3]=='F')
156  {
157  return true; // yes, this is a goto binary
158  }
159  else if(hdr[0]==0x7f && hdr[1]=='E' && hdr[2]=='L' && hdr[3]=='F')
160  {
161  // this _may_ have a goto-cc section
162  try
163  {
164  in.seekg(0);
165  elf_readert elf_reader(in);
166  if(elf_reader.has_section("goto-cc"))
167  return true;
168  }
169 
170  catch(...)
171  {
172  // ignore any errors
173  }
174  }
175  else if(is_osx_fat_magic(hdr))
176  {
177  // this _may_ have a goto binary as hppa7100LC architecture
178  try
179  {
180  in.seekg(0);
181  osx_fat_readert osx_fat_reader(in);
182  if(osx_fat_reader.has_gb())
183  return true;
184  }
185 
186  catch(...)
187  {
188  // ignore any errors
189  }
190  }
191 
192  return false;
193 }
194 
199  const std::string &file_name,
200  goto_modelt &dest,
202 {
203  messaget(message_handler).statistics() << "Reading: "
204  << file_name << messaget::eom;
205 
206  // we read into a temporary model
207  goto_modelt temp_model;
208 
209  if(read_goto_binary(
210  file_name,
211  temp_model,
213  return true;
214 
215  try
216  {
217  link_goto_model(dest, temp_model, message_handler);
218  }
219  catch(...)
220  {
221  return true;
222  }
223 
224  // reading successful, let's update config
226 
227  return false;
228 }
229 
234  const std::string &file_name,
235  symbol_tablet &dest_symbol_table,
236  goto_functionst &dest_functions,
238 {
239  goto_modelt goto_model;
240 
241  goto_model.symbol_table.swap(dest_symbol_table);
242  goto_model.goto_functions.swap(dest_functions);
243 
244  bool result=read_object_and_link(
245  file_name,
246  goto_model,
248 
249  goto_model.symbol_table.swap(dest_symbol_table);
250  goto_model.goto_functions.swap(dest_functions);
251 
252  return result;
253 }
bool has_section(const std::string &name) const
Definition: elf_reader.cpp:142
std::wstring widen(const char *s)
Definition: unicode.cpp:56
Read goto object files.
bool is_goto_binary(const std::string &filename)
Read Goto Programs.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
configt config
Definition: config.cpp:23
Read OS X Fat Binaries.
std::string section_name(std::size_t index) const
Definition: elf_reader.h:137
Read ELF.
bool read_goto_binary(const std::string &filename, goto_modelt &dest, message_handlert &message_handler)
Symbol Table + CFG.
bool extract_gb(const std::string &source, const std::string &dest) const
bool has_gb() const
std::streampos section_offset(std::size_t index) const
Definition: elf_reader.h:144
void swap(goto_functionst &other)
The symbol table.
Definition: symbol_table.h:19
mstreamt & error() const
Definition: message.h:302
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1116
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
bool is_osx_fat_magic(char hdr[4])
std::size_t number_of_sections
Definition: elf_reader.h:135
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
void swap(symbol_tablet &other)
Definition: symbol_table.h:71
Base Type Computation.
bool read_object_and_link(const std::string &file_name, goto_modelt &dest, message_handlert &message_handler)
reads an object file
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
mstreamt & statistics() const
Definition: message.h:322