type_handler Class Reference

#include <type_handler.h>

Public Member Functions
	type_handler (const python_converter &converter)
bool	is_constructor_call (const nlohmann::json &json) const
bool	is_pointer_free (const typet &t) const
bool	is_pointer_record (const typet &t) const
exprt	ptr_free_arg (const exprt &payload, const typet &elem_type) const
std::string	type_to_string (const typet &t) const
	This utility maps internal ESBMC types to their corresponding Python type strings.
std::string	get_python_type_name (const typet &t) const
	Returns the Python type name for an ESBMC type, as produced by type().
std::string	get_var_type (const std::string &var_name) const
std::string	get_var_classname (const nlohmann::json &value_node) const
typet	build_array (const typet &sub_type, const size_t size) const
	This method creates a typet representing a statically sized array.
std::vector< int >	get_array_type_shape (const typet &array_type) const
typet	get_typet (const std::string &ast_type, size_t type_size=0) const
typet	get_typet (const nlohmann::json &elem) const
std::optional< typet >	scalar_array_element_type (const nlohmann::json &elem) const
bool	has_multiple_types (const nlohmann::json &container) const
typet	get_list_type (const nlohmann::json &list_value) const
const typet	get_list_type () const
typet	get_list_element_type () const
typet	get_tagged_object_type () const
bool	is_tagged_scalar_type (const typet &t) const
exprt	tagged_scalar_type_id (const typet &type) const
exprt	tagged_scalar_type_matches (const exprt &tagged_type_id, const typet &literal_type) const
exprt	tagged_scalar_byte_size (const exprt &value) const
bool	is_string_type (const typet &t) const
bool	is_numeric_scalar_type (const typet &t) const
const typet	get_dict_type () const
typet	get_dict_type (const nlohmann::json &dict_value) const
typet	get_slice_type () const
	Returns the registered struct type used for Python slice objects.
std::string	get_operand_type (const nlohmann::json &operand) const
	This method inspects the JSON representation of a Python operand node and attempts to infer its type based on its AST node type (_type).
bool	is_2d_array (const nlohmann::json &arr) const
int	get_array_dimensions (const nlohmann::json &arr) const
size_t	get_type_width (const typet &type) const
typet	get_generic_typet (const std::string &ast_type, size_t bracket_pos, size_t type_size) const
	Convert a Python AST type to an ESBMC internal irep type.
typet	build_optional_type (const typet &base_type) const
bool	class_derives_from (const std::string &class_name, const std::string &expected_base) const
std::string	resolve_builtin_alias (const std::string &name) const
	Resolves Alias = builtin (e.g.

Static Public Member Functions
static typet	class_value_type ()
	A class used as a value that is not known statically, as a variable bound to one of several classes is: a struct holding the class's id, so two such values compare by id (#8390).
static bool	is_class_value_type (const typet &type)
static typet	python_int_typet ()
	Lowering for Python int — arbitrarily large in the language spec.
static unsigned	python_int_width ()
	Bit width of python_int_typet() — exposed for callsites that need to compute representable ranges (e.g.

Constructor & Destructor Documentation

type_handler()

type_handler::type_handler

(

const python_converter &

converter

)

Member Function Documentation

build_array()

typet type_handler::build_array	(	const typet &	sub_type,
		const size_t	size ) const

This method creates a typet representing a statically sized array.

It is typically used to model Python sequences like strings and byte arrays

build_optional_type()

typet type_handler::build_optional_type

(

const typet &

base_type

)

const

class_derives_from()

bool type_handler::class_derives_from	(	const std::string &	class_name,
		const std::string &	expected_base ) const

class_value_type()

typet type_handler::class_value_type ( )

static

A class used as a value that is not known statically, as a variable bound to one of several classes is: a struct holding the class's id, so two such values compare by id (#8390).

get_array_dimensions()

int type_handler::get_array_dimensions

(

const nlohmann::json &

arr

)

const

get_array_type_shape()

std::vector< int > type_handler::get_array_type_shape

(

const typet &

array_type

)

const

get_dict_type() [1/2]

const typet type_handler::get_dict_type

(

)

const

get_dict_type() [2/2]

typet type_handler::get_dict_type

(

const nlohmann::json &

dict_value

)

const

get_generic_typet()

typet type_handler::get_generic_typet	(	const std::string &	ast_type,
		size_t	bracket_pos,
		size_t	type_size ) const

Convert a Python AST type to an ESBMC internal irep type.

This function maps high-level Python types (from AST) to low-level internal ESBMC representations using typet. It supports core built-in types

References:

• Python 3 type system: https://docs.python.org/3/library/stdtypes.html
• ESBMC irep type system: src/util/type.h The type a generic spelling Base[...] names: its base type, except that "Optional[T]" spelled as one name (a preprocessor-generated or inferred annotation) resolves like the Optional[T] subscript does (#8016).

get_list_element_type()

typet type_handler::get_list_element_type

(

)

const

get_list_type() [1/2]

const typet type_handler::get_list_type

(

)

const

get_list_type() [2/2]

typet type_handler::get_list_type

(

const nlohmann::json &

list_value

)

const

get_operand_type()

std::string type_handler::get_operand_type

(

const nlohmann::json &

operand

)

const

This method inspects the JSON representation of a Python operand node and attempts to infer its type based on its AST node type (_type).

It currently supports variable names, constants (literals), and list subscripts. This type information is used for symbolic execution or translation within ESBMC.

get_python_type_name()

std::string type_handler::get_python_type_name

(

const typet &

t

)

const

Returns the Python type name for an ESBMC type, as produced by type().

Maps: bool→"bool", floatbv→"float", signedbv/unsignedbv→"int", char array/pointer→"str", complex→"complex", struct→class name.

get_slice_type()

typet type_handler::get_slice_type

(

)

const

Returns the registered struct type used for Python slice objects.

The struct is defined in c2goto/library/python/python_types.h as __ESBMC_PySliceObj. The frontend constructs values of this type when lowering Slice AST nodes and the slice() builtin.

get_tagged_object_type()

typet type_handler::get_tagged_object_type

(

)

const

get_type_width()

size_t type_handler::get_type_width

(

const typet &

type

)

const

get_typet() [1/2]

typet type_handler::get_typet

(

const nlohmann::json &

elem

)

const

get_typet() [2/2]

typet type_handler::get_typet	(	const std::string &	ast_type,
		size_t	type_size = 0 ) const

get_var_classname()

std::string type_handler::get_var_classname

(

const nlohmann::json &

value_node

)

const

get_var_type()

std::string type_handler::get_var_type

(

const std::string &

var_name

)

const

has_multiple_types()

bool type_handler::has_multiple_types

(

const nlohmann::json &

container

)

const

is_2d_array()

bool type_handler::is_2d_array

(

const nlohmann::json &

arr

)

const

is_class_value_type()

bool type_handler::is_class_value_type ( const typet & type )

static

is_constructor_call()

bool type_handler::is_constructor_call

(

const nlohmann::json &

json

)

const

is_numeric_scalar_type()

bool type_handler::is_numeric_scalar_type

(

const typet &

t

)

const

is_pointer_free()

bool type_handler::is_pointer_free

(

const typet &

t

)

const

is_pointer_record()

bool type_handler::is_pointer_record

(

const typet &

t

)

const

is_string_type()

bool type_handler::is_string_type

(

const typet &

t

)

const

is_tagged_scalar_type()

bool type_handler::is_tagged_scalar_type

(

const typet &

t

)

const

ptr_free_arg()

exprt type_handler::ptr_free_arg	(	const exprt &	payload,
		const typet &	elem_type ) const

python_int_typet()

typet type_handler::python_int_typet ( )

static

Lowering for Python int — arbitrarily large in the language spec.

Default (bitvector backends): int64 approximation via long_long_int_type(). Under –ir (int-encoding=true): a wide signed bitvector. SMT layer strips the width at conversion time, giving true unbounded semantics; the width exists only to keep the IR self-consistent and to size constant-fold intermediate values. See issue #4642.

python_int_width()

unsigned type_handler::python_int_width ( )

static

Bit width of python_int_typet() — exposed for callsites that need to compute representable ranges (e.g.

constant-fold exponent caps).

resolve_builtin_alias()

std::string type_handler::resolve_builtin_alias

(

const std::string &

name

)

const

Resolves Alias = builtin (e.g.

Bytes32 = bytes) to the builtin's name, or "" if name is not such an alias.

scalar_array_element_type()

std::optional< typet > type_handler::scalar_array_element_type

(

const nlohmann::json &

elem

)

const

tagged_scalar_byte_size()

exprt type_handler::tagged_scalar_byte_size

(

const exprt &

value

)

const

tagged_scalar_type_id()

exprt type_handler::tagged_scalar_type_id

(

const typet &

type

)

const

tagged_scalar_type_matches()

exprt type_handler::tagged_scalar_type_matches	(	const exprt &	tagged_type_id,
		const typet &	literal_type ) const

type_to_string()

std::string type_handler::type_to_string

(

const typet &

t

)

const

This utility maps internal ESBMC types to their corresponding Python type strings.

---

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

• src/python-frontend/type/type_handler.h
• src/python-frontend/type/type_handler.cpp