Main converter for transforming Python AST into ESBMC's intermediate representation. More...

#include <python_converter.h>

Classes
struct	scope_bindings
	How one scope binds a name: by an import, by anything else, or by a global/nonlocal declaration handing it to an outer scope. More...

Public Member Functions
	python_converter (contextt &_context, const nlohmann::json ast, const global_scope &gs, const std::vector< nlohmann::json > extra_asts=nullptr)
	~python_converter ()
void	convert ()
void	set_converting_rhs (bool value)
void	set_current_lhs (exprt *value)
void	set_current_func_name (const std::string &name)
void	set_current_element_type (const typet &type)
symbolt *	add_symbol_and_get_ptr (symbolt &symbol)
exprt	create_lhs_expression (const nlohmann::json &target, symbolt *lhs_symbol, const locationt &location)
const std::string &	get_current_func_name () const
const nlohmann::json &	get_ast_json () const
symbolt *	contract_return_value_symbol (const std::string &var_name, const nlohmann::json &element)
	Symbol for __ESBMC_return_value in an ensures clause, null when the name is something else or the function returns nothing.
exprt	get_expr (const nlohmann::json &element)
exprt	handle_tuple_operations (const std::string &op, exprt &lhs, exprt &rhs, const nlohmann::json &element)
	Handles tuple +/* operators and lexicographic ordering.
std::string	get_op (const std::string &op, const typet &type) const
typet	get_callable_type (const nlohmann::json &annotation, const nlohmann::json &stmt)
	Callable[[A, B], R] as the function-pointer type R (*)(A, B); the generic Callable pointer when the signature is not spelled.
typet	returned_function_type (const nlohmann::json &function_node)
	A bare Callable return as the pointer type of the functions the body returns by name, when they agree on a signature (#7802).
typet	named_return_type (const std::string &name, const nlohmann::json &return_node, const nlohmann::json &function_node)
typet	named_callee_type (const std::string &name)
	The type of the function a call of the name name runs: the function a variable holds, else a nested or module function of that name.
std::optional< code_typet >	returned_function (const nlohmann::json &callee)
	The function a call of callee returns, when its type is known before converting it: get() or get()() where get names a function.
std::optional< exprt >	call_returned_function (const nlohmann::json &element)
	get()(): a call through the function pointer that get() returns.
void	convert_lambda_call (const nlohmann::json &element, side_effect_expr_function_callt &call)
const symbolt *	lambda_copy_for_call (const nlohmann::json &call, const symbolt &var)
	The copy of the once-bound lambda `var` points to, converted for a call passing an int where its one signature has a float (#8941), or null.
bool	call_lambda_copy (const nlohmann::json &element, const symbolt &var, side_effect_expr_function_callt &call, const code_typet *&callee_type)
	Retarget `call` to that copy, if there is one.
std::optional< exprt >	call_property_value (const nlohmann::json &element)
bool	may_be_callable (const typet &type)
	Unknown, function or class-instance types: a call on such a value may succeed.
exprt	not_callable_function (const typet &function, const typet &value, const locationt &location)
	A function with function's type whose only effect is to raise the TypeError CPython raises on calling a value-typed object (#8475).
void	decay_function_choice (exprt &then, exprt &else_expr)
	A choice between two functions of one type is a pointer to either.
typet	get_type_from_annotation (const nlohmann::json &annotation_node, const nlohmann::json &element)
typet	get_optional_type (const nlohmann::json &slice)
	The type of Optional[<slice>], or an empty typet when the slice is not handled.
typet	optional_container_type (const nlohmann::json &slice)
	Optional[C[...]] for a subscripted container C: a list or set is already a pointer, so NULL represents None; a tuple or dict is a struct value with no NULL to spare, so it gets the Optional<T> struct a scalar does (#8017).
string_builder &	get_string_builder ()
python_dict_handler *	get_dict_handler ()
python_exception_handler &	get_exception_handler ()
const python_exception_handler &	get_exception_handler () const
python_math &	get_math_handler ()
complex_handler &	get_complex_handler ()
string_handler &	get_string_handler ()
tuple_handler &	get_tuple_handler () const
const nlohmann::json &	ast () const
contextt &	symbol_table () const
type_handler &	get_type_handler ()
element_type_registry &	get_element_type_registry ()
const element_type_registry &	get_element_type_registry () const
void	mark_list_call_escaped (const std::string &id)
	Record that a list symbol escaped into a function/method call and may have been mutated by the callee; see call_escaped_lists_ (GitHub #5991).
bool	is_list_call_escaped (const std::string &id) const
void	outlive_scope (const std::string &id)
	Makes `id`, a local of a nested body that has been closed, outlive that body, so that a later read does not follow its DEAD (#9185).
void	defer_check (std::function< void()> check)
	Runs `check` once every statement has been converted.
bool	type_assertions_enabled () const
const std::string &	python_file () const
const std::string &	main_python_filename () const
const std::string &	current_function_name () const
const std::string &	current_classname () const
std::string	current_ast_scope () const
	The current function as the AST lookups in json_utils name it: a method is "Cls@C@m", so a same-named method of another class is not found.
const namespacet &	name_space () const
function_call_cache &	get_function_call_cache ()
const function_call_cache &	get_function_call_cache () const
void	add_symbol (const symbolt s)
void	add_instruction (const exprt &expr)
bool	emit_statement_into_current_block (const nlohmann::json &ast_node)
bool	safe_to_emit_side_effecting_statement () const
bool	can_emit_runtime_guard () const
bool	can_emit_catchable_guard () const
void	capture_lambda_free_variables (const nlohmann::json &lambda_node, const std::string &lambda_id, const locationt &location)
	Bind a static cell, named under `lambda_id`, for each scalar free variable of `lambda_node` that is a local of the enclosing function, as create_capture_cells does for a nested def.
exprt	hoist_side_effecting_operand (const exprt &operand, const nlohmann::json &element, const std::string &prefix)
void	guard_attribute_on_none (const exprt &base, const std::string &attr_name, const nlohmann::json &element, bool is_self=false)
	Before an access to base.attr_name through a class pointer that may be None, raises AttributeError when it is, as CPython does.
codet	get_compound_store (const exprt &lhs, const exprt &rhs, const locationt &location)
void	emit_guarded_raise (const exprt &cond, const std::string &exception, const std::string &message, const locationt &location)
exprt	handle_tuple_add (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
	a + b where an operand is a tuple struct.
exprt	concat_tuple_with_list (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
exprt	guard_nonfinite_float_to_int (exprt operand, const nlohmann::json &element, bool reject_none=false)
exprt	guard_none_conversion (exprt operand, const std::string &message, const nlohmann::json &element)
exprt	fit_numpy_integer_store (const exprt &lhs, const exprt &rhs, const nlohmann::json &value)
void	update_symbol (const exprt &expr) const
symbolt *	find_symbol (const std::string &symbol_id) const
bool	is_imported_module (const std::string &module_name) const
nlohmann::json	callable_function_stubs () const
	FunctionDef stubs, each only a name and its returns, for the functions a call in the current module can name: its own and those an import binds, as mk after from helper import mk and helper.mk after import helper.
bool	is_retyped (const irep_idt &id) const
	Whether a straight-line retype moved `id's` value to another symbol.
bool	name_shadows_module (const nlohmann::json &receiver, const nlohmann::json &use) const
	Whether `receiver`, a Name read by the call at `use`, is bound in its scope by something other than an import, so that it is not the module of the same name.
bool	is_module_receiver (const std::string &module_name, const nlohmann::json &receiver, const nlohmann::json &use) const
	Whether `receiver` of the call at `use` is the imported module `module_name` rather than a binding that shadows it.
std::string	current_module_name () const
	Stem of the file being converted, i.e.
const std::string	get_imported_module_path (const std::string &module_name) const
symbolt	create_symbol (const std::string &module, const std::string &name, const std::string &id, const locationt &location, const typet &type) const
void	ensure_void_void_intrinsic (const std::string &name, const locationt &location)
exprt	make_char_array_expr (const std::vector< unsigned char > &string_literal, const typet &t)
exprt	make_class_object (const std::string &name)
	A class used as a value (x = int, type(v)): its name as a char array, also held in value for the folds that read it back.
exprt	class_value (const std::string &name)
	The runtime class value (#8390) of the class name.
exprt	as_class_value (const exprt &e)
	e as a runtime class value when it is one, a class object, or a conditional between such; nil otherwise.
exprt	compare_class_values (const std::string &op, const exprt &lhs, const exprt &rhs)
	is, is not, == or != with a runtime class value on a side; nil when neither side is one.
bool	binds_runtime_class (const nlohmann::json &ast_node, const exprt &rhs)
	Whether assigning rhs to the variable ast_node targets makes that variable a runtime class value: a class on one of several paths.
bool	settle_target_type (symbolt *lhs_symbol, exprt &lhs, exprt &rhs, const nlohmann::json &ast_node)
	Whether the assignment's target type is settled without the usual adjustments: a subscript keeps its own, and a variable that binds_runtime_class takes the class-value type, as does rhs.
ExpressionType	expression_type (const nlohmann::json &element) const
	The category get_expr converts `element` as; CLASS_MRO for Cls.__mro__ on a class whose MRO is known.
exprt	class_mro_tuple (const nlohmann::json &element)
	Cls.__mro__ as a tuple of class objects.
exprt	get_literal (const nlohmann::json &element)
locationt	get_location_from_decl (const nlohmann::json &element) const
void	copy_location_fields_from_decl (const nlohmann::json &from, nlohmann::json &to) const
exprt	handle_string_comparison (const std::string &op, exprt &lhs, exprt &rhs, const nlohmann::json &element)
bool	scalar_order (exprt a, exprt b, const nlohmann::json &element, expr2tc &lt, expr2tc &eq)
	The strict order and equality of two tuple components that are numbers (a mixed int/float pair compares as doubles, as Python promotes int to float) or strs (by content).
size_t	unordered_tuple_component (exprt &lhs, exprt &rhs, const nlohmann::json &element)
	The index of the first component pair, within the common prefix of two tuples, that is neither two numbers, two strs nor two tuples; SIZE_MAX if there is none.
void	raise_on_unordered_tie (const std::string &op, const exprt &lhs, const exprt &rhs, size_t unordered, const expr2tc &prefix_eq, const nlohmann::json &element)
	Raise CPython's TypeError when two tuples tie on every component before the pair at `unordered`, which has no order.
python_typechecking &	get_typechecker ()
const python_typechecking &	get_typechecker () const
bool	enter_contract_clause (bool entering)
	Enters a contract clause or loop invariant, staying entered when already inside one.
void	restore_contract_clause (bool saved)
bool	in_contract_clause () const
size_t	current_block_statement_count () const
const std::string *	class_object_name (const irep_idt &id) const
	The class a variable was last assigned as a value (x = int), or null.

Static Public Member Functions
static scope_bindings	module_scope_bindings (const nlohmann::json &module, const std::string &name)
	The bindings of `name` in `module's` own scope, with declared_outer meaning that a function rebinds it through global.
static std::optional< bool >	binding_is_import (const nlohmann::json &module, const scope_bindings &global, const nlohmann::json *function, bool in_class, bool in_order, const std::string &name, const nlohmann::json &use)
	Whether `name`, read at `use` inside `function` (null at module or class level), reads a binding made by an import (true), another binding (false), or none in this module (empty).
static bool	is_class_object (const exprt &expr)

Friends
class	bounded_math
class	complex_handler
class	function_call_expr
class	numpy_call_expr
class	numpy_random
class	numpy_nditer
class	function_call_builder
class	type_handler
class	python_list
class	string_handler
class	tuple_handler
class	dynamic_type_handler
class	python_typechecking
class	python_class_builder
class	python_dict_handler
class	python_set
class	python_exception_handler
class	get_expr_depth_guard
class	python_converter_test_access

Detailed Description

Main converter for transforming Python AST into ESBMC's intermediate representation.

This class is responsible for converting Python source code (represented as JSON AST) into GOTO programs that can be processed by ESBMC's symbolic execution engine.

Constructor & Destructor Documentation

◆ python_converter()

python_converter::python_converter	(	contextt &	_context,
		const nlohmann::json *	ast,
		const global_scope &	gs,
		const std::vector< nlohmann::json > *	extra_asts = nullptr )

◆ ~python_converter()

python_converter::~python_converter ( )

Member Function Documentation

◆ add_instruction()

void python_converter::add_instruction ( const exprt & expr )

inline

◆ add_symbol()

void python_converter::add_symbol ( const symbolt s )

inline

◆ add_symbol_and_get_ptr()

symbolt * python_converter::add_symbol_and_get_ptr ( symbolt & symbol )

inline

◆ as_class_value()

exprt python_converter::as_class_value ( const exprt & e )

e as a runtime class value when it is one, a class object, or a conditional between such; nil otherwise.

◆ ast()

const nlohmann::json & python_converter::ast ( ) const

inline

◆ binding_is_import()

std::optional< bool > python_converter::binding_is_import	(	const nlohmann::json &	module,
		const scope_bindings &	global,
		const nlohmann::json *	function,
		bool	in_class,
		bool	in_order,
		const std::string &	name,
		const nlohmann::json &	use )

static

Whether name, read at use inside function (null at module or class level), reads a binding made by an import (true), another binding (false), or none in this module (empty).

global is module_scope_bindings for name. With in_order, use runs in source order at module level, and an import must complete before it. Throws when the bindings leave that undecided.

◆ binds_runtime_class()

bool python_converter::binds_runtime_class	(	const nlohmann::json &	ast_node,
		const exprt &	rhs )

Whether assigning rhs to the variable ast_node targets makes that variable a runtime class value: a class on one of several paths.

◆ call_lambda_copy()

bool python_converter::call_lambda_copy	(	const nlohmann::json &	element,
		const symbolt &	var,
		side_effect_expr_function_callt &	call,
		const code_typet *&	callee_type )

Retarget call to that copy, if there is one.

◆ call_property_value()

std::optional< exprt > python_converter::call_property_value ( const nlohmann::json & element )

◆ call_returned_function()

std::optional< exprt > python_converter::call_returned_function ( const nlohmann::json & element )

get()(): a call through the function pointer that get() returns.

(lambda x: ...)(a): a call of the lambda, typed by its arguments.

◆ callable_function_stubs()

nlohmann::json python_converter::callable_function_stubs ( ) const

FunctionDef stubs, each only a name and its returns, for the functions a call in the current module can name: its own and those an import binds, as mk after from helper import mk and helper.mk after import helper.

◆ can_emit_catchable_guard()

bool python_converter::can_emit_catchable_guard ( ) const

inline

◆ can_emit_runtime_guard()

bool python_converter::can_emit_runtime_guard ( ) const

inline

◆ capture_lambda_free_variables()

void python_converter::capture_lambda_free_variables	(	const nlohmann::json &	lambda_node,
		const std::string &	lambda_id,
		const locationt &	location )

Bind a static cell, named under lambda_id, for each scalar free variable of lambda_node that is a local of the enclosing function, as create_capture_cells does for a nested def.

◆ class_mro_tuple()

exprt python_converter::class_mro_tuple ( const nlohmann::json & element )

Cls.__mro__ as a tuple of class objects.

◆ class_object_name()

const std::string * python_converter::class_object_name ( const irep_idt & id ) const

inline

The class a variable was last assigned as a value (x = int), or null.

Kept here rather than read back from the symbol's value, which the IREP2 seam cannot carry in this shape (docs/roadmap/scope-python-irep2.md §14).

◆ class_value()

exprt python_converter::class_value ( const std::string & name )

The runtime class value (#8390) of the class name.

◆ compare_class_values()

exprt python_converter::compare_class_values	(	const std::string &	op,
		const exprt &	lhs,
		const exprt &	rhs )

is, is not, == or != with a runtime class value on a side; nil when neither side is one.

◆ concat_tuple_with_list()

exprt python_converter::concat_tuple_with_list	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

◆ contract_return_value_symbol()

symbolt * python_converter::contract_return_value_symbol	(	const std::string &	var_name,
		const nlohmann::json &	element )

Symbol for __ESBMC_return_value in an ensures clause, null when the name is something else or the function returns nothing.

The symbol __ESBMC_return_value names inside an __ESBMC_ensures clause, or null when the name is something else or the enclosing function returns nothing.

The contracts pass rewrites it to the real return value, so the frontend only has to give it the enclosing function's return type for the clause to type-check.

◆ convert()

void python_converter::convert ( )

◆ convert_lambda_call()

void python_converter::convert_lambda_call	(	const nlohmann::json &	element,
		side_effect_expr_function_callt &	call )

◆ copy_location_fields_from_decl()

void python_converter::copy_location_fields_from_decl	(	const nlohmann::json &	from,
		nlohmann::json &	to ) const

◆ create_lhs_expression()

exprt python_converter::create_lhs_expression	(	const nlohmann::json &	target,
		symbolt *	lhs_symbol,
		const locationt &	location )

◆ create_symbol()

symbolt python_converter::create_symbol	(	const std::string &	module,
		const std::string &	name,
		const std::string &	id,
		const locationt &	location,
		const typet &	type ) const

◆ current_ast_scope()

std::string python_converter::current_ast_scope ( ) const

The current function as the AST lookups in json_utils name it: a method is "Cls@C@m", so a same-named method of another class is not found.

◆ current_block_statement_count()

size_t python_converter::current_block_statement_count ( ) const

inline

◆ current_classname()

const std::string & python_converter::current_classname ( ) const

inline

◆ current_function_name()

const std::string & python_converter::current_function_name ( ) const

inline

◆ current_module_name()

std::string python_converter::current_module_name ( ) const

Stem of the file being converted, i.e.

the module name it would be imported under.

◆ decay_function_choice()

void python_converter::decay_function_choice	(	exprt &	then,
		exprt &	else_expr )

A choice between two functions of one type is a pointer to either.

The result of a choice between types would have no single type (#8404). An arm that cannot be called becomes a function that raises when it is.

◆ defer_check()

void python_converter::defer_check ( std::function< void()> check )

inline

Runs check once every statement has been converted.

◆ emit_guarded_raise()

void python_converter::emit_guarded_raise	(	const exprt &	cond,
		const std::string &	exception,
		const std::string &	message,
		const locationt &	location )

◆ emit_statement_into_current_block()

bool python_converter::emit_statement_into_current_block ( const nlohmann::json & ast_node )

inline

◆ ensure_void_void_intrinsic()

void python_converter::ensure_void_void_intrinsic	(	const std::string &	name,
		const locationt &	location )

◆ enter_contract_clause()

bool python_converter::enter_contract_clause ( bool entering )

inline

Enters a contract clause or loop invariant, staying entered when already inside one.

Returns the previous state for restore_contract_clause.

◆ expression_type()

ExpressionType python_converter::expression_type ( const nlohmann::json & element ) const

The category get_expr converts element as; CLASS_MRO for Cls.__mro__ on a class whose MRO is known.

◆ find_symbol()

symbolt * python_converter::find_symbol ( const std::string & symbol_id ) const

◆ fit_numpy_integer_store()

exprt python_converter::fit_numpy_integer_store	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	value )

◆ get_ast_json()

const nlohmann::json & python_converter::get_ast_json ( ) const

inline

◆ get_callable_type()

typet python_converter::get_callable_type	(	const nlohmann::json &	annotation,
		const nlohmann::json &	stmt )

Callable[[A, B], R] as the function-pointer type R (*)(A, B); the generic Callable pointer when the signature is not spelled.

Callable[[A, B], R] as R (*)(A, B), which parses as Subscript(slice=Tuple([List([A, B]), R])).

Carrying the signature lets a call through the value recover the return type; a bare Callable, or one whose signature is not spelled, keeps the generic function pointer, whose empty return type leaves every call through it nondet.

◆ get_complex_handler()

complex_handler & python_converter::get_complex_handler ( )

inline

◆ get_compound_store()

codet python_converter::get_compound_store	(	const exprt &	lhs,
		const exprt &	rhs,
		const locationt &	location )

◆ get_current_func_name()

const std::string & python_converter::get_current_func_name ( ) const

inline

◆ get_dict_handler()

python_dict_handler * python_converter::get_dict_handler ( )

inline

◆ get_element_type_registry() [1/2]

element_type_registry & python_converter::get_element_type_registry ( )

inline

◆ get_element_type_registry() [2/2]

const element_type_registry & python_converter::get_element_type_registry ( ) const

inline

◆ get_exception_handler() [1/2]

python_exception_handler & python_converter::get_exception_handler ( )

inline

◆ get_exception_handler() [2/2]

const python_exception_handler & python_converter::get_exception_handler ( ) const

inline

◆ get_expr()

exprt python_converter::get_expr ( const nlohmann::json & element )

◆ get_function_call_cache() [1/2]

function_call_cache & python_converter::get_function_call_cache ( )

inline

◆ get_function_call_cache() [2/2]

const function_call_cache & python_converter::get_function_call_cache ( ) const

inline

◆ get_imported_module_path()

const std::string python_converter::get_imported_module_path ( const std::string & module_name ) const

inline

◆ get_literal()

exprt python_converter::get_literal ( const nlohmann::json & element )

◆ get_location_from_decl()

locationt python_converter::get_location_from_decl ( const nlohmann::json & element ) const

◆ get_math_handler()

python_math & python_converter::get_math_handler ( )

inline

◆ get_op()

std::string python_converter::get_op	(	const std::string &	op,
		const typet &	type ) const

◆ get_optional_type()

typet python_converter::get_optional_type ( const nlohmann::json & slice )

The type of Optional[<slice>], or an empty typet when the slice is not handled.

◆ get_string_builder()

string_builder & python_converter::get_string_builder ( )

◆ get_string_handler()

string_handler & python_converter::get_string_handler ( )

inline

◆ get_tuple_handler()

tuple_handler & python_converter::get_tuple_handler ( ) const

inline

◆ get_type_from_annotation()

typet python_converter::get_type_from_annotation	(	const nlohmann::json &	annotation_node,
		const nlohmann::json &	element )

◆ get_type_handler()

type_handler & python_converter::get_type_handler ( )

inline

◆ get_typechecker() [1/2]

python_typechecking & python_converter::get_typechecker ( )

◆ get_typechecker() [2/2]

const python_typechecking & python_converter::get_typechecker ( ) const

◆ guard_attribute_on_none()

void python_converter::guard_attribute_on_none	(	const exprt &	base,
		const std::string &	attr_name,
		const nlohmann::json &	element,
		bool	is_self = false )

Before an access to base.attr_name through a class pointer that may be None, raises AttributeError when it is, as CPython does.

Planted only where the read runs exactly when the statement does, so never in an and/or tail or a while test, whose reads are left as before. self is never None, so is_self skips the guard.

◆ guard_none_conversion()

exprt python_converter::guard_none_conversion	(	exprt	operand,
		const std::string &	message,
		const nlohmann::json &	element )

◆ guard_nonfinite_float_to_int()

exprt python_converter::guard_nonfinite_float_to_int	(	exprt	operand,
		const nlohmann::json &	element,
		bool	reject_none = false )

◆ handle_string_comparison()

exprt python_converter::handle_string_comparison	(	const std::string &	op,
		exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	element )

◆ handle_tuple_add()

exprt python_converter::handle_tuple_add	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

a + b where an operand is a tuple struct.

Nil when neither is one, or the other operand's type is not one Python is known to reject or concatenate.

◆ handle_tuple_operations()

exprt python_converter::handle_tuple_operations	(	const std::string &	op,
		exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	element )

Handles tuple +/* operators and lexicographic ordering.

Concatenation builds a new tuple struct; repetition with a constant int builds an n-fold repeat; Lt/LtE/Gt/GtE lower to element-wise lexicographic comparisons. Returns nil_exprt for non-tuple operands or unsupported variants. Public so the sorted()/reversed() lowering can reuse the comparator for a convert-time sorting network over tuples.

◆ hoist_side_effecting_operand()

exprt python_converter::hoist_side_effecting_operand	(	const exprt &	operand,
		const nlohmann::json &	element,
		const std::string &	prefix )

◆ in_contract_clause()

bool python_converter::in_contract_clause ( ) const

inline

◆ is_class_object()

bool python_converter::is_class_object ( const exprt & expr )

inlinestatic

◆ is_imported_module()

bool python_converter::is_imported_module ( const std::string & module_name ) const

◆ is_list_call_escaped()

bool python_converter::is_list_call_escaped ( const std::string & id ) const

inline

◆ is_module_receiver()

bool python_converter::is_module_receiver	(	const std::string &	module_name,
		const nlohmann::json &	receiver,
		const nlohmann::json &	use ) const

Whether receiver of the call at use is the imported module module_name rather than a binding that shadows it.

◆ is_retyped()

bool python_converter::is_retyped ( const irep_idt & id ) const

inline

Whether a straight-line retype moved id's value to another symbol.

◆ lambda_copy_for_call()

const symbolt * python_converter::lambda_copy_for_call	(	const nlohmann::json &	call,
		const symbolt &	var )

The copy of the once-bound lambda var points to, converted for a call passing an int where its one signature has a float (#8941), or null.

◆ main_python_filename()

const std::string & python_converter::main_python_filename ( ) const

inline

◆ make_char_array_expr()

exprt python_converter::make_char_array_expr	(	const std::vector< unsigned char > &	string_literal,
		const typet &	t )

◆ make_class_object()

exprt python_converter::make_class_object ( const std::string & name )

A class used as a value (x = int, type(v)): its name as a char array, also held in value for the folds that read it back.

◆ mark_list_call_escaped()

void python_converter::mark_list_call_escaped ( const std::string & id )

inline

Record that a list symbol escaped into a function/method call and may have been mutated by the callee; see call_escaped_lists_ (GitHub #5991).

◆ may_be_callable()

bool python_converter::may_be_callable ( const typet & type )

Unknown, function or class-instance types: a call on such a value may succeed.

◆ module_scope_bindings()

python_converter::scope_bindings python_converter::module_scope_bindings	(	const nlohmann::json &	module,
		const std::string &	name )

static

The bindings of name in module's own scope, with declared_outer meaning that a function rebinds it through global.

◆ name_shadows_module()

bool python_converter::name_shadows_module	(	const nlohmann::json &	receiver,
		const nlohmann::json &	use ) const

Whether receiver, a Name read by the call at use, is bound in its scope by something other than an import, so that it is not the module of the same name.

Throws when the bindings leave that undecided.

◆ name_space()

const namespacet & python_converter::name_space ( ) const

inline

◆ named_callee_type()

typet python_converter::named_callee_type ( const std::string & name )

The type of the function a call of the name name runs: the function a variable holds, else a nested or module function of that name.

◆ named_return_type()

typet python_converter::named_return_type	(	const std::string &	name,
		const nlohmann::json &	return_node,
		const nlohmann::json &	function_node )

◆ not_callable_function()

exprt python_converter::not_callable_function	(	const typet &	function,
		const typet &	value,
		const locationt &	location )

A function with function's type whose only effect is to raise the TypeError CPython raises on calling a value-typed object (#8475).

◆ optional_container_type()

typet python_converter::optional_container_type ( const nlohmann::json & slice )

Optional[C[...]] for a subscripted container C: a list or set is already a pointer, so NULL represents None; a tuple or dict is a struct value with no NULL to spare, so it gets the Optional<T> struct a scalar does (#8017).

Empty for any other C.

◆ outlive_scope()

void python_converter::outlive_scope ( const std::string & id )

Makes id, a local of a nested body that has been closed, outlive that body, so that a later read does not follow its DEAD (#9185).

◆ python_file()

const std::string & python_converter::python_file ( ) const

inline

◆ raise_on_unordered_tie()

void python_converter::raise_on_unordered_tie	(	const std::string &	op,
		const exprt &	lhs,
		const exprt &	rhs,
		size_t	unordered,
		const expr2tc &	prefix_eq,
		const nlohmann::json &	element )

Raise CPython's TypeError when two tuples tie on every component before the pair at unordered, which has no order.

◆ restore_contract_clause()

void python_converter::restore_contract_clause ( bool saved )

inline

◆ returned_function()

std::optional< code_typet > python_converter::returned_function ( const nlohmann::json & callee )

The function a call of callee returns, when its type is known before converting it: get() or get()() where get names a function.

◆ returned_function_type()

typet python_converter::returned_function_type ( const nlohmann::json & function_node )

A bare Callable return as the pointer type of the functions the body returns by name, when they agree on a signature (#7802).

◆ safe_to_emit_side_effecting_statement()

bool python_converter::safe_to_emit_side_effecting_statement ( ) const

inline

◆ scalar_order()

bool python_converter::scalar_order	(	exprt	a,
		exprt	b,
		const nlohmann::json &	element,
		expr2tc &	lt,
		expr2tc &	eq )

The strict order and equality of two tuple components that are numbers (a mixed int/float pair compares as doubles, as Python promotes int to float) or strs (by content).

False for any other pair.

◆ set_converting_rhs()

void python_converter::set_converting_rhs ( bool value )

inline

◆ set_current_element_type()

void python_converter::set_current_element_type ( const typet & type )

inline

◆ set_current_func_name()

void python_converter::set_current_func_name ( const std::string & name )

inline

◆ set_current_lhs()

void python_converter::set_current_lhs ( exprt * value )

inline

◆ settle_target_type()

bool python_converter::settle_target_type	(	symbolt *	lhs_symbol,
		exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	ast_node )

Whether the assignment's target type is settled without the usual adjustments: a subscript keeps its own, and a variable that binds_runtime_class takes the class-value type, as does rhs.

◆ symbol_table()

contextt & python_converter::symbol_table ( ) const

inline

◆ type_assertions_enabled()

bool python_converter::type_assertions_enabled ( ) const

◆ unordered_tuple_component()

size_t python_converter::unordered_tuple_component	(	exprt &	lhs,
		exprt &	rhs,
		const nlohmann::json &	element )

The index of the first component pair, within the common prefix of two tuples, that is neither two numbers, two strs nor two tuples; SIZE_MAX if there is none.

When there is one, the operands are hoisted so that the TypeError guard and the comparison read them once.

◆ update_symbol()

void python_converter::update_symbol ( const exprt & expr ) const

◆ bounded_math

friend class bounded_math

friend

◆ complex_handler

friend class complex_handler

friend

◆ dynamic_type_handler

friend class dynamic_type_handler

friend

◆ function_call_builder

friend class function_call_builder

friend

◆ function_call_expr

friend class function_call_expr

friend

◆ get_expr_depth_guard

friend class get_expr_depth_guard

friend

◆ numpy_call_expr

friend class numpy_call_expr

friend

◆ numpy_nditer

friend class numpy_nditer

friend

◆ numpy_random

friend class numpy_random

friend

◆ python_class_builder

friend class python_class_builder

friend

◆ python_converter_test_access

friend class python_converter_test_access

friend

◆ python_dict_handler

friend class python_dict_handler

friend

◆ python_exception_handler

friend class python_exception_handler

friend

◆ python_list

friend class python_list

friend

◆ python_set

friend class python_set

friend

◆ python_typechecking

friend class python_typechecking

friend

◆ string_handler

friend class string_handler

friend

◆ tuple_handler

friend class tuple_handler

friend

◆ type_handler

friend class type_handler

friend

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

src/python-frontend/python_converter.h
src/python-frontend/converter/converter_binop.cpp
src/python-frontend/converter/converter_class.cpp
src/python-frontend/converter/converter_compare.cpp
src/python-frontend/converter/converter_dunder.cpp
src/python-frontend/converter/converter_expr.cpp
src/python-frontend/converter/converter_funcall.cpp
src/python-frontend/converter/converter_funcdef.cpp
src/python-frontend/converter/converter_stmt.cpp
src/python-frontend/converter/converter_symbols.cpp
src/python-frontend/converter/converter_types.cpp
src/python-frontend/converter/converter_unop.cpp
src/python-frontend/converter/converter_util.cpp
src/python-frontend/converter/converter_view_builtins.cpp
src/python-frontend/converter/converter_view_escape.cpp
src/python-frontend/converter/converter_view_hoist.cpp
src/python-frontend/converter/converter_view_rebind.cpp
src/python-frontend/python_converter.cpp

Classes

Public Member Functions

Static Public Member Functions

Friends

Detailed Description

Constructor & Destructor Documentation

◆ python_converter()

◆ ~python_converter()

Member Function Documentation

◆ add_instruction()

◆ add_symbol()

◆ add_symbol_and_get_ptr()

◆ as_class_value()

◆ ast()

◆ binding_is_import()

◆ binds_runtime_class()

◆ call_lambda_copy()

◆ call_property_value()

◆ call_returned_function()

◆ callable_function_stubs()

◆ can_emit_catchable_guard()

◆ can_emit_runtime_guard()

◆ capture_lambda_free_variables()

◆ class_mro_tuple()

◆ class_object_name()

◆ class_value()

◆ compare_class_values()

◆ concat_tuple_with_list()

◆ contract_return_value_symbol()

◆ convert()

◆ convert_lambda_call()

◆ copy_location_fields_from_decl()

◆ create_lhs_expression()

◆ create_symbol()

◆ current_ast_scope()

◆ current_block_statement_count()

◆ current_classname()

◆ current_function_name()

◆ current_module_name()

◆ decay_function_choice()

◆ defer_check()

◆ emit_guarded_raise()

◆ emit_statement_into_current_block()

◆ ensure_void_void_intrinsic()

◆ enter_contract_clause()

◆ expression_type()

◆ find_symbol()

◆ fit_numpy_integer_store()

◆ get_ast_json()

◆ get_callable_type()

◆ get_complex_handler()

◆ get_compound_store()

◆ get_current_func_name()

◆ get_dict_handler()

◆ get_element_type_registry() [1/2]

◆ get_element_type_registry() [2/2]

◆ get_exception_handler() [1/2]

◆ get_exception_handler() [2/2]

◆ get_expr()

◆ get_function_call_cache() [1/2]

◆ get_function_call_cache() [2/2]

◆ get_imported_module_path()

◆ get_literal()

◆ get_location_from_decl()

◆ get_math_handler()

◆ get_op()

◆ get_optional_type()

◆ get_string_builder()

◆ get_string_handler()

◆ get_tuple_handler()

◆ get_type_from_annotation()

◆ get_type_handler()

◆ get_typechecker() [1/2]

◆ get_typechecker() [2/2]

◆ guard_attribute_on_none()

◆ guard_none_conversion()

◆ guard_nonfinite_float_to_int()

◆ handle_string_comparison()

◆ handle_tuple_add()

◆ handle_tuple_operations()