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/rational.h>
17 #include <util/replace_expr.h>
18 #include <util/rational_tools.h>
19 #include <util/source_location.h>
20 #include <util/cprover_prefix.h>
21 #include <util/prefix.h>
22 #include <util/arith_tools.h>
23 #include <util/simplify_expr.h>
24 #include <util/std_code.h>
25 #include <util/std_expr.h>
26 #include <util/symbol.h>
29 
31 
32 #include <util/c_types.h>
33 #include <ansi-c/string_constant.h>
34 
35 #include "format_strings.h"
36 
38  const exprt &lhs,
39  const exprt &function,
40  const exprt::operandst &arguments,
41  goto_programt &dest)
42 {
43  const irep_idt &identifier=function.get(ID_identifier);
44 
45  // make it a side effect if there is an LHS
46  if(arguments.size()!=2)
47  {
48  error().source_location=function.find_source_location();
49  error() << "`" << identifier
50  << "' expected to have two arguments" << eom;
51  throw 0;
52  }
53 
54  if(lhs.is_nil())
55  {
56  error().source_location=function.find_source_location();
57  error() << "`" << identifier << "' expected to have LHS" << eom;
58  throw 0;
59  }
60 
61  exprt rhs=side_effect_exprt("prob_uniform", lhs.type());
62  rhs.add_source_location()=function.source_location();
63 
64  if(lhs.type().id()!=ID_unsignedbv &&
65  lhs.type().id()!=ID_signedbv)
66  {
67  error().source_location=function.find_source_location();
68  error() << "`" << identifier << "' expected other type" << eom;
69  throw 0;
70  }
71 
72  if(arguments[0].type().id()!=lhs.type().id() ||
73  arguments[1].type().id()!=lhs.type().id())
74  {
75  error().source_location=function.find_source_location();
76  error() << "`" << identifier
77  << "' expected operands to be of same type as LHS" << eom;
78  throw 0;
79  }
80 
81  if(!arguments[0].is_constant() ||
82  !arguments[1].is_constant())
83  {
84  error().source_location=function.find_source_location();
85  error() << "`" << identifier
86  << "' expected operands to be constant literals" << eom;
87  throw 0;
88  }
89 
90  mp_integer lb, ub;
91 
92  if(to_integer(arguments[0], lb) ||
93  to_integer(arguments[1], ub))
94  {
95  error().source_location=function.find_source_location();
96  error() << "error converting operands" << eom;
97  throw 0;
98  }
99 
100  if(lb > ub)
101  {
102  error().source_location=function.find_source_location();
103  error() << "expected lower bound to be smaller or equal to the "
104  << "upper bound" << eom;
105  throw 0;
106  }
107 
108  rhs.copy_to_operands(arguments[0], arguments[1]);
109 
110  code_assignt assignment(lhs, rhs);
111  assignment.add_source_location()=function.source_location();
112  copy(assignment, ASSIGN, dest);
113 }
114 
116  const exprt &lhs,
117  const exprt &function,
118  const exprt::operandst &arguments,
119  goto_programt &dest)
120 {
121  const irep_idt &identifier=function.get(ID_identifier);
122 
123  // make it a side effect if there is an LHS
124  if(arguments.size()!=2)
125  {
126  error().source_location=function.find_source_location();
127  error() << "`" << identifier << "' expected to have two arguments"
128  << eom;
129  throw 0;
130  }
131 
132  if(lhs.is_nil())
133  {
134  error().source_location=function.find_source_location();
135  error() << "`" << identifier << "' expected to have LHS" << eom;
136  throw 0;
137  }
138 
139  exprt rhs=side_effect_exprt("prob_coin", lhs.type());
140  rhs.add_source_location()=function.source_location();
141 
142  if(lhs.type()!=bool_typet())
143  {
144  error().source_location=function.find_source_location();
145  error() << "`" << identifier << "' expected bool" << eom;
146  throw 0;
147  }
148 
149  if(arguments[0].type().id()!=ID_unsignedbv ||
150  arguments[0].id()!=ID_constant)
151  {
152  error().source_location=function.find_source_location();
153  error() << "`" << identifier << "' expected first 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(to_integer(arguments[0], num) ||
161  to_integer(arguments[1], den))
162  {
163  error().source_location=function.find_source_location();
164  error() << "error converting operands" << eom;
165  throw 0;
166  }
167 
168  if(num-den > mp_integer(0))
169  {
170  error().source_location=function.find_source_location();
171  error() << "probability has to be smaller than 1" << eom;
172  throw 0;
173  }
174 
175  if(den == mp_integer(0))
176  {
177  error().source_location=function.find_source_location();
178  error() << "denominator may not be zero" << eom;
179  throw 0;
180  }
181 
182  rationalt numerator(num), denominator(den);
183  rationalt prob = numerator / denominator;
184 
185  rhs.copy_to_operands(from_rational(prob));
186 
187  code_assignt assignment(lhs, rhs);
188  assignment.add_source_location()=function.source_location();
189  copy(assignment, ASSIGN, dest);
190 }
191 
193  const exprt &lhs,
194  const exprt &function,
195  const exprt::operandst &arguments,
196  goto_programt &dest)
197 {
198  const irep_idt &f_id=function.get(ID_identifier);
199 
200  if(f_id==CPROVER_PREFIX "printf" ||
201  f_id=="printf")
202  {
203  typet return_type=
204  static_cast<const typet &>(function.type().find(ID_return_type));
205  side_effect_exprt printf_code(ID_printf, return_type);
206 
207  printf_code.operands()=arguments;
208  printf_code.add_source_location()=function.source_location();
209 
210  if(lhs.is_not_nil())
211  {
212  code_assignt assignment(lhs, printf_code);
213  assignment.add_source_location()=function.source_location();
214  copy(assignment, ASSIGN, dest);
215  }
216  else
217  {
218  printf_code.id(ID_code);
219  printf_code.type()=typet(ID_code);
220  copy(to_code(printf_code), OTHER, dest);
221  }
222  }
223  else
224  assert(false);
225 }
226 
228  const exprt &lhs,
229  const exprt &function,
230  const exprt::operandst &arguments,
231  goto_programt &dest)
232 {
233  const irep_idt &f_id=function.get(ID_identifier);
234 
235  if(f_id==CPROVER_PREFIX "scanf")
236  {
237  if(arguments.empty())
238  {
239  error().source_location=function.find_source_location();
240  error() << "scanf takes at least one argument" << eom;
241  throw 0;
242  }
243 
244  irep_idt format_string;
245 
246  if(!get_string_constant(arguments[0], format_string))
247  {
248  // use our model
249  format_token_listt token_list=
250  parse_format_string(id2string(format_string));
251 
252  std::size_t argument_number=1;
253 
254  for(const auto &t : token_list)
255  {
256  typet type=get_type(t);
257 
258  if(type.is_not_nil())
259  {
260  if(argument_number<arguments.size())
261  {
262  exprt ptr=
263  typecast_exprt(arguments[argument_number], pointer_type(type));
264  argument_number++;
265 
266  if(type.id()==ID_array)
267  {
268  #if 0
269  // A string. We first need a nondeterministic size.
271  to_array_type(type).size()=size;
272 
273  const symbolt &tmp_symbol=
275  type, "scanf_string", dest, function.source_location());
276 
277  exprt rhs=
279  index_exprt(
280  tmp_symbol.symbol_expr(),
281  from_integer(0, index_type())));
282 
283  // now use array copy
284  codet array_copy_statement;
285  array_copy_statement.set_statement(ID_array_copy);
286  array_copy_statement.operands().resize(2);
287  array_copy_statement.op0()=ptr;
288 \ array_copy_statement.op1()=rhs;
289  array_copy_statement.add_source_location()=
290  function.source_location();
291 
292  copy(array_copy_statement, OTHER, dest);
293  #else
294  exprt lhs=
295  index_exprt(
296  dereference_exprt(ptr, type), from_integer(0, index_type()));
298  code_assignt assign(lhs, rhs);
299  assign.add_source_location()=function.source_location();
300  copy(assign, ASSIGN, dest);
301  #endif
302  }
303  else
304  {
305  // make it nondet for now
306  exprt lhs=dereference_exprt(ptr, type);
308  code_assignt assign(lhs, rhs);
309  assign.add_source_location()=function.source_location();
310  copy(assign, ASSIGN, dest);
311  }
312  }
313  }
314  }
315  }
316  else
317  {
318  // we'll just do nothing
319  code_function_callt function_call;
320  function_call.lhs()=lhs;
321  function_call.function()=function;
322  function_call.arguments()=arguments;
323  function_call.add_source_location()=function.source_location();
324 
325  copy(function_call, FUNCTION_CALL, dest);
326  }
327  }
328  else
329  assert(false);
330 }
331 
333  const exprt &lhs,
334  const exprt &function,
335  const exprt::operandst &arguments,
336  goto_programt &dest)
337 {
338  codet input_code;
339  input_code.set_statement(ID_input);
340  input_code.operands()=arguments;
341  input_code.add_source_location()=function.source_location();
342 
343  if(arguments.size()<2)
344  {
345  error().source_location=function.find_source_location();
346  error() << "input takes at least two arguments" << eom;
347  throw 0;
348  }
349 
350  copy(input_code, OTHER, dest);
351 }
352 
354  const exprt &lhs,
355  const exprt &function,
356  const exprt::operandst &arguments,
357  goto_programt &dest)
358 {
359  codet output_code;
360  output_code.set_statement(ID_output);
361  output_code.operands()=arguments;
362  output_code.add_source_location()=function.source_location();
363 
364  if(arguments.size()<2)
365  {
366  error().source_location=function.find_source_location();
367  error() << "output takes at least two arguments" << eom;
368  throw 0;
369  }
370 
371  copy(output_code, OTHER, dest);
372 }
373 
375  const exprt &lhs,
376  const exprt &function,
377  const exprt::operandst &arguments,
378  goto_programt &dest)
379 {
380  if(lhs.is_not_nil())
381  {
383  error() << "atomic_begin does not expect an LHS" << eom;
384  throw 0;
385  }
386 
387  if(!arguments.empty())
388  {
389  error().source_location=function.find_source_location();
390  error() << "atomic_begin takes no arguments" << eom;
391  throw 0;
392  }
393 
395  t->source_location=function.source_location();
396 }
397 
399  const exprt &lhs,
400  const exprt &function,
401  const exprt::operandst &arguments,
402  goto_programt &dest)
403 {
404  if(lhs.is_not_nil())
405  {
407  error() << "atomic_end does not expect an LHS" << eom;
408  throw 0;
409  }
410 
411  if(!arguments.empty())
412  {
413  error().source_location=function.find_source_location();
414  error() << "atomic_end takes no arguments" << eom;
415  throw 0;
416  }
417 
419  t->source_location=function.source_location();
420 }
421 
423  const exprt &lhs,
424  const side_effect_exprt &rhs,
425  goto_programt &dest)
426 {
427  if(lhs.is_nil())
428  {
430  error() << "do_cpp_new without lhs is yet to be implemented" << eom;
431  throw 0;
432  }
433 
434  // build size expression
436  static_cast<const exprt &>(rhs.find(ID_sizeof));
437 
438  bool new_array=rhs.get(ID_statement)==ID_cpp_new_array;
439 
440  exprt count;
441 
442  if(new_array)
443  {
444  count=static_cast<const exprt &>(rhs.find(ID_size));
445 
446  if(count.type()!=object_size.type())
447  count.make_typecast(object_size.type());
448 
449  // might have side-effect
450  clean_expr(count, dest);
451  }
452 
453  exprt tmp_symbol_expr;
454 
455  // is this a placement new?
456  if(rhs.operands().empty()) // no, "regular" one
457  {
458  // call __new or __new_array
459  exprt new_symbol=
460  ns.lookup(new_array?"__new_array":"__new").symbol_expr();
461 
462  const code_typet &code_type=
463  to_code_type(new_symbol.type());
464 
465  const typet &return_type=
466  code_type.return_type();
467 
468  assert(code_type.parameters().size()==1 ||
469  code_type.parameters().size()==2);
470 
471  const symbolt &tmp_symbol=
472  new_tmp_symbol(return_type, "new", dest, rhs.source_location());
473 
474  tmp_symbol_expr=tmp_symbol.symbol_expr();
475 
476  code_function_callt new_call;
477  new_call.function()=new_symbol;
478  if(new_array)
479  new_call.arguments().push_back(count);
480  new_call.arguments().push_back(object_size);
481  new_call.set(ID_C_cxx_alloc_type, lhs.type().subtype());
482  new_call.lhs()=tmp_symbol_expr;
483  new_call.add_source_location()=rhs.source_location();
484 
485  convert(new_call, dest);
486  }
487  else if(rhs.operands().size()==1)
488  {
489  // call __placement_new
490  exprt new_symbol=
491  ns.lookup(
492  new_array?"__placement_new_array":"__placement_new").symbol_expr();
493 
494  const code_typet &code_type=
495  to_code_type(new_symbol.type());
496 
497  const typet &return_type=code_type.return_type();
498 
499  assert(code_type.parameters().size()==2 ||
500  code_type.parameters().size()==3);
501 
502  const symbolt &tmp_symbol=
503  new_tmp_symbol(return_type, "new", dest, rhs.source_location());
504 
505  tmp_symbol_expr=tmp_symbol.symbol_expr();
506 
507  code_function_callt new_call;
508  new_call.function()=new_symbol;
509  if(new_array)
510  new_call.arguments().push_back(count);
511  new_call.arguments().push_back(object_size);
512  new_call.arguments().push_back(rhs.op0()); // memory location
513  new_call.set(ID_C_cxx_alloc_type, lhs.type().subtype());
514  new_call.lhs()=tmp_symbol_expr;
515  new_call.add_source_location()=rhs.source_location();
516 
517  for(unsigned i=0; i<code_type.parameters().size(); i++)
518  if(new_call.arguments()[i].type()!=code_type.parameters()[i].type())
519  new_call.arguments()[i].make_typecast(code_type.parameters()[i].type());
520 
521  convert(new_call, dest);
522  }
523  else
524  {
526  error() << "cpp_new expected to have 0 or 1 operands" << eom;
527  throw 0;
528  }
529 
531  t_n->code=code_assignt(
532  lhs, typecast_exprt(tmp_symbol_expr, lhs.type()));
533  t_n->source_location=rhs.find_source_location();
534 
535  // grab initializer
536  goto_programt tmp_initializer;
537  cpp_new_initializer(lhs, rhs, tmp_initializer);
538 
539  dest.destructive_append(tmp_initializer);
540 }
541 
543  struct_exprt &expr,
544  const namespacet &ns,
545  const symbol_typet &class_type)
546 {
547  const struct_typet &struct_type=
548  to_struct_type(ns.follow(expr.type()));
549  const struct_typet::componentst &components=struct_type.components();
550 
551  if(components.empty())
552  return;
553  assert(!expr.operands().empty());
554 
555  if(components.front().get_name()=="@class_identifier")
556  {
557  assert(expr.op0().id()==ID_constant);
558  expr.op0()=constant_exprt(class_type.get_identifier(), string_typet());
559  }
560  else
561  {
562  assert(expr.op0().id()==ID_struct);
563  set_class_identifier(to_struct_expr(expr.op0()), ns, class_type);
564  }
565 }
566 
568  const exprt &lhs,
569  const side_effect_exprt &rhs,
570  goto_programt &dest)
571 {
572  if(lhs.is_nil())
573  {
575  error() << "do_java_new without lhs is yet to be implemented" << eom;
576  throw 0;
577  }
578 
579  source_locationt location=rhs.source_location();
580 
581  assert(rhs.operands().empty());
582 
583  if(rhs.type().id()!=ID_pointer)
584  {
586  error() << "do_java_new returns pointer" << eom;
587  throw 0;
588  }
589 
590  typet object_type=rhs.type().subtype();
591 
592  // build size expression
593  exprt object_size=size_of_expr(object_type, ns);
594 
595  if(object_size.is_nil())
596  {
598  error() << "do_java_new got nil object_size" << eom;
599  throw 0;
600  }
601 
602  // we produce a malloc side-effect, which stays
603  side_effect_exprt malloc_expr(ID_malloc);
604  malloc_expr.copy_to_operands(object_size);
605  malloc_expr.type()=rhs.type();
606 
608  t_n->code=code_assignt(lhs, malloc_expr);
609  t_n->source_location=location;
610 
611  // zero-initialize the object
612  dereference_exprt deref(lhs, object_type);
613  exprt zero_object=
614  zero_initializer(object_type, location, ns, get_message_handler());
616  to_struct_expr(zero_object), ns, to_symbol_type(object_type));
618  t_i->code=code_assignt(deref, zero_object);
619  t_i->source_location=location;
620 }
621 
623  const exprt &lhs,
624  const side_effect_exprt &rhs,
625  goto_programt &dest)
626 {
627  if(lhs.is_nil())
628  {
630  error() << "do_java_new_array without lhs is yet to be implemented"
631  << eom;
632  throw 0;
633  }
634 
635  source_locationt location=rhs.source_location();
636 
637  assert(rhs.operands().size()>=1); // one per dimension
638 
639  if(rhs.type().id()!=ID_pointer)
640  {
642  error() << "do_java_new_array returns pointer" << eom;
643  throw 0;
644  }
645 
646  typet object_type=rhs.type().subtype();
647 
648  // build size expression
649  exprt object_size=size_of_expr(object_type, ns);
650 
651  if(object_size.is_nil())
652  {
654  error() << "do_java_new_array got nil object_size" << eom;
655  throw 0;
656  }
657 
658  // we produce a malloc side-effect, which stays
659  side_effect_exprt malloc_expr(ID_malloc);
660  malloc_expr.copy_to_operands(object_size);
661  malloc_expr.type()=rhs.type();
662 
664  t_n->code=code_assignt(lhs, malloc_expr);
665  t_n->source_location=location;
666 
667  // multi-dimensional?
668 
669  assert(ns.follow(object_type).id()==ID_struct);
670  const struct_typet &struct_type=to_struct_type(ns.follow(object_type));
671  assert(struct_type.components().size()==3);
672 
673  // if it's an array, we need to set the length field
674  dereference_exprt deref(lhs, object_type);
675  member_exprt length(
676  deref,
677  struct_type.components()[1].get_name(),
678  struct_type.components()[1].type());
680  t_s->code=code_assignt(length, rhs.op0());
681  t_s->source_location=location;
682 
683  // we also need to allocate space for the data
685  deref,
686  struct_type.components()[2].get_name(),
687  struct_type.components()[2].type());
688  side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, data.type());
689 
690  // The instruction may specify a (hopefully small) upper bound on the
691  // array size, in which case we allocate a fixed-length array that may
692  // be larger than the `length` member rather than use a true variable-
693  // length array, which produces a more complex formula in the current
694  // backend.
695  const irept size_bound=rhs.find(ID_length_upper_bound);
696  if(size_bound.is_nil())
697  data_cpp_new_expr.set(ID_size, rhs.op0());
698  else
699  data_cpp_new_expr.set(ID_size, size_bound);
701  t_p->code=code_assignt(data, data_cpp_new_expr);
702  t_p->source_location=location;
703 
704  // zero-initialize the data
705  exprt zero_element=
707  data.type().subtype(),
708  location,
709  ns,
711  codet array_set(ID_array_set);
712  array_set.copy_to_operands(data, zero_element);
714  t_d->code=array_set;
715  t_d->source_location=location;
716 
717  if(rhs.operands().size()>=2)
718  {
719  // produce
720  // for(int i=0; i<size; i++) tmp[i]=java_new(dim-1);
721  // This will be converted recursively.
722 
723  goto_programt tmp;
724 
725  symbol_exprt tmp_i=
726  new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
727 
728  code_fort for_loop;
729 
730  side_effect_exprt sub_java_new=rhs;
731  sub_java_new.operands().erase(sub_java_new.operands().begin());
732 
733  assert(rhs.type().id()==ID_pointer);
734  typet sub_type=
735  static_cast<const typet &>(rhs.type().subtype().find("#element_type"));
736  assert(sub_type.id()==ID_pointer);
737  sub_java_new.type()=sub_type;
738 
739  side_effect_exprt inc(ID_assign);
740  inc.operands().resize(2);
741  inc.op0()=tmp_i;
742  inc.op1()=plus_exprt(tmp_i, from_integer(1, tmp_i.type()));
743 
744  dereference_exprt deref_expr(
745  plus_exprt(data, tmp_i), data.type().subtype());
746 
747  code_blockt for_body;
748  symbol_exprt init_sym=
749  new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr();
750 
751  code_assignt init_subarray(init_sym, sub_java_new);
752  code_assignt assign_subarray(
753  deref_expr,
754  typecast_exprt(init_sym, deref_expr.type()));
755  for_body.move_to_operands(init_subarray);
756  for_body.move_to_operands(assign_subarray);
757 
758  for_loop.init()=code_assignt(tmp_i, from_integer(0, tmp_i.type()));
759  for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0());
760  for_loop.iter()=inc;
761  for_loop.body()=for_body;
762 
763  convert(for_loop, tmp);
764  dest.destructive_append(tmp);
765  }
766 }
767 
770  const exprt &lhs,
771  const side_effect_exprt &rhs,
772  goto_programt &dest)
773 {
774  exprt initializer=
775  static_cast<const exprt &>(rhs.find(ID_initializer));
776 
777  if(initializer.is_not_nil())
778  {
779  if(rhs.get_statement()=="cpp_new[]")
780  {
781  // build loop
782  }
783  else if(rhs.get_statement()==ID_cpp_new)
784  {
785  // just one object
786  exprt deref_lhs(ID_dereference, rhs.type().subtype());
787  deref_lhs.copy_to_operands(lhs);
788 
789  replace_new_object(deref_lhs, initializer);
790  convert(to_code(initializer), dest);
791  }
792  else
793  assert(false);
794  }
795 }
796 
798 {
799  if(src.id()==ID_typecast)
800  {
801  assert(src.operands().size()==1);
802  return get_array_argument(src.op0());
803  }
804 
805  if(src.id()!=ID_address_of)
806  {
808  error() << "expected array-pointer as argument" << eom;
809  throw 0;
810  }
811 
812  assert(src.operands().size()==1);
813 
814  if(src.op0().id()!=ID_index)
815  {
817  error() << "expected array-element as argument" << eom;
818  throw 0;
819  }
820 
821  assert(src.op0().operands().size()==2);
822 
823  if(ns.follow(src.op0().op0().type()).id()!=ID_array)
824  {
826  error() << "expected array as argument" << eom;
827  throw 0;
828  }
829 
830  return src.op0().op0();
831 }
832 
834  const irep_idt &id,
835  const exprt &lhs,
836  const exprt &function,
837  const exprt::operandst &arguments,
838  goto_programt &dest)
839 {
840  if(arguments.size()!=2)
841  {
842  error().source_location=function.find_source_location();
843  error() << id << " expects two arguments" << eom;
844  throw 0;
845  }
846 
847  codet array_op_statement;
848  array_op_statement.set_statement(id);
849  array_op_statement.operands()=arguments;
850  array_op_statement.add_source_location()=function.source_location();
851 
852  copy(array_op_statement, OTHER, dest);
853 }
854 
856  const exprt &lhs,
857  const exprt &function,
858  const exprt::operandst &arguments,
859  goto_programt &dest)
860 {
861  if(arguments.size()!=2)
862  {
863  error().source_location=function.find_source_location();
864  error() << "array_equal expects two arguments" << eom;
865  throw 0;
866  }
867 
868  const typet &arg0_type=ns.follow(arguments[0].type());
869  const typet &arg1_type=ns.follow(arguments[1].type());
870 
871  if(arg0_type.id()!=ID_pointer ||
872  arg1_type.id()!=ID_pointer)
873  {
874  error().source_location=function.find_source_location();
875  error() << "array_equal expects pointer arguments" << eom;
876  throw 0;
877  }
878 
879  if(lhs.is_not_nil())
880  {
881  code_assignt assignment;
882 
883  // add dereferencing here
884  dereference_exprt lhs_array, rhs_array;
885  lhs_array.op0()=arguments[0];
886  rhs_array.op0()=arguments[1];
887  lhs_array.type()=arg0_type.subtype();
888  rhs_array.type()=arg1_type.subtype();
889 
890  assignment.lhs()=lhs;
891  assignment.rhs()=binary_exprt(
892  lhs_array, ID_array_equal, rhs_array, lhs.type());
893  assignment.add_source_location()=function.source_location();
894 
895  convert(assignment, dest);
896  }
897 }
898 
899 bool is_lvalue(const exprt &expr)
900 {
901  if(expr.id()==ID_index)
902  return is_lvalue(to_index_expr(expr).op0());
903  else if(expr.id()==ID_member)
904  return is_lvalue(to_member_expr(expr).op0());
905  else if(expr.id()==ID_dereference)
906  return true;
907  else if(expr.id()==ID_symbol)
908  return true;
909  else
910  return false;
911 }
912 
914 {
915  // we first strip any typecast
916  if(expr.id()==ID_typecast)
917  return make_va_list(to_typecast_expr(expr).op());
918 
919  // if it's an address of an lvalue, we take that
920  if(expr.id()==ID_address_of &&
921  expr.operands().size()==1 &&
922  is_lvalue(expr.op0()))
923  return expr.op0();
924 
925  return expr;
926 }
927 
930  const exprt &lhs,
931  const symbol_exprt &function,
932  const exprt::operandst &arguments,
933  goto_programt &dest)
934 {
935  if(function.get_bool("#invalid_object"))
936  return; // ignore
937 
938  // lookup symbol
939  const irep_idt &identifier=function.get_identifier();
940 
941  const symbolt *symbol;
942  if(ns.lookup(identifier, symbol))
943  {
944  error().source_location=function.find_source_location();
945  error() << "error: function `" << identifier << "' not found"
946  << eom;
947  throw 0;
948  }
949 
950  if(symbol->type.id()!=ID_code)
951  {
952  error().source_location=function.find_source_location();
953  error() << "error: function `" << identifier
954  << "' type mismatch: expected code" << eom;
955  throw 0;
956  }
957 
958  if(identifier==CPROVER_PREFIX "assume" ||
959  identifier=="__VERIFIER_assume")
960  {
961  if(arguments.size()!=1)
962  {
963  error().source_location=function.find_source_location();
964  error() << "`" << identifier << "' expected to have one argument"
965  << eom;
966  throw 0;
967  }
968 
970  t->guard=arguments.front();
971  t->source_location=function.source_location();
972  t->source_location.set("user-provided", true);
973 
974  // let's double-check the type of the argument
975  if(t->guard.type().id()!=ID_bool)
976  t->guard.make_typecast(bool_typet());
977 
978  if(lhs.is_not_nil())
979  {
980  error().source_location=function.find_source_location();
981  error() << identifier << " expected not to have LHS" << eom;
982  throw 0;
983  }
984  }
985  else if(identifier=="__VERIFIER_error")
986  {
987  if(!arguments.empty())
988  {
989  error().source_location=function.find_source_location();
990  error() << "`" << identifier << "' expected to have no arguments"
991  << eom;
992  throw 0;
993  }
994 
996  t->guard=false_exprt();
997  t->source_location=function.source_location();
998  t->source_location.set("user-provided", true);
999  t->source_location.set_property_class(ID_assertion);
1000 
1001  if(lhs.is_not_nil())
1002  {
1003  error().source_location=function.find_source_location();
1004  error() << identifier << " expected not to have LHS" << eom;
1005  throw 0;
1006  }
1007 
1008  // __VERIFIER_error has abort() semantics, even if no assertions
1009  // are being checked
1011  a->guard=false_exprt();
1012  a->source_location=function.source_location();
1013  a->source_location.set("user-provided", true);
1014  }
1015  else if(has_prefix(
1016  id2string(identifier), "java::java.lang.AssertionError.<init>:"))
1017  {
1018  // insert function call anyway
1019  code_function_callt function_call;
1020  function_call.lhs()=lhs;
1021  function_call.function()=function;
1022  function_call.arguments()=arguments;
1023  function_call.add_source_location()=function.source_location();
1024 
1025  copy(function_call, FUNCTION_CALL, dest);
1026 
1027  if(arguments.size()!=1 && arguments.size()!=2)
1028  {
1029  error().source_location=function.find_source_location();
1030  error() << "`" << identifier
1031  << "' expected to have one or two arguments" << eom;
1032  throw 0;
1033  }
1034 
1036  t->guard=false_exprt();
1037  t->source_location=function.source_location();
1038  t->source_location.set("user-provided", true);
1039  t->source_location.set_property_class(ID_assertion);
1040  t->source_location.set_comment(
1041  "assertion at "+function.source_location().as_string());
1042  }
1043  else if(identifier=="assert" &&
1044  !ns.lookup(identifier).location.get_function().empty())
1045  {
1046  if(arguments.size()!=1)
1047  {
1048  error().source_location=function.find_source_location();
1049  error() << "`" << identifier << "' expected to have one argument"
1050  << eom;
1051  throw 0;
1052  }
1053 
1055  t->guard=arguments.front();
1056  t->source_location=function.source_location();
1057  t->source_location.set("user-provided", true);
1058  t->source_location.set_property_class(ID_assertion);
1059  t->source_location.set_comment(
1060  "assertion "+id2string(from_expr(ns, "", t->guard)));
1061 
1062  // let's double-check the type of the argument
1063  if(t->guard.type().id()!=ID_bool)
1064  t->guard.make_typecast(bool_typet());
1065 
1066  if(lhs.is_not_nil())
1067  {
1068  error().source_location=function.find_source_location();
1069  error() << identifier << " expected not to have LHS" << eom;
1070  throw 0;
1071  }
1072  }
1073  else if(identifier==CPROVER_PREFIX "assert")
1074  {
1075  if(arguments.size()!=2)
1076  {
1077  error().source_location=function.find_source_location();
1078  error() << "`" << identifier << "' expected to have two arguments"
1079  << eom;
1080  throw 0;
1081  }
1082 
1083  const irep_idt description=
1084  get_string_constant(arguments[1]);
1085 
1087  t->guard=arguments[0];
1088  t->source_location=function.source_location();
1089  t->source_location.set(
1090  "user-provided",
1091  !function.source_location().is_built_in());
1092  t->source_location.set_property_class(ID_assertion);
1093  t->source_location.set_comment(description);
1094 
1095  // let's double-check the type of the argument
1096  if(t->guard.type().id()!=ID_bool)
1097  t->guard.make_typecast(bool_typet());
1098 
1099  if(lhs.is_not_nil())
1100  {
1101  error().source_location=function.find_source_location();
1102  error() << identifier << " expected not to have LHS" << eom;
1103  throw 0;
1104  }
1105  }
1106  else if(identifier==CPROVER_PREFIX "printf")
1107  {
1108  do_printf(lhs, function, arguments, dest);
1109  }
1110  else if(identifier==CPROVER_PREFIX "scanf")
1111  {
1112  do_scanf(lhs, function, arguments, dest);
1113  }
1114  else if(identifier==CPROVER_PREFIX "input" ||
1115  identifier=="__CPROVER::input")
1116  {
1117  do_input(lhs, function, arguments, dest);
1118  }
1119  else if(identifier==CPROVER_PREFIX "output" ||
1120  identifier=="__CPROVER::output")
1121  {
1122  do_output(lhs, function, arguments, dest);
1123  }
1124  else if(identifier==CPROVER_PREFIX "atomic_begin" ||
1125  identifier=="__CPROVER::atomic_begin" ||
1126  identifier=="__VERIFIER_atomic_begin")
1127  {
1128  do_atomic_begin(lhs, function, arguments, dest);
1129  }
1130  else if(identifier==CPROVER_PREFIX "atomic_end" ||
1131  identifier=="__CPROVER::atomic_end" ||
1132  identifier=="__VERIFIER_atomic_end")
1133  {
1134  do_atomic_end(lhs, function, arguments, dest);
1135  }
1136  else if(identifier==CPROVER_PREFIX "prob_biased_coin")
1137  {
1138  do_prob_coin(lhs, function, arguments, dest);
1139  }
1140  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "prob_uniform_"))
1141  {
1142  do_prob_uniform(lhs, function, arguments, dest);
1143  }
1144  else if(has_prefix(id2string(identifier), "nondet_") ||
1145  has_prefix(id2string(identifier), "__VERIFIER_nondet_"))
1146  {
1147  // make it a side effect if there is an LHS
1148  if(lhs.is_nil())
1149  return;
1150 
1151  exprt rhs;
1152 
1153  // We need to special-case for _Bool, which
1154  // can only be 0 or 1.
1155  if(lhs.type().id()==ID_c_bool)
1156  {
1158  rhs.add_source_location()=function.source_location();
1159  rhs.set(ID_C_identifier, identifier);
1160  rhs=typecast_exprt(rhs, lhs.type());
1161  }
1162  else
1163  {
1164  rhs=side_effect_expr_nondett(lhs.type());
1165  rhs.add_source_location()=function.source_location();
1166  rhs.set(ID_C_identifier, identifier);
1167  }
1168 
1169  code_assignt assignment(lhs, rhs);
1170  assignment.add_source_location()=function.source_location();
1171  copy(assignment, ASSIGN, dest);
1172  }
1173  else if(has_prefix(id2string(identifier), CPROVER_PREFIX "uninterpreted_"))
1174  {
1175  // make it a side effect if there is an LHS
1176  if(lhs.is_nil())
1177  return;
1178 
1180  rhs.type()=lhs.type();
1181  rhs.add_source_location()=function.source_location();
1182  rhs.function()=function;
1183  rhs.arguments()=arguments;
1184 
1185  code_assignt assignment(lhs, rhs);
1186  assignment.add_source_location()=function.source_location();
1187  copy(assignment, ASSIGN, dest);
1188  }
1189  else if(identifier==CPROVER_PREFIX "array_equal")
1190  {
1191  do_array_equal(lhs, function, arguments, dest);
1192  }
1193  else if(identifier==CPROVER_PREFIX "array_set")
1194  {
1195  do_array_op(ID_array_set, lhs, function, arguments, dest);
1196  }
1197  else if(identifier==CPROVER_PREFIX "array_copy")
1198  {
1199  do_array_op(ID_array_copy, lhs, function, arguments, dest);
1200  }
1201  else if(identifier==CPROVER_PREFIX "array_replace")
1202  {
1203  do_array_op(ID_array_replace, lhs, function, arguments, dest);
1204  }
1205  else if(identifier=="printf")
1206  /*
1207  identifier=="fprintf" ||
1208  identifier=="sprintf" ||
1209  identifier=="snprintf")
1210  */
1211  {
1212  do_printf(lhs, function, arguments, dest);
1213  }
1214  else if(identifier=="__assert_fail" ||
1215  identifier=="_assert" ||
1216  identifier=="__assert_c99" ||
1217  identifier=="_wassert")
1218  {
1219  // __assert_fail is Linux
1220  // These take four arguments:
1221  // "expression", "file.c", line, __func__
1222  // klibc has __assert_fail with 3 arguments
1223  // "expression", "file.c", line
1224 
1225  // MingW has
1226  // void _assert (const char*, const char*, int);
1227  // with three arguments:
1228  // "expression", "file.c", line
1229 
1230  // This has been seen in Solaris 11.
1231  // Signature:
1232  // void __assert_c99(
1233  // const char *desc, const char *file, int line, const char *func);
1234 
1235  // _wassert is Windows. The arguments are
1236  // L"expression", L"file.c", line
1237 
1238  if(arguments.size()!=4 &&
1239  arguments.size()!=3)
1240  {
1241  error().source_location=function.find_source_location();
1242  error() << "`" << identifier << "' expected to have four arguments"
1243  << eom;
1244  throw 0;
1245  }
1246 
1247  const irep_idt description=
1248  "assertion "+id2string(get_string_constant(arguments[0]));
1249 
1251  t->guard=false_exprt();
1252  t->source_location=function.source_location();
1253  t->source_location.set("user-provided", true);
1254  t->source_location.set_property_class(ID_assertion);
1255  t->source_location.set_comment(description);
1256  // we ignore any LHS
1257  }
1258  else if(identifier=="__assert_rtn" ||
1259  identifier=="__assert")
1260  {
1261  // __assert_rtn has been seen on MacOS;
1262  // __assert is FreeBSD and Solaris 11.
1263  // These take four arguments:
1264  // __func__, "file.c", line, "expression"
1265  // On Solaris 11, it's three arguments:
1266  // "expression", "file", line
1267 
1268  irep_idt description;
1269 
1270  if(arguments.size()==4)
1271  {
1272  description=
1273  "assertion "+id2string(get_string_constant(arguments[3]));
1274  }
1275  else if(arguments.size()==3)
1276  {
1277  description=
1278  "assertion "+id2string(get_string_constant(arguments[1]));
1279  }
1280  else
1281  {
1282  error().source_location=function.find_source_location();
1283  error() << "`" << identifier << "' expected to have four arguments"
1284  << eom;
1285  throw 0;
1286  }
1287 
1289  t->guard=false_exprt();
1290  t->source_location=function.source_location();
1291  t->source_location.set("user-provided", true);
1292  t->source_location.set_property_class(ID_assertion);
1293  t->source_location.set_comment(description);
1294  // we ignore any LHS
1295  }
1296  else if(identifier=="__assert_func")
1297  {
1298  // __assert_func is newlib (used by, e.g., cygwin)
1299  // These take four arguments:
1300  // "file.c", line, __func__, "expression"
1301  if(arguments.size()!=4)
1302  {
1303  error().source_location=function.find_source_location();
1304  error() << "`" << identifier << "' expected to have four arguments"
1305  << eom;
1306  throw 0;
1307  }
1308 
1309  irep_idt description;
1310  try
1311  {
1312  description="assertion "+id2string(get_string_constant(arguments[3]));
1313  }
1314  catch(int)
1315  {
1316  // we might be building newlib, where __assert_func is passed
1317  // a pointer-typed symbol; the warning will still have been
1318  // printed
1319  description="assertion";
1320  }
1321 
1323  t->guard=false_exprt();
1324  t->source_location=function.source_location();
1325  t->source_location.set("user-provided", true);
1326  t->source_location.set_property_class(ID_assertion);
1327  t->source_location.set_comment(description);
1328  // we ignore any LHS
1329  }
1330  else if(identifier==CPROVER_PREFIX "fence")
1331  {
1332  if(arguments.empty())
1333  {
1334  error().source_location=function.find_source_location();
1335  error() << "`" << identifier
1336  << "' expected to have at least one argument" << eom;
1337  throw 0;
1338  }
1339 
1341  t->source_location=function.source_location();
1342  t->code.set(ID_statement, ID_fence);
1343 
1344  forall_expr(it, arguments)
1345  {
1346  const irep_idt kind=get_string_constant(*it);
1347  t->code.set(kind, true);
1348  }
1349  }
1350  else if(identifier=="__builtin_prefetch")
1351  {
1352  // does nothing
1353  }
1354  else if(identifier=="__builtin_unreachable")
1355  {
1356  // says something like assert(false);
1357  }
1358  else if(identifier==ID_gcc_builtin_va_arg)
1359  {
1360  // This does two things.
1361  // 1) Move list pointer to next argument.
1362  // Done by gcc_builtin_va_arg_next.
1363  // 2) Return value of argument.
1364  // This is just dereferencing.
1365 
1366  if(arguments.size()!=1)
1367  {
1368  error().source_location=function.find_source_location();
1369  error() << "`" << identifier << "' expected to have one argument"
1370  << eom;
1371  throw 0;
1372  }
1373 
1374  exprt list_arg=make_va_list(arguments[0]);
1375 
1376  {
1377  side_effect_exprt rhs(ID_gcc_builtin_va_arg_next, list_arg.type());
1378  rhs.copy_to_operands(list_arg);
1379  rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
1381  t1->source_location=function.source_location();
1382  t1->code=code_assignt(list_arg, rhs);
1383  }
1384 
1385  if(lhs.is_not_nil())
1386  {
1387  typet t=pointer_type(lhs.type());
1388  dereference_exprt rhs(lhs.type());
1389  rhs.op0()=typecast_exprt(list_arg, t);
1390  rhs.add_source_location()=function.source_location();
1392  t2->source_location=function.source_location();
1393  t2->code=code_assignt(lhs, rhs);
1394  }
1395  }
1396  else if(identifier=="__builtin_va_copy")
1397  {
1398  if(arguments.size()!=2)
1399  {
1400  error().source_location=function.find_source_location();
1401  error() << "`" << identifier << "' expected to have two arguments"
1402  << eom;
1403  throw 0;
1404  }
1405 
1406  exprt dest_expr=make_va_list(arguments[0]);
1407  exprt src_expr=typecast_exprt(arguments[1], dest_expr.type());
1408 
1409  if(!is_lvalue(dest_expr))
1410  {
1412  error() << "va_copy argument expected to be lvalue" << eom;
1413  throw 0;
1414  }
1415 
1417  t->source_location=function.source_location();
1418  t->code=code_assignt(dest_expr, src_expr);
1419  }
1420  else if(identifier=="__builtin_va_start")
1421  {
1422  // Set the list argument to be the address of the
1423  // parameter argument.
1424  if(arguments.size()!=2)
1425  {
1426  error().source_location=function.find_source_location();
1427  error() << "`" << identifier << "' expected to have two arguments"
1428  << eom;
1429  throw 0;
1430  }
1431 
1432  exprt dest_expr=make_va_list(arguments[0]);
1433  exprt src_expr=typecast_exprt(
1434  address_of_exprt(arguments[1]), dest_expr.type());
1435 
1436  if(!is_lvalue(dest_expr))
1437  {
1439  error() << "va_start argument expected to be lvalue" << eom;
1440  throw 0;
1441  }
1442 
1444  t->source_location=function.source_location();
1445  t->code=code_assignt(dest_expr, src_expr);
1446  }
1447  else if(identifier=="__builtin_va_end")
1448  {
1449  // Invalidates the argument. We do so by setting it to NULL.
1450  if(arguments.size()!=1)
1451  {
1452  error().source_location=function.find_source_location();
1453  error() << "`" << identifier << "' expected to have one argument"
1454  << eom;
1455  throw 0;
1456  }
1457 
1458  exprt dest_expr=make_va_list(arguments[0]);
1459 
1460  if(!is_lvalue(dest_expr))
1461  {
1463  error() << "va_end argument expected to be lvalue" << eom;
1464  throw 0;
1465  }
1466 
1467  // our __builtin_va_list is a pointer
1468  if(ns.follow(dest_expr.type()).id()==ID_pointer)
1469  {
1471  t->source_location=function.source_location();
1472  exprt zero=
1474  dest_expr.type(),
1475  function.source_location(),
1476  ns,
1478  t->code=code_assignt(dest_expr, zero);
1479  }
1480  }
1481  else if(identifier=="__sync_fetch_and_add" ||
1482  identifier=="__sync_fetch_and_sub" ||
1483  identifier=="__sync_fetch_and_or" ||
1484  identifier=="__sync_fetch_and_and" ||
1485  identifier=="__sync_fetch_and_xor" ||
1486  identifier=="__sync_fetch_and_nand")
1487  {
1488  // type __sync_fetch_and_OP(type *ptr, type value, ...)
1489  // { tmp = *ptr; *ptr OP= value; return tmp; }
1490 
1491  if(arguments.size()<2)
1492  {
1493  error().source_location=function.find_source_location();
1494  error() << "`" << identifier
1495  << "' expected to have at least two arguments" << eom;
1496  throw 0;
1497  }
1498 
1499  if(arguments[0].type().id()!=ID_pointer)
1500  {
1501  error().source_location=function.find_source_location();
1502  error() << "`" << identifier << "' expected to have pointer argument"
1503  << eom;
1504  throw 0;
1505  }
1506 
1507  // build *ptr
1508  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1509 
1511  t1->source_location=function.source_location();
1512 
1513  if(lhs.is_not_nil())
1514  {
1515  // return *ptr
1517  t2->source_location=function.source_location();
1518  t2->code=code_assignt(lhs, deref_ptr);
1519  if(t2->code.op0().type()!=t2->code.op1().type())
1520  t2->code.op1().make_typecast(t2->code.op0().type());
1521  }
1522 
1523  irep_idt op_id=
1524  identifier=="__sync_fetch_and_add"?ID_plus:
1525  identifier=="__sync_fetch_and_sub"?ID_minus:
1526  identifier=="__sync_fetch_and_or"?ID_bitor:
1527  identifier=="__sync_fetch_and_and"?ID_bitand:
1528  identifier=="__sync_fetch_and_xor"?ID_bitxor:
1529  identifier=="__sync_fetch_and_nand"?ID_bitnand:
1530  ID_nil;
1531 
1532  // build *ptr=*ptr OP arguments[1];
1533  binary_exprt op_expr(deref_ptr, op_id, arguments[1], deref_ptr.type());
1534  if(op_expr.op1().type()!=op_expr.type())
1535  op_expr.op1().make_typecast(op_expr.type());
1536 
1538  t3->source_location=function.source_location();
1539  t3->code=code_assignt(deref_ptr, op_expr);
1540 
1541  // this instruction implies an mfence, i.e., WRfence
1543  t4->source_location=function.source_location();
1544  t4->code=codet(ID_fence);
1545  t4->code.set(ID_WRfence, true);
1546 
1548  t5->source_location=function.source_location();
1549  }
1550  else if(identifier=="__sync_add_and_fetch" ||
1551  identifier=="__sync_sub_and_fetch" ||
1552  identifier=="__sync_or_and_fetch" ||
1553  identifier=="__sync_and_and_fetch" ||
1554  identifier=="__sync_xor_and_fetch" ||
1555  identifier=="__sync_nand_and_fetch")
1556  {
1557  // type __sync_OP_and_fetch (type *ptr, type value, ...)
1558  // { *ptr OP= value; return *ptr; }
1559 
1560  if(arguments.size()<2)
1561  {
1562  error().source_location=function.find_source_location();
1563  error() << "`" << identifier
1564  << "' expected to have at least two arguments" << eom;
1565  throw 0;
1566  }
1567 
1568  if(arguments[0].type().id()!=ID_pointer)
1569  {
1570  error().source_location=function.find_source_location();
1571  error() << "`" << identifier
1572  << "' expected to have pointer argument" << eom;
1573  throw 0;
1574  }
1575 
1576  // build *ptr
1577  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1578 
1580  t1->source_location=function.source_location();
1581 
1582  irep_idt op_id=
1583  identifier=="__sync_add_and_fetch"?ID_plus:
1584  identifier=="__sync_sub_and_fetch"?ID_minus:
1585  identifier=="__sync_or_and_fetch"?ID_bitor:
1586  identifier=="__sync_and_and_fetch"?ID_bitand:
1587  identifier=="__sync_xor_and_fetch"?ID_bitxor:
1588  identifier=="__sync_nand_and_fetch"?ID_bitnand:
1589  ID_nil;
1590 
1591  // build *ptr=*ptr OP arguments[1];
1592  binary_exprt op_expr(deref_ptr, op_id, arguments[1], deref_ptr.type());
1593  if(op_expr.op1().type()!=op_expr.type())
1594  op_expr.op1().make_typecast(op_expr.type());
1595 
1597  t3->source_location=function.source_location();
1598  t3->code=code_assignt(deref_ptr, op_expr);
1599 
1600  if(lhs.is_not_nil())
1601  {
1602  // return *ptr
1604  t2->source_location=function.source_location();
1605  t2->code=code_assignt(lhs, deref_ptr);
1606  if(t2->code.op0().type()!=t2->code.op1().type())
1607  t2->code.op1().make_typecast(t2->code.op0().type());
1608  }
1609 
1610  // this instruction implies an mfence, i.e., WRfence
1612  t4->source_location=function.source_location();
1613  t4->code=codet(ID_fence);
1614  t4->code.set(ID_WRfence, true);
1615 
1617  t5->source_location=function.source_location();
1618  }
1619  else if(identifier=="__sync_bool_compare_and_swap")
1620  {
1621  // These builtins perform an atomic compare and swap. That is, if the
1622  // current value of *ptr is oldval, then write newval into *ptr. The
1623  // "bool" version returns true if the comparison is successful and
1624  // newval was written. The "val" version returns the contents of *ptr
1625  // before the operation.
1626 
1627  // These are type-polymorphic, which makes it hard to put
1628  // them into ansi-c/library.
1629 
1630  // bool __sync_bool_compare_and_swap(
1631  // type *ptr, type oldval, type newval, ...)
1632 
1633  if(arguments.size()<3)
1634  {
1635  error().source_location=function.find_source_location();
1636  error() << "`" << identifier
1637  << "' expected to have at least three arguments" << eom;
1638  throw 0;
1639  }
1640 
1641  if(arguments[0].type().id()!=ID_pointer)
1642  {
1643  error().source_location=function.find_source_location();
1644  error() << "`" << identifier
1645  << "' expected to have pointer argument" << eom;
1646  throw 0;
1647  }
1648 
1649  // build *ptr
1650  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1651 
1653  t1->source_location=function.source_location();
1654 
1655  // build *ptr==oldval
1656  equal_exprt equal(deref_ptr, arguments[1]);
1657  if(equal.op1().type()!=equal.op0().type())
1658  equal.op1().make_typecast(equal.op0().type());
1659 
1660  if(lhs.is_not_nil())
1661  {
1662  // return *ptr==oldval
1664  t2->source_location=function.source_location();
1665  t2->code=code_assignt(lhs, equal);
1666  if(t2->code.op0().type()!=t2->code.op1().type())
1667  t2->code.op1().make_typecast(t2->code.op0().type());
1668  }
1669 
1670  // build (*ptr==oldval)?newval:*ptr
1671  if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type());
1672  if(if_expr.op1().type()!=if_expr.type())
1673  if_expr.op1().make_typecast(if_expr.type());
1674 
1676  t3->source_location=function.source_location();
1677  t3->code=code_assignt(deref_ptr, if_expr);
1678 
1679  // this instruction implies an mfence, i.e., WRfence
1681  t4->source_location=function.source_location();
1682  t4->code=codet(ID_fence);
1683  t4->code.set(ID_WRfence, true);
1684 
1686  t5->source_location=function.source_location();
1687  }
1688  else if(identifier=="__sync_val_compare_and_swap")
1689  {
1690  // type __sync_val_compare_and_swap(
1691  // type *ptr, type oldval, type newval, ...)
1692  if(arguments.size()<3)
1693  {
1694  error().source_location=function.find_source_location();
1695  error() << "`" << identifier
1696  << "' expected to have at least three arguments" << eom;
1697  throw 0;
1698  }
1699 
1700  if(arguments[0].type().id()!=ID_pointer)
1701  {
1702  error().source_location=function.find_source_location();
1703  error() << "`" << identifier
1704  << "' expected to have pointer argument" << eom;
1705  throw 0;
1706  }
1707 
1708  // build *ptr
1709  dereference_exprt deref_ptr(arguments[0], arguments[0].type().subtype());
1710 
1712  t1->source_location=function.source_location();
1713 
1714  if(lhs.is_not_nil())
1715  {
1716  // return *ptr
1718  t2->source_location=function.source_location();
1719  t2->code=code_assignt(lhs, deref_ptr);
1720  if(t2->code.op0().type()!=t2->code.op1().type())
1721  t2->code.op1().make_typecast(t2->code.op0().type());
1722  }
1723 
1724  // build *ptr==oldval
1725  equal_exprt equal(deref_ptr, arguments[1]);
1726  if(equal.op1().type()!=equal.op0().type())
1727  equal.op1().make_typecast(equal.op0().type());
1728 
1729  // build (*ptr==oldval)?newval:*ptr
1730  if_exprt if_expr(equal, arguments[2], deref_ptr, deref_ptr.type());
1731  if(if_expr.op1().type()!=if_expr.type())
1732  if_expr.op1().make_typecast(if_expr.type());
1733 
1735  t3->source_location=function.source_location();
1736  t3->code=code_assignt(deref_ptr, if_expr);
1737 
1738  // this instruction implies an mfence, i.e., WRfence
1740  t4->source_location=function.source_location();
1741  t4->code=codet(ID_fence);
1742  t4->code.set(ID_WRfence, true);
1743 
1745  t5->source_location=function.source_location();
1746  }
1747  else if(identifier=="__sync_lock_test_and_set")
1748  {
1749  // type __sync_lock_test_and_set (type *ptr, type value, ...)
1750 
1751  // This builtin, as described by Intel, is not a traditional
1752  // test-and-set operation, but rather an atomic exchange operation.
1753  // It writes value into *ptr, and returns the previous contents of
1754  // *ptr. Many targets have only minimal support for such locks, and
1755  // do not support a full exchange operation. In this case, a target
1756  // may support reduced functionality here by which the only valid
1757  // value to store is the immediate constant 1. The exact value
1758  // actually stored in *ptr is implementation defined.
1759  }
1760  else if(identifier=="__sync_lock_release")
1761  {
1762  // This builtin is not a full barrier, but rather an acquire barrier.
1763  // This means that references after the builtin cannot move to (or be
1764  // speculated to) before the builtin, but previous memory stores may
1765  // not be globally visible yet, and previous memory loads may not yet
1766  // be satisfied.
1767 
1768  // void __sync_lock_release (type *ptr, ...)
1769  }
1770  else if(identifier=="__builtin_isgreater" ||
1771  identifier=="__builtin_isgreater" ||
1772  identifier=="__builtin_isgreaterequal" ||
1773  identifier=="__builtin_isless" ||
1774  identifier=="__builtin_islessequal" ||
1775  identifier=="__builtin_islessgreater" ||
1776  identifier=="__builtin_isunordered")
1777  {
1778  // these support two double or two float arguments; we call the
1779  // appropriate internal version
1780  if(arguments.size()!=2 ||
1781  (arguments[0].type()!=double_type() &&
1782  arguments[0].type()!=float_type()) ||
1783  (arguments[1].type()!=double_type() &&
1784  arguments[1].type()!=float_type()))
1785  {
1786  error().source_location=function.find_source_location();
1787  error() << "`" << identifier
1788  << "' expected to have two float/double arguments"
1789  << eom;
1790  throw 0;
1791  }
1792 
1793  exprt::operandst new_arguments=arguments;
1794 
1795  bool use_double=arguments[0].type()==double_type();
1796  if(arguments[0].type()!=arguments[1].type())
1797  {
1798  if(use_double)
1799  new_arguments[1].make_typecast(arguments[0].type());
1800  else
1801  {
1802  new_arguments[0].make_typecast(arguments[1].type());
1803  use_double=true;
1804  }
1805  }
1806 
1807  code_typet f_type=to_code_type(function.type());
1808  f_type.remove_ellipsis();
1809  const typet &a_t=new_arguments[0].type();
1810  f_type.parameters()=
1812 
1813  // replace __builtin_ by CPROVER_PREFIX
1814  std::string name=CPROVER_PREFIX+id2string(identifier).substr(10);
1815  // append d or f for double/float
1816  name+=use_double?'d':'f';
1817 
1818  symbol_exprt new_function=function;
1819  new_function.set_identifier(name);
1820  new_function.type()=f_type;
1821 
1822  code_function_callt function_call;
1823  function_call.lhs()=lhs;
1824  function_call.function()=new_function;
1825  function_call.arguments()=new_arguments;
1826  function_call.add_source_location()=function.source_location();
1827 
1828  if(!symbol_table.has_symbol(name))
1829  {
1830  code_typet();
1831  symbolt new_symbol;
1832  new_symbol.base_name=name;
1833  new_symbol.name=name;
1834  new_symbol.type=f_type;
1835  new_symbol.location=function.source_location();
1836  symbol_table.add(new_symbol);
1837  }
1838 
1839  copy(function_call, FUNCTION_CALL, dest);
1840  }
1841  else
1842  {
1843  do_function_call_symbol(*symbol);
1844 
1845  // insert function call
1846  code_function_callt function_call;
1847  function_call.lhs()=lhs;
1848  function_call.function()=function;
1849  function_call.arguments()=arguments;
1850  function_call.add_source_location()=function.source_location();
1851 
1852  copy(function_call, FUNCTION_CALL, dest);
1853  }
1854 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
exprt size_of_expr(const typet &type, const namespacet &ns)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
semantic type conversion
Definition: std_expr.h:1725
constant_exprt from_rational(const rationalt &a)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
BigInt mp_integer
Definition: mp_arith.h:19
Linking: Zero Initialization.
targett add_instruction()
Adds an instruction at the end.
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert(const codet &code, goto_programt &dest)
converts &#39;code&#39; and appends the result to &#39;dest&#39;
bool is_not_nil() const
Definition: irep.h:104
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:296
const exprt & init() const
Definition: std_code.h:556
symbol_tablet & symbol_table
application of (mathematical) function
Definition: std_expr.h:3785
Symbol table entry.
format_token_listt parse_format_string(const std::string &arg_string)
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
void do_input(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const codet & body() const
Definition: std_code.h:586
bool is_lvalue(const exprt &expr)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
#define forall_expr(it, expr)
Definition: expr.h:28
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< componentt > componentst
Definition: std_types.h:240
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3302
std::vector< parametert > parameterst
Definition: std_types.h:829
argumentst & arguments()
Definition: std_expr.h:3805
Format String Parser.
const componentst & components() const
Definition: std_types.h:242
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
void do_atomic_begin(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_array_equal(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1487
The trinary if-then-else operator.
Definition: std_expr.h:2771
bitvector_typet double_type()
Definition: c_types.cpp:203
typet & type()
Definition: expr.h:60
unsignedbv_typet size_type()
Definition: c_types.cpp:57
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
A constant literal expression.
Definition: std_expr.h:3685
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Structure type.
Definition: std_types.h:296
exprt & op()
Definition: std_expr.h:1739
typet get_type(const format_tokent &token)
Extract member of struct or union.
Definition: std_expr.h:3214
TO_BE_DOCUMENTED.
Definition: std_types.h:1490
equality
Definition: std_expr.h:1082
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1229
const char * as_string(coverage_criteriont c)
Definition: cover.cpp:71
exprt make_va_list(const exprt &expr)
exprt object_size(const exprt &pointer)
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
exprt & lhs()
Definition: std_code.h:157
void do_java_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
irep_idt get_string_constant(const exprt &expr)
argumentst & arguments()
Definition: std_code.h:689
virtual void do_cpp_new(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
void remove_ellipsis()
Definition: std_types.h:824
A reference into the symbol table.
Definition: std_types.h:109
A generic base class for binary expressions.
Definition: std_expr.h:471
bitvector_typet float_type()
Definition: c_types.cpp:184
exprt & rhs()
Definition: std_code.h:162
const source_locationt & find_source_location() const
Definition: expr.cpp:466
const exprt & cond() const
Definition: std_code.h:566
source_locationt source_location
Definition: message.h:175
Operator to dereference a pointer.
Definition: std_expr.h:2701
Program Transformation.
API to expression classes.
void do_prob_coin(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void do_prob_uniform(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1037
const exprt & size() const
Definition: std_types.h:915
Base class for tree-like data structures with sharing.
Definition: irep.h:87
A function call.
Definition: std_code.h:657
The plus expression.
Definition: std_expr.h:702
bitvector_typet index_type()
Definition: c_types.cpp:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void do_java_new_array(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
Operator to return the address of an object.
Definition: std_expr.h:2593
void clean_expr(exprt &expr, goto_programt &dest, bool result_is_used=true)
Various predicates over pointers in programs.
exprt get_array_argument(const exprt &src)
The boolean constant false.
Definition: std_expr.h:3753
void do_array_op(const irep_idt &id, const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
Pointer Logic.
void do_printf(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const source_locationt & source_location() const
Definition: type.h:95
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
message_handlert & get_message_handler()
Definition: message.h:127
void do_scanf(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void do_output(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
void cpp_new_initializer(const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest)
builds a goto program for object initialization after new
exprt & function()
Definition: std_code.h:677
void set_statement(const irep_idt &statement)
Definition: std_code.h:32
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
symbolt & new_tmp_symbol(const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &)
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const source_locationt & source_location() const
Definition: expr.h:142
const exprt & iter() const
Definition: std_code.h:576
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
void copy(const codet &code, goto_program_instruction_typet type, goto_programt &dest)
A statement in a programming language.
Definition: std_code.h:19
A `for&#39; instruction.
Definition: std_code.h:547
const typet & subtype() const
Definition: type.h:31
An expression containing a side effect.
Definition: std_code.h:997
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1464
void make_typecast(const typet &_type)
Definition: expr.cpp:90
static void replace_new_object(const exprt &object, exprt &dest)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
void do_atomic_end(const exprt &lhs, const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest)
const typet & return_type() const
Definition: std_types.h:831
const irep_idt & get_identifier() const
Definition: std_types.h:126
Assignment.
Definition: std_code.h:144
Definition: kdev_t.h:24
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
const irep_idt & get_statement() const
Definition: std_code.h:1012
array index operator
Definition: std_expr.h:1170