cprover
cpp_typecheck_enum_type.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cpp_typecheck.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/config.h>
17 
18 #include <ansi-c/c_qualifiers.h>
19 
20 #include "cpp_enum_type.h"
21 
23 {
24  c_enum_typet &c_enum_type=to_c_enum_type(enum_symbol.type);
25 
26  exprt &body=static_cast<exprt &>(c_enum_type.add(ID_body));
27  irept::subt &components=body.get_sub();
28 
29  c_enum_tag_typet enum_tag_type(enum_symbol.name);
30 
31  mp_integer i=0;
32 
33  Forall_irep(it, components)
34  {
35  const irep_idt &name=it->get(ID_name);
36 
37  if(it->find(ID_value).is_not_nil())
38  {
39  exprt &value=static_cast<exprt &>(it->add(ID_value));
40  typecheck_expr(value);
41  implicit_typecast(value, c_enum_type.subtype());
42  make_constant(value);
43  if(to_integer(value, i))
44  {
46  error() << "failed to produce integer for enum constant" << eom;
47  throw 0;
48  }
49  }
50 
51  exprt value_expr=from_integer(i, c_enum_type.subtype());
52  value_expr.type()=enum_tag_type; // override type
53 
54  symbolt symbol;
55 
56  symbol.name=id2string(enum_symbol.name)+"::"+id2string(name);
57  symbol.base_name=name;
58  symbol.value=value_expr;
59  symbol.location=
60  static_cast<const source_locationt &>(it->find(ID_C_source_location));
61  symbol.mode=ID_cpp;
62  symbol.module=module;
63  symbol.type=enum_tag_type;
64  symbol.is_type=false;
65  symbol.is_macro=true;
66 
67  symbolt *new_symbol;
68  if(symbol_table.move(symbol, new_symbol))
69  {
71  error() << "cpp_typecheckt::typecheck_enum_body: "
72  << "symbol_table.move() failed" << eom;
73  throw 0;
74  }
75 
76  cpp_idt &scope_identifier=
77  cpp_scopes.put_into_scope(*new_symbol);
78 
79  scope_identifier.id_class=cpp_idt::id_classt::SYMBOL;
80 
81  ++i;
82  }
83 }
84 
86 {
87  // first save qualifiers
88  c_qualifierst qualifiers;
89  qualifiers.read(type);
90 
91  cpp_enum_typet &enum_type=to_cpp_enum_type(type);
92  bool anonymous=!enum_type.has_tag();
93  irep_idt base_name;
94 
95  cpp_save_scopet save_scope(cpp_scopes);
96 
97  if(anonymous)
98  {
99  // we fabricate a tag based on the enum constants contained
100  base_name=enum_type.generate_anon_tag();
101  }
102  else
103  {
104  const cpp_namet &tag=enum_type.tag();
105 
106  cpp_template_args_non_tct template_args;
107  template_args.make_nil();
108 
109  cpp_typecheck_resolvet resolver(*this);
110  resolver.resolve_scope(tag, base_name, template_args);
111  }
112 
113  bool has_body=enum_type.has_body();
114  bool tag_only_declaration=enum_type.get_tag_only_declaration();
115 
116  cpp_scopet &dest_scope=
117  tag_scope(base_name, has_body, tag_only_declaration);
118 
119  const irep_idt symbol_name=
120  dest_scope.prefix+"tag-"+id2string(base_name);
121 
122  // check if we have it
123 
124  symbol_tablet::symbolst::const_iterator previous_symbol=
125  symbol_table.symbols.find(symbol_name);
126 
127  if(previous_symbol!=symbol_table.symbols.end())
128  {
129  // we do!
130 
131  const symbolt &symbol=previous_symbol->second;
132 
133  if(has_body)
134  {
136  error() << "error: enum symbol `" << base_name
137  << "' declared previously\n"
138  << "location of previous definition: "
139  << symbol.location << eom;
140  throw 0;
141  }
142  }
143  else if(
144  has_body ||
146  {
147  std::string pretty_name=
149 
150  // C++11 enumerations have an underlying type,
151  // which defaults to int.
152  // enums without underlying type may be 'packed'.
153  if(type.subtype().is_nil())
154  type.subtype()=signed_int_type();
155  else
156  {
157  typecheck_type(type.subtype());
158  if(type.subtype().id()==ID_signedbv ||
159  type.subtype().id()==ID_unsignedbv)
160  {
161  }
162  else
163  {
165  error() << "underlying type must be integral" << eom;
166  throw 0;
167  }
168  }
169 
170  symbolt symbol;
171 
172  symbol.name=symbol_name;
173  symbol.base_name=base_name;
174  symbol.value.make_nil();
175  symbol.location=type.source_location();
176  symbol.mode=ID_cpp;
177  symbol.module=module;
178  symbol.type.swap(type);
179  symbol.is_type=true;
180  symbol.is_macro=false;
181  symbol.pretty_name=pretty_name;
182 
183  // move early, must be visible before doing body
184  symbolt *new_symbol;
185  if(symbol_table.move(symbol, new_symbol))
186  {
187  error().source_location=symbol.location;
188  error() << "cpp_typecheckt::typecheck_enum_type: "
189  << "symbol_table.move() failed" << eom;
190  throw 0;
191  }
192 
193  // put into scope
194  cpp_idt &scope_identifier=
195  cpp_scopes.put_into_scope(*new_symbol, dest_scope);
196 
197  scope_identifier.id_class=cpp_idt::id_classt::CLASS;
198  scope_identifier.is_scope = true;
199 
200  cpp_save_scopet save_scope_before_enum_typecheck(cpp_scopes);
201 
202  if(new_symbol->type.get_bool(ID_C_class))
203  cpp_scopes.go_to(scope_identifier);
204 
205  if(has_body)
206  typecheck_enum_body(*new_symbol);
207  }
208  else
209  {
211  error() << "use of enum `" << base_name
212  << "' without previous declaration" << eom;
213  throw 0;
214  }
215 
216  // create enum tag expression, and add the qualifiers
217  type=c_enum_tag_typet(symbol_name);
218  qualifiers.write(type);
219 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
struct configt::ansi_ct ansi_c
BigInt mp_integer
Definition: mp_arith.h:22
irep_idt generate_anon_tag() const
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< irept > subt
Definition: irep.h:160
virtual void make_constant(exprt &expr)
irep_idt mode
Language mode.
Definition: symbol.h:49
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
void typecheck_expr(exprt &) override
exprt value
Initial value of symbol.
Definition: symbol.h:34
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
bool has_body() const
Definition: cpp_enum_type.h:51
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:56
void typecheck_enum_body(symbolt &symbol)
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
typet & type()
Return the type of the expression.
Definition: expr.h:68
Symbol table entry.
Definition: symbol.h:27
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
configt config
Definition: config.cpp:24
subt & get_sub()
Definition: irep.h:317
const cpp_namet & tag() const
Definition: cpp_enum_type.h:26
symbol_tablet & symbol_table
void typecheck_enum_type(typet &type)
std::string prefix
Definition: cpp_id.h:80
const irep_idt & id() const
Definition: irep.h:259
bool is_scope
Definition: cpp_id.h:48
bool has_tag() const
Definition: cpp_enum_type.h:31
flavourt mode
Definition: config.h:115
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
source_locationt source_location
Definition: message.h:236
void typecheck_type(typet &) override
id_classt id_class
Definition: cpp_id.h:51
void implicit_typecast(exprt &expr, const typet &type) override
mstreamt & error() const
Definition: message.h:386
virtual void read(const typet &src) override
C++ Language Type Checking.
C++ Language Type Checking.
#define Forall_irep(it, irep)
Definition: irep.h:66
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:64
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
const symbolst & symbols
const source_locationt & source_location() const
Definition: type.h:62
static eomt eom
Definition: message.h:284
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
Base class for all expressions.
Definition: expr.h:54
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
irept & add(const irep_namet &name)
Definition: irep.cpp:305
const irep_idt module
void make_nil()
Definition: irep.h:315
void swap(irept &irep)
Definition: irep.h:303
virtual void write(typet &src) const override
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: std_types.h:697
Definition: cpp_id.h:28
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
bool is_type
Definition: symbol.h:61
const typet & subtype() const
Definition: type.h:38
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
The type of C enums.
Definition: std_types.h:647
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:711
bool is_macro
Definition: symbol.h:61
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
cpp_scopest cpp_scopes