cprover
Loading...
Searching...
No Matches
remove_internal_symbols.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove symbols that are internal only
4
5Author: Daniel Kroening
6
7\*******************************************************************/
8
11
13
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/find_symbols.h>
17#include <util/message.h>
18#include <util/namespace.h>
19#include <util/std_types.h>
21
23
25
26static void get_symbols(
27 const namespacet &ns,
28 const symbolt &in_symbol,
30{
31 std::vector<const symbolt *> working_set;
32
33 working_set.push_back(&in_symbol);
34
35 while(!working_set.empty())
36 {
38 working_set.pop_back();
39 const symbolt &symbol = *current_symbol_ptr;
40
41 if(!dest.insert(symbol.name).second)
42 continue;
43
45
48
49 for(const auto &s : new_symbols)
50 working_set.push_back(&ns.lookup(s));
51
52 if(symbol.type.id() == ID_code)
53 {
54 const code_typet &code_type = to_code_type(symbol.type);
55 const code_typet::parameterst &parameters = code_type.parameters();
56
57 for(const auto &p : parameters)
58 {
59 const symbolt *s;
60 // identifiers for prototypes need not exist
61 if(!ns.lookup(p.get_identifier(), s))
62 working_set.push_back(s);
63 }
64
65 // check for contract definitions
68
70 for(const exprt &a : maybe_contract.c_assigns())
72 for(const exprt &e : maybe_contract.c_ensures())
74 for(const exprt &r : maybe_contract.c_requires())
76
77 for(const auto &s : new_symbols)
78 {
79 const symbolt *symbol_ptr;
80 // identifiers for parameters of prototypes need not exist, and neither
81 // does __CPROVER_return_value
82 if(!ns.lookup(s, symbol_ptr))
83 working_set.push_back(symbol_ptr);
84 }
85 }
86 }
87}
88
103 symbol_table_baset &symbol_table,
105 const bool keep_file_local)
106{
107 remove_internal_symbols(symbol_table, mh, keep_file_local, {});
108}
109
126 symbol_table_baset &symbol_table,
128 const bool keep_file_local,
129 const std::set<irep_idt> &keep)
130{
131 namespacet ns(symbol_table);
133 messaget log(mh);
134
135 // we retain certain special ones
137 special.insert("argc'");
138 special.insert("argv'");
139 special.insert("envp'");
140 special.insert("envp_size'");
141 special.insert(CPROVER_PREFIX "memory");
143 special.insert(CPROVER_PREFIX "deallocated");
144 special.insert(CPROVER_PREFIX "dead_object");
145 special.insert(CPROVER_PREFIX "assignable");
146 special.insert(CPROVER_PREFIX "object_upto");
147 special.insert(CPROVER_PREFIX "object_from");
148 special.insert(CPROVER_PREFIX "object_whole");
149 special.insert(CPROVER_PREFIX "freeable");
150 special.insert(CPROVER_PREFIX "is_freeable");
151 special.insert(CPROVER_PREFIX "was_freed");
153 special.insert("__new");
154 special.insert("__new_array");
155 special.insert("__placement_new");
156 special.insert("__placement_new_array");
157 special.insert("__delete");
158 special.insert("__delete_array");
159 // plus any extra symbols we wish to keep
160 special.insert(keep.begin(), keep.end());
161
162 for(symbol_table_baset::symbolst::const_iterator it =
163 symbol_table.symbols.begin();
164 it != symbol_table.symbols.end();
165 it++)
166 {
167 // already marked?
168 if(exported.find(it->first)!=exported.end())
169 continue;
170
171 // not marked yet
172 const symbolt &symbol=it->second;
173
174 if(special.find(symbol.name)!=special.end())
175 {
176 get_symbols(ns, symbol, exported);
177 continue;
178 }
179
180 bool is_function=symbol.type.id()==ID_code;
181 bool is_file_local=symbol.is_file_local;
182 bool is_type=symbol.is_type;
183 bool has_body=symbol.value.is_not_nil();
184 bool has_initializer = symbol.value.is_not_nil();
185 bool is_contract = is_function && symbol.is_property;
186
187 // __attribute__((constructor)), __attribute__((destructor))
188 if(symbol.mode==ID_C && is_function && is_file_local)
189 {
190 const code_typet &code_type=to_code_type(symbol.type);
191 if(code_type.return_type().id()==ID_constructor ||
192 code_type.return_type().id()==ID_destructor)
193 is_file_local=false;
194 }
195
196 if(is_type || symbol.is_macro)
197 {
198 // never EXPORTED by itself
199 }
200 else if(is_function)
201 {
202 // body? not local (i.e., "static")?
203 if(
204 has_body &&
205 (!is_file_local ||
206 (config.main.has_value() && symbol.base_name == config.main.value())))
207 {
208 get_symbols(ns, symbol, exported);
209 }
210 else if(has_body && is_file_local && keep_file_local)
211 {
212 get_symbols(ns, symbol, exported);
213 }
214 else if(is_contract)
215 get_symbols(ns, symbol, exported);
216 }
217 else
218 {
219 // 'extern' symbols are only exported if there
220 // is an initializer.
221 if((has_initializer || !symbol.is_extern) &&
222 !is_file_local)
223 {
224 get_symbols(ns, symbol, exported);
225 }
226 }
227 }
228
229 // remove all that are _not_ exported!
230 for(symbol_table_baset::symbolst::const_iterator it =
231 symbol_table.symbols.begin();
232 it != symbol_table.symbols.end();) // no it++
233 {
234 if(exported.find(it->first)==exported.end())
235 {
236 symbol_table_baset::symbolst::const_iterator next = std::next(it);
237 log.debug() << "Removing unused symbol " << it->first << messaget::eom;
238 symbol_table.erase(it);
239 it=next;
240 }
241 else
242 {
243 it++;
244 }
245 }
246}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
configt config
Definition config.cpp:25
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
Definition c_types.h:467
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base type of functions.
Definition std_types.h:539
std::vector< parametert > parameterst
Definition std_types.h:542
optionalt< std::string > main
Definition config.h:353
Base class for all expressions.
Definition expr.h:56
bool is_not_nil() const
Definition irep.h:380
const irep_idt & id() const
Definition irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:155
mstreamt & debug() const
Definition message.h:429
static eomt eom
Definition message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The symbol table base class interface.
virtual void erase(const symbolst::const_iterator &entry)=0
Remove a symbol from the symbol table.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition symbol.h:28
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_file_local
Definition symbol.h:73
bool is_property
Definition symbol.h:67
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
exprt value
Initial value of symbol.
Definition symbol.h:34
irep_idt mode
Language mode.
Definition symbol.h:49
#define CPROVER_PREFIX
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Find identifiers of the sub expressions with id ID_symbol, considering both free and bound variables,...
std::unordered_set< irep_idt > find_symbols_sett
static int8_t r
Definition irep_hash.h:60
static void get_symbols(const namespacet &ns, const symbolt &in_symbol, find_symbols_sett &dest)
void remove_internal_symbols(symbol_table_baset &symbol_table, message_handlert &mh, const bool keep_file_local)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
Remove symbols that are internal only.
#define INITIALIZE_FUNCTION
Pre-defined types.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Author: Diffblue Ltd.