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
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
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_table_baset &symbol_table)
614{
615 symbolt symbol{id2string(identifier) + "::1::result", type, ID_C};
616 symbol.base_name = "result";
617 symbol.location = source_location;
618 symbol.is_file_local = true;
619 symbol.is_lvalue = true;
620 symbol.is_thread_local = true;
621
622 symbol_table.add(symbol);
623
624 return symbol;
625}
626
628 const irep_idt &identifier,
629 const irep_idt &identifier_with_type,
630 const code_typet &code_type,
631 const source_locationt &source_location,
632 const std::vector<symbol_exprt> &parameter_exprs,
633 symbol_table_baset &symbol_table,
634 code_blockt &block)
635{
636 // type __sync_fetch_and_OP(type *ptr, type value, ...)
637 // { type result; result = *ptr; *ptr = result OP value; return result; }
638 const typet &type = code_type.return_type();
639
640 const symbol_exprt result =
641 result_symbol(identifier_with_type, type, source_location, symbol_table)
642 .symbol_expr();
643 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
644
645 // place operations on *ptr in an atomic section
648 {},
649 code_typet{{}, void_type()},
650 source_location}});
651
652 // build *ptr
653 const dereference_exprt deref_ptr{parameter_exprs[0]};
654
655 block.add(code_frontend_assignt{result, deref_ptr});
656
657 // build *ptr = result OP arguments[1];
658 irep_idt op_id = identifier == ID___atomic_fetch_add
659 ? ID_plus
660 : identifier == ID___atomic_fetch_sub
661 ? ID_minus
662 : identifier == ID___atomic_fetch_or
663 ? ID_bitor
664 : identifier == ID___atomic_fetch_and
665 ? ID_bitand
666 : identifier == ID___atomic_fetch_xor
667 ? ID_bitxor
668 : identifier == ID___atomic_fetch_nand
669 ? ID_bitnand
670 : ID_nil;
671 binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
672 block.add(code_frontend_assignt{deref_ptr, std::move(op_expr)});
673
675 symbol_exprt::typeless("__atomic_thread_fence"),
676 {parameter_exprs[2]},
677 typet{},
678 source_location}});
679
682 {},
683 code_typet{{}, void_type()},
684 source_location}});
685
686 block.add(code_returnt{result});
687}
688
690 const irep_idt &identifier,
691 const irep_idt &identifier_with_type,
692 const code_typet &code_type,
693 const source_locationt &source_location,
694 const std::vector<symbol_exprt> &parameter_exprs,
695 symbol_table_baset &symbol_table,
696 code_blockt &block)
697{
698 // type __sync_OP_and_fetch(type *ptr, type value, ...)
699 // { type result; result = *ptr OP value; *ptr = result; return result; }
700 const typet &type = code_type.return_type();
701
702 const symbol_exprt result =
703 result_symbol(identifier_with_type, type, source_location, symbol_table)
704 .symbol_expr();
705 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
706
707 // place operations on *ptr in an atomic section
710 {},
711 code_typet{{}, void_type()},
712 source_location}});
713
714 // build *ptr
715 const dereference_exprt deref_ptr{parameter_exprs[0]};
716
717 // build result = *ptr OP arguments[1];
718 irep_idt op_id = identifier == ID___atomic_add_fetch
719 ? ID_plus
720 : identifier == ID___atomic_sub_fetch
721 ? ID_minus
722 : identifier == ID___atomic_or_fetch
723 ? ID_bitor
724 : identifier == ID___atomic_and_fetch
725 ? ID_bitand
726 : identifier == ID___atomic_xor_fetch
727 ? ID_bitxor
728 : identifier == ID___atomic_nand_fetch
729 ? ID_bitnand
730 : ID_nil;
731 binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
732 block.add(code_frontend_assignt{result, std::move(op_expr)});
733
734 block.add(code_frontend_assignt{deref_ptr, result});
735
736 // this instruction implies an mfence, i.e., WRfence
738 symbol_exprt::typeless("__atomic_thread_fence"),
739 {parameter_exprs[2]},
740 typet{},
741 source_location}});
742
745 {},
746 code_typet{{}, void_type()},
747 source_location}});
748
749 block.add(code_returnt{result});
750}
751
753 const irep_idt &identifier,
754 const irep_idt &identifier_with_type,
755 const code_typet &code_type,
756 const source_locationt &source_location,
757 const std::vector<symbol_exprt> &parameter_exprs,
758 code_blockt &block)
759{
760 // implement by calling their __atomic_ counterparts with memorder SEQ_CST
761 std::string atomic_name = "__atomic_" + id2string(identifier).substr(7);
762 atomic_name.replace(atomic_name.find("_and_"), 5, "_");
763
764 exprt::operandst arguments{
765 parameter_exprs[0],
766 parameter_exprs[1],
767 from_integer(std::memory_order_seq_cst, signed_int_type())};
768
769 block.add(code_returnt{
771 std::move(arguments),
772 typet{},
773 source_location}});
774}
775
777 const irep_idt &identifier_with_type,
778 const code_typet &code_type,
779 const source_locationt &source_location,
780 const std::vector<symbol_exprt> &parameter_exprs,
781 code_blockt &block)
782{
783 // These builtins perform an atomic compare and swap. That is, if the
784 // current value of *ptr is oldval, then write newval into *ptr. The
785 // "bool" version returns true if the comparison is successful and
786 // newval was written. The "val" version returns the contents of *ptr
787 // before the operation.
788
789 // _Bool __sync_bool_compare_and_swap(type *ptr, type old, type new, ...)
790
792 symbol_exprt::typeless(ID___atomic_compare_exchange),
793 {parameter_exprs[0],
794 address_of_exprt{parameter_exprs[1]},
795 address_of_exprt{parameter_exprs[2]},
797 from_integer(std::memory_order_seq_cst, signed_int_type()),
798 from_integer(std::memory_order_seq_cst, signed_int_type())},
799 typet{},
800 source_location}});
801}
802
804 const irep_idt &identifier_with_type,
805 const code_typet &code_type,
806 const source_locationt &source_location,
807 const std::vector<symbol_exprt> &parameter_exprs,
808 symbol_table_baset &symbol_table,
809 code_blockt &block)
810{
811 // type __sync_val_compare_and_swap(type *ptr, type old, type new, ...)
812 // { type result = *ptr; if(result == old) *ptr = new; return result; }
813 const typet &type = code_type.return_type();
814
815 const symbol_exprt result =
816 result_symbol(identifier_with_type, type, source_location, symbol_table)
817 .symbol_expr();
818 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
819
820 // place operations on *ptr in an atomic section
823 {},
824 code_typet{{}, void_type()},
825 source_location}});
826
827 // build *ptr
828 const dereference_exprt deref_ptr{parameter_exprs[0]};
829
830 block.add(code_frontend_assignt{result, deref_ptr});
831
832 code_frontend_assignt assign{deref_ptr, parameter_exprs[2]};
833 assign.add_source_location() = source_location;
834 block.add(code_ifthenelset{equal_exprt{result, parameter_exprs[1]},
835 std::move(assign)});
836
837 // this instruction implies an mfence, i.e., WRfence
840 {string_constantt{ID_WRfence}},
841 typet{},
842 source_location}});
843
846 {},
847 code_typet{{}, void_type()},
848 source_location}});
849
850 block.add(code_returnt{result});
851}
852
854 const irep_idt &identifier_with_type,
855 const code_typet &code_type,
856 const source_locationt &source_location,
857 const std::vector<symbol_exprt> &parameter_exprs,
858 symbol_table_baset &symbol_table,
859 code_blockt &block)
860{
861 // type __sync_lock_test_and_set (type *ptr, type value, ...)
862
863 // This builtin, as described by Intel, is not a traditional
864 // test-and-set operation, but rather an atomic exchange operation.
865 // It writes value into *ptr, and returns the previous contents of
866 // *ptr. Many targets have only minimal support for such locks, and
867 // do not support a full exchange operation. In this case, a target
868 // may support reduced functionality here by which the only valid
869 // value to store is the immediate constant 1. The exact value
870 // actually stored in *ptr is implementation defined.
871 const typet &type = code_type.return_type();
872
873 const symbol_exprt result =
874 result_symbol(identifier_with_type, type, source_location, symbol_table)
875 .symbol_expr();
876 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
877
878 // place operations on *ptr in an atomic section
881 {},
882 code_typet{{}, void_type()},
883 source_location}});
884
885 // build *ptr
886 const dereference_exprt deref_ptr{parameter_exprs[0]};
887
888 block.add(code_frontend_assignt{result, deref_ptr});
889
890 block.add(code_frontend_assignt{deref_ptr, parameter_exprs[1]});
891
892 // This built-in function is not a full barrier, but rather an acquire
893 // barrier.
896 {string_constantt{ID_RRfence}, {string_constantt{ID_RRfence}}},
897 typet{},
898 source_location}});
899
902 {},
903 code_typet{{}, void_type()},
904 source_location}});
905
906 block.add(code_returnt{result});
907}
908
910 const irep_idt &identifier_with_type,
911 const code_typet &code_type,
912 const source_locationt &source_location,
913 const std::vector<symbol_exprt> &parameter_exprs,
914 code_blockt &block)
915{
916 // void __sync_lock_release (type *ptr, ...)
917
918 // This built-in function releases the lock acquired by
919 // __sync_lock_test_and_set. Normally this means writing the constant 0 to
920 // *ptr.
921 const typet &type = to_pointer_type(parameter_exprs[0].type()).base_type();
922
923 // place operations on *ptr in an atomic section
926 {},
927 code_typet{{}, void_type()},
928 source_location}});
929
930 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]},
932 from_integer(0, signed_int_type()), type)});
933
934 // This built-in function is not a full barrier, but rather a release
935 // barrier.
938 {string_constantt{ID_WRfence}, {string_constantt{ID_WWfence}}},
939 typet{},
940 source_location}});
941
944 {},
945 code_typet{{}, void_type()},
946 source_location}});
947}
948
950 const irep_idt &identifier_with_type,
951 const code_typet &code_type,
952 const source_locationt &source_location,
953 const std::vector<symbol_exprt> &parameter_exprs,
954 code_blockt &block)
955{
956 // void __atomic_load (type *ptr, type *ret, int memorder)
957 // This is the generic version of an atomic load. It returns the contents of
958 // *ptr in *ret.
959
962 {},
963 code_typet{{}, void_type()},
964 source_location}});
965
966 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[1]},
967 dereference_exprt{parameter_exprs[0]}});
968
970 symbol_exprt::typeless("__atomic_thread_fence"),
971 {parameter_exprs[2]},
972 typet{},
973 source_location}});
974
977 {},
978 code_typet{{}, void_type()},
979 source_location}});
980}
981
983 const irep_idt &identifier_with_type,
984 const code_typet &code_type,
985 const source_locationt &source_location,
986 const std::vector<symbol_exprt> &parameter_exprs,
987 symbol_table_baset &symbol_table,
988 code_blockt &block)
989{
990 // type __atomic_load_n (type *ptr, int memorder)
991 // This built-in function implements an atomic load operation. It returns
992 // the contents of *ptr.
993 const typet &type = code_type.return_type();
994
995 const symbol_exprt result =
996 result_symbol(identifier_with_type, type, source_location, symbol_table)
997 .symbol_expr();
998 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
999
1001 symbol_exprt::typeless(ID___atomic_load),
1002 {parameter_exprs[0], address_of_exprt{result}, parameter_exprs[1]},
1003 typet{},
1004 source_location}});
1005
1006 block.add(code_returnt{result});
1007}
1008
1010 const irep_idt &identifier_with_type,
1011 const code_typet &code_type,
1012 const source_locationt &source_location,
1013 const std::vector<symbol_exprt> &parameter_exprs,
1014 code_blockt &block)
1015{
1016 // void __atomic_store (type *ptr, type *val, int memorder)
1017 // This is the generic version of an atomic store. It stores the value of
1018 // *val into *ptr.
1019
1021 symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1022 {},
1023 code_typet{{}, void_type()},
1024 source_location}});
1025
1026 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]},
1027 dereference_exprt{parameter_exprs[1]}});
1028
1030 symbol_exprt::typeless("__atomic_thread_fence"),
1031 {parameter_exprs[2]},
1032 typet{},
1033 source_location}});
1034
1037 {},
1038 code_typet{{}, void_type()},
1039 source_location}});
1040}
1041
1043 const irep_idt &identifier_with_type,
1044 const code_typet &code_type,
1045 const source_locationt &source_location,
1046 const std::vector<symbol_exprt> &parameter_exprs,
1047 code_blockt &block)
1048{
1049 // void __atomic_store_n (type *ptr, type val, int memorder)
1050 // This built-in function implements an atomic store operation. It writes
1051 // val into *ptr.
1052
1053 block.add(code_expressiont{
1055 {parameter_exprs[0],
1056 address_of_exprt{parameter_exprs[1]},
1057 parameter_exprs[2]},
1058 typet{},
1059 source_location}});
1060}
1061
1063 const irep_idt &identifier_with_type,
1064 const code_typet &code_type,
1065 const source_locationt &source_location,
1066 const std::vector<symbol_exprt> &parameter_exprs,
1067 code_blockt &block)
1068{
1069 // void __atomic_exchange (type *ptr, type *val, type *ret, int memorder)
1070 // This is the generic version of an atomic exchange. It stores the contents
1071 // of *val into *ptr. The original value of *ptr is copied into *ret.
1072
1074 symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1075 {},
1076 code_typet{{}, void_type()},
1077 source_location}});
1078
1079 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[2]},
1080 dereference_exprt{parameter_exprs[0]}});
1081 block.add(code_frontend_assignt{dereference_exprt{parameter_exprs[0]},
1082 dereference_exprt{parameter_exprs[1]}});
1083
1085 symbol_exprt::typeless("__atomic_thread_fence"),
1086 {parameter_exprs[3]},
1087 typet{},
1088 source_location}});
1089
1092 {},
1093 code_typet{{}, void_type()},
1094 source_location}});
1095}
1096
1098 const irep_idt &identifier_with_type,
1099 const code_typet &code_type,
1100 const source_locationt &source_location,
1101 const std::vector<symbol_exprt> &parameter_exprs,
1102 symbol_table_baset &symbol_table,
1103 code_blockt &block)
1104{
1105 // type __atomic_exchange_n (type *ptr, type val, int memorder)
1106 // This built-in function implements an atomic exchange operation. It writes
1107 // val into *ptr, and returns the previous contents of *ptr.
1108 const typet &type = code_type.return_type();
1109
1110 const symbol_exprt result =
1111 result_symbol(identifier_with_type, type, source_location, symbol_table)
1112 .symbol_expr();
1113 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
1114
1116 symbol_exprt::typeless(ID___atomic_exchange),
1117 {parameter_exprs[0],
1118 address_of_exprt{parameter_exprs[1]},
1119 address_of_exprt{result},
1120 parameter_exprs[2]},
1121 typet{},
1122 source_location}});
1123
1124 block.add(code_returnt{result});
1125}
1126
1128 const irep_idt &identifier_with_type,
1129 const code_typet &code_type,
1130 const source_locationt &source_location,
1131 const std::vector<symbol_exprt> &parameter_exprs,
1132 symbol_table_baset &symbol_table,
1133 code_blockt &block)
1134{
1135 // bool __atomic_compare_exchange (type *ptr, type *expected, type *desired,
1136 // bool weak, int success_memorder, int failure_memorder)
1137 // This built-in function implements an atomic compare and exchange
1138 // operation. This compares the contents of *ptr with the contents of
1139 // *expected. If equal, the operation is a read-modify-write operation that
1140 // writes *desired into *ptr. If they are not equal, the operation is a read
1141 // and the current contents of *ptr are written into *expected. weak is true
1142 // for weak compare_exchange, which may fail spuriously, and false for the
1143 // strong variation, which never fails spuriously. Many targets only offer
1144 // the strong variation and ignore the parameter.
1145
1146 const symbol_exprt result =
1148 identifier_with_type, c_bool_type(), source_location, symbol_table)
1149 .symbol_expr();
1150 block.add(codet{ID_decl_block, {code_frontend_declt{result}}});
1151
1152 // place operations on *ptr in an atomic section
1154 symbol_exprt::typeless(CPROVER_PREFIX "atomic_begin"),
1155 {},
1156 code_typet{{}, void_type()},
1157 source_location}});
1158
1159 // build *ptr
1160 const dereference_exprt deref_ptr{parameter_exprs[0]};
1161
1163 result,
1165 equal_exprt{deref_ptr, dereference_exprt{parameter_exprs[1]}},
1166 result.type())});
1167
1168 // we never fail spuriously, and ignore parameter_exprs[3]
1169 code_frontend_assignt assign{deref_ptr,
1170 dereference_exprt{parameter_exprs[2]}};
1171 assign.add_source_location() = source_location;
1173 symbol_exprt::typeless("__atomic_thread_fence"),
1174 {parameter_exprs[4]},
1175 typet{},
1176 source_location}};
1177 success_fence.add_source_location() = source_location;
1178
1179 code_frontend_assignt assign_not_equal{dereference_exprt{parameter_exprs[1]},
1180 deref_ptr};
1181 assign_not_equal.add_source_location() = source_location;
1183 symbol_exprt::typeless("__atomic_thread_fence"),
1184 {parameter_exprs[5]},
1185 typet{},
1186 source_location}};
1187 failure_fence.add_source_location() = source_location;
1188
1189 block.add(code_ifthenelset{
1190 result,
1191 code_blockt{{std::move(assign), std::move(success_fence)}},
1192 code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1193
1196 {},
1197 code_typet{{}, void_type()},
1198 source_location}});
1199
1200 block.add(code_returnt{result});
1201}
1202
1204 const irep_idt &identifier_with_type,
1205 const code_typet &code_type,
1206 const source_locationt &source_location,
1207 const std::vector<symbol_exprt> &parameter_exprs,
1208 code_blockt &block)
1209{
1210 // bool __atomic_compare_exchange_n (type *ptr, type *expected, type
1211 // desired, bool weak, int success_memorder, int failure_memorder)
1212
1214 symbol_exprt::typeless(ID___atomic_compare_exchange),
1215 {parameter_exprs[0],
1216 parameter_exprs[1],
1217 address_of_exprt{parameter_exprs[2]},
1218 parameter_exprs[3],
1219 parameter_exprs[4],
1220 parameter_exprs[5]},
1221 typet{},
1222 source_location}});
1223}
1224
1226 const irep_idt &identifier,
1227 const symbol_exprt &function_symbol)
1228{
1229 const irep_idt &identifier_with_type = function_symbol.get_identifier();
1230 const code_typet &code_type = to_code_type(function_symbol.type());
1231 const source_locationt &source_location = function_symbol.source_location();
1232
1233 std::vector<symbol_exprt> parameter_exprs;
1234 parameter_exprs.reserve(code_type.parameters().size());
1235 for(const auto &parameter : code_type.parameters())
1236 {
1237 parameter_exprs.push_back(lookup(parameter.get_identifier()).symbol_expr());
1238 }
1239
1240 code_blockt block;
1241
1242 if(
1243 identifier == ID___atomic_fetch_add ||
1244 identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1245 identifier == ID___atomic_fetch_and ||
1246 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1247 {
1249 identifier,
1250 identifier_with_type,
1251 code_type,
1252 source_location,
1253 parameter_exprs,
1255 block);
1256 }
1257 else if(
1258 identifier == ID___atomic_add_fetch ||
1259 identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1260 identifier == ID___atomic_and_fetch ||
1261 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1262 {
1264 identifier,
1265 identifier_with_type,
1266 code_type,
1267 source_location,
1268 parameter_exprs,
1270 block);
1271 }
1272 else if(
1273 identifier == ID___sync_fetch_and_add ||
1274 identifier == ID___sync_fetch_and_sub ||
1275 identifier == ID___sync_fetch_and_or ||
1276 identifier == ID___sync_fetch_and_and ||
1277 identifier == ID___sync_fetch_and_xor ||
1278 identifier == ID___sync_fetch_and_nand ||
1279 identifier == ID___sync_add_and_fetch ||
1280 identifier == ID___sync_sub_and_fetch ||
1281 identifier == ID___sync_or_and_fetch ||
1282 identifier == ID___sync_and_and_fetch ||
1283 identifier == ID___sync_xor_and_fetch ||
1284 identifier == ID___sync_nand_and_fetch)
1285 {
1287 identifier,
1288 identifier_with_type,
1289 code_type,
1290 source_location,
1291 parameter_exprs,
1292 block);
1293 }
1294 else if(identifier == ID___sync_bool_compare_and_swap)
1295 {
1297 identifier_with_type, code_type, source_location, parameter_exprs, block);
1298 }
1299 else if(identifier == ID___sync_val_compare_and_swap)
1300 {
1302 identifier_with_type,
1303 code_type,
1304 source_location,
1305 parameter_exprs,
1307 block);
1308 }
1309 else if(identifier == ID___sync_lock_test_and_set)
1310 {
1312 identifier_with_type,
1313 code_type,
1314 source_location,
1315 parameter_exprs,
1317 block);
1318 }
1319 else if(identifier == ID___sync_lock_release)
1320 {
1322 identifier_with_type, code_type, source_location, parameter_exprs, block);
1323 }
1324 else if(identifier == ID___atomic_load)
1325 {
1327 identifier_with_type, code_type, source_location, parameter_exprs, block);
1328 }
1329 else if(identifier == ID___atomic_load_n)
1330 {
1332 identifier_with_type,
1333 code_type,
1334 source_location,
1335 parameter_exprs,
1337 block);
1338 }
1339 else if(identifier == ID___atomic_store)
1340 {
1342 identifier_with_type, code_type, source_location, parameter_exprs, block);
1343 }
1344 else if(identifier == ID___atomic_store_n)
1345 {
1347 identifier_with_type, code_type, source_location, parameter_exprs, block);
1348 }
1349 else if(identifier == ID___atomic_exchange)
1350 {
1352 identifier_with_type, code_type, source_location, parameter_exprs, block);
1353 }
1354 else if(identifier == ID___atomic_exchange_n)
1355 {
1357 identifier_with_type,
1358 code_type,
1359 source_location,
1360 parameter_exprs,
1362 block);
1363 }
1364 else if(identifier == ID___atomic_compare_exchange)
1365 {
1367 identifier_with_type,
1368 code_type,
1369 source_location,
1370 parameter_exprs,
1372 block);
1373 }
1374 else if(identifier == ID___atomic_compare_exchange_n)
1375 {
1377 identifier_with_type, code_type, source_location, parameter_exprs, block);
1378 }
1379 else
1380 {
1382 }
1383
1384 for(auto &statement : block.statements())
1385 statement.add_source_location() = source_location;
1386
1387 return block;
1388}
1389
1392{
1393 const exprt &f_op = expr.function();
1394 const source_locationt &source_location = expr.source_location();
1395 const irep_idt &identifier = to_symbol_expr(f_op).get_identifier();
1396
1397 exprt::operandst arguments = expr.arguments();
1398
1399 if(identifier == "__builtin_shuffle")
1400 {
1401 // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html and
1402 // https://github.com/OpenCL/man/blob/master/shuffle.adoc
1403 if(arguments.size() != 2 && arguments.size() != 3)
1404 {
1406 error() << "__builtin_shuffle expects two or three arguments" << eom;
1407 throw 0;
1408 }
1409
1410 for(exprt &arg : arguments)
1411 {
1412 if(arg.type().id() != ID_vector)
1413 {
1415 error() << "__builtin_shuffle expects vector arguments" << eom;
1416 throw 0;
1417 }
1418 }
1419
1420 const exprt &arg0 = arguments[0];
1421 const vector_typet &input_vec_type = to_vector_type(arg0.type());
1422
1423 optionalt<exprt> arg1;
1424 if(arguments.size() == 3)
1425 {
1426 if(arguments[1].type() != input_vec_type)
1427 {
1429 error() << "__builtin_shuffle expects input vectors of the same type"
1430 << eom;
1431 throw 0;
1432 }
1433 arg1 = arguments[1];
1434 }
1435 const exprt &indices = arguments.back();
1436 const vector_typet &indices_type = to_vector_type(indices.type());
1437 const std::size_t indices_size =
1438 numeric_cast_v<std::size_t>(indices_type.size());
1439
1440 exprt::operandst operands;
1441 operands.reserve(indices_size);
1442
1443 auto input_size = numeric_cast<mp_integer>(input_vec_type.size());
1444 CHECK_RETURN(input_size.has_value());
1445 if(arg1.has_value())
1446 input_size = *input_size * 2;
1447 constant_exprt size =
1448 from_integer(*input_size, indices_type.element_type());
1449
1450 for(std::size_t i = 0; i < indices_size; ++i)
1451 {
1452 // only the least significant bits of each mask element are considered
1453 mod_exprt mod_index{index_exprt{indices, from_integer(i, c_index_type())},
1454 size};
1455 mod_index.add_source_location() = source_location;
1456 operands.push_back(std::move(mod_index));
1457 }
1458
1459 return shuffle_vector_exprt{arg0, arg1, std::move(operands)};
1460 }
1461 else if(identifier == "__builtin_shufflevector")
1462 {
1463 // https://clang.llvm.org/docs/LanguageExtensions.html#langext-builtin-shufflevector
1464 if(arguments.size() < 2)
1465 {
1467 error() << "__builtin_shufflevector expects two or more arguments" << eom;
1468 throw 0;
1469 }
1470
1471 exprt::operandst operands;
1472 operands.reserve(arguments.size() - 2);
1473
1474 for(std::size_t i = 0; i < arguments.size(); ++i)
1475 {
1476 exprt &arg_i = arguments[i];
1477
1478 if(i <= 1 && arg_i.type().id() != ID_vector)
1479 {
1481 error() << "__builtin_shufflevector expects two vectors as argument"
1482 << eom;
1483 throw 0;
1484 }
1485 else if(i > 1)
1486 {
1488 {
1490 error() << "__builtin_shufflevector expects integer index" << eom;
1491 throw 0;
1492 }
1493
1494 make_constant(arg_i);
1495
1496 const auto int_index = numeric_cast<mp_integer>(arg_i);
1497 CHECK_RETURN(int_index.has_value());
1498
1499 if(*int_index == -1)
1500 {
1501 operands.push_back(from_integer(0, arg_i.type()));
1502 operands.back().add_source_location() = source_location;
1503 }
1504 else
1505 operands.push_back(arg_i);
1506 }
1507 }
1508
1509 return shuffle_vector_exprt{
1510 arguments[0], arguments[1], std::move(operands)};
1511 }
1512 else
1514}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral 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...
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:250
signedbv_typet signed_int_type()
Definition c_types.cpp:27
pointer_typet pointer_type(const typet &subtype)
Definition c_types.cpp:240
typet c_bool_type()
Definition c_types.cpp:105
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:583
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 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
goto_instruction_codet representation of a "return from afunction" 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.
A constant literal expression.
Definition std_expr.h:2942
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Equality.
Definition std_expr.h:1306
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:223
source_locationt & add_source_location()
Definition expr.h:228
Array index operator.
Definition std_expr.h:1410
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:1168
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:20
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:113
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
Definition std_expr.h:132
const irep_idt & get_identifier() const
Definition std_expr.h:142
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
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition std_expr.h:2025
The type of an expression, extends irept.
Definition type.h:29
The vector type.
Definition std_types.h:1008
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
Definition std_types.h:1024
#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.
#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:222
Pre-defined types.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
Definition std_types.h:1060
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
Author: Diffblue Ltd.