cprover
Loading...
Searching...
No Matches
c_typecheck_expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "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)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
void base_type(typet &type, const namespacet &ns)
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
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.
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
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.
exprt & op0()
Definition expr.h:99
const irep_idt & get_statement() const
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.
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.
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
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".
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Evaluates to true if the operand is a pointer to a dynamic object.
Evaluates to true if the operand is finite.
Evaluates to true if the operand is infinite.
Evaluates to true if the operand is NaN.
Evaluates to true if the operand is a normal number.
A type for mathematical functions (do not confuse with functions/methods in code)
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().
The NIL expression.
Definition std_expr.h:2874
The null pointer constant.
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.
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.
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
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
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const std::string & id2string(const irep_idt &d)
Definition irep.h: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.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition std_code.h:1506
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition std_code.h:1669
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition std_code.h:1739
const code_blockt & to_code_block(const codet &code)
Definition std_code.h:203
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition std_code.h:429
const codet & to_code(const exprt &expr)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp: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
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.
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177