Closed-world numeric type-id registry for symbolic exception dispatch (issue #5075). More...

#include <exception_typeid.h>

Public Member Functions
	exception_typeidt ()=default
	Empty registry (populate with register_chain).
	exception_typeidt (const namespacet &ns)
	Seed the table from every type symbol's "bases" metadata reachable through `ns`; register_chain then adds throw-list ancestry on top.
void	register_chain (const std::vector< irep_idt > &chain)
	Ingest an exception type's ancestry from a THROW's exception_list (front = dynamic type, rest = its flattened transitive bases).
unsigned	id_of (const irep_idt &name)
	Stable id for `name`.
bool	is_registered (const irep_idt &name) const
	True iff `name` is an actual program type seen in a throw list (not a primitive #cpp_type, opaque, or lazily-minted name).
bool	is_subtype (const irep_idt &thrown, const irep_idt &caught) const
	Reflexive-transitive subtype test: true iff `thrown` equals `caught` or derives from it transitively through the bases graph.
std::set< unsigned >	concrete_subtype_ids (const irep_idt &caught) const
	{ id_of(T) : T <: caught } over all registered program types — the right-hand side of the catch-match guard.
std::vector< std::pair< irep_idt, unsigned > >	concrete_subtypes (const irep_idt &caught) const
	{ (T, id_of(T)) : T <: caught } over all registered program types.
std::size_t	size () const
	Number of registered program types (excludes lazily-added unknowns).

Static Public Attributes
static constexpr unsigned	no_type = 0
	Reserved id meaning "no in-flight exception type".

Detailed Description

Closed-world numeric type-id registry for symbolic exception dispatch (issue #5075).

ESBMC sees the whole program, so the set of exception types and the subtype ("is-a") relation between them are fixed once the GOTO program is built. The relation is populated from two sources: the symbol table's "bases" metadata (the namespacet constructor) and THROW exception_lists (register_chain). C++ throw lists carry a type's full flattened ancestry, so register_chain alone suffices for them; Python lists stop short (e.g. at Exception), so the symbol-table bases supply the rest (Exception -> BaseException). The typeid the dispatch guards compare against is always a thrown dynamic type.

The match guard for catch (C) becomes the finite disjunction __ESBMC_exc_typeid in concrete_subtype_ids(C) over a symbolic thrown type-id; catch (...) is just thrown == true. The relation is static (closed-world) while the thrown type stays symbolic, which is exactly what makes GOTO-level dispatch fully symbolic.

Constructor & Destructor Documentation

◆ exception_typeidt() [1/2]

exception_typeidt::exception_typeidt ( )

default

Empty registry (populate with register_chain).

◆ exception_typeidt() [2/2]

exception_typeidt::exception_typeidt ( const namespacet & ns )

explicit

Seed the table from every type symbol's "bases" metadata reachable through ns; register_chain then adds throw-list ancestry on top.

Member Function Documentation

◆ concrete_subtype_ids()

std::set< unsigned > exception_typeidt::concrete_subtype_ids ( const irep_idt & caught ) const

{ id_of(T) : T <: caught } over all registered program types — the right-hand side of the catch-match guard.

◆ concrete_subtypes()

std::vector< std::pair< irep_idt, unsigned > > exception_typeidt::concrete_subtypes ( const irep_idt & caught ) const

{ (T, id_of(T)) : T <: caught } over all registered program types.

Like concrete_subtype_ids but keeps the names, so a caller can recover each dynamic type's struct (e.g. to compute a base-subobject offset for catch-by-base binding).

◆ id_of()

unsigned exception_typeidt::id_of ( const irep_idt & name )

Stable id for name.

Names use the unprefixed convention of code_cpp_throw2t::exception_list (e.g. "std::bad_cast", never "tag-std::bad_cast"). A name absent from the program is assigned a fresh id on first request, so opaque/library types remain dispatchable.

◆ is_registered()

bool exception_typeidt::is_registered ( const irep_idt & name ) const

inline

True iff name is an actual program type seen in a throw list (not a primitive #cpp_type, opaque, or lazily-minted name).

The lowering pass only matches over registered types, so this gates whether a throw/catch can be lowered at all.

◆ is_subtype()

bool exception_typeidt::is_subtype	(	const irep_idt &	thrown,
		const irep_idt &	caught ) const

Reflexive-transitive subtype test: true iff thrown equals caught or derives from it transitively through the bases graph.

Reproduces the semantics of goto_symext::is_python_exception_subtype.

◆ register_chain()

void exception_typeidt::register_chain ( const std::vector< irep_idt > & chain )

Ingest an exception type's ancestry from a THROW's exception_list (front = dynamic type, rest = its flattened transitive bases).

Only the front is a subtype of the rest; the tail are independent bases, so they are not chained (struct D : A, B throws as [D, A, B], NOT A <: B). Idempotent; unions into any existing bases.

◆ size()

std::size_t exception_typeidt::size ( ) const

inline

Number of registered program types (excludes lazily-added unknowns).

Member Data Documentation

◆ no_type

unsigned exception_typeidt::no_type = 0

staticconstexpr

Reserved id meaning "no in-flight exception type".

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

src/goto-programs/exception_typeid.h
src/goto-programs/exception_typeid.cpp

Public Member Functions

Static Public Attributes