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
15
16#include <util/config.h>
17#include <util/find_symbols.h>
18#include <util/message.h>
19#include <util/namespace.h>
20#include <util/std_types.h>
21#include <util/symbol_table.h>
22
24
25static void get_symbols(
26 const namespacet &ns,
27 const symbolt &in_symbol,
29{
30 std::vector<const symbolt *> working_set;
31
32 working_set.push_back(&in_symbol);
33
34 while(!working_set.empty())
35 {
36 const symbolt *current_symbol_ptr = working_set.back();
37 working_set.pop_back();
38 const symbolt &symbol = *current_symbol_ptr;
39
40 if(!dest.insert(symbol.name).second)
41 continue;
42
43 find_symbols_sett new_symbols;
44
45 find_type_and_expr_symbols(symbol.type, new_symbols);
46 find_type_and_expr_symbols(symbol.value, new_symbols);
47
48 for(const auto &s : new_symbols)
49 working_set.push_back(&ns.lookup(s));
50
51 if(symbol.type.id() == ID_code)
52 {
53 const code_typet &code_type = to_code_type(symbol.type);
54 const code_typet::parameterst &parameters = code_type.parameters();
55
56 for(const auto &p : parameters)
57 {
58 const symbolt *s;
59 // identifiers for prototypes need not exist
60 if(!ns.lookup(p.get_identifier(), s))
61 working_set.push_back(s);
62 }
63
64 // check for contract definitions
65 const exprt ensures =
66 static_cast<const exprt &>(code_type.find(ID_C_spec_ensures));
67 const exprt requires =
68 static_cast<const exprt &>(code_type.find(ID_C_spec_requires));
69
70 find_symbols_sett new_symbols;
71 find_type_and_expr_symbols(ensures, new_symbols);
72 find_type_and_expr_symbols(requires, new_symbols);
73
74 for(const auto &s : new_symbols)
75 {
76 // keep functions called in contracts within scope.
77 // should we keep local variables from the contract as well?
78 const symbolt *new_symbol = nullptr;
79 if(!ns.lookup(s, new_symbol))
80 {
81 if(new_symbol->type.id() == ID_code)
82 {
83 working_set.push_back(new_symbol);
84 }
85 }
86 }
87 }
88 }
89}
90
105 symbol_tablet &symbol_table,
107 const bool keep_file_local)
108{
109 namespacet ns(symbol_table);
110 find_symbols_sett exported;
111 messaget log(mh);
112
113 // we retain certain special ones
114 find_symbols_sett special;
115 special.insert("argc'");
116 special.insert("argv'");
117 special.insert("envp'");
118 special.insert("envp_size'");
119 special.insert(CPROVER_PREFIX "memory");
120 special.insert(INITIALIZE_FUNCTION);
121 special.insert(CPROVER_PREFIX "deallocated");
122 special.insert(CPROVER_PREFIX "dead_object");
123 special.insert(rounding_mode_identifier());
124 special.insert("__new");
125 special.insert("__new_array");
126 special.insert("__placement_new");
127 special.insert("__placement_new_array");
128 special.insert("__delete");
129 special.insert("__delete_array");
130
131 for(symbol_tablet::symbolst::const_iterator
132 it=symbol_table.symbols.begin();
133 it!=symbol_table.symbols.end();
134 it++)
135 {
136 // already marked?
137 if(exported.find(it->first)!=exported.end())
138 continue;
139
140 // not marked yet
141 const symbolt &symbol=it->second;
142
143 if(special.find(symbol.name)!=special.end())
144 {
145 get_symbols(ns, symbol, exported);
146 continue;
147 }
148
149 bool is_function=symbol.type.id()==ID_code;
150 bool is_file_local=symbol.is_file_local;
151 bool is_type=symbol.is_type;
152 bool has_body=symbol.value.is_not_nil();
153 bool has_initializer = symbol.value.is_not_nil();
154
155 // __attribute__((constructor)), __attribute__((destructor))
156 if(symbol.mode==ID_C && is_function && is_file_local)
157 {
158 const code_typet &code_type=to_code_type(symbol.type);
159 if(code_type.return_type().id()==ID_constructor ||
160 code_type.return_type().id()==ID_destructor)
161 is_file_local=false;
162 }
163
164 if(is_type || symbol.is_macro)
165 {
166 // never EXPORTED by itself
167 }
168 else if(is_function)
169 {
170 // body? not local (i.e., "static")?
171 if(
172 has_body &&
173 (!is_file_local ||
174 (config.main.has_value() && symbol.base_name == config.main.value())))
175 {
176 get_symbols(ns, symbol, exported);
177 }
178 else if(has_body && is_file_local && keep_file_local)
179 {
180 get_symbols(ns, symbol, exported);
181 }
182 }
183 else
184 {
185 // 'extern' symbols are only exported if there
186 // is an initializer.
187 if((has_initializer || !symbol.is_extern) &&
188 !is_file_local)
189 {
190 get_symbols(ns, symbol, exported);
191 }
192 }
193 }
194
195 // remove all that are _not_ exported!
196 for(symbol_tablet::symbolst::const_iterator
197 it=symbol_table.symbols.begin();
198 it!=symbol_table.symbols.end();
199 ) // no it++
200 {
201 if(exported.find(it->first)==exported.end())
202 {
203 symbol_tablet::symbolst::const_iterator next=std::next(it);
204 symbol_table.erase(it);
205 it=next;
206 }
207 else
208 {
209 it++;
210 }
211 }
212}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
Base type of functions.
Definition: std_types.h:539
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
optionalt< std::string > main
Definition: config.h:326
Base class for all expressions.
Definition: expr.h:54
const irept & find(const irep_idt &name) const
Definition: irep.cpp:106
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
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().
Definition: namespace.cpp:138
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
bool is_file_local
Definition: symbol.h:66
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
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:23
void remove_internal_symbols(symbol_tablet &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.
static void get_symbols(const namespacet &ns, const symbolt &in_symbol, find_symbols_sett &dest)
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.