cprover
Loading...
Searching...
No Matches
remove_asm.h File Reference

Remove 'asm' statements by compiling them into suitable standard goto program instructions. More...

+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void remove_asm (goto_functionst &, symbol_tablet &)
 Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a code member of type code_asmt) with an appropriate (sequence of) non-assembly goto program instruction(s).
 
void remove_asm (goto_modelt &)
 Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a code member of type code_asmt) with an appropriate (sequence of) non-assembly goto program instruction(s).
 

Detailed Description

Remove 'asm' statements by compiling them into suitable standard goto program instructions.

Inline assembly statements in the source program (in either gcc- or msc-style) are represented by instructions of kind OTHER with a code member of type code_asmt in the goto program.

For example, the gcc inline assembly statement below

int input = 1;
int result;
asm volatile (
"mov %1, %0; add $1, %0"
: "=r" (result)
: "r" (input)
: "cc");

would be represented by a code_asmt statement with op0() being the string literal "mov %1, %0; add $1, %0" (as a string_constantt expression) and op1(), op2(), and op3(), respectively, containing the output list, input list, and clobbered registers.

The remove_asm() function replaces the inline assembly statements in a given goto program with appropriate (sequences of) non-assembly goto program instructions.

It first parses the assembly instructions string (via assembler_parsert) and inspects the input/output/clobber lists. Then, it generates a sequence of goto program instructions that either directly implement the assembly instructions, or call a suitable library function (see library/x86_assembler.c).

At present only a small number of x86 and Power instructions are supported. Unrecognised assembly instructions are ignored (i.e., they are simply removed from the goto program).

Definition in file remove_asm.h.

Function Documentation

◆ remove_asm() [1/2]

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 code member of type code_asmt) with an appropriate (sequence of) non-assembly goto program instruction(s).

Parameters
goto_functionsThe goto functions
symbol_tableThe symbol table

Definition at line 551 of file remove_asm.cpp.

◆ remove_asm() [2/2]

void remove_asm ( goto_modelt & goto_model)

Replaces inline assembly instructions in the goto program (i.e., instructions of kind OTHER with a code member of type code_asmt) with an appropriate (sequence of) non-assembly goto program instruction(s).

At present only a small number of x86 and Power instructions are supported. Unrecognised assembly instructions are ignored.

Parameters
goto_modelThe goto model

Definition at line 564 of file remove_asm.cpp.