cprover
linker_script_merge.h
Go to the documentation of this file.
1 
5 #ifndef CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
6 #define CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
7 
8 #include <functional>
9 
10 #include <util/cout_message.h>
11 #include <util/json.h>
12 
13 #include "compile.h"
14 #include "gcc_cmdline.h"
15 
24 {
25 public:
27  const std::string &description,
28  const std::function<const symbol_exprt&(const exprt&)> inner_symbol,
29  const std::function<bool(const exprt&, const namespacet&)> match)
32  _match(match)
33  {}
34 
36  const std::string &description() const
37  {
38  return _description;
39  }
40 
43  const symbol_exprt &inner_symbol(const exprt &expr) const
44  {
45  return _inner_symbol(expr);
46  }
47 
53  const bool match(const exprt &expr, const namespacet &ns) const
54  {
55  return _match(expr, ns);
56  };
57 
58 private:
59  std::string _description;
60  std::function<const symbol_exprt&(const exprt&)> _inner_symbol;
61  std::function<bool(const exprt&, const namespacet&)> _match;
62 };
63 
66 {
67 public:
81 
82  typedef std::map<irep_idt, std::pair<symbol_exprt, exprt>> linker_valuest;
83 
85  compilet &,
86  const std::string &elf_binary,
87  const std::string &goto_binary,
88  const cmdlinet &,
90 
91 protected:
93  const std::string &elf_binary;
94  const std::string &goto_binary;
95  const cmdlinet &cmdline;
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 
125  jsont &data,
126  const std::string &linker_script,
127  goto_programt &gp,
128  symbol_tablet &symbol_table,
129  linker_valuest &linker_values);
130 
160  goto_functionst &goto_functions,
161  symbol_tablet &symbol_table,
162  const linker_valuest &linker_values);
163 
177  exprt &expr,
178  std::list<symbol_exprt> &to_pointerize,
179  const linker_valuest &linker_values,
180  const namespacet &ns);
181 
183  int replace_expr(
184  exprt &old_expr,
185  const linker_valuest &linker_values,
186  const symbol_exprt &old_symbol,
187  const irep_idt &ident,
188  const std::string &shape);
189 
192  const linker_valuest &linker_values,
193  const exprt &expr,
194  std::list<symbol_exprt> &to_pointerize) const;
195 
210  const std::list<irep_idt> &linker_defined_symbols,
211  const linker_valuest &linker_values);
212 
214  int linker_data_is_malformed(const jsont &data) const;
215 };
216 
217 #endif // CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
std::function< bool(const exprt &, const namespacet &)> _match
A special command line object for the gcc-like options.
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
Definition: json.h:23
linker_script_merget(compilet &, const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &, message_handlert &)
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*
std::map< irep_idt, std::pair< symbol_exprt, exprt > > linker_valuest
int pointerize_subexprs_of(exprt &expr, std::list< symbol_exprt > &to_pointerize, const linker_valuest &linker_values, const namespacet &ns)
std::function< const symbol_exprt &(const exprt &)> _inner_symbol
const std::string & elf_binary
Patterns of expressions that should be replaced.
std::list< replacement_predicatet > replacement_predicates
The "shapes" of expressions to be replaced by a pointer.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const std::string & description() const
a textual description of the expression that we&#39;re trying to match
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
const bool match(const exprt &expr, const namespacet &ns) const
Predicate: does the given expression match an interesting pattern?
int linker_data_is_malformed(const jsont &data) const
Validate output of the scripts/ls_parse.py tool.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
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
Compile and link source and object files.
const cmdlinet & cmdline
Base class for all expressions.
Definition: expr.h:42
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
replacement_predicatet(const std::string &description, const std::function< const symbol_exprt &(const exprt &)> inner_symbol, const std::function< bool(const exprt &, const namespacet &)> match)
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
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:90
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&#39;s instructions member.
const std::string & goto_binary
Definition: kdev_t.h:24
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.
Synthesise definitions of symbols that are defined in linker scripts.