43 log.
error() <<
"Unable to read goto binary for linker script merging"
83 log.
error() <<
"Could not add linkerscript defs to symbol table"
105 log.
error() <<
"Could not pointerize all linker-defined expressions"
113 cmdline.isset(
"validate-goto-model"),
118 log.
error() <<
"Could not write linkerscript-augmented binary"
126 const std::string &elf_binary,
127 const std::string &goto_binary,
130 : elf_binary(elf_binary),
131 goto_binary(goto_binary),
133 log(message_handler),
134 replacement_predicates(
136 "address of array's first member",
141 [](
const exprt &expr) {
170 [](
const exprt &expr) {
182 [](
const exprt &expr) {
196 [](
const exprt &expr) {
200 "pointer (does not need pointerizing)",
204 [](
const exprt &expr) {
228 log.
debug() <<
"Pointerizing the symbol-table value of symbol " << it->first
237 log.
error() <<
" Could not pointerize '" <<
sym.get_identifier()
238 <<
"' in symbol table entry " << it->first <<
". Pretty:\n"
239 <<
sym.pretty() <<
"\n";
251 std::list<exprt *> expressions = {&instruction.code_nonconst()};
252 if(instruction.has_condition())
253 expressions.push_back(&instruction.condition_nonconst());
268 log.
error() <<
" Could not pointerize '" <<
sym.get_identifier()
269 <<
"' in function " <<
gf.first <<
". Pretty:\n"
270 <<
sym.pretty() <<
"\n";
285 const std::string &
shape)
290 log.
error() <<
"Could not find a new expression for linker script-defined "
296 log.
debug() <<
"Pointerizing linker-defined symbol '" <<
ident
350 for(
const auto &op : expr.
operands())
359 for(
const auto &op : expr.
operands())
419 bool has_end=d[
"has-end-symbol"].is_true();
423 << d[
"start-symbol"].value;
432 log.warning() <<
"Object section '" << d[
"section"].value <<
"' of size "
433 <<
array_size <<
" is too large to model. Truncating to "
446 array_comment <<
"Object section '" << d[
"section"].value <<
"' of size "
476 d[
"start-symbol"].value,
481 auto it = std::find_if(
484 [&d](
const jsont &add) {
485 return add[
"sym"].
value == d[
"start-symbol"].value;
489 log.error() <<
"Start: Could not find address corresponding to symbol '"
490 << d[
"start-symbol"].value <<
"' (start of section)"
498 << d[
"section"].value <<
"'. Original address in object file"
499 <<
" is " << (*it)[
"val"].value;
512 end_sym.is_static_lifetime =
true;
517 d[
"end-symbol"].value,
520 auto entry = std::find_if(
523 [&d](
const jsont &add) {
524 return add[
"sym"].
value == d[
"end-symbol"].value;
528 log.debug() <<
"Could not find address corresponding to symbol '"
529 << d[
"end-symbol"].value <<
"' (end of section)"
536 end_comment <<
"Pointer to end of object section '" << d[
"section"].value
537 <<
"'. Original address in object file"
538 <<
" is " << (*entry)[
"val"].value;
569 <<
"Truncating the value of symbol " << d[
"sym"].value <<
" from "
571 <<
" because it corresponds to the size of a too-large section."
578 loc.
set_comment(
"linker script-defined symbol: char *"+
616 loc.set_comment(
"linker script-defined region:\n"+d[
"commt"].value+
":\n"+
618 f.add_source_location()=loc;
621 i.make_function_call(f);
631 sym.is_lvalue=
sym.is_static_lifetime=
true;
639 loc.
set_comment(
"linker script-defined symbol: char *"+
640 d[
"sym"].value+
"="+
"(char *)"+d[
"val"].value+
"u;");
656 assign.add_source_location()=loc;
668 const std::string &out_file,
674 pair.second.is_extern &&
pair.second.value.is_nil() &&
694 std::vector<std::string> argv=
697 "--script",
cmdline.get_value(
'T'),
698 "--object", out_file,
704 argv.push_back(
"--very-verbose");
706 argv.push_back(
"--verbose");
709 for(std::size_t i=0; i<argv.size(); i++)
729 <<
"' was declared extern but never given a value, even in "
745 <<
"Linker script-defined symbol '" <<
pair.first <<
"' was "
746 <<
"either defined in the C source code, not declared extern in "
747 <<
"the C source code, or does not appear in the C source code"
772 return address.
find(
"val") != address.
end() &&
773 address.
find(
"sym") != address.
end() &&
791 region[
"start"].is_number() &&
region[
"size"].is_number() &&
792 region[
"annot"].is_string() &&
793 region[
"start-symbol"].is_string() &&
794 region[
"section"].is_string() &&
region[
"commt"].is_string() &&
795 ((
region[
"has-end-symbol"].is_true() &&
797 region[
"end-symbol"].is_string()) ||
801 region[
"size-symbol"].is_string()));
std::string array_name(const namespacet &ns, const exprt &expr)
unsignedbv_typet unsigned_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet char_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A goto_instruction_codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
static bool write_bin_object_file(const std::string &file_name, const goto_modelt &src_goto_model, bool validate_goto_model, message_handlert &message_handler)
Writes the goto functions of src_goto_model to a binary format object file.
A constant literal expression.
void set_value(const irep_idt &value)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
const source_locationt & source_location() const
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
std::list< instructiont > instructionst
const irep_idt & id() const
iterator find(const std::string &key)
void output(std::ostream &out) const
linker_script_merget(const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &, message_handlert &)
int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &)
convert the type of linker script-defined symbols to char*
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
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
const std::string & elf_binary
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.
std::map< irep_idt, std::pair< symbol_exprt, exprt > > linker_valuest
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
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.
int pointerize_subexprs_of(exprt &expr, std::list< symbol_exprt > &to_pointerize, const linker_valuest &linker_values)
std::list< replacement_predicatet > replacement_predicates
The "shapes" of expressions to be replaced by a pointer.
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
int linker_data_is_malformed(const jsont &data) const
Validate output of the scripts/ls_parse.py tool.
const std::string & goto_binary
unsigned get_verbosity() const
source_locationt source_location
message_handlert & get_message_handler()
mstreamt & warning() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
The plus expression Associativity is not specified.
Patterns of expressions that should be replaced.
void set_comment(const irep_idt &comment)
void set_file(const irep_idt &file)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
virtual iteratort begin() override
virtual iteratort end() override
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
exprt value
Initial value of symbol.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
Compile and link source and object files.
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
json_objectt & to_json_object(jsont &json)
json_arrayt & to_json_array(jsont &json)
bool parse_json(std::istream &in, const std::string &filename, message_handlert &message_handler, jsont &dest)
Merge linker script-defined symbols into a goto-program.
bool is_false(const literalt &l)
Magic numbers used throughout the codebase.
const std::size_t MAX_FLATTENED_ARRAY_SIZE
const mp_integer string2integer(const std::string &n, unsigned base)
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
static bool read_goto_binary(const std::string &filename, symbol_tablet &, goto_functionst &, message_handlert &)
Read a goto binary from a file, but do not update config.
int run(const std::string &what, const std::vector< std::string > &argv)
#define CHECK_RETURN(CONDITION)
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
unsigned safe_string2unsigned(const std::string &str, int base)
void * memset(void *s, int c, size_t n)
void * memcpy(void *dst, const void *src, size_t n)
static bool failed(bool error_indicator)