expr.cpp File Reference

#include <python-frontend/function_call/expr.h>
#include <python-frontend/math/bounded_math.h>
#include <python-frontend/math/cmath_lowering_policy.h>
#include <python-frontend/math/complex_handler.h>
#include <python-frontend/math/complex_handler_utils.h>
#include <python-frontend/json_utils.h>
#include <python-frontend/lambda/python_lambda.h>
#include <python-frontend/math/math_guard_utils.h>
#include <python-frontend/math/python_int_overflow.h>
#include <python-frontend/math/python_math.h>
#include <python-frontend/numpy/numpy_reducer_shared.h>
#include <util/base/host_rounding_mode.h>
#include <python-frontend/exception/python_exception_handler.h>
#include <python-frontend/python-list/python_list.h>
#include <python-frontend/set/python_set.h>
#include <python-frontend/string/string_builder.h>
#include <python-frontend/symbol_id.h>
#include <python-frontend/tuple/tuple_handler.h>
#include <python-frontend/type/type_handler.h>
#include <python-frontend/type/type_utils.h>
#include <python-frontend/python_expr_builder.h>
#include <util/arith/arith_tools.h>
#include <util/arith/bitvector.h>
#include <util/expr/base_type.h>
#include <util/lang/c_typecast.h>
#include <util/expr/expr_util.h>
#include <util/arith/ieee_float.h>
#include <util/message/message.h>
#include <util/lang/python_types.h>
#include <util/irep/std_expr.h>
#include <util/lang/c_sizeof.h>
#include <util/expr/string_constant.h>
#include <irep2/irep2_utils.h>
#include <util/irep/migrate.h>
#include <algorithm>
#include <cctype>
#include <cmath>
#include <limits>
#include <unordered_map>
#include <boost/algorithm/string/predicate.hpp>
#include <deque>
#include <optional>
#include <python-frontend/consteval/python_consteval.h>
#include <regex>
#include <stdexcept>
#include <unordered_set>

Include dependency graph for expr.cpp:

Functions
bool	is_cpp_throw_expr (const exprt &e)
	True when the expression is a synthesized C++ throw used by the Python frontend to propagate exceptions through value positions.
static std::string	get_classname_from_symbol_id (const std::string &symbol_id)
static bool	class_defines_init (const nlohmann::json &ast, const std::string &class_name)
static std::string	node_name (const nlohmann::json &node)
static bool	is_abstract_method (const nlohmann::json &member)
static bool	has_abcmeta_metaclass (const nlohmann::json &class_node)
static std::string	format_double_for_complex (double d)
static bool	try_extract_complex_parts_from_json (const nlohmann::json &arg, const nlohmann::json &ast, const std::string &current_func, double &real_val, double &imag_val)
static std::string	format_complex_string (double real_val, double imag_val)
static std::string	exact_class_of (const nlohmann::json &arg, const nlohmann::json &ast)
	The class arg evaluates to when the source alone fixes it: a class name, or type() of a constructor call or of a non-str literal (ast2json spells str, bytes and complex constants alike).
static bool	is_builtin_class (const std::string &name, const nlohmann::json &ast)
	Whether name is a builtin class that the module never rebinds.
static bool	is_plain_class (const std::string &name, const nlohmann::json &ast)
	Whether name is a class defined once at the top level of ast whose construction yields an instance of it: no decorator or metaclass on it or its bases, and no new anywhere in the module.
static std::string	class_object_str (const std::string &name, const nlohmann::json &arg, const python_converter &converter)
	What str() of the class object name, converted from arg, gives, or "" when that is not known: a class object holds only the bare name.
static std::string	py_float_hex (double d)
exprt	to_value_expr (const exprt &arg, const namespacet &ns)
	Convert a code_function_callt to a side_effect_expr_function_callt so it can be used as a value expression (e.g., as an operand of if_exprt).
static typet	resolve_astype_target_type (const nlohmann::json &dtype_node)
static std::string	numpy_spelling (const std::string &math_name)
static std::optional< std::string >	math_import_of (const nlohmann::json &ast, const std::string &name)
static bool	is_number_literal (const nlohmann::json &node)
static std::string	math_function_name (const std::string &raw_func_name)
static bool	has_common_subclass (const type_handler &th, const nlohmann::json &ast, const std::string &a, const std::string &b)
static std::optional< long long >	extract_any_all_axis_literal (const nlohmann::json &node)
static const nlohmann::json *	find_any_all_axis_keyword (const nlohmann::json &call)
static void	reject_unfoldable_key (const nlohmann::json &call, const std::string &func_name, bool is_sorted_min_max)
	Reaching the runtime model means the preprocessor could not fold the call, and the model has no key parameter – the key is dropped, which silently reorders the result (sorted([a, a + 1], key=lambda v: -v) then reports a spurious counterexample).
static bool	is_value_only_array (const exprt &arg)
static exprt	array_argument_address (const exprt &arg)
static bool	is_tuple_struct (const typet &type)
static std::string	random_element_suffix (const typet &elem_type)
static bool	tuple_members_are_numeric (const struct_typet::componentst &members, const namespacet &ns, bool &any_float)
static nlohmann::json	forward_function_node (const nlohmann::json &ast, const std::string &name)
	The FunctionDef for a call's callee: a module-level name, or a nested path such as "outer@F@b" for a sibling the enclosing body defines later.
static bool	defines_function (const nlohmann::json &ast, const std::string &name)
static std::optional< std::string >	string_literal (const nlohmann::json &node)
static std::optional< std::string >	constant_byteorder (const nlohmann::json &node, const nlohmann::json &module)
static void	reject_unmodelled_numpy_array_argument (const typet &type)

Function Documentation

array_argument_address()

exprt array_argument_address ( const exprt & arg )

static

class_defines_init()

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

static

class_object_str()

std::string class_object_str ( const std::string & name, const nlohmann::json & arg, const python_converter & converter )

static

What str() of the class object name, converted from arg, gives, or "" when that is not known: a class object holds only the bare name.

constant_byteorder()

std::optional< std::string > constant_byteorder ( const nlohmann::json & node, const nlohmann::json & module )

static

defines_function()

bool defines_function ( const nlohmann::json & ast, const std::string & name )

static

exact_class_of()

std::string exact_class_of ( const nlohmann::json & arg, const nlohmann::json & ast )

static

The class arg evaluates to when the source alone fixes it: a class name, or type() of a constructor call or of a non-str literal (ast2json spells str, bytes and complex constants alike).

"" otherwise, as the class type() derives from a static type may be a base of the runtime class.

extract_any_all_axis_literal()

std::optional< long long > extract_any_all_axis_literal ( const nlohmann::json & node )

static

find_any_all_axis_keyword()

const nlohmann::json * find_any_all_axis_keyword ( const nlohmann::json & call )

static

format_complex_string()

std::string format_complex_string ( double real_val, double imag_val )

static

format_double_for_complex()

std::string format_double_for_complex ( double d )

static

forward_function_node()

nlohmann::json forward_function_node ( const nlohmann::json & ast, const std::string & name )

static

The FunctionDef for a call's callee: a module-level name, or a nested path such as "outer@F@b" for a sibling the enclosing body defines later.

get_classname_from_symbol_id()

std::string get_classname_from_symbol_id ( const std::string & symbol_id )

static

has_abcmeta_metaclass()

bool has_abcmeta_metaclass ( const nlohmann::json & class_node )

static

has_common_subclass()

bool has_common_subclass ( const type_handler & th, const nlohmann::json & ast, const std::string & a, const std::string & b )

static

is_abstract_method()

bool is_abstract_method ( const nlohmann::json & member )

static

is_builtin_class()

bool is_builtin_class ( const std::string & name, const nlohmann::json & ast )

static

Whether name is a builtin class that the module never rebinds.

is_cpp_throw_expr()

bool is_cpp_throw_expr

(

const exprt &

e

)

True when the expression is a synthesized C++ throw used by the Python frontend to propagate exceptions through value positions.

is_number_literal()

bool is_number_literal ( const nlohmann::json & node )

static

is_plain_class()

bool is_plain_class ( const std::string & name, const nlohmann::json & ast )

static

Whether name is a class defined once at the top level of ast whose construction yields an instance of it: no decorator or metaclass on it or its bases, and no new anywhere in the module.

The preprocessor names the classes it hoists or renames with a "__" (Outer__Inner, C__esbmc_shadowed), which CPython would not print.

is_tuple_struct()

bool is_tuple_struct ( const typet & type )

static

is_value_only_array()

bool is_value_only_array ( const exprt & arg )

static

math_function_name()

std::string math_function_name ( const std::string & raw_func_name )

static

math_import_of()

std::optional< std::string > math_import_of ( const nlohmann::json & ast, const std::string & name )

static

node_name()

std::string node_name ( const nlohmann::json & node )

static

numpy_spelling()

std::string numpy_spelling ( const std::string & math_name )

static

py_float_hex()

std::string py_float_hex ( double d )

static

random_element_suffix()

std::string random_element_suffix ( const typet & elem_type )

static

reject_unfoldable_key()

void reject_unfoldable_key ( const nlohmann::json & call, const std::string & func_name, bool is_sorted_min_max )

static

Reaching the runtime model means the preprocessor could not fold the call, and the model has no key parameter – the key is dropped, which silently reorders the result (sorted([a, a + 1], key=lambda v: -v) then reports a spurious counterexample).

Refuse instead of answering wrongly.

reject_unmodelled_numpy_array_argument()

void reject_unmodelled_numpy_array_argument ( const typet & type )

static

resolve_astype_target_type()

typet resolve_astype_target_type ( const nlohmann::json & dtype_node )

static

string_literal()

std::optional< std::string > string_literal ( const nlohmann::json & node )

static

to_value_expr()

exprt to_value_expr	(	const exprt &	arg,
		const namespacet &	ns )

Convert a code_function_callt to a side_effect_expr_function_callt so it can be used as a value expression (e.g., as an operand of if_exprt).

try_extract_complex_parts_from_json()

bool try_extract_complex_parts_from_json ( const nlohmann::json & arg, const nlohmann::json & ast, const std::string & current_func, double & real_val, double & imag_val )

static

tuple_members_are_numeric()

bool tuple_members_are_numeric ( const struct_typet::componentst & members, const namespacet & ns, bool & any_float )

static