Read goto-cc section from Mach-O object files

A basic Mach-O header parser, only functional on OS X.

Author: tautschnig

src/goto-programs/osx_fat_reader.cpp

@@ -16,7 +16,10 @@ Module: Read Mach-O
 #include <util/invariant.h>
 
 #ifdef __APPLE__
+#include <architecture/byte_order.h>
 #include <mach-o/fat.h>
+#include <mach-o/loader.h>
+#include <mach-o/swap.h>
 #endif
 
 #include <util/run.h>
@@ -92,3 +95,140 @@ bool osx_fat_readert::extract_gb(
            "lipo", {"lipo", "-thin", "hppa7100LC", "-output", dest, source}) !=
          0;
 }
+
+// guided by https://lowlevelbits.org/parsing-mach-o-files/
+bool is_osx_mach_object(char hdr[4])
+{
+#ifdef __APPLE__
+  uint32_t *magic = reinterpret_cast<uint32_t *>(hdr);
+
+  switch(*magic)
+  {
+  case MH_MAGIC:
+  case MH_CIGAM:
+  case MH_MAGIC_64:
+  case MH_CIGAM_64:
+    return true;
+  }
+#else
+  (void)hdr; // unused parameter
+#endif
+
+  return false;
+}
+
+osx_mach_o_readert::osx_mach_o_readert(std::istream &_in) : in(_in)
+{
+  // read magic
+  uint32_t magic;
+  in.read(reinterpret_cast<char *>(&magic), sizeof(magic));
+
+  if(!in)
+    throw deserialization_exceptiont("failed to read Mach-O magic");
+
+#ifdef __APPLE__
+  bool is_64 = false, need_swap = false;
+  switch(magic)
+  {
+  case MH_CIGAM:
+    need_swap = true;
+    break;
+  case MH_MAGIC:
+    break;
+  case MH_CIGAM_64:
+    need_swap = true;
+    is_64 = true;
+    break;
+  case MH_MAGIC_64:
+    is_64 = true;
+    break;
+  default:
+    throw deserialization_exceptiont("no Mach-O magic");
+  }
+
+  uint32_t ncmds = 0;
+  std::size_t offset = 0;
+
+  if(!is_64)
+  {
+    // NOLINTNEXTLINE(readability/identifiers)
+    struct mach_header mh;
+    in.read(reinterpret_cast<char *>(&mh), sizeof(mh));
+
+    if(!in)
+      throw deserialization_exceptiont("failed to read 32-bit Mach-O header");
+
+    if(need_swap)
+      swap_mach_header(&mh, NXHostByteOrder());
+
+    ncmds = mh.ncmds;
+    offset = sizeof(mh);
+  }
+  else
+  {
+    // NOLINTNEXTLINE(readability/identifiers)
+    struct mach_header_64 mh;
+    in.read(reinterpret_cast<char *>(&mh), sizeof(mh));
+
+    if(!in)
+      throw deserialization_exceptiont("failed to read 64-bit Mach-O header");
+
+    if(need_swap)
+      swap_mach_header_64(mh, NXHostByteOrder());
+
+    ncmds = mh.ncmds;
+    offset = sizeof(mh);
+  }
+
+  for(uint32_t i = 0; i < ncmds; ++i)
+  {
+    // NOLINTNEXTLINE(readability/identifiers)
+    struct load_command lc;
+    in.read(reinterpret_cast<char *>(&lc), sizeof(lc));
+
+    if(!in)
+      throw deserialization_exceptiont("failed to read Mach-O command");
+
+    if(need_swap)
+      swap_load_command(&lc, NXHostByteOrder());
+
+    switch(lc.cmd)
+    {
+    case LC_SEGMENT:
+    {
+      // NOLINTNEXTLINE(readability/identifiers)
+      struct segment_command seg;
+      in.read(reinterpret_cast<char *>(&seg), sizeof(seg));
+
+      if(!in)
+        throw deserialization_exceptiont("failed to read Mach-O segment");
+
+      if(need_swap)
+        swap_segment_command(&seg, NXHostByteOrder());
+
+      segments.emplace(seg.segname, segmentt(seg.segname, offset, lc.cmdsize));
+      break;
+    }
+    case LC_SEGMENT_64:
+    {
+      // NOLINTNEXTLINE(readability/identifiers)
+      struct segment_command_64 seg;
+      in.read(reinterpret_cast<char *>(&seg), sizeof(seg));
+
+      if(!in)
+        throw deserialization_exceptiont("failed to read Mach-O segment");
+
+      if(need_swap)
+        swap_segment_command_64(&seg, NXHostByteOrder());
+
+      segments.emplace(seg.segname, segmentt(seg.segname, offset, lc.cmdsize));
+      break;
+    }
+    default:
+      break;
+    }
+
+    offset += lc.cmdsize;
+  }
+#endif
+}

src/goto-programs/osx_fat_reader.h

@@ -13,6 +13,7 @@ Module: Read OS X Fat Binaries
 #define CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H
 
 #include <fstream>
+#include <map>
 #include <string>
 
 // we follow
@@ -35,4 +36,35 @@ class osx_fat_readert
 
 bool is_osx_fat_magic(char hdr[4]);
 
+class osx_mach_o_readert
+{
+public:
+  explicit osx_mach_o_readert(std::istream &_in);
+
+  struct segmentt
+  {
+    segmentt(const std::string &_name, std::size_t _offset, std::size_t _size)
+      : name(_name), offset(_offset), size(_size)
+    {
+    }
+
+    std::string name;
+    std::size_t offset;
+    std::size_t size;
+  };
+
+  using segmentst = std::map<std::string, segmentt>;
+  segmentst segments;
+
+  bool has_section(const std::string &name) const
+  {
+    return segments.find(name) != segments.end();
+  }
+
+private:
+  std::istream &in;
+};
+
+bool is_osx_mach_object(char hdr[4]);
+
 #endif // CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H

src/goto-programs/read_goto_binary.cpp

@@ -156,6 +156,34 @@ bool read_goto_binary(
     message.error() << "failed to find goto binary in Mach-O file"
                     << messaget::eom;
   }
+  else if(is_osx_mach_object(hdr))
+  {
+    messaget message(message_handler);
+
+    // Mach-O object file, may contain a goto-cc section
+    try
+    {
+      osx_mach_o_readert mach_o_reader(in);
+
+      osx_mach_o_readert::segmentst::const_iterator entry =
+        mach_o_reader.segments.find("goto-cc");
+      if(entry != mach_o_reader.segments.end())
+      {
+        in.seekg(entry->second.offset);
+        return read_bin_goto_object(
+          in, filename, symbol_table, goto_functions, message_handler);
+      }
+
+      // section not found
+      messaget(message_handler).error()
+        << "failed to find goto-cc section in Mach-O binary" << messaget::eom;
+    }
+
+    catch(const deserialization_exceptiont &e)
+    {
+      messaget(message_handler).error() << e.what() << messaget::eom;
+    }
+  }
   else
   {
     messaget(message_handler).error() <<
@@ -222,6 +250,22 @@ bool is_goto_binary(const std::string &filename)
       // ignore any errors
     }
   }
+  else if(is_osx_mach_object(hdr))
+  {
+    // this _may_ have a goto-cc section
+    try
+    {
+      in.seekg(0);
+      osx_mach_o_readert mach_o_reader(in);
+      if(mach_o_reader.has_section("goto-cc"))
+        return true;
+    }
+
+    catch(...)
+    {
+      // ignore any errors
+    }
+  }
 
   return false;
 }