CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
46 // ID of named subs of loop contracts
47 std::vector<irep_idt> loop_contracts_subs{
49
52
53 for(const auto &s : new_symbols)
54 working_set.push_back(&ns.lookup(s));
55
56 if(symbol.type.id() == ID_code)
57 {
58 const code_typet &code_type = to_code_type(symbol.type);
59 const code_typet::parameterst &parameters = code_type.parameters();
60
61 for(const auto &p : parameters)
62 {
63 const symbolt *s;
64 // identifiers for prototypes need not exist
65 if(!ns.lookup(p.get_identifier(), s))
66 working_set.push_back(s);
67 }
68
69 // check for contract definitions
72
74 for(const exprt &a : maybe_contract.c_assigns())
76 for(const exprt &e : maybe_contract.c_ensures())
78 for(const exprt &r : maybe_contract.c_requires())
80
81 for(const auto &s : new_symbols)
82 {
83 const symbolt *symbol_ptr;
84 // identifiers for parameters of prototypes need not exist, and neither
85 // does __CPROVER_return_value
86 if(!ns.lookup(s, symbol_ptr))
87 working_set.push_back(symbol_ptr);
88 }
89 }
90 }
91}
92
107 symbol_table_baset &symbol_table,
109 const bool keep_file_local)
110{
111 remove_internal_symbols(symbol_table, mh, keep_file_local, {});
112}
113
130 symbol_table_baset &symbol_table,
132 const bool keep_file_local,
133 const std::set<irep_idt> &keep)
134{
135 namespacet ns(symbol_table);
137 messaget log(mh);
138
139 // we retain certain special ones
141 special.insert("argc'");
142 special.insert("argv'");
143 special.insert("envp'");
144 special.insert("envp_size'");
145 special.insert(CPROVER_PREFIX "memory");
147 special.insert(CPROVER_PREFIX "deallocated");
148 special.insert(CPROVER_PREFIX "dead_object");
149 special.insert(CPROVER_PREFIX "assignable");
150 special.insert(CPROVER_PREFIX "object_upto");
151 special.insert(CPROVER_PREFIX "object_from");
152 special.insert(CPROVER_PREFIX "object_whole");
153 special.insert(CPROVER_PREFIX "freeable");
154 special.insert(CPROVER_PREFIX "is_freeable");
155 special.insert(CPROVER_PREFIX "was_freed");
157 special.insert("__new");
158 special.insert("__new_array");
159 special.insert("__placement_new");
160 special.insert("__placement_new_array");
161 special.insert("__delete");
162 special.insert("__delete_array");
163 // plus any extra symbols we wish to keep
164 special.insert(keep.begin(), keep.end());
165
166 for(symbol_table_baset::symbolst::const_iterator it =
167 symbol_table.symbols.begin();
168 it != symbol_table.symbols.end();
169 it++)
170 {
171 // already marked?
172 if(exported.find(it->first)!=exported.end())
173 continue;
174
175 // not marked yet
176 const symbolt &symbol=it->second;
177
178 if(special.find(symbol.name)!=special.end())
179 {
180 get_symbols(ns, symbol, exported);
181 continue;
182 }
183
184 bool is_function=symbol.type.id()==ID_code;
185 bool is_file_local=symbol.is_file_local;
186 bool is_type=symbol.is_type;
187 bool has_body=symbol.value.is_not_nil();
188 bool has_initializer = symbol.value.is_not_nil();
189 bool is_contract = is_function && symbol.is_property;
190
191 // __attribute__((constructor)), __attribute__((destructor))
192 if(symbol.mode==ID_C && is_function && is_file_local)
193 {
194 const code_typet &code_type=to_code_type(symbol.type);
195 if(code_type.return_type().id()==ID_constructor ||
196 code_type.return_type().id()==ID_destructor)
197 is_file_local=false;
198 }
199
200 if(is_type || symbol.is_macro)
201 {
202 // never EXPORTED by itself
203 }
204 else if(is_function)
205 {
206 // body? not local (i.e., "static")?
207 if(
208 has_body &&
209 (!is_file_local ||
210 (config.main.has_value() && symbol.base_name == config.main.value())))
211 {
212 get_symbols(ns, symbol, exported);
213 }
214 else if(has_body && is_file_local && keep_file_local)
215 {
216 get_symbols(ns, symbol, exported);
217 }
218 else if(is_contract)
219 get_symbols(ns, symbol, exported);
220 }
221 else
222 {
223 // 'extern' symbols are only exported if there
224 // is an initializer.
225 if((has_initializer || !symbol.is_extern) &&
226 !is_file_local)
227 {
228 get_symbols(ns, symbol, exported);
229 }
230 }
231 }
232
233 // remove all that are _not_ exported!
234 for(symbol_table_baset::symbolst::const_iterator it =
235 symbol_table.symbols.begin();
236 it != symbol_table.symbols.end();) // no it++
237 {
238 if(exported.find(it->first)==exported.end())
239 {
240 symbol_table_baset::symbolst::const_iterator next = std::next(it);
241 log.debug() << "Removing unused symbol " << it->first << messaget::eom;
242 symbol_table.erase(it);
243 it=next;
244 }
245 else
246 {
247 it++;
248 }
249 }
250}
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:562
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
std::optional< std::string > main
Definition config.h:372
Base class for all expressions.
Definition expr.h:56
bool is_not_nil() const
Definition irep.h:372
const irep_idt & id() const
Definition irep.h:388
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
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, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
std::unordered_set< irep_idt > find_symbols_sett
static int8_t r
Definition irep_hash.h:60
double log(double x)
Definition math.c:2449
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:788
Author: Diffblue Ltd.