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