cprover
c_typecheck_gcc_polymorphic_builtins.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: ANSI-C Language Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "c_typecheck_base.h"
13 
14 #include <util/arith_tools.h>
15 #include <util/c_types.h>
16 #include <util/cprover_prefix.h>
17 #include <util/pointer_expr.h>
18 #include <util/std_types.h>
19 #include <util/string_constant.h>
20 
21 #include <atomic>
22 
23 #include "c_expr.h"
24 
26  const irep_idt &identifier,
27  const exprt::operandst &arguments,
28  const source_locationt &source_location,
29  message_handlert &message_handler)
30 {
31  messaget log(message_handler);
32 
33  // adjust return type of function to match pointer subtype
34  if(arguments.size() < 2)
35  {
36  log.error().source_location = source_location;
37  log.error() << identifier << " expects at least two arguments"
38  << messaget::eom;
39  throw 0;
40  }
41 
42  const exprt &ptr_arg = arguments.front();
43 
44  if(ptr_arg.type().id() != ID_pointer)
45  {
46  log.error().source_location = source_location;
47  log.error() << identifier << " takes a pointer as first argument"
48  << messaget::eom;
49  throw 0;
50  }
51 
53  code_typet::parametert(ptr_arg.type().subtype())},
54  ptr_arg.type().subtype()};
55  t.make_ellipsis();
56  symbol_exprt result{identifier, std::move(t)};
57  result.add_source_location() = source_location;
58 
59  return result;
60 }
61 
63  const irep_idt &identifier,
64  const exprt::operandst &arguments,
65  const source_locationt &source_location,
66  message_handlert &message_handler)
67 {
68  messaget log(message_handler);
69 
70  // adjust return type of function to match pointer subtype
71  if(arguments.size() < 3)
72  {
73  log.error().source_location = source_location;
74  log.error() << identifier << " expects at least three arguments"
75  << messaget::eom;
76  throw 0;
77  }
78 
79  const exprt &ptr_arg = arguments.front();
80 
81  if(ptr_arg.type().id() != ID_pointer)
82  {
83  log.error().source_location = source_location;
84  log.error() << identifier << " takes a pointer as first argument"
85  << messaget::eom;
86  throw 0;
87  }
88 
89  const typet &subtype = ptr_arg.type().subtype();
90  typet sync_return_type = subtype;
91  if(identifier == ID___sync_bool_compare_and_swap)
92  sync_return_type = c_bool_type();
93 
95  code_typet::parametert(subtype),
96  code_typet::parametert(subtype)},
97  sync_return_type};
98  t.make_ellipsis();
99  symbol_exprt result{identifier, std::move(t)};
100  result.add_source_location() = source_location;
101 
102  return result;
103 }
104 
106  const irep_idt &identifier,
107  const exprt::operandst &arguments,
108  const source_locationt &source_location,
109  message_handlert &message_handler)
110 {
111  messaget log(message_handler);
112 
113  // adjust return type of function to match pointer subtype
114  if(arguments.empty())
115  {
116  log.error().source_location = source_location;
117  log.error() << identifier << " expects at least one argument"
118  << messaget::eom;
119  throw 0;
120  }
121 
122  const exprt &ptr_arg = arguments.front();
123 
124  if(ptr_arg.type().id() != ID_pointer)
125  {
126  log.error().source_location = source_location;
127  log.error() << identifier << " takes a pointer as first argument"
128  << messaget::eom;
129  throw 0;
130  }
131 
132  code_typet t{{code_typet::parametert(ptr_arg.type())}, void_type()};
133  t.make_ellipsis();
134  symbol_exprt result{identifier, std::move(t)};
135  result.add_source_location() = source_location;
136 
137  return result;
138 }
139 
141  const irep_idt &identifier,
142  const exprt::operandst &arguments,
143  const source_locationt &source_location,
144  message_handlert &message_handler)
145 {
146  // type __atomic_load_n(type *ptr, int memorder)
147  messaget log(message_handler);
148 
149  if(arguments.size() != 2)
150  {
151  log.error().source_location = source_location;
152  log.error() << identifier << " expects two arguments" << messaget::eom;
153  throw 0;
154  }
155 
156  const exprt &ptr_arg = arguments.front();
157 
158  if(ptr_arg.type().id() != ID_pointer)
159  {
160  log.error().source_location = source_location;
161  log.error() << identifier << " takes a pointer as first argument"
162  << messaget::eom;
163  throw 0;
164  }
165 
166  const code_typet t(
167  {code_typet::parametert(ptr_arg.type()),
169  ptr_arg.type().subtype());
170  symbol_exprt result(identifier, t);
171  result.add_source_location() = source_location;
172  return result;
173 }
174 
176  const irep_idt &identifier,
177  const exprt::operandst &arguments,
178  const source_locationt &source_location,
179  message_handlert &message_handler)
180 {
181  // void __atomic_store_n(type *ptr, type val, int memorder)
182  messaget log(message_handler);
183 
184  if(arguments.size() != 3)
185  {
186  log.error().source_location = source_location;
187  log.error() << identifier << " expects three arguments" << messaget::eom;
188  throw 0;
189  }
190 
191  const exprt &ptr_arg = arguments.front();
192 
193  if(ptr_arg.type().id() != ID_pointer)
194  {
195  log.error().source_location = source_location;
196  log.error() << identifier << " takes a pointer as first argument"
197  << messaget::eom;
198  throw 0;
199  }
200 
201  const code_typet t(
202  {code_typet::parametert(ptr_arg.type()),
203  code_typet::parametert(ptr_arg.type().subtype()),
205  void_type());
206  symbol_exprt result(identifier, t);
207  result.add_source_location() = source_location;
208  return result;
209 }
210 
212  const irep_idt &identifier,
213  const exprt::operandst &arguments,
214  const source_locationt &source_location,
215  message_handlert &message_handler)
216 {
217  // type __atomic_exchange_n(type *ptr, type val, int memorder)
218  messaget log(message_handler);
219 
220  if(arguments.size() != 3)
221  {
222  log.error().source_location = source_location;
223  log.error() << identifier << " expects three arguments" << messaget::eom;
224  throw 0;
225  }
226 
227  const exprt &ptr_arg = arguments.front();
228 
229  if(ptr_arg.type().id() != ID_pointer)
230  {
231  log.error().source_location = source_location;
232  log.error() << identifier << " takes a pointer as first argument"
233  << messaget::eom;
234  throw 0;
235  }
236 
237  const code_typet t(
238  {code_typet::parametert(ptr_arg.type()),
239  code_typet::parametert(ptr_arg.type().subtype()),
241  ptr_arg.type().subtype());
242  symbol_exprt result(identifier, t);
243  result.add_source_location() = source_location;
244  return result;
245 }
246 
248  const irep_idt &identifier,
249  const exprt::operandst &arguments,
250  const source_locationt &source_location,
251  message_handlert &message_handler)
252 {
253  // void __atomic_load(type *ptr, type *ret, int memorder)
254  // void __atomic_store(type *ptr, type *val, int memorder)
255  messaget log(message_handler);
256 
257  if(arguments.size() != 3)
258  {
259  log.error().source_location = source_location;
260  log.error() << identifier << " expects three arguments" << messaget::eom;
261  throw 0;
262  }
263 
264  if(arguments[0].type().id() != ID_pointer)
265  {
266  log.error().source_location = source_location;
267  log.error() << identifier << " takes a pointer as first argument"
268  << messaget::eom;
269  throw 0;
270  }
271 
272  if(arguments[1].type().id() != ID_pointer)
273  {
274  log.error().source_location = source_location;
275  log.error() << identifier << " takes a pointer as second argument"
276  << messaget::eom;
277  throw 0;
278  }
279 
280  const exprt &ptr_arg = arguments.front();
281 
282  const code_typet t(
283  {code_typet::parametert(ptr_arg.type()),
284  code_typet::parametert(ptr_arg.type()),
286  void_type());
287  symbol_exprt result(identifier, t);
288  result.add_source_location() = source_location;
289  return result;
290 }
291 
293  const irep_idt &identifier,
294  const exprt::operandst &arguments,
295  const source_locationt &source_location,
296  message_handlert &message_handler)
297 {
298  // void __atomic_exchange(type *ptr, type *val, type *ret, int memorder)
299  messaget log(message_handler);
300 
301  if(arguments.size() != 4)
302  {
303  log.error().source_location = source_location;
304  log.error() << identifier << " expects four arguments" << messaget::eom;
305  throw 0;
306  }
307 
308  if(arguments[0].type().id() != ID_pointer)
309  {
310  log.error().source_location = source_location;
311  log.error() << identifier << " takes a pointer as first argument"
312  << messaget::eom;
313  throw 0;
314  }
315 
316  if(arguments[1].type().id() != ID_pointer)
317  {
318  log.error().source_location = source_location;
319  log.error() << identifier << " takes a pointer as second argument"
320  << messaget::eom;
321  throw 0;
322  }
323 
324  if(arguments[2].type().id() != ID_pointer)
325  {
326  log.error().source_location = source_location;
327  log.error() << identifier << " takes a pointer as third argument"
328  << messaget::eom;
329  throw 0;
330  }
331 
332  const exprt &ptr_arg = arguments.front();
333 
334  const code_typet t(
335  {code_typet::parametert(ptr_arg.type()),
336  code_typet::parametert(ptr_arg.type()),
337  code_typet::parametert(ptr_arg.type()),
339  void_type());
340  symbol_exprt result(identifier, t);
341  result.add_source_location() = source_location;
342  return result;
343 }
344 
346  const irep_idt &identifier,
347  const exprt::operandst &arguments,
348  const source_locationt &source_location,
349  message_handlert &message_handler)
350 {
351  // bool __atomic_compare_exchange_n(type *ptr, type *expected, type
352  // desired, bool weak, int success_memorder, int failure_memorder)
353  // bool __atomic_compare_exchange(type *ptr, type *expected, type
354  // *desired, bool weak, int success_memorder, int failure_memorder)
355  messaget log(message_handler);
356 
357  if(arguments.size() != 6)
358  {
359  log.error().source_location = source_location;
360  log.error() << identifier << " expects six arguments" << messaget::eom;
361  throw 0;
362  }
363 
364  if(arguments[0].type().id() != ID_pointer)
365  {
366  log.error().source_location = source_location;
367  log.error() << identifier << " takes a pointer as first argument"
368  << messaget::eom;
369  throw 0;
370  }
371 
372  if(arguments[1].type().id() != ID_pointer)
373  {
374  log.error().source_location = source_location;
375  log.error() << identifier << " takes a pointer as second argument"
376  << messaget::eom;
377  throw 0;
378  }
379 
380  if(
381  identifier == ID___atomic_compare_exchange &&
382  arguments[2].type().id() != ID_pointer)
383  {
384  log.error().source_location = source_location;
385  log.error() << identifier << " takes a pointer as third argument"
386  << messaget::eom;
387  throw 0;
388  }
389 
390  const exprt &ptr_arg = arguments.front();
391 
392  code_typet::parameterst parameters;
393  parameters.push_back(code_typet::parametert(ptr_arg.type()));
394  parameters.push_back(code_typet::parametert(ptr_arg.type()));
395 
396  if(identifier == ID___atomic_compare_exchange)
397  parameters.push_back(code_typet::parametert(ptr_arg.type()));
398  else
399  parameters.push_back(code_typet::parametert(ptr_arg.type().subtype()));
400 
401  parameters.push_back(code_typet::parametert(c_bool_type()));
402  parameters.push_back(code_typet::parametert(signed_int_type()));
403  parameters.push_back(code_typet::parametert(signed_int_type()));
404  code_typet t(std::move(parameters), c_bool_type());
405  symbol_exprt result(identifier, t);
406  result.add_source_location() = source_location;
407  return result;
408 }
409 
411  const irep_idt &identifier,
412  const exprt::operandst &arguments,
413  const source_locationt &source_location,
414  message_handlert &message_handler)
415 {
416  messaget log(message_handler);
417 
418  if(arguments.size() != 3)
419  {
420  log.error().source_location = source_location;
421  log.error() << "__atomic_*_fetch primitives take three arguments"
422  << messaget::eom;
423  throw 0;
424  }
425 
426  const exprt &ptr_arg = arguments.front();
427 
428  if(ptr_arg.type().id() != ID_pointer)
429  {
430  log.error().source_location = source_location;
431  log.error()
432  << "__atomic_*_fetch primitives take a pointer as first argument"
433  << messaget::eom;
434  throw 0;
435  }
436 
437  code_typet t(
438  {code_typet::parametert(ptr_arg.type()),
439  code_typet::parametert(ptr_arg.type().subtype()),
441  ptr_arg.type().subtype());
442  symbol_exprt result(identifier, std::move(t));
443  result.add_source_location() = source_location;
444  return result;
445 }
446 
448  const irep_idt &identifier,
449  const exprt::operandst &arguments,
450  const source_locationt &source_location,
451  message_handlert &message_handler)
452 {
453  messaget log(message_handler);
454 
455  if(arguments.size() != 3)
456  {
457  log.error().source_location = source_location;
458  log.error() << "__atomic_fetch_* primitives take three arguments"
459  << messaget::eom;
460  throw 0;
461  }
462 
463  const exprt &ptr_arg = arguments.front();
464 
465  if(ptr_arg.type().id() != ID_pointer)
466  {
467  log.error().source_location = source_location;
468  log.error()
469  << "__atomic_fetch_* primitives take a pointer as first argument"
470  << messaget::eom;
471  throw 0;
472  }
473 
474  code_typet t(
475  {code_typet::parametert(ptr_arg.type()),
476  code_typet::parametert(ptr_arg.type().subtype()),
478  ptr_arg.type().subtype());
479  symbol_exprt result(identifier, std::move(t));
480  result.add_source_location() = source_location;
481  return result;
482 }
483 
485  const irep_idt &identifier,
486  const exprt::operandst &arguments,
487  const source_locationt &source_location)
488 {
489  // the arguments need not be type checked just yet, thus do not make
490  // assumptions that would require type checking
491 
492  if(
493  identifier == ID___sync_fetch_and_add ||
494  identifier == ID___sync_fetch_and_sub ||
495  identifier == ID___sync_fetch_and_or ||
496  identifier == ID___sync_fetch_and_and ||
497  identifier == ID___sync_fetch_and_xor ||
498  identifier == ID___sync_fetch_and_nand ||
499  identifier == ID___sync_add_and_fetch ||
500  identifier == ID___sync_sub_and_fetch ||
501  identifier == ID___sync_or_and_fetch ||
502  identifier == ID___sync_and_and_fetch ||
503  identifier == ID___sync_xor_and_fetch ||
504  identifier == ID___sync_nand_and_fetch ||
505  identifier == ID___sync_lock_test_and_set)
506  {
507  // These are polymorphic, see
508  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
510  identifier, arguments, source_location, get_message_handler());
511  }
512  else if(
513  identifier == ID___sync_bool_compare_and_swap ||
514  identifier == ID___sync_val_compare_and_swap)
515  {
516  // These are polymorphic, see
517  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
519  identifier, arguments, source_location, get_message_handler());
520  }
521  else if(identifier == ID___sync_lock_release)
522  {
523  // This is polymorphic, see
524  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
526  identifier, arguments, source_location, get_message_handler());
527  }
528  else if(identifier == ID___atomic_load_n)
529  {
530  // These are polymorphic
531  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
533  identifier, arguments, source_location, get_message_handler());
534  }
535  else if(identifier == ID___atomic_store_n)
536  {
537  // These are polymorphic
538  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
540  identifier, arguments, source_location, get_message_handler());
541  }
542  else if(identifier == ID___atomic_exchange_n)
543  {
544  // These are polymorphic
545  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
547  identifier, arguments, source_location, get_message_handler());
548  }
549  else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
550  {
551  // These are polymorphic
552  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
554  identifier, arguments, source_location, get_message_handler());
555  }
556  else if(identifier == ID___atomic_exchange)
557  {
558  // These are polymorphic
559  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
561  identifier, arguments, source_location, get_message_handler());
562  }
563  else if(
564  identifier == ID___atomic_compare_exchange_n ||
565  identifier == ID___atomic_compare_exchange)
566  {
567  // These are polymorphic
568  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
570  identifier, arguments, source_location, get_message_handler());
571  }
572  else if(
573  identifier == ID___atomic_add_fetch ||
574  identifier == ID___atomic_sub_fetch ||
575  identifier == ID___atomic_and_fetch ||
576  identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
577  identifier == ID___atomic_nand_fetch)
578  {
579  // These are polymorphic
580  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
582  identifier, arguments, source_location, get_message_handler());
583  }
584  else if(
585  identifier == ID___atomic_fetch_add ||
586  identifier == ID___atomic_fetch_sub ||
587  identifier == ID___atomic_fetch_and ||
588  identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
589  identifier == ID___atomic_fetch_nand)
590  {
591  // These are polymorphic
592  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
594  identifier, arguments, source_location, get_message_handler());
595  }
596 
597  return {};
598 }
599 
601  const irep_idt &identifier,
602  const typet &type,
603  const source_locationt &source_location,
604  symbol_tablet &symbol_table)
605 {
606  symbolt symbol;
607  symbol.name = id2string(identifier) + "::1::result";
608  symbol.base_name = "result";
609  symbol.type = type;
610  symbol.mode = ID_C;
611  symbol.location = source_location;
612  symbol.is_file_local = true;
613  symbol.is_lvalue = true;
614  symbol.is_thread_local = true;
615 
616  symbol_table.add(symbol);
617 
618  return symbol;
619 }
620 
622  const irep_idt &identifier,
623  const irep_idt &identifier_with_type,
624  const code_typet &code_type,
625  const source_locationt &source_location,
626  const std::vector<symbol_exprt> &parameter_exprs,
627  symbol_tablet &symbol_table,
628  code_blockt &block)
629 {
630  // type __sync_fetch_and_OP(type *ptr, type value, ...)
631  // { type result; result = *ptr; *ptr = result OP value; return result; }
632  const typet &type = code_type.return_type();
633 
634  const symbol_exprt result =
635  result_symbol(identifier_with_type, type, source_location, symbol_table)
636  .symbol_expr();
637  block.add(codet{ID_decl_block, {code_declt{result}}});
638 
639  // place operations on *ptr in an atomic section
641  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
642  {},
643  code_typet{{}, void_type()},
644  source_location}});
645 
646  // build *ptr
647  const dereference_exprt deref_ptr{parameter_exprs[0]};
648 
649  block.add(code_assignt{result, deref_ptr});
650 
651  // build *ptr = result OP arguments[1];
652  irep_idt op_id = identifier == ID___atomic_fetch_add
653  ? ID_plus
654  : identifier == ID___atomic_fetch_sub
655  ? ID_minus
656  : identifier == ID___atomic_fetch_or
657  ? ID_bitor
658  : identifier == ID___atomic_fetch_and
659  ? ID_bitand
660  : identifier == ID___atomic_fetch_xor
661  ? ID_bitxor
662  : identifier == ID___atomic_fetch_nand
663  ? ID_bitnand
664  : ID_nil;
665  binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
666  block.add(code_assignt{deref_ptr, std::move(op_expr)});
667 
669  symbol_exprt::typeless("__atomic_thread_fence"),
670  {parameter_exprs[2]},
671  typet{},
672  source_location}});
673 
676  {},
677  code_typet{{}, void_type()},
678  source_location}});
679 
680  block.add(code_returnt{result});
681 }
682 
684  const irep_idt &identifier,
685  const irep_idt &identifier_with_type,
686  const code_typet &code_type,
687  const source_locationt &source_location,
688  const std::vector<symbol_exprt> &parameter_exprs,
689  symbol_tablet &symbol_table,
690  code_blockt &block)
691 {
692  // type __sync_OP_and_fetch(type *ptr, type value, ...)
693  // { type result; result = *ptr OP value; *ptr = result; return result; }
694  const typet &type = code_type.return_type();
695 
696  const symbol_exprt result =
697  result_symbol(identifier_with_type, type, source_location, symbol_table)
698  .symbol_expr();
699  block.add(codet{ID_decl_block, {code_declt{result}}});
700 
701  // place operations on *ptr in an atomic section
703  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
704  {},
705  code_typet{{}, void_type()},
706  source_location}});
707 
708  // build *ptr
709  const dereference_exprt deref_ptr{parameter_exprs[0]};
710 
711  // build result = *ptr OP arguments[1];
712  irep_idt op_id = identifier == ID___atomic_add_fetch
713  ? ID_plus
714  : identifier == ID___atomic_sub_fetch
715  ? ID_minus
716  : identifier == ID___atomic_or_fetch
717  ? ID_bitor
718  : identifier == ID___atomic_and_fetch
719  ? ID_bitand
720  : identifier == ID___atomic_xor_fetch
721  ? ID_bitxor
722  : identifier == ID___atomic_nand_fetch
723  ? ID_bitnand
724  : ID_nil;
725  binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
726  block.add(code_assignt{result, std::move(op_expr)});
727 
728  block.add(code_assignt{deref_ptr, result});
729 
730  // this instruction implies an mfence, i.e., WRfence
732  symbol_exprt::typeless("__atomic_thread_fence"),
733  {parameter_exprs[2]},
734  typet{},
735  source_location}});
736 
739  {},
740  code_typet{{}, void_type()},
741  source_location}});
742 
743  block.add(code_returnt{result});
744 }
745 
747  const irep_idt &identifier,
748  const irep_idt &identifier_with_type,
749  const code_typet &code_type,
750  const source_locationt &source_location,
751  const std::vector<symbol_exprt> &parameter_exprs,
752  code_blockt &block)
753 {
754  // implement by calling their __atomic_ counterparts with memorder SEQ_CST
755  std::string atomic_name = "__atomic_" + id2string(identifier).substr(7);
756  atomic_name.replace(atomic_name.find("_and_"), 5, "_");
757 
758  exprt::operandst arguments{
759  parameter_exprs[0],
760  parameter_exprs[1],
761  from_integer(std::memory_order_seq_cst, signed_int_type())};
762 
763  block.add(code_returnt{
765  std::move(arguments),
766  typet{},
767  source_location}});
768 }
769 
771  const irep_idt &identifier_with_type,
772  const code_typet &code_type,
773  const source_locationt &source_location,
774  const std::vector<symbol_exprt> &parameter_exprs,
775  code_blockt &block)
776 {
777  // These builtins perform an atomic compare and swap. That is, if the
778  // current value of *ptr is oldval, then write newval into *ptr. The
779  // "bool" version returns true if the comparison is successful and
780  // newval was written. The "val" version returns the contents of *ptr
781  // before the operation.
782 
783  // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
784 
786  symbol_exprt::typeless(ID___atomic_compare_exchange),
787  {parameter_exprs[0],
788  address_of_exprt{parameter_exprs[1]},
789  address_of_exprt{parameter_exprs[2]},
791  from_integer(std::memory_order_seq_cst, signed_int_type()),
792  from_integer(std::memory_order_seq_cst, signed_int_type())},
793  typet{},
794  source_location}});
795 }
796 
798  const irep_idt &identifier_with_type,
799  const code_typet &code_type,
800  const source_locationt &source_location,
801  const std::vector<symbol_exprt> &parameter_exprs,
802  symbol_tablet &symbol_table,
803  code_blockt &block)
804 {
805  // type __sync_val_compare_and_swap(type *ptr, type old, type new, ...)
806  // { type result = *ptr; if(result == old) *ptr = new; return result; }
807  const typet &type = code_type.return_type();
808 
809  const symbol_exprt result =
810  result_symbol(identifier_with_type, type, source_location, symbol_table)
811  .symbol_expr();
812  block.add(codet{ID_decl_block, {code_declt{result}}});
813 
814  // place operations on *ptr in an atomic section
816  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
817  {},
818  code_typet{{}, void_type()},
819  source_location}});
820 
821  // build *ptr
822  const dereference_exprt deref_ptr{parameter_exprs[0]};
823 
824  block.add(code_assignt{result, deref_ptr});
825 
826  code_assignt assign{deref_ptr, parameter_exprs[2]};
827  assign.add_source_location() = source_location;
828  block.add(code_ifthenelset{equal_exprt{result, parameter_exprs[1]},
829  std::move(assign)});
830 
831  // this instruction implies an mfence, i.e., WRfence
834  {string_constantt{ID_WRfence}},
835  typet{},
836  source_location}});
837 
840  {},
841  code_typet{{}, void_type()},
842  source_location}});
843 
844  block.add(code_returnt{result});
845 }
846 
848  const irep_idt &identifier_with_type,
849  const code_typet &code_type,
850  const source_locationt &source_location,
851  const std::vector<symbol_exprt> &parameter_exprs,
852  symbol_tablet &symbol_table,
853  code_blockt &block)
854 {
855  // type __sync_lock_test_and_set (type *ptr, type value, ...)
856 
857  // This builtin, as described by Intel, is not a traditional
858  // test-and-set operation, but rather an atomic exchange operation.
859  // It writes value into *ptr, and returns the previous contents of
860  // *ptr. Many targets have only minimal support for such locks, and
861  // do not support a full exchange operation. In this case, a target
862  // may support reduced functionality here by which the only valid
863  // value to store is the immediate constant 1. The exact value
864  // actually stored in *ptr is implementation defined.
865  const typet &type = code_type.return_type();
866 
867  const symbol_exprt result =
868  result_symbol(identifier_with_type, type, source_location, symbol_table)
869  .symbol_expr();
870  block.add(codet{ID_decl_block, {code_declt{result}}});
871 
872  // place operations on *ptr in an atomic section
874  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
875  {},
876  code_typet{{}, void_type()},
877  source_location}});
878 
879  // build *ptr
880  const dereference_exprt deref_ptr{parameter_exprs[0]};
881 
882  block.add(code_assignt{result, deref_ptr});
883 
884  block.add(code_assignt{deref_ptr, parameter_exprs[1]});
885 
886  // This built-in function is not a full barrier, but rather an acquire
887  // barrier.
890  {string_constantt{ID_RRfence}, {string_constantt{ID_RRfence}}},
891  typet{},
892  source_location}});
893 
896  {},
897  code_typet{{}, void_type()},
898  source_location}});
899 
900  block.add(code_returnt{result});
901 }
902 
904  const irep_idt &identifier_with_type,
905  const code_typet &code_type,
906  const source_locationt &source_location,
907  const std::vector<symbol_exprt> &parameter_exprs,
908  code_blockt &block)
909 {
910  // void __sync_lock_release (type *ptr, ...)
911 
912  // This built-in function releases the lock acquired by
913  // __sync_lock_test_and_set. Normally this means writing the constant 0 to
914  // *ptr.
915  const typet &type = to_pointer_type(parameter_exprs[0].type()).subtype();
916 
917  // place operations on *ptr in an atomic section
919  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
920  {},
921  code_typet{{}, void_type()},
922  source_location}});
923 
924  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
926  from_integer(0, signed_int_type()), type)});
927 
928  // This built-in function is not a full barrier, but rather a release
929  // barrier.
932  {string_constantt{ID_WRfence}, {string_constantt{ID_WWfence}}},
933  typet{},
934  source_location}});
935 
938  {},
939  code_typet{{}, void_type()},
940  source_location}});
941 }
942 
944  const irep_idt &identifier_with_type,
945  const code_typet &code_type,
946  const source_locationt &source_location,
947  const std::vector<symbol_exprt> &parameter_exprs,
948  code_blockt &block)
949 {
950  // void __atomic_load (type *ptr, type *ret, int memorder)
951  // This is the generic version of an atomic load. It returns the contents of
952  // *ptr in *ret.
953 
955  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
956  {},
957  code_typet{{}, void_type()},
958  source_location}});
959 
960  block.add(code_assignt{dereference_exprt{parameter_exprs[1]},
961  dereference_exprt{parameter_exprs[0]}});
962 
964  symbol_exprt::typeless("__atomic_thread_fence"),
965  {parameter_exprs[2]},
966  typet{},
967  source_location}});
968 
971  {},
972  code_typet{{}, void_type()},
973  source_location}});
974 }
975 
977  const irep_idt &identifier_with_type,
978  const code_typet &code_type,
979  const source_locationt &source_location,
980  const std::vector<symbol_exprt> &parameter_exprs,
981  symbol_tablet &symbol_table,
982  code_blockt &block)
983 {
984  // type __atomic_load_n (type *ptr, int memorder)
985  // This built-in function implements an atomic load operation. It returns
986  // the contents of *ptr.
987  const typet &type = code_type.return_type();
988 
989  const symbol_exprt result =
990  result_symbol(identifier_with_type, type, source_location, symbol_table)
991  .symbol_expr();
992  block.add(codet{ID_decl_block, {code_declt{result}}});
993 
995  symbol_exprt::typeless(ID___atomic_load),
996  {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
997  typet{},
998  source_location}});
999 
1000  block.add(code_returnt{result});
1001 }
1002 
1004  const irep_idt &identifier_with_type,
1005  const code_typet &code_type,
1006  const source_locationt &source_location,
1007  const std::vector<symbol_exprt> &parameter_exprs,
1008  code_blockt &block)
1009 {
1010  // void __atomic_store (type *ptr, type *val, int memorder)
1011  // This is the generic version of an atomic store. It stores the value of
1012  // *val into *ptr.
1013 
1015  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1016  {},
1017  code_typet{{}, void_type()},
1018  source_location}});
1019 
1020  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
1021  dereference_exprt{parameter_exprs[1]}});
1022 
1024  symbol_exprt::typeless("__atomic_thread_fence"),
1025  {parameter_exprs[2]},
1026  typet{},
1027  source_location}});
1028 
1030  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1031  {},
1032  code_typet{{}, void_type()},
1033  source_location}});
1034 }
1035 
1037  const irep_idt &identifier_with_type,
1038  const code_typet &code_type,
1039  const source_locationt &source_location,
1040  const std::vector<symbol_exprt> &parameter_exprs,
1041  code_blockt &block)
1042 {
1043  // void __atomic_store_n (type *ptr, type val, int memorder)
1044  // This built-in function implements an atomic store operation. It writes
1045  // val into *ptr.
1046 
1047  block.add(code_expressiont{
1049  {parameter_exprs[0],
1050  address_of_exprt{parameter_exprs[1]},
1051  parameter_exprs[2]},
1052  typet{},
1053  source_location}});
1054 }
1055 
1057  const irep_idt &identifier_with_type,
1058  const code_typet &code_type,
1059  const source_locationt &source_location,
1060  const std::vector<symbol_exprt> &parameter_exprs,
1061  code_blockt &block)
1062 {
1063  // void __atomic_exchange (type *ptr, type *val, type *ret, int memorder)
1064  // This is the generic version of an atomic exchange. It stores the contents
1065  // of *val into *ptr. The original value of *ptr is copied into *ret.
1066 
1068  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1069  {},
1070  code_typet{{}, void_type()},
1071  source_location}});
1072 
1073  block.add(code_assignt{dereference_exprt{parameter_exprs[2]},
1074  dereference_exprt{parameter_exprs[0]}});
1075  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
1076  dereference_exprt{parameter_exprs[1]}});
1077 
1079  symbol_exprt::typeless("__atomic_thread_fence"),
1080  {parameter_exprs[3]},
1081  typet{},
1082  source_location}});
1083 
1085  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1086  {},
1087  code_typet{{}, void_type()},
1088  source_location}});
1089 }
1090 
1092  const irep_idt &identifier_with_type,
1093  const code_typet &code_type,
1094  const source_locationt &source_location,
1095  const std::vector<symbol_exprt> &parameter_exprs,
1096  symbol_tablet &symbol_table,
1097  code_blockt &block)
1098 {
1099  // type __atomic_exchange_n (type *ptr, type val, int memorder)
1100  // This built-in function implements an atomic exchange operation. It writes
1101  // val into *ptr, and returns the previous contents of *ptr.
1102  const typet &type = code_type.return_type();
1103 
1104  const symbol_exprt result =
1105  result_symbol(identifier_with_type, type, source_location, symbol_table)
1106  .symbol_expr();
1107  block.add(codet{ID_decl_block, {code_declt{result}}});
1108 
1110  symbol_exprt::typeless(ID___atomic_exchange),
1111  {parameter_exprs[0],
1112  address_of_exprt{parameter_exprs[1]},
1113  address_of_exprt{result},
1114  parameter_exprs[2]},
1115  typet{},
1116  source_location}});
1117 
1118  block.add(code_returnt{result});
1119 }
1120 
1122  const irep_idt &identifier_with_type,
1123  const code_typet &code_type,
1124  const source_locationt &source_location,
1125  const std::vector<symbol_exprt> &parameter_exprs,
1126  symbol_tablet &symbol_table,
1127  code_blockt &block)
1128 {
1129  // bool __atomic_compare_exchange (type *ptr, type *expected, type *desired,
1130  // bool weak, int success_memorder, int failure_memorder)
1131  // This built-in function implements an atomic compare and exchange
1132  // operation. This compares the contents of *ptr with the contents of
1133  // *expected. If equal, the operation is a read-modify-write operation that
1134  // writes *desired into *ptr. If they are not equal, the operation is a read
1135  // and the current contents of *ptr are written into *expected. weak is true
1136  // for weak compare_exchange, which may fail spuriously, and false for the
1137  // strong variation, which never fails spuriously. Many targets only offer
1138  // the strong variation and ignore the parameter.
1139 
1140  const symbol_exprt result =
1141  result_symbol(
1142  identifier_with_type, c_bool_type(), source_location, symbol_table)
1143  .symbol_expr();
1144  block.add(codet{ID_decl_block, {code_declt{result}}});
1145 
1146  // place operations on *ptr in an atomic section
1148  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1149  {},
1150  code_typet{{}, void_type()},
1151  source_location}});
1152 
1153  // build *ptr
1154  const dereference_exprt deref_ptr{parameter_exprs[0]};
1155 
1156  block.add(code_assignt{
1157  result,
1159  equal_exprt{deref_ptr, dereference_exprt{parameter_exprs[1]}},
1160  result.type())});
1161 
1162  // we never fail spuriously, and ignore parameter_exprs[3]
1163  code_assignt assign{deref_ptr, dereference_exprt{parameter_exprs[2]}};
1164  assign.add_source_location() = source_location;
1166  symbol_exprt::typeless("__atomic_thread_fence"),
1167  {parameter_exprs[4]},
1168  typet{},
1169  source_location}};
1170  success_fence.add_source_location() = source_location;
1171 
1172  code_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]},
1173  deref_ptr};
1174  assign_not_equal.add_source_location() = source_location;
1176  symbol_exprt::typeless("__atomic_thread_fence"),
1177  {parameter_exprs[5]},
1178  typet{},
1179  source_location}};
1180  failure_fence.add_source_location() = source_location;
1181 
1182  block.add(code_ifthenelset{
1183  result,
1184  code_blockt{{std::move(assign), std::move(success_fence)}},
1185  code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1186 
1188  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1189  {},
1190  code_typet{{}, void_type()},
1191  source_location}});
1192 
1193  block.add(code_returnt{result});
1194 }
1195 
1197  const irep_idt &identifier_with_type,
1198  const code_typet &code_type,
1199  const source_locationt &source_location,
1200  const std::vector<symbol_exprt> &parameter_exprs,
1201  code_blockt &block)
1202 {
1203  // bool __atomic_compare_exchange_n (type *ptr, type *expected, type
1204  // desired, bool weak, int success_memorder, int failure_memorder)
1205 
1207  symbol_exprt::typeless(ID___atomic_compare_exchange),
1208  {parameter_exprs[0],
1209  parameter_exprs[1],
1210  address_of_exprt{parameter_exprs[2]},
1211  parameter_exprs[3],
1212  parameter_exprs[4],
1213  parameter_exprs[5]},
1214  typet{},
1215  source_location}});
1216 }
1217 
1219  const irep_idt &identifier,
1220  const symbol_exprt &function_symbol)
1221 {
1222  const irep_idt &identifier_with_type = function_symbol.get_identifier();
1223  const code_typet &code_type = to_code_type(function_symbol.type());
1224  const source_locationt &source_location = function_symbol.source_location();
1225 
1226  std::vector<symbol_exprt> parameter_exprs;
1227  parameter_exprs.reserve(code_type.parameters().size());
1228  for(const auto &parameter : code_type.parameters())
1229  {
1230  parameter_exprs.push_back(lookup(parameter.get_identifier()).symbol_expr());
1231  }
1232 
1233  code_blockt block;
1234 
1235  if(
1236  identifier == ID___atomic_fetch_add ||
1237  identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1238  identifier == ID___atomic_fetch_and ||
1239  identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1240  {
1242  identifier,
1243  identifier_with_type,
1244  code_type,
1245  source_location,
1246  parameter_exprs,
1247  symbol_table,
1248  block);
1249  }
1250  else if(
1251  identifier == ID___atomic_add_fetch ||
1252  identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1253  identifier == ID___atomic_and_fetch ||
1254  identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1255  {
1257  identifier,
1258  identifier_with_type,
1259  code_type,
1260  source_location,
1261  parameter_exprs,
1262  symbol_table,
1263  block);
1264  }
1265  else if(
1266  identifier == ID___sync_fetch_and_add ||
1267  identifier == ID___sync_fetch_and_sub ||
1268  identifier == ID___sync_fetch_and_or ||
1269  identifier == ID___sync_fetch_and_and ||
1270  identifier == ID___sync_fetch_and_xor ||
1271  identifier == ID___sync_fetch_and_nand ||
1272  identifier == ID___sync_add_and_fetch ||
1273  identifier == ID___sync_sub_and_fetch ||
1274  identifier == ID___sync_or_and_fetch ||
1275  identifier == ID___sync_and_and_fetch ||
1276  identifier == ID___sync_xor_and_fetch ||
1277  identifier == ID___sync_nand_and_fetch)
1278  {
1280  identifier,
1281  identifier_with_type,
1282  code_type,
1283  source_location,
1284  parameter_exprs,
1285  block);
1286  }
1287  else if(identifier == ID___sync_bool_compare_and_swap)
1288  {
1290  identifier_with_type, code_type, source_location, parameter_exprs, block);
1291  }
1292  else if(identifier == ID___sync_val_compare_and_swap)
1293  {
1295  identifier_with_type,
1296  code_type,
1297  source_location,
1298  parameter_exprs,
1299  symbol_table,
1300  block);
1301  }
1302  else if(identifier == ID___sync_lock_test_and_set)
1303  {
1305  identifier_with_type,
1306  code_type,
1307  source_location,
1308  parameter_exprs,
1309  symbol_table,
1310  block);
1311  }
1312  else if(identifier == ID___sync_lock_release)
1313  {
1315  identifier_with_type, code_type, source_location, parameter_exprs, block);
1316  }
1317  else if(identifier == ID___atomic_load)
1318  {
1320  identifier_with_type, code_type, source_location, parameter_exprs, block);
1321  }
1322  else if(identifier == ID___atomic_load_n)
1323  {
1325  identifier_with_type,
1326  code_type,
1327  source_location,
1328  parameter_exprs,
1329  symbol_table,
1330  block);
1331  }
1332  else if(identifier == ID___atomic_store)
1333  {
1335  identifier_with_type, code_type, source_location, parameter_exprs, block);
1336  }
1337  else if(identifier == ID___atomic_store_n)
1338  {
1340  identifier_with_type, code_type, source_location, parameter_exprs, block);
1341  }
1342  else if(identifier == ID___atomic_exchange)
1343  {
1345  identifier_with_type, code_type, source_location, parameter_exprs, block);
1346  }
1347  else if(identifier == ID___atomic_exchange_n)
1348  {
1350  identifier_with_type,
1351  code_type,
1352  source_location,
1353  parameter_exprs,
1354  symbol_table,
1355  block);
1356  }
1357  else if(identifier == ID___atomic_compare_exchange)
1358  {
1360  identifier_with_type,
1361  code_type,
1362  source_location,
1363  parameter_exprs,
1364  symbol_table,
1365  block);
1366  }
1367  else if(identifier == ID___atomic_compare_exchange_n)
1368  {
1370  identifier_with_type, code_type, source_location, parameter_exprs, block);
1371  }
1372  else
1373  {
1374  UNREACHABLE;
1375  }
1376 
1377  for(auto &statement : block.statements())
1378  statement.add_source_location() = source_location;
1379 
1380  return block;
1381 }
1382 
1384  const side_effect_expr_function_callt &expr)
1385 {
1386  const exprt &f_op = expr.function();
1387  const source_locationt &source_location = expr.source_location();
1388  const irep_idt &identifier = to_symbol_expr(f_op).get_identifier();
1389 
1390  exprt::operandst arguments = expr.arguments();
1391 
1392  if(identifier == "__builtin_shuffle")
1393  {
1394  // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html and
1395  // https://github.com/OpenCL/man/blob/master/shuffle.adoc
1396  if(arguments.size() != 2 && arguments.size() != 3)
1397  {
1399  error() << "__builtin_shuffle expects two or three arguments" << eom;
1400  throw 0;
1401  }
1402 
1403  for(exprt &arg : arguments)
1404  {
1405  if(arg.type().id() != ID_vector)
1406  {
1408  error() << "__builtin_shuffle expects vector arguments" << eom;
1409  throw 0;
1410  }
1411  }
1412 
1413  const exprt &arg0 = arguments[0];
1414  const vector_typet &input_vec_type = to_vector_type(arg0.type());
1415 
1416  optionalt<exprt> arg1;
1417  if(arguments.size() == 3)
1418  {
1419  if(arguments[1].type() != input_vec_type)
1420  {
1422  error() << "__builtin_shuffle expects input vectors of the same type"
1423  << eom;
1424  throw 0;
1425  }
1426  arg1 = arguments[1];
1427  }
1428  const exprt &indices = arguments.back();
1429  const vector_typet &indices_type = to_vector_type(indices.type());
1430  const std::size_t indices_size =
1431  numeric_cast_v<std::size_t>(indices_type.size());
1432 
1433  exprt::operandst operands;
1434  operands.reserve(indices_size);
1435 
1436  auto input_size = numeric_cast<mp_integer>(input_vec_type.size());
1437  CHECK_RETURN(input_size.has_value());
1438  if(arg1.has_value())
1439  input_size = *input_size * 2;
1440  constant_exprt size = from_integer(*input_size, indices_type.subtype());
1441 
1442  for(std::size_t i = 0; i < indices_size; ++i)
1443  {
1444  // only the least significant bits of each mask element are considered
1445  mod_exprt mod_index{index_exprt{indices, from_integer(i, index_type())},
1446  size};
1447  mod_index.add_source_location() = source_location;
1448  operands.push_back(std::move(mod_index));
1449  }
1450 
1451  return shuffle_vector_exprt{arg0, arg1, std::move(operands)}.lower();
1452  }
1453  else if(identifier == "__builtin_shufflevector")
1454  {
1455  // https://clang.llvm.org/docs/LanguageExtensions.html#langext-builtin-shufflevector
1456  if(arguments.size() < 2)
1457  {
1459  error() << "__builtin_shufflevector expects two or more arguments" << eom;
1460  throw 0;
1461  }
1462 
1463  exprt::operandst operands;
1464  operands.reserve(arguments.size() - 2);
1465 
1466  for(std::size_t i = 0; i < arguments.size(); ++i)
1467  {
1468  exprt &arg_i = arguments[i];
1469 
1470  if(i <= 1 && arg_i.type().id() != ID_vector)
1471  {
1473  error() << "__builtin_shufflevector expects two vectors as argument"
1474  << eom;
1475  throw 0;
1476  }
1477  else if(i > 1)
1478  {
1480  {
1482  error() << "__builtin_shufflevector expects integer index" << eom;
1483  throw 0;
1484  }
1485 
1486  make_constant(arg_i);
1487 
1488  const auto int_index = numeric_cast<mp_integer>(arg_i);
1489  CHECK_RETURN(int_index.has_value());
1490 
1491  if(*int_index == -1)
1492  {
1493  operands.push_back(from_integer(0, arg_i.type()));
1494  operands.back().add_source_location() = source_location;
1495  }
1496  else
1497  operands.push_back(arg_i);
1498  }
1499  }
1500 
1501  return shuffle_vector_exprt{arguments[0], arguments[1], std::move(operands)}
1502  .lower();
1503  }
1504  else
1505  UNREACHABLE;
1506 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typecheck_sync_compare_swap
static symbol_exprt typecheck_sync_compare_swap(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:62
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1874
typecheck_atomic_load_store
static symbol_exprt typecheck_atomic_load_store(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:247
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
typet::subtype
const typet & subtype() const
Definition: type.h:47
instantiate_atomic_load_n
static void instantiate_atomic_load_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:976
arith_tools.h
typecheck_atomic_op_fetch
static symbol_exprt typecheck_atomic_op_fetch(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:410
typecheck_atomic_exchange
static symbol_exprt typecheck_atomic_exchange(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:292
instantiate_atomic_store_n
static void instantiate_atomic_store_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1036
instantiate_atomic_exchange_n
static void instantiate_atomic_exchange_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1091
shuffle_vector_exprt
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
Definition: c_expr.h:20
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
c_typecheck_base.h
ANSI-C Language Type Checking.
typecheck_atomic_fetch_op
static symbol_exprt typecheck_atomic_fetch_op(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:447
instantiate_sync_fetch
static void instantiate_sync_fetch(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:746
instantiate_atomic_compare_exchange
static void instantiate_atomic_compare_exchange(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1121
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:628
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2138
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:99
typecheck_atomic_exchange_n
static symbol_exprt typecheck_atomic_exchange_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:211
instantiate_sync_lock_test_and_set
static void instantiate_sync_lock_test_and_set(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:847
c_bool_type
typet c_bool_type()
Definition: c_types.cpp:108
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
typecheck_atomic_store_n
static symbol_exprt typecheck_atomic_store_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:175
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:54
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:550
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
vector_typet
The vector type.
Definition: std_types.h:975
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
string_constantt
Definition: string_constant.h:15
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1225
void_type
empty_typet void_type()
Definition: c_types.cpp:253
code_ifthenelset
codet representation of an if-then-else statement.
Definition: std_code.h:776
c_typecheck_baset::make_constant
virtual void make_constant(exprt &expr)
Definition: c_typecheck_expr.cpp:3928
instantiate_sync_val_compare_and_swap
static void instantiate_sync_val_compare_and_swap(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:797
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:176
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
symbolt::is_thread_local
bool is_thread_local
Definition: symbol.h:65
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:744
result_symbol
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:600
instantiate_atomic_op_fetch
static void instantiate_atomic_op_fetch(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:683
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
signed_int_type
signedbv_typet signed_int_type()
Definition: c_types.cpp:30
instantiate_atomic_exchange
static void instantiate_atomic_exchange(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1056
instantiate_atomic_compare_exchange_n
static void instantiate_atomic_compare_exchange_n(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1196
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
c_typecheck_baset::instantiate_gcc_polymorphic_builtin
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1218
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
c_expr.h
API to expression classes that are internal to the C frontend.
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:109
instantiate_sync_lock_release
static void instantiate_sync_lock_release(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:903
std_types.h
Pre-defined types.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
pointer_expr.h
API to expression classes for Pointers.
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
is_signed_or_unsigned_bitvector
bool is_signed_or_unsigned_bitvector(const typet &type)
This method tests, if the given typet is a signed or unsigned bitvector.
Definition: bitvector_types.h:19
c_typecheck_baset::typecheck_gcc_polymorphic_builtin
virtual optionalt< symbol_exprt > typecheck_gcc_polymorphic_builtin(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:484
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:68
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
code_typet
Base type of functions.
Definition: std_types.h:539
c_typecheck_baset::typecheck_shuffle_vector
virtual exprt typecheck_shuffle_vector(const side_effect_expr_function_callt &expr)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1383
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
code_blockt::add
void add(const codet &code)
Definition: std_code.h:206
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
cprover_prefix.h
typecheck_sync_lock_release
static symbol_exprt typecheck_sync_lock_release(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:105
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
vector_typet::size
const constant_exprt & size() const
Definition: std_types.cpp:239
shuffle_vector_exprt::lower
vector_exprt lower() const
Definition: c_expr.cpp:32
typecheck_atomic_compare_exchange
static symbol_exprt typecheck_atomic_compare_exchange(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:345
source_locationt
Definition: source_location.h:19
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
code_returnt
codet representation of a "return from a function" statement.
Definition: std_code.h:1340
typecheck_atomic_load_n
static symbol_exprt typecheck_atomic_load_n(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:140
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
side_effect_expr_function_callt::arguments
exprt::operandst & arguments()
Definition: std_code.h:2164
instantiate_atomic_load
static void instantiate_atomic_load(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:943
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
instantiate_atomic_store
static void instantiate_atomic_store(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:1003
code_typet::parametert
Definition: std_types.h:556
instantiate_sync_bool_compare_and_swap
static void instantiate_sync_bool_compare_and_swap(const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:770
to_vector_type
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition: std_types.h:1000
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
side_effect_expr_function_callt::function
exprt & function()
Definition: std_code.h:2154
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
index_exprt
Array index operator.
Definition: std_expr.h:1328
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:341
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:230
c_types.h
instantiate_atomic_fetch_op
static void instantiate_atomic_fetch_op(const irep_idt &identifier, const irep_idt &identifier_with_type, const code_typet &code_type, const source_locationt &source_location, const std::vector< symbol_exprt > &parameter_exprs, symbol_tablet &symbol_table, code_blockt &block)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:621
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
mod_exprt
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
typecheck_sync_with_pointer_parameter
static symbol_exprt typecheck_sync_with_pointer_parameter(const irep_idt &identifier, const exprt::operandst &arguments, const source_locationt &source_location, message_handlert &message_handler)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:25
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1840
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33