32 if(arguments.size() < 2)
35 log.
error() << identifier <<
" expects at least two arguments"
40 const exprt &ptr_arg = arguments.front();
42 if(ptr_arg.
type().
id() != ID_pointer)
45 log.
error() << identifier <<
" takes a pointer as first argument"
55 result.add_source_location() = source_location;
69 if(arguments.size() < 3)
72 log.
error() << identifier <<
" expects at least three arguments"
77 const exprt &ptr_arg = arguments.front();
79 if(ptr_arg.
type().
id() != ID_pointer)
82 log.
error() << identifier <<
" takes a pointer as first argument"
88 typet sync_return_type = subtype;
89 if(identifier == ID___sync_bool_compare_and_swap)
98 result.add_source_location() = source_location;
112 if(arguments.empty())
115 log.
error() << identifier <<
" expects at least one argument"
120 const exprt &ptr_arg = arguments.front();
122 if(ptr_arg.
type().
id() != ID_pointer)
125 log.
error() << identifier <<
" takes a pointer as first argument"
133 result.add_source_location() = source_location;
147 if(arguments.size() != 2)
154 const exprt &ptr_arg = arguments.front();
156 if(ptr_arg.
type().
id() != ID_pointer)
159 log.
error() << identifier <<
" takes a pointer as first argument"
169 result.add_source_location() = source_location;
182 if(arguments.size() != 3)
189 const exprt &ptr_arg = arguments.front();
191 if(ptr_arg.
type().
id() != ID_pointer)
194 log.
error() << identifier <<
" takes a pointer as first argument"
205 result.add_source_location() = source_location;
218 if(arguments.size() != 3)
225 const exprt &ptr_arg = arguments.front();
227 if(ptr_arg.
type().
id() != ID_pointer)
230 log.
error() << identifier <<
" takes a pointer as first argument"
241 result.add_source_location() = source_location;
255 if(arguments.size() != 3)
262 if(arguments[0].type().
id() != ID_pointer)
265 log.
error() << identifier <<
" takes a pointer as first argument"
270 if(arguments[1].type().
id() != ID_pointer)
273 log.
error() << identifier <<
" takes a pointer as second argument"
278 const exprt &ptr_arg = arguments.front();
286 result.add_source_location() = source_location;
299 if(arguments.size() != 4)
306 if(arguments[0].type().
id() != ID_pointer)
309 log.
error() << identifier <<
" takes a pointer as first argument"
314 if(arguments[1].type().
id() != ID_pointer)
317 log.
error() << identifier <<
" takes a pointer as second argument"
322 if(arguments[2].type().
id() != ID_pointer)
325 log.
error() << identifier <<
" takes a pointer as third argument"
330 const exprt &ptr_arg = arguments.front();
339 result.add_source_location() = source_location;
355 if(arguments.size() != 6)
362 if(arguments[0].type().
id() != ID_pointer)
365 log.
error() << identifier <<
" takes a pointer as first argument"
370 if(arguments[1].type().
id() != ID_pointer)
373 log.
error() << identifier <<
" takes a pointer as second argument"
379 identifier == ID___atomic_compare_exchange &&
380 arguments[2].type().
id() != ID_pointer)
383 log.
error() << identifier <<
" takes a pointer as third argument"
388 const exprt &ptr_arg = arguments.front();
394 if(identifier == ID___atomic_compare_exchange)
416 if(arguments.size() != 3)
419 log.
error() <<
"__atomic_*_fetch primitives take three arguments"
424 const exprt &ptr_arg = arguments.front();
426 if(ptr_arg.
type().
id() != ID_pointer)
430 <<
"__atomic_*_fetch primitives take a pointer as first argument"
441 result.add_source_location() = source_location;
453 if(arguments.size() != 3)
456 log.
error() <<
"__atomic_fetch_* primitives take three arguments"
461 const exprt &ptr_arg = arguments.front();
463 if(ptr_arg.
type().
id() != ID_pointer)
467 <<
"__atomic_fetch_* primitives take a pointer as first argument"
478 result.add_source_location() = source_location;
491 identifier == ID___sync_fetch_and_add ||
492 identifier == ID___sync_fetch_and_sub ||
493 identifier == ID___sync_fetch_and_or ||
494 identifier == ID___sync_fetch_and_and ||
495 identifier == ID___sync_fetch_and_xor ||
496 identifier == ID___sync_fetch_and_nand ||
497 identifier == ID___sync_add_and_fetch ||
498 identifier == ID___sync_sub_and_fetch ||
499 identifier == ID___sync_or_and_fetch ||
500 identifier == ID___sync_and_and_fetch ||
501 identifier == ID___sync_xor_and_fetch ||
502 identifier == ID___sync_nand_and_fetch ||
503 identifier == ID___sync_lock_test_and_set)
511 identifier == ID___sync_bool_compare_and_swap ||
512 identifier == ID___sync_val_compare_and_swap)
519 else if(identifier == ID___sync_lock_release)
526 else if(identifier == ID___atomic_load_n)
533 else if(identifier == ID___atomic_store_n)
540 else if(identifier == ID___atomic_exchange_n)
547 else if(identifier == ID___atomic_load || identifier == ID___atomic_store)
554 else if(identifier == ID___atomic_exchange)
562 identifier == ID___atomic_compare_exchange_n ||
563 identifier == ID___atomic_compare_exchange)
571 identifier == ID___atomic_add_fetch ||
572 identifier == ID___atomic_sub_fetch ||
573 identifier == ID___atomic_and_fetch ||
574 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_or_fetch ||
575 identifier == ID___atomic_nand_fetch)
583 identifier == ID___atomic_fetch_add ||
584 identifier == ID___atomic_fetch_sub ||
585 identifier == ID___atomic_fetch_and ||
586 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_or ||
587 identifier == ID___atomic_fetch_nand)
614 symbol_table.
add(symbol);
621 const irep_idt &identifier_with_type,
624 const std::vector<symbol_exprt> ¶meter_exprs,
633 result_symbol(identifier_with_type, type, source_location, symbol_table)
650 irep_idt op_id = identifier == ID___atomic_fetch_add
652 : identifier == ID___atomic_fetch_sub
654 : identifier == ID___atomic_fetch_or
656 : identifier == ID___atomic_fetch_and
658 : identifier == ID___atomic_fetch_xor
660 : identifier == ID___atomic_fetch_nand
663 binary_exprt op_expr{result, op_id, parameter_exprs[1], type};
668 {parameter_exprs[2]},
683 const irep_idt &identifier_with_type,
686 const std::vector<symbol_exprt> ¶meter_exprs,
695 result_symbol(identifier_with_type, type, source_location, symbol_table)
710 irep_idt op_id = identifier == ID___atomic_add_fetch
712 : identifier == ID___atomic_sub_fetch
714 : identifier == ID___atomic_or_fetch
716 : identifier == ID___atomic_and_fetch
718 : identifier == ID___atomic_xor_fetch
720 : identifier == ID___atomic_nand_fetch
723 binary_exprt op_expr{deref_ptr, op_id, parameter_exprs[1], type};
731 {parameter_exprs[2]},
746 const irep_idt &identifier_with_type,
749 const std::vector<symbol_exprt> ¶meter_exprs,
753 std::string atomic_name =
"__atomic_" +
id2string(identifier).substr(7);
754 atomic_name.replace(atomic_name.find(
"_and_"), 5,
"_");
763 std::move(arguments),
769 const irep_idt &identifier_with_type,
772 const std::vector<symbol_exprt> ¶meter_exprs,
796 const irep_idt &identifier_with_type,
799 const std::vector<symbol_exprt> ¶meter_exprs,
808 result_symbol(identifier_with_type, type, source_location, symbol_table)
846 const irep_idt &identifier_with_type,
849 const std::vector<symbol_exprt> ¶meter_exprs,
866 result_symbol(identifier_with_type, type, source_location, symbol_table)
902 const irep_idt &identifier_with_type,
905 const std::vector<symbol_exprt> ¶meter_exprs,
942 const irep_idt &identifier_with_type,
945 const std::vector<symbol_exprt> ¶meter_exprs,
963 {parameter_exprs[2]},
975 const irep_idt &identifier_with_type,
978 const std::vector<symbol_exprt> ¶meter_exprs,
988 result_symbol(identifier_with_type, type, source_location, symbol_table)
1002 const irep_idt &identifier_with_type,
1005 const std::vector<symbol_exprt> ¶meter_exprs,
1023 {parameter_exprs[2]},
1035 const irep_idt &identifier_with_type,
1038 const std::vector<symbol_exprt> ¶meter_exprs,
1047 {parameter_exprs[0],
1049 parameter_exprs[2]},
1055 const irep_idt &identifier_with_type,
1058 const std::vector<symbol_exprt> ¶meter_exprs,
1078 {parameter_exprs[3]},
1090 const irep_idt &identifier_with_type,
1093 const std::vector<symbol_exprt> ¶meter_exprs,
1103 result_symbol(identifier_with_type, type, source_location, symbol_table)
1109 {parameter_exprs[0],
1112 parameter_exprs[2]},
1120 const irep_idt &identifier_with_type,
1123 const std::vector<symbol_exprt> ¶meter_exprs,
1140 identifier_with_type,
c_bool_type(), source_location, symbol_table)
1165 {parameter_exprs[4]},
1168 success_fence.add_source_location() = source_location;
1175 {parameter_exprs[5]},
1178 failure_fence.add_source_location() = source_location;
1182 code_blockt{{std::move(assign), std::move(success_fence)}},
1183 code_blockt{{std::move(assign_not_equal), std::move(failure_fence)}}});
1195 const irep_idt &identifier_with_type,
1198 const std::vector<symbol_exprt> ¶meter_exprs,
1206 {parameter_exprs[0],
1211 parameter_exprs[5]},
1224 std::vector<symbol_exprt> parameter_exprs;
1225 parameter_exprs.reserve(code_type.
parameters().size());
1226 for(
const auto ¶meter : code_type.
parameters())
1234 identifier == ID___atomic_fetch_add ||
1235 identifier == ID___atomic_fetch_sub || identifier == ID___atomic_fetch_or ||
1236 identifier == ID___atomic_fetch_and ||
1237 identifier == ID___atomic_fetch_xor || identifier == ID___atomic_fetch_nand)
1241 identifier_with_type,
1249 identifier == ID___atomic_add_fetch ||
1250 identifier == ID___atomic_sub_fetch || identifier == ID___atomic_or_fetch ||
1251 identifier == ID___atomic_and_fetch ||
1252 identifier == ID___atomic_xor_fetch || identifier == ID___atomic_nand_fetch)
1256 identifier_with_type,
1264 identifier == ID___sync_fetch_and_add ||
1265 identifier == ID___sync_fetch_and_sub ||
1266 identifier == ID___sync_fetch_and_or ||
1267 identifier == ID___sync_fetch_and_and ||
1268 identifier == ID___sync_fetch_and_xor ||
1269 identifier == ID___sync_fetch_and_nand ||
1270 identifier == ID___sync_add_and_fetch ||
1271 identifier == ID___sync_sub_and_fetch ||
1272 identifier == ID___sync_or_and_fetch ||
1273 identifier == ID___sync_and_and_fetch ||
1274 identifier == ID___sync_xor_and_fetch ||
1275 identifier == ID___sync_nand_and_fetch)
1279 identifier_with_type,
1285 else if(identifier == ID___sync_bool_compare_and_swap)
1288 identifier_with_type, code_type, source_location, parameter_exprs, block);
1290 else if(identifier == ID___sync_val_compare_and_swap)
1293 identifier_with_type,
1300 else if(identifier == ID___sync_lock_test_and_set)
1303 identifier_with_type,
1310 else if(identifier == ID___sync_lock_release)
1313 identifier_with_type, code_type, source_location, parameter_exprs, block);
1315 else if(identifier == ID___atomic_load)
1318 identifier_with_type, code_type, source_location, parameter_exprs, block);
1320 else if(identifier == ID___atomic_load_n)
1323 identifier_with_type,
1330 else if(identifier == ID___atomic_store)
1333 identifier_with_type, code_type, source_location, parameter_exprs, block);
1335 else if(identifier == ID___atomic_store_n)
1338 identifier_with_type, code_type, source_location, parameter_exprs, block);
1340 else if(identifier == ID___atomic_exchange)
1343 identifier_with_type, code_type, source_location, parameter_exprs, block);
1345 else if(identifier == ID___atomic_exchange_n)
1348 identifier_with_type,
1355 else if(identifier == ID___atomic_compare_exchange)
1358 identifier_with_type,
1365 else if(identifier == ID___atomic_compare_exchange_n)
1368 identifier_with_type, code_type, source_location, parameter_exprs, block);
1376 statement.add_source_location() = source_location;
ANSI-C Language Type Checking.
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_tablet &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 symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
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_tablet &symbol_table, code_blockt &block)
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_tablet &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_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 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_tablet &symbol_table, code_blockt &block)
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_tablet &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_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_tablet &symbol_table, 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_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_tablet &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()
Operator to return the address of an object.
A base class for binary expressions.
symbol_tablet & symbol_table
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)
A codet representing an assignment in the program.
A codet representing sequential composition of program statements.
void add(const codet &code)
code_operandst & statements()
A codet representing the declaration of a local variable.
codet representation of an expression statement.
codet representation of an if-then-else statement.
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.
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()
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
A side_effect_exprt representation of a function call side effect.
Expression to hold a symbol (variable)
static symbol_exprt typeless(const irep_idt &id)
Generate a symbol_exprt without a proper type.
const irep_idt & get_identifier() const
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
irep_idt mode
Language mode.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
const typet & subtype() const
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.