parser.rewrite_re Namespace Reference

Functions
bool	_is_re_match_call (ast.AST node)
ast.Call	_build_re_helper_call (str helper, ast.expr pat, ast.expr string, list[ast.expr] extra_args)
	_iter_same_scope (ast.AST node)
None	_rewrite_re_calls_in_node (ast.AST node, dict[str, tuple[ast.expr, ast.expr]] bindings)
list[list[ast.stmt]]	_nested_statement_bodies (ast.stmt stmt)
ast.Call|None	_re_call_from_assignment (ast.stmt stmt)
list[tuple[str, ast.Call]]	_collect_walrus_re_bindings (ast.AST node)
list[str]	_names_from (ast.expr target)
	_iter_same_function_scope (ast.AST node)
set[str]	_collect_assigned_names_anywhere (list[ast.stmt] body)
None	_walk_target_names (ast.expr target, list[str] into)
tuple[list[str], list[str]]	_assigned_names_for_re_binding (ast.stmt stmt)
None	_rewrite_re_calls_in_body (list[ast.stmt] body, dict[str, tuple[ast.expr, ast.expr]] parent_bindings)
None	rewrite_re_match_attribute_calls (ast.Module tree)

Variables
	_RE_ENTRY_FUNCS = frozenset({"match", "search", "fullmatch"})
	_RE_MATCH_METHODS = frozenset({"group", "groups", "span"})
dict	_RE_HELPER_BY_METHOD
	_NESTED_BODY_FIELDS

Detailed Description

Rewrite `re.match`-bound Match-method calls into model helper calls.

Function Documentation

_assigned_names_for_re_binding()

tuple[list[str], list[str]] parser.rewrite_re._assigned_names_for_re_binding ( ast.stmt stmt )

protected

Return ``(top_level_names, all_names)`` bound by ``stmt``.

Only ``top_level_names`` (single-Name targets) can hold the result of
an ``re.match`` call directly; ``all_names`` are every Name reassigned
(including tuple-destructure elements) — used to invalidate stale
bindings on a reassignment that does not point at an ``re.match`` call.

_build_re_helper_call()

ast.Call parser.rewrite_re._build_re_helper_call ( str helper, ast.expr pat, ast.expr string, list[ast.expr] extra_args )

protected

Build ``re.<helper>(pat, string, *extra_args)``.

_collect_assigned_names_anywhere()

set[str] parser.rewrite_re._collect_assigned_names_anywhere ( list[ast.stmt] body )

protected

Return every ``Name`` id bound anywhere within ``body``.

Used to invalidate parent-scope bindings after recursing into a
nested branch (if/for/while/with/try/match): a name reassigned
inside the branch must not retain its pre-branch ``re.match`` cache
once control re-joins the outer scope.

_collect_walrus_re_bindings()

list[tuple[str, ast.Call]] parser.rewrite_re._collect_walrus_re_bindings ( ast.AST node )

protected

Find every ``NamedExpr`` whose value is an ``re.match`` call.

Returns ``[(target_name, re_call), ...]`` for ``(m := re.match(p, s))``
occurrences anywhere inside ``node`` (same lexical scope only).

_is_re_match_call()

bool parser.rewrite_re._is_re_match_call ( ast.AST node )

protected

Return True iff ``node`` is ``re.match/search/fullmatch(pat, str)``.

_iter_same_function_scope()

parser.rewrite_re._iter_same_function_scope ( ast.AST node )

protected

Yield ``node`` and every descendant inside the same function scope.

Like :func:`_iter_same_scope` but does *not* stop at compound-statement
body fields, so the visitor sees every assignment in every nested
branch. Still stops at nested function/lambda boundaries.

_iter_same_scope()

parser.rewrite_re._iter_same_scope ( ast.AST node )

protected

Yield ``node`` and every descendant in the same lexical scope.

Stops at nested ``FunctionDef`` / ``AsyncFunctionDef`` / ``Lambda``
boundaries (variables there are local) and at compound-statement body
fields (``If.body``, ``For.body``, ...): those nested statement lists
are processed by :func:`_rewrite_re_calls_in_body` with the bindings
visible at their entry, so visiting them here would use stale
outer-scope bindings and silently rewrite an inner-scope ``m.group``
against the wrong ``(pat, str)`` pair.

_names_from()

list[str] parser.rewrite_re._names_from ( ast.expr target )

protected

Return every ``Name`` id bound by ``target`` (including nested tuples).

_nested_statement_bodies()

list[list[ast.stmt]] parser.rewrite_re._nested_statement_bodies ( ast.stmt stmt )

protected

Return the lists of nested statements inside ``stmt`` for recursion.

_re_call_from_assignment()

ast.Call | None parser.rewrite_re._re_call_from_assignment ( ast.stmt stmt )

protected

Return the ``re.<entry>(...)`` Call node bound by ``stmt``, or None.

Recognises plain assignments (``m = re.match(...)``) and annotated
assignments with a value (``m: ... = re.search(...)``).

_rewrite_re_calls_in_body()

None parser.rewrite_re._rewrite_re_calls_in_body ( list[ast.stmt] body, dict[str, tuple[ast.expr, ast.expr]] parent_bindings )

protected

Rewrite re-match attribute calls inside ``body``.

Walks statements in order, maintaining a {var: (pat, str)} map of
variables bound to an ``re.match/search/fullmatch(pat, str)`` call.
On each statement: first rewrite descendant ``m.group/groups/span``
calls using the bindings visible *before* the statement executes,
then update the bindings based on this statement's assignment, then
recurse into nested bodies with the updated map.

_rewrite_re_calls_in_node()

None parser.rewrite_re._rewrite_re_calls_in_node ( ast.AST node, dict[str, tuple[ast.expr, ast.expr]] bindings )

protected

In-place rewrite of ``m.group/groups/span(...)`` inside ``node``.

Walks every same-scope Call descendant; when the receiver name is in
``bindings`` and the attribute is one of group/groups/span, replaces
the Call in place with a direct call to the corresponding re._<method>
helper. Nested functions/lambdas are not visited here — they are
enrolled separately by :func:`rewrite_re_match_attribute_calls`.

_walk_target_names()

None parser.rewrite_re._walk_target_names ( ast.expr target, list[str] into )

protected

Collect every ``Name`` id bound by ``target`` (handles nested tuples).

rewrite_re_match_attribute_calls()

None parser.rewrite_re.rewrite_re_match_attribute_calls

(

ast.Module

tree

)

Rewrite ``m.group(N)`` / ``m.groups()`` / ``m.span(N)`` into direct
calls to ``re._group/_groups/_span(pat, string, ...)`` when ``m`` was
bound by ``re.match/search/fullmatch(pat, string)``.

CPython returns a Match-or-None object from these entry points; the
ESBMC Python frontend cannot soundly model that without breaking
existing truthiness assertions, so we keep the model boolean and
redirect the Match accessor methods to side-channel helpers in
``models/re.py`` that recompute the result from the original
``(pattern, string)`` pair.

Limitations: the rewriter tracks direct bindings only — aliasing via
``m2 = m`` does not propagate the cached ``(pat, string)``, so
``m2.group(...)`` is left as an unmodelled attribute call. The
converter's existing ``Unsupported function`` diagnostic surfaces this.

Variable Documentation

_NESTED_BODY_FIELDS

parser.rewrite_re._NESTED_BODY_FIELDS

protected

Initial value:

=  frozenset({
    "body",
    "orelse",
    "handlers",
    "finalbody",
    "cases",
})

_RE_ENTRY_FUNCS

parser.rewrite_re._RE_ENTRY_FUNCS = frozenset({"match", "search", "fullmatch"})

protected

_RE_HELPER_BY_METHOD

dict parser.rewrite_re._RE_HELPER_BY_METHOD

protected

Initial value:

=  {
    "group": "_group",
    "groups": "_groups",
    "span": "_span",
}

_RE_MATCH_METHODS

parser.rewrite_re._RE_MATCH_METHODS = frozenset({"group", "groups", "span"})

protected