converter_expr.cpp File Reference

#include <python-frontend/converter/converter_internal.h>
#include <optional>
#include <limits>
#include <python-frontend/math/convert_float_literal.h>
#include <python-frontend/function_call/expr.h>
#include <python-frontend/json_utils.h>
#include <python-frontend/python_annotation/python_annotation.h>
#include <python-frontend/consteval/python_consteval.h>
#include <python-frontend/python_converter.h>
#include <python-frontend/python-dict/python_dict_handler.h>
#include <python-frontend/exception/python_exception_handler.h>
#include <python-frontend/python_expr_builder.h>
#include <python-frontend/math/python_int_overflow.h>
#include <python-frontend/lambda/python_lambda.h>
#include <python-frontend/python-list/python_list.h>
#include <python-frontend/math/python_math.h>
#include <python-frontend/string/string_builder.h>
#include <python-frontend/string/string_handler.h>
#include <python-frontend/symbol_id.h>
#include <python-frontend/tuple/tuple_handler.h>
#include <python-frontend/dynamic_type/dynamic_type_handler.h>
#include <python-frontend/type/type_handler.h>
#include <python-frontend/type/type_utils.h>
#include <irep2/irep2_utils.h>
#include <util/arith/arith_tools.h>
#include <util/lang/c_types.h>
#include <util/base/encoding.h>
#include <util/expr/expr_util.h>
#include <util/message/message.h>
#include <util/irep/migrate.h>
#include <util/lang/python_types.h>
#include <util/irep/std_code.h>
#include <util/expr/string_constant.h>

Include dependency graph for converter_expr.cpp:

Classes
class	get_expr_depth_guard

Typedefs
using	name_type_test
	Whether a name has a given annotated type where it is read.

Functions
static bool	contains_cpp_throw (const exprt &expr)
static exprt	build_shape_tuple_expr (python_converter &converter, const std::vector< exprt > &dims)
static exprt	build_shape_size_expr (const std::vector< exprt > &dims)
static std::vector< exprt >	build_dim_exprs (const std::vector< int > &dims)
static exprt	build_runtime_list_len_expr (contextt &symbol_table, const exprt &list_expr, const std::string &diagnostic)
static bool	is_python_list_model_type (typet type, const typet &list_type, const namespacet &ns)
static nlohmann::json	normalize_bool_index_node (const nlohmann::json &node)
static void	throw_numpy_multidim_index_error (python_converter &converter, const nlohmann::json &element)
static typet	stored_member_type (const typet &value_type)
static bool	is_full_slice_node (const nlohmann::json &node)
static void	throw_numpy_too_many_indices_error (python_converter &converter, const nlohmann::json &element, std::size_t num_indices)
static ExpressionType	get_expression_type (const nlohmann::json &element)
static double	nonfinite_aware_double (const nlohmann::json &node, const std::string &key, double fallback)
	Convert Python AST literal to expression.
static std::optional< exprt >	get_complex_literal (const nlohmann::json &element, const nlohmann::json &annotated_node)
	The complex constant annotated_node denotes, or empty when it is not one.
static bool	is_attribute_base_expression (const nlohmann::json &node_type)
	Node kinds whose value an attribute access may be applied to directly, as opposed to a plain name.
static std::string	module_binding_name (const nlohmann::json &stmt)
	The name stmt binds, if it is a def or an annotated assignment to a name; otherwise empty.
static const nlohmann::json *	find_module_binding (const nlohmann::json &body, const std::string &name)
	The statement binding name in body or in a block nested in it at module scope (an if, loop or try), or nullptr.
static bool	constant_keeps_type (const nlohmann::json &value, const std::string &type)
	Whether value is a constant that leaves a global of annotated type type that type when added to it.
static bool	keeps_type (const nlohmann::json &aug, const std::string &type, const name_type_test &has_type)
	Whether aug adds to a global of annotated type type a constant, or a name has_type gives that type, that leaves it that type.
static std::size_t	count_type_keeping_aug_assigns (const nlohmann::json &node, const std::string &name, const std::string &type, const name_type_test &has_type)
	The augmented assignments to name under node that keep it type.
static const nlohmann::json *	sole_module_binding (const nlohmann::json &module, const std::string &name, const name_type_test &has_type)
	The module-scope statement binding name when that is the one binding of the name anywhere in the module, or nullptr.
static std::string	undefined_variable_message (const std::string &var_name, const std::string &func_name, const locationt &location)
	The "variable is not defined" diagnostic for a Name that resolved to no symbol, naming the enclosing function when the reference is inside one.
static bool	is_numpy_shape_subscript_node (const nlohmann::json &element)
static std::optional< exprt >	numpy_shape_dim_expr (const std::vector< std::size_t > &shape, const nlohmann::json &slice)
static std::optional< std::vector< std::size_t > >	numpy_subscript_shape (const std::vector< std::size_t > &source_shape, const nlohmann::json &slice_node)
static bool	is_numpy_shape_attribute (const std::string &attr_name)
static bool	is_declared_any (const nlohmann::json &node, const std::string &function, const nlohmann::json &ast)
static bool	mentions_self_attribute (const nlohmann::json &node, const std::string &attr)
static bool	assigns_class_attribute (const nlohmann::json &body, const std::string &attr)
static bool	class_binds_attribute (const nlohmann::json &ast, const std::string &class_name, const std::string &attr)
static exprt	make_slice_struct_expr (python_converter &conv, const nlohmann::json *lower, const nlohmann::json *upper, const nlohmann::json *step, const nlohmann::json &source_node)
static bool	stored_exactly (const nlohmann::json &value, const typet &type)
	Whether value survives the C type type unchanged: a float is exact only for an integral literal, and an int in a double only for a literal of at most 2**53.

Typedef Documentation

name_type_test

using name_type_test

Initial value:

 
  std::function<bool(const std::string &, const std::string &)>

Whether a name has a given annotated type where it is read.

Function Documentation

assigns_class_attribute()

bool assigns_class_attribute ( const nlohmann::json & body, const std::string & attr )

static

build_dim_exprs()

std::vector< exprt > build_dim_exprs ( const std::vector< int > & dims )

static

build_runtime_list_len_expr()

exprt build_runtime_list_len_expr ( contextt & symbol_table, const exprt & list_expr, const std::string & diagnostic )

static

build_shape_size_expr()

exprt build_shape_size_expr ( const std::vector< exprt > & dims )

static

build_shape_tuple_expr()

exprt build_shape_tuple_expr ( python_converter & converter, const std::vector< exprt > & dims )

static

class_binds_attribute()

bool class_binds_attribute ( const nlohmann::json & ast, const std::string & class_name, const std::string & attr )

static

constant_keeps_type()

bool constant_keeps_type ( const nlohmann::json & value, const std::string & type )

static

Whether value is a constant that leaves a global of annotated type type that type when added to it.

contains_cpp_throw()

bool contains_cpp_throw ( const exprt & expr )

static

count_type_keeping_aug_assigns()

std::size_t count_type_keeping_aug_assigns ( const nlohmann::json & node, const std::string & name, const std::string & type, const name_type_test & has_type )

static

The augmented assignments to name under node that keep it type.

find_module_binding()

const nlohmann::json * find_module_binding ( const nlohmann::json & body, const std::string & name )

static

The statement binding name in body or in a block nested in it at module scope (an if, loop or try), or nullptr.

get_complex_literal()

std::optional< exprt > get_complex_literal ( const nlohmann::json & element, const nlohmann::json & annotated_node )

static

The complex constant annotated_node denotes, or empty when it is not one.

element is the outer node, which is a UnaryOp when the literal is signed.

get_expression_type()

ExpressionType get_expression_type ( const nlohmann::json & element )

static

is_attribute_base_expression()

bool is_attribute_base_expression ( const nlohmann::json & node_type )

static

Node kinds whose value an attribute access may be applied to directly, as opposed to a plain name.

Each converts to an object that resolve_member_on_base can look a member up on.

is_declared_any()

bool is_declared_any ( const nlohmann::json & node, const std::string & function, const nlohmann::json & ast )

static

is_full_slice_node()

bool is_full_slice_node ( const nlohmann::json & node )

static

is_numpy_shape_attribute()

bool is_numpy_shape_attribute ( const std::string & attr_name )

static

is_numpy_shape_subscript_node()

bool is_numpy_shape_subscript_node ( const nlohmann::json & element )

static

is_python_list_model_type()

bool is_python_list_model_type ( typet type, const typet & list_type, const namespacet & ns )

static

keeps_type()

bool keeps_type ( const nlohmann::json & aug, const std::string & type, const name_type_test & has_type )

static

Whether aug adds to a global of annotated type type a constant, or a name has_type gives that type, that leaves it that type.

make_slice_struct_expr()

exprt make_slice_struct_expr ( python_converter & conv, const nlohmann::json * lower, const nlohmann::json * upper, const nlohmann::json * step, const nlohmann::json & source_node )

static

mentions_self_attribute()

bool mentions_self_attribute ( const nlohmann::json & node, const std::string & attr )

static

module_binding_name()

std::string module_binding_name ( const nlohmann::json & stmt )

static

The name stmt binds, if it is a def or an annotated assignment to a name; otherwise empty.

nonfinite_aware_double()

double nonfinite_aware_double ( const nlohmann::json & node, const std::string & key, double fallback )

static

Convert Python AST literal to expression.

Handles integers, booleans, floats, chars, strings, and byte literals. Example: {"_type": "Constant", "value": 42} -> integer constant expr The double node carries for key. A non-finite literal has no JSON number form, so the parser nulls it and records the spelling under "<key>_nonfinite" (#7545).

normalize_bool_index_node()

nlohmann::json normalize_bool_index_node ( const nlohmann::json & node )

static

numpy_shape_dim_expr()

std::optional< exprt > numpy_shape_dim_expr ( const std::vector< std::size_t > & shape, const nlohmann::json & slice )

static

numpy_subscript_shape()

std::optional< std::vector< std::size_t > > numpy_subscript_shape ( const std::vector< std::size_t > & source_shape, const nlohmann::json & slice_node )

static

sole_module_binding()

const nlohmann::json * sole_module_binding ( const nlohmann::json & module, const std::string & name, const name_type_test & has_type )

static

The module-scope statement binding name when that is the one binding of the name anywhere in the module, or nullptr.

Any other binding (a second one, a local) leaves the name's value at a read depending on which binding ran. An augmented assignment that keeps the binding's type does not count: it reads the name first, so it raises unless the binding has already run.

stored_exactly()

bool stored_exactly ( const nlohmann::json & value, const typet & type )

static

Whether value survives the C type type unchanged: a float is exact only for an integral literal, and an int in a double only for a literal of at most 2**53.

stored_member_type()

typet stored_member_type ( const typet & value_type )

static

throw_numpy_multidim_index_error()

void throw_numpy_multidim_index_error ( python_converter & converter, const nlohmann::json & element )

static

throw_numpy_too_many_indices_error()

void throw_numpy_too_many_indices_error ( python_converter & converter, const nlohmann::json & element, std::size_t num_indices )

static

undefined_variable_message()

std::string undefined_variable_message ( const std::string & var_name, const std::string & func_name, const locationt & location )

static

The "variable is not defined" diagnostic for a Name that resolved to no symbol, naming the enclosing function when the reference is inside one.