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