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 <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/base_type.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/ieee_float.h>
25 #include <util/simplify_expr.h>
26 #include <util/string_constant.h>
27 
29 
30 #include "builtin_factory.h"
31 #include "c_typecast.h"
32 #include "c_qualifiers.h"
33 #include "anonymous_member.h"
34 #include "padding.h"
35 
37 {
38  if(expr.id()==ID_already_typechecked)
39  {
40  assert(expr.operands().size()==1);
41  exprt tmp;
42  tmp.swap(expr.op0());
43  expr.swap(tmp);
44  return;
45  }
46 
47  // fist do sub-nodes
49 
50  // now do case-split
51  typecheck_expr_main(expr);
52 }
53 
55 {
56  for(auto &op : expr.operands())
58 
59  if(expr.id()==ID_div ||
60  expr.id()==ID_mult ||
61  expr.id()==ID_plus ||
62  expr.id()==ID_minus)
63  {
64  if(expr.type().id()==ID_floatbv &&
65  expr.operands().size()==2)
66  {
67  // The rounding mode to be used at compile time is non-obvious.
68  // We'll simply use round to even (0), which is suggested
69  // by Sec. F.7.2 Translation, ISO-9899:1999.
70  expr.operands().resize(3);
71 
72  if(expr.id()==ID_div)
73  expr.id(ID_floatbv_div);
74  else if(expr.id()==ID_mult)
75  expr.id(ID_floatbv_mult);
76  else if(expr.id()==ID_plus)
77  expr.id(ID_floatbv_plus);
78  else if(expr.id()==ID_minus)
79  expr.id(ID_floatbv_minus);
80  else
82 
83  expr.op2()=from_integer(0, unsigned_int_type());
84  }
85  }
86 }
87 
89  const typet &type1,
90  const typet &type2)
91 {
92  // read
93  // http://gcc.gnu.org/onlinedocs/gcc-3.3.6/gcc/Other-Builtins.html
94 
95  // check qualifiers first
96  if(c_qualifierst(type1)!=c_qualifierst(type2))
97  return false;
98 
99  if(type1.id()==ID_c_enum_tag)
101  else if(type2.id()==ID_c_enum_tag)
103 
104  if(type1.id()==ID_c_enum)
105  {
106  if(type2.id()==ID_c_enum) // both are enums
107  return type1==type2; // compares the tag
108  else if(type2==type1.subtype())
109  return true;
110  }
111  else if(type2.id()==ID_c_enum)
112  {
113  if(type1==type2.subtype())
114  return true;
115  }
116  else if(type1.id()==ID_pointer &&
117  type2.id()==ID_pointer)
118  {
119  return gcc_types_compatible_p(type1.subtype(), type2.subtype());
120  }
121  else if(type1.id()==ID_array &&
122  type2.id()==ID_array)
123  {
124  return
125  gcc_types_compatible_p(type1.subtype(), type2.subtype()); // ignore size
126  }
127  else if(type1.id()==ID_code &&
128  type2.id()==ID_code)
129  {
130  const code_typet &c_type1=to_code_type(type1);
131  const code_typet &c_type2=to_code_type(type2);
132 
134  c_type1.return_type(),
135  c_type2.return_type()))
136  return false;
137 
138  if(c_type1.parameters().size()!=c_type2.parameters().size())
139  return false;
140 
141  for(std::size_t i=0; i<c_type1.parameters().size(); i++)
143  c_type1.parameters()[i].type(),
144  c_type2.parameters()[i].type()))
145  return false;
146 
147  return true;
148  }
149  else
150  {
151  if(type1==type2)
152  {
153  // Need to distinguish e.g. long int from int or
154  // long long int from long int.
155  // The rules appear to match those of C++.
156 
157  if(type1.get(ID_C_c_type)==type2.get(ID_C_c_type))
158  return true;
159  }
160  }
161 
162  return false;
163 }
164 
166 {
167  if(expr.id()==ID_side_effect)
169  else if(expr.id()==ID_constant)
171  else if(expr.id()==ID_infinity)
172  {
173  // ignore
174  }
175  else if(expr.id()==ID_symbol)
176  typecheck_expr_symbol(expr);
177  else if(expr.id()==ID_unary_plus ||
178  expr.id()==ID_unary_minus ||
179  expr.id()==ID_bitnot)
181  else if(expr.id()==ID_not)
183  else if(
184  expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies ||
185  expr.id() == ID_xor)
187  else if(expr.id()==ID_address_of)
189  else if(expr.id()==ID_dereference)
191  else if(expr.id()==ID_member)
192  typecheck_expr_member(expr);
193  else if(expr.id()==ID_ptrmember)
195  else if(expr.id()==ID_equal ||
196  expr.id()==ID_notequal ||
197  expr.id()==ID_lt ||
198  expr.id()==ID_le ||
199  expr.id()==ID_gt ||
200  expr.id()==ID_ge)
202  else if(expr.id()==ID_index)
203  typecheck_expr_index(expr);
204  else if(expr.id()==ID_typecast)
206  else if(expr.id()==ID_sizeof)
207  typecheck_expr_sizeof(expr);
208  else if(expr.id()==ID_alignof)
210  else if(expr.id()==ID_plus || expr.id()==ID_minus ||
211  expr.id()==ID_mult || expr.id()==ID_div ||
212  expr.id()==ID_mod ||
213  expr.id()==ID_bitand || expr.id()==ID_bitxor || expr.id()==ID_bitor)
215  else if(expr.id()==ID_shl || expr.id()==ID_shr)
217  else if(expr.id()==ID_comma)
218  typecheck_expr_comma(expr);
219  else if(expr.id()==ID_if)
221  else if(expr.id()==ID_code)
222  {
224  error() << "typecheck_expr_main got code: " << expr.pretty() << eom;
225  throw 0;
226  }
227  else if(expr.id()==ID_gcc_builtin_va_arg)
229  else if(expr.id()==ID_cw_va_arg_typeof)
231  else if(expr.id()==ID_gcc_builtin_types_compatible_p)
232  {
233  expr.type()=bool_typet();
234  auto &subtypes =
235  (static_cast<type_with_subtypest &>(expr.add(ID_type_arg))).subtypes();
236  assert(subtypes.size()==2);
237  typecheck_type(subtypes[0]);
238  typecheck_type(subtypes[1]);
239  source_locationt source_location=expr.source_location();
240 
241  // ignores top-level qualifiers
242  subtypes[0].remove(ID_C_constant);
243  subtypes[0].remove(ID_C_volatile);
244  subtypes[0].remove(ID_C_restricted);
245  subtypes[1].remove(ID_C_constant);
246  subtypes[1].remove(ID_C_volatile);
247  subtypes[1].remove(ID_C_restricted);
248 
249  expr.make_bool(gcc_types_compatible_p(subtypes[0], subtypes[1]));
250  expr.add_source_location()=source_location;
251  }
252  else if(expr.id()==ID_clang_builtin_convertvector)
253  {
254  // This has one operand and a type, and acts like a typecast
255  DATA_INVARIANT(expr.operands().size()==1, "clang_builtin_convertvector has one operand");
256  typecheck_type(expr.type());
257  typecast_exprt tmp(expr.op0(), expr.type());
259  expr.swap(tmp);
260  }
261  else if(expr.id()==ID_builtin_offsetof)
263  else if(expr.id()==ID_string_constant)
264  {
265  // already fine -- mark as lvalue
266  expr.set(ID_C_lvalue, true);
267  }
268  else if(expr.id()==ID_arguments)
269  {
270  // already fine
271  }
272  else if(expr.id()==ID_designated_initializer)
273  {
274  exprt &designator=static_cast<exprt &>(expr.add(ID_designator));
275 
276  Forall_operands(it, designator)
277  {
278  if(it->id()==ID_index)
279  {
280  assert(it->operands().size()==1);
281  typecheck_expr(it->op0()); // still needs typechecking
282  }
283  }
284  }
285  else if(expr.id()==ID_initializer_list)
286  {
287  // already fine, just set some type
288  expr.type()=void_type();
289  }
290  else if(expr.id()==ID_forall ||
291  expr.id()==ID_exists)
292  {
293  // op0 is a declaration,
294  // op1 the bound expression
295  assert(expr.operands().size()==2);
296  expr.type()=bool_typet();
297 
298  if(expr.op0().get(ID_statement)!=ID_decl)
299  {
301  error() << "expected declaration as operand of quantifier" << eom;
302  throw 0;
303  }
304 
305  if(has_subexpr(expr.op1(), ID_side_effect))
306  {
308  error() << "quantifier must not contain side effects" << eom;
309  throw 0;
310  }
311 
312  // replace declaration by symbol expression
313  symbol_exprt bound=to_symbol_expr(expr.op0().op0());
314  expr.op0().swap(bound);
315 
316  implicit_typecast_bool(expr.op1());
317  }
318  else if(expr.id()==ID_label)
319  {
320  expr.type()=void_type();
321  }
322  else if(expr.id()==ID_array)
323  {
324  // these pop up as string constants, and are already typed
325  }
326  else if(expr.id()==ID_complex)
327  {
328  // these should only exist as constants,
329  // and should already be typed
330  }
331  else if(expr.id() == ID_complex_real)
332  {
333  INVARIANT(
334  expr.operands().size() == 1,
335  "real part retrieval operation should have one operand");
336 
337  exprt op = expr.op0();
338  op.type() = follow(op.type());
339 
340  if(op.type().id() != ID_complex)
341  {
342  if(!is_number(op.type()))
343  {
344  error().source_location = op.source_location();
345  error() << "real part retrieval expects numerical operand, "
346  << "but got `" << to_string(op.type()) << "'" << eom;
347  throw 0;
348  }
349 
350  typecast_exprt typecast_expr(op, complex_typet(op.type()));
351  complex_real_exprt complex_real_expr(typecast_expr);
352 
353  expr.swap(complex_real_expr);
354  }
355  else
356  {
357  complex_real_exprt complex_real_expr(op);
358 
359  // these are lvalues if the operand is one
360  if(op.get_bool(ID_C_lvalue))
361  complex_real_expr.set(ID_C_lvalue, true);
362 
363  if(op.type().get_bool(ID_C_constant))
364  complex_real_expr.type().set(ID_C_constant, true);
365 
366  expr.swap(complex_real_expr);
367  }
368  }
369  else if(expr.id() == ID_complex_imag)
370  {
371  INVARIANT(
372  expr.operands().size() == 1,
373  "imaginary part retrieval operation should have one operand");
374 
375  exprt op = expr.op0();
376  op.type() = follow(op.type());
377 
378  if(op.type().id() != ID_complex)
379  {
380  if(!is_number(op.type()))
381  {
382  error().source_location = op.source_location();
383  error() << "real part retrieval expects numerical operand, "
384  << "but got `" << to_string(op.type()) << "'" << eom;
385  throw 0;
386  }
387 
388  typecast_exprt typecast_expr(op, complex_typet(op.type()));
389  complex_imag_exprt complex_imag_expr(typecast_expr);
390 
391  expr.swap(complex_imag_expr);
392  }
393  else
394  {
395  complex_imag_exprt complex_imag_expr(op);
396 
397  // these are lvalues if the operand is one
398  if(op.get_bool(ID_C_lvalue))
399  complex_imag_expr.set(ID_C_lvalue, true);
400 
401  if(op.type().get_bool(ID_C_constant))
402  complex_imag_expr.type().set(ID_C_constant, true);
403 
404  expr.swap(complex_imag_expr);
405  }
406  }
407  else if(expr.id()==ID_generic_selection)
408  {
409  // This is C11.
410  // The operand is already typechecked. Depending
411  // on its type, we return one of the generic associations.
412 
413  if(expr.operands().size()!=1)
414  {
416  error() << "_Generic expects one operand" << eom;
417  throw 0;
418  }
419 
420  // This is one of the few places where it's detectable
421  // that we are using "bool" for boolean operators instead
422  // of "int". We convert for this reason.
423  if(follow(expr.op0().type()).id()==ID_bool)
425 
426  irept::subt &generic_associations=
427  expr.add(ID_generic_associations).get_sub();
428 
429  // first typecheck all types
430  Forall_irep(it, generic_associations)
431  if(it->get(ID_type_arg)!=ID_default)
432  {
433  typet &type=static_cast<typet &>(it->add(ID_type_arg));
434  typecheck_type(type);
435  }
436 
437  // first try non-default match
438  exprt default_match=nil_exprt();
439  exprt assoc_match=nil_exprt();
440 
441  const typet &op_type=follow(expr.op0().type());
442 
443  forall_irep(it, generic_associations)
444  {
445  if(it->get(ID_type_arg)==ID_default)
446  default_match=static_cast<const exprt &>(it->find(ID_value));
447  else if(op_type==
448  follow(static_cast<const typet &>(it->find(ID_type_arg))))
449  assoc_match=static_cast<const exprt &>(it->find(ID_value));
450  }
451 
452  if(assoc_match.is_nil())
453  {
454  if(default_match.is_not_nil())
455  expr.swap(default_match);
456  else
457  {
459  error() << "unmatched generic selection: "
460  << to_string(expr.op0().type()) << eom;
461  throw 0;
462  }
463  }
464  else
465  expr.swap(assoc_match);
466 
467  // still need to typecheck the result
468  typecheck_expr(expr);
469  }
470  else if(expr.id()==ID_gcc_asm_input ||
471  expr.id()==ID_gcc_asm_output ||
472  expr.id()==ID_gcc_asm_clobbered_register)
473  {
474  }
475  else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
476  expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
477  {
478  // already type checked
479  }
480  else
481  {
483  error() << "unexpected expression: " << expr.pretty() << eom;
484  throw 0;
485  }
486 }
487 
489 {
490  if(expr.operands().size()!=2)
491  {
493  error() << "comma operator expects two operands" << eom;
494  throw 0;
495  }
496 
497  expr.type()=expr.op1().type();
498 
499  // make this an l-value if the last operand is one
500  if(expr.op1().get_bool(ID_C_lvalue))
501  expr.set(ID_C_lvalue, true);
502 }
503 
505 {
506  // The first parameter is the va_list, and the second
507  // is the type, which will need to be fixed and checked.
508  // The type is given by the parser as type of the expression.
509 
510  typet arg_type=expr.type();
511  typecheck_type(arg_type);
512 
513  const code_typet new_type(
514  {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
515 
516  assert(expr.operands().size()==1);
517  exprt arg=expr.op0();
518 
520 
521  symbol_exprt function(ID_gcc_builtin_va_arg, new_type);
522  function.add_source_location() = expr.source_location();
523 
524  // turn into function call
526  function, {arg}, new_type.return_type(), expr.source_location());
527 
528  expr.swap(result);
529 
530  // Make sure symbol exists, but we have it return void
531  // to avoid collisions of the same symbol with different
532  // types.
533 
534  code_typet symbol_type=new_type;
535  symbol_type.return_type()=void_type();
536 
537  symbolt symbol;
538  symbol.base_name=ID_gcc_builtin_va_arg;
539  symbol.name=ID_gcc_builtin_va_arg;
540  symbol.type=symbol_type;
541 
542  symbol_table.insert(std::move(symbol));
543 }
544 
546 {
547  // used in Code Warrior via
548  //
549  // __va_arg( <Symbol>, _var_arg_typeof( <Typ> ) )
550  //
551  // where __va_arg is declared as
552  //
553  // extern void* __va_arg(void*, int);
554 
555  typet &type=static_cast<typet &>(expr.add(ID_type_arg));
556  typecheck_type(type);
557 
558  // these return an integer
559  expr.type()=signed_int_type();
560 }
561 
563 {
564  // these need not be constant, due to array indices!
565 
566  if(!expr.operands().empty())
567  {
569  error() << "builtin_offsetof expects no operands" << eom;
570  throw 0;
571  }
572 
573  typet &type=static_cast<typet &>(expr.add(ID_type_arg));
574  typecheck_type(type);
575 
576  exprt &member=static_cast<exprt &>(expr.add(ID_designator));
577 
579 
580  forall_operands(m_it, member)
581  {
582  type = follow(type);
583 
584  if(m_it->id()==ID_member)
585  {
586  if(type.id()!=ID_union && type.id()!=ID_struct)
587  {
589  error() << "offsetof of member expects struct/union type, "
590  << "but got `" << to_string(type) << "'" << eom;
591  throw 0;
592  }
593 
594  bool found=false;
595  irep_idt component_name=m_it->get(ID_component_name);
596 
597  while(!found)
598  {
599  assert(type.id()==ID_union || type.id()==ID_struct);
600 
601  const struct_union_typet &struct_union_type=
602  to_struct_union_type(type);
603 
604  // direct member?
605  if(struct_union_type.has_component(component_name))
606  {
607  found=true;
608 
609  if(type.id()==ID_struct)
610  {
611  exprt o=
613  to_struct_type(type), component_name, *this);
614 
615  if(o.is_nil())
616  {
618  error() << "offsetof failed to determine offset of `"
619  << component_name << "'" << eom;
620  throw 0;
621  }
622 
623  if(o.type()!=size_type())
625 
627  }
628 
629  type=struct_union_type.get_component(component_name).type();
630  }
631  else
632  {
633  // maybe anonymous?
634  bool found2=false;
635 
636  for(const auto &c : struct_union_type.components())
637  {
638  if(
639  c.get_anonymous() && (follow(c.type()).id() == ID_struct ||
640  follow(c.type()).id() == ID_union))
641  {
642  if(has_component_rec(c.type(), component_name, *this))
643  {
644  if(type.id()==ID_struct)
645  {
647  to_struct_type(type), c.get_name(), *this);
648 
649  if(o.is_nil())
650  {
652  error() << "offsetof failed to determine offset of `"
653  << component_name << "'" << eom;
654  throw 0;
655  }
656 
657  if(o.type()!=size_type())
659 
661  }
662 
663  typet tmp = follow(c.type());
664  type=tmp;
665  assert(type.id()==ID_union || type.id()==ID_struct);
666  found2=true;
667  break; // we run into another iteration of the outer loop
668  }
669  }
670  }
671 
672  if(!found2)
673  {
675  error() << "offset-of of member failed to find component `"
676  << component_name << "' in `"
677  << to_string(type) << "'" << eom;
678  throw 0;
679  }
680  }
681  }
682  }
683  else if(m_it->id()==ID_index)
684  {
685  assert(m_it->operands().size()==1);
686 
687  if(type.id()!=ID_array)
688  {
690  error() << "offsetof of index expects array type" << eom;
691  throw 0;
692  }
693 
694  exprt index=m_it->op0();
695 
696  // still need to typecheck index
697  typecheck_expr(index);
698 
699  exprt sub_size=size_of_expr(type.subtype(), *this);
700  if(index.type()!=size_type())
701  index.make_typecast(size_type());
702  result=plus_exprt(result, mult_exprt(sub_size, index));
703 
704  typet tmp=type.subtype();
705  type=tmp;
706  }
707  }
708 
709  // We make an effort to produce a constant,
710  // but this may depend on variables
711  simplify(result, *this);
712  result.add_source_location()=expr.source_location();
713 
714  expr.swap(result);
715 }
716 
718 {
719  if(expr.id()==ID_side_effect &&
720  expr.get(ID_statement)==ID_function_call)
721  {
722  // don't do function operand
723  assert(expr.operands().size()==2);
724 
725  typecheck_expr(expr.op1()); // arguments
726  }
727  else if(expr.id()==ID_side_effect &&
728  expr.get(ID_statement)==ID_statement_expression)
729  {
730  typecheck_code(to_code(expr.op0()));
731  }
732  else if(expr.id()==ID_forall || expr.id()==ID_exists)
733  {
734  assert(expr.operands().size()==2);
735 
736  ansi_c_declarationt &declaration=
737  to_ansi_c_declaration(expr.op0());
738 
739  typecheck_declaration(declaration);
740 
741  if(declaration.declarators().size()!=1)
742  {
744  error() << "expected one declarator exactly" << eom;
745  throw 0;
746  }
747 
748  irep_idt identifier=
749  declaration.declarators().front().get_name();
750 
751  // look it up
752  symbol_tablet::symbolst::const_iterator s_it=
753  symbol_table.symbols.find(identifier);
754 
755  if(s_it==symbol_table.symbols.end())
756  {
758  error() << "failed to find decl symbol `" << identifier
759  << "' in symbol table" << eom;
760  throw 0;
761  }
762 
763  const symbolt &symbol=s_it->second;
764 
765  if(symbol.is_type || symbol.is_extern || symbol.is_static_lifetime ||
766  !is_complete_type(symbol.type) || symbol.type.id()==ID_code)
767  {
769  error() << "unexpected quantified symbol" << eom;
770  throw 0;
771  }
772 
773  code_declt decl(symbol.symbol_expr());
774  decl.add_source_location()=declaration.source_location();
775 
776  expr.op0()=decl;
777 
778  typecheck_expr(expr.op1());
779  }
780  else
781  {
782  Forall_operands(it, expr)
783  typecheck_expr(*it);
784  }
785 }
786 
788 {
789  irep_idt identifier=to_symbol_expr(expr).get_identifier();
790 
791  // Is it a parameter? We do this while checking parameter lists.
792  id_type_mapt::const_iterator p_it=parameter_map.find(identifier);
793  if(p_it!=parameter_map.end())
794  {
795  // yes
796  expr.type()=p_it->second;
797  expr.set(ID_C_lvalue, true);
798  return;
799  }
800 
801  // renaming via GCC asm label
802  asm_label_mapt::const_iterator entry=
803  asm_label_map.find(identifier);
804  if(entry!=asm_label_map.end())
805  {
806  identifier=entry->second;
807  to_symbol_expr(expr).set_identifier(identifier);
808  }
809 
810  // look it up
811  const symbolt *symbol_ptr;
812  if(lookup(identifier, symbol_ptr))
813  {
815  error() << "failed to find symbol `"
816  << identifier << "'" << eom;
817  throw 0;
818  }
819 
820  const symbolt &symbol=*symbol_ptr;
821 
822  if(symbol.is_type)
823  {
825  error() << "did not expect a type symbol here, but got `"
826  << symbol.display_name() << "'" << eom;
827  throw 0;
828  }
829 
830  // save the source location
831  source_locationt source_location=expr.source_location();
832 
833  if(symbol.is_macro)
834  {
835  // preserve enum key
836  #if 0
837  irep_idt base_name=expr.get(ID_C_base_name);
838  #endif
839 
840  follow_macros(expr);
841 
842  #if 0
843  if(expr.id()==ID_constant &&
844  !base_name.empty())
845  expr.set(ID_C_cformat, base_name);
846  else
847  #endif
848  typecheck_expr(expr);
849 
850  // preserve location
851  expr.add_source_location()=source_location;
852  }
853  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "constant_infinity"))
854  {
855  expr=infinity_exprt(symbol.type);
856 
857  // put it back
858  expr.add_source_location()=source_location;
859  }
860  else if(identifier=="__func__" ||
861  identifier=="__FUNCTION__" ||
862  identifier=="__PRETTY_FUNCTION__")
863  {
864  // __func__ is an ANSI-C standard compliant hack to get the function name
865  // __FUNCTION__ and __PRETTY_FUNCTION__ are GCC-specific
866  string_constantt s(source_location.get_function());
867  s.add_source_location()=source_location;
868  s.set(ID_C_lvalue, true);
869  expr.swap(s);
870  }
871  else
872  {
873  expr=symbol.symbol_expr();
874 
875  // put it back
876  expr.add_source_location()=source_location;
877 
878  if(symbol.is_lvalue)
879  expr.set(ID_C_lvalue, true);
880 
881  if(expr.type().id()==ID_code) // function designator
882  { // special case: this is sugar for &f
883  address_of_exprt tmp(expr, pointer_type(expr.type()));
884  tmp.set(ID_C_implicit, true);
886  expr=tmp;
887  }
888  }
889 }
890 
892  side_effect_exprt &expr)
893 {
894  if(expr.operands().size()!=1)
895  {
897  error() << "statement expression expects one operand" << eom;
898  throw 0;
899  }
900 
901  codet &code=to_code(expr.op0());
902 
903  // the type is the type of the last statement in the
904  // block, but do worry about labels!
905 
907 
908  irep_idt last_statement=last.get_statement();
909 
910  if(last_statement==ID_expression)
911  {
912  assert(last.operands().size()==1);
913  exprt &op=last.op0();
914 
915  // arrays here turn into pointers (array decay)
916  if(op.type().id()==ID_array)
917  implicit_typecast(op, pointer_type(op.type().subtype()));
918 
919  expr.type()=op.type();
920  }
921  else if(last_statement==ID_function_call)
922  {
923  // this is suspected to be dead
924  UNREACHABLE;
925 
926  // make the last statement an expression
927 
929 
931  fc.function(),
932  fc.arguments(),
934  fc.source_location());
935 
936  expr.type()=sideeffect.type();
937 
938  if(fc.lhs().is_nil())
939  {
940  code_expressiont code_expr(sideeffect);
941  code_expr.add_source_location() = fc.source_location();
942  last.swap(code_expr);
943  }
944  else
945  {
946  side_effect_exprt assign(
947  ID_assign, sideeffect.type(), fc.source_location());
948  assign.move_to_operands(fc.lhs(), sideeffect);
949 
950  code_expressiont code_expr(assign);
951  code_expr.add_source_location() = fc.source_location();
952 
953  last.swap(code_expr);
954  }
955  }
956  else
957  expr.type()=typet(ID_empty);
958 }
959 
961 {
962  typet type;
963 
964  if(expr.operands().empty())
965  {
966  type.swap(static_cast<typet &>(expr.add(ID_type_arg)));
967  typecheck_type(type);
968  }
969  else if(expr.operands().size()==1)
970  {
971  type.swap(expr.op0().type());
972  }
973  else
974  {
976  error() << "sizeof operator expects zero or one operand, "
977  "but got " << expr.operands().size() << eom;
978  throw 0;
979  }
980 
981  exprt new_expr;
982 
983  if(type.id()==ID_c_bit_field)
984  {
986  error() << "sizeof cannot be applied to bit fields" << eom;
987  throw 0;
988  }
989  else if(type.id() == ID_bool)
990  {
992  error() << "sizeof cannot be applied to single bits" << eom;
993  throw 0;
994  }
995  else if(type.id() == ID_empty)
996  {
997  // This is a gcc extension.
998  // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
999  new_expr = size_of_expr(char_type(), *this);
1000  }
1001  else
1002  {
1003  new_expr = size_of_expr(type, *this);
1004 
1005  if(new_expr.is_nil())
1006  {
1008  error() << "type has no size: " << to_string(type) << eom;
1009  throw 0;
1010  }
1011  }
1012 
1013  new_expr.swap(expr);
1014 
1015  expr.add(ID_C_c_sizeof_type)=type;
1016 
1017  // The type may contain side-effects.
1018  if(!clean_code.empty())
1019  {
1020  side_effect_exprt side_effect_expr(
1021  ID_statement_expression, void_type(), expr.source_location());
1022  auto decl_block=code_blockt::from_list(clean_code);
1023  decl_block.set_statement(ID_decl_block);
1024  side_effect_expr.copy_to_operands(decl_block);
1025  clean_code.clear();
1026 
1027  // We merge the side-effect into the operand of the typecast,
1028  // using a comma-expression.
1029  // I.e., (type)e becomes (type)(side-effect, e)
1030  // It is not obvious whether the type or 'e' should be evaluated
1031  // first.
1032 
1033  exprt comma_expr(ID_comma, expr.type());
1034  comma_expr.copy_to_operands(side_effect_expr, expr);
1035  expr.swap(comma_expr);
1036  }
1037 }
1038 
1040 {
1041  typet argument_type;
1042 
1043  if(expr.operands().size()==1)
1044  argument_type=expr.op0().type();
1045  else
1046  {
1047  typet &op_type=static_cast<typet &>(expr.add(ID_type_arg));
1048  typecheck_type(op_type);
1049  argument_type=op_type;
1050  }
1051 
1052  // we only care about the type
1053  mp_integer a=alignment(argument_type, *this);
1054 
1055  exprt tmp=from_integer(a, size_type());
1056  tmp.add_source_location()=expr.source_location();
1057 
1058  expr.swap(tmp);
1059 }
1060 
1062 {
1063  if(expr.operands().size()!=1)
1064  {
1066  error() << "typecast operator expects one operand" << eom;
1067  throw 0;
1068  }
1069 
1070  exprt &op=expr.op0();
1071 
1072  typecheck_type(expr.type());
1073 
1074  // The type may contain side-effects.
1075  if(!clean_code.empty())
1076  {
1077  side_effect_exprt side_effect_expr(
1078  ID_statement_expression, void_type(), expr.source_location());
1079  auto decl_block=code_blockt::from_list(clean_code);
1080  decl_block.set_statement(ID_decl_block);
1081  side_effect_expr.copy_to_operands(decl_block);
1082  clean_code.clear();
1083 
1084  // We merge the side-effect into the operand of the typecast,
1085  // using a comma-expression.
1086  // I.e., (type)e becomes (type)(side-effect, e)
1087  // It is not obvious whether the type or 'e' should be evaluated
1088  // first.
1089 
1090  exprt comma_expr(ID_comma, op.type());
1091  comma_expr.copy_to_operands(side_effect_expr, op);
1092  op.swap(comma_expr);
1093  }
1094 
1095  const typet expr_type=follow(expr.type());
1096 
1097  if(expr_type.id()==ID_union &&
1098  !base_type_eq(expr_type, op.type(), *this) &&
1099  op.id()!=ID_initializer_list)
1100  {
1101  // This is a GCC extension. It's either a 'temporary union',
1102  // where the argument is one of the member types.
1103 
1104  // This is one of the few places where it's detectable
1105  // that we are using "bool" for boolean operators instead
1106  // of "int". We convert for this reason.
1107  if(follow(op.type()).id()==ID_bool)
1109 
1110  // we need to find a member with the right type
1111  for(const auto &c : to_union_type(expr_type).components())
1112  {
1113  if(base_type_eq(c.type(), op.type(), *this))
1114  {
1115  // found! build union constructor
1116  union_exprt union_expr(expr.type());
1117  union_expr.add_source_location()=expr.source_location();
1118  union_expr.op()=op;
1119  union_expr.set_component_name(c.get_name());
1120  expr=union_expr;
1121  expr.set(ID_C_lvalue, true);
1122  return;
1123  }
1124  }
1125 
1126  // not found, complain
1128  error() << "type cast to union: type `"
1129  << to_string(op.type()) << "' not found in union" << eom;
1130  throw 0;
1131  }
1132 
1133  // We allow (TYPE){ initializer_list }
1134  // This is called "compound literal", and is syntactic
1135  // sugar for a (possibly local) declaration.
1136  if(op.id()==ID_initializer_list)
1137  {
1138  // just do a normal initialization
1139  do_initializer(op, expr.type(), false);
1140 
1141  // This produces a struct-expression,
1142  // union-expression, array-expression,
1143  // or an expression for a pointer or scalar.
1144  // We produce a compound_literal expression.
1145  exprt tmp(ID_compound_literal, expr.type());
1146  tmp.copy_to_operands(op);
1147 
1148  // handle the case of TYPE being an array with unspecified size
1149  if(op.id()==ID_array &&
1150  expr.type().id()==ID_array &&
1151  to_array_type(expr.type()).size().is_nil())
1152  tmp.type()=op.type();
1153 
1154  expr=tmp;
1155  expr.set(ID_C_lvalue, true); // these are l-values
1156  return;
1157  }
1158 
1159  // a cast to void is always fine
1160  if(expr_type.id()==ID_empty)
1161  return;
1162 
1163  const typet op_type=follow(op.type());
1164 
1165  // cast to same type?
1166  if(base_type_eq(expr_type, op_type, *this))
1167  return; // it's ok
1168 
1169  // vectors?
1170 
1171  if(expr_type.id()==ID_vector)
1172  {
1173  // we are generous -- any vector to vector is fine
1174  if(op_type.id()==ID_vector)
1175  return;
1176  else if(op_type.id()==ID_signedbv ||
1177  op_type.id()==ID_unsignedbv)
1178  return;
1179  }
1180 
1181  if(!is_numeric_type(expr_type) && expr_type.id()!=ID_pointer)
1182  {
1184  error() << "type cast to `"
1185  << to_string(expr_type) << "' is not permitted" << eom;
1186  throw 0;
1187  }
1188 
1189  if(is_numeric_type(op_type) || op_type.id()==ID_pointer)
1190  {
1191  }
1192  else if(op_type.id()==ID_array)
1193  {
1194  index_exprt index;
1195  index.array()=op;
1196  index.index()=from_integer(0, index_type());
1197  index.type()=op_type.subtype();
1198  op=address_of_exprt(index);
1199  }
1200  else if(op_type.id()==ID_empty)
1201  {
1202  if(expr_type.id()!=ID_empty)
1203  {
1205  error() << "type cast from void only permitted to void, but got `"
1206  << to_string(expr.type()) << "'" << eom;
1207  throw 0;
1208  }
1209  }
1210  else if(op_type.id()==ID_vector)
1211  {
1212  const vector_typet &op_vector_type=
1213  to_vector_type(op_type);
1214 
1215  // gcc allows conversion of a vector of size 1 to
1216  // an integer/float of the same size
1217  if((expr_type.id()==ID_signedbv ||
1218  expr_type.id()==ID_unsignedbv) &&
1219  pointer_offset_bits(expr_type, *this)==
1220  pointer_offset_bits(op_vector_type, *this))
1221  {
1222  }
1223  else
1224  {
1226  error() << "type cast from vector to `"
1227  << to_string(expr.type()) << "' not permitted" << eom;
1228  throw 0;
1229  }
1230  }
1231  else
1232  {
1234  error() << "type cast from `"
1235  << to_string(op_type) << "' not permitted" << eom;
1236  throw 0;
1237  }
1238 
1239  // The new thing is an lvalue if the previous one is
1240  // an lvalue and it's just a pointer type cast.
1241  // This isn't really standard conformant!
1242  // Note that gcc says "warning: target of assignment not really an lvalue;
1243  // this will be a hard error in the future", i.e., we
1244  // can hope that the code below will one day simply go away.
1245 
1246  // Current versions of gcc in fact refuse to do this! Yay!
1247 
1248  if(expr.op0().get_bool(ID_C_lvalue))
1249  {
1250  if(expr_type.id()==ID_pointer)
1251  expr.set(ID_C_lvalue, true);
1252  }
1253 }
1254 
1256 {
1257  implicit_typecast(expr, index_type());
1258 }
1259 
1261 {
1262  if(expr.operands().size()!=2)
1263  {
1265  error() << "operator `" << expr.id()
1266  << "' expects two operands" << eom;
1267  throw 0;
1268  }
1269 
1270  exprt &array_expr=expr.op0();
1271  exprt &index_expr=expr.op1();
1272 
1273  // we might have to swap them
1274 
1275  {
1276  const typet &array_full_type=follow(array_expr.type());
1277  const typet &index_full_type=follow(index_expr.type());
1278 
1279  if(array_full_type.id()!=ID_array &&
1280  array_full_type.id()!=ID_pointer &&
1281  array_full_type.id()!=ID_vector &&
1282  (index_full_type.id()==ID_array ||
1283  index_full_type.id()==ID_pointer ||
1284  index_full_type.id()==ID_vector))
1285  std::swap(array_expr, index_expr);
1286  }
1287 
1288  make_index_type(index_expr);
1289 
1290  // array_expr is a reference to one of expr.operands(), when that vector is
1291  // swapped below the reference is no longer valid. final_array_type exists
1292  // beyond that point so can't be a reference
1293  const typet final_array_type = follow(array_expr.type());
1294 
1295  if(final_array_type.id()==ID_array ||
1296  final_array_type.id()==ID_vector)
1297  {
1298  expr.type() = final_array_type.subtype();
1299 
1300  if(array_expr.get_bool(ID_C_lvalue))
1301  expr.set(ID_C_lvalue, true);
1302 
1303  if(final_array_type.get_bool(ID_C_constant))
1304  expr.type().set(ID_C_constant, true);
1305  }
1306  else if(final_array_type.id()==ID_pointer)
1307  {
1308  // p[i] is syntactic sugar for *(p+i)
1309 
1311  exprt addition(ID_plus, array_expr.type());
1312  addition.operands().swap(expr.operands());
1313  expr.move_to_operands(addition);
1314  expr.id(ID_dereference);
1315  expr.set(ID_C_lvalue, true);
1316  expr.type() = final_array_type.subtype();
1317  }
1318  else
1319  {
1321  error() << "operator [] must take array/vector or pointer but got `"
1322  << to_string(array_expr.type()) << "'" << eom;
1323  throw 0;
1324  }
1325 }
1326 
1328 {
1329  // equality and disequality on float is not mathematical equality!
1330  assert(expr.operands().size()==2);
1331 
1332  if(follow(expr.op0().type()).id()==ID_floatbv)
1333  {
1334  if(expr.id()==ID_equal)
1335  expr.id(ID_ieee_float_equal);
1336  else if(expr.id()==ID_notequal)
1337  expr.id(ID_ieee_float_notequal);
1338  }
1339 }
1340 
1342  binary_relation_exprt &expr)
1343 {
1344  exprt &op0=expr.op0();
1345  exprt &op1=expr.op1();
1346 
1347  const typet o_type0=op0.type();
1348  const typet o_type1=op1.type();
1349 
1350  if(follow(o_type0).id()==ID_vector ||
1351  follow(o_type1).id()==ID_vector)
1352  {
1354  return;
1355  }
1356 
1357  expr.type()=bool_typet();
1358 
1359  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1360  {
1361  if(follow(o_type0)==follow(o_type1))
1362  {
1363  const typet &final_type=follow(o_type0);
1364  if(final_type.id()!=ID_array &&
1365  final_type.id()!=ID_incomplete_struct)
1366  {
1367  adjust_float_rel(expr);
1368  return; // no promotion necessary
1369  }
1370  }
1371  }
1372 
1373  implicit_typecast_arithmetic(op0, op1);
1374 
1375  const typet &type0=op0.type();
1376  const typet &type1=op1.type();
1377 
1378  if(type0==type1)
1379  {
1380  if(is_number(type0))
1381  {
1382  adjust_float_rel(expr);
1383  return;
1384  }
1385 
1386  if(type0.id()==ID_pointer)
1387  {
1388  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1389  return;
1390 
1391  if(expr.id()==ID_le || expr.id()==ID_lt ||
1392  expr.id()==ID_ge || expr.id()==ID_gt)
1393  return;
1394  }
1395 
1396  if(type0.id()==ID_string_constant)
1397  {
1398  if(expr.id()==ID_equal || expr.id()==ID_notequal)
1399  return;
1400  }
1401  }
1402  else
1403  {
1404  // pointer and zero
1405  if(type0.id()==ID_pointer &&
1406  simplify_expr(op1, *this).is_zero())
1407  {
1408  op1=constant_exprt(ID_NULL, type0);
1409  return;
1410  }
1411 
1412  if(type1.id()==ID_pointer &&
1413  simplify_expr(op0, *this).is_zero())
1414  {
1415  op0=constant_exprt(ID_NULL, type1);
1416  return;
1417  }
1418 
1419  // pointer and integer
1420  if(type0.id()==ID_pointer && is_number(type1))
1421  {
1422  op1.make_typecast(type0);
1423  return;
1424  }
1425 
1426  if(type1.id()==ID_pointer && is_number(type0))
1427  {
1428  op0.make_typecast(type1);
1429  return;
1430  }
1431 
1432  if(type0.id()==ID_pointer && type1.id()==ID_pointer)
1433  {
1434  op1.make_typecast(type0);
1435  return;
1436  }
1437  }
1438 
1440  error() << "operator `" << expr.id()
1441  << "' not defined for types `"
1442  << to_string(o_type0) << "' and `"
1443  << to_string(o_type1) << "'" << eom;
1444  throw 0;
1445 }
1446 
1448  binary_relation_exprt &expr)
1449 {
1450  exprt &op0=expr.op0();
1451  exprt &op1=expr.op1();
1452 
1453  const typet o_type0=follow(op0.type());
1454  const typet o_type1=follow(op1.type());
1455 
1456  if(o_type0.id()!=ID_vector ||
1457  o_type1.id()!=ID_vector ||
1458  follow(o_type0.subtype())!=follow(o_type1.subtype()))
1459  {
1461  error() << "vector operator `" << expr.id()
1462  << "' not defined for types `"
1463  << to_string(o_type0) << "' and `"
1464  << to_string(o_type1) << "'" << eom;
1465  throw 0;
1466  }
1467 
1468  // Comparisons between vectors produce a vector
1469  // of integers with the same dimension.
1470  expr.type()=vector_typet(signed_int_type(), to_vector_type(o_type0).size());
1471 }
1472 
1474 {
1475  if(expr.operands().size()!=1)
1476  {
1478  error() << "ptrmember operator expects one operand" << eom;
1479  throw 0;
1480  }
1481 
1482  const typet &final_op0_type=follow(expr.op0().type());
1483 
1484  if(final_op0_type.id()==ID_array)
1485  {
1486  // a->f is the same as a[0].f
1487  exprt zero=from_integer(0, index_type());
1488  index_exprt index_expr(expr.op0(), zero, final_op0_type.subtype());
1489  index_expr.set(ID_C_lvalue, true);
1490  expr.op0().swap(index_expr);
1491  }
1492  else if(final_op0_type.id()==ID_pointer)
1493  {
1494  // turn x->y into (*x).y
1495  dereference_exprt deref_expr(expr.op0());
1496  deref_expr.add_source_location()=expr.source_location();
1497  typecheck_expr_dereference(deref_expr);
1498  expr.op0().swap(deref_expr);
1499  }
1500  else
1501  {
1503  error() << "ptrmember operator requires pointer or array type "
1504  "on left hand side, but got `"
1505  << to_string(expr.op0().type()) << "'" << eom;
1506  throw 0;
1507  }
1508 
1509  expr.id(ID_member);
1510  typecheck_expr_member(expr);
1511 }
1512 
1514 {
1515  if(expr.operands().size()!=1)
1516  {
1518  error() << "member operator expects one operand" << eom;
1519  throw 0;
1520  }
1521 
1522  exprt &op0=expr.op0();
1523  typet type=op0.type();
1524 
1525  type = follow(type);
1526 
1527  if(type.id()==ID_incomplete_struct)
1528  {
1530  error() << "member operator got incomplete struct type "
1531  "on left hand side" << eom;
1532  throw 0;
1533  }
1534 
1535  if(type.id()==ID_incomplete_union)
1536  {
1538  error() << "member operator got incomplete union type "
1539  "on left hand side" << eom;
1540  throw 0;
1541  }
1542 
1543  if(type.id()!=ID_struct &&
1544  type.id()!=ID_union)
1545  {
1547  error() << "member operator requires structure type "
1548  "on left hand side but got `"
1549  << to_string(type) << "'" << eom;
1550  throw 0;
1551  }
1552 
1553  const struct_union_typet &struct_union_type=
1554  to_struct_union_type(type);
1555 
1556  const irep_idt &component_name=
1557  expr.get(ID_component_name);
1558 
1559  // first try to find directly
1561  struct_union_type.get_component(component_name);
1562 
1563  // if that fails, search the anonymous members
1564 
1565  if(component.is_nil())
1566  {
1567  exprt tmp=get_component_rec(op0, component_name, *this);
1568 
1569  if(tmp.is_nil())
1570  {
1571  // give up
1573  error() << "member `" << component_name
1574  << "' not found in `"
1575  << to_string(type) << "'" << eom;
1576  throw 0;
1577  }
1578 
1579  // done!
1580  expr.swap(tmp);
1581  return;
1582  }
1583 
1584  expr.type()=component.type();
1585 
1586  if(op0.get_bool(ID_C_lvalue))
1587  expr.set(ID_C_lvalue, true);
1588 
1589  if(op0.type().get_bool(ID_C_constant) || type.get_bool(ID_C_constant))
1590  expr.type().set(ID_C_constant, true);
1591 
1592  // copy method identifier
1593  const irep_idt &identifier=component.get(ID_C_identifier);
1594 
1595  if(!identifier.empty())
1596  expr.set(ID_C_identifier, identifier);
1597 
1598  const irep_idt &access=component.get_access();
1599 
1600  if(access==ID_private)
1601  {
1603  error() << "member `" << component_name
1604  << "' is " << access << eom;
1605  throw 0;
1606  }
1607 }
1608 
1610 {
1611  exprt::operandst &operands=expr.operands();
1612 
1613  assert(operands.size()==3);
1614 
1615  // copy (save) original types
1616  const typet o_type0=operands[0].type();
1617  const typet o_type1=operands[1].type();
1618  const typet o_type2=operands[2].type();
1619 
1620  implicit_typecast_bool(operands[0]);
1621  implicit_typecast_arithmetic(operands[1], operands[2]);
1622 
1623  if(operands[1].type().id()==ID_pointer &&
1624  operands[2].type().id()!=ID_pointer)
1625  implicit_typecast(operands[2], operands[1].type());
1626  else if(operands[2].type().id()==ID_pointer &&
1627  operands[1].type().id()!=ID_pointer)
1628  implicit_typecast(operands[1], operands[2].type());
1629 
1630  if(operands[1].type().id()==ID_pointer &&
1631  operands[2].type().id()==ID_pointer &&
1632  operands[1].type()!=operands[2].type())
1633  {
1634  exprt tmp1=simplify_expr(operands[1], *this);
1635  exprt tmp2=simplify_expr(operands[2], *this);
1636 
1637  // is one of them void * AND null? Convert that to the other.
1638  // (at least that's how GCC behaves)
1639  if(operands[1].type().subtype().id()==ID_empty &&
1640  tmp1.is_constant() &&
1641  to_constant_expr(tmp1).get_value()==ID_NULL)
1642  implicit_typecast(operands[1], operands[2].type());
1643  else if(operands[2].type().subtype().id()==ID_empty &&
1644  tmp2.is_constant() &&
1645  to_constant_expr(tmp2).get_value()==ID_NULL)
1646  implicit_typecast(operands[2], operands[1].type());
1647  else if(operands[1].type().subtype().id()!=ID_code ||
1648  operands[2].type().subtype().id()!=ID_code)
1649  {
1650  // Make it void *.
1651  // gcc and clang issue a warning for this.
1652  expr.type()=pointer_type(empty_typet());
1653  implicit_typecast(operands[1], expr.type());
1654  implicit_typecast(operands[2], expr.type());
1655  }
1656  else
1657  {
1658  // maybe functions without parameter lists
1659  const code_typet &c_type1=to_code_type(operands[1].type().subtype());
1660  const code_typet &c_type2=to_code_type(operands[2].type().subtype());
1661 
1662  if(c_type1.return_type()==c_type2.return_type())
1663  {
1664  if(c_type1.parameters().empty() && c_type1.has_ellipsis())
1665  implicit_typecast(operands[1], operands[2].type());
1666  else if(c_type2.parameters().empty() && c_type2.has_ellipsis())
1667  implicit_typecast(operands[2], operands[1].type());
1668  }
1669  }
1670  }
1671 
1672  if(operands[1].type().id()==ID_empty ||
1673  operands[2].type().id()==ID_empty)
1674  {
1675  expr.type()=void_type();
1676  return;
1677  }
1678 
1679  if(follow(operands[1].type())==follow(operands[2].type()))
1680  {
1681  expr.type()=operands[1].type();
1682 
1683  // GCC says: "A conditional expression is a valid lvalue
1684  // if its type is not void and the true and false branches
1685  // are both valid lvalues."
1686 
1687  if(operands[1].get_bool(ID_C_lvalue) &&
1688  operands[2].get_bool(ID_C_lvalue))
1689  expr.set(ID_C_lvalue, true);
1690 
1691  return;
1692  }
1693 
1695  error() << "operator ?: not defined for types `"
1696  << to_string(o_type1) << "' and `"
1697  << to_string(o_type2) << "'" << eom;
1698  throw 0;
1699 }
1700 
1702  side_effect_exprt &expr)
1703 {
1704  // x ? : y is almost the same as x ? x : y,
1705  // but not quite, as x is evaluated only once
1706 
1707  exprt::operandst &operands=expr.operands();
1708 
1709  if(operands.size()!=2)
1710  {
1712  error() << "gcc conditional_expr expects two operands" << eom;
1713  throw 0;
1714  }
1715 
1716  // use typechecking code for "if"
1717 
1718  if_exprt if_expr;
1719  if_expr.cond()=operands[0];
1720  if_expr.true_case()=operands[0];
1721  if_expr.false_case()=operands[1];
1722  if_expr.add_source_location()=expr.source_location();
1723 
1724  typecheck_expr_trinary(if_expr);
1725 
1726  // copy the result
1727  expr.op0()=if_expr.op1();
1728  expr.op1()=if_expr.op2();
1729  expr.type()=if_expr.type();
1730 }
1731 
1733 {
1734  if(expr.operands().size()!=1)
1735  {
1737  error() << "unary operator & expects one operand" << eom;
1738  throw 0;
1739  }
1740 
1741  exprt &op=expr.op0();
1742 
1743  if(op.type().id()==ID_c_bit_field)
1744  {
1746  error() << "cannot take address of a bit field" << eom;
1747  throw 0;
1748  }
1749 
1750  if(op.type().id() == ID_bool)
1751  {
1753  error() << "cannot take address of a single bit" << eom;
1754  throw 0;
1755  }
1756 
1757  // special case: address of label
1758  if(op.id()==ID_label)
1759  {
1760  expr.type()=pointer_type(void_type());
1761 
1762  // remember the label
1763  labels_used[op.get(ID_identifier)]=op.source_location();
1764  return;
1765  }
1766 
1767  // special case: address of function designator
1768  // ANSI-C 99 section 6.3.2.1 paragraph 4
1769 
1770  if(op.id()==ID_address_of &&
1771  op.get_bool(ID_C_implicit) &&
1772  op.operands().size()==1 &&
1773  op.op0().type().id()==ID_code)
1774  {
1775  // make the implicit address_of an explicit address_of
1776  exprt tmp;
1777  tmp.swap(op);
1778  tmp.set(ID_C_implicit, false);
1779  expr.swap(tmp);
1780  return;
1781  }
1782 
1783  if(op.id()==ID_struct ||
1784  op.id()==ID_union ||
1785  op.id()==ID_array ||
1786  op.id()==ID_string_constant)
1787  {
1788  // these are really objects
1789  }
1790  else if(op.get_bool(ID_C_lvalue))
1791  {
1792  // ok
1793  }
1794  else if(op.type().id()==ID_code)
1795  {
1796  // ok
1797  }
1798  else
1799  {
1801  error() << "address_of error: `" << to_string(op)
1802  << "' not an lvalue" << eom;
1803  throw 0;
1804  }
1805 
1806  expr.type()=pointer_type(op.type());
1807 }
1808 
1810 {
1811  if(expr.operands().size()!=1)
1812  {
1814  error() << "unary operator * expects one operand" << eom;
1815  throw 0;
1816  }
1817 
1818  exprt &op=expr.op0();
1819 
1820  const typet op_type=follow(op.type());
1821 
1822  if(op_type.id()==ID_array)
1823  {
1824  // *a is the same as a[0]
1825  expr.id(ID_index);
1826  expr.type()=op_type.subtype();
1828  assert(expr.operands().size()==2);
1829  }
1830  else if(op_type.id()==ID_pointer)
1831  {
1832  expr.type()=op_type.subtype();
1833  }
1834  else
1835  {
1837  error() << "operand of unary * `" << to_string(op)
1838  << "' is not a pointer, but got `"
1839  << to_string(op_type) << "'" << eom;
1840  throw 0;
1841  }
1842 
1843  expr.set(ID_C_lvalue, true);
1844 
1845  // if you dereference a pointer pointing to
1846  // a function, you get a pointer again
1847  // allowing ******...*p
1848 
1850 }
1851 
1853 {
1854  if(expr.type().id()==ID_code)
1855  {
1856  address_of_exprt tmp(expr, pointer_type(expr.type()));
1857  tmp.set(ID_C_implicit, true);
1858  tmp.add_source_location()=expr.source_location();
1859  expr=tmp;
1860  }
1861 }
1862 
1864 {
1865  const irep_idt &statement=expr.get_statement();
1866 
1867  if(statement==ID_preincrement ||
1868  statement==ID_predecrement ||
1869  statement==ID_postincrement ||
1870  statement==ID_postdecrement)
1871  {
1872  if(expr.operands().size()!=1)
1873  {
1875  error() << statement << "operator expects one operand" << eom;
1876  }
1877 
1878  const exprt &op0=expr.op0();
1879  const typet &type0=op0.type();
1880  const typet &final_type0=follow(type0);
1881 
1882  if(!op0.get_bool(ID_C_lvalue))
1883  {
1885  error() << "prefix operator error: `" << to_string(op0)
1886  << "' not an lvalue" << eom;
1887  throw 0;
1888  }
1889 
1890  if(type0.get_bool(ID_C_constant))
1891  {
1893  error() << "error: `" << to_string(op0)
1894  << "' is constant" << eom;
1895  throw 0;
1896  }
1897 
1898  if(final_type0.id()==ID_c_enum_tag)
1899  {
1900  if(follow_tag(to_c_enum_tag_type(final_type0)).id()==
1901  ID_incomplete_c_enum)
1902  {
1904  error() << "operator `" << statement
1905  << "' given incomplete type `"
1906  << to_string(type0) << "'" << eom;
1907  throw 0;
1908  }
1909  else
1910  expr.type()=type0;
1911  }
1912  else if(final_type0.id()==ID_c_bit_field)
1913  {
1914  // promote to underlying type
1915  typet underlying_type=to_c_bit_field_type(final_type0).subtype();
1916  expr.op0().make_typecast(underlying_type);
1917  expr.type()=underlying_type;
1918  }
1919  else if(is_numeric_type(final_type0))
1920  {
1921  expr.type()=type0;
1922  }
1923  else if(final_type0.id()==ID_pointer)
1924  {
1925  expr.type()=type0;
1927  }
1928  else
1929  {
1931  error() << "operator `" << statement
1932  << "' not defined for type `"
1933  << to_string(type0) << "'" << eom;
1934  throw 0;
1935  }
1936  }
1937  else if(has_prefix(id2string(statement), "assign"))
1939  else if(statement==ID_function_call)
1942  else if(statement==ID_statement_expression)
1944  else if(statement==ID_gcc_conditional_expression)
1946  else
1947  {
1949  error() << "unknown side effect: " << statement << eom;
1950  throw 0;
1951  }
1952 }
1953 
1956 {
1957  if(expr.operands().size()!=2)
1958  {
1960  error() << "function_call side effect expects two operands" << eom;
1961  throw 0;
1962  }
1963 
1964  exprt &f_op=expr.function();
1965 
1966  // f_op is not yet typechecked, in contrast to the other arguments.
1967  // This is a big special case!
1968 
1969  if(f_op.id()==ID_symbol)
1970  {
1971  irep_idt identifier=to_symbol_expr(f_op).get_identifier();
1972 
1973  asm_label_mapt::const_iterator entry=
1974  asm_label_map.find(identifier);
1975  if(entry!=asm_label_map.end())
1976  identifier=entry->second;
1977 
1978  if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end())
1979  {
1980  // This is an undeclared function.
1981  // Is this a builtin?
1982  if(!builtin_factory(identifier, symbol_table, get_message_handler()))
1983  {
1984  // yes, it's a builtin
1985  }
1986  else
1987  {
1988  // This is an undeclared function that's not a builtin.
1989  // Let's just add it.
1990  // We do a bit of return-type guessing, but just a bit.
1991  typet guessed_return_type = signed_int_type();
1992 
1993  // The following isn't really right and sound, but there
1994  // are too many idiots out there who use malloc and the like
1995  // without the right header file.
1996  if(identifier=="malloc" ||
1997  identifier=="realloc" ||
1998  identifier=="reallocf" ||
1999  identifier=="valloc")
2000  {
2001  guessed_return_type = pointer_type(void_type()); // void *
2002  }
2003 
2004  symbolt new_symbol;
2005 
2006  new_symbol.name=identifier;
2007  new_symbol.base_name=identifier;
2008  new_symbol.location=expr.source_location();
2009  new_symbol.type = code_typet({}, guessed_return_type);
2010  new_symbol.type.set(ID_C_incomplete, true);
2011 
2012  // TODO: should also guess some argument types
2013 
2014  symbolt *symbol_ptr;
2015  move_symbol(new_symbol, symbol_ptr);
2016 
2018  warning() << "function `" << identifier << "' is not declared" << eom;
2019  }
2020  }
2021  }
2022 
2023  // typecheck it now
2024  typecheck_expr(f_op);
2025 
2026  const typet f_op_type=follow(f_op.type());
2027 
2028  if(f_op_type.id()!=ID_pointer)
2029  {
2031  error() << "expected function/function pointer as argument but got `"
2032  << to_string(f_op_type) << "'" << eom;
2033  throw 0;
2034  }
2035 
2036  // do implicit dereference
2037  if(f_op.id()==ID_address_of &&
2038  f_op.get_bool(ID_C_implicit) &&
2039  f_op.operands().size()==1)
2040  {
2041  exprt tmp;
2042  tmp.swap(f_op.op0());
2043  f_op.swap(tmp);
2044  }
2045  else
2046  {
2047  dereference_exprt tmp(f_op, f_op_type.subtype());
2048  tmp.set(ID_C_implicit, true);
2049  tmp.add_source_location()=f_op.source_location();
2050  f_op.swap(tmp);
2051  }
2052 
2053  if(f_op.type().id()!=ID_code)
2054  {
2056  error() << "expected code as argument" << eom;
2057  throw 0;
2058  }
2059 
2060  const code_typet &code_type=to_code_type(f_op.type());
2061 
2062  expr.type()=code_type.return_type();
2063 
2064  exprt tmp=do_special_functions(expr);
2065 
2066  if(tmp.is_not_nil())
2067  expr.swap(tmp);
2068  else
2070 }
2071 
2074 {
2075  const exprt &f_op=expr.function();
2076  const source_locationt &source_location=expr.source_location();
2077 
2078  // some built-in functions
2079  if(f_op.id()!=ID_symbol)
2080  return nil_exprt();
2081 
2082  const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
2083 
2084  if(identifier==CPROVER_PREFIX "same_object")
2085  {
2086  if(expr.arguments().size()!=2)
2087  {
2089  error() << "same_object expects two operands" << eom;
2090  throw 0;
2091  }
2092 
2093  exprt same_object_expr=
2094  same_object(expr.arguments()[0], expr.arguments()[1]);
2095  same_object_expr.add_source_location()=source_location;
2096 
2097  return same_object_expr;
2098  }
2099  else if(identifier==CPROVER_PREFIX "get_must")
2100  {
2101  if(expr.arguments().size()!=2)
2102  {
2104  error() << "get_must expects two operands" << eom;
2105  throw 0;
2106  }
2107 
2109 
2110  binary_predicate_exprt get_must_expr(
2111  expr.arguments()[0], "get_must", expr.arguments()[1]);
2112  get_must_expr.add_source_location()=source_location;
2113 
2114  return std::move(get_must_expr);
2115  }
2116  else if(identifier==CPROVER_PREFIX "get_may")
2117  {
2118  if(expr.arguments().size()!=2)
2119  {
2121  error() << "get_may expects two operands" << eom;
2122  throw 0;
2123  }
2124 
2126 
2127  binary_predicate_exprt get_may_expr(
2128  expr.arguments()[0], "get_may", expr.arguments()[1]);
2129  get_may_expr.add_source_location()=source_location;
2130 
2131  return std::move(get_may_expr);
2132  }
2133  else if(identifier==CPROVER_PREFIX "invalid_pointer")
2134  {
2135  if(expr.arguments().size()!=1)
2136  {
2138  error() << "invalid_pointer expects one operand" << eom;
2139  throw 0;
2140  }
2141 
2142  exprt same_object_expr = invalid_pointer(expr.arguments().front());
2143  same_object_expr.add_source_location()=source_location;
2144 
2145  return same_object_expr;
2146  }
2147  else if(identifier==CPROVER_PREFIX "buffer_size")
2148  {
2149  if(expr.arguments().size()!=1)
2150  {
2152  error() << "buffer_size expects one operand" << eom;
2153  throw 0;
2154  }
2155 
2156  exprt buffer_size_expr("buffer_size", size_type());
2157  buffer_size_expr.operands()=expr.arguments();
2158  buffer_size_expr.add_source_location()=source_location;
2159 
2160  return buffer_size_expr;
2161  }
2162  else if(identifier==CPROVER_PREFIX "is_zero_string")
2163  {
2164  if(expr.arguments().size()!=1)
2165  {
2167  error() << "is_zero_string expects one operand" << eom;
2168  throw 0;
2169  }
2170 
2171  predicate_exprt is_zero_string_expr("is_zero_string");
2172  is_zero_string_expr.operands()=expr.arguments();
2173  is_zero_string_expr.set(ID_C_lvalue, true); // make it an lvalue
2174  is_zero_string_expr.add_source_location()=source_location;
2175 
2176  return std::move(is_zero_string_expr);
2177  }
2178  else if(identifier==CPROVER_PREFIX "zero_string_length")
2179  {
2180  if(expr.arguments().size()!=1)
2181  {
2183  error() << "zero_string_length expects one operand" << eom;
2184  throw 0;
2185  }
2186 
2187  exprt zero_string_length_expr("zero_string_length", size_type());
2188  zero_string_length_expr.operands()=expr.arguments();
2189  zero_string_length_expr.set(ID_C_lvalue, true); // make it an lvalue
2190  zero_string_length_expr.add_source_location()=source_location;
2191 
2192  return zero_string_length_expr;
2193  }
2194  else if(identifier==CPROVER_PREFIX "DYNAMIC_OBJECT")
2195  {
2196  if(expr.arguments().size()!=1)
2197  {
2199  error() << "dynamic_object expects one argument" << eom;
2200  throw 0;
2201  }
2202 
2203  exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
2204  dynamic_object_expr.operands()=expr.arguments();
2205  dynamic_object_expr.add_source_location()=source_location;
2206 
2207  return dynamic_object_expr;
2208  }
2209  else if(identifier==CPROVER_PREFIX "POINTER_OFFSET")
2210  {
2211  if(expr.arguments().size()!=1)
2212  {
2214  error() << "pointer_offset expects one argument" << eom;
2215  throw 0;
2216  }
2217 
2218  exprt pointer_offset_expr=pointer_offset(expr.arguments().front());
2219  pointer_offset_expr.add_source_location()=source_location;
2220 
2221  return typecast_exprt::conditional_cast(pointer_offset_expr, expr.type());
2222  }
2223  else if(identifier == CPROVER_PREFIX "OBJECT_SIZE")
2224  {
2225  if(expr.arguments().size() != 1)
2226  {
2228  error() << "object_size expects one operand" << eom;
2229  throw 0;
2230  }
2231 
2232  unary_exprt object_size_expr(
2233  ID_object_size, expr.arguments()[0], size_type());
2234  object_size_expr.add_source_location() = source_location;
2235 
2236  return std::move(object_size_expr);
2237  }
2238  else if(identifier==CPROVER_PREFIX "POINTER_OBJECT")
2239  {
2240  if(expr.arguments().size()!=1)
2241  {
2243  error() << "pointer_object expects one argument" << eom;
2244  throw 0;
2245  }
2246 
2247  exprt pointer_object_expr = pointer_object(expr.arguments().front());
2248  pointer_object_expr.add_source_location() = source_location;
2249 
2250  return typecast_exprt::conditional_cast(pointer_object_expr, expr.type());
2251  }
2252  else if(identifier=="__builtin_bswap16" ||
2253  identifier=="__builtin_bswap32" ||
2254  identifier=="__builtin_bswap64")
2255  {
2257 
2258  if(expr.arguments().size()!=1)
2259  {
2261  error() << identifier << " expects one operand" << eom;
2262  throw 0;
2263  }
2264 
2265  // these are hard-wired to 8 bits according to the gcc manual
2266  bswap_exprt bswap_expr(expr.arguments().front(), 8, expr.type());
2267  bswap_expr.add_source_location()=source_location;
2268 
2269  return std::move(bswap_expr);
2270  }
2271  else if(identifier=="__builtin_nontemporal_load")
2272  {
2274 
2275  if(expr.arguments().size()!=1)
2276  {
2278  error() << identifier << " expects one operand" << eom;
2279  throw 0;
2280  }
2281 
2282  // these return the subtype of the argument
2283  exprt &ptr_arg=expr.arguments().front();
2284 
2285  if(ptr_arg.type().id()!=ID_pointer)
2286  {
2288  error() << "__builtin_nontemporal_load takes pointer as argument" << eom;
2289  throw 0;
2290  }
2291 
2292  expr.type()=expr.arguments().front().type().subtype();
2293 
2294  return expr;
2295  }
2296  else if(
2297  identifier == "__builtin_fpclassify" ||
2298  identifier == CPROVER_PREFIX "fpclassify")
2299  {
2300  if(expr.arguments().size() != 6)
2301  {
2303  error() << identifier << " expects six arguments" << eom;
2304  throw 0;
2305  }
2306 
2307  // This gets 5 integers followed by a float or double.
2308  // The five integers are the return values for the cases
2309  // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO.
2310  // gcc expects this to be able to produce compile-time constants.
2311 
2312  const exprt &fp_value = expr.arguments()[5];
2313 
2314  if(fp_value.type().id() != ID_floatbv)
2315  {
2316  error().source_location = fp_value.source_location();
2317  error() << "non-floating-point argument for " << identifier << eom;
2318  throw 0;
2319  }
2320 
2321  const auto &floatbv_type = to_floatbv_type(fp_value.type());
2322 
2323  const exprt zero = ieee_floatt::zero(floatbv_type).to_expr();
2324 
2325  const auto &arguments = expr.arguments();
2326 
2327  return if_exprt(
2328  isnan_exprt(fp_value),
2329  arguments[0],
2330  if_exprt(
2331  isinf_exprt(fp_value),
2332  arguments[1],
2333  if_exprt(
2334  isnormal_exprt(fp_value),
2335  arguments[2],
2336  if_exprt(
2337  ieee_float_equal_exprt(fp_value, zero),
2338  arguments[4],
2339  arguments[3])))); // subnormal
2340  }
2341  else if(identifier==CPROVER_PREFIX "isnanf" ||
2342  identifier==CPROVER_PREFIX "isnand" ||
2343  identifier==CPROVER_PREFIX "isnanld" ||
2344  identifier=="__builtin_isnan")
2345  {
2346  if(expr.arguments().size()!=1)
2347  {
2349  error() << "isnan expects one operand" << eom;
2350  throw 0;
2351  }
2352 
2353  isnan_exprt isnan_expr(expr.arguments().front());
2354  isnan_expr.add_source_location()=source_location;
2355 
2356  return typecast_exprt::conditional_cast(isnan_expr, expr.type());
2357  }
2358  else if(identifier==CPROVER_PREFIX "isfinitef" ||
2359  identifier==CPROVER_PREFIX "isfinited" ||
2360  identifier==CPROVER_PREFIX "isfiniteld")
2361  {
2362  if(expr.arguments().size()!=1)
2363  {
2365  error() << "isfinite expects one operand" << eom;
2366  throw 0;
2367  }
2368 
2369  isfinite_exprt isfinite_expr(expr.arguments().front());
2370  isfinite_expr.add_source_location()=source_location;
2371 
2372  return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
2373  }
2374  else if(identifier==CPROVER_PREFIX "inf" ||
2375  identifier=="__builtin_inf")
2376  {
2377  constant_exprt inf_expr=
2380  inf_expr.add_source_location()=source_location;
2381 
2382  return std::move(inf_expr);
2383  }
2384  else if(identifier==CPROVER_PREFIX "inff")
2385  {
2386  constant_exprt inff_expr=
2389  inff_expr.add_source_location()=source_location;
2390 
2391  return std::move(inff_expr);
2392  }
2393  else if(identifier==CPROVER_PREFIX "infl")
2394  {
2396  constant_exprt infl_expr=
2398  infl_expr.add_source_location()=source_location;
2399 
2400  return std::move(infl_expr);
2401  }
2402  else if(identifier==CPROVER_PREFIX "abs" ||
2403  identifier==CPROVER_PREFIX "labs" ||
2404  identifier==CPROVER_PREFIX "llabs" ||
2405  identifier==CPROVER_PREFIX "fabs" ||
2406  identifier==CPROVER_PREFIX "fabsf" ||
2407  identifier==CPROVER_PREFIX "fabsl")
2408  {
2409  if(expr.arguments().size()!=1)
2410  {
2412  error() << "abs-functions expect one operand" << eom;
2413  throw 0;
2414  }
2415 
2416  abs_exprt abs_expr(expr.arguments().front());
2417  abs_expr.add_source_location()=source_location;
2418 
2419  return std::move(abs_expr);
2420  }
2421  else if(identifier==CPROVER_PREFIX "allocate")
2422  {
2423  if(expr.arguments().size()!=2)
2424  {
2426  error() << "allocate expects two operands" << eom;
2427  throw 0;
2428  }
2429 
2430  side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
2431  malloc_expr.operands()=expr.arguments();
2432 
2433  return std::move(malloc_expr);
2434  }
2435  else if(
2436  identifier == CPROVER_PREFIX "r_ok" || identifier == CPROVER_PREFIX "w_ok")
2437  {
2438  if(expr.arguments().size() != 2)
2439  {
2441  error() << identifier << " expects two operands" << eom;
2442  throw 0;
2443  }
2444 
2445  irep_idt id = identifier == CPROVER_PREFIX "r_ok" ? ID_r_ok : ID_w_ok;
2446 
2447  predicate_exprt ok_expr(id, expr.arguments()[0], expr.arguments()[1]);
2448  ok_expr.add_source_location() = source_location;
2449 
2450  return std::move(ok_expr);
2451  }
2452  else if(identifier==CPROVER_PREFIX "isinff" ||
2453  identifier==CPROVER_PREFIX "isinfd" ||
2454  identifier==CPROVER_PREFIX "isinfld" ||
2455  identifier=="__builtin_isinf")
2456  {
2457  if(expr.arguments().size()!=1)
2458  {
2460  error() << identifier << " expects one operand" << eom;
2461  throw 0;
2462  }
2463 
2464  isinf_exprt isinf_expr(expr.arguments().front());
2465  isinf_expr.add_source_location()=source_location;
2466 
2467  return typecast_exprt::conditional_cast(isinf_expr, expr.type());
2468  }
2469  else if(identifier == "__builtin_isinf_sign")
2470  {
2471  if(expr.arguments().size() != 1)
2472  {
2474  error() << identifier << " expects one operand" << eom;
2475  throw 0;
2476  }
2477 
2478  // returns 1 for +inf and -1 for -inf, and 0 otherwise
2479 
2480  const exprt &fp_value = expr.arguments().front();
2481 
2482  isinf_exprt isinf_expr(fp_value);
2483  isinf_expr.add_source_location() = source_location;
2484 
2485  return if_exprt(
2486  isinf_exprt(fp_value),
2487  if_exprt(
2488  sign_exprt(fp_value),
2489  from_integer(-1, expr.type()),
2490  from_integer(1, expr.type())),
2491  from_integer(0, expr.type()));
2492  }
2493  else if(identifier == CPROVER_PREFIX "isnormalf" ||
2494  identifier == CPROVER_PREFIX "isnormald" ||
2495  identifier == CPROVER_PREFIX "isnormalld" ||
2496  identifier == "__builtin_isnormal")
2497  {
2498  if(expr.arguments().size()!=1)
2499  {
2501  error() << identifier << " expects one operand" << eom;
2502  throw 0;
2503  }
2504 
2505  const exprt &fp_value = expr.arguments()[0];
2506 
2507  if(fp_value.type().id() != ID_floatbv)
2508  {
2509  error().source_location = fp_value.source_location();
2510  error() << "non-floating-point argument for " << identifier << eom;
2511  throw 0;
2512  }
2513 
2514  isnormal_exprt isnormal_expr(expr.arguments().front());
2515  isnormal_expr.add_source_location()=source_location;
2516 
2517  return typecast_exprt::conditional_cast(isnormal_expr, expr.type());
2518  }
2519  else if(identifier==CPROVER_PREFIX "signf" ||
2520  identifier==CPROVER_PREFIX "signd" ||
2521  identifier==CPROVER_PREFIX "signld" ||
2522  identifier=="__builtin_signbit" ||
2523  identifier=="__builtin_signbitf" ||
2524  identifier=="__builtin_signbitl")
2525  {
2526  if(expr.arguments().size()!=1)
2527  {
2529  error() << identifier << " expects one operand" << eom;
2530  throw 0;
2531  }
2532 
2533  sign_exprt sign_expr(expr.arguments().front());
2534  sign_expr.add_source_location()=source_location;
2535 
2536  return typecast_exprt::conditional_cast(sign_expr, expr.type());
2537  }
2538  else if(identifier=="__builtin_popcount" ||
2539  identifier=="__builtin_popcountl" ||
2540  identifier=="__builtin_popcountll" ||
2541  identifier=="__popcnt16" ||
2542  identifier=="__popcnt" ||
2543  identifier=="__popcnt64")
2544  {
2545  if(expr.arguments().size()!=1)
2546  {
2548  error() << identifier << " expects one operand" << eom;
2549  throw 0;
2550  }
2551 
2552  popcount_exprt popcount_expr(expr.arguments().front(), expr.type());
2553  popcount_expr.add_source_location()=source_location;
2554 
2555  return std::move(popcount_expr);
2556  }
2557  else if(identifier==CPROVER_PREFIX "equal")
2558  {
2559  if(expr.arguments().size()!=2)
2560  {
2562  error() << "equal expects two operands" << eom;
2563  throw 0;
2564  }
2565 
2566  equal_exprt equality_expr;
2567  equality_expr.operands()=expr.arguments();
2568  equality_expr.add_source_location()=source_location;
2569 
2570  if(!base_type_eq(equality_expr.lhs().type(),
2571  equality_expr.rhs().type(), *this))
2572  {
2574  error() << "equal expects two operands of same type" << eom;
2575  throw 0;
2576  }
2577 
2578  return std::move(equality_expr);
2579  }
2580  else if(identifier=="__builtin_expect")
2581  {
2582  // This is a gcc extension to provide branch prediction.
2583  // We compile it away, but adding some IR instruction for
2584  // this would clearly be an option. Note that the type
2585  // of the return value is wired to "long", i.e.,
2586  // this may trigger a type conversion due to the signature
2587  // of this function.
2588  if(expr.arguments().size()!=2)
2589  {
2591  error() << "__builtin_expect expects two arguments" << eom;
2592  throw 0;
2593  }
2594 
2595  return typecast_exprt(expr.arguments()[0], expr.type());
2596  }
2597  else if(identifier=="__builtin_object_size")
2598  {
2599  // this is a gcc extension to provide information about
2600  // object sizes at compile time
2601  // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
2602 
2603  if(expr.arguments().size()!=2)
2604  {
2606  error() << "__builtin_object_size expects two arguments" << eom;
2607  throw 0;
2608  }
2609 
2610  make_constant(expr.arguments()[1]);
2611 
2612  mp_integer arg1;
2613 
2614  if(expr.arguments()[1].is_true())
2615  arg1=1;
2616  else if(expr.arguments()[1].is_false())
2617  arg1=0;
2618  else if(to_integer(expr.arguments()[1], arg1))
2619  {
2621  error() << "__builtin_object_size expects constant as second argument, "
2622  << "but got " << to_string(expr.arguments()[1]) << eom;
2623  throw 0;
2624  }
2625 
2626  exprt tmp;
2627 
2628  // the following means "don't know"
2629  if(arg1==0 || arg1==1)
2630  {
2631  tmp=from_integer(-1, size_type());
2632  tmp.add_source_location()=f_op.source_location();
2633  }
2634  else
2635  {
2636  tmp=from_integer(0, size_type());
2637  tmp.add_source_location()=f_op.source_location();
2638  }
2639 
2640  return tmp;
2641  }
2642  else if(identifier=="__builtin_choose_expr")
2643  {
2644  // this is a gcc extension similar to ?:
2645  if(expr.arguments().size()!=3)
2646  {
2648  error() << "__builtin_choose_expr expects three arguments" << eom;
2649  throw 0;
2650  }
2651 
2652  expr.arguments()[0].make_typecast(bool_typet());
2653  make_constant(expr.arguments()[0]);
2654 
2655  if(expr.arguments()[0].is_true())
2656  return expr.arguments()[1];
2657  else
2658  return expr.arguments()[2];
2659  }
2660  else if(identifier=="__builtin_constant_p")
2661  {
2662  // this is a gcc extension to tell whether the argument
2663  // is known to be a compile-time constant
2664  if(expr.arguments().size()!=1)
2665  {
2667  error() << "__builtin_constant_p expects one argument" << eom;
2668  throw 0;
2669  }
2670 
2671  // try to produce constant
2672  exprt tmp1=expr.arguments().front();
2673  simplify(tmp1, *this);
2674 
2675  bool is_constant=false;
2676 
2677  // Need to do some special treatment for string literals,
2678  // which are (void *)&("lit"[0])
2679  if(tmp1.id()==ID_typecast &&
2680  tmp1.operands().size()==1 &&
2681  tmp1.op0().id()==ID_address_of &&
2682  tmp1.op0().operands().size()==1 &&
2683  tmp1.op0().op0().id()==ID_index &&
2684  tmp1.op0().op0().operands().size()==2 &&
2685  tmp1.op0().op0().op0().id()==ID_string_constant)
2686  {
2687  is_constant=true;
2688  }
2689  else
2690  is_constant=tmp1.is_constant();
2691 
2692  exprt tmp2=from_integer(is_constant, expr.type());
2693  tmp2.add_source_location()=source_location;
2694 
2695  return tmp2;
2696  }
2697  else if(identifier=="__builtin_classify_type")
2698  {
2699  // This is a gcc/clang extension that produces an integer
2700  // constant for the type of the argument expression.
2701  if(expr.arguments().size()!=1)
2702  {
2704  error() << "__builtin_classify_type expects one argument" << eom;
2705  throw 0;
2706  }
2707 
2708  exprt object=expr.arguments()[0];
2709 
2710  // The value doesn't matter at all, we only care about the type.
2711  // Need to sync with typeclass.h.
2712  typet type = follow(object.type());
2713 
2714  // use underlying type for bit fields
2715  if(type.id() == ID_c_bit_field)
2716  type = to_c_bit_field_type(type).subtype();
2717 
2718  unsigned type_number;
2719 
2720  if(type.id() == ID_bool || type.id() == ID_c_bool)
2721  {
2722  // clang returns 4 for _Bool, gcc treats these as 'int'.
2723  type_number =
2725  ? 4u
2726  : 1u;
2727  }
2728  else
2729  {
2730  type_number =
2731  type.id() == ID_empty
2732  ? 0u
2733  : (type.id() == ID_bool || type.id() == ID_c_bool)
2734  ? 4u
2735  : (type.id() == ID_pointer || type.id() == ID_array)
2736  ? 5u
2737  : type.id() == ID_floatbv
2738  ? 8u
2739  : (type.id() == ID_complex && type.subtype().id() == ID_floatbv)
2740  ? 9u
2741  : type.id() == ID_struct
2742  ? 12u
2743  : type.id() == ID_union
2744  ? 13u
2745  : 1u; // int, short, char, enum_tag
2746  }
2747 
2748  exprt tmp=from_integer(type_number, expr.type());
2749  tmp.add_source_location()=source_location;
2750 
2751  return tmp;
2752  }
2753  else if(identifier=="__sync_fetch_and_add" ||
2754  identifier=="__sync_fetch_and_sub" ||
2755  identifier=="__sync_fetch_and_or" ||
2756  identifier=="__sync_fetch_and_and" ||
2757  identifier=="__sync_fetch_and_xor" ||
2758  identifier=="__sync_fetch_and_nand" ||
2759  identifier=="__sync_add_and_fetch" ||
2760  identifier=="__sync_sub_and_fetch" ||
2761  identifier=="__sync_or_and_fetch" ||
2762  identifier=="__sync_and_and_fetch" ||
2763  identifier=="__sync_xor_and_fetch" ||
2764  identifier=="__sync_nand_and_fetch" ||
2765  identifier=="__sync_val_compare_and_swap" ||
2766  identifier=="__sync_lock_test_and_set" ||
2767  identifier=="__sync_lock_release")
2768  {
2769  // These are polymorphic, see
2770  // http://gcc.gnu.org/onlinedocs/gcc-4.1.1/gcc/Atomic-Builtins.html
2771 
2772  // adjust return type of function to match pointer subtype
2773  if(expr.arguments().empty())
2774  {
2776  error() << "__sync_* primitives take as least one argument" << eom;
2777  throw 0;
2778  }
2779 
2780  exprt &ptr_arg=expr.arguments().front();
2781 
2782  if(ptr_arg.type().id()!=ID_pointer)
2783  {
2785  error() << "__sync_* primitives take pointer as first argument" << eom;
2786  throw 0;
2787  }
2788 
2789  expr.type()=expr.arguments().front().type().subtype();
2790 
2791  return expr;
2792  }
2793  else
2794  return nil_exprt();
2795 }
2796 
2801 {
2802  const exprt &f_op=expr.function();
2803  const code_typet &code_type=to_code_type(f_op.type());
2804  exprt::operandst &arguments=expr.arguments();
2805  const code_typet::parameterst &parameter_types=
2806  code_type.parameters();
2807 
2808  // no. of arguments test
2809 
2810  if(code_type.get_bool(ID_C_incomplete))
2811  {
2812  // can't check
2813  }
2814  else if(code_type.is_KnR())
2815  {
2816  // We are generous on KnR; any number is ok.
2817  // We will in missing ones with "NIL".
2818 
2819  while(parameter_types.size()>arguments.size())
2820  arguments.push_back(nil_exprt());
2821  }
2822  else if(code_type.has_ellipsis())
2823  {
2824  if(parameter_types.size()>arguments.size())
2825  {
2827  error() << "not enough function arguments" << eom;
2828  throw 0;
2829  }
2830  }
2831  else if(parameter_types.size()!=arguments.size())
2832  {
2834  error() << "wrong number of function arguments: "
2835  << "expected " << parameter_types.size()
2836  << ", but got " << arguments.size() << eom;
2837  throw 0;
2838  }
2839 
2840  for(std::size_t i=0; i<arguments.size(); i++)
2841  {
2842  exprt &op=arguments[i];
2843 
2844  if(op.is_nil())
2845  {
2846  // ignore
2847  }
2848  else if(i<parameter_types.size())
2849  {
2850  const code_typet::parametert &parameter_type=
2851  parameter_types[i];
2852 
2853  const typet &op_type=parameter_type.type();
2854 
2855  if(op_type.id()==ID_bool &&
2856  op.id()==ID_side_effect &&
2857  op.get(ID_statement)==ID_assign &&
2858  op.type().id()!=ID_bool)
2859  {
2861  warning() << "assignment where Boolean argument is expected" << eom;
2862  }
2863 
2864  implicit_typecast(op, op_type);
2865  }
2866  else
2867  {
2868  // don't know type, just do standard conversion
2869 
2870  const typet &type=follow(op.type());
2871  if(type.id()==ID_array)
2872  {
2873  typet dest_type=pointer_type(void_type());
2874  dest_type.subtype().set(ID_C_constant, true);
2875  implicit_typecast(op, dest_type);
2876  }
2877  }
2878  }
2879 }
2880 
2882 {
2883  // nothing to do
2884 }
2885 
2887 {
2888  if(expr.operands().size()!=1)
2889  {
2891  error() << "operator `" << expr.id()
2892  << "' expects one operand" << eom;
2893  throw 0;
2894  }
2895 
2896  exprt &operand=expr.op0();
2897 
2898  const typet &o_type=follow(operand.type());
2899 
2900  if(o_type.id()==ID_vector)
2901  {
2902  if(is_number(follow(o_type.subtype())))
2903  {
2904  // Vector arithmetic.
2905  expr.type()=operand.type();
2906  return;
2907  }
2908  }
2909 
2911 
2912  if(is_number(operand.type()))
2913  {
2914  expr.type()=operand.type();
2915  return;
2916  }
2917 
2919  error() << "operator `" << expr.id()
2920  << "' not defined for type `"
2921  << to_string(operand.type()) << "'" << eom;
2922  throw 0;
2923 }
2924 
2926 {
2927  if(expr.operands().size()!=1)
2928  {
2930  error() << "operator `" << expr.id()
2931  << "' expects one operand" << eom;
2932  throw 0;
2933  }
2934 
2935  exprt &operand=expr.op0();
2936 
2937  implicit_typecast_bool(operand);
2938 
2939  // This is not quite accurate: the standard says the result
2940  // should be of type 'int'.
2941  // We do 'bool' anyway to get more compact formulae. Eventually,
2942  // this should be achieved by means of simplification, and not
2943  // in the frontend.
2944  expr.type()=bool_typet();
2945 }
2946 
2948  const vector_typet &type0,
2949  const vector_typet &type1)
2950 {
2951  // This is relatively restrictive!
2952 
2953  // compare dimension
2954  mp_integer s0, s1;
2955  if(to_integer(type0.size(), s0))
2956  return false;
2957  if(to_integer(type1.size(), s1))
2958  return false;
2959  if(s0!=s1)
2960  return false;
2961 
2962  // compare subtype
2963  if((type0.subtype().id()==ID_signedbv ||
2964  type0.subtype().id()==ID_unsignedbv) &&
2965  (type1.subtype().id()==ID_signedbv ||
2966  type1.subtype().id()==ID_unsignedbv) &&
2967  to_bitvector_type(type0.subtype()).get_width()==
2968  to_bitvector_type(type1.subtype()).get_width())
2969  return true;
2970 
2971  return type0.subtype()==type1.subtype();
2972 }
2973 
2975 {
2976  if(expr.operands().size()!=2)
2977  {
2979  error() << "operator `" << expr.id()
2980  << "' expects two operands" << eom;
2981  throw 0;
2982  }
2983 
2984  exprt &op0=expr.op0();
2985  exprt &op1=expr.op1();
2986 
2987  const typet o_type0=follow(op0.type());
2988  const typet o_type1=follow(op1.type());
2989 
2990  if(o_type0.id()==ID_vector &&
2991  o_type1.id()==ID_vector)
2992  {
2994  to_vector_type(o_type0), to_vector_type(o_type1)) &&
2995  is_number(follow(o_type0.subtype())))
2996  {
2997  // Vector arithmetic has fairly strict typing rules, no promotion
2998  if(o_type0!=o_type1)
2999  op1.make_typecast(op0.type());
3000  expr.type()=op0.type();
3001  return;
3002  }
3003  }
3004  else if(
3005  o_type0.id() == ID_vector && o_type1.id() != ID_vector &&
3006  is_number(o_type1))
3007  {
3008  // convert op1 to the vector type
3009  op1.make_typecast(o_type0);
3010  expr.type() = o_type0;
3011  return;
3012  }
3013  else if(
3014  o_type0.id() != ID_vector && o_type1.id() == ID_vector &&
3015  is_number(o_type0))
3016  {
3017  // convert op0 to the vector type
3018  op0.make_typecast(o_type1);
3019  expr.type() = o_type1;
3020  return;
3021  }
3022 
3023  // promote!
3024 
3025  implicit_typecast_arithmetic(op0, op1);
3026 
3027  const typet &type0=follow(op0.type());
3028  const typet &type1=follow(op1.type());
3029 
3030  if(expr.id()==ID_plus || expr.id()==ID_minus ||
3031  expr.id()==ID_mult || expr.id()==ID_div)
3032  {
3033  if(type0.id()==ID_pointer || type1.id()==ID_pointer)
3034  {
3036  return;
3037  }
3038  else if(type0==type1)
3039  {
3040  if(is_number(type0))
3041  {
3042  expr.type()=type0;
3043  return;
3044  }
3045  }
3046  }
3047  else if(expr.id()==ID_mod)
3048  {
3049  if(type0==type1)
3050  {
3051  if(type0.id()==ID_signedbv || type0.id()==ID_unsignedbv)
3052  {
3053  expr.type()=type0;
3054  return;
3055  }
3056  }
3057  }
3058  else if(expr.id()==ID_bitand ||
3059  expr.id()==ID_bitxor ||
3060  expr.id()==ID_bitor)
3061  {
3062  if(type0==type1)
3063  {
3064  if(is_number(type0))
3065  {
3066  expr.type()=type0;
3067  return;
3068  }
3069  else if(type0.id()==ID_bool)
3070  {
3071  if(expr.id()==ID_bitand)
3072  expr.id(ID_and);
3073  else if(expr.id()==ID_bitor)
3074  expr.id(ID_or);
3075  else if(expr.id()==ID_bitxor)
3076  expr.id(ID_xor);
3077  else
3078  UNREACHABLE;
3079  expr.type()=type0;
3080  return;
3081  }
3082  }
3083  }
3084 
3086  error() << "operator `" << expr.id()
3087  << "' not defined for types `"
3088  << to_string(o_type0) << "' and `"
3089  << to_string(o_type1) << "'" << eom;
3090  throw 0;
3091 }
3092 
3094 {
3095  assert(expr.id()==ID_shl || expr.id()==ID_shr);
3096 
3097  exprt &op0=expr.op0();
3098  exprt &op1=expr.op1();
3099 
3100  const typet o_type0=follow(op0.type());
3101  const typet o_type1=follow(op1.type());
3102 
3103  if(o_type0.id()==ID_vector &&
3104  o_type1.id()==ID_vector)
3105  {
3106  if(follow(o_type0.subtype())==follow(o_type1.subtype()) &&
3107  is_number(follow(o_type0.subtype())))
3108  {
3109  // {a0, a1, ..., an} >> {b0, b1, ..., bn} ==
3110  // {a0 >> b0, a1 >> b1, ..., an >> bn}
3111  // Fairly strict typing rules, no promotion
3112  expr.type()=op0.type();
3113  return;
3114  }
3115  }
3116 
3117  if(o_type0.id()==ID_vector &&
3118  is_number(follow(o_type0.subtype())) &&
3119  is_number(o_type1))
3120  {
3121  // {a0, a1, ..., an} >> b == {a0 >> b, a1 >> b, ..., an >> b}
3122  expr.type()=op0.type();
3123  return;
3124  }
3125 
3126  // must do the promotions _separately_!
3129 
3130  if(is_number(op0.type()) &&
3131  is_number(op1.type()))
3132  {
3133  expr.type()=op0.type();
3134 
3135  if(expr.id()==ID_shr) // shifting operation depends on types
3136  {
3137  const typet &op0_type=follow(op0.type());
3138 
3139  if(op0_type.id()==ID_unsignedbv)
3140  {
3141  expr.id(ID_lshr);
3142  return;
3143  }
3144  else if(op0_type.id()==ID_signedbv)
3145  {
3146  expr.id(ID_ashr);
3147  return;
3148  }
3149  }
3150 
3151  return;
3152  }
3153 
3155  error() << "operator `" << expr.id()
3156  << "' not defined for types `"
3157  << to_string(o_type0) << "' and `"
3158  << to_string(o_type1) << "'" << eom;
3159  throw 0;
3160 }
3161 
3163 {
3164  const typet &type=expr.type();
3165  assert(type.id()==ID_pointer);
3166 
3167  typet subtype=type.subtype();
3168 
3169  if(subtype.id()==ID_incomplete_struct)
3170  {
3172  error() << "pointer arithmetic with unknown object size" << eom;
3173  throw 0;
3174  }
3175 }
3176 
3178 {
3179  assert(expr.operands().size()==2);
3180 
3181  exprt &op0=expr.op0();
3182  exprt &op1=expr.op1();
3183 
3184  const typet &type0=follow(op0.type());
3185  const typet &type1=follow(op1.type());
3186 
3187  if(expr.id()==ID_minus ||
3188  (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_minus))
3189  {
3190  if(type0.id()==ID_pointer &&
3191  type1.id()==ID_pointer)
3192  {
3193  // We should check the subtypes, and complain if
3194  // they are really different.
3195  expr.type()=pointer_diff_type();
3198  return;
3199  }
3200 
3201  if(type0.id()==ID_pointer &&
3202  (type1.id()==ID_bool ||
3203  type1.id()==ID_c_bool ||
3204  type1.id()==ID_unsignedbv ||
3205  type1.id()==ID_signedbv ||
3206  type1.id()==ID_c_bit_field ||
3207  type1.id()==ID_c_enum_tag))
3208  {
3210  make_index_type(op1);
3211  expr.type()=type0;
3212  return;
3213  }
3214  }
3215  else if(expr.id()==ID_plus ||
3216  (expr.id()==ID_side_effect && expr.get(ID_statement)==ID_assign_plus))
3217  {
3218  exprt *p_op, *int_op;
3219 
3220  if(type0.id()==ID_pointer)
3221  {
3222  p_op=&op0;
3223  int_op=&op1;
3224  }
3225  else if(type1.id()==ID_pointer)
3226  {
3227  p_op=&op1;
3228  int_op=&op0;
3229  }
3230  else
3231  {
3232  p_op=int_op=nullptr;
3233  UNREACHABLE;
3234  }
3235 
3236  const typet &int_op_type=follow(int_op->type());
3237 
3238  if(int_op_type.id()==ID_bool ||
3239  int_op_type.id()==ID_c_bool ||
3240  int_op_type.id()==ID_unsignedbv ||
3241  int_op_type.id()==ID_signedbv ||
3242  int_op_type.id()==ID_c_bit_field ||
3243  int_op_type.id()==ID_c_enum_tag)
3244  {
3246  make_index_type(*int_op);
3247  expr.type()=p_op->type();
3248  return;
3249  }
3250  }
3251 
3252  irep_idt op_name;
3253 
3254  if(expr.id()==ID_side_effect)
3255  op_name=to_side_effect_expr(expr).get_statement();
3256  else
3257  op_name=expr.id();
3258 
3260  error() << "operator `" << op_name
3261  << "' not defined for types `"
3262  << to_string(type0) << "' and `"
3263  << to_string(type1) << "'" << eom;
3264  throw 0;
3265 }
3266 
3268 {
3269  if(expr.operands().size()!=2)
3270  {
3272  error() << "operator `" << expr.id()
3273  << "' expects two operands" << eom;
3274  throw 0;
3275  }
3276 
3277  implicit_typecast_bool(expr.op0());
3278  implicit_typecast_bool(expr.op1());
3279 
3280  // This is not quite accurate: the standard says the result
3281  // should be of type 'int'.
3282  // We do 'bool' anyway to get more compact formulae. Eventually,
3283  // this should be achieved by means of simplification, and not
3284  // in the frontend.
3285  expr.type()=bool_typet();
3286 }
3287 
3289  side_effect_exprt &expr)
3290 {
3291  if(expr.operands().size()!=2)
3292  {
3294  error() << "operator `" << expr.get_statement()
3295  << "' expects two operands" << eom;
3296  throw 0;
3297  }
3298 
3299  const irep_idt &statement=expr.get_statement();
3300 
3301  exprt &op0=expr.op0();
3302  exprt &op1=expr.op1();
3303 
3304  {
3305  const typet &type0=op0.type();
3306 
3307  if(type0.id()==ID_empty)
3308  {
3310  error() << "cannot assign void" << eom;
3311  throw 0;
3312  }
3313 
3314  if(!op0.get_bool(ID_C_lvalue))
3315  {
3317  error() << "assignment error: `" << to_string(op0)
3318  << "' not an lvalue" << eom;
3319  throw 0;
3320  }
3321 
3322  if(type0.get_bool(ID_C_constant))
3323  {
3325  error() << "`" << to_string(op0)
3326  << "' is constant" << eom;
3327  throw 0;
3328  }
3329 
3330  // refuse to assign arrays
3331  if(type0.id()==ID_array ||
3332  type0.id()==ID_incomplete_array)
3333  {
3335  error() << "direct assignments to arrays not permitted" << eom;
3336  throw 0;
3337  }
3338  }
3339 
3340  // Add a cast to the underlying type for bit fields.
3341  // In particular, sizeof(s.f=1) works for bit fields.
3342  if(op0.type().id()==ID_c_bit_field)
3343  op0.make_typecast(op0.type().subtype());
3344 
3345  const typet o_type0=op0.type();
3346  const typet o_type1=op1.type();
3347 
3348  expr.type()=o_type0;
3349 
3350  if(statement==ID_assign)
3351  {
3352  implicit_typecast(op1, o_type0);
3353  return;
3354  }
3355  else if(statement==ID_assign_shl ||
3356  statement==ID_assign_shr)
3357  {
3359 
3360  if(is_number(op1.type()))
3361  {
3362  if(statement==ID_assign_shl)
3363  {
3364  return;
3365  }
3366  else // assign_shr
3367  {
3368  // distinguish arithmetic from logical shifts by looking at type
3369 
3370  typet underlying_type=op0.type();
3371 
3372  if(underlying_type.id()==ID_c_enum_tag)
3373  {
3374  const typet &c_enum_type=
3375  follow_tag(to_c_enum_tag_type(underlying_type));
3376  underlying_type=c_enum_type.subtype();
3377  }
3378 
3379  if(underlying_type.id()==ID_unsignedbv ||
3380  underlying_type.id()==ID_c_bool)
3381  {
3382  expr.set(ID_statement, ID_assign_lshr);
3383  return;
3384  }
3385  else if(underlying_type.id()==ID_signedbv)
3386  {
3387  expr.set(ID_statement, ID_assign_ashr);
3388  return;
3389  }
3390  }
3391  }
3392  }
3393  else if(statement==ID_assign_bitxor ||
3394  statement==ID_assign_bitand ||
3395  statement==ID_assign_bitor)
3396  {
3397  // these are more restrictive
3398  if(o_type0.id()==ID_bool ||
3399  o_type0.id()==ID_c_bool)
3400  {
3402  if(op1.type().id()==ID_bool ||
3403  op1.type().id()==ID_c_bool ||
3404  op1.type().id()==ID_c_enum_tag ||
3405  op1.type().id()==ID_unsignedbv ||
3406  op1.type().id()==ID_signedbv)
3407  return;
3408  }
3409  else if(o_type0.id()==ID_c_enum_tag ||
3410  o_type0.id()==ID_unsignedbv ||
3411  o_type0.id()==ID_signedbv ||
3412  o_type0.id()==ID_c_bit_field)
3413  {
3414  implicit_typecast(op1, o_type0);
3415  return;
3416  }
3417  else if(o_type0.id()==ID_vector &&
3418  o_type1.id()==ID_vector)
3419  {
3420  // We are willing to do a modest amount of conversion
3422  to_vector_type(o_type0), to_vector_type(o_type1)))
3423  {
3424  if(o_type0!=o_type1)
3425  op1.make_typecast(o_type0);
3426  return;
3427  }
3428  }
3429  }
3430  else
3431  {
3432  if(o_type0.id()==ID_pointer &&
3433  (statement==ID_assign_minus || statement==ID_assign_plus))
3434  {
3436  return;
3437  }
3438  else if(o_type0.id()==ID_vector &&
3439  o_type1.id()==ID_vector)
3440  {
3441  // We are willing to do a modest amount of conversion
3443  to_vector_type(o_type0), to_vector_type(o_type1)))
3444  {
3445  if(o_type0!=o_type1)
3446  op1.make_typecast(o_type0);
3447  return;
3448  }
3449  }
3450  else if(o_type0.id()==ID_bool ||
3451  o_type0.id()==ID_c_bool)
3452  {
3454  if(op1.type().id()==ID_bool ||
3455  op1.type().id()==ID_c_bool ||
3456  op1.type().id()==ID_c_enum_tag ||
3457  op1.type().id()==ID_unsignedbv ||
3458  op1.type().id()==ID_signedbv)
3459  return;
3460  }
3461  else
3462  {
3463  implicit_typecast(op1, o_type0);
3464 
3465  if(is_number(op1.type()) ||
3466  op1.type().id()==ID_bool ||
3467  op1.type().id()==ID_c_bool ||
3468  op1.type().id()==ID_c_enum_tag)
3469  return;
3470  }
3471  }
3472 
3474  error() << "assignment `" << statement
3475  << "' not defined for types `"
3476  << to_string(o_type0) << "' and `"
3477  << to_string(o_type1) << "'" << eom;
3478 
3479  throw 0;
3480 }
3481 
3483 {
3484  // Floating-point expressions may require a rounding mode.
3485  // ISO 9899:1999 F.7.2 says that the default is "round to nearest".
3486  // Some compilers have command-line options to override.
3487  const auto rounding_mode =
3489  adjust_float_expressions(expr, rounding_mode);
3490 
3491  simplify(expr, *this);
3492 
3493  if(!expr.is_constant() &&
3494  expr.id()!=ID_infinity)
3495  {
3497  error() << "expected constant expression, but got `"
3498  << to_string(expr) << "'" << eom;
3499  throw 0;
3500  }
3501 }
3502 
3504 {
3505  make_constant(expr);
3506  make_index_type(expr);
3507  simplify(expr, *this);
3508 
3509  if(!expr.is_constant() &&
3510  expr.id()!=ID_infinity)
3511  {
3513  error() << "conversion to integer constant failed" << eom;
3514  throw 0;
3515  }
3516 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
virtual void typecheck_expr_binary_boolean(exprt &expr)
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1775
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
Symbolic Execution.
exprt size_of_expr(const typet &type, const namespacet &ns)
std::map< irep_idt, source_locationt > labels_used
struct configt::ansi_ct ansi_c
exprt & true_case()
Definition: std_expr.h:3455
typet void_type()
Definition: c_types.cpp:253
virtual void typecheck_side_effect_assignment(side_effect_exprt &expr)
Semantic type conversion.
Definition: std_expr.h:2277
virtual void implicit_typecast_bool(exprt &expr)
virtual bool is_complete_type(const typet &type) const
BigInt mp_integer
Definition: mp_arith.h:22
void typecheck_declaration(ansi_c_declarationt &)
Base type of functions.
Definition: std_types.h:751
exprt member_offset_expr(const member_exprt &member_expr, const namespacet &ns)
bool is_nil() const
Definition: irep.h:172
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
asm_label_mapt asm_label_map
virtual void typecheck_expr_index(exprt &expr)
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
#define CPROVER_PREFIX
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
codet & find_last_statement()
Definition: std_code.cpp:112
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1398
std::vector< irept > subt
Definition: irep.h:160
virtual void make_constant(exprt &expr)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
Evaluates to true if the operand is infinite.
Definition: std_expr.h:4035
void move_symbol(symbolt &symbol, symbolt *&new_symbol)
bool has_ellipsis() const
Definition: std_types.h:849
Deprecated expression utility functions.
virtual void typecheck_expr_rel_vector(binary_relation_exprt &expr)
unsignedbv_typet unsigned_int_type()
Definition: c_types.cpp:44
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
const irep_idt & get_function() const
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt&#39;s operands.
Definition: expr.h:123
const irep_idt & get_identifier() const
Definition: std_expr.h:176
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
const irep_idt & get_value() const
Definition: std_expr.h:4403
std::vector< parametert > parameterst
Definition: std_types.h:754
Type with multiple subtypes.
Definition: type.h:169
id_type_mapt parameter_map
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
Evaluates to true if the operand is a normal number.
Definition: std_expr.h:4131
bool has_component_rec(const typet &type, const irep_idt &component_name, const namespacet &ns)
typet & type()
Return the type of the expression.
Definition: expr.h:68
unsignedbv_typet size_type()
Definition: c_types.cpp:58
The Boolean type.
Definition: std_types.h:28
Symbol table entry.
Definition: symbol.h:27
static code_blockt from_list(const std::list< codet > &_list)
Definition: std_code.h:169
A constant literal expression.
Definition: std_expr.h:4384
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
configt config
Definition: config.cpp:24
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:228
virtual std::string to_string(const exprt &expr)
codet representation of an expression statement.
Definition: std_code.h:1504
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
virtual void typecheck_side_effect_gcc_conditional_expression(side_effect_exprt &expr)
exprt get_component_rec(const exprt &struct_union, const irep_idt &component_name, const namespacet &ns)
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2087
bool is_static_lifetime
Definition: symbol.h:65
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
This adds the rounding mode to floating-point operations, including those in vectors and complex numb...
subt & get_sub()
Definition: irep.h:317
side_effect_exprt & to_side_effect_expr(exprt &expr)
Definition: std_code.h:1620
static ieee_float_spect double_precision()
Definition: ieee_float.h:80
bool builtin_factory(const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh)
Check whether given identifier is a compiler built-in.
symbol_tablet & symbol_table
mstreamt & warning() const
Definition: message.h:391
Equality.
Definition: std_expr.h:1484
virtual void typecheck_expr_cw_va_arg_typeof(exprt &expr)
preprocessort preprocessor
Definition: config.h:119
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:125
virtual void typecheck_expr_symbol(exprt &expr)
static bool is_numeric_type(const typet &src)
const irep_idt & id() const
Definition: irep.h:259
Evaluates to true if the operand is NaN.
Definition: std_expr.h:3989
An expression denoting infinity.
Definition: std_expr.h:4625
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
virtual void typecheck_expr_side_effect(side_effect_exprt &expr)
argumentst & arguments()
Definition: std_code.h:1109
virtual void typecheck_expr_operands(exprt &expr)
ANSI-C Language Type Checking.
ANSI-C Language Type Checking.
A codet representing the declaration of a local variable.
Definition: std_code.h:352
virtual void typecheck_expr_member(exprt &expr)
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:139
The NIL expression.
Definition: std_expr.h:4461
Real part of the expression describing a complex number.
Definition: std_expr.h:2040
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
source_locationt source_location
Definition: message.h:236
The empty type.
Definition: std_types.h:48
Operator to dereference a pointer.
Definition: std_expr.h:3355
The vector type.
Definition: std_types.h:1755
exprt pointer_object(const exprt &p)
virtual void make_index_type(exprt &expr)
virtual void typecheck_expr_binary_arithmetic(exprt &expr)
Union constructor from single element.
Definition: std_expr.h:1840
exprt & op1()
Definition: expr.h:87
mp_integer alignment(const typet &type, const namespacet &ns)
Definition: padding.cpp:21
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
virtual void typecheck_expr_trinary(if_exprt &expr)
virtual void typecheck_expr_unary_boolean(exprt &expr)
mstreamt & error() const
Definition: message.h:386
Generic base class for unary expressions.
Definition: std_expr.h:331
static ieee_float_spect single_precision()
Definition: ieee_float.h:74
virtual void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
const exprt & size() const
Definition: std_types.h:1765
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:948
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1793
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
virtual void typecheck_expr(exprt &expr)
codet representation of a function call statement.
Definition: std_code.h:1036
#define forall_operands(it, expr)
Definition: expr.h:20
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
virtual void typecheck_side_effect_statement_expression(side_effect_exprt &expr)
virtual void typecheck_expr_typecast(exprt &expr)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bitvector_typet index_type()
Definition: c_types.cpp:16
#define Forall_irep(it, irep)
Definition: irep.h:66
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
std::list< codet > clean_code
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt & false_case()
Definition: std_expr.h:3465
const symbolst & symbols
Various predicates over pointers in programs.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
virtual void typecheck_expr_function_identifier(exprt &expr)
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:737
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2291
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
virtual void typecheck_expr_builtin_offsetof(exprt &expr)
Pointer Logic.
bool gcc_vector_types_compatible(const vector_typet &, const vector_typet &)
const irep_idt & display_name() const
Return language specific display name if present.
Definition: symbol.h:55
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...
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
bool is_extern
Definition: symbol.h:66
static eomt eom
Definition: message.h:284
Complex numbers made of pair of given subtype.
Definition: std_types.h:1807
floatbv_typet long_double_type()
Definition: c_types.cpp:201
virtual exprt do_special_functions(side_effect_expr_function_callt &expr)
virtual void implicit_typecast(exprt &expr, const typet &type)
virtual void typecheck_expr_unary_arithmetic(exprt &expr)
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
virtual void typecheck_expr_sizeof(exprt &expr)
message_handlert & get_message_handler()
Definition: message.h:174
bool is_KnR() const
Definition: std_types.h:868
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Definition: std_expr.h:2917
Base type for structs and unions.
Definition: std_types.h:114
mstreamt & result() const
Definition: message.h:396
exprt & index()
Definition: std_expr.h:1631
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
Definition: std_types.h:1442
The popcount (counting the number of bits set to 1) expression.
Definition: std_expr.h:4815
Evaluates to true if the operand is finite.
Definition: std_expr.h:4085
exprt & function()
Definition: std_code.h:1099
exprt invalid_pointer(const exprt &pointer)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
Absolute value.
Definition: std_expr.h:419
Sign of an expression Predicate is true if _op is negative, false otherwise.
Definition: std_expr.h:690
virtual void typecheck_expr_builtin_va_arg(exprt &expr)
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
exprt pointer_offset(const exprt &pointer)
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
virtual void typecheck_expr_pointer_arithmetic(exprt &expr)
const source_locationt & source_location() const
Definition: expr.h:228
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
virtual void typecheck_expr_dereference(exprt &expr)
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
Definition: irep.cpp:305
exprt::operandst & arguments()
Definition: std_code.h:1754
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
void swap(irept &irep)
Definition: irep.h:303
#define Forall_operands(it, expr)
Definition: expr.h:26
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
virtual bool gcc_types_compatible_p(const typet &, const typet &)
source_locationt & add_source_location()
Definition: expr.h:233
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
virtual void implicit_typecast_arithmetic(exprt &expr)
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition: std_types.h:1491
static void add_rounding_mode(exprt &)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv, signedbv, floatbv or fixedbv.
Expression to hold a symbol (variable)
Definition: std_expr.h:143
exprt & op2()
Definition: expr.h:90
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
Definition: ieee_float.h:200
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
virtual void typecheck_type(typet &type)
int8_t s1
Definition: bytecode_info.h:59
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
virtual void typecheck_expr_rel(binary_relation_exprt &expr)
virtual void do_initializer(exprt &initializer, const typet &type, bool force_constant)
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:835
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
ansi_c_declarationt & to_ansi_c_declaration(exprt &expr)
void remove(const irep_namet &name)
Definition: irep.cpp:269
bool is_type
Definition: symbol.h:61
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
virtual void typecheck_expr_address_of(exprt &expr)
virtual void typecheck_expr_constant(exprt &expr)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Definition: invariant.h:485
virtual void typecheck_expr_comma(exprt &expr)
An expression containing a side effect.
Definition: std_code.h:1560
virtual void typecheck_expr_main(exprt &expr)
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
virtual void typecheck_arithmetic_pointer(const exprt &expr)
virtual void typecheck_expr_alignof(exprt &expr)
exprt same_object(const exprt &p1, const exprt &p2)
bool empty() const
Definition: dstring.h:75
exprt & array()
Definition: std_expr.h:1621
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
A base class for shift operators.
Definition: std_expr.h:2866
bitvector_typet char_type()
Definition: c_types.cpp:114
const typet & return_type() const
Definition: std_types.h:883
bool is_macro
Definition: symbol.h:61
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
The byte swap expression.
Definition: std_expr.h:568
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
virtual void typecheck_expr_shifts(shift_exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
Definition: std_types.cpp:53
const irep_idt & get_statement() const
Definition: std_code.h:1586
virtual void typecheck_expr_ptrmember(exprt &expr)
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
virtual void typecheck_code(codet &code)
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
bool simplify(exprt &expr, const namespacet &ns)
A base class for expressions that are predicates, i.e., Boolean-typed.
Definition: std_expr.h:633
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:184
IEEE-floating-point equality.
Definition: std_expr.h:4177
bool is_lvalue
Definition: symbol.h:66
#define forall_irep(it, irep)
Definition: irep.h:62
Array index operator.
Definition: std_expr.h:1595
C Language Type Checking.
virtual void adjust_float_rel(exprt &expr)