53 irep_idt function_identifier=function_base_name;
58 const typet void_pointer=
64 if(it->operands().size()==2)
74 if(it->operands().size()==2)
89 call->code=function_call;
97 symbol.
name=function_identifier;
122 std::istringstream str(
id2string(i_str));
129 bool x86_32_locked_atomic=
false;
133 if(instruction.empty())
137 std::cout <<
"A ********************\n";
138 for(
const auto &ins : instruction)
140 std::cout <<
"XX: " << ins.pretty() <<
'\n';
143 std::cout <<
"B ********************\n";
150 if(instruction.front().id()==ID_symbol &&
151 instruction.front().get(ID_identifier)==
"lock")
153 x86_32_locked_atomic=
true;
158 if(
pos==instruction.size())
161 if(instruction[
pos].
id()==ID_symbol)
163 command=instruction[
pos].get(ID_identifier);
167 if(command==
"xchg" || command==
"xchgl")
168 x86_32_locked_atomic=
true;
170 if(x86_32_locked_atomic)
177 t->code=
codet(ID_fence);
179 t->code.
set(ID_WWfence,
true);
180 t->code.set(ID_RRfence,
true);
181 t->code.set(ID_RWfence,
true);
182 t->code.set(ID_WRfence,
true);
185 if(command==
"fstcw" ||
191 else if(command==
"mfence" ||
197 else if(command == ID_sync)
201 t->code=
codet(ID_fence);
203 t->code.
set(ID_WWfence,
true);
204 t->code.set(ID_RRfence,
true);
205 t->code.set(ID_RWfence,
true);
206 t->code.set(ID_WRfence,
true);
207 t->code.set(ID_WWcumul,
true);
208 t->code.set(ID_RWcumul,
true);
209 t->code.set(ID_RRcumul,
true);
210 t->code.set(ID_WRcumul,
true);
212 else if(command == ID_lwsync)
216 t->code=
codet(ID_fence);
218 t->code.
set(ID_WWfence,
true);
219 t->code.set(ID_RRfence,
true);
220 t->code.set(ID_RWfence,
true);
221 t->code.set(ID_WWcumul,
true);
222 t->code.set(ID_RWcumul,
true);
223 t->code.set(ID_RRcumul,
true);
225 else if(command == ID_isync)
229 t->code=
codet(ID_fence);
234 else if(command==
"dmb" || command==
"dsb")
238 t->code=
codet(ID_fence);
240 t->code.
set(ID_WWfence,
true);
241 t->code.set(ID_RRfence,
true);
242 t->code.set(ID_RWfence,
true);
243 t->code.set(ID_WRfence,
true);
244 t->code.set(ID_WWcumul,
true);
245 t->code.set(ID_RWcumul,
true);
246 t->code.set(ID_RRcumul,
true);
247 t->code.set(ID_WRcumul,
true);
249 else if(command==
"isb")
253 t->code=
codet(ID_fence);
261 if(x86_32_locked_atomic)
266 x86_32_locked_atomic=
false;
283 bool did_something =
false;
287 if(it->is_other() && it->code.get_statement()==ID_asm)
292 did_something =
true;
297 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)
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...
Remove 'asm' statements by compiling into suitable standard code.
This class represents an instruction in the GOTO intermediate representation.
void gcc_asm_function_call(const irep_idt &function_base_name, const codet &code, goto_programt &dest)
symbol_tablet & symbol_table
instructionst::iterator targett
void process_function(goto_functionst::goto_functiont &)
removes assembler
::goto_functiont goto_functiont
void process_instruction(goto_programt::instructiont &instruction, goto_programt &dest)
removes assembler
#define forall_operands(it, expr)
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.
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.
code_asmt & to_code_asm(codet &code)
goto_functionst goto_functions
GOTO functions.
void set(const irep_namet &name, const irep_idt &value)
remove_asmt(symbol_tablet &_symbol_table)
void remove_asm(goto_functionst::goto_functiont &goto_function, symbol_tablet &symbol_table)
removes assembler