ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
preprocessor.zip_lowering Namespace Reference

Functions

 _bound_names (module)
 _plain_call (node, name, nargs)
 _zip_build (stmt)
 _loop (stmt, build, counter)
 _statement_lists (module)
 lower_zip_builds (module)
 _zip_binding (stmt)
 _is_zip_call (node)
 _mentions (tree, name)
 _reader (stmt, name)
 _inline_zip (stmts, i, module)
 inline_zip_names (module)

Detailed Description

Lower `T = dict(zip(A, B))` to a loop (#8283).

`zip` is lowered as a for loop's iterable and inside `list(...)`, but building a
dict from it reached the unsupported-function marker. The assignment becomes an
empty dict filled by a loop over the same `zip`.

Function Documentation

◆ _bound_names()

preprocessor.zip_lowering._bound_names ( module)
protected

◆ _inline_zip()

preprocessor.zip_lowering._inline_zip ( stmts,
i,
module )
protected
Moves the zip bound by `stmts[i]` into the one sibling reading it.

◆ _is_zip_call()

preprocessor.zip_lowering._is_zip_call ( node)
protected

◆ _loop()

preprocessor.zip_lowering._loop ( stmt,
build,
counter )
protected

◆ _mentions()

preprocessor.zip_lowering._mentions ( tree,
name )
protected

◆ _plain_call()

preprocessor.zip_lowering._plain_call ( node,
name,
nargs )
protected
Whether `node` is `name(...)` with `nargs` positional arguments.

◆ _reader()

preprocessor.zip_lowering._reader ( stmt,
name )
protected
The `for` loop or `list(name)` call in `stmt` that reads `name`, else None.

◆ _statement_lists()

preprocessor.zip_lowering._statement_lists ( module)
protected

◆ _zip_binding()

preprocessor.zip_lowering._zip_binding ( stmt)
protected
`(name, zip_call)` for `name = zip(...)` over names and literals, else None.

◆ _zip_build()

preprocessor.zip_lowering._zip_build ( stmt)
protected
`(target, zip_call)` for `target = dict(zip(a, b))`, else None.

◆ inline_zip_names()

preprocessor.zip_lowering.inline_zip_names ( module)
Reads `z = zip(...)` at its one `list(z)` or `for ... in z` (#8967).

The iterator is consumed once, so the call moves to its reader, where the
existing `list(zip(...))` and `for ... in zip(...)` lowerings apply. Its
operands are names and literals not rebound in between, so they evaluate
to the same objects.

◆ lower_zip_builds()

preprocessor.zip_lowering.lower_zip_builds ( module)
Rewrites every eligible zip-built dict in `module`.