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 
21 class linkingt:public typecheckt
22 {
23 public:
25  symbol_tablet &_main_symbol_table,
26  symbol_tablet &_src_symbol_table,
27  message_handlert &_message_handler):
28  typecheckt(_message_handler),
29  main_symbol_table(_main_symbol_table),
30  src_symbol_table(_src_symbol_table),
31  ns(_main_symbol_table)
32  {
33  }
34 
35  virtual void typecheck();
36 
39 
40 protected:
42  const symbolt &old_symbol,
43  const symbolt &new_symbol);
44 
46  const symbolt &old_symbol,
47  const symbolt &new_symbol);
48 
50  const symbolt &old_symbol,
51  const symbolt &new_symbol)
52  {
53  if(new_symbol.is_type)
54  return needs_renaming_type(old_symbol, new_symbol);
55  else
56  return needs_renaming_non_type(old_symbol, new_symbol);
57  }
58 
59  void do_type_dependencies(std::unordered_set<irep_idt> &);
60 
61  void rename_symbols(const std::unordered_set<irep_idt> &needs_to_be_renamed);
62  void copy_symbols();
63 
65  symbolt &old_symbol,
66  symbolt &new_symbol);
67 
69  symbolt &old_symbol,
70  symbolt &new_symbol);
71 
73  symbolt &old_symbol,
74  symbolt &new_symbol);
75 
76  bool adjust_object_type(
77  const symbolt &old_symbol,
78  const symbolt &new_symbol,
79  bool &set_to_new);
80 
82  {
84  const symbolt &_old_symbol,
85  const symbolt &_new_symbol):
86  old_symbol(_old_symbol),
87  new_symbol(_new_symbol),
88  set_to_new(false)
89  {
90  }
91 
94  bool set_to_new;
95  std::unordered_set<irep_idt> o_symbols;
96  std::unordered_set<irep_idt> n_symbols;
97  };
98 
100  const typet &type1,
101  const typet &type2,
102  adjust_type_infot &info);
103 
105  symbolt &old_symbol,
106  const symbolt &new_symbol);
107 
108  std::string expr_to_string(
109  const namespacet &ns,
110  const irep_idt &identifier,
111  const exprt &expr) const;
112 
113  std::string type_to_string(
114  const namespacet &ns,
115  const irep_idt &identifier,
116  const typet &type) const;
117 
118  std::string type_to_string_verbose(
119  const namespacet &ns,
120  const symbolt &symbol,
121  const typet &type) const;
122 
124  const namespacet &ns,
125  const symbolt &symbol) const
126  {
127  return type_to_string_verbose(ns, symbol, symbol.type);
128  }
129 
131  const symbolt &old_symbol,
132  const symbolt &new_symbol,
133  const typet &type1,
134  const typet &type2,
135  unsigned depth,
136  exprt &conflict_path);
137 
139  const symbolt &old_symbol,
140  const symbolt &new_symbol,
141  const typet &type1,
142  const typet &type2)
143  {
144  symbol_exprt conflict_path(ID_C_this);
146  old_symbol,
147  new_symbol,
148  type1,
149  type2,
150  10, // somewhat arbitrary limit
151  conflict_path);
152  }
153 
154  void link_error(
155  const symbolt &old_symbol,
156  const symbolt &new_symbol,
157  const std::string &msg);
158 
159  void link_warning(
160  const symbolt &old_symbol,
161  const symbolt &new_symbol,
162  const std::string &msg);
163 
164  void show_struct_diff(
165  const struct_typet &old_type,
166  const struct_typet &new_type);
167 
170 
172 
173  // X -> Y iff Y uses X for new symbol type IDs X and Y
174  typedef std::unordered_map<irep_idt, std::unordered_set<irep_idt>> used_byt;
175 
177 
178  // the new IDs created by renaming
179  std::unordered_set<irep_idt> renamed_ids;
180 };
181 
182 #endif // CPROVER_LINKING_LINKING_CLASS_H
void do_type_dependencies(std::unordered_set< irep_idt > &)
Definition: linking.cpp:1208
The type of an expression.
Definition: type.h:22
virtual void typecheck()
Definition: linking.cpp:1345
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:367
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
symbol_tablet & main_symbol_table
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:385
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
std::string expr_to_string(const namespacet &ns, const irep_idt &identifier, const exprt &expr) const
Definition: linking.cpp:27
Structure type.
Definition: std_types.h:297
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:113
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:427
const symbolt & new_symbol
Definition: linking_class.h:93
std::unordered_map< irep_idt, std::unordered_set< irep_idt > > used_byt
std::unordered_set< irep_idt > n_symbols
Definition: linking_class.h:96
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking_class.h:49
void show_struct_diff(const struct_typet &old_type, const struct_typet &new_type)
std::unordered_set< irep_idt > renamed_ids
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const symbolt & old_symbol
Definition: linking_class.h:92
adjust_type_infot(const symbolt &_old_symbol, const symbolt &_new_symbol)
Definition: linking_class.h:83
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1164
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
namespacet ns
irep_idt rename(irep_idt)
Definition: linking.cpp:403
std::string type_to_string(const namespacet &ns, const irep_idt &identifier, const typet &type) const
Definition: linking.cpp:35
replace_symbolt object_type_updates
Definition: linking_class.h:38
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:441
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition: linking.cpp:785
typet type
Type of symbol.
Definition: symbol.h:34
symbol_tablet & src_symbol_table
Base class for all expressions.
Definition: expr.h:42
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1048
std::string type_to_string_verbose(const namespacet &ns, const symbolt &symbol) const
void copy_symbols()
Definition: linking.cpp:1283
rename_symbolt rename_symbol
Definition: linking_class.h:37
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:959
linkingt(symbol_tablet &_main_symbol_table, symbol_tablet &_src_symbol_table, message_handlert &_message_handler)
Definition: linking_class.h:24
std::string type_to_string_verbose(const namespacet &ns, const symbolt &symbol, const typet &type) const
Definition: linking.cpp:59
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition: linking.cpp:944
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::unordered_set< irep_idt > o_symbols
Definition: linking_class.h:95
bool is_type
Definition: symbol.h:63
void rename_symbols(const std::unordered_set< irep_idt > &needs_to_be_renamed)
Definition: linking.cpp:1253
void duplicate_type_symbol(symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1082