86 irep_idt function_identifier = function_base_name;
95 if(it->operands().size() == 2)
105 if(it->operands().size() == 2)
127 symbolt symbol{function_identifier, fkt_type, ID_C};
128 symbol.base_name = function_base_name;
138 "function types should match");
156 irep_idt function_identifier = function_base_name;
162 for(
const auto &op : operands)
180 symbolt symbol{function_identifier, fkt_type, ID_C};
181 symbol.base_name = function_base_name;
191 "function types should match");
213 else if(flavor == ID_msc)
230 std::istringstream str(
id2string(i_str));
236 bool unknown =
false;
237 bool x86_32_locked_atomic =
false;
241 if(instruction.empty())
245 std::cout <<
"A ********************\n";
246 for(
const auto &ins : instruction)
248 std::cout <<
"XX: " << ins.pretty() <<
'\n';
251 std::cout <<
"B ********************\n";
259 instruction.front().id() == ID_symbol &&
260 instruction.front().get(ID_identifier) ==
"lock")
262 x86_32_locked_atomic =
true;
267 if(
pos == instruction.size())
270 if(instruction[
pos].
id() == ID_symbol)
272 command = instruction[
pos].get(ID_identifier);
276 if(command ==
"xchg" || command ==
"xchgl")
277 x86_32_locked_atomic =
true;
279 if(x86_32_locked_atomic)
283 codet code_fence(ID_fence);
285 code_fence.
set(ID_WWfence,
true);
286 code_fence.
set(ID_RRfence,
true);
287 code_fence.
set(ID_RWfence,
true);
288 code_fence.
set(ID_WRfence,
true);
294 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
299 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
303 else if(command == ID_sync)
305 codet code_fence(ID_fence);
307 code_fence.
set(ID_WWfence,
true);
308 code_fence.
set(ID_RRfence,
true);
309 code_fence.
set(ID_RWfence,
true);
310 code_fence.
set(ID_WRfence,
true);
311 code_fence.
set(ID_WWcumul,
true);
312 code_fence.
set(ID_RWcumul,
true);
313 code_fence.
set(ID_RRcumul,
true);
314 code_fence.
set(ID_WRcumul,
true);
319 else if(command == ID_lwsync)
321 codet code_fence(ID_fence);
323 code_fence.
set(ID_WWfence,
true);
324 code_fence.
set(ID_RRfence,
true);
325 code_fence.
set(ID_RWfence,
true);
326 code_fence.
set(ID_WWcumul,
true);
327 code_fence.
set(ID_RWcumul,
true);
328 code_fence.
set(ID_RRcumul,
true);
333 else if(command == ID_isync)
335 codet code_fence(ID_fence);
343 else if(command ==
"dmb" || command ==
"dsb")
345 codet code_fence(ID_fence);
347 code_fence.
set(ID_WWfence,
true);
348 code_fence.
set(ID_RRfence,
true);
349 code_fence.
set(ID_RWfence,
true);
350 code_fence.
set(ID_WRfence,
true);
351 code_fence.
set(ID_WWcumul,
true);
352 code_fence.
set(ID_RWcumul,
true);
353 code_fence.
set(ID_RRcumul,
true);
354 code_fence.
set(ID_WRcumul,
true);
359 else if(command ==
"isb")
361 codet code_fence(ID_fence);
372 if(x86_32_locked_atomic)
376 x86_32_locked_atomic =
false;
401 std::istringstream str(
id2string(i_str));
407 bool unknown =
false;
408 bool x86_32_locked_atomic =
false;
412 if(instruction.empty())
416 std::cout <<
"A ********************\n";
417 for(
const auto &ins : instruction)
419 std::cout <<
"XX: " << ins.pretty() <<
'\n';
422 std::cout <<
"B ********************\n";
430 instruction.front().id() == ID_symbol &&
431 instruction.front().get(ID_identifier) ==
"lock")
433 x86_32_locked_atomic =
true;
438 if(
pos == instruction.size())
441 if(instruction[
pos].
id() == ID_symbol)
443 command = instruction[
pos].get(ID_identifier);
447 if(command ==
"xchg" || command ==
"xchgl")
448 x86_32_locked_atomic =
true;
450 if(x86_32_locked_atomic)
454 codet code_fence(ID_fence);
456 code_fence.
set(ID_WWfence,
true);
457 code_fence.
set(ID_RRfence,
true);
458 code_fence.
set(ID_RWfence,
true);
459 code_fence.
set(ID_WRfence,
true);
465 if(command ==
"fstcw" || command ==
"fnstcw" || command ==
"fldcw")
469 if(
pos != instruction.size() && instruction[
pos].id() == ID_symbol)
471 const irep_idt &name = instruction[
pos].get(ID_identifier);
475 if(entry.second == name && args[0].id() != ID_address_of)
490 "__asm_" +
id2string(command), args, code, tmp_dest);
493 command ==
"mfence" || command ==
"lfence" || command ==
"sfence")
500 if(x86_32_locked_atomic)
504 x86_32_locked_atomic =
false;
525 bool did_something =
false;
529 if(it->is_other() && it->get_other().get_statement() == ID_asm)
533 it->turn_into_skip();
534 did_something =
true;
539 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
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
const source_locationt & source_location() const
source_locationt & add_source_location()
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.
void set(const irep_idt &name, const irep_idt &value)
The null pointer constant.
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.
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 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_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 ...
const irep_idt & get_value() const
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.
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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)
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)