builder.cpp File Reference

#include <python-frontend/function_call/builder.h>
#include <python-frontend/exception/python_exception_handler.h>
#include <python-frontend/function_call/expr.h>
#include <python-frontend/json_utils.h>
#include <python-frontend/numpy/numpy_call_expr.h>
#include <python-frontend/python-dict/python_dict_handler.h>
#include <python-frontend/python-list/python_list.h>
#include <python-frontend/python_converter.h>
#include <python-frontend/symbol_id.h>
#include <python-frontend/type/type_utils.h>
#include <util/arith/arith_tools.h>
#include <util/lang/c_types.h>
#include <util/lang/python_types.h>
#include <util/message/message.h>
#include <util/irep/std_expr.h>
#include <python-frontend/python_expr_builder.h>
#include <boost/algorithm/string/predicate.hpp>
#include <optional>
#include <set>
#include <unordered_map>

Include dependency graph for builder.cpp:

Functions
static const std::unordered_map< std::string, std::string > &	tagged_scalar_method_class ()
static bool	is_full_slice_node (const nlohmann::json &node)
static typet	normalize_pylist_candidate_type (typet type, const namespacet &ns)
static std::optional< struct_typet >	try_get_pylist_struct_type (const typet &type, const namespacet &ns)
static bool	is_pylist_object_type (const typet &type, const namespacet &ns)
static exprt	list_length (const exprt &list, const struct_typet &list_struct, bool in_contract_clause)
	len(list).
static bool	is_unsized_python_type (const std::string &python_type)
	Python types that define no len.
static bool	needs_bool_intrinsic_symbol (const std::string &name)
static bool	is_unsupported_contract_intrinsic (const std::string &name)
static bool	is_pure_clause_node (const std::string &node_type)
static std::string	describe_clause_node (const std::string &node_type)
	Names the Python construct rather than the AST spelling where they differ.
static bool	is_snapshottable_scalar (const typet &type)
	Scalars the wrapper can snapshot by value.
static bool	is_int_literal (const nlohmann::json &node)
static bool	is_name_subscript (const nlohmann::json &arg, const char *slice_kind)
	True when arg is name[...] whose slice node is of kind slice_kind and whose base is a plain Name; the caller then tests that name's type.
static bool	is_name (const nlohmann::json &node, const std::string &name)
static void	scan_list_uses (const nlohmann::json &node, const std::string &name, list_name_uses &uses)
static void	scan_store_target (const nlohmann::json &target, const std::string &name, list_name_uses &uses)
static std::string	list_param_class (const nlohmann::json &arg)
static bool	scan_name_use (const nlohmann::json &node, const std::string &name, list_name_uses &uses)
	Records a bare use of the list's name: a parameter, or an occurrence no enclosing node accounted for, which lets the list escape.
static bool	scan_tracked_use (const nlohmann::json &node, const std::string &name, list_name_uses &uses)
	Whether the node reads an item of the list, calls a method on it or takes its length: the registry follows the first two and the last reads nothing.
static std::set< std::string >	recorded_element_classes (const python_converter &converter, const std::string &id)
	The classes of the elements recorded for a list, "" standing for an element that is not a class instance.
static std::string	super_start_class (const nlohmann::json &super_call, const std::string &current_class, const nlohmann::json &ast)
static std::string	rebase_method_id (std::string id, const std::string &from, const std::string &to, const std::string &method, bool is_ctor)
static std::string	none_has_no_attribute (const nlohmann::json &call)
static bool	annotation_is_optional (const nlohmann::json &ann)
static bool	is_none_valued (const nlohmann::json &value)
static bool	binds_name (const nlohmann::json &node, const std::string &name)
static bool	may_hold_none (const nlohmann::json &node, const std::string &name)
static std::string	constant_number_type_name (const nlohmann::json &value)
static bool	reuses_c_model (const nlohmann::json &call, const symbol_id &function_id)

Variables
const std::string	kGetObjectSize = "__ESBMC_get_object_size"
const std::string	kStrlen = "strlen"
const std::string	kEsbmcAssume = "__ESBMC_assume"
const std::string	kVerifierAssume = "__VERIFIER_assume"
const std::string	kEsbmcAssert = "__ESBMC_assert"
const std::string	kEsbmcUnreachable = "__ESBMC_unreachable"
const std::string	kLoopInvariant = "__loop_invariant"
const std::string	kEsbmcLoopInvariant = "__ESBMC_loop_invariant"
const std::string	kEsbmcRequires = "__ESBMC_requires"
const std::string	kEsbmcEnsures = "__ESBMC_ensures"
const std::string	kEsbmcAssigns = "__ESBMC_assigns"
const std::string	kEsbmcOld = "__ESBMC_old"
const std::string	kEsbmcOldRaw = "__ESBMC_old_raw"
const std::string	kEsbmcReturnValue = "__ESBMC_return_value"
const std::string	kEsbmcCover = "__ESBMC_cover"
const std::string	kEsbmcAtomicBegin = "__ESBMC_atomic_begin"
const std::string	kEsbmcAtomicEnd = "__ESBMC_atomic_end"
const std::string	kEsbmcSpawnThread = "__ESBMC_spawn_thread"
const std::string	kPytInitTid = "__pyt_init_tid"
const std::string	kPytJoin = "__pyt_join"
const std::string	kPytTerminate = "__pyt_terminate"
const std::string	kPyLockBlockAndCheck = "__ESBMC_pylock_block_and_check"
const std::string	kPyLockReleaseWaiters = "__pyt_lock_release_waiters"

Function Documentation

annotation_is_optional()

bool annotation_is_optional ( const nlohmann::json & ann )

static

binds_name()

bool binds_name ( const nlohmann::json & node, const std::string & name )

static

constant_number_type_name()

std::string constant_number_type_name ( const nlohmann::json & value )

static

describe_clause_node()

std::string describe_clause_node ( const std::string & node_type )

static

Names the Python construct rather than the AST spelling where they differ.

is_full_slice_node()

bool is_full_slice_node ( const nlohmann::json & node )

static

is_int_literal()

bool is_int_literal ( const nlohmann::json & node )

static

is_name()

bool is_name ( const nlohmann::json & node, const std::string & name )

static

is_name_subscript()

bool is_name_subscript ( const nlohmann::json & arg, const char * slice_kind )

static

True when arg is name[...] whose slice node is of kind slice_kind and whose base is a plain Name; the caller then tests that name's type.

is_none_valued()

bool is_none_valued ( const nlohmann::json & value )

static

is_pure_clause_node()

bool is_pure_clause_node ( const std::string & node_type )

static

is_pylist_object_type()

bool is_pylist_object_type ( const typet & type, const namespacet & ns )

static

is_snapshottable_scalar()

bool is_snapshottable_scalar ( const typet & type )

static

Scalars the wrapper can snapshot by value.

Anything else is a pointer into the Python object model, whose extent and aliasing the contract layer has no way to state yet (#6938 P4).

is_unsized_python_type()

bool is_unsized_python_type ( const std::string & python_type )

static

Python types that define no len.

Named rather than tested inline so the len() lowering stays one decision point wide.

is_unsupported_contract_intrinsic()

bool is_unsupported_contract_intrinsic ( const std::string & name )

static

list_length()

exprt list_length ( const exprt & list, const struct_typet & list_struct, bool in_contract_clause )

static

len(list).

A contract clause cannot name the result of a call, so there it reads the size field directly.

list_param_class()

std::string list_param_class ( const nlohmann::json & arg )

static

may_hold_none()

bool may_hold_none ( const nlohmann::json & node, const std::string & name )

static

needs_bool_intrinsic_symbol()

bool needs_bool_intrinsic_symbol ( const std::string & name )

static

none_has_no_attribute()

std::string none_has_no_attribute ( const nlohmann::json & call )

static

normalize_pylist_candidate_type()

typet normalize_pylist_candidate_type ( typet type, const namespacet & ns )

static

rebase_method_id()

std::string rebase_method_id ( std::string id, const std::string & from, const std::string & to, const std::string & method, bool is_ctor )

static

recorded_element_classes()

std::set< std::string > recorded_element_classes ( const python_converter & converter, const std::string & id )

static

The classes of the elements recorded for a list, "" standing for an element that is not a class instance.

reuses_c_model()

bool reuses_c_model ( const nlohmann::json & call, const symbol_id & function_id )

static

scan_list_uses()

void scan_list_uses ( const nlohmann::json & node, const std::string & name, list_name_uses & uses )

static

scan_name_use()

bool scan_name_use ( const nlohmann::json & node, const std::string & name, list_name_uses & uses )

static

Records a bare use of the list's name: a parameter, or an occurrence no enclosing node accounted for, which lets the list escape.

scan_store_target()

void scan_store_target ( const nlohmann::json & target, const std::string & name, list_name_uses & uses )

static

scan_tracked_use()

bool scan_tracked_use ( const nlohmann::json & node, const std::string & name, list_name_uses & uses )

static

Whether the node reads an item of the list, calls a method on it or takes its length: the registry follows the first two and the last reads nothing.

super_start_class()

std::string super_start_class ( const nlohmann::json & super_call, const std::string & current_class, const nlohmann::json & ast )

static

tagged_scalar_method_class()

const std::unordered_map< std::string, std::string > & tagged_scalar_method_class ( )

static

try_get_pylist_struct_type()

std::optional< struct_typet > try_get_pylist_struct_type ( const typet & type, const namespacet & ns )

static

Variable Documentation

kEsbmcAssert

const std::string kEsbmcAssert = "__ESBMC_assert"

kEsbmcAssigns

const std::string kEsbmcAssigns = "__ESBMC_assigns"

kEsbmcAssume

const std::string kEsbmcAssume = "__ESBMC_assume"

kEsbmcAtomicBegin

const std::string kEsbmcAtomicBegin = "__ESBMC_atomic_begin"

kEsbmcAtomicEnd

const std::string kEsbmcAtomicEnd = "__ESBMC_atomic_end"

kEsbmcCover

const std::string kEsbmcCover = "__ESBMC_cover"

kEsbmcEnsures

const std::string kEsbmcEnsures = "__ESBMC_ensures"

kEsbmcLoopInvariant

const std::string kEsbmcLoopInvariant = "__ESBMC_loop_invariant"

kEsbmcOld

const std::string kEsbmcOld = "__ESBMC_old"

kEsbmcOldRaw

const std::string kEsbmcOldRaw = "__ESBMC_old_raw"

kEsbmcRequires

const std::string kEsbmcRequires = "__ESBMC_requires"

kEsbmcReturnValue

const std::string kEsbmcReturnValue = "__ESBMC_return_value"

kEsbmcSpawnThread

const std::string kEsbmcSpawnThread = "__ESBMC_spawn_thread"

kEsbmcUnreachable

const std::string kEsbmcUnreachable = "__ESBMC_unreachable"

kGetObjectSize

const std::string kGetObjectSize = "__ESBMC_get_object_size"

kLoopInvariant

const std::string kLoopInvariant = "__loop_invariant"

kPyLockBlockAndCheck

const std::string kPyLockBlockAndCheck = "__ESBMC_pylock_block_and_check"

kPyLockReleaseWaiters

const std::string kPyLockReleaseWaiters = "__pyt_lock_release_waiters"

kPytInitTid

const std::string kPytInitTid = "__pyt_init_tid"

kPytJoin

const std::string kPytJoin = "__pyt_join"

kPytTerminate

const std::string kPytTerminate = "__pyt_terminate"

kStrlen

const std::string kStrlen = "strlen"

kVerifierAssume

const std::string kVerifierAssume = "__VERIFIER_assume"