cprover
linking_class.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Linking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_LINKING_LINKING_CLASS_H
13 #define CPROVER_LINKING_LINKING_CLASS_H
14 
15 #include <util/namespace.h>
16 #include <util/rename_symbol.h>
17 #include <util/replace_symbol.h>
18 #include <util/typecheck.h>
19 #include <util/std_expr.h>
20 
22 {
23 private:
24  bool replace_symbol_expr(symbol_exprt &dest) const override;
25 };
26 
27 class linkingt:public typecheckt
28 {
29 public:
31  symbol_table_baset &_main_symbol_table,
32  symbol_table_baset &_src_symbol_table,
33  message_handlert &_message_handler)
34  : typecheckt(_message_handler),
35  main_symbol_table(_main_symbol_table),
36  src_symbol_table(_src_symbol_table),
37  ns(_main_symbol_table)
38  {
39  }
40 
41  virtual void typecheck();
42 
45 
46 protected:
48  const symbolt &old_symbol,
49  const symbolt &new_symbol);
50 
52  const symbolt &old_symbol,
53  const symbolt &new_symbol);
54 
56  const symbolt &old_symbol,
57  const symbolt &new_symbol)
58  {
59  if(new_symbol.is_type)
60  return needs_renaming_type(old_symbol, new_symbol);
61  else
62  return needs_renaming_non_type(old_symbol, new_symbol);
63  }
64 
65  void do_type_dependencies(std::unordered_set<irep_idt> &);
66 
67  void rename_symbols(const std::unordered_set<irep_idt> &needs_to_be_renamed);
68  void copy_symbols();
69 
71  symbolt &old_symbol,
72  symbolt &new_symbol);
73 
75  symbolt &old_symbol,
76  symbolt &new_symbol);
77 
79  symbolt &old_symbol,
80  symbolt &new_symbol);
81 
82  bool adjust_object_type(
83  const symbolt &old_symbol,
84  const symbolt &new_symbol,
85  bool &set_to_new);
86 
88  {
90  const symbolt &_old_symbol,
91  const symbolt &_new_symbol):
92  old_symbol(_old_symbol),
93  new_symbol(_new_symbol),
94  set_to_new(false)
95  {
96  }
97 
101  std::unordered_set<irep_idt> o_symbols;
102  std::unordered_set<irep_idt> n_symbols;
103  };
104 
106  const typet &type1,
107  const typet &type2,
108  adjust_type_infot &info);
109 
111  symbolt &old_symbol,
112  const symbolt &new_symbol);
113 
114  std::string expr_to_string(
115  const irep_idt &identifier,
116  const exprt &expr) const;
117 
118  std::string type_to_string(
119  const irep_idt &identifier,
120  const typet &type) const;
121 
122  std::string type_to_string_verbose(
123  const symbolt &symbol,
124  const typet &type) const;
125 
127  const symbolt &symbol) const
128  {
129  return type_to_string_verbose(symbol, symbol.type);
130  }
131 
133  const symbolt &old_symbol,
134  const symbolt &new_symbol,
135  const typet &type1,
136  const typet &type2,
137  unsigned depth,
138  exprt &conflict_path);
139 
141  const symbolt &old_symbol,
142  const symbolt &new_symbol,
143  const typet &type1,
144  const typet &type2)
145  {
146  symbol_exprt conflict_path = symbol_exprt::typeless(ID_C_this);
148  old_symbol,
149  new_symbol,
150  type1,
151  type2,
152  10, // somewhat arbitrary limit
153  conflict_path);
154  }
155 
156  void link_error(
157  const symbolt &old_symbol,
158  const symbolt &new_symbol,
159  const std::string &msg);
160 
161  void link_warning(
162  const symbolt &old_symbol,
163  const symbolt &new_symbol,
164  const std::string &msg);
165 
167  const struct_typet &old_type,
168  const struct_typet &new_type);
169 
172 
174 
175  // X -> Y iff Y uses X for new symbol type IDs X and Y
176  typedef std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_byt;
177 
179 
180  // the new IDs created by renaming
181  std::unordered_set<irep_idt> renamed_ids;
182 };
183 
184 #endif // CPROVER_LINKING_LINKING_CLASS_H
linkingt::needs_renaming_type
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1212
linkingt::adjust_object_type
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition: linking.cpp:975
linkingt::src_symbol_table
symbol_table_baset & src_symbol_table
Definition: linking_class.h:171
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
casting_replace_symbolt
Definition: linking_class.h:22
linkingt::adjust_type_infot
Definition: linking_class.h:88
linkingt::needs_renaming
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking_class.h:55
linkingt::typecheck
virtual void typecheck()
Definition: linking.cpp:1405
linkingt::adjust_type_infot::new_symbol
const symbolt & new_symbol
Definition: linking_class.h:99
linkingt::copy_symbols
void copy_symbols()
Definition: linking.cpp:1343
linkingt::object_type_updates
casting_replace_symbolt object_type_updates
Definition: linking_class.h:44
typet
The type of an expression, extends irept.
Definition: type.h:29
linkingt::type_to_string_verbose
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
Definition: linking.cpp:71
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
replace_symbol.h
linkingt::type_to_string
std::string type_to_string(const irep_idt &identifier, const typet &type) const
Definition: linking.cpp:50
linkingt::needs_renaming_non_type
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:441
exprt
Base class for all expressions.
Definition: expr.h:53
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
rename_symbol.h
namespace.h
linkingt::link_warning
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:399
linkingt::type_to_string_verbose
std::string type_to_string_verbose(const symbolt &symbol) const
Definition: linking_class.h:126
linkingt::duplicate_code_symbol
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:455
linkingt::main_symbol_table
symbol_table_baset & main_symbol_table
Definition: linking_class.h:170
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
linkingt::adjust_object_type_rec
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition: linking.cpp:796
linkingt::used_byt
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > used_byt
Definition: linking_class.h:176
linkingt::show_struct_diff
void show_struct_diff(const struct_typet &old_type, const struct_typet &new_type)
linkingt::do_type_dependencies
void do_type_dependencies(std::unordered_set< irep_idt > &)
Definition: linking.cpp:1268
typecheck.h
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
casting_replace_symbolt::replace_symbol_expr
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: linking.cpp:28
linkingt
Definition: linking_class.h:28
linkingt::duplicate_non_type_symbol
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1084
message_handlert
Definition: message.h:28
linkingt::rename
irep_idt rename(irep_idt)
Definition: linking.cpp:417
linkingt::detailed_conflict_report_rec
void detailed_conflict_report_rec(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2, unsigned depth, exprt &conflict_path)
Definition: linking.cpp:121
linkingt::duplicate_object_symbol
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:990
linkingt::expr_to_string
std::string expr_to_string(const irep_idt &identifier, const exprt &expr) const
Definition: linking.cpp:43
linkingt::rename_symbol
rename_symbolt rename_symbol
Definition: linking_class.h:43
linkingt::link_error
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:382
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
linkingt::adjust_type_infot::set_to_new
bool set_to_new
Definition: linking_class.h:100
linkingt::duplicate_type_symbol
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1118
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
linkingt::linkingt
linkingt(symbol_table_baset &_main_symbol_table, symbol_table_baset &_src_symbol_table, message_handlert &_message_handler)
Definition: linking_class.h:30
rename_symbolt
Definition: rename_symbol.h:26
linkingt::detailed_conflict_report
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
Definition: linking_class.h:140
linkingt::renamed_ids
std::unordered_set< irep_idt > renamed_ids
Definition: linking_class.h:181
linkingt::adjust_type_infot::n_symbols
std::unordered_set< irep_idt > n_symbols
Definition: linking_class.h:102
linkingt::adjust_type_infot::old_symbol
const symbolt & old_symbol
Definition: linking_class.h:98
typecheckt
Definition: typecheck.h:17
linkingt::ns
namespacet ns
Definition: linking_class.h:173
std_expr.h
API to expression classes.
linkingt::adjust_type_infot::o_symbols
std::unordered_set< irep_idt > o_symbols
Definition: linking_class.h:101
linkingt::adjust_type_infot::adjust_type_infot
adjust_type_infot(const symbolt &_old_symbol, const symbolt &_new_symbol)
Definition: linking_class.h:89
linkingt::rename_symbols
void rename_symbols(const std::unordered_set< irep_idt > &needs_to_be_renamed)
Definition: linking.cpp:1313
replace_symbolt
Replace expression or type symbols by an expression or type, respectively.
Definition: replace_symbol.h:25