cprover
c_typecheck_gcc_polymorphic_builtins.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: ANSI-C Language Type Checking
4
5Author: 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>
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"
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"
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"
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"
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
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
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
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
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
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
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
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
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
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 =
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
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
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,
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,
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,
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,
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,
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,
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,
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 {
1385 }
1386
1387 for(auto &statement : block.statements())
1388 statement.add_source_location() = source_location;
1389
1390 return block;
1391}
1392
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
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
code_operandst & statements()
Definition: std_code.h:138
void add(const codet &code)
Definition: std_code.h:168
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:542
const parameterst & parameters() const
Definition: std_types.h:655
const typet & return_type() const
Definition: std_types.h:645
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
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