CBMC
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 "c_types.h"
15 #include "std_expr.h"
16 #include "symbol_table_base.h"
17 
18 #include <algorithm>
19 
21 {
22 }
23 
30 const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
31 {
32  return lookup(expr.get_identifier());
33 }
34 
41 const symbolt &namespace_baset::lookup(const tag_typet &type) const
42 {
43  return lookup(type.get_identifier());
44 }
45 
49 const typet &namespace_baset::follow(const typet &src) const
50 {
51  if(src.id() == ID_union_tag)
52  return follow_tag(to_union_tag_type(src));
53 
54  if(src.id() == ID_struct_tag)
55  return follow_tag(to_struct_tag_type(src));
56 
57  return src;
58 }
59 
64 {
65  const symbolt &symbol=lookup(src.get_identifier());
66  CHECK_RETURN(symbol.is_type);
67  CHECK_RETURN(symbol.type.id() == ID_union);
68  return to_union_type(symbol.type);
69 }
70 
74 const struct_typet &
76 {
77  const symbolt &symbol=lookup(src.get_identifier());
78  CHECK_RETURN(symbol.is_type);
79  CHECK_RETURN(symbol.type.id() == ID_struct);
80  return to_struct_type(symbol.type);
81 }
82 
86 const c_enum_typet &
88 {
89  const symbolt &symbol=lookup(src.get_identifier());
90  CHECK_RETURN(symbol.is_type);
91  CHECK_RETURN(symbol.type.id() == ID_c_enum);
92  return to_c_enum_type(symbol.type);
93 }
94 
96 const struct_union_typet &
98 {
99  const symbolt &symbol = lookup(src.get_identifier());
100  CHECK_RETURN(symbol.is_type);
101  CHECK_RETURN(symbol.type.id() == ID_struct || symbol.type.id() == ID_union);
102  return to_struct_union_type(symbol.type);
103 }
104 
108 {
109  if(expr.id()==ID_symbol)
110  {
111  const symbolt &symbol = lookup(to_symbol_expr(expr));
112 
113  if(symbol.is_macro && !symbol.value.is_nil())
114  {
115  expr=symbol.value;
116  follow_macros(expr);
117  }
118 
119  return;
120  }
121 
122  Forall_operands(it, expr)
123  follow_macros(*it);
124 }
125 
130 std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
131 {
132  std::size_t m = 0;
133 
134  if(symbol_table1!=nullptr)
135  m = std::max(m, symbol_table1->next_unused_suffix(prefix));
136 
137  if(symbol_table2!=nullptr)
138  m = std::max(m, symbol_table2->next_unused_suffix(prefix));
139 
140  return m;
141 }
142 
149  const irep_idt &name,
150  const symbolt *&symbol) const
151 {
152  symbol_table_baset::symbolst::const_iterator it;
153 
154  if(symbol_table1!=nullptr)
155  {
156  it=symbol_table1->symbols.find(name);
157 
158  if(it!=symbol_table1->symbols.end())
159  {
160  symbol=&(it->second);
161  return false;
162  }
163  }
164 
165  if(symbol_table2!=nullptr)
166  {
167  it=symbol_table2->symbols.find(name);
168 
169  if(it!=symbol_table2->symbols.end())
170  {
171  symbol=&(it->second);
172  return false;
173  }
174  }
175 
176  return true;
177 }
178 
182 std::size_t
183 multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
184 {
185  std::size_t m = 0;
186 
187  for(const auto &st : symbol_table_list)
188  m = std::max(m, st->next_unused_suffix(prefix));
189 
190  return m;
191 }
192 
200  const irep_idt &name,
201  const symbolt *&symbol) const
202 {
203  symbol_table_baset::symbolst::const_iterator s_it;
204 
205  for(symbol_table_listt::const_iterator
206  c_it=symbol_table_list.begin();
207  c_it!=symbol_table_list.end();
208  c_it++)
209  {
210  s_it=(*c_it)->symbols.find(name);
211 
212  if(s_it!=(*c_it)->symbols.end())
213  {
214  symbol=&(s_it->second);
215  return false;
216  }
217  }
218 
219  return true;
220 }
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:335
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:184
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:352
The type of C enums.
Definition: c_types.h:239
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:388
bool is_nil() const
Definition: irep.h:368
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:183
symbol_table_listt symbol_table_list
Definition: namespace.h:172
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:107
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
virtual ~namespace_baset()
Definition: namespace.cpp:20
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
const symbol_table_baset * symbol_table1
Definition: namespace.h:132
const symbol_table_baset * symbol_table2
Definition: namespace.h:132
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:130
A struct or union tag type.
Definition: std_types.h:451
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Base type for structs and unions.
Definition: std_types.h:62
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
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.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
bool is_macro
Definition: symbol.h:62
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:396
const irep_idt & get_identifier() const
Definition: std_types.h:410
The type of an expression, extends irept.
Definition: type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:199
The union type.
Definition: c_types.h:147
#define Forall_operands(it, expr)
Definition: expr.h:27
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
Author: Diffblue Ltd.