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(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.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 = 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.subtype().is_nil())
155  type.subtype()=signed_int_type();
156  else
157  {
158  typecheck_type(type.subtype());
159  if(
160  type.subtype().id() != ID_signedbv &&
161  type.subtype().id() != ID_unsignedbv &&
162  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:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
c_enum_typet
The type of C enums.
Definition: std_types.h:620
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:82
cpp_scopet
Definition: cpp_scope.h:21
to_cpp_enum_type
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:64
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:129
cpp_typecheckt::cpp_scopes
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:109
irept::make_nil
void make_nil()
Definition: irep.h:475
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
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
configt::ansi_ct::flavourt::VISUAL_STUDIO
@ VISUAL_STUDIO
cpp_typecheck_resolvet
Definition: cpp_typecheck_resolve.h:21
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
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:19
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:22
Forall_irep
#define Forall_irep(it, irep)
Definition: irep.h:66
cpp_idt
Definition: cpp_id.h:29
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:3552
cpp_idt::is_scope
bool is_scope
Definition: cpp_id.h:49
cpp_enum_typet::get_tag_only_declaration
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:56
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
c_typecheck_baset::module
const irep_idt module
Definition: c_typecheck_base.h:68
cpp_enum_typet::generate_anon_tag
irep_idt generate_anon_tag() const
Definition: cpp_enum_type.cpp:20
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:30
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
typet::source_location
const source_locationt & source_location() const
Definition: type.h:71
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:231
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:67
irept::swap
void swap(irept &irep)
Definition: irep.h:463
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
cpp_typecheck.h
C++ Language Type Checking.
cpp_enum_typet
Definition: cpp_enum_type.h:22
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
cpp_template_args_non_tct
Definition: cpp_template_args.h:45
symbol_tablet::move
virtual bool move(symbolt &symbol, symbolt *&new_symbol) override
Move a symbol into the symbol table.
Definition: symbol_table.cpp:69
config
configt config
Definition: config.cpp:24
cpp_enum_type.h
C++ Language Type Checking.
source_locationt
Definition: source_location.h:20
cpp_enum_typet::has_body
bool has_body() const
Definition: cpp_enum_type.h:51
configt::ansi_ct::mode
flavourt mode
Definition: config.h:116
cpp_typecheckt::typecheck_expr
void typecheck_expr(exprt &) override
Definition: cpp_typecheck_expr.cpp:2251
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:696
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:854
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:31
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:26
symbolt::is_type
bool is_type
Definition: symbol.h:61
cpp_idt::id_class
id_classt id_class
Definition: cpp_id.h:51
cpp_typecheckt::implicit_typecast
void implicit_typecast(exprt &expr, const typet &type) override
Definition: cpp_typecheck_conversions.cpp:1480
irept::get_sub
subt & get_sub()
Definition: irep.h:477
config.h
cpp_idt::prefix
std::string prefix
Definition: cpp_id.h:85
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
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
cpp_namet
Definition: cpp_name.h:17
c_types.h
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939