34 if(arguments.size() < 2)
37 log.
error() << identifier <<
" expects at least two arguments"
42 const exprt &ptr_arg = arguments.front();
44 if(ptr_arg.
type().
id() != ID_pointer)
47 log.
error() << identifier <<
" takes a pointer as first argument"
57 result.add_source_location() = source_location;
71 if(arguments.size() < 3)
74 log.
error() << identifier <<
" expects at least three arguments"
79 const exprt &ptr_arg = arguments.front();
81 if(ptr_arg.
type().
id() != ID_pointer)
84 log.
error() << identifier <<
" takes a pointer as first argument"
90 typet sync_return_type = subtype;
91 if(identifier == ID___sync_bool_compare_and_swap)
100 result.add_source_location() = source_location;
114 if(arguments.empty())
117 log.
error() << identifier <<
" expects at least one argument"
122 const exprt &ptr_arg = arguments.front();
124 if(ptr_arg.
type().
id() != ID_pointer)
127 log.
error() << identifier <<
" takes a pointer as first argument"
135 result.add_source_location() = source_location;
149 if(arguments.size() != 2)
156 const exprt &ptr_arg = arguments.front();
158 if(ptr_arg.
type().
id() != ID_pointer)
161 log.
error() << identifier <<
" takes a pointer as first argument"
171 result.add_source_location() = source_location;
184 if(arguments.size() != 3)
191 const exprt &ptr_arg = arguments.front();
193 if(ptr_arg.
type().
id() != ID_pointer)
196 log.
error() << identifier <<
" takes a pointer as first argument"
207 result.add_source_location() = source_location;
220 if(arguments.size() != 3)
227 const exprt &ptr_arg = arguments.front();
229 if(ptr_arg.
type().
id() != ID_pointer)
232 log.
error() << identifier <<
" takes a pointer as first argument"
243 result.add_source_location() = source_location;
257 if(arguments.size() != 3)
264 if(arguments[0].type().
id() != ID_pointer)
267 log.
error() << identifier <<
" takes a pointer as first argument"
272 if(arguments[1].type().
id() != ID_pointer)
275 log.
error() << identifier <<
" takes a pointer as second argument"
280 const exprt &ptr_arg = arguments.front();
288 result.add_source_location() = source_location;
301 if(arguments.size() != 4)
308 if(arguments[0].type().
id() != ID_pointer)
311 log.
error() << identifier <<
" takes a pointer as first argument"
316 if(arguments[1].type().
id() != ID_pointer)
319 log.
error() << identifier <<
" takes a pointer as second argument"
324 if(arguments[2].type().
id() != ID_pointer)
327 log.
error() << identifier <<
" takes a pointer as third argument"
332 const exprt &ptr_arg = arguments.front();
341 result.add_source_location() = source_location;
357 if(arguments.size() != 6)
364 if(arguments[0].type().
id() != ID_pointer)
367 log.
error() << identifier <<
" takes a pointer as first argument"
372 if(arguments[1].type().
id() != ID_pointer)
375 log.
error() << identifier <<
" takes a pointer as second argument"
381 identifier == ID___atomic_compare_exchange &&
382 arguments[2].type().
id() != ID_pointer)
385 log.
error() << identifier <<
" takes a pointer as third argument"
390 const exprt &ptr_arg = arguments.front();
396 if(identifier == ID___atomic_compare_exchange)
418 if(arguments.size() != 3)
421 log.
error() <<
"__atomic_*_fetch primitives take three arguments"
426 const exprt &ptr_arg = arguments.front();
428 if(ptr_arg.
type().
id() != ID_pointer)
432 <<
"__atomic_*_fetch primitives take a pointer as first argument"
443 result.add_source_location() = source_location;
455 if(arguments.size() != 3)
458 log.
error() <<
"__atomic_fetch_* primitives take three arguments"
463 const exprt &ptr_arg = arguments.front();
465 if(ptr_arg.
type().
id() != ID_pointer)
469 <<
"__atomic_fetch_* primitives take a pointer as first argument"
480 result.add_source_location() = source_location;
493 identifier == ID___sync_fetch_and_add ||
494 identifier == ID___sync_fetch_and_sub ||
495 identifier == ID___sync_fetch_and_or ||
496 identifier == ID___sync_fetch_and_and ||
497 identifier == ID___sync_fetch_and_xor ||
498 identifier == ID___sync_fetch_and_nand ||
499 identifier == ID___sync_add_and_fetch ||
500 identifier == ID___sync_sub_and_fetch ||
501 identifier == ID___sync_or_and_fetch ||
502 identifier == ID___sync_and_and_fetch ||
503 identifier == ID___sync_xor_and_fetch ||
504 identifier == ID___sync_nand_and_fetch ||
505 identifier == ID___sync_lock_test_and_set)
513 identifier == ID___sync_bool_compare_and_swap ||
514 identifier == ID___sync_val_compare_and_swap)
521 else if(identifier == ID___sync_lock_release)
528 else if(identifier == ID___atomic_load_n)
535 else if(identifier == ID___atomic_store_n)
542 else if(identifier == ID___atomic_exchange_n)
549 else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
556 else if(identifier == ID___atomic_exchange)
564 identifier == ID___atomic_compare_exchange_n ||
565 identifier == ID___atomic_compare_exchange)
573 identifier == ID___atomic_add_fetch ||
574 identifier == ID___atomic_sub_fetch ||
575 identifier == ID___atomic_and_fetch ||
576 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
577 identifier == ID___atomic_nand_fetch)
585 identifier == ID___atomic_fetch_add ||
586 identifier == ID___atomic_fetch_sub ||
587 identifier == ID___atomic_fetch_and ||
588 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
589 identifier == ID___atomic_fetch_nand)
616 symbol_table.
add(symbol);
623 const irep_idt &identifier_with_type,
626 const std::vector<symbol_exprt> ¶meter_exprs,
635 result_symbol(identifier_with_type, type, source_location, symbol_table)
652 irep_idt op_id = identifier == ID___atomic_fetch_add
654 : identifier == ID___atomic_fetch_sub
656 : identifier == ID___atomic_fetch_or
658 : identifier == ID___atomic_fetch_and
660 : identifier == ID___atomic_fetch_xor
662 : identifier == ID___atomic_fetch_nand
665 binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
670 {parameter_exprs[2]},
685 const irep_idt &identifier_with_type,
688 const std::vector<symbol_exprt> ¶meter_exprs,
697 result_symbol(identifier_with_type, type, source_location, symbol_table)
712 irep_idt op_id = identifier == ID___atomic_add_fetch
714 : identifier == ID___atomic_sub_fetch
716 : identifier == ID___atomic_or_fetch
718 : identifier == ID___atomic_and_fetch
720 : identifier == ID___atomic_xor_fetch
722 : identifier == ID___atomic_nand_fetch
725 binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
733 {parameter_exprs[2]},
748 const irep_idt &identifier_with_type,
751 const std::vector<symbol_exprt> ¶meter_exprs,
755 std::string atomic_name =
"__atomic_" +
id2string(identifier).substr(7);
756 atomic_name.replace(atomic_name.find(
"_and_"), 5,
"_");
765 std::move(arguments),
771 const irep_idt &identifier_with_type,
774 const std::vector<symbol_exprt> ¶meter_exprs,
798 const irep_idt &identifier_with_type,
801 const std::vector<symbol_exprt> ¶meter_exprs,
810 result_symbol(identifier_with_type, type, source_location, symbol_table)
827 assign.add_source_location() = source_location;
848 const irep_idt &identifier_with_type,
851 const std::vector<symbol_exprt> ¶meter_exprs,
868 result_symbol(identifier_with_type, type, source_location, symbol_table)
904 const irep_idt &identifier_with_type,
907 const std::vector<symbol_exprt> ¶meter_exprs,
944 const irep_idt &identifier_with_type,
947 const std::vector<symbol_exprt> ¶meter_exprs,
965 {parameter_exprs[2]},
977 const irep_idt &identifier_with_type,
980 const std::vector<symbol_exprt> ¶meter_exprs,
990 result_symbol(identifier_with_type, type, source_location, symbol_table)
1004 const irep_idt &identifier_with_type,
1007 const std::vector<symbol_exprt> ¶meter_exprs,
1025 {parameter_exprs[2]},
1037 const irep_idt &identifier_with_type,
1040 const std::vector<symbol_exprt> ¶meter_exprs,
1049 {parameter_exprs[0],
1051 parameter_exprs[2]},
1057 const irep_idt &identifier_with_type,
1060 const std::vector<symbol_exprt> ¶meter_exprs,
1080 {parameter_exprs[3]},
1092 const irep_idt &identifier_with_type,
1095 const std::vector<symbol_exprt> ¶meter_exprs,
1105 result_symbol(identifier_with_type, type, source_location, symbol_table)
1111 {parameter_exprs[0],
1114 parameter_exprs[2]},
1122 const irep_idt &identifier_with_type,
1125 const std::vector<symbol_exprt> ¶meter_exprs,
1142 identifier_with_type,
c_bool_type(), source_location, symbol_table)
1164 assign.add_source_location() = source_location;
1167 {parameter_exprs[4]},
1170 success_fence.add_source_location() = source_location;
1174 assign_not_equal.add_source_location() = source_location;
1177 {parameter_exprs[5]},
1180 failure_fence.add_source_location() = source_location;
1184 code_blockt{{std::move(assign), std::move(success_fence)}},
1185 code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1197 const irep_idt &identifier_with_type,
1200 const std::vector<symbol_exprt> ¶meter_exprs,
1208 {parameter_exprs[0],
1213 parameter_exprs[5]},
1226 std::vector<symbol_exprt> parameter_exprs;
1227 parameter_exprs.reserve(code_type.
parameters().size());
1228 for(
const auto ¶meter : code_type.
parameters())
1236 identifier == ID___atomic_fetch_add ||
1237 identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1238 identifier == ID___atomic_fetch_and ||
1239 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1243 identifier_with_type,
1251 identifier == ID___atomic_add_fetch ||
1252 identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1253 identifier == ID___atomic_and_fetch ||
1254 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1258 identifier_with_type,
1266 identifier == ID___sync_fetch_and_add ||
1267 identifier == ID___sync_fetch_and_sub ||
1268 identifier == ID___sync_fetch_and_or ||
1269 identifier == ID___sync_fetch_and_and ||
1270 identifier == ID___sync_fetch_and_xor ||
1271 identifier == ID___sync_fetch_and_nand ||
1272 identifier == ID___sync_add_and_fetch ||
1273 identifier == ID___sync_sub_and_fetch ||
1274 identifier == ID___sync_or_and_fetch ||
1275 identifier == ID___sync_and_and_fetch ||
1276 identifier == ID___sync_xor_and_fetch ||
1277 identifier == ID___sync_nand_and_fetch)
1281 identifier_with_type,
1287 else if(identifier == ID___sync_bool_compare_and_swap)
1290 identifier_with_type, code_type, source_location, parameter_exprs, block);
1292 else if(identifier == ID___sync_val_compare_and_swap)
1295 identifier_with_type,
1302 else if(identifier == ID___sync_lock_test_and_set)
1305 identifier_with_type,
1312 else if(identifier == ID___sync_lock_release)
1315 identifier_with_type, code_type, source_location, parameter_exprs, block);
1317 else if(identifier == ID___atomic_load)
1320 identifier_with_type, code_type, source_location, parameter_exprs, block);
1322 else if(identifier == ID___atomic_load_n)
1325 identifier_with_type,
1332 else if(identifier == ID___atomic_store)
1335 identifier_with_type, code_type, source_location, parameter_exprs, block);
1337 else if(identifier == ID___atomic_store_n)
1340 identifier_with_type, code_type, source_location, parameter_exprs, block);
1342 else if(identifier == ID___atomic_exchange)
1345 identifier_with_type, code_type, source_location, parameter_exprs, block);
1347 else if(identifier == ID___atomic_exchange_n)
1350 identifier_with_type,
1357 else if(identifier == ID___atomic_compare_exchange)
1360 identifier_with_type,
1367 else if(identifier == ID___atomic_compare_exchange_n)
1370 identifier_with_type, code_type, source_location, parameter_exprs, block);
1378 statement.add_source_location() = source_location;
1392 if(identifier ==
"__builtin_shuffle")
1396 if(arguments.size() != 2 && arguments.size() != 3)
1399 error() <<
"__builtin_shuffle expects two or three arguments" <<
eom;
1403 for(
exprt &arg : arguments)
1405 if(arg.type().id() != ID_vector)
1408 error() <<
"__builtin_shuffle expects vector arguments" <<
eom;
1413 const exprt &arg0 = arguments[0];
1417 if(arguments.size() == 3)
1419 if(arguments[1].type() != input_vec_type)
1422 error() <<
"__builtin_shuffle expects input vectors of the same type"
1426 arg1 = arguments[1];
1428 const exprt &indices = arguments.back();
1430 const std::size_t indices_size =
1431 numeric_cast_v<std::size_t>(indices_type.
size());
1434 operands.reserve(indices_size);
1436 auto input_size = numeric_cast<mp_integer>(input_vec_type.
size());
1438 if(arg1.has_value())
1439 input_size = *input_size * 2;
1442 for(std::size_t i = 0; i < indices_size; ++i)
1448 operands.push_back(std::move(mod_index));
1453 else if(identifier ==
"__builtin_shufflevector")
1456 if(arguments.size() < 2)
1459 error() <<
"__builtin_shufflevector expects two or more arguments" <<
eom;
1464 operands.reserve(arguments.size() - 2);
1466 for(std::size_t i = 0; i < arguments.size(); ++i)
1468 exprt &arg_i = arguments[i];
1470 if(i <= 1 && arg_i.
type().
id() != ID_vector)
1473 error() <<
"__builtin_shufflevector expects two vectors as argument"
1482 error() <<
"__builtin_shufflevector expects integer index" <<
eom;
1488 const auto int_index = numeric_cast<mp_integer>(arg_i);
1491 if(*int_index == -1)
1494 operands.back().add_source_location() = source_location;
1497 operands.push_back(arg_i);