Skip to content

Linker-script processing fixes #1888

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 3, 2018
Merged

Linker-script processing fixes #1888

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
1f753d8
fixup! goto-gcc removes CPROVER macros for native gcc
tautschnig Sep 7, 2017
631ea60
Make linker-script processing failures non-fatal
tautschnig Sep 7, 2017
60487f7
Distribute ls_parse.py with goto-cc
tautschnig Sep 7, 2017
1612f74
Do not modify object_files list while processing it
tautschnig Sep 8, 2017
e999552
Linker-script processing: mind temporaries
tautschnig Feb 27, 2018
b371e28
Linker-scripts: support linker symbols with struct type
tautschnig Feb 27, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 1 addition & 4 deletions src/goto-cc/compile.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
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
Open in desktop
Original file line number Diff line number Diff line change
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 [email protected]:/home/www/cprover.org/goto-cc/download/
Expand Down
9 changes: 2 additions & 7 deletions src/goto-cc/gcc_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
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())
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is not clear to me where this is set / why this would work but in this part of the code I am willing to take your word for it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

act_as_ld is a class member set upon construction, with its value dependent on the name of the executable that is running this code ("goto-ld" -> true, "goto-cc" -> false). When acting as a linker, we shouldn't be adding preprocessor command-line options.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK; fair.

{
// 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
Open in desktop
Original file line number Diff line number Diff line change
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
Open in desktop
Original file line number Diff line number Diff line change
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