Synthesise definitions of symbols that are defined in linker scripts.
More...
#include <linker_script_merge.h>
|
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_modelt &, const linker_valuest &) |
| 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) |
|
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...
|
|
Synthesise definitions of symbols that are defined in linker scripts.
Definition at line 62 of file linker_script_merge.h.
◆ linker_valuest
◆ linker_script_merget()
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 |
|
) |
| |
◆ add_linker_script_definitions()
int linker_script_merget::add_linker_script_definitions |
( |
| ) |
|
Add values of linkerscript-defined symbols to the goto-binary.
- Precondition
- There is a single output file in each of
elf_binaries
and goto_binaries
, and the codebase is being linked with a custom linker script passed to the compiler with the -T
option.
- Postcondition
- The
__CPROVER_initialize
function contains synthesized definitions for all symbols that are declared in the C codebase and defined in the linker script.
-
All uses of these symbols throughout the code base are re-typed to match the type of the synthesized definitions.
-
The
__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.
◆ get_linker_script_data()
int linker_script_merget::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 |
|
) |
| |
|
protected |
◆ goto_and_object_mismatch()
int linker_script_merget::goto_and_object_mismatch |
( |
const std::list< irep_idt > & |
linker_defined_symbols, |
|
|
const linker_valuest & |
linker_values |
|
) |
| |
|
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.
- Parameters
-
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. |
- Returns
1
if there is some mismatch between the list and map, 0
if everything is OK.
Definition at line 722 of file linker_script_merge.cpp.
◆ linker_data_is_malformed()
int linker_script_merget::linker_data_is_malformed |
( |
const jsont & |
data | ) |
const |
|
protected |
◆ ls_data2instructions()
Write a list of definitions derived from data
into gp's instructions
member.
- Precondition
data
is in the format verified by linker_data_is_malformed.
- Postcondition
- For every memory region in
data
, a function call to __CPROVER_allocated_memory
is prepended to initialize_instructions
.
-
For every symbol in
data
, a declaration and initialization of that symbol is prepended to initialize_instructions
.
-
Every symbol in
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 405 of file linker_script_merge.cpp.
◆ pointerize_linker_defined_symbols()
int linker_script_merget::pointerize_linker_defined_symbols |
( |
goto_modelt & |
goto_model, |
|
|
const linker_valuest & |
linker_values |
|
) |
| |
|
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.
- Postcondition
- The types of linker-script defined symbols in the symbol table have been converted to
char*
.
-
Expressions of the shape
&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 200 of file linker_script_merge.cpp.
◆ pointerize_subexprs_of()
- Parameters
-
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. |
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 298 of file linker_script_merge.cpp.
◆ replace_expr()
◆ symbols_to_pointerize()
void linker_script_merget::symbols_to_pointerize |
( |
const linker_valuest & |
linker_values, |
|
|
const exprt & |
expr, |
|
|
std::list< symbol_exprt > & |
to_pointerize |
|
) |
| const |
|
protected |
◆ cmdline
const cmdlinet& linker_script_merget::cmdline |
|
protected |
◆ compiler
compilet& linker_script_merget::compiler |
|
protected |
◆ elf_binary
const std::string& linker_script_merget::elf_binary |
|
protected |
◆ goto_binary
const std::string& linker_script_merget::goto_binary |
|
protected |
◆ replacement_predicates
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 101 of file linker_script_merge.h.
The documentation for this class was generated from the following files: