#include <dynamic_type_handler.h>

Classes
class	scope_guard
	RAII: adds dynamic_type_names to the transient tagged-name set for the duration of converting one if/else's branches; removes on exit only what it added, keeping nested invocations independent. More...

Public Member Functions
	dynamic_type_handler (python_converter &converter, type_handler &type_handler)
std::unordered_set< std::string >	detect_dynamic_type_names (const nlohmann::json &if_node) const
	Names assigned genuinely incompatible literal types across every branch of if_node, following nested if/else (including elif) on either side; a name must be assigned in every branch to qualify.
void	declare_dynamic_type_names (const std::unordered_set< std::string > &dynamic_type_names, const nlohmann::json &ast_node)
	Declares (or aliases) each name's tagged-object symbol before either branch converts, so goto-symex's struct-merge resolves the join for free.
bool	is_tagged (const std::string &name) const
	True if name currently resolves to a tagged-object symbol, either because it is one of the current if/else's dynamic-type names, or because an earlier branch join already flagged it.
std::string	tagged_symbol_id (const std::string &name) const
	The id of the symbol that currently holds name's tagged object, following the alias created for a pre-existing variable.
symbol_id	bound_symbol_id (const std::string &name) const
	The id of the symbol name binds in the scope being converted: a variable, or class C's own attribute v for a name C.v.
bool	tagged_binop_result_may_be_tagged (const std::string &op) const
	True if op on two tagged operands can produce either scalar type at runtime (only '+' today); an untagged assignment target then needs to become tagged too.
void	assign (const exprt &rhs, const locationt &location, const std::string &name, codet &target_block)
	Fills in the tagged-object fields for name from an already-converted value.
void	resolve_read (symbolt *&symbol) const
	Redirects symbol to its tagged-object alias, if a pre-existing variable was aliased for it; no-op otherwise.
exprt	handle_comparison (const std::string &op, const exprt &lhs, const exprt &rhs)
	Dispatches Eq/NotEq/Lt/LtE/Gt/GtE between a tagged-scalar operand and the other side.
exprt	handle_arithmetic (const std::string &op, const exprt &lhs, const exprt &rhs, const locationt &location)
	Dispatches Add/Sub/Div between a tagged-scalar operand and a literal.
void	guard_type_error (const std::string &op, const exprt &lhs, const exprt &rhs, const locationt &location)
	Inside a try body, raises a catchable TypeError ahead of an Add/Sub/Div or ordered comparison on the path where the operands' runtime types do not support it.
exprt	build_neg_tagged (const exprt &tagged, const locationt &location)
	Builds unary minus on a tagged-scalar operand, as 0 - tagged, after guard_type_error for that subtraction.
exprt	build_isinstance_check (const exprt &tagged, const std::string &type_name, bool type_is_user_class) const
	Builds isinstance(tagged, type_name).
exprt	build_truthiness (const exprt &tagged)
	Python truthiness of a tagged value, decided by its runtime type.
bool	detect_dynamic_return_type (const nlohmann::json &function_node) const
	True if a function's top-level if/elif/else chain – including an early return with no else, falling through to the next statement – can return genuinely incompatible kinds (num vs str) of literals or scalar-annotated parameters.
bool	parameter_call_returns_tagged (const nlohmann::json &call) const
	call goes through a parameter of the current function, and every call of that function passes a def returning a dynamic value (#9030).
bool	scope_assigns_divergent_literal_types (const std::string &name, const nlohmann::json &scope_body, const nlohmann::json &module_body=nlohmann::json()) const
	True if some top-level If in scope_body (a function body or the module body) assigns name genuinely incompatible literal kinds across every branch.
exprt	build_tagged_value (const exprt &value, const locationt &location, codet &target_block)
	Builds a tagged-object temporary from an already-converted value, for use as either a RETURN value or a function-call ARGUMENT.
exprt	build_numeric_conversion (const exprt &tagged, const typet &result_type, const locationt &location)
	int(`tagged`) or float(`tagged`), as `result_type` says: a str is parsed at runtime and raises ValueError when it does not parse, a number converts by value
void	refuse_float_tag_operation (const exprt &lhs, const exprt &rhs) const
	Throws when a tag may hold a float and lhs op rhs is not a str operation.
void	refuse_tagged_argument () const
	Throws the shared "tagged argument, no known parameter type" refusal.
void	assign_tagged_object (const exprt &rhs, const locationt &location, const std::string &name, codet &target_block)
	Whole-struct copy: fills name's tagged-object symbol from a value that is already tagged-object-typed.

Constructor & Destructor Documentation

◆ dynamic_type_handler()

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

Member Function Documentation

◆ assign()

void dynamic_type_handler::assign	(	const exprt &	rhs,
		const locationt &	location,
		const std::string &	name,
		codet &	target_block )

Fills in the tagged-object fields for name from an already-converted value.

◆ assign_tagged_object()

void dynamic_type_handler::assign_tagged_object	(	const exprt &	rhs,
		const locationt &	location,
		const std::string &	name,
		codet &	target_block )

Whole-struct copy: fills name's tagged-object symbol from a value that is already tagged-object-typed.

◆ bound_symbol_id()

symbol_id dynamic_type_handler::bound_symbol_id ( const std::string & name ) const

The id of the symbol name binds in the scope being converted: a variable, or class C's own attribute v for a name C.v.

◆ build_isinstance_check()

exprt dynamic_type_handler::build_isinstance_check	(	const exprt &	tagged,
		const std::string &	type_name,
		bool	type_is_user_class ) const

Builds isinstance(tagged, type_name).

type_is_user_class says whether type_name names a class defined in the program, which a tag can never hold

◆ build_neg_tagged()

exprt dynamic_type_handler::build_neg_tagged	(	const exprt &	tagged,
		const locationt &	location )

Builds unary minus on a tagged-scalar operand, as 0 - tagged, after guard_type_error for that subtraction.

◆ build_numeric_conversion()

exprt dynamic_type_handler::build_numeric_conversion	(	const exprt &	tagged,
		const typet &	result_type,
		const locationt &	location )

int(tagged) or float(tagged), as result_type says: a str is parsed at runtime and raises ValueError when it does not parse, a number converts by value

◆ build_tagged_value()

exprt dynamic_type_handler::build_tagged_value	(	const exprt &	value,
		const locationt &	location,
		codet &	target_block )

Builds a tagged-object temporary from an already-converted value, for use as either a RETURN value or a function-call ARGUMENT.

◆ build_truthiness()

exprt dynamic_type_handler::build_truthiness ( const exprt & tagged )

Python truthiness of a tagged value, decided by its runtime type.

◆ declare_dynamic_type_names()

void dynamic_type_handler::declare_dynamic_type_names	(	const std::unordered_set< std::string > &	dynamic_type_names,
		const nlohmann::json &	ast_node )

Declares (or aliases) each name's tagged-object symbol before either branch converts, so goto-symex's struct-merge resolves the join for free.

◆ detect_dynamic_return_type()

bool dynamic_type_handler::detect_dynamic_return_type ( const nlohmann::json & function_node ) const

True if a function's top-level if/elif/else chain – including an early return with no else, falling through to the next statement – can return genuinely incompatible kinds (num vs str) of literals or scalar-annotated parameters.

◆ detect_dynamic_type_names()

std::unordered_set< std::string > dynamic_type_handler::detect_dynamic_type_names ( const nlohmann::json & if_node ) const

Names assigned genuinely incompatible literal types across every branch of if_node, following nested if/else (including elif) on either side; a name must be assigned in every branch to qualify.

The value a name holds before the if counts as one more branch, and a name C.v stands for class C's own attribute v

◆ guard_type_error()

void dynamic_type_handler::guard_type_error	(	const std::string &	op,
		const exprt &	lhs,
		const exprt &	rhs,
		const locationt &	location )

Inside a try body, raises a catchable TypeError ahead of an Add/Sub/Div or ordered comparison on the path where the operands' runtime types do not support it.

Elsewhere the scalar helper's assert reports it.

◆ handle_arithmetic()

exprt dynamic_type_handler::handle_arithmetic	(	const std::string &	op,
		const exprt &	lhs,
		const exprt &	rhs,
		const locationt &	location )

Dispatches Add/Sub/Div between a tagged-scalar operand and a literal.

◆ handle_comparison()

exprt dynamic_type_handler::handle_comparison	(	const std::string &	op,
		const exprt &	lhs,
		const exprt &	rhs )

Dispatches Eq/NotEq/Lt/LtE/Gt/GtE between a tagged-scalar operand and the other side.

◆ is_tagged()

bool dynamic_type_handler::is_tagged ( const std::string & name ) const

True if name currently resolves to a tagged-object symbol, either because it is one of the current if/else's dynamic-type names, or because an earlier branch join already flagged it.

◆ parameter_call_returns_tagged()

bool dynamic_type_handler::parameter_call_returns_tagged ( const nlohmann::json & call ) const

call goes through a parameter of the current function, and every call of that function passes a def returning a dynamic value (#9030).

◆ refuse_float_tag_operation()

void dynamic_type_handler::refuse_float_tag_operation	(	const exprt &	lhs,
		const exprt &	rhs ) const

Throws when a tag may hold a float and lhs op rhs is not a str operation.

◆ refuse_tagged_argument()

void dynamic_type_handler::refuse_tagged_argument ( ) const

Throws the shared "tagged argument, no known parameter type" refusal.

◆ resolve_read()

void dynamic_type_handler::resolve_read ( symbolt *& symbol ) const

Redirects symbol to its tagged-object alias, if a pre-existing variable was aliased for it; no-op otherwise.

◆ scope_assigns_divergent_literal_types()

bool dynamic_type_handler::scope_assigns_divergent_literal_types	(	const std::string &	name,
		const nlohmann::json &	scope_body,
		const nlohmann::json &	module_body = nlohmann::json() ) const

True if some top-level If in scope_body (a function body or the module body) assigns name genuinely incompatible literal kinds across every branch.

◆ tagged_binop_result_may_be_tagged()

bool dynamic_type_handler::tagged_binop_result_may_be_tagged ( const std::string & op ) const

True if op on two tagged operands can produce either scalar type at runtime (only '+' today); an untagged assignment target then needs to become tagged too.

◆ tagged_symbol_id()

std::string dynamic_type_handler::tagged_symbol_id ( const std::string & name ) const

The id of the symbol that currently holds name's tagged object, following the alias created for a pre-existing variable.

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

src/python-frontend/dynamic_type/dynamic_type_handler.h
src/python-frontend/dynamic_type/dynamic_type_handler.cpp

Classes

Public Member Functions