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