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