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