69 irep_idt function_identifier=function_base_name;
74 const typet void_pointer=
80 if(it->operands().size()==2)
90 if(it->operands().size()==2)
105 call->code=function_call;
113 symbol.
name=function_identifier;
114 symbol.
type=fkt_type;
136 irep_idt function_identifier = function_base_name;
151 call->code = function_call;
159 symbol.
name = function_identifier;
160 symbol.
type = fkt_type;
188 else if(flavor == ID_msc)
201 std::istringstream str(
id2string(i_str));
207 bool unknown =
false;
208 bool x86_32_locked_atomic =
false;
212 if(instruction.empty())
216 std::cout <<
"A ********************\n";
217 for(
const auto &ins : instruction)
219 std::cout <<
"XX: " << ins.pretty() <<
'\n';
222 std::cout <<
"B ********************\n";
230 instruction.front().id() == ID_symbol &&
231 instruction.front().get(ID_identifier) ==
"lock")
233 x86_32_locked_atomic =
true;
238 if(
pos == instruction.size())
241 if(instruction[
pos].
id() == ID_symbol)
243 command = instruction[
pos].get(ID_identifier);
247 if(command ==
"xchg" || command ==
"xchgl")
248 x86_32_locked_atomic =
true;
250 if(x86_32_locked_atomic)
257 t->code =
codet(ID_fence);
259 t->code.
set(ID_WWfence,
true);
260 t->code.set(ID_RRfence,
true);
261 t->code.set(ID_RWfence,
true);
262 t->code.set(ID_WRfence,
true);
265 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
270 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
274 else if(command == ID_sync)
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);
284 t->code.set(ID_WWcumul,
true);
285 t->code.set(ID_RWcumul,
true);
286 t->code.set(ID_RRcumul,
true);
287 t->code.set(ID_WRcumul,
true);
289 else if(command == ID_lwsync)
293 t->code =
codet(ID_fence);
295 t->code.
set(ID_WWfence,
true);
296 t->code.set(ID_RRfence,
true);
297 t->code.set(ID_RWfence,
true);
298 t->code.set(ID_WWcumul,
true);
299 t->code.set(ID_RWcumul,
true);
300 t->code.set(ID_RRcumul,
true);
302 else if(command == ID_isync)
306 t->code =
codet(ID_fence);
311 else if(command ==
"dmb" || command ==
"dsb")
315 t->code =
codet(ID_fence);
317 t->code.
set(ID_WWfence,
true);
318 t->code.set(ID_RRfence,
true);
319 t->code.set(ID_RWfence,
true);
320 t->code.set(ID_WRfence,
true);
321 t->code.set(ID_WWcumul,
true);
322 t->code.set(ID_RWcumul,
true);
323 t->code.set(ID_RRcumul,
true);
324 t->code.set(ID_WRcumul,
true);
326 else if(command ==
"isb")
330 t->code =
codet(ID_fence);
338 if(x86_32_locked_atomic)
343 x86_32_locked_atomic =
false;
362 std::istringstream str(
id2string(i_str));
368 bool unknown =
false;
369 bool x86_32_locked_atomic =
false;
373 if(instruction.empty())
377 std::cout <<
"A ********************\n";
378 for(
const auto &ins : instruction)
380 std::cout <<
"XX: " << ins.pretty() <<
'\n';
383 std::cout <<
"B ********************\n";
391 instruction.front().id() == ID_symbol &&
392 instruction.front().get(ID_identifier) ==
"lock")
394 x86_32_locked_atomic =
true;
399 if(
pos == instruction.size())
402 if(instruction[
pos].
id() == ID_symbol)
404 command = instruction[
pos].get(ID_identifier);
408 if(command ==
"xchg" || command ==
"xchgl")
409 x86_32_locked_atomic =
true;
411 if(x86_32_locked_atomic)
418 t->code =
codet(ID_fence);
420 t->code.
set(ID_WWfence,
true);
421 t->code.set(ID_RRfence,
true);
422 t->code.set(ID_RWfence,
true);
423 t->code.set(ID_WRfence,
true);
426 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
431 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
438 if(x86_32_locked_atomic)
443 x86_32_locked_atomic =
false;
459 bool did_something =
false;
463 if(it->is_other() && it->code.get_statement()==ID_asm)
468 did_something =
true;
473 goto_function.body.destructive_insert(next, tmp_dest);
The type of an expression.
irep_idt name
The unique identifier.
assembler_parsert assembler_parser
const std::string & id2string(const irep_idt &d)
pointer_typet pointer_type(const typet &subtype)
irep_idt mode
Language mode.
void process_instruction_gcc(const code_asmt &, goto_programt &dest)
removes gcc assembler
void destructive_append(goto_programt &p)
Appends the given program, which is destroyed.
exprt value
Initial value of symbol.
function_mapt function_map
const irep_idt & get_flavor() const
symbol_tablet symbol_table
Symbol table.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void gcc_asm_function_call(const irep_idt &function_base_name, const code_asmt &code, goto_programt &dest)
remove_asmt(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
Remove 'asm' statements by compiling into suitable standard code.
This class represents an instruction in the GOTO intermediate representation.
symbol_tablet & symbol_table
instructionst::iterator targett
void process_function(goto_functionst::goto_functiont &)
removes assembler
::goto_functiont goto_functiont
void msc_asm_function_call(const irep_idt &function_base_name, const code_asmt &code, goto_programt &dest)
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
removes assembler
#define forall_operands(it, expr)
goto_functionst & goto_functions
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
A generic container class for the GOTO intermediate representation of one function.
void remove_asm(goto_functionst &goto_functions, symbol_tablet &symbol_table)
removes assembler
typet type
Type of symbol.
const string_constantt & to_string_constant(const exprt &expr)
targett add_instruction()
Adds an instruction at the end.
irep_idt base_name
Base (non-scoped) name.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::list< instructiont > instructions
const source_locationt & source_location() const
An inline assembler statement.
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
A statement in a programming language.
#define DATA_INVARIANT(CONDITION, REASON)
void process_instruction_msc(const code_asmt &, goto_programt &dest)
removes msc assembler
code_asmt & to_code_asm(codet &code)
goto_functionst goto_functions
GOTO functions.
void set(const irep_namet &name, const irep_idt &value)