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/std_types.h>
18 #include <util/string_constant.h>
19 
20 #include <atomic>
21 
23  const irep_idt &identifier,
24  const exprt::operandst &arguments,
25  const source_locationt &source_location,
26  message_handlert &message_handler)
27 {
28  messaget log(message_handler);
29 
30  // adjust return type of function to match pointer subtype
31  if(arguments.size() < 2)
32  {
33  log.error().source_location = source_location;
34  log.error() << identifier << " expects at least two arguments"
35  << messaget::eom;
36  throw 0;
37  }
38 
39  const exprt &ptr_arg = arguments.front();
40 
41  if(ptr_arg.type().id() != ID_pointer)
42  {
43  log.error().source_location = source_location;
44  log.error() << identifier << " takes a pointer as first argument"
45  << messaget::eom;
46  throw 0;
47  }
48 
50  code_typet::parametert(ptr_arg.type().subtype())},
51  ptr_arg.type().subtype()};
52  t.make_ellipsis();
53  symbol_exprt result{identifier, std::move(t)};
54  result.add_source_location() = source_location;
55 
56  return result;
57 }
58 
60  const irep_idt &identifier,
61  const exprt::operandst &arguments,
62  const source_locationt &source_location,
63  message_handlert &message_handler)
64 {
65  messaget log(message_handler);
66 
67  // adjust return type of function to match pointer subtype
68  if(arguments.size() < 3)
69  {
70  log.error().source_location = source_location;
71  log.error() << identifier << " expects at least three arguments"
72  << messaget::eom;
73  throw 0;
74  }
75 
76  const exprt &ptr_arg = arguments.front();
77 
78  if(ptr_arg.type().id() != ID_pointer)
79  {
80  log.error().source_location = source_location;
81  log.error() << identifier << " takes a pointer as first argument"
82  << messaget::eom;
83  throw 0;
84  }
85 
86  const typet &subtype = ptr_arg.type().subtype();
87  typet sync_return_type = subtype;
88  if(identifier == ID___sync_bool_compare_and_swap)
89  sync_return_type = c_bool_type();
90 
92  code_typet::parametert(subtype),
93  code_typet::parametert(subtype)},
94  sync_return_type};
95  t.make_ellipsis();
96  symbol_exprt result{identifier, std::move(t)};
97  result.add_source_location() = source_location;
98 
99  return result;
100 }
101 
103  const irep_idt &identifier,
104  const exprt::operandst &arguments,
105  const source_locationt &source_location,
106  message_handlert &message_handler)
107 {
108  messaget log(message_handler);
109 
110  // adjust return type of function to match pointer subtype
111  if(arguments.empty())
112  {
113  log.error().source_location = source_location;
114  log.error() << identifier << " expects at least one argument"
115  << messaget::eom;
116  throw 0;
117  }
118 
119  const exprt &ptr_arg = arguments.front();
120 
121  if(ptr_arg.type().id() != ID_pointer)
122  {
123  log.error().source_location = source_location;
124  log.error() << identifier << " takes a pointer as first argument"
125  << messaget::eom;
126  throw 0;
127  }
128 
129  code_typet t{{code_typet::parametert(ptr_arg.type())}, void_type()};
130  t.make_ellipsis();
131  symbol_exprt result{identifier, std::move(t)};
132  result.add_source_location() = source_location;
133 
134  return result;
135 }
136 
138  const irep_idt &identifier,
139  const exprt::operandst &arguments,
140  const source_locationt &source_location,
141  message_handlert &message_handler)
142 {
143  // type __atomic_load_n(type *ptr, int memorder)
144  messaget log(message_handler);
145 
146  if(arguments.size() != 2)
147  {
148  log.error().source_location = source_location;
149  log.error() << identifier << " expects two arguments" << messaget::eom;
150  throw 0;
151  }
152 
153  const exprt &ptr_arg = arguments.front();
154 
155  if(ptr_arg.type().id() != ID_pointer)
156  {
157  log.error().source_location = source_location;
158  log.error() << identifier << " takes a pointer as first argument"
159  << messaget::eom;
160  throw 0;
161  }
162 
163  const code_typet t(
164  {code_typet::parametert(ptr_arg.type()),
166  ptr_arg.type().subtype());
167  symbol_exprt result(identifier, t);
168  result.add_source_location() = source_location;
169  return result;
170 }
171 
173  const irep_idt &identifier,
174  const exprt::operandst &arguments,
175  const source_locationt &source_location,
176  message_handlert &message_handler)
177 {
178  // void __atomic_store_n(type *ptr, type val, int memorder)
179  messaget log(message_handler);
180 
181  if(arguments.size() != 3)
182  {
183  log.error().source_location = source_location;
184  log.error() << identifier << " expects three arguments" << messaget::eom;
185  throw 0;
186  }
187 
188  const exprt &ptr_arg = arguments.front();
189 
190  if(ptr_arg.type().id() != ID_pointer)
191  {
192  log.error().source_location = source_location;
193  log.error() << identifier << " takes a pointer as first argument"
194  << messaget::eom;
195  throw 0;
196  }
197 
198  const code_typet t(
199  {code_typet::parametert(ptr_arg.type()),
200  code_typet::parametert(ptr_arg.type().subtype()),
202  void_type());
203  symbol_exprt result(identifier, t);
204  result.add_source_location() = source_location;
205  return result;
206 }
207 
209  const irep_idt &identifier,
210  const exprt::operandst &arguments,
211  const source_locationt &source_location,
212  message_handlert &message_handler)
213 {
214  // type __atomic_exchange_n(type *ptr, type val, int memorder)
215  messaget log(message_handler);
216 
217  if(arguments.size() != 3)
218  {
219  log.error().source_location = source_location;
220  log.error() << identifier << " expects three arguments" << messaget::eom;
221  throw 0;
222  }
223 
224  const exprt &ptr_arg = arguments.front();
225 
226  if(ptr_arg.type().id() != ID_pointer)
227  {
228  log.error().source_location = source_location;
229  log.error() << identifier << " takes a pointer as first argument"
230  << messaget::eom;
231  throw 0;
232  }
233 
234  const code_typet t(
235  {code_typet::parametert(ptr_arg.type()),
236  code_typet::parametert(ptr_arg.type().subtype()),
238  ptr_arg.type().subtype());
239  symbol_exprt result(identifier, t);
240  result.add_source_location() = source_location;
241  return result;
242 }
243 
245  const irep_idt &identifier,
246  const exprt::operandst &arguments,
247  const source_locationt &source_location,
248  message_handlert &message_handler)
249 {
250  // void __atomic_load(type *ptr, type *ret, int memorder)
251  // void __atomic_store(type *ptr, type *val, int memorder)
252  messaget log(message_handler);
253 
254  if(arguments.size() != 3)
255  {
256  log.error().source_location = source_location;
257  log.error() << identifier << " expects three arguments" << messaget::eom;
258  throw 0;
259  }
260 
261  if(arguments[0].type().id() != ID_pointer)
262  {
263  log.error().source_location = source_location;
264  log.error() << identifier << " takes a pointer as first argument"
265  << messaget::eom;
266  throw 0;
267  }
268 
269  if(arguments[1].type().id() != ID_pointer)
270  {
271  log.error().source_location = source_location;
272  log.error() << identifier << " takes a pointer as second argument"
273  << messaget::eom;
274  throw 0;
275  }
276 
277  const exprt &ptr_arg = arguments.front();
278 
279  const code_typet t(
280  {code_typet::parametert(ptr_arg.type()),
281  code_typet::parametert(ptr_arg.type()),
283  void_type());
284  symbol_exprt result(identifier, t);
285  result.add_source_location() = source_location;
286  return result;
287 }
288 
290  const irep_idt &identifier,
291  const exprt::operandst &arguments,
292  const source_locationt &source_location,
293  message_handlert &message_handler)
294 {
295  // void __atomic_exchange(type *ptr, type *val, type *ret, int memorder)
296  messaget log(message_handler);
297 
298  if(arguments.size() != 4)
299  {
300  log.error().source_location = source_location;
301  log.error() << identifier << " expects four arguments" << messaget::eom;
302  throw 0;
303  }
304 
305  if(arguments[0].type().id() != ID_pointer)
306  {
307  log.error().source_location = source_location;
308  log.error() << identifier << " takes a pointer as first argument"
309  << messaget::eom;
310  throw 0;
311  }
312 
313  if(arguments[1].type().id() != ID_pointer)
314  {
315  log.error().source_location = source_location;
316  log.error() << identifier << " takes a pointer as second argument"
317  << messaget::eom;
318  throw 0;
319  }
320 
321  if(arguments[2].type().id() != ID_pointer)
322  {
323  log.error().source_location = source_location;
324  log.error() << identifier << " takes a pointer as third argument"
325  << messaget::eom;
326  throw 0;
327  }
328 
329  const exprt &ptr_arg = arguments.front();
330 
331  const code_typet t(
332  {code_typet::parametert(ptr_arg.type()),
333  code_typet::parametert(ptr_arg.type()),
334  code_typet::parametert(ptr_arg.type()),
336  void_type());
337  symbol_exprt result(identifier, t);
338  result.add_source_location() = source_location;
339  return result;
340 }
341 
343  const irep_idt &identifier,
344  const exprt::operandst &arguments,
345  const source_locationt &source_location,
346  message_handlert &message_handler)
347 {
348  // bool __atomic_compare_exchange_n(type *ptr, type *expected, type
349  // desired, bool weak, int success_memorder, int failure_memorder)
350  // bool __atomic_compare_exchange(type *ptr, type *expected, type
351  // *desired, bool weak, int success_memorder, int failure_memorder)
352  messaget log(message_handler);
353 
354  if(arguments.size() != 6)
355  {
356  log.error().source_location = source_location;
357  log.error() << identifier << " expects six arguments" << messaget::eom;
358  throw 0;
359  }
360 
361  if(arguments[0].type().id() != ID_pointer)
362  {
363  log.error().source_location = source_location;
364  log.error() << identifier << " takes a pointer as first argument"
365  << messaget::eom;
366  throw 0;
367  }
368 
369  if(arguments[1].type().id() != ID_pointer)
370  {
371  log.error().source_location = source_location;
372  log.error() << identifier << " takes a pointer as second argument"
373  << messaget::eom;
374  throw 0;
375  }
376 
377  if(
378  identifier == ID___atomic_compare_exchange &&
379  arguments[2].type().id() != ID_pointer)
380  {
381  log.error().source_location = source_location;
382  log.error() << identifier << " takes a pointer as third argument"
383  << messaget::eom;
384  throw 0;
385  }
386 
387  const exprt &ptr_arg = arguments.front();
388 
389  code_typet::parameterst parameters;
390  parameters.push_back(code_typet::parametert(ptr_arg.type()));
391  parameters.push_back(code_typet::parametert(ptr_arg.type()));
392 
393  if(identifier == ID___atomic_compare_exchange)
394  parameters.push_back(code_typet::parametert(ptr_arg.type()));
395  else
396  parameters.push_back(code_typet::parametert(ptr_arg.type().subtype()));
397 
398  parameters.push_back(code_typet::parametert(c_bool_type()));
399  parameters.push_back(code_typet::parametert(signed_int_type()));
400  parameters.push_back(code_typet::parametert(signed_int_type()));
401  code_typet t(std::move(parameters), c_bool_type());
402  symbol_exprt result(identifier, t);
403  result.add_source_location() = source_location;
404  return result;
405 }
406 
408  const irep_idt &identifier,
409  const exprt::operandst &arguments,
410  const source_locationt &source_location,
411  message_handlert &message_handler)
412 {
413  messaget log(message_handler);
414 
415  if(arguments.size() != 3)
416  {
417  log.error().source_location = source_location;
418  log.error() << "__atomic_*_fetch primitives take three arguments"
419  << messaget::eom;
420  throw 0;
421  }
422 
423  const exprt &ptr_arg = arguments.front();
424 
425  if(ptr_arg.type().id() != ID_pointer)
426  {
427  log.error().source_location = source_location;
428  log.error()
429  << "__atomic_*_fetch primitives take a pointer as first argument"
430  << messaget::eom;
431  throw 0;
432  }
433 
434  code_typet t(
435  {code_typet::parametert(ptr_arg.type()),
436  code_typet::parametert(ptr_arg.type().subtype()),
438  ptr_arg.type().subtype());
439  symbol_exprt result(identifier, std::move(t));
440  result.add_source_location() = source_location;
441  return result;
442 }
443 
445  const irep_idt &identifier,
446  const exprt::operandst &arguments,
447  const source_locationt &source_location,
448  message_handlert &message_handler)
449 {
450  messaget log(message_handler);
451 
452  if(arguments.size() != 3)
453  {
454  log.error().source_location = source_location;
455  log.error() << "__atomic_fetch_* primitives take three arguments"
456  << messaget::eom;
457  throw 0;
458  }
459 
460  const exprt &ptr_arg = arguments.front();
461 
462  if(ptr_arg.type().id() != ID_pointer)
463  {
464  log.error().source_location = source_location;
465  log.error()
466  << "__atomic_fetch_* primitives take a pointer as first argument"
467  << messaget::eom;
468  throw 0;
469  }
470 
471  code_typet t(
472  {code_typet::parametert(ptr_arg.type()),
473  code_typet::parametert(ptr_arg.type().subtype()),
475  ptr_arg.type().subtype());
476  symbol_exprt result(identifier, std::move(t));
477  result.add_source_location() = source_location;
478  return result;
479 }
480 
482  const irep_idt &identifier,
483  const exprt::operandst &arguments,
484  const source_locationt &source_location)
485 {
486  // the arguments need not be type checked just yet, thus do not make
487  // assumptions that would require type checking
488 
489  if(
490  identifier == ID___sync_fetch_and_add ||
491  identifier == ID___sync_fetch_and_sub ||
492  identifier == ID___sync_fetch_and_or ||
493  identifier == ID___sync_fetch_and_and ||
494  identifier == ID___sync_fetch_and_xor ||
495  identifier == ID___sync_fetch_and_nand ||
496  identifier == ID___sync_add_and_fetch ||
497  identifier == ID___sync_sub_and_fetch ||
498  identifier == ID___sync_or_and_fetch ||
499  identifier == ID___sync_and_and_fetch ||
500  identifier == ID___sync_xor_and_fetch ||
501  identifier == ID___sync_nand_and_fetch ||
502  identifier == ID___sync_lock_test_and_set)
503  {
504  // These are polymorphic, see
505  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
507  identifier, arguments, source_location, get_message_handler());
508  }
509  else if(
510  identifier == ID___sync_bool_compare_and_swap ||
511  identifier == ID___sync_val_compare_and_swap)
512  {
513  // These are polymorphic, see
514  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
516  identifier, arguments, source_location, get_message_handler());
517  }
518  else if(identifier == ID___sync_lock_release)
519  {
520  // This is polymorphic, see
521  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
523  identifier, arguments, source_location, get_message_handler());
524  }
525  else if(identifier == ID___atomic_load_n)
526  {
527  // These are polymorphic
528  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
530  identifier, arguments, source_location, get_message_handler());
531  }
532  else if(identifier == ID___atomic_store_n)
533  {
534  // These are polymorphic
535  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
537  identifier, arguments, source_location, get_message_handler());
538  }
539  else if(identifier == ID___atomic_exchange_n)
540  {
541  // These are polymorphic
542  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
544  identifier, arguments, source_location, get_message_handler());
545  }
546  else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
547  {
548  // These are polymorphic
549  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
551  identifier, arguments, source_location, get_message_handler());
552  }
553  else if(identifier == ID___atomic_exchange)
554  {
555  // These are polymorphic
556  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
558  identifier, arguments, source_location, get_message_handler());
559  }
560  else if(
561  identifier == ID___atomic_compare_exchange_n ||
562  identifier == ID___atomic_compare_exchange)
563  {
564  // These are polymorphic
565  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
567  identifier, arguments, source_location, get_message_handler());
568  }
569  else if(
570  identifier == ID___atomic_add_fetch ||
571  identifier == ID___atomic_sub_fetch ||
572  identifier == ID___atomic_and_fetch ||
573  identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
574  identifier == ID___atomic_nand_fetch)
575  {
576  // These are polymorphic
577  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
579  identifier, arguments, source_location, get_message_handler());
580  }
581  else if(
582  identifier == ID___atomic_fetch_add ||
583  identifier == ID___atomic_fetch_sub ||
584  identifier == ID___atomic_fetch_and ||
585  identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
586  identifier == ID___atomic_fetch_nand)
587  {
588  // These are polymorphic
589  // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
591  identifier, arguments, source_location, get_message_handler());
592  }
593 
594  return {};
595 }
596 
598  const irep_idt &identifier,
599  const typet &type,
600  const source_locationt &source_location,
601  symbol_tablet &symbol_table)
602 {
603  symbolt symbol;
604  symbol.name = id2string(identifier) + "::1::result";
605  symbol.base_name = "result";
606  symbol.type = type;
607  symbol.mode = ID_C;
608  symbol.location = source_location;
609  symbol.is_file_local = true;
610  symbol.is_lvalue = true;
611  symbol.is_thread_local = true;
612 
613  symbol_table.add(symbol);
614 
615  return symbol;
616 }
617 
619  const irep_idt &identifier,
620  const irep_idt &identifier_with_type,
621  const code_typet &code_type,
622  const source_locationt &source_location,
623  const std::vector<symbol_exprt> &parameter_exprs,
624  symbol_tablet &symbol_table,
625  code_blockt &block)
626 {
627  // type __sync_fetch_and_OP(type *ptr, type value, ...)
628  // { type result; result = *ptr; *ptr = result OP value; return result; }
629  const typet &type = code_type.return_type();
630 
631  const symbol_exprt result =
632  result_symbol(identifier_with_type, type, source_location, symbol_table)
633  .symbol_expr();
634  block.add(codet{ID_decl_block, {code_declt{result}}});
635 
636  // place operations on *ptr in an atomic section
638  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
639  {},
640  code_typet{{}, void_type()},
641  source_location}});
642 
643  // build *ptr
644  const dereference_exprt deref_ptr{parameter_exprs[0]};
645 
646  block.add(code_assignt{result, deref_ptr});
647 
648  // build *ptr = result OP arguments[1];
649  irep_idt op_id = identifier == ID___atomic_fetch_add
650  ? ID_plus
651  : identifier == ID___atomic_fetch_sub
652  ? ID_minus
653  : identifier == ID___atomic_fetch_or
654  ? ID_bitor
655  : identifier == ID___atomic_fetch_and
656  ? ID_bitand
657  : identifier == ID___atomic_fetch_xor
658  ? ID_bitxor
659  : identifier == ID___atomic_fetch_nand
660  ? ID_bitnand
661  : ID_nil;
662  binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
663  block.add(code_assignt{deref_ptr, std::move(op_expr)});
664 
666  symbol_exprt::typeless("__atomic_thread_fence"),
667  {parameter_exprs[2]},
668  typet{},
669  source_location}});
670 
673  {},
674  code_typet{{}, void_type()},
675  source_location}});
676 
677  block.add(code_returnt{result});
678 }
679 
681  const irep_idt &identifier,
682  const irep_idt &identifier_with_type,
683  const code_typet &code_type,
684  const source_locationt &source_location,
685  const std::vector<symbol_exprt> &parameter_exprs,
686  symbol_tablet &symbol_table,
687  code_blockt &block)
688 {
689  // type __sync_OP_and_fetch(type *ptr, type value, ...)
690  // { type result; result = *ptr OP value; *ptr = result; return result; }
691  const typet &type = code_type.return_type();
692 
693  const symbol_exprt result =
694  result_symbol(identifier_with_type, type, source_location, symbol_table)
695  .symbol_expr();
696  block.add(codet{ID_decl_block, {code_declt{result}}});
697 
698  // place operations on *ptr in an atomic section
700  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
701  {},
702  code_typet{{}, void_type()},
703  source_location}});
704 
705  // build *ptr
706  const dereference_exprt deref_ptr{parameter_exprs[0]};
707 
708  // build result = *ptr OP arguments[1];
709  irep_idt op_id = identifier == ID___atomic_add_fetch
710  ? ID_plus
711  : identifier == ID___atomic_sub_fetch
712  ? ID_minus
713  : identifier == ID___atomic_or_fetch
714  ? ID_bitor
715  : identifier == ID___atomic_and_fetch
716  ? ID_bitand
717  : identifier == ID___atomic_xor_fetch
718  ? ID_bitxor
719  : identifier == ID___atomic_nand_fetch
720  ? ID_bitnand
721  : ID_nil;
722  binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
723  block.add(code_assignt{result, std::move(op_expr)});
724 
725  block.add(code_assignt{deref_ptr, result});
726 
727  // this instruction implies an mfence, i.e., WRfence
729  symbol_exprt::typeless("__atomic_thread_fence"),
730  {parameter_exprs[2]},
731  typet{},
732  source_location}});
733 
736  {},
737  code_typet{{}, void_type()},
738  source_location}});
739 
740  block.add(code_returnt{result});
741 }
742 
744  const irep_idt &identifier,
745  const irep_idt &identifier_with_type,
746  const code_typet &code_type,
747  const source_locationt &source_location,
748  const std::vector<symbol_exprt> &parameter_exprs,
749  code_blockt &block)
750 {
751  // implement by calling their __atomic_ counterparts with memorder SEQ_CST
752  std::string atomic_name = "__atomic_" + id2string(identifier).substr(7);
753  atomic_name.replace(atomic_name.find("_and_"), 5, "_");
754 
755  exprt::operandst arguments{
756  parameter_exprs[0],
757  parameter_exprs[1],
758  from_integer(std::memory_order_seq_cst, signed_int_type())};
759 
760  block.add(code_returnt{
762  std::move(arguments),
763  typet{},
764  source_location}});
765 }
766 
768  const irep_idt &identifier_with_type,
769  const code_typet &code_type,
770  const source_locationt &source_location,
771  const std::vector<symbol_exprt> &parameter_exprs,
772  code_blockt &block)
773 {
774  // These builtins perform an atomic compare and swap. That is, if the
775  // current value of *ptr is oldval, then write newval into *ptr. The
776  // "bool" version returns true if the comparison is successful and
777  // newval was written. The "val" version returns the contents of *ptr
778  // before the operation.
779 
780  // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
781 
783  symbol_exprt::typeless(ID___atomic_compare_exchange),
784  {parameter_exprs[0],
785  address_of_exprt{parameter_exprs[1]},
786  address_of_exprt{parameter_exprs[2]},
788  from_integer(std::memory_order_seq_cst, signed_int_type()),
789  from_integer(std::memory_order_seq_cst, signed_int_type())},
790  typet{},
791  source_location}});
792 }
793 
795  const irep_idt &identifier_with_type,
796  const code_typet &code_type,
797  const source_locationt &source_location,
798  const std::vector<symbol_exprt> &parameter_exprs,
799  symbol_tablet &symbol_table,
800  code_blockt &block)
801 {
802  // type __sync_val_compare_and_swap(type *ptr, type old, type new, ...)
803  // { type result = *ptr; if(result == old) *ptr = new; return result; }
804  const typet &type = code_type.return_type();
805 
806  const symbol_exprt result =
807  result_symbol(identifier_with_type, type, source_location, symbol_table)
808  .symbol_expr();
809  block.add(codet{ID_decl_block, {code_declt{result}}});
810 
811  // place operations on *ptr in an atomic section
813  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
814  {},
815  code_typet{{}, void_type()},
816  source_location}});
817 
818  // build *ptr
819  const dereference_exprt deref_ptr{parameter_exprs[0]};
820 
821  block.add(code_assignt{result, deref_ptr});
822 
823  code_assignt assign{deref_ptr, parameter_exprs[2]};
824  assign.add_source_location() = source_location;
825  block.add(code_ifthenelset{equal_exprt{result, parameter_exprs[1]},
826  std::move(assign)});
827 
828  // this instruction implies an mfence, i.e., WRfence
831  {string_constantt{ID_WRfence}},
832  typet{},
833  source_location}});
834 
837  {},
838  code_typet{{}, void_type()},
839  source_location}});
840 
841  block.add(code_returnt{result});
842 }
843 
845  const irep_idt &identifier_with_type,
846  const code_typet &code_type,
847  const source_locationt &source_location,
848  const std::vector<symbol_exprt> &parameter_exprs,
849  symbol_tablet &symbol_table,
850  code_blockt &block)
851 {
852  // type __sync_lock_test_and_set (type *ptr, type value, ...)
853 
854  // This builtin, as described by Intel, is not a traditional
855  // test-and-set operation, but rather an atomic exchange operation.
856  // It writes value into *ptr, and returns the previous contents of
857  // *ptr. Many targets have only minimal support for such locks, and
858  // do not support a full exchange operation. In this case, a target
859  // may support reduced functionality here by which the only valid
860  // value to store is the immediate constant 1. The exact value
861  // actually stored in *ptr is implementation defined.
862  const typet &type = code_type.return_type();
863 
864  const symbol_exprt result =
865  result_symbol(identifier_with_type, type, source_location, symbol_table)
866  .symbol_expr();
867  block.add(codet{ID_decl_block, {code_declt{result}}});
868 
869  // place operations on *ptr in an atomic section
871  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
872  {},
873  code_typet{{}, void_type()},
874  source_location}});
875 
876  // build *ptr
877  const dereference_exprt deref_ptr{parameter_exprs[0]};
878 
879  block.add(code_assignt{result, deref_ptr});
880 
881  block.add(code_assignt{deref_ptr, parameter_exprs[1]});
882 
883  // This built-in function is not a full barrier, but rather an acquire
884  // barrier.
887  {string_constantt{ID_RRfence}, {string_constantt{ID_RRfence}}},
888  typet{},
889  source_location}});
890 
893  {},
894  code_typet{{}, void_type()},
895  source_location}});
896 
897  block.add(code_returnt{result});
898 }
899 
901  const irep_idt &identifier_with_type,
902  const code_typet &code_type,
903  const source_locationt &source_location,
904  const std::vector<symbol_exprt> &parameter_exprs,
905  code_blockt &block)
906 {
907  // void __sync_lock_release (type *ptr, ...)
908 
909  // This built-in function releases the lock acquired by
910  // __sync_lock_test_and_set. Normally this means writing the constant 0 to
911  // *ptr.
912  const typet &type = to_pointer_type(parameter_exprs[0].type()).subtype();
913 
914  // place operations on *ptr in an atomic section
916  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
917  {},
918  code_typet{{}, void_type()},
919  source_location}});
920 
921  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
923  from_integer(0, signed_int_type()), type)});
924 
925  // This built-in function is not a full barrier, but rather a release
926  // barrier.
929  {string_constantt{ID_WRfence}, {string_constantt{ID_WWfence}}},
930  typet{},
931  source_location}});
932 
935  {},
936  code_typet{{}, void_type()},
937  source_location}});
938 }
939 
941  const irep_idt &identifier_with_type,
942  const code_typet &code_type,
943  const source_locationt &source_location,
944  const std::vector<symbol_exprt> &parameter_exprs,
945  code_blockt &block)
946 {
947  // void __atomic_load (type *ptr, type *ret, int memorder)
948  // This is the generic version of an atomic load. It returns the contents of
949  // *ptr in *ret.
950 
952  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
953  {},
954  code_typet{{}, void_type()},
955  source_location}});
956 
957  block.add(code_assignt{dereference_exprt{parameter_exprs[1]},
958  dereference_exprt{parameter_exprs[0]}});
959 
961  symbol_exprt::typeless("__atomic_thread_fence"),
962  {parameter_exprs[2]},
963  typet{},
964  source_location}});
965 
968  {},
969  code_typet{{}, void_type()},
970  source_location}});
971 }
972 
974  const irep_idt &identifier_with_type,
975  const code_typet &code_type,
976  const source_locationt &source_location,
977  const std::vector<symbol_exprt> &parameter_exprs,
978  symbol_tablet &symbol_table,
979  code_blockt &block)
980 {
981  // type __atomic_load_n (type *ptr, int memorder)
982  // This built-in function implements an atomic load operation. It returns
983  // the contents of *ptr.
984  const typet &type = code_type.return_type();
985 
986  const symbol_exprt result =
987  result_symbol(identifier_with_type, type, source_location, symbol_table)
988  .symbol_expr();
989  block.add(codet{ID_decl_block, {code_declt{result}}});
990 
992  symbol_exprt::typeless(ID___atomic_load),
993  {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
994  typet{},
995  source_location}});
996 
997  block.add(code_returnt{result});
998 }
999 
1001  const irep_idt &identifier_with_type,
1002  const code_typet &code_type,
1003  const source_locationt &source_location,
1004  const std::vector<symbol_exprt> &parameter_exprs,
1005  code_blockt &block)
1006 {
1007  // void __atomic_store (type *ptr, type *val, int memorder)
1008  // This is the generic version of an atomic store. It stores the value of
1009  // *val into *ptr.
1010 
1012  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1013  {},
1014  code_typet{{}, void_type()},
1015  source_location}});
1016 
1017  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
1018  dereference_exprt{parameter_exprs[1]}});
1019 
1021  symbol_exprt::typeless("__atomic_thread_fence"),
1022  {parameter_exprs[2]},
1023  typet{},
1024  source_location}});
1025 
1027  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1028  {},
1029  code_typet{{}, void_type()},
1030  source_location}});
1031 }
1032 
1034  const irep_idt &identifier_with_type,
1035  const code_typet &code_type,
1036  const source_locationt &source_location,
1037  const std::vector<symbol_exprt> &parameter_exprs,
1038  code_blockt &block)
1039 {
1040  // void __atomic_store_n (type *ptr, type val, int memorder)
1041  // This built-in function implements an atomic store operation. It writes
1042  // val into *ptr.
1043 
1044  block.add(code_expressiont{
1046  {parameter_exprs[0],
1047  address_of_exprt{parameter_exprs[1]},
1048  parameter_exprs[2]},
1049  typet{},
1050  source_location}});
1051 }
1052 
1054  const irep_idt &identifier_with_type,
1055  const code_typet &code_type,
1056  const source_locationt &source_location,
1057  const std::vector<symbol_exprt> &parameter_exprs,
1058  code_blockt &block)
1059 {
1060  // void __atomic_exchange (type *ptr, type *val, type *ret, int memorder)
1061  // This is the generic version of an atomic exchange. It stores the contents
1062  // of *val into *ptr. The original value of *ptr is copied into *ret.
1063 
1065  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1066  {},
1067  code_typet{{}, void_type()},
1068  source_location}});
1069 
1070  block.add(code_assignt{dereference_exprt{parameter_exprs[2]},
1071  dereference_exprt{parameter_exprs[0]}});
1072  block.add(code_assignt{dereference_exprt{parameter_exprs[0]},
1073  dereference_exprt{parameter_exprs[1]}});
1074 
1076  symbol_exprt::typeless("__atomic_thread_fence"),
1077  {parameter_exprs[3]},
1078  typet{},
1079  source_location}});
1080 
1082  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1083  {},
1084  code_typet{{}, void_type()},
1085  source_location}});
1086 }
1087 
1089  const irep_idt &identifier_with_type,
1090  const code_typet &code_type,
1091  const source_locationt &source_location,
1092  const std::vector<symbol_exprt> &parameter_exprs,
1093  symbol_tablet &symbol_table,
1094  code_blockt &block)
1095 {
1096  // type __atomic_exchange_n (type *ptr, type val, int memorder)
1097  // This built-in function implements an atomic exchange operation. It writes
1098  // val into *ptr, and returns the previous contents of *ptr.
1099  const typet &type = code_type.return_type();
1100 
1101  const symbol_exprt result =
1102  result_symbol(identifier_with_type, type, source_location, symbol_table)
1103  .symbol_expr();
1104  block.add(codet{ID_decl_block, {code_declt{result}}});
1105 
1107  symbol_exprt::typeless(ID___atomic_exchange),
1108  {parameter_exprs[0],
1109  address_of_exprt{parameter_exprs[1]},
1110  address_of_exprt{result},
1111  parameter_exprs[2]},
1112  typet{},
1113  source_location}});
1114 
1115  block.add(code_returnt{result});
1116 }
1117 
1119  const irep_idt &identifier_with_type,
1120  const code_typet &code_type,
1121  const source_locationt &source_location,
1122  const std::vector<symbol_exprt> &parameter_exprs,
1123  symbol_tablet &symbol_table,
1124  code_blockt &block)
1125 {
1126  // bool __atomic_compare_exchange (type *ptr, type *expected, type *desired,
1127  // bool weak, int success_memorder, int failure_memorder)
1128  // This built-in function implements an atomic compare and exchange
1129  // operation. This compares the contents of *ptr with the contents of
1130  // *expected. If equal, the operation is a read-modify-write operation that
1131  // writes *desired into *ptr. If they are not equal, the operation is a read
1132  // and the current contents of *ptr are written into *expected. weak is true
1133  // for weak compare_exchange, which may fail spuriously, and false for the
1134  // strong variation, which never fails spuriously. Many targets only offer
1135  // the strong variation and ignore the parameter.
1136 
1137  const symbol_exprt result =
1138  result_symbol(
1139  identifier_with_type, c_bool_type(), source_location, symbol_table)
1140  .symbol_expr();
1141  block.add(codet{ID_decl_block, {code_declt{result}}});
1142 
1143  // place operations on *ptr in an atomic section
1145  symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1146  {},
1147  code_typet{{}, void_type()},
1148  source_location}});
1149 
1150  // build *ptr
1151  const dereference_exprt deref_ptr{parameter_exprs[0]};
1152 
1153  block.add(code_assignt{
1154  result,
1156  equal_exprt{deref_ptr, dereference_exprt{parameter_exprs[1]}},
1157  result.type())});
1158 
1159  // we never fail spuriously, and ignore parameter_exprs[3]
1160  code_assignt assign{deref_ptr, dereference_exprt{parameter_exprs[2]}};
1161  assign.add_source_location() = source_location;
1163  symbol_exprt::typeless("__atomic_thread_fence"),
1164  {parameter_exprs[4]},
1165  typet{},
1166  source_location}};
1167  success_fence.add_source_location() = source_location;
1168 
1170  symbol_exprt::typeless("__atomic_thread_fence"),
1171  {parameter_exprs[5]},
1172  typet{},
1173  source_location}};
1174  failure_fence.add_source_location() = source_location;
1175 
1176  block.add(
1177  code_ifthenelset{result,
1178  code_blockt{{std::move(assign), std::move(success_fence)}},
1179  std::move(failure_fence)});
1180 
1182  symbol_exprt::typeless(CPROVER_PREFIX "atomic_end"),
1183  {},
1184  code_typet{{}, void_type()},
1185  source_location}});
1186 
1187  block.add(code_returnt{result});
1188 }
1189 
1191  const irep_idt &identifier_with_type,
1192  const code_typet &code_type,
1193  const source_locationt &source_location,
1194  const std::vector<symbol_exprt> &parameter_exprs,
1195  code_blockt &block)
1196 {
1197  // bool __atomic_compare_exchange_n (type *ptr, type *expected, type
1198  // desired, bool weak, int success_memorder, int failure_memorder)
1199 
1201  symbol_exprt::typeless(ID___atomic_compare_exchange),
1202  {parameter_exprs[0],
1203  parameter_exprs[1],
1204  address_of_exprt{parameter_exprs[2]},
1205  parameter_exprs[3],
1206  parameter_exprs[4],
1207  parameter_exprs[5]},
1208  typet{},
1209  source_location}});
1210 }
1211 
1213  const irep_idt &identifier,
1214  const symbol_exprt &function_symbol)
1215 {
1216  const irep_idt &identifier_with_type = function_symbol.get_identifier();
1217  const code_typet &code_type = to_code_type(function_symbol.type());
1218  const source_locationt &source_location = function_symbol.source_location();
1219 
1220  std::vector<symbol_exprt> parameter_exprs;
1221  parameter_exprs.reserve(code_type.parameters().size());
1222  for(const auto &parameter : code_type.parameters())
1223  {
1224  parameter_exprs.push_back(lookup(parameter.get_identifier()).symbol_expr());
1225  }
1226 
1227  code_blockt block;
1228 
1229  if(
1230  identifier == ID___atomic_fetch_add ||
1231  identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1232  identifier == ID___atomic_fetch_and ||
1233  identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1234  {
1236  identifier,
1237  identifier_with_type,
1238  code_type,
1239  source_location,
1240  parameter_exprs,
1241  symbol_table,
1242  block);
1243  }
1244  else if(
1245  identifier == ID___atomic_add_fetch ||
1246  identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1247  identifier == ID___atomic_and_fetch ||
1248  identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1249  {
1251  identifier,
1252  identifier_with_type,
1253  code_type,
1254  source_location,
1255  parameter_exprs,
1256  symbol_table,
1257  block);
1258  }
1259  else if(
1260  identifier == ID___sync_fetch_and_add ||
1261  identifier == ID___sync_fetch_and_sub ||
1262  identifier == ID___sync_fetch_and_or ||
1263  identifier == ID___sync_fetch_and_and ||
1264  identifier == ID___sync_fetch_and_xor ||
1265  identifier == ID___sync_fetch_and_nand ||
1266  identifier == ID___sync_add_and_fetch ||
1267  identifier == ID___sync_sub_and_fetch ||
1268  identifier == ID___sync_or_and_fetch ||
1269  identifier == ID___sync_and_and_fetch ||
1270  identifier == ID___sync_xor_and_fetch ||
1271  identifier == ID___sync_nand_and_fetch)
1272  {
1274  identifier,
1275  identifier_with_type,
1276  code_type,
1277  source_location,
1278  parameter_exprs,
1279  block);
1280  }
1281  else if(identifier == ID___sync_bool_compare_and_swap)
1282  {
1284  identifier_with_type, code_type, source_location, parameter_exprs, block);
1285  }
1286  else if(identifier == ID___sync_val_compare_and_swap)
1287  {
1289  identifier_with_type,
1290  code_type,
1291  source_location,
1292  parameter_exprs,
1293  symbol_table,
1294  block);
1295  }
1296  else if(identifier == ID___sync_lock_test_and_set)
1297  {
1299  identifier_with_type,
1300  code_type,
1301  source_location,
1302  parameter_exprs,
1303  symbol_table,
1304  block);
1305  }
1306  else if(identifier == ID___sync_lock_release)
1307  {
1309  identifier_with_type, code_type, source_location, parameter_exprs, block);
1310  }
1311  else if(identifier == ID___atomic_load)
1312  {
1314  identifier_with_type, code_type, source_location, parameter_exprs, block);
1315  }
1316  else if(identifier == ID___atomic_load_n)
1317  {
1319  identifier_with_type,
1320  code_type,
1321  source_location,
1322  parameter_exprs,
1323  symbol_table,
1324  block);
1325  }
1326  else if(identifier == ID___atomic_store)
1327  {
1329  identifier_with_type, code_type, source_location, parameter_exprs, block);
1330  }
1331  else if(identifier == ID___atomic_store_n)
1332  {
1334  identifier_with_type, code_type, source_location, parameter_exprs, block);
1335  }
1336  else if(identifier == ID___atomic_exchange)
1337  {
1339  identifier_with_type, code_type, source_location, parameter_exprs, block);
1340  }
1341  else if(identifier == ID___atomic_exchange_n)
1342  {
1344  identifier_with_type,
1345  code_type,
1346  source_location,
1347  parameter_exprs,
1348  symbol_table,
1349  block);
1350  }
1351  else if(identifier == ID___atomic_compare_exchange)
1352  {
1354  identifier_with_type,
1355  code_type,
1356  source_location,
1357  parameter_exprs,
1358  symbol_table,
1359  block);
1360  }
1361  else if(identifier == ID___atomic_compare_exchange_n)
1362  {
1364  identifier_with_type, code_type, source_location, parameter_exprs, block);
1365  }
1366  else
1367  {
1368  UNREACHABLE;
1369  }
1370 
1371  for(auto &statement : block.statements())
1372  statement.add_source_location() = source_location;
1373 
1374  return block;
1375 }
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:504
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:59
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:170
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:2021
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:244
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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:973
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:407
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:289
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:1033
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:1088
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
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:444
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:743
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:1118
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
side_effect_expr_function_callt
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:2117
symbol_exprt::typeless
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition: std_expr.h:101
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:208
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:844
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:402
namespacet::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
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:172
string_constant.h
exprt
Base class for all expressions.
Definition: expr.h:53
binary_exprt
A base class for binary expressions.
Definition: std_expr.h:601
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
messaget::eom
static eomt eom
Definition: message.h:297
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
string_constantt
Definition: string_constant.h:16
equal_exprt
Equality.
Definition: std_expr.h:1190
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:746
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:794
code_blockt::statements
code_operandst & statements()
Definition: std_code.h:178
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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:946
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:597
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:680
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:1053
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:1190
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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:1212
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
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:900
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:122
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:481
c_typecheck_baset::symbol_table
symbol_tablet & symbol_table
Definition: c_typecheck_base.h:67
code_typet
Base type of functions.
Definition: std_types.h:736
irept::id
const irep_idt & id() const
Definition: irep.h:418
message_handlert
Definition: message.h:28
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
code_blockt::add
void add(const codet &code)
Definition: std_code.h:208
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1526
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:102
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
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:342
source_locationt
Definition: source_location.h:20
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:1310
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:137
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
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:940
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:1000
code_typet::parametert
Definition: std_types.h:753
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:767
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
symbolt::is_file_local
bool is_file_local
Definition: symbol.h:66
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:2786
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
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:618
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
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:22
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1810
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35