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(ID_C),
39  break_is_allowed(false),
40  continue_is_allowed(false),
41  case_is_allowed(false)
42  {
43  }
44 
46  symbol_tablet &_symbol_table1,
47  const symbol_tablet &_symbol_table2,
48  const std::string &_module,
49  message_handlert &_message_handler):
50  typecheckt(_message_handler),
51  namespacet(_symbol_table1, _symbol_table2),
52  symbol_table(_symbol_table1),
53  module(_module),
54  mode(ID_C),
55  break_is_allowed(false),
56  continue_is_allowed(false),
57  case_is_allowed(false)
58  {
59  }
60 
61  virtual ~c_typecheck_baset() { }
62 
63  virtual void typecheck()=0;
64  virtual void typecheck_expr(exprt &expr);
65 
66 protected:
69  const irep_idt mode;
71 
72  typedef std::unordered_map<irep_idt, typet> id_type_mapt;
74 
75  // overload to use language specific syntax
76  virtual std::string to_string(const exprt &expr);
77  virtual std::string to_string(const typet &type);
78 
79  //
80  // service functions
81  //
82 
83  virtual void do_initializer(
84  exprt &initializer,
85  const typet &type,
86  bool force_constant);
87 
88  virtual exprt do_initializer_rec(
89  const exprt &value,
90  const typet &type,
91  bool force_constant);
92 
93  virtual exprt do_initializer_list(
94  const exprt &value,
95  const typet &type,
96  bool force_constant);
97 
98  virtual exprt::operandst::const_iterator do_designated_initializer(
99  exprt &result,
100  designatort &designator,
101  const exprt &initializer_list,
102  exprt::operandst::const_iterator init_it,
103  bool force_constant);
104 
105  designatort make_designator(const typet &type, const exprt &src);
106  void designator_enter(const typet &type, designatort &designator); // go down
107  void increment_designator(designatort &designator);
108 
109  // typecasts
110 
112 
113  virtual void implicit_typecast(exprt &expr, const typet &type);
114  virtual void implicit_typecast_arithmetic(exprt &expr);
115  virtual void implicit_typecast_arithmetic(exprt &expr1, exprt &expr2);
116 
117  virtual void implicit_typecast_bool(exprt &expr)
118  {
119  implicit_typecast(expr, bool_typet());
120  }
121 
122  // code
123  virtual void start_typecheck_code();
124  virtual void typecheck_code(codet &code);
125 
126  virtual void typecheck_assign(codet &expr);
127  virtual void typecheck_asm(codet &code);
128  virtual void typecheck_block(codet &code);
129  virtual void typecheck_break(codet &code);
130  virtual void typecheck_continue(codet &code);
131  virtual void typecheck_decl(codet &code);
132  virtual void typecheck_expression(codet &code);
133  virtual void typecheck_for(codet &code);
134  virtual void typecheck_goto(code_gotot &code);
135  virtual void typecheck_ifthenelse(code_ifthenelset &code);
136  virtual void typecheck_label(code_labelt &code);
137  virtual void typecheck_switch_case(code_switch_caset &code);
138  virtual void typecheck_gcc_computed_goto(codet &code);
139  virtual void typecheck_gcc_switch_case_range(codet &code);
140  virtual void typecheck_gcc_local_label(codet &code);
141  virtual void typecheck_return(codet &code);
142  virtual void typecheck_switch(code_switcht &code);
143  virtual void typecheck_while(code_whilet &code);
144  virtual void typecheck_dowhile(code_dowhilet &code);
145  virtual void typecheck_start_thread(codet &code);
146  virtual void typecheck_spec_expr(codet &code, const irep_idt &spec);
147 
153 
154  // to check that all labels used are also defined
155  std::map<irep_idt, source_locationt> labels_defined, labels_used;
156 
157  // expressions
158  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
159  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
160  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
161  virtual void typecheck_expr_main(exprt &expr);
162  virtual void typecheck_expr_operands(exprt &expr);
163  virtual void typecheck_expr_comma(exprt &expr);
164  virtual void typecheck_expr_constant(exprt &expr);
165  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
166  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
167  virtual void typecheck_expr_unary_boolean(exprt &expr);
168  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
169  virtual void typecheck_expr_shifts(shift_exprt &expr);
170  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
171  virtual void typecheck_arithmetic_pointer(const exprt &expr);
172  virtual void typecheck_expr_binary_boolean(exprt &expr);
173  virtual void typecheck_expr_trinary(if_exprt &expr);
174  virtual void typecheck_expr_address_of(exprt &expr);
175  virtual void typecheck_expr_dereference(exprt &expr);
176  virtual void typecheck_expr_member(exprt &expr);
177  virtual void typecheck_expr_ptrmember(exprt &expr);
178  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
180  virtual void adjust_float_rel(exprt &expr);
181  static void add_rounding_mode(exprt &);
182  virtual void typecheck_expr_index(exprt &expr);
183  virtual void typecheck_expr_typecast(exprt &expr);
184  virtual void typecheck_expr_symbol(exprt &expr);
185  virtual void typecheck_expr_sizeof(exprt &expr);
186  virtual void typecheck_expr_alignof(exprt &expr);
187  virtual void typecheck_expr_function_identifier(exprt &expr);
189  side_effect_exprt &expr);
194  side_effect_exprt &expr);
198 
199  virtual void make_index_type(exprt &expr);
200  virtual void make_constant(exprt &expr);
201  virtual void make_constant_index(exprt &expr);
202  virtual void make_constant_rec(exprt &expr);
203 
204  virtual bool gcc_types_compatible_p(const typet &, const typet &);
205 
206  // types
207  virtual void typecheck_type(typet &type);
208  virtual void typecheck_compound_type(struct_union_typet &type);
209  virtual void typecheck_compound_body(struct_union_typet &type);
210  virtual void typecheck_c_enum_type(typet &type);
211  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
212  virtual void typecheck_code_type(code_typet &type);
213  virtual void typecheck_symbol_type(typet &type);
214  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
215  virtual void typecheck_typeof_type(typet &type);
216  virtual void typecheck_array_type(array_typet &type);
217  virtual void typecheck_vector_type(vector_typet &type);
218  virtual void typecheck_custom_type(typet &type);
219  virtual void adjust_function_parameter(typet &type) const;
220  virtual bool is_complete_type(const typet &type) const;
221 
223  const mp_integer &min, const mp_integer &max) const;
224 
226  const mp_integer &min, const mp_integer &max,
227  bool is_packed) const;
228 
230  {
231  typet result(ID_already_typechecked);
232  result.subtype().swap(dest);
233  result.swap(dest);
234  }
235 
236  // this cleans expressions in array types
237  std::list<codet> clean_code;
238 
239  // environment
240  void add_argc_argv(const symbolt &main_symbol);
241 
242  // symbol table management
243  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
244  void move_symbol(symbolt &symbol)
245  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
246 
247  // top-level stuff
249  void typecheck_symbol(symbolt &symbol);
250  void typecheck_new_symbol(symbolt &symbol);
251  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
253  symbolt &old_symbol, symbolt &new_symbol);
254  void typecheck_function_body(symbolt &symbol);
255 
256  virtual void do_initializer(symbolt &symbol);
257 
258  static bool is_numeric_type(const typet &src)
259  {
260  return src.id()==ID_complex ||
261  src.id()==ID_unsignedbv ||
262  src.id()==ID_signedbv ||
263  src.id()==ID_floatbv ||
264  src.id()==ID_fixedbv ||
265  src.id()==ID_c_bool ||
266  src.id()==ID_bool ||
267  src.id()==ID_c_enum_tag ||
268  src.id()==ID_c_bit_field ||
269  src.id()==ID_integer ||
270  src.id()==ID_real;
271  }
272 
273  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
275 
276  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
277 };
278 
279 #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:22
std::map< irep_idt, source_locationt > labels_used
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:22
virtual void typecheck_start_thread(codet &code)
A ‘switch’ instruction.
Definition: std_code.h:533
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:764
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
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:3361
virtual void typecheck_switch_case(code_switch_caset &code)
A ‘goto’ instruction.
Definition: std_code.h:774
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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:1381
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)
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)
std::unordered_map< irep_idt, irep_idt > asm_label_mapt
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:1629
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:19
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:74
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:947
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’ instruction.
Definition: std_code.h:588
Author: Diffblue Ltd.
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’ with given value ‘value’
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:1352
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:162
mstreamt & result() const
Definition: message.h:312
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:42
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’ instruction.
Definition: std_code.h:643
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)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
arrays with given size
Definition: std_types.h:1004
virtual void typecheck_array_type(array_typet &type)
virtual void implicit_typecast_arithmetic(exprt &expr)
An if-then-else.
Definition: std_code.h:461
void typecheck_function_body(symbolt &symbol)
static void add_rounding_mode(exprt &)
std::unordered_map< irep_idt, typet > id_type_mapt
virtual void typecheck_type(typet &type)
A switch-case.
Definition: std_code.h:1014
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:21
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:1238
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:2765
virtual void typecheck_dowhile(code_dowhilet &code)
An enum tag type.
Definition: std_types.h:728
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)