36 if(arguments.size() < 2)
38 log.error().source_location = source_location;
39 log.error() << identifier <<
" expects at least two arguments"
44 const exprt &ptr_arg = arguments.front();
46 if(ptr_arg.
type().
id() != ID_pointer)
48 log.error().source_location = source_location;
49 log.error() << identifier <<
" takes a pointer as first argument"
61 result.add_source_location() = source_location;
75 if(arguments.size() < 3)
77 log.error().source_location = source_location;
78 log.error() << identifier <<
" expects at least three arguments"
83 const exprt &ptr_arg = arguments.front();
85 if(ptr_arg.
type().
id() != ID_pointer)
87 log.error().source_location = source_location;
88 log.error() << identifier <<
" takes a pointer as first argument"
94 typet sync_return_type = base_type;
95 if(identifier == ID___sync_bool_compare_and_swap)
104 result.add_source_location() = source_location;
118 if(arguments.empty())
120 log.error().source_location = source_location;
121 log.error() << identifier <<
" expects at least one argument"
126 const exprt &ptr_arg = arguments.front();
128 if(ptr_arg.
type().
id() != ID_pointer)
130 log.error().source_location = source_location;
131 log.error() << identifier <<
" takes a pointer as first argument"
139 result.add_source_location() = source_location;
153 if(arguments.size() != 2)
155 log.error().source_location = source_location;
160 const exprt &ptr_arg = arguments.front();
162 if(ptr_arg.
type().
id() != ID_pointer)
164 log.error().source_location = source_location;
165 log.error() << identifier <<
" takes a pointer as first argument"
175 result.add_source_location() = source_location;
188 if(arguments.size() != 3)
190 log.error().source_location = source_location;
195 const exprt &ptr_arg = arguments.front();
197 if(ptr_arg.
type().
id() != ID_pointer)
199 log.error().source_location = source_location;
200 log.error() << identifier <<
" takes a pointer as first argument"
213 result.add_source_location() = source_location;
226 if(arguments.size() != 3)
228 log.error().source_location = source_location;
233 const exprt &ptr_arg = arguments.front();
235 if(ptr_arg.
type().
id() != ID_pointer)
237 log.error().source_location = source_location;
238 log.error() << identifier <<
" takes a pointer as first argument"
251 result.add_source_location() = source_location;
265 if(arguments.size() != 3)
267 log.error().source_location = source_location;
272 if(arguments[0].type().
id() != ID_pointer)
274 log.error().source_location = source_location;
275 log.error() << identifier <<
" takes a pointer as first argument"
280 if(arguments[1].type().
id() != ID_pointer)
282 log.error().source_location = source_location;
283 log.error() << identifier <<
" takes a pointer as second argument"
288 const exprt &ptr_arg = arguments.front();
296 result.add_source_location() = source_location;
309 if(arguments.size() != 4)
311 log.error().source_location = source_location;
316 if(arguments[0].type().
id() != ID_pointer)
318 log.error().source_location = source_location;
319 log.error() << identifier <<
" takes a pointer as first argument"
324 if(arguments[1].type().
id() != ID_pointer)
326 log.error().source_location = source_location;
327 log.error() << identifier <<
" takes a pointer as second argument"
332 if(arguments[2].type().
id() != ID_pointer)
334 log.error().source_location = source_location;
335 log.error() << identifier <<
" takes a pointer as third argument"
340 const exprt &ptr_arg = arguments.front();
349 result.add_source_location() = source_location;
365 if(arguments.size() != 6)
367 log.error().source_location = source_location;
372 if(arguments[0].type().
id() != ID_pointer)
374 log.error().source_location = source_location;
375 log.error() << identifier <<
" takes a pointer as first argument"
380 if(arguments[1].type().
id() != ID_pointer)
382 log.error().source_location = source_location;
383 log.error() << identifier <<
" takes a pointer as second argument"
389 identifier == ID___atomic_compare_exchange &&
390 arguments[2].type().
id() != ID_pointer)
392 log.error().source_location = source_location;
393 log.error() << identifier <<
" takes a pointer as third argument"
398 const exprt &ptr_arg = arguments.front();
404 if(identifier == ID___atomic_compare_exchange)
407 parameters.push_back(
427 if(arguments.size() != 3)
429 log.error().source_location = source_location;
430 log.error() <<
"__atomic_*_fetch primitives take three arguments"
435 const exprt &ptr_arg = arguments.front();
437 if(ptr_arg.
type().
id() != ID_pointer)
439 log.error().source_location = source_location;
441 <<
"__atomic_*_fetch primitives take a pointer as first argument"
452 result.add_source_location() = source_location;
464 if(arguments.size() != 3)
466 log.error().source_location = source_location;
467 log.error() <<
"__atomic_fetch_* primitives take three arguments"
472 const exprt &ptr_arg = arguments.front();
474 if(ptr_arg.
type().
id() != ID_pointer)
476 log.error().source_location = source_location;
478 <<
"__atomic_fetch_* primitives take a pointer as first argument"
489 result.add_source_location() = source_location;
493 std::optional<symbol_exprt>
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)
523 identifier == ID___sync_bool_compare_and_swap ||
524 identifier == ID___sync_val_compare_and_swap)
531 else if(identifier == ID___sync_lock_release)
538 else if(identifier == ID___atomic_load_n)
545 else if(identifier == ID___atomic_store_n)
552 else if(identifier == ID___atomic_exchange_n)
559 else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
566 else if(identifier == ID___atomic_exchange)
574 identifier == ID___atomic_compare_exchange_n ||
575 identifier == ID___atomic_compare_exchange)
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)
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)
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;
623 symbol_table.
add(symbol);
630 const irep_idt &identifier_with_type,
633 const std::vector<symbol_exprt> ¶meter_exprs,
642 result_symbol(identifier_with_type, type, source_location, symbol_table)
659 irep_idt op_id = identifier == ID___atomic_fetch_add
661 : identifier == ID___atomic_fetch_sub
663 : identifier == ID___atomic_fetch_or
665 : identifier == ID___atomic_fetch_and
667 : identifier == ID___atomic_fetch_xor
669 : identifier == ID___atomic_fetch_nand
672 binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
678 {parameter_exprs[2]},
693 const irep_idt &identifier_with_type,
696 const std::vector<symbol_exprt> ¶meter_exprs,
705 result_symbol(identifier_with_type, type, source_location, symbol_table)
720 irep_idt op_id = identifier == ID___atomic_add_fetch
722 : identifier == ID___atomic_sub_fetch
724 : identifier == ID___atomic_or_fetch
726 : identifier == ID___atomic_and_fetch
728 : identifier == ID___atomic_xor_fetch
730 : identifier == ID___atomic_nand_fetch
733 binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
742 {parameter_exprs[2]},
757 const irep_idt &identifier_with_type,
760 const std::vector<symbol_exprt> ¶meter_exprs,
764 std::string atomic_name =
"__atomic_" +
id2string(identifier).substr(7);
765 atomic_name.replace(atomic_name.find(
"_and_"), 5,
"_");
774 std::move(arguments),
780 const irep_idt &identifier_with_type,
783 const std::vector<symbol_exprt> ¶meter_exprs,
808 const irep_idt &identifier_with_type,
811 const std::vector<symbol_exprt> ¶meter_exprs,
820 result_symbol(identifier_with_type, type, source_location, symbol_table)
858 const irep_idt &identifier_with_type,
861 const std::vector<symbol_exprt> ¶meter_exprs,
878 result_symbol(identifier_with_type, type, source_location, symbol_table)
914 const irep_idt &identifier_with_type,
917 const std::vector<symbol_exprt> ¶meter_exprs,
954 const irep_idt &identifier_with_type,
957 const std::vector<symbol_exprt> ¶meter_exprs,
976 {parameter_exprs[2]},
988 const irep_idt &identifier_with_type,
991 const std::vector<symbol_exprt> ¶meter_exprs,
1001 result_symbol(identifier_with_type, type, source_location, symbol_table)
1016 const irep_idt &identifier_with_type,
1019 const std::vector<symbol_exprt> ¶meter_exprs,
1038 {parameter_exprs[2]},
1050 const irep_idt &identifier_with_type,
1053 const std::vector<symbol_exprt> ¶meter_exprs,
1063 {parameter_exprs[0],
1065 parameter_exprs[2]},
1071 const irep_idt &identifier_with_type,
1074 const std::vector<symbol_exprt> ¶meter_exprs,
1095 {parameter_exprs[3]},
1107 const irep_idt &identifier_with_type,
1110 const std::vector<symbol_exprt> ¶meter_exprs,
1120 result_symbol(identifier_with_type, type, source_location, symbol_table)
1127 {parameter_exprs[0],
1130 parameter_exprs[2]},
1138 const irep_idt &identifier_with_type,
1141 const std::vector<symbol_exprt> ¶meter_exprs,
1158 identifier_with_type,
c_bool_type(), source_location, symbol_table)
1185 {parameter_exprs[4]},
1188 success_fence.add_source_location() = source_location;
1196 {parameter_exprs[5]},
1199 failure_fence.add_source_location() = source_location;
1203 code_blockt{{std::move(assign), std::move(success_fence)}},
1204 code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1216 const irep_idt &identifier_with_type,
1219 const std::vector<symbol_exprt> ¶meter_exprs,
1228 {parameter_exprs[0],
1233 parameter_exprs[5]},
1246 std::vector<symbol_exprt> parameter_exprs;
1247 parameter_exprs.reserve(code_type.
parameters().size());
1248 for(
const auto ¶meter : code_type.
parameters())
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)
1263 identifier_with_type,
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)
1278 identifier_with_type,
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)
1301 identifier_with_type,
1307 else if(identifier == ID___sync_bool_compare_and_swap)
1310 identifier_with_type, code_type, source_location, parameter_exprs, block);
1312 else if(identifier == ID___sync_val_compare_and_swap)
1315 identifier_with_type,
1322 else if(identifier == ID___sync_lock_test_and_set)
1325 identifier_with_type,
1332 else if(identifier == ID___sync_lock_release)
1335 identifier_with_type, code_type, source_location, parameter_exprs, block);
1337 else if(identifier == ID___atomic_load)
1340 identifier_with_type, code_type, source_location, parameter_exprs, block);
1342 else if(identifier == ID___atomic_load_n)
1345 identifier_with_type,
1352 else if(identifier == ID___atomic_store)
1355 identifier_with_type, code_type, source_location, parameter_exprs, block);
1357 else if(identifier == ID___atomic_store_n)
1360 identifier_with_type, code_type, source_location, parameter_exprs, block);
1362 else if(identifier == ID___atomic_exchange)
1365 identifier_with_type, code_type, source_location, parameter_exprs, block);
1367 else if(identifier == ID___atomic_exchange_n)
1370 identifier_with_type,
1377 else if(identifier == ID___atomic_compare_exchange)
1380 identifier_with_type,
1387 else if(identifier == ID___atomic_compare_exchange_n)
1390 identifier_with_type, code_type, source_location, parameter_exprs, block);
1398 statement.add_source_location() = source_location;
1412 if(identifier ==
"__builtin_shuffle")
1416 if(arguments.size() != 2 && arguments.size() != 3)
1419 error() <<
"__builtin_shuffle expects two or three arguments" <<
eom;
1423 for(
exprt &arg : arguments)
1425 if(arg.type().id() != ID_vector)
1428 error() <<
"__builtin_shuffle expects vector arguments" <<
eom;
1433 const exprt &arg0 = arguments[0];
1436 std::optional<exprt> arg1;
1437 if(arguments.size() == 3)
1439 if(arguments[1].type() != input_vec_type)
1442 error() <<
"__builtin_shuffle expects input vectors of the same type"
1446 arg1 = arguments[1];
1448 const exprt &indices = arguments.back();
1450 const std::size_t indices_size =
1451 numeric_cast_v<std::size_t>(indices_type.
size());
1454 operands.reserve(indices_size);
1456 auto input_size = numeric_cast<mp_integer>(input_vec_type.
size());
1458 if(arg1.has_value())
1459 input_size = *input_size * 2;
1463 for(std::size_t i = 0; i < indices_size; ++i)
1469 operands.push_back(std::move(mod_index));
1474 else if(identifier ==
"__builtin_shufflevector")
1477 if(arguments.size() < 2)
1480 error() <<
"__builtin_shufflevector expects two or more arguments" <<
eom;
1485 operands.reserve(arguments.size() - 2);
1487 for(std::size_t i = 0; i < arguments.size(); ++i)
1489 exprt &arg_i = arguments[i];
1491 if(i <= 1 && arg_i.
type().
id() != ID_vector)
1494 error() <<
"__builtin_shufflevector expects two vectors as argument"
1503 error() <<
"__builtin_shufflevector expects integer index" <<
eom;
1509 const auto int_index = numeric_cast<mp_integer>(arg_i);
1512 if(*int_index == -1)
1515 operands.back().add_source_location() = source_location;
1518 operands.push_back(arg_i);
1523 arguments[0], arguments[1], std::move(operands)};
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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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 > ¶meter_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)
signedbv_typet signed_int_type()
pointer_typet pointer_type(const typet &subtype)
bitvector_typet c_index_type()
Operator to return the address of an object.
A base class for binary expressions.
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.
void add(const codet &code)
code_operandst & statements()
codet representation of an expression statement.
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
codet representation of an if-then-else statement.
goto_instruction_codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
const typet & return_type() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
A constant literal expression.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
const irep_idt & id() const
source_locationt source_location
Class that provides messages with a built-in verbosity 'level'.
message_handlert & get_message_handler()
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
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.
A side_effect_exprt representation of a function call side effect.
exprt::operandst & arguments()
Expression to hold a symbol (variable)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
symbol_exprt & with_source_location(source_locationt location) &
Add the source location from location, if it is non-nil.
const irep_idt & get_identifier() const
The symbol table base class interface.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const constant_exprt & size() const
const typet & element_type() const
The type of the elements of the vector.
const std::string & id2string(const irep_idt &d)
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)
#define UNREACHABLE
This should be used to mark dead code.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.