element_type_registry Class Reference

The single owner of per-instance element-type tracking for the Python frontend: "which types does this container instance hold?". More...

#include <element_type_registry.h>

Public Types
using	entry = std::pair<std::string, typet>
	A recorded element: its symbol id, empty when the type came from an annotation rather than a concrete element expression, and its type.
using	entries = std::vector<entry>

Public Member Functions
void	record (const std::string &id, const std::string &elem_id, const typet &elem_type, type_slot slot=type_slot::elements)
void	set_element_type (const std::string &id, size_t index, const typet &elem_type, type_slot slot=type_slot::elements)
	Updates the type of the element at index.
void	assign (const std::string &id, const typet &elem_type, type_slot slot=type_slot::elements)
	Replaces id's entries with one entry of elem_type, which index lookups past it reuse as the type of every element.
void	assign_from (const std::string &from, const std::string &to, type_slot slot=type_slot::elements)
	Replaces to's entries with from's, leaving to untouched when from has nothing recorded.
void	append_from (const std::string &from, const std::string &to, size_t times=1, type_slot slot=type_slot::elements)
	Appends from's entries onto to's, times over.
void	pop_last (const std::string &id, type_slot slot=type_slot::elements)
	Removes the most recently recorded entry, mirroring a pop from the end.
void	reverse (const std::string &id, type_slot slot=type_slot::elements)
	Mirrors an in-place reversal so later index-based lookups stay correct.
void	replace (const std::string &id, size_t index, const std::string &elem_id, const typet &elem_type, type_slot slot=type_slot::elements)
	Mirrors a store of elem_id, of type elem_type, into element index.
size_t	size (const std::string &id, type_slot slot=type_slot::elements) const
const entries *	find (const std::string &id, type_slot slot=type_slot::elements) const
	The recorded entries, or nullptr when nothing is recorded.
typet	element_type (const std::string &id, size_t index=0, type_slot slot=type_slot::elements) const
	The type at index, falling back to the first element's type when index is out of bounds.
typet	last_element_type (const std::string &id, type_slot slot=type_slot::elements) const
	The last recorded element's type; nil when nothing is recorded.
std::string	element_id (const std::string &id, size_t index, type_slot slot=type_slot::elements) const
	The symbol id at index; empty when out of bounds or unrecorded.
bool	has_mixed_numeric (const std::string &id, type_slot slot=type_slot::elements) const
	True when both integer and floating-point elements are recorded.
bool	mixes_str_and_number (const std::string &id, type_slot slot=type_slot::elements) const
	True when both a string and a number (int, float or bool) are recorded: no single static type reads every element.
typet	uniform_element_type (const std::string &id, type_slot slot=type_slot::elements) const
	The shared type of every recorded element, or nil when nothing is recorded or the elements disagree.
typet	numeric_element_type (const std::string &id, type_slot slot=type_slot::elements) const
	Non-throwing element type of an all-numeric instance: double_type() when int and float mix (Python promotes int to float), the single shared integer type when every element shares it, otherwise nil — including for any non-numeric element or integers of differing widths.
typet	homogeneous_element_type (const std::string &id, const std::string &func_name, type_slot slot=type_slot::elements) const
	The common element type for an operation requiring one, promoting an int/float mix to double_type() as Python does.
typet	memoized_pop_type (const std::string &site) const
	The element type already answered for one syntactic pop() site, or nil when that site has not been answered yet.
void	memoize_pop_type (const std::string &site, const typet &elem_type)
void	type_flags (const std::string &id, const type_handler &th, int &type_flag, size_t &float_type_id, type_slot slot=type_slot::elements) const
	Computes the type_flag and float_type_id encoding shared with __ESBMC_list_sort and __ESBMC_list_lt: 0 = all-integer, 1 = all-float, 2 = string, 3 = mixed int+float.

Detailed Description

The single owner of per-instance element-type tracking for the Python frontend: "which types does this container instance hold?".

One instance lives on python_converter, so the tracked state has the lifetime of a conversion rather than of the process. Every container operation that must forward element types through it — a slice, a sort, a pop, a dict subscript — consults this registry instead of reaching into a shared map, so a new operation has one place to preserve type information.

Invariant: an instance is either absent or has at least one recorded entry. Only record()/assign()/assign_from()/append_from() create entries and each adds at least one, so queries never observe a present-but-empty instance. find() therefore answers both "is anything recorded?" and "is this known?".

Member Typedef Documentation

entries

using element_type_registry::entries = std::vector<entry>

entry

using element_type_registry::entry = std::pair<std::string, typet>

A recorded element: its symbol id, empty when the type came from an annotation rather than a concrete element expression, and its type.

Member Function Documentation

append_from()

void element_type_registry::append_from	(	const std::string &	from,
		const std::string &	to,
		size_t	times = 1,
		type_slot	slot = type_slot::elements )

Appends from's entries onto to's, times over.

from is read once, so to == from (a l = l * n repetition) repeats the original sequence rather than compounding what earlier repetitions appended.

assign()

void element_type_registry::assign	(	const std::string &	id,
		const typet &	elem_type,
		type_slot	slot = type_slot::elements )

Replaces id's entries with one entry of elem_type, which index lookups past it reuse as the type of every element.

assign_from()

void element_type_registry::assign_from	(	const std::string &	from,
		const std::string &	to,
		type_slot	slot = type_slot::elements )

Replaces to's entries with from's, leaving to untouched when from has nothing recorded.

element_id()

std::string element_type_registry::element_id	(	const std::string &	id,
		size_t	index,
		type_slot	slot = type_slot::elements ) const

The symbol id at index; empty when out of bounds or unrecorded.

Unlike element_type(), an out-of-bounds index does not fall back.

element_type()

typet element_type_registry::element_type	(	const std::string &	id,
		size_t	index = 0,
		type_slot	slot = type_slot::elements ) const

The type at index, falling back to the first element's type when index is out of bounds.

Nil when nothing is recorded.

find()

const element_type_registry::entries * element_type_registry::find	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

The recorded entries, or nullptr when nothing is recorded.

has_mixed_numeric()

bool element_type_registry::has_mixed_numeric	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

True when both integer and floating-point elements are recorded.

homogeneous_element_type()

typet element_type_registry::homogeneous_element_type	(	const std::string &	id,
		const std::string &	func_name,
		type_slot	slot = type_slot::elements ) const

The common element type for an operation requiring one, promoting an int/float mix to double_type() as Python does.

Nil when nothing is recorded.

Exceptions

std::runtime_error

when the elements mix incompatibly, naming func_name.

last_element_type()

typet element_type_registry::last_element_type	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

The last recorded element's type; nil when nothing is recorded.

memoize_pop_type()

void element_type_registry::memoize_pop_type	(	const std::string &	site,
		const typet &	elem_type )

memoized_pop_type()

typet element_type_registry::memoized_pop_type

(

const std::string &

site

)

const

The element type already answered for one syntactic pop() site, or nil when that site has not been answered yet.

The assignment path converts its RHS more than once, and a pop consumes a recorded entry, so the second conversion must replay the first answer rather than consume another entry (#4780).

mixes_str_and_number()

bool element_type_registry::mixes_str_and_number	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

True when both a string and a number (int, float or bool) are recorded: no single static type reads every element.

numeric_element_type()

typet element_type_registry::numeric_element_type	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

Non-throwing element type of an all-numeric instance: double_type() when int and float mix (Python promotes int to float), the single shared integer type when every element shares it, otherwise nil — including for any non-numeric element or integers of differing widths.

pop_last()

void element_type_registry::pop_last	(	const std::string &	id,
		type_slot	slot = type_slot::elements )

Removes the most recently recorded entry, mirroring a pop from the end.

Erases the instance when its last entry goes, preserving the invariant.

record()

void element_type_registry::record	(	const std::string &	id,
		const std::string &	elem_id,
		const typet &	elem_type,
		type_slot	slot = type_slot::elements )

replace()

void element_type_registry::replace	(	const std::string &	id,
		size_t	index,
		const std::string &	elem_id,
		const typet &	elem_type,
		type_slot	slot = type_slot::elements )

Mirrors a store of elem_id, of type elem_type, into element index.

An index outside the recorded entries (e.g. one not known statically) erases the instance, since no single entry can be updated.

reverse()

void element_type_registry::reverse	(	const std::string &	id,
		type_slot	slot = type_slot::elements )

Mirrors an in-place reversal so later index-based lookups stay correct.

A no-op for an unknown or single-element instance.

set_element_type()

void element_type_registry::set_element_type	(	const std::string &	id,
		size_t	index,
		const typet &	elem_type,
		type_slot	slot = type_slot::elements )

Updates the type of the element at index.

size()

size_t element_type_registry::size	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

type_flags()

void element_type_registry::type_flags	(	const std::string &	id,
		const type_handler &	th,
		int &	type_flag,
		size_t &	float_type_id,
		type_slot	slot = type_slot::elements ) const

Computes the type_flag and float_type_id encoding shared with __ESBMC_list_sort and __ESBMC_list_lt: 0 = all-integer, 1 = all-float, 2 = string, 3 = mixed int+float.

Inspects one instance only; a caller comparing two operands (e.g. an int list against a float list) must merge both flags itself.

uniform_element_type()

typet element_type_registry::uniform_element_type	(	const std::string &	id,
		type_slot	slot = type_slot::elements ) const

The shared type of every recorded element, or nil when nothing is recorded or the elements disagree.

---

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

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