cprover
type2name.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Type Naming for C
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #include "type2name.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/invariant.h>
16 #include <util/namespace.h>
18 #include <util/std_expr.h>
19 #include <util/std_types.h>
20 #include <util/symbol_table.h>
21 
22 typedef std::unordered_map<irep_idt, std::pair<size_t, bool>> symbol_numbert;
23 
24 static std::string type2name(
25  const typet &type,
26  const namespacet &ns,
27  symbol_numbert &symbol_number);
28 
29 static std::string type2name_tag(
30  const tag_typet &type,
31  const namespacet &ns,
32  symbol_numbert &symbol_number)
33 {
34  const irep_idt &identifier = type.get_identifier();
35 
36  const symbolt *symbol;
37 
38  if(ns.lookup(identifier, symbol))
39  return "SYM#"+id2string(identifier)+"#";
40 
41  assert(symbol && symbol->is_type);
42 
43  if(symbol->type.id()!=ID_struct &&
44  symbol->type.id()!=ID_union)
45  return type2name(symbol->type, ns, symbol_number);
46 
47  // assign each symbol a number when seen for the first time
48  std::pair<symbol_numbert::iterator, bool> entry=
49  symbol_number.insert(std::make_pair(
50  identifier,
51  std::make_pair(symbol_number.size(), true)));
52 
53  std::string result = "SYM" +
55  '#' + std::to_string(entry.first->second.first);
56 
57  // new entry, add definition
58  if(entry.second)
59  {
60  result+="={";
61  result+=type2name(symbol->type, ns, symbol_number);
62  result+='}';
63 
64  entry.first->second.second=false;
65  }
66 
67  return result;
68 }
69 
70 static std::string pointer_offset_bits_as_string(
71  const typet &type,
72  const namespacet &ns)
73 {
74  auto bits = pointer_offset_bits(type, ns);
75  CHECK_RETURN(bits.has_value());
76  return integer2string(*bits);
77 }
78 
79 static std::string type2name(
80  const typet &type,
81  const namespacet &ns,
82  symbol_numbert &symbol_number)
83 {
84  std::string result;
85 
86  // qualifiers first
87  if(type.get_bool(ID_C_constant))
88  result+='c';
89 
90  if(type.get_bool(ID_C_restricted))
91  result+='r';
92 
93  if(type.get_bool(ID_C_volatile))
94  result+='v';
95 
96  if(type.get_bool(ID_C_transparent_union))
97  result+='t';
98 
99  if(type.get_bool(ID_C_noreturn))
100  result+='n';
101 
102  // this isn't really a qualifier, but the linker needs to
103  // distinguish these - should likely be fixed in the linker instead
104  if(!type.source_location().get_function().empty())
105  result+='l';
106 
107  if(type.id().empty())
108  throw "empty type encountered";
109  else if(type.id()==ID_empty)
110  result+='V';
111  else if(type.id()==ID_signedbv)
112  result+="S" + pointer_offset_bits_as_string(type, ns);
113  else if(type.id()==ID_unsignedbv)
114  result+="U" + pointer_offset_bits_as_string(type, ns);
115  else if(type.id()==ID_bool ||
116  type.id()==ID_c_bool)
117  result+='B';
118  else if(type.id()==ID_integer)
119  result+='I';
120  else if(type.id()==ID_real)
121  result+='R';
122  else if(type.id()==ID_complex)
123  result+='C';
124  else if(type.id()==ID_floatbv)
125  result+="F" + pointer_offset_bits_as_string(type, ns);
126  else if(type.id()==ID_fixedbv)
127  result+="X" + pointer_offset_bits_as_string(type, ns);
128  else if(type.id()==ID_natural)
129  result+='N';
130  else if(type.id()==ID_pointer)
131  {
132  if(type.get_bool(ID_C_reference))
133  result+='&';
134  else
135  result+='*';
136  }
137  else if(type.id()==ID_code)
138  {
139  const code_typet &t=to_code_type(type);
140  const code_typet::parameterst parameters=t.parameters();
141  result+=type2name(t.return_type(), ns, symbol_number)+"(";
142 
143  for(code_typet::parameterst::const_iterator
144  it=parameters.begin();
145  it!=parameters.end();
146  it++)
147  {
148  if(it!=parameters.begin())
149  result+='|';
150  result+=type2name(it->type(), ns, symbol_number);
151  }
152 
153  if(t.has_ellipsis())
154  {
155  if(!parameters.empty())
156  result+='|';
157  result+="...";
158  }
159 
160  result+=")->";
161  result+=type2name(t.return_type(), ns, symbol_number);
162  }
163  else if(type.id()==ID_array)
164  {
165  const exprt &size = to_array_type(type).size();
166 
167  if(size.id() == ID_symbol)
168  result += "ARR" + id2string(to_symbol_expr(size).get_identifier());
169  else
170  {
171  const auto size_int = numeric_cast<mp_integer>(size);
172 
173  if(!size_int.has_value())
174  result += "ARR?";
175  else
176  result += "ARR" + integer2string(*size_int);
177  }
178  }
179  else if(
180  type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
181  type.id() == ID_union_tag)
182  {
183  result += type2name_tag(to_tag_type(type), ns, symbol_number);
184  }
185  else if(type.id()==ID_struct ||
186  type.id()==ID_union)
187  {
188  const auto &struct_union_type = to_struct_union_type(type);
189 
190  if(struct_union_type.is_incomplete())
191  {
192  if(type.id() == ID_struct)
193  result += "ST?";
194  else if(type.id() == ID_union)
195  result += "UN?";
196  }
197  else
198  {
199  if(type.id() == ID_struct)
200  result += "ST";
201  if(type.id() == ID_union)
202  result += "UN";
203  result += '[';
204  bool first = true;
205  for(const auto &c : struct_union_type.components())
206  {
207  if(!first)
208  result += '|';
209  else
210  first = false;
211 
212  result += type2name(c.type(), ns, symbol_number);
213  const irep_idt &component_name = c.get_name();
214  CHECK_RETURN(!component_name.empty());
215  result += "'" + id2string(component_name) + "'";
216  }
217  result += ']';
218  }
219  }
220  else if(type.id()==ID_c_enum)
221  {
222  const c_enum_typet &t=to_c_enum_type(type);
223 
224  if(t.is_incomplete())
225  result += "EN?";
226  else
227  {
228  result += "EN";
229  const c_enum_typet::memberst &members = t.members();
230  result += '[';
231  for(c_enum_typet::memberst::const_iterator it = members.begin();
232  it != members.end();
233  ++it)
234  {
235  if(it != members.begin())
236  result += '|';
237  result += id2string(it->get_value());
238  result += "'" + id2string(it->get_identifier()) + "'";
239  }
240  }
241  }
242  else if(type.id()==ID_c_bit_field)
243  result+="BF"+pointer_offset_bits_as_string(type, ns);
244  else if(type.id()==ID_vector)
245  result+="VEC"+type.get_string(ID_size);
246  else
247  throw "unknown type '"+type.id_string()+"' encountered";
248 
249  if(type.has_subtype())
250  {
251  result+='{';
252  result+=type2name(type.subtype(), ns, symbol_number);
253  result+='}';
254  }
255 
256  if(type.has_subtypes())
257  {
258  result+='$';
259  forall_subtypes(it, type)
260  {
261  result+=type2name(*it, ns, symbol_number);
262  result+='|';
263  }
264  result[result.size()-1]='$';
265  }
266 
267  return result;
268 }
269 
270 std::string type2name(const typet &type, const namespacet &ns)
271 {
272  symbol_numbert symbol_number;
273  return type2name(type, ns, symbol_number);
274 }
tag_typet::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:451
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:56
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:813
symbol_numbert
std::unordered_map< irep_idt, std::pair< size_t, bool > > symbol_numbert
Definition: type2name.cpp:22
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:620
c_enum_typet::is_incomplete
bool is_incomplete() const
enum types may be incomplete
Definition: std_types.h:652
arith_tools.h
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:681
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
typet::has_subtype
bool has_subtype() const
Definition: type.h:65
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
c_enum_typet::memberst
std::vector< c_enum_membert > memberst
Definition: std_types.h:644
type2name.h
typet::has_subtypes
bool has_subtypes() const
Definition: type.h:62
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
namespace.h
pointer_offset_bits_as_string
static std::string pointer_offset_bits_as_string(const typet &type, const namespacet &ns)
Definition: type2name.cpp:70
array_typet::size
const exprt & size() const
Definition: std_types.h:973
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:163
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
messaget::result
mstreamt & result() const
Definition: message.h:395
to_tag_type
const tag_typet & to_tag_type(const typet &type)
Cast a typet to a tag_typet.
Definition: std_types.h:475
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
type2name
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:79
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
std_types.h
irept::id_string
const std::string & id_string() const
Definition: irep.h:421
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
dstringt::empty
bool empty() const
Definition: dstring.h:88
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:437
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
type2name_tag
static std::string type2name_tag(const tag_typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:29
forall_subtypes
#define forall_subtypes(it, type)
Definition: type.h:216
irept::get_string
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:431
symbolt
Symbol table entry.
Definition: symbol.h:28
symbolt::is_type
bool is_type
Definition: symbol.h:61
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
symbol_table.h
Author: Diffblue Ltd.
std_expr.h
c_enum_typet::members
const memberst & members() const
Definition: std_types.h:646
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106