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/namespace.h>
16 #include <util/std_code.h>
17 #include <util/symbol_table.h>
18 #include <util/typecheck.h>
19 
20 #include "designator.h"
21 
23 class c_bit_field_typet;
24 class shift_exprt;
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_loop_invariant(codet &code);
148  virtual void typecheck_spec_decreases(codet &code);
149 
155 
156  // to check that all labels used are also defined
157  std::map<irep_idt, source_locationt> labels_defined, labels_used;
158 
159  // expressions
160  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
161  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
162  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
163  virtual void typecheck_expr_main(exprt &expr);
164  virtual void typecheck_expr_operands(exprt &expr);
165  virtual void typecheck_expr_comma(exprt &expr);
166  virtual void typecheck_expr_constant(exprt &expr);
167  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
168  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
169  virtual void typecheck_expr_unary_boolean(exprt &expr);
170  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
171  virtual void typecheck_expr_shifts(shift_exprt &expr);
172  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
173  virtual void typecheck_arithmetic_pointer(const exprt &expr);
174  virtual void typecheck_expr_binary_boolean(exprt &expr);
175  virtual void typecheck_expr_trinary(if_exprt &expr);
176  virtual void typecheck_expr_address_of(exprt &expr);
177  virtual void typecheck_expr_dereference(exprt &expr);
178  virtual void typecheck_expr_member(exprt &expr);
179  virtual void typecheck_expr_ptrmember(exprt &expr);
180  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
181  virtual void typecheck_expr_rel_vector(binary_exprt &expr);
182  virtual void adjust_float_rel(binary_relation_exprt &);
183  static void add_rounding_mode(exprt &);
184  virtual void typecheck_expr_index(exprt &expr);
185  virtual void typecheck_expr_typecast(exprt &expr);
186  virtual void typecheck_expr_symbol(exprt &expr);
187  virtual void typecheck_expr_sizeof(exprt &expr);
188  virtual void typecheck_expr_alignof(exprt &expr);
189  virtual void typecheck_expr_function_identifier(exprt &expr);
191  side_effect_exprt &expr);
196  side_effect_exprt &expr);
201  const irep_idt &identifier,
202  const exprt::operandst &arguments,
203  const source_locationt &source_location);
205  const irep_idt &identifier,
206  const symbol_exprt &function_symbol);
207  virtual exprt
210  const exprt &,
211  const irep_idt &,
212  const std::string &) const;
213 
214  virtual void make_index_type(exprt &expr);
215  virtual void make_constant(exprt &expr);
216  virtual void make_constant_index(exprt &expr);
217 
218  virtual bool gcc_types_compatible_p(const typet &, const typet &);
219 
220  // types
221  virtual void typecheck_type(typet &type);
222  virtual void typecheck_compound_type(struct_union_typet &type);
223  virtual void typecheck_compound_body(struct_union_typet &type);
224  virtual void typecheck_c_enum_type(typet &type);
225  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
226  virtual void typecheck_code_type(code_typet &type);
227  virtual void typecheck_typedef_type(typet &type);
228  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
229  virtual void typecheck_typeof_type(typet &type);
230  virtual void typecheck_array_type(array_typet &type);
231  virtual void typecheck_vector_type(typet &type);
232  virtual void typecheck_custom_type(typet &type);
233  virtual void adjust_function_parameter(typet &type) const;
234  virtual bool is_complete_type(const typet &type) const;
235 
237  const mp_integer &min, const mp_integer &max) const;
238 
240  const mp_integer &min,
241  const mp_integer &max,
242  bool is_packed) const;
243 
244  // this cleans expressions in array types
245  std::list<codet> clean_code;
246 
247  // symbol table management
248  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
249  void move_symbol(symbolt &symbol)
250  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
251 
252  // top-level stuff
254  void typecheck_symbol(symbolt &symbol);
255  void typecheck_new_symbol(symbolt &symbol);
256  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
258  symbolt &old_symbol, symbolt &new_symbol);
259  void typecheck_function_body(symbolt &symbol);
260 
261  virtual void do_initializer(symbolt &symbol);
262 
263  static bool is_numeric_type(const typet &src)
264  {
265  return src.id()==ID_complex ||
266  src.id()==ID_unsignedbv ||
267  src.id()==ID_signedbv ||
268  src.id()==ID_floatbv ||
269  src.id()==ID_fixedbv ||
270  src.id()==ID_c_bool ||
271  src.id()==ID_bool ||
272  src.id()==ID_c_enum_tag ||
273  src.id()==ID_c_bit_field ||
274  src.id()==ID_integer ||
275  src.id()==ID_real;
276  }
277 
278  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
280 
281  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
282 };
283 
285 {
286 public:
288  : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
289  {
290  }
291 
292  static void make_already_typechecked(exprt &expr)
293  {
295  expr.swap(a);
296  }
297 
299  {
300  return op0();
301  }
302 };
303 
305 {
306 public:
308  : type_with_subtypet(ID_already_typechecked, std::move(type))
309  {
310  }
311 
312  static void make_already_typechecked(typet &type)
313  {
315  type.swap(a);
316  }
317 
319  {
320  return subtype();
321  }
322 };
323 
325 {
326  PRECONDITION(expr.id() == ID_already_typechecked);
327  PRECONDITION(expr.operands().size() == 1);
328 
329  return static_cast<already_typechecked_exprt &>(expr);
330 }
331 
333 {
334  PRECONDITION(type.id() == ID_already_typechecked);
335  PRECONDITION(type.has_subtype());
336 
337  return static_cast<already_typechecked_typet &>(type);
338 }
339 
340 #endif // CPROVER_ANSI_C_C_TYPECHECK_BASE_H
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:763
A base class for binary expressions.
Definition: std_expr.h:550
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Base class of fixed-width bit-vector types.
Definition: std_types.h:832
The Boolean type.
Definition: std_types.h:36
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition: c_types.h:19
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:292
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_rel_vector(binary_exprt &expr)
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)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
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 typecheck_spec_decreases(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)
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_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)
virtual void typecheck_spec_loop_invariant(codet &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 exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
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_expr_builtin_offsetof(exprt &expr)
codet representation of an inline assembler statement.
Definition: std_code.h:1699
A codet representing sequential composition of program statements.
Definition: std_code.h:168
codet representation of a do while statement.
Definition: std_code.h:988
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1543
codet representation of a goto statement.
Definition: std_code.h:1157
codet representation of an if-then-else statement.
Definition: std_code.h:776
codet representation of a label for branch targets.
Definition: std_code.h:1405
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1469
Base type of functions.
Definition: std_types.h:539
codet representing a while statement.
Definition: std_code.h:926
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33
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:343
exprt & op0()
Definition: expr.h:99
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
operandst & operands()
Definition: expr.h:92
The trinary if-then-else operator.
Definition: std_expr.h:2172
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
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:91
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
An expression containing a side effect.
Definition: std_code.h:1896
Base type for structs and unions.
Definition: std_types.h:62
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
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:975
ANSI-C Language Type Checking.
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Author: Diffblue Ltd.