cprover
Loading...
Searching...
No Matches
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 <util/arith_tools.h>
13#include <util/c_types.h>
14#include <util/cprover_prefix.h>
15#include <util/pointer_expr.h>
16#include <util/std_types.h>
19
21
22#include "c_expr.h"
23#include "c_typecheck_base.h"
24
25#include <atomic>
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
58 pointer_type.base_type()};
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
99 code_typet::parametert(base_type),
100 code_typet::parametert(base_type)},
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()),
209 code_typet::parametert(base_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()),
247 code_typet::parametert(base_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
493std::optional<symbol_exprt>
495 const irep_idt &identifier,
496 const exprt::operandst &arguments,
497 const source_locationt &source_location)
498{
499 // the arguments need not be type checked just yet, thus do not make
500 // assumptions that would require type checking
501
502 if(
503 identifier == ID___sync_fetch_and_add ||
504 identifier == ID___sync_fetch_and_sub ||
505 identifier == ID___sync_fetch_and_or ||
506 identifier == ID___sync_fetch_and_and ||
507 identifier == ID___sync_fetch_and_xor ||
508 identifier == ID___sync_fetch_and_nand ||
509 identifier == ID___sync_add_and_fetch ||
510 identifier == ID___sync_sub_and_fetch ||
511 identifier == ID___sync_or_and_fetch ||
512 identifier == ID___sync_and_and_fetch ||
513 identifier == ID___sync_xor_and_fetch ||
514 identifier == ID___sync_nand_and_fetch ||
515 identifier == ID___sync_lock_test_and_set)
516 {
517 // These are polymorphic, see
518 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
520 identifier, arguments, source_location, get_message_handler());
521 }
522 else if(
523 identifier == ID___sync_bool_compare_and_swap ||
524 identifier == ID___sync_val_compare_and_swap)
525 {
526 // These are polymorphic, see
527 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
529 identifier, arguments, source_location, get_message_handler());
530 }
531 else if(identifier == ID___sync_lock_release)
532 {
533 // This is polymorphic, see
534 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html
536 identifier, arguments, source_location, get_message_handler());
537 }
538 else if(identifier == ID___atomic_load_n)
539 {
540 // These are polymorphic
541 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
543 identifier, arguments, source_location, get_message_handler());
544 }
545 else if(identifier == ID___atomic_store_n)
546 {
547 // These are polymorphic
548 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
550 identifier, arguments, source_location, get_message_handler());
551 }
552 else if(identifier == ID___atomic_exchange_n)
553 {
554 // These are polymorphic
555 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
557 identifier, arguments, source_location, get_message_handler());
558 }
559 else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
560 {
561 // These are polymorphic
562 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
564 identifier, arguments, source_location, get_message_handler());
565 }
566 else if(identifier == ID___atomic_exchange)
567 {
568 // These are polymorphic
569 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
571 identifier, arguments, source_location, get_message_handler());
572 }
573 else if(
574 identifier == ID___atomic_compare_exchange_n ||
575 identifier == ID___atomic_compare_exchange)
576 {
577 // These are polymorphic
578 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
580 identifier, arguments, source_location, get_message_handler());
581 }
582 else if(
583 identifier == ID___atomic_add_fetch ||
584 identifier == ID___atomic_sub_fetch ||
585 identifier == ID___atomic_and_fetch ||
586 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
587 identifier == ID___atomic_nand_fetch)
588 {
589 // These are polymorphic
590 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
592 identifier, arguments, source_location, get_message_handler());
593 }
594 else if(
595 identifier == ID___atomic_fetch_add ||
596 identifier == ID___atomic_fetch_sub ||
597 identifier == ID___atomic_fetch_and ||
598 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
599 identifier == ID___atomic_fetch_nand)
600 {
601 // These are polymorphic
602 // https://gcc.gnu.org/onlinedocs/gcc/_005f_005fatomic-Builtins.html
604 identifier, arguments, source_location, get_message_handler());
605 }
606
607 return {};
608}
609
611 const irep_idt &identifier,
612 const typet &type,
613 const source_locationt &source_location,
614 symbol_table_baset &symbol_table)
615{
616 symbolt symbol{id2string(identifier) + "::1::result", type, ID_C};
617 symbol.base_name = "result";
618 symbol.location = source_location;
619 symbol.is_file_local = true;
620 symbol.is_lvalue = true;
621 symbol.is_thread_local = true;
622
623 symbol_table.add(symbol);
624
625 return symbol;
626}
627
629 const irep_idt &identifier,
630 const irep_idt &identifier_with_type,
631 const code_typet &code_type,
632 const source_locationt &source_location,
633 const std::vector<symbol_exprt> &parameter_exprs,
634 symbol_table_baset &symbol_table,
635 code_blockt &block)
636{
637 // type __sync_fetch_and_OP(type *ptr, type value, ...)
638 // { type result; result = *ptr; *ptr = result OP value; return result; }
639 const typet &type = code_type.return_type();
640
641 const symbol_exprt result =
642 result_symbol(identifier_with_type, type, source_location, symbol_table)
643 .symbol_expr();
644 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
645
646 // place operations on *ptr in an atomic section
649 {},
650 code_typet{{}, void_type()},
651 source_location}});
652
653 // build *ptr
654 const dereference_exprt deref_ptr{parameter_exprs[0]};
655
656 block.add(code_frontend_assignt{result, deref_ptr});
657
658 // build *ptr = result OP arguments[1];
659 irep_idt op_id = identifier == ID___atomic_fetch_add
660 ? ID_plus
661 : identifier == ID___atomic_fetch_sub
662 ? ID_minus
663 : identifier == ID___atomic_fetch_or
664 ? ID_bitor
665 : identifier == ID___atomic_fetch_and
666 ? ID_bitand
667 : identifier == ID___atomic_fetch_xor
668 ? ID_bitxor
669 : identifier == ID___atomic_fetch_nand
670 ? ID_bitnand
671 : ID_nil;
672 binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
673 block.add(code_frontend_assignt{deref_ptr, std::move(op_expr)});
674
676 symbol_exprt::typeless("__atomic_thread_fence")
677 .with_source_location(source_location),
678 {parameter_exprs[2]},
679 typet{},
680 source_location}});
681
684 {},
685 code_typet{{}, void_type()},
686 source_location}});
687
688 block.add(code_returnt{result});
689}
690
692 const irep_idt &identifier,
693 const irep_idt &identifier_with_type,
694 const code_typet &code_type,
695 const source_locationt &source_location,
696 const std::vector<symbol_exprt> &parameter_exprs,
697 symbol_table_baset &symbol_table,
698 code_blockt &block)
699{
700 // type __sync_OP_and_fetch(type *ptr, type value, ...)
701 // { type result; result = *ptr OP value; *ptr = result; return result; }
702 const typet &type = code_type.return_type();
703
704 const symbol_exprt result =
705 result_symbol(identifier_with_type, type, source_location, symbol_table)
706 .symbol_expr();
707 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
708
709 // place operations on *ptr in an atomic section
712 {},
713 code_typet{{}, void_type()},
714 source_location}});
715
716 // build *ptr
717 const dereference_exprt deref_ptr{parameter_exprs[0]};
718
719 // build result = *ptr OP arguments[1];
720 irep_idt op_id = identifier == ID___atomic_add_fetch
721 ? ID_plus
722 : identifier == ID___atomic_sub_fetch
723 ? ID_minus
724 : identifier == ID___atomic_or_fetch
725 ? ID_bitor
726 : identifier == ID___atomic_and_fetch
727 ? ID_bitand
728 : identifier == ID___atomic_xor_fetch
729 ? ID_bitxor
730 : identifier == ID___atomic_nand_fetch
731 ? ID_bitnand
732 : ID_nil;
733 binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
734 block.add(code_frontend_assignt{result, std::move(op_expr)});
735
736 block.add(code_frontend_assignt{deref_ptr, result});
737
738 // this instruction implies an mfence, i.e., WRfence
740 symbol_exprt::typeless("__atomic_thread_fence")
741 .with_source_location(source_location),
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
773 symbol_exprt::typeless(atomic_name).with_source_location(source_location),
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 .with_source_location(source_location),
797 {parameter_exprs[0],
798 address_of_exprt{parameter_exprs[1]},
799 address_of_exprt{parameter_exprs[2]},
801 from_integer(std::memory_order_seq_cst, signed_int_type()),
802 from_integer(std::memory_order_seq_cst, signed_int_type())},
803 typet{},
804 source_location}});
805}
806
808 const irep_idt &identifier_with_type,
809 const code_typet &code_type,
810 const source_locationt &source_location,
811 const std::vector<symbol_exprt> &parameter_exprs,
812 symbol_table_baset &symbol_table,
813 code_blockt &block)
814{
815 // type __sync_val_compare_and_swap(type *ptr, type old, type new, ...)
816 // { type result = *ptr; if(result == old) *ptr = new; return result; }
817 const typet &type = code_type.return_type();
818
819 const symbol_exprt result =
820 result_symbol(identifier_with_type, type, source_location, symbol_table)
821 .symbol_expr();
822 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
823
824 // place operations on *ptr in an atomic section
827 {},
828 code_typet{{}, void_type()},
829 source_location}});
830
831 // build *ptr
832 const dereference_exprt deref_ptr{parameter_exprs[0]};
833
834 block.add(code_frontend_assignt{result, deref_ptr});
835
836 code_frontend_assignt assign{deref_ptr, parameter_exprs[2]};
837 assign.add_source_location() = source_location;
838 block.add(code_ifthenelset{equal_exprt{result, parameter_exprs[1]},
839 std::move(assign)});
840
841 // this instruction implies an mfence, i.e., WRfence
844 {string_constantt{ID_WRfence}},
845 typet{},
846 source_location}});
847
850 {},
851 code_typet{{}, void_type()},
852 source_location}});
853
854 block.add(code_returnt{result});
855}
856
858 const irep_idt &identifier_with_type,
859 const code_typet &code_type,
860 const source_locationt &source_location,
861 const std::vector<symbol_exprt> &parameter_exprs,
862 symbol_table_baset &symbol_table,
863 code_blockt &block)
864{
865 // type __sync_lock_test_and_set (type *ptr, type value, ...)
866
867 // This builtin, as described by Intel, is not a traditional
868 // test-and-set operation, but rather an atomic exchange operation.
869 // It writes value into *ptr, and returns the previous contents of
870 // *ptr. Many targets have only minimal support for such locks, and
871 // do not support a full exchange operation. In this case, a target
872 // may support reduced functionality here by which the only valid
873 // value to store is the immediate constant 1. The exact value
874 // actually stored in *ptr is implementation defined.
875 const typet &type = code_type.return_type();
876
877 const symbol_exprt result =
878 result_symbol(identifier_with_type, type, source_location, symbol_table)
879 .symbol_expr();
880 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
881
882 // place operations on *ptr in an atomic section
885 {},
886 code_typet{{}, void_type()},
887 source_location}});
888
889 // build *ptr
890 const dereference_exprt deref_ptr{parameter_exprs[0]};
891
892 block.add(code_frontend_assignt{result, deref_ptr});
893
894 block.add(code_frontend_assignt{deref_ptr, parameter_exprs[1]});
895
896 // This built-in function is not a full barrier, but rather an acquire
897 // barrier.
900 {string_constantt{ID_RRfence}, {string_constantt{ID_RRfence}}},
901 typet{},
902 source_location}});
903
906 {},
907 code_typet{{}, void_type()},
908 source_location}});
909
910 block.add(code_returnt{result});
911}
912
914 const irep_idt &identifier_with_type,
915 const code_typet &code_type,
916 const source_locationt &source_location,
917 const std::vector<symbol_exprt> &parameter_exprs,
918 code_blockt &block)
919{
920 // void __sync_lock_release (type *ptr, ...)
921
922 // This built-in function releases the lock acquired by
923 // __sync_lock_test_and_set. Normally this means writing the constant 0 to
924 // *ptr.
925 const typet &type = to_pointer_type(parameter_exprs[0].type()).base_type();
926
927 // place operations on *ptr in an atomic section
930 {},
931 code_typet{{}, void_type()},
932 source_location}});
933
934 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]},
936 from_integer(0, signed_int_type()), type)});
937
938 // This built-in function is not a full barrier, but rather a release
939 // barrier.
942 {string_constantt{ID_WRfence}, {string_constantt{ID_WWfence}}},
943 typet{},
944 source_location}});
945
948 {},
949 code_typet{{}, void_type()},
950 source_location}});
951}
952
954 const irep_idt &identifier_with_type,
955 const code_typet &code_type,
956 const source_locationt &source_location,
957 const std::vector<symbol_exprt> &parameter_exprs,
958 code_blockt &block)
959{
960 // void __atomic_load (type *ptr, type *ret, int memorder)
961 // This is the generic version of an atomic load. It returns the contents of
962 // *ptr in *ret.
963
966 {},
967 code_typet{{}, void_type()},
968 source_location}});
969
970 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[1]},
971 dereference_exprt{parameter_exprs[0]}});
972
974 symbol_exprt::typeless("__atomic_thread_fence")
975 .with_source_location(source_location),
976 {parameter_exprs[2]},
977 typet{},
978 source_location}});
979
982 {},
983 code_typet{{}, void_type()},
984 source_location}});
985}
986
988 const irep_idt &identifier_with_type,
989 const code_typet &code_type,
990 const source_locationt &source_location,
991 const std::vector<symbol_exprt> &parameter_exprs,
992 symbol_table_baset &symbol_table,
993 code_blockt &block)
994{
995 // type __atomic_load_n (type *ptr, int memorder)
996 // This built-in function implements an atomic load operation. It returns
997 // the contents of *ptr.
998 const typet &type = code_type.return_type();
999
1000 const symbol_exprt result =
1001 result_symbol(identifier_with_type, type, source_location, symbol_table)
1002 .symbol_expr();
1003 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
1004
1006 symbol_exprt::typeless(ID___atomic_load)
1007 .with_source_location(source_location),
1008 {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
1009 typet{},
1010 source_location}});
1011
1012 block.add(code_returnt{result});
1013}
1014
1016 const irep_idt &identifier_with_type,
1017 const code_typet &code_type,
1018 const source_locationt &source_location,
1019 const std::vector<symbol_exprt> &parameter_exprs,
1020 code_blockt &block)
1021{
1022 // void __atomic_store (type *ptr, type *val, int memorder)
1023 // This is the generic version of an atomic store. It stores the value of
1024 // *val into *ptr.
1025
1027 symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1028 {},
1029 code_typet{{}, void_type()},
1030 source_location}});
1031
1032 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]},
1033 dereference_exprt{parameter_exprs[1]}});
1034
1036 symbol_exprt::typeless("__atomic_thread_fence")
1037 .with_source_location(source_location),
1038 {parameter_exprs[2]},
1039 typet{},
1040 source_location}});
1041
1044 {},
1045 code_typet{{}, void_type()},
1046 source_location}});
1047}
1048
1050 const irep_idt &identifier_with_type,
1051 const code_typet &code_type,
1052 const source_locationt &source_location,
1053 const std::vector<symbol_exprt> &parameter_exprs,
1054 code_blockt &block)
1055{
1056 // void __atomic_store_n (type *ptr, type val, int memorder)
1057 // This built-in function implements an atomic store operation. It writes
1058 // val into *ptr.
1059
1061 symbol_exprt::typeless(ID___atomic_store)
1062 .with_source_location(source_location),
1063 {parameter_exprs[0],
1064 address_of_exprt{parameter_exprs[1]},
1065 parameter_exprs[2]},
1066 typet{},
1067 source_location}});
1068}
1069
1071 const irep_idt &identifier_with_type,
1072 const code_typet &code_type,
1073 const source_locationt &source_location,
1074 const std::vector<symbol_exprt> &parameter_exprs,
1075 code_blockt &block)
1076{
1077 // void __atomic_exchange (type *ptr, type *val, type *ret, int memorder)
1078 // This is the generic version of an atomic exchange. It stores the contents
1079 // of *val into *ptr. The original value of *ptr is copied into *ret.
1080
1082 symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1083 {},
1084 code_typet{{}, void_type()},
1085 source_location}});
1086
1087 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[2]},
1088 dereference_exprt{parameter_exprs[0]}});
1089 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]},
1090 dereference_exprt{parameter_exprs[1]}});
1091
1093 symbol_exprt::typeless("__atomic_thread_fence")
1094 .with_source_location(source_location),
1095 {parameter_exprs[3]},
1096 typet{},
1097 source_location}});
1098
1101 {},
1102 code_typet{{}, void_type()},
1103 source_location}});
1104}
1105
1107 const irep_idt &identifier_with_type,
1108 const code_typet &code_type,
1109 const source_locationt &source_location,
1110 const std::vector<symbol_exprt> &parameter_exprs,
1111 symbol_table_baset &symbol_table,
1112 code_blockt &block)
1113{
1114 // type __atomic_exchange_n (type *ptr, type val, int memorder)
1115 // This built-in function implements an atomic exchange operation. It writes
1116 // val into *ptr, and returns the previous contents of *ptr.
1117 const typet &type = code_type.return_type();
1118
1119 const symbol_exprt result =
1120 result_symbol(identifier_with_type, type, source_location, symbol_table)
1121 .symbol_expr();
1122 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
1123
1125 symbol_exprt::typeless(ID___atomic_exchange)
1126 .with_source_location(source_location),
1127 {parameter_exprs[0],
1128 address_of_exprt{parameter_exprs[1]},
1129 address_of_exprt{result},
1130 parameter_exprs[2]},
1131 typet{},
1132 source_location}});
1133
1134 block.add(code_returnt{result});
1135}
1136
1138 const irep_idt &identifier_with_type,
1139 const code_typet &code_type,
1140 const source_locationt &source_location,
1141 const std::vector<symbol_exprt> &parameter_exprs,
1142 symbol_table_baset &symbol_table,
1143 code_blockt &block)
1144{
1145 // bool __atomic_compare_exchange (type *ptr, type *expected, type *desired,
1146 // bool weak, int success_memorder, int failure_memorder)
1147 // This built-in function implements an atomic compare and exchange
1148 // operation. This compares the contents of *ptr with the contents of
1149 // *expected. If equal, the operation is a read-modify-write operation that
1150 // writes *desired into *ptr. If they are not equal, the operation is a read
1151 // and the current contents of *ptr are written into *expected. weak is true
1152 // for weak compare_exchange, which may fail spuriously, and false for the
1153 // strong variation, which never fails spuriously. Many targets only offer
1154 // the strong variation and ignore the parameter.
1155
1156 const symbol_exprt result =
1158 identifier_with_type, c_bool_type(), source_location, symbol_table)
1159 .symbol_expr();
1160 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
1161
1162 // place operations on *ptr in an atomic section
1164 symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1165 {},
1166 code_typet{{}, void_type()},
1167 source_location}});
1168
1169 // build *ptr
1170 const dereference_exprt deref_ptr{parameter_exprs[0]};
1171
1173 result,
1175 equal_exprt{deref_ptr, dereference_exprt{parameter_exprs[1]}},
1176 result.type())});
1177
1178 // we never fail spuriously, and ignore parameter_exprs[3]
1179 code_frontend_assignt assign{deref_ptr,
1180 dereference_exprt{parameter_exprs[2]}};
1181 assign.add_source_location() = source_location;
1183 symbol_exprt::typeless("__atomic_thread_fence")
1184 .with_source_location(source_location),
1185 {parameter_exprs[4]},
1186 typet{},
1187 source_location}};
1188 success_fence.add_source_location() = source_location;
1189
1190 code_frontend_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]},
1191 deref_ptr};
1192 assign_not_equal.add_source_location() = source_location;
1194 symbol_exprt::typeless("__atomic_thread_fence")
1195 .with_source_location(source_location),
1196 {parameter_exprs[5]},
1197 typet{},
1198 source_location}};
1199 failure_fence.add_source_location() = source_location;
1200
1201 block.add(code_ifthenelset{
1202 result,
1203 code_blockt{{std::move(assign), std::move(success_fence)}},
1204 code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1205
1208 {},
1209 code_typet{{}, void_type()},
1210 source_location}});
1211
1212 block.add(code_returnt{result});
1213}
1214
1216 const irep_idt &identifier_with_type,
1217 const code_typet &code_type,
1218 const source_locationt &source_location,
1219 const std::vector<symbol_exprt> &parameter_exprs,
1220 code_blockt &block)
1221{
1222 // bool __atomic_compare_exchange_n (type *ptr, type *expected, type
1223 // desired, bool weak, int success_memorder, int failure_memorder)
1224
1226 symbol_exprt::typeless(ID___atomic_compare_exchange)
1227 .with_source_location(source_location),
1228 {parameter_exprs[0],
1229 parameter_exprs[1],
1230 address_of_exprt{parameter_exprs[2]},
1231 parameter_exprs[3],
1232 parameter_exprs[4],
1233 parameter_exprs[5]},
1234 typet{},
1235 source_location}});
1236}
1237
1239 const irep_idt &identifier,
1240 const symbol_exprt &function_symbol)
1241{
1242 const irep_idt &identifier_with_type = function_symbol.get_identifier();
1243 const code_typet &code_type = to_code_type(function_symbol.type());
1244 const source_locationt &source_location = function_symbol.source_location();
1245
1246 std::vector<symbol_exprt> parameter_exprs;
1247 parameter_exprs.reserve(code_type.parameters().size());
1248 for(const auto &parameter : code_type.parameters())
1249 {
1250 parameter_exprs.push_back(lookup(parameter.get_identifier()).symbol_expr());
1251 }
1252
1253 code_blockt block;
1254
1255 if(
1256 identifier == ID___atomic_fetch_add ||
1257 identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1258 identifier == ID___atomic_fetch_and ||
1259 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1260 {
1262 identifier,
1263 identifier_with_type,
1264 code_type,
1265 source_location,
1266 parameter_exprs,
1268 block);
1269 }
1270 else if(
1271 identifier == ID___atomic_add_fetch ||
1272 identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1273 identifier == ID___atomic_and_fetch ||
1274 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1275 {
1277 identifier,
1278 identifier_with_type,
1279 code_type,
1280 source_location,
1281 parameter_exprs,
1283 block);
1284 }
1285 else if(
1286 identifier == ID___sync_fetch_and_add ||
1287 identifier == ID___sync_fetch_and_sub ||
1288 identifier == ID___sync_fetch_and_or ||
1289 identifier == ID___sync_fetch_and_and ||
1290 identifier == ID___sync_fetch_and_xor ||
1291 identifier == ID___sync_fetch_and_nand ||
1292 identifier == ID___sync_add_and_fetch ||
1293 identifier == ID___sync_sub_and_fetch ||
1294 identifier == ID___sync_or_and_fetch ||
1295 identifier == ID___sync_and_and_fetch ||
1296 identifier == ID___sync_xor_and_fetch ||
1297 identifier == ID___sync_nand_and_fetch)
1298 {
1300 identifier,
1301 identifier_with_type,
1302 code_type,
1303 source_location,
1304 parameter_exprs,
1305 block);
1306 }
1307 else if(identifier == ID___sync_bool_compare_and_swap)
1308 {
1310 identifier_with_type, code_type, source_location, parameter_exprs, block);
1311 }
1312 else if(identifier == ID___sync_val_compare_and_swap)
1313 {
1315 identifier_with_type,
1316 code_type,
1317 source_location,
1318 parameter_exprs,
1320 block);
1321 }
1322 else if(identifier == ID___sync_lock_test_and_set)
1323 {
1325 identifier_with_type,
1326 code_type,
1327 source_location,
1328 parameter_exprs,
1330 block);
1331 }
1332 else if(identifier == ID___sync_lock_release)
1333 {
1335 identifier_with_type, code_type, source_location, parameter_exprs, block);
1336 }
1337 else if(identifier == ID___atomic_load)
1338 {
1340 identifier_with_type, code_type, source_location, parameter_exprs, block);
1341 }
1342 else if(identifier == ID___atomic_load_n)
1343 {
1345 identifier_with_type,
1346 code_type,
1347 source_location,
1348 parameter_exprs,
1350 block);
1351 }
1352 else if(identifier == ID___atomic_store)
1353 {
1355 identifier_with_type, code_type, source_location, parameter_exprs, block);
1356 }
1357 else if(identifier == ID___atomic_store_n)
1358 {
1360 identifier_with_type, code_type, source_location, parameter_exprs, block);
1361 }
1362 else if(identifier == ID___atomic_exchange)
1363 {
1365 identifier_with_type, code_type, source_location, parameter_exprs, block);
1366 }
1367 else if(identifier == ID___atomic_exchange_n)
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)
1378 {
1380 identifier_with_type,
1381 code_type,
1382 source_location,
1383 parameter_exprs,
1385 block);
1386 }
1387 else if(identifier == ID___atomic_compare_exchange_n)
1388 {
1390 identifier_with_type, code_type, source_location, parameter_exprs, block);
1391 }
1392 else
1393 {
1395 }
1396
1397 for(auto &statement : block.statements())
1398 statement.add_source_location() = source_location;
1399
1400 return block;
1401}
1402
1405{
1406 const exprt &f_op = expr.function();
1407 const source_locationt &source_location = expr.source_location();
1408 const irep_idt &identifier = to_symbol_expr(f_op).get_identifier();
1409
1410 exprt::operandst arguments = expr.arguments();
1411
1412 if(identifier == "__builtin_shuffle")
1413 {
1414 // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html and
1415 // https://github.com/OpenCL/man/blob/master/shuffle.adoc
1416 if(arguments.size() != 2 && arguments.size() != 3)
1417 {
1419 error() << "__builtin_shuffle expects two or three arguments" << eom;
1420 throw 0;
1421 }
1422
1423 for(exprt &arg : arguments)
1424 {
1425 if(arg.type().id() != ID_vector)
1426 {
1428 error() << "__builtin_shuffle expects vector arguments" << eom;
1429 throw 0;
1430 }
1431 }
1432
1433 const exprt &arg0 = arguments[0];
1434 const vector_typet &input_vec_type = to_vector_type(arg0.type());
1435
1436 std::optional<exprt> arg1;
1437 if(arguments.size() == 3)
1438 {
1439 if(arguments[1].type() != input_vec_type)
1440 {
1442 error() << "__builtin_shuffle expects input vectors of the same type"
1443 << eom;
1444 throw 0;
1445 }
1446 arg1 = arguments[1];
1447 }
1448 const exprt &indices = arguments.back();
1449 const vector_typet &indices_type = to_vector_type(indices.type());
1450 const std::size_t indices_size =
1451 numeric_cast_v<std::size_t>(indices_type.size());
1452
1453 exprt::operandst operands;
1454 operands.reserve(indices_size);
1455
1456 auto input_size = numeric_cast<mp_integer>(input_vec_type.size());
1457 CHECK_RETURN(input_size.has_value());
1458 if(arg1.has_value())
1459 input_size = *input_size * 2;
1460 constant_exprt size =
1461 from_integer(*input_size, indices_type.element_type());
1462
1463 for(std::size_t i = 0; i < indices_size; ++i)
1464 {
1465 // only the least significant bits of each mask element are considered
1466 mod_exprt mod_index{index_exprt{indices, from_integer(i, c_index_type())},
1467 size};
1468 mod_index.add_source_location() = source_location;
1469 operands.push_back(std::move(mod_index));
1470 }
1471
1472 return shuffle_vector_exprt{arg0, arg1, std::move(operands)};
1473 }
1474 else if(identifier == "__builtin_shufflevector")
1475 {
1476 // https://clang.llvm.org/docs/LanguageExtensions.html#langext-builtin-shufflevector
1477 if(arguments.size() < 2)
1478 {
1480 error() << "__builtin_shufflevector expects two or more arguments" << eom;
1481 throw 0;
1482 }
1483
1484 exprt::operandst operands;
1485 operands.reserve(arguments.size() - 2);
1486
1487 for(std::size_t i = 0; i < arguments.size(); ++i)
1488 {
1489 exprt &arg_i = arguments[i];
1490
1491 if(i <= 1 && arg_i.type().id() != ID_vector)
1492 {
1494 error() << "__builtin_shufflevector expects two vectors as argument"
1495 << eom;
1496 throw 0;
1497 }
1498 else if(i > 1)
1499 {
1501 {
1503 error() << "__builtin_shufflevector expects integer index" << eom;
1504 throw 0;
1505 }
1506
1507 make_constant(arg_i);
1508
1509 const auto int_index = numeric_cast<mp_integer>(arg_i);
1510 CHECK_RETURN(int_index.has_value());
1511
1512 if(*int_index == -1)
1513 {
1514 operands.push_back(from_integer(0, arg_i.type()));
1515 operands.back().add_source_location() = source_location;
1516 }
1517 else
1518 operands.push_back(arg_i);
1519 }
1520 }
1521
1522 return shuffle_vector_exprt{
1523 arguments[0], arguments[1], std::move(operands)};
1524 }
1525 else
1527}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
std::optional< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
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_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_table_baset &symbol_table, code_blockt &block)
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_table_baset &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 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_table_baset &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_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_table_baset &symbol_table, 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 symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_table_baset &symbol_table)
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_table_baset &symbol_table, code_blockt &block)
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_table_baset &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_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_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_table_baset &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:245
signedbv_typet signed_int_type()
Definition c_types.cpp:22
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:235
typet c_bool_type()
Definition c_types.cpp:100
bitvector_typet c_index_type()
Definition c_types.cpp:16
Operator to return the address of an object.
A base class for binary expressions.
Definition std_expr.h:638
symbol_table_baset & symbol_table
virtual void make_constant(exprt &expr)
virtual code_blockt instantiate_gcc_polymorphic_builtin(const irep_idt &identifier, const symbol_exprt &function_symbol)
virtual std::optional< 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
goto_instruction_codet representation of a "return from afunction" statement.
Base type of functions.
Definition std_types.h:583
std::vector< parametert > parameterst
Definition std_types.h:586
const parameterst & parameters() const
Definition std_types.h:699
const typet & return_type() const
Definition std_types.h:689
void make_ellipsis()
Definition std_types.h:679
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Definition std_expr.h:3118
Operator to dereference a pointer.
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
typet & type()
Return the type of the expression.
Definition expr.h:84
const source_locationt & source_location() const
Definition expr.h:231
source_locationt & add_source_location()
Definition expr.h:236
Array index operator.
Definition std_expr.h:1470
const irep_idt & id() const
Definition irep.h:388
source_locationt source_location
Definition message.h:239
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
mstreamt & error() const
Definition message.h:391
message_handlert & get_message_handler()
Definition message.h:183
static eomt eom
Definition message.h:289
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition std_expr.h:1228
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const typet & base_type() const
The type of the data what we point to.
Shuffle elements of one or two vectors, modelled after Clang's __builtin_shufflevector.
Definition c_expr.h:21
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:131
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:150
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
Definition std_expr.h:166
const irep_idt & get_identifier() const
Definition std_expr.h:160
The symbol table base class interface.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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:73
bool is_thread_local
Definition symbol.h:71
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
bool is_lvalue
Definition symbol.h:72
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2081
The type of an expression, extends irept.
Definition type.h:29
The vector type.
Definition std_types.h:1064
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1080
#define CPROVER_PREFIX
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1116
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:788
Author: Diffblue Ltd.
dstringt irep_idt