python_dict_handler.h File Reference

Handler for Python dictionary operations in ESBMC's Python frontend. More...

#include <python-frontend/symbol_id.h>
#include <python-frontend/type/element_type_registry.h>
#include <util/irep/std_types.h>
#include <util/irep/std_code.h>
#include <util/irep/expr.h>
#include <nlohmann/json.hpp>
#include <optional>
#include <string>
#include <unordered_map>

Include dependency graph for python_dict_handler.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	python_dict_handler
	Handles Python dictionary operations for ESBMC verification. More...

Detailed Description

Handler for Python dictionary operations in ESBMC's Python frontend.

This module provides support for converting Python dictionary constructs into ESBMC's intermediate representation (GOTO programs). It handles dictionary literals, subscript access, assignment, membership testing, and deletion operations.

Dictionary Representation

Python dictionaries are represented as a struct containing two parallel lists: one for keys and one for values. The struct type is defined as:

struct __python_dict__ {
  PyListObject* keys;    // List of dictionary keys
  PyListObject* values;  // List of dictionary values (parallel to keys)
};

Dictionary values are stored as PyObject instances with type information (type_id) that allows runtime type identification for proper value extraction.

Nested Dictionary Support

Nested dictionaries (e.g., dict[int, dict[int, int]]) require special handling because dict structs contain pointer fields. Instead of copying the entire nested dict struct, we store a pointer to the dict.

Memory Model:

Parent Dict:
  values_list -> [ptr1, ptr2, ...]
                  ↓
              [Points to nested dict struct]

Type Safety: Each nested dict type gets a unique hash based on its full type structure, ensuring dict[int, dict[int, int]] has a different hash than dict[str, dict[str, str]]. This prevents type confusion during retrieval.

Supported Value Types

The handler supports dictionaries with values of the following types:

• Strings (char*)
• Integers (signed/unsigned bitvectors)
• Booleans
• Floating-point numbers
• Lists
• Nested dictionaries (with pointer-based storage)

Usage Example

// Python code:
config: dict = {'port': 8080, 'debug': True}
x = config['port']
assert config['debug'] == True
 
// Nested dict example:
nested: dict[int, dict[int, int]] = {1: {3: 4}}
value = nested[1][3]
assert value == 4

See also

python_converter

python_list

type_handler