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:
41  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
42 
44  const symbolt &old_symbol,
45  const symbolt &new_symbol);
46 
48  const symbolt &old_symbol,
49  const symbolt &new_symbol);
50 
52  const symbolt &old_symbol,
53  const symbolt &new_symbol)
54  {
55  if(new_symbol.is_type)
56  return needs_renaming_type(old_symbol, new_symbol);
57  else
58  return needs_renaming_non_type(old_symbol, new_symbol);
59  }
60 
62 
63  void rename_symbols(const id_sett &needs_to_be_renamed);
64  void copy_symbols();
65 
67  symbolt &old_symbol,
68  symbolt &new_symbol);
69 
71  symbolt &old_symbol,
72  symbolt &new_symbol);
73 
75  symbolt &old_symbol,
76  symbolt &new_symbol);
77 
78  bool adjust_object_type(
79  const symbolt &old_symbol,
80  const symbolt &new_symbol,
81  bool &set_to_new);
82 
84  {
86  const symbolt &_old_symbol,
87  const symbolt &_new_symbol):
88  old_symbol(_old_symbol),
89  new_symbol(_new_symbol),
90  set_to_new(false)
91  {
92  }
93 
96  bool set_to_new;
99  };
100 
102  const typet &type1,
103  const typet &type2,
104  adjust_type_infot &info);
105 
107  symbolt &old_symbol,
108  symbolt &new_symbol);
109 
110  std::string expr_to_string(
111  const namespacet &ns,
112  const irep_idt &identifier,
113  const exprt &expr) const;
114 
115  std::string type_to_string(
116  const namespacet &ns,
117  const irep_idt &identifier,
118  const typet &type) const;
119 
120  std::string type_to_string_verbose(
121  const namespacet &ns,
122  const symbolt &symbol,
123  const typet &type) const;
124 
126  const namespacet &ns,
127  const symbolt &symbol) const
128  {
129  return type_to_string_verbose(ns, 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(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 
166  void show_struct_diff(
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, id_sett, irep_id_hash> used_byt;
177 
179 
180  // the new IDs created by renaming
182 };
183 
184 #endif // CPROVER_LINKING_LINKING_CLASS_H
The type of an expression.
Definition: type.h:20
virtual void typecheck()
Definition: linking.cpp:1300
std::unordered_map< irep_idt, id_sett, irep_id_hash > used_byt
void link_error(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:369
void detailed_conflict_report(const symbolt &old_symbol, const symbolt &new_symbol, const typet &type1, const typet &type2)
void do_type_dependencies(id_sett &)
Definition: linking.cpp:1152
symbol_tablet & main_symbol_table
void link_warning(const symbolt &old_symbol, const symbolt &new_symbol, const std::string &msg)
Definition: linking.cpp:389
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
std::string expr_to_string(const namespacet &ns, const irep_idt &identifier, const exprt &expr) const
Definition: linking.cpp:29
Structure type.
Definition: std_types.h:296
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:115
bool needs_renaming_non_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:431
const symbolt & new_symbol
Definition: linking_class.h:95
bool needs_renaming(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking_class.h:51
void rename_symbols(const id_sett &needs_to_be_renamed)
Definition: linking.cpp:1207
void show_struct_diff(const struct_typet &old_type, const struct_typet &new_type)
API to expression classes.
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const symbolt & old_symbol
Definition: linking_class.h:94
adjust_type_infot(const symbolt &_old_symbol, const symbolt &_new_symbol)
Definition: linking_class.h:85
bool needs_renaming_type(const symbolt &old_symbol, const symbolt &new_symbol)
Definition: linking.cpp:1108
namespacet ns
irep_idt rename(irep_idt)
Definition: linking.cpp:407
id_sett renamed_ids
std::string type_to_string(const namespacet &ns, const irep_idt &identifier, const typet &type) const
Definition: linking.cpp:37
replace_symbolt object_type_updates
Definition: linking_class.h:38
void duplicate_code_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:445
bool adjust_object_type_rec(const typet &type1, const typet &type2, adjust_type_infot &info)
Definition: linking.cpp:747
typet type
Type of symbol.
Definition: symbol.h:37
symbol_tablet & src_symbol_table
Base class for all expressions.
Definition: expr.h:46
void duplicate_non_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1002
std::string type_to_string_verbose(const namespacet &ns, const symbolt &symbol) const
void copy_symbols()
Definition: linking.cpp:1239
rename_symbolt rename_symbol
Definition: linking_class.h:37
void duplicate_object_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:916
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:61
bool adjust_object_type(const symbolt &old_symbol, const symbolt &new_symbol, bool &set_to_new)
Definition: linking.cpp:901
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool is_type
Definition: symbol.h:66
void duplicate_type_symbol(symbolt &old_symbol, symbolt &new_symbol)
Definition: linking.cpp:1031
std::unordered_set< irep_idt, irep_id_hash > id_sett
Definition: linking_class.h:41