cprover
builtin_functions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "goto_convert_class.h"
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/cprover_prefix.h>
19 #include <util/expr_initializer.h>
21 #include <util/rational.h>
22 #include <util/rational_tools.h>
23 
24 #include <langapi/language_util.h>
25 
26 #include "format_strings.h"
27 #include "class_identifier.h"
28 
30  const exprt &lhs,
31  const symbol_exprt &function,
32  const exprt::operandst &arguments,
33  goto_programt &dest)
34 {
35  const irep_idt &identifier = function.get_identifier();
36 
37  // make it a side effect if there is an LHS
38  if(arguments.size()!=2)
39  {
40  error().source_location=function.find_source_location();
41  error() << "`" << identifier
42  << "' expected to have two arguments" << eom;
43  throw 0;
44  }
45 
46  if(lhs.is_nil())
47  {
48  error().source_location=function.find_source_location();
49  error() << "`" << identifier << "' expected to have LHS" << eom;
50  throw 0;
51  }
52 
53  side_effect_exprt rhs("prob_uniform", lhs.type());
54  rhs.add_source_location()=function.source_location();
55 
56  if(lhs.type().id()!=ID_unsignedbv &&
57  lhs.type().id()!=ID_signedbv)
58  {
59  error().source_location=function.find_source_location();
60  error() << "`" << identifier << "' expected other type" << eom;
61  throw 0;
62  }
63 
64  if(arguments[0].type().id()!=lhs.type().id() ||
65  arguments[1].type().id()!=lhs.type().id())
66  {
67  error().source_location=function.find_source_location();
68  error() << "`" << identifier
69  << "' expected operands to be of same type as LHS" << eom;
70  throw 0;
71  }
72 
73  if(!arguments[0].is_constant() ||
74  !arguments[1].is_constant())
75  {
76  error().source_location=function.find_source_location();
77  error() << "`" << identifier
78  << "' expected operands to be constant literals" << eom;
79  throw 0;
80  }
81 
82  mp_integer lb, ub;
83 
84  if(to_integer(arguments[0], lb) ||
85  to_integer(arguments[1], ub))
86  {
87  error().source_location=function.find_source_location();
88  error() << "error converting operands" << eom;
89  throw 0;
90  }
91 
92  if(lb > ub)
93  {
94  error().source_location=function.find_source_location();
95  error() << "expected lower bound to be smaller or equal to the "
96  << "upper bound" << eom;
97  throw 0;
98  }
99 
100  rhs.copy_to_operands(arguments[0], arguments[1]);
101 
102  code_assignt assignment(lhs, rhs);
103  assignment.add_source_location()=function.source_location();
104  copy(assignment, ASSIGN, dest);
105 }
106 
108  const exprt &lhs,
109  const symbol_exprt &function,
110  const exprt::operandst &arguments,
111  goto_programt &dest)
112 {
113  const irep_idt &identifier = function.get_identifier();
114 
115  // make it a side effect if there is an LHS
116  if(arguments.size()!=2)
117  {
118  error().source_location=function.find_source_location();
119  error() << "`" << identifier << "' expected to have two arguments"
120  << eom;
121  throw 0;
122  }
123 
124  if(lhs.is_nil())
125  {
126  error().source_location=function.find_source_location();
127  error() << "`" << identifier << "' expected to have LHS" << eom;
128  throw 0;
129  }
130 
131  side_effect_exprt rhs("prob_coin", lhs.type());
132  rhs.add_source_location()=function.source_location();
133 
134  if(lhs.type()!=bool_typet())
135  {
136  error().source_location=function.find_source_location();
137  error() << "`" << identifier << "' expected bool" << eom;
138  throw 0;
139  }
140 
141  if(arguments[0].type().id()!=ID_unsignedbv ||
142  arguments[0].id()!=ID_constant)
143  {
144  error().source_location=function.find_source_location();
145  error() << "`" << identifier << "' expected first operand to be "
146  << "a constant literal of type unsigned long" << eom;
147  throw 0;
148  }
149 
150  mp_integer num, den;
151 
152  if(to_integer(arguments[0], num) ||
153  to_integer(arguments[1], den))
154  {
155  error().source_location=function.find_source_location();
156  error() << "error converting operands" << eom;
157  throw 0;
158  }
159 
160  if(num-den > mp_integer(0))
161  {
162  error().source_location=function.find_source_location();
163  error() << "probability has to be smaller than 1" << eom;
164  throw 0;
165  }
166 
167  if(den == mp_integer(0))
168  {
169  error().source_location=function.find_source_location();
170  error() << "denominator may not be zero" << eom;
171  throw 0;
172  }
173 
174  rationalt numerator(num), denominator(den);
175  rationalt prob = numerator / denominator;
176 
177  rhs.copy_to_operands(from_rational(prob));
178 
179  code_assignt assignment(lhs, rhs);
180  assignment.add_source_location()=function.source_location();
181  copy(assignment, ASSIGN, dest);
182 }
183 
185  const exprt &lhs,
186  const symbol_exprt &function,
187  const exprt::operandst &arguments,
188  goto_programt &dest)
189 {
190  const irep_idt &f_id = function.get_identifier();
191 
192  if(f_id==CPROVER_PREFIX "printf" ||
193  f_id=="printf")
194  {
195  typet return_type=
196  static_cast<const typet &>(function.type().find(ID_return_type));
197  side_effect_exprt printf_code(ID_printf, return_type);
198 
199  printf_code.operands()=arguments;
200  printf_code.add_source_location()=function.source_location();
201 
202  if(lhs.is_not_nil())
203  {
204  code_assignt assignment(lhs, printf_code);
205  assignment.add_source_location()=function.source_location();
206  copy(assignment, ASSIGN, dest);
207  }
208  else
209  {
210  printf_code.id(ID_code);
211  printf_code.type()=typet(ID_code);
212  copy(to_code(printf_code), OTHER, dest);
213  }
214  }
215  else
216  UNREACHABLE;
217 }
218 
220  const exprt &lhs,
221  const symbol_exprt &function,
222  const exprt::operandst &arguments,
223  goto_programt &dest)
224 {
225  const irep_idt &f_id = function.get_identifier();
226 
227  if(f_id==CPROVER_PREFIX "scanf")
228  {
229  if(arguments.empty())
230  {
231  error().source_location=function.find_source_location();
232  error() << "scanf takes at least one argument" << eom;
233  throw 0;
234  }
235 
236  irep_idt format_string;
237 
238  if(!get_string_constant(arguments[0], format_string))
239  {
240  // use our model
241  format_token_listt token_list=
242  parse_format_string(id2string(format_string));
243 
244  std::size_t argument_number=1;
245 
246  for(const auto &t : token_list)
247  {
248  typet type=get_type(t);
249 
250  if(type.is_not_nil())
251  {
252  if(argument_number<arguments.size())
253  {
254  const typecast_exprt ptr(
255  arguments[argument_number], pointer_type(type));
256  argument_number++;
257 
258  if(type.id()==ID_array)
259  {
260  #if 0
261  // A string. We first need a nondeterministic size.
263  to_array_type(type).size()=size;
264 
265  const symbolt &tmp_symbol=
267  type, "scanf_string", dest, function.source_location());
268 
269  const address_of_exprt rhs(
270  index_exprt(
271  tmp_symbol.symbol_expr(),
272  from_integer(0, index_type())));
273 
274  // now use array copy
275  codet array_copy_statement;
276  array_copy_statement.set_statement(ID_array_copy);
277  array_copy_statement.operands().resize(2);
278  array_copy_statement.op0()=ptr;
279 \ array_copy_statement.op1()=rhs;
280  array_copy_statement.add_source_location()=
281  function.source_location();
282 
283  copy(array_copy_statement, OTHER, dest);
284  #else
285  const index_exprt lhs(
286  dereference_exprt(ptr, type), from_integer(0, index_type()));
287  const side_effect_expr_nondett rhs(type.subtype());
288  code_assignt assign(lhs, rhs);
289  assign.add_source_location()=function.source_location();
290  copy(assign, ASSIGN, dest);
291  #endif
292  }
293  else
294  {
295  // make it nondet for now
296  const dereference_exprt lhs(ptr, type);
297  const side_effect_expr_nondett rhs(type);
298  code_assignt assign(lhs, rhs);
299  assign.add_source_location()=function.source_location();
300  copy(assign, ASSIGN, dest);
301  }
302  }
303  }
304  }
305  }
306  else
307  {
308  // we'll just do nothing
309  code_function_callt function_call;
310  function_call.lhs()=lhs;
311  function_call.function()=function;
312  function_call.arguments()=arguments;
313  function_call.add_source_location()=function.source_location();
314 
315  copy(function_call, FUNCTION_CALL, dest);
316  }
317  }
318  else
319  UNREACHABLE;
320 }
321 
323  const exprt &lhs,
324  const exprt &function,
325  const exprt::operandst &arguments,
326  goto_programt &dest)
327 {
328  codet input_code;
329  input_code.set_statement(ID_input);
330  input_code.operands()=arguments;
331  input_code.add_source_location()=function.source_location();
332 
333  if(arguments.size()<2)
334  {
335  error().source_location=function.find_source_location();
336  error() << "input takes at least two arguments" << eom;
337  throw 0;
338  }
339 
340  copy(input_code, OTHER, dest);
341 }
342 
344  const exprt &lhs,
345  const exprt &function,
346  const exprt::operandst &arguments,
347  goto_programt &dest)
348 {
349  codet output_code;
350  output_code.set_statement(ID_output);
351  output_code.operands()=arguments;
352  output_code.add_source_location()=function.source_location();
353 
354  if(arguments.size()<2)
355  {
356  error().source_location=function.find_source_location();
357  error() << "output takes at least two arguments" << eom;
358  throw 0;
359  }
360 
361  copy(output_code, OTHER, dest);
362 }
363 
365  const exprt &lhs,
366  const symbol_exprt &function,
367  const exprt::operandst &arguments,
368  goto_programt &dest)
369 {
370  if(lhs.is_not_nil())
371  {
373  error() << "atomic_begin does not expect an LHS" << eom;
374  throw 0;
375  }
376 
377  if(!arguments.empty())
378  {
379  error().source_location=function.find_source_location();
380  error() << "atomic_begin takes no arguments" << eom;
381  throw 0;
382  }
383 
385  t->source_location=function.source_location();
386 }
387 
389  const exprt &lhs,
390  const symbol_exprt &function,
391  const exprt::operandst &arguments,
392  goto_programt &dest)
393 {
394  if(lhs.is_not_nil())
395  {
397  error() << "atomic_end does not expect an LHS" << eom;
398  throw 0;
399  }
400 
401  if(!arguments.empty())
402  {
403  error().source_location=function.find_source_location();
404  error() << "atomic_end takes no arguments" << eom;
405  throw 0;
406  }
407 
409  t->source_location=function.source_location();
410 }
411 
413  const exprt &lhs,
414  const side_effect_exprt &rhs,
415  goto_programt &dest)
416 {
417  if(lhs.is_nil())
418  {
420  error() << "do_cpp_new without lhs is yet to be implemented" << eom;
421  throw 0;
422  }
423 
424  // build size expression
426  static_cast<const exprt &>(rhs.find(ID_sizeof));
427 
428  bool new_array=rhs.get(ID_statement)==ID_cpp_new_array;
429 
430  exprt count;
431 
432  if(new_array)
433  {
434  count=static_cast<const exprt &>(rhs.find(ID_size));
435 
436  if(count.type()!=object_size.type())
437  count.make_typecast(object_size.type());
438 
439  // might have side-effect
440  clean_expr(count, dest, ID_cpp);
441  }
442 
443  exprt tmp_symbol_expr;
444 
445  // is this a placement new?
446  if(rhs.operands().empty()) // no, "regular" one
447  {
448  // call __new or __new_array
449  exprt new_symbol=
450  ns.lookup(new_array?"__new_array":"__new").symbol_expr();
451 
452  const code_typet &code_type=
453  to_code_type(new_symbol.type());
454 
455  const typet &return_type=
456  code_type.return_type();
457 
458  assert(code_type.parameters().size()==1 ||
459  code_type.parameters().size()==2);
460 
461  const symbolt &tmp_symbol =
462  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
463 
464  tmp_symbol_expr=tmp_symbol.symbol_expr();
465 
466  code_function_callt new_call;
467  new_call.function()=new_symbol;
468  if(new_array)
469  new_call.arguments().push_back(count);
470  new_call.arguments().push_back(object_size);
471  new_call.set(ID_C_cxx_alloc_type, lhs.type().subtype());
472  new_call.lhs()=tmp_symbol_expr;
473  new_call.add_source_location()=rhs.source_location();
474 
475  convert(new_call, dest, ID_cpp);
476  }
477  else if(rhs.operands().size()==1)
478  {
479  // call __placement_new
480  exprt new_symbol=
481  ns.lookup(
482  new_array?"__placement_new_array":"__placement_new").symbol_expr();
483 
484  const code_typet &code_type=
485  to_code_type(new_symbol.type());
486 
487  const typet &return_type=code_type.return_type();
488 
489  assert(code_type.parameters().size()==2 ||
490  code_type.parameters().size()==3);
491 
492  const symbolt &tmp_symbol =
493  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
494 
495  tmp_symbol_expr=tmp_symbol.symbol_expr();
496 
497  code_function_callt new_call;
498  new_call.function()=new_symbol;
499  if(new_array)
500  new_call.arguments().push_back(count);
501  new_call.arguments().push_back(object_size);
502  new_call.arguments().push_back(rhs.op0()); // memory location
503  new_call.set(ID_C_cxx_alloc_type, lhs.type().subtype());
504  new_call.lhs()=tmp_symbol_expr;
505  new_call.add_source_location()=rhs.source_location();
506 
507  for(std::size_t i=0; i<code_type.parameters().size(); i++)
508  if(new_call.arguments()[i].type()!=code_type.parameters()[i].type())
509  new_call.arguments()[i].make_typecast(code_type.parameters()[i].type());
510 
511  convert(new_call, dest, ID_cpp);
512  }
513  else
514  {
516  error() << "cpp_new expected to have 0 or 1 operands" << eom;
517  throw 0;
518  }
519 
521  t_n->code=code_assignt(
522  lhs, typecast_exprt(tmp_symbol_expr, lhs.type()));
523  t_n->source_location=rhs.find_source_location();
524 
525  // grab initializer
526  goto_programt tmp_initializer;
527  cpp_new_initializer(lhs, rhs, tmp_initializer);
528 
529  dest.destructive_append(tmp_initializer);
530 }
531 
534  const exprt &lhs,
535  const side_effect_exprt &rhs,
536  goto_programt &dest)
537 {
538  exprt initializer=
539  static_cast<const exprt &>(rhs.find(ID_initializer));
540 
541  if(initializer.is_not_nil())
542  {
543  if(rhs.get_statement()=="cpp_new[]")
544  {
545  // build loop
546  }
547  else if(rhs.get_statement()==ID_cpp_new)
548  {
549  // just one object
550  const dereference_exprt deref_lhs(lhs, rhs.type().subtype());
551 
552  replace_new_object(deref_lhs, initializer);
553  convert(to_code(initializer), dest, ID_cpp);
554  }
555  else
556  UNREACHABLE;
557  }
558 }
559 
561 {
562  if(src.id()==ID_typecast)
563  {
564  assert(src.operands().size()==1);
565  return get_array_argument(src.op0());
566  }
567 
568  if(src.id()!=ID_address_of)
569  {
571  error() << "expected array-pointer as argument" << eom;
572  throw 0;
573  }
574 
575  assert(src.operands().size()==1);
576 
577  if(src.op0().id()!=ID_index)
578  {
580  error() << "expected array-element as argument" << eom;
581  throw 0;
582  }
583 
584  assert(src.op0().operands().size()==2);
585 
586  if(ns.follow(src.op0().op0().type()).id()!=ID_array)
587  {
589  error() << "expected array as argument" << eom;
590  throw 0;
591  }
592 
593  return src.op0().op0();
594 }
595 
597  const irep_idt &id,
598  const exprt &lhs,
599  const symbol_exprt &function,
600  const exprt::operandst &arguments,
601  goto_programt &dest)
602 {
603  if(arguments.size()!=2)
604  {
605  error().source_location=function.find_source_location();
606  error() << id << " expects two arguments" << eom;
607  throw 0;
608  }
609 
610  codet array_op_statement;
611  array_op_statement.set_statement(id);
612  array_op_statement.operands()=arguments;
613  array_op_statement.add_source_location()=function.source_location();
614 
615  // lhs is only used with array_equal, in all other cases it should be nil (as
616  // they are of type void)
617  if(id == ID_array_equal)
618  array_op_statement.copy_to_operands(lhs);
619 
620  copy(array_op_statement, OTHER, dest);
621 }
622 
623 bool is_lvalue(const exprt &expr)
624 {
625  if(expr.id()==ID_index)
626  return is_lvalue(to_index_expr(expr).op0());
627  else if(expr.id()==ID_member)
628  return is_lvalue(to_member_expr(expr).op0());
629  else if(expr.id()==ID_dereference)
630  return true;
631  else if(expr.id()==ID_symbol)
632  return true;
633  else
634  return false;
635 }
636 
638 {
639  // we first strip any typecast
640  if(expr.id()==ID_typecast)
641  return make_va_list(to_typecast_expr(expr).op());
642 
643  // if it's an address of an lvalue, we take that
644  if(expr.id()==ID_address_of &&
645  expr.operands().size()==1 &&
646  is_lvalue(expr.op0()))
647  return expr.op0();
648 
649  return expr;
650 }
651 
654  const exprt &lhs,
655  const symbol_exprt &function,
656  const exprt::operandst &arguments,
657  goto_programt &dest)
658 {
659  if(function.get_bool("#invalid_object"))
660  return; // ignore
661 
662  // lookup symbol
663  const irep_idt &identifier=function.get_identifier();
664 
665  const symbolt *symbol;
666  if(ns.lookup(identifier, symbol))
667  {
668  error().source_location=function.find_source_location();
669  error() << "error: function `" << identifier << "' not found"
670  << eom;
671  throw 0;
672  }
673 
674  if(symbol->type.id()!=ID_code)
675  {
676  error().source_location=function.find_source_location();
677  error() << "error: function `" << identifier
678  << "' type mismatch: expected code" << eom;
679  throw 0;
680  }
681 
682  if(identifier==CPROVER_PREFIX "assume" ||
683  identifier=="__VERIFIER_assume")
684  {
685  if(arguments.size()!=1)
686  {
687  error().source_location=function.find_source_location();
688  error() << "`" << identifier << "' expected to have one argument"
689  << eom;
690  throw 0;
691  }
692 
694  t->guard=arguments.front();
695  t->source_location=function.source_location();
696  t->source_location.set("user-provided", true);
697 
698  // let's double-check the type of the argument
699  if(t->guard.type().id()!=ID_bool)
700  t->guard.make_typecast(bool_typet());
701 
702  if(lhs.is_not_nil())
703  {
704  error().source_location=function.find_source_location();
705  error() << identifier << " expected not to have LHS" << eom;
706  throw 0;
707  }
708  }
709  else if(identifier=="__VERIFIER_error")
710  {
711  if(!arguments.empty())
712  {
713  error().source_location=function.find_source_location();
714  error() << "`" << identifier << "' expected to have no arguments"
715  << eom;
716  throw 0;
717  }
718 
720  t->guard=false_exprt();
721  t->source_location=function.source_location();
722  t->source_location.set("user-provided", true);
723  t->source_location.set_property_class(ID_assertion);
724 
725  if(lhs.is_not_nil())
726  {
727  error().source_location=function.find_source_location();
728  error() << identifier << " expected not to have LHS" << eom;
729  throw 0;
730  }
731 
732  // __VERIFIER_error has abort() semantics, even if no assertions
733  // are being checked
735  a->guard=false_exprt();
736  a->source_location=function.source_location();
737  a->source_location.set("user-provided", true);
738  }
739  else if(identifier=="assert" &&
740  !ns.lookup(identifier).location.get_function().empty())
741  {
742  if(arguments.size()!=1)
743  {
744  error().source_location=function.find_source_location();
745  error() << "`" << identifier << "' expected to have one argument"
746  << eom;
747  throw 0;
748  }
749 
751  t->guard=arguments.front();
752  t->source_location=function.source_location();
753  t->source_location.set("user-provided", true);
754  t->source_location.set_property_class(ID_assertion);
755  t->source_location.set_comment(
756  "assertion " + id2string(from_expr(ns, identifier, t->guard)));
757 
758  // let's double-check the type of the argument
759  if(t->guard.type().id()!=ID_bool)
760  t->guard.make_typecast(bool_typet());
761 
762  if(lhs.is_not_nil())
763  {
764  error().source_location=function.find_source_location();
765  error() << identifier << " expected not to have LHS" << eom;
766  throw 0;
767  }
768  }
769  else if(identifier==CPROVER_PREFIX "assert" ||
770  identifier==CPROVER_PREFIX "precondition")
771  {
772  if(arguments.size()!=2)
773  {
774  error().source_location=function.find_source_location();
775  error() << "`" << identifier << "' expected to have two arguments"
776  << eom;
777  throw 0;
778  }
779 
780  bool is_precondition=
781  identifier==CPROVER_PREFIX "precondition";
782 
783  const irep_idt description=
784  get_string_constant(arguments[1]);
785 
787  t->guard=arguments[0];
788  t->source_location=function.source_location();
789 
790  if(is_precondition)
791  {
792  t->source_location.set_property_class(ID_precondition);
793  }
794  else
795  {
796  t->source_location.set(
797  "user-provided",
798  !function.source_location().is_built_in());
799  t->source_location.set_property_class(ID_assertion);
800  }
801 
802  t->source_location.set_comment(description);
803 
804  // let's double-check the type of the argument
805  if(t->guard.type().id()!=ID_bool)
806  t->guard.make_typecast(bool_typet());
807 
808  if(lhs.is_not_nil())
809  {
810  error().source_location=function.find_source_location();
811  error() << identifier << " expected not to have LHS" << eom;
812  throw 0;
813  }
814  }
815  else if(identifier==CPROVER_PREFIX "havoc_object")
816  {
817  if(arguments.size()!=1)
818  {
819  error().source_location=function.find_source_location();
820  error() << "`" << identifier << "' expected to have one argument"
821  << eom;
822  throw 0;
823  }
824 
825  if(lhs.is_not_nil())
826  {
827  error().source_location=function.find_source_location();
828  error() << identifier << " expected not to have LHS" << eom;
829  throw 0;
830  }
831 
833  t->source_location=function.source_location();
834  t->code=codet(ID_havoc_object);
835  t->code.add_source_location()=function.source_location();
836  t->code.copy_to_operands(arguments[0]);
837  }
838  else if(identifier==CPROVER_PREFIX "printf")
839  {
840  do_printf(lhs, function, arguments, dest);
841  }
842  else if(identifier==CPROVER_PREFIX "scanf")
843  {
844  do_scanf(lhs, function, arguments, dest);
845  }
846  else if(identifier==CPROVER_PREFIX "input" ||
847  identifier=="__CPROVER::input")
848  {
849  do_input(lhs, function, arguments, dest);
850  }
851  else if(identifier==CPROVER_PREFIX "output" ||
852  identifier=="__CPROVER::output")
853  {
854  do_output(lhs, function, arguments, dest);
855  }
856  else if(identifier==CPROVER_PREFIX "atomic_begin" ||
857  identifier=="__CPROVER::atomic_begin" ||
858  identifier=="__VERIFIER_atomic_begin")
859  {
860  do_atomic_begin(lhs, function, arguments, dest);
861  }
862  else if(identifier==CPROVER_PREFIX "atomic_end" ||
863  identifier=="__CPROVER::atomic_end" ||
864  identifier=="__VERIFIER_atomic_end")
865  {
866  do_atomic_end(lhs, function, arguments, dest);
867  }
868  else if(identifier==CPROVER_PREFIX "prob_biased_coin")
869  {
870  do_prob_coin(lhs, function, arguments, dest);
871  }
872  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_"))
873  {
874  do_prob_uniform(lhs, function, arguments, dest);
875  }
876  else if(has_prefix(id2string(identifier), "nondet_") ||
877  has_prefix(id2string(identifier), "__VERIFIER_nondet_"))
878  {
879  // make it a side effect if there is an LHS
880  if(lhs.is_nil())
881  return;
882 
883  exprt rhs;
884 
885  // We need to special-case for _Bool, which
886  // can only be 0 or 1.
887  if(lhs.type().id()==ID_c_bool)
888  {
890  rhs.add_source_location()=function.source_location();
891  rhs.set(ID_C_identifier, identifier);
892  rhs=typecast_exprt(rhs, lhs.type());
893  }
894  else
895  {
896  rhs=side_effect_expr_nondett(lhs.type());
897  rhs.add_source_location()=function.source_location();
898  rhs.set(ID_C_identifier, identifier);
899  }
900 
901  code_assignt assignment(lhs, rhs);
902  assignment.add_source_location()=function.source_location();
903  copy(assignment, ASSIGN, dest);
904  }
905  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_"))
906  {
907  // make it a side effect if there is an LHS
908  if(lhs.is_nil())
909  return;
910 
912  rhs.type()=lhs.type();
913  rhs.add_source_location()=function.source_location();
914  rhs.function()=function;
915  rhs.arguments()=arguments;
916 
917  code_assignt assignment(lhs, rhs);
918  assignment.add_source_location()=function.source_location();
919  copy(assignment, ASSIGN, dest);
920  }
921  else if(identifier==CPROVER_PREFIX "array_equal")
922  {
923  do_array_op(ID_array_equal, lhs, function, arguments, dest);
924  }
925  else if(identifier==CPROVER_PREFIX "array_set")
926  {
927  do_array_op(ID_array_set, lhs, function, arguments, dest);
928  }
929  else if(identifier==CPROVER_PREFIX "array_copy")
930  {
931  do_array_op(ID_array_copy, lhs, function, arguments, dest);
932  }
933  else if(identifier==CPROVER_PREFIX "array_replace")
934  {
935  do_array_op(ID_array_replace, lhs, function, arguments, dest);
936  }
937  else if(identifier=="printf")
938  /*
939  identifier=="fprintf" ||
940  identifier=="sprintf" ||
941  identifier=="snprintf")
942  */
943  {
944  do_printf(lhs, function, arguments, dest);
945  }
946  else if(identifier=="__assert_fail" ||
947  identifier=="_assert" ||
948  identifier=="__assert_c99" ||
949  identifier=="_wassert")
950  {
951  // __assert_fail is Linux
952  // These take four arguments:
953  // "expression", "file.c", line, __func__
954  // klibc has __assert_fail with 3 arguments
955  // "expression", "file.c", line
956 
957  // MingW has
958  // void _assert (const char*, const char*, int);
959  // with three arguments:
960  // "expression", "file.c", line
961 
962  // This has been seen in Solaris 11.
963  // Signature:
964  // void __assert_c99(
965  // const char *desc, const char *file, int line, const char *func);
966 
967  // _wassert is Windows. The arguments are
968  // L"expression", L"file.c", line
969 
970  if(arguments.size()!=4 &&
971  arguments.size()!=3)
972  {
973  error().source_location=function.find_source_location();
974  error() << "`" << identifier << "' expected to have four arguments"
975  << eom;
976  throw 0;
977  }
978 
979  const irep_idt description=
980  "assertion "+id2string(get_string_constant(arguments[0]));
981 
983  t->guard=false_exprt();
984  t->source_location=function.source_location();
985  t->source_location.set("user-provided", true);
986  t->source_location.set_property_class(ID_assertion);
987  t->source_location.set_comment(description);
988  // we ignore any LHS
989  }
990  else if(identifier=="__assert_rtn" ||
991  identifier=="__assert")
992  {
993  // __assert_rtn has been seen on MacOS;
994  // __assert is FreeBSD and Solaris 11.
995  // These take four arguments:
996  // __func__, "file.c", line, "expression"
997  // On Solaris 11, it's three arguments:
998  // "expression", "file", line
999 
1000  irep_idt description;
1001 
1002  if(arguments.size()==4)
1003  {
1004  description=
1005  "assertion "+id2string(get_string_constant(arguments[3]));
1006  }
1007  else if(arguments.size()==3)
1008  {
1009  description=
1010  "assertion "+id2string(get_string_constant(arguments[1]));
1011  }
1012  else
1013  {
1014  error().source_location=function.find_source_location();
1015  error() << "`" << identifier << "' expected to have four arguments"
1016  << eom;
1017  throw 0;
1018  }
1019 
1021  t->guard=false_exprt();
1022  t->source_location=function.source_location();
1023  t->source_location.set("user-provided", true);
1024  t->source_location.set_property_class(ID_assertion);
1025  t->source_location.set_comment(description);
1026  // we ignore any LHS
1027  }
1028  else if(identifier=="__assert_func")
1029  {
1030  // __assert_func is newlib (used by, e.g., cygwin)
1031  // These take four arguments:
1032  // "file.c", line, __func__, "expression"
1033  if(arguments.size()!=4)
1034  {
1035  error().source_location=function.find_source_location();
1036  error() << "`" << identifier << "' expected to have four arguments"
1037  << eom;
1038  throw 0;
1039  }
1040 
1041  irep_idt description;
1042  try
1043  {
1044  description="assertion "+id2string(get_string_constant(arguments[3]));
1045  }
1046  catch(int)
1047  {
1048  // we might be building newlib, where __assert_func is passed
1049  // a pointer-typed symbol; the warning will still have been
1050  // printed
1051  description="assertion";
1052  }
1053 
1055  t->guard=false_exprt();
1056  t->source_location=function.source_location();
1057  t->source_location.set("user-provided", true);
1058  t->source_location.set_property_class(ID_assertion);
1059  t->source_location.set_comment(description);
1060  // we ignore any LHS
1061  }
1062  else if(identifier==CPROVER_PREFIX "fence")
1063  {
1064  if(arguments.empty())
1065  {
1066  error().source_location=function.find_source_location();
1067  error() << "`" << identifier
1068  << "' expected to have at least one argument" << eom;
1069  throw 0;
1070  }
1071 
1073  t->source_location=function.source_location();
1074  t->code.set(ID_statement, ID_fence);
1075 
1076  forall_expr(it, arguments)
1077  {
1078  const irep_idt kind=get_string_constant(*it);
1079  t->code.set(kind, true);
1080  }
1081  }
1082  else if(identifier=="__builtin_prefetch")
1083  {
1084  // does nothing
1085  }
1086  else if(identifier=="__builtin_unreachable")
1087  {
1088  // says something like UNREACHABLE;
1089  }
1090  else if(identifier==ID_gcc_builtin_va_arg)
1091  {
1092  // This does two things.
1093  // 1) Move list pointer to next argument.
1094  // Done by gcc_builtin_va_arg_next.
1095  // 2) Return value of argument.
1096  // This is just dereferencing.
1097 
1098  if(arguments.size()!=1)
1099  {
1100  error().source_location=function.find_source_location();
1101  error() << "`" << identifier << "' expected to have one argument"
1102  << eom;
1103  throw 0;
1104  }
1105 
1106  exprt list_arg=make_va_list(arguments[0]);
1107 
1108  {
1109  side_effect_exprt rhs(ID_gcc_builtin_va_arg_next, list_arg.type());
1110  rhs.copy_to_operands(list_arg);
1111  rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
1113  t1->source_location=function.source_location();
1114  t1->code=code_assignt(list_arg, rhs);
1115  }
1116 
1117  if(lhs.is_not_nil())
1118  {
1119  typet t=pointer_type(lhs.type());
1120  dereference_exprt rhs(lhs.type());
1121  rhs.op0()=typecast_exprt(list_arg, t);
1122  rhs.add_source_location()=function.source_location();
1124  t2->source_location=function.source_location();
1125  t2->code=code_assignt(lhs, rhs);
1126  }
1127  }
1128  else if(identifier=="__builtin_va_copy")
1129  {
1130  if(arguments.size()!=2)
1131  {
1132  error().source_location=function.find_source_location();
1133  error() << "`" << identifier << "' expected to have two arguments"
1134  << eom;
1135  throw 0;
1136  }
1137 
1138  exprt dest_expr=make_va_list(arguments[0]);
1139  const typecast_exprt src_expr(arguments[1], dest_expr.type());
1140 
1141  if(!is_lvalue(dest_expr))
1142  {
1144  error() << "va_copy argument expected to be lvalue" << eom;
1145  throw 0;
1146  }
1147 
1149  t->source_location=function.source_location();
1150  t->code=code_assignt(dest_expr, src_expr);
1151  }
1152  else if(identifier=="__builtin_va_start")
1153  {
1154  // Set the list argument to be the address of the
1155  // parameter argument.
1156  if(arguments.size()!=2)
1157  {
1158  error().source_location=function.find_source_location();
1159  error() << "`" << identifier << "' expected to have two arguments"
1160  << eom;
1161  throw 0;
1162  }
1163 
1164  exprt dest_expr=make_va_list(arguments[0]);
1165  const typecast_exprt src_expr(
1166  address_of_exprt(arguments[1]), dest_expr.type());
1167 
1168  if(!is_lvalue(dest_expr))
1169  {
1171  error() << "va_start argument expected to be lvalue" << eom;
1172  throw 0;
1173  }
1174 
1176  t->source_location=function.source_location();
1177  t->code=code_assignt(dest_expr, src_expr);
1178  }
1179  else if(identifier=="__builtin_va_end")
1180  {
1181  // Invalidates the argument. We do so by setting it to NULL.
1182  if(arguments.size()!=1)
1183  {
1184  error().source_location=function.find_source_location();
1185  error() << "`" << identifier << "' expected to have one argument"
1186  << eom;
1187  throw 0;
1188  }
1189 
1190  exprt dest_expr=make_va_list(arguments[0]);
1191 
1192  if(!is_lvalue(dest_expr))
1193  {
1195  error() << "va_end argument expected to be lvalue" << eom;
1196  throw 0;
1197  }
1198 
1199  // our __builtin_va_list is a pointer
1200  if(ns.follow(dest_expr.type()).id()==ID_pointer)
1201  {
1203  t->source_location=function.source_location();
1204  exprt zero=
1206  dest_expr.type(),
1207  function.source_location(),
1208  ns,
1210  t->code=code_assignt(dest_expr, zero);
1211  }
1212  }
1213  else if(identifier=="__sync_fetch_and_add" ||
1214  identifier=="__sync_fetch_and_sub" ||
1215  identifier=="__sync_fetch_and_or" ||
1216  identifier=="__sync_fetch_and_and" ||
1217  identifier=="__sync_fetch_and_xor" ||
1218  identifier=="__sync_fetch_and_nand")
1219  {
1220  // type __sync_fetch_and_OP(type *ptr, type value, ...)
1221  // { tmp = *ptr; *ptr OP= value; return tmp; }
1222 
1223  if(arguments.size()<2)
1224  {
1225  error().source_location=function.find_source_location();
1226  error() << "`" << identifier
1227  << "' expected to have at least two arguments" << eom;
1228  throw 0;
1229  }
1230 
1231  if(arguments[0].type().id()!=ID_pointer)
1232  {
1233  error().source_location=function.find_source_location();
1234  error() << "`" << identifier << "' expected to have pointer argument"
1235  << eom;
1236  throw 0;
1237  }
1238 
1239  // build *ptr
1240  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1241 
1243  t1->source_location=function.source_location();
1244 
1245  if(lhs.is_not_nil())
1246  {
1247  // return *ptr
1249  t2->source_location=function.source_location();
1250  t2->code=code_assignt(lhs, deref_ptr);
1251  if(t2->code.op0().type()!=t2->code.op1().type())
1252  t2->code.op1().make_typecast(t2->code.op0().type());
1253  }
1254 
1255  irep_idt op_id=
1256  identifier=="__sync_fetch_and_add"?ID_plus:
1257  identifier=="__sync_fetch_and_sub"?ID_minus:
1258  identifier=="__sync_fetch_and_or"?ID_bitor:
1259  identifier=="__sync_fetch_and_and"?ID_bitand:
1260  identifier=="__sync_fetch_and_xor"?ID_bitxor:
1261  identifier=="__sync_fetch_and_nand"?ID_bitnand:
1262  ID_nil;
1263 
1264  // build *ptr=*ptr OP arguments[1];
1265  binary_exprt op_expr(deref_ptr, op_id, arguments[1], deref_ptr.type());
1266  if(op_expr.op1().type()!=op_expr.type())
1267  op_expr.op1().make_typecast(op_expr.type());
1268 
1270  t3->source_location=function.source_location();
1271  t3->code=code_assignt(deref_ptr, op_expr);
1272 
1273  // this instruction implies an mfence, i.e., WRfence
1275  t4->source_location=function.source_location();
1276  t4->code=codet(ID_fence);
1277  t4->code.set(ID_WRfence, true);
1278 
1280  t5->source_location=function.source_location();
1281  }
1282  else if(identifier=="__sync_add_and_fetch" ||
1283  identifier=="__sync_sub_and_fetch" ||
1284  identifier=="__sync_or_and_fetch" ||
1285  identifier=="__sync_and_and_fetch" ||
1286  identifier=="__sync_xor_and_fetch" ||
1287  identifier=="__sync_nand_and_fetch")
1288  {
1289  // type __sync_OP_and_fetch (type *ptr, type value, ...)
1290  // { *ptr OP= value; return *ptr; }
1291 
1292  if(arguments.size()<2)
1293  {
1294  error().source_location=function.find_source_location();
1295  error() << "`" << identifier
1296  << "' expected to have at least two arguments" << eom;
1297  throw 0;
1298  }
1299 
1300  if(arguments[0].type().id()!=ID_pointer)
1301  {
1302  error().source_location=function.find_source_location();
1303  error() << "`" << identifier
1304  << "' expected to have pointer argument" << eom;
1305  throw 0;
1306  }
1307 
1308  // build *ptr
1309  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1310 
1312  t1->source_location=function.source_location();
1313 
1314  irep_idt op_id=
1315  identifier=="__sync_add_and_fetch"?ID_plus:
1316  identifier=="__sync_sub_and_fetch"?ID_minus:
1317  identifier=="__sync_or_and_fetch"?ID_bitor:
1318  identifier=="__sync_and_and_fetch"?ID_bitand:
1319  identifier=="__sync_xor_and_fetch"?ID_bitxor:
1320  identifier=="__sync_nand_and_fetch"?ID_bitnand:
1321  ID_nil;
1322 
1323  // build *ptr=*ptr OP arguments[1];
1324  binary_exprt op_expr(deref_ptr, op_id, arguments[1], deref_ptr.type());
1325  if(op_expr.op1().type()!=op_expr.type())
1326  op_expr.op1().make_typecast(op_expr.type());
1327 
1329  t3->source_location=function.source_location();
1330  t3->code=code_assignt(deref_ptr, op_expr);
1331 
1332  if(lhs.is_not_nil())
1333  {
1334  // return *ptr
1336  t2->source_location=function.source_location();
1337  t2->code=code_assignt(lhs, deref_ptr);
1338  if(t2->code.op0().type()!=t2->code.op1().type())
1339  t2->code.op1().make_typecast(t2->code.op0().type());
1340  }
1341 
1342  // this instruction implies an mfence, i.e., WRfence
1344  t4->source_location=function.source_location();
1345  t4->code=codet(ID_fence);
1346  t4->code.set(ID_WRfence, true);
1347 
1349  t5->source_location=function.source_location();
1350  }
1351  else if(identifier=="__sync_bool_compare_and_swap")
1352  {
1353  // These builtins perform an atomic compare and swap. That is, if the
1354  // current value of *ptr is oldval, then write newval into *ptr. The
1355  // "bool" version returns true if the comparison is successful and
1356  // newval was written. The "val" version returns the contents of *ptr
1357  // before the operation.
1358 
1359  // These are type-polymorphic, which makes it hard to put
1360  // them into ansi-c/library.
1361 
1362  // bool __sync_bool_compare_and_swap(
1363  // type *ptr, type oldval, type newval, ...)
1364 
1365  if(arguments.size()<3)
1366  {
1367  error().source_location=function.find_source_location();
1368  error() << "`" << identifier
1369  << "' expected to have at least three arguments" << eom;
1370  throw 0;
1371  }
1372 
1373  if(arguments[0].type().id()!=ID_pointer)
1374  {
1375  error().source_location=function.find_source_location();
1376  error() << "`" << identifier
1377  << "' expected to have pointer argument" << eom;
1378  throw 0;
1379  }
1380 
1381  // build *ptr
1382  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1383 
1385  t1->source_location=function.source_location();
1386 
1387  // build *ptr==oldval
1388  equal_exprt equal(deref_ptr, arguments[1]);
1389  if(equal.op1().type()!=equal.op0().type())
1390  equal.op1().make_typecast(equal.op0().type());
1391 
1392  if(lhs.is_not_nil())
1393  {
1394  // return *ptr==oldval
1396  t2->source_location=function.source_location();
1397  t2->code=code_assignt(lhs, equal);
1398  if(t2->code.op0().type()!=t2->code.op1().type())
1399  t2->code.op1().make_typecast(t2->code.op0().type());
1400  }
1401 
1402  // build (*ptr==oldval)?newval:*ptr
1403  if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type());
1404  if(if_expr.op1().type()!=if_expr.type())
1405  if_expr.op1().make_typecast(if_expr.type());
1406 
1408  t3->source_location=function.source_location();
1409  t3->code=code_assignt(deref_ptr, if_expr);
1410 
1411  // this instruction implies an mfence, i.e., WRfence
1413  t4->source_location=function.source_location();
1414  t4->code=codet(ID_fence);
1415  t4->code.set(ID_WRfence, true);
1416 
1418  t5->source_location=function.source_location();
1419  }
1420  else if(identifier=="__sync_val_compare_and_swap")
1421  {
1422  // type __sync_val_compare_and_swap(
1423  // type *ptr, type oldval, type newval, ...)
1424  if(arguments.size()<3)
1425  {
1426  error().source_location=function.find_source_location();
1427  error() << "`" << identifier
1428  << "' expected to have at least three arguments" << eom;
1429  throw 0;
1430  }
1431 
1432  if(arguments[0].type().id()!=ID_pointer)
1433  {
1434  error().source_location=function.find_source_location();
1435  error() << "`" << identifier
1436  << "' expected to have pointer argument" << eom;
1437  throw 0;
1438  }
1439 
1440  // build *ptr
1441  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1442 
1444  t1->source_location=function.source_location();
1445 
1446  if(lhs.is_not_nil())
1447  {
1448  // return *ptr
1450  t2->source_location=function.source_location();
1451  t2->code=code_assignt(lhs, deref_ptr);
1452  if(t2->code.op0().type()!=t2->code.op1().type())
1453  t2->code.op1().make_typecast(t2->code.op0().type());
1454  }
1455 
1456  // build *ptr==oldval
1457  equal_exprt equal(deref_ptr, arguments[1]);
1458  if(equal.op1().type()!=equal.op0().type())
1459  equal.op1().make_typecast(equal.op0().type());
1460 
1461  // build (*ptr==oldval)?newval:*ptr
1462  if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type());
1463  if(if_expr.op1().type()!=if_expr.type())
1464  if_expr.op1().make_typecast(if_expr.type());
1465 
1467  t3->source_location=function.source_location();
1468  t3->code=code_assignt(deref_ptr, if_expr);
1469 
1470  // this instruction implies an mfence, i.e., WRfence
1472  t4->source_location=function.source_location();
1473  t4->code=codet(ID_fence);
1474  t4->code.set(ID_WRfence, true);
1475 
1477  t5->source_location=function.source_location();
1478  }
1479  else if(identifier=="__sync_lock_test_and_set")
1480  {
1481  // type __sync_lock_test_and_set (type *ptr, type value, ...)
1482 
1483  // This builtin, as described by Intel, is not a traditional
1484  // test-and-set operation, but rather an atomic exchange operation.
1485  // It writes value into *ptr, and returns the previous contents of
1486  // *ptr. Many targets have only minimal support for such locks, and
1487  // do not support a full exchange operation. In this case, a target
1488  // may support reduced functionality here by which the only valid
1489  // value to store is the immediate constant 1. The exact value
1490  // actually stored in *ptr is implementation defined.
1491  }
1492  else if(identifier=="__sync_lock_release")
1493  {
1494  // This builtin is not a full barrier, but rather an acquire barrier.
1495  // This means that references after the builtin cannot move to (or be
1496  // speculated to) before the builtin, but previous memory stores may
1497  // not be globally visible yet, and previous memory loads may not yet
1498  // be satisfied.
1499 
1500  // void __sync_lock_release (type *ptr, ...)
1501  }
1502  else if(identifier=="__builtin_isgreater" ||
1503  identifier=="__builtin_isgreater" ||
1504  identifier=="__builtin_isgreaterequal" ||
1505  identifier=="__builtin_isless" ||
1506  identifier=="__builtin_islessequal" ||
1507  identifier=="__builtin_islessgreater" ||
1508  identifier=="__builtin_isunordered")
1509  {
1510  // these support two double or two float arguments; we call the
1511  // appropriate internal version
1512  if(arguments.size()!=2 ||
1513  (arguments[0].type()!=double_type() &&
1514  arguments[0].type()!=float_type()) ||
1515  (arguments[1].type()!=double_type() &&
1516  arguments[1].type()!=float_type()))
1517  {
1518  error().source_location=function.find_source_location();
1519  error() << "`" << identifier
1520  << "' expected to have two float/double arguments"
1521  << eom;
1522  throw 0;
1523  }
1524 
1525  exprt::operandst new_arguments=arguments;
1526 
1527  bool use_double=arguments[0].type()==double_type();
1528  if(arguments[0].type()!=arguments[1].type())
1529  {
1530  if(use_double)
1531  new_arguments[1].make_typecast(arguments[0].type());
1532  else
1533  {
1534  new_arguments[0].make_typecast(arguments[1].type());
1535  use_double=true;
1536  }
1537  }
1538 
1539  code_typet f_type=to_code_type(function.type());
1540  f_type.remove_ellipsis();
1541  const typet &a_t=new_arguments[0].type();
1542  f_type.parameters()=
1544 
1545  // replace __builtin_ by CPROVER_PREFIX
1546  std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1547  // append d or f for double/float
1548  name+=use_double?'d':'f';
1549 
1550  symbol_exprt new_function=function;
1551  new_function.set_identifier(name);
1552  new_function.type()=f_type;
1553 
1554  code_function_callt function_call;
1555  function_call.lhs()=lhs;
1556  function_call.function()=new_function;
1557  function_call.arguments()=new_arguments;
1558  function_call.add_source_location()=function.source_location();
1559 
1560  if(!symbol_table.has_symbol(name))
1561  {
1562  symbolt new_symbol;
1563  new_symbol.base_name=name;
1564  new_symbol.name=name;
1565  new_symbol.type=f_type;
1566  new_symbol.location=function.source_location();
1567  symbol_table.add(new_symbol);
1568  }
1569 
1570  copy(function_call, FUNCTION_CALL, dest);
1571  }
1572  else
1573  {
1574  do_function_call_symbol(*symbol);
1575 
1576  // insert function call
1577  code_function_callt function_call;
1578  function_call.lhs()=lhs;
1579  function_call.function()=function;
1580  function_call.arguments()=arguments;
1581  function_call.add_source_location()=function.source_location();
1582 
1583  copy(function_call, FUNCTION_CALL, dest);
1584  }
1585 }
The type of an expression.
Definition: type.h:22
irep_idt get_string_constant(const exprt &expr)
irep_idt name
The unique identifier.
Definition: symbol.h:43
semantic type conversion
Definition: std_expr.h:2111
constant_exprt from_rational(const rationalt &a)
BigInt mp_integer
Definition: mp_arith.h:22
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
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
application of (mathematical) function
Definition: std_expr.h:4531
format_token_listt parse_format_string(const std::string &arg_string)
exprt & op0()
Definition: expr.h:72
#define CPROVER_PREFIX
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
const exprt & op() const
Definition: std_expr.h:340
void do_input(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
bool is_lvalue(const exprt &expr)
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
#define forall_expr(it, expr)
Definition: expr.h:28
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
Definition: std_types.h:767
argumentst & arguments()
Definition: std_expr.h:4564
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
Format String Parser.
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
Definition: goto_program.h:486
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
add function calls to function queue for later processing
The trinary if-then-else operator.
Definition: std_expr.h:3361
bitvector_typet double_type()
Definition: c_types.cpp:193
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
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
typet get_type(const format_tokent &token)
equality
Definition: std_expr.h:1354
Expression Initialization.
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt make_va_list(const exprt &expr)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:189
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
argumentst & arguments()
Definition: std_code.h:860
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void remove_ellipsis()
Definition: std_types.h:890
A generic base class for binary expressions.
Definition: std_expr.h:649
bitvector_typet float_type()
Definition: c_types.cpp:185
instructionst::iterator targett
Definition: goto_program.h:397
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
Operator to dereference a pointer.
Definition: std_expr.h:3284
Program Transformation.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3955
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const exprt & size() const
Definition: std_types.h:1014
A function call.
Definition: std_code.h:828
const typet & follow(const typet &) const
Definition: namespace.cpp:55
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: std_expr.h:3170
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
exprt get_array_argument(const exprt &src)
The boolean constant false.
Definition: std_expr.h:4499
symbol_exprt & function()
Definition: std_expr.h:4552
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
Definition: expr.h:45
Pointer Logic.
const source_locationt & source_location() const
Definition: type.h:97
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
message_handlert & get_message_handler()
Definition: message.h:153
void do_output(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
exprt & function()
Definition: std_code.h:848
void set_statement(const irep_idt &statement)
Definition: std_code.h:34
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
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
const parameterst & parameters() const
Definition: std_types.h:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
symbol_table_baset & symbol_table
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
std::list< format_tokent > format_token_listt
source_locationt & add_source_location()
Definition: expr.h:130
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
Extract class identifier.
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A statement in a programming language.
Definition: std_code.h:21
const typet & subtype() const
Definition: type.h:33
An expression containing a side effect.
Definition: std_code.h:1238
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_typecast(const typet &_type)
Definition: expr.cpp:84
static void replace_new_object(const exprt &object, exprt &dest)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const irep_idt & get_statement() const
Definition: std_code.h:1253
array index operator
Definition: std_expr.h:1462