CBMC
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  for(auto &component : components)
34  {
35  const irep_idt &name = component.get(ID_name);
36 
37  if(component.find(ID_value).is_not_nil())
38  {
39  exprt &value = static_cast<exprt &>(component.add(ID_value));
40  typecheck_expr(value);
41  implicit_typecast(value, c_enum_type.underlying_type());
42  make_constant(value);
43  if(to_integer(to_constant_expr(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.underlying_type());
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 = static_cast<const source_locationt &>(
60  component.find(ID_C_source_location));
61  symbol.mode = enum_symbol.mode;
62  symbol.module=module;
63  symbol.type=enum_tag_type;
64  symbol.is_type=false;
65  symbol.is_macro=true;
66  symbol.is_file_local = true;
67  symbol.is_thread_local = true;
68 
69  symbolt *new_symbol;
70  if(symbol_table.move(symbol, new_symbol))
71  {
73  error() << "cpp_typecheckt::typecheck_enum_body: "
74  << "symbol_table.move() failed" << eom;
75  throw 0;
76  }
77 
78  cpp_idt &scope_identifier=
79  cpp_scopes.put_into_scope(*new_symbol);
80 
81  scope_identifier.id_class=cpp_idt::id_classt::SYMBOL;
82 
83  ++i;
84  }
85 }
86 
88 {
89  // first save qualifiers
90  c_qualifierst qualifiers;
91  qualifiers.read(type);
92 
93  cpp_enum_typet &enum_type=to_cpp_enum_type(type);
94  bool anonymous=!enum_type.has_tag();
95  irep_idt base_name;
96 
97  cpp_save_scopet save_scope(cpp_scopes);
98 
99  if(anonymous)
100  {
101  // we fabricate a tag based on the enum constants contained
102  base_name=enum_type.generate_anon_tag();
103  }
104  else
105  {
106  const cpp_namet &tag=enum_type.tag();
107 
108  cpp_template_args_non_tct template_args;
109  template_args.make_nil();
110 
111  cpp_typecheck_resolvet resolver(*this);
112  resolver.resolve_scope(tag, base_name, template_args);
113  }
114 
115  bool has_body=enum_type.has_body();
116  bool tag_only_declaration=enum_type.get_tag_only_declaration();
117 
118  cpp_scopet &dest_scope=
119  tag_scope(base_name, has_body, tag_only_declaration);
120 
121  const irep_idt symbol_name=
122  dest_scope.prefix+"tag-"+id2string(base_name);
123 
124  // check if we have it
125 
126  symbol_tablet::symbolst::const_iterator previous_symbol=
127  symbol_table.symbols.find(symbol_name);
128 
129  if(previous_symbol!=symbol_table.symbols.end())
130  {
131  // we do!
132 
133  const symbolt &symbol=previous_symbol->second;
134 
135  if(has_body)
136  {
138  error() << "error: enum symbol '" << base_name
139  << "' declared previously\n"
140  << "location of previous definition: " << symbol.location << eom;
141  throw 0;
142  }
143  }
144  else if(
145  has_body ||
147  {
148  std::string pretty_name=
150 
151  // C++11 enumerations have an underlying type,
152  // which defaults to int.
153  // enums without underlying type may be 'packed'.
154  if(type.add_subtype().is_nil())
155  type.add_subtype() = signed_int_type();
156  else
157  {
158  typecheck_type(to_type_with_subtype(type).subtype());
159  if(
160  to_type_with_subtype(type).subtype().id() != ID_signedbv &&
161  to_type_with_subtype(type).subtype().id() != ID_unsignedbv &&
162  to_type_with_subtype(type).subtype().id() != ID_c_bool)
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 << "' without previous declaration"
212  << 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 }
c_qualifierst::read
virtual void read(const typet &src) override
Definition: c_qualifiers.cpp:62
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
c_enum_typet
The type of C enums.
Definition: c_types.h:216
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
cpp_typecheckt::tag_scope
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
Definition: cpp_typecheck_compound_type.cpp:87
cpp_scopet
Definition: cpp_scope.h:20
to_cpp_enum_type
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:62
arith_tools.h
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
cpp_idt::id_classt::CLASS
@ CLASS
cpp_save_scopet
Definition: cpp_scopes.h:127
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:104
irept::make_nil
void make_nil()
Definition: irep.h:454
typet
The type of an expression, extends irept.
Definition: type.h:28
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
to_c_enum_type
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
cpp_typecheck_resolvet
Definition: cpp_typecheck_resolve.h:23
to_type_with_subtype
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:193
exprt
Base class for all expressions.
Definition: expr.h:55
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:76
to_integer
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
messaget::eom
static eomt eom
Definition: message.h:297
c_qualifiers.h
configt::ansi_c
struct configt::ansi_ct ansi_c
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
cpp_idt
Definition: cpp_id.h:22
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:4394
cpp_idt::is_scope
bool is_scope
Definition: cpp_id.h:43
cpp_enum_typet::get_tag_only_declaration
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:54
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:84
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
cpp_typecheckt::typecheck_type
void typecheck_type(typet &) override
Definition: cpp_typecheck_type.cpp:23
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:69
cpp_enum_typet::generate_anon_tag
irep_idt generate_anon_tag() const
Definition: cpp_enum_type.cpp:18
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
cpp_idt::id_classt::SYMBOL
@ SYMBOL
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
typet::source_location
const source_locationt & source_location() const
Definition: type.h:90
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
c_qualifierst::write
virtual void write(typet &src) const override
Definition: c_qualifiers.cpp:89
c_qualifierst
Definition: c_qualifiers.h:61
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:68
irept::swap
void swap(irept &irep)
Definition: irep.h:442
irept::is_nil
bool is_nil() const
Definition: irep.h:376
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_typecheck.h
typet::add_subtype
typet & add_subtype()
Definition: type.h:71
cpp_enum_typet
Definition: cpp_enum_type.h:19
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition: irep.h:160
cpp_template_args_non_tct
Definition: cpp_template_args.h:44
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:67
config
configt config
Definition: config.cpp:25
cpp_enum_type.h
source_locationt
Definition: source_location.h:18
cpp_enum_typet::has_body
bool has_body() const
Definition: cpp_enum_type.h:49
configt::ansi_ct::mode
flavourt mode
Definition: config.h:237
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2263
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
irept::add
irept & add(const irep_idt &name)
Definition: irep.cpp:116
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:318
cpp_typecheckt::typecheck_enum_body
void typecheck_enum_body(symbolt &symbol)
Definition: cpp_typecheck_enum_type.cpp:22
cpp_typecheck_resolvet::resolve_scope
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
Definition: cpp_typecheck_resolve.cpp:856
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
cpp_enum_typet::has_tag
bool has_tag() const
Definition: cpp_enum_type.h:29
symbolt
Symbol table entry.
Definition: symbol.h:27
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
cpp_enum_typet::tag
const cpp_namet & tag() const
Definition: cpp_enum_type.h:24
symbolt::is_type
bool is_type
Definition: symbol.h:61
cpp_idt::id_class
id_classt id_class
Definition: cpp_id.h:45
cpp_typecheckt::implicit_typecast
void implicit_typecast(exprt &expr, const typet &type) override
Definition: cpp_typecheck_conversions.cpp:1493
irept::get_sub
subt & get_sub()
Definition: irep.h:456
config.h
cpp_idt::prefix
std::string prefix
Definition: cpp_id.h:79
cpp_typecheckt::typecheck_enum_type
void typecheck_enum_type(typet &type)
Definition: cpp_typecheck_enum_type.cpp:87
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
c_enum_typet::underlying_type
const typet & underlying_type() const
Definition: c_types.h:274
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
cpp_namet
Definition: cpp_name.h:16
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2992