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