cprover
Loading...
Searching...
No Matches
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 <functional>
9#include <map>
10
11#include <util/message.h>
12
13class cmdlinet;
14class exprt; // IWYU pragma: keep
15class goto_modelt;
16class symbol_exprt; // IWYU pragma: keep
17class symbol_tablet;
18
27{
28public:
30 const std::string &description,
31 const std::function<const symbol_exprt &(const exprt &)> inner_symbol,
32 const std::function<bool(const exprt &)> match)
34 {}
35
37 const std::string &description() const
38 {
39 return _description;
40 }
41
44 const symbol_exprt &inner_symbol(const exprt &expr) const
45 {
46 return _inner_symbol(expr);
47 }
48
54 bool match(const exprt &expr) const
55 {
56 return _match(expr);
57 };
58
59private:
60 std::string _description;
61 std::function<const symbol_exprt&(const exprt&)> _inner_symbol;
62 std::function<bool(const exprt &)> _match;
63};
64
67{
68public:
82
83 typedef std::map<irep_idt, std::pair<symbol_exprt, exprt>> linker_valuest;
84
86 const std::string &elf_binary,
87 const std::string &goto_binary,
88 const cmdlinet &,
90
91protected:
92 const std::string &elf_binary;
93 const std::string &goto_binary;
96
104 std::list<replacement_predicatet> replacement_predicates;
105
108 std::list<irep_idt> &linker_defined_symbols,
109 const symbol_tablet &symbol_table,
110 const std::string &out_file,
111 const std::string &def_out_file);
112
122 jsont &data,
123 const std::string &linker_script,
124 symbol_tablet &symbol_table,
125 linker_valuest &linker_values);
126
156
169 exprt &expr,
170 std::list<symbol_exprt> &to_pointerize,
171 const linker_valuest &linker_values);
172
174 int replace_expr(
175 exprt &old_expr,
176 const linker_valuest &linker_values,
177 const symbol_exprt &old_symbol,
178 const irep_idt &ident,
179 const std::string &shape);
180
183 const linker_valuest &linker_values,
184 const exprt &expr,
185 std::list<symbol_exprt> &to_pointerize) const;
186
200 const std::list<irep_idt> &linker_defined_symbols,
201 linker_valuest &linker_values);
202
204 int linker_data_is_malformed(const jsont &data) const;
205};
206
207#endif // CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
Definition json.h:27
Synthesise definitions of symbols that are defined in linker scripts.
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
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:113
The symbol table.
Definition kdev_t.h:24