CBMC
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 <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"
25
26#include <fstream>
27
28static bool read_goto_binary(
29 const std::string &filename,
33
38std::optional<goto_modelt>
39read_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
58static 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 << "'"
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 {
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 {
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));
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);
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);
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
264static 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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
void set_from_symbol_table(const symbol_table_baset &)
Definition config.cpp:1363
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.
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:154
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
mstreamt & status() const
Definition message.h:406
std::unordered_map< irep_idt, exprt > expr_mapt
The symbol table.
Read ELF.
Symbol Table + CFG.
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 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.
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
Read Goto Programs.
#define widen_if_needed(s)
Definition unicode.h:28