cprover
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 "c_typecheck_base.h"
13
14#include <sstream>
15
16#include <util/arith_tools.h>
17#include <util/bitvector_expr.h>
18#include <util/c_types.h>
19#include <util/config.h>
20#include <util/cprover_prefix.h>
21#include <util/expr_util.h>
22#include <util/floatbv_expr.h>
23#include <util/ieee_float.h>
26#include <util/pointer_expr.h>
29#include <util/prefix.h>
30#include <util/range.h>
31#include <util/simplify_expr.h>
33#include <util/suffix.h>
34
36
37#include "anonymous_member.h"
38#include "ansi_c_declaration.h"
39#include "builtin_factory.h"
40#include "c_expr.h"
41#include "c_qualifiers.h"
42#include "expr2c.h"
43#include "padding.h"
44#include "type2name.h"
45
47{
48 if(expr.id()==ID_already_typechecked)
49 {
50 expr.swap(to_already_typechecked_expr(expr).get_expr());
51 return;
52 }
53
54 // first do sub-nodes
56
57 // now do case-split
59}
60
62{
63 for(auto &op : expr.operands())
65
66 if(expr.id()==ID_div ||
67 expr.id()==ID_mult ||
68 expr.id()==ID_plus ||
69 expr.id()==ID_minus)
70 {
71 if(expr.type().id()==ID_floatbv &&
72 expr.operands().size()==2)
73 {
74 // The rounding mode to be used at compile time is non-obvious.
75 // We'll simply use round to even (0), which is suggested
76 // by Sec. F.7.2 Translation, ISO-9899:1999.
77 expr.operands().resize(3);
78
79 if(expr.id()==ID_div)
80 expr.id(ID_floatbv_div);
81 else if(expr.id()==ID_mult)
82 expr.id(ID_floatbv_mult);
83 else if(expr.id()==ID_plus)
84 expr.id(ID_floatbv_plus);
85 else if(expr.id()==ID_minus)
86 expr.id(ID_floatbv_minus);
87 else
89
92 }
93 }
94}
95
97 const typet &type1,
98 const typet &type2)
99{
100 // read
101 // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
102
103 // check qualifiers first
104 if(c_qualifierst(type1)!=c_qualifierst(type2))
105 return false;
106
107 if(type1.id()==ID_c_enum_tag)
109 else if(type2.id()==ID_c_enum_tag)
111
112 if(type1.id()==ID_c_enum)
113 {
114 if(type2.id()==ID_c_enum) // both are enums
115 return type1==type2; // compares the tag
116 else if(type2 == to_c_enum_type(type1).underlying_type())
117 return true;
118 }
119 else if(type2.id()==ID_c_enum)
120 {
121 if(type1 == to_c_enum_type(type2).underlying_type())
122 return true;
123 }
124 else if(type1.id()==ID_pointer &&
125 type2.id()==ID_pointer)
126 {
129 }
130 else if(type1.id()==ID_array &&
131 type2.id()==ID_array)
132 {
134 to_array_type(type1).element_type(),
135 to_array_type(type2).element_type()); // ignore size
136 }
137 else if(type1.id()==ID_code &&
138 type2.id()==ID_code)
139 {
140 const code_typet &c_type1=to_code_type(type1);
141 const code_typet &c_type2=to_code_type(type2);
142
144 c_type1.return_type(),
145 c_type2.return_type()))
146 return false;
147
148 if(c_type1.parameters().size()!=c_type2.parameters().size())
149 return false;
150
151 for(std::size_t i=0; i<c_type1.parameters().size(); i++)
153 c_type1.parameters()[i].type(),
154 c_type2.parameters()[i].type()))
155 return false;
156
157 return true;
158 }
159 else
160 {
161 if(type1==type2)
162 {
163 // Need to distinguish e.g. long int from int or
164 // long long int from long int.
165 // The rules appear to match those of C++.
166
167 if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type))
168 return true;
169 }
170 }
171
172 return false;
173}
174
176{
177 if(expr.id()==ID_side_effect)
179 else if(expr.id()==ID_constant)
181 else if(expr.id()==ID_infinity)
182 {
183 // ignore
184 }
185 else if(expr.id()==ID_symbol)
187 else if(expr.id()==ID_unary_plus ||
188 expr.id()==ID_unary_minus ||
189 expr.id()==ID_bitnot)
191 else if(expr.id()==ID_not)
193 else if(
194 expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies ||
195 expr.id() == ID_xor)
197 else if(expr.id()==ID_address_of)
199 else if(expr.id()==ID_dereference)
201 else if(expr.id()==ID_member)
203 else if(expr.id()==ID_ptrmember)
205 else if(expr.id()==ID_equal ||
206 expr.id()==ID_notequal ||
207 expr.id()==ID_lt ||
208 expr.id()==ID_le ||
209 expr.id()==ID_gt ||
210 expr.id()==ID_ge)
212 else if(expr.id()==ID_index)
214 else if(expr.id()==ID_typecast)
216 else if(expr.id()==ID_sizeof)
218 else if(expr.id()==ID_alignof)
220 else if(
221 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
222 expr.id() == ID_div || expr.id() == ID_mod || expr.id() == ID_bitand ||
223 expr.id() == ID_bitxor || expr.id() == ID_bitor || expr.id() == ID_bitnand)
224 {
226 }
227 else if(expr.id()==ID_shl || expr.id()==ID_shr)
229 else if(expr.id()==ID_comma)
231 else if(expr.id()==ID_if)
233 else if(expr.id()==ID_code)
234 {
236 error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
237 throw 0;
238 }
239 else if(expr.id()==ID_gcc_builtin_va_arg)
241 else if(expr.id()==ID_cw_va_arg_typeof)
243 else if(expr.id()==ID_gcc_builtin_types_compatible_p)
244 {
245 expr.type()=bool_typet();
246 auto &subtypes =
247 (static_cast<type_with_subtypest &>(expr.add(ID_type_arg))).subtypes();
248 assert(subtypes.size()==2);
249 typecheck_type(subtypes[0]);
250 typecheck_type(subtypes[1]);
251 source_locationt source_location=expr.source_location();
252
253 // ignores top-level qualifiers
254 subtypes[0].remove(ID_C_constant);
255 subtypes[0].remove(ID_C_volatile);
256 subtypes[0].remove(ID_C_restricted);
257 subtypes[1].remove(ID_C_constant);
258 subtypes[1].remove(ID_C_volatile);
259 subtypes[1].remove(ID_C_restricted);
260
261 expr = make_boolean_expr(gcc_types_compatible_p(subtypes[0], subtypes[1]));
262 expr.add_source_location()=source_location;
263 }
264 else if(expr.id()==ID_clang_builtin_convertvector)
265 {
266 // This has one operand and a type, and acts like a typecast
267 DATA_INVARIANT(expr.operands().size()==1, "clang_builtin_convertvector has one operand");
268 typecheck_type(expr.type());
269 typecast_exprt tmp(to_unary_expr(expr).op(), expr.type());
271 expr.swap(tmp);
272 }
273 else if(expr.id()==ID_builtin_offsetof)
275 else if(expr.id()==ID_string_constant)
276 {
277 // already fine -- mark as lvalue
278 expr.set(ID_C_lvalue, true);
279 }
280 else if(expr.id()==ID_arguments)
281 {
282 // already fine
283 }
284 else if(expr.id()==ID_designated_initializer)
285 {
286 exprt &designator=static_cast<exprt &>(expr.add(ID_designator));
287
288 Forall_operands(it, designator)
289 {
290 if(it->id()==ID_index)
291 typecheck_expr(to_unary_expr(*it).op()); // still needs typechecking
292 }
293 }
294 else if(expr.id()==ID_initializer_list)
295 {
296 // already fine, just set some type
297 expr.type()=void_type();
298 }
299 else if(
300 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
301 {
302 // These have two operands.
303 // op0 is a tuple with declarations,
304 // op1 is the bound expression
305 auto &binary_expr = to_binary_expr(expr);
306 auto &bindings = binary_expr.op0().operands();
307 auto &where = binary_expr.op1();
308
309 for(const auto &binding : bindings)
310 {
311 if(binding.get(ID_statement) != ID_decl)
312 {
314 error() << "expected declaration as operand of quantifier" << eom;
315 throw 0;
316 }
317 }
318
319 if(has_subexpr(where, ID_side_effect))
320 {
322 error() << "quantifier must not contain side effects" << eom;
323 throw 0;
324 }
325
326 // replace declarations by symbol expressions
327 for(auto &binding : bindings)
328 binding = to_code_frontend_decl(to_code(binding)).symbol();
329
330 if(expr.id() == ID_lambda)
331 {
333
334 for(auto &binding : bindings)
335 domain.push_back(binding.type());
336
337 expr.type() = mathematical_function_typet(domain, where.type());
338 }
339 else
340 {
341 expr.type() = bool_typet();
343 }
344 }
345 else if(expr.id()==ID_label)
346 {
347 expr.type()=void_type();
348 }
349 else if(expr.id()==ID_array)
350 {
351 // these pop up as string constants, and are already typed
352 }
353 else if(expr.id()==ID_complex)
354 {
355 // these should only exist as constants,
356 // and should already be typed
357 }
358 else if(expr.id() == ID_complex_real)
359 {
360 const exprt &op = to_unary_expr(expr).op();
361
362 if(op.type().id() != ID_complex)
363 {
364 if(!is_number(op.type()))
365 {
367 error() << "real part retrieval expects numerical operand, "
368 << "but got '" << to_string(op.type()) << "'" << eom;
369 throw 0;
370 }
371
372 typecast_exprt typecast_expr(op, complex_typet(op.type()));
373 complex_real_exprt complex_real_expr(typecast_expr);
374
375 expr.swap(complex_real_expr);
376 }
377 else
378 {
379 complex_real_exprt complex_real_expr(op);
380
381 // these are lvalues if the operand is one
382 if(op.get_bool(ID_C_lvalue))
383 complex_real_expr.set(ID_C_lvalue, true);
384
385 if(op.type().get_bool(ID_C_constant))
386 complex_real_expr.type().set(ID_C_constant, true);
387
388 expr.swap(complex_real_expr);
389 }
390 }
391 else if(expr.id() == ID_complex_imag)
392 {
393 const exprt &op = to_unary_expr(expr).op();
394
395 if(op.type().id() != ID_complex)
396 {
397 if(!is_number(op.type()))
398 {
400 error() << "real part retrieval expects numerical operand, "
401 << "but got '" << to_string(op.type()) << "'" << eom;
402 throw 0;
403 }
404
405 typecast_exprt typecast_expr(op, complex_typet(op.type()));
406 complex_imag_exprt complex_imag_expr(typecast_expr);
407
408 expr.swap(complex_imag_expr);
409 }
410 else
411 {
412 complex_imag_exprt complex_imag_expr(op);
413
414 // these are lvalues if the operand is one
415 if(op.get_bool(ID_C_lvalue))
416 complex_imag_expr.set(ID_C_lvalue, true);
417
418 if(op.type().get_bool(ID_C_constant))
419 complex_imag_expr.type().set(ID_C_constant, true);
420
421 expr.swap(complex_imag_expr);
422 }
423 }
424 else if(expr.id()==ID_generic_selection)
425 {
426 // This is C11.
427 // The operand is already typechecked. Depending
428 // on its type, we return one of the generic associations.
429 auto &op = to_unary_expr(expr).op();
430
431 // This is one of the few places where it's detectable
432 // that we are using "bool" for boolean operators instead
433 // of "int". We convert for this reason.
434 if(op.type().id() == ID_bool)
436
437 irept::subt &generic_associations=
438 expr.add(ID_generic_associations).get_sub();
439
440 // first typecheck all types
441 for(auto &irep : generic_associations)
442 {
443 if(irep.get(ID_type_arg) != ID_default)
444 {
445 typet &type = static_cast<typet &>(irep.add(ID_type_arg));
446 typecheck_type(type);
447 }
448 }
449
450 // first try non-default match
451 exprt default_match=nil_exprt();
452 exprt assoc_match=nil_exprt();
453
454 const typet &op_type = follow(op.type());
455
456 for(const auto &irep : generic_associations)
457 {
458 if(irep.get(ID_type_arg) == ID_default)
459 default_match = static_cast<const exprt &>(irep.find(ID_value));
460 else if(
461 op_type == follow(static_cast<const typet &>(irep.find(ID_type_arg))))
462 {
463 assoc_match = static_cast<const exprt &>(irep.find(ID_value));
464 }
465 }
466
467 if(assoc_match.is_nil())
468 {
469 if(default_match.is_not_nil())
470 expr.swap(default_match);
471 else
472 {
474 error() << "unmatched generic selection: " << to_string(op.type())
475 << eom;
476 throw 0;
477 }
478 }
479 else
480 expr.swap(assoc_match);
481
482 // still need to typecheck the result
483 typecheck_expr(expr);
484 }
485 else if(expr.id()==ID_gcc_asm_input ||
486 expr.id()==ID_gcc_asm_output ||
487 expr.id()==ID_gcc_asm_clobbered_register)
488 {
489 }
490 else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
491 expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
492 {
493 // already type checked
494 }
495 else if(expr.id() == ID_C_spec_assigns || expr.id() == ID_target_list)
496 {
497 // already type checked
498 }
499 else
500 {
502 error() << "unexpected expression: " << expr.pretty() << eom;
503 throw 0;
504 }
505}
506
508{
509 expr.type() = to_binary_expr(expr).op1().type();
510
511 // make this an l-value if the last operand is one
512 if(to_binary_expr(expr).op1().get_bool(ID_C_lvalue))
513 expr.set(ID_C_lvalue, true);
514}
515
517{
518 // The first parameter is the va_list, and the second
519 // is the type, which will need to be fixed and checked.
520 // The type is given by the parser as type of the expression.
521
522 typet arg_type=expr.type();
523 typecheck_type(arg_type);
524
525 const code_typet new_type(
526 {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
527
528 exprt arg = to_unary_expr(expr).op();
529
531
532 symbol_exprt function(ID_gcc_builtin_va_arg, new_type);
533 function.add_source_location() = expr.source_location();
534
535 // turn into function call
537 function, {arg}, new_type.return_type(), expr.source_location());
538
539 expr.swap(result);
540
541 // Make sure symbol exists, but we have it return void
542 // to avoid collisions of the same symbol with different
543 // types.
544
545 code_typet symbol_type=new_type;
546 symbol_type.return_type()=void_type();
547
548 symbolt symbol;
549 symbol.base_name=ID_gcc_builtin_va_arg;
550 symbol.name=ID_gcc_builtin_va_arg;
551 symbol.type=symbol_type;
552 symbol.mode = ID_C;
553
554 symbol_table.insert(std::move(symbol));
555}
556
558{
559 // used in Code Warrior via
560 //
561 // __va_arg( <Symbol>, _var_arg_typeof( <Typ> ) )
562 //
563 // where __va_arg is declared as
564 //
565 // extern void* __va_arg(void*, int);
566
567 typet &type=static_cast<typet &>(expr.add(ID_type_arg));
568 typecheck_type(type);
569
570 // these return an integer
571 expr.type()=signed_int_type();
572}
573
575{
576 // these need not be constant, due to array indices!
577
578 if(!expr.operands().empty())
579 {
581 error() << "builtin_offsetof expects no operands" << eom;
582 throw 0;
583 }
584
585 typet &type=static_cast<typet &>(expr.add(ID_type_arg));
586 typecheck_type(type);
587
588 exprt &member=static_cast<exprt &>(expr.add(ID_designator));
589
591
592 forall_operands(m_it, member)
593 {
594 type = follow(type);
595
596 if(m_it->id()==ID_member)
597 {
598 if(type.id()!=ID_union && type.id()!=ID_struct)
599 {
601 error() << "offsetof of member expects struct/union type, "
602 << "but got '" << to_string(type) << "'" << eom;
603 throw 0;
604 }
605
606 bool found=false;
607 irep_idt component_name=m_it->get(ID_component_name);
608
609 while(!found)
610 {
611 assert(type.id()==ID_union || type.id()==ID_struct);
612
613 const struct_union_typet &struct_union_type=
615
616 // direct member?
617 if(struct_union_type.has_component(component_name))
618 {
619 found=true;
620
621 if(type.id()==ID_struct)
622 {
623 auto o_opt =
624 member_offset_expr(to_struct_type(type), component_name, *this);
625
626 if(!o_opt.has_value())
627 {
629 error() << "offsetof failed to determine offset of '"
630 << component_name << "'" << eom;
631 throw 0;
632 }
633
635 result,
637 }
638
639 type=struct_union_type.get_component(component_name).type();
640 }
641 else
642 {
643 // maybe anonymous?
644 bool found2=false;
645
646 for(const auto &c : struct_union_type.components())
647 {
648 if(
649 c.get_anonymous() &&
650 (c.type().id() == ID_struct_tag || c.type().id() == ID_union_tag))
651 {
652 if(has_component_rec(c.type(), component_name, *this))
653 {
654 if(type.id()==ID_struct)
655 {
656 auto o_opt = member_offset_expr(
657 to_struct_type(type), c.get_name(), *this);
658
659 if(!o_opt.has_value())
660 {
662 error() << "offsetof failed to determine offset of '"
663 << component_name << "'" << eom;
664 throw 0;
665 }
666
668 result,
670 o_opt.value(), size_type()));
671 }
672
673 typet tmp = follow(c.type());
674 type=tmp;
675 assert(type.id()==ID_union || type.id()==ID_struct);
676 found2=true;
677 break; // we run into another iteration of the outer loop
678 }
679 }
680 }
681
682 if(!found2)
683 {
685 error() << "offset-of of member failed to find component '"
686 << component_name << "' in '" << to_string(type) << "'"
687 << eom;
688 throw 0;
689 }
690 }
691 }
692 }
693 else if(m_it->id()==ID_index)
694 {
695 if(type.id()!=ID_array)
696 {
698 error() << "offsetof of index expects array type" << eom;
699 throw 0;
700 }
701
702 exprt index = to_unary_expr(*m_it).op();
703
704 // still need to typecheck index
705 typecheck_expr(index);
706
707 auto element_size_opt =
708 size_of_expr(to_array_type(type).element_type(), *this);
709
710 if(!element_size_opt.has_value())
711 {
713 error() << "offsetof failed to determine array element size" << eom;
714 throw 0;
715 }
716
718
719 result = plus_exprt(result, mult_exprt(element_size_opt.value(), index));
720
721 typet tmp=type.subtype();
722 type=tmp;
723 }
724 }
725
726 // We make an effort to produce a constant,
727 // but this may depend on variables
728 simplify(result, *this);
729 result.add_source_location()=expr.source_location();
730
731 expr.swap(result);
732}
733
735{
736 if(expr.id()==ID_side_effect &&
737 expr.get(ID_statement)==ID_function_call)
738 {
739 // don't do function operand
740 typecheck_expr(to_binary_expr(expr).op1()); // arguments
741 }
742 else if(expr.id()==ID_side_effect &&
743 expr.get(ID_statement)==ID_statement_expression)
744 {
746 }
747 else if(
748 expr.id() == ID_forall || expr.id() == ID_exists || expr.id() == ID_lambda)
749 {
750 // These introduce new symbols, which need to be added to the symbol table
751 // before the second operand is typechecked.
752
753 auto &binary_expr = to_binary_expr(expr);
754 auto &bindings = binary_expr.op0().operands();
755
756 for(auto &binding : bindings)
757 {
758 ansi_c_declarationt &declaration = to_ansi_c_declaration(binding);
759
760 typecheck_declaration(declaration);
761
762 if(declaration.declarators().size() != 1)
763 {
765 error() << "forall/exists expects one declarator exactly" << eom;
766 throw 0;
767 }
768
769 irep_idt identifier = declaration.declarators().front().get_name();
770
771 // look it up
772 symbol_tablet::symbolst::const_iterator s_it =
773 symbol_table.symbols.find(identifier);
774
775 if(s_it == symbol_table.symbols.end())
776 {
778 error() << "failed to find bound symbol `" << identifier
779 << "' in symbol table" << eom;
780 throw 0;
781 }
782
783 const symbolt &symbol = s_it->second;
784
785 if(
786 symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
787 !is_complete_type(symbol.type) || symbol.type.id() == ID_code)
788 {
790 error() << "unexpected quantified symbol" << eom;
791 throw 0;
792 }
793
794 code_frontend_declt decl(symbol.symbol_expr());
795 decl.add_source_location() = declaration.source_location();
796
797 binding = decl;
798 }
799
800 typecheck_expr(binary_expr.op1());
801 }
802 else
803 {
804 Forall_operands(it, expr)
805 typecheck_expr(*it);
806 }
807}
808
810{
811 irep_idt identifier=to_symbol_expr(expr).get_identifier();
812
813 // Is it a parameter? We do this while checking parameter lists.
814 id_type_mapt::const_iterator p_it=parameter_map.find(identifier);
815 if(p_it!=parameter_map.end())
816 {
817 // yes
818 expr.type()=p_it->second;
819 expr.set(ID_C_lvalue, true);
820 return;
821 }
822
823 // renaming via GCC asm label
824 asm_label_mapt::const_iterator entry=
825 asm_label_map.find(identifier);
826 if(entry!=asm_label_map.end())
827 {
828 identifier=entry->second;
829 to_symbol_expr(expr).set_identifier(identifier);
830 }
831
832 // look it up
833 const symbolt *symbol_ptr;
834 if(lookup(identifier, symbol_ptr))
835 {
837 error() << "failed to find symbol '" << identifier << "'" << eom;
838 throw 0;
839 }
840
841 const symbolt &symbol=*symbol_ptr;
842
843 if(symbol.is_type)
844 {
846 error() << "did not expect a type symbol here, but got '"
847 << symbol.display_name() << "'" << eom;
848 throw 0;
849 }
850
851 // save the source location
852 source_locationt source_location=expr.source_location();
853
854 if(symbol.is_macro)
855 {
856 // preserve enum key
857 #if 0
858 irep_idt base_name=expr.get(ID_C_base_name);
859 #endif
860
861 follow_macros(expr);
862
863 #if 0
864 if(expr.id()==ID_constant &&
865 !base_name.empty())
866 expr.set(ID_C_cformat, base_name);
867 else
868 #endif
869 typecheck_expr(expr);
870
871 // preserve location
872 expr.add_source_location()=source_location;
873 }
874 else if(has_prefix(id2string(identifier), CPROVER_PREFIX "constant_infinity"))
875 {
876 expr=infinity_exprt(symbol.type);
877
878 // put it back
879 expr.add_source_location()=source_location;
880 }
881 else if(identifier=="__func__" ||
882 identifier=="__FUNCTION__" ||
883 identifier=="__PRETTY_FUNCTION__")
884 {
885 // __func__ is an ANSI-C standard compliant hack to get the function name
886 // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
887 string_constantt s(source_location.get_function());
888 s.add_source_location()=source_location;
889 s.set(ID_C_lvalue, true);
890 expr.swap(s);
891 }
892 else
893 {
894 expr=symbol.symbol_expr();
895
896 // put it back
897 expr.add_source_location()=source_location;
898
899 if(symbol.is_lvalue)
900 expr.set(ID_C_lvalue, true);
901
902 if(expr.type().id()==ID_code) // function designator
903 { // special case: this is sugar for &f
904 address_of_exprt tmp(expr, pointer_type(expr.type()));
905 tmp.set(ID_C_implicit, true);
907 expr=tmp;
908 }
909 }
910}
911
913 side_effect_exprt &expr)
914{
915 codet &code = to_code(to_unary_expr(expr).op());
916
917 // the type is the type of the last statement in the
918 // block, but do worry about labels!
919
921
922 irep_idt last_statement=last.get_statement();
923
924 if(last_statement==ID_expression)
925 {
926 assert(last.operands().size()==1);
927 exprt &op=last.op0();
928
929 // arrays here turn into pointers (array decay)
930 if(op.type().id()==ID_array)
932
933 expr.type()=op.type();
934 }
935 else
936 {
937 // we used to do this, but don't expect it any longer
938 PRECONDITION(last_statement != ID_function_call);
939
940 expr.type()=typet(ID_empty);
941 }
942}
943
945{
946 typet type;
947
948 // these come in two flavors: with zero operands, for a type,
949 // and with one operand, for an expression.
950 PRECONDITION(expr.operands().size() <= 1);
951
952 if(expr.operands().empty())
953 {
954 type.swap(static_cast<typet &>(expr.add(ID_type_arg)));
955 typecheck_type(type);
956 }
957 else
958 {
959 const exprt &op = to_unary_expr(as_const(expr)).op();
960 // This is one of the few places where it's detectable
961 // that we are using "bool" for boolean operators instead
962 // of "int". We convert for this reason.
963 if(op.type().id() == ID_bool)
964 type = signed_int_type();
965 else
966 type = op.type();
967 }
968
969 exprt new_expr;
970
971 if(type.id()==ID_c_bit_field)
972 {
974 error() << "sizeof cannot be applied to bit fields" << eom;
975 throw 0;
976 }
977 else if(type.id() == ID_bool)
978 {
980 error() << "sizeof cannot be applied to single bits" << eom;
981 throw 0;
982 }
983 else if(type.id() == ID_empty)
984 {
985 // This is a gcc extension.
986 // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
987 new_expr = from_integer(1, size_type());
988 }
989 else
990 {
991 if(
992 (type.id() == ID_struct_tag &&
993 follow_tag(to_struct_tag_type(type)).is_incomplete()) ||
994 (type.id() == ID_union_tag &&
995 follow_tag(to_union_tag_type(type)).is_incomplete()) ||
996 (type.id() == ID_c_enum_tag &&
997 follow_tag(to_c_enum_tag_type(type)).is_incomplete()) ||
998 (type.id() == ID_array && to_array_type(type).is_incomplete()))
999 {
1001 error() << "invalid application of \'sizeof\' to an incomplete type\n\t\'"
1002 << to_string(type) << "\'" << eom;
1003 throw 0;
1004 }
1005
1006 auto size_of_opt = size_of_expr(type, *this);
1007
1008 if(!size_of_opt.has_value())
1009 {
1011 error() << "type has no size: " << to_string(type) << eom;
1012 throw 0;
1013 }
1014
1015 new_expr = size_of_opt.value();
1016 }
1017
1018 new_expr.swap(expr);
1019
1020 expr.add(ID_C_c_sizeof_type)=type;
1021
1022 // The type may contain side-effects.
1023 if(!clean_code.empty())
1024 {
1025 side_effect_exprt side_effect_expr(
1026 ID_statement_expression, void_type(), expr.source_location());
1027 auto decl_block=code_blockt::from_list(clean_code);
1028 decl_block.set_statement(ID_decl_block);
1029 side_effect_expr.copy_to_operands(decl_block);
1030 clean_code.clear();
1031
1032 // We merge the side-effect into the operand of the typecast,
1033 // using a comma-expression.
1034 // I.e., (type)e becomes (type)(side-effect, e)
1035 // It is not obvious whether the type or 'e' should be evaluated
1036 // first.
1037
1038 exprt comma_expr(ID_comma, expr.type());
1039 comma_expr.copy_to_operands(side_effect_expr, expr);
1040 expr.swap(comma_expr);
1041 }
1042}
1043
1045{
1046 typet argument_type;
1047
1048 if(expr.operands().size()==1)
1049 argument_type = to_unary_expr(expr).op().type();
1050 else
1051 {
1052 typet &op_type=static_cast<typet &>(expr.add(ID_type_arg));
1053 typecheck_type(op_type);
1054 argument_type=op_type;
1055 }
1056
1057 // we only care about the type
1058 mp_integer a=alignment(argument_type, *this);
1059
1060 exprt tmp=from_integer(a, size_type());
1062
1063 expr.swap(tmp);
1064}
1065
1067{
1068 exprt &op = to_unary_expr(expr).op();
1069
1070 typecheck_type(expr.type());
1071
1072 // The type may contain side-effects.
1073 if(!clean_code.empty())
1074 {
1075 side_effect_exprt side_effect_expr(
1076 ID_statement_expression, void_type(), expr.source_location());
1077 auto decl_block=code_blockt::from_list(clean_code);
1078 decl_block.set_statement(ID_decl_block);
1079 side_effect_expr.copy_to_operands(decl_block);
1080 clean_code.clear();
1081
1082 // We merge the side-effect into the operand of the typecast,
1083 // using a comma-expression.
1084 // I.e., (type)e becomes (type)(side-effect, e)
1085 // It is not obvious whether the type or 'e' should be evaluated
1086 // first.
1087
1088 exprt comma_expr(ID_comma, op.type());
1089 comma_expr.copy_to_operands(side_effect_expr, op);
1090 op.swap(comma_expr);
1091 }
1092
1093 const typet expr_type = expr.type();
1094
1095 if(
1096 expr_type.id() == ID_union_tag && expr_type != op.type() &&
1097 op.id() != ID_initializer_list)
1098 {
1099 // This is a GCC extension. It's either a 'temporary union',
1100 // where the argument is one of the member types.
1101
1102 // This is one of the few places where it's detectable
1103 // that we are using "bool" for boolean operators instead
1104 // of "int". We convert for this reason.
1105 if(op.type().id() == ID_bool)
1106 op = typecast_exprt(op, signed_int_type());
1107
1108 // we need to find a member with the right type
1109 const auto &union_type = follow_tag(to_union_tag_type(expr_type));
1110 for(const auto &c : union_type.components())
1111 {
1112 if(c.type() == op.type())
1113 {
1114 // found! build union constructor
1115 union_exprt union_expr(c.get_name(), op, expr.type());
1116 union_expr.add_source_location()=expr.source_location();
1117 expr=union_expr;
1118 expr.set(ID_C_lvalue, true);
1119 return;
1120 }
1121 }
1122
1123 // not found, complain
1125 error() << "type cast to union: type '" << to_string(op.type())
1126 << "' not found in union" << eom;
1127 throw 0;
1128 }
1129
1130 // We allow (TYPE){ initializer_list }
1131 // This is called "compound literal", and is syntactic
1132 // sugar for a (possibly local) declaration.
1133 if(op.id()==ID_initializer_list)
1134 {
1135 // just do a normal initialization
1136 do_initializer(op, expr.type(), false);
1137
1138 // This produces a struct-expression,
1139 // union-expression, array-expression,
1140 // or an expression for a pointer or scalar.
1141 // We produce a compound_literal expression.
1142 exprt tmp(ID_compound_literal, expr.type());
1143 tmp.copy_to_operands(op);
1144
1145 // handle the case of TYPE being an array with unspecified size
1146 if(op.id()==ID_array &&
1147 expr.type().id()==ID_array &&
1148 to_array_type(expr.type()).size().is_nil())
1149 tmp.type()=op.type();
1150
1151 expr=tmp;
1152 expr.set(ID_C_lvalue, true); // these are l-values
1153 return;
1154 }
1155
1156 // a cast to void is always fine
1157 if(expr_type.id()==ID_empty)
1158 return;
1159
1160 const typet op_type = op.type();
1161
1162 // cast to same type?
1163 if(expr_type == op_type)
1164 return; // it's ok
1165
1166 // vectors?
1167
1168 if(expr_type.id()==ID_vector)
1169 {
1170 // we are generous -- any vector to vector is fine
1171 if(op_type.id()==ID_vector)
1172 return;
1173 else if(op_type.id()==ID_signedbv ||
1174 op_type.id()==ID_unsignedbv)
1175 return;
1176 }
1177
1178 if(!is_numeric_type(expr_type) && expr_type.id()!=ID_pointer)
1179 {
1181 error() << "type cast to '" << to_string(expr_type) << "' is not permitted"
1182 << eom;
1183 throw 0;
1184 }
1185
1186 if(is_numeric_type(op_type) || op_type.id()==ID_pointer)
1187 {
1188 }
1189 else if(op_type.id()==ID_array)
1190 {
1191 index_exprt index(op, from_integer(0, c_index_type()));
1192 op=address_of_exprt(index);
1193 }
1194 else if(op_type.id()==ID_empty)
1195 {
1196 if(expr_type.id()!=ID_empty)
1197 {
1199 error() << "type cast from void only permitted to void, but got '"
1200 << to_string(expr.type()) << "'" << eom;
1201 throw 0;
1202 }
1203 }
1204 else if(op_type.id()==ID_vector)
1205 {
1206 const vector_typet &op_vector_type=
1207 to_vector_type(op_type);
1208
1209 // gcc allows conversion of a vector of size 1 to
1210 // an integer/float of the same size
1211 if((expr_type.id()==ID_signedbv ||
1212 expr_type.id()==ID_unsignedbv) &&
1213 pointer_offset_bits(expr_type, *this)==
1214 pointer_offset_bits(op_vector_type, *this))
1215 {
1216 }
1217 else
1218 {
1220 error() << "type cast from vector to '" << to_string(expr.type())
1221 << "' not permitted" << eom;
1222 throw 0;
1223 }
1224 }
1225 else
1226 {
1228 error() << "type cast from '" << to_string(op_type) << "' not permitted"
1229 << eom;
1230 throw 0;
1231 }
1232
1233 // The new thing is an lvalue if the previous one is
1234 // an lvalue and it's just a pointer type cast.
1235 // This isn't really standard conformant!
1236 // Note that gcc says "warning: target of assignment not really an lvalue;
1237 // this will be a hard error in the future", i.e., we
1238 // can hope that the code below will one day simply go away.
1239
1240 // Current versions of gcc in fact refuse to do this! Yay!
1241
1242 if(op.get_bool(ID_C_lvalue))
1243 {
1244 if(expr_type.id()==ID_pointer)
1245 expr.set(ID_C_lvalue, true);
1246 }
1247}
1248
1250{
1252}
1253
1255{
1256 exprt &array_expr = to_binary_expr(expr).op0();
1257 exprt &index_expr = to_binary_expr(expr).op1();
1258
1259 // we might have to swap them
1260
1261 {
1262 const typet &array_type = array_expr.type();
1263 const typet &index_type = index_expr.type();
1264
1265 if(
1266 array_type.id() != ID_array && array_type.id() != ID_pointer &&
1267 array_type.id() != ID_vector &&
1268 (index_type.id() == ID_array || index_type.id() == ID_pointer ||
1269 index_type.id() == ID_vector))
1270 std::swap(array_expr, index_expr);
1271 }
1272
1273 make_index_type(index_expr);
1274
1275 // array_expr is a reference to one of expr.operands(), when that vector is
1276 // swapped below the reference is no longer valid. final_array_type exists
1277 // beyond that point so can't be a reference
1278 const typet final_array_type = array_expr.type();
1279
1280 if(final_array_type.id()==ID_array ||
1281 final_array_type.id()==ID_vector)
1282 {
1283 expr.type() = to_type_with_subtype(final_array_type).subtype();
1284
1285 if(array_expr.get_bool(ID_C_lvalue))
1286 expr.set(ID_C_lvalue, true);
1287
1288 if(final_array_type.get_bool(ID_C_constant))
1289 expr.type().set(ID_C_constant, true);
1290 }
1291 else if(final_array_type.id()==ID_pointer)
1292 {
1293 // p[i] is syntactic sugar for *(p+i)
1294
1296 exprt::operandst summands;
1297 std::swap(summands, expr.operands());
1298 expr.add_to_operands(plus_exprt(std::move(summands), array_expr.type()));
1299 expr.id(ID_dereference);
1300 expr.set(ID_C_lvalue, true);
1301 expr.type() = to_pointer_type(final_array_type).base_type();
1302 }
1303 else
1304 {
1306 error() << "operator [] must take array/vector or pointer but got '"
1307 << to_string(array_expr.type()) << "'" << eom;
1308 throw 0;
1309 }
1310}
1311
1313{
1314 // equality and disequality on float is not mathematical equality!
1315 if(expr.op0().type().id() == ID_floatbv)
1316 {
1317 if(expr.id()==ID_equal)
1318 expr.id(ID_ieee_float_equal);
1319 else if(expr.id()==ID_notequal)
1320 expr.id(ID_ieee_float_notequal);
1321 }
1322}
1323
1326{
1327 exprt &op0=expr.op0();
1328 exprt &op1=expr.op1();
1329
1330 const typet o_type0=op0.type();
1331 const typet o_type1=op1.type();
1332
1333 if(o_type0.id() == ID_vector || o_type1.id() == ID_vector)
1334 {
1336 return;
1337 }
1338
1339 expr.type()=bool_typet();
1340
1341 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1342 {
1343 if(follow(o_type0)==follow(o_type1))
1344 {
1345 if(o_type0.id() != ID_array)
1346 {
1347 adjust_float_rel(expr);
1348 return; // no promotion necessary
1349 }
1350 }
1351 }
1352
1354
1355 const typet &type0=op0.type();
1356 const typet &type1=op1.type();
1357
1358 if(type0==type1)
1359 {
1360 if(is_number(type0))
1361 {
1362 adjust_float_rel(expr);
1363 return;
1364 }
1365
1366 if(type0.id()==ID_pointer)
1367 {
1368 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1369 return;
1370
1371 if(expr.id()==ID_le || expr.id()==ID_lt ||
1372 expr.id()==ID_ge || expr.id()==ID_gt)
1373 return;
1374 }
1375
1376 if(type0.id()==ID_string_constant)
1377 {
1378 if(expr.id()==ID_equal || expr.id()==ID_notequal)
1379 return;
1380 }
1381 }
1382 else
1383 {
1384 // pointer and zero
1385 if(type0.id()==ID_pointer &&
1386 simplify_expr(op1, *this).is_zero())
1387 {
1388 op1 = null_pointer_exprt{to_pointer_type(type0)};
1389 return;
1390 }
1391
1392 if(type1.id()==ID_pointer &&
1393 simplify_expr(op0, *this).is_zero())
1394 {
1395 op0 = null_pointer_exprt{to_pointer_type(type1)};
1396 return;
1397 }
1398
1399 // pointer and integer
1400 if(type0.id()==ID_pointer && is_number(type1))
1401 {
1402 op1 = typecast_exprt(op1, type0);
1403 return;
1404 }
1405
1406 if(type1.id()==ID_pointer && is_number(type0))
1407 {
1408 op0 = typecast_exprt(op0, type1);
1409 return;
1410 }
1411
1412 if(type0.id()==ID_pointer && type1.id()==ID_pointer)
1413 {
1414 op1 = typecast_exprt(op1, type0);
1415 return;
1416 }
1417 }
1418
1420 error() << "operator '" << expr.id() << "' not defined for types '"
1421 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
1422 << eom;
1423 throw 0;
1424}
1425
1427{
1428 const typet &o_type0 = as_const(expr).op0().type();
1429 const typet &o_type1 = as_const(expr).op1().type();
1430
1431 if(o_type0.id() != ID_vector || o_type0 != o_type1)
1432 {
1434 error() << "vector operator '" << expr.id() << "' not defined for types '"
1435 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
1436 << eom;
1437 throw 0;
1438 }
1439
1440 // Comparisons between vectors produce a vector of integers of the same width
1441 // with the same dimension.
1442 auto subtype_width =
1443 to_bitvector_type(to_vector_type(o_type0).element_type()).get_width();
1444 expr.type() =
1445 vector_typet{signedbv_typet{subtype_width}, to_vector_type(o_type0).size()};
1446
1447 // Replace the id as the semantics of these are point-wise application (and
1448 // the result is not of bool type).
1449 if(expr.id() == ID_notequal)
1450 expr.id(ID_vector_notequal);
1451 else
1452 expr.id("vector-" + id2string(expr.id()));
1453}
1454
1456{
1457 auto &op = to_unary_expr(expr).op();
1458 const typet &op0_type = op.type();
1459
1460 if(op0_type.id() == ID_array)
1461 {
1462 // a->f is the same as a[0].f
1463 exprt zero = from_integer(0, c_index_type());
1464 index_exprt index_expr(op, zero, to_array_type(op0_type).element_type());
1465 index_expr.set(ID_C_lvalue, true);
1466 op.swap(index_expr);
1467 }
1468 else if(op0_type.id() == ID_pointer)
1469 {
1470 // turn x->y into (*x).y
1471 dereference_exprt deref_expr(op);
1472 deref_expr.add_source_location()=expr.source_location();
1473 typecheck_expr_dereference(deref_expr);
1474 op.swap(deref_expr);
1475 }
1476 else
1477 {
1479 error() << "ptrmember operator requires pointer or array type "
1480 "on left hand side, but got '"
1481 << to_string(op0_type) << "'" << eom;
1482 throw 0;
1483 }
1484
1485 expr.id(ID_member);
1487}
1488
1490{
1491 exprt &op0 = to_unary_expr(expr).op();
1492 typet type=op0.type();
1493
1494 type = follow(type);
1495
1496 if(type.id()!=ID_struct &&
1497 type.id()!=ID_union)
1498 {
1500 error() << "member operator requires structure type "
1501 "on left hand side but got '"
1502 << to_string(type) << "'" << eom;
1503 throw 0;
1504 }
1505
1506 const struct_union_typet &struct_union_type=
1508
1509 if(struct_union_type.is_incomplete())
1510 {
1512 error() << "member operator got incomplete " << type.id()
1513 << " type on left hand side" << eom;
1514 throw 0;
1515 }
1516
1517 const irep_idt &component_name=
1518 expr.get(ID_component_name);
1519
1520 // first try to find directly
1522 struct_union_type.get_component(component_name);
1523
1524 // if that fails, search the anonymous members
1525
1526 if(component.is_nil())
1527 {
1528 exprt tmp=get_component_rec(op0, component_name, *this);
1529
1530 if(tmp.is_nil())
1531 {
1532 // give up
1534 error() << "member '" << component_name << "' not found in '"
1535 << to_string(type) << "'" << eom;
1536 throw 0;
1537 }
1538
1539 // done!
1540 expr.swap(tmp);
1541 return;
1542 }
1543
1544 expr.type()=component.type();
1545
1546 if(op0.get_bool(ID_C_lvalue))
1547 expr.set(ID_C_lvalue, true);
1548
1549 if(op0.type().get_bool(ID_C_constant) || type.get_bool(ID_C_constant))
1550 expr.type().set(ID_C_constant, true);
1551
1552 // copy method identifier
1553 const irep_idt &identifier=component.get(ID_C_identifier);
1554
1555 if(!identifier.empty())
1556 expr.set(ID_C_identifier, identifier);
1557
1558 const irep_idt &access=component.get_access();
1559
1560 if(access==ID_private)
1561 {
1563 error() << "member '" << component_name << "' is " << access << eom;
1564 throw 0;
1565 }
1566}
1567
1569{
1570 exprt::operandst &operands=expr.operands();
1571
1572 assert(operands.size()==3);
1573
1574 // copy (save) original types
1575 const typet o_type0=operands[0].type();
1576 const typet o_type1=operands[1].type();
1577 const typet o_type2=operands[2].type();
1578
1579 implicit_typecast_bool(operands[0]);
1580
1581 if(o_type1.id() == ID_empty || o_type2.id() == ID_empty)
1582 {
1583 operands[1] = typecast_exprt::conditional_cast(operands[1], void_type());
1584 operands[2] = typecast_exprt::conditional_cast(operands[2], void_type());
1585 expr.type() = void_type();
1586 return;
1587 }
1588
1589 if(operands[1].type().id()==ID_pointer &&
1590 operands[2].type().id()!=ID_pointer)
1591 implicit_typecast(operands[2], operands[1].type());
1592 else if(operands[2].type().id()==ID_pointer &&
1593 operands[1].type().id()!=ID_pointer)
1594 implicit_typecast(operands[1], operands[2].type());
1595
1596 if(operands[1].type().id()==ID_pointer &&
1597 operands[2].type().id()==ID_pointer &&
1598 operands[1].type()!=operands[2].type())
1599 {
1600 exprt tmp1=simplify_expr(operands[1], *this);
1601 exprt tmp2=simplify_expr(operands[2], *this);
1602
1603 // is one of them void * AND null? Convert that to the other.
1604 // (at least that's how GCC behaves)
1605 if(operands[1].type().subtype().id()==ID_empty &&
1606 tmp1.is_constant() &&
1607 to_constant_expr(tmp1).get_value()==ID_NULL)
1608 implicit_typecast(operands[1], operands[2].type());
1609 else if(operands[2].type().subtype().id()==ID_empty &&
1610 tmp2.is_constant() &&
1611 to_constant_expr(tmp2).get_value()==ID_NULL)
1612 implicit_typecast(operands[2], operands[1].type());
1613 else if(operands[1].type().subtype().id()!=ID_code ||
1614 operands[2].type().subtype().id()!=ID_code)
1615 {
1616 // Make it void *.
1617 // gcc and clang issue a warning for this.
1618 expr.type() = pointer_type(void_type());
1619 implicit_typecast(operands[1], expr.type());
1620 implicit_typecast(operands[2], expr.type());
1621 }
1622 else
1623 {
1624 // maybe functions without parameter lists
1625 const code_typet &c_type1=to_code_type(operands[1].type().subtype());
1626 const code_typet &c_type2=to_code_type(operands[2].type().subtype());
1627
1628 if(c_type1.return_type()==c_type2.return_type())
1629 {
1630 if(c_type1.parameters().empty() && c_type1.has_ellipsis())
1631 implicit_typecast(operands[1], operands[2].type());
1632 else if(c_type2.parameters().empty() && c_type2.has_ellipsis())
1633 implicit_typecast(operands[2], operands[1].type());
1634 }
1635 }
1636 }
1637
1638 if(operands[1].type().id()==ID_empty ||
1639 operands[2].type().id()==ID_empty)
1640 {
1641 expr.type()=void_type();
1642 return;
1643 }
1644
1645 if(
1646 operands[1].type() != operands[2].type() ||
1647 operands[1].type().id() == ID_array)
1648 {
1649 implicit_typecast_arithmetic(operands[1], operands[2]);
1650 }
1651
1652 if(operands[1].type() == operands[2].type())
1653 {
1654 expr.type()=operands[1].type();
1655
1656 // GCC says: "A conditional expression is a valid lvalue
1657 // if its type is not void and the true and false branches
1658 // are both valid lvalues."
1659
1660 if(operands[1].get_bool(ID_C_lvalue) &&
1661 operands[2].get_bool(ID_C_lvalue))
1662 expr.set(ID_C_lvalue, true);
1663
1664 return;
1665 }
1666
1668 error() << "operator ?: not defined for types '" << to_string(o_type1)
1669 << "' and '" << to_string(o_type2) << "'" << eom;
1670 throw 0;
1671}
1672
1674 side_effect_exprt &expr)
1675{
1676 // x ? : y is almost the same as x ? x : y,
1677 // but not quite, as x is evaluated only once
1678
1679 exprt::operandst &operands=expr.operands();
1680
1681 if(operands.size()!=2)
1682 {
1684 error() << "gcc conditional_expr expects two operands" << eom;
1685 throw 0;
1686 }
1687
1688 // use typechecking code for "if"
1689
1690 if_exprt if_expr(operands[0], operands[0], operands[1]);
1691 if_expr.add_source_location()=expr.source_location();
1692
1693 typecheck_expr_trinary(if_expr);
1694
1695 // copy the result
1696 operands[0] = if_expr.true_case();
1697 operands[1] = if_expr.false_case();
1698 expr.type()=if_expr.type();
1699}
1700
1702{
1703 exprt &op = to_unary_expr(expr).op();
1704
1705 if(op.type().id()==ID_c_bit_field)
1706 {
1708 error() << "cannot take address of a bit field" << eom;
1709 throw 0;
1710 }
1711
1712 if(op.type().id() == ID_bool)
1713 {
1715 error() << "cannot take address of a single bit" << eom;
1716 throw 0;
1717 }
1718
1719 // special case: address of label
1720 if(op.id()==ID_label)
1721 {
1722 expr.type()=pointer_type(void_type());
1723
1724 // remember the label
1725 labels_used[op.get(ID_identifier)]=op.source_location();
1726 return;
1727 }
1728
1729 // special case: address of function designator
1730 // ANSI-C 99 section 6.3.2.1 paragraph 4
1731
1732 if(
1733 op.id() == ID_address_of && op.get_bool(ID_C_implicit) &&
1734 to_address_of_expr(op).object().type().id() == ID_code)
1735 {
1736 // make the implicit address_of an explicit address_of
1737 exprt tmp;
1738 tmp.swap(op);
1739 tmp.set(ID_C_implicit, false);
1740 expr.swap(tmp);
1741 return;
1742 }
1743
1744 if(op.id()==ID_struct ||
1745 op.id()==ID_union ||
1746 op.id()==ID_array ||
1747 op.id()==ID_string_constant)
1748 {
1749 // these are really objects
1750 }
1751 else if(op.get_bool(ID_C_lvalue))
1752 {
1753 // ok
1754 }
1755 else if(op.type().id()==ID_code)
1756 {
1757 // ok
1758 }
1759 else
1760 {
1762 error() << "address_of error: '" << to_string(op) << "' not an lvalue"
1763 << eom;
1764 throw 0;
1765 }
1766
1767 expr.type()=pointer_type(op.type());
1768}
1769
1771{
1772 exprt &op = to_unary_expr(expr).op();
1773
1774 const typet op_type = op.type();
1775
1776 if(op_type.id()==ID_array)
1777 {
1778 // *a is the same as a[0]
1779 expr.id(ID_index);
1780 expr.type() = to_array_type(op_type).element_type();
1782 assert(expr.operands().size()==2);
1783 }
1784 else if(op_type.id()==ID_pointer)
1785 {
1786 expr.type() = to_pointer_type(op_type).base_type();
1787 }
1788 else
1789 {
1791 error() << "operand of unary * '" << to_string(op)
1792 << "' is not a pointer, but got '" << to_string(op_type) << "'"
1793 << eom;
1794 throw 0;
1795 }
1796
1797 expr.set(ID_C_lvalue, true);
1798
1799 // if you dereference a pointer pointing to
1800 // a function, you get a pointer again
1801 // allowing ******...*p
1802
1804}
1805
1807{
1808 if(expr.type().id()==ID_code)
1809 {
1810 address_of_exprt tmp(expr, pointer_type(expr.type()));
1811 tmp.set(ID_C_implicit, true);
1813 expr=tmp;
1814 }
1815}
1816
1818{
1819 const irep_idt &statement=expr.get_statement();
1820
1821 if(statement==ID_preincrement ||
1822 statement==ID_predecrement ||
1823 statement==ID_postincrement ||
1824 statement==ID_postdecrement)
1825 {
1826 const exprt &op0 = to_unary_expr(expr).op();
1827 const typet &type0=op0.type();
1828
1829 if(!op0.get_bool(ID_C_lvalue))
1830 {
1832 error() << "prefix operator error: '" << to_string(op0)
1833 << "' not an lvalue" << eom;
1834 throw 0;
1835 }
1836
1837 if(type0.get_bool(ID_C_constant))
1838 {
1840 error() << "error: '" << to_string(op0) << "' is constant" << eom;
1841 throw 0;
1842 }
1843
1844 if(type0.id() == ID_c_enum_tag)
1845 {
1846 const c_enum_typet &enum_type = follow_tag(to_c_enum_tag_type(type0));
1847 if(enum_type.is_incomplete())
1848 {
1850 error() << "operator '" << statement << "' given incomplete type '"
1851 << to_string(type0) << "'" << eom;
1852 throw 0;
1853 }
1854
1855 // increment/decrement on underlying type
1856 to_unary_expr(expr).op() =
1857 typecast_exprt(op0, enum_type.underlying_type());
1858 expr.type() = enum_type.underlying_type();
1859 }
1860 else if(type0.id() == ID_c_bit_field)
1861 {
1862 // promote to underlying type
1863 typet underlying_type = to_c_bit_field_type(type0).underlying_type();
1864 to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
1865 expr.type()=underlying_type;
1866 }
1867 else if(type0.id() == ID_bool || type0.id() == ID_c_bool)
1868 {
1870 expr.type() = op0.type();
1871 }
1872 else if(is_numeric_type(type0))
1873 {
1874 expr.type()=type0;
1875 }
1876 else if(type0.id() == ID_pointer)
1877 {
1878 expr.type()=type0;
1880 }
1881 else
1882 {
1884 error() << "operator '" << statement << "' not defined for type '"
1885 << to_string(type0) << "'" << eom;
1886 throw 0;
1887 }
1888 }
1889 else if(has_prefix(id2string(statement), "assign"))
1891 else if(statement==ID_function_call)
1894 else if(statement==ID_statement_expression)
1896 else if(statement==ID_gcc_conditional_expression)
1898 else
1899 {
1901 error() << "unknown side effect: " << statement << eom;
1902 throw 0;
1903 }
1904}
1905
1908{
1909 if(expr.operands().size()!=2)
1910 {
1912 error() << "function_call side effect expects two operands" << eom;
1913 throw 0;
1914 }
1915
1916 exprt &f_op=expr.function();
1917
1918 // f_op is not yet typechecked, in contrast to the other arguments.
1919 // This is a big special case!
1920
1921 if(f_op.id()==ID_symbol)
1922 {
1923 irep_idt identifier=to_symbol_expr(f_op).get_identifier();
1924
1925 asm_label_mapt::const_iterator entry=
1926 asm_label_map.find(identifier);
1927 if(entry!=asm_label_map.end())
1928 identifier=entry->second;
1929
1930 if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
1931 {
1932 // This is an undeclared function.
1933 // Is this a builtin?
1935 {
1936 // yes, it's a builtin
1937 }
1938 else if(
1939 identifier == "__noop" &&
1941 {
1942 // https://docs.microsoft.com/en-us/cpp/intrinsics/noop
1943 // typecheck and discard, just generating 0 instead
1944 for(auto &op : expr.arguments())
1945 typecheck_expr(op);
1946
1948 expr.swap(result);
1949
1950 return;
1951 }
1952 else if(
1953 identifier == "__builtin_shuffle" &&
1955 {
1957 expr.swap(result);
1958
1959 return;
1960 }
1961 else if(
1962 identifier == "__builtin_shufflevector" &&
1964 {
1966 expr.swap(result);
1967
1968 return;
1969 }
1970 else if(
1971 auto gcc_polymorphic = typecheck_gcc_polymorphic_builtin(
1972 identifier, expr.arguments(), f_op.source_location()))
1973 {
1974 irep_idt identifier_with_type = gcc_polymorphic->get_identifier();
1975 auto &parameters = to_code_type(gcc_polymorphic->type()).parameters();
1976 INVARIANT(
1977 !parameters.empty(),
1978 "GCC polymorphic built-ins should have at least one parameter");
1979
1980 // For all atomic/sync polymorphic built-ins (which are the ones handled
1981 // by typecheck_gcc_polymorphic_builtin), looking at the first parameter
1982 // suffices to distinguish different implementations.
1983 if(parameters.front().type().id() == ID_pointer)
1984 {
1985 identifier_with_type = id2string(identifier) + "_" +
1987 parameters.front().type().subtype(), *this);
1988 }
1989 else
1990 {
1991 identifier_with_type =
1992 id2string(identifier) + "_" +
1993 type_to_partial_identifier(parameters.front().type(), *this);
1994 }
1995 gcc_polymorphic->set_identifier(identifier_with_type);
1996
1997 if(!symbol_table.has_symbol(identifier_with_type))
1998 {
1999 for(std::size_t i = 0; i < parameters.size(); ++i)
2000 {
2001 const std::string base_name = "p_" + std::to_string(i);
2002
2003 parameter_symbolt new_symbol;
2004
2005 new_symbol.name =
2006 id2string(identifier_with_type) + "::" + base_name;
2007 new_symbol.base_name = base_name;
2008 new_symbol.location = f_op.source_location();
2009 new_symbol.type = parameters[i].type();
2010 new_symbol.is_parameter = true;
2011 new_symbol.is_lvalue = true;
2012 new_symbol.mode = ID_C;
2013
2014 parameters[i].set_identifier(new_symbol.name);
2015 parameters[i].set_base_name(new_symbol.base_name);
2016
2017 symbol_table.add(new_symbol);
2018 }
2019
2020 symbolt new_symbol;
2021
2022 new_symbol.name = identifier_with_type;
2023 new_symbol.base_name = identifier_with_type;
2024 new_symbol.location = f_op.source_location();
2025 new_symbol.type = gcc_polymorphic->type();
2026 new_symbol.mode = ID_C;
2027 code_blockt implementation =
2028 instantiate_gcc_polymorphic_builtin(identifier, *gcc_polymorphic);
2029 typet parent_return_type = return_type;
2030 return_type = to_code_type(gcc_polymorphic->type()).return_type();
2031 typecheck_code(implementation);
2032 return_type = parent_return_type;
2033 new_symbol.value = implementation;
2034
2035 symbol_table.add(new_symbol);
2036 }
2037
2038 f_op = std::move(*gcc_polymorphic);
2039 }
2040 else
2041 {
2042 // This is an undeclared function that's not a builtin.
2043 // Let's just add it.
2044 // We do a bit of return-type guessing, but just a bit.
2045 typet guessed_return_type = signed_int_type();
2046
2047 // The following isn't really right and sound, but there
2048 // are too many idiots out there who use malloc and the like
2049 // without the right header file.
2050 if(identifier=="malloc" ||
2051 identifier=="realloc" ||
2052 identifier=="reallocf" ||
2053 identifier=="valloc")
2054 {
2055 guessed_return_type = pointer_type(void_type()); // void *
2056 }
2057
2058 symbolt new_symbol;
2059
2060 new_symbol.name=identifier;
2061 new_symbol.base_name=identifier;
2062 new_symbol.location=expr.source_location();
2063 new_symbol.type = code_typet({}, guessed_return_type);
2064 new_symbol.type.set(ID_C_incomplete, true);
2065
2066 // TODO: should also guess some argument types
2067
2068 symbolt *symbol_ptr;
2069 move_symbol(new_symbol, symbol_ptr);
2070
2072 warning() << "function '" << identifier << "' is not declared" << eom;
2073 }
2074 }
2075 }
2076
2077 // typecheck it now
2078 typecheck_expr(f_op);
2079
2080 const typet f_op_type = f_op.type();
2081
2082 if(f_op_type.id() == ID_mathematical_function)
2083 {
2084 const auto &mathematical_function_type =
2086
2087 // check number of arguments
2088 if(expr.arguments().size() != mathematical_function_type.domain().size())
2089 {
2091 error() << "expected " << mathematical_function_type.domain().size()
2092 << " arguments but got " << expr.arguments().size() << eom;
2093 throw 0;
2094 }
2095
2096 // check the types of the arguments
2097 for(auto &p :
2098 make_range(expr.arguments()).zip(mathematical_function_type.domain()))
2099 {
2100 if(p.first.type() != p.second)
2101 {
2102 error().source_location = p.first.source_location();
2103 error() << "expected argument of type " << to_string(p.second)
2104 << " but got " << to_string(p.first.type()) << eom;
2105 throw 0;
2106 }
2107 }
2108
2109 function_application_exprt function_application(f_op, expr.arguments());
2110
2111 function_application.add_source_location() = expr.source_location();
2112
2113 expr.swap(function_application);
2114 return;
2115 }
2116
2117 if(f_op_type.id()!=ID_pointer)
2118 {
2120 error() << "expected function/function pointer as argument but got '"
2121 << to_string(f_op_type) << "'" << eom;
2122 throw 0;
2123 }
2124
2125 // do implicit dereference
2126 if(f_op.id() == ID_address_of && f_op.get_bool(ID_C_implicit))
2127 {
2128 f_op = to_address_of_expr(f_op).object();
2129 }
2130 else
2131 {
2132 dereference_exprt tmp{f_op};
2133 tmp.set(ID_C_implicit, true);
2134 tmp.add_source_location()=f_op.source_location();
2135 f_op.swap(tmp);
2136 }
2137
2138 if(f_op.type().id()!=ID_code)
2139 {
2141 error() << "expected code as argument" << eom;
2142 throw 0;
2143 }
2144
2145 const code_typet &code_type=to_code_type(f_op.type());
2146
2147 expr.type()=code_type.return_type();
2148
2149 exprt tmp=do_special_functions(expr);
2150
2151 if(tmp.is_not_nil())
2152 expr.swap(tmp);
2153 else
2155}
2156
2159{
2160 const exprt &f_op=expr.function();
2161 const source_locationt &source_location=expr.source_location();
2162
2163 // some built-in functions
2164 if(f_op.id()!=ID_symbol)
2165 return nil_exprt();
2166
2167 const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
2168
2169 if(identifier == CPROVER_PREFIX "is_fresh")
2170 {
2171 if(expr.arguments().size() != 2)
2172 {
2174 error() << CPROVER_PREFIX "is_fresh expects two operands; "
2175 << expr.arguments().size() << "provided." << eom;
2176 throw 0;
2177 }
2179 return nil_exprt();
2180 }
2181 else if(identifier == CPROVER_PREFIX "same_object")
2182 {
2183 if(expr.arguments().size()!=2)
2184 {
2186 error() << "same_object expects two operands" << eom;
2187 throw 0;
2188 }
2189
2191
2192 exprt same_object_expr=
2193 same_object(expr.arguments()[0], expr.arguments()[1]);
2194 same_object_expr.add_source_location()=source_location;
2195
2196 return same_object_expr;
2197 }
2198 else if(identifier==CPROVER_PREFIX "get_must")
2199 {
2200 if(expr.arguments().size()!=2)
2201 {
2203 error() << "get_must expects two operands" << eom;
2204 throw 0;
2205 }
2206
2208
2209 binary_predicate_exprt get_must_expr(
2210 expr.arguments()[0], ID_get_must, expr.arguments()[1]);
2211 get_must_expr.add_source_location()=source_location;
2212
2213 return std::move(get_must_expr);
2214 }
2215 else if(identifier==CPROVER_PREFIX "get_may")
2216 {
2217 if(expr.arguments().size()!=2)
2218 {
2220 error() << "get_may expects two operands" << eom;
2221 throw 0;
2222 }
2223
2225
2226 binary_predicate_exprt get_may_expr(
2227 expr.arguments()[0], ID_get_may, expr.arguments()[1]);
2228 get_may_expr.add_source_location()=source_location;
2229
2230 return std::move(get_may_expr);
2231 }
2232 else if(identifier == CPROVER_PREFIX "is_invalid_pointer")
2233 {
2234 if(expr.arguments().size()!=1)
2235 {
2237 error() << "is_invalid_pointer expects one operand" << eom;
2238 throw 0;
2239 }
2240
2242
2243 exprt same_object_expr = is_invalid_pointer_exprt{expr.arguments().front()};
2244 same_object_expr.add_source_location()=source_location;
2245
2246 return same_object_expr;
2247 }
2248 else if(identifier==CPROVER_PREFIX "buffer_size")
2249 {
2250 if(expr.arguments().size()!=1)
2251 {
2253 error() << "buffer_size expects one operand" << eom;
2254 throw 0;
2255 }
2256
2258
2259 exprt buffer_size_expr("buffer_size", size_type());
2260 buffer_size_expr.operands()=expr.arguments();
2261 buffer_size_expr.add_source_location()=source_location;
2262
2263 return buffer_size_expr;
2264 }
2265 else if(identifier==CPROVER_PREFIX "is_zero_string")
2266 {
2267 if(expr.arguments().size()!=1)
2268 {
2270 error() << "is_zero_string expects one operand" << eom;
2271 throw 0;
2272 }
2273
2275
2276 unary_exprt is_zero_string_expr(
2277 "is_zero_string", expr.arguments()[0], c_bool_type());
2278 is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
2279 is_zero_string_expr.add_source_location()=source_location;
2280
2281 return std::move(is_zero_string_expr);
2282 }
2283 else if(identifier==CPROVER_PREFIX "zero_string_length")
2284 {
2285 if(expr.arguments().size()!=1)
2286 {
2288 error() << "zero_string_length expects one operand" << eom;
2289 throw 0;
2290 }
2291
2293
2294 exprt zero_string_length_expr("zero_string_length", size_type());
2295 zero_string_length_expr.operands()=expr.arguments();
2296 zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
2297 zero_string_length_expr.add_source_location()=source_location;
2298
2299 return zero_string_length_expr;
2300 }
2301 else if(identifier==CPROVER_PREFIX "DYNAMIC_OBJECT")
2302 {
2303 if(expr.arguments().size()!=1)
2304 {
2306 error() << "dynamic_object expects one argument" << eom;
2307 throw 0;
2308 }
2309
2311
2312 exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]);
2313 is_dynamic_object_expr.add_source_location() = source_location;
2314
2315 return is_dynamic_object_expr;
2316 }
2317 else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
2318 {
2319 if(expr.arguments().size()!=1)
2320 {
2322 error() << "pointer_offset expects one argument" << eom;
2323 throw 0;
2324 }
2325
2327
2328 exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
2329 pointer_offset_expr.add_source_location()=source_location;
2330
2331 return typecast_exprt::conditional_cast(pointer_offset_expr, expr.type());
2332 }
2333 else if(identifier == CPROVER_PREFIX "OBJECT_SIZE")
2334 {
2335 if(expr.arguments().size() != 1)
2336 {
2338 error() << "object_size expects one operand" << eom;
2339 throw 0;
2340 }
2341
2343
2344 unary_exprt object_size_expr(
2345 ID_object_size, expr.arguments()[0], size_type());
2346 object_size_expr.add_source_location() = source_location;
2347
2348 return std::move(object_size_expr);
2349 }
2350 else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
2351 {
2352 if(expr.arguments().size()!=1)
2353 {
2355 error() << "pointer_object expects one argument" << eom;
2356 throw 0;
2357 }
2358
2360
2361 exprt pointer_object_expr = pointer_object(expr.arguments().front());
2362 pointer_object_expr.add_source_location() = source_location;
2363
2364 return typecast_exprt::conditional_cast(pointer_object_expr, expr.type());
2365 }
2366 else if(identifier=="__builtin_bswap16" ||
2367 identifier=="__builtin_bswap32" ||
2368 identifier=="__builtin_bswap64")
2369 {
2370 if(expr.arguments().size()!=1)
2371 {
2373 error() << identifier << " expects one operand" << eom;
2374 throw 0;
2375 }
2376
2378
2379 // these are hard-wired to 8 bits according to the gcc manual
2380 bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
2381 bswap_expr.add_source_location()=source_location;
2382
2383 return std::move(bswap_expr);
2384 }
2385 else if(
2386 identifier == "__builtin_rotateleft8" ||
2387 identifier == "__builtin_rotateleft16" ||
2388 identifier == "__builtin_rotateleft32" ||
2389 identifier == "__builtin_rotateleft64" ||
2390 identifier == "__builtin_rotateright8" ||
2391 identifier == "__builtin_rotateright16" ||
2392 identifier == "__builtin_rotateright32" ||
2393 identifier == "__builtin_rotateright64")
2394 {
2395 // clang only
2396 if(expr.arguments().size() != 2)
2397 {
2399 error() << identifier << " expects two operands" << eom;
2400 throw 0;
2401 }
2402
2404
2405 irep_idt id = (identifier == "__builtin_rotateleft8" ||
2406 identifier == "__builtin_rotateleft16" ||
2407 identifier == "__builtin_rotateleft32" ||
2408 identifier == "__builtin_rotateleft64")
2409 ? ID_rol
2410 : ID_ror;
2411
2412 shift_exprt rotate_expr(expr.arguments()[0], id, expr.arguments()[1]);
2413 rotate_expr.add_source_location() = source_location;
2414
2415 return std::move(rotate_expr);
2416 }
2417 else if(identifier=="__builtin_nontemporal_load")
2418 {
2419 if(expr.arguments().size()!=1)
2420 {
2422 error() << identifier << " expects one operand" << eom;
2423 throw 0;
2424 }
2425
2427
2428 // these return the subtype of the argument
2429 exprt &ptr_arg=expr.arguments().front();
2430
2431 if(ptr_arg.type().id()!=ID_pointer)
2432 {
2434 error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
2435 throw 0;
2436 }
2437
2438 expr.type()=expr.arguments().front().type().subtype();
2439
2440 return expr;
2441 }
2442 else if(
2443 identifier == "__builtin_fpclassify" ||
2444 identifier == CPROVER_PREFIX "fpclassify")
2445 {
2446 if(expr.arguments().size() != 6)
2447 {
2449 error() << identifier << " expects six arguments" << eom;
2450 throw 0;
2451 }
2452
2454
2455 // This gets 5 integers followed by a float or double.
2456 // The five integers are the return values for the cases
2457 // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
2458 // gcc expects this to be able to produce compile-time constants.
2459
2460 const exprt &fp_value = expr.arguments()[5];
2461
2462 if(fp_value.type().id() != ID_floatbv)
2463 {
2464 error().source_location = fp_value.source_location();
2465 error() << "non-floating-point argument for " << identifier << eom;
2466 throw 0;
2467 }
2468
2469 const auto &floatbv_type = to_floatbv_type(fp_value.type());
2470
2471 const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();
2472
2473 const auto &arguments = expr.arguments();
2474
2475 return if_exprt(
2476 isnan_exprt(fp_value),
2477 arguments[0],
2478 if_exprt(
2479 isinf_exprt(fp_value),
2480 arguments[1],
2481 if_exprt(
2482 isnormal_exprt(fp_value),
2483 arguments[2],
2484 if_exprt(
2485 ieee_float_equal_exprt(fp_value, zero),
2486 arguments[4],
2487 arguments[3])))); // subnormal
2488 }
2489 else if(identifier==CPROVER_PREFIX "isnanf" ||
2490 identifier==CPROVER_PREFIX "isnand" ||
2491 identifier==CPROVER_PREFIX "isnanld" ||
2492 identifier=="__builtin_isnan")
2493 {
2494 if(expr.arguments().size()!=1)
2495 {
2497 error() << "isnan expects one operand" << eom;
2498 throw 0;
2499 }
2500
2502
2503 isnan_exprt isnan_expr(expr.arguments().front());
2504 isnan_expr.add_source_location()=source_location;
2505
2506 return typecast_exprt::conditional_cast(isnan_expr, expr.type());
2507 }
2508 else if(identifier==CPROVER_PREFIX "isfinitef" ||
2509 identifier==CPROVER_PREFIX "isfinited" ||
2510 identifier==CPROVER_PREFIX "isfiniteld")
2511 {
2512 if(expr.arguments().size()!=1)
2513 {
2515 error() << "isfinite expects one operand" << eom;
2516 throw 0;
2517 }
2518
2520
2521 isfinite_exprt isfinite_expr(expr.arguments().front());
2522 isfinite_expr.add_source_location()=source_location;
2523
2524 return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
2525 }
2526 else if(identifier==CPROVER_PREFIX "inf" ||
2527 identifier=="__builtin_inf")
2528 {
2529 constant_exprt inf_expr=
2532 inf_expr.add_source_location()=source_location;
2533
2534 return std::move(inf_expr);
2535 }
2536 else if(identifier==CPROVER_PREFIX "inff")
2537 {
2538 constant_exprt inff_expr=
2541 inff_expr.add_source_location()=source_location;
2542
2543 return std::move(inff_expr);
2544 }
2545 else if(identifier==CPROVER_PREFIX "infl")
2546 {
2548 constant_exprt infl_expr=
2550 infl_expr.add_source_location()=source_location;
2551
2552 return std::move(infl_expr);
2553 }
2554 else if(identifier==CPROVER_PREFIX "abs" ||
2555 identifier==CPROVER_PREFIX "labs" ||
2556 identifier==CPROVER_PREFIX "llabs" ||
2557 identifier==CPROVER_PREFIX "fabs" ||
2558 identifier==CPROVER_PREFIX "fabsf" ||
2559 identifier==CPROVER_PREFIX "fabsl")
2560 {
2561 if(expr.arguments().size()!=1)
2562 {
2564 error() << "abs-functions expect one operand" << eom;
2565 throw 0;
2566 }
2567
2569
2570 abs_exprt abs_expr(expr.arguments().front());
2571 abs_expr.add_source_location()=source_location;
2572
2573 return std::move(abs_expr);
2574 }
2575 else if(
2576 identifier == CPROVER_PREFIX "fmod" ||
2577 identifier == CPROVER_PREFIX "fmodf" ||
2578 identifier == CPROVER_PREFIX "fmodl")
2579 {
2580 if(expr.arguments().size() != 2)
2581 {
2583 error() << "fmod-functions expect two operands" << eom;
2584 throw 0;
2585 }
2586
2588
2589 // Note that the semantics differ from the
2590 // "floating point remainder" operation as defined by IEEE.
2591 // Note that these do not take a rounding mode.
2592 binary_exprt fmod_expr(
2593 expr.arguments()[0], ID_floatbv_mod, expr.arguments()[1]);
2594
2595 fmod_expr.add_source_location() = source_location;
2596
2597 return std::move(fmod_expr);
2598 }
2599 else if(
2600 identifier == CPROVER_PREFIX "remainder" ||
2601 identifier == CPROVER_PREFIX "remainderf" ||
2602 identifier == CPROVER_PREFIX "remainderl")
2603 {
2604 if(expr.arguments().size() != 2)
2605 {
2607 error() << "remainder-functions expect two operands" << eom;
2608 throw 0;
2609 }
2610
2612
2613 // The semantics of these functions is meant to match the
2614 // "floating point remainder" operation as defined by IEEE.
2615 // Note that these do not take a rounding mode.
2616 binary_exprt floatbv_rem_expr(
2617 expr.arguments()[0], ID_floatbv_rem, expr.arguments()[1]);
2618
2619 floatbv_rem_expr.add_source_location() = source_location;
2620
2621 return std::move(floatbv_rem_expr);
2622 }
2623 else if(identifier==CPROVER_PREFIX "allocate")
2624 {
2625 if(expr.arguments().size()!=2)
2626 {
2628 error() << "allocate expects two operands" << eom;
2629 throw 0;
2630 }
2631
2633
2634 side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
2635 malloc_expr.operands()=expr.arguments();
2636
2637 return std::move(malloc_expr);
2638 }
2639 else if(
2640 identifier == CPROVER_PREFIX "r_ok" ||
2641 identifier == CPROVER_PREFIX "w_ok" || identifier == CPROVER_PREFIX "rw_ok")
2642 {
2643 if(expr.arguments().size() != 1 && expr.arguments().size() != 2)
2644 {
2646 error() << identifier << " expects one or two operands" << eom;
2647 throw 0;
2648 }
2649
2651
2652 // the first argument must be a pointer
2653 const auto &pointer_expr = expr.arguments()[0];
2654 if(pointer_expr.type().id() != ID_pointer)
2655 {
2657 error() << identifier << " expects a pointer as first argument" << eom;
2658 throw 0;
2659 }
2660
2661 // The second argument, when given, is a size_t.
2662 // When not given, use the pointer subtype.
2663 exprt size_expr;
2664
2665 if(expr.arguments().size() == 2)
2666 {
2668 size_expr = expr.arguments()[1];
2669 }
2670 else
2671 {
2672 // Won't do void *
2673 const auto &subtype = to_pointer_type(pointer_expr.type()).base_type();
2674 if(subtype.id() == ID_empty)
2675 {
2677 error() << identifier << " expects a size when given a void pointer"
2678 << eom;
2679 throw 0;
2680 }
2681
2682 auto size_expr_opt = size_of_expr(subtype, *this);
2683 if(!size_expr_opt.has_value())
2684 {
2686 error() << identifier << " was given object pointer without size"
2687 << eom;
2688 throw 0;
2689 }
2690
2691 size_expr = std::move(size_expr_opt.value());
2692 }
2693
2694 irep_idt id = identifier == CPROVER_PREFIX "r_ok"
2695 ? ID_r_ok
2696 : identifier == CPROVER_PREFIX "w_ok" ? ID_w_ok : ID_rw_ok;
2697
2698 r_or_w_ok_exprt ok_expr(id, pointer_expr, size_expr);
2699 ok_expr.add_source_location() = source_location;
2700
2701 return std::move(ok_expr);
2702 }
2703 else if(
2704 (identifier == CPROVER_PREFIX "old") ||
2705 (identifier == CPROVER_PREFIX "loop_entry"))
2706 {
2707 if(expr.arguments().size() != 1)
2708 {
2710 error() << identifier << " expects one operand" << eom;
2711 throw 0;
2712 }
2713
2714 irep_idt id = identifier == CPROVER_PREFIX "old" ? ID_old : ID_loop_entry;
2715
2716 history_exprt old_expr(expr.arguments()[0], id);
2717 old_expr.add_source_location() = source_location;
2718
2719 return std::move(old_expr);
2720 }
2721 else if(identifier==CPROVER_PREFIX "isinff" ||
2722 identifier==CPROVER_PREFIX "isinfd" ||
2723 identifier==CPROVER_PREFIX "isinfld" ||
2724 identifier=="__builtin_isinf")
2725 {
2726 if(expr.arguments().size()!=1)
2727 {
2729 error() << identifier << " expects one operand" << eom;
2730 throw 0;
2731 }
2732
2734
2735 const exprt &fp_value = expr.arguments().front();
2736
2737 if(fp_value.type().id() != ID_floatbv)
2738 {
2739 error().source_location = fp_value.source_location();
2740 error() << "non-floating-point argument for " << identifier << eom;
2741 throw 0;
2742 }
2743
2744 isinf_exprt isinf_expr(expr.arguments().front());
2745 isinf_expr.add_source_location()=source_location;
2746
2747 return typecast_exprt::conditional_cast(isinf_expr, expr.type());
2748 }
2749 else if(identifier == "__builtin_isinf_sign")
2750 {
2751 if(expr.arguments().size() != 1)
2752 {
2754 error() << identifier << " expects one operand" << eom;
2755 throw 0;
2756 }
2757
2759
2760 // returns 1 for +inf and -1 for -inf, and 0 otherwise
2761
2762 const exprt &fp_value = expr.arguments().front();
2763
2764 if(fp_value.type().id() != ID_floatbv)
2765 {
2766 error().source_location = fp_value.source_location();
2767 error() << "non-floating-point argument for " << identifier << eom;
2768 throw 0;
2769 }
2770
2771 isinf_exprt isinf_expr(fp_value);
2772 isinf_expr.add_source_location() = source_location;
2773
2774 return if_exprt(
2775 isinf_exprt(fp_value),
2776 if_exprt(
2777 sign_exprt(fp_value),
2778 from_integer(-1, expr.type()),
2779 from_integer(1, expr.type())),
2780 from_integer(0, expr.type()));
2781 }
2782 else if(identifier == CPROVER_PREFIX "isnormalf" ||
2783 identifier == CPROVER_PREFIX "isnormald" ||
2784 identifier == CPROVER_PREFIX "isnormalld" ||
2785 identifier == "__builtin_isnormal")
2786 {
2787 if(expr.arguments().size()!=1)
2788 {
2790 error() << identifier << " expects one operand" << eom;
2791 throw 0;
2792 }
2793
2795
2796 const exprt &fp_value = expr.arguments()[0];
2797
2798 if(fp_value.type().id() != ID_floatbv)
2799 {
2800 error().source_location = fp_value.source_location();
2801 error() << "non-floating-point argument for " << identifier << eom;
2802 throw 0;
2803 }
2804
2805 isnormal_exprt isnormal_expr(expr.arguments().front());
2806 isnormal_expr.add_source_location()=source_location;
2807
2808 return typecast_exprt::conditional_cast(isnormal_expr, expr.type());
2809 }
2810 else if(identifier==CPROVER_PREFIX "signf" ||
2811 identifier==CPROVER_PREFIX "signd" ||
2812 identifier==CPROVER_PREFIX "signld" ||
2813 identifier=="__builtin_signbit" ||
2814 identifier=="__builtin_signbitf" ||
2815 identifier=="__builtin_signbitl")
2816 {
2817 if(expr.arguments().size()!=1)
2818 {
2820 error() << identifier << " expects one operand" << eom;
2821 throw 0;
2822 }
2823
2825
2826 sign_exprt sign_expr(expr.arguments().front());
2827 sign_expr.add_source_location()=source_location;
2828
2829 return typecast_exprt::conditional_cast(sign_expr, expr.type());
2830 }
2831 else if(identifier=="__builtin_popcount" ||
2832 identifier=="__builtin_popcountl" ||
2833 identifier=="__builtin_popcountll" ||
2834 identifier=="__popcnt16" ||
2835 identifier=="__popcnt" ||
2836 identifier=="__popcnt64")
2837 {
2838 if(expr.arguments().size()!=1)
2839 {
2841 error() << identifier << " expects one operand" << eom;
2842 throw 0;
2843 }
2844
2846
2847 popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
2848 popcount_expr.add_source_location()=source_location;
2849
2850 return std::move(popcount_expr);
2851 }
2852 else if(
2853 identifier == "__builtin_clz" || identifier == "__builtin_clzl" ||
2854 identifier == "__builtin_clzll" || identifier == "__lzcnt16" ||
2855 identifier == "__lzcnt" || identifier == "__lzcnt64")
2856 {
2857 if(expr.arguments().size() != 1)
2858 {
2860 error() << identifier << " expects one operand" << eom;
2861 throw 0;
2862 }
2863
2865
2866 count_leading_zeros_exprt clz{expr.arguments().front(),
2867 has_prefix(id2string(identifier), "__lzcnt"),
2868 expr.type()};
2869 clz.add_source_location() = source_location;
2870
2871 return std::move(clz);
2872 }
2873 else if(
2874 identifier == "__builtin_ctz" || identifier == "__builtin_ctzl" ||
2875 identifier == "__builtin_ctzll")
2876 {
2877 if(expr.arguments().size() != 1)
2878 {
2880 error() << identifier << " expects one operand" << eom;
2881 throw 0;
2882 }
2883
2885
2887 expr.arguments().front(), false, expr.type()};
2888 ctz.add_source_location() = source_location;
2889
2890 return std::move(ctz);
2891 }
2892 else if(identifier==CPROVER_PREFIX "equal")
2893 {
2894 if(expr.arguments().size()!=2)
2895 {
2897 error() << "equal expects two operands" << eom;
2898 throw 0;
2899 }
2900
2902
2903 equal_exprt equality_expr(
2904 expr.arguments().front(), expr.arguments().back());
2905 equality_expr.add_source_location()=source_location;
2906
2907 if(equality_expr.lhs().type() != equality_expr.rhs().type())
2908 {
2910 error() << "equal expects two operands of same type" << eom;
2911 throw 0;
2912 }
2913
2914 return std::move(equality_expr);
2915 }
2916 else if(identifier=="__builtin_expect")
2917 {
2918 // This is a gcc extension to provide branch prediction.
2919 // We compile it away, but adding some IR instruction for
2920 // this would clearly be an option. Note that the type
2921 // of the return value is wired to "long", i.e.,
2922 // this may trigger a type conversion due to the signature
2923 // of this function.
2924 if(expr.arguments().size()!=2)
2925 {
2927 error() << "__builtin_expect expects two arguments" << eom;
2928 throw 0;
2929 }
2930
2932
2933 return typecast_exprt(expr.arguments()[0], expr.type());
2934 }
2935 else if(identifier=="__builtin_object_size")
2936 {
2937 // this is a gcc extension to provide information about
2938 // object sizes at compile time
2939 // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
2940
2941 if(expr.arguments().size()!=2)
2942 {
2944 error() << "__builtin_object_size expects two arguments" << eom;
2945 throw 0;
2946 }
2947
2949
2950 make_constant(expr.arguments()[1]);
2951
2952 mp_integer arg1;
2953
2954 if(expr.arguments()[1].is_true())
2955 arg1=1;
2956 else if(expr.arguments()[1].is_false())
2957 arg1=0;
2958 else if(to_integer(to_constant_expr(expr.arguments()[1]), arg1))
2959 {
2961 error() << "__builtin_object_size expects constant as second argument, "
2962 << "but got " << to_string(expr.arguments()[1]) << eom;
2963 throw 0;
2964 }
2965
2966 exprt tmp;
2967
2968 // the following means "don't know"
2969 if(arg1==0 || arg1==1)
2970 {
2971 tmp=from_integer(-1, size_type());
2973 }
2974 else
2975 {
2976 tmp=from_integer(0, size_type());
2978 }
2979
2980 return tmp;
2981 }
2982 else if(identifier=="__builtin_choose_expr")
2983 {
2984 // this is a gcc extension similar to ?:
2985 if(expr.arguments().size()!=3)
2986 {
2988 error() << "__builtin_choose_expr expects three arguments" << eom;
2989 throw 0;
2990 }
2991
2993
2994 exprt arg0 =
2996 make_constant(arg0);
2997
2998 if(arg0.is_true())
2999 return expr.arguments()[1];
3000 else
3001 return expr.arguments()[2];
3002 }
3003 else if(identifier=="__builtin_constant_p")
3004 {
3005 // this is a gcc extension to tell whether the argument
3006 // is known to be a compile-time constant
3007 if(expr.arguments().size()!=1)
3008 {
3010 error() << "__builtin_constant_p expects one argument" << eom;
3011 throw 0;
3012 }
3013
3014 // do not typecheck the argument - it is never evaluated, and thus side
3015 // effects must not show up either
3016
3017 // try to produce constant
3018 exprt tmp1=expr.arguments().front();
3019 simplify(tmp1, *this);
3020
3021 bool is_constant=false;
3022
3023 // Need to do some special treatment for string literals,
3024 // which are (void *)&("lit"[0])
3025 if(
3026 tmp1.id() == ID_typecast &&
3027 to_typecast_expr(tmp1).op().id() == ID_address_of &&
3028 to_address_of_expr(to_typecast_expr(tmp1).op()).object().id() ==
3029 ID_index &&
3031 .array()
3032 .id() == ID_string_constant)
3033 {
3034 is_constant=true;
3035 }
3036 else
3037 is_constant=tmp1.is_constant();
3038
3039 exprt tmp2=from_integer(is_constant, expr.type());
3040 tmp2.add_source_location()=source_location;
3041
3042 return tmp2;
3043 }
3044 else if(identifier=="__builtin_classify_type")
3045 {
3046 // This is a gcc/clang extension that produces an integer
3047 // constant for the type of the argument expression.
3048 if(expr.arguments().size()!=1)
3049 {
3051 error() << "__builtin_classify_type expects one argument" << eom;
3052 throw 0;
3053 }
3054
3056
3057 exprt object=expr.arguments()[0];
3058
3059 // The value doesn't matter at all, we only care about the type.
3060 // Need to sync with typeclass.h.
3061 typet type = follow(object.type());
3062
3063 // use underlying type for bit fields
3064 if(type.id() == ID_c_bit_field)
3065 type = to_c_bit_field_type(type).underlying_type();
3066
3067 unsigned type_number;
3068
3069 if(type.id() == ID_bool || type.id() == ID_c_bool)
3070 {
3071 // clang returns 4 for _Bool, gcc treats these as 'int'.
3072 type_number =
3074 ? 4u
3075 : 1u;
3076 }
3077 else
3078 {
3079 type_number =
3080 type.id() == ID_empty
3081 ? 0u
3082 : (type.id() == ID_bool || type.id() == ID_c_bool)
3083 ? 4u
3084 : (type.id() == ID_pointer || type.id() == ID_array)
3085 ? 5u
3086 : type.id() == ID_floatbv
3087 ? 8u
3088 : (type.id() == ID_complex && type.subtype().id() == ID_floatbv)
3089 ? 9u
3090 : type.id() == ID_struct
3091 ? 12u
3092 : type.id() == ID_union
3093 ? 13u
3094 : 1u; // int, short, char, enum_tag
3095 }
3096
3097 exprt tmp=from_integer(type_number, expr.type());
3098 tmp.add_source_location()=source_location;
3099
3100 return tmp;
3101 }
3102 else if(
3103 identifier == CPROVER_PREFIX "overflow_minus" ||
3104 identifier == CPROVER_PREFIX "overflow_mult" ||
3105 identifier == CPROVER_PREFIX "overflow_plus" ||
3106 identifier == CPROVER_PREFIX "overflow_shl")
3107 {
3108 exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
3109 overflow.add_source_location() = f_op.source_location();
3110
3111 if(identifier == CPROVER_PREFIX "overflow_minus")
3112 {
3113 overflow.id(ID_minus);
3115 }
3116 else if(identifier == CPROVER_PREFIX "overflow_mult")
3117 {
3118 overflow.id(ID_mult);
3120 }
3121 else if(identifier == CPROVER_PREFIX "overflow_plus")
3122 {
3123 overflow.id(ID_plus);
3125 }
3126 else if(identifier == CPROVER_PREFIX "overflow_shl")
3127 {
3128 overflow.id(ID_shl);
3130 }
3131
3133 overflow.operands()[0], overflow.id(), overflow.operands()[1]};
3134 of.add_source_location() = overflow.source_location();
3135 return std::move(of);
3136 }
3137 else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
3138 {
3139 exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
3140 tmp.add_source_location() = f_op.source_location();
3141
3143
3144 unary_overflow_exprt overflow{ID_unary_minus, tmp.operands().front()};
3145 overflow.add_source_location() = tmp.source_location();
3146 return std::move(overflow);
3147 }
3148 else if(identifier == CPROVER_PREFIX "enum_is_in_range")
3149 {
3150 // Check correct number of arguments
3151 if(expr.arguments().size() != 1)
3152 {
3153 std::ostringstream error_message;
3154 error_message << expr.source_location().as_string() << ": " << identifier
3155 << " takes exactly 1 argument, but "
3156 << expr.arguments().size() << " were provided";
3157 throw invalid_source_file_exceptiont{error_message.str()};
3158 }
3159 auto arg1 = expr.arguments()[0];
3160 typecheck_expr(arg1);
3161 if(!can_cast_type<c_enum_tag_typet>(arg1.type()))
3162 {
3163 // Can't enum range check a non-enum
3164 std::ostringstream error_message;
3165 error_message << expr.source_location().as_string() << ": " << identifier
3166 << " expects enum, but (" << expr2c(arg1, *this)
3167 << ") has type `" << type2c(arg1.type(), *this) << '`';
3168 throw invalid_source_file_exceptiont{error_message.str()};
3169 }
3170 else
3171 {
3172 return expr;
3173 }
3174 }
3175 else if(
3176 identifier == "__builtin_add_overflow" ||
3177 identifier == "__builtin_sadd_overflow" ||
3178 identifier == "__builtin_saddl_overflow" ||
3179 identifier == "__builtin_saddll_overflow" ||
3180 identifier == "__builtin_uadd_overflow" ||
3181 identifier == "__builtin_uaddl_overflow" ||
3182 identifier == "__builtin_uaddll_overflow" ||
3183 identifier == "__builtin_add_overflow_p")
3184 {
3185 return typecheck_builtin_overflow(expr, ID_plus);
3186 }
3187 else if(
3188 identifier == "__builtin_sub_overflow" ||
3189 identifier == "__builtin_ssub_overflow" ||
3190 identifier == "__builtin_ssubl_overflow" ||
3191 identifier == "__builtin_ssubll_overflow" ||
3192 identifier == "__builtin_usub_overflow" ||
3193 identifier == "__builtin_usubl_overflow" ||
3194 identifier == "__builtin_usubll_overflow" ||
3195 identifier == "__builtin_sub_overflow_p")
3196 {
3197 return typecheck_builtin_overflow(expr, ID_minus);
3198 }
3199 else if(
3200 identifier == "__builtin_mul_overflow" ||
3201 identifier == "__builtin_smul_overflow" ||
3202 identifier == "__builtin_smull_overflow" ||
3203 identifier == "__builtin_smulll_overflow" ||
3204 identifier == "__builtin_umul_overflow" ||
3205 identifier == "__builtin_umull_overflow" ||
3206 identifier == "__builtin_umulll_overflow" ||
3207 identifier == "__builtin_mul_overflow_p")
3208 {
3209 return typecheck_builtin_overflow(expr, ID_mult);
3210 }
3211 else if(
3212 identifier == "__builtin_bitreverse8" ||
3213 identifier == "__builtin_bitreverse16" ||
3214 identifier == "__builtin_bitreverse32" ||
3215 identifier == "__builtin_bitreverse64")
3216 {
3217 // clang only
3218 if(expr.arguments().size() != 1)
3219 {
3220 std::ostringstream error_message;
3221 error_message << expr.source_location().as_string()
3222 << ": error: " << identifier << " expects one operand";
3223 throw invalid_source_file_exceptiont{error_message.str()};
3224 }
3225
3227
3228 bitreverse_exprt bitreverse{expr.arguments()[0]};
3229 bitreverse.add_source_location() = source_location;
3230
3231 return std::move(bitreverse);
3232 }
3233 else
3234 return nil_exprt();
3235 // NOLINTNEXTLINE(readability/fn_size)
3236}
3237
3240 const irep_idt &arith_op)
3241{
3242 const irep_idt &identifier = to_symbol_expr(expr.function()).get_identifier();
3243
3244 // check function signature
3245 if(expr.arguments().size() != 3)
3246 {
3247 std::ostringstream error_message;
3248 error_message << expr.source_location().as_string() << ": " << identifier
3249 << " takes exactly 3 arguments, but "
3250 << expr.arguments().size() << " were provided";
3251 throw invalid_source_file_exceptiont{error_message.str()};
3252 }
3253
3255
3256 auto lhs = expr.arguments()[0];
3257 auto rhs = expr.arguments()[1];
3258 auto result = expr.arguments()[2];
3259
3260 const bool is__p_variant = has_suffix(id2string(identifier), "_p");
3261
3262 {
3263 auto const raise_wrong_argument_error =
3264 [this, identifier](
3265 const exprt &wrong_argument, std::size_t argument_number, bool _p) {
3266 std::ostringstream error_message;
3267 error_message << wrong_argument.source_location().as_string() << ": "
3268 << identifier << " has signature " << identifier
3269 << "(integral, integral, integral" << (_p ? "" : "*")
3270 << "), "
3271 << "but argument " << argument_number << " ("
3272 << expr2c(wrong_argument, *this) << ") has type `"
3273 << type2c(wrong_argument.type(), *this) << '`';
3274 throw invalid_source_file_exceptiont{error_message.str()};
3275 };
3276 for(int arg_index = 0; arg_index <= (!is__p_variant ? 1 : 2); ++arg_index)
3277 {
3278 auto const &argument = expr.arguments()[arg_index];
3279
3280 if(!is_signed_or_unsigned_bitvector(argument.type()))
3281 {
3282 raise_wrong_argument_error(argument, arg_index + 1, is__p_variant);
3283 }
3284 }
3285 if(
3286 !is__p_variant &&
3287 (result.type().id() != ID_pointer ||
3288 !is_signed_or_unsigned_bitvector(result.type().subtype())))
3289 {
3290 raise_wrong_argument_error(result, 3, is__p_variant);
3291 }
3292 }
3293
3294 return side_effect_expr_overflowt{arith_op,
3295 std::move(lhs),
3296 std::move(rhs),
3297 std::move(result),
3298 expr.source_location()};
3299}
3300
3305{
3306 const exprt &f_op=expr.function();
3307 const code_typet &code_type=to_code_type(f_op.type());
3308 exprt::operandst &arguments=expr.arguments();
3309 const code_typet::parameterst &parameter_types=
3310 code_type.parameters();
3311
3312 // no. of arguments test
3313
3314 if(code_type.get_bool(ID_C_incomplete))
3315 {
3316 // can't check
3317 }
3318 else if(code_type.is_KnR())
3319 {
3320 // We are generous on KnR; any number is ok.
3321 // We will in missing ones with "NIL".
3322
3323 while(parameter_types.size()>arguments.size())
3324 arguments.push_back(nil_exprt());
3325 }
3326 else if(code_type.has_ellipsis())
3327 {
3328 if(parameter_types.size()>arguments.size())
3329 {
3331 error() << "not enough function arguments" << eom;
3332 throw 0;
3333 }
3334 }
3335 else if(parameter_types.size()!=arguments.size())
3336 {
3338 error() << "wrong number of function arguments: "
3339 << "expected " << parameter_types.size()
3340 << ", but got " << arguments.size() << eom;
3341 throw 0;
3342 }
3343
3344 for(std::size_t i=0; i<arguments.size(); i++)
3345 {
3346 exprt &op=arguments[i];
3347
3348 if(op.is_nil())
3349 {
3350 // ignore
3351 }
3352 else if(i<parameter_types.size())
3353 {
3354 const code_typet::parametert &parameter_type=
3355 parameter_types[i];
3356
3357 const typet &op_type=parameter_type.type();
3358
3359 if(op_type.id()==ID_bool &&
3360 op.id()==ID_side_effect &&
3361 op.get(ID_statement)==ID_assign &&
3362 op.type().id()!=ID_bool)
3363 {
3365 warning() << "assignment where Boolean argument is expected" << eom;
3366 }
3367
3368 implicit_typecast(op, op_type);
3369 }
3370 else
3371 {
3372 // don't know type, just do standard conversion
3373
3374 if(op.type().id() == ID_array)
3375 {
3376 typet dest_type=pointer_type(void_type());
3377 dest_type.subtype().set(ID_C_constant, true);
3378 implicit_typecast(op, dest_type);
3379 }
3380 }
3381 }
3382}
3383
3385{
3386 // nothing to do
3387}
3388
3390{
3391 exprt &operand = to_unary_expr(expr).op();
3392
3393 const typet &o_type = operand.type();
3394
3395 if(o_type.id()==ID_vector)
3396 {
3397 if(is_number(to_vector_type(o_type).element_type()))
3398 {
3399 // Vector arithmetic.
3400 expr.type()=operand.type();
3401 return;
3402 }
3403 }
3404
3406
3407 if(is_number(operand.type()))
3408 {
3409 expr.type()=operand.type();
3410 return;
3411 }
3412
3414 error() << "operator '" << expr.id() << "' not defined for type '"
3415 << to_string(operand.type()) << "'" << eom;
3416 throw 0;
3417}
3418
3420{
3422
3423 // This is not quite accurate: the standard says the result
3424 // should be of type 'int'.
3425 // We do 'bool' anyway to get more compact formulae. Eventually,
3426 // this should be achieved by means of simplification, and not
3427 // in the frontend.
3428 expr.type()=bool_typet();
3429}
3430
3432 const vector_typet &type0,
3433 const vector_typet &type1)
3434{
3435 // This is relatively restrictive!
3436
3437 // compare dimension
3438 const auto s0 = numeric_cast<mp_integer>(type0.size());
3439 const auto s1 = numeric_cast<mp_integer>(type1.size());
3440 if(!s0.has_value())
3441 return false;
3442 if(!s1.has_value())
3443 return false;
3444 if(*s0 != *s1)
3445 return false;
3446
3447 // compare subtype
3448 if(
3449 (type0.element_type().id() == ID_signedbv ||
3450 type0.element_type().id() == ID_unsignedbv) &&
3451 (type1.element_type().id() == ID_signedbv ||
3452 type1.element_type().id() == ID_unsignedbv) &&
3455 return true;
3456
3457 return type0.element_type() == type1.element_type();
3458}
3459
3461{
3462 auto &binary_expr = to_binary_expr(expr);
3463 exprt &op0 = binary_expr.op0();
3464 exprt &op1 = binary_expr.op1();
3465
3466 const typet o_type0 = op0.type();
3467 const typet o_type1 = op1.type();
3468
3469 if(o_type0.id()==ID_vector &&
3470 o_type1.id()==ID_vector)
3471 {
3472 if(
3474 to_vector_type(o_type0), to_vector_type(o_type1)) &&
3475 is_number(to_vector_type(o_type0).element_type()))
3476 {
3477 // Vector arithmetic has fairly strict typing rules, no promotion
3478 op1 = typecast_exprt::conditional_cast(op1, op0.type());
3479 expr.type()=op0.type();
3480 return;
3481 }
3482 }
3483 else if(
3484 o_type0.id() == ID_vector && o_type1.id() != ID_vector &&
3485 is_number(o_type1))
3486 {
3487 // convert op1 to the vector type
3488 op1 = typecast_exprt(op1, o_type0);
3489 expr.type() = o_type0;
3490 return;
3491 }
3492 else if(
3493 o_type0.id() != ID_vector && o_type1.id() == ID_vector &&
3494 is_number(o_type0))
3495 {
3496 // convert op0 to the vector type
3497 op0 = typecast_exprt(op0, o_type1);
3498 expr.type() = o_type1;
3499 return;
3500 }
3501
3502 // promote!
3503
3505
3506 const typet &type0 = op0.type();
3507 const typet &type1 = op1.type();
3508
3509 if(expr.id()==ID_plus || expr.id()==ID_minus ||
3510 expr.id()==ID_mult || expr.id()==ID_div)
3511 {
3512 if(type0.id()==ID_pointer || type1.id()==ID_pointer)
3513 {
3515 return;
3516 }
3517 else if(type0==type1)
3518 {
3519 if(is_number(type0))
3520 {
3521 expr.type()=type0;
3522 return;
3523 }
3524 }
3525 }
3526 else if(expr.id()==ID_mod)
3527 {
3528 if(type0==type1)
3529 {
3530 if(type0.id()==ID_signedbv || type0.id()==ID_unsignedbv)
3531 {
3532 expr.type()=type0;
3533 return;
3534 }
3535 }
3536 }
3537 else if(
3538 expr.id() == ID_bitand || expr.id() == ID_bitnand ||
3539 expr.id() == ID_bitxor || expr.id() == ID_bitor)
3540 {
3541 if(type0==type1)
3542 {
3543 if(is_number(type0))
3544 {
3545 expr.type()=type0;
3546 return;
3547 }
3548 else if(type0.id()==ID_bool)
3549 {
3550 if(expr.id()==ID_bitand)
3551 expr.id(ID_and);
3552 else if(expr.id() == ID_bitnand)
3553 expr.id(ID_nand);
3554 else if(expr.id()==ID_bitor)
3555 expr.id(ID_or);
3556 else if(expr.id()==ID_bitxor)
3557 expr.id(ID_xor);
3558 else
3560 expr.type()=type0;
3561 return;
3562 }
3563 }
3564 }
3565
3567 error() << "operator '" << expr.id() << "' not defined for types '"
3568 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
3569 << eom;
3570 throw 0;
3571}
3572
3574{
3575 assert(expr.id()==ID_shl || expr.id()==ID_shr);
3576
3577 exprt &op0=expr.op0();
3578 exprt &op1=expr.op1();
3579
3580 const typet o_type0 = op0.type();
3581 const typet o_type1 = op1.type();
3582
3583 if(o_type0.id()==ID_vector &&
3584 o_type1.id()==ID_vector)
3585 {
3586 if(
3587 to_vector_type(o_type0).element_type() ==
3588 to_vector_type(o_type1).element_type() &&
3589 is_number(to_vector_type(o_type0).element_type()))
3590 {
3591 // {a0, a1, ..., an} >> {b0, b1, ..., bn} ==
3592 // {a0 >> b0, a1 >> b1, ..., an >> bn}
3593 // Fairly strict typing rules, no promotion
3594 expr.type()=op0.type();
3595 return;
3596 }
3597 }
3598
3599 if(
3600 o_type0.id() == ID_vector &&
3601 is_number(to_vector_type(o_type0).element_type()) && is_number(o_type1))
3602 {
3603 // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
3604 op1 = typecast_exprt(op1, o_type0);
3605 expr.type()=op0.type();
3606 return;
3607 }
3608
3609 // must do the promotions _separately_!
3612
3613 if(is_number(op0.type()) &&
3614 is_number(op1.type()))
3615 {
3616 expr.type()=op0.type();
3617
3618 if(expr.id()==ID_shr) // shifting operation depends on types
3619 {
3620 const typet &op0_type = op0.type();
3621
3622 if(op0_type.id()==ID_unsignedbv)
3623 {
3624 expr.id(ID_lshr);
3625 return;
3626 }
3627 else if(op0_type.id()==ID_signedbv)
3628 {
3629 expr.id(ID_ashr);
3630 return;
3631 }
3632 }
3633
3634 return;
3635 }
3636
3638 error() << "operator '" << expr.id() << "' not defined for types '"
3639 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
3640 << eom;
3641 throw 0;
3642}
3643
3645{
3646 const typet &type=expr.type();
3647 PRECONDITION(type.id() == ID_pointer);
3648
3649 const typet &base_type = to_pointer_type(type).base_type();
3650
3651 if(
3652 base_type.id() == ID_struct_tag &&
3653 follow_tag(to_struct_tag_type(base_type)).is_incomplete())
3654 {
3656 error() << "pointer arithmetic with unknown object size" << eom;
3657 throw 0;
3658 }
3659 else if(
3660 base_type.id() == ID_union_tag &&
3661 follow_tag(to_union_tag_type(base_type)).is_incomplete())
3662 {
3664 error() << "pointer arithmetic with unknown object size" << eom;
3665 throw 0;
3666 }
3667}
3668
3670{
3671 auto &binary_expr = to_binary_expr(expr);
3672 exprt &op0 = binary_expr.op0();
3673 exprt &op1 = binary_expr.op1();
3674
3675 const typet &type0 = op0.type();
3676 const typet &type1 = op1.type();
3677
3678 if(expr.id()==ID_minus ||
3679 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_minus))
3680 {
3681 if(type0.id()==ID_pointer &&
3682 type1.id()==ID_pointer)
3683 {
3684 // We should check the subtypes, and complain if
3685 // they are really different.
3686 expr.type()=pointer_diff_type();
3689 return;
3690 }
3691
3692 if(type0.id()==ID_pointer &&
3693 (type1.id()==ID_bool ||
3694 type1.id()==ID_c_bool ||
3695 type1.id()==ID_unsignedbv ||
3696 type1.id()==ID_signedbv ||
3697 type1.id()==ID_c_bit_field ||
3698 type1.id()==ID_c_enum_tag))
3699 {
3701 make_index_type(op1);
3702 expr.type()=type0;
3703 return;
3704 }
3705 }
3706 else if(expr.id()==ID_plus ||
3707 (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_plus))
3708 {
3709 exprt *p_op, *int_op;
3710
3711 if(type0.id()==ID_pointer)
3712 {
3713 p_op=&op0;
3714 int_op=&op1;
3715 }
3716 else if(type1.id()==ID_pointer)
3717 {
3718 p_op=&op1;
3719 int_op=&op0;
3720 }
3721 else
3722 {
3723 p_op=int_op=nullptr;
3725 }
3726
3727 const typet &int_op_type = int_op->type();
3728
3729 if(int_op_type.id()==ID_bool ||
3730 int_op_type.id()==ID_c_bool ||
3731 int_op_type.id()==ID_unsignedbv ||
3732 int_op_type.id()==ID_signedbv ||
3733 int_op_type.id()==ID_c_bit_field ||
3734 int_op_type.id()==ID_c_enum_tag)
3735 {
3737 make_index_type(*int_op);
3738 expr.type()=p_op->type();
3739 return;
3740 }
3741 }
3742
3743 irep_idt op_name;
3744
3745 if(expr.id()==ID_side_effect)
3746 op_name=to_side_effect_expr(expr).get_statement();
3747 else
3748 op_name=expr.id();
3749
3751 error() << "operator '" << op_name << "' not defined for types '"
3752 << to_string(type0) << "' and '" << to_string(type1) << "'" << eom;
3753 throw 0;
3754}
3755
3757{
3758 auto &binary_expr = to_binary_expr(expr);
3759 implicit_typecast_bool(binary_expr.op0());
3760 implicit_typecast_bool(binary_expr.op1());
3761
3762 // This is not quite accurate: the standard says the result
3763 // should be of type 'int'.
3764 // We do 'bool' anyway to get more compact formulae. Eventually,
3765 // this should be achieved by means of simplification, and not
3766 // in the frontend.
3767 expr.type()=bool_typet();
3768}
3769
3771 side_effect_exprt &expr)
3772{
3773 const irep_idt &statement=expr.get_statement();
3774
3775 auto &binary_expr = to_binary_expr(expr);
3776 exprt &op0 = binary_expr.op0();
3777 exprt &op1 = binary_expr.op1();
3778
3779 {
3780 const typet &type0=op0.type();
3781
3782 if(type0.id()==ID_empty)
3783 {
3785 error() << "cannot assign void" << eom;
3786 throw 0;
3787 }
3788
3789 if(!op0.get_bool(ID_C_lvalue))
3790 {
3792 error() << "assignment error: '" << to_string(op0) << "' not an lvalue"
3793 << eom;
3794 throw 0;
3795 }
3796
3797 if(type0.get_bool(ID_C_constant))
3798 {
3800 error() << "'" << to_string(op0) << "' is constant" << eom;
3801 throw 0;
3802 }
3803
3804 // refuse to assign arrays
3805 if(type0.id() == ID_array)
3806 {
3808 error() << "direct assignments to arrays not permitted" << eom;
3809 throw 0;
3810 }
3811 }
3812
3813 // Add a cast to the underlying type for bit fields.
3814 // In particular, sizeof(s.f=1) works for bit fields.
3815 if(op0.type().id()==ID_c_bit_field)
3816 op0 = typecast_exprt(op0, op0.type().subtype());
3817
3818 const typet o_type0=op0.type();
3819 const typet o_type1=op1.type();
3820
3821 expr.type()=o_type0;
3822
3823 if(statement==ID_assign)
3824 {
3825 implicit_typecast(op1, o_type0);
3826 return;
3827 }
3828 else if(statement==ID_assign_shl ||
3829 statement==ID_assign_shr)
3830 {
3831 if(o_type0.id() == ID_vector)
3832 {
3833 auto &vector_o_type0 = to_vector_type(o_type0);
3834
3835 if(
3836 o_type1.id() == ID_vector &&
3837 vector_o_type0.element_type() ==
3838 to_vector_type(o_type1).element_type() &&
3839 is_number(vector_o_type0.element_type()))
3840 {
3841 return;
3842 }
3843 else if(is_number(vector_o_type0.element_type()) && is_number(o_type1))
3844 {
3845 op1 = typecast_exprt(op1, o_type0);
3846 return;
3847 }
3848 }
3849
3852
3853 if(is_number(op0.type()) && is_number(op1.type()))
3854 {
3855 if(statement==ID_assign_shl)
3856 {
3857 return;
3858 }
3859 else // assign_shr
3860 {
3861 // distinguish arithmetic from logical shifts by looking at type
3862
3863 typet underlying_type=op0.type();
3864
3865 if(underlying_type.id()==ID_unsignedbv ||
3866 underlying_type.id()==ID_c_bool)
3867 {
3868 expr.set(ID_statement, ID_assign_lshr);
3869 return;
3870 }
3871 else if(underlying_type.id()==ID_signedbv)
3872 {
3873 expr.set(ID_statement, ID_assign_ashr);
3874 return;
3875 }
3876 }
3877 }
3878 }
3879 else if(statement==ID_assign_bitxor ||
3880 statement==ID_assign_bitand ||
3881 statement==ID_assign_bitor)
3882 {
3883 // these are more restrictive
3884 if(o_type0.id()==ID_bool ||
3885 o_type0.id()==ID_c_bool)
3886 {
3888 if(
3889 op1.type().id() == ID_bool || op1.type().id() == ID_c_bool ||
3890 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
3891 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
3892 {
3893 return;
3894 }
3895 }
3896 else if(o_type0.id()==ID_c_enum_tag ||
3897 o_type0.id()==ID_unsignedbv ||
3898 o_type0.id()==ID_signedbv ||
3899 o_type0.id()==ID_c_bit_field)
3900 {
3902 if(
3903 op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
3904 op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
3905 {
3906 return;
3907 }
3908 }
3909 else if(o_type0.id()==ID_vector &&
3910 o_type1.id()==ID_vector)
3911 {
3912 // We are willing to do a modest amount of conversion
3914 to_vector_type(o_type0), to_vector_type(o_type1)))
3915 {
3916 op1 = typecast_exprt::conditional_cast(op1, o_type0);
3917 return;
3918 }
3919 }
3920 else if(
3921 o_type0.id() == ID_vector &&
3922 (o_type1.id() == ID_bool || o_type1.id() == ID_c_bool ||
3923 o_type1.id() == ID_c_enum_tag || o_type1.id() == ID_unsignedbv ||
3924 o_type1.id() == ID_signedbv))
3925 {
3927 op1 = typecast_exprt(op1, o_type0);
3928 return;
3929 }
3930 }
3931 else
3932 {
3933 if(o_type0.id()==ID_pointer &&
3934 (statement==ID_assign_minus || statement==ID_assign_plus))
3935 {
3937 return;
3938 }
3939 else if(o_type0.id()==ID_vector &&
3940 o_type1.id()==ID_vector)
3941 {
3942 // We are willing to do a modest amount of conversion
3944 to_vector_type(o_type0), to_vector_type(o_type1)))
3945 {
3946 op1 = typecast_exprt::conditional_cast(op1, o_type0);
3947 return;
3948 }
3949 }
3950 else if(o_type0.id() == ID_vector)
3951 {
3953
3954 if(
3955 is_number(op1.type()) || op1.type().id() == ID_bool ||
3956 op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
3957 {
3958 op1 = typecast_exprt(op1, o_type0);
3959 return;
3960 }
3961 }
3962 else if(o_type0.id()==ID_bool ||
3963 o_type0.id()==ID_c_bool)
3964 {
3966 if(op1.type().id()==ID_bool ||
3967 op1.type().id()==ID_c_bool ||
3968 op1.type().id()==ID_c_enum_tag ||
3969 op1.type().id()==ID_unsignedbv ||
3970 op1.type().id()==ID_signedbv)
3971 return;
3972 }
3973 else
3974 {
3976
3977 if(is_number(op1.type()) ||
3978 op1.type().id()==ID_bool ||
3979 op1.type().id()==ID_c_bool ||
3980 op1.type().id()==ID_c_enum_tag)
3981 return;
3982 }
3983 }
3984
3986 error() << "assignment '" << statement << "' not defined for types '"
3987 << to_string(o_type0) << "' and '" << to_string(o_type1) << "'"
3988 << eom;
3989
3990 throw 0;
3991}
3992
3994{
3995public:
3997 {
3998 }
3999
4000protected:
4002
4003 bool is_constant(const exprt &e) const override
4004 {
4005 if(e.id() == ID_infinity)
4006 return true;
4007 else
4008 return is_constantt::is_constant(e);
4009 }
4010
4011 bool is_constant_address_of(const exprt &e) const override
4012 {
4013 if(e.id() == ID_symbol)
4014 {
4015 return e.type().id() == ID_code ||
4016 ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
4017 }
4018 else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
4019 return true;
4020 else
4022 }
4023};
4024
4026{
4027 // Floating-point expressions may require a rounding mode.
4028 // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
4029 // Some compilers have command-line options to override.
4030 const auto rounding_mode =
4032 adjust_float_expressions(expr, rounding_mode);
4033
4034 simplify(expr, *this);
4035
4036 if(!is_compile_time_constantt(*this)(expr))
4037 {
4039 error() << "expected constant expression, but got '" << to_string(expr)
4040 << "'" << eom;
4041 throw 0;
4042 }
4043}
4044
4046{
4047 make_constant(expr);
4048 make_index_type(expr);
4049 simplify(expr, *this);
4050
4051 if(!is_compile_time_constantt(*this)(expr))
4052 {
4054 error() << "conversion to integer constant failed" << eom;
4055 throw 0;
4056 }
4057}
4058
4060 const exprt &expr,
4061 const irep_idt &id,
4062 const std::string &message) const
4063{
4064 if(!has_subexpr(expr, id))
4065 return;
4066
4068 error() << message << eom;
4069 throw 0;
4070}
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)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
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.
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
int8_t s1
Definition: bytecode_info.h:59
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)
bitvector_typet index_type()
Definition: c_types.cpp:22
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:54
unsignedbv_typet size_type()
Definition: c_types.cpp:68
empty_typet void_type()
Definition: c_types.cpp:263
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
floatbv_typet long_double_type()
Definition: c_types.cpp:211
typet c_bool_type()
Definition: c_types.cpp:118
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:58
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
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:344
bool can_cast_type< c_enum_tag_typet >(const typet &type)
Check whether a reference to a typet is a c_enum_tag_typet.
Definition: c_types.h:331
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
Absolute value.
Definition: std_expr.h:346
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
const declaratorst & declarators() const
const exprt & size() const
Definition: std_types.h:790
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
A base class for binary expressions.
Definition: std_expr.h:550
exprt & lhs()
Definition: std_expr.h:580
exprt & rhs()
Definition: std_expr.h:590
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
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:643
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Reverse the order of bits in a bit-vector.
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
The byte swap expression.
const typet & underlying_type() const
Definition: c_types.h:30
The type of C enums.
Definition: c_types.h:217
const typet & underlying_type() const
Definition: c_types.h:274
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:261
virtual void typecheck_expr_main(exprt &expr)
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)
symbol_tablet & symbol_table
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
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 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 optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
virtual void make_constant_index(exprt &expr)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_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_arithmetic_pointer(const 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)
A codet representing sequential composition of program statements.
Definition: std_code.h:130
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:148
codet & find_last_statement()
Definition: std_code.cpp:99
A codet representing the declaration of a local variable.
Definition: std_code.h:347
symbol_exprt & symbol()
Definition: std_code.h:354
Base type of functions.
Definition: std_types.h:539
bool is_KnR() const
Definition: std_types.h:630
std::vector< parametert > parameterst
Definition: std_types.h:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
bool has_ellipsis() const
Definition: std_types.h:611
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
Complex numbers made of pair of given subtype.
Definition: std_types.h:1057
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2807
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...
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
exprt & op0()
Definition: expr.h:99
exprt & op1()
Definition: expr.h:102
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
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:205
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
exprt & rounding_mode()
Definition: floatbv_expr.h:395
static ieee_float_spect single_precision()
Definition: ieee_float.h:71
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:196
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Array index operator.
Definition: std_expr.h:1328
An expression denoting infinity.
Definition: std_expr.h:2890
Thrown when we can't handle something in an input source file.
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
void remove(const irep_idt &name)
Definition: irep.cpp:96
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:420
bool is_not_nil() const
Definition: irep.h:380
subt & get_sub()
Definition: irep.h:456
void swap(irept &irep)
Definition: irep.h:442
const irep_idt & id() const
Definition: irep.h:396
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
bool is_constant(const exprt &e) const override
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const override
this function determines which reference-typed expressions are constant
is_compile_time_constantt(const namespacet &ns)
Determine whether an expression is constant.
Definition: expr_util.h:89
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:226
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:254
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:321
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
message_handlert & get_message_handler()
Definition: message.h:184
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:97
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
The null pointer constant.
Definition: pointer_expr.h:723
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
The plus expression Associativity is not specified.
Definition: std_expr.h:914
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
The popcount (counting the number of bits set to 1) expression.
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:734
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 Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
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:506
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
std::string as_string() const
Base type for structs and unions.
Definition: std_types.h:62
const componentst & components() const
Definition: std_types.h:147
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:57
bool has_component(const irep_idt &component_name) const
Definition: std_types.h:157
bool is_incomplete() const
A struct/union may be incomplete.
Definition: std_types.h:185
Expression to hold a symbol (variable)
Definition: std_expr.h:80
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:104
const irep_idt & get_identifier() const
Definition: std_expr.h:109
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.
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_extern
Definition: symbol.h:66
bool is_macro
Definition: symbol.h:61
bool is_static_lifetime
Definition: symbol.h:65
bool is_parameter
Definition: symbol.h:67
bool is_type
Definition: symbol.h:61
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
Type with multiple subtypes.
Definition: type.h:191
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Definition: std_expr.h:1611
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4027
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
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.
Definition: floatbv_expr.h:425
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
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.
Definition: pointer_expr.h:398
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, 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:524
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition: std_code.h:1669
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition: std_code.h:429
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:48
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:807
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:328
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor
Definition: config.h:233
flavourt mode
Definition: config.h:222
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
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.
Definition: type2name.cpp:324
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177