95 irep_idt function_identifier = function_base_name;
104 if(it->operands().size() == 2)
114 if(it->operands().size() == 2)
124 arguments.size() >= n_args,
125 "insufficient number of arguments for calling " +
129 arguments.resize(n_args);
136 auto fkt =
symbol_exprt{function_identifier, fkt_type}.with_source_location(
147 symbolt symbol{function_identifier, fkt_type, ID_C};
148 symbol.base_name = function_base_name;
158 "types of function " +
id2string(function_identifier) +
" should match",
179 irep_idt function_identifier = function_base_name;
185 for(
const auto &op : operands)
193 auto fkt =
symbol_exprt{function_identifier, fkt_type}.with_source_location(
203 symbolt symbol{function_identifier, fkt_type, ID_C};
204 symbol.base_name = function_base_name;
214 "function types should match");
236 else if(flavor == ID_msc)
253 std::istringstream str(
id2string(i_str));
255 assembler_parser.in = &str;
256 assembler_parser.parse();
259 bool unknown =
false;
260 bool x86_32_locked_atomic =
false;
262 for(
const auto &instruction : assembler_parser.instructions)
264 if(instruction.empty())
268 std::cout <<
"A ********************\n";
269 for(
const auto &ins : instruction)
271 std::cout <<
"XX: " << ins.pretty() <<
'\n';
274 std::cout <<
"B ********************\n";
282 instruction.front().id() == ID_symbol &&
283 instruction.front().get(ID_identifier) ==
"lock")
285 x86_32_locked_atomic =
true;
290 if(
pos == instruction.size())
293 if(instruction[
pos].
id() == ID_symbol)
295 command = instruction[
pos].get(ID_identifier);
299 if(command ==
"xchg" || command ==
"xchgl")
300 x86_32_locked_atomic =
true;
302 if(x86_32_locked_atomic)
306 codet code_fence(ID_fence);
308 code_fence.
set(ID_WWfence,
true);
309 code_fence.
set(ID_RRfence,
true);
310 code_fence.
set(ID_RWfence,
true);
311 code_fence.
set(ID_WRfence,
true);
317 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
322 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
326 else if(command == ID_sync)
328 codet code_fence(ID_fence);
330 code_fence.
set(ID_WWfence,
true);
331 code_fence.
set(ID_RRfence,
true);
332 code_fence.
set(ID_RWfence,
true);
333 code_fence.
set(ID_WRfence,
true);
334 code_fence.
set(ID_WWcumul,
true);
335 code_fence.
set(ID_RWcumul,
true);
336 code_fence.
set(ID_RRcumul,
true);
337 code_fence.
set(ID_WRcumul,
true);
342 else if(command == ID_lwsync)
344 codet code_fence(ID_fence);
346 code_fence.
set(ID_WWfence,
true);
347 code_fence.
set(ID_RRfence,
true);
348 code_fence.
set(ID_RWfence,
true);
349 code_fence.
set(ID_WWcumul,
true);
350 code_fence.
set(ID_RWcumul,
true);
351 code_fence.
set(ID_RRcumul,
true);
356 else if(command == ID_isync)
358 codet code_fence(ID_fence);
366 else if(command ==
"dmb" || command ==
"dsb")
368 codet code_fence(ID_fence);
370 code_fence.
set(ID_WWfence,
true);
371 code_fence.
set(ID_RRfence,
true);
372 code_fence.
set(ID_RWfence,
true);
373 code_fence.
set(ID_WRfence,
true);
374 code_fence.
set(ID_WWcumul,
true);
375 code_fence.
set(ID_RWcumul,
true);
376 code_fence.
set(ID_RRcumul,
true);
377 code_fence.
set(ID_WRcumul,
true);
382 else if(command ==
"isb")
384 codet code_fence(ID_fence);
395 if(x86_32_locked_atomic)
399 x86_32_locked_atomic =
false;
424 std::istringstream str(
id2string(i_str));
426 assembler_parser.in = &str;
427 assembler_parser.parse();
430 bool unknown =
false;
431 bool x86_32_locked_atomic =
false;
433 for(
const auto &instruction : assembler_parser.instructions)
435 if(instruction.empty())
439 std::cout <<
"A ********************\n";
440 for(
const auto &ins : instruction)
442 std::cout <<
"XX: " << ins.pretty() <<
'\n';
445 std::cout <<
"B ********************\n";
453 instruction.front().id() == ID_symbol &&
454 instruction.front().get(ID_identifier) ==
"lock")
456 x86_32_locked_atomic =
true;
461 if(
pos == instruction.size())
464 if(instruction[
pos].
id() == ID_symbol)
466 command = instruction[
pos].get(ID_identifier);
470 if(command ==
"xchg" || command ==
"xchgl")
471 x86_32_locked_atomic =
true;
473 if(x86_32_locked_atomic)
477 codet code_fence(ID_fence);
479 code_fence.
set(ID_WWfence,
true);
480 code_fence.
set(ID_RRfence,
true);
481 code_fence.
set(ID_RWfence,
true);
482 code_fence.
set(ID_WRfence,
true);
488 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
492 if(
pos != instruction.size() && instruction[
pos].id() == ID_symbol)
494 const irep_idt &name = instruction[
pos].get(ID_identifier);
498 if(entry.second == name && args[0].id() != ID_address_of)
513 "__asm_" +
id2string(command), args, code, tmp_dest);
516 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
523 if(x86_32_locked_atomic)
527 x86_32_locked_atomic =
false;
548 bool did_something =
false;
552 if(it->is_other() && it->get_other().get_statement() == ID_asm)
556 it->turn_into_skip();
557 did_something =
true;
562 goto_function.body.destructive_insert(next, tmp_dest);
580 remove_asmt rem(symbol_table, goto_functions, message_handler);
601 for(
auto &instruction : function_it.second.body.instructions)
603 instruction.is_other() &&
604 instruction.get_other().get_statement() == ID_asm)
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
codet representation of an inline assembler statement, for the gcc flavor.
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
goto_instruction_codet representation of a function call statement.
exprt::operandst argumentst
std::vector< parametert > parameterst
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
std::vector< exprt > operandst
source_locationt & add_source_location()
const source_locationt & source_location() const
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & get_other() const
Get the statement for OTHER.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
static instructiont make_atomic_end(const source_locationt &l=source_locationt::nil())
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_atomic_begin(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void set(const irep_idt &name, const irep_idt &value)
The null pointer constant.
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions, message_handlert &message_handler)
goto_functionst & goto_functions
symbol_tablet & symbol_table
void process_function(const irep_idt &, goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
void process_instruction_msc(const irep_idt &, const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in msc style) to non-assembly goto program instructions.
void msc_asm_function_call(const irep_idt &function_base_name, const exprt::operandst &operands, const code_asmt &code, goto_programt &dest)
Adds a call to a library function that implements the given msc-style inline assembly statement.
void process_instruction_gcc(const code_asm_gcct &, goto_programt &dest)
Translates the given inline assembly code (in gcc style) to non-assembly goto program instructions.
message_handlert & message_handler
void gcc_asm_function_call(const irep_idt &function_base_name, const code_asm_gcct &code, std::size_t n_args, goto_programt &dest)
Adds a call to a library function that implements the given gcc-style inline assembly statement.
void process_instruction(const irep_idt &function_id, goto_programt::instructiont &instruction, goto_programt &dest)
Translates the given inline assembly code (which must be in either gcc or msc style) to non-assembly ...
void value(const irep_idt &)
Expression to hold a symbol (variable)
const symbol_base_mapt & symbol_base_map
Read-only field, used to look up symbol names given their base names.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
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.
typet type
Type of symbol.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< typename multimapt::const_iterator > equal_range(const multimapt &multimap, const typename multimapt::key_type &key)
Utility function to make equal_range method of multimap easier to use by returning a ranget object.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
bool has_asm(const goto_functionst &goto_functions)
returns true iff the given goto functions use asm instructions
Remove 'asm' statements by compiling them into suitable standard goto program instructions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
code_asm_gcct & to_code_asm_gcc(codet &code)
code_asmt & to_code_asm(codet &code)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
const string_constantt & to_string_constant(const exprt &expr)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.