cprover
linker_script_merget Class Reference

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

#include <linker_script_merge.h>

Inheritance diagram for linker_script_merget:
[legend]
Collaboration diagram for linker_script_merget:
[legend]

Public Types

typedef std::map< irep_idt, std::pair< symbol_exprt, exprt > > linker_valuest
 
- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

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 &)
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

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

compiletcompiler
 
const std::string & elf_binary
 
const std::string & goto_binary
 
const cmdlinetcmdline
 
std::list< replacement_predicatetreplacement_predicates
 The "shapes" of expressions to be replaced by a pointer. More...
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Additional Inherited Members

- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Detailed Description

Synthesise definitions of symbols that are defined in linker scripts.

Definition at line 65 of file linker_script_merge.h.

Member Typedef Documentation

◆ linker_valuest

Definition at line 82 of file linker_script_merge.h.

Constructor & Destructor Documentation

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

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 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().

◆ 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_symbolsthe list of symbols that were extern with no value in the goto-program)
linker_valuesmap 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 706 of file linker_script_merge.cpp.

References messaget::eom(), and messaget::error().

Referenced by add_linker_script_definitions().

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

References is_false().

Referenced by add_linker_script_definitions().

◆ ls_data2instructions()

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

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 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().

◆ pointerize_linker_defined_symbols()

int linker_script_merget::pointerize_linker_defined_symbols ( goto_functionst goto_functions,
symbol_tablet symbol_table,
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 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().

◆ pointerize_subexprs_of()

int linker_script_merget::pointerize_subexprs_of ( exprt expr,
std::list< symbol_exprt > &  to_pointerize,
const linker_valuest linker_values,
const namespacet ns 
)
protected
Parameters
expran expr whose subexpressions may need to be pointerized
to_pointerizeThe symbols that are contained in the subexpressions that we will pointerize.
linker_valuesthe names of symbols defined in linker scripts.
nsa 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().

◆ 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 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().

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

References symbol_exprt::get_identifier(), exprt::operands(), and to_symbol_expr().

Referenced by pointerize_linker_defined_symbols().

Member Data Documentation

◆ cmdline

const cmdlinet& linker_script_merget::cmdline
protected

Definition at line 95 of file linker_script_merge.h.

Referenced by add_linker_script_definitions(), and get_linker_script_data().

◆ compiler

compilet& linker_script_merget::compiler
protected

Definition at line 92 of file linker_script_merge.h.

Referenced by add_linker_script_definitions().

◆ elf_binary

const std::string& linker_script_merget::elf_binary
protected

Definition at line 93 of file linker_script_merge.h.

Referenced by add_linker_script_definitions().

◆ goto_binary

const std::string& linker_script_merget::goto_binary
protected

Definition at line 94 of file linker_script_merge.h.

Referenced by add_linker_script_definitions().

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

Referenced by pointerize_subexprs_of().


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