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/std_expr.h>
19 #include <util/symbol.h>
20 #include <util/typecheck.h>
21 
23 {
24 private:
25  bool replace_symbol_expr(symbol_exprt &dest) const override;
26 };
27 
28 class linkingt:public typecheckt
29 {
30 public:
32  symbol_table_baset &_main_symbol_table,
33  const symbol_table_baset &_src_symbol_table,
34  message_handlert &_message_handler)
35  : typecheckt(_message_handler),
36  main_symbol_table(_main_symbol_table),
37  src_symbol_table(_src_symbol_table),
38  ns(_main_symbol_table)
39  {
40  }
41 
42  virtual void typecheck();
43 
46 
47 protected:
49  const symbolt &old_symbol,
50  const symbolt &new_symbol);
51 
53  const symbolt &old_symbol,
54  const symbolt &new_symbol);
55 
57  const symbolt &old_symbol,
58  const symbolt &new_symbol)
59  {
60  if(new_symbol.is_type)
61  return needs_renaming_type(old_symbol, new_symbol);
62  else
63  return needs_renaming_non_type(old_symbol, new_symbol);
64  }
65 
66  void do_type_dependencies(std::unordered_set<irep_idt> &);
67 
68  std::unordered_map<irep_idt, irep_idt>
69  rename_symbols(const std::unordered_set<irep_idt> &needs_to_be_renamed);
70  void copy_symbols(const std::unordered_map<irep_idt, irep_idt> &);
71 
73  symbolt &old_symbol,
74  symbolt &new_symbol);
75 
77  symbolt &old_symbol,
78  symbolt &new_symbol);
79 
81  symbolt &old_symbol,
82  symbolt &new_symbol);
83 
84  bool adjust_object_type(
85  const symbolt &old_symbol,
86  const symbolt &new_symbol,
87  bool &set_to_new);
88 
90  {
92  const symbolt &_old_symbol,
93  const symbolt &_new_symbol):
94  old_symbol(_old_symbol),
95  new_symbol(_new_symbol),
96  set_to_new(false)
97  {
98  }
99 
103  std::unordered_set<irep_idt> o_symbols;
104  std::unordered_set<irep_idt> n_symbols;
105  };
106 
108  const typet &type1,
109  const typet &type2,
110  adjust_type_infot &info);
111 
113  symbolt &old_symbol,
114  const symbolt &new_symbol);
115 
116  std::string expr_to_string(
117  const irep_idt &identifier,
118  const exprt &expr) const;
119 
120  std::string type_to_string(
121  const irep_idt &identifier,
122  const typet &type) const;
123 
124  std::string type_to_string_verbose(
125  const symbolt &symbol,
126  const typet &type) const;
127 
129  const symbolt &symbol) const
130  {
131  return type_to_string_verbose(symbol, symbol.type);
132  }
133 
135  const symbolt &old_symbol,
136  const symbolt &new_symbol,
137  const typet &type1,
138  const typet &type2,
139  unsigned depth,
140  exprt &conflict_path);
141 
143  const symbolt &old_symbol,
144  const symbolt &new_symbol,
145  const typet &type1,
146  const typet &type2)
147  {
148  symbol_exprt conflict_path = symbol_exprt::typeless(ID_C_this);
150  old_symbol,
151  new_symbol,
152  type1,
153  type2,
154  10, // somewhat arbitrary limit
155  conflict_path);
156  }
157 
158  void link_error(
159  const symbolt &old_symbol,
160  const symbolt &new_symbol,
161  const std::string &msg);
162 
163  void link_warning(
164  const symbolt &old_symbol,
165  const symbolt &new_symbol,
166  const std::string &msg);
167 
169  const struct_typet &old_type,
170  const struct_typet &new_type);
171 
174 
176 
177  // X -> Y iff Y uses X for new symbol type IDs X and Y
178  typedef std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_byt;
179 
180  irep_idt rename(const irep_idt &);
181 
182  // the new IDs created by renaming
183  std::unordered_set<irep_idt> renamed_ids;
184 };
185 
186 #endif // CPROVER_LINKING_LINKING_CLASS_H
bool replace_symbol_expr(symbol_exprt &dest) const override
Definition: linking.cpp:30
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1100
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition: linking.cpp:995
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1231
rename_symbolt rename_symbol
Definition: linking_class.h:44
void copy_symbols(const std::unordered_map< irep_idt, irep_idt > &)
Definition: linking.cpp:1368
std::string type_to_string_verbose(const symbolt &symbol) const
namespacet ns
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition: linking.cpp:814
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:459
virtual void typecheck()
Definition: linking.cpp:1434
std::unordered_map< irep_idt, irep_idt > rename_symbols(const std::unordered_set< irep_idt > &needs_to_be_renamed)
Definition: linking.cpp:1335
irep_idt rename(const irep_idt &)
Definition: linking.cpp:435
void show_struct_diff(const struct_typet &old_type, const struct_typet &new_type)
symbol_table_baset & main_symbol_table
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > used_byt
std::string expr_to_string(const irep_idt &identifier, const exprt &expr) const
Definition: linking.cpp:50
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:130
void do_type_dependencies(std::unordered_set< irep_idt > &)
Definition: linking.cpp:1290
const symbol_table_baset & src_symbol_table
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:417
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1010
casting_replace_symbolt object_type_updates
Definition: linking_class.h:45
std::string type_to_string(const irep_idt &identifier, const typet &type) const
Definition: linking.cpp:57
linkingt(symbol_table_baset &_main_symbol_table, const symbol_table_baset &_src_symbol_table, message_handlert &_message_handler)
Definition: linking_class.h:31
std::unordered_set< irep_idt > renamed_ids
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1134
std::string type_to_string_verbose(const symbolt &symbol, const typet &type) const
Definition: linking.cpp:78
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking_class.h:56
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:473
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:400
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Replace expression or type symbols by an expression or type, respectively.
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Expression to hold a symbol (variable)
Definition: std_expr.h:80
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
The symbol table base class interface.
Symbol table entry.
Definition: symbol.h:28
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
The type of an expression, extends irept.
Definition: type.h:29
API to expression classes.
adjust_type_infot(const symbolt &_old_symbol, const symbolt &_new_symbol)
Definition: linking_class.h:91
std::unordered_set< irep_idt > o_symbols
std::unordered_set< irep_idt > n_symbols
Symbol table entry.