Go to the documentation of this file.
77 irep_idt function_identifier=function_base_name;
82 const typet void_pointer=
88 if(it->operands().size()==2)
98 if(it->operands().size()==2)
113 call->code=function_call;
121 symbol.
name=function_identifier;
122 symbol.
type=fkt_type;
151 irep_idt function_identifier = function_base_name;
163 call->code = function_call;
171 symbol.
name = function_identifier;
172 symbol.
type = fkt_type;
205 else if(flavor == ID_msc)
222 std::istringstream str(
id2string(i_str));
228 bool unknown =
false;
229 bool x86_32_locked_atomic =
false;
233 if(instruction.empty())
237 std::cout <<
"A ********************\n";
238 for(
const auto &ins : instruction)
240 std::cout <<
"XX: " << ins.pretty() <<
'\n';
243 std::cout <<
"B ********************\n";
251 instruction.front().id() == ID_symbol &&
252 instruction.front().get(ID_identifier) ==
"lock")
254 x86_32_locked_atomic =
true;
259 if(
pos == instruction.size())
262 if(instruction[
pos].
id() == ID_symbol)
264 command = instruction[
pos].get(ID_identifier);
268 if(command ==
"xchg" || command ==
"xchgl")
269 x86_32_locked_atomic =
true;
271 if(x86_32_locked_atomic)
278 t->code =
codet(ID_fence);
280 t->code.
set(ID_WWfence,
true);
281 t->code.set(ID_RRfence,
true);
282 t->code.set(ID_RWfence,
true);
283 t->code.set(ID_WRfence,
true);
286 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
291 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
295 else if(command == ID_sync)
299 t->code =
codet(ID_fence);
301 t->code.
set(ID_WWfence,
true);
302 t->code.set(ID_RRfence,
true);
303 t->code.set(ID_RWfence,
true);
304 t->code.set(ID_WRfence,
true);
305 t->code.set(ID_WWcumul,
true);
306 t->code.set(ID_RWcumul,
true);
307 t->code.set(ID_RRcumul,
true);
308 t->code.set(ID_WRcumul,
true);
310 else if(command == ID_lwsync)
314 t->code =
codet(ID_fence);
316 t->code.
set(ID_WWfence,
true);
317 t->code.set(ID_RRfence,
true);
318 t->code.set(ID_RWfence,
true);
319 t->code.set(ID_WWcumul,
true);
320 t->code.set(ID_RWcumul,
true);
321 t->code.set(ID_RRcumul,
true);
323 else if(command == ID_isync)
327 t->code =
codet(ID_fence);
332 else if(command ==
"dmb" || command ==
"dsb")
336 t->code =
codet(ID_fence);
338 t->code.
set(ID_WWfence,
true);
339 t->code.set(ID_RRfence,
true);
340 t->code.set(ID_RWfence,
true);
341 t->code.set(ID_WRfence,
true);
342 t->code.set(ID_WWcumul,
true);
343 t->code.set(ID_RWcumul,
true);
344 t->code.set(ID_RRcumul,
true);
345 t->code.set(ID_WRcumul,
true);
347 else if(command ==
"isb")
351 t->code =
codet(ID_fence);
359 if(x86_32_locked_atomic)
364 x86_32_locked_atomic =
false;
387 std::istringstream str(
id2string(i_str));
393 bool unknown =
false;
394 bool x86_32_locked_atomic =
false;
398 if(instruction.empty())
402 std::cout <<
"A ********************\n";
403 for(
const auto &ins : instruction)
405 std::cout <<
"XX: " << ins.pretty() <<
'\n';
408 std::cout <<
"B ********************\n";
416 instruction.front().id() == ID_symbol &&
417 instruction.front().get(ID_identifier) ==
"lock")
419 x86_32_locked_atomic =
true;
424 if(
pos == instruction.size())
427 if(instruction[
pos].
id() == ID_symbol)
429 command = instruction[
pos].get(ID_identifier);
433 if(command ==
"xchg" || command ==
"xchgl")
434 x86_32_locked_atomic =
true;
436 if(x86_32_locked_atomic)
443 t->code =
codet(ID_fence);
445 t->code.
set(ID_WWfence,
true);
446 t->code.set(ID_RRfence,
true);
447 t->code.set(ID_RWfence,
true);
448 t->code.set(ID_WRfence,
true);
451 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
456 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
463 if(x86_32_locked_atomic)
468 x86_32_locked_atomic =
false;
487 bool did_something =
false;
491 if(it->is_other() && it->code.get_statement()==ID_asm)
496 did_something =
true;
499 instruction.function = it->function;
504 goto_function.body.destructive_insert(next, tmp_dest);
#define Forall_goto_program_instructions(it, program)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
codet representation of an inline assembler statement.
The type of an expression, extends irept.
goto_functionst & goto_functions
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
const string_constantt & to_string_constant(const exprt &expr)
irep_idt base_name
Base (non-scoped) name.
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.
function_mapt function_map
Expression to hold a symbol (variable)
assembler_parsert assembler_parser
void process_function(goto_functionst::goto_functiont &)
Replaces inline assembly instructions in the goto function by non-assembly goto program instructions.
targett add_instruction()
Adds an instruction at the end.
codet representation of a function call statement.
irep_idt mode
Language mode.
The void type, the same as empty_typet.
const std::string & id2string(const irep_idt &d)
#define forall_operands(it, expr)
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
pointer_typet pointer_type(const typet &subtype)
std::list< instructiont > instructions
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
::goto_functiont goto_functiont
code_asmt & to_code_asm(codet &code)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
exprt value
Initial value of symbol.
goto_functionst goto_functions
GOTO functions.
void set(const irep_namet &name, const irep_idt &value)
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...
A generic container class for the GOTO intermediate representation of one function.
Operator to return the address of an object.
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.
const irep_idt & get_flavor() const
Semantic type conversion.
symbol_tablet & symbol_table
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
irep_idt name
The unique identifier.
instructionst::iterator targett
void gcc_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 gcc-style inline assembly statement.
void process_instruction_gcc(const code_asmt &, goto_programt &dest)
Translates the given inline assembly code (in gcc 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 ...
Data structure for representing an arbitrary statement in a program.