Skip to content

Commit 1c8bca7

Browse files
tautschnigtautschnig
committed
Read goto-cc section from Mach-O object files
A basic Mach-O header parser, only functional on OS X.
1 parent 85bc89d commit 1c8bca7

File tree

4 files changed

+295
-0
lines changed

4 files changed

+295
-0
lines changed

‎src/goto-programs/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
analyses # dubious - concerns call_graph and does_remove_const
2+
architecture # system
23
goto-programs
34
goto-symex # dubious - spurious inclusion of symex_target_equation in graphml_witness
45
json

‎src/goto-programs/osx_fat_reader.cpp

Lines changed: 213 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,10 @@ Module: Read Mach-O
1616
#include <util/invariant.h>
1717

1818
#ifdef __APPLE__
19+
#include <architecture/byte_order.h>
1920
#include <mach-o/fat.h>
21+
#include <mach-o/loader.h>
22+
#include <mach-o/swap.h>
2023
#endif
2124

2225
#include <util/run.h>
@@ -92,3 +95,213 @@ bool osx_fat_readert::extract_gb(
9295
"lipo", {"lipo", "-thin", "hppa7100LC", "-output", dest, source}) !=
9396
0;
9497
}
98+
99+
// guided by https://lowlevelbits.org/parsing-mach-o-files/
100+
bool is_osx_mach_object(char hdr[4])
101+
{
102+
#ifdef __APPLE__
103+
uint32_t *magic = reinterpret_cast<uint32_t *>(hdr);
104+
105+
switch(*magic)
106+
{
107+
case MH_MAGIC:
108+
case MH_CIGAM:
109+
case MH_MAGIC_64:
110+
case MH_CIGAM_64:
111+
return true;
112+
}
113+
#else
114+
(void)hdr; // unused parameter
115+
#endif
116+
117+
return false;
118+
}
119+
120+
void osx_mach_o_readert::process_sections_32(uint32_t nsects, bool need_swap)
121+
{
122+
#ifdef __APPLE__
123+
for(uint32_t i = 0; i < nsects; ++i)
124+
{
125+
// NOLINTNEXTLINE(readability/identifiers)
126+
struct section s;
127+
in.read(reinterpret_cast<char *>(&s), sizeof(s));
128+
129+
if(!in)
130+
throw deserialization_exceptiont("failed to read Mach-O section");
131+
132+
if(need_swap)
133+
swap_section(&s, 1, NXHostByteOrder());
134+
135+
sections.emplace(s.sectname, sectiont(s.sectname, s.offset, s.size));
136+
}
137+
#else
138+
// unused parameters
139+
(void)nsects;
140+
(void)need_swap;
141+
#endif
142+
}
143+
144+
void osx_mach_o_readert::process_sections_64(uint32_t nsects, bool need_swap)
145+
{
146+
#ifdef __APPLE__
147+
for(uint32_t i = 0; i < nsects; ++i)
148+
{
149+
// NOLINTNEXTLINE(readability/identifiers)
150+
struct section_64 s;
151+
in.read(reinterpret_cast<char *>(&s), sizeof(s));
152+
153+
if(!in)
154+
throw deserialization_exceptiont("failed to read 64-bit Mach-O section");
155+
156+
if(need_swap)
157+
swap_section_64(&s, 1, NXHostByteOrder());
158+
159+
sections.emplace(s.sectname, sectiont(s.sectname, s.offset, s.size));
160+
}
161+
#else
162+
// unused parameters
163+
(void)nsects;
164+
(void)need_swap;
165+
#endif
166+
}
167+
168+
void osx_mach_o_readert::process_commands(
169+
uint32_t ncmds,
170+
std::size_t offset,
171+
bool need_swap)
172+
{
173+
#ifdef __APPLE__
174+
for(uint32_t i = 0; i < ncmds; ++i)
175+
{
176+
in.seekg(offset);
177+
178+
// NOLINTNEXTLINE(readability/identifiers)
179+
struct load_command lc;
180+
in.read(reinterpret_cast<char *>(&lc), sizeof(lc));
181+
182+
if(!in)
183+
throw deserialization_exceptiont("failed to read Mach-O command");
184+
185+
if(need_swap)
186+
swap_load_command(&lc, NXHostByteOrder());
187+
188+
// we may need to re-read the command once we have figured out its type; in
189+
// particular, segment commands contain additional information that we have
190+
// now just read a prefix of
191+
in.seekg(offset);
192+
193+
switch(lc.cmd)
194+
{
195+
case LC_SEGMENT:
196+
{
197+
// NOLINTNEXTLINE(readability/identifiers)
198+
struct segment_command seg;
199+
in.read(reinterpret_cast<char *>(&seg), sizeof(seg));
200+
201+
if(!in)
202+
throw deserialization_exceptiont("failed to read Mach-O segment");
203+
204+
if(need_swap)
205+
swap_segment_command(&seg, NXHostByteOrder());
206+
207+
process_sections_32(seg.nsects, need_swap);
208+
break;
209+
}
210+
case LC_SEGMENT_64:
211+
{
212+
// NOLINTNEXTLINE(readability/identifiers)
213+
struct segment_command_64 seg;
214+
in.read(reinterpret_cast<char *>(&seg), sizeof(seg));
215+
216+
if(!in)
217+
throw deserialization_exceptiont("failed to read Mach-O segment");
218+
219+
if(need_swap)
220+
swap_segment_command_64(&seg, NXHostByteOrder());
221+
222+
process_sections_64(seg.nsects, need_swap);
223+
break;
224+
}
225+
default:
226+
break;
227+
}
228+
229+
offset += lc.cmdsize;
230+
}
231+
#else
232+
// unused parameters
233+
(void)ncmds;
234+
(void)offset;
235+
(void)need_swap;
236+
#endif
237+
}
238+
239+
osx_mach_o_readert::osx_mach_o_readert(std::istream &_in) : in(_in)
240+
{
241+
// read magic
242+
uint32_t magic;
243+
in.read(reinterpret_cast<char *>(&magic), sizeof(magic));
244+
245+
if(!in)
246+
throw deserialization_exceptiont("failed to read Mach-O magic");
247+
248+
#ifdef __APPLE__
249+
bool is_64 = false, need_swap = false;
250+
switch(magic)
251+
{
252+
case MH_CIGAM:
253+
need_swap = true;
254+
break;
255+
case MH_MAGIC:
256+
break;
257+
case MH_CIGAM_64:
258+
need_swap = true;
259+
is_64 = true;
260+
break;
261+
case MH_MAGIC_64:
262+
is_64 = true;
263+
break;
264+
default:
265+
throw deserialization_exceptiont("no Mach-O magic");
266+
}
267+
268+
uint32_t ncmds = 0;
269+
std::size_t offset = 0;
270+
271+
// re-read from the beginning, now reading the full header
272+
in.seekg(0);
273+
274+
if(!is_64)
275+
{
276+
// NOLINTNEXTLINE(readability/identifiers)
277+
struct mach_header mh;
278+
in.read(reinterpret_cast<char *>(&mh), sizeof(mh));
279+
280+
if(!in)
281+
throw deserialization_exceptiont("failed to read 32-bit Mach-O header");
282+
283+
if(need_swap)
284+
swap_mach_header(&mh, NXHostByteOrder());
285+
286+
ncmds = mh.ncmds;
287+
offset = sizeof(mh);
288+
}
289+
else
290+
{
291+
// NOLINTNEXTLINE(readability/identifiers)
292+
struct mach_header_64 mh;
293+
in.read(reinterpret_cast<char *>(&mh), sizeof(mh));
294+
295+
if(!in)
296+
throw deserialization_exceptiont("failed to read 64-bit Mach-O header");
297+
298+
if(need_swap)
299+
swap_mach_header_64(&mh, NXHostByteOrder());
300+
301+
ncmds = mh.ncmds;
302+
offset = sizeof(mh);
303+
}
304+
305+
process_commands(ncmds, offset, need_swap);
306+
#endif
307+
}

‎src/goto-programs/osx_fat_reader.h

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Module: Read OS X Fat Binaries
1313
#define CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H
1414

1515
#include <fstream>
16+
#include <map>
1617
#include <string>
1718

1819
// we follow
@@ -35,4 +36,40 @@ class osx_fat_readert
3536

3637
bool is_osx_fat_magic(char hdr[4]);
3738

39+
class osx_mach_o_readert
40+
{
41+
public:
42+
explicit osx_mach_o_readert(std::istream &_in);
43+
44+
struct sectiont
45+
{
46+
sectiont(const std::string &_name, std::size_t _offset, std::size_t _size)
47+
: name(_name), offset(_offset), size(_size)
48+
{
49+
}
50+
51+
std::string name;
52+
std::size_t offset;
53+
std::size_t size;
54+
};
55+
56+
using sectionst = std::map<std::string, sectiont>;
57+
sectionst sections;
58+
59+
bool has_section(const std::string &name) const
60+
{
61+
return sections.find(name) != sections.end();
62+
}
63+
64+
private:
65+
std::istream &in;
66+
67+
void process_commands(uint32_t ncmds, std::size_t offset, bool need_swap);
68+
69+
void process_sections_32(uint32_t nsects, bool need_swap);
70+
void process_sections_64(uint32_t nsects, bool need_swap);
71+
};
72+
73+
bool is_osx_mach_object(char hdr[4]);
74+
3875
#endif // CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H

‎src/goto-programs/read_goto_binary.cpp

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -146,6 +146,34 @@ static bool read_goto_binary(
146146
message.error() << "failed to find goto binary in Mach-O file"
147147
<< messaget::eom;
148148
}
149+
else if(is_osx_mach_object(hdr))
150+
{
151+
messaget message(message_handler);
152+
153+
// Mach-O object file, may contain a goto-cc section
154+
try
155+
{
156+
osx_mach_o_readert mach_o_reader(in);
157+
158+
osx_mach_o_readert::sectionst::const_iterator entry =
159+
mach_o_reader.sections.find("goto-cc");
160+
if(entry != mach_o_reader.sections.end())
161+
{
162+
in.seekg(entry->second.offset);
163+
return read_bin_goto_object(
164+
in, filename, symbol_table, goto_functions, message_handler);
165+
}
166+
167+
// section not found
168+
messaget(message_handler).error()
169+
<< "failed to find goto-cc section in Mach-O binary" << messaget::eom;
170+
}
171+
172+
catch(const deserialization_exceptiont &e)
173+
{
174+
messaget(message_handler).error() << e.what() << messaget::eom;
175+
}
176+
}
149177
else
150178
{
151179
messaget(message_handler).error() <<
@@ -212,6 +240,22 @@ bool is_goto_binary(const std::string &filename, message_handlert &)
212240
// ignore any errors
213241
}
214242
}
243+
else if(is_osx_mach_object(hdr))
244+
{
245+
// this _may_ have a goto-cc section
246+
try
247+
{
248+
in.seekg(0);
249+
osx_mach_o_readert mach_o_reader(in);
250+
if(mach_o_reader.has_section("goto-cc"))
251+
return true;
252+
}
253+
254+
catch(...)
255+
{
256+
// ignore any errors
257+
}
258+
}
215259

216260
return false;
217261
}

0 commit comments

Comments
 (0)