CBMC
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 <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/expr_initializer.h>
18 #include <util/expr_util.h>
19 #include <util/fresh_symbol.h>
20 #include <util/mathematical_expr.h>
22 #include <util/pointer_expr.h>
23 #include <util/rational.h>
24 #include <util/rational_tools.h>
25 #include <util/simplify_expr.h>
26 #include <util/symbol.h>
27 
28 #include <langapi/language_util.h>
29 
30 #include "format_strings.h"
31 
33  const exprt &lhs,
34  const symbol_exprt &function,
35  const exprt::operandst &arguments,
36  goto_programt &dest)
37 {
38  const irep_idt &identifier = function.get_identifier();
39 
40  // make it a side effect if there is an LHS
41  if(arguments.size()!=2)
42  {
43  error().source_location=function.find_source_location();
44  error() << "'" << identifier << "' expected to have two arguments" << eom;
45  throw 0;
46  }
47 
48  if(lhs.is_nil())
49  {
50  error().source_location=function.find_source_location();
51  error() << "'" << identifier << "' expected to have LHS" << eom;
52  throw 0;
53  }
54 
55  auto rhs =
56  side_effect_exprt("prob_uniform", lhs.type(), function.source_location());
57 
58  if(lhs.type().id()!=ID_unsignedbv &&
59  lhs.type().id()!=ID_signedbv)
60  {
61  error().source_location=function.find_source_location();
62  error() << "'" << identifier << "' expected other type" << eom;
63  throw 0;
64  }
65 
66  if(arguments[0].type().id()!=lhs.type().id() ||
67  arguments[1].type().id()!=lhs.type().id())
68  {
69  error().source_location=function.find_source_location();
70  error() << "'" << identifier
71  << "' expected operands to be of same type as LHS" << eom;
72  throw 0;
73  }
74 
75  if(!arguments[0].is_constant() ||
76  !arguments[1].is_constant())
77  {
78  error().source_location=function.find_source_location();
79  error() << "'" << identifier
80  << "' expected operands to be constant literals" << eom;
81  throw 0;
82  }
83 
84  mp_integer lb, ub;
85 
86  if(
87  to_integer(to_constant_expr(arguments[0]), lb) ||
88  to_integer(to_constant_expr(arguments[1]), ub))
89  {
90  error().source_location=function.find_source_location();
91  error() << "error converting operands" << eom;
92  throw 0;
93  }
94 
95  if(lb > ub)
96  {
97  error().source_location=function.find_source_location();
98  error() << "expected lower bound to be smaller or equal to the "
99  << "upper bound" << eom;
100  throw 0;
101  }
102 
103  rhs.add_to_operands(exprt{arguments[0]}, exprt{arguments[1]});
104 
105  code_assignt assignment(lhs, rhs);
106  assignment.add_source_location()=function.source_location();
107  copy(assignment, ASSIGN, dest);
108 }
109 
111  const exprt &lhs,
112  const symbol_exprt &function,
113  const exprt::operandst &arguments,
114  goto_programt &dest)
115 {
116  const irep_idt &identifier = function.get_identifier();
117 
118  // make it a side effect if there is an LHS
119  if(arguments.size()!=2)
120  {
121  error().source_location=function.find_source_location();
122  error() << "'" << identifier << "' expected to have two arguments" << eom;
123  throw 0;
124  }
125 
126  if(lhs.is_nil())
127  {
128  error().source_location=function.find_source_location();
129  error() << "'" << identifier << "' expected to have LHS" << eom;
130  throw 0;
131  }
132 
133  side_effect_exprt rhs("prob_coin", lhs.type(), function.source_location());
134 
135  if(lhs.type()!=bool_typet())
136  {
137  error().source_location=function.find_source_location();
138  error() << "'" << identifier << "' expected bool" << eom;
139  throw 0;
140  }
141 
142  if(arguments[0].type().id() != ID_unsignedbv || !arguments[0].is_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  if(arguments[1].type().id() != ID_unsignedbv || !arguments[1].is_constant())
151  {
152  error().source_location = function.find_source_location();
153  error() << "'" << identifier << "' expected second operand to be "
154  << "a constant literal of type unsigned long" << eom;
155  throw 0;
156  }
157 
158  mp_integer num, den;
159 
160  if(
161  to_integer(to_constant_expr(arguments[0]), num) ||
162  to_integer(to_constant_expr(arguments[1]), den))
163  {
164  error().source_location=function.find_source_location();
165  error() << "error converting operands" << eom;
166  throw 0;
167  }
168 
169  if(num-den > mp_integer(0))
170  {
171  error().source_location=function.find_source_location();
172  error() << "probability has to be smaller than 1" << eom;
173  throw 0;
174  }
175 
176  if(den == mp_integer(0))
177  {
178  error().source_location=function.find_source_location();
179  error() << "denominator may not be zero" << eom;
180  throw 0;
181  }
182 
183  rationalt numerator(num), denominator(den);
184  rationalt prob = numerator / denominator;
185 
186  rhs.copy_to_operands(from_rational(prob));
187 
188  code_assignt assignment(lhs, rhs);
189  assignment.add_source_location()=function.source_location();
190  copy(assignment, ASSIGN, dest);
191 }
192 
194  const exprt &lhs,
195  const symbol_exprt &function,
196  const exprt::operandst &arguments,
197  goto_programt &dest)
198 {
199  const irep_idt &f_id = function.get_identifier();
200 
201  PRECONDITION(f_id == CPROVER_PREFIX "printf");
202 
203  codet printf_code(ID_printf, arguments, function.source_location());
204  copy(printf_code, OTHER, dest);
205 }
206 
208  const exprt &lhs,
209  const symbol_exprt &function,
210  const exprt::operandst &arguments,
211  goto_programt &dest)
212 {
213  const irep_idt &f_id = function.get_identifier();
214 
215  if(f_id==CPROVER_PREFIX "scanf")
216  {
217  if(arguments.empty())
218  {
219  error().source_location=function.find_source_location();
220  error() << "scanf takes at least one argument" << eom;
221  throw 0;
222  }
223 
224  irep_idt format_string;
225 
226  if(!get_string_constant(arguments[0], format_string))
227  {
228  // use our model
229  format_token_listt token_list=
230  parse_format_string(id2string(format_string));
231 
232  std::size_t argument_number=1;
233 
234  for(const auto &t : token_list)
235  {
236  const auto type = get_type(t);
237 
238  if(type.has_value())
239  {
240  if(argument_number<arguments.size())
241  {
242  const typecast_exprt ptr(
243  arguments[argument_number], pointer_type(*type));
244  argument_number++;
245 
246  if(type->id() == ID_array)
247  {
248  #if 0
249  // A string. We first need a nondeterministic size.
251  to_array_type(*type).size()=size;
252 
253  const symbolt &tmp_symbol=
255  *type, "scanf_string", dest, function.source_location());
256 
257  const address_of_exprt rhs(
258  index_exprt(
259  tmp_symbol.symbol_expr(),
260  from_integer(0, c_index_type())));
261 
262  // now use array copy
263  codet array_copy_statement;
264  array_copy_statement.set_statement(ID_array_copy);
265  array_copy_statement.operands().resize(2);
266  array_copy_statement.op0()=ptr;
267 \ array_copy_statement.op1()=rhs;
268  array_copy_statement.add_source_location()=
269  function.source_location();
270 
271  copy(array_copy_statement, OTHER, dest);
272  #else
273  const index_exprt new_lhs(
275  const side_effect_expr_nondett rhs(
276  to_array_type(*type).element_type(),
277  function.source_location());
278  code_assignt assign(new_lhs, rhs);
279  assign.add_source_location()=function.source_location();
280  copy(assign, ASSIGN, dest);
281  #endif
282  }
283  else
284  {
285  // make it nondet for now
286  const dereference_exprt new_lhs{ptr};
287  const side_effect_expr_nondett rhs(
288  *type, function.source_location());
289  code_assignt assign(new_lhs, rhs);
290  assign.add_source_location()=function.source_location();
291  copy(assign, ASSIGN, dest);
292  }
293  }
294  }
295  }
296  }
297  else
298  {
299  // we'll just do nothing
300  code_function_callt function_call(lhs, function, arguments);
301  function_call.add_source_location()=function.source_location();
302 
303  copy(function_call, FUNCTION_CALL, dest);
304  }
305  }
306  else
307  UNREACHABLE;
308 }
309 
311  const exprt &function,
312  const exprt::operandst &arguments,
313  goto_programt &dest)
314 {
315  if(arguments.size()<2)
316  {
317  error().source_location=function.find_source_location();
318  error() << "input takes at least two arguments" << eom;
319  throw 0;
320  }
321 
322  copy(code_inputt{arguments, function.source_location()}, OTHER, dest);
323 }
324 
326  const exprt &function,
327  const exprt::operandst &arguments,
328  goto_programt &dest)
329 {
330  if(arguments.size()<2)
331  {
332  error().source_location=function.find_source_location();
333  error() << "output takes at least two arguments" << eom;
334  throw 0;
335  }
336 
337  copy(code_outputt{arguments, function.source_location()}, OTHER, dest);
338 }
339 
341  const exprt &lhs,
342  const symbol_exprt &function,
343  const exprt::operandst &arguments,
344  goto_programt &dest)
345 {
346  if(lhs.is_not_nil())
347  {
349  error() << "atomic_begin does not expect an LHS" << eom;
350  throw 0;
351  }
352 
353  if(!arguments.empty())
354  {
355  error().source_location=function.find_source_location();
356  error() << "atomic_begin takes no arguments" << eom;
357  throw 0;
358  }
359 
360  dest.add(goto_programt::make_atomic_begin(function.source_location()));
361 }
362 
364  const exprt &lhs,
365  const symbol_exprt &function,
366  const exprt::operandst &arguments,
367  goto_programt &dest)
368 {
369  if(lhs.is_not_nil())
370  {
372  error() << "atomic_end does not expect an LHS" << eom;
373  throw 0;
374  }
375 
376  if(!arguments.empty())
377  {
378  error().source_location=function.find_source_location();
379  error() << "atomic_end takes no arguments" << eom;
380  throw 0;
381  }
382 
383  dest.add(goto_programt::make_atomic_end(function.source_location()));
384 }
385 
387  const exprt &lhs,
388  const side_effect_exprt &rhs,
389  goto_programt &dest)
390 {
391  if(lhs.is_nil())
392  {
394  error() << "do_cpp_new without lhs is yet to be implemented" << eom;
395  throw 0;
396  }
397 
398  // build size expression
400  static_cast<const exprt &>(rhs.find(ID_sizeof));
401 
402  bool new_array=rhs.get(ID_statement)==ID_cpp_new_array;
403 
404  exprt count;
405 
406  if(new_array)
407  {
409  static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
410 
411  // might have side-effect
412  clean_expr(count, dest, ID_cpp);
413  }
414 
415  exprt tmp_symbol_expr;
416 
417  // is this a placement new?
418  if(rhs.operands().empty()) // no, "regular" one
419  {
420  // call __new or __new_array
421  exprt new_symbol=
422  ns.lookup(new_array?"__new_array":"__new").symbol_expr();
423 
424  const code_typet &code_type=
425  to_code_type(new_symbol.type());
426 
427  const typet &return_type=
428  code_type.return_type();
429 
431  code_type.parameters().size() == 1 || code_type.parameters().size() == 2,
432  "new has one or two parameters");
433 
434  const symbolt &tmp_symbol =
435  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
436 
437  tmp_symbol_expr=tmp_symbol.symbol_expr();
438 
439  code_function_callt new_call(new_symbol);
440  if(new_array)
441  new_call.arguments().push_back(count);
442  new_call.arguments().push_back(object_size);
443  new_call.set(
444  ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
445  new_call.lhs()=tmp_symbol_expr;
446  new_call.add_source_location()=rhs.source_location();
447 
448  convert(new_call, dest, ID_cpp);
449  }
450  else if(rhs.operands().size()==1)
451  {
452  // call __placement_new
453  exprt new_symbol=
454  ns.lookup(
455  new_array?"__placement_new_array":"__placement_new").symbol_expr();
456 
457  const code_typet &code_type=
458  to_code_type(new_symbol.type());
459 
460  const typet &return_type=code_type.return_type();
461 
463  code_type.parameters().size() == 2 || code_type.parameters().size() == 3,
464  "placement new has two or three parameters");
465 
466  const symbolt &tmp_symbol =
467  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
468 
469  tmp_symbol_expr=tmp_symbol.symbol_expr();
470 
471  code_function_callt new_call(new_symbol);
472  if(new_array)
473  new_call.arguments().push_back(count);
474  new_call.arguments().push_back(object_size);
475  new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location
476  new_call.set(
477  ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
478  new_call.lhs()=tmp_symbol_expr;
479  new_call.add_source_location()=rhs.source_location();
480 
481  for(std::size_t i=0; i<code_type.parameters().size(); i++)
482  {
484  new_call.arguments()[i], code_type.parameters()[i].type());
485  }
486 
487  convert(new_call, dest, ID_cpp);
488  }
489  else
490  {
492  error() << "cpp_new expected to have 0 or 1 operands" << eom;
493  throw 0;
494  }
495 
497  lhs,
498  typecast_exprt(tmp_symbol_expr, lhs.type()),
499  rhs.find_source_location()));
500 
501  // grab initializer
502  goto_programt tmp_initializer;
503  cpp_new_initializer(lhs, rhs, tmp_initializer);
504 
505  dest.destructive_append(tmp_initializer);
506 }
507 
510  const exprt &lhs,
511  const side_effect_exprt &rhs,
512  goto_programt &dest)
513 {
514  exprt initializer=
515  static_cast<const exprt &>(rhs.find(ID_initializer));
516 
517  if(initializer.is_not_nil())
518  {
519  if(rhs.get_statement()=="cpp_new[]")
520  {
521  // build loop
522  }
523  else if(rhs.get_statement()==ID_cpp_new)
524  {
525  // just one object
526  const dereference_exprt deref_lhs(
527  lhs, to_pointer_type(rhs.type()).base_type());
528 
529  replace_new_object(deref_lhs, initializer);
530  convert(to_code(initializer), dest, ID_cpp);
531  }
532  else
533  UNREACHABLE;
534  }
535 }
536 
538 {
539  if(src.id()==ID_typecast)
540  return get_array_argument(to_typecast_expr(src).op());
541 
542  if(src.id()!=ID_address_of)
543  {
545  error() << "expected array-pointer as argument" << eom;
546  throw 0;
547  }
548 
549  const auto &address_of_expr = to_address_of_expr(src);
550 
551  if(address_of_expr.object().id() != ID_index)
552  {
554  error() << "expected array-element as argument" << eom;
555  throw 0;
556  }
557 
558  const auto &index_expr = to_index_expr(address_of_expr.object());
559 
560  if(index_expr.array().type().id() != ID_array)
561  {
563  error() << "expected array as argument" << eom;
564  throw 0;
565  }
566 
567  return index_expr.array();
568 }
569 
571  const irep_idt &id,
572  const exprt &lhs,
573  const symbol_exprt &function,
574  const exprt::operandst &arguments,
575  goto_programt &dest)
576 {
577  if(arguments.size()!=2)
578  {
579  error().source_location=function.find_source_location();
580  error() << id << " expects two arguments" << eom;
581  throw 0;
582  }
583 
584  codet array_op_statement(id);
585  array_op_statement.operands()=arguments;
586  array_op_statement.add_source_location()=function.source_location();
587 
588  // lhs is only used with array_equal, in all other cases it should be nil (as
589  // they are of type void)
590  if(id == ID_array_equal)
591  array_op_statement.copy_to_operands(lhs);
592 
593  copy(array_op_statement, OTHER, dest);
594 }
595 
597 {
598  exprt result = skip_typecast(expr);
599 
600  // if it's an address of an lvalue, we take that
601  if(result.id() == ID_address_of)
602  {
603  const auto &address_of_expr = to_address_of_expr(result);
604  if(is_assignable(address_of_expr.object()))
605  result = address_of_expr.object();
606  }
607 
608  while(result.type().id() == ID_array &&
609  to_array_type(result.type()).size().is_one())
610  {
611  result = index_exprt{result, from_integer(0, c_index_type())};
612  }
613 
614  return result;
615 }
616 
618  const exprt &lhs,
619  const symbol_exprt &function,
620  const exprt::operandst &arguments,
621  goto_programt &dest,
622  const irep_idt &mode)
623 {
624  irep_idt identifier = CPROVER_PREFIX "havoc_slice";
625 
626  // We disable checks on the generated instructions
627  // because we add our own rw_ok assertion that takes size into account
628  auto source_location = function.find_source_location();
629  source_location.add_pragma("disable:pointer-check");
630  source_location.add_pragma("disable:pointer-overflow-check");
631  source_location.add_pragma("disable:pointer-primitive-check");
632 
633  // check # arguments
634  if(arguments.size() != 2)
635  {
636  error().source_location = source_location;
637  error() << "'" << identifier << "' expected to have two arguments" << eom;
638  throw 0;
639  }
640 
641  // check argument types
642  if(arguments[0].type().id() != ID_pointer)
643  {
644  error().source_location = source_location;
645  error() << "'" << identifier
646  << "' first argument expected to have `void *` type" << eom;
647  throw 0;
648  }
649 
650  if(arguments[1].type().id() != ID_unsignedbv)
651  {
652  error().source_location = source_location;
653  error() << "'" << identifier
654  << "' second argument expected to have `size_t` type" << eom;
655  throw 0;
656  }
657 
658  // check nil lhs
659  if(lhs.is_not_nil())
660  {
661  error().source_location = source_location;
662  error() << "'" << identifier << "' not expected to have a LHS" << eom;
663  throw 0;
664  }
665 
666  // insert instructions
667  // assert(rw_ok(argument[0], argument[1]));
668  // char nondet_contents[argument[1]];
669  // __CPROVER_array_replace(p, nondet_contents);
670 
671  r_or_w_ok_exprt ok_expr(ID_w_ok, arguments[0], arguments[1]);
672  ok_expr.add_source_location() = source_location;
673  source_locationt annotated_location = source_location;
674  annotated_location.set("user-provided", false);
675  annotated_location.set_property_class(ID_assertion);
676  annotated_location.set_comment(
677  "assertion havoc_slice " + from_expr(ns, identifier, ok_expr));
678  dest.add(goto_programt::make_assertion(ok_expr, annotated_location));
679 
680  const array_typet array_type(char_type(), simplify_expr(arguments[1], ns));
681 
682  const symbolt &nondet_contents =
683  new_tmp_symbol(array_type, "nondet_contents", dest, source_location, mode);
684  const exprt &nondet_contents_expr = address_of_exprt{index_exprt{
685  nondet_contents.symbol_expr(), from_integer(0, c_index_type())}};
686 
687  const exprt &arg0 =
690  nondet_contents_expr, pointer_type(empty_typet{}));
691 
692  codet array_replace(ID_array_replace, {arg0, arg1}, source_location);
693  dest.add(goto_programt::make_other(array_replace, source_location));
694 }
695 
699  const exprt &lhs,
700  const symbol_exprt &function,
701  const exprt::operandst &arguments,
702  goto_programt &dest,
703  const irep_idt &mode)
704 {
705  const source_locationt &source_location = function.source_location();
706  const auto alloca_type = to_code_type(function.type());
707 
708  if(alloca_type.return_type() != pointer_type(void_type()))
709  {
710  error().source_location = source_location;
711  error() << "'alloca' function called, but 'alloca' has not been declared "
712  << "with expected 'void *' return type." << eom;
713  throw 0;
714  }
715  if(
716  alloca_type.parameters().size() != 1 ||
717  alloca_type.parameters()[0].type() != size_type())
718  {
719  error().source_location = source_location;
720  error() << "'alloca' function called, but 'alloca' has not been declared "
721  << "with expected single 'size_t' parameter." << eom;
722  throw 0;
723  }
724 
725  exprt new_lhs = lhs;
726 
727  // make sure we have a left-hand side to track the allocation even when the
728  // original program did not
729  if(lhs.is_nil())
730  {
731  new_lhs =
733  alloca_type.return_type(), "alloca", dest, source_location, mode)
734  .symbol_expr();
735  }
736 
737  // do the actual function call
738  code_function_callt function_call(new_lhs, function, arguments);
739  function_call.add_source_location() = source_location;
740  copy(function_call, FUNCTION_CALL, dest);
741 
742  // Don't add instrumentation when we're in alloca (which might in turn call
743  // __builtin_alloca) -- the instrumentation will be done for the call of
744  // alloca. Also, we can only add instrumentation when we're in a function
745  // context.
746  if(
747  function.source_location().get_function() == "alloca" || !targets.prefix ||
748  !targets.suffix)
749  {
750  return;
751  }
752 
753  // create a symbol to eventually (and non-deterministically) mark the
754  // allocation as dead; this symbol has function scope and is initialised to
755  // NULL
756  symbol_exprt this_alloca_ptr =
758  alloca_type.return_type(),
759  id2string(function.source_location().get_function()),
760  "tmp_alloca",
761  source_location,
762  mode,
763  symbol_table)
764  .symbol_expr();
765  goto_programt decl_prg;
766  decl_prg.add(goto_programt::make_decl(this_alloca_ptr, source_location));
768  this_alloca_ptr,
769  null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())},
770  source_location));
772  targets.prefix->instructions.begin(), decl_prg);
773 
774  // non-deterministically update this_alloca_ptr
775  if_exprt rhs{
776  side_effect_expr_nondett{bool_typet(), source_location},
777  new_lhs,
778  this_alloca_ptr};
780  this_alloca_ptr, std::move(rhs), source_location));
781 
782  // mark pointer to alloca result as dead, unless the alloca result (in
783  // this_alloca_ptr) is still NULL
784  symbol_exprt dead_object_sym =
785  ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
786  exprt alloca_result =
787  typecast_exprt::conditional_cast(this_alloca_ptr, dead_object_sym.type());
788  if_exprt not_null{
789  equal_exprt{
790  this_alloca_ptr,
791  null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())}},
792  dead_object_sym,
793  std::move(alloca_result)};
794  auto assign = goto_programt::make_assignment(
795  std::move(dead_object_sym), std::move(not_null), source_location);
797  targets.suffix->instructions.begin(), assign);
799  targets.suffix->instructions.begin(),
800  goto_programt::make_dead(this_alloca_ptr, source_location));
801 }
802 
805  const exprt &lhs,
806  const symbol_exprt &function,
807  const exprt::operandst &arguments,
808  goto_programt &dest,
809  const irep_idt &mode)
810 {
811  if(function.get_bool(ID_C_invalid_object))
812  return; // ignore
813 
814  // lookup symbol
815  const irep_idt &identifier=function.get_identifier();
816 
817  const symbolt *symbol;
818  if(ns.lookup(identifier, symbol))
819  {
820  error().source_location=function.find_source_location();
821  error() << "error: function '" << identifier << "' not found" << eom;
822  throw 0;
823  }
824 
825  if(symbol->type.id()!=ID_code)
826  {
827  error().source_location=function.find_source_location();
828  error() << "error: function '" << identifier
829  << "' type mismatch: expected code" << eom;
830  throw 0;
831  }
832 
833  // User-provided function definitions always take precedence over built-ins.
834  // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
835  // whether the symbol actually has some non-nil value (which might be
836  // "compiled").
837  if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
838  {
839  do_function_call_symbol(*symbol);
840 
841  // use symbol->symbol_expr() to ensure we use the type from the symbol table
842  code_function_callt function_call(
843  lhs, symbol->symbol_expr().with_source_location(function), arguments);
844  function_call.add_source_location() = function.source_location();
845 
846  // remove void-typed assignments, which may have been created when the
847  // front-end was unable to detect them in type checking for a lack of
848  // available declarations
849  if(
850  lhs.is_not_nil() &&
851  to_code_type(symbol->type).return_type().id() == ID_empty)
852  {
853  function_call.lhs().make_nil();
854  }
855 
856  copy(function_call, FUNCTION_CALL, dest);
857 
858  return;
859  }
860 
861  if(identifier == CPROVER_PREFIX "havoc_slice")
862  {
863  do_havoc_slice(lhs, function, arguments, dest, mode);
864  }
865  else if(
866  identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume")
867  {
868  if(arguments.size()!=1)
869  {
870  error().source_location=function.find_source_location();
871  error() << "'" << identifier << "' expected to have one argument" << eom;
872  throw 0;
873  }
874 
875  // let's double-check the type of the argument
876  source_locationt annotated_location = function.source_location();
877  annotated_location.set("user-provided", true);
879  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
880  annotated_location));
881 
882  if(lhs.is_not_nil())
883  {
884  error().source_location=function.find_source_location();
885  error() << identifier << " expected not to have LHS" << eom;
886  throw 0;
887  }
888  }
889  else if(identifier=="__VERIFIER_error")
890  {
891  if(!arguments.empty())
892  {
893  error().source_location=function.find_source_location();
894  error() << "'" << identifier << "' expected to have no arguments" << eom;
895  throw 0;
896  }
897 
898  source_locationt annotated_location = function.source_location();
899  annotated_location.set("user-provided", true);
900  annotated_location.set_property_class(ID_assertion);
901  dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
902 
903  if(lhs.is_not_nil())
904  {
905  error().source_location=function.find_source_location();
906  error() << identifier << " expected not to have LHS" << eom;
907  throw 0;
908  }
909 
910  // __VERIFIER_error has abort() semantics, even if no assertions
911  // are being checked
912  annotated_location = function.source_location();
913  annotated_location.set("user-provided", true);
914  dest.add(goto_programt::make_assumption(false_exprt(), annotated_location));
915  dest.instructions.back().labels.push_back("__VERIFIER_abort");
916  }
917  else if(
918  identifier == "assert" &&
920  {
921  if(arguments.size()!=1)
922  {
923  error().source_location=function.find_source_location();
924  error() << "'" << identifier << "' expected to have one argument" << eom;
925  throw 0;
926  }
927 
928  // let's double-check the type of the argument
929  source_locationt annotated_location = function.source_location();
930  annotated_location.set("user-provided", true);
931  annotated_location.set_property_class(ID_assertion);
932  annotated_location.set_comment(
933  "assertion " + from_expr(ns, identifier, arguments.front()));
935  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
936  annotated_location));
937 
938  if(lhs.is_not_nil())
939  {
940  error().source_location=function.find_source_location();
941  error() << identifier << " expected not to have LHS" << eom;
942  throw 0;
943  }
944  }
945  else if(
946  identifier == CPROVER_PREFIX "assert" ||
947  identifier == CPROVER_PREFIX "precondition" ||
948  identifier == CPROVER_PREFIX "postcondition")
949  {
950  if(arguments.size()!=2)
951  {
952  error().source_location=function.find_source_location();
953  error() << "'" << identifier << "' expected to have two arguments" << eom;
954  throw 0;
955  }
956 
957  bool is_precondition=
958  identifier==CPROVER_PREFIX "precondition";
959  bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
960 
961  const irep_idt description=
962  get_string_constant(arguments[1]);
963 
964  // let's double-check the type of the argument
965  source_locationt annotated_location = function.source_location();
966  if(is_precondition)
967  {
968  annotated_location.set_property_class(ID_precondition);
969  }
970  else if(is_postcondition)
971  {
972  annotated_location.set_property_class(ID_postcondition);
973  }
974  else
975  {
976  annotated_location.set(
977  "user-provided", !function.source_location().is_built_in());
978  annotated_location.set_property_class(ID_assertion);
979  }
980 
981  annotated_location.set_comment(description);
982 
985  annotated_location));
986 
987  if(lhs.is_not_nil())
988  {
989  error().source_location=function.find_source_location();
990  error() << identifier << " expected not to have LHS" << eom;
991  throw 0;
992  }
993  }
994  else if(identifier==CPROVER_PREFIX "havoc_object")
995  {
996  if(arguments.size()!=1)
997  {
998  error().source_location=function.find_source_location();
999  error() << "'" << identifier << "' expected to have one argument" << eom;
1000  throw 0;
1001  }
1002 
1003  if(lhs.is_not_nil())
1004  {
1005  error().source_location=function.find_source_location();
1006  error() << identifier << " expected not to have LHS" << eom;
1007  throw 0;
1008  }
1009 
1010  codet havoc(ID_havoc_object);
1011  havoc.add_source_location() = function.source_location();
1012  havoc.copy_to_operands(arguments[0]);
1013 
1014  dest.add(goto_programt::make_other(havoc, function.source_location()));
1015  }
1016  else if(identifier==CPROVER_PREFIX "printf")
1017  {
1018  do_printf(lhs, function, arguments, dest);
1019  }
1020  else if(identifier==CPROVER_PREFIX "scanf")
1021  {
1022  do_scanf(lhs, function, arguments, dest);
1023  }
1024  else if(identifier==CPROVER_PREFIX "input" ||
1025  identifier=="__CPROVER::input")
1026  {
1027  if(lhs.is_not_nil())
1028  {
1029  error().source_location=function.find_source_location();
1030  error() << identifier << " expected not to have LHS" << eom;
1031  throw 0;
1032  }
1033 
1034  do_input(function, arguments, dest);
1035  }
1036  else if(identifier==CPROVER_PREFIX "output" ||
1037  identifier=="__CPROVER::output")
1038  {
1039  if(lhs.is_not_nil())
1040  {
1041  error().source_location=function.find_source_location();
1042  error() << identifier << " expected not to have LHS" << eom;
1043  throw 0;
1044  }
1045 
1046  do_output(function, arguments, dest);
1047  }
1048  else if(identifier==CPROVER_PREFIX "atomic_begin" ||
1049  identifier=="__CPROVER::atomic_begin" ||
1050  identifier=="java::org.cprover.CProver.atomicBegin:()V" ||
1051  identifier=="__VERIFIER_atomic_begin")
1052  {
1053  do_atomic_begin(lhs, function, arguments, dest);
1054  }
1055  else if(identifier==CPROVER_PREFIX "atomic_end" ||
1056  identifier=="__CPROVER::atomic_end" ||
1057  identifier=="java::org.cprover.CProver.atomicEnd:()V" ||
1058  identifier=="__VERIFIER_atomic_end")
1059  {
1060  do_atomic_end(lhs, function, arguments, dest);
1061  }
1062  else if(identifier==CPROVER_PREFIX "prob_biased_coin")
1063  {
1064  do_prob_coin(lhs, function, arguments, dest);
1065  }
1066  else if(identifier.starts_with(CPROVER_PREFIX "prob_uniform_"))
1067  {
1068  do_prob_uniform(lhs, function, arguments, dest);
1069  }
1070  else if(
1071  identifier.starts_with("nondet_") ||
1072  identifier.starts_with("__VERIFIER_nondet_"))
1073  {
1074  // make it a side effect if there is an LHS
1075  if(lhs.is_nil())
1076  return;
1077 
1078  exprt rhs;
1079 
1080  // We need to special-case for _Bool, which
1081  // can only be 0 or 1.
1082  if(lhs.type().id()==ID_c_bool)
1083  {
1084  rhs = side_effect_expr_nondett(bool_typet(), function.source_location());
1085  rhs.set(ID_C_identifier, identifier);
1086  rhs=typecast_exprt(rhs, lhs.type());
1087  }
1088  else
1089  {
1090  rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
1091  rhs.set(ID_C_identifier, identifier);
1092  }
1093 
1094  code_assignt assignment(lhs, rhs);
1095  assignment.add_source_location()=function.source_location();
1096  copy(assignment, ASSIGN, dest);
1097  }
1098  else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_"))
1099  {
1100  // make it a side effect if there is an LHS
1101  if(lhs.is_nil())
1102  return;
1103 
1104  if(function.type().get_bool(ID_C_incomplete))
1105  {
1106  error().source_location = function.find_source_location();
1107  error() << "'" << identifier << "' is not declared, "
1108  << "missing type information required to construct call to "
1109  << "uninterpreted function" << eom;
1110  throw 0;
1111  }
1112 
1113  const code_typet &function_call_type = to_code_type(function.type());
1115  for(const auto &parameter : function_call_type.parameters())
1116  domain.push_back(parameter.type());
1117  mathematical_function_typet function_type{domain,
1118  function_call_type.return_type()};
1119  const function_application_exprt rhs(
1120  symbol_exprt{function.get_identifier(), function_type}, arguments);
1121 
1122  code_assignt assignment(lhs, rhs);
1123  assignment.add_source_location()=function.source_location();
1124  copy(assignment, ASSIGN, dest);
1125  }
1126  else if(identifier==CPROVER_PREFIX "array_equal")
1127  {
1128  do_array_op(ID_array_equal, lhs, function, arguments, dest);
1129  }
1130  else if(identifier==CPROVER_PREFIX "array_set")
1131  {
1132  do_array_op(ID_array_set, lhs, function, arguments, dest);
1133  }
1134  else if(identifier==CPROVER_PREFIX "array_copy")
1135  {
1136  do_array_op(ID_array_copy, lhs, function, arguments, dest);
1137  }
1138  else if(identifier==CPROVER_PREFIX "array_replace")
1139  {
1140  do_array_op(ID_array_replace, lhs, function, arguments, dest);
1141  }
1142  else if(identifier=="__assert_fail" ||
1143  identifier=="_assert" ||
1144  identifier=="__assert_c99" ||
1145  identifier=="_wassert")
1146  {
1147  // __assert_fail is Linux
1148  // These take four arguments:
1149  // "expression", "file.c", line, __func__
1150  // klibc has __assert_fail with 3 arguments
1151  // "expression", "file.c", line
1152 
1153  // MingW has
1154  // void _assert (const char*, const char*, int);
1155  // with three arguments:
1156  // "expression", "file.c", line
1157 
1158  // This has been seen in Solaris 11.
1159  // Signature:
1160  // void __assert_c99(
1161  // const char *desc, const char *file, int line, const char *func);
1162 
1163  // _wassert is Windows. The arguments are
1164  // L"expression", L"file.c", line
1165 
1166  if(arguments.size()!=4 &&
1167  arguments.size()!=3)
1168  {
1169  error().source_location=function.find_source_location();
1170  error() << "'" << identifier << "' expected to have four arguments"
1171  << eom;
1172  throw 0;
1173  }
1174 
1175  const irep_idt description=
1176  "assertion "+id2string(get_string_constant(arguments[0]));
1177 
1178  source_locationt annotated_location = function.source_location();
1179  annotated_location.set("user-provided", true);
1180  annotated_location.set_property_class(ID_assertion);
1181  annotated_location.set_comment(description);
1182  dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1183  // we ignore any LHS
1184  }
1185  else if(identifier=="__assert_rtn" ||
1186  identifier=="__assert")
1187  {
1188  // __assert_rtn has been seen on MacOS;
1189  // __assert is FreeBSD and Solaris 11.
1190  // These take four arguments:
1191  // __func__, "file.c", line, "expression"
1192  // On Solaris 11, it's three arguments:
1193  // "expression", "file", line
1194 
1195  irep_idt description;
1196 
1197  if(arguments.size()==4)
1198  {
1199  description=
1200  "assertion "+id2string(get_string_constant(arguments[3]));
1201  }
1202  else if(arguments.size()==3)
1203  {
1204  description=
1205  "assertion "+id2string(get_string_constant(arguments[1]));
1206  }
1207  else
1208  {
1209  error().source_location=function.find_source_location();
1210  error() << "'" << identifier << "' expected to have four arguments"
1211  << eom;
1212  throw 0;
1213  }
1214 
1215  source_locationt annotated_location = function.source_location();
1216  annotated_location.set("user-provided", true);
1217  annotated_location.set_property_class(ID_assertion);
1218  annotated_location.set_comment(description);
1219  dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1220  // we ignore any LHS
1221  }
1222  else if(
1223  identifier == "__assert_func" || identifier == "__assert2" ||
1224  identifier == "__assert13")
1225  {
1226  // __assert_func is newlib (used by, e.g., cygwin)
1227  // __assert2 is OpenBSD
1228  // __assert13 is NetBSD
1229  // These take four arguments:
1230  // "file.c", line, __func__, "expression"
1231  if(arguments.size()!=4)
1232  {
1233  error().source_location=function.find_source_location();
1234  error() << "'" << identifier << "' expected to have four arguments"
1235  << eom;
1236  throw 0;
1237  }
1238 
1239  irep_idt description;
1240  try
1241  {
1242  description="assertion "+id2string(get_string_constant(arguments[3]));
1243  }
1244  catch(int)
1245  {
1246  // we might be building newlib, where __assert_func is passed
1247  // a pointer-typed symbol; the warning will still have been
1248  // printed
1249  description="assertion";
1250  }
1251 
1252  source_locationt annotated_location = function.source_location();
1253  annotated_location.set("user-provided", true);
1254  annotated_location.set_property_class(ID_assertion);
1255  annotated_location.set_comment(description);
1256  dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1257  // we ignore any LHS
1258  }
1259  else if(identifier==CPROVER_PREFIX "fence")
1260  {
1261  if(arguments.empty())
1262  {
1263  error().source_location=function.find_source_location();
1264  error() << "'" << identifier << "' expected to have at least one argument"
1265  << eom;
1266  throw 0;
1267  }
1268 
1269  codet fence(ID_fence);
1270 
1271  for(const auto &argument : arguments)
1272  fence.set(get_string_constant(argument), true);
1273 
1274  dest.add(goto_programt::make_other(fence, function.source_location()));
1275  }
1276  else if(identifier=="__builtin_prefetch")
1277  {
1278  // does nothing
1279  }
1280  else if(identifier=="__builtin_unreachable")
1281  {
1282  // says something like UNREACHABLE;
1283  }
1284  else if(identifier==ID_gcc_builtin_va_arg)
1285  {
1286  // This does two things.
1287  // 1) Return value of argument.
1288  // This is just dereferencing.
1289  // 2) Move list pointer to next argument.
1290  // This is just an increment.
1291 
1292  if(arguments.size()!=1)
1293  {
1294  error().source_location=function.find_source_location();
1295  error() << "'" << identifier << "' expected to have one argument" << eom;
1296  throw 0;
1297  }
1298 
1299  exprt list_arg=make_va_list(arguments[0]);
1300 
1301  if(lhs.is_not_nil())
1302  {
1303  exprt list_arg_cast = list_arg;
1304  if(
1305  list_arg.type().id() == ID_pointer &&
1306  to_pointer_type(list_arg.type()).base_type().id() == ID_empty)
1307  {
1308  list_arg_cast =
1310  }
1311 
1312  typet t=pointer_type(lhs.type());
1313  dereference_exprt rhs{
1314  typecast_exprt{dereference_exprt{std::move(list_arg_cast)}, t}};
1315  rhs.add_source_location()=function.source_location();
1316  dest.add(
1317  goto_programt::make_assignment(lhs, rhs, function.source_location()));
1318  }
1319 
1320  code_assignt assign{
1321  list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
1322  assign.rhs().set(
1323  ID_C_va_arg_type, to_code_type(function.type()).return_type());
1325  std::move(assign), function.source_location()));
1326  }
1327  else if(identifier=="__builtin_va_copy")
1328  {
1329  if(arguments.size()!=2)
1330  {
1331  error().source_location=function.find_source_location();
1332  error() << "'" << identifier << "' expected to have two arguments" << eom;
1333  throw 0;
1334  }
1335 
1336  exprt dest_expr=make_va_list(arguments[0]);
1337  const typecast_exprt src_expr(arguments[1], dest_expr.type());
1338 
1339  if(!is_assignable(dest_expr))
1340  {
1342  error() << "va_copy argument expected to be lvalue" << eom;
1343  throw 0;
1344  }
1345 
1347  dest_expr, src_expr, function.source_location()));
1348  }
1349  else if(identifier == "__builtin_va_start" || identifier == "__va_start")
1350  {
1351  // Set the list argument to be the address of the
1352  // parameter argument.
1353  if(arguments.size()!=2)
1354  {
1355  error().source_location=function.find_source_location();
1356  error() << "'" << identifier << "' expected to have two arguments" << eom;
1357  throw 0;
1358  }
1359 
1360  exprt dest_expr=make_va_list(arguments[0]);
1361 
1362  if(!is_assignable(dest_expr))
1363  {
1365  error() << "va_start argument expected to be lvalue" << eom;
1366  throw 0;
1367  }
1368 
1369  if(
1370  dest_expr.type().id() == ID_pointer &&
1371  to_pointer_type(dest_expr.type()).base_type().id() == ID_empty)
1372  {
1373  dest_expr =
1375  }
1376 
1377  side_effect_exprt rhs{
1378  ID_va_start, dest_expr.type(), function.source_location()};
1379  rhs.add_to_operands(
1380  typecast_exprt{address_of_exprt{arguments[1]}, dest_expr.type()});
1381 
1383  std::move(dest_expr), std::move(rhs), function.source_location()));
1384  }
1385  else if(identifier=="__builtin_va_end")
1386  {
1387  // Invalidates the argument. We do so by setting it to NULL.
1388  if(arguments.size()!=1)
1389  {
1390  error().source_location=function.find_source_location();
1391  error() << "'" << identifier << "' expected to have one argument" << eom;
1392  throw 0;
1393  }
1394 
1395  exprt dest_expr=make_va_list(arguments[0]);
1396 
1397  if(!is_assignable(dest_expr))
1398  {
1400  error() << "va_end argument expected to be lvalue" << eom;
1401  throw 0;
1402  }
1403 
1404  // our __builtin_va_list is a pointer
1405  if(dest_expr.type().id() == ID_pointer)
1406  {
1407  const auto zero =
1408  zero_initializer(dest_expr.type(), function.source_location(), ns);
1409  CHECK_RETURN(zero.has_value());
1411  dest_expr, *zero, function.source_location()));
1412  }
1413  }
1414  else if(
1415  identifier == "__builtin_isgreater" ||
1416  identifier == "__builtin_isgreaterequal" ||
1417  identifier == "__builtin_isless" || identifier == "__builtin_islessequal" ||
1418  identifier == "__builtin_islessgreater" ||
1419  identifier == "__builtin_isunordered")
1420  {
1421  // these support two double or two float arguments; we call the
1422  // appropriate internal version
1423  if(arguments.size()!=2 ||
1424  (arguments[0].type()!=double_type() &&
1425  arguments[0].type()!=float_type()) ||
1426  (arguments[1].type()!=double_type() &&
1427  arguments[1].type()!=float_type()))
1428  {
1429  error().source_location=function.find_source_location();
1430  error() << "'" << identifier
1431  << "' expected to have two float/double arguments" << eom;
1432  throw 0;
1433  }
1434 
1435  exprt::operandst new_arguments=arguments;
1436 
1437  bool use_double=arguments[0].type()==double_type();
1438  if(arguments[0].type()!=arguments[1].type())
1439  {
1440  if(use_double)
1441  {
1442  new_arguments[1] =
1443  typecast_exprt(new_arguments[1], arguments[0].type());
1444  }
1445  else
1446  {
1447  new_arguments[0] =
1448  typecast_exprt(new_arguments[0], arguments[1].type());
1449  use_double=true;
1450  }
1451  }
1452 
1453  code_typet f_type=to_code_type(function.type());
1454  f_type.remove_ellipsis();
1455  const typet &a_t=new_arguments[0].type();
1456  f_type.parameters()=
1458 
1459  // replace __builtin_ by CPROVER_PREFIX
1460  std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1461  // append d or f for double/float
1462  name+=use_double?'d':'f';
1463 
1465  ns.lookup(name).type == f_type,
1466  "builtin declaration should match constructed type");
1467 
1468  symbol_exprt new_function=function;
1469  new_function.set_identifier(name);
1470  new_function.type()=f_type;
1471 
1472  code_function_callt function_call(lhs, new_function, new_arguments);
1473  function_call.add_source_location()=function.source_location();
1474 
1475  copy(function_call, FUNCTION_CALL, dest);
1476  }
1477  else if(identifier == "alloca" || identifier == "__builtin_alloca")
1478  {
1479  do_alloca(lhs, function, arguments, dest, mode);
1480  }
1481  else
1482  {
1483  do_function_call_symbol(*symbol);
1484 
1485  // insert function call
1486  // use symbol->symbol_expr() to ensure we use the type from the symbol table
1487  code_function_callt function_call(
1488  lhs, symbol->symbol_expr().with_source_location(function), arguments);
1489  function_call.add_source_location()=function.source_location();
1490 
1491  // remove void-typed assignments, which may have been created when the
1492  // front-end was unable to detect them in type checking for a lack of
1493  // available declarations
1494  if(
1495  lhs.is_not_nil() &&
1496  to_code_type(symbol->type).return_type().id() == ID_empty)
1497  {
1498  function_call.lhs().make_nil();
1499  }
1500 
1501  copy(function_call, FUNCTION_CALL, dest);
1502  }
1503 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
Definition: arith_tools.cpp:20
exprt make_va_list(const exprt &expr)
floatbv_typet float_type()
Definition: c_types.cpp:177
empty_typet void_type()
Definition: c_types.cpp:245
signedbv_typet signed_int_type()
Definition: c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:235
signedbv_typet pointer_diff_type()
Definition: c_types.cpp:220
bitvector_typet char_type()
Definition: c_types.cpp:106
bitvector_typet c_index_type()
Definition: c_types.cpp:16
floatbv_typet double_type()
Definition: c_types.cpp:185
Operator to return the address of an object.
Definition: pointer_expr.h:540
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
The Boolean type.
Definition: std_types.h:36
A goto_instruction_codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
A goto_instruction_codet representing the declaration that an input of a particular description has a...
A goto_instruction_codet representing the declaration that an output of a particular description has ...
Base type of functions.
Definition: std_types.h:583
std::vector< parametert > parameterst
Definition: std_types.h:585
const typet & return_type() const
Definition: std_types.h:689
void remove_ellipsis()
Definition: std_types.h:684
const parameterst & parameters() const
Definition: std_types.h:699
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
exprt & op0()
Definition: expr.h:133
void set_statement(const irep_idt &statement)
Definition: std_code_base.h:60
Operator to dereference a pointer.
Definition: pointer_expr.h:834
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition: dstring.h:95
The empty type.
Definition: std_types.h:51
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
std::vector< exprt > operandst
Definition: expr.h:58
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:96
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:163
source_locationt & add_source_location()
Definition: expr.h:236
const source_locationt & source_location() const
Definition: expr.h:231
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3064
Application of (mathematical) function.
void do_havoc_slice(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
symbol_table_baset & symbol_table
void do_input(const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_array_op(const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
irep_idt get_string_constant(const exprt &expr)
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
void do_prob_coin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
struct goto_convertt::targetst targets
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode)
void do_atomic_end(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
virtual void do_function_call_symbol(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
add function calls to function queue for later processing
void clean_expr(exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true)
void do_output(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
void do_printf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
exprt get_array_argument(const exprt &src)
void do_alloca(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
alloca allocates memory that is freed when leaving the function (and not the block,...
void do_scanf(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
void convert(const codet &code, goto_programt &dest, const irep_idt &mode)
converts 'code' and appends the result to 'dest'
void do_atomic_begin(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
static void replace_new_object(const exprt &object, exprt &dest)
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void do_prob_uniform(const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:945
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:971
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:643
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:730
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:722
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:990
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:708
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:957
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:979
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:739
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:964
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:933
The trinary if-then-else operator.
Definition: std_expr.h:2370
Array index operator.
Definition: std_expr.h:1465
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
void make_nil()
Definition: irep.h:442
bool is_nil() const
Definition: irep.h:364
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
Definition: message.h:247
mstreamt & error() const
Definition: message.h:399
static eomt eom
Definition: message.h:297
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
The null pointer constant.
Definition: pointer_expr.h:909
The plus expression Associativity is not specified.
Definition: std_expr.h:1002
const typet & base_type() const
The type of the data what we point to.
Definition: pointer_expr.h:35
A base class for a predicate that indicates that an address range is ok to read or write or both.
Definition: pointer_expr.h:920
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
An expression containing a side effect.
Definition: std_code.h:1450
const irep_idt & get_statement() const
Definition: std_code.h:1472
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
Definition: std_expr.h:131
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:155
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition: std_expr.h:166
const irep_idt & get_identifier() const
Definition: std_expr.h:160
Symbol table entry.
Definition: symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
const typet & subtype() const
Definition: type.h:187
Semantic type conversion.
Definition: std_expr.h:2068
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2076
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:72
source_locationt & add_source_location()
Definition: type.h:77
const exprt & op1() const =delete
#define CPROVER_PREFIX
std::optional< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Expression Initialization.
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:24
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
Deprecated expression utility functions.
std::optional< typet > get_type(const format_tokent &token)
format_token_listt parse_format_string(const std::string &arg_string)
Format String Parser.
std::list< format_tokent > format_token_listt
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
Program Transformation.
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ASSIGN
Definition: goto_program.h:46
@ OTHER
Definition: goto_program.h:37
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for 'mathematical' expressions.
Mathematical types.
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:93
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
exprt object_size(const exprt &pointer)
constant_exprt from_rational(const rationalt &a)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const codet & to_code(const exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:426
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
Definition: std_types.h:29
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
Symbol table entry.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:208
#define size_type
Definition: unistd.c:347