Module `refinery.lib.scripts.au3.analysis`

Static-analysis substrate for AutoIt3 deobfuscation. Transforms query a shared, computed model of the program here instead of each re-deriving scope, binding, and constant-value facts on their own.

refinery.lib.scripts.au3.analysis.values owns the value domain and every operator's semantics over it, refinery.lib.scripts.au3.analysis.builtins the emulation table for the pure builtin functions, refinery.lib.scripts.au3.analysis.scopes the documented scoping rules that decide which storage a write targets, refinery.lib.scripts.au3.analysis.existence the census of the names a global may take, refinery.lib.scripts.au3.analysis.aliases the per-scope map of variables that provably name one function, and refinery.lib.scripts.au3.analysis.propagation the constant-binding walk with the may-write summaries it rests on. refinery.lib.scripts.au3.analysis.cache binds them into the per-run model cache the pipeline shares across transforms.

Expand source code Browse git

"""
Static-analysis substrate for AutoIt3 deobfuscation. Transforms query a shared, computed model of
the program here instead of each re-deriving scope, binding, and constant-value facts on their own.

`values` owns the value domain and every operator's semantics over it, `builtins` the emulation
table for the pure builtin functions, `scopes` the documented scoping rules that decide which
storage a write targets, `existence` the census of the names a global may take, `aliases` the
per-scope map of variables that provably name one function, and `propagation` the
constant-binding walk with the may-write summaries it rests on. `cache` binds them into the
per-run model cache the pipeline shares across transforms.
"""
from refinery.lib.scripts.au3.analysis.cache import Au3ModelCache, model_cache
from refinery.lib.scripts.au3.analysis.existence import (
    Au3ExistenceModel,
    build_existence_model,
)
from refinery.lib.scripts.au3.analysis.propagation import (
    Au3PropagationModel,
    build_propagation_model,
)
from refinery.lib.scripts.au3.analysis.scopes import Au3ScopeModel, Binding, build_scope_model
from refinery.lib.scripts.au3.analysis.values import Au3Value

__all__ = [
    'Au3ExistenceModel',
    'Au3ModelCache',
    'Au3PropagationModel',
    'Au3ScopeModel',
    'Au3Value',
    'Binding',
    'build_existence_model',
    'build_propagation_model',
    'build_scope_model',
    'model_cache',
]

Sub-modules

refinery.lib.scripts.au3.analysis.aliases: The alias map: which variables provably name one function, per scope. The indirection obfuscation assigns a builtin or a function name to a variable …
refinery.lib.scripts.au3.analysis.builtins: The AutoIt3 builtin emulation table: the functions a call folds over when every argument is a known value. A rule is pinned by the probe outputs in …
refinery.lib.scripts.au3.analysis.cache: A per-run cache of the AutoIt3 analysis models. The deobfuscation pipeline builds one cache over the script being transformed and shares it across …
refinery.lib.scripts.au3.analysis.constants: The one constant evaluator: the value an expression provably holds, over the operator tables of refinery.lib.scripts.au3.analysis.values and the …
refinery.lib.scripts.au3.analysis.existence: The existence model: the names a global may take when the tree runs. The may-write summary refinement asks it — a bare write inside a function creates …
refinery.lib.scripts.au3.analysis.interpreter: One script function of an AutoIt3 tree, run over the value domain. The Phase 3 transform calls it on a call whose every argument is a literal, and …
refinery.lib.scripts.au3.analysis.propagation: The constant-binding walk: which variable holds which value at every read, and which globals every script function may write. The propagate transform …
refinery.lib.scripts.au3.analysis.scopes: AutoIt3 scoping: the documented rules that decide which storage a write or a read targets and which storage an occurrence may reach, and the script's …
refinery.lib.scripts.au3.analysis.unparsed: The reader for source text the parser could not read: an error node's verbatim line, or an Execute payload this parser refuses. The interpreter may …
refinery.lib.scripts.au3.analysis.usage: The usage model: what the script does with its names. The dead-code elimination in refinery.lib.scripts.au3.deobfuscation.eliminate asks it what a …
refinery.lib.scripts.au3.analysis.values: The AutoIt3 value domain: the kinds a value can have, the coercions between them, and the result of every operator over known values. Operator …

Functions

def build_existence_model(root, scope_model, memo=None)

Walk every global-creation channel of root and collect the names a global may take, over the functions and the include answer of scope_model. A memo the run holds across its tree versions answers the probes an earlier census already made.

Expand source code Browse git

def build_existence_model(
    root: Au3Script,
    scope_model: Au3ScopeModel,
    memo: Au3ProbeMemo | None = None,
) -> Au3ExistenceModel:
    """
    Walk every global-creation channel of *root* and collect the names a global may take, over
    the functions and the include answer of *scope_model*. A *memo* the run holds across its tree
    versions answers the probes an earlier census already made.
    """
    if memo is None:
        memo = Au3ProbeMemo()
    memo.renew()
    return _Census(scope_model, memo).collect(root)

def build_propagation_model(root, scope_model, existence)

Walk every scope of root — the script body and every function body — and record the value at each variable read the walk reaches, along with the may-write summaries the calls rest on, over the global-existence answer of existence.

Expand source code Browse git

def build_propagation_model(
    root: Au3Script,
    scope_model: Au3ScopeModel,
    existence: Au3ExistenceModel,
) -> Au3PropagationModel:
    """
    Walk every scope of *root* — the script body and every function body — and record the value
    at each variable read the walk reaches, along with the may-write summaries the calls rest on,
    over the global-existence answer of *existence*.
    """
    summaries = _build_summaries(scope_model, existence)
    walker = _Walker(scope_model, summaries)
    for scope, body in ast.scope_bodies(root):
        walker.walk_scope(scope, body)
    return Au3PropagationModel(walker.values, summaries, walker.entries)

def build_scope_model(root)

Collect the function declarations of root, the local facts of each body, the script body's first Global claims, the names the tree declares constants, whether the tree holds an include — the node the parser reads an include line without trailing text into, or the directive one with trailing text becomes — and every error node the parser recovered, in walk order. Two functions of one name never coexist in a script AutoIt runs, so the mapping keeps the last of them without comment.

Expand source code Browse git

def build_scope_model(root: Au3Script) -> Au3ScopeModel:
    """
    Collect the function declarations of *root*, the local facts of each body, the script body's
    first `Global` claims, the names the tree declares constants, whether the tree holds an
    include — the node the parser reads an include line without trailing text into, or the
    directive one with trailing text becomes — and every error node the parser recovered, in
    walk order. Two functions of one name never coexist in a script AutoIt runs, so the mapping
    keeps the last of them without comment.
    """
    functions: dict[str, Au3FunctionDeclaration] = {}
    holds_an_include = False
    error_nodes: list[Au3ErrorNode] = []
    for node in root.walk():
        if isinstance(node, Au3FunctionDeclaration):
            if node.name is not None:
                functions[node.name.name] = node
        elif isinstance(node, (Au3Include, Au3IncludeOnce)):
            holds_an_include = True
        elif isinstance(node, Au3Directive) and INCLUDE_SPELLING.match(node.text):
            holds_an_include = True
        elif isinstance(node, Au3ErrorNode):
            error_nodes.append(node)
    local_facts = {function: _local_facts(function) for function in functions.values()}
    return Au3ScopeModel(
        functions,
        local_facts,
        _first_global_claims(root.body),
        _constant_names(root),
        holds_an_include,
        tuple(error_nodes),
    )

def model_cache(transformer, root)

The pipeline's shared Au3ModelCache for root when one is attached to transformer and built over that same root, otherwise a fresh cache stashed back onto transformer for reuse within its single-pass lifetime. See ModelCacheBase.for_transformer().

Expand source code Browse git

def model_cache(transformer: Transformer, root: Node) -> Au3ModelCache:
    """
    The pipeline's shared `Au3ModelCache` for *root* when one is attached to *transformer* and
    built over that same root, otherwise a fresh cache stashed back onto *transformer* for reuse
    within its single-pass lifetime. See
    `refinery.lib.scripts.modelcache.ModelCacheBase.for_transformer`.
    """
    return Au3ModelCache.for_transformer(transformer, root)

Classes

class Au3ExistenceModel (possible_globals, implicit_writes_are_fatal)

What the census learned about one tree version: the names a global may take — None when any name may — and whether the tree may set MustDeclareVars, which makes every implicit write fatal; with both, which writes inside a function may target a global. Built once per tree version by build_existence_model().

Expand source code Browse git

@dataclass(frozen=True)
class Au3ExistenceModel:
    """
    What the census learned about one tree version: the names a global may take — `None` when
    any name may — and whether the tree may set `MustDeclareVars`, which makes every implicit
    write fatal; with both, which writes inside a function may target a global. Built once per
    tree version by `build_existence_model`.
    """
    possible_globals: frozenset[str] | None
    implicit_writes_are_fatal: bool

    def global_may_exist(self, name: str) -> bool:
        """
        Whether a global of *name* may exist when the tree runs.
        """
        return self.possible_globals is None or name in self.possible_globals

    def write_may_target_global(self, binding: Binding, name: str, creates_storage: bool) -> bool:
        """
        Whether a write of *name* inside a function, whose storage *binding* answers, may target
        a global. A provable local never does and a provable global always does. A write that
        proves nothing creates a local where no global of the name exists, so it may target one
        only where the census answers that one may exist, or where the tree may make every
        implicit write fatal. A write that creates no storage — a `ReDim`, which resizes an array
        that exists or ends the script — is outside that refinement and may target a global
        wherever no local provably holds the name.
        """
        if binding is Binding.LOCAL:
            return False
        if binding is Binding.GLOBAL or not creates_storage:
            return True
        return self.implicit_writes_are_fatal or self.global_may_exist(name)

    def write_is_fatal(self, name: str) -> bool:
        """
        Whether a store of *name* is a fatal error the tree runs into: one of the command-line
        constants every script starts with is read-only, so its store can never leave.
        """
        return name in _PREDEFINED_GLOBALS

Instance variables

var possible_globals: The type of the None singleton.
var implicit_writes_are_fatal: The type of the None singleton.

Methods

def global_may_exist(self, name)

Whether a global of name may exist when the tree runs.

Expand source code Browse git

def global_may_exist(self, name: str) -> bool:
    """
    Whether a global of *name* may exist when the tree runs.
    """
    return self.possible_globals is None or name in self.possible_globals

def write_may_target_global(self, binding, name, creates_storage)

Whether a write of name inside a function, whose storage binding answers, may target a global. A provable local never does and a provable global always does. A write that proves nothing creates a local where no global of the name exists, so it may target one only where the census answers that one may exist, or where the tree may make every implicit write fatal. A write that creates no storage — a ReDim, which resizes an array that exists or ends the script — is outside that refinement and may target a global wherever no local provably holds the name.

Expand source code Browse git

def write_may_target_global(self, binding: Binding, name: str, creates_storage: bool) -> bool:
    """
    Whether a write of *name* inside a function, whose storage *binding* answers, may target
    a global. A provable local never does and a provable global always does. A write that
    proves nothing creates a local where no global of the name exists, so it may target one
    only where the census answers that one may exist, or where the tree may make every
    implicit write fatal. A write that creates no storage — a `ReDim`, which resizes an array
    that exists or ends the script — is outside that refinement and may target a global
    wherever no local provably holds the name.
    """
    if binding is Binding.LOCAL:
        return False
    if binding is Binding.GLOBAL or not creates_storage:
        return True
    return self.implicit_writes_are_fatal or self.global_may_exist(name)

def write_is_fatal(self, name)

Whether a store of name is a fatal error the tree runs into: one of the command-line constants every script starts with is read-only, so its store can never leave.

Expand source code Browse git

def write_is_fatal(self, name: str) -> bool:
    """
    Whether a store of *name* is a fatal error the tree runs into: one of the command-line
    constants every script starts with is read-only, so its store can never leave.
    """
    return name in _PREDEFINED_GLOBALS

class Au3ModelCache (root, options=None)

Lazily builds and memoizes the analysis models for one root script — the scope model the transforms ask which storage a write targets and which names are constant, the existence census the summary refinement leans on, the alias map the indirection rewrite reads, the propagation model the constant substitution reads, and the usage model the dead-code elimination reads — each dropped, together, whenever this root's tree changes. The probes the census makes are remembered for the whole run instead: their answers depend on what each probe reads, not on the tree version. Beside the models, the cache owns the facts composed over several of them — entry_is_open, whether the script runs from its own top-level statements rather than from outside the tree, and may_read_error_state, whether the script may read the interpreter's @error or @extended at run time.

Expand source code Browse git

class Au3ModelCache(ModelCacheBase):
    """
    Lazily builds and memoizes the analysis models for one root script — the scope model the
    transforms ask which storage a write targets and which names are constant, the existence
    census the summary refinement leans on, the alias map the indirection rewrite reads, the
    propagation model the constant substitution reads, and the usage model the dead-code
    elimination reads — each dropped, together, whenever this root's tree changes. The probes
    the census makes are remembered for the whole run instead: their answers depend on what each
    probe reads, not on the tree version. Beside the models, the cache owns the facts composed
    over several of them — `entry_is_open`, whether the script runs from its own top-level
    statements rather than from outside the tree, and `may_read_error_state`, whether the script
    may read the interpreter's `@error` or `@extended` at run time.
    """

    _SLOTS = (
        '_scopes',
        '_existence',
        '_aliases',
        '_propagation',
        '_usage',
    )

    root: Au3Script
    _scopes: Au3ScopeModel | None
    _existence: Au3ExistenceModel | None
    _aliases: Au3AliasModel | None
    _propagation: Au3PropagationModel | None
    _usage: Au3UsageModel | None

    def __init__(self, root: Node, options: object | None = None):
        super().__init__(root, options)
        self._probes = Au3ProbeMemo()

    @property
    def scopes(self) -> Au3ScopeModel:
        return self._lazy('_scopes', lambda: build_scope_model(self.root))

    @property
    def existence(self) -> Au3ExistenceModel:
        """
        The names a global may take when the root runs, and whether the tree may make every
        implicit write fatal by setting `MustDeclareVars`.
        """
        return self._lazy(
            '_existence',
            lambda: build_existence_model(self.root, self.scopes, self._probes),
        )

    @property
    def aliases(self) -> Au3AliasModel:
        """
        The per-scope map of variables that provably name one function, cut by every name a
        rebinding write — an `Assign`, a code-running `Execute`, or a script function call — may
        cost, which the propagation summaries feed.
        """
        return self._lazy('_aliases', lambda: build_alias_model(
            self.root, self.scopes, self.propagation.summaries))

    @property
    def propagation(self) -> Au3PropagationModel:
        """
        The value at every variable read and the may-write summary of every script function, over
        the scope model's binding answers.
        """
        return self._lazy(
            '_propagation',
            lambda: build_propagation_model(self.root, self.scopes, self.existence),
        )

    @property
    def usage(self) -> Au3UsageModel:
        """
        What the script does with its names — the call counts, purity, channels, spellings, and
        storage bindings the dead-code elimination asks — over the scope model's bindings and the
        propagation walk's may-write summaries.
        """
        return self._lazy('_usage', lambda: build_usage_model(
            self.root, self.scopes, self.propagation.summaries))

    @property
    def entry_is_open(self) -> bool:
        """
        Whether the root runs from its own top-level statements: it holds a statement that is
        neither a declaration, a function definition nor a directive, and no include — read from
        the scope model in both spellings the parser answers with, and from the unread text the
        usage model holds — because an included file's contents are called from outside the tree.
        """
        if self.scopes.holds_an_include:
            return False
        if self.usage.holds_unread_include():
            return False
        for statement in self.root.body:
            if not isinstance(statement, (
                Au3VariableDeclaration,
                Au3EnumDeclaration,
                Au3FunctionDeclaration,
                Au3Directive,
            )):
                return True
        return False

    @property
    def may_read_error_state(self) -> bool:
        """
        Whether the script may read the interpreter's `@error` or `@extended` at run time: a read
        of either macro anywhere in the tree, a callee computed at run time — which may name
        `Execute` over a payload no walk reads — an include, whose contents no fact of the tree
        holds, or an `Execute` the tree spells, in text the parser could not read included, whose
        payload is not provably free of such a read. Entering a user function clears both (probe9
        A17/A17b), so a pass that replaces a call with its value drops a write a later read may
        observe.
        """
        census = callee_census(self.root, self.usage.functions, self.usage.unparsed)
        if census.reads_error_macros or census.computed_callee:
            return True
        if self.scopes.holds_an_include or self.usage.holds_unread_include():
            return True
        if any(
            'execute' in facts.identifiers
            for facts in self.usage.unparsed.values()
        ):
            return True
        return any(
            isinstance(node, Au3Call)
            and _call_may_read_error_state(node, self.usage.functions)
            for node in self.root.walk()
        )

Ancestors

ModelCacheBase

Instance variables

var scopes

Expand source code Browse git

@property
def scopes(self) -> Au3ScopeModel:
    return self._lazy('_scopes', lambda: build_scope_model(self.root))

var existence

The names a global may take when the root runs, and whether the tree may make every implicit write fatal by setting MustDeclareVars.

Expand source code Browse git

@property
def existence(self) -> Au3ExistenceModel:
    """
    The names a global may take when the root runs, and whether the tree may make every
    implicit write fatal by setting `MustDeclareVars`.
    """
    return self._lazy(
        '_existence',
        lambda: build_existence_model(self.root, self.scopes, self._probes),
    )

var aliases

The per-scope map of variables that provably name one function, cut by every name a rebinding write — an Assign, a code-running Execute, or a script function call — may cost, which the propagation summaries feed.

Expand source code Browse git

@property
def aliases(self) -> Au3AliasModel:
    """
    The per-scope map of variables that provably name one function, cut by every name a
    rebinding write — an `Assign`, a code-running `Execute`, or a script function call — may
    cost, which the propagation summaries feed.
    """
    return self._lazy('_aliases', lambda: build_alias_model(
        self.root, self.scopes, self.propagation.summaries))

var propagation

The value at every variable read and the may-write summary of every script function, over the scope model's binding answers.

Expand source code Browse git

@property
def propagation(self) -> Au3PropagationModel:
    """
    The value at every variable read and the may-write summary of every script function, over
    the scope model's binding answers.
    """
    return self._lazy(
        '_propagation',
        lambda: build_propagation_model(self.root, self.scopes, self.existence),
    )

var usage

What the script does with its names — the call counts, purity, channels, spellings, and storage bindings the dead-code elimination asks — over the scope model's bindings and the propagation walk's may-write summaries.

Expand source code Browse git

@property
def usage(self) -> Au3UsageModel:
    """
    What the script does with its names — the call counts, purity, channels, spellings, and
    storage bindings the dead-code elimination asks — over the scope model's bindings and the
    propagation walk's may-write summaries.
    """
    return self._lazy('_usage', lambda: build_usage_model(
        self.root, self.scopes, self.propagation.summaries))

var entry_is_open

Whether the root runs from its own top-level statements: it holds a statement that is neither a declaration, a function definition nor a directive, and no include — read from the scope model in both spellings the parser answers with, and from the unread text the usage model holds — because an included file's contents are called from outside the tree.

Expand source code Browse git

@property
def entry_is_open(self) -> bool:
    """
    Whether the root runs from its own top-level statements: it holds a statement that is
    neither a declaration, a function definition nor a directive, and no include — read from
    the scope model in both spellings the parser answers with, and from the unread text the
    usage model holds — because an included file's contents are called from outside the tree.
    """
    if self.scopes.holds_an_include:
        return False
    if self.usage.holds_unread_include():
        return False
    for statement in self.root.body:
        if not isinstance(statement, (
            Au3VariableDeclaration,
            Au3EnumDeclaration,
            Au3FunctionDeclaration,
            Au3Directive,
        )):
            return True
    return False

var may_read_error_state

Whether the script may read the interpreter's @error or @extended at run time: a read of either macro anywhere in the tree, a callee computed at run time — which may name Execute over a payload no walk reads — an include, whose contents no fact of the tree holds, or an Execute the tree spells, in text the parser could not read included, whose payload is not provably free of such a read. Entering a user function clears both (probe9 A17/A17b), so a pass that replaces a call with its value drops a write a later read may observe.

Expand source code Browse git

@property
def may_read_error_state(self) -> bool:
    """
    Whether the script may read the interpreter's `@error` or `@extended` at run time: a read
    of either macro anywhere in the tree, a callee computed at run time — which may name
    `Execute` over a payload no walk reads — an include, whose contents no fact of the tree
    holds, or an `Execute` the tree spells, in text the parser could not read included, whose
    payload is not provably free of such a read. Entering a user function clears both (probe9
    A17/A17b), so a pass that replaces a call with its value drops a write a later read may
    observe.
    """
    census = callee_census(self.root, self.usage.functions, self.usage.unparsed)
    if census.reads_error_macros or census.computed_callee:
        return True
    if self.scopes.holds_an_include or self.usage.holds_unread_include():
        return True
    if any(
        'execute' in facts.identifiers
        for facts in self.usage.unparsed.values()
    ):
        return True
    return any(
        isinstance(node, Au3Call)
        and _call_may_read_error_state(node, self.usage.functions)
        for node in self.root.walk()
    )

Inherited members

ModelCacheBase:
- for_transformer
- invalidate
- options
- pinned
- renew
- root
- warm

class Au3PropagationModel (values, summaries, entries)

What the walk learned about one tree version: the value at every variable read a substitution may replace — a read in a target or ByRef position is never recorded — the may-write summary of every script function, and the globals proven at every script-level call to a function that writes none. Built once per tree version by build_propagation_model().

Expand source code Browse git

@dataclass(frozen=True)
class Au3PropagationModel:
    """
    What the walk learned about one tree version: the value at every variable read a
    substitution may replace — a read in a target or `ByRef` position is never recorded — the
    may-write summary of every script function, and the globals proven at every script-level call
    to a function that writes none. Built once per tree version by `build_propagation_model`.
    """
    values: dict[Au3Variable, Au3Value]
    summaries: dict[str, frozenset[str] | None]
    entries: dict[Au3Call, dict[str, Au3Value]]

    def value_at(self, node: Au3Variable) -> Au3Value | None:
        """
        The value *node* provably holds where it is read, or `None` when the walk does not know.
        """
        return self.values.get(node)

    def may_write(self, function: str) -> frozenset[str] | None:
        """
        The globals *function* may write, or `None` when it may write any.
        """
        return self.summaries.get(function)

    def entry_globals(self, call: Au3Call) -> Mapping[str, Au3Value]:
        """
        The globals the walk proves a value for where *call* stands — a call at script level to a
        function whose summary is empty, so nothing it does can change them and the values hold
        for the whole call. Inside a function body the walk knows no globals, so the answer there
        is empty.
        """
        return self.entries.get(call, {})

Instance variables

var values: The type of the None singleton.
var summaries: The type of the None singleton.
var entries: The type of the None singleton.

Methods

def value_at(self, node)

The value node provably holds where it is read, or None when the walk does not know.

Expand source code Browse git

def value_at(self, node: Au3Variable) -> Au3Value | None:
    """
    The value *node* provably holds where it is read, or `None` when the walk does not know.
    """
    return self.values.get(node)

def may_write(self, function)

The globals function may write, or None when it may write any.

Expand source code Browse git

def may_write(self, function: str) -> frozenset[str] | None:
    """
    The globals *function* may write, or `None` when it may write any.
    """
    return self.summaries.get(function)

def entry_globals(self, call)

The globals the walk proves a value for where call stands — a call at script level to a function whose summary is empty, so nothing it does can change them and the values hold for the whole call. Inside a function body the walk knows no globals, so the answer there is empty.

Expand source code Browse git

def entry_globals(self, call: Au3Call) -> Mapping[str, Au3Value]:
    """
    The globals the walk proves a value for where *call* stands — a call at script level to a
    function whose summary is empty, so nothing it does can change them and the values hold
    for the whole call. Inside a function body the walk knows no globals, so the answer there
    is empty.
    """
    return self.entries.get(call, {})

class Au3ScopeModel (functions, local_facts=<factory>, script_first_global=<factory>, constant_names=frozenset(), holds_an_include=False, error_nodes=())

The script's declared functions, the answers to which storage a write or a read targets and which storage an occurrence may reach, whether a write reaches a caller's storage, whether a declaration backs a plain write, the names the tree declares constants, whether the tree holds an include, and the error nodes the parser recovered. Built once per tree version by build_scope_model().

Expand source code Browse git

@dataclass(frozen=True)
class Au3ScopeModel:
    """
    The script's declared functions, the answers to which storage a write or a read targets and
    which storage an occurrence may reach, whether a write reaches a caller's storage, whether a
    declaration backs a plain write, the names the tree declares constants, whether the tree
    holds an include, and the error nodes the parser recovered. Built once per tree version by
    `build_scope_model`.
    """
    functions: dict[str, Au3FunctionDeclaration]
    local_facts: dict[Au3FunctionDeclaration, Au3LocalFacts] = field(default_factory=dict)
    script_first_global: dict[str, int] = field(default_factory=dict)
    constant_names: frozenset[str] = frozenset()
    holds_an_include: bool = False
    error_nodes: tuple[Au3ErrorNode, ...] = ()

    @property
    def function_names(self) -> frozenset[str]:
        return frozenset(self.functions)

    @property
    def holds_a_parse_error(self) -> bool:
        """
        Whether the parser recovered an error node anywhere in the tree: live source text or a
        repaired construct no walk reads, which may hold any declaration.
        """
        return bool(self.error_nodes)

    def binding(
        self,
        scope: Au3FunctionDeclaration | None,
        write: Node,
        name: str,
    ) -> Binding:
        """
        The storage the write *write* performs on *name* targets when it stands in *scope*: the
        whole script when `None`, one function's body otherwise. The write is the declaration,
        assignment, loop, or ReDim statement that performs it —
        `refinery.lib.scripts.au3.ast.owning_statement` names it from any node inside. A bare,
        compound, `Dim`, or `ReDim` write whose name is a parameter of the function, whose name a
        local-forcing declaration in the body precedes, or whose name a `For`/`For…In` loop in
        the body claims at or before it, targets that local — unless a `Global` declaration of
        the name anywhere in the function claims the global.
        """
        if scope is None:
            return Binding.GLOBAL
        if isinstance(write, (Au3ForStatement, Au3ForInStatement)):
            return Binding.LOCAL
        if isinstance(write, (Au3VariableDeclaration, Au3EnumDeclaration)):
            if write.scope is Au3ScopeKind.GLOBAL:
                return Binding.GLOBAL
            if write.scope is Au3ScopeKind.LOCAL:
                return Binding.LOCAL
            if isinstance(write, Au3VariableDeclaration) and write.is_static:
                return Binding.LOCAL
            if write.is_const:
                return Binding.LOCAL
        facts = self.local_facts.get(scope)
        if facts is None or name in facts.global_names:
            return Binding.NONE
        if name in facts.parameters:
            return Binding.LOCAL
        first = facts.first_local.get(name)
        if first is None:
            return Binding.NONE
        if first <= _top_level_index(scope, write):
            return Binding.LOCAL
        return Binding.NONE

    def writes_caller_storage(self, scope: Au3FunctionDeclaration | None, name: str) -> bool:
        """
        Whether a write of *name* in *scope* may reach storage the caller holds: the name is a
        `ByRef` parameter of the function. `binding` answers such a write `Binding.LOCAL` — the
        parameter is the function's own name for the variable — so a caller that removes a write
        because no read in the function observes it asks this as well. A function the model holds
        no facts for may write any caller's storage.
        """
        if scope is None:
            return False
        facts = self.local_facts.get(scope)
        return facts is None or name in facts.reference_parameters

    def declaration_backs_write(
        self,
        scope: Au3FunctionDeclaration | None,
        write: Node,
        name: str,
    ) -> bool:
        """
        Whether a declaration of *name* backs the plain write *write* standing in *scope*: a
        parameter, or a claim the function's body precedes the write with — `binding` answers
        both — or a `Global` declaration standing directly in the body the write stands in, the
        function's own or the script's, before the statement that holds it. A claim a branch
        holds runs only when the branch does, and a declaration in another body runs when that
        body runs, which the caller cannot order, so neither backs a write. A `Dim` claim backs
        nothing — the option names `Local` and `Global` alone — and a `Local` standing at script
        level backs nothing either, the storage it creates there being unpinned.
        """
        if scope is not None:
            if self.binding(scope, write, name) is Binding.LOCAL:
                return True
            facts = self.local_facts.get(scope)
            first = facts.first_global.get(name) if facts is not None else None
            if first is None:
                return False
            return first <= _top_level_index(scope, write)
        first = self.script_first_global.get(name)
        if first is None:
            return False
        return first <= _script_level_index(write)

    def read_binding(
        self,
        scope: Au3FunctionDeclaration | None,
        read: Node,
        name: str,
    ) -> Binding:
        """
        The storage the read *read* of *name* targets when it stands in *scope*: the whole script
        when `None`, one function's body otherwise. A read before a same-named local-forcing
        declaration in the body sees the global and a read after it the local (probe4 22-23), and
        a function that declares the name `Global` reads the global throughout. A name a `Dim`
        in the function declares forces no storage, so a read of it keeps the global: the
        function created no local the read could see. A parameter read inside the body targets
        the local, but a read inside a parameter default runs before any parameter is bound, so
        it keeps the global — the only storage that could exist where it stands.
        """
        if scope is None:
            return Binding.GLOBAL
        facts = self.local_facts.get(scope)
        if facts is None or name in facts.global_names:
            return Binding.GLOBAL
        if name in facts.parameters:
            if _top_level_index(scope, read) < 0:
                return Binding.GLOBAL
            return Binding.LOCAL
        first = facts.first_local.get(name)
        if first is None:
            return Binding.GLOBAL
        if first <= _top_level_index(scope, read):
            return Binding.LOCAL
        return Binding.GLOBAL

    def local_precedes_read(
        self,
        scope: Au3FunctionDeclaration | None,
        read: Node,
        name: str,
    ) -> bool:
        """
        Whether the read *read* of *name* in *scope* targets a local that exists when the read
        runs and whose claim strictly precedes it. `read_binding` counts the statement that
        claims a local as covering a read inside it, but the local does not exist while that
        statement's own initializer runs — `Local $x = $x` is an interpreter refusal (probe9g)
        where the dynamic read of the same name answers `""` — so a caller that replaces a
        dynamic read with the plain one asks this instead. A parameter needs no claim: it exists
        once the function's parameters are bound, and the defaults that fill them run before any
        is, so a read inside a parameter default — of the very parameter being defaulted no less
        — targets nothing the plain read may name and counts only inside the body.
        """
        if scope is None:
            return False
        facts = self.local_facts.get(scope)
        if facts is None or name in facts.global_names:
            return False
        if name in facts.parameters:
            return _top_level_index(scope, read) >= 0
        first = facts.first_local.get(name)
        if first is None:
            return False
        return first < _top_level_index(scope, read)

    def read_storages(
        self,
        scope: Au3FunctionDeclaration | None,
        occurrence: Au3Variable,
        name: str,
    ) -> frozenset[Binding]:
        """
        The storages the occurrence *occurrence* of *name* standing in *scope* may read: the
        whole script when `None`, one function's body otherwise. A write occurrence resolves
        through `binding` and a pure read through `read_binding`, each occurrence by exactly one
        call — the two do not coincide everywhere, a `For` loop's variable being local to its own
        write and global to a read inside a function declaring the name `Global`, so the
        classifier never compares them. A resolved global reads the global alone, except where
        the scope claims the name `Static`: a static's local survives the call that created it,
        so a read the claim does not cover — one standing before it — may still reach the local
        on a later call, and both storages stay protected. A resolved local reads the local alone
        only where its claim strictly precedes the occurrence; where the claim shares the
        occurrence's top-level statement, the local does not exist while that statement's own
        initializer or loop header runs, so the read may reach the global as well and both
        storages stay protected. A write occurrence that proves nothing reads the global or the
        implicit local its own write creates.
        """
        if ast.is_write_occurrence(occurrence):
            statement = ast.owning_statement(occurrence)
            assert statement is not None
            resolved = self.binding(scope, statement, name)
        else:
            resolved = self.read_binding(scope, occurrence, name)
        if resolved is Binding.GLOBAL:
            facts = self.local_facts.get(scope) if scope is not None else None
            if facts is not None and name in facts.static_names:
                return frozenset({Binding.LOCAL, Binding.GLOBAL})
            return frozenset({Binding.GLOBAL})
        if resolved is Binding.LOCAL and self.local_precedes_read(scope, occurrence, name):
            return frozenset({Binding.LOCAL})
        return frozenset({Binding.LOCAL, Binding.GLOBAL})

    def may_bind_local(
        self,
        scope: Au3FunctionDeclaration | None,
        occurrence: Node,
        name: str,
    ) -> bool:
        """
        Whether the occurrence *occurrence* of *name* may bind a local of *scope*: the name is a
        parameter of the function, or a local-forcing declaration or `For`/`For…In` claim of it
        stands in a top-level statement at or before the occurrence's. A declaration inside a
        branch creates its local the moment the branch runs it, and a loop's second iteration
        sees one an earlier iteration created, so the occurrence and the claim sharing their
        top-level statement counts as preceding it. A read that provably precedes every claim —
        `read_binding` answering `Binding.GLOBAL` with no claim behind it — is one no local can
        reach. An occurrence inside a parameter default may bind no local at all: no parameter
        is bound and no body statement has run where it stands.
        """
        if scope is None:
            return False
        facts = self.local_facts.get(scope)
        if facts is None or name in facts.global_names:
            return False
        if name in facts.parameters:
            return _top_level_index(scope, occurrence) >= 0
        index = _top_level_index(scope, occurrence)
        return any(position <= index for position in facts.local_positions.get(name, ()))