cprover
namespace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Namespace
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "namespace.h"
13 
14 #include <algorithm>
15 
16 #include "prefix.h"
17 #include "std_expr.h"
18 #include "std_types.h"
19 #include "string2int.h"
20 #include "symbol_table.h"
21 
23 {
24 }
25 
32 const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
33 {
34  return lookup(expr.get_identifier());
35 }
36 
43 const symbolt &namespace_baset::lookup(const symbol_typet &type) const
44 {
45  return lookup(type.get_identifier());
46 }
47 
54 const symbolt &namespace_baset::lookup(const tag_typet &type) const
55 {
56  return lookup(type.get_identifier());
57 }
58 
62 const typet &namespace_baset::follow(const typet &src) const
63 {
64  if(src.id() == ID_union_tag)
65  return follow_tag(to_union_tag_type(src));
66 
67  if(src.id() == ID_struct_tag)
68  return follow_tag(to_struct_tag_type(src));
69 
70  if(src.id() != ID_symbol_type)
71  return src;
72 
73  const symbolt *symbol = &lookup(to_symbol_type(src));
74 
75  // let's hope it's not cyclic...
76  while(true)
77  {
78  DATA_INVARIANT(symbol->is_type, "symbol type points to type");
79 
80  if(symbol->type.id() == ID_symbol_type)
81  symbol = &lookup(to_symbol_type(symbol->type));
82  else
83  return symbol->type;
84  }
85 }
86 
91 {
92  const symbolt &symbol=lookup(src.get_identifier());
93  CHECK_RETURN(symbol.is_type);
95  symbol.type.id() == ID_union || symbol.type.id() == ID_incomplete_union);
96  return symbol.type;
97 }
98 
103 {
104  const symbolt &symbol=lookup(src.get_identifier());
105  CHECK_RETURN(symbol.is_type);
106  CHECK_RETURN(
107  symbol.type.id() == ID_struct || symbol.type.id() == ID_incomplete_struct);
108  return symbol.type;
109 }
110 
115 {
116  const symbolt &symbol=lookup(src.get_identifier());
117  CHECK_RETURN(symbol.is_type);
118  CHECK_RETURN(
119  symbol.type.id() == ID_c_enum || symbol.type.id() == ID_incomplete_c_enum);
120  return symbol.type;
121 }
122 
126 {
127  if(expr.id()==ID_symbol)
128  {
129  const symbolt &symbol = lookup(to_symbol_expr(expr));
130 
131  if(symbol.is_macro && !symbol.value.is_nil())
132  {
133  expr=symbol.value;
134  follow_macros(expr);
135  }
136 
137  return;
138  }
139 
140  Forall_operands(it, expr)
141  follow_macros(*it);
142 }
143 
148 std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
149 {
150  std::size_t m = 0;
151 
152  if(symbol_table1!=nullptr)
153  m = std::max(m, symbol_table1->next_unused_suffix(prefix));
154 
155  if(symbol_table2!=nullptr)
156  m = std::max(m, symbol_table2->next_unused_suffix(prefix));
157 
158  return m;
159 }
160 
167  const irep_idt &name,
168  const symbolt *&symbol) const
169 {
170  symbol_tablet::symbolst::const_iterator it;
171 
172  if(symbol_table1!=nullptr)
173  {
174  it=symbol_table1->symbols.find(name);
175 
176  if(it!=symbol_table1->symbols.end())
177  {
178  symbol=&(it->second);
179  return false;
180  }
181  }
182 
183  if(symbol_table2!=nullptr)
184  {
185  it=symbol_table2->symbols.find(name);
186 
187  if(it!=symbol_table2->symbols.end())
188  {
189  symbol=&(it->second);
190  return false;
191  }
192  }
193 
194  return true;
195 }
196 
200 std::size_t
201 multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
202 {
203  std::size_t m = 0;
204 
205  for(const auto &st : symbol_table_list)
206  m = std::max(m, st->next_unused_suffix(prefix));
207 
208  return m;
209 }
210 
218  const irep_idt &name,
219  const symbolt *&symbol) const
220 {
221  symbol_tablet::symbolst::const_iterator s_it;
222 
223  for(symbol_table_listt::const_iterator
224  c_it=symbol_table_list.begin();
225  c_it!=symbol_table_list.end();
226  c_it++)
227  {
228  s_it=(*c_it)->symbols.find(name);
229 
230  if(s_it!=(*c_it)->symbols.end())
231  {
232  symbol=&(s_it->second);
233  return false;
234  }
235  }
236 
237  return true;
238 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:479
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
namespacet::symbol_table2
const symbol_table_baset * symbol_table2
Definition: namespace.h:132
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
typet
The type of an expression, extends irept.
Definition: type.h:27
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
prefix.h
exprt
Base class for all expressions.
Definition: expr.h:54
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
symbol_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:75
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
namespace.h
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:557
multi_namespacet::symbol_table_list
symbol_table_listt symbol_table_list
Definition: namespace.h:172
namespace_baset::follow_macros
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:125
string2int.h
multi_namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:217
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
namespace_baset::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:45
namespacet::smallest_unused_suffix
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:148
namespace_baset::follow_tag
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
namespace_baset::~namespace_baset
virtual ~namespace_baset()
Definition: namespace.cpp:22
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std_types.h
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
namespacet::symbol_table1
const symbol_table_baset * symbol_table1
Definition: namespace.h:132
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:464
to_symbol_type
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Definition: std_types.h:98
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:711
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbol_typet
A reference into the symbol table.
Definition: std_types.h:62
symbol_table.h
Author: Diffblue Ltd.
symbol_table_baset::next_unused_suffix
std::size_t next_unused_suffix(const std::string &prefix, std::size_t start_number) const
Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.
Definition: symbol_table_base.h:54
std_expr.h
multi_namespacet::smallest_unused_suffix
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:201
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470