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 <util/arith_tools.h>
13 #include <util/c_types.h>
14 #include <util/config.h>
15 #include <util/symbol_table_base.h>
16 
17 #include <ansi-c/c_qualifiers.h>
18 
19 #include "cpp_enum_type.h"
20 #include "cpp_typecheck.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  id2string(enum_symbol.name) + "::" + id2string(name),
56  enum_tag_type,
57  enum_symbol.mode};
58  symbol.base_name=name;
59  symbol.value=value_expr;
60  symbol.location = static_cast<const source_locationt &>(
61  component.find(ID_C_source_location));
62  symbol.module=module;
63  symbol.is_macro=true;
64  symbol.is_file_local = true;
65  symbol.is_thread_local = true;
66 
67  symbolt *new_symbol;
68  if(symbol_table.move(symbol, new_symbol))
69  {
70  error().source_location=symbol.location;
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_table_baset::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() << "enum symbol '" << base_name << "' declared previously\n"
137  << "location of previous definition: " << symbol.location << eom;
138  throw 0;
139  }
140  }
141  else if(
142  has_body ||
144  {
145  std::string pretty_name=
147 
148  // C++11 enumerations have an underlying type,
149  // which defaults to int.
150  // enums without underlying type may be 'packed'.
151  if(type.add_subtype().is_nil())
152  type.add_subtype() = signed_int_type();
153  else
154  {
155  typecheck_type(to_type_with_subtype(type).subtype());
156  if(
157  to_type_with_subtype(type).subtype().id() != ID_signedbv &&
158  to_type_with_subtype(type).subtype().id() != ID_unsignedbv &&
159  to_type_with_subtype(type).subtype().id() != ID_c_bool)
160  {
162  error() << "underlying type must be integral" << eom;
163  throw 0;
164  }
165  }
166 
167  type_symbolt symbol{symbol_name, type, ID_cpp};
168  symbol.base_name=base_name;
169  symbol.value.make_nil();
170  symbol.location=type.source_location();
171  symbol.module=module;
172  symbol.pretty_name=pretty_name;
173 
174  // move early, must be visible before doing body
175  symbolt *new_symbol;
176  if(symbol_table.move(symbol, new_symbol))
177  {
178  error().source_location=symbol.location;
179  error() << "cpp_typecheckt::typecheck_enum_type: "
180  << "symbol_table.move() failed" << eom;
181  throw 0;
182  }
183 
184  // put into scope
185  cpp_idt &scope_identifier=
186  cpp_scopes.put_into_scope(*new_symbol, dest_scope);
187 
188  scope_identifier.id_class=cpp_idt::id_classt::CLASS;
189  scope_identifier.is_scope = true;
190 
191  cpp_save_scopet save_scope_before_enum_typecheck(cpp_scopes);
192 
193  if(new_symbol->type.get_bool(ID_C_class))
194  cpp_scopes.go_to(scope_identifier);
195 
196  if(has_body)
197  typecheck_enum_body(*new_symbol);
198  }
199  else
200  {
202  error() << "use of enum '" << base_name << "' without previous declaration"
203  << eom;
204  throw 0;
205  }
206 
207  // create enum tag expression, and add the qualifiers
208  type=c_enum_tag_typet(symbol_name);
209  qualifiers.write(type);
210 }
configt config
Definition: config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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
signedbv_typet signed_int_type()
Definition: c_types.cpp:22
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:335
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:352
The type of C enums.
Definition: c_types.h:239
const typet & underlying_type() const
Definition: c_types.h:307
virtual void write(typet &src) const
virtual void read(const typet &src)
symbol_table_baset & symbol_table
virtual void make_constant(exprt &expr)
const irep_idt module
struct configt::ansi_ct ansi_c
bool has_body() const
Definition: cpp_enum_type.h:49
const cpp_namet & tag() const
Definition: cpp_enum_type.h:24
bool has_tag() const
Definition: cpp_enum_type.h:29
irep_idt generate_anon_tag() const
bool get_tag_only_declaration() const
Definition: cpp_enum_type.h:54
Definition: cpp_id.h:23
std::string prefix
Definition: cpp_id.h:79
bool is_scope
Definition: cpp_id.h:43
id_classt id_class
Definition: cpp_id.h:45
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:103
cpp_scopet & current_scope()
Definition: cpp_scopes.h:32
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:24
cpp_scopet & resolve_scope(const cpp_namet &cpp_name, irep_idt &base_name, cpp_template_args_non_tct &template_args)
void typecheck_type(typet &) override
void typecheck_enum_type(typet &type)
void implicit_typecast(exprt &expr, const typet &type) override
cpp_scopet & tag_scope(const irep_idt &_base_name, bool has_body, bool tag_only_declaration)
void typecheck_expr(exprt &) override
void typecheck_enum_body(symbolt &symbol)
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
subt & get_sub()
Definition: irep.h:448
void make_nil()
Definition: irep.h:446
irept & add(const irep_idt &name)
Definition: irep.cpp:103
bool is_nil() const
Definition: irep.h:368
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
static eomt eom
Definition: message.h:289
virtual bool move(symbolt &symbol, symbolt *&new_symbol)=0
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt mode
Language mode.
Definition: symbol.h:49
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
Definition: symbol.h:139
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
typet & add_subtype()
Definition: type.h:53
C++ Language Type Checking.
const cpp_enum_typet & to_cpp_enum_type(const irept &irep)
Definition: cpp_enum_type.h:62
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
BigInt mp_integer
Definition: smt_terms.h:17
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:97
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3055
flavourt mode
Definition: config.h:256
Author: Diffblue Ltd.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208