|
| | _iter_module_scope (cls, root, shadow_names) |
| | _collect_module_const_ints (self, module_node) |
| | _fold_module_const_range_args (self, module_node) |
| | _rewrite_range_aliases (self, module_node, seed=frozenset()) |
| | _collect_param_subscripting_funcs (self, module_node) |
| | _inline_range_wrappers (self, module_node, seed=None) |
| | _rewrite_module_aliases (self, module_node) |
| | _scan_iterator_classes (self, node) |
| | _scan_iterator_params (self, node) |
| | _iterator_params_of (self, func, calls) |
| | _is_iterator_construction (self, expr) |
| | _scan_dict_literal_bindings_and_calls (self, node) |
| | _scan_imported_module_names (self, node) |
| | _scan_shadowed_nondet_collections (self, node) |
| | _collect_scope_dict_binds (self, stmts) |
| | _record_scope_calls (self, stmts, local_binds, local_names, module_binds) |
◆ _appears_before()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._appears_before |
( |
| module_node, |
|
|
| name, |
|
|
| stmt ) |
|
staticprotected |
Whether a Name *name* occurs in *module_node* before *stmt*.
◆ _binding_sites()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._binding_sites |
( |
| module_node | ) |
|
|
staticprotected |
How many places anywhere in *module_node* bind or declare each name.
◆ _bound_names_of()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._bound_names_of |
( |
| node | ) |
|
|
staticprotected |
Names a single statement/expression node binds in its own scope.
◆ _capture_dunder_all()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._capture_dunder_all |
( |
| module_node | ) |
|
|
staticprotected |
Return the literal list/tuple of names assigned to __all__.
◆ _collect_module_const_ints()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._collect_module_const_ints |
( |
| self, |
|
|
| module_node ) |
|
protected |
Names bound exactly once, unconditionally at module top level, to an
integer literal, and never rebound — genuine module constants.
``_rebound_module_names`` already flags names assigned more than once,
assigned inside any conditional/loop/``with``, or declared ``global``,
so excluding it leaves only names that hold one fixed integer on every
path. Comprehension / generator-expression loop targets are a separate
local scope that ``_rebound_module_names`` does not see, so they are
excluded explicitly: a same-named module constant must never be folded
into ``[... range(N) ... for N in ...]``, where ``N`` is the loop
variable, not the constant.
◆ _collect_param_subscripting_funcs()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._collect_param_subscripting_funcs |
( |
| self, |
|
|
| module_node ) |
|
protected |
Names that may index the first argument they are called with.
Covers defs whose body subscripts their first parameter, plus every
imported name, whose body this scan cannot see. Keyed on name alone, so
a nested or rebound def of the same name counts too: over-refusing
costs a clear error, under-refusing costs a verdict.
◆ _collect_scope_dict_binds()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._collect_scope_dict_binds |
( |
| self, |
|
|
| stmts ) |
|
protected |
Map names bound to a dict literal in this scope to their dict[K, V]
annotation. A name reassigned to a conflicting shape or to a non-dict is
poisoned (dropped) so it is never used as recovery evidence. Returns
(bindings, all-assigned-names).
◆ _collect_single_return_funcs()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._collect_single_return_funcs |
( |
| module_node | ) |
|
|
staticprotected |
One-parameter single-return defs as name -> (param, expr), so a
``key=f`` folds like a lambda.
◆ _fold_module_const_range_args()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._fold_module_const_range_args |
( |
| self, |
|
|
| module_node ) |
|
protected |
Replace module-constant ``Name`` args of ``range()`` calls with their
integer literals.
``list(range(N))`` with a constant ``N`` otherwise takes the *symbolic*
range path, which builds a list whose ``size`` is set but whose elements
are nondet garbage — reading/slicing/copying it raises a spurious
``dereference failure`` (an unsound false positive). Folding a genuine
constant so the *concrete* range path materialises real elements removes
the false alarm. ``_iter_module_scope`` skips any nested function/class
scope that locally rebinds the name, so a shadowing parameter/local is
never folded to the module constant.
Only ``list(range(...))`` / ``tuple(range(...))`` — the sequence
*materialisation* contexts where the false deref occurs — are folded. A
``range()`` used directly as a ``for`` iterable is left untouched: it
never materialises elements, and its lowering models a zero ``step`` as
a runtime ``step != 0`` assertion that folding to a literal would turn
into a preprocess-time error (regression/python/range23_fail).
◆ _has_iter()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._has_iter |
( |
| cls, |
|
|
| iterable ) |
|
staticprotected |
◆ _inline_range_wrappers()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._inline_range_wrappers |
( |
| self, |
|
|
| module_node, |
|
|
| seed = None ) |
|
protected |
Inline trivial def f(p): return range(p_or_const, ...) wrappers.
◆ _int_literal_value()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._int_literal_value |
( |
| node | ) |
|
|
staticprotected |
Int value of an integer-literal AST node (or unary +/- of one), else
None. Booleans are excluded — ``True``/``False`` are not range sizes.
◆ _is_iterator_construction()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._is_iterator_construction |
( |
| self, |
|
|
| expr ) |
|
protected |
◆ _iter_module_scope()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._iter_module_scope |
( |
| cls, |
|
|
| root, |
|
|
| shadow_names ) |
|
protected |
Yield descendants of *root* whose enclosing scope is the module.
◆ _iterator_params_of()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._iterator_params_of |
( |
| self, |
|
|
| func, |
|
|
| calls ) |
|
protected |
The plain positional parameters of `func` that each of `calls`
passes positionally as a `Cls(...)` of an iterator class.
◆ _names_bound_without_import()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._names_bound_without_import |
( |
| n | ) |
|
|
staticprotected |
Names `n` binds in its scope, for any node but an `import`.
◆ _rebound_module_names()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._rebound_module_names |
( |
| module_node | ) |
|
|
staticprotected |
Module-top names that may be rebound after their first binding.
◆ _record_scope_calls()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._record_scope_calls |
( |
| self, |
|
|
| stmts, |
|
|
| local_binds, |
|
|
| local_names, |
|
|
| module_binds ) |
|
protected |
Record the per-call positional dict shapes for every direct call in
this scope, resolving Name arguments against the local bindings (or the
module bindings for free names).
◆ _rewrite_module_aliases()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._rewrite_module_aliases |
( |
| self, |
|
|
| module_node ) |
|
protected |
Rewrite a top-level `alias = mod` into `import <module> as alias`.
Only when `mod` is bound solely by an earlier top-level import, `alias`
solely by this statement, and nothing reads `alias` before it: then
both forms bind the same module at the same point, and the converter
resolves calls through the import form only (#8366).
◆ _rewrite_range_aliases()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._rewrite_range_aliases |
( |
| self, |
|
|
| module_node, |
|
|
| seed = frozenset() ) |
|
protected |
Rewrite module-scope alias = range (and chains) to canonical range.
◆ _scan_dict_literal_bindings_and_calls()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._scan_dict_literal_bindings_and_calls |
( |
| self, |
|
|
| node ) |
|
protected |
Collect evidence for parameter-dict element recovery (#5444).
For each scope (the module body and every function body, independently)
records its dict-literal name bindings, then resolves each direct
``name(...)`` call's positional arguments against that scope's bindings
(falling back to the module scope for free names). The result maps a
function name to its per-call list of argument dict[K, V] shapes, which
_recover_param_dict_annotation collapses only when every call agrees —
keeping the inference sound and scope-correct (a function-local dict
never poisons a same-named module global).
◆ _scan_imported_module_names()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._scan_imported_module_names |
( |
| self, |
|
|
| node ) |
|
protected |
Record names bound by a module-level `import` and by nothing else.
Only such a name denotes the module wherever it is read, so only its
attributes may stand for the module's nondet functions.
◆ _scan_iterator_classes()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._scan_iterator_classes |
( |
| self, |
|
|
| node ) |
|
protected |
Classes whose instances a for loop iterates through `__iter__`, for visit_For.
A class qualifies when it defines `__iter__` or inherits it from a
module class that does. A class without `__iter__` is not iterable,
and CPython's TypeError for it is already reported. The class name
must be bound only by its class statement, so a call of it constructs
the class.
◆ _scan_iterator_params()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._scan_iterator_params |
( |
| self, |
|
|
| node ) |
|
protected |
`(id(def), param)` for each parameter of a module function that
every reference to the function passes a `Cls(...)` of an iterator
class, so a for loop over the parameter can use `__iter__` (#8628).
The function name must be bound once and only ever called directly,
so no call goes unseen.
◆ _scan_shadowed_nondet_collections()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._scan_shadowed_nondet_collections |
( |
| self, |
|
|
| node ) |
|
protected |
Record `nondet_list`/`nondet_dict` names this module defines itself.
The rewrite to a typed builder matches on the callee name, so without
this a user's own `def nondet_list(...)` would be replaced by ESBMC's
model and its body never verified. A name that is only *imported* stays
interceptable: SV-COMP harnesses import `_sv_verifier.nondet_list`
expecting ESBMC's model, not the stub's body.
◆ _scope_locally_binds()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._scope_locally_binds |
( |
| scope_node, |
|
|
| names ) |
|
staticprotected |
True iff any of *names* is locally bound inside *scope_node*.
◆ _simple_single_return_defs()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._simple_single_return_defs |
( |
| module_node | ) |
|
|
staticprotected |
Yield ``(stmt, params, expr)`` for each undecorated, never-rebound
module-level ``def f(p, ...): return <expr>`` with plain parameters.
◆ _target_names()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._target_names |
( |
| target | ) |
|
|
staticprotected |
Names bound by an assignment target, including tuple/list unpacking.
◆ _walk_scope()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._walk_scope |
( |
| stmts | ) |
|
|
staticprotected |
Yield AST nodes within ``stmts`` without crossing into a nested
function/class/lambda scope (which binds its own names).
◆ apply_range_rewrites()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.apply_range_rewrites |
( |
| self, |
|
|
| module_node, |
|
|
| alias_seed = frozenset(), |
|
|
| wrapper_seed = None ) |
Run the range-alias and range-wrapper rewrites on *module_node*.
◆ collect_range_aliases()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.collect_range_aliases |
( |
| module_node, |
|
|
| seed = frozenset() ) |
|
static |
Collect module-scope canonical-range aliases.
◆ collect_range_wrappers()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.collect_range_wrappers |
( |
| module_node | ) |
|
|
static |
Collect trivial def f(p): return range(...) wrappers at module scope.
◆ prepare_module()
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.prepare_module |
( |
| self, |
|
|
| node, |
|
|
| alias_seed = frozenset(), |
|
|
| wrapper_seed = None, |
|
|
| entry = False ) |
Run pre-visit analyses and range-alias/wrapper canonicalization.
`entry` marks the program itself, whose module-level names no other
module imports.
◆ _dict_param_call_shapes
| dict preprocessor.module_rewrite_mixin.ModuleRewriteMixin._dict_param_call_shapes = {} |
|
protected |
◆ _names_bound_by
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._names_bound_by |
|
protected |
◆ _next_unpack_tmp_id
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._next_unpack_tmp_id |
|
protected |
◆ _param_subscripting_funcs
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._param_subscripting_funcs = self._collect_param_subscripting_funcs(node) |
|
protected |
◆ _single_return_funcs
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin._single_return_funcs = self._collect_single_return_funcs(node) |
|
protected |
◆ attr_list_element_classes
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.attr_list_element_classes = self._scan_attr_list_element_classes(node) |
◆ bases
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.bases |
◆ body
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.body |
◆ fixed_receivers
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.fixed_receivers |
◆ imported_module_names
| dict preprocessor.module_rewrite_mixin.ModuleRewriteMixin.imported_module_names = {m for m in imports if imports.count(m) == 1} - others |
◆ instance_var_classes
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.instance_var_classes |
Initial value:= \
self._build_var_class_map(node)
◆ iterator_classes
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.iterator_classes = self._scan_iterator_classes(node) |
◆ iterator_params
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.iterator_params = self._scan_iterator_params(node) |
◆ list_var_element_classes
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.list_var_element_classes = self._scan_list_var_element_classes(node) |
◆ module_class_names
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.module_class_names |
◆ module_dunder_all
| list preprocessor.module_rewrite_mixin.ModuleRewriteMixin.module_dunder_all | None |
|
static |
◆ module_name
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.module_name |
◆ referenced_names
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.referenced_names = _referenced_names(node) |
◆ scope_binding_counts
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.scope_binding_counts = self._scope_binding_counts(node) |
◆ variable_names
| preprocessor.module_rewrite_mixin.ModuleRewriteMixin.variable_names = self._variable_names(node) |
The documentation for this class was generated from the following file:
1.15.0