python_dict_handler Class Reference

Handles Python dictionary operations for ESBMC verification. More...

#include <python_dict_handler.h>

Public Member Functions
	python_dict_handler (python_converter &converter, contextt &symbol_table, type_handler &type_handler)
	Constructs a new dictionary handler.
bool	is_dict_literal (const nlohmann::json &element) const
	Checks if a JSON AST node represents a dictionary literal.
exprt	get_dict_literal (const nlohmann::json &element)
	Creates a dictionary literal expression.
exprt	get_dict_comprehension (const nlohmann::json &element)
exprt	build_range_dict_comprehension (const nlohmann::json &element, const nlohmann::json &generator, symbolt &dict_sym)
exprt	create_dict_from_literal (const nlohmann::json &element, const exprt &target_symbol)
	Creates and initializes a dictionary from a literal expression.
void	create_empty_dict (const nlohmann::json &element, const exprt &target_symbol)
	Initialises target_symbol as an empty dict located at element.
exprt	create_dict_with_unpacking (const nlohmann::json &element, const exprt &target_symbol)
	Builds a dict display holding a ** unpack ({**a, "k": v, **b}) by applying its entries in order to an empty dict.
exprt	handle_dict_subscript (const exprt &dict_expr, const nlohmann::json &slice_node, const typet &expected_type=typet(), bool check_type=false)
	Handles dictionary subscript access (e.g., dict['key']).
void	check_value_type (bool enabled, const exprt &obj, const typet &type, const locationt &location)
	When enabled, assert that the PyObject obj holds a value of type.
void	handle_dict_subscript_assign (const exprt &dict_expr, const exprt &key_expr, const exprt &value, const locationt &location, const nlohmann::json &node, codet &target_block)
	Handles dictionary subscript assignment (e.g., dict['key'] = value).
exprt	handle_dict_membership (const exprt &key_expr, const exprt &dict_expr, bool negated)
	Handles dictionary membership testing (in / not in operators).
void	handle_dict_delete (const exprt &dict_expr, const nlohmann::json &slice_node, codet &target_block)
	Handles dictionary key deletion (e.g., del dict['key']).
bool	is_dict_type (const typet &type) const
	Checks if a type represents a Python dictionary.
bool	holds_dict_lists (const typet &type) const
	True when a dict value of type holds a dict's list pointers, which a byte copy into the values list does not preserve: a dict or an Optional<dict> (#9081).
struct_typet	get_dict_struct_type ()
	Gets or creates the dictionary struct type.
void	resolve_dict_subscript_types (const nlohmann::json &left, const nlohmann::json &right, exprt &lhs, exprt &rhs)
	Resolve dictionary subscript types for comparisons.
bool	is_retypable_subscript (const nlohmann::json &node)
	A subscript whose base can be converted again to retype the read.
typet	get_dict_value_type_from_annotation (const nlohmann::json &annotation_node)
	Extract value type from dict type annotation.
typet	get_popitem_tuple_type (const exprt &dict_expr)
	Returns the tuple type (key_type, value_type) for dict.popitem().
exprt	handle_dict_popitem (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.popitem() method calls.
typet	resolve_expected_type_for_dict_subscript (const exprt &dict_expr)
	Resolve expected type for dict subscript using variable annotation.
exprt	read_struct_value (const exprt &obj_value, const typet &type)
	Read a struct value of type type from a dict item's value pointer obj_value.
typet	literal_value_type (const exprt &target)
	The Optional<T> value type a literal assigned to target stores, from the target's annotation or, for an argument, the parameter's (#8016).
typet	recorded_tuple_value_type (const exprt &dict_expr) const
	Stored tuple struct type of a literal dict's values, recorded at construction; empty unless every value has the same tuple type.
bool	reads_value_as_tagged (const exprt &dict_expr, const nlohmann::json &slice_node, const element_type_registry::entries &entries)
	Whether a read of dict_expr yields the stored item as a tagged scalar.
char	annotated_value_kind (const exprt &dict_expr)
	's' or 'n' when dict_expr is written dict[K, V] with a str or number V, else '\0'.
typet	uniform_list_dict_value_type (const std::string &list_id) const
	The scalar or str value type shared by every dict literal recorded as an element of list list_id; empty when an element is not one, the types differ, or the type is an aggregate.
bool	handle_subscript_assignment_check (python_converter &converter, const nlohmann::json &ast_node, const nlohmann::json &target, codet &target_block)
	Check and handle dictionary subscript assignment.
bool	handle_literal_assignment_check (python_converter &converter, const nlohmann::json &ast_node, const exprt &lhs)
	Check and handle dictionary literal assignment.
bool	handle_unannotated_literal_check (python_converter &converter, const nlohmann::json &ast_node, const nlohmann::json &target, const symbol_id &sid)
	Check and handle unannotated dictionary literal.
exprt	handle_dict_get (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.get() method calls.
exprt	handle_dict_setdefault (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.setdefault() method calls.
exprt	handle_dict_pop (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.pop() method calls.
std::string	materialize_tuple_key (exprt &key_expr, const nlohmann::json &element)
	Gives a tuple key an identity so value-reading folds can resolve it.
exprt	handle_dict_update (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.update() method calls.
exprt	bind_dict_source (const exprt &source, const nlohmann::json &node)
	A call returning a dict is a statement; binds its result so its members can be read.
void	copy_dict_entries (const exprt &dict_expr, const exprt &source, const nlohmann::json &call_node)
	Copies every entry of source into dict_expr, overwriting keys already present (dict.update(other) semantics).
exprt	handle_dict_union (const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
	Builds lhs | rhs (PEP 584) as a new dict holding lhs's entries updated with rhs's.
exprt	handle_dict_copy (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.copy() method calls.
exprt	handle_dict_clear (const exprt &dict_expr, const nlohmann::json &call_node)
	Handles dict.clear() method calls.
exprt	handle_dict_fromkeys (const nlohmann::json &call_node)
	Handles dict.fromkeys() class method calls.
exprt	handle_dict_constructor (const nlohmann::json &call_node)
	Handles dict(iterable) constructor calls.
exprt	compare (const exprt &lhs, const exprt &rhs, const std::string &op)
	Compares two dictionaries for equality or inequality.
std::optional< bool >	try_constant_fold_eq (const nlohmann::json &lhs, const nlohmann::json &rhs) const
	Constant-fold a dict-vs-dict equality when both AST operands are literal int-keyed, int-valued dicts (or their dict.fromkeys([...], v) equivalent).

Static Public Member Functions
static bool	is_value_returning_method (const std::string &method_name)
	Returns true for dict methods that return a value and emit IR.
static const std::string &	get_internal_list_id (const std::string &dict_sym_id, bool keys)
	Return the keys-list or values-list symbol id for dict_sym_id.

Public Attributes
typet	literal_value_type_hint
	The value type a dict literal not bound to an annotated name takes, such as one passed straight to an annotated parameter (#8016).

Detailed Description

Handles Python dictionary operations for ESBMC verification.

This class is responsible for converting Python dictionary operations into equivalent C/GOTO constructs that can be processed by ESBMC's symbolic execution engine.

The handler works in conjunction with python_converter to process dictionary-related AST nodes from the Python frontend.

Key Features:

• Dictionary literal creation
• Subscript access with type-safe value retrieval
• Dictionary mutation (assignment, deletion)
• Membership testing (in / not in)
• Nested dictionary support with proper reference semantics
• Type resolution for dictionary subscripts

Constructor & Destructor Documentation

python_dict_handler()

python_dict_handler::python_dict_handler	(	python_converter &	converter,
		contextt &	symbol_table,
		type_handler &	type_handler )

Constructs a new dictionary handler.

Parameters

converter	Reference to the main Python converter for expression handling.
symbol_table	Reference to the symbol table (context) for symbol management.
type_handler	Reference to the type handler for type operations.

Member Function Documentation

annotated_value_kind()

char python_dict_handler::annotated_value_kind

(

const exprt &

dict_expr

)

's' or 'n' when dict_expr is written dict[K, V] with a str or number V, else '\0'.

The preprocessor's guess from a literal's first value is no annotation.

bind_dict_source()

exprt python_dict_handler::bind_dict_source	(	const exprt &	source,
		const nlohmann::json &	node )

A call returning a dict is a statement; binds its result so its members can be read.

Any other expression is returned as is.

build_range_dict_comprehension()

exprt python_dict_handler::build_range_dict_comprehension	(	const nlohmann::json &	element,
		const nlohmann::json &	generator,
		symbolt &	dict_sym )

check_value_type()

void python_dict_handler::check_value_type	(	bool	enabled,
		const exprt &	obj,
		const typet &	type,
		const locationt &	location )

When enabled, assert that the PyObject obj holds a value of type.

compare()

exprt python_dict_handler::compare	(	const exprt &	lhs,
		const exprt &	rhs,
		const std::string &	op )

Compares two dictionaries for equality or inequality.

Implements Python's dictionary comparison semantics by performing order-independent content comparison:

• Calls __ESBMC_dict_eq which checks if all key-value pairs in lhs exist in rhs with matching values (regardless of insertion order)
• Returns true only if both dictionaries have the same keys and corresponding values are equal

This correctly handles cases such as {"a": 1, "b": 2} == {"b": 2, "a": 1}

Supports both == (Eq) and != (NotEq) operators.

Parameters

lhs	Left-hand side dictionary expression
rhs	Right-hand side dictionary expression
op	Comparison operator ("Eq" or "NotEq")

Returns

Boolean expression representing the comparison result

copy_dict_entries()

void python_dict_handler::copy_dict_entries	(	const exprt &	dict_expr,
		const exprt &	source,
		const nlohmann::json &	call_node )

Copies every entry of source into dict_expr, overwriting keys already present (dict.update(other) semantics).

create_dict_from_literal()

exprt python_dict_handler::create_dict_from_literal	(	const nlohmann::json &	element,
		const exprt &	target_symbol )

Creates and initializes a dictionary from a literal expression.

Generates the GOTO instructions to:

1. Create empty keys and values lists
2. Push all key-value pairs from the literal
   • For nested dicts: stores pointer to dict (reference semantics)
   • For regular values: stores value directly (value semantics)
3. Assign the lists to the target dictionary struct

Nested Dictionary Handling: When a value is a nested dict, the implementation:

• Creates a pointer to the dict struct
• Generates a unique type hash for the specific dict type
• Stores the pointer (8 bytes) instead of copying the struct

Parameters

element	The JSON AST node containing the dictionary literal.
target_symbol	The LHS expression (dictionary variable) to assign to.

Returns

The target symbol expression after initialization.

create_dict_with_unpacking()

exprt python_dict_handler::create_dict_with_unpacking	(	const nlohmann::json &	element,
		const exprt &	target_symbol )

Builds a dict display holding a ** unpack ({**a, "k": v, **b}) by applying its entries in order to an empty dict.

create_empty_dict()

void python_dict_handler::create_empty_dict	(	const nlohmann::json &	element,
		const exprt &	target_symbol )

Initialises target_symbol as an empty dict located at element.

get_dict_comprehension()

exprt python_dict_handler::get_dict_comprehension

(

const nlohmann::json &

element

)

get_dict_literal()

exprt python_dict_handler::get_dict_literal

(

const nlohmann::json &

element

)

Creates a dictionary literal expression.

Returns a symbol expression for a dictionary literal. For nested dictionaries, this creates a temporary variable to ensure the dict exists as a concrete symbol that can be referenced via pointer.

The actual initialization is performed by create_dict_from_literal().

Parameters

element

The JSON AST node containing the dictionary literal.

Returns

A symbol expression representing the initialized dictionary.

Exceptions

std::runtime_error

if the element is not a dictionary literal.

get_dict_struct_type()

struct_typet python_dict_handler::get_dict_struct_type

(

)

Gets or creates the dictionary struct type.

Returns the struct type used to represent Python dictionaries. If the type doesn't exist in the symbol table, it is created and added.

The dict struct contains:

• keys: PyListObject* - list of dictionary keys
• values: PyListObject* - list of dictionary values

Returns

The struct_typet representing Python dictionaries.

get_dict_value_type_from_annotation()

typet python_dict_handler::get_dict_value_type_from_annotation

(

const nlohmann::json &

annotation_node

)

Extract value type from dict type annotation.

For annotations like dict[K, V], extracts the value type V.

Parameters

annotation_node

The annotation AST node (Subscript with slice)

Returns

The value type, or empty_typet if cannot be determined

get_internal_list_id()

const std::string & python_dict_handler::get_internal_list_id ( const std::string & dict_sym_id, bool keys )

inlinestatic

Return the keys-list or values-list symbol id for dict_sym_id.

Returns an empty string when the dict was not created via a literal (e.g. it is a function parameter).

get_popitem_tuple_type()

typet python_dict_handler::get_popitem_tuple_type

(

const exprt &

dict_expr

)

Returns the tuple type (key_type, value_type) for dict.popitem().

Parameters

dict_expr

The dictionary expression (must be a symbol)

Returns

struct_typet with element_0=key_type, element_1=value_type

handle_dict_clear()

exprt python_dict_handler::handle_dict_clear	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.clear() method calls.

Empties the dictionary in place by clearing both backing lists (keys and values). Returns nil; dict.clear() has no return value in Python.

Parameters

dict_expr	The dictionary expression to clear
call_node	The function call AST node

Returns

nil_exprt (the method returns None).

handle_dict_constructor()

exprt python_dict_handler::handle_dict_constructor

(

const nlohmann::json &

call_node

)

Handles dict(iterable) constructor calls.

Synthesises a Dict literal from the iterable and routes through get_dict_literal. Supported iterable forms:

• list/tuple/set of 2-tuples: dict([(k1,v1), (k2,v2), ...])
• list of 2-char strings: dict(["ab", "cd"])
• set wrapping any of the above: dict(set([(k,v),...]))

Returns nil_exprt for unsupported forms. The caller falls back to generic call dispatch, which may produce broken GOTO for iterables this handler does not recognise — extend the matcher in the .cpp implementation rather than relying on the fallback for new forms.

Parameters

call_node

The function call AST node (Call(Name("dict"), [arg])).

Returns

Expression for the resulting dict symbol, or nil_exprt.

handle_dict_copy()

exprt python_dict_handler::handle_dict_copy	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.copy() method calls.

Returns a shallow copy of the dictionary: a new dict whose keys and values lists are independent copies of the source's, so mutating the copy does not affect the original.

Parameters

dict_expr	The source dictionary expression
call_node	The function call AST node

Returns

Expression representing the copied dict.

handle_dict_delete()

void python_dict_handler::handle_dict_delete	(	const exprt &	dict_expr,
		const nlohmann::json &	slice_node,
		codet &	target_block )

Handles dictionary key deletion (e.g., del dict['key']).

Generates GOTO instructions to:

• Check if key exists (membership test)
• If exists: find index and remove from both keys and values lists
• If not exists: raise KeyError exception

This provides proper Python semantics where deleting a non-existent key raises an error.

Parameters

dict_expr	The expression representing the dictionary.
slice_node	The JSON AST node for the key to delete.
target_block	The code block to append generated instructions to.

handle_dict_fromkeys()

exprt python_dict_handler::handle_dict_fromkeys

(

const nlohmann::json &

call_node

)

Handles dict.fromkeys() class method calls.

Implements dict.fromkeys(iterable, value=None):

• Creates a new dict whose keys come from iterable and whose values all share the same given value (None by default).
• Only supports iterable passed as a list literal (e.g. dict.fromkeys([1, 2, 3])).

Parameters

call_node

The function call AST node.

Returns

Expression for the resulting dict symbol.

handle_dict_get()

exprt python_dict_handler::handle_dict_get	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.get() method calls.

Implements Python's dict.get(key, default=None) semantics:

• Returns value if key exists
• Returns default (or None) if key doesn't exist

Parameters

dict_expr	The dictionary expression
call_node	The function call AST node containing arguments

Returns

Expression representing the result (value or default)

handle_dict_membership()

exprt python_dict_handler::handle_dict_membership	(	const exprt &	key_expr,
		const exprt &	dict_expr,
		bool	negated )

Handles dictionary membership testing (in / not in operators).

Checks whether a key exists in the dictionary's keys list.

Parameters

key_expr	The expression representing the key to search for.
dict_expr	The expression representing the dictionary.
negated	If true, implements not in; if false, implements in.

Returns

A boolean expression representing the membership test result.

// Python: 'key' in my_dict
// Python: 'key' not in my_dict

handle_dict_pop()

exprt python_dict_handler::handle_dict_pop	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.pop() method calls.

Implements Python's dict.pop(key[, default]) semantics:

• If key exists: removes it and returns its value.
• If key doesn't exist and default is given: returns default.
• If key doesn't exist and no default: raises KeyError.

Parameters

dict_expr	The dictionary expression
call_node	The function call AST node containing arguments

Returns

Expression representing the removed value (or default)

handle_dict_popitem()

exprt python_dict_handler::handle_dict_popitem	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.popitem() method calls.

Implements Python's dict.popitem() semantics:

• Raises KeyError if the dictionary is empty.
• Otherwise removes and returns the last (key, value) pair as a tuple.

  Parameters

  dict_expr	The dictionary expression
  call_node	The function call AST node

  Returns

  Expression representing the (key, value) tuple

handle_dict_setdefault()

exprt python_dict_handler::handle_dict_setdefault	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.setdefault() method calls.

Implements Python's dict.setdefault(key, default=None) semantics:

• If key exists in the dictionary: returns its current value (no mutation)
• If key does not exist: inserts (key, default) into the dictionary and returns default

Parameters

dict_expr	The dictionary expression
call_node	The function call AST node containing arguments

Returns

Expression representing the result (existing value or default)

handle_dict_subscript()

exprt python_dict_handler::handle_dict_subscript	(	const exprt &	dict_expr,
		const nlohmann::json &	slice_node,
		const typet &	expected_type = typet(),
		bool	check_type = false )

Handles dictionary subscript access (e.g., dict['key']).

Generates GOTO instructions to:

1. Find the index of the key in the keys list
2. Retrieve the value at that index from the values list
3. Extract and cast the value based on the expected type

Type-Safe Retrieval:

• For nested dicts: reconstructs dict reference from stored pointer
• For primitive types: casts void* to appropriate type
• Uses expected_type to ensure correct casting

Parameters

dict_expr	The expression representing the dictionary.
slice_node	The JSON AST node for the subscript key.
expected_type	The expected type of the value (used for proper type casting). If not specified, defaults to string (char*). Supported types: signedbv, unsignedbv, bool, floatbv, string, list, and nested dict types.

Returns

An expression representing the accessed value, properly typed.

Note

When comparing dictionary values with primitive types (int, bool, float), the caller should pass the comparison operand's type as expected_type to ensure proper value extraction.

For nested dicts, the expected_type must be the complete dict type. This enables type-safe retrieval with proper hash validation.

Parameters

check_type

Assert that the stored value has expected_type, for an expected_type inferred from records a later store may not update.

handle_dict_subscript_assign()

void python_dict_handler::handle_dict_subscript_assign	(	const exprt &	dict_expr,
		const exprt &	key_expr,
		const exprt &	value,
		const locationt &	location,
		const nlohmann::json &	node,
		codet &	target_block )

Handles dictionary subscript assignment (e.g., dict['key'] = value).

Generates GOTO instructions to update or insert a key-value pair:

• If key exists: updates the existing value at that index
• If key doesn't exist: appends new key-value pair

This provides proper Python dictionary semantics where assignment either updates or creates entries.

Parameters

dict_expr	The expression representing the dictionary.
slice_node	The JSON AST node for the subscript key.
value	The expression representing the value to assign.
target_block	The code block to append generated instructions to.

handle_dict_union()

exprt python_dict_handler::handle_dict_union	(	const exprt &	lhs,
		const exprt &	rhs,
		const nlohmann::json &	element )

Builds lhs | rhs (PEP 584) as a new dict holding lhs's entries updated with rhs's.

handle_dict_update()

exprt python_dict_handler::handle_dict_update	(	const exprt &	dict_expr,
		const nlohmann::json &	call_node )

Handles dict.update() method calls.

Implements Python's dict.update(other) semantics:

• For each key-value pair in other: if key exists, update value; otherwise insert the new key-value pair.
• Returns nil_exprt (update() is a void operation).

  Parameters

  dict_expr	The dictionary expression to update
  call_node	The function call AST node containing the argument dict

  Returns

  nil_exprt (void operation)

handle_literal_assignment_check()

bool python_dict_handler::handle_literal_assignment_check	(	python_converter &	converter,
		const nlohmann::json &	ast_node,
		const exprt &	lhs )

Check and handle dictionary literal assignment.

Parameters

converter	Reference to python_converter
ast_node	Assignment AST node
lhs	Left-hand side expression

Returns

true if handled, false otherwise

handle_subscript_assignment_check()

bool python_dict_handler::handle_subscript_assignment_check	(	python_converter &	converter,
		const nlohmann::json &	ast_node,
		const nlohmann::json &	target,
		codet &	target_block )

Check and handle dictionary subscript assignment.

Checks if the target is a dictionary subscript and handles the assignment

Parameters

converter	Reference to python_converter
ast_node	Assignment AST node
target	Target subscript node
target_block	Code block to append instructions

Returns

true if handled, false otherwise

handle_unannotated_literal_check()

bool python_dict_handler::handle_unannotated_literal_check	(	python_converter &	converter,
		const nlohmann::json &	ast_node,
		const nlohmann::json &	target,
		const symbol_id &	sid )

Check and handle unannotated dictionary literal.

Parameters

converter	Reference to python_converter
ast_node	Assignment AST node
target	Target node
sid	Symbol identifier

Returns

true if handled, false otherwise

holds_dict_lists()

bool python_dict_handler::holds_dict_lists

(

const typet &

type

)

const

True when a dict value of type holds a dict's list pointers, which a byte copy into the values list does not preserve: a dict or an Optional<dict> (#9081).

is_dict_literal()

bool python_dict_handler::is_dict_literal

(

const nlohmann::json &

element

)

const

Checks if a JSON AST node represents a dictionary literal.

Determines whether the given AST element is a Python dictionary literal (e.g., {'key': 'value'}).

Parameters

element

The JSON AST node to check.

Returns

true if the element is a dictionary literal, false otherwise.

is_dict_type()

bool python_dict_handler::is_dict_type

(

const typet &

type

)

const

Checks if a type represents a Python dictionary.

Parameters

type	The type to check.

Returns

true if the type is the dictionary struct type, false otherwise.

is_retypable_subscript()

bool python_dict_handler::is_retypable_subscript

(

const nlohmann::json &

node

)

A subscript whose base can be converted again to retype the read.

A call to a module-level function was typed by its first conversion, and converting it again would call it twice.

is_value_returning_method()

bool python_dict_handler::is_value_returning_method ( const std::string & method_name )

static

Returns true for dict methods that return a value and emit IR.

Used to avoid double-evaluation during type inference: these methods must not be called via get_expr() in create_symbol_for_unannotated_assign(), because they already emit GOTO instructions as a side-effect.

Keep in sync with handle_dict_method() when adding new value-returning dict methods.

Parameters

method_name

The method name to check.

Returns

true if the method is a value-returning, IR-emitting dict method.

literal_value_type()

typet python_dict_handler::literal_value_type

(

const exprt &

target

)

The Optional<T> value type a literal assigned to target stores, from the target's annotation or, for an argument, the parameter's (#8016).

materialize_tuple_key()

std::string python_dict_handler::materialize_tuple_key	(	exprt &	key_expr,
		const nlohmann::json &	element )

Gives a tuple key an identity so value-reading folds can resolve it.

Gives a tuple key an identity of its own, as a list literal already does for its elements.

Folds that read an element's value (sorted() over tuple keys) resolve it through the recorded element id; without one they decline and fall back to a path that retypes tuple elements as int. Returns the id to record, empty when the key has none.

read_struct_value()

exprt python_dict_handler::read_struct_value	(	const exprt &	obj_value,
		const typet &	type )

Read a struct value of type type from a dict item's value pointer obj_value.

A class instance is stored by reference, as a list stores it (#7685); any other struct is stored by value.

Returns

The value, or nil when type is not a struct

reads_value_as_tagged()

bool python_dict_handler::reads_value_as_tagged	(	const exprt &	dict_expr,
		const nlohmann::json &	slice_node,
		const element_type_registry::entries &	entries )

Whether a read of dict_expr yields the stored item as a tagged scalar.

Whether a read of dict_expr at slice_node, whose recorded values are entries, yields the stored item as a tagged scalar: every value is tagged, or the read's constant key was written a string where the written dict[K, V] annotation has a number V, or the reverse.

The latter is read like an element of a list mixing strings and numbers (#4797): its type_id, not V, then answers isinstance. A key not known statically, at the read or the write, leaves the read typed V.

recorded_tuple_value_type()

typet python_dict_handler::recorded_tuple_value_type

(

const exprt &

dict_expr

)

const

Stored tuple struct type of a literal dict's values, recorded at construction; empty unless every value has the same tuple type.

Homogeneous tuple values: the struct type recorded at construction (tagged and string-padded), which neither an annotation nor an AST literal peek reproduces.

Parameters

dict_expr

The dictionary expression (must be a symbol)

Empty when the dict was not built from a literal or its value types are not a single tuple type.

resolve_dict_subscript_types()

void python_dict_handler::resolve_dict_subscript_types	(	const nlohmann::json &	left,
		const nlohmann::json &	right,
		exprt &	lhs,
		exprt &	rhs )

Resolve dictionary subscript types for comparisons.

When comparing dict[key] with primitives, this method ensures both operands have compatible types by dereferencing dict subscripts.

Handles three cases:

1. LHS is dict subscript, RHS is primitive
2. RHS is dict subscript, LHS is primitive
3. Both are dict subscripts

Parameters

left	Left JSON AST node
right	Right JSON AST node
lhs	Left operand expression (modified in place)
rhs	Right operand expression (modified in place)

resolve_expected_type_for_dict_subscript()

typet python_dict_handler::resolve_expected_type_for_dict_subscript

(

const exprt &

dict_expr

)

Resolve expected type for dict subscript using variable annotation.

Looks up the dict variable's annotation to determine what type the subscript operation should return.

Parameters

dict_expr

The dictionary expression (must be a symbol)

Returns

The expected value type from annotation, or empty_typet

try_constant_fold_eq()

std::optional< bool > python_dict_handler::try_constant_fold_eq	(	const nlohmann::json &	lhs,
		const nlohmann::json &	rhs ) const

Constant-fold a dict-vs-dict equality when both AST operands are literal int-keyed, int-valued dicts (or their dict.fromkeys([...], v) equivalent).

Replaces the otherwise-quadratic __ESBMC_dict_eq runtime model call for the common literal-vs-literal pattern, which is the dominant cost under --incremental-bmc when each k iteration re-symbolises the comparison from scratch.

Returns nullopt when either operand falls outside the recognised literal shape; callers must then fall back to the runtime model. Only int keys and int values are recognised today: string / nested / mixed-type dict literals fall through unchanged.

Parameters

lhs	Left-hand AST node (Compare.left or BinOp.left).
rhs	Right-hand AST node (Compare.comparators[0] or BinOp.right).

Returns

true / false if both sides fold; nullopt otherwise.

uniform_list_dict_value_type()

typet python_dict_handler::uniform_list_dict_value_type

(

const std::string &

list_id

)

const

The scalar or str value type shared by every dict literal recorded as an element of list list_id; empty when an element is not one, the types differ, or the type is an aggregate.

Member Data Documentation

literal_value_type_hint

typet python_dict_handler::literal_value_type_hint

The value type a dict literal not bound to an annotated name takes, such as one passed straight to an annotated parameter (#8016).

---

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

• src/python-frontend/python-dict/python_dict_handler.h
• src/python-frontend/python-dict/dict_access.cpp
• src/python-frontend/python-dict/dict_assignment.cpp
• src/python-frontend/python-dict/dict_compare.cpp
• src/python-frontend/python-dict/dict_construction.cpp
• src/python-frontend/python-dict/dict_core.cpp
• src/python-frontend/python-dict/dict_methods.cpp
• src/python-frontend/python-dict/dict_nested.cpp
• src/python-frontend/python-dict/dict_type_resolution.cpp