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