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 "destructor.h"
31 #include "format_strings.h"
32 
34  const exprt &lhs,
35  const symbol_exprt &function,
36  const exprt::operandst &arguments,
37  goto_programt &dest)
38 {
39  const irep_idt &identifier = function.get_identifier();
40 
41  // make it a side effect if there is an LHS
42  if(arguments.size() != 2)
43  {
44  error().source_location = function.find_source_location();
45  error() << "'" << identifier << "' expected to have two arguments" << eom;
46  throw 0;
47  }
48 
49  if(lhs.is_nil())
50  {
51  error().source_location = function.find_source_location();
52  error() << "'" << identifier << "' expected to have LHS" << eom;
53  throw 0;
54  }
55 
56  auto rhs =
57  side_effect_exprt("prob_uniform", lhs.type(), function.source_location());
58 
59  if(lhs.type().id() != ID_unsignedbv && 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(
67  arguments[0].type().id() != lhs.type().id() ||
68  arguments[1].type().id() != lhs.type().id())
69  {
70  error().source_location = function.find_source_location();
71  error() << "'" << identifier
72  << "' expected operands to be of same type as LHS" << eom;
73  throw 0;
74  }
75 
76  if(!arguments[0].is_constant() || !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
399  exprt object_size = static_cast<const exprt &>(rhs.find(ID_sizeof));
400 
401  bool new_array = rhs.get(ID_statement) == ID_cpp_new_array;
402 
403  exprt count;
404  clean_expr_resultt side_effects;
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  side_effects.add(clean_expr(count, ID_cpp));
413  dest.destructive_append(side_effects.side_effects);
414  }
415 
416  exprt tmp_symbol_expr;
417 
418  // is this a placement new?
419  if(rhs.operands().empty()) // no, "regular" one
420  {
421  // call __new or __new_array
422  exprt new_symbol =
423  ns.lookup(new_array ? "__new_array" : "__new").symbol_expr();
424 
425  const code_typet &code_type = to_code_type(new_symbol.type());
426 
427  const typet &return_type = code_type.return_type();
428 
430  code_type.parameters().size() == 1 || code_type.parameters().size() == 2,
431  "new has one or two parameters");
432 
433  const symbolt &tmp_symbol =
434  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
435 
436  tmp_symbol_expr = tmp_symbol.symbol_expr();
437 
438  code_function_callt new_call(new_symbol);
439  if(new_array)
440  new_call.arguments().push_back(count);
441  new_call.arguments().push_back(object_size);
442  new_call.set(
443  ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
444  new_call.lhs() = tmp_symbol_expr;
445  new_call.add_source_location() = rhs.source_location();
446 
447  convert(new_call, dest, ID_cpp);
448  }
449  else if(rhs.operands().size() == 1)
450  {
451  // call __placement_new
452  exprt new_symbol =
453  ns.lookup(new_array ? "__placement_new_array" : "__placement_new")
454  .symbol_expr();
455 
456  const code_typet &code_type = to_code_type(new_symbol.type());
457 
458  const typet &return_type = code_type.return_type();
459 
461  code_type.parameters().size() == 2 || code_type.parameters().size() == 3,
462  "placement new has two or three parameters");
463 
464  const symbolt &tmp_symbol =
465  new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
466 
467  tmp_symbol_expr = tmp_symbol.symbol_expr();
468 
469  code_function_callt new_call(new_symbol);
470  if(new_array)
471  new_call.arguments().push_back(count);
472  new_call.arguments().push_back(object_size);
473  new_call.arguments().push_back(to_unary_expr(rhs).op()); // memory location
474  new_call.set(
475  ID_C_cxx_alloc_type, to_type_with_subtype(lhs.type()).subtype());
476  new_call.lhs() = tmp_symbol_expr;
477  new_call.add_source_location() = rhs.source_location();
478 
479  for(std::size_t i = 0; i < code_type.parameters().size(); i++)
480  {
482  new_call.arguments()[i], code_type.parameters()[i].type());
483  }
484 
485  convert(new_call, dest, ID_cpp);
486  }
487  else
488  {
490  error() << "cpp_new expected to have 0 or 1 operands" << eom;
491  throw 0;
492  }
493 
495  lhs,
496  typecast_exprt(tmp_symbol_expr, lhs.type()),
497  rhs.find_source_location()));
498 
499  side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).get_identifier());
500  destruct_locals(side_effects.temporaries, dest, ns);
501 
502  // grab initializer
503  goto_programt tmp_initializer;
504  cpp_new_initializer(lhs, rhs, tmp_initializer);
505 
506  dest.destructive_append(tmp_initializer);
507 }
508 
511  const exprt &lhs,
512  const side_effect_exprt &rhs,
513  goto_programt &dest)
514 {
515  exprt initializer = 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  destruct_locals({nondet_contents.name}, dest, ns);
696 }
697 
701  const exprt &lhs,
702  const symbol_exprt &function,
703  const exprt::operandst &arguments,
704  goto_programt &dest,
705  const irep_idt &mode)
706 {
707  const source_locationt &source_location = function.source_location();
708  const auto alloca_type = to_code_type(function.type());
709 
710  if(alloca_type.return_type() != pointer_type(void_type()))
711  {
712  error().source_location = source_location;
713  error() << "'alloca' function called, but 'alloca' has not been declared "
714  << "with expected 'void *' return type." << eom;
715  throw 0;
716  }
717  if(
718  alloca_type.parameters().size() != 1 ||
719  alloca_type.parameters()[0].type() != size_type())
720  {
721  error().source_location = source_location;
722  error() << "'alloca' function called, but 'alloca' has not been declared "
723  << "with expected single 'size_t' parameter." << eom;
724  throw 0;
725  }
726 
727  exprt new_lhs = lhs;
728 
729  // make sure we have a left-hand side to track the allocation even when the
730  // original program did not
731  if(lhs.is_nil())
732  {
733  new_lhs =
735  alloca_type.return_type(), "alloca", dest, source_location, mode)
736  .symbol_expr();
737  }
738 
739  // do the actual function call
740  code_function_callt function_call(new_lhs, function, arguments);
741  function_call.add_source_location() = source_location;
742  copy(function_call, FUNCTION_CALL, dest);
743 
744  // Don't add instrumentation when we're in alloca (which might in turn call
745  // __builtin_alloca) -- the instrumentation will be done for the call of
746  // alloca. Also, we can only add instrumentation when we're in a function
747  // context.
748  if(
749  function.source_location().get_function() == "alloca" || !targets.prefix ||
750  !targets.suffix)
751  {
752  return;
753  }
754 
755  // create a symbol to eventually (and non-deterministically) mark the
756  // allocation as dead; this symbol has function scope and is initialised to
757  // NULL
758  symbol_exprt this_alloca_ptr =
760  alloca_type.return_type(),
761  id2string(function.source_location().get_function()),
762  "tmp_alloca",
763  source_location,
764  mode,
765  symbol_table)
766  .symbol_expr();
767  goto_programt decl_prg;
768  decl_prg.add(goto_programt::make_decl(this_alloca_ptr, source_location));
770  this_alloca_ptr,
771  null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())},
772  source_location));
774  targets.prefix->instructions.begin(), decl_prg);
775 
776  // non-deterministically update this_alloca_ptr
777  if_exprt rhs{
778  side_effect_expr_nondett{bool_typet(), source_location},
779  new_lhs,
780  this_alloca_ptr};
782  this_alloca_ptr, std::move(rhs), source_location));
783 
784  if(lhs.is_nil())
785  destruct_locals({to_symbol_expr(new_lhs).get_identifier()}, dest, ns);
786 
787  // mark pointer to alloca result as dead, unless the alloca result (in
788  // this_alloca_ptr) is still NULL
789  symbol_exprt dead_object_sym =
790  ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr();
791  exprt alloca_result =
792  typecast_exprt::conditional_cast(this_alloca_ptr, dead_object_sym.type());
793  if_exprt not_null{
794  equal_exprt{
795  this_alloca_ptr,
796  null_pointer_exprt{to_pointer_type(this_alloca_ptr.type())}},
797  dead_object_sym,
798  std::move(alloca_result)};
799  auto assign = goto_programt::make_assignment(
800  std::move(dead_object_sym), std::move(not_null), source_location);
802  targets.suffix->instructions.begin(), assign);
804  targets.suffix->instructions.begin(),
805  goto_programt::make_dead(this_alloca_ptr, source_location));
806 }
807 
810  const exprt &lhs,
811  const symbol_exprt &function,
812  const exprt::operandst &arguments,
813  goto_programt &dest,
814  const irep_idt &mode)
815 {
816  if(function.get_bool(ID_C_invalid_object))
817  return; // ignore
818 
819  // lookup symbol
820  const irep_idt &identifier = function.get_identifier();
821 
822  const symbolt *symbol;
823  if(ns.lookup(identifier, symbol))
824  {
825  error().source_location = function.find_source_location();
826  error() << "function '" << identifier << "' not found" << eom;
827  throw 0;
828  }
829 
830  if(symbol->type.id() != ID_code)
831  {
832  error().source_location = function.find_source_location();
833  error() << "function '" << identifier << "' type mismatch: expected code"
834  << eom;
835  throw 0;
836  }
837 
838  // User-provided function definitions always take precedence over built-ins.
839  // Front-ends do not (yet) consistently set ID_C_incomplete, thus also test
840  // whether the symbol actually has some non-nil value (which might be
841  // "compiled").
842  if(!symbol->type.get_bool(ID_C_incomplete) && symbol->value.is_not_nil())
843  {
844  do_function_call_symbol(*symbol);
845 
846  // use symbol->symbol_expr() to ensure we use the type from the symbol table
847  code_function_callt function_call(
848  lhs, symbol->symbol_expr().with_source_location(function), arguments);
849  function_call.add_source_location() = function.source_location();
850 
851  // remove void-typed assignments, which may have been created when the
852  // front-end was unable to detect them in type checking for a lack of
853  // available declarations
854  if(
855  lhs.is_not_nil() &&
856  to_code_type(symbol->type).return_type().id() == ID_empty)
857  {
858  function_call.lhs().make_nil();
859  }
860 
861  copy(function_call, FUNCTION_CALL, dest);
862 
863  return;
864  }
865 
866  if(identifier == CPROVER_PREFIX "havoc_slice")
867  {
868  do_havoc_slice(lhs, function, arguments, dest, mode);
869  }
870  else if(
871  identifier == CPROVER_PREFIX "assume" || identifier == "__VERIFIER_assume")
872  {
873  if(arguments.size() != 1)
874  {
875  error().source_location = function.find_source_location();
876  error() << "'" << identifier << "' expected to have one argument" << eom;
877  throw 0;
878  }
879 
880  // let's double-check the type of the argument
881  source_locationt annotated_location = function.source_location();
882  annotated_location.set("user-provided", true);
884  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
885  annotated_location));
886 
887  if(lhs.is_not_nil())
888  {
889  error().source_location = function.find_source_location();
890  error() << identifier << " expected not to have LHS" << eom;
891  throw 0;
892  }
893  }
894  else if(identifier == "__VERIFIER_error")
895  {
896  if(!arguments.empty())
897  {
898  error().source_location = function.find_source_location();
899  error() << "'" << identifier << "' expected to have no arguments" << eom;
900  throw 0;
901  }
902 
903  source_locationt annotated_location = function.source_location();
904  annotated_location.set("user-provided", true);
905  annotated_location.set_property_class(ID_assertion);
906  dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
907 
908  if(lhs.is_not_nil())
909  {
910  error().source_location = function.find_source_location();
911  error() << identifier << " expected not to have LHS" << eom;
912  throw 0;
913  }
914 
915  // __VERIFIER_error has abort() semantics, even if no assertions
916  // are being checked
917  annotated_location = function.source_location();
918  annotated_location.set("user-provided", true);
919  dest.add(goto_programt::make_assumption(false_exprt(), annotated_location));
920  dest.instructions.back().labels.push_back("__VERIFIER_abort");
921  }
922  else if(
923  identifier == "assert" &&
925  {
926  if(arguments.size() != 1)
927  {
928  error().source_location = function.find_source_location();
929  error() << "'" << identifier << "' expected to have one argument" << eom;
930  throw 0;
931  }
932 
933  // let's double-check the type of the argument
934  source_locationt annotated_location = function.source_location();
935  annotated_location.set("user-provided", true);
936  annotated_location.set_property_class(ID_assertion);
937  annotated_location.set_comment(
938  "assertion " + from_expr(ns, identifier, arguments.front()));
940  typecast_exprt::conditional_cast(arguments.front(), bool_typet()),
941  annotated_location));
942 
943  if(lhs.is_not_nil())
944  {
945  error().source_location = function.find_source_location();
946  error() << identifier << " expected not to have LHS" << eom;
947  throw 0;
948  }
949  }
950  else if(
951  identifier == CPROVER_PREFIX "assert" ||
952  identifier == CPROVER_PREFIX "precondition" ||
953  identifier == CPROVER_PREFIX "postcondition")
954  {
955  if(arguments.size() != 2)
956  {
957  error().source_location = function.find_source_location();
958  error() << "'" << identifier << "' expected to have two arguments" << eom;
959  throw 0;
960  }
961 
962  bool is_precondition = identifier == CPROVER_PREFIX "precondition";
963  bool is_postcondition = identifier == CPROVER_PREFIX "postcondition";
964 
965  const irep_idt description = get_string_constant(arguments[1]);
966 
967  // let's double-check the type of the argument
968  source_locationt annotated_location = function.source_location();
969  if(is_precondition)
970  {
971  annotated_location.set_property_class(ID_precondition);
972  }
973  else if(is_postcondition)
974  {
975  annotated_location.set_property_class(ID_postcondition);
976  }
977  else
978  {
979  annotated_location.set(
980  "user-provided", !function.source_location().is_built_in());
981  annotated_location.set_property_class(ID_assertion);
982  }
983 
984  annotated_location.set_comment(description);
985 
988  annotated_location));
989 
990  if(lhs.is_not_nil())
991  {
992  error().source_location = function.find_source_location();
993  error() << identifier << " expected not to have LHS" << eom;
994  throw 0;
995  }
996  }
997  else if(identifier == CPROVER_PREFIX "havoc_object")
998  {
999  if(arguments.size() != 1)
1000  {
1001  error().source_location = function.find_source_location();
1002  error() << "'" << identifier << "' expected to have one argument" << eom;
1003  throw 0;
1004  }
1005 
1006  if(lhs.is_not_nil())
1007  {
1008  error().source_location = function.find_source_location();
1009  error() << identifier << " expected not to have LHS" << eom;
1010  throw 0;
1011  }
1012 
1013  codet havoc(ID_havoc_object);
1014  havoc.add_source_location() = function.source_location();
1015  havoc.copy_to_operands(arguments[0]);
1016 
1017  dest.add(goto_programt::make_other(havoc, function.source_location()));
1018  }
1019  else if(identifier == CPROVER_PREFIX "printf")
1020  {
1021  do_printf(lhs, function, arguments, dest);
1022  }
1023  else if(identifier == CPROVER_PREFIX "scanf")
1024  {
1025  do_scanf(lhs, function, arguments, dest);
1026  }
1027  else if(
1028  identifier == CPROVER_PREFIX "input" || identifier == "__CPROVER::input")
1029  {
1030  if(lhs.is_not_nil())
1031  {
1032  error().source_location = function.find_source_location();
1033  error() << identifier << " expected not to have LHS" << eom;
1034  throw 0;
1035  }
1036 
1037  do_input(function, arguments, dest);
1038  }
1039  else if(
1040  identifier == CPROVER_PREFIX "output" || identifier == "__CPROVER::output")
1041  {
1042  if(lhs.is_not_nil())
1043  {
1044  error().source_location = function.find_source_location();
1045  error() << identifier << " expected not to have LHS" << eom;
1046  throw 0;
1047  }
1048 
1049  do_output(function, arguments, dest);
1050  }
1051  else if(
1052  identifier == CPROVER_PREFIX "atomic_begin" ||
1053  identifier == "__CPROVER::atomic_begin" ||
1054  identifier == "java::org.cprover.CProver.atomicBegin:()V" ||
1055  identifier == "__VERIFIER_atomic_begin")
1056  {
1057  do_atomic_begin(lhs, function, arguments, dest);
1058  }
1059  else if(
1060  identifier == CPROVER_PREFIX "atomic_end" ||
1061  identifier == "__CPROVER::atomic_end" ||
1062  identifier == "java::org.cprover.CProver.atomicEnd:()V" ||
1063  identifier == "__VERIFIER_atomic_end")
1064  {
1065  do_atomic_end(lhs, function, arguments, dest);
1066  }
1067  else if(identifier == CPROVER_PREFIX "prob_biased_coin")
1068  {
1069  do_prob_coin(lhs, function, arguments, dest);
1070  }
1071  else if(identifier.starts_with(CPROVER_PREFIX "prob_uniform_"))
1072  {
1073  do_prob_uniform(lhs, function, arguments, dest);
1074  }
1075  else if(
1076  identifier.starts_with("nondet_") ||
1077  identifier.starts_with("__VERIFIER_nondet_"))
1078  {
1079  // make it a side effect if there is an LHS
1080  if(lhs.is_nil())
1081  return;
1082 
1083  exprt rhs;
1084 
1085  // We need to special-case for _Bool, which
1086  // can only be 0 or 1.
1087  if(lhs.type().id() == ID_c_bool)
1088  {
1089  rhs = side_effect_expr_nondett(bool_typet(), function.source_location());
1090  rhs.set(ID_C_identifier, identifier);
1091  rhs = typecast_exprt(rhs, lhs.type());
1092  }
1093  else
1094  {
1095  rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
1096  rhs.set(ID_C_identifier, identifier);
1097  }
1098 
1099  code_assignt assignment(lhs, rhs);
1100  assignment.add_source_location() = function.source_location();
1101  copy(assignment, ASSIGN, dest);
1102  }
1103  else if(identifier.starts_with(CPROVER_PREFIX "uninterpreted_"))
1104  {
1105  // make it a side effect if there is an LHS
1106  if(lhs.is_nil())
1107  return;
1108 
1109  if(function.type().get_bool(ID_C_incomplete))
1110  {
1111  error().source_location = function.find_source_location();
1112  error() << "'" << identifier << "' is not declared, "
1113  << "missing type information required to construct call to "
1114  << "uninterpreted function" << eom;
1115  throw 0;
1116  }
1117 
1118  const code_typet &function_call_type = to_code_type(function.type());
1120  for(const auto &parameter : function_call_type.parameters())
1121  domain.push_back(parameter.type());
1122  mathematical_function_typet function_type{
1123  domain, function_call_type.return_type()};
1124  const function_application_exprt rhs(
1125  symbol_exprt{function.get_identifier(), function_type}, arguments);
1126 
1127  code_assignt assignment(lhs, rhs);
1128  assignment.add_source_location() = function.source_location();
1129  copy(assignment, ASSIGN, dest);
1130  }
1131  else if(identifier == CPROVER_PREFIX "array_equal")
1132  {
1133  do_array_op(ID_array_equal, lhs, function, arguments, dest);
1134  }
1135  else if(identifier == CPROVER_PREFIX "array_set")
1136  {
1137  do_array_op(ID_array_set, lhs, function, arguments, dest);
1138  }
1139  else if(identifier == CPROVER_PREFIX "array_copy")
1140  {
1141  do_array_op(ID_array_copy, lhs, function, arguments, dest);
1142  }
1143  else if(identifier == CPROVER_PREFIX "array_replace")
1144  {
1145  do_array_op(ID_array_replace, lhs, function, arguments, dest);
1146  }
1147  else if(
1148  identifier == "__assert_fail" || identifier == "_assert" ||
1149  identifier == "__assert_c99" || identifier == "_wassert")
1150  {
1151  // __assert_fail is Linux
1152  // These take four arguments:
1153  // "expression", "file.c", line, __func__
1154  // klibc has __assert_fail with 3 arguments
1155  // "expression", "file.c", line
1156 
1157  // MingW has
1158  // void _assert (const char*, const char*, int);
1159  // with three arguments:
1160  // "expression", "file.c", line
1161 
1162  // This has been seen in Solaris 11.
1163  // Signature:
1164  // void __assert_c99(
1165  // const char *desc, const char *file, int line, const char *func);
1166 
1167  // _wassert is Windows. The arguments are
1168  // L"expression", L"file.c", line
1169 
1170  if(arguments.size() != 4 && arguments.size() != 3)
1171  {
1172  error().source_location = function.find_source_location();
1173  error() << "'" << identifier << "' expected to have four arguments"
1174  << eom;
1175  throw 0;
1176  }
1177 
1178  const irep_idt description =
1179  "assertion " + id2string(get_string_constant(arguments[0]));
1180 
1181  source_locationt annotated_location = function.source_location();
1182  annotated_location.set("user-provided", true);
1183  annotated_location.set_property_class(ID_assertion);
1184  annotated_location.set_comment(description);
1185  dest.add(goto_programt::make_assertion(false_exprt(), annotated_location));
1186  // we ignore any LHS
1187  }
1188  else if(identifier == "__assert_rtn" || identifier == "__assert")
1189  {
1190  // __assert_rtn has been seen on MacOS;
1191  // __assert is FreeBSD and Solaris 11.
1192  // These take four arguments:
1193  // __func__, "file.c", line, "expression"
1194  // On Solaris 11, it's three arguments:
1195  // "expression", "file", line
1196 
1197  irep_idt description;
1198 
1199  if(arguments.size() == 4)
1200  {
1201  description = "assertion " + id2string(get_string_constant(arguments[3]));
1202  }
1203  else if(arguments.size() == 3)
1204  {
1205  description = "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  {
1341  error().source_location = dest_expr.find_source_location();
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  {
1364  error().source_location = dest_expr.find_source_location();
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  {
1399  error().source_location = dest_expr.find_source_location();
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(
1424  arguments.size() != 2 ||
1425  (arguments[0].type() != double_type() &&
1426  arguments[0].type() != float_type()) ||
1427  (arguments[1].type() != double_type() &&
1428  arguments[1].type() != float_type()))
1429  {
1430  error().source_location = function.find_source_location();
1431  error() << "'" << identifier
1432  << "' expected to have two float/double arguments" << eom;
1433  throw 0;
1434  }
1435 
1436  exprt::operandst new_arguments = arguments;
1437 
1438  bool use_double = arguments[0].type() == double_type();
1439  if(arguments[0].type() != arguments[1].type())
1440  {
1441  if(use_double)
1442  {
1443  new_arguments[1] =
1444  typecast_exprt(new_arguments[1], arguments[0].type());
1445  }
1446  else
1447  {
1448  new_arguments[0] =
1449  typecast_exprt(new_arguments[0], arguments[1].type());
1450  use_double = true;
1451  }
1452  }
1453 
1454  code_typet f_type = to_code_type(function.type());
1455  f_type.remove_ellipsis();
1456  const typet &a_t = new_arguments[0].type();
1457  f_type.parameters() =
1459 
1460  // replace __builtin_ by CPROVER_PREFIX
1461  std::string name = CPROVER_PREFIX + id2string(identifier).substr(10);
1462  // append d or f for double/float
1463  name += use_double ? 'd' : 'f';
1464 
1466  ns.lookup(name).type == f_type,
1467  "builtin declaration should match constructed type");
1468 
1469  symbol_exprt new_function = function;
1470  new_function.set_identifier(name);
1471  new_function.type() = f_type;
1472 
1473  code_function_callt function_call(lhs, new_function, new_arguments);
1474  function_call.add_source_location() = function.source_location();
1475 
1476  copy(function_call, FUNCTION_CALL, dest);
1477  }
1478  else if(identifier == "alloca" || identifier == "__builtin_alloca")
1479  {
1480  do_alloca(lhs, function, arguments, dest, mode);
1481  }
1482  else
1483  {
1484  do_function_call_symbol(*symbol);
1485 
1486  // insert function call
1487  // use symbol->symbol_expr() to ensure we use the type from the symbol table
1488  code_function_callt function_call(
1489  lhs, symbol->symbol_expr().with_source_location(function), arguments);
1490  function_call.add_source_location() = function.source_location();
1491 
1492  // remove void-typed assignments, which may have been created when the
1493  // front-end was unable to detect them in type checking for a lack of
1494  // available declarations
1495  if(
1496  lhs.is_not_nil() &&
1497  to_code_type(symbol->type).return_type().id() == ID_empty)
1498  {
1499  function_call.lhs().make_nil();
1500  }
1501 
1502  copy(function_call, FUNCTION_CALL, dest);
1503  }
1504 }
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:1366
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:3077
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 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)
clean_expr_resultt clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used=true)
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:2375
Array index operator.
Definition: std_expr.h:1470
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:412
bool is_not_nil() const
Definition: irep.h:372
const irep_idt & id() const
Definition: irep.h:388
void make_nil()
Definition: irep.h:446
bool is_nil() const
Definition: irep.h:368
A type for mathematical functions (do not confuse with functions/methods in code)
std::vector< typet > domaint
source_locationt source_location
Definition: message.h:239
mstreamt & error() const
Definition: message.h:391
static eomt eom
Definition: message.h:289
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
irep_idt name
The unique identifier.
Definition: symbol.h:40
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:2073
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2081
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
void destruct_locals(const std::list< irep_idt > &vars, goto_programt &dest, const namespacet &ns)
Definition: destructor.cpp:62
Destructor Calls.
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:193
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:44
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:3050
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2107
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:1538
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
std::list< irep_idt > temporaries
Identifiers of temporaries introduced while cleaning an expression.
void add(clean_expr_resultt &&other)
void add_temporary(const irep_idt &id)
goto_programt side_effects
Statements implementing side effects of the expression that was subject to cleaning.
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