Synthesise definitions of symbols that are defined in linker scripts. More...

#include <linker_script_merge.h>

Collaboration diagram for linker_script_merget:

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 (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, symbol_tablet &symbol_table, linker_valuest &linker_values)
	Write a list of definitions derived from `data` into the `symbol_table`. 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, 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
const std::string &	elf_binary

const std::string &	goto_binary

const cmdlinet &	cmdline

messaget	log

std::list< replacement_predicatet >	replacement_predicates
	The "shapes" of expressions to be replaced by a pointer. More...

Detailed Description

Synthesise definitions of symbols that are defined in linker scripts.

Definition at line 67 of file linker_script_merge.h.

Member Typedef Documentation

◆ linker_valuest

typedef std::map<irep_idt, std::pair<symbol_exprt, exprt> > linker_script_merget::linker_valuest

Definition at line 84 of file linker_script_merge.h.

Constructor & Destructor Documentation

◆ linker_script_merget()

linker_script_merget::linker_script_merget	(	const std::string &	elf_binary,
		const std::string &	goto_binary,
		const cmdlinet &	cmdline,
		message_handlert &	message_handler
	)

Definition at line 125 of file linker_script_merge.cpp.

Member Function Documentation

◆ 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 33 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

Write linker script definitions to linker_data.

Definition at line 665 of file linker_script_merge.cpp.

◆ goto_and_object_mismatch()

int linker_script_merget::goto_and_object_mismatch	(	const std::list< irep_idt > &	linker_defined_symbols,
		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 720 of file linker_script_merge.cpp.

◆ linker_data_is_malformed()

int linker_script_merget::linker_data_is_malformed ( const jsont & data ) const

protected

Validate output of the scripts/ls_parse.py tool.

Definition at line 754 of file linker_script_merge.cpp.

◆ ls_data2instructions()

int linker_script_merget::ls_data2instructions	(	jsont &	data,
		const std::string &	linker_script,
		symbol_tablet &	symbol_table,
		linker_valuest &	linker_values
	)

protected

Write a list of definitions derived from data into the symbol_table.

Precondition: data is in the format verified by linker_data_is_malformed.

Postcondition: For every symbol in data, a declaration and initialization of that symbol is added to symbol_table.; 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 409 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 209 of file linker_script_merge.cpp.

◆ pointerize_subexprs_of()

int linker_script_merget::pointerize_subexprs_of	(	exprt &	expr,
		std::list< symbol_exprt > &	to_pointerize,
		const linker_valuest &	linker_values
	)

protected

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 302 of file linker_script_merge.cpp.

◆ replace_expr()

int linker_script_merget::replace_expr	(	exprt &	old_expr,
		const linker_valuest &	linker_values,
		const symbol_exprt &	old_symbol,
		const irep_idt &	ident,
		const std::string &	shape
	)

protected

do the actual replacement of an expr with a new pointer expr

Definition at line 280 of file linker_script_merge.cpp.

◆ 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

fill to_pointerize with names of linker symbols appearing in expr

Definition at line 345 of file linker_script_merge.cpp.

Member Data Documentation

◆ cmdline

const cmdlinet& linker_script_merget::cmdline

protected

Definition at line 95 of file linker_script_merge.h.

◆ elf_binary

const std::string& linker_script_merget::elf_binary

protected

Definition at line 93 of file linker_script_merge.h.

◆ goto_binary

const std::string& linker_script_merget::goto_binary

protected

Definition at line 94 of file linker_script_merge.h.

◆ log

messaget linker_script_merget::log

protected

Definition at line 96 of file linker_script_merge.h.

◆ replacement_predicates

std::list<replacement_predicatet> linker_script_merget::replacement_predicates

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 105 of file linker_script_merge.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/goto-cc/linker_script_merge.h
/home/runner/work/cbmc/cbmc/src/goto-cc/linker_script_merge.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ linker_valuest

Constructor & Destructor Documentation

◆ linker_script_merget()

Member Function Documentation

◆ add_linker_script_definitions()

◆ get_linker_script_data()

◆ goto_and_object_mismatch()

◆ linker_data_is_malformed()

◆ ls_data2instructions()

◆ pointerize_linker_defined_symbols()

◆ pointerize_subexprs_of()

◆ replace_expr()

◆ symbols_to_pointerize()

Member Data Documentation

◆ cmdline

◆ elf_binary

◆ goto_binary

◆ log

◆ replacement_predicates