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_symbol(
30  const typet &type,
31  const namespacet &ns,
32  symbol_numbert &symbol_number)
33 {
34  const irep_idt &identifier=type.get(ID_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  std::string result;
48 
49  // assign each symbol a number when seen for the first time
50  std::pair<symbol_numbert::iterator, bool> entry=
51  symbol_number.insert(std::make_pair(
52  identifier,
53  std::make_pair(symbol_number.size(), true)));
54 
55  // new entry, add definition
56  if(entry.second)
57  {
58  result="SYM#"+std::to_string(entry.first->second.first);
59  result+="={";
60  result+=type2name(symbol->type, ns, symbol_number);
61  result+='}';
62 
63  entry.first->second.second=false;
64  }
65 #if 0
66  // in recursion, print the shorthand only
67  else if(entry.first->second.second)
68  result="SYM#"+std::to_string(entry.first->second.first);
69  // entering recursion
70  else
71  {
72  entry.first->second.second=true;
73  result=type2name(symbol->type, ns, symbol_number);
74  entry.first->second.second=false;
75  }
76 #else
77  // shorthand only as structs/unions are always symbols
78  else
79  result="SYM#"+std::to_string(entry.first->second.first);
80 #endif
81 
82  return result;
83 }
84 
85 static std::string pointer_offset_bits_as_string(
86  const typet &type,
87  const namespacet &ns)
88 {
89  mp_integer bits = pointer_offset_bits(type, ns);
90  CHECK_RETURN(bits != -1);
91  return integer2string(bits);
92 }
93 
94 static bool parent_is_sym_check=false;
95 static std::string type2name(
96  const typet &type,
97  const namespacet &ns,
98  symbol_numbert &symbol_number)
99 {
100  std::string result;
101 
102  // qualifiers first
103  if(type.get_bool(ID_C_constant))
104  result+='c';
105 
106  if(type.get_bool(ID_C_restricted))
107  result+='r';
108 
109  if(type.get_bool(ID_C_volatile))
110  result+='v';
111 
112  if(type.get_bool(ID_C_transparent_union))
113  result+='t';
114 
115  if(type.get_bool(ID_C_noreturn))
116  result+='n';
117 
118  // this isn't really a qualifier, but the linker needs to
119  // distinguish these - should likely be fixed in the linker instead
120  if(!type.source_location().get_function().empty())
121  result+='l';
122 
123  if(type.id().empty())
124  throw "empty type encountered";
125  else if(type.id()==ID_empty)
126  result+='V';
127  else if(type.id()==ID_signedbv)
128  result+="S" + pointer_offset_bits_as_string(type, ns);
129  else if(type.id()==ID_unsignedbv)
130  result+="U" + pointer_offset_bits_as_string(type, ns);
131  else if(type.id()==ID_bool ||
132  type.id()==ID_c_bool)
133  result+='B';
134  else if(type.id()==ID_integer)
135  result+='I';
136  else if(type.id()==ID_real)
137  result+='R';
138  else if(type.id()==ID_complex)
139  result+='C';
140  else if(type.id()==ID_floatbv)
141  result+="F" + pointer_offset_bits_as_string(type, ns);
142  else if(type.id()==ID_fixedbv)
143  result+="X" + pointer_offset_bits_as_string(type, ns);
144  else if(type.id()==ID_natural)
145  result+='N';
146  else if(type.id()==ID_pointer)
147  {
148  if(type.get_bool(ID_C_reference))
149  result+='&';
150  else
151  result+='*';
152  }
153  else if(type.id()==ID_code)
154  {
155  const code_typet &t=to_code_type(type);
156  const code_typet::parameterst parameters=t.parameters();
157  result+=type2name(t.return_type(), ns, symbol_number)+"(";
158 
159  for(code_typet::parameterst::const_iterator
160  it=parameters.begin();
161  it!=parameters.end();
162  it++)
163  {
164  if(it!=parameters.begin())
165  result+='|';
166  result+=type2name(it->type(), ns, symbol_number);
167  }
168 
169  if(t.has_ellipsis())
170  {
171  if(!parameters.empty())
172  result+='|';
173  result+="...";
174  }
175 
176  result+=")->";
177  result+=type2name(t.return_type(), ns, symbol_number);
178  }
179  else if(type.id()==ID_array)
180  {
181  const array_typet &t=to_array_type(type);
182  mp_integer size;
183  if(t.size().id()==ID_symbol)
184  result += "ARR" + id2string(to_symbol_expr(t.size()).get_identifier());
185  else if(to_integer(t.size(), size))
186  result+="ARR?";
187  else
188  result+="ARR"+integer2string(size);
189  }
190  else if(type.id()==ID_symbol ||
191  type.id()==ID_c_enum_tag ||
192  type.id()==ID_struct_tag ||
193  type.id()==ID_union_tag)
194  {
195  parent_is_sym_check=true;
196  result+=type2name_symbol(type, ns, symbol_number);
197  }
198  else if(type.id()==ID_struct ||
199  type.id()==ID_union)
200  {
201  assert(parent_is_sym_check);
202  parent_is_sym_check=false;
203  if(type.id()==ID_struct)
204  result+="ST";
205  if(type.id()==ID_union)
206  result+="UN";
208  const struct_union_typet::componentst &components = t.components();
209  result+='[';
210  for(struct_union_typet::componentst::const_iterator
211  it=components.begin();
212  it!=components.end();
213  it++)
214  {
215  if(it!=components.begin())
216  result+='|';
217  result+=type2name(it->type(), ns, symbol_number);
218  irep_idt component_name = it->get_name();
219  CHECK_RETURN(!component_name.empty());
220  result+="'"+id2string(component_name)+"'";
221  }
222  result+=']';
223  }
224  else if(type.id()==ID_incomplete_struct)
225  result +="ST?";
226  else if(type.id()==ID_incomplete_union)
227  result +="UN?";
228  else if(type.id()==ID_c_enum)
229  {
230  result +="EN";
231  const c_enum_typet &t=to_c_enum_type(type);
232  const c_enum_typet::memberst &members=t.members();
233  result+='[';
234  for(c_enum_typet::memberst::const_iterator
235  it=members.begin();
236  it!=members.end();
237  ++it)
238  {
239  if(it!=members.begin())
240  result+='|';
241  result+=id2string(it->get_value());
242  result+="'"+id2string(it->get_identifier())+"'";
243  }
244  }
245  else if(type.id()==ID_incomplete_c_enum)
246  result +="EN?";
247  else if(type.id()==ID_c_bit_field)
248  result+="BF"+pointer_offset_bits_as_string(type, ns);
249  else if(type.id()==ID_vector)
250  result+="VEC"+type.get_string(ID_size);
251  else
252  throw "unknown type '"+type.id_string()+"' encountered";
253 
254  if(type.has_subtype())
255  {
256  result+='{';
257  result+=type2name(type.subtype(), ns, symbol_number);
258  result+='}';
259  }
260 
261  if(type.has_subtypes())
262  {
263  result+='$';
264  forall_subtypes(it, type)
265  {
266  result+=type2name(*it, ns, symbol_number);
267  result+='|';
268  }
269  result[result.size()-1]='$';
270  }
271 
272  return result;
273 }
274 
275 std::string type2name(const typet &type, const namespacet &ns)
276 {
277  parent_is_sym_check=true;
278  symbol_numbert symbol_number;
279  return type2name(type, ns, symbol_number);
280 }
281 
282 std::string type2name(const typet &type)
283 {
284  symbol_tablet symbol_table;
285  return type2name(type, namespacet(symbol_table));
286 }
static std::string type2name(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:95
The type of an expression.
Definition: type.h:22
#define forall_subtypes(it, type)
Definition: type.h:161
bool has_subtypes() const
Definition: type.h:72
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
bool has_subtype() const
Definition: type.h:79
bool has_ellipsis() const
Definition: std_types.h:861
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
const irep_idt & get_function() const
std::vector< componentt > componentst
Definition: std_types.h:243
std::vector< parametert > parameterst
Definition: std_types.h:767
const componentst & components() const
Definition: std_types.h:245
const memberst & members() const
Definition: std_types.h:694
mp_integer pointer_offset_bits(const typet &type, const namespacet &ns)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
const irep_idt & id() const
Definition: irep.h:189
API to expression classes.
The symbol table.
Definition: symbol_table.h:19
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
static bool parent_is_sym_check
Definition: type2name.cpp:94
const exprt & size() const
Definition: std_types.h:1014
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Author: Diffblue Ltd.
std::unordered_map< irep_idt, std::pair< size_t, bool > > symbol_numbert
Definition: type2name.cpp:22
static std::string pointer_offset_bits_as_string(const typet &type, const namespacet &ns)
Definition: type2name.cpp:85
Pointer Logic.
const source_locationt & source_location() const
Definition: type.h:97
Type Naming for C.
static std::string type2name_symbol(const typet &type, const namespacet &ns, symbol_numbert &symbol_number)
Definition: type2name.cpp:29
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
mstreamt & result() const
Definition: message.h:312
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
const parameterst & parameters() const
Definition: std_types.h:905
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const std::string & id_string() const
Definition: irep.h:192
arrays with given size
Definition: std_types.h:1004
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a generic typet to a c_enum_typet.
Definition: std_types.h:710
bool is_type
Definition: symbol.h:63
const typet & subtype() const
Definition: type.h:33
std::vector< c_enum_membert > memberst
Definition: std_types.h:692
bool empty() const
Definition: dstring.h:61
The type of C enums.
Definition: std_types.h:667
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130