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 <cassert>
17 
18 #include "prefix.h"
19 #include "std_expr.h"
20 #include "std_types.h"
21 #include "string2int.h"
22 #include "symbol_table.h"
23 
24 static std::size_t smallest_unused_suffix(
25  const std::string &prefix,
26  const symbol_tablet::symbolst &symbols)
27 {
28  std::size_t max_nr = 0;
29 
30  while(symbols.find(prefix + std::to_string(max_nr)) != symbols.end())
31  ++max_nr;
32 
33  return max_nr;
34 }
35 
37 {
38 }
39 
40 const symbolt &namespace_baset::lookup(const symbol_exprt &expr) const
41 {
42  return lookup(expr.get_identifier());
43 }
44 
45 const symbolt &namespace_baset::lookup(const symbol_typet &type) const
46 {
47  return lookup(type.get_identifier());
48 }
49 
50 const symbolt &namespace_baset::lookup(const tag_typet &type) const
51 {
52  return lookup(type.get_identifier());
53 }
54 
55 const typet &namespace_baset::follow(const typet &src) const
56 {
57  if(src.id() == ID_union_tag)
58  return follow_tag(to_union_tag_type(src));
59 
60  if(src.id() == ID_struct_tag)
61  return follow_tag(to_struct_tag_type(src));
62 
63  if(src.id()!=ID_symbol)
64  return src;
65 
66  const symbolt *symbol = &lookup(to_symbol_type(src));
67 
68  // let's hope it's not cyclic...
69  while(true)
70  {
71  DATA_INVARIANT(symbol->is_type, "symbol type points to type");
72 
73  if(symbol->type.id() == ID_symbol)
74  symbol = &lookup(to_symbol_type(symbol->type));
75  else
76  return symbol->type;
77  }
78 }
79 
81 {
82  const symbolt &symbol=lookup(src.get_identifier());
83  assert(symbol.is_type);
84  assert(symbol.type.id()==ID_union || symbol.type.id()==ID_incomplete_union);
85  return symbol.type;
86 }
87 
89 {
90  const symbolt &symbol=lookup(src.get_identifier());
91  assert(symbol.is_type);
92  assert(symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct);
93  return symbol.type;
94 }
95 
97 {
98  const symbolt &symbol=lookup(src.get_identifier());
99  assert(symbol.is_type);
100  assert(symbol.type.id()==ID_c_enum || symbol.type.id()==ID_incomplete_c_enum);
101  return symbol.type;
102 }
103 
105 {
106  if(expr.id()==ID_symbol)
107  {
108  const symbolt &symbol = lookup(to_symbol_expr(expr));
109 
110  if(symbol.is_macro && !symbol.value.is_nil())
111  {
112  expr=symbol.value;
113  follow_macros(expr);
114  }
115 
116  return;
117  }
118 
119  Forall_operands(it, expr)
120  follow_macros(*it);
121 }
122 
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, ::smallest_unused_suffix(prefix, symbol_table1->symbols));
129 
130  if(symbol_table2!=nullptr)
131  m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table2->symbols));
132 
133  return m;
134 }
135 
137  const irep_idt &name,
138  const symbolt *&symbol) const
139 {
140  symbol_tablet::symbolst::const_iterator it;
141 
142  if(symbol_table1!=nullptr)
143  {
144  it=symbol_table1->symbols.find(name);
145 
146  if(it!=symbol_table1->symbols.end())
147  {
148  symbol=&(it->second);
149  return false;
150  }
151  }
152 
153  if(symbol_table2!=nullptr)
154  {
155  it=symbol_table2->symbols.find(name);
156 
157  if(it!=symbol_table2->symbols.end())
158  {
159  symbol=&(it->second);
160  return false;
161  }
162  }
163 
164  return true;
165 }
166 
167 std::size_t
168 multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
169 {
170  std::size_t m = 0;
171 
172  for(const auto &st : symbol_table_list)
173  m = std::max(m, ::smallest_unused_suffix(prefix, st->symbols));
174 
175  return m;
176 }
177 
179  const irep_idt &name,
180  const symbolt *&symbol) const
181 {
182  symbol_tablet::symbolst::const_iterator s_it;
183 
184  for(symbol_table_listt::const_iterator
185  c_it=symbol_table_list.begin();
186  c_it!=symbol_table_list.end();
187  c_it++)
188  {
189  s_it=(*c_it)->symbols.find(name);
190 
191  if(s_it!=(*c_it)->symbols.end())
192  {
193  symbol=&(s_it->second);
194  return false;
195  }
196  }
197 
198  return true;
199 }
The type of an expression.
Definition: type.h:22
A generic tag-based type.
Definition: std_types.h:494
const irep_idt & get_identifier() const
Definition: std_types.h:509
bool is_nil() const
Definition: irep.h:172
symbol_table_listt symbol_table_list
Definition: namespace.h:142
const irep_idt & get_identifier() const
Definition: std_expr.h:128
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
exprt value
Initial value of symbol.
Definition: symbol.h:37
A union tag type.
Definition: std_types.h:584
A struct tag type.
Definition: std_types.h:547
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
static std::size_t smallest_unused_suffix(const std::string &prefix, const symbol_tablet::symbolst &symbols)
Definition: namespace.cpp:24
const symbolt & lookup(const irep_idt &name) const
Definition: namespace.h:33
virtual ~namespace_baset()
Definition: namespace.cpp:36
void follow_macros(exprt &) const
Definition: namespace.cpp:104
const irep_idt & id() const
Definition: irep.h:259
A reference into the symbol table.
Definition: std_types.h:110
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:168
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a generic typet to a union_tag_typet.
Definition: std_types.h:603
const symbol_tablet * symbol_table1
Definition: namespace.h:112
std::unordered_map< irep_idt, symbolt > symbolst
API to expression classes.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a generic typet to a struct_tag_typet.
Definition: std_types.h:566
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const typet & follow(const typet &) const
Definition: namespace.cpp:55
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
const symbolst & symbols
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:178
Base class for all expressions.
Definition: expr.h:42
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:123
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const symbol_tablet * symbol_table2
Definition: namespace.h:112
#define Forall_operands(it, expr)
Definition: expr.h:23
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool is_type
Definition: symbol.h:63
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
An enum tag type.
Definition: std_types.h:728
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:136
const irep_idt & get_identifier() const
Definition: std_types.h:123