- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Public Member Functions | |
| hoist_nested_classes (self, module) | |
| copy_aliased_methods (self, module) | |
| visit_ClassDef (self, node) | |
| class_scope_default (self, default_node, method) | |
| names_bound_in (self, tree) | |
Public Attributes | |
| hoisted_classes = renames | |
| body | |
| name | |
| current_class_name = node.name | |
| is_entry_module | |
| blocked_type_functions | |
| dict | fixed_receivers |
| dict | once_bound_names = {name for name, count in counts.items() if count == 1} |
| dict | module_statements = {id(stmt): stmt for stmt in module.body} |
| class_attr_annotations | |
Static Protected Member Functions | |
| _names_bound_by (node) | |
| _class_ancestry (classes, node) | |
| _class_defines (node, name) | |
| _indirect_attributes (module, classes) | |
| _top_level_classes (module) | |
| _names_mentioned (module) | |
| _recovers_classes (module) | |
| _is_name_copy (node) | |
| _module_level_nodes (module) | |
| _fold_class_generator (node, classes, copies, counts) | |
| _class_generator (node, counts) | |
| _known_classes (module, counts) | |
| _typing_any (module) | |
| _is_plain_function (stmt) | |
| _lambda_as_def (stmt, counts) | |
| _called_parameters (func) | |
| _module_level_calls (node) | |
| _replace_reads (nodes, name, value) | |
| _is_type_of_none (arg, known) | |
| _class_argument (call, func, index, known) | |
| _class_value (node, known) | |
| _class_tuple (node, known) | |
| _class_name (node, known) | |
| _drop_tuple_arguments (call, func, indexes, key) | |
| _construction (stmt) | |
| _assigned_attributes (module) | |
| _variable_names (module) | |
| _scope_binding_counts (module) | |
| _function_may_return_truthy (func_node) | |
| _return_may_be_truthy (value) | |
Protected Attributes | |
| _pending_method_default_inits | |
| _class_stack | |
| _exit_suppresses_all = set() | |
| _classes_with_exit = set() | |
|
protected |
The def that `cls.body[index]` aliases, when a renamed copy of it is exact, else None.
|
staticprotected |
The attribute names `module` assigns or deletes anywhere.
|
protected |
Rewrite `alias(...)` to `Class(...)` where a top-level `alias = Class` statement is the only binding of `alias`, to a top-level class the module never rebinds: the converter recognises a constructor call only by the class's own name (#8352). A module-level call before the binding stays as written, since CPython raises NameError there.
|
protected |
Rewrite `cls(...)` in a @classmethod to the class the method runs on. Only in the entry module, and only when that class is known statically: every reference to the method is a direct `Class.method(...)` call and the classes involved use single inheritance. A subclass inheriting the method gets its own copy. Anything else keeps `cls(...)`, which the converter rejects.
|
protected |
|
protected |
Rewrite `self.Inner` in a method to the class hoisted out of the method's class or one of its ancestors (#8357). Only in the entry module, where every subclass is visible, and for a class that it and its subclasses only construct, subclass or test with isinstance, with single inheritance and no metaclass: otherwise a method may run on an instance of another class. And only for a name hoisted out of one class that the module mentions nowhere but in attribute loads: any other mention could bind it on an instance or a subclass, as could overriding `__getattribute__`.
|
protected |
Give a subclass its own copy of an inherited method that calls `self.m()` where the subclass resolves `m` to another definition than the method's class does, so the copy types `self` as the subclass and the call reaches the override (#9035). Only in the entry module, with single inheritance and no metaclass.
|
protected |
Replace a parameter or local that only ever holds one known class by that class's name, which the converter resolves statically (#8389). A known class is a top-level class or undecorated function bound only by its definition, or a builtin class the module never binds, so its name denotes the same object wherever it is read. A local qualifies when a statement `t = C` directly in its function's body is its only binding: the reads after that statement become `C`. A parameter qualifies when, in the entry module, every reference to its undecorated top-level function is a call passing a known class for it and nothing rebinds it; each distinct combination of such classes gets its own copy of the function, and the calls keep their arguments, so they are still evaluated.
|
protected |
Whether any node in `tree` other than `skip` binds `name`.
|
staticprotected |
The indexes of `func`'s positional parameters it calls by name.
|
protected |
Whether `method` of `cls` calls `self.x(...)` with an `x` that no class in the ancestry of `cls` defines, so only an attribute an instance gets elsewhere can supply it.
|
protected |
Whether `member` can be bound to each class in `targets`, copying it if needed.
|
protected |
Whether `cls.body[index]` is a nested class that keeps its meaning at module level: its name is bound by nothing else in the class scope, and moving its definition ahead of the outer class does not reorder two calls.
|
staticprotected |
`node` and its single-inheritance ancestors in `classes`, nearest first.
|
staticprotected |
The known class `call` passes for `func`'s positional parameter `index`, else None.
|
protected |
Whether a statement directly in a class body binds `name` there.
|
staticprotected |
|
staticprotected |
The one plain `for x in ...` clause of a call `any(...)` or `all(...)` on a generator, with neither name rebound, else None.
|
protected |
|
staticprotected |
The known class `node` names, or `NoneType` for `type(None)`, else None.
|
staticprotected |
The source of a tuple whose elements each spell a known class or `type(None)`, else None.
|
staticprotected |
The source of the known class, `type(None)`, or tuple of them that `node` spells, else None.
|
protected |
Classes other than `owner` whose `name` resolves to `owner`'s method.
|
protected |
The `cls(...)` calls of a @classmethod whose `cls` is never rebound, else [].
|
protected |
Scan __init__ for self.attr: T = ... and cache annotations.
|
staticprotected |
`(o, C)` for a statement `o = C(...)`, else None.
|
protected |
Whether a copy of `method` named `alias` behaves as the alias: the def is undecorated, its defaults are constants, since a copy evaluates them again, and both names are bound once in the class scope.
|
protected |
Give each subclass inheriting a method that calls `self.x(...)`, with `x` defined by no ancestor, its own copy (#8956). The copy types its receiver as the subclass, which may give `x`. Only in the entry module, for a class that no other class's object reaches (see _bind_nested_classes_via_self). The original is dropped when it can run on no object; otherwise the converter refuses its call.
|
staticprotected |
Pass `None` for each tuple of classes `call` gives a specialised parameter: the copy reads the tuple in place, and spelling it has no effect to keep, while a tuple argument would not match the copy's unread, untyped parameter.
|
protected |
Classes whose object may reach a method with a receiver of another class: all of them when the module can recover a class, else those named other than as a constructor call, a base, or the class tested by isinstance or issubclass.
|
staticprotected |
`bool(e1 or e2 ...)` for `any(e for x in <classes>)`, with `and` for `all`, else None.
|
staticprotected |
|
protected |
The subclasses of `owner` to give their own copy of `member`, or none when one overrides it or it uses `super()`, which would bind another class.
|
protected |
`cls` preceded by the classes hoisted out of it, recursively.
|
protected |
Turn a lambda passed at module level to a top-level function that calls that parameter into a def named for it, so that the function is specialised on it as on any def (#8979); whether any was. At module level a lambda's free names are globals either way.
|
staticprotected |
Attribute names used anywhere other than as a direct `Class.name(...)` call.
|
protected |
The classes hoisted out of `cls` or its ancestors, by attribute name, leaving out the names in `excluded`.
|
protected |
Whether a class named in `names` is `cls` or a subclass of it.
|
staticprotected |
Whether `node` is a plain `x = y` assignment.
|
staticprotected |
Whether `stmt` defines an undecorated function without *args or **kwargs: calls to a variadic function are lowered before this pass, so a call a copy introduces would be left unlowered (#8498).
|
staticprotected |
Whether `arg` is `type(None)`, which has no builtin name; the frontend reads NoneType as it (#8764).
|
staticprotected |
|
staticprotected |
`def f(...): return body` for a statement `f = lambda ...: body` that is the only binding of `f`, else None.
|
protected |
Rewrite a top-level `f = lambda ...` that calls one of its parameters to `def f(...)` when every reference to `f` is a call passing a known class or function for each called parameter, so that the def is specialised. The converter types lambda parameters as numbers and cannot call them (#8485).
|
protected |
The nearest class in `node`'s ancestry that defines `name`, or None.
|
staticprotected |
The calls in `node` that run at module level, outside any def, lambda or comprehension whose names a lambda could capture.
|
staticprotected |
The nodes of `module` outside any function or lambda body.
|
staticprotected |
The names a single AST node binds in its scope.
|
staticprotected |
Every identifier or string `module` mentions other than by loading an attribute.
|
protected |
|
protected |
The first parameter of an undecorated method that never rebinds it, else None.
|
protected |
Cache classes whose __exit__ may suppress exceptions.
|
protected |
Cache classes whose __exit__ unconditionally returns True.
|
staticprotected |
Whether `module` can reach a class from an instance or by name. A `type(x)` that is only an operand of `is` or `is not` reaches no method.
|
staticprotected |
Reads of `name` in `nodes` become `value`: a class name, or the source of a tuple of classes.
|
staticprotected |
|
protected |
Whether `member` of `owner`, which every subclass copies, runs on no object: `owner` is never constructed, nothing in `owner` names the method, and no class deriving from it names `super`, which could reach the original.
|
protected |
Map each `o` of a top-level `o = C(...)` to the methods `C` defines, where `o` and `C` are each bound only once and `C` is a top-level class, less any attribute name the module ever assigns: there `o.m` names the same method wherever it is evaluated (#8354).
|
staticprotected |
For each def in `module`, keyed by node id, and for `module`, keyed by None, the node and how often each name is bound in it outside its nested defs.
|
protected |
The names `member` calls on its receiver, when a copy of `member` is exact: it is undecorated, never rebinds its receiver, does not use `super` or `__class__`, and has constant defaults.
|
protected |
Specialise the first top-level function that only ever is called directly by name; whether one was.
|
protected |
Specialise the first top-level function the entry module calls with builtin classes (#9049) and nothing else references; whether one was. The entry module's calls are renamed to the copies.
|
protected |
Copy `func` once per combination of known classes its `calls` pass for its type parameters, naming no copy after a name in `taken`; whether it did.
|
staticprotected |
Top-level classes by name, or None when a name is defined twice.
|
protected |
A copy of `func` called `name` that reads each `(param, cls)` in `bindings` as `cls`.
|
protected |
The indexes of the parameters `func` reads and never rebinds, for which every one of `calls` passes a known class.
|
staticprotected |
The names `from typing import Any` binds, when nothing rebinds them. Counted afresh, as `self._names_bound_by` resolves to GeneratorMixin's, which skips imports.
|
protected |
Classes reached through multiple inheritance or a metaclass keyword.
|
protected |
Unroll a `for` loop, and an `any`/`all` over a generator, that runs over a tuple of known classes, so each copy reads one class by name (#8765). A loop qualifies when its target is a name and it has no `break`, `continue` or `else`; the target is left bound to the last class, as the loop leaves it. The tuple is written in place, or bound to a name nothing else binds.
|
staticprotected |
The names `module` binds anywhere other than by an import or a definition.
| preprocessor.class_context_mixin.ClassContextMixin.class_scope_default | ( | self, | |
| default_node, | |||
| method ) |
A method default naming an attribute its top-level class bound before the method, as `Class.name`: the default is hoisted past the class, where the bare name no longer resolves (#8200).
| preprocessor.class_context_mixin.ClassContextMixin.copy_aliased_methods | ( | self, | |
| module ) |
Replace each class-body `alias = name` that names an earlier def of the same class body with a copy of that def called `alias` (#8356). Python binds the alias to the def's function object, so the copy runs the same body even when a subclass overrides `name`.
| preprocessor.class_context_mixin.ClassContextMixin.hoist_nested_classes | ( | self, | |
| module ) |
Lift each class nested in a module-level class body to module level as `Outer__Inner`, since the converter only builds module-level classes (#8256). `Outer.Inner` is rewritten everywhere, and so is a bare `Inner` that the outer class body's scope resolves to the nested class. The rewrite is purely by name, so an outer class whose name is bound anywhere else in the module is left alone.
| preprocessor.class_context_mixin.ClassContextMixin.names_bound_in | ( | self, | |
| tree ) |
Every name `tree` binds.
| preprocessor.class_context_mixin.ClassContextMixin.visit_ClassDef | ( | self, | |
| node ) |
Track class context for method definitions.
|
protected |
|
protected |
|
protected |
|
protected |
| preprocessor.class_context_mixin.ClassContextMixin.blocked_type_functions |
| preprocessor.class_context_mixin.ClassContextMixin.body |
| preprocessor.class_context_mixin.ClassContextMixin.class_attr_annotations |
| preprocessor.class_context_mixin.ClassContextMixin.current_class_name = node.name |
| dict preprocessor.class_context_mixin.ClassContextMixin.fixed_receivers |
| preprocessor.class_context_mixin.ClassContextMixin.hoisted_classes = renames |
| preprocessor.class_context_mixin.ClassContextMixin.is_entry_module |
| dict preprocessor.class_context_mixin.ClassContextMixin.module_statements = {id(stmt): stmt for stmt in module.body} |
| preprocessor.class_context_mixin.ClassContextMixin.name |
| dict preprocessor.class_context_mixin.ClassContextMixin.once_bound_names = {name for name, count in counts.items() if count == 1} |
1.15.0