Detect OSX fat archives or Mach-O objects on all architectures

Hard-code the magic values as extracted from OS X header files, but check them
when actually building on OS X.

Author: tautschnig

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -290,7 +290,7 @@ int jdiff_parse_optionst::get_goto_program(
 {
   status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
 
-  if(is_goto_binary(cmdline.args[0]))
+  if(is_goto_binary(cmdline.args[0], languages.get_message_handler()))
   {
     if(read_goto_binary(
          cmdline.args[0],

src/cbmc/cbmc_parse_options.cpp

@@ -484,8 +484,9 @@ int cbmc_parse_optionst::doit()
 
   if(cmdline.isset("show-parse-tree"))
   {
-    if(cmdline.args.size()!=1 ||
-       is_goto_binary(cmdline.args[0]))
+    if(
+      cmdline.args.size() != 1 ||
+      is_goto_binary(cmdline.args[0], ui_message_handler))
     {
       error() << "Please give exactly one source file" << eom;
       return CPROVER_EXIT_INCORRECT_TASK;

src/goto-cc/compile.cpp

@@ -125,7 +125,9 @@ enum class file_typet
   ELF_OBJECT
 };
 
-static file_typet detect_file_type(const std::string &file_name)
+static file_typet detect_file_type(
+  const std::string &file_name,
+  message_handlert &message_handler)
 {
   // first of all, try to open the file
   std::ifstream in(file_name);
@@ -153,7 +155,7 @@ static file_typet detect_file_type(const std::string &file_name)
   if(ext == "a")
     return file_typet::NORMAL_ARCHIVE;
 
-  if(is_goto_binary(file_name))
+  if(is_goto_binary(file_name, message_handler))
     return file_typet::GOTO_BINARY;
 
   if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
@@ -166,7 +168,7 @@ static file_typet detect_file_type(const std::string &file_name)
 /// \return false on success, true on error.
 bool compilet::add_input_file(const std::string &file_name)
 {
-  switch(detect_file_type(file_name))
+  switch(detect_file_type(file_name, get_message_handler()))
   {
   case file_typet::FAILED_TO_OPEN_FILE:
     warning() << "failed to open file `" << file_name
@@ -248,7 +250,7 @@ bool compilet::add_files_from_archive(
   {
     std::string t = concat_dir_file(tstr, line);
 
-    if(is_goto_binary(t))
+    if(is_goto_binary(t, get_message_handler()))
       object_files.push_back(t);
     else
       debug() << "Object file is not a goto binary: " << line << eom;
@@ -279,7 +281,7 @@ bool compilet::find_library(const std::string &name)
     {
       library_file_name = concat_dir_file(library_path, "lib" + name + ".so");
 
-      switch(detect_file_type(library_file_name))
+      switch(detect_file_type(library_file_name, get_message_handler()))
       {
       case file_typet::GOTO_BINARY:
         return !add_input_file(library_file_name);

src/goto-diff/goto_diff_parse_options.cpp

@@ -330,7 +330,7 @@ int goto_diff_parse_optionst::get_goto_program(
 {
   status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
 
-  if(is_goto_binary(cmdline.args[0]))
+  if(is_goto_binary(cmdline.args[0], languages.get_message_handler()))
   {
     if(read_goto_binary(
         cmdline.args[0],

src/goto-programs/initialize_goto_model.cpp

@@ -49,7 +49,7 @@ goto_modelt initialize_goto_model(
 
   for(const auto &file : files)
   {
-    if(is_goto_binary(file))
+    if(is_goto_binary(file, message_handler))
       binaries.push_back(file);
     else
       sources.push_back(file);

src/goto-programs/lazy_goto_model.cpp

@@ -128,7 +128,7 @@ void lazy_goto_modelt::initialize(
 
   for(const auto &file : files)
   {
-    if(is_goto_binary(file))
+    if(is_goto_binary(file, message_handler))
       binaries.push_back(file);
     else
       sources.push_back(file);

src/goto-programs/osx_fat_reader.cpp

@@ -15,35 +15,48 @@ Module: Read Mach-O
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 
+// we define file-type magic values for all platforms to detect when we find a
+// file that we might not be able to process
+#define CPROVER_FAT_MAGIC 0xcafebabe
+#define CPROVER_FAT_CIGAM 0xbebafeca
+#define CPROVER_MH_MAGIC 0xfeedface
+#define CPROVER_MH_CIGAM 0xcefaedfe
+#define CPROVER_MH_MAGIC_64 0xfeedfacf
+#define CPROVER_MH_CIGAM_64 0xcffaedfe
+
 #ifdef __APPLE__
 #include <architecture/byte_order.h>
 #include <mach-o/fat.h>
 #include <mach-o/loader.h>
 #include <mach-o/swap.h>
+
+#if(CPROVER_FAT_MAGIC != FAT_MAGIC) || (CPROVER_FAT_CIGAM != FAT_CIGAM) ||     \
+  (CPROVER_MH_MAGIC != MH_MAGIC) || (CPROVER_MH_CIGAM != MH_CIGAM) ||          \
+  (CPROVER_MH_MAGIC_64 != MH_MAGIC_64) || (CPROVER_MH_CIGAM != MH_CIGAM_64)
+#error "Mach-O magic has inconsistent value"
+#endif
 #endif
 
 #include <util/run.h>
 
 bool is_osx_fat_magic(char hdr[4])
 {
-#ifdef __APPLE__
   uint32_t *magic=reinterpret_cast<uint32_t*>(hdr);
 
   switch(*magic)
   {
-    case FAT_MAGIC:
-    case FAT_CIGAM:
-      return true;
+  case CPROVER_FAT_MAGIC:
+  case CPROVER_FAT_CIGAM:
+    return true;
   }
-#else
-  (void)hdr; // unused parameter
-#endif
 
   return false;
 }
 
-osx_fat_readert::osx_fat_readert(std::ifstream &in) :
-  has_gb_arch(false)
+osx_fat_readert::osx_fat_readert(
+  std::ifstream &in,
+  message_handlert &message_handler)
+  : log(message_handler), has_gb_arch(false)
 {
 #ifdef __APPLE__
   // NOLINTNEXTLINE(readability/identifiers)
@@ -82,6 +95,9 @@ osx_fat_readert::osx_fat_readert(std::ifstream &in) :
   }
 #else
   (void)in;  // unused parameter
+
+  log.warning() << "Cannot read OSX fat archive on this platform"
+                << messaget::eom;
 #endif
 }
 
@@ -99,20 +115,16 @@ bool osx_fat_readert::extract_gb(
 // 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:
+  case CPROVER_MH_MAGIC:
+  case CPROVER_MH_CIGAM:
+  case CPROVER_MH_MAGIC_64:
+  case CPROVER_MH_CIGAM_64:
     return true;
   }
-#else
-  (void)hdr; // unused parameter
-#endif
 
   return false;
 }
@@ -236,7 +248,10 @@ void osx_mach_o_readert::process_commands(
 #endif
 }
 
-osx_mach_o_readert::osx_mach_o_readert(std::istream &_in) : in(_in)
+osx_mach_o_readert::osx_mach_o_readert(
+  std::istream &_in,
+  message_handlert &message_handler)
+  : log(message_handler), in(_in)
 {
   // read magic
   uint32_t magic;
@@ -249,16 +264,16 @@ osx_mach_o_readert::osx_mach_o_readert(std::istream &_in) : in(_in)
   bool is_64 = false, need_swap = false;
   switch(magic)
   {
-  case MH_CIGAM:
+  case CPROVER_MH_CIGAM:
     need_swap = true;
     break;
-  case MH_MAGIC:
+  case CPROVER_MH_MAGIC:
     break;
-  case MH_CIGAM_64:
+  case CPROVER_MH_CIGAM_64:
     need_swap = true;
     is_64 = true;
     break;
-  case MH_MAGIC_64:
+  case CPROVER_MH_MAGIC_64:
     is_64 = true;
     break;
   default:
@@ -303,5 +318,6 @@ osx_mach_o_readert::osx_mach_o_readert(std::istream &_in) : in(_in)
   }
 
   process_commands(ncmds, offset, need_swap);
+#else
 #endif
 }

src/goto-programs/osx_fat_reader.h

@@ -12,6 +12,8 @@ Module: Read OS X Fat Binaries
 #ifndef CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H
 #define CPROVER_GOTO_PROGRAMS_OSX_FAT_READER_H
 
+#include <util/message.h>
+
 #include <fstream>
 #include <map>
 #include <string>
@@ -22,7 +24,7 @@ Module: Read OS X Fat Binaries
 class osx_fat_readert
 {
 public:
-  explicit osx_fat_readert(std::ifstream &in);
+  osx_fat_readert(std::ifstream &, message_handlert &);
 
   bool has_gb() const { return has_gb_arch; }
 
@@ -31,6 +33,7 @@ class osx_fat_readert
     const std::string &dest) const;
 
 private:
+  messaget log;
   bool has_gb_arch;
 };
 
@@ -39,7 +42,7 @@ bool is_osx_fat_magic(char hdr[4]);
 class osx_mach_o_readert
 {
 public:
-  explicit osx_mach_o_readert(std::istream &_in);
+  osx_mach_o_readert(std::istream &, message_handlert &);
 
   struct sectiont
   {
@@ -62,6 +65,7 @@ class osx_mach_o_readert
   }
 
 private:
+  messaget log;
   std::istream &in;
 
   void process_commands(uint32_t ncmds, std::size_t offset, bool need_swap);

src/goto-programs/read_goto_binary.cpp

@@ -130,7 +130,7 @@ bool read_goto_binary(
 
     // Mach-O universal binary
     // This _may_ have a goto binary as hppa7100LC architecture
-    osx_fat_readert osx_fat_reader(in);
+    osx_fat_readert osx_fat_reader(in, message_handler);
 
     if(osx_fat_reader.has_gb())
     {
@@ -163,7 +163,7 @@ bool read_goto_binary(
     // Mach-O object file, may contain a goto-cc section
     try
     {
-      osx_mach_o_readert mach_o_reader(in);
+      osx_mach_o_readert mach_o_reader(in, message_handler);
 
       osx_mach_o_readert::sectionst::const_iterator entry =
         mach_o_reader.sections.find("goto-cc");
@@ -193,7 +193,9 @@ bool read_goto_binary(
   return true;
 }
 
-bool is_goto_binary(const std::string &filename)
+bool is_goto_binary(
+  const std::string &filename,
+  message_handlert &message_handler)
 {
   #ifdef _MSC_VER
   std::ifstream in(widen(filename), std::ios::binary);
@@ -240,7 +242,7 @@ bool is_goto_binary(const std::string &filename)
     try
     {
       in.seekg(0);
-      osx_fat_readert osx_fat_reader(in);
+      osx_fat_readert osx_fat_reader(in, message_handler);
       if(osx_fat_reader.has_gb())
         return true;
     }
@@ -256,7 +258,7 @@ bool is_goto_binary(const std::string &filename)
     try
     {
       in.seekg(0);
-      osx_mach_o_readert mach_o_reader(in);
+      osx_mach_o_readert mach_o_reader(in, message_handler);
       if(mach_o_reader.has_section("goto-cc"))
         return true;
     }

src/goto-programs/read_goto_binary.h

@@ -37,7 +37,7 @@ bool read_goto_binary(
 optionalt<goto_modelt>
 read_goto_binary(const std::string &filename, message_handlert &);
 
-bool is_goto_binary(const std::string &filename);
+bool is_goto_binary(const std::string &filename, message_handlert &);
 
 bool read_object_and_link(
   const std::string &file_name,