cprover
remove_internal_symbols.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove symbols that are internal only
4 
5 Author: 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 
23 #include "static_lifetime_init.h"
24 
25 static void get_symbols(
26  const namespacet &ns,
27  const symbolt &in_symbol,
28  find_symbols_sett &dest)
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,
106  message_handlert &mh,
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 "malloc_size");
122  special.insert(CPROVER_PREFIX "deallocated");
123  special.insert(CPROVER_PREFIX "dead_object");
124  special.insert(rounding_mode_identifier());
125  special.insert("__new");
126  special.insert("__new_array");
127  special.insert("__placement_new");
128  special.insert("__placement_new_array");
129  special.insert("__delete");
130  special.insert("__delete_array");
131 
132  for(symbol_tablet::symbolst::const_iterator
133  it=symbol_table.symbols.begin();
134  it!=symbol_table.symbols.end();
135  it++)
136  {
137  // already marked?
138  if(exported.find(it->first)!=exported.end())
139  continue;
140 
141  // not marked yet
142  const symbolt &symbol=it->second;
143 
144  if(special.find(symbol.name)!=special.end())
145  {
146  get_symbols(ns, symbol, exported);
147  continue;
148  }
149 
150  bool is_function=symbol.type.id()==ID_code;
151  bool is_file_local=symbol.is_file_local;
152  bool is_type=symbol.is_type;
153  bool has_body=symbol.value.is_not_nil();
154  bool has_initializer = symbol.value.is_not_nil();
155 
156  // __attribute__((constructor)), __attribute__((destructor))
157  if(symbol.mode==ID_C && is_function && is_file_local)
158  {
159  const code_typet &code_type=to_code_type(symbol.type);
160  if(code_type.return_type().id()==ID_constructor ||
161  code_type.return_type().id()==ID_destructor)
162  is_file_local=false;
163  }
164 
165  if(is_type || symbol.is_macro)
166  {
167  // never EXPORTED by itself
168  }
169  else if(is_function)
170  {
171  // body? not local (i.e., "static")?
172  if(
173  has_body &&
174  (!is_file_local ||
175  (config.main.has_value() && symbol.base_name == config.main.value())))
176  {
177  get_symbols(ns, symbol, exported);
178  }
179  else if(has_body && is_file_local && keep_file_local)
180  {
181  get_symbols(ns, symbol, exported);
182  }
183  }
184  else
185  {
186  // 'extern' symbols are only exported if there
187  // is an initializer.
188  if((has_initializer || !symbol.is_extern) &&
189  !is_file_local)
190  {
191  get_symbols(ns, symbol, exported);
192  }
193  }
194  }
195 
196  // remove all that are _not_ exported!
197  for(symbol_tablet::symbolst::const_iterator
198  it=symbol_table.symbols.begin();
199  it!=symbol_table.symbols.end();
200  ) // no it++
201  {
202  if(exported.find(it->first)==exported.end())
203  {
204  symbol_tablet::symbolst::const_iterator next=std::next(it);
205  symbol_table.erase(it);
206  it=next;
207  }
208  else
209  {
210  it++;
211  }
212  }
213 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
find_type_and_expr_symbols
void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:200
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:106
configt::main
optionalt< std::string > main
Definition: config.h:260
exprt
Base class for all expressions.
Definition: expr.h:54
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
namespace.h
remove_internal_symbols
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.
Definition: remove_internal_symbols.cpp:104
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
find_symbols.h
std_types.h
Pre-defined types.
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
code_typet
Base type of functions.
Definition: std_types.h:539
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
get_symbols
static void get_symbols(const namespacet &ns, const symbolt &in_symbol, find_symbols_sett &dest)
Definition: remove_internal_symbols.cpp:25
rounding_mode_identifier
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Definition: adjust_float_expressions.cpp:24
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
config
configt config
Definition: config.cpp:25
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:21
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
remove_internal_symbols.h
Remove symbols that are internal only.
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
config.h
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
symbol_tablet::erase
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
Definition: symbol_table.cpp:90
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
static_lifetime_init.h
symbol_table.h
Author: Diffblue Ltd.
message.h
adjust_float_expressions.h
Symbolic Execution.
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40