CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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.h>
18#include <util/typecheck.h>
19
20#include "designator.h"
21
22#include <map>
23
26class shift_exprt;
27
29 public typecheckt,
30 public namespacet
31{
32public:
47
63
64 virtual ~c_typecheck_baset() { }
65
66 virtual void typecheck()=0;
67 virtual void typecheck_expr(exprt &expr);
68 virtual void typecheck_spec_assigns(exprt::operandst &targets);
69
70protected:
72 const irep_idt module;
75
76 typedef std::unordered_map<irep_idt, typet> id_type_mapt;
78
79 // overload to use language specific syntax
80 virtual std::string to_string(const exprt &expr);
81 virtual std::string to_string(const typet &type);
82
83 //
84 // service functions
85 //
86
87 virtual void do_initializer(
88 exprt &initializer,
89 const typet &type,
90 bool force_constant);
91
93 const exprt &value,
94 const typet &type,
95 bool force_constant);
96
98 const exprt &value,
99 const typet &type,
100 bool force_constant);
101
102 virtual exprt::operandst::const_iterator do_designated_initializer(
103 exprt &result,
104 designatort &designator,
105 const exprt &initializer_list,
106 exprt::operandst::const_iterator init_it,
107 bool force_constant);
108
109 designatort make_designator(const typet &type, const exprt &src);
110 void designator_enter(const typet &type, designatort &designator); // go down
111 void increment_designator(designatort &designator);
112
113 // typecasts
114
116
117 virtual void implicit_typecast(exprt &expr, const typet &type);
118 virtual void implicit_typecast_arithmetic(exprt &expr);
120
121 virtual void implicit_typecast_bool(exprt &expr)
122 {
124 }
125
126 // code
127 virtual void start_typecheck_code();
128 virtual void typecheck_code(codet &code);
129
130 virtual void typecheck_assign(codet &expr);
131 virtual void typecheck_asm(code_asmt &code);
132 virtual void typecheck_block(code_blockt &code);
133 virtual void typecheck_break(codet &code);
134 virtual void typecheck_continue(codet &code);
135 virtual void typecheck_decl(codet &code);
136 virtual void typecheck_expression(codet &code);
137 virtual void typecheck_for(codet &code);
138 virtual void typecheck_goto(code_gotot &code);
139 virtual void typecheck_ifthenelse(code_ifthenelset &code);
140 virtual void typecheck_label(code_labelt &code);
141 virtual void typecheck_switch_case(code_switch_caset &code);
142 virtual void typecheck_gcc_computed_goto(codet &code);
144 virtual void typecheck_gcc_local_label(codet &code);
146 virtual void typecheck_switch(codet &code);
147 virtual void typecheck_while(code_whilet &code);
148 virtual void typecheck_dowhile(code_dowhilet &code);
149 virtual void typecheck_start_thread(codet &code);
150
151 // contracts
152 virtual void
155 virtual void
158 virtual void
159 check_history_expr_return_value(const exprt &expr, std::string &clause_type);
162 virtual void check_was_freed(const exprt &expr, std::string &clause_type);
163
164 virtual void typecheck_spec_frees(exprt::operandst &targets);
166 exprt::operandst &targets,
167 const std::function<void(exprt &)> typecheck_target,
168 const std::string &clause_type);
169 virtual void typecheck_spec_condition(exprt &condition);
170 virtual void typecheck_spec_assigns_target(exprt &target);
171 virtual void typecheck_spec_frees_target(exprt &target);
172 virtual void typecheck_spec_loop_invariant(codet &code);
173 virtual void typecheck_spec_decreases(codet &code);
174 virtual void throw_on_side_effects(const exprt &expr);
175
181
182 // to check that all labels used are also defined
183 std::map<irep_idt, source_locationt> labels_defined, labels_used;
184
185 // expressions
186 virtual void typecheck_expr_builtin_va_arg(exprt &expr);
187 virtual void typecheck_expr_builtin_offsetof(exprt &expr);
188 virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr);
189 virtual void typecheck_expr_main(exprt &expr);
190 virtual void typecheck_expr_operands(exprt &expr);
191 virtual void typecheck_expr_comma(exprt &expr);
192 virtual void typecheck_expr_constant(exprt &expr);
194 virtual void typecheck_expr_unary_arithmetic(exprt &expr);
195 virtual void typecheck_expr_unary_boolean(exprt &expr);
196 virtual void typecheck_expr_binary_arithmetic(exprt &expr);
197 virtual void typecheck_expr_shifts(shift_exprt &expr);
198 virtual void typecheck_expr_pointer_arithmetic(exprt &expr);
199 virtual void typecheck_arithmetic_pointer(exprt &expr);
200 virtual void typecheck_expr_binary_boolean(exprt &expr);
201 virtual void typecheck_expr_trinary(if_exprt &expr);
202 virtual void typecheck_expr_address_of(exprt &expr);
203 virtual void typecheck_expr_dereference(exprt &expr);
204 virtual void typecheck_expr_member(exprt &expr);
205 virtual void typecheck_expr_ptrmember(exprt &expr);
206 virtual void typecheck_expr_rel(binary_relation_exprt &expr);
207 virtual void typecheck_expr_rel_vector(binary_exprt &expr);
209 static void add_rounding_mode(exprt &);
210 virtual void typecheck_expr_index(exprt &expr);
211 virtual void typecheck_expr_typecast(exprt &expr);
212 virtual void typecheck_expr_symbol(exprt &expr);
213 virtual void typecheck_expr_sizeof(exprt &expr);
214 virtual void typecheck_expr_alignof(exprt &expr);
215 virtual void typecheck_expr_function_identifier(exprt &expr);
217 side_effect_exprt &expr);
222 side_effect_exprt &expr);
228 const irep_idt &arith_op);
229 exprt
231 virtual std::optional<symbol_exprt> typecheck_gcc_polymorphic_builtin(
232 const irep_idt &identifier,
233 const exprt::operandst &arguments,
234 const source_locationt &source_location);
236 const irep_idt &identifier,
238 virtual std::optional<symbol_exprt>
240 virtual exprt
243 const exprt &,
244 const irep_idt &,
245 const std::string &) const;
246
247 virtual void make_index_type(exprt &expr);
248 virtual void make_constant(exprt &expr);
249 virtual void make_constant_index(exprt &expr);
250
251 virtual bool gcc_types_compatible_p(const typet &, const typet &);
252
253 virtual bool builtin_factory(const irep_idt &);
254
255 // types
256 virtual void typecheck_type(typet &type);
259 virtual void typecheck_c_enum_type(typet &type);
261 virtual void typecheck_code_type(code_typet &type);
262 virtual void typecheck_typedef_type(typet &type);
264 virtual void typecheck_typeof_type(typet &type);
265 virtual void typecheck_array_type(array_typet &type);
266 virtual void typecheck_vector_type(typet &type);
267 virtual void typecheck_custom_type(typet &type);
268 virtual void adjust_function_parameter(typet &type) const;
269 virtual bool is_complete_type(const typet &type) const;
270
272 const mp_integer &min, const mp_integer &max) const;
273
275 const mp_integer &min,
276 const mp_integer &max,
277 bool is_packed) const;
278
279 // this cleans expressions in array types
280 std::list<codet> clean_code;
281
282 // symbol table management
283 void move_symbol(symbolt &symbol, symbolt *&new_symbol);
284 void move_symbol(symbolt &symbol)
285 { symbolt *new_symbol; move_symbol(symbol, new_symbol); }
286
287 // top-level stuff
289 void typecheck_symbol(symbolt &symbol);
290 void typecheck_new_symbol(symbolt &symbol);
291 void typecheck_redefinition_type(symbolt &old_symbol, symbolt &new_symbol);
293 symbolt &old_symbol, symbolt &new_symbol);
294 void typecheck_function_body(symbolt &symbol);
295
298
299 virtual void do_initializer(symbolt &symbol);
300
301 static bool is_numeric_type(const typet &src)
302 {
303 return src.id()==ID_complex ||
304 src.id()==ID_unsignedbv ||
305 src.id()==ID_signedbv ||
306 src.id()==ID_floatbv ||
307 src.id()==ID_fixedbv ||
308 src.id()==ID_c_bool ||
309 src.id()==ID_bool ||
310 src.id()==ID_c_enum_tag ||
311 src.id()==ID_c_bit_field ||
312 src.id()==ID_integer ||
313 src.id()==ID_real;
314 }
315
316 typedef std::unordered_map<irep_idt, irep_idt> asm_label_mapt;
318
319 void apply_asm_label(const irep_idt &asm_label, symbolt &symbol);
320};
321
323{
324public:
326 : expr_protectedt(ID_already_typechecked, typet{}, {std::move(expr)})
327 {
328 }
329
331 {
333 expr.swap(a);
334 }
335
337 {
338 return op0();
339 }
340};
341
343{
344public:
347 {
348 }
349
351 {
353 type.swap(a);
354 }
355
357 {
358 return subtype();
359 }
360};
361
363{
365 PRECONDITION(expr.operands().size() == 1);
366
367 return static_cast<already_typechecked_exprt &>(expr);
368}
369
371{
374
375 return static_cast<already_typechecked_typet &>(type);
376}
377
378#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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
static void make_already_typechecked(exprt &expr)
static void make_already_typechecked(typet &type)
Arrays with given size.
Definition std_types.h:807
A base class for binary expressions.
Definition std_expr.h:638
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Base class of fixed-width bit-vector types.
Definition std_types.h:909
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:352
virtual exprt do_initializer_list(const exprt &value, const typet &type, bool force_constant)
virtual void typecheck_obeys_contract_call(side_effect_expr_function_callt &expr)
Checks an obeys_contract predicate occurrence.
virtual void typecheck_expr_main(exprt &expr)
symbol_table_baset & symbol_table
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 check_history_expr_return_value(const exprt &expr, std::string &clause_type)
Checks that no history expr or return_value exists in expr.
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)
virtual void typecheck_while(code_whilet &code)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void check_was_freed(const exprt &expr, std::string &clause_type)
Checks that no occurence of the CPROVER_PREFIX was_freed predicate is found in expr.
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 void throw_on_side_effects(const exprt &expr)
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)
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)
exprt typecheck_saturating_arithmetic(const side_effect_expr_function_callt &expr)
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)
virtual void typecheck_spec_frees_target(exprt &target)
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 std::optional< symbol_exprt > typecheck_shadow_memory_builtin(const side_effect_expr_function_callt &expr)
Typecheck the function if it is a shadow_memory builtin and return a symbol for it.
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 typecheck_spec_condition(exprt &condition)
virtual void start_typecheck_code()
virtual void typecheck_asm(code_asmt &code)
c_typecheck_baset(symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2, const std::string &_module, message_handlert &_message_handler)
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 void typecheck_gcc_computed_goto(codet &code)
virtual void typecheck_conditional_targets(exprt::operandst &targets, const std::function< void(exprt &)> typecheck_target, const std::string &clause_type)
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 add_parameters_to_symbol_table(symbolt &symbol)
Create symbols for parameter of the code-typed symbol symbol.
virtual std::optional< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
void increment_designator(designatort &designator)
virtual void typecheck_typed_target_call(side_effect_expr_function_callt &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)
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 typecheck_spec_frees(exprt::operandst &targets)
const irep_idt const irep_idt mode
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_arithmetic_pointer(exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
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)
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)
c_typecheck_baset(symbol_table_baset &_symbol_table, const std::string &_module, message_handlert &_message_handler)
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)
virtual bool builtin_factory(const irep_idt &)
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:583
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:38
Base class for all expressions.
Definition expr.h:344
exprt & op0()
Definition expr.h:133
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
operandst & operands()
Definition expr.h:94
The trinary if-then-else operator.
Definition std_expr.h:2497
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
mstreamt & result() const
Definition message.h:401
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:131
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
Type with a single subtype.
Definition type.h:180
const typet & subtype() const
Definition type.h:187
The type of an expression, extends irept.
Definition type.h:29
bool has_subtype() const
Definition type.h:64
The vector type.
Definition std_types.h:1064
ANSI-C Language Type Checking.
STL namespace.
BigInt mp_integer
Definition smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Symbol table entry.