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 
23  const namespacet &ns,
24  const symbolt &symbol,
25  find_symbols_sett &dest)
26 {
27  dest.insert(symbol.name);
28 
29  find_symbols_sett new_symbols;
30 
31  find_type_and_expr_symbols(symbol.type, new_symbols);
32  find_type_and_expr_symbols(symbol.value, new_symbols);
33 
34  if(symbol.type.id()==ID_code)
35  {
36  const code_typet &code_type=to_code_type(symbol.type);
37  const code_typet::parameterst &parameters=code_type.parameters();
38 
39  for(code_typet::parameterst::const_iterator
40  it=parameters.begin();
41  it!=parameters.end();
42  it++)
43  {
44  irep_idt id=it->get_identifier();
45  const symbolt *s;
46  // identifiers for prototypes need not exist
47  if(!ns.lookup(id, s))
48  new_symbols.insert(id);
49  }
50  }
51 
52  for(find_symbols_sett::const_iterator
53  it=new_symbols.begin();
54  it!=new_symbols.end();
55  it++)
56  {
57  if(dest.find(*it)==dest.end())
58  {
59  dest.insert(*it);
60  get_symbols_rec(ns, ns.lookup(*it), dest); // recursive call
61  }
62  }
63 }
64 
76  symbol_tablet &symbol_table)
77 {
78  namespacet ns(symbol_table);
79  find_symbols_sett exported;
80 
81  // we retain certain special ones
82  find_symbols_sett special;
83  special.insert("argc'");
84  special.insert("argv'");
85  special.insert("envp'");
86  special.insert("envp_size'");
87  special.insert(CPROVER_PREFIX "memory");
88  special.insert(INITIALIZE_FUNCTION);
89  special.insert(CPROVER_PREFIX "malloc_size");
90  special.insert(CPROVER_PREFIX "deallocated");
91  special.insert(CPROVER_PREFIX "dead_object");
92  special.insert(CPROVER_PREFIX "rounding_mode");
93 
94  for(symbol_tablet::symbolst::const_iterator
95  it=symbol_table.symbols.begin();
96  it!=symbol_table.symbols.end();
97  it++)
98  {
99  // already marked?
100  if(exported.find(it->first)!=exported.end())
101  continue;
102 
103  // not marked yet
104  const symbolt &symbol=it->second;
105 
106  if(special.find(symbol.name)!=special.end())
107  {
108  get_symbols_rec(ns, symbol, exported);
109  continue;
110  }
111 
112  bool is_function=symbol.type.id()==ID_code;
113  bool is_file_local=symbol.is_file_local;
114  bool is_type=symbol.is_type;
115  bool has_body=symbol.value.is_not_nil();
116  bool has_initializer=
117  symbol.value.is_not_nil() &&
118  !symbol.value.get_bool(ID_C_zero_initializer);
119 
120  // __attribute__((constructor)), __attribute__((destructor))
121  if(symbol.mode==ID_C && is_function && is_file_local)
122  {
123  const code_typet &code_type=to_code_type(symbol.type);
124  if(code_type.return_type().id()==ID_constructor ||
125  code_type.return_type().id()==ID_destructor)
126  is_file_local=false;
127  }
128 
129  if(is_type || symbol.is_macro)
130  {
131  // never EXPORTED by itself
132  }
133  else if(is_function)
134  {
135  // body? not local (i.e., "static")?
136  if(has_body &&
137  (!is_file_local || (config.main==symbol.name.c_str())))
138  get_symbols_rec(ns, symbol, exported);
139  }
140  else
141  {
142  // 'extern' symbols are only exported if there
143  // is an initializer.
144  if((has_initializer || !symbol.is_extern) &&
145  !is_file_local)
146  {
147  get_symbols_rec(ns, symbol, exported);
148  }
149  }
150  }
151 
152  // remove all that are _not_ exported!
153  for(symbol_tablet::symbolst::const_iterator
154  it=symbol_table.symbols.begin();
155  it!=symbol_table.symbols.end();
156  ) // no it++
157  {
158  if(exported.find(it->first)==exported.end())
159  {
160  symbol_tablet::symbolst::const_iterator next=std::next(it);
161  symbol_table.erase(it);
162  it=next;
163  }
164  else
165  {
166  it++;
167  }
168  }
169 }
irep_idt name
The unique identifier.
Definition: symbol.h:43
Base type of functions.
Definition: std_types.h:764
bool is_not_nil() const
Definition: irep.h:103
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:52
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
std::vector< parametert > parameterst
Definition: std_types.h:767
exprt value
Initial value of symbol.
Definition: symbol.h:37
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
configt config
Definition: config.cpp:23
const irep_idt & id() const
Definition: irep.h:189
void remove_internal_symbols(symbol_tablet &symbol_table)
Removes internal symbols from a symbol table A symbol is EXPORTED if it is a.
std::string main
Definition: config.h:163
#define INITIALIZE_FUNCTION
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Author: Diffblue Ltd.
const symbolst & symbols
virtual void erase(const symbolst::const_iterator &entry) override
Remove a symbol from the symbol table.
bool is_extern
Definition: symbol.h:68
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
const parameterst & parameters() const
Definition: std_types.h:905
bool is_file_local
Definition: symbol.h:68
const char * c_str() const
Definition: dstring.h:72
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:20
bool is_type
Definition: symbol.h:63
Remove symbols that are internal only.
const typet & return_type() const
Definition: std_types.h:895
bool is_macro
Definition: symbol.h:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
void get_symbols_rec(const namespacet &ns, const symbolt &symbol, find_symbols_sett &dest)