31 if(arguments.size() < 2)
34 log.
error() << identifier <<
" expects at least two arguments"
39 const exprt &ptr_arg = arguments.front();
41 if(ptr_arg.
type().
id() != ID_pointer)
44 log.
error() << identifier <<
" takes a pointer as first argument"
54 result.add_source_location() = source_location;
68 if(arguments.size() < 3)
71 log.
error() << identifier <<
" expects at least three arguments"
76 const exprt &ptr_arg = arguments.front();
78 if(ptr_arg.
type().
id() != ID_pointer)
81 log.
error() << identifier <<
" takes a pointer as first argument"
87 typet sync_return_type = subtype;
88 if(identifier == ID___sync_bool_compare_and_swap)
97 result.add_source_location() = source_location;
111 if(arguments.empty())
114 log.
error() << identifier <<
" expects at least one argument"
119 const exprt &ptr_arg = arguments.front();
121 if(ptr_arg.
type().
id() != ID_pointer)
124 log.
error() << identifier <<
" takes a pointer as first argument"
132 result.add_source_location() = source_location;
146 if(arguments.size() != 2)
153 const exprt &ptr_arg = arguments.front();
155 if(ptr_arg.
type().
id() != ID_pointer)
158 log.
error() << identifier <<
" takes a pointer as first argument"
168 result.add_source_location() = source_location;
181 if(arguments.size() != 3)
188 const exprt &ptr_arg = arguments.front();
190 if(ptr_arg.
type().
id() != ID_pointer)
193 log.
error() << identifier <<
" takes a pointer as first argument"
204 result.add_source_location() = source_location;
217 if(arguments.size() != 3)
224 const exprt &ptr_arg = arguments.front();
226 if(ptr_arg.
type().
id() != ID_pointer)
229 log.
error() << identifier <<
" takes a pointer as first argument"
240 result.add_source_location() = source_location;
254 if(arguments.size() != 3)
261 if(arguments[0].type().
id() != ID_pointer)
264 log.
error() << identifier <<
" takes a pointer as first argument"
269 if(arguments[1].type().
id() != ID_pointer)
272 log.
error() << identifier <<
" takes a pointer as second argument"
277 const exprt &ptr_arg = arguments.front();
285 result.add_source_location() = source_location;
298 if(arguments.size() != 4)
305 if(arguments[0].type().
id() != ID_pointer)
308 log.
error() << identifier <<
" takes a pointer as first argument"
313 if(arguments[1].type().
id() != ID_pointer)
316 log.
error() << identifier <<
" takes a pointer as second argument"
321 if(arguments[2].type().
id() != ID_pointer)
324 log.
error() << identifier <<
" takes a pointer as third argument"
329 const exprt &ptr_arg = arguments.front();
338 result.add_source_location() = source_location;
354 if(arguments.size() != 6)
361 if(arguments[0].type().
id() != ID_pointer)
364 log.
error() << identifier <<
" takes a pointer as first argument"
369 if(arguments[1].type().
id() != ID_pointer)
372 log.
error() << identifier <<
" takes a pointer as second argument"
378 identifier == ID___atomic_compare_exchange &&
379 arguments[2].type().
id() != ID_pointer)
382 log.
error() << identifier <<
" takes a pointer as third argument"
387 const exprt &ptr_arg = arguments.front();
393 if(identifier == ID___atomic_compare_exchange)
415 if(arguments.size() != 3)
418 log.
error() <<
"__atomic_*_fetch primitives take three arguments"
423 const exprt &ptr_arg = arguments.front();
425 if(ptr_arg.
type().
id() != ID_pointer)
429 <<
"__atomic_*_fetch primitives take a pointer as first argument"
440 result.add_source_location() = source_location;
452 if(arguments.size() != 3)
455 log.
error() <<
"__atomic_fetch_* primitives take three arguments"
460 const exprt &ptr_arg = arguments.front();
462 if(ptr_arg.
type().
id() != ID_pointer)
466 <<
"__atomic_fetch_* primitives take a pointer as first argument"
477 result.add_source_location() = source_location;
490 identifier == ID___sync_fetch_and_add ||
491 identifier == ID___sync_fetch_and_sub ||
492 identifier == ID___sync_fetch_and_or ||
493 identifier == ID___sync_fetch_and_and ||
494 identifier == ID___sync_fetch_and_xor ||
495 identifier == ID___sync_fetch_and_nand ||
496 identifier == ID___sync_add_and_fetch ||
497 identifier == ID___sync_sub_and_fetch ||
498 identifier == ID___sync_or_and_fetch ||
499 identifier == ID___sync_and_and_fetch ||
500 identifier == ID___sync_xor_and_fetch ||
501 identifier == ID___sync_nand_and_fetch ||
502 identifier == ID___sync_lock_test_and_set)
510 identifier == ID___sync_bool_compare_and_swap ||
511 identifier == ID___sync_val_compare_and_swap)
518 else if(identifier == ID___sync_lock_release)
525 else if(identifier == ID___atomic_load_n)
532 else if(identifier == ID___atomic_store_n)
539 else if(identifier == ID___atomic_exchange_n)
546 else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
553 else if(identifier == ID___atomic_exchange)
561 identifier == ID___atomic_compare_exchange_n ||
562 identifier == ID___atomic_compare_exchange)
570 identifier == ID___atomic_add_fetch ||
571 identifier == ID___atomic_sub_fetch ||
572 identifier == ID___atomic_and_fetch ||
573 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
574 identifier == ID___atomic_nand_fetch)
582 identifier == ID___atomic_fetch_add ||
583 identifier == ID___atomic_fetch_sub ||
584 identifier == ID___atomic_fetch_and ||
585 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
586 identifier == ID___atomic_fetch_nand)
613 symbol_table.
add(symbol);
620 const irep_idt &identifier_with_type,
623 const std::vector<symbol_exprt> ¶meter_exprs,
632 result_symbol(identifier_with_type, type, source_location, symbol_table)
649 irep_idt op_id = identifier == ID___atomic_fetch_add
651 : identifier == ID___atomic_fetch_sub
653 : identifier == ID___atomic_fetch_or
655 : identifier == ID___atomic_fetch_and
657 : identifier == ID___atomic_fetch_xor
659 : identifier == ID___atomic_fetch_nand
662 binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
667 {parameter_exprs[2]},
682 const irep_idt &identifier_with_type,
685 const std::vector<symbol_exprt> ¶meter_exprs,
694 result_symbol(identifier_with_type, type, source_location, symbol_table)
709 irep_idt op_id = identifier == ID___atomic_add_fetch
711 : identifier == ID___atomic_sub_fetch
713 : identifier == ID___atomic_or_fetch
715 : identifier == ID___atomic_and_fetch
717 : identifier == ID___atomic_xor_fetch
719 : identifier == ID___atomic_nand_fetch
722 binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
730 {parameter_exprs[2]},
745 const irep_idt &identifier_with_type,
748 const std::vector<symbol_exprt> ¶meter_exprs,
752 std::string atomic_name =
"__atomic_" +
id2string(identifier).substr(7);
753 atomic_name.replace(atomic_name.find(
"_and_"), 5,
"_");
762 std::move(arguments),
768 const irep_idt &identifier_with_type,
771 const std::vector<symbol_exprt> ¶meter_exprs,
795 const irep_idt &identifier_with_type,
798 const std::vector<symbol_exprt> ¶meter_exprs,
807 result_symbol(identifier_with_type, type, source_location, symbol_table)
824 assign.add_source_location() = source_location;
845 const irep_idt &identifier_with_type,
848 const std::vector<symbol_exprt> ¶meter_exprs,
865 result_symbol(identifier_with_type, type, source_location, symbol_table)
901 const irep_idt &identifier_with_type,
904 const std::vector<symbol_exprt> ¶meter_exprs,
941 const irep_idt &identifier_with_type,
944 const std::vector<symbol_exprt> ¶meter_exprs,
962 {parameter_exprs[2]},
974 const irep_idt &identifier_with_type,
977 const std::vector<symbol_exprt> ¶meter_exprs,
987 result_symbol(identifier_with_type, type, source_location, symbol_table)
1001 const irep_idt &identifier_with_type,
1004 const std::vector<symbol_exprt> ¶meter_exprs,
1022 {parameter_exprs[2]},
1034 const irep_idt &identifier_with_type,
1037 const std::vector<symbol_exprt> ¶meter_exprs,
1046 {parameter_exprs[0],
1048 parameter_exprs[2]},
1054 const irep_idt &identifier_with_type,
1057 const std::vector<symbol_exprt> ¶meter_exprs,
1077 {parameter_exprs[3]},
1089 const irep_idt &identifier_with_type,
1092 const std::vector<symbol_exprt> ¶meter_exprs,
1102 result_symbol(identifier_with_type, type, source_location, symbol_table)
1108 {parameter_exprs[0],
1111 parameter_exprs[2]},
1119 const irep_idt &identifier_with_type,
1122 const std::vector<symbol_exprt> ¶meter_exprs,
1139 identifier_with_type,
c_bool_type(), source_location, symbol_table)
1161 assign.add_source_location() = source_location;
1164 {parameter_exprs[4]},
1167 success_fence.add_source_location() = source_location;
1171 {parameter_exprs[5]},
1174 failure_fence.add_source_location() = source_location;
1178 code_blockt{{std::move(assign), std::move(success_fence)}},
1179 std::move(failure_fence)});
1191 const irep_idt &identifier_with_type,
1194 const std::vector<symbol_exprt> ¶meter_exprs,
1202 {parameter_exprs[0],
1207 parameter_exprs[5]},
1220 std::vector<symbol_exprt> parameter_exprs;
1221 parameter_exprs.reserve(code_type.
parameters().size());
1222 for(
const auto ¶meter : code_type.
parameters())
1230 identifier == ID___atomic_fetch_add ||
1231 identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1232 identifier == ID___atomic_fetch_and ||
1233 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1237 identifier_with_type,
1245 identifier == ID___atomic_add_fetch ||
1246 identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1247 identifier == ID___atomic_and_fetch ||
1248 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1252 identifier_with_type,
1260 identifier == ID___sync_fetch_and_add ||
1261 identifier == ID___sync_fetch_and_sub ||
1262 identifier == ID___sync_fetch_and_or ||
1263 identifier == ID___sync_fetch_and_and ||
1264 identifier == ID___sync_fetch_and_xor ||
1265 identifier == ID___sync_fetch_and_nand ||
1266 identifier == ID___sync_add_and_fetch ||
1267 identifier == ID___sync_sub_and_fetch ||
1268 identifier == ID___sync_or_and_fetch ||
1269 identifier == ID___sync_and_and_fetch ||
1270 identifier == ID___sync_xor_and_fetch ||
1271 identifier == ID___sync_nand_and_fetch)
1275 identifier_with_type,
1281 else if(identifier == ID___sync_bool_compare_and_swap)
1284 identifier_with_type, code_type, source_location, parameter_exprs, block);
1286 else if(identifier == ID___sync_val_compare_and_swap)
1289 identifier_with_type,
1296 else if(identifier == ID___sync_lock_test_and_set)
1299 identifier_with_type,
1306 else if(identifier == ID___sync_lock_release)
1309 identifier_with_type, code_type, source_location, parameter_exprs, block);
1311 else if(identifier == ID___atomic_load)
1314 identifier_with_type, code_type, source_location, parameter_exprs, block);
1316 else if(identifier == ID___atomic_load_n)
1319 identifier_with_type,
1326 else if(identifier == ID___atomic_store)
1329 identifier_with_type, code_type, source_location, parameter_exprs, block);
1331 else if(identifier == ID___atomic_store_n)
1334 identifier_with_type, code_type, source_location, parameter_exprs, block);
1336 else if(identifier == ID___atomic_exchange)
1339 identifier_with_type, code_type, source_location, parameter_exprs, block);
1341 else if(identifier == ID___atomic_exchange_n)
1344 identifier_with_type,
1351 else if(identifier == ID___atomic_compare_exchange)
1354 identifier_with_type,
1361 else if(identifier == ID___atomic_compare_exchange_n)
1364 identifier_with_type, code_type, source_location, parameter_exprs, block);
1372 statement.add_source_location() = source_location;