CBMC
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 #include <map>
10 
11 #include <util/message.h>
12 
13 class cmdlinet;
14 class exprt;
15 class goto_modelt;
16 class goto_programt;
17 class symbol_exprt;
18 class symbol_tablet;
19 
28 {
29 public:
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 
60 private:
61  std::string _description;
62  std::function<const symbol_exprt&(const exprt&)> _inner_symbol;
63  std::function<bool(const exprt &)> _match;
64 };
65 
68 {
69 public:
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 
92 protected:
93  const std::string &elf_binary;
94  const std::string &goto_binary;
95  const cmdlinet &cmdline;
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,
126  linker_valuest &linker_values);
127 
157 
170  exprt &expr,
171  std::list<symbol_exprt> &to_pointerize,
172  const linker_valuest &linker_values);
173 
175  int replace_expr(
176  exprt &old_expr,
177  const linker_valuest &linker_values,
178  const symbol_exprt &old_symbol,
179  const irep_idt &ident,
180  const std::string &shape);
181 
184  const linker_valuest &linker_values,
185  const exprt &expr,
186  std::list<symbol_exprt> &to_pointerize) const;
187 
201  const std::list<irep_idt> &linker_defined_symbols,
202  const linker_valuest &linker_values);
203 
205  int linker_data_is_malformed(const jsont &data) const;
206 };
207 
208 #endif // CPROVER_GOTO_CC_LINKER_SCRIPT_MERGE_H
replacement_predicatet::_match
std::function< bool(const exprt &)> _match
Definition: linker_script_merge.h:63
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
linker_script_merget::linker_valuest
std::map< irep_idt, std::pair< symbol_exprt, exprt > > linker_valuest
Definition: linker_script_merge.h:84
linker_script_merget::get_linker_script_data
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.
Definition: linker_script_merge.cpp:682
replacement_predicatet::replacement_predicatet
replacement_predicatet(const std::string &description, const std::function< const symbol_exprt &(const exprt &)> inner_symbol, const std::function< bool(const exprt &)> match)
Definition: linker_script_merge.h:30
replacement_predicatet::match
bool match(const exprt &expr) const
Predicate: does the given expression match an interesting pattern?
Definition: linker_script_merge.h:55
linker_script_merget::add_linker_script_definitions
int add_linker_script_definitions()
Add values of linkerscript-defined symbols to the goto-binary.
Definition: linker_script_merge.cpp:34
linker_script_merget::ls_data2instructions
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.
Definition: linker_script_merge.cpp:419
exprt
Base class for all expressions.
Definition: expr.h:55
linker_script_merget::replace_expr
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
Definition: linker_script_merge.cpp:290
goto_modelt
Definition: goto_model.h:25
linker_script_merget::log
messaget log
Definition: linker_script_merge.h:96
linker_script_merget
Synthesise definitions of symbols that are defined in linker scripts.
Definition: linker_script_merge.h:67
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
replacement_predicatet::description
const std::string & description() const
a textual description of the expression that we're trying to match
Definition: linker_script_merge.h:38
jsont
Definition: json.h:26
linker_script_merget::pointerize_subexprs_of
int pointerize_subexprs_of(exprt &expr, std::list< symbol_exprt > &to_pointerize, const linker_valuest &linker_values)
Definition: linker_script_merge.cpp:312
linker_script_merget::goto_binary
const std::string & goto_binary
Definition: linker_script_merge.h:94
replacement_predicatet
Patterns of expressions that should be replaced.
Definition: linker_script_merge.h:27
linker_script_merget::linker_data_is_malformed
int linker_data_is_malformed(const jsont &data) const
Validate output of the scripts/ls_parse.py tool.
Definition: linker_script_merge.cpp:768
cmdlinet
Definition: cmdline.h:20
linker_script_merget::cmdline
const cmdlinet & cmdline
Definition: linker_script_merge.h:95
linker_script_merget::symbols_to_pointerize
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: linker_script_merge.cpp:355
linker_script_merget::elf_binary
const std::string & elf_binary
Definition: linker_script_merge.h:93
message_handlert
Definition: message.h:27
replacement_predicatet::_inner_symbol
std::function< const symbol_exprt &(const exprt &)> _inner_symbol
Definition: linker_script_merge.h:62
linker_script_merget::linker_script_merget
linker_script_merget(const std::string &elf_binary, const std::string &goto_binary, const cmdlinet &, message_handlert &)
Definition: linker_script_merge.cpp:135
linker_script_merget::goto_and_object_mismatch
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
Definition: linker_script_merge.cpp:737
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
replacement_predicatet::_description
std::string _description
Definition: linker_script_merge.h:58
linker_script_merget::replacement_predicates
std::list< replacement_predicatet > replacement_predicates
The "shapes" of expressions to be replaced by a pointer.
Definition: linker_script_merge.h:105
message.h
linker_script_merget::pointerize_linker_defined_symbols
int pointerize_linker_defined_symbols(goto_modelt &, const linker_valuest &)
convert the type of linker script-defined symbols to char*
Definition: linker_script_merge.cpp:219
replacement_predicatet::inner_symbol
const symbol_exprt & inner_symbol(const exprt &expr) const
Return the underlying symbol of the matched expression.
Definition: linker_script_merge.h:45