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