Functions
None	_emit_error (str source_filename, int\|str line, str message)
None	reject_unsupported_threading_usage (ast.AST tree, str source_filename)
tuple[set[str], set[str]]	_collect_thread_aliases (ast.AST tree)
bool	_is_thread_constructor (ast.Call call_node, set[str] module_aliases, set[str] thread_aliases)
bool	_is_thread_construction_with_target_kw (ast.expr\|None value, set[str] module_aliases, set[str] thread_aliases)
bool	_base_is_thread (ast.expr base, set[str] module_aliases, set[str] thread_aliases)
dict[str, ast.ClassDef]	_collect_thread_subclass_defs (ast.AST tree, set[str] module_aliases, set[str] thread_aliases)
bool	_is_subclass_constructor (ast.Call call_node, set[str] subclass_names)
tuple[str\|None, ast.expr\|None]	_extract_name_binding (ast.stmt stmt)
str	_call_class_name (ast.Call call_node)
bool	_is_super_call_expr (ast.AST node)
bool	_is_super_init_call_stmt (ast.stmt stmt)
str\|None	_target_name_chain (ast.AST node)
list[list[ast.stmt]]	_scope_bodies (ast.Module tree)
list[ast.stmt]	_collect_scope_statements (list[ast.stmt] body)
set[str]	_declared_outer_names (list[ast.stmt] body)
Iterator[ast.AST]	_iter_scope_nodes (list[ast.stmt] body)
Iterator[list[ast.stmt]]	_iter_scope_stmt_lists (list[ast.stmt] body)
dict[int, ast.AST]	_parent_map (ast.AST tree)
bool	_inside_loop_within_scope (ast.AST node, dict[int, ast.AST] parents)
dict[str, int]	_scope_name_assign_counts (list[ast.stmt] body)
None	validate_threading_thread_usage (ast.Module tree, str source_filename)
str\|None	_thread_method_receiver (ast.AST node, set[str] thread_var_names, str method)
tuple[dict[int, dict[str, tuple[int, ast.Call]]], int]	_collect_thread_var_sites (ast.Module tree, set[str] module_aliases, set[str] thread_aliases, int starting_id=0)
tuple[dict[str, tuple[int, ast.Call]], int]	_collect_subclass_sites (ast.Module tree, set[str] subclass_names, int starting_id)
tuple[dict[int, dict[str, tuple[int, ast.Call]]], int]	_collect_func_subclass_sites (ast.Module tree, set[str] subclass_names, int starting_id)
None	_hoist_func_subclass_binding (list[ast.stmt] scope_body, str var_name, str obj_name)
tuple[ast.expr, list[ast.expr]]	_thread_call_keywords (ast.Call call_node)
ast.expr	_build_target_call (ast.expr target_expr, int site_id, int n_args)
ast.FunctionDef	_build_trampoline (int site_id, ast.expr target_expr, int n_args)
ast.FunctionDef	_build_subclass_trampoline (int site_id, str var_name)
ast.AnnAssign	_build_obj_declaration (str obj_name, str class_name)
ast.Assign	_build_tid_declaration (int site_id)
None	_strip_thread_inheritance (ast.ClassDef class_node, set[str] module_aliases, set[str] thread_aliases)
ast.stmt	_build_arg_declaration (int site_id, int arg_index, ast.expr arg_value)
ast.Assign	_build_arg_assignment (int site_id, int arg_index, ast.expr value)
ast.Call	_build_bare_thread_call (ast.Call original_call)
list[ast.stmt]	_build_start_statements (int site_id)
ast.Expr	_build_join_call (int site_id)
list[ast.stmt]	_rewrite_construction_stmt (ast.stmt stmt, ast.Call call_node, int site_id)
None	lower_threading_thread_usage (ast.Module tree, str source_filename)
int\|None	_find_binding_stmt_index (ast.Module tree, ast.Call call_node)
None	_rewrite_body_in_place (list[ast.stmt] body, dict[str, tuple[int, ast.Call]] scope_sites, set[str] module_aliases, set[str] thread_aliases)
list[ast.stmt]\|None	_try_rewrite_statement (ast.stmt stmt, dict[str, tuple[int, ast.Call]] scope_sites, set[str] module_aliases, set[str] thread_aliases)

Variables
	SUPPORTED_THREADING_SYMBOLS = frozenset({"Lock", "Thread"})
	UNSUPPORTED_THREAD_KWARGS = frozenset({"daemon", "name", "kwargs", "group"})
	THREAD_OVERRIDE_REJECTED_METHODS = frozenset({"start", "join"})
tuple	_SCOPE_NODES
	lineno
	body

Detailed Description

Threading validation and lowering helpers for the Python parser frontend.

Function Documentation

◆ _base_is_thread()

bool parser.threading_lowering._base_is_thread	(	ast.expr	base,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Return ``True`` iff ``base`` resolves to ``threading.Thread``.

Recognises both ``threading.Thread`` (qualified through an
``import threading [as X]`` alias) and the bare name when it
came in via ``from threading import Thread [as X]``.

◆ _build_arg_assignment()

ast.Assign parser.threading_lowering._build_arg_assignment	(	int	site_id,
		int	arg_index,
		ast.expr	value )

protected

Return ``__pythread_arg_<N>_<i> = <value>`` as an AST node.

The deep-copied ``value`` is the construction-site expression; the
assignment runs in the user's calling frame just before the
rewritten bare ``Thread()`` construction so module globals carry
the construction-time value into the spawned thread.

◆ _build_arg_declaration()

ast.stmt parser.threading_lowering._build_arg_declaration	(	int	site_id,
		int	arg_index,
		ast.expr	arg_value )

protected

Return a module-top declaration for ``__pythread_arg_<N>_<i>``.

A plain ``Assign`` or an ``AnnAssign`` with a non-null ``value`` is
required so the ESBMC Python frontend creates a *module-level*
binding: an annotation-only declaration silently degrades to a
function-local at the first construction-site write, and the
spawned trampoline would then read an uninitialised global rather
than the user-supplied argument.

The declared shape is chosen by ``arg_value`` (the construction-
site expression, treated read-only):

  * Numeric / string constants — emit ``= <zero-of-that-kind>`` so
    the symbol's inferred type matches the construction-site rebind
    and the trampoline call site type-checks against the target's
    parameter.
  * Anything else (Name references, attribute chains, calls,
    list/dict/set literals, ``None``) — emit ``: object = None``.
    ``object`` lowers to ``any_type()`` (``void *``) in the Python
    frontend, so a class-instance arg carrying a struct pointer is
    forwarded to the trampoline call site without the
    int-degradation that ``= 0`` would force.

◆ _build_bare_thread_call()

ast.Call parser.threading_lowering._build_bare_thread_call ( ast.Call original_call )

protected

Return a no-kwargs ``Thread()`` call mirroring ``original_call.func``.

Preserves the original constructor reference (``threading.Thread``
vs ``MyThread``) so the Python frontend's class resolution still
finds the skeleton, but strips the ``target=`` / ``args=`` keywords
so the skeleton's zero-arg ``__init__`` accepts the call.

◆ _build_join_call()

ast.Expr parser.threading_lowering._build_join_call ( int site_id )

protected

Return ``__pyt_join(__pythread_tid_<N>)`` as a statement.

◆ _build_obj_declaration()

ast.AnnAssign parser.threading_lowering._build_obj_declaration	(	str	obj_name,
		str	class_name )

protected

Return ``<obj_name>: <class_name> = None`` as a module-top declaration.

The ``= None`` is load-bearing. A value-less annotation gives the
symbol the *value* type ``<class_name>``, and a value-typed module
global rebound from a function is not observed by the spawned
thread — it reads the pre-assignment contents. Initialising to
``None`` types the symbol as ``<class_name> *`` instead, matching
what a module-scope ``<name> = <class_name>(...)`` produces, and the
rebind is then visible across threads. Constructing here instead
would run the user's ``__init__`` a second time with made-up
arguments.

◆ _build_start_statements()

list[ast.stmt] parser.threading_lowering._build_start_statements ( int site_id )

protected

Return the atomic spawn-and-init sequence replacing ``t.start()``.

Emits, in order:

  1. ``global __pythread_tid_<N>`` — binds the tid assignment to
     the module-level slot the prelude declared, even when
     ``t.start()`` is called inside a function scope.
  2. ``__ESBMC_atomic_begin()``.
  3. ``__pythread_tid_<N> = __ESBMC_spawn_thread(__pythread_trampoline_<N>)``.
  4. ``__pyt_init_tid(__pythread_tid_<N>)``.
  5. ``__ESBMC_atomic_end()``.

The atomic block is essential: without it, the spawned trampoline
can run (and reach ``__pyt_terminate``, setting
``pthread_thread_ended[tid] = 1``) between the spawn and the init,
after which ``__pyt_init_tid`` would reset the ended flag back to
0 and the subsequent ``__pyt_join`` would deadlock-falsely.

◆ _build_subclass_trampoline()

ast.FunctionDef parser.threading_lowering._build_subclass_trampoline	(	int	site_id,
		str	var_name )

protected

Synthesise the trampoline for a Thread subclass instance bound to ``var_name``.

Body is::

    global <var_name>
    <var_name>.run()
    __pyt_terminate()

The ``global`` lets the trampoline read the user's module-level
instance binding (validator C2 guarantees module scope). The
trampoline must be inserted *after* the user's ``<var_name> = X(...)``
statement so the Python frontend resolves the type of ``<var_name>``
by the time it sees the trampoline body.

◆ _build_target_call()

ast.expr parser.threading_lowering._build_target_call	(	ast.expr	target_expr,
		int	site_id,
		int	n_args )

protected

Return an AST for ``<target>(<arg0>, ..., <argN-1>)``.

``<argI>`` is the module-level global ``__pythread_arg_<site>_<i>``
populated at construction time. ``<target>`` is a deep copy of the
original ``target=`` chain so the trampoline calls the same function
the user named.

◆ _build_tid_declaration()

ast.Assign parser.threading_lowering._build_tid_declaration ( int site_id )

protected

Return ``__pythread_tid_<N> = 0`` as a module-top assignment.

◆ _build_trampoline()

ast.FunctionDef parser.threading_lowering._build_trampoline	(	int	site_id,
		ast.expr	target_expr,
		int	n_args )

protected

Synthesise the per-site Python trampoline ``FunctionDef``.

Body is::

    target(__pythread_arg_<N>_0, ..., __pythread_arg_<N>_n-1)
    __pyt_terminate()

The trampoline is invoked by ``__ESBMC_spawn_thread`` as a spawned
thread; ``__pyt_terminate`` marks the thread ended so ``__pyt_join``
can observe completion. The leading ``global`` declaration is what
lets the trampoline read the construction-site arg globals — without
it Python's name resolution treats every ``__pythread_arg_<N>_<i>``
as a local lookup, which the ESBMC frontend rejects with an
undefined-variable error.

◆ _call_class_name()

str parser.threading_lowering._call_class_name ( ast.Call call_node )

protected

Return the class name from a ``Name(...)`` call for error messages.

◆ _collect_func_subclass_sites()

tuple[dict[int, dict[str, tuple[int, ast.Call]]], int] parser.threading_lowering._collect_func_subclass_sites	(	ast.Module	tree,
		set[str]	subclass_names,
		int	starting_id )

protected

Return ``({id(scope_body): {var_name: (site_id, call_node)}}, next_id)``.

The function-scope counterpart of :func:`_collect_subclass_sites`.
Module-top bindings are excluded — they keep the simpler lowering
that reads the user's own global — so every site returned here needs
the hoist performed by :func:`_hoist_func_subclass_binding`.

◆ _collect_scope_statements()

list[ast.stmt] parser.threading_lowering._collect_scope_statements ( list[ast.stmt] body )

protected

Yield every statement in a scope, descending control-flow constructs.

Descends into ``If``/``For``/``While``/``With``/``Try`` and their
``orelse``/``finalbody``/handler bodies (those share the enclosing
scope's name bindings) but stops at nested ``FunctionDef`` /
``AsyncFunctionDef`` / ``ClassDef`` — those introduce new scopes that
the caller already handles via :func:`_scope_bodies`.

◆ _collect_subclass_sites()

tuple[dict[str, tuple[int, ast.Call]], int] parser.threading_lowering._collect_subclass_sites	(	ast.Module	tree,
		set[str]	subclass_names,
		int	starting_id )

protected

Return ``({var_name: (site_id, call_node)}, next_id)`` for module-top subclass bindings.

Validator C2 guarantees subclass instance bindings are module-scope
only, so we walk ``tree.body`` (not the per-scope helper) and the
returned map is flat — every entry is a module-global var name
visible to every other scope. Site ids continue from
``starting_id`` so target= and subclass sites share one id space
and the generated trampoline / tid names never collide.

◆ _collect_thread_aliases()

tuple[set[str], set[str]] parser.threading_lowering._collect_thread_aliases ( ast.AST tree )

protected

Return ``(module_aliases, thread_aliases)`` for the ``threading`` module.

``module_aliases`` are the names bound by ``import threading [as X]``;
``thread_aliases`` are the names bound by
``from threading import Thread [as X]``. The two sets disambiguate
qualified (``X.Thread``) from bare (``X``) references at every Thread
construction site.

◆ _collect_thread_subclass_defs()

dict[str, ast.ClassDef] parser.threading_lowering._collect_thread_subclass_defs	(	ast.AST	tree,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Return ``{class_name: ClassDef}`` for module-top direct subclasses.

Only direct subclasses (``class X(threading.Thread)``) at module
scope are picked up. Transitive subclasses (``class B(A)`` where
``A`` is itself a Thread subclass) and nested subclass defs are out
of MVP scope; the validator's C1 rule rejects nested defs and
transitive subclassing fails the constructor-recognition check at
the call site.

◆ _collect_thread_var_sites()

tuple[dict[int, dict[str, tuple[int, ast.Call]]], int] parser.threading_lowering._collect_thread_var_sites	(	ast.Module	tree,
		set[str]	module_aliases,
		set[str]	thread_aliases,
		int	starting_id = 0 )

protected

Return ``({id(scope_body): {var_name: (site_id, construction_call)}}, next_id)``.

Each scope (module top, each function body) gets its own inner map
because the validator's single-definition check is per-scope: the
same name ``t`` may legally bind a Thread in two distinct function
scopes, and each binding must allocate its own site id (otherwise
the second scope's ``t.start()`` would silently reuse the first
scope's trampoline). Site ids are assigned in deterministic source
order so the generated globals / trampolines stay stable across
parser runs.

``starting_id`` lets the caller chain this collector with the
subclass-site collector under one continuous id space.

◆ _declared_outer_names()

set[str] parser.threading_lowering._declared_outer_names ( list[ast.stmt] body )

protected

Return names bound outside a scope via ``global``/``nonlocal``, nested scopes included.

Nested declarations count. ``Global``/``Nonlocal`` hold their names
as plain strings, so the hoist's ``Name`` rename cannot rewrite
them: an inner ``nonlocal w`` would survive pointing at a name the
rename has just retired.

◆ _emit_error()

None parser.threading_lowering._emit_error	(	str	source_filename,
		int \| str	line,
		str	message )

protected

Emit a parser-stage threading error and abort.

◆ _extract_name_binding()

tuple[str | None, ast.expr | None] parser.threading_lowering._extract_name_binding ( ast.stmt stmt )

protected

Return ``(target_name, value)`` for ``Name = value`` / ``Name: T = value``.

Returns ``(None, None)`` for tuple-targets, attribute-targets, augmented
assigns, and any other statement shape. Used wherever we need to ask
"is this a simple single-name binding, and what does it assign?"

◆ _find_binding_stmt_index()

int \| None parser.threading_lowering._find_binding_stmt_index	(	ast.Module	tree,
		ast.Call	call_node )

protected

Return the module-top index of the Assign/AnnAssign whose value is ``call_node``.

◆ _hoist_func_subclass_binding()

None parser.threading_lowering._hoist_func_subclass_binding	(	list[ast.stmt]	scope_body,
		str	var_name,
		str	obj_name )

protected

Rename a function-local subclass instance to the module global ``obj_name``.

The spawned trampoline runs at module scope and can only reach the
instance through a global, so the local binding is renamed rather
than copied: one object, no aliasing question about whether the
frontend assigns instances by reference.

Both passes stop at nested scope boundaries — an inner ``def``'s
parameter or local of the same name is a different variable, and
renaming it would either orphan the parameter or redirect the inner
binding at this scope's thread object.

Annotations on the target are dropped: a name cannot be both
annotated and ``global``, and re-annotating inside the function
would restore the value type that :func:`_build_obj_declaration`
exists to avoid.

◆ _inside_loop_within_scope()

bool parser.threading_lowering._inside_loop_within_scope	(	ast.AST	node,
		dict[int, ast.AST]	parents )

protected

Return ``True`` iff ``node`` is inside a loop body in its own scope.

Walks the ``parents`` chain rooted at ``node`` and stops at a scope
boundary (``FunctionDef``/``AsyncFunctionDef``/``Lambda``/``ClassDef``
/``Module``). Loop ancestors are ``For``/``AsyncFor``/``While`` plus
the comprehension forms (``ListComp``/``SetComp``/``DictComp``/
``GeneratorExp``) — each re-evaluates the node per iteration, which
the per-site converter state cannot represent.

◆ _is_subclass_constructor()

bool parser.threading_lowering._is_subclass_constructor	(	ast.Call	call_node,
		set[str]	subclass_names )

protected

Return ``True`` iff ``call_node`` constructs a tracked Thread subclass.

◆ _is_super_call_expr()

bool parser.threading_lowering._is_super_call_expr ( ast.AST node )

protected

Return ``True`` iff ``node`` is a call whose function is ``super().X``.

Matches the AST shape ``Call(func=Attribute(value=Call(func=Name('super'))))``
for any attribute. Used to enumerate every super-method call inside
a subclass body so the validator can refuse the ones we cannot
soundly strip.

◆ _is_super_init_call_stmt()

bool parser.threading_lowering._is_super_init_call_stmt ( ast.stmt stmt )

protected

Return ``True`` iff ``stmt`` is ``super().__init__()`` at statement level.

Strict: zero positional args, zero keywords, both for the
``super(...)`` call (must be bare ``super()``) and the
``.__init__(...)`` call. Anything richer falls through to the
validator, which refuses non-trivial super calls.

◆ _is_thread_construction_with_target_kw()

bool parser.threading_lowering._is_thread_construction_with_target_kw	(	ast.expr \| None	value,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Return ``True`` iff ``value`` is a real ``Thread(target=...)`` call.

Used by the threading-rewrite path to recognise the construction
arm: a ``threading.Thread`` call with no positional arguments and a
``target=`` keyword. A user subclass whose ``__init__`` accepts a
parameter named ``target`` is excluded by the ``_is_thread_constructor``
check.

◆ _is_thread_constructor()

bool parser.threading_lowering._is_thread_constructor	(	ast.Call	call_node,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Return ``True`` iff ``call_node`` constructs ``threading.Thread``.

Recognises both ``threading.Thread(...)`` (qualified through an
``import threading [as X]`` alias) and ``Thread(...)`` (bare, through
a ``from threading import Thread [as X]`` alias).

◆ _iter_scope_nodes()

Iterator[ast.AST] parser.threading_lowering._iter_scope_nodes ( list[ast.stmt] body )

protected

Yield every node reachable from ``body`` without crossing a scope boundary.

◆ _iter_scope_stmt_lists()

Iterator[list[ast.stmt]] parser.threading_lowering._iter_scope_stmt_lists ( list[ast.stmt] body )

protected

Yield ``body`` and every statement list nested below it in the same scope.

◆ _parent_map()

dict[int, ast.AST] parser.threading_lowering._parent_map ( ast.AST tree )

protected

Build a child-to-parent map for ``tree`` keyed by ``id(node)``.

``ast`` does not expose parent pointers; the validator needs them to
answer "is this Thread construction lexically inside a loop body
within its own scope" without walking the whole tree per call site.

◆ _rewrite_body_in_place()

None parser.threading_lowering._rewrite_body_in_place	(	list[ast.stmt]	body,
		dict[str, tuple[int, ast.Call]]	scope_sites,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Walk ``body`` recursively, rewriting this scope's Thread sites.

``scope_sites`` is the inner map from :func:`_collect_thread_var_sites`
for *this* scope only — sibling scopes are visited separately so
their Thread variables with the same name resolve to distinct site
ids. Descends into control-flow constructs (``If``/``For``/``While``
/``With``/``Try``) but not into nested defs (those are independent
scopes already enrolled in the outer site map).

``module_aliases`` / ``thread_aliases`` are forwarded so the
construction-rewrite predicate in :func:`_try_rewrite_statement`
can require a real ``threading.Thread`` call rather than misfiring
on a subclass constructor whose own ``__init__`` happens to take a
``target=`` keyword argument.

◆ _rewrite_construction_stmt()

list[ast.stmt] parser.threading_lowering._rewrite_construction_stmt	(	ast.stmt	stmt,
		ast.Call	call_node,
		int	site_id )

protected

Return the replacement statements for a Thread construction.

The original ``t = Thread(target=f, args=(x, y))`` becomes::

    global __pythread_arg_<N>_0, __pythread_arg_<N>_1
    __pythread_arg_<N>_0 = x
    __pythread_arg_<N>_1 = y
    t = Thread()

The leading ``global`` ensures the arg writes bind to the module-
level placeholders the prelude declared, not to function locals
that the spawned trampoline could never see. (For module-scope
constructions the ``global`` is redundant but harmless.) The spawn
happens later at ``t.start()``, by which time the args are visible
to the spawned trampoline (cross-thread visibility follows from
the spawn happens-before edge).

◆ _scope_bodies()

list[list[ast.stmt]] parser.threading_lowering._scope_bodies ( ast.Module tree )

protected

Return the statement list of every Python scope in ``tree``.

A "scope" is a region with its own local-name binding rules: the
module top level and the body of every (sync or async) function
definition. Class bodies and lambdas are intentionally excluded:
Thread variables cannot meaningfully live in either under the MVP.

◆ _scope_name_assign_counts()

dict[str, int] parser.threading_lowering._scope_name_assign_counts ( list[ast.stmt] body )

protected

Count direct Name-target value bindings per name within a single scope.

Counts every ``Assign``, ``AnnAssign`` *with* a value, and ``AugAssign``
whose target is a plain ``Name``, descending into control-flow bodies
but not into nested defs. ``AnnAssign`` without a value (e.g.
``t: Thread``) is intentionally skipped: Python evaluates the
annotation but does not bind a value, so it is not a definition.

The result drives the single-definition check that lets the converter
bind each Thread variable to a unique site id without runtime
resolution. Rebinds via ``def t(...)``, ``class t``, ``import t``,
``for t in ...``, ``with ... as t``, and walrus expressions are not
counted — those are acceptable MVP gaps documented in
:func:`validate_threading_thread_usage`.

◆ _strip_thread_inheritance()

None parser.threading_lowering._strip_thread_inheritance	(	ast.ClassDef	class_node,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Remove ``threading.Thread`` from ``class_node.bases`` and neuter ``super().__init__()``.

Two in-place transforms required to make the user's subclass
survive the Python frontend's class converter:

  * Strip every base that resolves to ``threading.Thread``. The
    converter cannot resolve the operational-model ``Thread``
    skeleton as a base (probe: ``nlohmann::json`` key-not-found
    assertion). After stripping, ``class X(threading.Thread)``
    becomes ``class X:`` (implicit ``object`` base).
  * Replace any bare ``super().__init__()`` statement inside
    ``__init__`` with ``Pass``. The converter cannot resolve
    ``super().__init__()`` on an implicit ``object`` base either
    (probe: ``_init_undefined`` / ``migrate expr failed``). The
    validator (C5) refuses every other ``super(...)`` shape, so
    we only need to neutralise the bare-init shape here.

◆ _target_name_chain()

str | None parser.threading_lowering._target_name_chain ( ast.AST node )

protected

Return the dotted form of a ``Name``/``Attribute`` chain, else ``None``.

Used to enforce the MVP rule that ``Thread(target=...)`` resolves to
a statically-known function. ``Name('f')`` returns ``"f"``;
``Attribute(Name('m'), 'f')`` returns ``"m.f"``; anything else
(lambdas, calls, subscripts, arbitrary expressions) returns ``None``.

◆ _thread_call_keywords()

tuple[ast.expr, list[ast.expr]] parser.threading_lowering._thread_call_keywords ( ast.Call call_node )

protected

Return ``(target_expr, list_of_arg_exprs)`` for a validated Thread call.

``args=`` (when omitted) yields an empty arg list. The validator has
already proven ``target=`` is present and ``args=`` (if present) is
a tuple literal, so this function only does the lookup.

◆ _thread_method_receiver()

str \| None parser.threading_lowering._thread_method_receiver	(	ast.AST	node,
		set[str]	thread_var_names,
		str	method )

protected

Return the receiver var name iff ``node`` is ``var.<method>()`` on a tracked Thread.

Recognises ``Name(var).method()`` shape only; attribute-chain
receivers (``obj.t.start()``) are out of MVP scope. Returning the
name directly (rather than a bool) lets the caller skip a separate
type-narrowing pass on ``call.func``.

◆ _try_rewrite_statement()

list[ast.stmt] \| None parser.threading_lowering._try_rewrite_statement	(	ast.stmt	stmt,
		dict[str, tuple[int, ast.Call]]	scope_sites,
		set[str]	module_aliases,
		set[str]	thread_aliases )

protected

Rewrite a single Thread construction / start / join statement.

Returns ``None`` if ``stmt`` is unrelated to threading; otherwise
returns the replacement statement list. ``scope_sites`` is the
per-scope ``{var_name: (site_id, call_node)}`` map.

The construction-rewrite arm requires the call to be a real
``threading.Thread`` constructor (via :func:`_is_thread_constructor`)
— *not* merely "has a ``target=`` keyword". A user subclass whose
``__init__`` accepts a parameter named ``target`` would otherwise
have its keyword silently dropped by :func:`_build_bare_thread_call`,
a soundness defect.

◆ lower_threading_thread_usage()

None parser.threading_lowering.lower_threading_thread_usage	(	ast.Module	tree,
		str	source_filename )

Rewrite ``threading.Thread`` usage into pthread-backed intrinsics.

Runs after :func:`validate_threading_thread_usage` has refused every
unsupported shape. For each accepted ``Thread(...)`` construction
site:

  * allocate a unique site id;
  * emit module-level globals ``__pythread_arg_<N>_<i>`` for each
    ``args=`` element and a ``__pythread_tid_<N>`` slot for the
    spawned thread's id;
  * emit a module-level trampoline ``__pythread_trampoline_<N>``
    whose body calls the user-supplied target with the per-site
    arg globals, then calls ``__pyt_terminate``;
  * rewrite the construction statement to populate the arg globals
    and bind the user's name to a bare ``Thread()``;
  * rewrite every ``t.start()`` call to an atomic block that
    captures the spawned tid into ``__pythread_tid_<N>`` and calls
    ``__pyt_init_tid``, then rewrite every ``t.join()`` call to
    ``__pyt_join(__pythread_tid_<N>)``.

Producing module-level globals (rather than function-locals
captured by closure) was the fix for #4571's three soundness
defects: it gives the spawned trampoline an unambiguous reader of
the construction-site values, and ``__pyt_join`` provides
the real synchronisation edge symex's interleaving search needs.

◆ reject_unsupported_threading_usage()

None parser.threading_lowering.reject_unsupported_threading_usage	(	ast.AST	tree,
		str	source_filename )

Refuse to compile programs using unsupported ``threading`` names.

Walks the AST for usages of names from the ``threading`` module that
ESBMC does not yet model and exits with a clear error rather than
silently emitting a weaker abstraction. The supported set is
``SUPPORTED_THREADING_SYMBOLS``. Detects three import shapes:

  ``import threading``         → ``threading.<X>`` attribute access
  ``import threading as t``    → ``t.<X>`` attribute access
  ``from threading import X``  → bare ``X`` reference

``from threading import *`` is refused outright because static name
resolution would require importing the real ``threading`` module.

◆ validate_threading_thread_usage()

None parser.threading_lowering.validate_threading_thread_usage	(	ast.Module	tree,
		str	source_filename )

Refuse ``threading.Thread`` usage outside the MVP-supported shape.

ESBMC's Thread lowering (tracked in #4568) is intentionally narrow so
no concurrency model can be silently weakened. This pass refuses,
with a precise error message and a non-zero exit, every construct
outside that shape:

  * subclassing ``threading.Thread``;
  * positional arguments to ``Thread()`` (real signature is
    ``Thread(group, target, name, args, ...)`` and ESBMC only
    accepts the keyword form);
  * ``**kwargs`` splats and ``daemon=``/``name=``/``kwargs=``/
    ``group=`` keyword arguments;
  * ``Thread()`` constructions with no ``target=`` keyword;
  * ``target=`` values that are not a ``Name`` or dotted attribute
    chain (lambdas, calls, runtime variables);
  * ``args=`` values that are not a tuple literal (lists, sets,
    runtime variables);
  * ``Thread()`` constructions lexically inside a loop body within
    their own scope (per-site converter state would be aliased);
  * reassignment of a name that already binds a ``Thread`` instance
    within the same scope (breaks the single-site binding the
    ``.start()`` / ``.join()`` lowering relies on).

Structurally-valid ``Thread()`` constructions are passed through to
:func:`lower_threading_thread_usage`, which rewrites them into
module-level globals, a per-site Python trampoline, and calls to
the C intrinsics ``__ESBMC_spawn_thread`` / ``__pyt_join`` so
symex's interleaving search can explore real concurrent behaviour.

Known gaps (acceptable for the MVP — soundness is preserved because
each is either over-rejected by the structural fallback or has no
silent failure path):

  * a ``target=`` bound to a runtime variable holding a callable is
    syntactically a ``Name`` and passes ``_target_name_chain`` —
    AST-only validation cannot distinguish a function name from a
    variable-bound callable without a name-resolution pass. The
    lowering generates a direct call by name; a mismatch surfaces
    as an undefined-symbol error at conversion time, not silent
    weakening of the concurrency model;
  * tuple-target assigns (``a, b = Thread(...), Thread(...)``) and
    walrus-bound Threads are not counted by the reassignment check;
  * rebinds via ``def``/``class``/``import``/``for``-target/
    ``with``-target are not counted by the reassignment check;
  * Thread-subclass name collision with a function-local class of
    the same name — the C2 walk matches subclass constructors by
    bare ``func.id``, so a function-local ``class Worker:`` that
    shadows the module-top ``class Worker(threading.Thread)`` has
    its ``Worker(...)`` calls wrongly refused. This is a false
    positive (valid code rejected), not a false verdict; the user
    can rename the local class. Resolving it would require a
    name-resolution pass.

Variable Documentation

◆ _SCOPE_NODES

tuple parser.threading_lowering._SCOPE_NODES

protected

Initial value:

=  (
    ast.FunctionDef,
    ast.AsyncFunctionDef,
    ast.ClassDef,
    ast.Lambda,
    ast.ListComp,
    ast.SetComp,
    ast.DictComp,
    ast.GeneratorExp,
)

◆ body

parser.threading_lowering.body

◆ lineno

parser.threading_lowering.lineno

◆ SUPPORTED_THREADING_SYMBOLS

parser.threading_lowering.SUPPORTED_THREADING_SYMBOLS = frozenset({"Lock", "Thread"})

◆ THREAD_OVERRIDE_REJECTED_METHODS

parser.threading_lowering.THREAD_OVERRIDE_REJECTED_METHODS = frozenset({"start", "join"})

◆ UNSUPPORTED_THREAD_KWARGS

parser.threading_lowering.UNSUPPORTED_THREAD_KWARGS = frozenset({"daemon", "name", "kwargs", "group"})

Functions

Variables

Detailed Description

Function Documentation

◆ _base_is_thread()

◆ _build_arg_assignment()

◆ _build_arg_declaration()

◆ _build_bare_thread_call()

◆ _build_join_call()

◆ _build_obj_declaration()

◆ _build_start_statements()

◆ _build_subclass_trampoline()

◆ _build_target_call()

◆ _build_tid_declaration()

◆ _build_trampoline()

◆ _call_class_name()

◆ _collect_func_subclass_sites()

◆ _collect_scope_statements()

◆ _collect_subclass_sites()

◆ _collect_thread_aliases()

◆ _collect_thread_subclass_defs()

◆ _collect_thread_var_sites()

◆ _declared_outer_names()

◆ _emit_error()

◆ _extract_name_binding()

◆ _find_binding_stmt_index()

◆ _hoist_func_subclass_binding()

◆ _inside_loop_within_scope()

◆ _is_subclass_constructor()

◆ _is_super_call_expr()

◆ _is_super_init_call_stmt()

◆ _is_thread_construction_with_target_kw()

◆ _is_thread_constructor()

◆ _iter_scope_nodes()

◆ _iter_scope_stmt_lists()

◆ _parent_map()

◆ _rewrite_body_in_place()

◆ _rewrite_construction_stmt()

◆ _scope_bodies()

◆ _scope_name_assign_counts()

◆ _strip_thread_inheritance()

◆ _target_name_chain()

◆ _thread_call_keywords()

◆ _thread_method_receiver()

◆ _try_rewrite_statement()

◆ lower_threading_thread_usage()

◆ reject_unsupported_threading_usage()

◆ validate_threading_thread_usage()

Variable Documentation

◆ _SCOPE_NODES

◆ body

◆ lineno

◆ SUPPORTED_THREADING_SYMBOLS

◆ THREAD_OVERRIDE_REJECTED_METHODS

◆ UNSUPPORTED_THREAD_KWARGS