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

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

Functions
void	remove_asm (goto_functionst &, symbol_tablet &, message_handlert &)
	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). More...

void	remove_asm (goto_modelt &, message_handlert &)
	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). More...

bool	has_asm (const goto_functionst &)
	returns true iff the given goto functions use asm instructions More...

bool	has_asm (const goto_modelt &)
	returns true iff the given goto model uses asm instructions More...

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

◆ has_asm() [1/2]

bool has_asm ( const goto_functionst & goto_functions )

returns true iff the given goto functions use asm instructions

Definition at line 598 of file remove_asm.cpp.

◆ has_asm() [2/2]

bool has_asm ( const goto_modelt & goto_model )

returns true iff the given goto model uses asm instructions

Definition at line 612 of file remove_asm.cpp.

◆ remove_asm() [1/2]

void remove_asm	(	goto_functionst &	goto_functions,
		symbol_tablet &	symbol_table,
		message_handlert &	message_handler
	)

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_functions	The goto functions
symbol_table	The symbol table
message_handler	Message handler

Definition at line 575 of file remove_asm.cpp.

◆ remove_asm() [2/2]

void remove_asm	(	goto_modelt &	goto_model,
		message_handlert &	message_handler
	)