CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
linker_script_merge.h
Go to the documentation of this file.
1
4
5#ifndef CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
6#define CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
7
8#include <util/message.h>
9
10#include <functional>
11#include <list>
12#include <map>
13
14class cmdlinet;
15class exprt; // IWYU pragma: keep
16class goto_modelt;
17class symbol_exprt; // IWYU pragma: keep
18class symbol_tablet;
19
28{
29public:
31 const std::string &description,
32 const std::function<const symbol_exprt &(const exprt &)> inner_symbol,
33 const std::function<bool(const exprt &)> match)
35 {}
36
38 const std::string &description() const
39 {
40 return _description;
41 }
42
45 const symbol_exprt &inner_symbol(const exprt &expr) const
46 {
47 return _inner_symbol(expr);
48 }
49
55 bool match(const exprt &expr) const
56 {
57 return _match(expr);
58 };
59
60private:
61 std::string _description;
62 std::function<const symbol_exprt&(const exprt&)> _inner_symbol;
63 std::function<bool(const exprt &)> _match;
64};
65
68{
69public:
83
84 typedef std::map<irep_idt, std::pair<symbol_exprt, exprt>> linker_valuest;
85
87 const std::string &elf_binary,
88 const std::string &goto_binary,
89 const cmdlinet &,
91
92protected:
93 const std::string &elf_binary;
94 const std::string &goto_binary;
97
105 std::list<replacement_predicatet> replacement_predicates;
106
109 std::list<irep_idt> &linker_defined_symbols,
110 const symbol_tablet &symbol_table,
111 const std::string &out_file,
112 const std::string &def_out_file);
113
123 jsont &data,
124 const std::string &linker_script,
125 symbol_tablet &symbol_table,
127
157
170 exprt &expr,
171 std::list<symbol_exprt> &to_pointerize,
173
175 int replace_expr(
178 const symbol_exprt &old_symbol,
179 const irep_idt &ident,
180 const std::string &shape);
181
185 const exprt &expr,
186 std::list<symbol_exprt> &to_pointerize) const;
187
201 const std::list<irep_idt> &linker_defined_symbols,
203
205 int linker_data_is_malformed(const jsont &data) const;
206};
207
208#endif // CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
Definition json.h:27
Synthesise definitions of symbols that are defined in linker scripts.
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Patterns of expressions that should be replaced.
bool match(const exprt &expr) const
Predicate: does the given expression match an interesting pattern?
std::function< const symbol_exprt &(const exprt &)> _inner_symbol
std::function< bool(const exprt &)> _match
replacement_predicatet(const std::string &description, const std::function< const symbol_exprt &(const exprt &)> inner_symbol, const std::function< bool(const exprt &)> match)
const std::string & description() const
a textual description of the expression that we're trying to match
const symbol_exprt & inner_symbol(const exprt &expr) const
Return the underlying symbol of the matched expression.
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table.