cprover
Loading...
Searching...
No Matches
c_typecheck_base.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: 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
24class shift_exprt;
25
27 public typecheckt,
28 public namespacet
29{
30public:
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),
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),
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
67protected:
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
90 const exprt &value,
91 const typet &type,
92 bool force_constant);
93
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 {
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);
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);
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);
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);
232 virtual void typecheck_c_enum_type(typet &type);
234 virtual void typecheck_code_type(code_typet &type);
235 virtual void typecheck_typedef_type(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{
294public:
296 : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
297 {
298 }
299
301 {
303 expr.swap(a);
304 }
305
307 {
308 return op0();
309 }
310};
311
313{
314public:
316 : type_with_subtypet(ID_already_typechecked, std::move(type))
317 {
318 }
319
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);
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)
bitvector_typet enum_constant_type()
Definition c_types.cpp:35
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)
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.
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
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
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.
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.
STL namespace.
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.