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",
142 [](
const exprt &expr)
171 [](
const exprt &expr)
183 [](
const exprt &expr)
197 [](
const exprt &expr)
200 "pointer (does not need pointerizing)",
203 [](
const exprt &expr)
226 log.
debug() <<
"Pointerizing the symbol-table value of symbol " << it->first
235 log.
error() <<
" Could not pointerize '" <<
sym.get_identifier()
236 <<
"' in symbol table entry " << it->first <<
". Pretty:\n"
237 <<
sym.pretty() <<
"\n";
249 std::list<exprt *> expressions = {&instruction.code_nonconst()};
250 if(instruction.has_condition())
251 expressions.push_back(&instruction.condition_nonconst());
266 log.
error() <<
" Could not pointerize '" <<
sym.get_identifier()
267 <<
"' in function " <<
gf.first <<
". Pretty:\n"
268 <<
sym.pretty() <<
"\n";
283 const std::string &
shape)
288 log.
error() <<
"Could not find a new expression for linker script-defined "
294 log.
debug() <<
"Pointerizing linker-defined symbol '" <<
ident
348 for(
const auto &op : expr.
operands())
357 for(
const auto &op : expr.
operands())
417 bool has_end=d[
"has-end-symbol"].is_true();
421 << d[
"start-symbol"].value;
430 log.warning() <<
"Object section '" << d[
"section"].value <<
"' of size "
431 <<
array_size <<
" is too large to model. Truncating to "
444 array_comment <<
"Object section '" << d[
"section"].value <<
"' of size "
474 d[
"start-symbol"].value,
479 auto it = std::find_if(
482 [&d](
const jsont &add) {
483 return add[
"sym"].
value == d[
"start-symbol"].value;
487 log.error() <<
"Start: Could not find address corresponding to symbol '"
488 << d[
"start-symbol"].value <<
"' (start of section)"
496 << d[
"section"].value <<
"'. Original address in object file"
497 <<
" is " << (*it)[
"val"].value;
510 end_sym.is_static_lifetime =
true;
515 d[
"end-symbol"].value,
518 auto entry = std::find_if(
521 [&d](
const jsont &add) {
522 return add[
"sym"].
value == d[
"end-symbol"].value;
526 log.debug() <<
"Could not find address corresponding to symbol '"
527 << d[
"end-symbol"].value <<
"' (end of section)"
534 end_comment <<
"Pointer to end of object section '" << d[
"section"].value
535 <<
"'. Original address in object file"
536 <<
" is " << (*entry)[
"val"].value;
567 <<
"Truncating the value of symbol " << d[
"sym"].value <<
" from "
569 <<
" because it corresponds to the size of a too-large section."
576 loc.
set_comment(
"linker script-defined symbol: char *"+
614 loc.set_comment(
"linker script-defined region:\n"+d[
"commt"].value+
":\n"+
616 f.add_source_location()=loc;
619 i.make_function_call(f);
629 sym.is_lvalue=
sym.is_static_lifetime=
true;
637 loc.
set_comment(
"linker script-defined symbol: char *"+
638 d[
"sym"].value+
"="+
"(char *)"+d[
"val"].value+
"u;");
654 assign.add_source_location()=loc;
666 const std::string &out_file,
672 pair.second.is_extern &&
pair.second.value.is_nil() &&
692 std::vector<std::string> argv=
695 "--script",
cmdline.get_value(
'T'),
696 "--object", out_file,
702 argv.push_back(
"--very-verbose");
704 argv.push_back(
"--verbose");
707 for(std::size_t i=0; i<argv.size(); i++)
727 <<
"' was declared extern but never given a value, even in "
743 <<
"Linker script-defined symbol '" <<
pair.first <<
"' was "
744 <<
"either defined in the C source code, not declared extern in "
745 <<
"the C source code, or does not appear in the C source code"
770 return address.
find(
"val") != address.
end() &&
771 address.
find(
"sym") != address.
end() &&
789 region[
"start"].is_number() &&
region[
"size"].is_number() &&
790 region[
"annot"].is_string() &&
791 region[
"start-symbol"].is_string() &&
792 region[
"section"].is_string() &&
region[
"commt"].is_string() &&
793 ((
region[
"has-end-symbol"].is_true() &&
795 region[
"end-symbol"].is_string()) ||
799 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)