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 "c_types.h"
17 #include "prefix.h"
18 #include "std_expr.h"
19 #include "std_types.h"
20 #include "string2int.h"
21 #include "symbol_table.h"
22 
24 {
25 }
26 
33 const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
34 {
35  return lookup(expr.get_identifier());
36 }
37 
44 const symbolt &namespace_baset::lookup(const tag_typet &type) const
45 {
46  return lookup(type.get_identifier());
47 }
48 
52 const typet &namespace_baset::follow(const typet &src) const
53 {
54  if(src.id() == ID_union_tag)
55  return follow_tag(to_union_tag_type(src));
56 
57  if(src.id() == ID_struct_tag)
58  return follow_tag(to_struct_tag_type(src));
59 
60  return src;
61 }
62 
67 {
68  const symbolt &symbol=lookup(src.get_identifier());
69  CHECK_RETURN(symbol.is_type);
70  CHECK_RETURN(symbol.type.id() == ID_union);
71  return to_union_type(symbol.type);
72 }
73 
77 const struct_typet &
79 {
80  const symbolt &symbol=lookup(src.get_identifier());
81  CHECK_RETURN(symbol.is_type);
82  CHECK_RETURN(symbol.type.id() == ID_struct);
83  return to_struct_type(symbol.type);
84 }
85 
89 const c_enum_typet &
91 {
92  const symbolt &symbol=lookup(src.get_identifier());
93  CHECK_RETURN(symbol.is_type);
94  CHECK_RETURN(symbol.type.id() == ID_c_enum);
95  return to_c_enum_type(symbol.type);
96 }
97 
101 {
102  if(expr.id()==ID_symbol)
103  {
104  const symbolt &symbol = lookup(to_symbol_expr(expr));
105 
106  if(symbol.is_macro && !symbol.value.is_nil())
107  {
108  expr=symbol.value;
109  follow_macros(expr);
110  }
111 
112  return;
113  }
114 
115  Forall_operands(it, expr)
116  follow_macros(*it);
117 }
118 
123 std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
124 {
125  std::size_t m = 0;
126 
127  if(symbol_table1!=nullptr)
128  m = std::max(m, symbol_table1->next_unused_suffix(prefix));
129 
130  if(symbol_table2!=nullptr)
131  m = std::max(m, symbol_table2->next_unused_suffix(prefix));
132 
133  return m;
134 }
135 
142  const irep_idt &name,
143  const symbolt *&symbol) const
144 {
145  symbol_tablet::symbolst::const_iterator it;
146 
147  if(symbol_table1!=nullptr)
148  {
149  it=symbol_table1->symbols.find(name);
150 
151  if(it!=symbol_table1->symbols.end())
152  {
153  symbol=&(it->second);
154  return false;
155  }
156  }
157 
158  if(symbol_table2!=nullptr)
159  {
160  it=symbol_table2->symbols.find(name);
161 
162  if(it!=symbol_table2->symbols.end())
163  {
164  symbol=&(it->second);
165  return false;
166  }
167  }
168 
169  return true;
170 }
171 
175 std::size_t
176 multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
177 {
178  std::size_t m = 0;
179 
180  for(const auto &st : symbol_table_list)
181  m = std::max(m, st->next_unused_suffix(prefix));
182 
183  return m;
184 }
185 
193  const irep_idt &name,
194  const symbolt *&symbol) const
195 {
196  symbol_tablet::symbolst::const_iterator s_it;
197 
198  for(symbol_table_listt::const_iterator
199  c_it=symbol_table_list.begin();
200  c_it!=symbol_table_list.end();
201  c_it++)
202  {
203  s_it=(*c_it)->symbols.find(name);
204 
205  if(s_it!=(*c_it)->symbols.end())
206  {
207  symbol=&(s_it->second);
208  return false;
209  }
210  }
211 
212  return true;
213 }
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:404
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
namespacet::symbol_table2
const symbol_table_baset * symbol_table2
Definition: namespace.h:130
c_enum_typet
The type of C enums.
Definition: c_types.h:204
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:25
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:302
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:277
prefix.h
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
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:443
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:66
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
namespace.h
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:164
multi_namespacet::symbol_table_list
symbol_table_listt symbol_table_list
Definition: namespace.h:170
namespace_baset::follow_macros
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:100
string2int.h
namespace_baset::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
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:123
namespace_baset::~namespace_baset
virtual ~namespace_baset()
Definition: namespace.cpp:23
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
std_types.h
Pre-defined types.
multi_namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
namespacet::symbol_table1
const symbol_table_baset * symbol_table1
Definition: namespace.h:130
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:468
union_typet
The union type.
Definition: c_types.h:112
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:390
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:52
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
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:63
std_expr.h
API to expression classes.
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:176
c_types.h