tuple_handler Class Reference

Handler for Python tuple operations. More...

#include <tuple_handler.h>

Public Member Functions
	tuple_handler (python_converter &converter, type_handler &type_handler)
	Construct a new tuple handler.
exprt	get_tuple_expr (const nlohmann::json &element)
	Create a tuple expression from AST elements.
exprt	handle_tuple_subscript (const exprt &array, const nlohmann::json &slice, const nlohmann::json &element)
	Handle tuple subscripting (e.g., t[0]).
bool	is_tuple_type (const typet &type) const
	Check if a type represents a tuple.
void	handle_tuple_unpacking (const nlohmann::json &ast_node, const nlohmann::json &target, exprt &rhs, codet &target_block)
	Handle tuple unpacking assignments.
typet	get_tuple_type_from_annotation (const nlohmann::json &annotation_node)
	Get tuple type from annotation (e.g., tuple[int, str]).
exprt	prepare_rhs_for_unpacking (const nlohmann::json &ast_node, exprt &rhs, codet &target_block)
	Prepare RHS for unpacking (handle function calls).
exprt	handle_tuple_membership (const exprt &lhs, const exprt &rhs, bool invert, const nlohmann::json &element)
	Handle tuple membership test (e.g., x in tuple).
struct_typet	create_tuple_struct_type (const std::vector< typet > &element_types) const
	Create a tuple struct type from element types.
exprt	get_tuple_element (const exprt &array, const struct_typet &tuple_type, size_t idx) const
	Obtain an addressable expression for tuple element idx.
exprt	coerce_to_tuple_type (const exprt &value, const typet &target, const locationt &loc, codet &target_block)
	Convert tuple value to the annotation-built tuple type target.

Static Public Attributes
static constexpr size_t	tuple_str_member_size = 16
	Fixed byte width of string tuple members (content + NUL padding).

Detailed Description

Handler for Python tuple operations.

This class manages tuple creation, subscripting, unpacking, and type handling for Python tuples in the ESBMC converter.

Constructor & Destructor Documentation

tuple_handler()

tuple_handler::tuple_handler	(	python_converter &	converter,
		type_handler &	type_handler )

Construct a new tuple handler.

Parameters

converter	Reference to the parent python_converter
type_handler	Reference to the type_handler for type operations

Member Function Documentation

coerce_to_tuple_type()

exprt tuple_handler::coerce_to_tuple_type	(	const exprt &	value,
		const typet &	target,
		const locationt &	loc,
		codet &	target_block )

Convert tuple value to the annotation-built tuple type target.

A str element held as a char* (e.g. from nondet_str() or a str parameter) is copied into the fixed-width char array member a tuple[str, ...] annotation declares, and an integer member is cast to the declared width. Any other member mismatch leaves value unchanged.

create_tuple_struct_type()

struct_typet tuple_handler::create_tuple_struct_type

(

const std::vector< typet > &

element_types

)

const

Create a tuple struct type from element types.

Parameters

element_types

Vector of types for tuple elements

Returns

struct_typet The tuple struct type with components

get_tuple_element()

exprt tuple_handler::get_tuple_element	(	const exprt &	array,
		const struct_typet &	tuple_type,
		size_t	idx ) const

Obtain an addressable expression for tuple element idx.

For an inline tuple literal (a struct_exprt whose operands are already-materialised temp symbols) a member access into the constant struct rvalue is not addressable, so any downstream address_of (e.g. a strcmp on a string element) aborts SMT encoding (#5185). In that case the operand symbol is returned directly; for a named tuple variable a member access is a proper lvalue.

Parameters

array	The tuple expression (literal or named variable)
tuple_type	The tuple struct type
idx	The element index

Returns

exprt An addressable expression denoting element idx

get_tuple_expr()

exprt tuple_handler::get_tuple_expr

(

const nlohmann::json &

element

)

Create a tuple expression from AST elements.

Parameters

element

JSON AST node representing a Tuple

Returns

exprt The tuple represented as a struct expression

get_tuple_type_from_annotation()

typet tuple_handler::get_tuple_type_from_annotation

(

const nlohmann::json &

annotation_node

)

Get tuple type from annotation (e.g., tuple[int, str]).

Parameters

annotation_node

The annotation AST node

Returns

typet The tuple struct type

handle_tuple_membership()

exprt tuple_handler::handle_tuple_membership	(	const exprt &	lhs,
		const exprt &	rhs,
		bool	invert,
		const nlohmann::json &	element )

Handle tuple membership test (e.g., x in tuple).

Parameters

lhs	The element to search for
rhs	The tuple to search in
invert	Whether this is "not in" operation
element	The original AST node (for location and string comparison)

Returns

exprt Boolean expression representing membership test

handle_tuple_subscript()

exprt tuple_handler::handle_tuple_subscript	(	const exprt &	array,
		const nlohmann::json &	slice,
		const nlohmann::json &	element )

Handle tuple subscripting (e.g., t[0]).

Parameters

array	The tuple expression to subscript
slice	The index expression
element	The original AST element for location info

Returns

exprt Member access expression for the tuple element

handle_tuple_unpacking()

void tuple_handler::handle_tuple_unpacking	(	const nlohmann::json &	ast_node,
		const nlohmann::json &	target,
		exprt &	rhs,
		codet &	target_block )

Handle tuple unpacking assignments.

Parameters

ast_node	The assignment AST node
target	The target tuple pattern (e.g., (x, y, z))
rhs	The right-hand side expression
target_block	The code block to append assignments to

is_tuple_type()

bool tuple_handler::is_tuple_type

(

const typet &

type

)

const

Check if a type represents a tuple.

Parameters

type	The type to check

Returns

bool True if the type is a tuple struct type

prepare_rhs_for_unpacking()

exprt tuple_handler::prepare_rhs_for_unpacking	(	const nlohmann::json &	ast_node,
		exprt &	rhs,
		codet &	target_block )

Prepare RHS for unpacking (handle function calls).

Parameters

ast_node	The assignment AST node
rhs	The right-hand side expression
target_block	The code block to append temporary declarations to

Returns

exprt The prepared expression (original or temporary variable)

Member Data Documentation

tuple_str_member_size

size_t tuple_handler::tuple_str_member_size = 16

staticconstexpr

Fixed byte width of string tuple members (content + NUL padding).

Tuple types built from annotations (tuple[str, ...]) cannot know each string's length, so construction and annotation agree on one static char-array width; strings needing more bytes are a conversion error.

---

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

• src/python-frontend/tuple/tuple_handler.h
• src/python-frontend/tuple/tuple_handler.cpp