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