cprover
Loading...
Searching...
No Matches
read_goto_binary.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Read Goto Programs
4
5Author:
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"
28#include "elf_reader.h"
29#include "osx_fat_reader.h"
30
31static bool read_goto_binary(
32 const std::string &filename,
36
42read_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
61static 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 << "'"
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 {
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));
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);
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}
void set_from_symbol_table(const symbol_tablet &)
Definition: config.cpp:1254
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
std::string what() const override
A human readable description of what went wrong.
std::size_t number_of_sections
Definition: elf_reader.h:135
bool has_section(const std::string &name) const
Definition: elf_reader.cpp:143
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:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
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
configt config
Definition: config.cpp:25
Read ELF.
Symbol Table + CFG.
nonstd::optional< T > optionalt
Definition: optional.h:35
bool is_osx_fat_header(char header_bytes[8])
bool is_osx_mach_object(char hdr[4])
Read OS X Fat Binaries.
static bool read_bin_goto_object(std::istream &in, symbol_tablet &symbol_table, goto_functionst &functions, irep_serializationt &irepconverter)
read goto binary format
Read goto object files.
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
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.
std::wstring widen(const char *s)
Definition: unicode.cpp:49