cprover
symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "symbol.h"
10 
11 #include <ostream>
12 
13 #include "source_location.h"
14 #include "std_expr.h"
15 #include "string_utils.h"
16 #include "suffix.h"
17 
20 void symbolt::show(std::ostream &out) const
21 {
22  out << " " << name << '\n';
23  out << " type: " << type.pretty(4) << '\n'
24  << " value: " << value.pretty(4) << '\n';
25 
26  out << " flags:";
27  if(is_lvalue)
28  out << " lvalue";
30  out << " static_lifetime";
31  if(is_thread_local)
32  out << " thread_local";
33  if(is_file_local)
34  out << " file_local";
35  if(is_type)
36  out << " type";
37  if(is_extern)
38  out << " extern";
39  if(is_input)
40  out << " input";
41  if(is_output)
42  out << " output";
43  if(is_macro)
44  out << " macro";
45  if(is_parameter)
46  out << " parameter";
47  if(is_auxiliary)
48  out << " auxiliary";
49  if(is_weak)
50  out << " weak";
51  if(is_property)
52  out << " property";
53  if(is_state_var)
54  out << " state_var";
55  if(is_exported)
56  out << " exported";
57  if(is_volatile)
58  out << " volatile";
59  if(!mode.empty())
60  out << " mode=" << mode;
61  if(!base_name.empty())
62  out << " base_name=" << base_name;
63  if(!module.empty())
64  out << " module=" << module;
65  if(!pretty_name.empty())
66  out << " pretty_name=" << pretty_name;
67  out << '\n';
68  out << " location: " << location << '\n';
69 
70  out << '\n';
71 }
72 
77 std::ostream &operator<<(std::ostream &out,
78  const symbolt &symbol)
79 {
80  symbol.show(out);
81  return out;
82 }
83 
87 {
88  #define SYM_SWAP1(x) x.swap(b.x)
89 
90  SYM_SWAP1(type);
92  SYM_SWAP1(name);
96  SYM_SWAP1(mode);
98 
99  #define SYM_SWAP2(x) std::swap(x, b.x)
100 
117 }
118 
123 {
124  return symbol_exprt(name, type);
125 }
126 
130 {
131  // Well-formedness criterion number 1 is for a symbol
132  // to have a non-empty mode (see #1880)
133  if(mode.empty())
134  {
135  return false;
136  }
137 
138  // Well-formedness criterion number 2 is for a symbol
139  // to have it's base name as a suffix to it's more
140  // general name.
141 
142  // Exception: Java symbols' base names do not have type signatures
143  // (for example, they can have name "someclass.method:(II)V" and base name
144  // "method")
145  if(
146  !has_suffix(id2string(name), id2string(base_name)) && mode != ID_java &&
147  mode != ID_cpp)
148  {
149  bool criterion_must_hold = true;
150 
151  // There are some special cases where this criterion doesn't hold, check
152  // to see if we have one of those cases
153 
154  if(is_type)
155  {
156  // Typedefs
157  if(
158  type.find(ID_C_typedef).is_not_nil() &&
159  type.find(ID_C_typedef).id() == base_name)
160  {
161  criterion_must_hold = false;
162  }
163 
164  // Tag types
165  if(type.find(ID_tag).is_not_nil() && type.find(ID_tag).id() == base_name)
166  {
167  criterion_must_hold = false;
168  }
169  }
170 
171  // Linker renaming may have added $linkN suffixes to the name, and other
172  // suffixes such as #return_value may have then be subsequently added.
173  // Strip out the first $linkN substring and then see if the criterion holds
174  const auto &unstripped_name = id2string(name);
175  const size_t dollar_link_start_pos = unstripped_name.find("$link");
176 
177  if(dollar_link_start_pos != std::string::npos)
178  {
179  size_t dollar_link_end_pos = dollar_link_start_pos + 5;
180  while(isdigit(unstripped_name[dollar_link_end_pos]))
181  {
182  ++dollar_link_end_pos;
183  }
184 
185  const auto stripped_name =
186  unstripped_name.substr(0, dollar_link_start_pos) +
187  unstripped_name.substr(dollar_link_end_pos, std::string::npos);
188 
189  if(has_suffix(stripped_name, id2string(base_name)))
190  criterion_must_hold = false;
191  }
192 
193  if(criterion_must_hold)
194  {
195  // For all other cases this criterion should hold
196  return false;
197  }
198  }
199 
200  return true;
201 }
202 
203 bool symbolt::operator==(const symbolt &other) const
204 {
205  // clang-format off
206  return
207  type == other.type &&
208  value == other.value &&
209  location == other.location &&
210  name == other.name &&
211  module == other.module &&
212  base_name == other.base_name &&
213  mode == other.mode &&
214  pretty_name == other.pretty_name &&
215  is_type == other.is_type &&
216  is_macro == other.is_macro &&
217  is_exported == other.is_exported &&
218  is_input == other.is_input &&
219  is_output == other.is_output &&
220  is_state_var == other.is_state_var &&
221  is_property == other.is_property &&
222  is_parameter == other.is_parameter &&
223  is_auxiliary == other.is_auxiliary &&
224  is_weak == other.is_weak &&
225  is_lvalue == other.is_lvalue &&
227  is_thread_local == other.is_thread_local &&
228  is_file_local == other.is_file_local &&
229  is_extern == other.is_extern &&
230  is_volatile == other.is_volatile;
231  // clang-format on
232 }
233 
234 bool symbolt::operator!=(const symbolt &other) const
235 {
236  return !(*this == other);
237 }
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
string_utils.h
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:488
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
symbolt::operator==
bool operator==(const symbolt &other) const
Definition: symbol.cpp:203
symbolt::is_input
bool is_input
Definition: symbol.h:62
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
symbolt::is_well_formed
bool is_well_formed() const
Check that a symbol is well formed.
Definition: symbol.cpp:129
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
source_location.h
symbolt::is_exported
bool is_exported
Definition: symbol.h:61
symbolt::is_parameter
bool is_parameter
Definition: symbol.h:67
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
SYM_SWAP1
#define SYM_SWAP1(x)
dstringt::empty
bool empty() const
Definition: dstring.h:88
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
symbolt::is_output
bool is_output
Definition: symbol.h:62
symbolt::is_extern
bool is_extern
Definition: symbol.h:66
suffix.h
symbolt::is_volatile
bool is_volatile
Definition: symbol.h:66
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
symbolt::show
void show(std::ostream &out) const
Dump the state of a symbol object to a given output stream.
Definition: symbol.cpp:20
symbolt::is_auxiliary
bool is_auxiliary
Definition: symbol.h:67
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
symbolt::swap
void swap(symbolt &b)
Swap values between two symbols.
Definition: symbol.cpp:86
symbolt::operator!=
bool operator!=(const symbolt &other) const
Definition: symbol.cpp:234
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
std_expr.h
API to expression classes.
symbolt::is_weak
bool is_weak
Definition: symbol.h:67
SYM_SWAP2
#define SYM_SWAP2(x)
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
symbolt::is_property
bool is_property
Definition: symbol.h:62
operator<<
std::ostream & operator<<(std::ostream &out, const symbolt &symbol)
Overload of stream operator to work with symbols.
Definition: symbol.cpp:77