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_frontend_returnt &);
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 
148  // contracts
149  virtual void typecheck_spec_assigns(exprt::operandst &targets);
150  virtual void typecheck_spec_assigns_condition(exprt &condition);
151  virtual void typecheck_spec_assigns_target(exprt &target);
152  virtual void typecheck_spec_loop_invariant(codet &code);
153  virtual void typecheck_spec_decreases(codet &code);
154 
160 
161  // to check that all labels used are also defined
162  std::map<irep_idt, source_locationt> labels_defined, labels_used;
163 
164  // expressions
165  virtual void typecheck_expr_builtin_va_arg(exprt &expr);
166  virtual void typecheck_expr_builtin_offsetof(exprt &expr);
167  virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
168  virtual void typecheck_expr_main(exprt &expr);
169  virtual void typecheck_expr_operands(exprt &expr);
170  virtual void typecheck_expr_comma(exprt &expr);
171  virtual void typecheck_expr_constant(exprt &expr);
172  virtual void typecheck_expr_side_effect(side_effect_exprt &expr);
173  virtual void typecheck_expr_unary_arithmetic(exprt &expr);
174  virtual void typecheck_expr_unary_boolean(exprt &expr);
175  virtual void typecheck_expr_binary_arithmetic(exprt &expr);
176  virtual void typecheck_expr_shifts(shift_exprt &expr);
177  virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
178  virtual void typecheck_arithmetic_pointer(const exprt &expr);
179  virtual void typecheck_expr_binary_boolean(exprt &expr);
180  virtual void typecheck_expr_trinary(if_exprt &expr);
181  virtual void typecheck_expr_address_of(exprt &expr);
182  virtual void typecheck_expr_dereference(exprt &expr);
183  virtual void typecheck_expr_member(exprt &expr);
184  virtual void typecheck_expr_ptrmember(exprt &expr);
185  virtual void typecheck_expr_rel(binary_relation_exprt &expr);
186  virtual void typecheck_expr_rel_vector(binary_exprt &expr);
187  virtual void adjust_float_rel(binary_relation_exprt &);
188  static void add_rounding_mode(exprt &);
189  virtual void typecheck_expr_index(exprt &expr);
190  virtual void typecheck_expr_typecast(exprt &expr);
191  virtual void typecheck_expr_symbol(exprt &expr);
192  virtual void typecheck_expr_sizeof(exprt &expr);
193  virtual void typecheck_expr_alignof(exprt &expr);
194  virtual void typecheck_expr_function_identifier(exprt &expr);
196  side_effect_exprt &expr);
201  side_effect_exprt &expr);
207  const irep_idt &arith_op);
209  const irep_idt &identifier,
210  const exprt::operandst &arguments,
211  const source_locationt &source_location);
213  const irep_idt &identifier,
214  const symbol_exprt &function_symbol);
215  virtual exprt
218  const exprt &,
219  const irep_idt &,
220  const std::string &) const;
221 
222  virtual void make_index_type(exprt &expr);
223  virtual void make_constant(exprt &expr);
224  virtual void make_constant_index(exprt &expr);
225 
226  virtual bool gcc_types_compatible_p(const typet &, const typet &);
227 
228  // types
229  virtual void typecheck_type(typet &type);
230  virtual void typecheck_compound_type(struct_union_typet &type);
231  virtual void typecheck_compound_body(struct_union_typet &type);
232  virtual void typecheck_c_enum_type(typet &type);
233  virtual void typecheck_c_enum_tag_type(c_enum_tag_typet &type);
234  virtual void typecheck_code_type(code_typet &type);
235  virtual void typecheck_typedef_type(typet &type);
236  virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
237  virtual void typecheck_typeof_type(typet &type);
238  virtual void typecheck_array_type(array_typet &type);
239  virtual void typecheck_vector_type(typet &type);
240  virtual void typecheck_custom_type(typet &type);
241  virtual void adjust_function_parameter(typet &type) const;
242  virtual bool is_complete_type(const typet &type) const;
243 
245  const mp_integer &min, const mp_integer &max) const;
246 
248  const mp_integer &min,
249  const mp_integer &max,
250  bool is_packed) const;
251 
252  // this cleans expressions in array types
253  std::list<codet> clean_code;
254 
255  // symbol table management
256  void move_symbol(symbolt &symbol, symbolt *&new_symbol);
257  void move_symbol(symbolt &symbol)
258  { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
259 
260  // top-level stuff
262  void typecheck_symbol(symbolt &symbol);
263  void typecheck_new_symbol(symbolt &symbol);
264  void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
266  symbolt &old_symbol, symbolt &new_symbol);
267  void typecheck_function_body(symbolt &symbol);
268 
269  virtual void do_initializer(symbolt &symbol);
270 
271  static bool is_numeric_type(const typet &src)
272  {
273  return src.id()==ID_complex ||
274  src.id()==ID_unsignedbv ||
275  src.id()==ID_signedbv ||
276  src.id()==ID_floatbv ||
277  src.id()==ID_fixedbv ||
278  src.id()==ID_c_bool ||
279  src.id()==ID_bool ||
280  src.id()==ID_c_enum_tag ||
281  src.id()==ID_c_bit_field ||
282  src.id()==ID_integer ||
283  src.id()==ID_real;
284  }
285 
286  typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
288 
289  void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
290 };
291 
293 {
294 public:
296  : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
297  {
298  }
299 
300  static void make_already_typechecked(exprt &expr)
301  {
303  expr.swap(a);
304  }
305 
307  {
308  return op0();
309  }
310 };
311 
313 {
314 public:
316  : type_with_subtypet(ID_already_typechecked, std::move(type))
317  {
318  }
319 
320  static void make_already_typechecked(typet &type)
321  {
323  type.swap(a);
324  }
325 
327  {
328  return subtype();
329  }
330 };
331 
333 {
334  PRECONDITION(expr.id() == ID_already_typechecked);
335  PRECONDITION(expr.operands().size() == 1);
336 
337  return static_cast<already_typechecked_exprt &>(expr);
338 }
339 
341 {
342  PRECONDITION(type.id() == ID_already_typechecked);
343  PRECONDITION(type.has_subtype());
344 
345  return static_cast<already_typechecked_typet &>(type);
346 }
347 
348 #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:853
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:20
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
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()=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_spec_assigns_condition(exprt &condition)
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_spec_assigns_target(exprt &target)
exprt typecheck_builtin_overflow(side_effect_expr_function_callt &expr, const irep_idt &arith_op)
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_return(code_frontend_returnt &)
virtual void typecheck_spec_assigns(exprt::operandst &targets)
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:1253
A codet representing sequential composition of program statements.
Definition: std_code.h:130
codet representation of a do while statement.
Definition: std_code.h:672
codet representation of a "return from a function" statement.
Definition: std_code.h:893
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1097
codet representation of a goto statement.
Definition: std_code.h:841
codet representation of an if-then-else statement.
Definition: std_code.h:460
codet representation of a label for branch targets.
Definition: std_code.h:959
codet representation of a switch-case, i.e. a case statement within a switch.
Definition: std_code.h:1023
Base type of functions.
Definition: std_types.h:539
codet representing a while statement.
Definition: std_code.h:610
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
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:2226
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
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:1692
An expression containing a side effect.
Definition: std_code.h:1450
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:149
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
bool has_subtype() const
Definition: type.h:66
The vector type.
Definition: std_types.h:996
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.