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