- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| visit_For (self, node) | |
| visit_With (self, node) | |
| visit_Name (self, node) | |
Public Attributes | |
| numpy_module_names | |
| iterator_params | |
| iterator_classes | |
| bool | is_range_loop = True |
| bool | helper_functions_added = True |
| generator_vars | |
| generator_funcs | |
| module_name | |
| target_name = target_name | |
| tuple | current_start_var |
| imported_module_names | |
| shadowed_nondet_collections | |
| old = old | |
| new = new | |
Static Public Attributes | |
| Dict | variable_annotations [str, ast.AST] |
| Dict | known_variable_types [str, str] |
| Dict | class_attr_annotations [str, Dict[str, ast.AST]] |
| Dict | function_return_annotations [str, ast.AST] |
| Dict | instance_class_map [str, str] |
| Dict | het_dict_literals [str, ast.Dict] |
| Dict | het_value_dict_literals [str, ast.Dict] |
| Dict | dict_items_vars [str, ast.AST] |
| Set | dataclasses_module_names [str] |
| visit_AsyncWith = visit_With | |
Protected Member Functions | |
| _pre_annotate_items_loop_vars (self, node) | |
| _pre_annotate_enumerate_loop_vars (self, node) | |
| _is_reversed_range_call (self, iter_node) | |
| _transform_reversed_range (self, reversed_call) | |
| _forget_literals_changed_in_loop (self, loop) | |
| _lower_iterator_protocol_for (self, node) | |
| _is_nditer_call (self, expr) | |
| _nditer_source (self, expr) | |
| _unwrap_nditer_iter (self, expr) | |
| _record_nditer_with_targets (self, node) | |
| _lower_nditer_for (self, node) | |
| _constructs_iterator_class (self, expr) | |
| _lower_for_else (self, node) | |
| _visit_for_inner (self, node) | |
| _can_safely_unroll_list_literal_for (self, node, list_literal) | |
| _unroll_list_literal_for (self, node, list_literal) | |
| _transform_enumerate_for (self, node) | |
| _validate_enumerate_call (self, enumerate_call) | |
| _parse_enumerate_target (self, target) | |
| _reject_unsupported_loop (self, node, message) | |
| _nested_enumerate_source (self, node, arity) | |
| _count_nested_enumerate_for (self, node, target_info) | |
| _tuple_literal_enumerate_source (self, node) | |
| _unroll_enumerate_over_tuples (self, node, target_info, literal, start) | |
| _unroll_nested_enumerate_for (self, node, target_info) | |
| _parse_enumerate_arguments (self, enumerate_call, node) | |
| _validate_start_value (self, start_value) | |
| _create_enumerate_setup_statements (self, node, iterable, start_value, loop_id) | |
| _create_enumerate_while_loop (self, node, target_info, loop_id) | |
| _create_unpacking_loop_body (self, node, target_info, loop_id) | |
| _create_single_var_loop_body (self, node, target_info, loop_id) | |
| _create_increment_statements (self, node, loop_id) | |
| _transform_original_body (self, node) | |
| _transform_range_for (self, node) | |
| _transform_items_for (self, node) | |
| _any_ann (self) | |
| _uses_string_subscript (self, var_name, body) | |
| _key_used_as_subscript (self, var_name, body) | |
| _value_used_in_float_arith (self, var_name, body) | |
| _kv_types_from_annotation (self, annotation) | |
| _is_concrete_tuple_ann (self, ann_node) | |
| _literal_tuple_annotation_node (self, iterable_node) | |
| _full_tuple_annotation_node (self, iterable_node) | |
| _get_base_type_name (self, ann_node) | |
| _get_dict_kv_types (self, dict_var_name) | |
| _get_kv_types_from_call (self, call_node) | |
| _get_kv_types_from_attribute (self, attr_node) | |
| _get_kv_types_from_subscript (self, subscript_node) | |
| _create_dict_list_assign (self, node, var_name, dict_node, method, elem_ann) | |
| _create_var_subscript_assign (self, node, var_name, list_var, index_var, elem_ann) | |
| _emit_items_unpack (self, node, body, target_elt, list_var, index_var, elem_ann) | |
| _create_dict_size_assertion (self, node, keys_var, length_var) | |
| _materialize_for_iter (self, node, seq, loop_id, suffix="") | |
| _make_target_assign (self, node, target, iter_var_name, index_var, element_type) | |
| _make_index_step (self, node, index_var, step) | |
| _transform_reversed_for (self, node) | |
| _transform_filter_for (self, node) | |
| _transform_zip_for (self, node) | |
| _transform_iterable_for (self, node) | |
| _create_iter_assignment (self, node, annotation_id, iter_var_name, element_type, full_element_ann=None) | |
| _create_index_assignment (self, node, index_var="ESBMC_index") | |
| _create_length_assignment (self, node, iter_var_name, length_var="ESBMC_length") | |
| _create_while_condition (self, node, index_var="ESBMC_index", length_var="ESBMC_length") | |
| _create_loop_body (self, node, target_var_name, iter_var_name, index_var, element_type, full_element_ann=None) | |
| _create_index_increment (self, node, index_var="ESBMC_index") | |
| _infer_type_from_value (self, value) | |
| _infer_type_from_constant (self, constant_node) | |
| _infer_type_from_call (self, call_node) | |
| _copy_location_info (self, source_node, target_node) | |
| _next_unpack_tmp_id (self) | |
| _create_individual_assignment (self, target, value, source_node) | |
| _update_variable_types_simple (self, target, value) | |
| _handle_tuple_unpacking (self, target, value, source_node) | |
| _create_annotation_node_from_value (self, value) | |
| _nondet_callee_name (self, node) | |
| _nondet_generator_type (self, node) | |
| _is_user_nondet_generator (self, node) | |
| _is_nondet_generator (self, node) | |
| _nondet_list_builder (self, elem_node, resolve) | |
| _resolve_nondet_type (self, node, allowed, func_name, role) | |
| _parse_nondet_collection_call (self, call) | |
| _rewrite_nondet_collection_call (self, call) | |
| _create_annotation_from_call (self, call_node) | |
| _create_list_annotation (self, list_node) | |
| _create_dict_annotation (self, dict_node) | |
| _has_heterogeneous_keys (self, dict_node) | |
| _has_heterogeneous_values (self, dict_node) | |
| _infer_constant_type (self, node) | |
| _unroll_het_for (self, node, typed_elts) | |
| _transform_het_dict_for (self, node) | |
| _transform_het_values_for (self, node, dict_node) | |
| _infer_dict_key_type (self, key_node) | |
| _infer_dict_value_annotation (self, value_node) | |
| _create_subscript_annotation (self, subscript_node) | |
| _is_defaultdict_call (self, call_node) | |
| _get_defaultdict_factory (self, call_node) | |
| _make_defaultdict_missing_check (self, dict_name, key_node, factory_node, template) | |
| _is_defaultdict_key_initialized (self, dict_name, key_node) | |
| _record_defaultdict_key_initialized (self, dict_name, key_node) | |
| _lower_defaultdict_reads_in_expr (self, expr, template) | |
Static Protected Member Functions | |
| Optional[str] | _name_id_or_none (ast.AST node) |
| bool | _is_nullary_lambda (ast.AST node) |
| _is_enumerate_preannotation_candidate (node) | |
| _is_constant_element (elt) | |
| _static_int_value (expr) | |
| _body_destructures_name (body, name) | |
| _is_zip_call (it) | |
| _is_filter_call (it) | |
| _is_reversed_call (it) | |
| _nondet_builder_call (builder, max_size_node) | |
| _nondet_collection_keywords (call, func_name) | |
| _nondet_builder_annotation (func_name) | |
| _defaultdict_key_signature (key_node) | |
Protected Attributes | |
| int | _for_else_counter = counter + 1 |
| _is_constant_element | |
| int | _unpack_tmp_counter = current + 1 |
Static Protected Attributes | |
| Dict | _defaultdict_factory [str, ast.AST] |
| _SIZABLE_TUPLE_MEMBER_TYPES = frozenset({"int", "float"}) | |
| tuple | _NONDET_LIST_ELEM_TYPES = ("int", "float", "bool", "str") |
| tuple | _NONDET_DICT_KEY_TYPES = ("int", "str", "bool") |
| tuple | _NONDET_DICT_VALUE_TYPES = ("int", "float", "bool", "str") |
| tuple | _NONDET_SCALAR_SUFFIXES = ("int", "float", "bool", "str", "char", "complex") |
| int | _DEFAULT_NONDET_COLLECTION_SIZE = 8 |
Loop/iteration lowering helpers mixed into `Preprocessor`.
|
protected |
Return a fresh ast.Name(id='Any') annotation node.
|
staticprotected |
True if `body` assigns `name` to a tuple/list target (`u, v = name`). Only a direct statement counts: a nested loop or branch may rebind the name first, and this only decides whether to keep the key's concrete type, so a missed case just falls back to the existing handling.
|
protected |
Decide whether a `for` over a tracked list literal is safe to unroll.
Skip the unroll when:
* the loop body contains ``break``/``continue``/``return`` (these
need a surrounding loop/function context);
* elements are constants of heterogeneous types (e.g. mixed ``int``
and ``str``), which would silently drop runtime ``isinstance``
checks during unrolling and constant folding.
|
protected |
Whether `expr` is `Cls(...)`, or a name bound only by `x = Cls(...)` in the scope being visited or a parameter every call passes such a construction, for a class in `iterator_classes`.
|
protected |
Copy all location information from source to target node
|
protected |
Lower `for i, (a, b) in enumerate(xs, s)` to a plain loop with a counter.
ESBMC_enum_count = s
for (a, b) in xs:
i = ESBMC_enum_count
ESBMC_enum_count = ESBMC_enum_count + 1
<body>
|
protected |
Create annotation from a nondet collection call or its builder. Both spellings are handled because the module pre-pass runs before the callee rewrite and the per-assignment pass runs after it.
|
protected |
Create an annotation AST node from a value node for storage
|
protected |
Create dict[K, V] annotation from a dict literal
|
protected |
Create: var_name: list[base(elem_ann)] = dict_node.method()
The list annotation uses only the BASE type name (e.g. 'dict' for
dict[str, int]) so the C++ list subscript handler can call
get_typet("dict") and correctly extract a dict struct from the PyObj.
Full nested type info is preserved via the loop variable's own annotation
(produced by _create_var_subscript_assign).
|
protected |
Create dict-size check to detect mutation during iteration.
|
protected |
Create the initial variable assignments for enumerate transformation.
|
protected |
Create the while loop for enumerate transformation.
|
protected |
Create the increment statements for both indices.
|
protected |
Create ESBMC_index assignment with custom name.
|
protected |
Create index increment statement with custom index variable name.
|
protected |
Create a single assignment node with proper location info
|
protected |
Create assignment for iterator variable with proper type annotation. ``full_element_ann`` carries the concrete tuple[A, B, ...] element annotation when one is known: the C++ list subscript read sizes the tuple from this list annotation, and the bare "tuple" name erases it to void* (#5444).
|
protected |
Create ESBMC_length assignment with custom name.
|
protected |
Create list[T] annotation from a list literal
|
protected |
Create the body of the while loop with proper type annotations. ``full_element_ann``, when given, is the full tuple[A, B, ...] annotation node for the per-index element and takes precedence over the bare ``element_type`` name -- needed so a tuple-unpacking target keeps its concrete member types instead of eroding to bare tuple (#5444).
|
protected |
Create loop body for single variable case: for item in enumerate(...)
|
protected |
Extract annotation from subscript operation (e.g., d["key"])
|
protected |
Create loop body for unpacking case: for i, x in enumerate(...)
|
protected |
Create: var_name: elem_ann = list_var[index_var] Uses the FULL annotation node (e.g. dict[str, int]) so that variable_annotations[var_name] carries nested type information for subsequent inner-loop type resolution.
|
protected |
Create while loop condition with custom variable names.
|
staticprotected |
Return a stable signature for literal keys whose value is known.
|
protected |
Append the assignment that binds the i-th key/value of d.items() to ``target_elt``.
Simple Name target — emits ``name: elem_ann = list_var[index_var]``.
Tuple/List target (nested unpacking, e.g. ``for (u, v), w in d.items():``) —
binds the element to a local tuple temp first, then destructures from that
temp. Unpacking directly from ``list_var[index_var]`` lowers each component
to ``(*(tuple*)elem->value).element_i``, which dereferences to an array
rvalue for string components and aborts ("Can't construct rvalue reference
to array type"). A whole-struct copy into a local makes each component read
a local member access instead, reusing the working ``u, v = t`` path.
|
protected |
Drop the tracked literals that @p loop rebinds or mutates anywhere. A statement late in the body runs before the early ones on the next iteration, so a literal it changes is not known anywhere in the loop (#8506).
|
protected |
Return the full tuple[A, B, ...] element annotation of a list[tuple[...]]-annotated Name iterable, or None if unavailable. `_get_element_type_from_container` collapses a list[tuple[str, str]] element type down to the bare string "tuple" (it only ever returns a base-type name), which is enough for a scalar loop target but loses the tuple's concrete member types for a tuple-unpacking target (`for u, v in <list[tuple[...]]>`). This mirrors that lookup but keeps the full annotation node so the per-index element assignment stays typed as tuple[str, str] instead of eroding to bare tuple, whose element_0/element_1 members the C++ converter cannot size (#5444).
|
protected |
Return the base type name string from an annotation node.
For simple names (int, str, dict) returns the id.
For subscripts (dict[str, int]) returns the outer name ('dict').
|
protected |
Return the factory node for a collections.defaultdict call, or None.
Returns None when:
- call_node is not a defaultdict call (_is_defaultdict_call is False)
- defaultdict() called with no args (no auto-insertion)
- defaultdict(None) called with explicit None (no auto-insertion)
Callers that need to distinguish "not a defaultdict" from "defaultdict
without a factory" should call _is_defaultdict_call() separately and
always rewrite the construction to {}, only recording a factory when
this method returns non-None.
|
protected |
Return (key_ann, val_ann) annotation nodes from a variable's dict[K, V] annotation.
|
protected |
Return (key_ann, val_ann) annotation nodes from c.d via class attribute lookup.
|
protected |
Return (key_ann, val_ann) annotation nodes from a function call's return annotation.
|
protected |
Return (key_ann, val_ann) for a subscript dict expression. For d["key"].items() where d: dict[str, dict[K, V]], returns (K, V). Uses _create_subscript_annotation to find the value type of d at the subscript key, then extracts the K/V types from that inner dict type.
|
protected |
Handle tuple unpacking assignments like x, y = 1, 2 or a, b = [1, 2] Convert them into individual assignments with proper type inference
|
protected |
Return True if a dict literal needs per-key loop unrolling at iteration.
Triggers on two cases:
* Mixed key types (e.g. ``{"a": 1, 2: "b"}``) — ESBMC stores keys in a
flat list with a type-specific byte size, so a single retrieval
stride cannot read both an ``int`` (8 bytes) and a ``str`` (variable
width) without tripping an array-bounds violation.
* Any tuple key (e.g. ``{(1, 2): 10}``) — the key is a struct rather
than a scalar, so when ``for k in d:`` is lowered to indexing the
synthesised keys list, the loop variable's runtime value is a
generic pointer. Downstream destructuring (``u, v = k``) then fails
in ``converter_stmt.cpp`` with "Cannot unpack pointer". Unrolling
inlines each tuple literal directly so the converter sees a struct.
|
protected |
Return True if a dict literal has values of more than one ESBMC type. Even when both types occupy the same number of bytes (e.g. int and float are both 8 bytes on 64-bit), retrieving a float element through an int-typed pointer gives the raw IEEE 754 bits, not the numeric value, producing a spurious counterexample.
|
protected |
Infer the ESBMC-representable Python type name from a constant node. Handles bool (must precede int because bool is a subclass of int), int, float, and str. Returns 'Any' for anything else.
|
protected |
Infer key type from dict literal's first key
|
protected |
Infer value annotation from dict literal's first value
|
protected |
Infer type from function call nodes
|
protected |
Infer type from ast.Constant node
|
protected |
Infer the type string from an AST value node
|
protected |
True for a full tuple[A, B, ...] annotation node (not the bare name 'tuple'). Such annotations must be preserved end-to-end so the C++ list subscript read rebuilds the concrete tuple struct instead of erasing it to void* (#5444).
|
staticprotected |
|
protected |
Return True if call_node is a collections.defaultdict(...) call. Matches only when defaultdict was actually imported from collections. Handles both: from collections import defaultdict → defaultdict(...) from collections import defaultdict as dd → dd(...) import collections → collections.defaultdict(...) import collections as col → col.defaultdict(...)
|
protected |
|
staticprotected |
Return True when node matches `for i, v in enumerate(iterable, ...)`.
|
staticprotected |
Return True if `it` is a filter(func, iterable) call.
|
protected |
|
protected |
|
staticprotected |
Return True when node is an `ast.Lambda` taking no parameters.
|
staticprotected |
Return True if `it` is a reversed(seq) call (seq is not range()).
|
protected |
Return True if iter_node is reversed(range(...)).
|
protected |
Whether `node` names a function the module defines once, at top level.
|
staticprotected |
Return True if `it` is a zip(...) call with at least one argument.
|
protected |
Return True if var_name appears as a subscript key anywhere in body. Detects patterns like some_dict[var_name] or some_dict[var_name] = value. When iterating a plain dict (key type = Any), this implies the key is str, since it is being used to index another dict in the loop body.
|
protected |
Extract (key_ann, val_ann) AST nodes from a dict[K, V] annotation node. Returns the raw AST slice elements so nested types like dict[str, int] are preserved intact (not flattened to a string).
|
protected |
tuple[A, B, ...] element annotation of a list literal whose elements are all same-arity tuples of one sizable scalar type per position, else None. A key'd sorted() over a constant dict of tuple keys folds to such a literal, which carries no annotation of its own to read (#5444).
|
protected |
Walk expr, find all Load-context d[k] where d is a known defaultdict, generate missing-key init stmts, and rewrite each subscript slice to use the (possibly temp) key expression. Returns (init_stmts, new_expr). init_stmts is a (possibly empty) list of AST statements that must be prepended before the containing statement. This enables correct auto-insertion semantics for defaultdict reads that appear inside arbitrary expressions (assert, return, function args, etc.) rather than only as the direct RHS of an assignment.
|
protected |
Lower `for ... else: <orelse>` into a did-not-break flag. Returns (pre_statements, post_statements) to bracket the result of the for-to-while transform. Pre: init `flag = True`. Post: emit `if flag: <orelse>`. Side effect: rewrites every reachable `break` in the body to `flag = False; break`, and clears `node.orelse` so downstream transformers see a plain for. No-op when `node.orelse` is empty.
|
protected |
Lower `for x in Obj(...)` over a class with `__iter__`.
The sequence lowering below indexes the iterable by position, which a
user iterator does not support, so the loop reported a TypeError on a
correct program. Spell out the protocol instead:
it = <iterable>.__iter__()
while True:
try:
x = it.__next__()
except StopIteration:
break
<body>
Only for a constructor call of such a class, or a name whose one
binding in its scope is such a call, and without a for-else.
|
protected |
Lower `for x in <nditer>` to the iterator's own protocol, so the
converter tracks its position (`multi_index`, write-back, exhaustion):
it = np.nditer(...) # when the loop iterates a call
while True:
it._esbmc_nditer_advance()
if it.finished:
break
x = it._esbmc_nditer_item() # x = it[0]; y = it[1] for x, y
<body>
|
protected |
Generate: if key not in dict: dict[key] = factory() Returns (stmts, key_expr) where: - stmts is the list of AST statements to insert before the original node - key_expr is the safe key expression to use in the original subscript When key_node is a complex expression (not a bare Name), a temp variable is introduced so the expression is evaluated exactly once. The caller must replace the original subscript's slice with the returned key_expr to avoid a second evaluation.
|
protected |
Build `index = index +/- |step|` as an annotated int assignment.
|
protected |
Build `target = iter_var[index]` plus any tuple/list unpacking assigns.
|
protected |
Bind `seq` to an iterable variable usable by index-based iteration. A bare Name is used directly (preserving its type annotation); any other expression is copied into a fresh annotated ESBMC_iter variable. Returns (iter_var_name, setup_statements, element_type).
|
staticprotected |
Return `node.id` when node is ast.Name, else None.
|
protected |
The `np.nditer(...)` call `expr` is, or the one a name was last bound to; None otherwise.
|
protected |
Return the (list literal, start) the unroll needs, or reject with the reason.
|
protected |
Monotonic counter for staged-temp names emitted by tuple unpacking. Avoids using `id(source_node)` (CPython object id), which gets recycled after GC and yields non-stable names across runs. The counter lives on the preprocessor instance so it persists across visits within a single pass.
|
staticprotected |
``list[T]``/``dict[K, V]`` annotation for a rewritten builder name.
|
staticprotected |
``builder(max_size)``, or ``[builder() for _ in range(_nondet_size(max_size))]`` for a user function.
|
protected |
Name of the function `node` refers to, else None. A bare name, or an attribute of a module bound only by `import`, so `_sv_verifier.nondet_list(_sv_verifier.nondet_int)` reads as `nondet_list(nondet_int)` does after `from _sv_verifier import ...`.
|
staticprotected |
Keyword arguments of a nondet collection call, keyed by name. A keyword this model does not know is rejected rather than dropped: a dropped one silently reverts the element type to int, which is the vacuous-proof failure mode of esbmc/esbmc#7575 arriving through a typo. ``**kwargs`` (``kw.arg is None``) hides the bound the same way.
|
protected |
Type name behind a scalar nondet generator, else None. Accepts a call (``nondet_bool()``) and the bare function reference SV-COMP passes (``nondet_int``). Only the stubbed suffixes qualify, so an ordinary variable that happens to be named ``nondet_size`` is not mistaken for a generator and swallowed as the element type.
|
protected |
The builder for a list of `elem_node`'s elements. A user function is its own builder: the rewrite calls it once per element (#8965).
|
protected |
Extract and validate iterable and start value from enumerate call.
|
protected |
Parse and validate the for loop target, return target information.
|
protected |
Resolve a ``nondet_list``/``nondet_dict`` call. Returns ``(builder_name, max_size_node)`` naming the monomorphic builder in models/nondet.py that produces the requested element types, or None when `call` is not one of these generators.
|
protected |
Pre-populate variable_annotations for enumerate() loop value variable. Called before generic_visit so that inner expressions (e.g. tuple(sorted([elem, elem2]))) can infer the element type from the loop variable when the iterable has a known generic annotation like List[float].
|
protected |
Pre-populate variable_annotations for the loop variables of a dict.items() for loop. Called before generic_visit so that nested inner loops can look up the type of the outer loop's value variable (e.g. 'inner' for dict[str, dict[str, int]]) and resolve their own K/V types correctly.
|
protected |
|
protected |
`with np.nditer(...) as it:` binds `it` to the iterator itself.
|
protected |
Emit a located parser-stage diagnostic and abort, as threading lowering does.
|
protected |
|
protected |
Rewrite a nondet collection call to its monomorphic builder. The builder calls ``nondet_T()`` fresh per element, so indices hold independent values. Rewriting the callee rather than expanding the call into statements keeps this valid in every expression position -- an annotated assignment, a return, a call argument (esbmc/esbmc#7575).
|
staticprotected |
Return the int an expression denotes statically, or None.
|
protected |
Transform enumerate-based for loops to while loops.
Transforms:
for index, value in enumerate(iterable, start):
# body
Into:
ESBMC_iter = iterable
ESBMC_index = start # or 0 if not provided (enumeration index)
ESBMC_array_index = 0 # always starts at 0 (array access index)
ESBMC_length = len(ESBMC_iter)
while ESBMC_array_index < ESBMC_length:
index = ESBMC_index
value = ESBMC_iter[ESBMC_array_index]
ESBMC_index = ESBMC_index + 1
ESBMC_array_index = ESBMC_array_index + 1
# body
Handles both cases:
1. for index, value in enumerate(iterable, start): # tuple unpacking
2. for item in enumerate(iterable, start): # single variable gets tuple
|
protected |
for x in filter(func, seq): -> while loop over seq guarded by func(x). filter(None, seq) keeps truthy elements.
|
protected |
Unroll a for-loop over a dict literal with heterogeneous key types.
|
protected |
Unroll a for-loop over d.values() where values have heterogeneous types.
|
protected |
Transform dict.items() for loops to while loops.
Tuple-unpacking form (for k, v in d.items()):
ESBMC_keys_N: list[key_type] = d.keys()
ESBMC_vals_N: list[val_type] = d.values()
ESBMC_index_N: int = 0
ESBMC_length_N: int = len(ESBMC_keys_N)
while ESBMC_index_N < ESBMC_length_N:
k: key_type = ESBMC_keys_N[ESBMC_index_N]
v: val_type = ESBMC_vals_N[ESBMC_index_N]
ESBMC_index_N: int = ESBMC_index_N + 1
# body
Single-variable form (for item in d.items()):
ESBMC_keys_N: list[key_type] = d.keys()
ESBMC_vals_N: list[val_type] = d.values()
ESBMC_index_N: int = 0
ESBMC_length_N: int = len(ESBMC_keys_N)
while ESBMC_index_N < ESBMC_length_N:
item: tuple = (ESBMC_keys_N[ESBMC_index_N], ESBMC_vals_N[ESBMC_index_N])
ESBMC_index_N: int = ESBMC_index_N + 1
# body
Using intermediate annotated list variables lets the C++ list subscript
handler resolve element types from the AnnAssign annotation.
|
protected |
Transform general iterable for loops to while loops with unique variable names.
|
protected |
Transform the original for loop body statements.
|
protected |
Transform range-based for loops to while loops
|
protected |
for x in reversed(seq): -> backward index-based while loop over seq.
|
protected |
Transform reversed(range(args)) into an equivalent range(new_args) call.
Python semantics:
reversed(range(n)) → range(n-1, -1, -1)
reversed(range(start, stop)) → range(stop-1, start-1, -1)
reversed(range(start, stop, step))
→ range(ESBMC_reversed_range_start_(start, stop, step),
start-step, -step)
The helper function computes the last element of the original range
(or start-step for an empty range, keeping the reversed range empty).
All divisions inside the helper use same-sign operands, so C and
Python floor-division agree without any adjustment.
|
protected |
for a, b, ... in zip(s0, s1, ...): -> parallel index-based while loop. Iterates up to the shortest sequence (Python's zip semantics).
|
protected |
Return (list literal, start) when unrolling would preserve tuple shape. `for i, v in enumerate(pairs)` is lowered to a while loop whose value variable is a bare-`tuple`-annotated subscript read, which carries no component types, so a later `a, b = v` is handed an untyped value and refuses to unpack. Unrolling binds each tuple literal directly and keeps its shape, exactly as the nested-target form already does. Returns (None, None) when this does not apply, leaving the ordinary lowering in place -- unlike the nested form, a plain value target is fully supported there.
|
protected |
Bind each tuple literal directly, keeping its shape.
|
protected |
Emit one typed assignment + one body copy per element. typed_elts — list of (type_str, ast_value_node) in iteration order. For a Name loop target the per-iteration symbol is renamed so ESBMC never holds two incompatible types in the same IR symbol. For a Tuple/List loop target (e.g. ``for u, v in d:`` over a tuple-keyed dict) we assign each key into the destructuring pattern directly — the per-element types are uniform across iterations, so no rename is needed and the converter handles the unpack through its normal tuple-assignment path.
|
protected |
Unroll `for` over a tracked list literal variable into straight-line code. For ``Name`` loop targets, snapshots each list element into a per-iteration temp *before* emitting the unrolled body. This preserves Python's "list elements are evaluated once at list construction" semantics: when the body mutates a name that also appears among the list elements (e.g. ``xs = [a, a]; for x in xs: a = ...``), later iterations still see the original value via the temp instead of re-reading the now-mutated source name. For tuple/list unpacking targets (``for a, b in pairs:``), the snapshot path is skipped because the converter's tuple-unpacking pipeline requires the RHS to be a tuple/list literal — not a symbol load — and tuple-literal elements rarely depend on body-mutated names in practice.
|
protected |
Unroll `for i, (a, b) in enumerate(seq)` over a statically known list. Nested patterns need a literal RHS; see _unroll_list_literal_for (#6744). Shares its evaluate-once caveat: elements are not snapshotted, so an element naming a body-mutated variable reads the mutated value.
|
protected |
`iter(it)` of an nditer is the iterator itself.
|
protected |
Update known variable types for a simple assignment target
|
protected |
Return True if var_name is subscripted with a string constant anywhere in body. Used to infer that a loop variable annotated as Any is actually a dict, because val["key"] access in Python is only valid on mappings.
|
protected |
Validate enumerate() call arguments.
|
protected |
Validate that the start value is an integer (matching Python's behavior).
|
protected |
Return True if var_name is combined with a float operand in arithmetic. Detects `acc += var` (and `-=`, `*=`, ...) where acc is float, and `acc + var` / `var * f` where the other operand is a float literal or a name known to hold a float. Used to recover the value element type of an unannotated-parameter dict whose values are floats (#5501): the loop variable is otherwise erased to void*, and reading a float through void* produces an ill-sorted IEEE node.
|
protected |
Inner dispatch for visit_For after for-else lowering.
| preprocessor.loop_mixin.LoopMixin.visit_For | ( | self, | |
| node ) |
Transform for loops into while loops. Python's for-else (`else` runs when the loop completes without break) is lowered here at the boundary so all sub-transformers can emit their `while ... orelse=[]` shape uniformly without each having to remember to preserve the original `orelse`.
| preprocessor.loop_mixin.LoopMixin.visit_Name | ( | self, | |
| node ) |
| preprocessor.loop_mixin.LoopMixin.visit_With | ( | self, | |
| node ) |
Desugar 'with EXPR as VAR: BODY' into __enter__/__exit__ calls.
Transforms each context manager item into:
__esbmc_mgr_N = EXPR # annotated if class type is known
VAR = __esbmc_mgr_N.__enter__() # omitted when there is no 'as' clause
BODY
__esbmc_mgr_N.__exit__(0, 0, 0) # non-exceptional path; zeros for int args
Multiple items are expanded left-to-right; __exit__ is called in reverse order.
AsyncWith is handled identically via the class-level alias below.
|
staticprotected |
|
staticprotected |
|
protected |
|
protected |
|
staticprotected |
|
staticprotected |
|
staticprotected |
|
staticprotected |
|
staticprotected |
|
protected |
| tuple preprocessor.loop_mixin.LoopMixin.current_start_var |
|
static |
|
static |
|
static |
| preprocessor.loop_mixin.LoopMixin.generator_funcs |
| preprocessor.loop_mixin.LoopMixin.generator_vars |
| bool preprocessor.loop_mixin.LoopMixin.helper_functions_added = True |
|
static |
|
static |
| preprocessor.loop_mixin.LoopMixin.imported_module_names |
|
static |
| bool preprocessor.loop_mixin.LoopMixin.is_range_loop = True |
| preprocessor.loop_mixin.LoopMixin.iterator_classes |
| preprocessor.loop_mixin.LoopMixin.iterator_params |
|
static |
| preprocessor.loop_mixin.LoopMixin.module_name |
| preprocessor.loop_mixin.LoopMixin.new = new |
| preprocessor.loop_mixin.LoopMixin.numpy_module_names |
| preprocessor.loop_mixin.LoopMixin.old = old |
| preprocessor.loop_mixin.LoopMixin.shadowed_nondet_collections |
| preprocessor.loop_mixin.LoopMixin.target_name = target_name |
|
static |
|
static |
1.15.0