cprover
c_typecheck_base.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANSI_C_C_TYPECHECK_BASE_H
13 #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
14 
15 #include <util/bitvector_expr.h>
16 #include <util/namespace.h>
17 #include <util/std_code.h>
18 #include <util/std_expr.h>
19 #include <util/std_types.h>
20 #include <util/symbol_table.h>
21 #include <util/typecheck.h>
22 
23 #include "ansi_c_declaration.h"
24 #include "designator.h"
25 
27  public typecheckt,
28  public namespacet
29 {
30 public:
32  symbol_tablet &_symbol_table,
33  const std::string &_module,
34  message_handlert &_message_handler):
35  typecheckt(_message_handler),
36  namespacet(_symbol_table),
37  symbol_table(_symbol_table),
38  module(_module),
39  mode(ID_C),
40  break_is_allowed(false),
41  continue_is_allowed(false),
42  case_is_allowed(false)
43  {
44  }
45 
47  symbol_tablet &_symbol_table1,
48  const symbol_tablet &_symbol_table2,
49  const std::string &_module,
50  message_handlert &_message_handler):
51  typecheckt(_message_handler),
52  namespacet(_symbol_table1, _symbol_table2),
53  symbol_table(_symbol_table1),
54  module(_module),
55  mode(ID_C),
56  break_is_allowed(false),
57  continue_is_allowed(false),
58  case_is_allowed(false)
59  {
60  }
61 
62  virtual ~c_typecheck_baset() { }
63 
64  virtual void typecheck()=0;
65  virtual void typecheck_expr(exprt &expr);
66 
67 protected:
70  const irep_idt mode;
72 
73  typedef std::unordered_map<irep_idt, typet> id_type_mapt;
75 
76  // overload to use language specific syntax
77  virtual std::string to_string(const exprt &expr);
78  virtual std::string to_string(const typet &type);
79 
80  //
81  // service functions
82  //
83 
84  virtual void do_initializer(
85  exprt &initializer,
86  const typet &type,
87  bool force_constant);
88 
89  virtual exprt do_initializer_rec(
90  const exprt &value,
91  const typet &type,
92  bool force_constant);
93 
94  virtual exprt do_initializer_list(
95  const exprt &value,
96  const typet &type,
97  bool force_constant);
98 
99  virtual exprt::operandst::const_iterator do_designated_initializer(
100  exprt &result,
101  designatort &designator,
102  const exprt &initializer_list,
103  exprt::operandst::const_iterator init_it,
104  bool force_constant);
105 
106  designatort make_designator(const typet &type, const exprt &src);
107  void designator_enter(const typet &type, designatort &designator); // go down
108  void increment_designator(designatort &designator);
109 
110  // typecasts
111 
113 
114  virtual void implicit_typecast(exprt &expr, const typet &type);
115  virtual void implicit_typecast_arithmetic(exprt &expr);
116  virtual void implicit_typecast_arithmetic(exprt &expr1, exprt &expr2);
117 
118  virtual void implicit_typecast_bool(exprt &expr)
119  {
120  implicit_typecast(expr, bool_typet());
121  }
122 
123  // code
124  virtual void start_typecheck_code();
125  virtual void typecheck_code(codet &code);
126 
127  virtual void typecheck_assign(codet &expr);
128  virtual void typecheck_asm(code_asmt &code);
129  virtual void typecheck_block(code_blockt &code);
130  virtual void typecheck_break(codet &code);
131  virtual void typecheck_continue(codet &code);
132  virtual void typecheck_decl(codet &code);
133  virtual void typecheck_expression(codet &code);
134  virtual void typecheck_for(codet &code);
135  virtual void typecheck_goto(code_gotot &code);
136  virtual void typecheck_ifthenelse(code_ifthenelset &code);
137  virtual void typecheck_label(code_labelt &code);
138  virtual void typecheck_switch_case(code_switch_caset &code);
139  virtual void typecheck_gcc_computed_goto(codet &code);
141  virtual void typecheck_gcc_local_label(codet &code);
142  virtual void typecheck_return(code_returnt &code);
143  virtual void typecheck_switch(codet &code);
144  virtual void typecheck_while(code_whilet &code);
145  virtual void typecheck_dowhile(code_dowhilet &code);
146  virtual void typecheck_start_thread(codet &code);
147  virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
148  virtual void
149  typecheck_assigns(const code_typet &function_declarator, const irept &spec);
150  virtual void
151  typecheck_assigns(const ansi_c_declaratort &declarator, const exprt &assigns);
152  virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec);
153 
159 
160  // to check that all labels used are also defined
161  std::map<irep_idt, source_locationt> labels_defined, labels_used;
162 
163  // expressions
164  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
165  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
166  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
167  virtual void typecheck_expr_main(exprt &expr);
168  virtual void typecheck_expr_operands(exprt &expr);
169  virtual void typecheck_expr_comma(exprt &expr);
170  virtual void typecheck_expr_constant(exprt &expr);
171  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
172  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
173  virtual void typecheck_expr_unary_boolean(exprt &expr);
174  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
175  virtual void typecheck_expr_shifts(shift_exprt &expr);
176  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
177  virtual void typecheck_arithmetic_pointer(const exprt &expr);
178  virtual void typecheck_expr_binary_boolean(exprt &expr);
179  virtual void typecheck_expr_trinary(if_exprt &expr);
180  virtual void typecheck_expr_address_of(exprt &expr);
181  virtual void typecheck_expr_dereference(exprt &expr);
182  virtual void typecheck_expr_member(exprt &expr);
183  virtual void typecheck_expr_ptrmember(exprt &expr);
184  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
186  virtual void adjust_float_rel(binary_relation_exprt &);
187  static void add_rounding_mode(exprt &);
188  virtual void typecheck_expr_index(exprt &expr);
189  virtual void typecheck_expr_typecast(exprt &expr);
190  virtual void typecheck_expr_symbol(exprt &expr);
191  virtual void typecheck_expr_sizeof(exprt &expr);
192  virtual void typecheck_expr_alignof(exprt &expr);
193  virtual void typecheck_expr_function_identifier(exprt &expr);
195  side_effect_exprt &expr);
200  side_effect_exprt &expr);
205  const irep_idt &identifier,
206  const exprt::operandst &arguments,
207  const source_locationt &source_location);
209  const irep_idt &identifier,
210  const symbol_exprt &function_symbol);
211 
212  virtual void make_index_type(exprt &expr);
213  virtual void make_constant(exprt &expr);
214  virtual void make_constant_index(exprt &expr);
215 
216  virtual bool gcc_types_compatible_p(const typet &, const typet &);
217 
218  // types
219  virtual void typecheck_type(typet &type);
220  virtual void typecheck_compound_type(struct_union_typet &type);
221  virtual void typecheck_compound_body(struct_union_typet &type);
222  virtual void typecheck_c_enum_type(typet &type);
223  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
224  virtual void typecheck_code_type(code_typet &type);
225  virtual void typecheck_typedef_type(typet &type);
226  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
227  virtual void typecheck_typeof_type(typet &type);
228  virtual void typecheck_array_type(array_typet &type);
229  virtual void typecheck_vector_type(typet &type);
230  virtual void typecheck_custom_type(typet &type);
231  virtual void adjust_function_parameter(typet &type) const;
232  virtual bool is_complete_type(const typet &type) const;
233 
235  const mp_integer &min, const mp_integer &max) const;
236 
238  const mp_integer &min,
239  const mp_integer &max,
240  bool is_packed) const;
241 
242  // this cleans expressions in array types
243  std::list<codet> clean_code;
244 
245  // symbol table management
246  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
247  void move_symbol(symbolt &symbol)
248  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
249 
250  // top-level stuff
252  void typecheck_symbol(symbolt &symbol);
253  void typecheck_new_symbol(symbolt &symbol);
254  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
256  symbolt &old_symbol, symbolt &new_symbol);
257  void typecheck_function_body(symbolt &symbol);
258 
259  virtual void do_initializer(symbolt &symbol);
260 
261  static bool is_numeric_type(const typet &src)
262  {
263  return src.id()==ID_complex ||
264  src.id()==ID_unsignedbv ||
265  src.id()==ID_signedbv ||
266  src.id()==ID_floatbv ||
267  src.id()==ID_fixedbv ||
268  src.id()==ID_c_bool ||
269  src.id()==ID_bool ||
270  src.id()==ID_c_enum_tag ||
271  src.id()==ID_c_bit_field ||
272  src.id()==ID_integer ||
273  src.id()==ID_real;
274  }
275 
276  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
278 
279  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
280 };
281 
283 {
284 public:
286  : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
287  {
288  }
289 
290  static void make_already_typechecked(exprt &expr)
291  {
293  expr.swap(a);
294  }
295 
297  {
298  return op0();
299  }
300 };
301 
303 {
304 public:
306  : type_with_subtypet(ID_already_typechecked, std::move(type))
307  {
308  }
309 
310  static void make_already_typechecked(typet &type)
311  {
313  type.swap(a);
314  }
315 
317  {
318  return subtype();
319  }
320 };
321 
323 {
324  PRECONDITION(expr.id() == ID_already_typechecked);
325  PRECONDITION(expr.operands().size() == 1);
326 
327  return static_cast<already_typechecked_exprt &>(expr);
328 }
329 
331 {
332  PRECONDITION(type.id() == ID_already_typechecked);
333  PRECONDITION(type.has_subtype());
334 
335  return static_cast<already_typechecked_typet &>(type);
336 }
337 
338 #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H
ANSI-CC Language Type Checking.
API to expression classes for bitvectors.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
already_typechecked_typet & to_already_typechecked_type(typet &type)
static void make_already_typechecked(exprt &expr)
static void make_already_typechecked(typet &type)
Arrays with given size.
Definition: std_types.h:968
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
Base class of fixed-width bit-vector types.
Definition: std_types.h:1037
The Boolean type.
Definition: std_types.h:37
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: std_types.h:1450
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:704
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
virtual void typecheck_expr_main(exprt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_break(codet &code)
void move_symbol(symbolt &symbol)
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type ‘type’ with given value ‘value’
virtual void typecheck_compound_body(struct_union_typet &type)
virtual void typecheck_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
void typecheck_function_body(symbolt &symbol)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void make_index_type(exprt &expr)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr_constant(exprt &expr)
virtual void typecheck_code_type(code_typet &type)
virtual void typecheck_expr(exprt &expr)
virtual void typecheck_return(code_returnt &code)
virtual void typecheck()=0
virtual void typecheck_block(code_blockt &code)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
c_typecheck_baset(symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler)
virtual void typecheck_while(code_whilet &code)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
std::unordered_map< irep_idt, irep_idt > asm_label_mapt
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_vector_type(typet &type)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
const irep_idt mode
virtual void typecheck_c_enum_type(typet &type)
virtual void typecheck_decl(codet &code)
virtual void make_constant(exprt &expr)
virtual void typecheck_assign(codet &expr)
virtual void typecheck_expr_comma(exprt &expr)
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
virtual void typecheck_continue(codet &code)
symbol_tablet & symbol_table
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
void typecheck_new_symbol(symbolt &symbol)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
asm_label_mapt asm_label_map
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
virtual void adjust_function_parameter(typet &type) const
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_gcc_local_label(codet &code)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_gcc_computed_goto(codet &code)
const irep_idt module
virtual void typecheck_expr_operands(exprt &expr)
std::unordered_map< irep_idt, typet > id_type_mapt
virtual void typecheck_for(codet &code)
virtual void typecheck_switch(codet &code)
void increment_designator(designatort &designator)
virtual exprt::operandst::const_iterator do_designated_initializer(exprt &result, designatort &designator, const exprt &initializer_list, exprt::operandst::const_iterator init_it, bool force_constant)
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual ~c_typecheck_baset()
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
virtual void typecheck_custom_type(typet &type)
virtual void make_constant_index(exprt &expr)
bitvector_typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
virtual void typecheck_expression(codet &code)
virtual void typecheck_compound_type(struct_union_typet &type)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
virtual bool is_complete_type(const typet &type) const
virtual void typecheck_start_thread(codet &code)
virtual void typecheck_switch_case(code_switch_caset &code)
designatort make_designator(const typet &type, const exprt &src)
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_gcc_switch_case_range(code_gcc_switch_case_ranget &)
virtual void typecheck_typedef_type(typet &type)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
c_typecheck_baset(symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
virtual void typecheck_dowhile(code_dowhilet &code)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_array_type(array_typet &type)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
void designator_enter(const typet &type, designatort &designator)
virtual void typecheck_typeof_type(typet &type)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_typecast(exprt &expr)
void typecheck_symbol(symbolt &symbol)
virtual void typecheck_label(code_labelt &code)
std::map< irep_idt, source_locationt > labels_defined
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void typecheck_assigns(const code_typet &function_declarator, const irept &spec)
virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec)
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
codet representation of an inline assembler statement.
Definition: std_code.h:1701
A codet representing sequential composition of program statements.
Definition: std_code.h:170
codet representation of a do while statement.
Definition: std_code.h:990
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1545
codet representation of a goto statement.
Definition: std_code.h:1159
codet representation of an if-then-else statement.
Definition: std_code.h:778
codet representation of a label for branch targets.
Definition: std_code.h:1407
codet representation of a "return from a function" statement.
Definition: std_code.h:1342
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1471
Base type of functions.
Definition: std_types.h:744
codet representing a while statement.
Definition: std_code.h:928
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:347
exprt & op0()
Definition: expr.h:103
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
operandst & operands()
Definition: expr.h:96
The trinary if-then-else operator.
Definition: std_expr.h:2087
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:452
mstreamt & result() const
Definition: message.h:409
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2140
An expression containing a side effect.
Definition: std_code.h:1898
Base type for structs and unions.
Definition: std_types.h:57
Expression to hold a symbol (variable)
Definition: std_expr.h:81
The symbol table.
Definition: symbol_table.h:20
Symbol table entry.
Definition: symbol.h:28
Type with a single subtype.
Definition: type.h:146
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
bool has_subtype() const
Definition: type.h:65
The vector type.
Definition: std_types.h:1764
ANSI-C Language Type Checking.
BigInt mp_integer
Definition: mp_arith.h:19
nonstd::optional< T > optionalt
Definition: optional.h:35
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
API to expression classes.
Pre-defined types.
Author: Diffblue Ltd.