78 irep_idt function_identifier = function_base_name;
87 if(it->operands().size() == 2)
97 if(it->operands().size() == 2)
118 symbol.
name = function_identifier;
119 symbol.
type = fkt_type;
132 "function types should match");
148 irep_idt function_identifier = function_base_name;
166 symbol.
name = function_identifier;
167 symbol.
type = fkt_type;
180 "function types should match");
200 else if(flavor == ID_msc)
217 std::istringstream str(
id2string(i_str));
223 bool unknown =
false;
224 bool x86_32_locked_atomic =
false;
228 if(instruction.empty())
232 std::cout <<
"A ********************\n";
233 for(
const auto &ins : instruction)
235 std::cout <<
"XX: " << ins.pretty() <<
'\n';
238 std::cout <<
"B ********************\n";
246 instruction.front().id() == ID_symbol &&
247 instruction.front().get(ID_identifier) ==
"lock")
249 x86_32_locked_atomic =
true;
254 if(
pos == instruction.size())
257 if(instruction[
pos].
id() == ID_symbol)
259 command = instruction[
pos].get(ID_identifier);
263 if(command ==
"xchg" || command ==
"xchgl")
264 x86_32_locked_atomic =
true;
266 if(x86_32_locked_atomic)
270 codet code_fence(ID_fence);
272 code_fence.
set(ID_WWfence,
true);
273 code_fence.
set(ID_RRfence,
true);
274 code_fence.
set(ID_RWfence,
true);
275 code_fence.
set(ID_WRfence,
true);
281 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
286 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
290 else if(command == ID_sync)
292 codet code_fence(ID_fence);
294 code_fence.
set(ID_WWfence,
true);
295 code_fence.
set(ID_RRfence,
true);
296 code_fence.
set(ID_RWfence,
true);
297 code_fence.
set(ID_WRfence,
true);
298 code_fence.
set(ID_WWcumul,
true);
299 code_fence.
set(ID_RWcumul,
true);
300 code_fence.
set(ID_RRcumul,
true);
301 code_fence.
set(ID_WRcumul,
true);
306 else if(command == ID_lwsync)
308 codet code_fence(ID_fence);
310 code_fence.
set(ID_WWfence,
true);
311 code_fence.
set(ID_RRfence,
true);
312 code_fence.
set(ID_RWfence,
true);
313 code_fence.
set(ID_WWcumul,
true);
314 code_fence.
set(ID_RWcumul,
true);
315 code_fence.
set(ID_RRcumul,
true);
320 else if(command == ID_isync)
322 codet code_fence(ID_fence);
330 else if(command ==
"dmb" || command ==
"dsb")
332 codet code_fence(ID_fence);
334 code_fence.
set(ID_WWfence,
true);
335 code_fence.
set(ID_RRfence,
true);
336 code_fence.
set(ID_RWfence,
true);
337 code_fence.
set(ID_WRfence,
true);
338 code_fence.
set(ID_WWcumul,
true);
339 code_fence.
set(ID_RWcumul,
true);
340 code_fence.
set(ID_RRcumul,
true);
341 code_fence.
set(ID_WRcumul,
true);
346 else if(command ==
"isb")
348 codet code_fence(ID_fence);
359 if(x86_32_locked_atomic)
363 x86_32_locked_atomic =
false;
386 std::istringstream str(
id2string(i_str));
392 bool unknown =
false;
393 bool x86_32_locked_atomic =
false;
397 if(instruction.empty())
401 std::cout <<
"A ********************\n";
402 for(
const auto &ins : instruction)
404 std::cout <<
"XX: " << ins.pretty() <<
'\n';
407 std::cout <<
"B ********************\n";
415 instruction.front().id() == ID_symbol &&
416 instruction.front().get(ID_identifier) ==
"lock")
418 x86_32_locked_atomic =
true;
423 if(
pos == instruction.size())
426 if(instruction[
pos].
id() == ID_symbol)
428 command = instruction[
pos].get(ID_identifier);
432 if(command ==
"xchg" || command ==
"xchgl")
433 x86_32_locked_atomic =
true;
435 if(x86_32_locked_atomic)
439 codet code_fence(ID_fence);
441 code_fence.
set(ID_WWfence,
true);
442 code_fence.
set(ID_RRfence,
true);
443 code_fence.
set(ID_RWfence,
true);
444 code_fence.
set(ID_WRfence,
true);
450 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
455 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
462 if(x86_32_locked_atomic)
466 x86_32_locked_atomic =
false;
485 bool did_something =
false;
489 if(it->is_other() && it->get_other().get_statement() == ID_asm)
493 it->turn_into_skip();
494 did_something =
true;
499 goto_function.body.destructive_insert(next, tmp_dest);
assembler_parsert assembler_parser
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
std::list< instructiont > instructions
codet representation of an inline assembler statement, for the gcc flavor.
codet representation of an inline assembler statement.
const irep_idt & get_flavor() const
codet representation of a function call statement.
exprt::operandst argumentst
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.
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 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_atomic_begin(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
void set(const irep_namet &name, const irep_idt &value)
goto_functionst & goto_functions
symbol_tablet & symbol_table
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
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.
void msc_asm_function_call(const irep_idt &function_base_name, 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_msc(const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in msc style) to non-assembly goto program instructions.
void process_instruction(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 gcc_asm_function_call(const irep_idt &function_base_name, const code_asm_gcct &code, goto_programt &dest)
Adds a call to a library function that implements the given gcc-style inline assembly statement.
void process_function(goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
const irep_idt & get_value() const
Expression to hold a symbol (variable)
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.
irep_idt base_name
Base (non-scoped) name.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Semantic type conversion.
The type of an expression, extends irept.
#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.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a co...
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,...
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)