cprover
c_typecheck_expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Language Type Checking
4 
5 Author: 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>
24 #include <util/mathematical_expr.h>
26 #include <util/pointer_expr.h>
29 #include <util/prefix.h>
30 #include <util/range.h>
31 #include <util/simplify_expr.h>
32 #include <util/string_constant.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
58  typecheck_expr_main(expr);
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  {
127  return gcc_types_compatible_p(
129  }
130  else if(type1.id()==ID_array &&
131  type2.id()==ID_array)
132  {
133  return gcc_types_compatible_p(
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)
186  typecheck_expr_symbol(expr);
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)
202  typecheck_expr_member(expr);
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)
213  typecheck_expr_index(expr);
214  else if(expr.id()==ID_typecast)
216  else if(expr.id()==ID_sizeof)
217  typecheck_expr_sizeof(expr);
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)
230  typecheck_expr_comma(expr);
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();
342  implicit_typecast_bool(where);
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)
435  op = typecast_exprt(op, signed_int_type());
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=
614  to_struct_union_type(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 
634  result = plus_exprt(
635  result,
636  typecast_exprt::conditional_cast(o_opt.value(), size_type()));
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 
667  result = plus_exprt(
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());
1061  tmp.add_source_location()=expr.source_location();
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 
1325  binary_relation_exprt &expr)
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 
1353  implicit_typecast_arithmetic(op0, op1);
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);
1486  typecheck_expr_member(expr);
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=
1507  to_struct_union_type(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);
1812  tmp.add_source_location()=expr.source_location();
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?
1934  if(!builtin_factory(identifier, symbol_table, get_message_handler()))
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 =
2085  to_mathematical_function_type(f_op_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  {
2667  implicit_typecast(expr.arguments()[1], size_type());
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());
2972  tmp.add_source_location()=f_op.source_location();
2973  }
2974  else
2975  {
2976  tmp=from_integer(0, size_type());
2977  tmp.add_source_location()=f_op.source_location();
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 &&
3030  to_index_expr(to_address_of_expr(to_typecast_expr(tmp1).op()).object())
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 
3504  implicit_typecast_arithmetic(op0, op1);
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
3559  UNREACHABLE;
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;
3724  UNREACHABLE;
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  {
3887  implicit_typecast_arithmetic(op0, op1);
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  {
3901  implicit_typecast_arithmetic(op0, op1);
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  {
3965  implicit_typecast_arithmetic(op0, op1);
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  {
3975  implicit_typecast_arithmetic(op0, op1);
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 {
3995 public:
3997  {
3998  }
3999 
4000 protected:
4001  const namespacet &ns;
4002 
4003  bool is_constant(const exprt &e) const override
4004  {
4005  if(e.id() == ID_infinity)
4006  return true;
4007  else
4008  return is_constantt::is_constant(e);
4009  }
4010 
4011  bool is_constant_address_of(const exprt &e) const override
4012  {
4013  if(e.id() == ID_symbol)
4014  {
4015  return e.type().id() == ID_code ||
4016  ns.lookup(to_symbol_expr(e).get_identifier()).is_static_lifetime;
4017  }
4018  else if(e.id() == ID_array && e.get_bool(ID_C_string_constant))
4019  return true;
4020  else
4022  }
4023 };
4024 
4026 {
4027  // Floating-point expressions may require a rounding mode.
4028  // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
4029  // Some compilers have command-line options to override.
4030  const auto rounding_mode =
4032  adjust_float_expressions(expr, rounding_mode);
4033 
4034  simplify(expr, *this);
4035 
4036  if(!is_compile_time_constantt(*this)(expr))
4037  {
4039  error() << "expected constant expression, but got '" << to_string(expr)
4040  << "'" << eom;
4041  throw 0;
4042  }
4043 }
4044 
4046 {
4047  make_constant(expr);
4048  make_index_type(expr);
4049  simplify(expr, *this);
4050 
4051  if(!is_compile_time_constantt(*this)(expr))
4052  {
4054  error() << "conversion to integer constant failed" << eom;
4055  throw 0;
4056  }
4057 }
4058 
4060  const exprt &expr,
4061  const irep_idt &id,
4062  const std::string &message) const
4063 {
4064  if(!has_subexpr(expr, id))
4065  return;
4066 
4068  error() << message << eom;
4069  throw 0;
4070 }
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Symbolic Execution.
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
C Language Type Checking.
ANSI-CC Language Type Checking.
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:19
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition: as_const.h:14
void base_type(typet &type, const namespacet &ns)
Definition: base_type.cpp:109
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
int8_t s1
Definition: bytecode_info.h:59
API to expression classes that are internal to the C frontend.
ANSI-C Language Type Checking.
already_typechecked_exprt & to_already_typechecked_expr(exprt &expr)
bitvector_typet index_type()
Definition: c_types.cpp:22
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:54
unsignedbv_typet size_type()
Definition: c_types.cpp:68
empty_typet void_type()
Definition: c_types.cpp:263
signedbv_typet signed_int_type()
Definition: c_types.cpp:40
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:253
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:238
floatbv_typet long_double_type()
Definition: c_types.cpp:211
typet c_bool_type()
Definition: c_types.cpp:118
bitvector_typet c_index_type()
Definition: c_types.cpp:16
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 c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
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_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:344
Absolute value.
Definition: std_expr.h:346
Operator to return the address of an object.
Definition: pointer_expr.h:361
exprt & object()
Definition: pointer_expr.h:370
const declaratorst & declarators() const
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:777
const exprt & size() const
Definition: std_types.h:790
A base class for binary expressions.
Definition: std_expr.h:550
exprt & op1()
Definition: expr.h:102
exprt & lhs()
Definition: std_expr.h:580
exprt & op0()
Definition: expr.h:99
exprt & rhs()
Definition: std_expr.h:590
A Boolean expression returning true, iff operation kind would result in an overflow when applied to o...
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:643
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
Reverse the order of bits in a bit-vector.
std::size_t get_width() const
Definition: std_types.h:864
The Boolean type.
Definition: std_types.h:36
The byte swap expression.
const typet & underlying_type() const
Definition: c_types.h:30
The type of C enums.
Definition: c_types.h:217
const typet & underlying_type() const
Definition: c_types.h:274
bool is_incomplete() const
enum types may be incomplete
Definition: c_types.h:261
virtual void typecheck_expr_main(exprt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_alignof(exprt &expr)
static bool is_numeric_type(const typet &src)
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
virtual void typecheck_expr_rel_vector(binary_exprt &expr)
virtual void typecheck_expr_address_of(exprt &expr)
virtual void make_index_type(exprt &expr)
std::map< irep_idt, source_locationt > labels_used
virtual void typecheck_expr_constant(exprt &expr)
virtual void typecheck_expr(exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
virtual void typecheck_code(codet &code)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
virtual void adjust_float_rel(binary_relation_exprt &)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
virtual void typecheck_expr_sizeof(exprt &expr)
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
void disallow_subexpr_by_id(const exprt &, const irep_idt &, const std::string &) const
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
virtual bool gcc_types_compatible_p(const typet &, const typet &)
virtual void typecheck_expr_index(exprt &expr)
virtual void typecheck_expr_function_identifier(exprt &expr)
virtual void typecheck_expr_shifts(shift_exprt &expr)
virtual void make_constant(exprt &expr)
virtual void typecheck_expr_comma(exprt &expr)
symbol_tablet & symbol_table
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
virtual void implicit_typecast_arithmetic(exprt &expr)
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
static void add_rounding_mode(exprt &)
std::list< codet > clean_code
virtual std::string to_string(const exprt &expr)
virtual void typecheck_expr_binary_boolean(exprt &expr)
void typecheck_declaration(ansi_c_declarationt &)
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
asm_label_mapt asm_label_map
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
exprt typecheck_builtin_overflow(side_effect_expr_function_callt &expr, const irep_idt &arith_op)
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
virtual void typecheck_expr_operands(exprt &expr)
virtual void make_constant_index(exprt &expr)
virtual void typecheck_function_call_arguments(side_effect_expr_function_callt &expr)
Typecheck the parameters in a function call expression, and where necessary, make implicit casts arou...
virtual bool is_complete_type(const typet &type) const
id_type_mapt parameter_map
virtual void typecheck_expr_symbol(exprt &expr)
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
virtual void implicit_typecast_bool(exprt &expr)
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
virtual void typecheck_expr_member(exprt &expr)
virtual void typecheck_expr_dereference(exprt &expr)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_type(typet &type)
virtual void typecheck_expr_typecast(exprt &expr)
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
A codet representing sequential composition of program statements.
Definition: std_code.h:130
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:148
codet & find_last_statement()
Definition: std_code.cpp:99
A codet representing the declaration of a local variable.
Definition: std_code.h:347
symbol_exprt & symbol()
Definition: std_code.h:354
Base type of functions.
Definition: std_types.h:539
bool is_KnR() const
Definition: std_types.h:630
std::vector< parametert > parameterst
Definition: std_types.h:541
const typet & return_type() const
Definition: std_types.h:645
bool has_ellipsis() const
Definition: std_types.h:611
const parameterst & parameters() const
Definition: std_types.h:655
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:99
const irep_idt & get_statement() const
Definition: std_code_base.h:65
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
Complex numbers made of pair of given subtype.
Definition: std_types.h:1057
struct configt::ansi_ct ansi_c
A constant literal expression.
Definition: std_expr.h:2807
The count leading zeros (counting the number of zero bits starting from the most-significant bit) exp...
The count trailing zeros (counting the number of zero bits starting from the least-significant bit) e...
Operator to dereference a pointer.
Definition: pointer_expr.h:648
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
exprt & op1()
Definition: expr.h:102
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:129
source_locationt & add_source_location()
Definition: expr.h:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
exprt & op0()
Definition: expr.h:99
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
Fixed-width bit-vector with IEEE floating-point interpretation.
Application of (mathematical) function.
A class for an expression that indicates a history variable.
Definition: c_expr.h:205
IEEE-floating-point equality.
Definition: floatbv_expr.h:264
exprt & rounding_mode()
Definition: floatbv_expr.h:395
static ieee_float_spect single_precision()
Definition: ieee_float.h:71
static ieee_float_spect double_precision()
Definition: ieee_float.h:77
constant_exprt to_expr() const
Definition: ieee_float.cpp:702
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:212
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:196
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
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
subt & get_sub()
Definition: irep.h:456
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
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
irept & add(const irep_idt &name)
Definition: irep.cpp:116
bool is_nil() const
Definition: irep.h:376
bool is_constant(const exprt &e) const override
This function determines what expressions are to be propagated as "constants".
bool is_constant_address_of(const exprt &e) const override
this function determines which reference-typed expressions are constant
is_compile_time_constantt(const namespacet &ns)
Determine whether an expression is constant.
Definition: expr_util.h:89
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:226
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:254
Evaluates to true if the operand is a pointer to a dynamic object.
Definition: pointer_expr.h:321
Evaluates to true if the operand is finite.
Definition: floatbv_expr.h:176
Evaluates to true if the operand is infinite.
Definition: floatbv_expr.h:132
Evaluates to true if the operand is NaN.
Definition: floatbv_expr.h:88
Evaluates to true if the operand is a normal number.
Definition: floatbv_expr.h:220
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & result() const
Definition: message.h:409
message_handlert & get_message_handler()
Definition: message.h:184
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
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
The NIL expression.
Definition: std_expr.h:2874
The null pointer constant.
Definition: pointer_expr.h:723
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
Definition: symbol.h:171
The plus expression Associativity is not specified.
Definition: std_expr.h:914
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
The popcount (counting the number of bits set to 1) expression.
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:734
A base class for shift and rotate operators.
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1692
exprt::operandst & arguments()
Definition: std_code.h:1718
A Boolean expression returning true, iff the result of performing operation kind on operands a and b ...
Definition: c_expr.h:117
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:506
Fixed-width bit-vector with two's complement interpretation.
const irep_idt & get_function() const
std::string as_string() const
Base type for structs and unions.
Definition: std_types.h:62
const 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
const componentst & components() const
Definition: std_types.h:147
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
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
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
bool is_lvalue
Definition: symbol.h:66
exprt value
Initial value of symbol.
Definition: symbol.h:34
irep_idt mode
Language mode.
Definition: symbol.h:49
Type with multiple subtypes.
Definition: type.h:191
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1928
The type of an expression, extends irept.
Definition: type.h:29
const typet & subtype() const
Definition: type.h:48
source_locationt & add_source_location()
Definition: type.h:79
Generic base class for unary expressions.
Definition: std_expr.h:281
const exprt & op() const
Definition: std_expr.h:293
A Boolean expression returning true, iff operation kind would result in an overflow when applied to t...
Union constructor from single element.
Definition: std_expr.h:1611
The vector type.
Definition: std_types.h:996
const constant_exprt & size() const
Definition: std_types.cpp:253
const typet & element_type() const
The type of the elements of the vector.
Definition: std_types.h:1006
configt config
Definition: config.cpp:25
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4011
std::string type2c(const typet &type, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:4027
#define forall_operands(it, expr)
Definition: expr.h:18
#define Forall_operands(it, expr)
Definition: expr.h:25
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:283
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:138
Deprecated expression utility functions.
API to expression classes for floating-point arithmetic.
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: floatbv_expr.h:425
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
API to expression classes for 'mathematical' expressions.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Mathematical types.
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a typet to a mathematical_function_typet.
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:23
ANSI-C Language Type Checking.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:79
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
optionalt< exprt > member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
Pointer Logic.
exprt pointer_offset(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt pointer_object(const exprt &p)
Various predicates over pointers in programs.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
side_effect_expr_statement_expressiont & to_side_effect_expr_statement_expression(exprt &expr)
Definition: std_code.h:1669
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1506
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1739
const code_frontend_declt & to_code_frontend_decl(const codet &code)
Definition: std_code.h:429
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:203
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 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 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 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 vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1040
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
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 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
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
preprocessort preprocessor
Definition: config.h:233
flavourt mode
Definition: config.h:222
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
std::string type_to_partial_identifier(const typet &type, const namespacet &ns)
Constructs a string describing the given type, which can be used as part of a C identifier.
Definition: type2name.cpp:324
Type Naming for C.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177