cprover
|
Synthesise definitions of symbols that are defined in linker scripts. More...
#include <linker_script_merge.h>
Public Types | |
typedef std::map< irep_idt, std::pair< symbol_exprt, exprt > > | linker_valuest |
Public Member Functions | |
int | add_linker_script_definitions () |
Add values of linkerscript-defined symbols to the goto-binary. More... | |
linker_script_merget (compilet &, const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &, message_handlert &) | |
Protected Member Functions | |
int | get_linker_script_data (std::list< irep_idt > &linker_defined_symbols, const symbol_tablet &symbol_table, const std::string &out_file, const std::string &def_out_file) |
Write linker script definitions to linker_data . More... | |
int | ls_data2instructions (jsont &data, const std::string &linker_script, goto_programt &gp, symbol_tablet &symbol_table, linker_valuest &linker_values) |
Write a list of definitions derived from data into gp's instructions member. More... | |
int | pointerize_linker_defined_symbols (goto_functionst &goto_functions, symbol_tablet &symbol_table, const linker_valuest &linker_values) |
convert the type of linker script-defined symbols to char* More... | |
int | pointerize_subexprs_of (exprt &expr, std::list< symbol_exprt > &to_pointerize, const linker_valuest &linker_values, const namespacet &ns) |
int | replace_expr (exprt &old_expr, const linker_valuest &linker_values, const symbol_exprt &old_symbol, const irep_idt &ident, const std::string &shape) |
do the actual replacement of an expr with a new pointer expr More... | |
void | symbols_to_pointerize (const linker_valuest &linker_values, const exprt &expr, std::list< symbol_exprt > &to_pointerize) const |
fill to_pointerize with names of linker symbols appearing in expr More... | |
int | goto_and_object_mismatch (const std::list< irep_idt > &linker_defined_symbols, const linker_valuest &linker_values) |
one-to-one correspondence between extern & linker symbols More... | |
int | linker_data_is_malformed (const jsont &data) const |
Validate output of the scripts/ls_parse.py tool. More... | |
Protected Attributes | |
compilet & | compiler |
const std::string & | elf_binary |
const std::string & | goto_binary |
const cmdlinet & | cmdline |
std::list< replacement_predicatet > | replacement_predicates |
The "shapes" of expressions to be replaced by a pointer. More... | |
Additional Inherited Members |
Synthesise definitions of symbols that are defined in linker scripts.
Definition at line 65 of file linker_script_merge.h.
typedef std::map<irep_idt, std::pair<symbol_exprt, exprt> > linker_script_merget::linker_valuest |
Definition at line 82 of file linker_script_merge.h.
linker_script_merget::linker_script_merget | ( | compilet & | compiler, |
const std::string & | elf_binary, | ||
const std::string & | goto_binary, | ||
const cmdlinet & | cmdline, | ||
message_handlert & | message_handler | ||
) |
Definition at line 118 of file linker_script_merge.cpp.
References irept::id(), exprt::op0(), exprt::op1(), to_symbol_expr(), and exprt::type().
int linker_script_merget::add_linker_script_definitions | ( | ) |
Add values of linkerscript-defined symbols to the goto-binary.
elf_binaries
and goto_binaries
, and the codebase is being linked with a custom linker script passed to the compiler with the -T
option. __CPROVER_initialize
function contains synthesized definitions for all symbols that are declared in the C codebase and defined in the linker script. __CPROVER_initialize
function contains one __CPROVER_allocated_memory
annotation for each object file section that is specified in the linker script. Definition at line 28 of file linker_script_merge.cpp.
References cmdline, compiler, elf_binary, messaget::eom(), messaget::error(), goto_functionst::function_map, get_linker_script_data(), messaget::get_message_handler(), cmdlinet::get_value(), goto_and_object_mismatch(), goto_binary, INITIALIZE_FUNCTION, cmdlinet::isset(), linker_data_is_malformed(), ls_data2instructions(), parse_json(), pointerize_linker_defined_symbols(), read_goto_binary(), language_uit::symbol_table, and compilet::write_object_file().
Referenced by ld_modet::ld_hybrid_binary().
|
protected |
Write linker script definitions to linker_data
.
Definition at line 656 of file linker_script_merge.cpp.
References cmdline, messaget::debug(), messaget::eom(), messaget::get_message_handler(), cmdlinet::get_value(), messaget::M_DEBUG, messaget::M_RESULT, run(), symbol_table_baset::symbols, and messaget::warning().
Referenced by add_linker_script_definitions().
|
protected |
one-to-one correspondence between extern & linker symbols
Check that a string is in linker_defined_symbols
iff it is a key in the linker_values
map. The error messages of this function describe what it means for this constraint to be violated.
linker_defined_symbols | the list of symbols that were extern with no value in the goto-program) |
linker_values | map from the names of linker-defined symbols from the object file, to synthesized values for those linker symbols. |
1
if there is some mismatch between the list and map, 0
if everything is OK. Definition at line 706 of file linker_script_merge.cpp.
References messaget::eom(), and messaget::error().
Referenced by add_linker_script_definitions().
|
protected |
Validate output of the scripts/ls_parse.py
tool.
Definition at line 735 of file linker_script_merge.cpp.
References is_false().
Referenced by add_linker_script_definitions().
|
protected |
Write a list of definitions derived from data
into gp's instructions
member.
data
is in the format verified by linker_data_is_malformed. data
, a function call to __CPROVER_allocated_memory
is prepended to initialize_instructions
. data
, a declaration and initialization of that symbol is prepended to initialize_instructions
. data
shall be a key in linker_values
; the value shall be a constant expression with the actual value of the symbol in the linker script. Definition at line 396 of file linker_script_merge.cpp.
References add(), symbol_table_baset::add(), exprt::add_source_location(), array_name(), char_type(), CPROVER_PREFIX, irept::find(), from_integer(), id2string(), goto_programt::instructions, integer2binary(), integer2size_t(), integer2unsigned(), symbolt::is_lvalue, symbolt::is_static_lifetime, loc, symbolt::location, goto_programt::instructiont::make_assignment(), exprt::make_typecast(), MAX_FLATTENED_ARRAY_SIZE, message_handler, symbolt::name, pointer_type(), symbolt::pretty_name, source_locationt::set_comment(), source_locationt::set_file(), constant_exprt::set_value(), size_type(), goto_programt::instructiont::source_location, string2integer(), to_string(), symbolt::type, exprt::type(), unsigned_int_type(), and zero_initializer().
Referenced by add_linker_script_definitions().
|
protected |
convert the type of linker script-defined symbols to char*
ls_data2instructions synthesizes definitions of linker script-defined symbols, and types those definitions as char*
. This means that if those symbols were declared extern with a different type throughout the target codebase, we need to change all expressions of those symbols to have type char*
within the goto functions—as well as in the symbol table.
The 'canonical' way for linker script-defined symbols to be declared within the codebase is as char[] variables, so we take care of converting those into char*s. However, the frontend occasionally converts expressions like &foo into &foo[0] (where foo is an array), so we have to convert expressions like that even when they don't appear in the original codebase.
Note that in general, there is no limitation on what type a linker script-defined symbol should be declared as in the C codebase, because we should only ever be reading its address. So this function is incomplete in that it assumes that linker script-defined symbols have been declared as arrays in the C codebase. If a linker script-defined symbol is declared as some other type, that would likely need some custom logic to be implemented in this function.
char*
. &foo[0]
, &foo
, and foo
, where foo
is a linker-script defined symbol with type array, have been converted to foo
whose type is char*
. Definition at line 187 of file linker_script_merge.cpp.
References char_type(), messaget::debug(), messaget::eom(), messaget::error(), Forall_goto_program_instructions, goto_functionst::function_map, symbol_tablet::get_writeable(), symbol_table_baset::get_writeable_ref(), symbolt::is_extern, pointer_type(), pointerize_subexprs_of(), messaget::mstreamt::source_location, symbol_table_baset::symbols, symbols_to_pointerize(), symbolt::type, and symbolt::value.
Referenced by add_linker_script_definitions().
|
protected |
expr | an expr whose subexpressions may need to be pointerized |
to_pointerize | The symbols that are contained in the subexpressions that we will pointerize. |
linker_values | the names of symbols defined in linker scripts. |
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 pointerize an expression containing a symbol in to_pointerize
, we remove that symbol from to_pointerize
. Therefore, when this function returns, to_pointerize
should be empty. If it is not, then the symbol is contained in a subexpression whose shape is not recognised.
Definition at line 288 of file linker_script_merge.cpp.
References messaget::eom(), messaget::error(), symbol_exprt::get_identifier(), exprt::operands(), replace_expr(), replacement_predicates, and messaget::result().
Referenced by pointerize_linker_defined_symbols().
|
protected |
do the actual replacement of an expr with a new pointer expr
Definition at line 266 of file linker_script_merge.cpp.
References exprt::add_source_location(), messaget::debug(), messaget::eom(), messaget::error(), and exprt::source_location().
Referenced by pointerize_subexprs_of().
|
protected |
fill to_pointerize
with names of linker symbols appearing in expr
Definition at line 332 of file linker_script_merge.cpp.
References symbol_exprt::get_identifier(), exprt::operands(), and to_symbol_expr().
Referenced by pointerize_linker_defined_symbols().
|
protected |
Definition at line 95 of file linker_script_merge.h.
Referenced by add_linker_script_definitions(), and get_linker_script_data().
|
protected |
Definition at line 92 of file linker_script_merge.h.
Referenced by add_linker_script_definitions().
|
protected |
Definition at line 93 of file linker_script_merge.h.
Referenced by add_linker_script_definitions().
|
protected |
Definition at line 94 of file linker_script_merge.h.
Referenced by add_linker_script_definitions().
|
protected |
The "shapes" of expressions to be replaced by a pointer.
Whenever this linker_script_merget encounters an expression expr
in the goto-program—if rp.match(expr)
returns true
for some rp
in this list, and the underlying symbol of expr
is a linker-defined symbol, then expr
will be replaced by a pointer whose value is taken from the value in the linker script.
Definition at line 104 of file linker_script_merge.h.
Referenced by pointerize_subexprs_of().