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