cprover
Loading...
Searching...
No Matches
linking_class.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Linking
4
5Author: 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{
24private:
25 bool replace_symbol_expr(symbol_exprt &dest) const override;
26};
27
28class linkingt:public typecheckt
29{
30public:
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
47protected:
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
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.