cprover
Loading...
Searching...
No Matches
c_typecheck_expr.cpp
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#include <util/arith_tools.h>
13#include <util/bitvector_expr.h>
14#include <util/c_types.h>
15#include <util/config.h>
16#include <util/cprover_prefix.h>
17#include <util/expr_util.h>
18#include <util/floatbv_expr.h>
19#include <util/ieee_float.h>
22#include <util/pointer_expr.h>
25#include <util/range.h>
26#include <util/simplify_expr.h>
28#include <util/suffix.h>
30
32
33#include "anonymous_member.h"
34#include "ansi_c_declaration.h"
35#include "builtin_factory.h"
36#include "c_expr.h"
37#include "c_qualifiers.h"
38#include "c_typecast.h"
39#include "c_typecheck_base.h"
40#include "expr2c.h"
41#include "padding.h"
42#include "type2name.h"
43
44#include <sstream>
45
47{
48 if(expr.id()==ID_already_typechecked)
49 {
50 expr.swap(to_already_typechecked_expr(expr).get_expr());
51 return;
52 }
53
54 // first do sub-nodes
56
57 // now do case-split
59}
60
62{
63 for(auto &op : expr.operands())
65
66 if(expr.id()==ID_div ||
67 expr.id()==ID_mult ||
68 expr.id()==ID_plus ||
69 expr.id()==ID_minus)
70 {
71 if(expr.type().id()==ID_floatbv &&
72 expr.operands().size()==2)
73 {
74 // The rounding mode to be used at compile time is non-obvious.
75 // We'll simply use round to even (0), which is suggested
76 // by Sec. F.7.2 Translation, ISO-9899:1999.
77 expr.operands().resize(3);
78
79 if(expr.id()==ID_div)
80 expr.id(ID_floatbv_div);
81 else if(expr.id()==ID_mult)
82 expr.id(ID_floatbv_mult);
83 else if(expr.id()==ID_plus)
84 expr.id(ID_floatbv_plus);
85 else if(expr.id()==ID_minus)
86 expr.id(ID_floatbv_minus);
87 else
89
92 }
93 }
94}
95
97 const typet &type1,
98 const typet &type2)
99{
100 // read
101 // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
102
103 // check qualifiers first
104 if(c_qualifierst(type1)!=c_qualifierst(type2))
105 return false;
106
107 if(type1.id()==ID_c_enum_tag)
109 else if(type2.id()==ID_c_enum_tag)
111
112 if(type1.id()==ID_c_enum)
113 {
114 if(type2.id()==ID_c_enum) // both are enums
115 return type1==type2; // compares the tag
116 else if(type2 == to_c_enum_type(type1).underlying_type())
117 return true;
118 }
119 else if(type2.id()==ID_c_enum)
120 {
121 if(type1 == to_c_enum_type(type2).underlying_type())
122 return true;
123 }
124 else if(type1.id()==ID_pointer &&
125 type2.id()==ID_pointer)
126 {
128 to_pointer_type(type1).base_type(), to_pointer_type(type2).base_type());
129 }
130 else if(type1.id()==ID_array &&
131 type2.id()==ID_array)
132 {
134 to_array_type(type1).element_type(),
135 to_array_type(type2).element_type()); // ignore size
136 }
137 else if(type1.id()==ID_code &&
138 type2.id()==ID_code)
139 {
140 const code_typet &c_type1=to_code_type(type1);
141 const code_typet &c_type2=to_code_type(type2);
142
144 c_type1.return_type(),
145 c_type2.return_type()))
146 return false;
147
148 if(c_type1.parameters().size()!=c_type2.parameters().size())
149 return false;
150
151 for(std::size_t i=0; i<c_type1.parameters().size(); i++)
153 c_type1.parameters()[i].type(),
154 c_type2.parameters()[i].type()))
155 return false;
156
157 return true;
158 }
159 else
160 {
161 if(type1==type2)
162 {
163 // Need to distinguish e.g. long int from int or
164 // long long int from long int.
165 // The rules appear to match those of C++.
166
167 if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type))
168 return true;
169 }
170 }
171
172 return false;
173}
174
176{
177 if(expr.id()==ID_side_effect)
179 else if(expr.is_constant())
181 else if(expr.id()==ID_infinity)
182 {
183 // ignore
184 }
185 else if(expr.id()==ID_symbol)
187 else if(expr.id()==ID_unary_plus ||
188 expr.id()==ID_unary_minus ||
189 expr.id()==ID_bitnot)
191 else if(expr.id()==ID_not)
193 else if(
194 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies ||
195 expr.id() == ID_xor)
197 else if(expr.id()==ID_address_of)
199 else if(expr.id()==ID_dereference)
201 else if(expr.id()==ID_member)
203 else if(expr.id()==ID_ptrmember)
205 else if(expr.id()==ID_equal ||
206 expr.id()==ID_notequal ||
207 expr.id()==ID_lt ||
208 expr.id()==ID_le ||
209 expr.id()==ID_gt ||
210 expr.id()==ID_ge)
212 else if(expr.id()==ID_index)
214 else if(expr.id()==ID_typecast)
216 else if(expr.id()==ID_sizeof)
218 else if(expr.id()==ID_alignof)
220 else if(
221 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
222 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand ||
223 expr.id() == ID_bitxor || expr.id() == ID_bitor || expr.id() == ID_bitnand)
224 {
226 }
227 else if(expr.id()==ID_shl || expr.id()==ID_shr)
229 else if(expr.id()==ID_comma)
231 else if(expr.id()==ID_if)
233 else if(expr.id()==ID_code)
234 {
236 error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
237 throw 0;
238 }
239 else if(expr.id()==ID_gcc_builtin_va_arg)
241 else if(expr.id()==ID_cw_va_arg_typeof)
243 else if(expr.id()==ID_gcc_builtin_types_compatible_p)
244 {
245 expr.type()=bool_typet();
246 auto &subtypes =
247 (static_cast<type_with_subtypest &>(expr.add(ID_type_arg))).subtypes();
248 PRECONDITION(subtypes.size() == 2);
249 typecheck_type(subtypes[0]);
250 typecheck_type(subtypes[1]);
251 source_locationt source_location=expr.source_location();
252
253 // ignores top-level qualifiers
254 subtypes[0].remove(ID_C_constant);
255 subtypes[0].remove(ID_C_volatile);
256 subtypes[0].remove(ID_C_restricted);
257 subtypes[1].remove(ID_C_constant);
258 subtypes[1].remove(ID_C_volatile);
259 subtypes[1].remove(ID_C_restricted);
260
261 expr = make_boolean_expr(gcc_types_compatible_p(subtypes[0], subtypes[1]));
262 expr.add_source_location()=source_location;
263 }
264 else if(expr.id()==ID_clang_builtin_convertvector)
265 {
266 // This has one operand and a type, and acts like a typecast
267 DATA_INVARIANT(expr.operands().size()==1, "clang_builtin_convertvector has one operand");
268 typecheck_type(expr.type());
269 typecast_exprt tmp(to_unary_expr(expr).op(), expr.type());
271 expr.swap(tmp);
272 }
273 else if(expr.id()==ID_builtin_offsetof)
275 else if(expr.id()==ID_string_constant)
276 {
277 // already fine -- mark as lvalue
278 expr.set(ID_C_lvalue, true);
279 }
280 else if(expr.id()==ID_arguments)
281 {
282 // already fine
283 }
284 else if(expr.id()==ID_designated_initializer)
285 {
286 exprt &designator=static_cast<exprt &>(expr.add(ID_designator));
287
288 Forall_operands(it, designator)
289 {
290 if(it->id()==ID_index)
291 typecheck_expr(to_unary_expr(*it).op()); // still needs typechecking
292 }
293 }
294 else if(expr.id()==ID_initializer_list)
295 {
296 // already fine, just set some type
297 expr.type()=void_type();
298 }
299 else if(
300 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
301 {
302 // These have two operands.
303 // op0 is a tuple with declarations,
304 // op1 is the bound expression
305 auto &binary_expr = to_binary_expr(expr);
306 auto &bindings = binary_expr.op0().operands();
307 auto &where = binary_expr.op1();
308
309 for(const auto &binding : bindings)
310 {
311 if(binding.get(ID_statement) != ID_decl)
312 {
314 error() << "expected declaration as operand of quantifier" << eom;
315 throw 0;
316 }
317 }
318
319 if(has_subexpr(
320 where,
321 [&](const exprt &subexpr)
322 {
323 return can_cast_expr<side_effect_exprt>(subexpr) &&
325 }))
326 {
328 error() << "quantifier must not contain function calls" << eom;
329 throw 0;
330 }
331
332 // replace declarations by symbol expressions
333 for(auto &binding : bindings)
334 binding = to_code_frontend_decl(to_code(binding)).symbol();
335
336 if(expr.id() == ID_lambda)
337 {
339
340 for(auto &binding : bindings)
341 domain.push_back(binding.type());
342
343 expr.type() = mathematical_function_typet(domain, where.type());
344 }
345 else
346 {
347 expr.type() = bool_typet();
349 }
350 }
351 else if(expr.id()==ID_label)
352 {
353 expr.type()=void_type();
354 }
355 else if(expr.id()==ID_array)
356 {
357 // these pop up as string constants, and are already typed
358 }
359 else if(expr.id()==ID_complex)
360 {
361 // these should only exist as constants,
362 // and should already be typed
363 }
364 else if(expr.id() == ID_complex_real)
365 {
366 const exprt &op = to_unary_expr(expr).op();
367
368 if(op.type().id() != ID_complex)
369 {
370 if(!is_number(op.type()))
371 {
373 error() << "real part retrieval expects numerical operand, "
374 << "but got '" << to_string(op.type()) << "'" << eom;
375 throw 0;
376 }
377
378 typecast_exprt typecast_expr(op, complex_typet(op.type()));
379 complex_real_exprt complex_real_expr(typecast_expr);
380
381 expr.swap(complex_real_expr);
382 }
383 else
384 {
385 complex_real_exprt complex_real_expr(op);
386
387 // these are lvalues if the operand is one
388 if(op.get_bool(ID_C_lvalue))
389 complex_real_expr.set(ID_C_lvalue, true);
390
391 if(op.type().get_bool(ID_C_constant))
392 complex_real_expr.type().set(ID_C_constant, true);
393
394 expr.swap(complex_real_expr);
395 }
396 }
397 else if(expr.id() == ID_complex_imag)
398 {
399 const exprt &op = to_unary_expr(expr).op();
400
401 if(op.type().id() != ID_complex)
402 {
403 if(!is_number(op.type()))
404 {
406 error() << "real part retrieval expects numerical operand, "
407 << "but got '" << to_string(op.type()) << "'" << eom;
408 throw 0;
409 }
410
411 typecast_exprt typecast_expr(op, complex_typet(op.type()));
412 complex_imag_exprt complex_imag_expr(typecast_expr);
413
414 expr.swap(complex_imag_expr);
415 }
416 else
417 {
418 complex_imag_exprt complex_imag_expr(op);
419
420 // these are lvalues if the operand is one
421 if(op.get_bool(ID_C_lvalue))
422 complex_imag_expr.set(ID_C_lvalue, true);
423
424 if(op.type().get_bool(ID_C_constant))
425 complex_imag_expr.type().set(ID_C_constant, true);
426
427 expr.swap(complex_imag_expr);
428 }
429 }
430 else if(expr.id()==ID_generic_selection)
431 {
432 // This is C11.
433 // The operand is already typechecked. Depending
434 // on its type, we return one of the generic associations.
435 auto &op = to_unary_expr(expr).op();
436
437 // This is one of the few places where it's detectable
438 // that we are using "bool" for boolean operators instead
439 // of "int". We convert for this reason.
440 if(op.is_boolean())
442
443 irept::subt &generic_associations=
444 expr.add(ID_generic_associations).get_sub();
445
446 // first typecheck all types
447 for(auto &irep : generic_associations)
448 {
449 if(irep.get(ID_type_arg) != ID_default)
450 {
451 typet &type = static_cast<typet &>(irep.add(ID_type_arg));
452 typecheck_type(type);
453 }
454 }
455
456 // first try non-default match
457 exprt default_match=nil_exprt();
458 exprt assoc_match=nil_exprt();
459
460 const typet &op_type = op.type();
461
462 for(const auto &irep : generic_associations)
463 {
464 if(irep.get(ID_type_arg) == ID_default)
465 default_match = static_cast<const exprt &>(irep.find(ID_value));
466 else if(op_type == static_cast<const typet &>(irep.find(ID_type_arg)))
467 {
468 assoc_match = static_cast<const exprt &>(irep.find(ID_value));
469 }
470 }
471
472 if(assoc_match.is_nil())
473 {
474 if(default_match.is_not_nil())
475 expr.swap(default_match);
476 else
477 {
479 error() << "unmatched generic selection: " << to_string(op.type())
480 << eom;
481 throw 0;
482 }
483 }
484 else
485 expr.swap(assoc_match);
486
487 // still need to typecheck the result
488 typecheck_expr(expr);
489 }
490 else if(expr.id()==ID_gcc_asm_input ||
491 expr.id()==ID_gcc_asm_output ||
492 expr.id()==ID_gcc_asm_clobbered_register)
493 {
494 }
495 else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
496 expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
497 {
498 // already type checked
499 }
500 else if(
501 expr.id() == ID_C_spec_assigns || expr.id() == ID_C_spec_frees ||
502 expr.id() == ID_target_list)
503 {
504 // already type checked
505 }
506 else if(auto bit_cast_expr = expr_try_dynamic_cast<bit_cast_exprt>(expr))
507 {
508 typecheck_type(expr.type());
509 if(
510 pointer_offset_bits(bit_cast_expr->type(), *this) ==
511 pointer_offset_bits(bit_cast_expr->op().type(), *this))
512 {
513 exprt tmp = bit_cast_expr->lower();
514 expr.swap(tmp);
515 }
516 else
517 {
519 error() << "bit cast from '" << to_string(bit_cast_expr->op().type())
520 << "' to '" << to_string(expr.type()) << "' not permitted" << eom;
521 throw 0;
522 }
523 }
524 else
525 {
527 error() << "unexpected expression: " << expr.pretty() << eom;
528 throw 0;
529 }
530}
531
533{
534 expr.type() = to_binary_expr(expr).op1().type();
535
536 // make this an l-value if the last operand is one
537 if(to_binary_expr(expr).op1().get_bool(ID_C_lvalue))
538 expr.set(ID_C_lvalue, true);
539}
540
542{
543 // The first parameter is the va_list, and the second
544 // is the type, which will need to be fixed and checked.
545 // The type is given by the parser as type of the expression.
546
547 typet arg_type=expr.type();
548 typecheck_type(arg_type);
549
550 const code_typet new_type(
551 {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
552
553 exprt arg = to_unary_expr(expr).op();
554
556
557 symbol_exprt function(ID_gcc_builtin_va_arg, new_type);
558 function.add_source_location() = expr.source_location();
559
560 // turn into function call
562 function, {arg}, new_type.return_type(), expr.source_location());
563
564 expr.swap(result);
565
566 // Make sure symbol exists, but we have it return void
567 // to avoid collisions of the same symbol with different
568 // types.
569
570 code_typet symbol_type=new_type;
571 symbol_type.return_type()=void_type();
572
573 symbolt symbol{ID_gcc_builtin_va_arg, symbol_type, ID_C};
574 symbol.base_name=ID_gcc_builtin_va_arg;
575
576 symbol_table.insert(std::move(symbol));
577}
578
580{
581 // used in Code Warrior via
582 //
583 // __va_arg( <Symbol>, _var_arg_typeof( <Typ> ) )
584 //
585 // where __va_arg is declared as
586 //
587 // extern void* __va_arg(void*, int);
588
589 typet &type=static_cast<typet &>(expr.add(ID_type_arg));
590 typecheck_type(type);
591
592 // these return an integer
593 expr.type()=signed_int_type();
594}
595
597{
598 // these need not be constant, due to array indices!
599
600 if(!expr.operands().empty())
601 {
603 error() << "builtin_offsetof expects no operands" << eom;
604 throw 0;
605 }
606
607 typet &type=static_cast<typet &>(expr.add(ID_type_arg));
608 typecheck_type(type);
609
610 const exprt &member = static_cast<const exprt &>(expr.add(ID_designator));
611
613
614 for(const auto &op : member.operands())
615 {
616 if(op.id() == ID_member)
617 {
618 if(type.id() != ID_union_tag && type.id() != ID_struct_tag)
619 {
621 error() << "offsetof of member expects struct/union type, "
622 << "but got '" << to_string(type) << "'" << eom;
623 throw 0;
624 }
625
626 bool found=false;
627 irep_idt component_name = op.get(ID_component_name);
628
629 while(!found)
630 {
631 PRECONDITION(type.id() == ID_union_tag || type.id() == ID_struct_tag);
632
633 const struct_union_typet &struct_union_type =
635
636 // direct member?
637 if(struct_union_type.has_component(component_name))
638 {
639 found=true;
640
641 if(type.id() == ID_struct_tag)
642 {
643 auto o_opt = member_offset_expr(
644 follow_tag(to_struct_tag_type(type)), component_name, *this);
645
646 if(!o_opt.has_value())
647 {
649 error() << "offsetof failed to determine offset of '"
650 << component_name << "'" << eom;
651 throw 0;
652 }
653
655 result,
657 }
658
659 type=struct_union_type.get_component(component_name).type();
660 }
661 else
662 {
663 // maybe anonymous?
664 bool found2=false;
665
666 for(const auto &c : struct_union_type.components())
667 {
668 if(
669 c.get_anonymous() &&
670 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
671 {
672 if(has_component_rec(c.type(), component_name, *this))
673 {
674 if(type.id() == ID_struct_tag)
675 {
676 auto o_opt = member_offset_expr(
677 follow_tag(to_struct_tag_type(type)), c.get_name(), *this);
678
679 if(!o_opt.has_value())
680 {
682 error() << "offsetof failed to determine offset of '"
683 << component_name << "'" << eom;
684 throw 0;
685 }
686
688 result,
690 o_opt.value(), size_type()));
691 }
692
693 typet tmp = c.type();
694 type=tmp;
696 type.id() == ID_union_tag || type.id() == ID_struct_tag);
697 found2=true;
698 break; // we run into another iteration of the outer loop
699 }
700 }
701 }
702
703 if(!found2)
704 {
706 error() << "offset-of of member failed to find component '"
707 << component_name << "' in '" << to_string(type) << "'"
708 << eom;
709 throw 0;
710 }
711 }
712 }
713 }
714 else if(op.id() == ID_index)
715 {
716 if(type.id()!=ID_array)
717 {
719 error() << "offsetof of index expects array type" << eom;
720 throw 0;
721 }
722
723 exprt index = to_unary_expr(op).op();
724
725 // still need to typecheck index
726 typecheck_expr(index);
727
728 auto element_size_opt =
729 size_of_expr(to_array_type(type).element_type(), *this);
730
731 if(!element_size_opt.has_value())
732 {
734 error() << "offsetof failed to determine array element size" << eom;
735 throw 0;
736 }
737
739
740 result = plus_exprt(result, mult_exprt(element_size_opt.value(), index));
741
742 typet tmp = to_array_type(type).element_type();
743 type=tmp;
744 }
745 }
746
747 // We make an effort to produce a constant,
748 // but this may depend on variables
749 simplify(result, *this);
750 result.add_source_location()=expr.source_location();
751
752 expr.swap(result);
753}
754
756{
757 if(expr.id()==ID_side_effect &&
758 expr.get(ID_statement)==ID_function_call)
759 {
760 // don't do function operand
761 typecheck_expr(to_binary_expr(expr).op1()); // arguments
762 }
763 else if(expr.id()==ID_side_effect &&
764 expr.get(ID_statement)==ID_statement_expression)
765 {
767 }
768 else if(
769 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
770 {
771 // These introduce new symbols, which need to be added to the symbol table
772 // before the second operand is typechecked.
773
774 auto &binary_expr = to_binary_expr(expr);
775 auto &bindings = binary_expr.op0().operands();
776
777 for(auto &binding : bindings)
778 {
779 ansi_c_declarationt &declaration = to_ansi_c_declaration(binding);
780
781 typecheck_declaration(declaration);
782
783 if(declaration.declarators().size() != 1)
784 {
786 error() << "forall/exists expects one declarator exactly" << eom;
787 throw 0;
788 }
789
790 irep_idt identifier = declaration.declarators().front().get_name();
791
792 // look it up
793 symbol_table_baset::symbolst::const_iterator s_it =
794 symbol_table.symbols.find(identifier);
795
796 if(s_it == symbol_table.symbols.end())
797 {
799 error() << "failed to find bound symbol `" << identifier
800 << "' in symbol table" << eom;
801 throw 0;
802 }
803
804 const symbolt &symbol = s_it->second;
805
806 if(
807 symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
808 !is_complete_type(symbol.type) || symbol.type.id() == ID_code)
809 {
811 error() << "unexpected quantified symbol" << eom;
812 throw 0;
813 }
814
815 code_frontend_declt decl(symbol.symbol_expr());
816 decl.add_source_location() = declaration.source_location();
817
818 binding = decl;
819 }
820
821 typecheck_expr(binary_expr.op1());
822 }
823 else
824 {
825 Forall_operands(it, expr)
826 typecheck_expr(*it);
827 }
828}
829
831{
832 irep_idt identifier=to_symbol_expr(expr).get_identifier();
833
834 // Is it a parameter? We do this while checking parameter lists.
835 id_type_mapt::const_iterator p_it=parameter_map.find(identifier);
836 if(p_it!=parameter_map.end())
837 {
838 // yes
839 expr.type()=p_it->second;
840 expr.set(ID_C_lvalue, true);
841 return;
842 }
843
844 // renaming via GCC asm label
845 asm_label_mapt::const_iterator entry=
846 asm_label_map.find(identifier);
847 if(entry!=asm_label_map.end())
848 {
849 identifier=entry->second;
850 to_symbol_expr(expr).set_identifier(identifier);
851 }
852
853 // look it up
854 const symbolt *symbol_ptr;
855 if(lookup(identifier, symbol_ptr))
856 {
858 error() << "failed to find symbol '" << identifier << "'" << eom;
859 throw 0;
860 }
861
862 const symbolt &symbol=*symbol_ptr;
863
864 if(symbol.is_type)
865 {
867 error() << "did not expect a type symbol here, but got '"
868 << symbol.display_name() << "'" << eom;
869 throw 0;
870 }
871
872 // save the source location
873 source_locationt source_location=expr.source_location();
874
875 if(symbol.is_macro)
876 {
877 // preserve enum key
878 #if 0
879 irep_idt base_name=expr.get(ID_C_base_name);
880 #endif
881
882 follow_macros(expr);
883
884 #if 0
885 if(expr.is_constant() && !base_name.empty())
886 expr.set(ID_C_cformat, base_name);
887 else
888 #endif
889 typecheck_expr(expr);
890
891 // preserve location
892 expr.add_source_location()=source_location;
893 }
894 else if(identifier.starts_with(CPROVER_PREFIX "constant_infinity"))
895 {
896 expr=infinity_exprt(symbol.type);
897
898 // put it back
899 expr.add_source_location()=source_location;
900 }
901 else if(identifier=="__func__" ||
902 identifier=="__FUNCTION__" ||
903 identifier=="__PRETTY_FUNCTION__")
904 {
905 // __func__ is an ANSI-C standard compliant hack to get the function name
906 // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
907 string_constantt s(source_location.get_function());
908 s.add_source_location()=source_location;
909 s.set(ID_C_lvalue, true);
910 expr.swap(s);
911 }
912 else
913 {
914 expr=symbol.symbol_expr();
915
916 // put it back
917 expr.add_source_location()=source_location;
918
919 if(symbol.is_lvalue)
920 expr.set(ID_C_lvalue, true);
921
922 if(expr.type().id()==ID_code) // function designator
923 { // special case: this is sugar for &f
924 address_of_exprt tmp(expr, pointer_type(expr.type()));
925 tmp.set(ID_C_implicit, true);
927 expr=tmp;
928 }
929 }
930}
931
933 side_effect_exprt &expr)
934{
935 codet &code = to_code(to_unary_expr(expr).op());
936
937 // the type is the type of the last statement in the
938 // block, but do worry about labels!
939
941
942 irep_idt last_statement=last.get_statement();
943
944 if(last_statement==ID_expression)
945 {
946 PRECONDITION(last.operands().size() == 1);
947 exprt &op=last.op0();
948
949 // arrays here turn into pointers (array decay)
950 if(op.type().id()==ID_array)
953
954 expr.type()=op.type();
955 }
956 else
957 {
958 // we used to do this, but don't expect it any longer
959 PRECONDITION(last_statement != ID_function_call);
960
961 expr.type()=typet(ID_empty);
962 }
963}
964
966{
967 typet type;
968
969 // these come in two flavors: with zero operands, for a type,
970 // and with one operand, for an expression.
971 PRECONDITION(expr.operands().size() <= 1);
972
973 if(expr.operands().empty())
974 {
975 type.swap(static_cast<typet &>(expr.add(ID_type_arg)));
976 typecheck_type(type);
977 }
978 else
979 {
980 const exprt &op = to_unary_expr(as_const(expr)).op();
981 // This is one of the few places where it's detectable
982 // that we are using "bool" for boolean operators instead
983 // of "int". We convert for this reason.
984 if(op.is_boolean())
985 type = signed_int_type();
986 else
987 type = op.type();
988 }
989
990 exprt new_expr;
991
992 if(type.id()==ID_c_bit_field)
993 {
994 // only comma or side-effect expressions are permitted
995 const exprt &op = skip_typecast(to_unary_expr(as_const(expr)).op());
996 if(op.id() == ID_comma || op.id() == ID_side_effect)
997 {
998 const c_bit_field_typet &bf_type = to_c_bit_field_type(type);
999 if(config.ansi_c.mode == configt::ansi_ct::flavourt::GCC)
1000 {
1001 new_expr = from_integer(
1002 (bf_type.get_width() + config.ansi_c.char_width - 1) /
1003 config.ansi_c.char_width,
1004 size_type());
1005 }
1006 else
1007 {
1008 auto size_of_opt = size_of_expr(bf_type.underlying_type(), *this);
1009
1010 if(!size_of_opt.has_value())
1011 {
1013 error() << "type has no size: "
1014 << to_string(bf_type.underlying_type()) << eom;
1015 throw 0;
1016 }
1017
1018 new_expr = size_of_opt.value();
1019 }
1020 }
1021 else
1022 {
1024 error() << "sizeof cannot be applied to bit fields" << eom;
1025 throw 0;
1026 }
1027 }
1028 else if(type.id() == ID_bool)
1029 {
1031 error() << "sizeof cannot be applied to single bits" << eom;
1032 throw 0;
1033 }
1034 else if(type.id() == ID_empty)
1035 {
1036 // This is a gcc extension.
1037 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
1038 new_expr = from_integer(1, size_type());
1039 }
1040 else
1041 {
1042 if(
1043 (type.id() == ID_struct_tag &&
1044 follow_tag(to_struct_tag_type(type)).is_incomplete()) ||
1045 (type.id() == ID_union_tag &&
1046 follow_tag(to_union_tag_type(type)).is_incomplete()) ||
1047 (type.id() == ID_c_enum_tag &&
1048 follow_tag(to_c_enum_tag_type(type)).is_incomplete()) ||
1049 (type.id() == ID_array && to_array_type(type).is_incomplete()))
1050 {
1052 error() << "invalid application of \'sizeof\' to an incomplete type\n\t\'"
1053 << to_string(type) << "\'" << eom;
1054 throw 0;
1055 }
1056
1057 auto size_of_opt = size_of_expr(type, *this);
1058
1059 if(!size_of_opt.has_value())
1060 {
1062 error() << "type has no size: " << to_string(type) << eom;
1063 throw 0;
1064 }
1065
1066 new_expr = size_of_opt.value();
1067 }
1068
1069 source_locationt location = expr.source_location();
1070 new_expr.swap(expr);
1071 expr.add_source_location() = location;
1072 expr.add(ID_C_c_sizeof_type)=type;
1073
1074 // The type may contain side-effects.
1075 if(!clean_code.empty())
1076 {
1077 side_effect_exprt side_effect_expr(
1078 ID_statement_expression, void_type(), location);
1079 auto decl_block=code_blockt::from_list(clean_code);
1080 decl_block.set_statement(ID_decl_block);
1081 side_effect_expr.copy_to_operands(decl_block);
1082 clean_code.clear();
1083
1084 // We merge the side-effect into the operand of the typecast,
1085 // using a comma-expression.
1086 // I.e., (type)e becomes (type)(side-effect, e)
1087 // It is not obvious whether the type or 'e' should be evaluated
1088 // first.
1089
1090 exprt comma_expr =
1091 binary_exprt{std::move(side_effect_expr), ID_comma, expr, expr.type()}
1092 .with_source_location(location);
1093 expr.swap(comma_expr);
1094 }
1095}
1096
1098{
1099 typet argument_type;
1100
1101 if(expr.operands().size()==1)
1102 argument_type = to_unary_expr(expr).op().type();
1103 else
1104 {
1105 typet &op_type=static_cast<typet &>(expr.add(ID_type_arg));
1106 typecheck_type(op_type);
1107 argument_type=op_type;
1108 }
1109
1110 // we only care about the type
1111 mp_integer a=alignment(argument_type, *this);
1112
1113 exprt tmp=from_integer(a, size_type());
1115
1116 expr.swap(tmp);
1117}
1118
1120{
1121 exprt &op = to_unary_expr(expr).op();
1122
1123 typecheck_type(expr.type());
1124
1125 // The type may contain side-effects.
1126 if(!clean_code.empty())
1127 {
1128 side_effect_exprt side_effect_expr(
1129 ID_statement_expression, void_type(), expr.source_location());
1130 auto decl_block=code_blockt::from_list(clean_code);
1131 decl_block.set_statement(ID_decl_block);
1132 side_effect_expr.copy_to_operands(decl_block);
1133 clean_code.clear();
1134
1135 // We merge the side-effect into the operand of the typecast,
1136 // using a comma-expression.
1137 // I.e., (type)e becomes (type)(side-effect, e)
1138 // It is not obvious whether the type or 'e' should be evaluated
1139 // first.
1140
1141 binary_exprt comma_expr{
1142 std::move(side_effect_expr), ID_comma, op, op.type()};
1143 op.swap(comma_expr);
1144 }
1145
1146 const typet expr_type = expr.type();
1147
1148 if(
1149 expr_type.id() == ID_union_tag && expr_type != op.type() &&
1150 op.id() != ID_initializer_list)
1151 {
1152 // This is a GCC extension. It's either a 'temporary union',
1153 // where the argument is one of the member types.
1154
1155 // This is one of the few places where it's detectable
1156 // that we are using "bool" for boolean operators instead
1157 // of "int". We convert for this reason.
1158 if(op.is_boolean())
1159 op = typecast_exprt(op, signed_int_type());
1160
1161 // we need to find a member with the right type
1162 const auto &union_type = follow_tag(to_union_tag_type(expr_type));
1163 for(const auto &c : union_type.components())
1164 {
1165 if(c.type() == op.type())
1166 {
1167 // found! build union constructor
1168 union_exprt union_expr(c.get_name(), op, expr.type());
1169 union_expr.add_source_location()=expr.source_location();
1170 expr=union_expr;
1171 expr.set(ID_C_lvalue, true);
1172 return;
1173 }
1174 }
1175
1176 // not found, complain
1178 error() << "type cast to union: type '" << to_string(op.type())
1179 << "' not found in union" << eom;
1180 throw 0;
1181 }
1182
1183 // We allow (TYPE){ initializer_list }
1184 // This is called "compound literal", and is syntactic
1185 // sugar for a (possibly local) declaration.
1186 if(op.id()==ID_initializer_list)
1187 {
1188 // just do a normal initialization
1189 do_initializer(op, expr.type(), false);
1190
1191 // This produces a struct-expression,
1192 // union-expression, array-expression,
1193 // or an expression for a pointer or scalar.
1194 // We produce a compound_literal expression.
1195 exprt tmp(ID_compound_literal, expr.type());
1196 tmp.copy_to_operands(op);
1197
1198 // handle the case of TYPE being an array with unspecified size
1199 if(op.id()==ID_array &&
1200 expr.type().id()==ID_array &&
1201 to_array_type(expr.type()).size().is_nil())
1202 tmp.type()=op.type();
1203
1204 expr=tmp;
1205 expr.set(ID_C_lvalue, true); // these are l-values
1206 return;
1207 }
1208
1209 // a cast to void is always fine
1210 if(expr_type.id()==ID_empty)
1211 return;
1212
1213 const typet op_type = op.type();
1214
1215 // cast to same type?
1216 if(expr_type == op_type)
1217 return; // it's ok
1218
1219 // vectors?
1220
1221 if(expr_type.id()==ID_vector)
1222 {
1223 // we are generous -- any vector to vector is fine
1224 if(op_type.id()==ID_vector)
1225 return;
1226 else if(op_type.id()==ID_signedbv ||
1227 op_type.id()==ID_unsignedbv)
1228 return;
1229 }
1230
1231 if(!is_numeric_type(expr_type) && expr_type.id()!=ID_pointer)
1232 {
1234 error() << "type cast to '" << to_string(expr_type) << "' is not permitted"
1235 << eom;
1236 throw 0;
1237 }
1238
1239 if(is_numeric_type(op_type) || op_type.id()==ID_pointer)
1240 {
1241 }
1242 else if(op_type.id()==ID_array)
1243 {
1244 // This is the promotion from an array
1245 // to a pointer to the first element.
1246 auto error_opt = c_typecastt::check_address_can_be_taken(op_type);
1247 if(error_opt.has_value())
1248 throw invalid_source_file_exceptiont{*error_opt, expr.source_location()};
1249
1250 index_exprt index(op, from_integer(0, c_index_type()));
1251 op=address_of_exprt(index);
1252 }
1253 else if(op_type.id()==ID_empty)
1254 {
1255 if(expr_type.id()!=ID_empty)
1256 {
1258 error() << "type cast from void only permitted to void, but got '"
1259 << to_string(expr.type()) << "'" << eom;
1260 throw 0;
1261 }
1262 }
1263 else if(op_type.id()==ID_vector)
1264 {
1265 const vector_typet &op_vector_type=
1266 to_vector_type(op_type);
1267
1268 // gcc allows conversion of a vector of size 1 to
1269 // an integer/float of the same size
1270 if((expr_type.id()==ID_signedbv ||
1271 expr_type.id()==ID_unsignedbv) &&
1272 pointer_offset_bits(expr_type, *this)==
1273 pointer_offset_bits(op_vector_type, *this))
1274 {
1275 }
1276 else
1277 {
1279 error() << "type cast from vector to '" << to_string(expr.type())
1280 << "' not permitted" << eom;
1281 throw 0;
1282 }
1283 }
1284 else
1285 {
1287 error() << "type cast from '" << to_string(op_type) << "' not permitted"
1288 << eom;
1289 throw 0;
1290 }
1291
1292 // The new thing is an lvalue if the previous one is
1293 // an lvalue and it's just a pointer type cast.
1294 // This isn't really standard conformant!
1295 // Note that gcc says "warning: target of assignment not really an lvalue;
1296 // this will be a hard error in the future", i.e., we
1297 // can hope that the code below will one day simply go away.
1298
1299 // Current versions of gcc in fact refuse to do this! Yay!
1300
1301 if(op.get_bool(ID_C_lvalue))
1302 {
1303 if(expr_type.id()==ID_pointer)
1304 expr.set(ID_C_lvalue, true);
1305 }
1306}
1307
1312
1314{
1315 exprt &array_expr = to_binary_expr(expr).op0();
1316 exprt &index_expr = to_binary_expr(expr).op1();
1317
1318 // we might have to swap them
1319
1320 {
1321 const typet &array_type = array_expr.type();
1322 const typet &index_type = index_expr.type();
1323
1324 if(
1325 array_type.id() != ID_array && array_type.id() != ID_pointer &&
1326 array_type.id() != ID_vector &&
1327 (index_type.id() == ID_array || index_type.id() == ID_pointer ||
1328 index_type.id() == ID_vector))
1329 std::swap(array_expr, index_expr);
1330 }
1331
1332 make_index_type(index_expr);
1333
1334 // array_expr is a reference to one of expr.operands(), when that vector is
1335 // swapped below the reference is no longer valid. final_array_type exists
1336 // beyond that point so can't be a reference
1337 const typet final_array_type = array_expr.type();
1338
1339 if(final_array_type.id()==ID_array ||
1340 final_array_type.id()==ID_vector)
1341 {
1342 expr.type() = to_type_with_subtype(final_array_type).subtype();
1343
1344 if(array_expr.get_bool(ID_C_lvalue))
1345 expr.set(ID_C_lvalue, true);
1346
1347 if(final_array_type.get_bool(ID_C_constant))
1348 expr.type().set(ID_C_constant, true);
1349 }
1350 else if(final_array_type.id()==ID_pointer)
1351 {
1352 // p[i] is syntactic sugar for *(p+i)
1353
1355 exprt::operandst summands;
1356 std::swap(summands, expr.operands());
1357 expr.add_to_operands(plus_exprt(std::move(summands), array_expr.type()));
1358 expr.id(ID_dereference);
1359 expr.set(ID_C_lvalue, true);
1360 expr.type() = to_pointer_type(final_array_type).base_type();
1361 }
1362 else
1363 {
1365 error() << "operator [] must take array/vector or pointer but got '"
1366 << to_string(array_expr.type()) << "'" << eom;
1367 throw 0;
1368 }
1369}
1370
1372{
1373 // equality and disequality on float is not mathematical equality!
1374 if(expr.op0().type().id() == ID_floatbv)
1375 {
1376 if(expr.id()==ID_equal)
1377 expr.id(ID_ieee_float_equal);
1378 else if(expr.id()==ID_notequal)
1379 expr.id(ID_ieee_float_notequal);
1380 }
1381}
1382
1385{
1386 exprt &op0=expr.op0();
1387 exprt &op1=expr.op1();
1388
1389 const typet o_type0=op0.type();
1390 const typet o_type1=op1.type();
1391
1392 if(o_type0.id() == ID_vector || o_type1.id() == ID_vector)
1393 {
1395 return;
1396 }
1397
1398 expr.type()=bool_typet();
1399
1400 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1401 {
1402 if(o_type0 == o_type1)
1403 {
1404 if(o_type0.id() != ID_array)
1405 {
1406 adjust_float_rel(expr);
1407 return; // no promotion necessary
1408 }
1409 }
1410 }
1411
1413
1414 const typet &type0=op0.type();
1415 const typet &type1=op1.type();
1416
1417 if(type0==type1)
1418 {
1419 if(is_number(type0))
1420 {
1421 adjust_float_rel(expr);
1422 return;
1423 }
1424
1425 if(type0.id()==ID_pointer)
1426 {
1427 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1428 return;
1429
1430 if(expr.id()==ID_le || expr.id()==ID_lt ||
1431 expr.id()==ID_ge || expr.id()==ID_gt)
1432 return;
1433 }
1434
1435 if(type0.id()==ID_string_constant)
1436 {
1437 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1438 return;
1439 }
1440 }
1441 else
1442 {
1443 // pointer and zero
1444 if(type0.id()==ID_pointer &&
1445 simplify_expr(op1, *this).is_zero())
1446 {
1447 op1 = null_pointer_exprt{to_pointer_type(type0)};
1448 return;
1449 }
1450
1451 if(type1.id()==ID_pointer &&
1452 simplify_expr(op0, *this).is_zero())
1453 {
1454 op0 = null_pointer_exprt{to_pointer_type(type1)};
1455 return;
1456 }
1457
1458 // pointer and integer
1459 if(type0.id()==ID_pointer && is_number(type1))
1460 {
1461 op1 = typecast_exprt(op1, type0);
1462 return;
1463 }
1464
1465 if(type1.id()==ID_pointer && is_number(type0))
1466 {
1467 op0 = typecast_exprt(op0, type1);
1468 return;
1469 }
1470
1471 if(type0.id()==ID_pointer && type1.id()==ID_pointer)
1472 {
1473 op1 = typecast_exprt(op1, type0);
1474 return;
1475 }
1476 }
1477
1479 error() << "operator '" << expr.id() << "' not defined for types '"
1480 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
1481 << eom;
1482 throw 0;
1483}
1484
1486{
1487 const typet &o_type0 = as_const(expr).op0().type();
1488 const typet &o_type1 = as_const(expr).op1().type();
1489
1490 if(o_type0.id() != ID_vector || o_type0 != o_type1)
1491 {
1493 error() << "vector operator '" << expr.id() << "' not defined for types '"
1494 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
1495 << eom;
1496 throw 0;
1497 }
1498
1499 // Comparisons between vectors produce a vector of integers of the same width
1500 // with the same dimension.
1501 auto subtype_width =
1502 to_bitvector_type(to_vector_type(o_type0).element_type()).get_width();
1503 expr.type() = vector_typet{
1504 to_vector_type(o_type0).index_type(),
1505 signedbv_typet{subtype_width},
1506 to_vector_type(o_type0).size()};
1507
1508 // Replace the id as the semantics of these are point-wise application (and
1509 // the result is not of bool type).
1510 if(expr.id() == ID_notequal)
1511 expr.id(ID_vector_notequal);
1512 else
1513 expr.id("vector-" + id2string(expr.id()));
1514}
1515
1517{
1518 auto &op = to_unary_expr(expr).op();
1519 const typet &op0_type = op.type();
1520
1521 if(op0_type.id() == ID_array)
1522 {
1523 // a->f is the same as a[0].f
1524 exprt zero = from_integer(0, c_index_type());
1525 index_exprt index_expr(op, zero, to_array_type(op0_type).element_type());
1526 index_expr.set(ID_C_lvalue, true);
1527 op.swap(index_expr);
1528 }
1529 else if(op0_type.id() == ID_pointer)
1530 {
1531 // turn x->y into (*x).y
1533 deref_expr.add_source_location()=expr.source_location();
1535 op.swap(deref_expr);
1536 }
1537 else
1538 {
1540 error() << "ptrmember operator requires pointer or array type "
1541 "on left hand side, but got '"
1542 << to_string(op0_type) << "'" << eom;
1543 throw 0;
1544 }
1545
1546 expr.id(ID_member);
1548}
1549
1551{
1552 exprt &op0 = to_unary_expr(expr).op();
1553 typet type=op0.type();
1554
1555 if(type.id() != ID_struct_tag && type.id() != ID_union_tag)
1556 {
1558 error() << "member operator requires structure type "
1559 "on left hand side but got '"
1560 << to_string(type) << "'" << eom;
1561 throw 0;
1562 }
1563
1564 const struct_union_typet &struct_union_type =
1566
1567 if(struct_union_type.is_incomplete())
1568 {
1570 error() << "member operator got incomplete " << type.id()
1571 << " type on left hand side" << eom;
1572 throw 0;
1573 }
1574
1575 const irep_idt &component_name=
1576 expr.get(ID_component_name);
1577
1578 // first try to find directly
1580 struct_union_type.get_component(component_name);
1581
1582 // if that fails, search the anonymous members
1583
1584 if(component.is_nil())
1585 {
1586 exprt tmp=get_component_rec(op0, component_name, *this);
1587
1588 if(tmp.is_nil())
1589 {
1590 // give up
1592 error() << "member '" << component_name << "' not found in '"
1593 << to_string(type) << "'" << eom;
1594 throw 0;
1595 }
1596
1597 // done!
1598 expr.swap(tmp);
1599 return;
1600 }
1601
1602 expr.type()=component.type();
1603
1604 if(op0.get_bool(ID_C_lvalue))
1605 expr.set(ID_C_lvalue, true);
1606
1607 if(
1608 op0.type().get_bool(ID_C_constant) ||
1609 struct_union_type.get_bool(ID_C_constant))
1610 {
1611 expr.type().set(ID_C_constant, true);
1612 }
1613
1614 // copy method identifier
1615 const irep_idt &identifier=component.get(ID_C_identifier);
1616
1617 if(!identifier.empty())
1618 expr.set(ID_C_identifier, identifier);
1619
1620 const irep_idt &access=component.get_access();
1621
1622 if(access==ID_private)
1623 {
1625 error() << "member '" << component_name << "' is " << access << eom;
1626 throw 0;
1627 }
1628}
1629
1631{
1632 exprt::operandst &operands=expr.operands();
1633
1634 PRECONDITION(operands.size() == 3);
1635
1636 // copy (save) original types
1637 const typet o_type0=operands[0].type();
1638 const typet o_type1=operands[1].type();
1639 const typet o_type2=operands[2].type();
1640
1641 implicit_typecast_bool(operands[0]);
1642
1643 if(o_type1.id() == ID_empty || o_type2.id() == ID_empty)
1644 {
1645 operands[1] = typecast_exprt::conditional_cast(operands[1], void_type());
1646 operands[2] = typecast_exprt::conditional_cast(operands[2], void_type());
1647 expr.type() = void_type();
1648 return;
1649 }
1650
1651 if(
1652 auto string_constant = expr_try_dynamic_cast<string_constantt>(operands[1]))
1653 {
1654 implicit_typecast(operands[1], pointer_type(string_constant->char_type()));
1655 }
1656
1657 if(
1658 auto string_constant = expr_try_dynamic_cast<string_constantt>(operands[2]))
1659 {
1660 implicit_typecast(operands[2], pointer_type(string_constant->char_type()));
1661 }
1662
1663 if(operands[1].type().id()==ID_pointer &&
1664 operands[2].type().id()!=ID_pointer)
1665 implicit_typecast(operands[2], operands[1].type());
1666 else if(operands[2].type().id()==ID_pointer &&
1667 operands[1].type().id()!=ID_pointer)
1668 implicit_typecast(operands[1], operands[2].type());
1669
1670 if(operands[1].type().id()==ID_pointer &&
1671 operands[2].type().id()==ID_pointer &&
1672 operands[1].type()!=operands[2].type())
1673 {
1674 exprt tmp1=simplify_expr(operands[1], *this);
1675 exprt tmp2=simplify_expr(operands[2], *this);
1676
1677 // is one of them void * AND null? Convert that to the other.
1678 // (at least that's how GCC behaves)
1679 if(
1680 to_pointer_type(operands[1].type()).base_type().id() == ID_empty &&
1682 {
1683 implicit_typecast(operands[1], operands[2].type());
1684 }
1685 else if(
1686 to_pointer_type(operands[2].type()).base_type().id() == ID_empty &&
1688 {
1689 implicit_typecast(operands[2], operands[1].type());
1690 }
1691 else if(
1692 to_pointer_type(operands[1].type()).base_type().id() != ID_code ||
1693 to_pointer_type(operands[2].type()).base_type().id() != ID_code)
1694 {
1695 // Make it void *.
1696 // gcc and clang issue a warning for this.
1697 expr.type() = pointer_type(void_type());
1698 implicit_typecast(operands[1], expr.type());
1699 implicit_typecast(operands[2], expr.type());
1700 }
1701 else
1702 {
1703 // maybe functions without parameter lists
1704 const code_typet &c_type1 =
1705 to_code_type(to_pointer_type(operands[1].type()).base_type());
1706 const code_typet &c_type2 =
1707 to_code_type(to_pointer_type(operands[2].type()).base_type());
1708
1709 if(c_type1.return_type()==c_type2.return_type())
1710 {
1711 if(c_type1.parameters().empty() && c_type1.has_ellipsis())
1712 implicit_typecast(operands[1], operands[2].type());
1713 else if(c_type2.parameters().empty() && c_type2.has_ellipsis())
1714 implicit_typecast(operands[2], operands[1].type());
1715 }
1716 }
1717 }
1718
1719 if(operands[1].type().id()==ID_empty ||
1720 operands[2].type().id()==ID_empty)
1721 {
1722 expr.type()=void_type();
1723 return;
1724 }
1725
1726 if(
1727 operands[1].type() != operands[2].type() ||
1728 operands[1].type().id() == ID_array)
1729 {
1730 implicit_typecast_arithmetic(operands[1], operands[2]);
1731 }
1732
1733 if(operands[1].type() == operands[2].type())
1734 {
1735 expr.type()=operands[1].type();
1736
1737 // GCC says: "A conditional expression is a valid lvalue
1738 // if its type is not void and the true and false branches
1739 // are both valid lvalues."
1740
1741 if(operands[1].get_bool(ID_C_lvalue) &&
1742 operands[2].get_bool(ID_C_lvalue))
1743 expr.set(ID_C_lvalue, true);
1744
1745 return;
1746 }
1747
1749 error() << "operator ?: not defined for types '" << to_string(o_type1)
1750 << "' and '" << to_string(o_type2) << "'" << eom;
1751 throw 0;
1752}
1753
1755 side_effect_exprt &expr)
1756{
1757 // x ? : y is almost the same as x ? x : y,
1758 // but not quite, as x is evaluated only once
1759
1760 exprt::operandst &operands=expr.operands();
1761
1762 if(operands.size()!=2)
1763 {
1765 error() << "gcc conditional_expr expects two operands" << eom;
1766 throw 0;
1767 }
1768
1769 // use typechecking code for "if"
1770
1771 if_exprt if_expr(operands[0], operands[0], operands[1]);
1772 if_expr.add_source_location()=expr.source_location();
1773
1774 typecheck_expr_trinary(if_expr);
1775
1776 // copy the result
1777 operands[0] = if_expr.true_case();
1778 operands[1] = if_expr.false_case();
1779 expr.type()=if_expr.type();
1780}
1781
1783{
1784 exprt &op = to_unary_expr(expr).op();
1785
1786 auto error_opt = c_typecastt::check_address_can_be_taken(op.type());
1787
1788 if(error_opt.has_value())
1789 throw invalid_source_file_exceptiont{*error_opt, expr.source_location()};
1790
1791 // special case: address of label
1792 if(op.id()==ID_label)
1793 {
1794 expr.type()=pointer_type(void_type());
1795
1796 // remember the label
1797 labels_used[op.get(ID_identifier)]=op.source_location();
1798 return;
1799 }
1800
1801 // special case: address of function designator
1802 // ANSI-C 99 section 6.3.2.1 paragraph 4
1803
1804 if(
1805 op.id() == ID_address_of && op.get_bool(ID_C_implicit) &&
1806 to_address_of_expr(op).object().type().id() == ID_code)
1807 {
1808 // make the implicit address_of an explicit address_of
1809 exprt tmp;
1810 tmp.swap(op);
1811 tmp.set(ID_C_implicit, false);
1812 expr.swap(tmp);
1813 return;
1814 }
1815
1816 if(op.id()==ID_struct ||
1817 op.id()==ID_union ||
1818 op.id()==ID_array ||
1819 op.id()==ID_string_constant)
1820 {
1821 // these are really objects
1822 }
1823 else if(op.get_bool(ID_C_lvalue))
1824 {
1825 // ok
1826 }
1827 else if(op.type().id()==ID_code)
1828 {
1829 // ok
1830 }
1831 else
1832 {
1834 error() << "address_of error: '" << to_string(op) << "' not an lvalue"
1835 << eom;
1836 throw 0;
1837 }
1838
1839 expr.type()=pointer_type(op.type());
1840}
1841
1843{
1844 exprt &op = to_unary_expr(expr).op();
1845
1846 const typet op_type = op.type();
1847
1848 if(op_type.id()==ID_array)
1849 {
1850 // *a is the same as a[0]
1851 expr.id(ID_index);
1852 expr.type() = to_array_type(op_type).element_type();
1854 CHECK_RETURN(expr.operands().size() == 2);
1855 }
1856 else if(op_type.id()==ID_pointer)
1857 {
1858 expr.type() = to_pointer_type(op_type).base_type();
1859
1860 if(
1861 expr.type().id() == ID_empty &&
1863 {
1865 error() << "dereferencing void pointer" << eom;
1866 throw 0;
1867 }
1868 }
1869 else
1870 {
1872 error() << "operand of unary * '" << to_string(op)
1873 << "' is not a pointer, but got '" << to_string(op_type) << "'"
1874 << eom;
1875 throw 0;
1876 }
1877
1878 expr.set(ID_C_lvalue, true);
1879
1880 // if you dereference a pointer pointing to
1881 // a function, you get a pointer again
1882 // allowing ******...*p
1883
1885}
1886
1888{
1889 if(expr.type().id()==ID_code)
1890 {
1891 address_of_exprt tmp(expr, pointer_type(expr.type()));
1892 tmp.set(ID_C_implicit, true);
1894 expr=tmp;
1895 }
1896}
1897
1899{
1900 const irep_idt &statement=expr.get_statement();
1901
1902 if(statement==ID_preincrement ||
1903 statement==ID_predecrement ||
1904 statement==ID_postincrement ||
1905 statement==ID_postdecrement)
1906 {
1907 const exprt &op0 = to_unary_expr(expr).op();
1908 const typet &type0=op0.type();
1909
1910 if(!op0.get_bool(ID_C_lvalue))
1911 {
1913 error() << "prefix operator error: '" << to_string(op0)
1914 << "' not an lvalue" << eom;
1915 throw 0;
1916 }
1917
1918 if(type0.get_bool(ID_C_constant))
1919 {
1921 error() << "'" << to_string(op0) << "' is constant" << eom;
1922 throw 0;
1923 }
1924
1925 if(type0.id() == ID_c_enum_tag)
1926 {
1927 const c_enum_typet &enum_type = follow_tag(to_c_enum_tag_type(type0));
1928 if(enum_type.is_incomplete())
1929 {
1931 error() << "operator '" << statement << "' given incomplete type '"
1932 << to_string(type0) << "'" << eom;
1933 throw 0;
1934 }
1935
1936 // increment/decrement on underlying type
1937 to_unary_expr(expr).op() =
1938 typecast_exprt(op0, enum_type.underlying_type());
1939 expr.type() = enum_type.underlying_type();
1940 }
1941 else if(type0.id() == ID_c_bit_field)
1942 {
1943 // promote to underlying type
1944 typet underlying_type = to_c_bit_field_type(type0).underlying_type();
1945 typet type_before{type0};
1946 to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
1947 expr.type()=underlying_type;
1948 typecast_exprt result{expr, type_before};
1949 expr.swap(result);
1950 }
1951 else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
1952 {
1954 expr.type() = op0.type();
1955 }
1956 else if(is_numeric_type(type0))
1957 {
1958 expr.type()=type0;
1959 }
1960 else if(type0.id() == ID_pointer)
1961 {
1963 expr.type() = to_unary_expr(expr).op().type();
1964 }
1965 else
1966 {
1968 error() << "operator '" << statement << "' not defined for type '"
1969 << to_string(type0) << "'" << eom;
1970 throw 0;
1971 }
1972 }
1973 else if(statement.starts_with("assign"))
1975 else if(statement==ID_function_call)
1978 else if(statement==ID_statement_expression)
1980 else if(statement==ID_gcc_conditional_expression)
1982 else
1983 {
1985 error() << "unknown side effect: " << statement << eom;
1986 throw 0;
1987 }
1988}
1989
1992{
1993 INVARIANT(
1994 expr.function().id() == ID_symbol &&
1995 to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX
1996 "typed_target",
1997 "expression must be a " CPROVER_PREFIX "typed_target function call");
1998
1999 auto &f_op = to_symbol_expr(expr.function());
2000
2001 if(expr.arguments().size() != 1)
2002 {
2004 "expected 1 argument for " CPROVER_PREFIX "typed_target, found " +
2005 std::to_string(expr.arguments().size()),
2006 expr.source_location()};
2007 }
2008
2009 auto arg0 = expr.arguments().front();
2010
2011 if(!is_assignable(arg0) || !arg0.get_bool(ID_C_lvalue))
2012 {
2014 "argument of " CPROVER_PREFIX "typed_target must be assignable",
2015 arg0.source_location()};
2016 }
2017
2018 const auto &size = size_of_expr(arg0.type(), *this);
2019 if(!size.has_value())
2020 {
2022 "sizeof not defined for argument of " CPROVER_PREFIX
2023 "typed_target of type " +
2024 to_string(arg0.type()),
2025 arg0.source_location()};
2026 }
2027
2028 // rewrite call to "assignable"
2029 f_op.set_identifier(CPROVER_PREFIX "assignable");
2030 exprt::operandst arguments;
2031 // pointer
2032 arguments.push_back(address_of_exprt(arg0));
2033 // size
2034 arguments.push_back(size.value());
2035 // is_pointer
2036 if(arg0.type().id() == ID_pointer)
2037 arguments.push_back(true_exprt());
2038 else
2039 arguments.push_back(false_exprt());
2040
2041 expr.arguments().swap(arguments);
2042 expr.type() = empty_typet();
2043}
2044
2047{
2048 INVARIANT(
2049 expr.function().id() == ID_symbol &&
2050 to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX
2051 "obeys_contract",
2052 "expression must be a " CPROVER_PREFIX "obeys_contract function call");
2053
2054 if(expr.arguments().size() != 2)
2055 {
2057 "expected 2 arguments for " CPROVER_PREFIX "obeys_contract, found " +
2058 std::to_string(expr.arguments().size()),
2059 expr.source_location()};
2060 }
2061
2062 // the first parameter must be a function pointer typed assignable path
2063 // expression, without side effects or ternary operator
2064 auto &function_pointer = expr.arguments()[0];
2065
2066 if(
2067 function_pointer.type().id() != ID_pointer ||
2068 to_pointer_type(function_pointer.type()).base_type().id() != ID_code ||
2069 !function_pointer.get_bool(ID_C_lvalue))
2070 {
2072 "the first argument of " CPROVER_PREFIX
2073 "obeys_contract must be a function pointer lvalue expression",
2074 function_pointer.source_location());
2075 }
2076
2077 if(has_subexpr(function_pointer, ID_if))
2078 {
2080 "the first argument of " CPROVER_PREFIX
2081 "obeys_contract must have no ternary operator",
2082 function_pointer.source_location());
2083 }
2084
2085 // second parameter must be the address of a function symbol
2086 auto &address_of_contract = expr.arguments()[1];
2087
2088 if(
2089 address_of_contract.id() != ID_address_of ||
2090 to_address_of_expr(address_of_contract).object().id() != ID_symbol ||
2091 address_of_contract.type().id() != ID_pointer ||
2092 to_pointer_type(address_of_contract.type()).base_type().id() != ID_code)
2093 {
2095 "the second argument of " CPROVER_PREFIX
2096 "obeys_contract must must be a function symbol",
2097 address_of_contract.source_location());
2098 }
2099
2100 if(function_pointer.type() != address_of_contract.type())
2101 {
2103 "the first and second arguments of " CPROVER_PREFIX
2104 "obeys_contract must have the same function pointer type",
2105 expr.source_location());
2106 }
2107
2108 expr.type() = bool_typet();
2109}
2110
2112{
2113 return ::builtin_factory(
2114 identifier,
2115 config.ansi_c.float16_type,
2118}
2119
2122{
2123 if(expr.operands().size()!=2)
2124 {
2126 error() << "function_call side effect expects two operands" << eom;
2127 throw 0;
2128 }
2129
2130 exprt &f_op=expr.function();
2131
2132 // f_op is not yet typechecked, in contrast to the other arguments.
2133 // This is a big special case!
2134
2135 if(f_op.id()==ID_symbol)
2136 {
2137 irep_idt identifier=to_symbol_expr(f_op).get_identifier();
2138
2139 asm_label_mapt::const_iterator entry=
2140 asm_label_map.find(identifier);
2141 if(entry!=asm_label_map.end())
2142 identifier=entry->second;
2143
2144 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
2145 {
2146 // This is an undeclared function.
2147
2148 // Is it the polymorphic typed_target function ?
2149 if(identifier == CPROVER_PREFIX "typed_target")
2150 {
2152 }
2153 // Is this a builtin?
2154 else if(!builtin_factory(identifier))
2155 {
2156 // yes, it's a builtin
2157 }
2158 else if(
2159 identifier == "__noop" &&
2161 {
2162 // https://docs.microsoft.com/en-us/cpp/intrinsics/noop
2163 // typecheck and discard, just generating 0 instead
2164 for(auto &op : expr.arguments())
2165 typecheck_expr(op);
2166
2168 expr.swap(result);
2169
2170 return;
2171 }
2172 else if(
2173 identifier == "__builtin_shuffle" &&
2175 {
2177 expr.swap(result);
2178
2179 return;
2180 }
2181 else if(identifier == "__builtin_shufflevector")
2182 {
2184 expr.swap(result);
2185
2186 return;
2187 }
2188 else if(
2189 identifier == CPROVER_PREFIX "saturating_minus" ||
2190 identifier == CPROVER_PREFIX "saturating_plus" ||
2191 identifier == "__builtin_elementwise_add_sat" ||
2192 identifier == "__builtin_elementwise_sub_sat")
2193 {
2195 expr.swap(result);
2196
2197 return;
2198 }
2199 else if(identifier == CPROVER_PREFIX "equal")
2200 {
2201 if(expr.arguments().size() != 2)
2202 {
2204 error() << "equal expects two operands" << eom;
2205 throw 0;
2206 }
2207
2208 equal_exprt equality_expr(
2209 expr.arguments().front(), expr.arguments().back());
2210 equality_expr.add_source_location() = expr.source_location();
2211
2212 if(equality_expr.lhs().type() != equality_expr.rhs().type())
2213 {
2215 error() << "equal expects two operands of same type" << eom;
2216 throw 0;
2217 }
2218
2219 expr.swap(equality_expr);
2220 return;
2221 }
2222 else if(
2223 identifier == CPROVER_PREFIX "overflow_minus" ||
2224 identifier == CPROVER_PREFIX "overflow_mult" ||
2225 identifier == CPROVER_PREFIX "overflow_plus" ||
2226 identifier == CPROVER_PREFIX "overflow_shl")
2227 {
2228 exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
2229 overflow.add_source_location() = f_op.source_location();
2230
2231 if(identifier == CPROVER_PREFIX "overflow_minus")
2232 {
2233 overflow.id(ID_minus);
2235 }
2236 else if(identifier == CPROVER_PREFIX "overflow_mult")
2237 {
2238 overflow.id(ID_mult);
2240 }
2241 else if(identifier == CPROVER_PREFIX "overflow_plus")
2242 {
2243 overflow.id(ID_plus);
2245 }
2246 else if(identifier == CPROVER_PREFIX "overflow_shl")
2247 {
2248 overflow.id(ID_shl);
2250 }
2251
2253 overflow.operands()[0], overflow.id(), overflow.operands()[1]};
2254 of.add_source_location() = overflow.source_location();
2255 expr.swap(of);
2256 return;
2257 }
2258 else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
2259 {
2260 exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
2261 tmp.add_source_location() = f_op.source_location();
2262
2264
2265 unary_minus_overflow_exprt overflow{tmp.operands().front()};
2266 overflow.add_source_location() = tmp.source_location();
2267 expr.swap(overflow);
2268 return;
2269 }
2270 else if(identifier == CPROVER_PREFIX "enum_is_in_range")
2271 {
2272 // Check correct number of arguments
2273 if(expr.arguments().size() != 1)
2274 {
2275 std::ostringstream error_message;
2276 error_message << identifier << " takes exactly 1 argument, but "
2277 << expr.arguments().size() << " were provided";
2279 error_message.str(), expr.source_location()};
2280 }
2281 const auto &arg1 = expr.arguments()[0];
2282 if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
2283 {
2284 // Can't enum range check a non-enum
2285 std::ostringstream error_message;
2286 error_message << identifier << " expects enum, but ("
2287 << expr2c(arg1, *this) << ") has type `"
2288 << type2c(arg1.type(), *this) << '`';
2290 error_message.str(), expr.source_location()};
2291 }
2292
2293 enum_is_in_range_exprt in_range{arg1};
2294 in_range.add_source_location() = expr.source_location();
2295 exprt lowered = in_range.lower(*this);
2296 expr.swap(lowered);
2297 return;
2298 }
2299 else if(
2300 identifier == CPROVER_PREFIX "r_ok" ||
2301 identifier == CPROVER_PREFIX "w_ok" ||
2302 identifier == CPROVER_PREFIX "rw_ok")
2303 {
2304 if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
2305 {
2307 id2string(identifier) + " expects one or two operands",
2308 f_op.source_location()};
2309 }
2310
2311 // the first argument must be a pointer
2312 auto &pointer_expr = expr.arguments()[0];
2313 if(pointer_expr.type().id() == ID_array)
2314 {
2315 auto dest_type = pointer_type(void_type());
2316 dest_type.base_type().set(ID_C_constant, true);
2317 implicit_typecast(pointer_expr, dest_type);
2318 }
2319 else if(pointer_expr.type().id() != ID_pointer)
2320 {
2322 id2string(identifier) + " expects a pointer as first argument",
2323 f_op.source_location()};
2324 }
2325
2326 // The second argument, when given, is a size_t.
2327 // When not given, use the pointer subtype.
2328 exprt size_expr;
2329
2330 if(expr.arguments().size() == 2)
2331 {
2333 size_expr = expr.arguments()[1];
2334 }
2335 else
2336 {
2337 // Won't do void *
2338 const auto &subtype =
2339 to_pointer_type(pointer_expr.type()).base_type();
2340 if(subtype.id() == ID_empty)
2341 {
2343 id2string(identifier) +
2344 " expects a size when given a void pointer",
2345 f_op.source_location()};
2346 }
2347
2348 auto size_expr_opt = size_of_expr(subtype, *this);
2349 CHECK_RETURN(size_expr_opt.has_value());
2350 size_expr = std::move(size_expr_opt.value());
2351 }
2352
2353 irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok
2354 : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok
2355 : ID_rw_ok;
2356
2357 r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
2358 ok_expr.add_source_location() = expr.source_location();
2359
2360 expr.swap(ok_expr);
2361 return;
2362 }
2363 else if(
2364 auto shadow_memory_builtin = typecheck_shadow_memory_builtin(expr))
2365 {
2366 irep_idt shadow_memory_builtin_id =
2367 shadow_memory_builtin->get_identifier();
2368
2369 const auto builtin_code_type =
2370 to_code_type(shadow_memory_builtin->type());
2371
2372 INVARIANT(
2373 builtin_code_type.has_ellipsis() &&
2374 builtin_code_type.parameters().empty(),
2375 "Shadow memory builtins should be an ellipsis with 0 parameter");
2376
2377 // Add the symbol to the symbol table if it is not present yet.
2378 if(!symbol_table.has_symbol(shadow_memory_builtin_id))
2379 {
2380 symbolt new_symbol{
2381 shadow_memory_builtin_id, shadow_memory_builtin->type(), ID_C};
2382 new_symbol.base_name = shadow_memory_builtin_id;
2383 new_symbol.location = f_op.source_location();
2384 // Add an empty implementation to avoid warnings about missing
2385 // implementation later on
2386 new_symbol.value = code_blockt{};
2387
2388 symbol_table.add(new_symbol);
2389 }
2390
2391 // Swap the current `function` field with the newly generated
2392 // `shadow_memory_builtin` `symbol_exprt` and carry on with typechecking
2393 f_op = std::move(*shadow_memory_builtin);
2394 }
2395 else if(
2396 auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
2397 identifier, expr.arguments(), f_op.source_location()))
2398 {
2399 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
2400 auto &parameters = to_code_type(gcc_polymorphic->type()).parameters();
2401 INVARIANT(
2402 !parameters.empty(),
2403 "GCC polymorphic built-ins should have at least one parameter");
2404
2405 // For all atomic/sync polymorphic built-ins (which are the ones handled
2406 // by typecheck_gcc_polymorphic_builtin), looking at the first parameter
2407 // suffices to distinguish different implementations.
2408 if(parameters.front().type().id() == ID_pointer)
2409 {
2410 identifier_with_type =
2411 id2string(identifier) + "_" +
2413 to_pointer_type(parameters.front().type()).base_type(), *this);
2414 }
2415 else
2416 {
2417 identifier_with_type =
2418 id2string(identifier) + "_" +
2419 type_to_partial_identifier(parameters.front().type(), *this);
2420 }
2421 gcc_polymorphic->set_identifier(identifier_with_type);
2422
2423 if(!symbol_table.has_symbol(identifier_with_type))
2424 {
2425 for(std::size_t i = 0; i < parameters.size(); ++i)
2426 {
2427 const std::string base_name = "p_" + std::to_string(i);
2428
2429 parameter_symbolt new_symbol;
2430
2431 new_symbol.name =
2432 id2string(identifier_with_type) + "::" + base_name;
2433 new_symbol.base_name = base_name;
2434 new_symbol.location = f_op.source_location();
2435 new_symbol.type = parameters[i].type();
2436 new_symbol.is_parameter = true;
2437 new_symbol.is_lvalue = true;
2438 new_symbol.mode = ID_C;
2439
2440 parameters[i].set_identifier(new_symbol.name);
2441 parameters[i].set_base_name(new_symbol.base_name);
2442
2443 symbol_table.add(new_symbol);
2444 }
2445
2446 symbolt new_symbol{
2447 identifier_with_type, gcc_polymorphic->type(), ID_C};
2448 new_symbol.base_name = identifier_with_type;
2449 new_symbol.location = f_op.source_location();
2450 code_blockt implementation =
2451 instantiate_gcc_polymorphic_builtin(identifier, *gcc_polymorphic);
2452 typet parent_return_type = return_type;
2453 return_type = to_code_type(gcc_polymorphic->type()).return_type();
2454 typecheck_code(implementation);
2455 return_type = parent_return_type;
2456 new_symbol.value = implementation;
2457
2458 symbol_table.add(new_symbol);
2459 }
2460
2461 f_op = std::move(*gcc_polymorphic);
2462 }
2463 else
2464 {
2465 // This is an undeclared function that's not a builtin.
2466 // Let's just add it.
2467 // We do a bit of return-type guessing, but just a bit.
2468 typet guessed_return_type = signed_int_type();
2469
2470 // The following isn't really right and sound, but there
2471 // are too many idiots out there who use malloc and the like
2472 // without the right header file.
2473 if(identifier=="malloc" ||
2474 identifier=="realloc" ||
2475 identifier=="reallocf" ||
2476 identifier=="valloc")
2477 {
2478 guessed_return_type = pointer_type(void_type()); // void *
2479 }
2480
2481 symbolt new_symbol{
2482 identifier, code_typet({}, guessed_return_type), mode};
2483 new_symbol.base_name=identifier;
2484 new_symbol.location=expr.source_location();
2485 new_symbol.type.set(ID_C_incomplete, true);
2486
2487 // TODO: should also guess some argument types
2488
2489 symbolt *symbol_ptr;
2490 move_symbol(new_symbol, symbol_ptr);
2491
2492 // We increase the verbosity level of the warning
2493 // for gcc/clang __builtin_ functions, since there are too many.
2494 if(identifier.starts_with("__builtin_"))
2495 {
2497 debug() << "builtin '" << identifier << "' is unknown" << eom;
2498 }
2499 else
2500 {
2502 warning() << "function '" << identifier << "' is not declared" << eom;
2503 }
2504 }
2505 }
2506 }
2507
2508 // typecheck it now
2509 typecheck_expr(f_op);
2510
2511 const typet f_op_type = f_op.type();
2512
2513 if(f_op_type.id() == ID_mathematical_function)
2514 {
2515 const auto &mathematical_function_type =
2517
2518 // check number of arguments
2519 if(expr.arguments().size() != mathematical_function_type.domain().size())
2520 {
2522 error() << "expected " << mathematical_function_type.domain().size()
2523 << " arguments but got " << expr.arguments().size() << eom;
2524 throw 0;
2525 }
2526
2527 // check the types of the arguments
2528 for(auto &p :
2529 make_range(expr.arguments()).zip(mathematical_function_type.domain()))
2530 {
2531 if(p.first.type() != p.second)
2532 {
2533 error().source_location = p.first.source_location();
2534 error() << "expected argument of type " << to_string(p.second)
2535 << " but got " << to_string(p.first.type()) << eom;
2536 throw 0;
2537 }
2538 }
2539
2540 function_application_exprt function_application(f_op, expr.arguments());
2541
2542 function_application.add_source_location() = expr.source_location();
2543
2544 expr.swap(function_application);
2545 return;
2546 }
2547
2548 if(f_op_type.id()!=ID_pointer)
2549 {
2551 error() << "expected function/function pointer as argument but got '"
2552 << to_string(f_op_type) << "'" << eom;
2553 throw 0;
2554 }
2555
2556 // do implicit dereference
2557 if(f_op.id() == ID_address_of && f_op.get_bool(ID_C_implicit))
2558 {
2559 f_op = to_address_of_expr(f_op).object();
2560 }
2561 else
2562 {
2563 dereference_exprt tmp{f_op};
2564 tmp.set(ID_C_implicit, true);
2565 tmp.add_source_location()=f_op.source_location();
2566 f_op.swap(tmp);
2567 }
2568
2569 if(f_op.type().id()!=ID_code)
2570 {
2572 error() << "expected code as argument" << eom;
2573 throw 0;
2574 }
2575
2576 const code_typet &code_type=to_code_type(f_op.type());
2577
2578 expr.type()=code_type.return_type();
2579
2580 exprt tmp=do_special_functions(expr);
2581
2582 if(tmp.is_not_nil())
2583 expr.swap(tmp);
2584 else
2586}
2587
2590{
2591 const exprt &f_op=expr.function();
2592 const source_locationt &source_location=expr.source_location();
2593
2594 // some built-in functions
2595 if(f_op.id()!=ID_symbol)
2596 return nil_exprt();
2597
2598 const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
2599
2600 if(identifier == CPROVER_PREFIX "pointer_equals")
2601 {
2602 if(expr.arguments().size() != 2)
2603 {
2605 error() << CPROVER_PREFIX "pointer_equals expects two operands; "
2606 << expr.arguments().size() << "provided." << eom;
2607 throw 0;
2608 }
2610 return nil_exprt();
2611 }
2612 else if(identifier == CPROVER_PREFIX "is_fresh")
2613 {
2614 if(expr.arguments().size() != 2)
2615 {
2617 error() << CPROVER_PREFIX "is_fresh expects two operands; "
2618 << expr.arguments().size() << "provided." << eom;
2619 throw 0;
2620 }
2622 return nil_exprt();
2623 }
2624 else if(identifier == CPROVER_PREFIX "obeys_contract")
2625 {
2627 // returning nil leaves the call expression in place
2628 return nil_exprt();
2629 }
2630 else if(identifier == CPROVER_PREFIX "pointer_in_range_dfcc")
2631 {
2632 // same as pointer_in_range with experimental support for DFCC contracts
2633 // -- do not use
2634 if(expr.arguments().size() != 3)
2635 {
2637 CPROVER_PREFIX "pointer_in_range_dfcc expects three arguments",
2638 expr.source_location()};
2639 }
2640
2641 for(const auto &arg : expr.arguments())
2642 {
2643 if(arg.type().id() != ID_pointer)
2644 {
2647 "pointer_in_range_dfcc expects pointer-typed arguments",
2648 arg.source_location()};
2649 }
2650 }
2651 return nil_exprt();
2652 }
2653 else if(identifier == CPROVER_PREFIX "same_object")
2654 {
2655 if(expr.arguments().size()!=2)
2656 {
2658 error() << "same_object expects two operands" << eom;
2659 throw 0;
2660 }
2661
2663
2664 exprt same_object_expr=
2665 same_object(expr.arguments()[0], expr.arguments()[1]);
2666 same_object_expr.add_source_location()=source_location;
2667
2668 return same_object_expr;
2669 }
2670 else if(identifier==CPROVER_PREFIX "get_must")
2671 {
2672 if(expr.arguments().size()!=2)
2673 {
2675 error() << "get_must expects two operands" << eom;
2676 throw 0;
2677 }
2678
2680
2681 binary_predicate_exprt get_must_expr(
2682 expr.arguments()[0], ID_get_must, expr.arguments()[1]);
2683 get_must_expr.add_source_location()=source_location;
2684
2685 return std::move(get_must_expr);
2686 }
2687 else if(identifier==CPROVER_PREFIX "get_may")
2688 {
2689 if(expr.arguments().size()!=2)
2690 {
2692 error() << "get_may expects two operands" << eom;
2693 throw 0;
2694 }
2695
2697
2698 binary_predicate_exprt get_may_expr(
2699 expr.arguments()[0], ID_get_may, expr.arguments()[1]);
2700 get_may_expr.add_source_location()=source_location;
2701
2702 return std::move(get_may_expr);
2703 }
2704 else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
2705 {
2706 if(expr.arguments().size()!=1)
2707 {
2709 error() << "is_invalid_pointer expects one operand" << eom;
2710 throw 0;
2711 }
2712
2714
2715 exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
2716 same_object_expr.add_source_location()=source_location;
2717
2718 return same_object_expr;
2719 }
2720 else if(identifier==CPROVER_PREFIX "buffer_size")
2721 {
2722 if(expr.arguments().size()!=1)
2723 {
2725 error() << "buffer_size expects one operand" << eom;
2726 throw 0;
2727 }
2728
2730
2731 exprt buffer_size_expr("buffer_size", size_type());
2732 buffer_size_expr.operands()=expr.arguments();
2733 buffer_size_expr.add_source_location()=source_location;
2734
2735 return buffer_size_expr;
2736 }
2737 else if(identifier == CPROVER_PREFIX "is_list")
2738 {
2739 // experimental feature for CHC encodings -- do not use
2740 if(expr.arguments().size() != 1)
2741 {
2743 error() << "is_list expects one operand" << eom;
2744 throw 0;
2745 }
2746
2748
2749 if(
2750 expr.arguments()[0].type().id() != ID_pointer ||
2751 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2752 ID_struct_tag)
2753 {
2754 error().source_location = expr.arguments()[0].source_location();
2755 error() << "is_list expects a struct-pointer operand" << eom;
2756 throw 0;
2757 }
2758
2759 predicate_exprt is_list_expr("is_list");
2760 is_list_expr.operands() = expr.arguments();
2761 is_list_expr.add_source_location() = source_location;
2762
2763 return std::move(is_list_expr);
2764 }
2765 else if(identifier == CPROVER_PREFIX "is_dll")
2766 {
2767 // experimental feature for CHC encodings -- do not use
2768 if(expr.arguments().size() != 1)
2769 {
2771 error() << "is_dll expects one operand" << eom;
2772 throw 0;
2773 }
2774
2776
2777 if(
2778 expr.arguments()[0].type().id() != ID_pointer ||
2779 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2780 ID_struct_tag)
2781 {
2782 error().source_location = expr.arguments()[0].source_location();
2783 error() << "is_dll expects a struct-pointer operand" << eom;
2784 throw 0;
2785 }
2786
2787 predicate_exprt is_dll_expr("is_dll");
2788 is_dll_expr.operands() = expr.arguments();
2789 is_dll_expr.add_source_location() = source_location;
2790
2791 return std::move(is_dll_expr);
2792 }
2793 else if(identifier == CPROVER_PREFIX "is_cyclic_dll")
2794 {
2795 // experimental feature for CHC encodings -- do not use
2796 if(expr.arguments().size() != 1)
2797 {
2799 error() << "is_cyclic_dll expects one operand" << eom;
2800 throw 0;
2801 }
2802
2804
2805 if(
2806 expr.arguments()[0].type().id() != ID_pointer ||
2807 to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
2808 ID_struct_tag)
2809 {
2810 error().source_location = expr.arguments()[0].source_location();
2811 error() << "is_cyclic_dll expects a struct-pointer operand" << eom;
2812 throw 0;
2813 }
2814
2815 predicate_exprt is_cyclic_dll_expr("is_cyclic_dll");
2816 is_cyclic_dll_expr.operands() = expr.arguments();
2817 is_cyclic_dll_expr.add_source_location() = source_location;
2818
2819 return std::move(is_cyclic_dll_expr);
2820 }
2821 else if(identifier == CPROVER_PREFIX "is_sentinel_dll")
2822 {
2823 // experimental feature for CHC encodings -- do not use
2824 if(expr.arguments().size() != 2 && expr.arguments().size() != 3)
2825 {
2827 error() << "is_sentinel_dll expects two or three operands" << eom;
2828 throw 0;
2829 }
2830
2832
2833 exprt::operandst args_no_cast;
2834 args_no_cast.reserve(expr.arguments().size());
2835 for(const auto &argument : expr.arguments())
2836 {
2837 args_no_cast.push_back(skip_typecast(argument));
2838 if(
2839 args_no_cast.back().type().id() != ID_pointer ||
2840 to_pointer_type(args_no_cast.back().type()).base_type().id() !=
2841 ID_struct_tag)
2842 {
2843 error().source_location = expr.arguments()[0].source_location();
2844 error() << "is_sentinel_dll_node expects struct-pointer operands"
2845 << eom;
2846 throw 0;
2847 }
2848 }
2849
2850 predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
2851 is_sentinel_dll_expr.operands() = args_no_cast;
2852 is_sentinel_dll_expr.add_source_location() = source_location;
2853
2854 return std::move(is_sentinel_dll_expr);
2855 }
2856 else if(identifier == CPROVER_PREFIX "is_cstring")
2857 {
2858 // experimental feature for CHC encodings -- do not use
2859 if(expr.arguments().size() != 1)
2860 {
2862 error() << "is_cstring expects one operand" << eom;
2863 throw 0;
2864 }
2865
2867
2868 if(expr.arguments()[0].type().id() != ID_pointer)
2869 {
2870 error().source_location = expr.arguments()[0].source_location();
2871 error() << "is_cstring expects a pointer operand" << eom;
2872 throw 0;
2873 }
2874
2875 is_cstring_exprt is_cstring_expr(expr.arguments()[0]);
2876 is_cstring_expr.add_source_location() = source_location;
2877
2878 return std::move(is_cstring_expr);
2879 }
2880 else if(identifier == CPROVER_PREFIX "cstrlen")
2881 {
2882 // experimental feature for CHC encodings -- do not use
2883 if(expr.arguments().size() != 1)
2884 {
2886 error() << "cstrlen expects one operand" << eom;
2887 throw 0;
2888 }
2889
2891
2892 if(expr.arguments()[0].type().id() != ID_pointer)
2893 {
2894 error().source_location = expr.arguments()[0].source_location();
2895 error() << "cstrlen expects a pointer operand" << eom;
2896 throw 0;
2897 }
2898
2899 cstrlen_exprt cstrlen_expr(expr.arguments()[0], size_type());
2900 cstrlen_expr.add_source_location() = source_location;
2901
2902 return std::move(cstrlen_expr);
2903 }
2904 else if(identifier==CPROVER_PREFIX "is_zero_string")
2905 {
2906 if(expr.arguments().size()!=1)
2907 {
2909 error() << "is_zero_string expects one operand" << eom;
2910 throw 0;
2911 }
2912
2914
2915 unary_exprt is_zero_string_expr(
2916 "is_zero_string", expr.arguments()[0], c_bool_type());
2917 is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
2918 is_zero_string_expr.add_source_location()=source_location;
2919
2920 return std::move(is_zero_string_expr);
2921 }
2922 else if(identifier==CPROVER_PREFIX "zero_string_length")
2923 {
2924 if(expr.arguments().size()!=1)
2925 {
2927 error() << "zero_string_length expects one operand" << eom;
2928 throw 0;
2929 }
2930
2932
2933 exprt zero_string_length_expr("zero_string_length", size_type());
2934 zero_string_length_expr.operands()=expr.arguments();
2935 zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
2936 zero_string_length_expr.add_source_location()=source_location;
2937
2938 return zero_string_length_expr;
2939 }
2940 else if(identifier==CPROVER_PREFIX "DYNAMIC_OBJECT")
2941 {
2942 if(expr.arguments().size()!=1)
2943 {
2945 error() << "dynamic_object expects one argument" << eom;
2946 throw 0;
2947 }
2948
2950
2951 exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
2952 is_dynamic_object_expr.add_source_location() = source_location;
2953
2954 return is_dynamic_object_expr;
2955 }
2956 else if(identifier == CPROVER_PREFIX "LIVE_OBJECT")
2957 {
2958 if(expr.arguments().size() != 1)
2959 {
2961 error() << "live_object expects one argument" << eom;
2962 throw 0;
2963 }
2964
2966
2967 exprt live_object_expr = live_object_exprt(expr.arguments()[0]);
2968 live_object_expr.add_source_location() = source_location;
2969
2970 return live_object_expr;
2971 }
2972 else if(identifier == CPROVER_PREFIX "pointer_in_range")
2973 {
2974 if(expr.arguments().size() != 3)
2975 {
2977 error() << "pointer_in_range expects three arguments" << eom;
2978 throw 0;
2979 }
2980
2982
2983 exprt pointer_in_range_expr = pointer_in_range_exprt(
2984 expr.arguments()[0], expr.arguments()[1], expr.arguments()[2]);
2985 pointer_in_range_expr.add_source_location() = source_location;
2986
2987 return pointer_in_range_expr;
2988 }
2989 else if(identifier == CPROVER_PREFIX "WRITEABLE_OBJECT")
2990 {
2991 if(expr.arguments().size() != 1)
2992 {
2994 error() << "writeable_object expects one argument" << eom;
2995 throw 0;
2996 }
2997
2999
3000 exprt writeable_object_expr = writeable_object_exprt(expr.arguments()[0]);
3001 writeable_object_expr.add_source_location() = source_location;
3002
3003 return writeable_object_expr;
3004 }
3005 else if(identifier == CPROVER_PREFIX "separate")
3006 {
3007 // experimental feature for CHC encodings -- do not use
3008 if(expr.arguments().size() < 2)
3009 {
3011 error() << "separate expects two or more arguments" << eom;
3012 throw 0;
3013 }
3014
3016
3017 exprt separate_expr = separate_exprt(expr.arguments());
3018 separate_expr.add_source_location() = source_location;
3019
3020 return separate_expr;
3021 }
3022 else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
3023 {
3024 if(expr.arguments().size()!=1)
3025 {
3027 error() << "pointer_offset expects one argument" << eom;
3028 throw 0;
3029 }
3030
3032
3033 exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
3034 pointer_offset_expr.add_source_location()=source_location;
3035
3036 return typecast_exprt::conditional_cast(pointer_offset_expr, expr.type());
3037 }
3038 else if(identifier == CPROVER_PREFIX "OBJECT_SIZE")
3039 {
3040 if(expr.arguments().size() != 1)
3041 {
3043 error() << "object_size expects one operand" << eom;
3044 throw 0;
3045 }
3046
3048
3049 object_size_exprt object_size_expr(expr.arguments()[0], size_type());
3050 object_size_expr.add_source_location() = source_location;
3051
3052 return std::move(object_size_expr);
3053 }
3054 else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
3055 {
3056 if(expr.arguments().size()!=1)
3057 {
3059 error() << "pointer_object expects one argument" << eom;
3060 throw 0;
3061 }
3062
3064
3065 exprt pointer_object_expr = pointer_object(expr.arguments().front());
3066 pointer_object_expr.add_source_location() = source_location;
3067
3068 return typecast_exprt::conditional_cast(pointer_object_expr, expr.type());
3069 }
3070 else if(identifier=="__builtin_bswap16" ||
3071 identifier=="__builtin_bswap32" ||
3072 identifier=="__builtin_bswap64")
3073 {
3074 if(expr.arguments().size()!=1)
3075 {
3077 error() << identifier << " expects one operand" << eom;
3078 throw 0;
3079 }
3080
3082
3083 // these are hard-wired to 8 bits according to the gcc manual
3084 bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
3085 bswap_expr.add_source_location()=source_location;
3086
3087 return std::move(bswap_expr);
3088 }
3089 else if(
3090 identifier == "__builtin_rotateleft8" ||
3091 identifier == "__builtin_rotateleft16" ||
3092 identifier == "__builtin_rotateleft32" ||
3093 identifier == "__builtin_rotateleft64" ||
3094 identifier == "__builtin_rotateright8" ||
3095 identifier == "__builtin_rotateright16" ||
3096 identifier == "__builtin_rotateright32" ||
3097 identifier == "__builtin_rotateright64")
3098 {
3099 // clang only
3100 if(expr.arguments().size() != 2)
3101 {
3103 error() << identifier << " expects two operands" << eom;
3104 throw 0;
3105 }
3106
3108
3109 irep_idt id = (identifier == "__builtin_rotateleft8" ||
3110 identifier == "__builtin_rotateleft16" ||
3111 identifier == "__builtin_rotateleft32" ||
3112 identifier == "__builtin_rotateleft64")
3113 ? ID_rol
3114 : ID_ror;
3115
3116 shift_exprt rotate_expr(expr.arguments()[0], id, expr.arguments()[1]);
3117 rotate_expr.add_source_location() = source_location;
3118
3119 return std::move(rotate_expr);
3120 }
3121 else if(identifier=="__builtin_nontemporal_load")
3122 {
3123 if(expr.arguments().size()!=1)
3124 {
3126 error() << identifier << " expects one operand" << eom;
3127 throw 0;
3128 }
3129
3131
3132 // these return the subtype of the argument
3133 exprt &ptr_arg=expr.arguments().front();
3134
3135 if(ptr_arg.type().id()!=ID_pointer)
3136 {
3138 error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
3139 throw 0;
3140 }
3141
3142 expr.type() = to_pointer_type(expr.arguments().front().type()).base_type();
3143
3144 return expr;
3145 }
3146 else if(
3147 identifier == "__builtin_fpclassify" ||
3148 identifier == CPROVER_PREFIX "fpclassify")
3149 {
3150 if(expr.arguments().size() != 6)
3151 {
3153 error() << identifier << " expects six arguments" << eom;
3154 throw 0;
3155 }
3156
3158
3159 // This gets 5 integers followed by a float or double.
3160 // The five integers are the return values for the cases
3161 // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
3162 // gcc expects this to be able to produce compile-time constants.
3163
3164 const exprt &fp_value = expr.arguments()[5];
3165
3166 if(fp_value.type().id() != ID_floatbv)
3167 {
3168 error().source_location = fp_value.source_location();
3169 error() << "non-floating-point argument for " << identifier << eom;
3170 throw 0;
3171 }
3172
3173 const auto &floatbv_type = to_floatbv_type(fp_value.type());
3174
3175 const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();
3176
3177 const auto &arguments = expr.arguments();
3178
3179 return if_exprt(
3180 isnan_exprt(fp_value),
3181 arguments[0],
3182 if_exprt(
3183 isinf_exprt(fp_value),
3184 arguments[1],
3185 if_exprt(
3186 isnormal_exprt(fp_value),
3187 arguments[2],
3188 if_exprt(
3189 ieee_float_equal_exprt(fp_value, zero),
3190 arguments[4],
3191 arguments[3])))); // subnormal
3192 }
3193 else if(identifier==CPROVER_PREFIX "isnanf" ||
3194 identifier==CPROVER_PREFIX "isnand" ||
3195 identifier==CPROVER_PREFIX "isnanld" ||
3196 identifier=="__builtin_isnan")
3197 {
3198 if(expr.arguments().size()!=1)
3199 {
3201 error() << "isnan expects one operand" << eom;
3202 throw 0;
3203 }
3204
3206
3207 isnan_exprt isnan_expr(expr.arguments().front());
3208 isnan_expr.add_source_location()=source_location;
3209
3210 return typecast_exprt::conditional_cast(isnan_expr, expr.type());
3211 }
3212 else if(identifier==CPROVER_PREFIX "isfinitef" ||
3213 identifier==CPROVER_PREFIX "isfinited" ||
3214 identifier==CPROVER_PREFIX "isfiniteld")
3215 {
3216 if(expr.arguments().size()!=1)
3217 {
3219 error() << "isfinite expects one operand" << eom;
3220 throw 0;
3221 }
3222
3224
3225 isfinite_exprt isfinite_expr(expr.arguments().front());
3226 isfinite_expr.add_source_location()=source_location;
3227
3228 return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
3229 }
3230 else if(identifier==CPROVER_PREFIX "inf" ||
3231 identifier=="__builtin_inf")
3232 {
3233 constant_exprt inf_expr=
3236 inf_expr.add_source_location()=source_location;
3237
3238 return std::move(inf_expr);
3239 }
3240 else if(identifier==CPROVER_PREFIX "inff")
3241 {
3242 constant_exprt inff_expr=
3245 inff_expr.add_source_location()=source_location;
3246
3247 return std::move(inff_expr);
3248 }
3249 else if(identifier==CPROVER_PREFIX "infl")
3250 {
3252 constant_exprt infl_expr=
3254 infl_expr.add_source_location()=source_location;
3255
3256 return std::move(infl_expr);
3257 }
3258 else if(
3259 identifier == CPROVER_PREFIX "round_to_integralf" ||
3260 identifier == CPROVER_PREFIX "round_to_integrald" ||
3261 identifier == CPROVER_PREFIX "round_to_integralld")
3262 {
3263 if(expr.arguments().size() != 2)
3264 {
3266 error() << identifier << " expects two arguments" << eom;
3267 throw 0;
3268 }
3269
3270 auto round_to_integral_expr =
3272 round_to_integral_expr.add_source_location() = source_location;
3273
3274 return std::move(round_to_integral_expr);
3275 }
3276 else if(
3277 identifier == CPROVER_PREFIX "abs" || identifier == CPROVER_PREFIX "labs" ||
3278 identifier == CPROVER_PREFIX "llabs" ||
3279 identifier == CPROVER_PREFIX "imaxabs" ||
3280 identifier == CPROVER_PREFIX "fabs" ||
3281 identifier == CPROVER_PREFIX "fabsf" ||
3282 identifier == CPROVER_PREFIX "fabsl")
3283 {
3284 if(expr.arguments().size()!=1)
3285 {
3287 error() << "abs-functions expect one operand" << eom;
3288 throw 0;
3289 }
3290
3292
3293 abs_exprt abs_expr(expr.arguments().front());
3294 abs_expr.add_source_location()=source_location;
3295
3296 return std::move(abs_expr);
3297 }
3298 else if(
3299 identifier == CPROVER_PREFIX "fmod" ||
3300 identifier == CPROVER_PREFIX "fmodf" ||
3301 identifier == CPROVER_PREFIX "fmodl")
3302 {
3303 if(expr.arguments().size() != 2)
3304 {
3306 error() << "fmod-functions expect two operands" << eom;
3307 throw 0;
3308 }
3309
3311
3312 // Note that the semantics differ from the
3313 // "floating point remainder" operation as defined by IEEE.
3314 // Note that these do not take a rounding mode.
3315 binary_exprt fmod_expr(
3316 expr.arguments()[0], ID_floatbv_mod, expr.arguments()[1]);
3317
3318 fmod_expr.add_source_location() = source_location;
3319
3320 return std::move(fmod_expr);
3321 }
3322 else if(
3323 identifier == CPROVER_PREFIX "remainder" ||
3324 identifier == CPROVER_PREFIX "remainderf" ||
3325 identifier == CPROVER_PREFIX "remainderl")
3326 {
3327 if(expr.arguments().size() != 2)
3328 {
3330 error() << "remainder-functions expect two operands" << eom;
3331 throw 0;
3332 }
3333
3335
3336 // The semantics of these functions is meant to match the
3337 // "floating point remainder" operation as defined by IEEE.
3338 // Note that these do not take a rounding mode.
3339 binary_exprt floatbv_rem_expr(
3340 expr.arguments()[0], ID_floatbv_rem, expr.arguments()[1]);
3341
3342 floatbv_rem_expr.add_source_location() = source_location;
3343
3344 return std::move(floatbv_rem_expr);
3345 }
3346 else if(identifier==CPROVER_PREFIX "allocate")
3347 {
3348 if(expr.arguments().size()!=2)
3349 {
3351 error() << "allocate expects two operands" << eom;
3352 throw 0;
3353 }
3354
3356
3357 side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
3358 malloc_expr.operands()=expr.arguments();
3359
3360 return std::move(malloc_expr);
3361 }
3362 else if(
3363 (identifier == CPROVER_PREFIX "old") ||
3364 (identifier == CPROVER_PREFIX "loop_entry"))
3365 {
3366 if(expr.arguments().size() != 1)
3367 {
3369 error() << identifier << " expects one operand" << eom;
3370 throw 0;
3371 }
3372
3373 const auto &param_id = expr.arguments().front().id();
3374 if(!(param_id == ID_dereference || param_id == ID_member ||
3375 param_id == ID_symbol || param_id == ID_ptrmember ||
3376 param_id == ID_constant || param_id == ID_typecast ||
3377 param_id == ID_index))
3378 {
3380 error() << "Tracking history of " << param_id
3381 << " expressions is not supported yet." << eom;
3382 throw 0;
3383 }
3384
3385 irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry;
3386
3387 history_exprt old_expr(expr.arguments()[0], id);
3388 old_expr.add_source_location() = source_location;
3389
3390 return std::move(old_expr);
3391 }
3392 else if(identifier==CPROVER_PREFIX "isinff" ||
3393 identifier==CPROVER_PREFIX "isinfd" ||
3394 identifier==CPROVER_PREFIX "isinfld" ||
3395 identifier=="__builtin_isinf")
3396 {
3397 if(expr.arguments().size()!=1)
3398 {
3400 error() << identifier << " expects one operand" << eom;
3401 throw 0;
3402 }
3403
3405
3406 const exprt &fp_value = expr.arguments().front();
3407
3408 if(fp_value.type().id() != ID_floatbv)
3409 {
3410 error().source_location = fp_value.source_location();
3411 error() << "non-floating-point argument for " << identifier << eom;
3412 throw 0;
3413 }
3414
3415 isinf_exprt isinf_expr(expr.arguments().front());
3416 isinf_expr.add_source_location()=source_location;
3417
3418 return typecast_exprt::conditional_cast(isinf_expr, expr.type());
3419 }
3420 else if(identifier == "__builtin_isinf_sign")
3421 {
3422 if(expr.arguments().size() != 1)
3423 {
3425 error() << identifier << " expects one operand" << eom;
3426 throw 0;
3427 }
3428
3430
3431 // returns 1 for +inf and -1 for -inf, and 0 otherwise
3432
3433 const exprt &fp_value = expr.arguments().front();
3434
3435 if(fp_value.type().id() != ID_floatbv)
3436 {
3437 error().source_location = fp_value.source_location();
3438 error() << "non-floating-point argument for " << identifier << eom;
3439 throw 0;
3440 }
3441
3442 isinf_exprt isinf_expr(fp_value);
3443 isinf_expr.add_source_location() = source_location;
3444
3445 return if_exprt(
3446 isinf_exprt(fp_value),
3447 if_exprt(
3448 sign_exprt(fp_value),
3449 from_integer(-1, expr.type()),
3450 from_integer(1, expr.type())),
3451 from_integer(0, expr.type()));
3452 }
3453 else if(identifier == CPROVER_PREFIX "isnormalf" ||
3454 identifier == CPROVER_PREFIX "isnormald" ||
3455 identifier == CPROVER_PREFIX "isnormalld" ||
3456 identifier == "__builtin_isnormal")
3457 {
3458 if(expr.arguments().size()!=1)
3459 {
3461 error() << identifier << " expects one operand" << eom;
3462 throw 0;
3463 }
3464
3466
3467 const exprt &fp_value = expr.arguments()[0];
3468
3469 if(fp_value.type().id() != ID_floatbv)
3470 {
3471 error().source_location = fp_value.source_location();
3472 error() << "non-floating-point argument for " << identifier << eom;
3473 throw 0;
3474 }
3475
3476 isnormal_exprt isnormal_expr(expr.arguments().front());
3477 isnormal_expr.add_source_location()=source_location;
3478
3479 return typecast_exprt::conditional_cast(isnormal_expr, expr.type());
3480 }
3481 else if(identifier==CPROVER_PREFIX "signf" ||
3482 identifier==CPROVER_PREFIX "signd" ||
3483 identifier==CPROVER_PREFIX "signld" ||
3484 identifier=="__builtin_signbit" ||
3485 identifier=="__builtin_signbitf" ||
3486 identifier=="__builtin_signbitl")
3487 {
3488 if(expr.arguments().size()!=1)
3489 {
3491 error() << identifier << " expects one operand" << eom;
3492 throw 0;
3493 }
3494
3496
3497 sign_exprt sign_expr(expr.arguments().front());
3498 sign_expr.add_source_location()=source_location;
3499
3500 return typecast_exprt::conditional_cast(sign_expr, expr.type());
3501 }
3502 else if(identifier=="__builtin_popcount" ||
3503 identifier=="__builtin_popcountl" ||
3504 identifier=="__builtin_popcountll" ||
3505 identifier=="__popcnt16" ||
3506 identifier=="__popcnt" ||
3507 identifier=="__popcnt64")
3508 {
3509 if(expr.arguments().size()!=1)
3510 {
3512 error() << identifier << " expects one operand" << eom;
3513 throw 0;
3514 }
3515
3517
3518 popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
3519 popcount_expr.add_source_location()=source_location;
3520
3521 return std::move(popcount_expr);
3522 }
3523 else if(
3524 identifier == "__builtin_clz" || identifier == "__builtin_clzl" ||
3525 identifier == "__builtin_clzll" || identifier == "__lzcnt16" ||
3526 identifier == "__lzcnt" || identifier == "__lzcnt64")
3527 {
3528 if(expr.arguments().size() != 1)
3529 {
3531 error() << identifier << " expects one operand" << eom;
3532 throw 0;
3533 }
3534
3536
3538 expr.arguments().front(), identifier.starts_with("__lzcnt"), expr.type()};
3539 clz.add_source_location() = source_location;
3540
3541 return std::move(clz);
3542 }
3543 else if(
3544 identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" ||
3545 identifier == "__builtin_ctzll")
3546 {
3547 if(expr.arguments().size() != 1)
3548 {
3550 error() << identifier << " expects one operand" << eom;
3551 throw 0;
3552 }
3553
3555
3557 expr.arguments().front(), false, expr.type()};
3558 ctz.add_source_location() = source_location;
3559
3560 return std::move(ctz);
3561 }
3562 else if(
3563 identifier == "__builtin_ffs" || identifier == "__builtin_ffsl" ||
3564 identifier == "__builtin_ffsll")
3565 {
3566 if(expr.arguments().size() != 1)
3567 {
3569 error() << identifier << " expects one operand" << eom;
3570 throw 0;
3571 }
3572
3574
3575 find_first_set_exprt ffs{expr.arguments().front(), expr.type()};
3576 ffs.add_source_location() = source_location;
3577
3578 return std::move(ffs);
3579 }
3580 else if(identifier=="__builtin_expect")
3581 {
3582 // This is a gcc extension to provide branch prediction.
3583 // We compile it away, but adding some IR instruction for
3584 // this would clearly be an option. Note that the type
3585 // of the return value is wired to "long", i.e.,
3586 // this may trigger a type conversion due to the signature
3587 // of this function.
3588 if(expr.arguments().size()!=2)
3589 {
3591 error() << "__builtin_expect expects two arguments" << eom;
3592 throw 0;
3593 }
3594
3596
3597 return typecast_exprt(expr.arguments()[0], expr.type());
3598 }
3599 else if(
3600 identifier == "__builtin_object_size" ||
3601 identifier == "__builtin_dynamic_object_size")
3602 {
3603 // These are gcc extensions to provide information about
3604 // object sizes at compile time
3605 // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
3606 // Our behavior is as if it was never possible to determine the object that
3607 // the pointer pointed to.
3608
3609 if(expr.arguments().size()!=2)
3610 {
3612 error() << "__builtin_object_size expects two arguments" << eom;
3613 throw 0;
3614 }
3615
3617
3618 make_constant(expr.arguments()[1]);
3619
3620 mp_integer arg1;
3621
3622 if(expr.arguments()[1].is_true())
3623 arg1=1;
3624 else if(expr.arguments()[1].is_false())
3625 arg1=0;
3626 else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1))
3627 {
3629 error() << "__builtin_object_size expects constant as second argument, "
3630 << "but got " << to_string(expr.arguments()[1]) << eom;
3631 throw 0;
3632 }
3633
3634 exprt tmp;
3635
3636 // the following means "don't know"
3637 if(arg1==0 || arg1==1)
3638 {
3639 tmp=from_integer(-1, size_type());
3641 }
3642 else
3643 {
3644 tmp=from_integer(0, size_type());
3646 }
3647
3648 return tmp;
3649 }
3650 else if(identifier=="__builtin_choose_expr")
3651 {
3652 // this is a gcc extension similar to ?:
3653 if(expr.arguments().size()!=3)
3654 {
3656 error() << "__builtin_choose_expr expects three arguments" << eom;
3657 throw 0;
3658 }
3659
3661
3662 exprt arg0 =
3664 make_constant(arg0);
3665
3666 if(arg0.is_true())
3667 return expr.arguments()[1];
3668 else
3669 return expr.arguments()[2];
3670 }
3671 else if(identifier=="__builtin_constant_p")
3672 {
3673 // this is a gcc extension to tell whether the argument
3674 // is known to be a compile-time constant
3675 if(expr.arguments().size()!=1)
3676 {
3678 error() << "__builtin_constant_p expects one argument" << eom;
3679 throw 0;
3680 }
3681
3682 // do not typecheck the argument - it is never evaluated, and thus side
3683 // effects must not show up either
3684
3685 // try to produce constant
3686 exprt tmp1=expr.arguments().front();
3687 simplify(tmp1, *this);
3688
3689 bool is_constant=false;
3690
3691 // Need to do some special treatment for string literals,
3692 // which are (void *)&("lit"[0])
3693 if(
3694 tmp1.id() == ID_typecast &&
3695 to_typecast_expr(tmp1).op().id() == ID_address_of &&
3696 to_address_of_expr(to_typecast_expr(tmp1).op()).object().id() ==
3697 ID_index &&
3699 .array()
3700 .id() == ID_string_constant)
3701 {
3702 is_constant=true;
3703 }
3704 else
3705 is_constant=tmp1.is_constant();
3706
3707 exprt tmp2=from_integer(is_constant, expr.type());
3708 tmp2.add_source_location()=source_location;
3709
3710 return tmp2;
3711 }
3712 else if(identifier=="__builtin_classify_type")
3713 {
3714 // This is a gcc/clang extension that produces an integer
3715 // constant for the type of the argument expression.
3716 if(expr.arguments().size()!=1)
3717 {
3719 error() << "__builtin_classify_type expects one argument" << eom;
3720 throw 0;
3721 }
3722
3724
3725 exprt object=expr.arguments()[0];
3726
3727 // The value doesn't matter at all, we only care about the type.
3728 // Need to sync with typeclass.h.
3729 // use underlying type for bit fields
3730 const typet &type = object.type().id() == ID_c_bit_field
3731 ? to_c_bit_field_type(object.type()).underlying_type()
3732 : object.type();
3733
3734 unsigned type_number;
3735
3736 if(type.id() == ID_bool || type.id() == ID_c_bool)
3737 {
3738 // clang returns 4 for _Bool, gcc treats these as 'int'.
3739 type_number =
3740 config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG ? 4u : 1u;
3741 }
3742 else
3743 {
3744 type_number = type.id() == ID_empty ? 0u
3745 : (type.id() == ID_bool || type.id() == ID_c_bool) ? 4u
3746 : (type.id() == ID_pointer || type.id() == ID_array) ? 5u
3747 : type.id() == ID_floatbv ? 8u
3748 : (type.id() == ID_complex &&
3749 to_complex_type(type).subtype().id() == ID_floatbv)
3750 ? 9u
3751 : type.id() == ID_struct_tag ? 12u
3752 : type.id() == ID_union_tag
3753 ? 13u
3754 : 1u; // int, short, char, enum_tag
3755 }
3756
3757 exprt tmp=from_integer(type_number, expr.type());
3758 tmp.add_source_location()=source_location;
3759
3760 return tmp;
3761 }
3762 else if(
3763 identifier == "__builtin_add_overflow" ||
3764 identifier == "__builtin_sadd_overflow" ||
3765 identifier == "__builtin_saddl_overflow" ||
3766 identifier == "__builtin_saddll_overflow" ||
3767 identifier == "__builtin_uadd_overflow" ||
3768 identifier == "__builtin_uaddl_overflow" ||
3769 identifier == "__builtin_uaddll_overflow" ||
3770 identifier == "__builtin_add_overflow_p")
3771 {
3772 return typecheck_builtin_overflow(expr, ID_plus);
3773 }
3774 else if(
3775 identifier == "__builtin_sub_overflow" ||
3776 identifier == "__builtin_ssub_overflow" ||
3777 identifier == "__builtin_ssubl_overflow" ||
3778 identifier == "__builtin_ssubll_overflow" ||
3779 identifier == "__builtin_usub_overflow" ||
3780 identifier == "__builtin_usubl_overflow" ||
3781 identifier == "__builtin_usubll_overflow" ||
3782 identifier == "__builtin_sub_overflow_p")
3783 {
3784 return typecheck_builtin_overflow(expr, ID_minus);
3785 }
3786 else if(
3787 identifier == "__builtin_mul_overflow" ||
3788 identifier == "__builtin_smul_overflow" ||
3789 identifier == "__builtin_smull_overflow" ||
3790 identifier == "__builtin_smulll_overflow" ||
3791 identifier == "__builtin_umul_overflow" ||
3792 identifier == "__builtin_umull_overflow" ||
3793 identifier == "__builtin_umulll_overflow" ||
3794 identifier == "__builtin_mul_overflow_p")
3795 {
3796 return typecheck_builtin_overflow(expr, ID_mult);
3797 }
3798 else if(
3799 identifier == "__builtin_bitreverse8" ||
3800 identifier == "__builtin_bitreverse16" ||
3801 identifier == "__builtin_bitreverse32" ||
3802 identifier == "__builtin_bitreverse64")
3803 {
3804 // clang only
3805 if(expr.arguments().size() != 1)
3806 {
3807 std::ostringstream error_message;
3808 error_message << "error: " << identifier << " expects one operand";
3810 error_message.str(), expr.source_location()};
3811 }
3812
3814
3815 bitreverse_exprt bitreverse{expr.arguments()[0]};
3816 bitreverse.add_source_location() = source_location;
3817
3818 return std::move(bitreverse);
3819 }
3820 else
3821 return nil_exprt();
3822 // NOLINTNEXTLINE(readability/fn_size)
3823}
3824
3827 const irep_idt &arith_op)
3828{
3829 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3830
3831 // check function signature
3832 if(expr.arguments().size() != 3)
3833 {
3834 std::ostringstream error_message;
3835 error_message << identifier << " takes exactly 3 arguments, but "
3836 << expr.arguments().size() << " were provided";
3838 error_message.str(), expr.source_location()};
3839 }
3840
3842
3843 auto lhs = expr.arguments()[0];
3844 auto rhs = expr.arguments()[1];
3845 auto result = expr.arguments()[2];
3846
3847 const bool is__p_variant = has_suffix(id2string(identifier), "_p");
3848
3849 {
3850 auto const raise_wrong_argument_error =
3851 [this, identifier](
3852 const exprt &wrong_argument, std::size_t argument_number, bool _p) {
3853 std::ostringstream error_message;
3854 error_message << "error: " << identifier << " has signature "
3855 << identifier << "(integral, integral, integral"
3856 << (_p ? "" : "*") << "), "
3857 << "but argument " << argument_number << " ("
3858 << expr2c(wrong_argument, *this) << ") has type `"
3859 << type2c(wrong_argument.type(), *this) << '`';
3861 error_message.str(), wrong_argument.source_location()};
3862 };
3863 for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3864 {
3865 auto const &argument = expr.arguments()[arg_index];
3866
3867 if(!is_signed_or_unsigned_bitvector(argument.type()))
3868 {
3869 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3870 }
3871 }
3872 if(
3873 !is__p_variant && (result.type().id() != ID_pointer ||
3875 to_pointer_type(result.type()).base_type())))
3876 {
3877 raise_wrong_argument_error(result, 3, is__p_variant);
3878 }
3879 }
3880
3881 return side_effect_expr_overflowt{arith_op,
3882 std::move(lhs),
3883 std::move(rhs),
3884 std::move(result),
3885 expr.source_location()};
3886}
3887
3890{
3891 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3892
3893 // check function signature
3894 if(expr.arguments().size() != 2)
3895 {
3896 std::ostringstream error_message;
3897 error_message << "error: " << identifier
3898 << " takes exactly two arguments, but "
3899 << expr.arguments().size() << " were provided";
3901 error_message.str(), expr.source_location()};
3902 }
3903
3904 exprt result;
3905 if(
3906 identifier == CPROVER_PREFIX "saturating_minus" ||
3907 identifier == "__builtin_elementwise_sub_sat")
3908 {
3909 result = saturating_minus_exprt{expr.arguments()[0], expr.arguments()[1]};
3910 }
3911 else if(
3912 identifier == CPROVER_PREFIX "saturating_plus" ||
3913 identifier == "__builtin_elementwise_add_sat")
3914 {
3915 result = saturating_plus_exprt{expr.arguments()[0], expr.arguments()[1]};
3916 }
3917 else
3919
3921 result.add_source_location() = expr.source_location();
3922
3923 return result;
3924}
3925
3930{
3931 const exprt &f_op=expr.function();
3932 const code_typet &code_type=to_code_type(f_op.type());
3933 exprt::operandst &arguments=expr.arguments();
3934 const code_typet::parameterst &parameters = code_type.parameters();
3935
3936 // no. of arguments test
3937
3938 if(code_type.get_bool(ID_C_incomplete))
3939 {
3940 // can't check
3941 }
3942 else if(code_type.is_KnR())
3943 {
3944 // We are generous on KnR; any number is ok.
3945 // We will fill in missing ones with "nondet".
3946 for(std::size_t i = arguments.size(); i < parameters.size(); ++i)
3947 {
3948 arguments.push_back(
3949 side_effect_expr_nondett{parameters[i].type(), expr.source_location()});
3950 }
3951 }
3952 else if(code_type.has_ellipsis())
3953 {
3954 if(parameters.size() > arguments.size())
3955 {
3957 error() << "not enough function arguments" << eom;
3958 throw 0;
3959 }
3960 }
3961 else if(parameters.size() != arguments.size())
3962 {
3964 error() << "wrong number of function arguments: "
3965 << "expected " << parameters.size() << ", but got "
3966 << arguments.size() << eom;
3967 throw 0;
3968 }
3969
3970 for(std::size_t i=0; i<arguments.size(); i++)
3971 {
3972 exprt &op=arguments[i];
3973
3974 if(op.is_nil())
3975 {
3976 // ignore
3977 }
3978 else if(i < parameters.size())
3979 {
3980 const code_typet::parametert &parameter = parameters[i];
3981
3982 if(
3983 parameter.is_boolean() && op.id() == ID_side_effect &&
3984 op.get(ID_statement) == ID_assign && op.type().id() != ID_bool)
3985 {
3987 warning() << "assignment where Boolean argument is expected" << eom;
3988 }
3989
3990 implicit_typecast(op, parameter.type());
3991 }
3992 else
3993 {
3994 // don't know type, just do standard conversion
3995
3996 if(op.type().id() == ID_array)
3997 {
3998 auto dest_type = pointer_type(void_type());
3999 dest_type.base_type().set(ID_C_constant, true);
4000 implicit_typecast(op, dest_type);
4001 }
4002 }
4003 }
4004}
4005
4007{
4008 // nothing to do
4009}
4010
4012{
4013 exprt &operand = to_unary_expr(expr).op();
4014
4015 const typet &o_type = operand.type();
4016
4017 if(o_type.id()==ID_vector)
4018 {
4019 if(is_number(to_vector_type(o_type).element_type()))
4020 {
4021 // Vector arithmetic.
4022 expr.type()=operand.type();
4023 return;
4024 }
4025 }
4026
4028
4029 if(is_number(operand.type()))
4030 {
4031 expr.type()=operand.type();
4032 return;
4033 }
4034
4036 error() << "operator '" << expr.id() << "' not defined for type '"
4037 << to_string(operand.type()) << "'" << eom;
4038 throw 0;
4039}
4040
4042{
4044
4045 // This is not quite accurate: the standard says the result
4046 // should be of type 'int'.
4047 // We do 'bool' anyway to get more compact formulae. Eventually,
4048 // this should be achieved by means of simplification, and not
4049 // in the frontend.
4050 expr.type()=bool_typet();
4051}
4052
4054 const vector_typet &type0,
4055 const vector_typet &type1)
4056{
4057 // This is relatively restrictive!
4058
4059 // compare dimension
4060 const auto s0 = numeric_cast<mp_integer>(type0.size());
4061 const auto s1 = numeric_cast<mp_integer>(type1.size());
4062 if(!s0.has_value())
4063 return false;
4064 if(!s1.has_value())
4065 return false;
4066 if(*s0 != *s1)
4067 return false;
4068
4069 // compare subtype
4070 if(
4071 (type0.element_type().id() == ID_signedbv ||
4072 type0.element_type().id() == ID_unsignedbv) &&
4073 (type1.element_type().id() == ID_signedbv ||
4074 type1.element_type().id() == ID_unsignedbv) &&
4075 to_bitvector_type(type0.element_type()).get_width() ==
4076 to_bitvector_type(type1.element_type()).get_width())
4077 return true;
4078
4079 return type0.element_type() == type1.element_type();
4080}
4081
4083{
4084 auto &binary_expr = to_binary_expr(expr);
4085 exprt &op0 = binary_expr.op0();
4086 exprt &op1 = binary_expr.op1();
4087
4088 const typet o_type0 = op0.type();
4089 const typet o_type1 = op1.type();
4090
4091 if(o_type0.id()==ID_vector &&
4092 o_type1.id()==ID_vector)
4093 {
4094 if(
4096 to_vector_type(o_type0), to_vector_type(o_type1)) &&
4097 is_number(to_vector_type(o_type0).element_type()))
4098 {
4099 // Vector arithmetic has fairly strict typing rules, no promotion
4100 op1 = typecast_exprt::conditional_cast(op1, op0.type());
4101 expr.type()=op0.type();
4102 return;
4103 }
4104 }
4105 else if(
4106 o_type0.id() == ID_vector && o_type1.id() != ID_vector &&
4107 is_number(o_type1))
4108 {
4109 // convert op1 to the vector type
4110 op1 = typecast_exprt(op1, o_type0);
4111 expr.type() = o_type0;
4112 return;
4113 }
4114 else if(
4115 o_type0.id() != ID_vector && o_type1.id() == ID_vector &&
4116 is_number(o_type0))
4117 {
4118 // convert op0 to the vector type
4119 op0 = typecast_exprt(op0, o_type1);
4120 expr.type() = o_type1;
4121 return;
4122 }
4123
4124 if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
4125 {
4126 implicit_typecast(op1, o_type0);
4127 }
4128 else
4129 {
4130 // promote!
4132 }
4133
4134 const typet &type0 = op0.type();
4135 const typet &type1 = op1.type();
4136
4137 if(expr.id()==ID_plus || expr.id()==ID_minus ||
4138 expr.id()==ID_mult || expr.id()==ID_div)
4139 {
4140 if(type0.id()==ID_pointer || type1.id()==ID_pointer)
4141 {
4143 return;
4144 }
4145 else if(type0==type1)
4146 {
4147 if(is_number(type0))
4148 {
4149 expr.type()=type0;
4150 return;
4151 }
4152 }
4153 }
4154 else if(expr.id()==ID_mod)
4155 {
4156 if(type0==type1)
4157 {
4158 if(type0.id()==ID_signedbv || type0.id()==ID_unsignedbv)
4159 {
4160 expr.type()=type0;
4161 return;
4162 }
4163 }
4164 }
4165 else if(
4166 expr.id() == ID_bitand || expr.id() == ID_bitnand ||
4167 expr.id() == ID_bitxor || expr.id() == ID_bitor)
4168 {
4169 if(type0==type1)
4170 {
4171 if(is_number(type0))
4172 {
4173 expr.type()=type0;
4174 return;
4175 }
4176 else if(type0.id()==ID_bool)
4177 {
4178 if(expr.id()==ID_bitand)
4179 expr.id(ID_and);
4180 else if(expr.id() == ID_bitnand)
4181 expr.id(ID_nand);
4182 else if(expr.id()==ID_bitor)
4183 expr.id(ID_or);
4184 else if(expr.id()==ID_bitxor)
4185 expr.id(ID_xor);
4186 else
4188 expr.type()=type0;
4189 return;
4190 }
4191 }
4192 }
4193 else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus)
4194 {
4195 if(
4196 type0 == type1 &&
4197 (type0.id() == ID_signedbv || type0.id() == ID_unsignedbv))
4198 {
4199 expr.type() = type0;
4200 return;
4201 }
4202 }
4203
4205 error() << "operator '" << expr.id() << "' not defined for types '"
4206 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4207 << eom;
4208 throw 0;
4209}
4210
4212{
4213 PRECONDITION(expr.id() == ID_shl || expr.id() == ID_shr);
4214
4215 exprt &op0=expr.op0();
4216 exprt &op1=expr.op1();
4217
4218 const typet o_type0 = op0.type();
4219 const typet o_type1 = op1.type();
4220
4221 if(o_type0.id()==ID_vector &&
4222 o_type1.id()==ID_vector)
4223 {
4224 if(
4225 to_vector_type(o_type0).element_type() ==
4226 to_vector_type(o_type1).element_type() &&
4227 is_number(to_vector_type(o_type0).element_type()))
4228 {
4229 // {a0, a1, ..., an} >> {b0, b1, ..., bn} ==
4230 // {a0 >> b0, a1 >> b1, ..., an >> bn}
4231 // Fairly strict typing rules, no promotion
4232 expr.type()=op0.type();
4233 return;
4234 }
4235 }
4236
4237 if(
4238 o_type0.id() == ID_vector &&
4239 is_number(to_vector_type(o_type0).element_type()) && is_number(o_type1))
4240 {
4241 // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
4242 op1 = typecast_exprt(op1, o_type0);
4243 expr.type()=op0.type();
4244 return;
4245 }
4246
4247 // must do the promotions _separately_!
4250
4251 if(is_number(op0.type()) &&
4252 is_number(op1.type()))
4253 {
4254 expr.type()=op0.type();
4255
4256 if(expr.id()==ID_shr) // shifting operation depends on types
4257 {
4258 const typet &op0_type = op0.type();
4259
4260 if(op0_type.id()==ID_unsignedbv)
4261 {
4262 expr.id(ID_lshr);
4263 return;
4264 }
4265 else if(op0_type.id()==ID_signedbv)
4266 {
4267 expr.id(ID_ashr);
4268 return;
4269 }
4270 }
4271
4272 return;
4273 }
4274
4276 error() << "operator '" << expr.id() << "' not defined for types '"
4277 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4278 << eom;
4279 throw 0;
4280}
4281
4283{
4284 const typet &type=expr.type();
4285 PRECONDITION(type.id() == ID_pointer);
4286
4287 const typet &base_type = to_pointer_type(type).base_type();
4288
4289 if(
4290 base_type.id() == ID_struct_tag &&
4291 follow_tag(to_struct_tag_type(base_type)).is_incomplete())
4292 {
4294 error() << "pointer arithmetic with unknown object size" << eom;
4295 throw 0;
4296 }
4297 else if(
4298 base_type.id() == ID_union_tag &&
4299 follow_tag(to_union_tag_type(base_type)).is_incomplete())
4300 {
4302 error() << "pointer arithmetic with unknown object size" << eom;
4303 throw 0;
4304 }
4305 else if(
4306 base_type.id() == ID_empty &&
4308 {
4310 error() << "pointer arithmetic with unknown object size" << eom;
4311 throw 0;
4312 }
4313 else if(base_type.id() == ID_empty)
4314 {
4315 // This is a gcc extension.
4316 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
4318 expr.swap(tc);
4319 }
4320}
4321
4323{
4324 auto &binary_expr = to_binary_expr(expr);
4325 exprt &op0 = binary_expr.op0();
4326 exprt &op1 = binary_expr.op1();
4327
4328 const typet &type0 = op0.type();
4329 const typet &type1 = op1.type();
4330
4331 if(expr.id()==ID_minus ||
4332 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_minus))
4333 {
4334 if(type0.id()==ID_pointer &&
4335 type1.id()==ID_pointer)
4336 {
4337 if(type0 != type1)
4338 {
4340 "pointer subtraction over different types", expr.source_location()};
4341 }
4342 expr.type()=pointer_diff_type();
4345 return;
4346 }
4347
4348 if(type0.id()==ID_pointer &&
4349 (type1.id()==ID_bool ||
4350 type1.id()==ID_c_bool ||
4351 type1.id()==ID_unsignedbv ||
4352 type1.id()==ID_signedbv ||
4353 type1.id()==ID_c_bit_field ||
4354 type1.id()==ID_c_enum_tag))
4355 {
4357 make_index_type(op1);
4358 expr.type() = op0.type();
4359 return;
4360 }
4361 }
4362 else if(expr.id()==ID_plus ||
4363 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_plus))
4364 {
4365 exprt *p_op, *int_op;
4366
4367 if(type0.id()==ID_pointer)
4368 {
4369 p_op=&op0;
4370 int_op=&op1;
4371 }
4372 else if(type1.id()==ID_pointer)
4373 {
4374 p_op=&op1;
4375 int_op=&op0;
4376 }
4377 else
4378 {
4379 p_op=int_op=nullptr;
4381 }
4382
4383 const typet &int_op_type = int_op->type();
4384
4385 if(int_op_type.id()==ID_bool ||
4386 int_op_type.id()==ID_c_bool ||
4387 int_op_type.id()==ID_unsignedbv ||
4388 int_op_type.id()==ID_signedbv ||
4389 int_op_type.id()==ID_c_bit_field ||
4390 int_op_type.id()==ID_c_enum_tag)
4391 {
4393 make_index_type(*int_op);
4394 expr.type()=p_op->type();
4395 return;
4396 }
4397 }
4398
4399 irep_idt op_name;
4400
4401 if(expr.id()==ID_side_effect)
4402 op_name=to_side_effect_expr(expr).get_statement();
4403 else
4404 op_name=expr.id();
4405
4407 error() << "operator '" << op_name << "' not defined for types '"
4408 << to_string(type0) << "' and '" << to_string(type1) << "'" << eom;
4409 throw 0;
4410}
4411
4413{
4414 auto &binary_expr = to_binary_expr(expr);
4415 implicit_typecast_bool(binary_expr.op0());
4416 implicit_typecast_bool(binary_expr.op1());
4417
4418 // This is not quite accurate: the standard says the result
4419 // should be of type 'int'.
4420 // We do 'bool' anyway to get more compact formulae. Eventually,
4421 // this should be achieved by means of simplification, and not
4422 // in the frontend.
4423 expr.type()=bool_typet();
4424}
4425
4427 side_effect_exprt &expr)
4428{
4429 const irep_idt &statement=expr.get_statement();
4430
4431 auto &binary_expr = to_binary_expr(expr);
4432 exprt &op0 = binary_expr.op0();
4433 exprt &op1 = binary_expr.op1();
4434
4435 {
4436 const typet &type0=op0.type();
4437
4438 if(type0.id()==ID_empty)
4439 {
4441 error() << "cannot assign void" << eom;
4442 throw 0;
4443 }
4444
4445 if(!op0.get_bool(ID_C_lvalue))
4446 {
4448 error() << "assignment error: '" << to_string(op0) << "' not an lvalue"
4449 << eom;
4450 throw 0;
4451 }
4452
4453 if(type0.get_bool(ID_C_constant))
4454 {
4456 error() << "'" << to_string(op0) << "' is constant" << eom;
4457 throw 0;
4458 }
4459
4460 // refuse to assign arrays
4461 if(type0.id() == ID_array)
4462 {
4464 error() << "direct assignments to arrays not permitted" << eom;
4465 throw 0;
4466 }
4467 }
4468
4469 // Add a cast to the underlying type for bit fields.
4470 if(op0.type() != op1.type() && op0.type().id() == ID_c_bit_field)
4471 {
4472 op1 =
4474 }
4475
4476 const typet o_type0=op0.type();
4477 const typet o_type1=op1.type();
4478
4479 expr.type()=o_type0;
4480
4481 if(statement==ID_assign)
4482 {
4483 implicit_typecast(op1, o_type0);
4484 return;
4485 }
4486 else if(statement==ID_assign_shl ||
4487 statement==ID_assign_shr)
4488 {
4489 if(o_type0.id() == ID_vector)
4490 {
4491 auto &vector_o_type0 = to_vector_type(o_type0);
4492
4493 if(
4494 o_type1.id() == ID_vector &&
4495 vector_o_type0.element_type() ==
4496 to_vector_type(o_type1).element_type() &&
4497 is_number(vector_o_type0.element_type()))
4498 {
4499 return;
4500 }
4501 else if(is_number(vector_o_type0.element_type()) && is_number(o_type1))
4502 {
4503 op1 = typecast_exprt(op1, o_type0);
4504 return;
4505 }
4506 }
4507
4510
4511 if(is_number(op0.type()) && is_number(op1.type()))
4512 {
4513 if(statement==ID_assign_shl)
4514 {
4515 return;
4516 }
4517 else // assign_shr
4518 {
4519 // distinguish arithmetic from logical shifts by looking at type
4520
4521 typet underlying_type=op0.type();
4522
4523 if(underlying_type.id()==ID_unsignedbv ||
4524 underlying_type.id()==ID_c_bool)
4525 {
4526 expr.set(ID_statement, ID_assign_lshr);
4527 return;
4528 }
4529 else if(underlying_type.id()==ID_signedbv)
4530 {
4531 expr.set(ID_statement, ID_assign_ashr);
4532 return;
4533 }
4534 }
4535 }
4536 }
4537 else if(statement==ID_assign_bitxor ||
4538 statement==ID_assign_bitand ||
4539 statement==ID_assign_bitor)
4540 {
4541 // these are more restrictive
4542 if(o_type0.id()==ID_bool ||
4543 o_type0.id()==ID_c_bool)
4544 {
4546 if(
4547 op1.is_boolean() || op1.type().id() == ID_c_bool ||
4548 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4549 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
4550 {
4551 return;
4552 }
4553 }
4554 else if(o_type0.id()==ID_c_enum_tag ||
4555 o_type0.id()==ID_unsignedbv ||
4556 o_type0.id()==ID_signedbv ||
4557 o_type0.id()==ID_c_bit_field)
4558 {
4560 if(
4561 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4562 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
4563 {
4564 return;
4565 }
4566 }
4567 else if(o_type0.id()==ID_vector &&
4568 o_type1.id()==ID_vector)
4569 {
4570 // We are willing to do a modest amount of conversion
4572 to_vector_type(o_type0), to_vector_type(o_type1)))
4573 {
4574 op1 = typecast_exprt::conditional_cast(op1, o_type0);
4575 return;
4576 }
4577 }
4578 else if(
4579 o_type0.id() == ID_vector &&
4580 (o_type1.id() == ID_bool || o_type1.id() == ID_c_bool ||
4581 o_type1.id() == ID_c_enum_tag || o_type1.id() == ID_unsignedbv ||
4582 o_type1.id() == ID_signedbv))
4583 {
4585 op1 = typecast_exprt(op1, o_type0);
4586 return;
4587 }
4588 }
4589 else
4590 {
4591 if(o_type0.id()==ID_pointer &&
4592 (statement==ID_assign_minus || statement==ID_assign_plus))
4593 {
4595 return;
4596 }
4597 else if(o_type0.id()==ID_vector &&
4598 o_type1.id()==ID_vector)
4599 {
4600 // We are willing to do a modest amount of conversion
4602 to_vector_type(o_type0), to_vector_type(o_type1)))
4603 {
4604 op1 = typecast_exprt::conditional_cast(op1, o_type0);
4605 return;
4606 }
4607 }
4608 else if(o_type0.id() == ID_vector)
4609 {
4611
4612 if(
4613 is_number(op1.type()) || op1.is_boolean() ||
4614 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4615 {
4616 op1 = typecast_exprt(op1, o_type0);
4617 return;
4618 }
4619 }
4620 else if(o_type0.id()==ID_bool ||
4621 o_type0.id()==ID_c_bool)
4622 {
4624 if(
4625 op1.is_boolean() || op1.type().id() == ID_c_bool ||
4626 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4627 op1.type().id() == ID_signedbv)
4628 {
4629 return;
4630 }
4631 }
4632 else
4633 {
4635
4636 if(
4637 is_number(op1.type()) || op1.is_boolean() ||
4638 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4639 {
4640 return;
4641 }
4642 }
4643 }
4644
4646 error() << "assignment '" << statement << "' not defined for types '"
4647 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
4648 << eom;
4649
4650 throw 0;
4651}
4652
4657{
4658public:
4660 {
4661 }
4662
4664 bool operator()(const exprt &e) const
4665 {
4666 return is_constant(e);
4667 }
4668
4669protected:
4671
4674 bool is_constant(const exprt &e) const
4675 {
4676 if(e.id() == ID_infinity)
4677 return true;
4678
4679 if(e.is_constant())
4680 return true;
4681
4682 if(e.id() == ID_address_of)
4683 {
4684 return is_constant_address_of(to_address_of_expr(e).object());
4685 }
4686 else if(
4687 e.id() == ID_typecast || e.id() == ID_array_of || e.id() == ID_plus ||
4688 e.id() == ID_mult || e.id() == ID_array || e.id() == ID_with ||
4689 e.id() == ID_struct || e.id() == ID_union || e.id() == ID_empty_union ||
4690 e.id() == ID_equal || e.id() == ID_notequal || e.id() == ID_lt ||
4691 e.id() == ID_le || e.id() == ID_gt || e.id() == ID_ge ||
4692 e.id() == ID_if || e.id() == ID_not || e.id() == ID_and ||
4693 e.id() == ID_or || e.id() == ID_bitnot || e.id() == ID_bitand ||
4694 e.id() == ID_bitor || e.id() == ID_bitxor || e.id() == ID_vector)
4695 {
4696 return std::all_of(
4697 e.operands().begin(), e.operands().end(), [this](const exprt &op) {
4698 return is_constant(op);
4699 });
4700 }
4701
4702 return false;
4703 }
4704
4706 bool is_constant_address_of(const exprt &e) const
4707 {
4708 if(e.id() == ID_symbol)
4709 {
4710 return e.type().id() == ID_code ||
4711 ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
4712 }
4713 else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
4714 return true;
4715 else if(e.id() == ID_label)
4716 return true;
4717 else if(e.id() == ID_index)
4718 {
4719 const index_exprt &index_expr = to_index_expr(e);
4720
4721 return is_constant_address_of(index_expr.array()) &&
4722 is_constant(index_expr.index());
4723 }
4724 else if(e.id() == ID_member)
4725 {
4726 return is_constant_address_of(to_member_expr(e).compound());
4727 }
4728 else if(e.id() == ID_dereference)
4729 {
4730 const dereference_exprt &deref = to_dereference_expr(e);
4731
4732 return is_constant(deref.pointer());
4733 }
4734 else if(e.id() == ID_string_constant)
4735 return true;
4736
4737 return false;
4738 }
4739};
4740
4742{
4743 source_locationt location = expr.find_source_location();
4744
4745 // Floating-point expressions may require a rounding mode.
4746 // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
4747 // Some compilers have command-line options to override.
4748 const auto rounding_mode =
4750 adjust_float_expressions(expr, rounding_mode);
4751
4752 simplify(expr, *this);
4753 expr.add_source_location() = location;
4754
4755 if(!is_compile_time_constantt(*this)(expr))
4756 {
4757 error().source_location = location;
4758 error() << "expected constant expression, but got '" << to_string(expr)
4759 << "'" << eom;
4760 throw 0;
4761 }
4762}
4763
4765{
4766 source_locationt location = expr.find_source_location();
4767 make_constant(expr);
4768 make_index_type(expr);
4769 simplify(expr, *this);
4770 expr.add_source_location() = location;
4771
4772 if(!is_compile_time_constantt(*this)(expr))
4773 {
4774 error().source_location = location;
4775 error() << "conversion to integer constant failed" << eom;
4776 throw 0;
4777 }
4778}
4779
4781 const exprt &expr,
4782 const irep_idt &id,
4783 const std::string &message) const
4784{
4785 if(!has_subexpr(expr, id))
4786 return;
4787
4789 error() << message << eom;
4790 throw 0;
4791}
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
configt config
Definition config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
int8_t s1
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
unsignedbv_typet unsigned_int_type()
Definition c_types.cpp:36
unsignedbv_typet size_type()
Definition c_types.cpp:50
empty_typet void_type()
Definition c_types.cpp:245
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
signedbv_typet pointer_diff_type()
Definition c_types.cpp:220
bitvector_typet char_type()
Definition c_types.cpp:106
floatbv_typet long_double_type()
Definition c_types.cpp:193
typet c_bool_type()
Definition c_types.cpp:100
bitvector_typet c_index_type()
Definition c_types.cpp:16
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:80
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition c_types.h:377
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition c_types.h:224
Absolute value.
Definition std_expr.h:442
Operator to return the address of an object.
const declaratorst & declarators() const
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:827
A base class for binary expressions.
Definition std_expr.h:638
exprt & lhs()
Definition std_expr.h:668
exprt & rhs()
Definition std_expr.h:678
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition std_expr.h:731
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:762
Reverse the order of bits in a bit-vector.
std::size_t get_width() const
Definition std_types.h:925
The Boolean type.
Definition std_types.h:36
The byte swap expression.
Type for C bit fields These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (...
Definition c_types.h:20
const typet & underlying_type() const
Definition c_types.h:30
The type of C enums.
Definition c_types.h:239
const typet & underlying_type() const
Definition c_types.h:307
bool is_incomplete() const
enum types may be incomplete
Definition c_types.h:294
static std::optional< std::string > check_address_can_be_taken(const typet &)
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_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
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_expr(exprt &expr)
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 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)
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_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
const irep_idt mode
virtual void make_constant(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
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)
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 &)
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)
exprt typecheck_builtin_overflow(side_effect_expr_function_callt &expr, const irep_idt &arith_op)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
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)
virtual void typecheck_expr_operands(exprt &expr)
virtual std::optional< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_typed_target_call(side_effect_expr_function_callt &expr)
virtual void make_constant_index(exprt &expr)
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
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
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_expr_member(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_typecast(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
virtual bool builtin_factory(const irep_idt &)
A codet representing sequential composition of program statements.
Definition std_code.h:130
static code_blockt from_list(const std::list< codet > &_list)
Definition std_code.h:148
codet & find_last_statement()
Definition std_code.cpp:96
A codet representing the declaration of a local variable.
Definition std_code.h:347
symbol_exprt & symbol()
Definition std_code.h:354
Base type of functions.
Definition std_types.h:583
bool is_KnR() const
Definition std_types.h:674
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
bool has_ellipsis() const
Definition std_types.h:655
Data structure for representing an arbitrary statement in a program.
exprt & op0()
Definition expr.h:133
const irep_idt & get_statement() const
Imaginary part of the expression describing a complex number.
Definition std_expr.h:2027
Real part of the expression describing a complex number.
Definition std_expr.h:1984
Complex numbers made of pair of given subtype.
Definition std_types.h:1133
A constant literal expression.
Definition std_expr.h:3117
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
An expression, akin to ISO C's strlen, that denotes the length of a zero-terminated string that start...
Operator to dereference a pointer.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
The empty type.
Definition std_types.h:51
A Boolean expression returning true, iff the value of an enum-typed symbol equals one of the enum's d...
Definition c_expr.h:327
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition expr.cpp:147
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:163
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:224
exprt & op0()
Definition expr.h:133
exprt & op1()
Definition expr.h:136
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:170
exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition expr.h:101
The Boolean constant false.
Definition std_expr.h:3199
Returns one plus the index of the least-significant one bit, or zero if the operand is zero.
Round a floating-point number to an integral value considering the given rounding mode.
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
A class for an expression that indicates a history variable.
Definition c_expr.h:206
IEEE-floating-point equality.
static ieee_float_spect single_precision()
Definition ieee_float.h:70
static ieee_float_spect double_precision()
Definition ieee_float.h:76
constant_exprt to_expr() const
static ieee_float_valuet zero(const floatbv_typet &type)
Definition ieee_float.h:172
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
Definition ieee_float.h:202
The trinary if-then-else operator.
Definition std_expr.h:2497
exprt & false_case()
Definition std_expr.h:2534
exprt & true_case()
Definition std_expr.h:2524
Array index operator.
Definition std_expr.h:1470
exprt & index()
Definition std_expr.h:1510
exprt & array()
Definition std_expr.h:1500
An expression denoting infinity.
Definition std_expr.h:3224
Thrown when we can't handle something in an input source file.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition irep.cpp:482
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
void remove(const irep_idt &name)
Definition irep.cpp:87
void set(const irep_idt &name, const irep_idt &value)
Definition irep.h:412
bool is_not_nil() const
Definition irep.h:372
subt & get_sub()
Definition irep.h:448
void swap(irept &irep)
Definition irep.h:434
const irep_idt & id() const
Definition irep.h:388
irept & add(const irep_idt &name)
Definition irep.cpp:103
bool is_nil() const
Definition irep.h:368
Architecturally similar to can_forward_propagatet, but specialized for what is a constexpr,...
is_compile_time_constantt(const namespacet &ns)
bool is_constant(const exprt &e) const
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const
this function determines which reference-typed expressions are constant
bool operator()(const exprt &e) const
returns true iff the expression can be considered constant
A predicate that indicates that a zero-terminated string starts at the given address.
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
A predicate that indicates that the object pointed to is live.
A type for mathematical functions (do not confuse with functions/methods in code)
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
mstreamt & debug() const
Definition message.h:421
message_handlert & get_message_handler()
Definition message.h:183
mstreamt & warning() const
Definition message.h:396
mstreamt & result() const
Definition message.h:401
static eomt eom
Definition message.h:289
Binary multiplication Associativity is not specified.
Definition std_expr.h:1107
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition namespace.cpp:93
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
The NIL expression.
Definition std_expr.h:3208
The null pointer constant.
Expression for finding the size (in bytes) of the object a pointer points to.
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition symbol.h:179
The plus expression Associativity is not specified.
Definition std_expr.h:1002
pointer_in_range(a, b, c) evaluates to true iff same_object(a, b, c) ∧ r_ok(a, offset(c)-offset(a)) ∧...
const typet & base_type() const
The type of the data what we point to.
The popcount (counting the number of bits set to 1) expression.
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition std_expr.h:574
A base class for a predicate that indicates that an address range is ok to read or write or both.
Saturating subtraction expression.
The saturating plus expression.
A predicate that indicates that the objects pointed to are distinct.
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
exprt::operandst & arguments()
Definition std_code.h:1718
A side_effect_exprt that returns a non-deterministically chosen value.
Definition std_code.h:1520
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition c_expr.h:118
An expression containing a side effect.
Definition std_code.h:1450
const irep_idt & get_statement() const
Definition std_code.h:1472
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition std_expr.h:596
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
Base type for structs and unions.
Definition std_types.h:62
const componentst & components() const
Definition std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition std_types.cpp:64
bool has_component(const irep_idt &component_name) const
Definition std_types.h:157
bool is_incomplete() const
A struct/union may be incomplete.
Definition std_types.h:185
Expression to hold a symbol (variable)
Definition std_expr.h:131
void set_identifier(const irep_idt &identifier)
Definition std_expr.h:155
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition symbol.h:46
bool is_extern
Definition symbol.h:74
bool is_macro
Definition symbol.h:62
bool is_static_lifetime
Definition symbol.h:70
bool is_parameter
Definition symbol.h:76
bool is_type
Definition symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition symbol.h:55
bool is_lvalue
Definition symbol.h:72
irep_idt mode
Language mode.
Definition symbol.h:49
The Boolean constant true.
Definition std_expr.h:3190
Type with multiple subtypes.
Definition type.h:222
const typet & subtype() const
Definition type.h:187
Semantic type conversion.
Definition std_expr.h:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
A Boolean expression returning true, iff negation would result in an overflow when applied to the (si...
Union constructor from single element.
Definition std_expr.h:1770
The vector type.
Definition std_types.h:1064
const constant_exprt & size() const
typet index_type() const
The type of any index expression into an instance of this type.
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1080
A predicate that indicates that the object pointed to is writeable.
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4184
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition expr2c.cpp:4200
#define Forall_operands(it, expr)
Definition expr.h:27
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition expr_cast.h:81
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition expr_util.cpp:24
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
Definition padding.cpp:23
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
exprt deref_expr(const exprt &expr)
Wraps a given expression into a dereference_exprt unless it is an address_of_exprt in which case it j...
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition std_code.h:1669
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
bool can_cast_expr< side_effect_expr_function_callt >(const exprt &base)
Definition std_code.h:1730
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
bool can_cast_expr< side_effect_exprt >(const exprt &base)
Definition std_code.h:1498
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition std_code.h:429
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:97
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:895
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1538
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2107
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition std_expr.h:715
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition std_expr.h:426
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2577
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition std_expr.h:3063
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition std_types.h:29
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1158
const struct_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_tag_typet.
Definition std_types.h:478
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
bool has_suffix(const std::string &s, const std::string &suffix)
Definition suffix.h:17
Author: Diffblue Ltd.
std::string type_to_partial_identifier(const typet &type, const namespacet &ns)
Constructs a string describing the given type, which can be used as part of a C identifier.
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208
dstringt irep_idt