Skip to content

Commit

Permalink
Merge pull request diffblue#1888 from tautschnig/linker-script-fixes
Browse files Browse the repository at this point in the history 
Linker-script processing fixes
  • Loading branch information
Daniel Kroening committed Mar 3, 2018
2 parents a75c4f0 + b371e28 commit 6ef804c
Show file tree
Hide file tree
Showing 5 changed files with 87 additions and 62 deletions.
5 changes: 1 addition & 4 deletions src/goto-cc/compile.cpp
View file
Expand Up @@ -346,11 +346,8 @@ bool compilet::link()
convert_symbols(compiled_functions);

// parse object files
while(!object_files.empty())
for(const auto &file_name : object_files)
{
std::string file_name=object_files.front();
object_files.pop_front();

if(read_object_and_link(file_name, symbol_table,
compiled_functions, get_message_handler()))
return true;
Expand Down
3 changes: 2 additions & 1 deletion src/goto-cc/dist-linux
View file
Expand Up @@ -14,9 +14,10 @@ mkdir /tmp/goto-cc-dist
cp goto-cc /tmp/goto-cc-dist/
cp ../goto-instrument/goto-instrument /tmp/goto-cc-dist/
cp ../../LICENSE /tmp/goto-cc-dist/
cp ../../scripts/ls_parse.py /tmp/goto-cc-dist/
cd /tmp/goto-cc-dist
tar cfz goto-cc-${VERSION_FILE}-linux.tgz goto-cc \
goto-instrument LICENSE
goto-instrument LICENSE ls_parse.py

echo Copying.
scp goto-cc-${VERSION_FILE}-linux.tgz kroening@dkr0.inf.ethz.ch:/home/www/cprover.org/goto-cc/download/
Expand Down
9 changes: 2 additions & 7 deletions src/goto-cc/gcc_mode.cpp
View file
Expand Up @@ -813,7 +813,7 @@ int gcc_modet::run_gcc(const compilet &compiler)
for(const auto &a : cmdline.parsed_argv)
new_argv.push_back(a.arg);

if(compiler.wrote_object_files())
if(!act_as_ld && compiler.wrote_object_files())
{
// Undefine all __CPROVER macros for the system compiler
std::map<irep_idt, std::size_t> arities;
Expand Down Expand Up @@ -935,12 +935,7 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
{
linker_script_merget ls_merge(
compiler, output_files, goto_binaries, cmdline, gcc_message_handler);
const int fail=ls_merge.add_linker_script_definitions();
if(fail!=0)
{
error() << "Unable to merge linker script symbols" << eom;
return fail;
}
result=ls_merge.add_linker_script_definitions();
}

// merge output from gcc with goto-binaries
Expand Down
116 changes: 73 additions & 43 deletions src/goto-cc/linker_script_merge.cpp
View file
Expand Up @@ -38,12 +38,25 @@ int linker_script_merget::add_linker_script_definitions()
const std::string &elf_file=*elf_binaries.begin();
const std::string &goto_file=*goto_binaries.begin();

jsont data;
temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
std::list<irep_idt> linker_defined_symbols;
int fail=get_linker_script_data(
data, linker_defined_symbols, compiler.symbol_table, elf_file);
int fail=
get_linker_script_data(
linker_defined_symbols,
compiler.symbol_table,
elf_file,
linker_def_outfile());
// ignore linker script parsing failures until the code is tested more widely
if(fail!=0)
return 0;

jsont data;
fail=parse_json(linker_def_outfile(), get_message_handler(), data);
if(fail!=0)
{
error() << "Problem parsing linker script JSON data" << eom;
return fail;
}

fail=linker_data_is_malformed(data);
if(fail!=0)
Expand Down Expand Up @@ -117,8 +130,9 @@ linker_script_merget::linker_script_merget(
replacement_predicates(
{
replacement_predicatet("address of array's first member",
[](const exprt expr){ return to_symbol_expr(expr.op0().op0()); },
[](const exprt expr)
[](const exprt &expr) -> const symbol_exprt&
{ return to_symbol_expr(expr.op0().op0()); },
[](const exprt &expr, const namespacet &ns)
{
return expr.id()==ID_address_of &&
expr.type().id()==ID_pointer &&
Expand All @@ -133,25 +147,39 @@ linker_script_merget::linker_script_merget(
expr.op0().op1().type().id()==ID_signedbv;
}),
replacement_predicatet("address of array",
[](const exprt expr){ return to_symbol_expr(expr.op0()); },
[](const exprt expr)
[](const exprt &expr) -> const symbol_exprt&
{ return to_symbol_expr(expr.op0()); },
[](const exprt &expr, const namespacet &ns)
{
return expr.id()==ID_address_of &&
expr.type().id()==ID_pointer &&

expr.op0().id()==ID_symbol &&
expr.op0().type().id()==ID_array;
}),
replacement_predicatet("address of struct",
[](const exprt &expr) -> const symbol_exprt&
{ return to_symbol_expr(expr.op0()); },
[](const exprt &expr, const namespacet &ns)
{
return expr.id()==ID_address_of &&
expr.type().id()==ID_pointer &&

expr.op0().id()==ID_symbol &&
ns.follow(expr.op0().type()).id()==ID_struct;
}),
replacement_predicatet("array variable",
[](const exprt expr){ return to_symbol_expr(expr); },
[](const exprt expr)
[](const exprt &expr) -> const symbol_exprt&
{ return to_symbol_expr(expr); },
[](const exprt &expr, const namespacet &ns)
{
return expr.id()==ID_symbol &&
expr.type().id()==ID_array;
}),
replacement_predicatet("pointer (does not need pointerizing)",
[](const exprt expr){ return to_symbol_expr(expr); },
[](const exprt expr)
[](const exprt &expr) -> const symbol_exprt&
{ return to_symbol_expr(expr); },
[](const exprt &expr, const namespacet &ns)
{
return expr.id()==ID_symbol &&
expr.type().id()==ID_pointer;
Expand All @@ -164,6 +192,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
symbol_tablet &symbol_table,
const linker_valuest &linker_values)
{
const namespacet ns(symbol_table);

int ret=0;
// First, pointerize the actual linker-defined symbols
for(const auto &pair : linker_values)
Expand Down Expand Up @@ -191,7 +221,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
int fail=pointerize_subexprs_of(
symbol_table.get_writeable_ref(pair.first).value,
to_pointerize,
linker_values);
linker_values,
ns);
if(to_pointerize.empty() && fail==0)
continue;
ret=1;
Expand All @@ -216,7 +247,8 @@ int linker_script_merget::pointerize_linker_defined_symbols(
if(to_pointerize.empty())
continue;
debug() << "Pointerizing a program expression..." << eom;
int fail=pointerize_subexprs_of(*insts, to_pointerize, linker_values);
int fail = pointerize_subexprs_of(
*insts, to_pointerize, linker_values, ns);
if(to_pointerize.empty() && fail==0)
continue;
ret=1;
Expand Down Expand Up @@ -259,15 +291,17 @@ int linker_script_merget::replace_expr(
int linker_script_merget::pointerize_subexprs_of(
exprt &expr,
std::list<symbol_exprt> &to_pointerize,
const linker_valuest &linker_values)
const linker_valuest &linker_values,
const namespacet &ns)
{
int fail=0, tmp=0;
for(auto const &pair : linker_values)
for(auto const &pattern : replacement_predicates)
{
if(!pattern.match(expr))
if(!pattern.match(expr, ns))
continue;
const symbol_exprt &inner_symbol=pattern.inner_symbol(expr);
// take a copy, expr will be changed below
const symbol_exprt inner_symbol=pattern.inner_symbol(expr);
if(pair.first!=inner_symbol.get_identifier())
continue;
tmp=replace_expr(expr, linker_values, inner_symbol, pair.first,
Expand All @@ -292,7 +326,7 @@ int linker_script_merget::pointerize_subexprs_of(

for(auto &op : expr.operands())
{
tmp=pointerize_subexprs_of(op, to_pointerize, linker_values);
tmp=pointerize_subexprs_of(op, to_pointerize, linker_values, ns);
fail=tmp?tmp:fail;
}
return fail;
Expand Down Expand Up @@ -625,23 +659,24 @@ int linker_script_merget::ls_data2instructions(
#endif

int linker_script_merget::get_linker_script_data(
jsont &linker_data,
std::list<irep_idt> &linker_defined_symbols,
const symbol_tablet &symbol_table,
const std::string &out_file)
const std::string &out_file,
const std::string &def_out_file)
{
for(auto const &pair : symbol_table.symbols)
if(pair.second.is_extern && pair.second.value.is_nil()
&& pair.second.name!="__CPROVER_memory")
if(pair.second.is_extern && pair.second.value.is_nil() &&
pair.second.name!="__CPROVER_memory")
linker_defined_symbols.push_back(pair.second.name);

std::ostringstream linker_def_str;
std::copy(linker_defined_symbols.begin(), linker_defined_symbols.end(),
std::ostream_iterator<irep_idt>(linker_def_str, "\n"));
std::copy(
linker_defined_symbols.begin(),
linker_defined_symbols.end(),
std::ostream_iterator<irep_idt>(linker_def_str, "\n"));
debug() << "Linker-defined symbols: [" << linker_def_str.str() << "]\n"
<< eom;

temporary_filet linker_def_outfile("goto-cc-linker-info", ".json");
temporary_filet linker_def_infile("goto-cc-linker-defs", "");
std::ofstream linker_def_file(linker_def_infile());
linker_def_file << linker_def_str.str();
Expand All @@ -653,29 +688,24 @@ int linker_script_merget::get_linker_script_data(
"--script", cmdline.get_value('T'),
"--object", out_file,
"--sym-file", linker_def_infile(),
"--out-file", linker_def_outfile()
"--out-file", def_out_file
};
if(cmdline.isset("verbosity"))
{
unsigned verb=safe_string2unsigned(cmdline.get_value("verbosity"));
if(verb>9)
argv.push_back("--very-verbose");
else if(verb>4)
argv.push_back("--verbose");
}

int rc=run(argv[0], argv, linker_def_infile(), linker_def_outfile());
if(get_message_handler().get_verbosity()>9)
argv.push_back("--very-verbose");
else if(get_message_handler().get_verbosity()>4)
argv.push_back("--verbose");

debug() << "RUN:";
for(std::size_t i=0; i<argv.size(); i++)
debug() << " " << argv[i];
debug() << eom;

int rc=run(argv[0], argv, linker_def_infile(), def_out_file);
if(rc!=0)
{
error() << "Problem parsing linker script" << eom;
return rc;
}
warning() << "Problem parsing linker script" << eom;

int fail=parse_json(linker_def_outfile(), get_message_handler(),
linker_data);
if(fail!=0)
error() << "Problem parsing linker script JSON data" << eom;
return fail;
return rc;
}

int linker_script_merget::goto_and_object_mismatch(
Expand Down
16 changes: 9 additions & 7 deletions src/goto-cc/linker_script_merge.h
View file
Expand Up @@ -26,7 +26,7 @@ class replacement_predicatet
replacement_predicatet(
const std::string &description,
const std::function<const symbol_exprt&(const exprt&)> inner_symbol,
const std::function<bool(const exprt&)> match)
const std::function<bool(const exprt&, const namespacet&)> match)
: _description(description),
_inner_symbol(inner_symbol),
_match(match)
Expand All @@ -50,15 +50,15 @@ class replacement_predicatet
/// If this function returns true, the entire expression should be replaced by
/// a pointer whose underlying symbol is the symbol returned by
/// replacement_predicatet::inner_symbol().
const bool match(const exprt &expr) const
const bool match(const exprt &expr, const namespacet &ns) const
{
return _match(expr);
return _match(expr, ns);
};

private:
std::string _description;
std::function<const symbol_exprt&(const exprt&)> _inner_symbol;
std::function<bool(const exprt&)> _match;
std::function<bool(const exprt&, const namespacet&)> _match;
};

/// \brief Synthesise definitions of symbols that are defined in linker scripts
Expand Down Expand Up @@ -105,10 +105,10 @@ class linker_script_merget:public messaget

/// \brief Write linker script definitions to `linker_data`.
int get_linker_script_data(
jsont &linker_data,
std::list<irep_idt> &linker_defined_symbols,
const symbol_tablet &symbol_table,
const std::string &out_file);
const std::string &out_file,
const std::string &def_out_file);

/// \brief Write a list of definitions derived from `data` into gp's
/// `instructions` member.
Expand Down Expand Up @@ -165,6 +165,7 @@ class linker_script_merget:public messaget
/// \param to_pointerize The symbols that are contained in the subexpressions
/// that we will pointerize.
/// \param linker_values the names of symbols defined in linker scripts.
/// \param ns a namespace to look up types.
///
/// The subexpressions that we pointerize should be in one-to-one
/// correspondence with the symbols in `to_pointerize`. Every time we
Expand All @@ -175,7 +176,8 @@ class linker_script_merget:public messaget
int pointerize_subexprs_of(
exprt &expr,
std::list<symbol_exprt> &to_pointerize,
const linker_valuest &linker_values);
const linker_valuest &linker_values,
const namespacet &ns);

/// \brief do the actual replacement of an expr with a new pointer expr
int replace_expr(
Expand Down

0 comments on commit 6ef804c

Please sign in to comment.