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