Class for saving the internal state of the conversion process. More...

#include <expr2statement_list.h>

Collaboration diagram for expr2stlt:

Public Member Functions
	expr2stlt (const namespacet &ns)
	Creates a new instance of the converter. More...

std::string	convert (const exprt &expr)
	Invokes the conversion process for the given expression and calls itself recursively in the process. More...

Private Member Functions
void	convert (const and_exprt &expr)
	Converts the given AND expression to human-readable STL code. More...

void	convert (const or_exprt &expr)
	Converts the given OR expression to human-readable STL code. More...

void	convert (const xor_exprt &expr)
	Converts the given XOR expression to human-readable STL code. More...

void	convert (const notequal_exprt &expr)
	Converts the given notequal (!=) expression to human-readable STL code. More...

void	convert (const equal_exprt &expr)
	Converts the given equal (==) expression to human-readable STL code. More...

void	convert (const not_exprt &expr)
	Converts the given NOT expression to human-readable STL code. More...

void	convert (const symbol_exprt &expr)
	Converts the given symbol expression to human-readable STL code. More...

void	convert_multiary_bool (std::vector< exprt > &operands, const char operation)
	Iterates through all the given operands and converts them depending on the operation. More...

void	convert_multiary_bool_operands (const std::vector< exprt > &operands, const char operation)
	Iterates through all the given operands and converts them depending on the operation. More...

void	convert_bool_operand (const exprt &op)
	Converts a single boolean operand and introduces an additional nesting layer if needed. More...

void	convert_first_non_trivial_operand (std::vector< exprt > &operands)
	Iterates through all the given operands in search for the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol). More...

irep_idt	id_shorthand (const irep_idt &identifier)
	Returns the given identifier in a form that is compatible with STL by looking up the symbol or cutting the scope when needed. More...

Private Attributes
bool	inside_bit_string
	Internal representation of the FC bit in STL. More...

bool	is_reference
	Flag to specify if the next symbol to convert is a reference to a variable. More...

const namespacet &	ns
	Contains the symbol table of the current program to convert. More...

std::stringstream	result
	Used for saving intermediate results of the conversion process. More...

Detailed Description

Class for saving the internal state of the conversion process.

Definition at line 40 of file expr2statement_list.h.

Constructor & Destructor Documentation

◆ expr2stlt()

expr2stlt::expr2stlt ( const namespacet & ns )

explicit

Creates a new instance of the converter.

Parameters

ns	Namespace containing the symbols of the program to convert.

Definition at line 123 of file expr2statement_list.cpp.

Member Function Documentation

◆ convert() [1/8]

void expr2stlt::convert ( const and_exprt & expr )

private

Converts the given AND expression to human-readable STL code.

If the expression marks the beginning of a bit string, the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol) is being converted first. This reduces nesting.

Parameters

expr	AND expression to convert.

Definition at line 154 of file expr2statement_list.cpp.

◆ convert() [2/8]

void expr2stlt::convert ( const equal_exprt & expr )

private

Converts the given equal (==) expression to human-readable STL code.

If the expression marks the beginning of a bit string, the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol) is being converted first. This reduces nesting.

Parameters

expr	Equal expression to convert.

Definition at line 178 of file expr2statement_list.cpp.

◆ convert() [3/8]

std::string expr2stlt::convert ( const exprt & expr )

Invokes the conversion process for the given expression and calls itself recursively in the process.

Parameters

expr	Expression to convert. Operands of this expression will be converted as well via recursion.

Returns: String containing human-readable STL code for the expression.

Definition at line 128 of file expr2statement_list.cpp.

◆ convert() [4/8]

void expr2stlt::convert ( const not_exprt & expr )

private

Converts the given NOT expression to human-readable STL code.

This function may only be called in the case of a new bit string. If the NOT expression wraps a symbol it is negated and loaded on the RLO via a simple AN instruction. In the case of a more complex expression, the expression is being converted first and negated afterwards.

Parameters

expr	Not expression to convert.

Definition at line 185 of file expr2statement_list.cpp.

◆ convert() [5/8]

void expr2stlt::convert ( const notequal_exprt & expr )

private

Converts the given notequal (!=) expression to human-readable STL code.

If the expression marks the beginning of a bit string, the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol) is being converted first. This reduces nesting.

Parameters

expr	Notequal expression to convert.

Definition at line 172 of file expr2statement_list.cpp.

◆ convert() [6/8]

void expr2stlt::convert ( const or_exprt & expr )

private

Converts the given OR expression to human-readable STL code.

If the expression marks the beginning of a bit string, the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol) is being converted first. This reduces nesting.

Parameters

expr	OR expression to convert.

Definition at line 160 of file expr2statement_list.cpp.

◆ convert() [7/8]

void expr2stlt::convert ( const symbol_exprt & expr )

private

Converts the given symbol expression to human-readable STL code.

This function also checks if the symbol should be a reference and adds the additional code if needed.

Parameters

expr	Symbol expression to convert.

Definition at line 207 of file expr2statement_list.cpp.

◆ convert() [8/8]

void expr2stlt::convert ( const xor_exprt & expr )

private

Converts the given XOR expression to human-readable STL code.

If the expression marks the beginning of a bit string, the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol) is being converted first. This reduces nesting.

Parameters

expr	XOR expression to convert.

Definition at line 166 of file expr2statement_list.cpp.

◆ convert_bool_operand()

void expr2stlt::convert_bool_operand ( const exprt & op )

private

Converts a single boolean operand and introduces an additional nesting layer if needed.

Definition at line 249 of file expr2statement_list.cpp.

◆ convert_first_non_trivial_operand()

void expr2stlt::convert_first_non_trivial_operand ( std::vector< exprt > & operands )

private

Iterates through all the given operands in search for the first non-trivial operand (that encloses all expressions which are not a symbol or a negation of a symbol).

If found, removes the operand from the list and converts it first. This is used to avoid unnecessary nesting.

Parameters

[out] operands List of operands. Gets modified by this function if it includes a non-trivial operand.

Definition at line 267 of file expr2statement_list.cpp.

◆ convert_multiary_bool()

void expr2stlt::convert_multiary_bool	(	std::vector< exprt > &	operands,
		const char	operation
	)

private

Iterates through all the given operands and converts them depending on the operation.

Performs a simplification by rearranging the operands if appropriate.

Parameters

[out]	operands	Operands of any multiary instruction.
	operation	Character specifying the operation in STL.

Definition at line 217 of file expr2statement_list.cpp.

◆ convert_multiary_bool_operands()

void expr2stlt::convert_multiary_bool_operands	(	const std::vector< exprt > &	operands,
		const char	operation
	)

private

Iterates through all the given operands and converts them depending on the operation.

Parameters

operands	Operands of any multiary instruction.
operation	Character specifying the operation in STL.

Definition at line 230 of file expr2statement_list.cpp.

◆ id_shorthand()

irep_idt expr2stlt::id_shorthand ( const irep_idt & identifier )

private

Returns the given identifier in a form that is compatible with STL by looking up the symbol or cutting the scope when needed.

Parameters

identifier Identifier that should be converted.

Returns: Converted identifier.

Definition at line 291 of file expr2statement_list.cpp.

Member Data Documentation

◆ inside_bit_string

bool expr2stlt::inside_bit_string

private

Internal representation of the FC bit in STL.

Used to track if the current boolean operation is part of another.

Definition at line 44 of file expr2statement_list.h.

◆ is_reference

bool expr2stlt::is_reference

private

Flag to specify if the next symbol to convert is a reference to a variable.

Definition at line 48 of file expr2statement_list.h.

◆ ns

const namespacet& expr2stlt::ns

private

Contains the symbol table of the current program to convert.

Definition at line 51 of file expr2statement_list.h.

◆ result

std::stringstream expr2stlt::result

private

Used for saving intermediate results of the conversion process.

Definition at line 54 of file expr2statement_list.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/statement-list/converters/expr2statement_list.h
/home/runner/work/cbmc/cbmc/src/statement-list/converters/expr2statement_list.cpp

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ expr2stlt()

Member Function Documentation

◆ convert() [1/8]

◆ convert() [2/8]

◆ convert() [3/8]

◆ convert() [4/8]

◆ convert() [5/8]

◆ convert() [6/8]

◆ convert() [7/8]

◆ convert() [8/8]

◆ convert_bool_operand()

◆ convert_first_non_trivial_operand()

◆ convert_multiary_bool()

◆ convert_multiary_bool_operands()

◆ id_shorthand()

Member Data Documentation

◆ inside_bit_string

◆ is_reference

◆ ns

◆ result