- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Classes | |
| class | _YieldFromToFor |
| class | _YieldToAppend |
| class | _YieldReplacer |
Public Member Functions | |
| visit_GeneratorExp (self, node) | |
Public Attributes | |
| comprehension_targets | |
| module_name | |
| generator_emitted_init | |
| early_return_generator_funcs | |
| dict_items_vars | |
Protected Member Functions | |
| _resolve_list_literal_iterable (self, iterable_expr) | |
| _rename_shadowing_targets (self, node) | |
| _hoist_shadowed_iter (self, gen_iter, bound_names, node) | |
| _lower_listcomp (self, node) | |
| _isolate_genexp_targets (self, genexp_node) | |
| _prepare_genexp (self, genexp_node) | |
| _combine_comprehension_ifs (self, ifs) | |
| _build_reduction_guard (self, tmp_name, source_node, negated) | |
| _build_genexp_for_body (self, generator, loop_body, guard, source_node) | |
| _finalize_lowered_genexp (self, for_stmt, source_node) | |
| _lower_reduction_genexp (self, genexp_node, reduction_stmt, state) | |
| _lower_any_genexp (self, genexp_node) | |
| _lower_all_genexp (self, genexp_node) | |
| _build_param_assigns (self, param_names, call_args, parent_node) | |
| _apply_yield_replacer (self, body_stmts, replacer_spec, func_name) | |
| _lower_list_gen_call (self, gen_call_node, parent_node) | |
| _has_early_return_before_yield (self, body) | |
| _transform_recursive_generator (self, node) | |
| _inline_generator_for (self, node) | |
| _inline_generator_call_for (self, node) | |
| _find_generator_next_call (self, node) | |
| _scan_generator_consumers (self, node) | |
| _consumers_in_order (self, var, scan, gen_defs) | |
| _collect_loop_yields (self, stmt, yields) | |
| _make_ternary_yield_value (self, stmt, if_val, else_val) | |
| _absorb_if_only_yields (self, if_init, if_yields, post, yields) | |
| _collect_if_yields (self, stmts, i, accum, in_loop) | |
| _collect_yields (self, stmts, in_loop=False) | |
| _make_stop_iteration_raise (self, template_node) | |
| _resolve_next_yield (self, gen_var, func_name) | |
| _inline_next_call (self, targets, func_name, gen_var, template_node) | |
| _lower_listcomp_in_expr (self, expr) | |
| _lower_sorted_with_key_call (self, call_node) | |
| _fold_dict_getitem_key (self, iterable, key_node) | |
| _const_element_value (self, node) | |
| _lower_min_max_with_key_call (self, call_node) | |
| _scan_unobservable_builtin_keys (cls, module_node) | |
| _scan_closed_lambda_bindings (cls, module_node) | |
| _resolve_lambda_key_name (self, key_kw) | |
| _const_scalar_list_literal (self, literal) | |
| _sorted_scan_key_supported (self, key_value, literal) | |
| _scan_key_argument (self, call_node, func_names) | |
| _key_indexes_element (self, key_value) | |
| _is_scan_supported (self, iterable_expr, key_value) | |
| _lower_sorted_key_iterable (self, call_node) | |
| _lower_sorted_key_scan (self, call_node) | |
| _lower_min_max_key_scan (self, call_node) | |
| _eval_const_key_values (self, key_node, elts) | |
| _eval_const_key_value (self, key_node, element) | |
| _eval_key_body (self, node, param, element) | |
| _const_dict_entry (self, node, param, element) | |
| _lower_tuple_sorted_pair_call (self, call_node) | |
| _maybe_rewrite_list_sort_with_key (self, expr_node) | |
| _lower_assert_eq_literal (self, test_node, source_node) | |
| _try_lower_expr_tuple_literal_eq (self, expr_side, tuple_side, source_node) | |
| _is_assert_literal_shape (self, node) | |
| _resolve_known_literal_expr (self, node) | |
| _is_pure_assert_expr (self, node) | |
| _build_assert_literal_checks (self, actual_expr, literal_node, source_node) | |
| _hoist_generator_inits (self, body, template_node) | |
| _get_dict_expr_from_items_call (self, call_node) | |
| _get_items_dict_expr (self, node, wrappers) | |
| _get_dict_view_call (self, node, attr) | |
| _try_transform_items_set_eq (self, set_side, literal_side, source_node) | |
| _try_transform_keys_view_eq (self, view_side, literal_side, source_node) | |
| _try_transform_values_view_eq (self, view_side, literal_side, source_node) | |
| _try_transform_items_list_eq (self, list_side, literal_side, source_node) | |
| _try_transform_list_tuple_eq (self, left_side, literal_side, source_node) | |
Static Protected Member Functions | |
| _select_min_max_index (key_values, is_min) | |
| _unguard_starred_call (call) | |
| _is_recursive_call (func_name, body) | |
| _recursive_calls (func_name, body) | |
| _has_yield (node) | |
| _collect_post (stmts, start) | |
| _use_in_order (first, last, ctx, kind, only_loop) | |
| _dict_getitem_key_receiver (iterable, key_node) | |
| _pack_min_max_key_args (call_node) | |
| _is_scannable_key (key_value) | |
| _scan_key_call (key_value, bind_name, arg_expr) | |
| _inlinable_key_lambda (key_value) | |
| _binds_key (key_value) | |
| _inline_key_lambda (key_value, arg_expr) | |
| _single_key_keyword (call_node, allowed=()) | |
| _keyword_value (call_node, name) | |
| _sorted_reverse (call_node) | |
| _is_bool_constant (node) | |
| _literal_contains_tuple (literal) | |
| _param_subscript_index (node, param) | |
| _apply_builtin (name, value) | |
| _apply_arith (op, left, right) | |
| _const_scalar_value (node) | |
| _all_constants_distinct (elts) | |
| _is_sorted_const_list (elts, *, by="self") | |
Protected Attributes | |
| dict | _gen_next_blacklist |
| _lower_sorted_with_key_call | |
| _lower_sorted_key_scan | |
| _single_return_funcs | |
| _known_literal_values | |
Static Protected Attributes | |
| dict | _BUILTIN_KEY_DUNDERS = {"len": "__len__", "abs": "__abs__"} |
|
protected |
Splice if-branch yields into the parent yields list, including outer post.
|
staticprotected |
Return True iff all elts are ast.Constant with statically distinct hashable values.
|
staticprotected |
|
staticprotected |
|
protected |
Inline a generator body, replacing ``yield val`` via ``_YieldReplacer``. ``replacer_spec`` is ``(target_name, body_dest, template_node)``. Returns the transformed statement list, or ``None`` if the body uses a construct ``_YieldReplacer`` cannot rewrite.
|
staticprotected |
Whether a scan binds its key lambda to a name before applying it.
|
protected |
|
protected |
|
protected |
Build ``param = arg`` assignments used when inlining generator calls.
|
protected |
|
protected |
Process an ``If``. Returns the next index if yields were absorbed, else ``None``. ``accum`` is ``(current_pre, yields)``.
|
protected |
Process a ``While``/``For`` body. Append yields and return ``True`` if any.
|
staticprotected |
Collect stmts[start:] up to (not including) the first yield-containing statement.
|
protected |
Collect yield points from a generator body.
Returns (outer_init, yields) where:
outer_init : top-level statements before the first yield/loop-with-yield
(generator initialisation -- emitted once per generator var).
yields : list of (pre_stmts, yield_val, post_stmts, is_repeating)
pre_stmts : statements inside the innermost scope before this yield.
For while-loop yields the first item is a guard:
`if not (loop_cond): raise StopIteration`
yield_val : the yielded expression (may be an IfExp ternary for if/else)
post_stmts: statements after this yield until the next yield
(e.g. `i += 1` after `yield i`)
is_repeating: True when the yield is inside a loop
|
protected |
Combine a generator's `if` clauses into one condition. Python allows several `if` clauses in a single comprehension generator (`[x for x in A if c1 if c2]`), which is equivalent to conjoining them (`if c1 and c2`). Return the visited single condition, or a BoolOp(And) over all of them.
|
protected |
Constant value of ``param["k"]`` over a dict literal of constants, else None.
|
protected |
Constant value of a scalar or tuple-of-scalars element, else None.
|
protected |
|
staticprotected |
Return the constant value of a literal `node`, handling unary +/- over a numeric constant (Python parses ``-5`` as UnaryOp(USub, 5)), or None when the node is not a constant literal.
|
protected |
|
staticprotected |
Name ``d`` when the call is ``sorted(d | d.keys(), key=d.__getitem__)``.
|
protected |
Evaluate a constant-foldable ``key=`` argument over one constant list element, returning the key's Python value or None when not foldable. ``element`` is the element's AST node (a constant scalar, a unary +/- over one, or a tuple of such constants). ``key_node`` is either a one-parameter ``lambda`` whose body is built from the parameter, numeric constants, unary +/-, binary arithmetic, a constant subscript ``p[K]``, and the ``abs``/``len`` builtins; or the bare ``abs``/``len`` builtin name. None means "leave the key unapplied" (the caller's existing fallback), so a value of None is never treated as a foldable key.
|
protected |
Return the list of constant key values for `key=` applied to each element, or None when the key form or elements are not constant- foldable. See ``_eval_const_key_value`` for the supported key forms.
|
protected |
Evaluate a lambda key body for the parameter bound to ``element``.
|
protected |
|
protected |
Return (gen_var, func_name) if node contains next(g) for a tracked generator, else None.
|
protected |
For ``sorted(d, key=d.__getitem__)`` (or ``d.keys()``) over a tracked constant dict literal, return ``(key_nodes, value_list)`` so the keys are ordered by their values; None when the pattern does not apply.
|
protected |
If call_node is d.items() on a known dict, return the dict expression. Else None.
|
protected |
If node is W(d.<attr>()) where W in {list, sorted, set}, return (dict_expr, wrapper).
Returns (None, None) on no match. The wrapper name lets the caller
enforce wrapper-vs-literal-type compatibility (e.g. set wrapper
requires a Set literal). ``sorted(list(...))`` is peeled to
``sorted(...)`` since list() is identity on a view.
|
protected |
Return (dict_expr, wrapper) if node is W(X) where W in `wrappers` and X is a dict_items source. Returns (None, None) on no match. The wrapper name lets the caller apply soundness checks that depend on which wrapper is in use (list/sorted/set differ in ordering semantics). ``sorted(list(...))`` folds to ``sorted(...)`` (list() is identity on a view) so the cascade matches both idioms.
|
protected |
Return True if body has a Return statement before any Yield (linear top-level scan).
|
staticprotected |
Return True if node contains a Yield or YieldFrom expression.
|
protected |
Scan a loop body for direct `var = next(gen_var)` assignments. For each normal generator whose outer_init hasn't been emitted yet, deep-copy the outer_init statements and return them (to be placed before the loop), and mark the generator as initialized so that _inline_next_call won't re-emit them inside the loop body.
|
protected |
Evaluate a leftmost iterable that the comprehension itself shadows. Python evaluates the leftmost iterable in the enclosing scope, before the comprehension binds its target. Leaving it in the generated `for` evaluated it after, so `[node for node in node.xs]` read `node.xs` off an element instead of the outer object.
|
staticprotected |
A ``lambda x: body`` a scan applies by substituting its argument, a pure read, for ``x``. Bound and called instead, its parameter is typed before the scan's temporaries exist and defaults to double (#7745).
|
protected |
Inline a for loop over a direct generator function call.
Transforms:
for x in gen_func(a, b):
body
Into the generator body with each `yield val` replaced by:
param_0 = a
param_1 = b
x = val
body
Returns the list of inlined statements, or None if inlining is not
possible (unknown generator, keyword args, arg count mismatch,
non-simple loop target, or generator body contains return/yield-from).
|
protected |
Inline a generator-based for loop.
Transforms:
for x in g: # where g = gen_func()
body
Into the generator body with each `yield val` replaced by:
x = val
body
Returns the list of inlined statements, or None if inlining is not possible.
|
staticprotected |
The body of @p key_value with its parameter replaced by @p arg_expr.
|
protected |
Inline `x = next(g)` for a normal generator. Emits outer_init (generator initialisation) on the first call for gen_var, then per-call: pre_stmts + assignment + post_stmts. For yields inside loops (is_repeating=True) the index is not advanced. Pass targets=None for a standalone next(g) with no assignment target. Returns list of statements, or None if inlining is not possible.
|
protected |
|
staticprotected |
|
protected |
|
staticprotected |
Return True if any Call in *body* references func_name directly. Skips nested FunctionDef/AsyncFunctionDef/Lambda bodies: a call to func_name from inside a nested helper belongs to that helper's scope, not the generator's, so it must not be treated as a recursive call (otherwise an unrelated nested helper that happens to reference the outer name triggers a false-positive recursive-generator transform).
|
protected |
True when a sort scan lowers to operations the frontend models. The scan copies the iterable with a full slice and applies the key to each element, and two shapes exceed what the frontend models: copying a dict view does not terminate at the default unwind, and an element the key subscripts raises a spurious IndexError. Declining leaves reject_unfoldable_key to report the unsupported key, which beats a hang or a wrong verdict.
|
staticprotected |
True for the key shapes a scan lowering can emit. A single-parameter lambda is inlined, or bound to a temporary and called when _inlinable_key_lambda declines it; a plain name is called directly (binding one yields a symbol the callee resolution does not accept). Of the bound methods only ``__getitem__`` qualifies, because it is emitted as a subscript -- a scan's own statements are not re-visited, so any other would be a call nothing gets the chance to rewrite.
|
staticprotected |
Return True iff elts is statically known to be sorted (ascending). by="self": each elt is ast.Constant, sort by elt.value. by="first": each elt is ast.Tuple of Constants, sort by first element. Returns False if any elt is non-Constant or has incomparable types (conservative — bail when sortedness cannot be statically verified).
|
protected |
|
protected |
True when applying ``key_value`` subscripts the element it is given. A key bound by assignment rather than by a def reads as not indexing, so such a call is still lowered to a scan.
|
staticprotected |
|
staticprotected |
|
protected |
Lower all(elt for target in iter [if cond]) to prefix stmts + boolean result.
Transforms:
all(elt for target in iter if cond)
Into:
ESBMC_all_N = True
for target in iter:
if cond: # only when ifs are present
if ESBMC_all_N:
if not elt:
ESBMC_all_N = False
<result: ESBMC_all_N>
Uses guard-based short-circuit (checking ESBMC_all_N before evaluating)
instead of break to avoid ESBMC's break+empty-list type inference issue.
|
protected |
Lower any(elt for target in iter [if cond]) to prefix stmts + boolean result.
Transforms:
any(elt for target in iter if cond)
Into:
ESBMC_any_N = False
for target in iter:
if cond: # only when ifs are present
if elt:
ESBMC_any_N = True
<result: ESBMC_any_N>
|
protected |
|
protected |
Lower list(gen_func(args...)) to an inline list construction.
Transforms list(gen_func(a, b)) into:
param_0 = a
param_1 = b
ESBMC_list_gen_N: list = []
# generator body with yield val -> ESBMC_list_gen_N.append(val)
Returns (prefix_stmts, result_name_expr), or (None, gen_call_node) if
inlining is not possible (body has return/yield-from, keyword args, or
positional-arg count mismatch).
|
protected |
Lower a list comprehension into prefix statements and result expression.
A comprehension with multiple `for` clauses is not a nested comprehension:
it is semantically equivalent to nested for-loops:
[f(i,j) for i in A for j in B] => for i in A: for j in B: tmp.append(f(i,j))
|
protected |
Lower all list comprehensions inside an expression node. Returns (prefix_stmts, new_expr, result_type) where result_type is inferred from the transformed root expression.
|
protected |
Lower ``min``/``max(iterable, key=f)`` to an explicit linear scan. Only reached once ``_lower_min_max_with_key_call`` has declined, i.e. the iterable or the key is not constant-foldable. The runtime model takes no key parameter, so without this the key is dropped and the call answers by natural order. Returns ``(prefix_statements, expr)``, or None when the shape does not apply. Ties keep the first occurrence, matching CPython. An empty iterable raises IndexError here where CPython raises ValueError.
|
protected |
Lower min/max(iterable, key=...) for literal-list iterables with a constant-foldable key. Two key forms are supported over a list literal whose relevant values are constants: a one-arg ``lambda x: x[K]`` (constant index) over a list of tuples, and the ``abs``/``len`` builtins over a list of constant scalars/strings. The key is evaluated at preprocess time and the winning *element* (not its key) is returned, breaking ties toward the first occurrence (CPython semantics). Returns (prefix, expr) on success, or None when the pattern does not apply (caller falls back to the regular dispatch, which today drops the key= keyword).
|
protected |
|
protected |
Lower a key'd ``sorted()`` standing where an iterable is expected. Applies the same order as the expression rewriter -- constant fold first, scan for what it could not fold -- on behalf of the loop lowering, which builds its iterable assignment after that rewriter has already run.
|
protected |
Lower ``sorted(iterable, key=f)`` to an explicit insertion sort. Only reached once ``_lower_sorted_with_key_call`` has declined, i.e. the iterable or the key is not constant-foldable. The runtime sort model takes no key parameter, so without this the key is dropped and the call answers by natural order. Returns ``(prefix_statements, expr)``, or None when the shape does not apply. Insertion sort with a strict ``>`` is stable, as CPython's sort is. The key is applied once per element, in order, into a parallel list the sort moves with the elements: CPython calls it exactly that way, and an impure key re-applied in the shift loop was observable. A builtin key whose call has no side effect is re-applied instead, since the second list costs the solver several times the sort itself (humaneval_149). The working list is copied with a full slice rather than ``list(iterable)``, which aliases its argument -- sorting through the alias would mutate the caller's list, and ``sorted`` must not.
|
protected |
Lower ``sorted(iterable, key=...)`` for constant list-literal iterables. Supports any constant-foldable ``key=`` (see ``_eval_const_key_value``): identity ``lambda x: x``, unary ``-x``/``+x``, binary arithmetic over the parameter and constants, a constant subscript ``lambda x: x[K]`` over a tuple element, and the ``abs``/``len`` builtins. The key is evaluated at preprocess time on each constant element and the original element nodes are reordered accordingly (a stable sort, matching CPython); the elements themselves are preserved, so their runtime values are unchanged. Returns ``(prefix, expr)`` on success, or None when the iterable or key is not constant-foldable (the caller then leaves ``key=`` unapplied, as before).
|
protected |
Lower tuple(sorted([a, b])) to a conditional pair assignment.
Instead of ``(a, b) if a <= b else (b, a)`` (which ESBMC encodes as a
pointer to a temporary struct — a known crash pattern), we emit:
_lo = a if a <= b else b
_hi = b if a <= b else a
(_lo, _hi)
The result is a 2-tuple whose elements are plain scalar variables.
ESBMC can handle named-scalar tuple construction without the
pointer-to-temporary issue.
|
protected |
Build `raise StopIteration('StopIteration')` AST node.
|
protected |
Combine if/else yield values into a single ternary expression.
|
protected |
If expr_node is `name.sort(key=lambda ...)` (with optional reverse=), rewrite to `name = sorted(name, key=..., reverse=...)`. Returns the replacement Assign, or None when the pattern does not apply.
|
staticprotected |
``min``/``max(a, b, ..., key=f)`` as ``min``/``max([a, b, ...], key=f)``, which CPython defines to be the same, so the key lowerings see their one-iterable form. A call argument is left alone: the element type of a list literal holding it cannot be inferred when the callee has no return annotation.
|
staticprotected |
Return the constant non-negative index of ``param[K]``, or None when ``node`` is not a constant subscript on the lambda parameter ``param``.
|
protected |
|
staticprotected |
Yield (call, parent) for each direct call to func_name in *body*.
|
protected |
Rename a comprehension target that shadows a known outer variable or the target of an earlier comprehension. Python 3 scopes a comprehension's target to the comprehension, so the rename is semantically free. Without it the outer and inner bindings share one symbol, and an outer object rebound to elements aborts the converter in member2t; two comprehensions over elements of different types give that symbol two types and crash the solver (#9126).
|
protected |
|
protected |
``key=k`` for a name _scan_closed_lambda_bindings recorded, as the lambda itself: called through the name, the scan's call resolves ``k`` as a function symbol and aborts conversion.
|
protected |
|
protected |
Look up the next yield to inline for ``gen_var``. Returns ``(outer_init, entry)`` where ``entry`` is one of: * ``None`` -- generator unknown or yields nothing (cannot inline) * ``"stop"`` -- generator is exhausted; caller should raise StopIteration * tuple -- ``(pre_stmts, yield_val, post_stmts, is_repeating)``
|
protected |
Names the module binds exactly once, to a one-parameter lambda whose body reads nothing but that parameter: inlining such a body wherever the name is used cannot capture a different variable.
|
protected |
Blacklist generator variables whose next() calls cannot be inlined.
_inline_next_call picks each next(g)'s yield by its place in the
source, emits the generator's setup at the first next(g), and pastes
the generator's statements into the caller. That matches execution
only when:
* g is bound once, in straight-line code, and consumed in that scope;
* every next(g) is the whole value of an assignment or a statement;
* each next(g) runs in source order: straight-line code, or the last
one inside a try body. A generator whose only yield sits in a loop
gives the same value at every call, so after the first call any
position works, and the first may be an assignment directly in a
straight-line loop, whose setup _hoist_generator_inits emits;
* no name the generator binds is used by the caller, nor (in a
function) any name it reads bound by the caller.
A blacklisted next(g) is left alone, so it stays unsupported.
|
protected |
Return the ``key=`` keyword a scan lowering should apply, else None. Rejects anything the scans cannot lower: a call that is not ``<name>(iterable, key=...)``, a second keyword, a multi-parameter lambda, and a key that is not a lambda, a plain name or a bound method (see _lower_min_max_key_scan for why). An all-constant list literal is rejected too: the constant fold above owns that case and declined only because the key values are mutually incomparable, which the regular dispatch reports as a mixed-element-type error -- scanning instead would bury that behind a vaguer one.
|
staticprotected |
Build one application of a scan lowering's ``key=``. ``d.__getitem__`` becomes a subscript rather than a call: the statements a lowering emits are not re-visited, so the dunder-to-operator rewrite in visit_Call would never reach it and the frontend would raise AttributeError on the method spelling.
|
protected |
Builtin keys a scan may re-apply: unbound in the module, and no class it can see defines their dunder, so a call has no side effect. A module importing anything but ``typing`` may receive such a class, and is excluded outright.
|
staticprotected |
|
staticprotected |
The call's one ``key=`` keyword, None when it has none or a keyword outside ``key`` and ``allowed``.
|
staticprotected |
The ``reverse=`` value of a ``sorted`` call, ``False`` when absent.
|
protected |
|
protected |
Transform a recursive generator function to accumulate-and-return.
Converts:
def f(args):
...
yield val
...
Into:
def f(args) -> list:
ESBMC_gen_result: list = []
...
ESBMC_gen_result.append(val)
...
return ESBMC_gen_result
|
protected |
Lower ``expr == (c0, c1, ...)`` where *expr* is not a bare Name.
Instead of a struct-to-struct equality (which requires identical Z3
sorts and fails when the function-return struct type differs from the
literal tuple struct type), we **unpack** the tuple and compare each
element individually:
_u0, _u1, ... = expr
assert _u0 == c0 and _u1 == c1 and ...
Tuple unpacking is implemented in ESBMC via struct member access
(``element_0``, ``element_1``, ...), so each unpacked variable carries
the correct element type (e.g. ``double_floatbv``). Element-wise scalar
comparisons then avoid the struct-sort mismatch entirely.
Returns ``(prefix_stmts, new_test)`` when the pattern matches, or
``(None, None)`` when it does not. Only applies when *tuple_side* is a
tuple literal whose elements are all ``_is_assert_literal_shape`` values
and *expr_side* is not already a ``Name``.
|
protected |
Transform list/sorted(d.items()) == [(k,v),...] into dict membership checks.
Rewrites to ``len(d) == N and k_i in d and d[k_i] == v_i`` per pair.
Soundness guards:
- pair keys must be statically distinct Constants. Dict keys are
distinct, so any literal pair list with duplicate keys never
equals a real dict's items view; without this guard, e.g.
``[(1,'a'),(1,'a')]`` would rewrite to a satisfiable formula
(``{1:'a', 2:anything}``) — unsound.
- sorted wrapper: literal must be statically sorted by first tuple
element (CPython sorts tuples by key first; an unsorted literal
would compare False but the rewrite would say True).
- list wrapper: literal must have at most one pair (ESBMC's dict
model does not preserve insertion order).
|
protected |
Transform set(d.items()) == {(k,v),...} into dict membership checks.
Rewrites to: set(d.keys()) == {k,...} and d[k1] == v1 and d[k2] == v2 ...
This avoids tuple struct comparison and uses only proven-working primitives.
Returns the new AST node, or None if the pattern doesn't match.
|
protected |
Transform W(d.keys()) == literal into membership checks, where W is one of
list/sorted/set.
Rewrites to ``len(d) == N and k1 in d and k2 in d ...`` — set-equality
semantics. Soundness guards (each bails when violated):
- wrapper-vs-literal type: set ↔ ast.Set; list/sorted ↔ ast.List
(CPython makes ``list == set`` always False otherwise).
- literal keys must be statically distinct Constants. Dict keys are
distinct, so any literal with duplicate keys mismatches CPython
semantics: for set wrapper, ``{1,1}`` dedupes to ``{1}`` (length
mismatch); for list/sorted, ``[1,1]`` never equals any view of a
real dict. Bailing here is sound.
- sorted wrapper: literal must be statically sorted ascending
(otherwise CPython is always False but the rewrite would say True).
- list wrapper: literal must have at most one element
(ESBMC's dict model does not preserve insertion order).
|
protected |
Transform x == [(a,b), ...] into len/index comparisons for x.
|
protected |
Transform list/sorted(d.values()) == [literal] into membership checks. Rewrites to ``len(d) == N and v1 in d.values() and ...``. Soundness guards (each bails when violated): - set wrapper is rejected entirely: dict values may repeat, so the rewrite cannot soundly relate ``len(d)`` to ``len(literal_set)``. - literal must be ast.List of distinct Constants (duplicates would collapse to fewer ``in`` checks but pass the length test, turning a False assertion into True). - sorted wrapper: literal must be statically sorted ascending. - list wrapper: literal must have at most one element (insertion order is not modelled).
|
staticprotected |
The one argument of `call`, with a statement raising the arity TypeError when it is the guard _lower_starred_call_argument spells `f(a, *xs)` as: then `f(xs[0], ..., xs[k-1])` and the statement. list(gen(*xs)) is inlined as statements, so the guard moves ahead of them (#8670).
|
staticprotected |
| preprocessor.generator_mixin.GeneratorMixin.visit_GeneratorExp | ( | self, | |
| node ) |
A generator expression reaches the converter unlowered, so rename its shadowing target here rather than in the comprehension lowering.
|
staticprotected |
|
protected |
|
protected |
|
protected |
|
protected |
|
protected |
| preprocessor.generator_mixin.GeneratorMixin.comprehension_targets |
| preprocessor.generator_mixin.GeneratorMixin.dict_items_vars |
| preprocessor.generator_mixin.GeneratorMixin.early_return_generator_funcs |
| preprocessor.generator_mixin.GeneratorMixin.generator_emitted_init |
| preprocessor.generator_mixin.GeneratorMixin.module_name |
1.15.0