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/symbol_table.h>
16 #include <util/typecheck.h>
17 #include <util/namespace.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
20 #include <util/std_types.h>
21 
22 #include "ansi_c_declaration.h"
23 #include "designator.h"
24 
26  public typecheckt,
27  public namespacet
28 {
29 public:
31  symbol_tablet &_symbol_table,
32  const std::string &_module,
33  message_handlert &_message_handler):
34  typecheckt(_message_handler),
35  namespacet(_symbol_table),
36  symbol_table(_symbol_table),
37  module(_module),
38  mode("C")
39  {
40  }
41 
43  symbol_tablet &_symbol_table1,
44  const symbol_tablet &_symbol_table2,
45  const std::string &_module,
46  message_handlert &_message_handler):
47  typecheckt(_message_handler),
48  namespacet(_symbol_table1, _symbol_table2),
49  symbol_table(_symbol_table1),
50  module(_module),
51  mode("C")
52  {
53  }
54 
55  virtual ~c_typecheck_baset() { }
56 
57  virtual void typecheck()=0;
58  virtual void typecheck_expr(exprt &expr);
59 
60 protected:
63  const irep_idt mode;
65 
66  typedef std::unordered_map<irep_idt, typet, irep_id_hash> id_type_mapt;
67  id_type_mapt parameter_map;
68 
69  // overload to use language specific syntax
70  virtual std::string to_string(const exprt &expr);
71  virtual std::string to_string(const typet &type);
72 
73  //
74  // service functions
75  //
76 
77  virtual void do_initializer(
78  exprt &initializer,
79  const typet &type,
80  bool force_constant);
81 
82  virtual exprt do_initializer_rec(
83  const exprt &value,
84  const typet &type,
85  bool force_constant);
86 
87  virtual exprt do_initializer_list(
88  const exprt &value,
89  const typet &type,
90  bool force_constant);
91 
92  virtual exprt::operandst::const_iterator do_designated_initializer(
93  exprt &result,
94  designatort &designator,
95  const exprt &initializer_list,
96  exprt::operandst::const_iterator init_it,
97  bool force_constant);
98 
99  designatort make_designator(const typet &type, const exprt &src);
100  void designator_enter(const typet &type, designatort &designator); // go down
101  void increment_designator(designatort &designator);
102 
103  // typecasts
104 
106 
107  virtual void implicit_typecast(exprt &expr, const typet &type);
108  virtual void implicit_typecast_arithmetic(exprt &expr);
109  virtual void implicit_typecast_arithmetic(exprt &expr1, exprt &expr2);
110 
111  virtual void implicit_typecast_bool(exprt &expr)
112  {
113  implicit_typecast(expr, bool_typet());
114  }
115 
116  // code
117  virtual void start_typecheck_code();
118  virtual void typecheck_code(codet &code);
119 
120  virtual void typecheck_assign(codet &expr);
121  virtual void typecheck_asm(codet &code);
122  virtual void typecheck_block(codet &code);
123  virtual void typecheck_break(codet &code);
124  virtual void typecheck_continue(codet &code);
125  virtual void typecheck_decl(codet &code);
126  virtual void typecheck_expression(codet &code);
127  virtual void typecheck_for(codet &code);
128  virtual void typecheck_goto(code_gotot &code);
129  virtual void typecheck_ifthenelse(code_ifthenelset &code);
130  virtual void typecheck_label(code_labelt &code);
131  virtual void typecheck_switch_case(code_switch_caset &code);
132  virtual void typecheck_gcc_computed_goto(codet &code);
133  virtual void typecheck_gcc_switch_case_range(codet &code);
134  virtual void typecheck_gcc_local_label(codet &code);
135  virtual void typecheck_return(codet &code);
136  virtual void typecheck_switch(code_switcht &code);
137  virtual void typecheck_while(code_whilet &code);
138  virtual void typecheck_dowhile(code_dowhilet &code);
139  virtual void typecheck_start_thread(codet &code);
140  virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
141 
147 
148  // to check that all labels used are also defined
149  std::map<irep_idt, source_locationt> labels_defined, labels_used;
150 
151  // expressions
152  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
153  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
154  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
155  virtual void typecheck_expr_main(exprt &expr);
156  virtual void typecheck_expr_operands(exprt &expr);
157  virtual void typecheck_expr_comma(exprt &expr);
158  virtual void typecheck_expr_constant(exprt &expr);
159  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
160  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
161  virtual void typecheck_expr_unary_boolean(exprt &expr);
162  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
163  virtual void typecheck_expr_shifts(shift_exprt &expr);
164  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
165  virtual void typecheck_arithmetic_pointer(const exprt &expr);
166  virtual void typecheck_expr_binary_boolean(exprt &expr);
167  virtual void typecheck_expr_trinary(if_exprt &expr);
168  virtual void typecheck_expr_address_of(exprt &expr);
169  virtual void typecheck_expr_dereference(exprt &expr);
170  virtual void typecheck_expr_member(exprt &expr);
171  virtual void typecheck_expr_ptrmember(exprt &expr);
172  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
174  virtual void adjust_float_rel(exprt &expr);
175  static void add_rounding_mode(exprt &);
176  virtual void typecheck_expr_index(exprt &expr);
177  virtual void typecheck_expr_typecast(exprt &expr);
178  virtual void typecheck_expr_symbol(exprt &expr);
179  virtual void typecheck_expr_sizeof(exprt &expr);
180  virtual void typecheck_expr_alignof(exprt &expr);
181  virtual void typecheck_expr_function_identifier(exprt &expr);
183  side_effect_exprt &expr);
188  side_effect_exprt &expr);
192 
193  virtual void make_index_type(exprt &expr);
194  virtual void make_constant(exprt &expr);
195  virtual void make_constant_index(exprt &expr);
196  virtual void make_constant_rec(exprt &expr);
197 
198  virtual bool gcc_types_compatible_p(const typet &, const typet &);
199 
200  // types
201  virtual void typecheck_type(typet &type);
202  virtual void typecheck_compound_type(struct_union_typet &type);
203  virtual void typecheck_compound_body(struct_union_typet &type);
204  virtual void typecheck_c_enum_type(typet &type);
205  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
206  virtual void typecheck_code_type(code_typet &type);
207  virtual void typecheck_symbol_type(typet &type);
208  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
209  virtual void typecheck_typeof_type(typet &type);
210  virtual void typecheck_array_type(array_typet &type);
211  virtual void typecheck_vector_type(vector_typet &type);
212  virtual void typecheck_custom_type(typet &type);
213  virtual void adjust_function_parameter(typet &type) const;
214  virtual bool is_complete_type(const typet &type) const;
215 
217  const mp_integer &min, const mp_integer &max) const;
218 
220  const mp_integer &min, const mp_integer &max,
221  bool is_packed) const;
222 
224  {
225  typet result(ID_already_typechecked);
226  result.subtype().swap(dest);
227  result.swap(dest);
228  }
229 
230  // this cleans expressions in array types
231  std::list<codet> clean_code;
232 
233  // environment
234  void add_argc_argv(const symbolt &main_symbol);
235 
236  // symbol table management
237  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
238  void move_symbol(symbolt &symbol)
239  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
240 
241  // top-level stuff
243  void typecheck_symbol(symbolt &symbol);
244  void typecheck_new_symbol(symbolt &symbol);
245  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
247  symbolt &old_symbol, symbolt &new_symbol);
248  void typecheck_function_body(symbolt &symbol);
249 
250  virtual void do_initializer(symbolt &symbol);
251 
252  static bool is_numeric_type(const typet &src)
253  {
254  return src.id()==ID_complex ||
255  src.id()==ID_unsignedbv ||
256  src.id()==ID_signedbv ||
257  src.id()==ID_floatbv ||
258  src.id()==ID_fixedbv ||
259  src.id()==ID_c_bool ||
260  src.id()==ID_bool ||
261  src.id()==ID_c_enum_tag ||
262  src.id()==ID_c_bit_field;
263  }
264 
265  typedef std::unordered_map<irep_idt, irep_idt, irep_id_hash> asm_label_mapt;
266  asm_label_mapt asm_label_map;
267 
268  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
269 };
270 
271 #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_typeof_type(typet &type)
The type of an expression.
Definition: type.h:20
std::map< irep_idt, source_locationt > labels_used
mstreamt & result()
Definition: message.h:233
std::unordered_map< irep_idt, typet, irep_id_hash > id_type_mapt
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
c_typecheck_baset(symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
BigInt mp_integer
Definition: mp_arith.h:19
virtual void typecheck_start_thread(codet &code)
A `switch&#39; instruction.
Definition: std_code.h:412
virtual void typecheck_spec_expr(codet &code, const irep_idt &spec)
void typecheck_declaration(ansi_c_declarationt &)
Base type of functions.
Definition: std_types.h:734
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
asm_label_mapt asm_label_map
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_while(code_whilet &code)
c_typecheck_baset(symbol_tablet &_symbol_table, const std::string &_module, message_handlert &_message_handler)
virtual void typecheck_gcc_switch_case_range(codet &code)
virtual void make_constant(exprt &expr)
virtual ~c_typecheck_baset()
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
id_type_mapt parameter_map
The trinary if-then-else operator.
Definition: std_expr.h:2771
virtual void typecheck_switch_case(code_switch_caset &code)
A `goto&#39; instruction.
Definition: std_code.h:613
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
virtual void typecheck_symbol_type(typet &type)
virtual std::string to_string(const exprt &expr)
virtual void typecheck_compound_type(struct_union_typet &type)
Type for c bit fields.
Definition: std_types.h:1294
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
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)
symbol_tablet & symbol_table
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type)
ANSI-C Language Type Checking.
virtual void typecheck_expr_symbol(exprt &expr)
static bool is_numeric_type(const typet &src)
std::unordered_map< irep_idt, irep_idt, irep_id_hash > asm_label_mapt
const irep_idt & id() const
Definition: irep.h:189
virtual void typecheck_break(codet &code)
void typecheck_new_symbol(symbolt &symbol)
void apply_asm_label(const irep_idt &asm_label, symbolt &symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
virtual void typecheck_expr_operands(exprt &expr)
virtual void typecheck_c_enum_type(typet &type)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_ifthenelse(code_ifthenelset &code)
virtual void typecheck_assign(codet &expr)
const irep_idt mode
void make_already_typechecked(typet &dest)
A constant-size array type.
Definition: std_types.h:1554
virtual void make_index_type(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
API to expression classes.
virtual void typecheck_continue(codet &code)
The symbol table.
Definition: symbol_table.h:52
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
void increment_designator(designatort &designator)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void move_symbol(symbolt &symbol)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
A label for branch targets.
Definition: std_code.h:760
virtual void typecheck_expr(exprt &expr)
typet enum_constant_type(const mp_integer &min, const mp_integer &max) const
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
A `while&#39; instruction.
Definition: std_code.h:457
Symbol table.
std::list< codet > clean_code
void typecheck_redefinition_non_type(symbolt &old_symbol, symbolt &new_symbol)
virtual void typecheck_switch(code_switcht &code)
virtual void typecheck_asm(codet &code)
void designator_enter(const typet &type, designatort &designator)
virtual void typecheck_block(codet &code)
virtual void typecheck_expr_function_identifier(exprt &expr)
typet enum_underlying_type(const mp_integer &min, const mp_integer &max, bool is_packed) const
virtual exprt do_initializer_rec(const exprt &value, const typet &type, bool force_constant)
initialize something of type `type&#39; with given value `value&#39;
virtual void typecheck_custom_type(typet &type)
virtual void adjust_function_parameter(typet &type) const
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
virtual void start_typecheck_code()
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual void typecheck_for(codet &code)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
virtual void typecheck_label(code_labelt &code)
A function call side effect.
Definition: std_code.h:1052
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_code_type(code_typet &type)
virtual void typecheck_expr_sizeof(exprt &expr)
API to type classes.
virtual void typecheck_vector_type(vector_typet &type)
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
virtual void typecheck_gcc_local_label(codet &code)
virtual void typecheck_compound_body(struct_union_typet &type)
Base class for all expressions.
Definition: expr.h:46
void add_argc_argv(const symbolt &main_symbol)
virtual void typecheck()=0
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_decl(codet &code)
A `do while&#39; instruction.
Definition: std_code.h:502
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void make_constant_index(exprt &expr)
ANSI-CC Language Type Checking.
designatort make_designator(const typet &type, const exprt &src)
std::map< irep_idt, source_locationt > labels_defined
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
const irep_idt module
void typecheck_symbol(symbolt &symbol)
void swap(irept &irep)
Definition: irep.h:231
virtual bool gcc_types_compatible_p(const typet &, const typet &)
arrays with given size
Definition: std_types.h:901
virtual void typecheck_array_type(array_typet &type)
virtual void implicit_typecast_arithmetic(exprt &expr)
An if-then-else.
Definition: std_code.h:350
void typecheck_function_body(symbolt &symbol)
static void add_rounding_mode(exprt &)
virtual void typecheck_type(typet &type)
A switch-case.
Definition: std_code.h:817
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
A statement in a programming language.
Definition: std_code.h:19
const typet & subtype() const
Definition: type.h:31
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr_constant(exprt &expr)
virtual void make_constant_rec(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
An expression containing a side effect.
Definition: std_code.h:997
virtual void typecheck_expr_main(exprt &expr)
virtual void typecheck_c_bit_field_type(c_bit_field_typet &type)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_expr_alignof(exprt &expr)
A base class for shift operators.
Definition: std_expr.h:2227
virtual void typecheck_dowhile(code_dowhilet &code)
An enum tag type.
Definition: std_types.h:698
virtual void typecheck_return(codet &code)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void typecheck_goto(code_gotot &code)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_code(codet &code)
virtual void typecheck_expression(codet &code)
virtual void adjust_float_rel(exprt &expr)