replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #2030 from tautschnig/goto-cc-linux-kernel 

Goto-cc extensions to build (and link) recent Linux kernels
This commit is contained in:
Daniel Kroening 2018-04-21 14:29:50 +01:00 committed by GitHub
parent 42e58d4657 177c8c1f2b
commit dd0d6025fb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
5 changed files with 167 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

198
src/goto-cc/compile.cpp
View File

@ -13,6 +13,7 @@ Date: June 2006
#include "compile.h"
#include <cstring>
#include <fstream>
#include <sstream>
#include <iostream>
@ -135,48 +136,99 @@ bool compilet::doit()
warnings_before;
}
enum class file_typet
{
FAILED_TO_OPEN_FILE,
UNKNOWN,
SOURCE_FILE,
NORMAL_ARCHIVE,
THIN_ARCHIVE,
GOTO_BINARY,
ELF_OBJECT
};
static file_typet detect_file_type(const std::string &file_name)
{
// first of all, try to open the file
std::ifstream in(file_name);
if(!in)
return file_typet::FAILED_TO_OPEN_FILE;
const std::string::size_type r = file_name.rfind('.');
const std::string ext =
r == std::string::npos ? "" : file_name.substr(r + 1, file_name.length());
if(
ext == "c" || ext == "cc" || ext == "cp" || ext == "cpp" || ext == "CPP" ||
ext == "c++" || ext == "C" || ext == "i" || ext == "ii" || ext == "class" ||
ext == "jar" || ext == "jsil")
{
return file_typet::SOURCE_FILE;
}
char hdr[8];
in.get(hdr, 8);
if((ext == "a" || ext == "o") && strncmp(hdr, "!<thin>", 8) == 0)
return file_typet::THIN_ARCHIVE;
if(ext == "a")
return file_typet::NORMAL_ARCHIVE;
if(is_goto_binary(file_name))
return file_typet::GOTO_BINARY;
if(hdr[0] == 0x7f && memcmp(hdr + 1, "ELF", 3) == 0)
return file_typet::ELF_OBJECT;
return file_typet::UNKNOWN;
}
/// puts input file names into a list and does preprocessing for libraries.
/// \return false on success, true on error.
bool compilet::add_input_file(const std::string &file_name)
{
// first of all, try to open the file
switch(detect_file_type(file_name))
{
std::ifstream in(file_name);
if(!in)
{
warning() << "failed to open file `" << file_name << "'" << eom;
case file_typet::FAILED_TO_OPEN_FILE:
warning() << "failed to open file `" << file_name
<< "': " << std::strerror(errno) << eom;
return warning_is_fatal; // generously ignore unless -Werror
}
}
size_t r=file_name.rfind('.', file_name.length()-1);
case file_typet::UNKNOWN:
// unknown extension, not a goto binary, will silently ignore
debug() << "unknown file type in `" << file_name << "'" << eom;
return false;
if(r==std::string::npos)
{
// a file without extension; will ignore
warning() << "input file `" << file_name
<< "' has no extension, not considered" << eom;
return warning_is_fatal;
}
case file_typet::ELF_OBJECT:
// ELF file without goto-cc section, silently ignore
debug() << "ELF object without goto-cc section: `" << file_name << "'"
<< eom;
return false;
std::string ext = file_name.substr(r+1, file_name.length());
if(ext=="c" ||
ext=="cc" ||
ext=="cp" ||
ext=="cpp" ||
ext=="CPP" ||
ext=="c++" ||
ext=="C" ||
ext=="i" ||
ext=="ii" ||
ext=="class" ||
ext=="jar" ||
ext=="jsil")
{
case file_typet::SOURCE_FILE:
source_files.push_back(file_name);
return false;
case file_typet::NORMAL_ARCHIVE:
return add_files_from_archive(file_name, false);
case file_typet::THIN_ARCHIVE:
return add_files_from_archive(file_name, true);
case file_typet::GOTO_BINARY:
object_files.push_back(file_name);
return false;
}
else if(ext=="a")
UNREACHABLE;
}
/// extracts goto binaries from AR archive and add them as input files.
/// \return false on success, true on error.
bool compilet::add_files_from_archive(
const std::string &file_name,
bool thin_archive)
{
#ifdef _WIN32
char td[MAX_PATH + 1];
@ -184,7 +236,14 @@ bool compilet::add_input_file(const std::string &file_name)
char td[] = "goto-cc.XXXXXX";
#endif
std::string tstr=get_temporary_directory(td);
std::stringstream cmd;
FILE *stream;
std::string tstr = working_directory;
if(!thin_archive)
{
tstr = get_temporary_directory(td);
if(tstr=="")
{
@ -193,7 +252,6 @@ bool compilet::add_input_file(const std::string &file_name)
}
tmp_dirs.push_back(tstr);
std::stringstream cmd("");
if(chdir(tmp_dirs.back().c_str())!=0)
{
error() << "Cannot switch to temporary directory" << eom;
@ -203,32 +261,15 @@ bool compilet::add_input_file(const std::string &file_name)
// unpack now
cmd << "ar x " << concat_dir_file(working_directory, file_name);
FILE *stream;
stream=popen(cmd.str().c_str(), "r");
pclose(stream);
cmd.clear();
cmd.str("");
}
// add the files from "ar t"
#ifdef _WIN32
if(file_name[0]!='/' && file_name[1]!=':') // NOLINT(readability/braces)
#else
if(file_name[0]!='/') // NOLINT(readability/braces)
#endif
{
cmd << "ar t " <<
#ifdef _WIN32
working_directory << "\\" << file_name;
#else
working_directory << "/" << file_name;
#endif
}
else
{
cmd << "ar t " << file_name;
}
cmd << "ar t " << concat_dir_file(working_directory, file_name);
stream = popen(cmd.str().c_str(), "r");
@ -244,15 +285,12 @@ bool compilet::add_input_file(const std::string &file_name)
}
else
{
std::string t;
#ifdef _WIN32
t = tmp_dirs.back() + '\\' + line;
#else
t = tmp_dirs.back() + '/' + line;
#endif
std::string t = concat_dir_file(tstr, line);
if(is_goto_binary(t))
object_files.push_back(t);
else
debug() << "Object file is not a goto binary: " << line << eom;
line = "";
}
@ -261,17 +299,8 @@ bool compilet::add_input_file(const std::string &file_name)
pclose(stream);
}
cmd.str("");
if(chdir(working_directory.c_str())!=0)
if(!thin_archive && chdir(working_directory.c_str()) != 0)
error() << "Could not change back to working directory" << eom;
}
else if(is_goto_binary(file_name))
object_files.push_back(file_name);
else
{
// unknown extension, not a goto binary, will silently ignore
}
return false;
}
@ -302,36 +331,19 @@ bool compilet::find_library(const std::string &name)
{
std::string libname=tmp+name+".so";
if(is_goto_binary(libname))
return !add_input_file(libname);
else if(is_elf_file(libname))
switch(detect_file_type(libname))
{
case file_typet::GOTO_BINARY:
return !add_input_file(libname);
case file_typet::ELF_OBJECT:
warning() << "Warning: Cannot read ELF library " << libname << eom;
return warning_is_fatal;
}
}
}
return false;
default:
break;
}
}
/// checking if we can load an object file
/// \par parameters: file name
/// \return true if the given file name exists and is an ELF file, false
/// otherwise
bool compilet::is_elf_file(const std::string &file_name)
{
std::fstream in;
in.open(file_name, std::ios::in);
if(in.is_open())
{
char buf[4];
for(std::size_t i=0; i<4; i++)
buf[i]=static_cast<char>(in.get());
if(buf[0]==0x7f && buf[1]=='E' &&
buf[2]=='L' && buf[3]=='F')
return true;
}
return false;

2
src/goto-cc/compile.h
View File

@ -53,7 +53,7 @@ public:
bool add_input_file(const std::string &);
bool find_library(const std::string &);
bool is_elf_file(const std::string &);
bool add_files_from_archive(const std::string &file_name, bool thin_archive);
bool parse(const std::string &filename);
bool parse_stdin();

10
src/goto-cc/gcc_cmdline.cpp
View File

@ -18,9 +18,7 @@ Author: CM Wintersteiger, 2006
#include <util/prefix.h>
/// parses the command line options into a cmdlinet
/// \par parameters: argument count, argument strings
/// \return none
// clang-format off
// non-gcc options
const char *goto_cc_options_with_separated_argument[]=
{
@ -163,6 +161,8 @@ const char *gcc_options_without_argument[]=
"-print-multi-directory",
"-print-multi-lib",
"-print-search-dirs",
"-print-sysroot",
"-print-sysroot-headers-suffix",
"-Q",
"-Qn",
"-Qy",
@ -211,7 +211,11 @@ const char *gcc_options_without_argument[]=
"-fast", // Apple only
nullptr
};
// clang-format on
/// parses the command line options into a cmdlinet
/// \par parameters: argument count, argument strings
/// \return none
bool gcc_cmdlinet::parse(int argc, const char **argv)
{
assert(argc>0);

14
src/goto-cc/gcc_mode.cpp
View File

@ -380,12 +380,24 @@ int gcc_modet::doit()
return EX_OK; // Exit!
}
if(cmdline.isset("dumpversion"))
if(
cmdline.isset("dumpmachine") || cmdline.isset("dumpspecs") ||
cmdline.isset("dumpversion") || cmdline.isset("print-sysroot") ||
cmdline.isset("print-sysroot-headers-suffix"))
{
if(produce_hybrid_binary)
return run_gcc(compiler);
// GCC will only print one of these, even when multiple arguments are
// passed, so we do the same
if(cmdline.isset("dumpmachine"))
std::cout << config.this_architecture() << '\n';
else if(cmdline.isset("dumpversion"))
std::cout << "3.4.4\n";
// we don't have any meaningful output for the other options, and GCC
// doesn't necessarily produce non-empty output either
return EX_OK;
}

9
src/goto-cc/ld_cmdline.cpp
View File

@ -16,9 +16,7 @@ Author: Daniel Kroening, 2013
#include <util/prefix.h>
/// parses the command line options into a cmdlinet
/// \par parameters: argument count, argument strings
/// \return none
// clang-format off
const char *goto_ld_options_with_argument[]=
{
"--verbosity",
@ -99,6 +97,7 @@ const char *ld_options_with_argument[]=
"--ios_version_min", // Apple only
"--macosx_version_min", // Apple only
"--install_name", // Apple only
"--build-id",
nullptr
};
@ -235,7 +234,11 @@ const char *ld_options_without_argument[]=
"--bundle", // Apple only
nullptr
};
// clang-format on
/// parses the command line options into a cmdlinet
/// \par parameters: argument count, argument strings
/// \return none
bool ld_cmdlinet::parse(int argc, const char **argv)
{
assert(argc>0);