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_symbol)
58  return src;
59 
60  const symbolt *symbol = &lookup(to_symbol_type(src));
61 
62  // let's hope it's not cyclic...
63  while(true)
64  {
65  DATA_INVARIANT(symbol->is_type, "symbol type points to type");
66 
67  if(symbol->type.id() == ID_symbol)
68  symbol = &lookup(to_symbol_type(symbol->type));
69  else
70  return symbol->type;
71  }
72 }
73 
75 {
76  const symbolt &symbol=lookup(src.get_identifier());
77  assert(symbol.is_type);
78  assert(symbol.type.id()==ID_union || symbol.type.id()==ID_incomplete_union);
79  return symbol.type;
80 }
81 
83 {
84  const symbolt &symbol=lookup(src.get_identifier());
85  assert(symbol.is_type);
86  assert(symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct);
87  return symbol.type;
88 }
89 
91 {
92  const symbolt &symbol=lookup(src.get_identifier());
93  assert(symbol.is_type);
94  assert(symbol.type.id()==ID_c_enum || symbol.type.id()==ID_incomplete_c_enum);
95  return symbol.type;
96 }
97 
99 {
100  if(expr.id()==ID_symbol)
101  {
102  const symbolt &symbol = lookup(to_symbol_expr(expr));
103 
104  if(symbol.is_macro && !symbol.value.is_nil())
105  {
106  expr=symbol.value;
107  follow_macros(expr);
108  }
109 
110  return;
111  }
112 
113  Forall_operands(it, expr)
114  follow_macros(*it);
115 }
116 
117 std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
118 {
119  std::size_t m = 0;
120 
121  if(symbol_table1!=nullptr)
122  m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table1->symbols));
123 
124  if(symbol_table2!=nullptr)
125  m = std::max(m, ::smallest_unused_suffix(prefix, symbol_table2->symbols));
126 
127  return m;
128 }
129 
131  const irep_idt &name,
132  const symbolt *&symbol) const
133 {
134  symbol_tablet::symbolst::const_iterator it;
135 
136  if(symbol_table1!=nullptr)
137  {
138  it=symbol_table1->symbols.find(name);
139 
140  if(it!=symbol_table1->symbols.end())
141  {
142  symbol=&(it->second);
143  return false;
144  }
145  }
146 
147  if(symbol_table2!=nullptr)
148  {
149  it=symbol_table2->symbols.find(name);
150 
151  if(it!=symbol_table2->symbols.end())
152  {
153  symbol=&(it->second);
154  return false;
155  }
156  }
157 
158  return true;
159 }
160 
161 std::size_t
162 multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
163 {
164  std::size_t m = 0;
165 
166  for(const auto &st : symbol_table_list)
167  m = std::max(m, ::smallest_unused_suffix(prefix, st->symbols));
168 
169  return m;
170 }
171 
173  const irep_idt &name,
174  const symbolt *&symbol) const
175 {
176  symbol_tablet::symbolst::const_iterator s_it;
177 
178  for(symbol_table_listt::const_iterator
179  c_it=symbol_table_list.begin();
180  c_it!=symbol_table_list.end();
181  c_it++)
182  {
183  s_it=(*c_it)->symbols.find(name);
184 
185  if(s_it!=(*c_it)->symbols.end())
186  {
187  symbol=&(s_it->second);
188  return false;
189  }
190  }
191 
192  return true;
193 }
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:102
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:74
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:98
const irep_idt & id() const
Definition: irep.h:189
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:162
const symbol_tablet * symbol_table1
Definition: namespace.h:112
std::unordered_map< irep_idt, symbolt > symbolst
API to expression classes.
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
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:172
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:117
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:257
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:130
const irep_idt & get_identifier() const
Definition: std_types.h:123