- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <python_list.h>
Classes | |
| struct | strided_axis |
| One axis of a strided view, in elements: its extent and stride are constants unless the matching expression is set (a signed 64-bit temporary computed at run time). More... | |
| struct | strided_view_desc |
| A numpy array or view as a scalar base pointer plus its axes: the descriptor every N-D view is built from. More... | |
| struct | shallow_push_call |
| struct | list_eq_target |
Public Types | |
| enum class | view_contiguity { contiguous , not_contiguous , unknown } |
Public Member Functions | |
| python_list (python_converter &converter, const nlohmann::json &list) | |
| exprt | get () |
| exprt | build_list_from_exprs (const std::vector< exprt > &elems) |
| Materialize a fresh list from already-evaluated element values. | |
| exprt | build_symbolic_fill_list (const exprt &size, const exprt &fill_value, const typet &elem_type, const exprt *index_base=nullptr) |
Build a runtime PyListObject filled with fill_value repeated size times. | |
| exprt | index (const exprt &array, const nlohmann::json &slice_node) |
| exprt | build_bool_mask_index (const exprt &array, const exprt &mask, const nlohmann::json &element) |
Lower boolean-mask indexing a[mask] to a runtime loop that builds a fresh list holding the elements of array whose matching mask entry is True (NumPy fancy-indexing semantics). | |
| exprt | build_bool_mask_row_select (const exprt &array, const exprt &mask, const nlohmann::json &element) |
| Lower whole-row boolean-mask selection a[mask] on a 2-D array. | |
| exprt | build_bool_mask_row_select_symbolic (const exprt &array, const exprt &mask, const nlohmann::json &element) |
Lower whole-row boolean-mask selection a[mask] on a 2-D array for a symbolic (non-literal) mask: the result is the canonical bounded descriptor shape — a worst-case-sized rows buffer (capacity == array's row count) plus a runtime count member holding the number of rows actually selected, so the logical size is part of the modelled value rather than a detached counter. | |
| exprt | index_bool_mask_rows (const exprt &array, const nlohmann::json &slice_node, const nlohmann::json &element) |
Index b[i] into a boolean-mask row-selection result (see build_bool_mask_row_select_symbolic): normalizes a negative slice_node index against the struct's runtime count member (not the rows buffer's physical capacity), bounds-checks it against count (raising IndexError out of bounds, mirroring build_list_at_call), and returns the selected row. | |
| exprt | build_column_select (const exprt &array, const nlohmann::json &col_index_node, const nlohmann::json &element) |
| Lower 2-D column selection a[:, j] to a bounded copy over every row of a fixed-shape 2-D array, collecting row[j] into a fresh 1-D array. | |
| exprt | build_strided_column_select (const exprt &array, const nlohmann::json &col_slice_node, const nlohmann::json &element) |
| Lower a strided column slice a[:, start:stop:step] on a fixed-shape 2-D array: the literal slice bounds are resolved at conversion time and each selected column is copied into a fresh 2-D result. | |
| std::optional< exprt > | try_build_diagonal_pointer_view (const exprt &array, long long k) |
| np.diagonal(a[, offset=k])/a.diagonal([k]): a read-only strided pointer view into a's own buffer (ADR-NP-003 etapa 2). | |
| std::optional< exprt > | build_trace_reduction (const exprt &array, long long k) |
| np.trace(a, offset=k): sum of the elements np.diagonal(a, k) would view, computed directly as a scalar reduction (no view is built). | |
| bool | try_build_fill_diagonal_mutation (const exprt &array, const nlohmann::json &value_node) |
| np.fill_diagonal(a, value): mutates a's main diagonal in place via converter_.add_instruction, using the same offset/stride math as try_build_diagonal_pointer_view/build_trace_reduction with k=0. | |
| std::optional< exprt > | try_build_ravel_pointer_view (const exprt &array) |
| np.ravel(a)/a.ravel(): a writable, contiguous strided pointer view into a's own buffer (ADR-NP-003 etapa 2), for a fixed-shape 1-D or 2-D array. | |
| std::optional< strided_view_desc > | describe_strided_view (const exprt &array) |
| std::optional< exprt > | try_build_numpy_param_slice_view (const exprt &array, const typet &resolved_array_type, const nlohmann::json &slice_node) |
| bool | is_runtime_numpy_slice (const exprt &array, const typet &elem_type, const nlohmann::json &slice_node) const |
| std::optional< exprt > | unnamed_nd_view_placeholder (const strided_view_desc &view, bool as_view, bool flat_result, const char *unnamed_error) const |
| std::optional< exprt > | alias_contiguous_ravel (const nlohmann::json &arg, const strided_view_desc &view) |
| exprt | emit_view_copy_buffer (const nlohmann::json &arg, const strided_view_desc &view, const exprt &count) |
| std::vector< strided_axis > | owned_copy_axes (const nlohmann::json &arg, const strided_view_desc &view, bool flatten, const exprt &count) |
| void | emit_reshape_size_guard (const nlohmann::json &arg, const exprt &count, const std::vector< std::size_t > &new_shape) |
| void | scale_split_axis_strides (const nlohmann::json &arg, const strided_axis &source, std::vector< strided_axis > &axes) |
| void | reshape_registered_copy (const std::string &lhs_id, const std::vector< std::size_t > &new_shape) |
| exprt | emit_view_accumulator (const nlohmann::json &arg, const typet &type, const exprt &init) |
| exprt | reduce_view_truth (bool is_any, const nlohmann::json &arg, const strided_view_desc &view) |
| exprt | reduce_view_extreme (const std::string &function, const nlohmann::json &arg, const strided_view_desc &view, const exprt &count) |
| bool | strided_basic_view_declines (const exprt &array, const std::vector< nlohmann::json > &idx_nodes, bool allow_plain_array) const |
| std::optional< strided_axis > | runtime_slice_axis (const strided_axis &source, const nlohmann::json &node, exprt &offset) |
| std::optional< strided_axis > | slice_strided_axis (const strided_axis &source, const nlohmann::json &node, exprt &offset) |
| bool | index_strided_axis (const strided_axis &source, const nlohmann::json &node, exprt &offset) |
| exprt | strided_index_offset (const strided_view_desc &src, const std::vector< nlohmann::json > &indices) |
| std::optional< strided_view_desc > | contiguous_view_desc (const exprt &array, const typet &elem_type, const std::vector< std::size_t > &shape) const |
| std::vector< strided_axis > | tracked_view_axes (const std::string &view_id) const |
| Axes of the pointer view registered under view_id. | |
| exprt | register_strided_view (const strided_view_desc &source, const exprt &offset, const std::vector< strided_axis > &axes, bool readonly=false) |
| base + offset as a registered view with these axes for the assignment target (offset is a size_type element count). | |
| exprt | copy_strided_view (const strided_view_desc &source, const exprt &offset, const std::vector< strided_axis > &axes, const std::vector< std::size_t > *out_shape=nullptr) |
| Independent array holding the elements a view with these axes reads, in row-major order. | |
| std::optional< strided_view_desc > | symbolic_view_operand (const nlohmann::json &arg) |
| The descriptor of the named view when its extents or strides are known only at run time; nullopt for anything else. | |
| exprt | view_element (const strided_view_desc &view, const std::vector< exprt > &index) const |
| Element lvalue of a view at a signed 64-bit multi-index. | |
| void | emit_counted_loop (const nlohmann::json &node, const exprt &extent, const std::function< void(const exprt &)> &body) |
| idx = 0; while (idx < extent) { body(idx); idx++; }, with the body's statements emitted inside the loop. | |
| void | emit_view_loops (const nlohmann::json &node, const strided_view_desc &view, const std::function< void(const exprt &)> &leaf) |
| Nested loops over every index of a view; leaf is called once, inside the innermost body, with the element lvalue. | |
| exprt | view_element_count (const nlohmann::json &node, const strided_view_desc &view) |
| std::optional< exprt > | reduce_view_argextreme (const std::string &function, const nlohmann::json &arg) |
| sum / mean / min / max / any / all of a run-time-extent view, as loops. | |
| std::optional< exprt > | try_reduce_symbolic_view (const std::string &function, const nlohmann::json &arg) |
| std::optional< exprt > | try_build_symbolic_view_list (const nlohmann::json &arg, bool nested) |
| A Python list of a run-time-extent view's elements (nested per axis when nested, flat otherwise). | |
| std::optional< exprt > | try_reshape_symbolic_view (const nlohmann::json &arg, const std::vector< std::size_t > &new_shape) |
| reshape of a run-time-extent view to constant new_shape: an alias when it is contiguous, a copy otherwise; ValueError if the sizes differ. | |
| std::optional< exprt > | try_copy_symbolic_view (const nlohmann::json &arg, bool flatten=false, bool alias_if_contiguous=false) |
| np.copy / np.array / .copy of a run-time-extent view. | |
| exprt | emit_ll_temp (const nlohmann::json &node, const char *name, const exprt &value) |
| Signed 64-bit temporary holding value, assigned once here. | |
| std::optional< exprt > | try_build_strided_basic_view (const exprt &array, const std::vector< nlohmann::json > &idx_nodes, bool allow_plain_array=false) |
| v = a[i, :, 1:3, ...] over a rank-3+ array or any N-D view, with literal or run-time indices and slice bounds: a view into the source's own storage (aliasing in both directions) when assigned to a bare name, otherwise an independent copy. | |
| std::optional< exprt > | try_build_strided_view_index (const nlohmann::json &element) |
| b[i][j], b[i, j] or x = b[i] over a registered N-D strided view. | |
| std::optional< flat_array_shape_info > | flat_shape_info_of (const exprt &array) const |
| Total element count and scalar element type of a fixed-shape array of any rank, or of a contiguous N-D subarray view. | |
| std::optional< exprt > | build_contiguous_shaped_view (const exprt &array, const std::vector< std::size_t > &shape, std::size_t offset, bool readonly) |
| Pointer into array's own contiguous storage, offset elements in, that reads as an N-D array of shape; registers it for the assignment target. | |
| exprt | scalar_storage_pointer (const exprt &array, const typet &scalar_ptr_type) const |
| array's storage as a pointer to its scalar element type. | |
| std::optional< exprt > | try_build_flat_index_assignment_target (const exprt &array, const nlohmann::json &index_node) |
| a.flat[i] = x: builds a dereferenced-pointer lvalue into a's own buffer at flat index i (bounds-checked and negative-index-normalized the same way a registered pointer view's index is), for a fixed-shape 1-D or 2-D array – the same eligibility and offset/stride=1 math as try_build_ravel_pointer_view, but built inline for an assignment target that has no intermediate bare-name view symbol to register into numpy_pointer_view_info_. | |
| exprt | build_mixed_slice_tuple_select (const exprt &array, const std::vector< nlohmann::json > &idx_nodes, const nlohmann::json &element) |
| Lower an N-D mixed slice/index tuple subscript with one or more bounded slice axes and fixed-index axes, e.g. | |
| exprt | build_fancy_index (const exprt &array, const std::vector< nlohmann::json > &indices, const nlohmann::json &element) |
Lower integer-array (fancy) indexing a[[0, 2]] to a bounded, unrolled sequence of element reads: each entry of indices must be a concrete integer literal (or its negation), resolved and bounds-checked at conversion time. | |
| void | handle_slice_assignment (const exprt &list_expr, const nlohmann::json &slice_node, const nlohmann::json &value_node) |
| Lower a list slice assignment l[lower:upper:step] = value to a __ESBMC_list_slice_assign model call. | |
| void | handle_subscript_assign_none (const exprt &list_expr, const nlohmann::json &slice_node) |
| size_t | eq_float_type_id (const std::string &lhs_id, const std::string &rhs_id) const |
| The float element type_id that lets list_eq compare mixed int and float elements numerically (Python's 1 == 1.0), merged from both operands. | |
| exprt | compare (const exprt &l1, const exprt &l2, const std::string &op) |
| exprt | contains (const exprt &item, const exprt &list) |
| exprt | list_repetition (const nlohmann::json &left_node, const nlohmann::json &right_node, const exprt &lhs, const exprt &rhs) |
| void | retype_element_store (exprt &lhs, exprt &rhs) |
Turn the store lhs = rhs into a replacement of the element record when the value cannot be written through the element's type. | |
| bool | has_shared_payload (const typet &type) const |
Whether a list slot holding type may share its payload with a copy of the list: list copies keep the PyObject record of a non-scalar element verbatim (#5102), so a store must not write through it. | |
| exprt | allocate_constructed_object (const exprt &lhs) |
Allocates the instance a constructor stores to lhs and returns the pointer to pass as self. | |
| void | record_element_store (const nlohmann::json &subscript, const std::string &elem_id, const typet &elem_type) |
Records elem_type as the type of the element subscript stores to. | |
| std::optional< expr2tc > | fast_elem_equality (exprt lhs_val, exprt rhs_val, const typet &lhs_type, const typet &rhs_type) const |
Equality of two list elements read as lhs_type and rhs_type for compare()'s fast path, or nullopt when it cannot relate them. | |
| void | require_stored_types (expr2tc &sizes_ok, std::size_t depth, const exprt &lhs_at, const typet &lhs_type, const exprt &rhs_at, const typet &rhs_type) const |
Conjoins to sizes_ok that the slots lhs_at and rhs_at hold lhs_type and rhs_type, for compare()'s nested fast path. | |
| exprt | build_push_list_call (const symbolt &list, const nlohmann::json &op, const exprt &elem, bool enable_float_path=true) |
| exprt | build_insert_list_call (const symbolt &list, const exprt &index, const nlohmann::json &op, const exprt &elem) |
| exprt | build_extend_list_call (const symbolt &list, const nlohmann::json &op, const exprt &other_list) |
| exprt | build_concat_list_call (const exprt &lhs, const exprt &rhs, const nlohmann::json &element) |
| std::vector< exprt > | literal_elems_for_variable_list (const nlohmann::json *source_node, const exprt &source_list) |
| The declaring literal's elements for a variable-held list, or empty when the literal cannot be used. | |
| bool | literal_still_describes_list (const exprt &source_list, size_t literal_elem_count) |
| True when a list's declaring literal still describes its contents. | |
| typet | bare_list_param_elem_type (const nlohmann::json ¶m_node, const std::string ¶m_id, const typet &annotated, size_t index) |
| Element type recovered for a bare list parameter, or a nil type. | |
| bool | mixes_list_and_other (const std::string &id) const |
True when the recorded elements of id mix a list with another type. | |
| void | reject_unresolved_element_read (const exprt &array, const nlohmann::json &slice_node) const |
| Refuses a read that no single recorded element type answers (#8472). | |
| void | reject_mixed_member_element_read (const exprt &array, const nlohmann::json &slice_node) const |
| Refuses an index other than a non-negative constant into a list attribute whose recorded elements have different types (#8666). | |
| exprt | get_empty_set () |
| Create an empty set. | |
| exprt | handle_comprehension (const nlohmann::json &element) |
| Convert generator expressions and list comprehensions to lists. | |
| exprt | build_pop_list_call (const symbolt &list, const exprt &index, const nlohmann::json &element) |
| Build a list pop operation. | |
| void | guard_pop_index (const symbolt &list, const exprt &index, const locationt &location) |
| Inside a try body, raises a catchable IndexError ahead of a pop() whose list is empty or whose index is out of range, before __ESBMC_list_pop asserts it. | |
| bool | store_replaces_element (const typet &old_type, const typet &new_type) const |
| Whether storing a new_type value into an element read as old_type replaces the element rather than writing into its storage. | |
| std::optional< exprt > | build_element_replacement (const exprt &lhs, const exprt &rhs, const nlohmann::json &op) |
| The __ESBMC_list_set_at call storing rhs into the list element lhs reads, when store_replaces_element holds; nullopt otherwise. | |
| exprt | extract_pyobject_value (const exprt &pyobject_expr, const typet &elem_type, bool mixed_numeric=false, bool string_safe=false) |
| Extract and dereference value from a PyObject* expression. | |
| typet | infer_literal_element_type (const nlohmann::json &list_literal) |
| Infer the element type of a list literal AST node, accounting for the int->float promotion applied at construction. | |
| exprt | build_min_max_for_mixed_numeric (const exprt &list_arg, const std::string &list_id, const std::string &func_name, irep_idt comparison_op) |
| Build an inline min/max computation for a mixed int/float list. | |
| exprt | build_copy_list_call (const symbolt &list, const nlohmann::json &element) |
| Build a list copy operation. | |
| exprt | build_shallow_copy_call (const exprt &src_list, const nlohmann::json &element) |
| Emit a __ESBMC_list_copy_shallow call producing a shallow copy of src_list (Python copy semantics: scalar elements get independent buffers, nested containers stay shared). | |
| exprt | build_tuple_copy_call (const exprt &src_list, const nlohmann::json &element) |
| tuple(x) of a list: a shallow copy marked as a tuple (#8777). | |
| void | build_mark_tuple_call (const exprt &list) |
| Mark list as built by tuple(x) (#8777). | |
| exprt | build_is_tuple_call (const exprt &list) |
| Whether list was built by tuple(x) (#8777). | |
| exprt | build_remove_list_call (const symbolt &list, const nlohmann::json &op, const exprt &elem) |
| Build a list remove operation (removes first matching element). | |
| exprt | build_count_list_call (const symbolt &list, const nlohmann::json &op, const exprt &elem) |
| Build a list.count(x) call — number of elements equal to x. | |
| exprt | build_index_list_call (const symbolt &list, const nlohmann::json &op, const exprt &elem) |
| Build a list.index(x) call — position of the first element equal to x. | |
| exprt | build_index_range_list_call (const symbolt &list, const nlohmann::json &op, const exprt &elem, const exprt &start, const exprt &end) |
| Build a list.index(x, start[, end]) call — position of the first element equal to x within the slice l[start:end]. | |
| exprt | build_count_index_list_call (const symbolt &list, const nlohmann::json &op, const exprt &elem, const std::string &func_id) |
Shared implementation of build_count_list_call / build_index_list_call; func_id selects the c:@F@__ESBMC_list_{count,index} model. | |
| exprt | build_set_membership_call (const symbolt &set, const nlohmann::json &op, const exprt &elem, const std::string &method_name) |
| Emit a call to a set membership-mutating C model function. | |
| BigInt | uniform_elem_size (const std::string &list_id) const |
The element byte width every recorded element of list_id shares, or 0 when there is no single answer. | |
| BigInt | uniform_elem_size (const exprt &list) const |
| Same, for a list reached as an expression: a non-symbol operand names no list to look up, so it has no single width and yields 0. | |
| typet | unrecorded_base_elem_type () |
| The element type a subscript's base declares when the type map has no record of the list: a name's annotation, or a called function's return annotation. | |
| typet | attribute_elem_type (const exprt &array) const |
The element type that a program class in the object's MRO annotates the instance-attribute list array with; empty when unannotated or nested. | |
| const element_type_registry::entries * | recorded_elem_types (const exprt &array) const |
The type map's record of array, or nullptr when it has none or is an annotated instance attribute. | |
| typet | attribute_elem_type_or_any (const exprt &array) const |
The element type of array's attribute annotation, or Any without one. | |
| bool | has_tagged_elements (const exprt &list) const |
| typet | tagged_elem_type_or (const exprt &array, bool constant_index, const nlohmann::json &list_node, const typet &fallback) const |
| The recorded element type when it is a tagged scalar and the index is not constant; otherwise the fallback (#7716 family). | |
| shallow_push_call | select_shallow_push (const exprt &src, const exprt &untagged_last_arg) const |
| Shallow-push entry point for a copy of src. | |
| shallow_push_call | select_list_extend (const exprt &src, const exprt &untagged_elem_size) const |
| list_eq_target | select_list_eq (const exprt &l1, const exprt &l2, const symbolt &generic_func, const std::vector< exprt > &generic_trailing_args) const |
| Equality entry point for l1 == l2 and the arguments that follow the two list operands. | |
| void | handle_list_var_unpacking (const nlohmann::json &ast_node, const nlohmann::json &target, const exprt &list_expr, codet &target_block) |
| Unpack a list variable into multiple targets, supporting starred expressions. | |
Static Public Member Functions | |
| static exprt | build_split_list (python_converter &converter, const nlohmann::json &call_node, const std::string &input, const std::string &separator, long long count, bool from_right=false) |
| static exprt | build_split_list (python_converter &converter, const nlohmann::json &call_node, const exprt &input_expr, const std::string &separator, long long count, bool from_right=false) |
| static bool | is_bool_mask_rows_type (const typet &type) |
True if type is a result struct built by build_bool_mask_row_select_symbolic (identified by its tag- prefix, mirroring tuple_handler::is_tuple_type). | |
| static exprt | axis_extent (const strided_axis &axis) |
| static exprt | axis_stride (const strided_axis &axis) |
| static view_contiguity | classify_view_contiguity (const strided_view_desc &view) |
| Whether a view covers its storage densely in row-major order. | |
| static exprt | build_list_from_range (python_converter &converter, const nlohmann::json &range_args, const nlohmann::json &element, bool materialise_elements=true) |
| Create a list from a range() call. | |
| static exprt | build_list_from_tuple (python_converter &converter, const exprt &tuple_expr, const nlohmann::json &element) |
| Materialise a tuple value into a fresh list, pushing each component in order. | |
Friends | |
| class | python_dict_handler |
|
strong |
|
inline |
| std::optional< exprt > python_list::alias_contiguous_ravel | ( | const nlohmann::json & | arg, |
| const strided_view_desc & | view ) |
Allocates the instance a constructor stores to lhs and returns the pointer to pass as self.
The element type that a program class in the object's MRO annotates the instance-attribute list array with; empty when unannotated or nested.
The element type of array's attribute annotation, or Any without one.
|
static |
|
static |
| typet python_list::bare_list_param_elem_type | ( | const nlohmann::json & | param_node, |
| const std::string & | param_id, | ||
| const typet & | annotated, | ||
| size_t | index ) |
Element type recovered for a bare list parameter, or a nil type.
A bare list annotation names no element type, so the read would carry none and neither arithmetic nor equality on it would behave.
Recover what the call sites told us about this parameter, seeded when the function was converted (#7187). Returns annotated unchanged when this is not a bare-list parameter, or nothing was inferred for it. Call sites that pass a list beside other types give each position its own type (#8472).
| exprt python_list::build_bool_mask_index | ( | const exprt & | array, |
| const exprt & | mask, | ||
| const nlohmann::json & | element ) |
Lower boolean-mask indexing a[mask] to a runtime loop that builds a fresh list holding the elements of array whose matching mask entry is True (NumPy fancy-indexing semantics).
Both operands must be fixed-size arrays (the numpy array model); a compile-time length mismatch between array and mask is rejected explicitly.
| array | Source 1-D array expression; multi-dimensional sources are rejected with TypeError at conversion time. |
| mask | Boolean array expression, same length as array. |
| element | The Subscript AST node, used for location info. |
| exprt python_list::build_bool_mask_row_select | ( | const exprt & | array, |
| const exprt & | mask, | ||
| const nlohmann::json & | element ) |
Lower whole-row boolean-mask selection a[mask] on a 2-D array.
The runtime-list model used by build_bool_mask_index cannot hold an array-typed element (confirmed empirically: pushing a row produces a bit-vector/array sort mismatch at the SMT backend), so this takes a different path: when mask resolves to a concrete boolean literal (np.array([True, False, ...])) whose declaring assignment is found via AST lookup, the selected row count is known at conversion time and the result is a fixed-size array, mirroring build_column_select. Otherwise (a symbolic/reassigned mask), it delegates to build_bool_mask_row_select_symbolic.
| array | Source 2-D array expression. |
| mask | Boolean mask array expression. |
| element | The Subscript AST node, used for location info and to recover the mask's variable name. |
| exprt python_list::build_bool_mask_row_select_symbolic | ( | const exprt & | array, |
| const exprt & | mask, | ||
| const nlohmann::json & | element ) |
Lower whole-row boolean-mask selection a[mask] on a 2-D array for a symbolic (non-literal) mask: the result is the canonical bounded descriptor shape — a worst-case-sized rows buffer (capacity == array's row count) plus a runtime count member holding the number of rows actually selected, so the logical size is part of the modelled value rather than a detached counter.
A single runtime while-loop scans mask once, copying each selected row (column by column, since whole-row assignment isn't valid GOTO) into the next free rows slot and incrementing count, preserving input order.
| array | Source 2-D array expression. |
| mask | Boolean mask array expression, same length as array's row count. |
| element | The Subscript AST node, used for location info. |
| exprt python_list::build_column_select | ( | const exprt & | array, |
| const nlohmann::json & | col_index_node, | ||
| const nlohmann::json & | element ) |
Lower 2-D column selection a[:, j] to a bounded copy over every row of a fixed-shape 2-D array, collecting row[j] into a fresh 1-D array.
array must be a fixed-size array of fixed-size rows (numpy static-shape model); anything else is rejected with TypeError.
| array | Source 2-D array expression. |
| col_index_node | AST node for the column index (axis 1). |
| element | The Subscript AST node, used for location info. |
| exprt python_list::build_concat_list_call | ( | const exprt & | lhs, |
| const exprt & | rhs, | ||
| const nlohmann::json & | element ) |
Build a list copy operation.
| list | The list symbol to copy from |
| element | The AST node for location information |
| exprt python_list::build_count_list_call | ( | const symbolt & | list, |
| const nlohmann::json & | op, | ||
| const exprt & | elem ) |
Build a list.count(x) call — number of elements equal to x.
Returns a size_t-typed value expression.
| std::optional< exprt > python_list::build_element_replacement | ( | const exprt & | lhs, |
| const exprt & | rhs, | ||
| const nlohmann::json & | op ) |
The __ESBMC_list_set_at call storing rhs into the list element lhs reads, when store_replaces_element holds; nullopt otherwise.
| exprt python_list::build_extend_list_call | ( | const symbolt & | list, |
| const nlohmann::json & | op, | ||
| const exprt & | other_list ) |
| exprt python_list::build_fancy_index | ( | const exprt & | array, |
| const std::vector< nlohmann::json > & | indices, | ||
| const nlohmann::json & | element ) |
Lower integer-array (fancy) indexing a[[0, 2]] to a bounded, unrolled sequence of element reads: each entry of indices must be a concrete integer literal (or its negation), resolved and bounds-checked at conversion time.
array must be a fixed-size 1-D or 2-D array; for 2-D arrays the selected rows are copied element-by-element. A 3-D+ element type (i.e. array itself being 3-D+) is rejected with TypeError, since a deeper row would require a recursive element-wise copy this helper does not implement.
| array | Source fixed-shape (1-D or 2-D) array expression. |
| indices | AST nodes for each requested index (elts of the List literal used as the subscript). |
| element | The Subscript AST node, used for location info. |
| exprt python_list::build_index_list_call | ( | const symbolt & | list, |
| const nlohmann::json & | op, | ||
| const exprt & | elem ) |
Build a list.index(x) call — position of the first element equal to x.
Raises ValueError (via assertion) if x is not found. Returns a size_t-typed value expression.
| exprt python_list::build_index_range_list_call | ( | const symbolt & | list, |
| const nlohmann::json & | op, | ||
| const exprt & | elem, | ||
| const exprt & | start, | ||
| const exprt & | end ) |
Build a list.index(x, start[, end]) call — position of the first element equal to x within the slice l[start:end].
start/end follow CPython slice-bound normalization. Raises ValueError (via assertion) if not found.
| exprt python_list::build_insert_list_call | ( | const symbolt & | list, |
| const exprt & | index, | ||
| const nlohmann::json & | op, | ||
| const exprt & | elem ) |
Whether list was built by tuple(x) (#8777).
Materialize a fresh list from already-evaluated element values.
Unlike get(), which converts AST element nodes, this builds the list from exprt values directly — used to emit the result of a frontend-computed sort over tuples, where each element is a conditional (ite) selection over the input elements. Records each element's type in the type map so later subscripting recovers the element type. The constructor's list_value_ node supplies the source location.
|
static |
Create a list from a range() call.
| converter | The python converter instance |
| range_args | The arguments to range() (1-3 arguments: stop, or start+stop, or start+stop+step) |
| element | The AST node for location information |
| std::runtime_error | if range parameters are invalid or too large |
|
static |
Materialise a tuple value into a fresh list, pushing each component in order.
Used by list(tuple) (and any context that converts a tuple to a list), so the list model sees a real PyListObject* rather than the tuple struct. tuple_expr must have tuple struct type.
| void python_list::build_mark_tuple_call | ( | const exprt & | list | ) |
Mark list as built by tuple(x) (#8777).
| exprt python_list::build_min_max_for_mixed_numeric | ( | const exprt & | list_arg, |
| const std::string & | list_id, | ||
| const std::string & | func_name, | ||
| irep_idt | comparison_op ) |
Build an inline min/max computation for a mixed int/float list.
Accesses each element with its original type, promotes int elements to double for comparison, and returns the winning value as double.
Note: Python's min/max returns the winning element in its original type (e.g., max([1, 2.5, 3]) returns int 3, not float 3.0). This implementation always returns double, which is correct for float comparisons and equality checks (via float promotion in handle_relational_type_mismatches), but will not work if the result is used as an array index or integer operand.
| list_arg | Expression for the list symbol |
| list_id | Symbol identifier of the list |
| func_name | "min" or "max" (used in error messages) |
| comparison_op | exprt::i_gt for max, exprt::i_lt for min |
| exprt python_list::build_mixed_slice_tuple_select | ( | const exprt & | array, |
| const std::vector< nlohmann::json > & | idx_nodes, | ||
| const nlohmann::json & | element ) |
Lower an N-D mixed slice/index tuple subscript with one or more bounded slice axes and fixed-index axes, e.g.
a[:, 0, 0], a[0:2, 0, 0], or a[:, :, 0] on a 3-D array. Slice bounds are resolved at conversion time, and the selected scalar cells are copied into a fresh fixed-shape result.
| array | Source N-D array expression. |
| idx_nodes | One AST node per axis, in order; at least one must be a slice and every non-slice node is treated as a fixed index. |
| element | The Subscript AST node, used for location info. |
| exprt python_list::build_pop_list_call | ( | const symbolt & | list, |
| const exprt & | index, | ||
| const nlohmann::json & | element ) |
Build a list pop operation.
| list | The list symbol to pop from |
| index | The index to pop (default -1 for last element) |
| element | The AST node for location information |
| exprt python_list::build_push_list_call | ( | const symbolt & | list, |
| const nlohmann::json & | op, | ||
| const exprt & | elem, | ||
| bool | enable_float_path = true ) |
| exprt python_list::build_remove_list_call | ( | const symbolt & | list, |
| const nlohmann::json & | op, | ||
| const exprt & | elem ) |
Build a list remove operation (removes first matching element).
Raises ValueError (via assertion) if element is not found.
| exprt python_list::build_set_membership_call | ( | const symbolt & | set, |
| const nlohmann::json & | op, | ||
| const exprt & | elem, | ||
| const std::string & | method_name ) |
Emit a call to a set membership-mutating C model function.
Used to implement set.add() and set.discard(): both wrap the same C argument layout (set, &elem, type_id, size) returning bool. The method_name selects between "add" and "discard"; the dispatcher resolves it to "__ESBMC_set_add" / "__ESBMC_set_discard".
| exprt python_list::build_shallow_copy_call | ( | const exprt & | src_list, |
| const nlohmann::json & | element ) |
Emit a __ESBMC_list_copy_shallow call producing a shallow copy of src_list (Python copy semantics: scalar elements get independent buffers, nested containers stay shared).
Used by tuple(list), which must snapshot the source so later list mutations do not show through the tuple.
| src_list | List-typed expression (symbol or list-returning call) |
| element | AST node used for location info and temp naming |
|
static |
|
static |
| exprt python_list::build_strided_column_select | ( | const exprt & | array, |
| const nlohmann::json & | col_slice_node, | ||
| const nlohmann::json & | element ) |
Lower a strided column slice a[:, start:stop:step] on a fixed-shape 2-D array: the literal slice bounds are resolved at conversion time and each selected column is copied into a fresh 2-D result.
Bare negative steps other than -1 are still rejected because their result width would differ from the old full-reversal path.
| array | Source 2-D array expression. |
| col_slice_node | AST Slice node for the column axis (axis 1); its step, lower, and upper must be literal integers when present. |
| element | The Subscript AST node, used for location info. |
| exprt python_list::build_symbolic_fill_list | ( | const exprt & | size, |
| const exprt & | fill_value, | ||
| const typet & | elem_type, | ||
| const exprt * | index_base = nullptr ) |
Build a runtime PyListObject filled with fill_value repeated size times.
size may be a symbolic expression; the resulting while- loop is bounded by the model checker's –unwind setting. A runtime guard rejects negative sizes with ValueError before the unsigned cast.
| size | Expression giving the number of elements (often symbolic). |
| fill_value | Element value pushed on each iteration. |
| elem_type | IRep2 type of fill_value, recorded in the registry. |
| index_base | When non-null, each element is index_base plus the loop index rather than fill_value, which is what a range needs. |
np.trace(a, offset=k): sum of the elements np.diagonal(a, k) would view, computed directly as a scalar reduction (no view is built).
Public for the same reason as try_build_diagonal_pointer_view. Declines for a non-symbol/non-numpy-tracked source or a source that isn't a fixed-shape 2-D array.
| array | Source 2-D array expression. |
| k | Literal diagonal offset (0 = main diagonal). |
tuple(x) of a list: a shallow copy marked as a tuple (#8777).
|
static |
Whether a view covers its storage densely in row-major order.
| std::optional< python_list::strided_view_desc > python_list::contiguous_view_desc | ( | const exprt & | array, |
| const typet & | elem_type, | ||
| const std::vector< std::size_t > & | shape ) const |
| exprt python_list::copy_strided_view | ( | const strided_view_desc & | source, |
| const exprt & | offset, | ||
| const std::vector< strided_axis > & | axes, | ||
| const std::vector< std::size_t > * | out_shape = nullptr ) |
Independent array holding the elements a view with these axes reads, in row-major order.
out_shape (constant axes only) lays them out in another shape of the same size.
| std::optional< python_list::strided_view_desc > python_list::describe_strided_view | ( | const exprt & | array | ) |
| void python_list::emit_counted_loop | ( | const nlohmann::json & | node, |
| const exprt & | extent, | ||
| const std::function< void(const exprt &)> & | body ) |
idx = 0; while (idx < extent) { body(idx); idx++; }, with the body's statements emitted inside the loop.
| exprt python_list::emit_ll_temp | ( | const nlohmann::json & | node, |
| const char * | name, | ||
| const exprt & | value ) |
Signed 64-bit temporary holding value, assigned once here.
| void python_list::emit_reshape_size_guard | ( | const nlohmann::json & | arg, |
| const exprt & | count, | ||
| const std::vector< std::size_t > & | new_shape ) |
| exprt python_list::emit_view_accumulator | ( | const nlohmann::json & | arg, |
| const typet & | type, | ||
| const exprt & | init ) |
| exprt python_list::emit_view_copy_buffer | ( | const nlohmann::json & | arg, |
| const strided_view_desc & | view, | ||
| const exprt & | count ) |
| void python_list::emit_view_loops | ( | const nlohmann::json & | node, |
| const strided_view_desc & | view, | ||
| const std::function< void(const exprt &)> & | leaf ) |
Nested loops over every index of a view; leaf is called once, inside the innermost body, with the element lvalue.
| size_t python_list::eq_float_type_id | ( | const std::string & | lhs_id, |
| const std::string & | rhs_id ) const |
The float element type_id that lets list_eq compare mixed int and float elements numerically (Python's 1 == 1.0), merged from both operands.
| exprt python_list::extract_pyobject_value | ( | const exprt & | pyobject_expr, |
| const typet & | elem_type, | ||
| bool | mixed_numeric = false, | ||
| bool | string_safe = false ) |
Extract and dereference value from a PyObject* expression.
| pyobject_expr | Expression representing PyObject* (from list_at or list_pop) |
| elem_type | The expected element type |
| mixed_numeric | When true and elem_type is float, the element may be either an int or a float at runtime (a dynamic index into a mixed int/float list). The float value is then read by dispatching on the stored type_id: float elements come from __ESBMC_float_buf, int elements are promoted from their payload to double. |
| std::optional< expr2tc > python_list::fast_elem_equality | ( | exprt | lhs_val, |
| exprt | rhs_val, | ||
| const typet & | lhs_type, | ||
| const typet & | rhs_type ) const |
Equality of two list elements read as lhs_type and rhs_type for compare()'s fast path, or nullopt when it cannot relate them.
Both types are numeric, bool or tuple.
| std::optional< flat_array_shape_info > python_list::flat_shape_info_of | ( | const exprt & | array | ) | const |
Total element count and scalar element type of a fixed-shape array of any rank, or of a contiguous N-D subarray view.
| exprt python_list::get | ( | ) |
| exprt python_list::get_empty_set | ( | ) |
Create an empty set.
| void python_list::guard_pop_index | ( | const symbolt & | list, |
| const exprt & | index, | ||
| const locationt & | location ) |
Inside a try body, raises a catchable IndexError ahead of a pop() whose list is empty or whose index is out of range, before __ESBMC_list_pop asserts it.
| exprt python_list::handle_comprehension | ( | const nlohmann::json & | element | ) |
Convert generator expressions and list comprehensions to lists.
| element | The GeneratorExp or ListComp AST node |
| void python_list::handle_list_var_unpacking | ( | const nlohmann::json & | ast_node, |
| const nlohmann::json & | target, | ||
| const exprt & | list_expr, | ||
| codet & | target_block ) |
Unpack a list variable into multiple targets, supporting starred expressions.
Handles assignments like a, *b, c = lst where lst is a list variable. Uses __ESBMC_list_at for element access and builds a new list for the starred target.
| ast_node | The assignment AST node (for location info and value["id"]) |
| target | The tuple/list target node containing the target variables |
| list_expr | The expression representing the source list (pointer type) |
| target_block | The code block to append assignment instructions to |
| void python_list::handle_slice_assignment | ( | const exprt & | list_expr, |
| const nlohmann::json & | slice_node, | ||
| const nlohmann::json & | value_node ) |
Lower a list slice assignment l[lower:upper:step] = value to a __ESBMC_list_slice_assign model call.
The step must be a constant literal (or absent); the value must evaluate to a list.
| list_expr | Expression for the target list (value or pointer) |
| slice_node | The Slice AST node holding lower/upper/step |
| value_node | The AST node of the assigned (right-hand side) value |
| void python_list::handle_subscript_assign_none | ( | const exprt & | list_expr, |
| const nlohmann::json & | slice_node ) |
Whether a list slot holding type may share its payload with a copy of the list: list copies keep the PyObject record of a non-scalar element verbatim (#5102), so a store must not write through it.
| exprt python_list::index_bool_mask_rows | ( | const exprt & | array, |
| const nlohmann::json & | slice_node, | ||
| const nlohmann::json & | element ) |
Index b[i] into a boolean-mask row-selection result (see build_bool_mask_row_select_symbolic): normalizes a negative slice_node index against the struct's runtime count member (not the rows buffer's physical capacity), bounds-checks it against count (raising IndexError out of bounds, mirroring build_list_at_call), and returns the selected row.
| array | The boolean-mask row-selection result expression. |
| slice_node | AST node for the row index (a plain integer index; slicing is not supported). |
| element | The Subscript AST node, used for location info. |
| bool python_list::index_strided_axis | ( | const strided_axis & | source, |
| const nlohmann::json & | node, | ||
| exprt & | offset ) |
| typet python_list::infer_literal_element_type | ( | const nlohmann::json & | list_literal | ) |
Infer the element type of a list literal AST node, accounting for the int->float promotion applied at construction.
A heterogeneous int/float literal is promoted to a homogeneous double list in python_list::get (promote_ints, #5156), so its values all live in __ESBMC_float_buf as doubles. A read of such a literal must therefore use a float element type whatever element the index selects; using the first element's (int) type misreads the stored double's bits (#5160 regression).
True if type is a result struct built by build_bool_mask_row_select_symbolic (identified by its tag- prefix, mirroring tuple_handler::is_tuple_type).
| bool python_list::is_runtime_numpy_slice | ( | const exprt & | array, |
| const typet & | elem_type, | ||
| const nlohmann::json & | slice_node ) const |
| exprt python_list::list_repetition | ( | const nlohmann::json & | left_node, |
| const nlohmann::json & | right_node, | ||
| const exprt & | lhs, | ||
| const exprt & | rhs ) |
| std::vector< exprt > python_list::literal_elems_for_variable_list | ( | const nlohmann::json * | source_node, |
| const exprt & | source_list ) |
The declaring literal's elements for a variable-held list, or empty when the literal cannot be used.
The declaring literal's elements for a list held in a variable, or empty when the literal cannot be used – it does not exist, or the list has been mutated since and the literal no longer describes it.
| bool python_list::literal_still_describes_list | ( | const exprt & | source_list, |
| size_t | literal_elem_count ) |
True when a list's declaring literal still describes its contents.
True when the declaring literal still describes the list's contents.
xs * n expands the literal's elements at convert time, which is wrong once the list has been mutated: after xs = [1, 2, 3]; xs += [4] the literal still has three elements, and the repetition silently produced a six-element result where Python gives eight. The recorded element types track every push, so a length mismatch means the literal is stale and the caller must build from those records instead.
| bool python_list::mixes_list_and_other | ( | const std::string & | id | ) | const |
True when the recorded elements of id mix a list with another type.
| std::vector< python_list::strided_axis > python_list::owned_copy_axes | ( | const nlohmann::json & | arg, |
| const strided_view_desc & | view, | ||
| bool | flatten, | ||
| const exprt & | count ) |
| void python_list::record_element_store | ( | const nlohmann::json & | subscript, |
| const std::string & | elem_id, | ||
| const typet & | elem_type ) |
Records elem_type as the type of the element subscript stores to.
| const element_type_registry::entries * python_list::recorded_elem_types | ( | const exprt & | array | ) | const |
The type map's record of array, or nullptr when it has none or is an annotated instance attribute.
| std::optional< exprt > python_list::reduce_view_argextreme | ( | const std::string & | function, |
| const nlohmann::json & | arg ) |
sum / mean / min / max / any / all of a run-time-extent view, as loops.
| exprt python_list::reduce_view_extreme | ( | const std::string & | function, |
| const nlohmann::json & | arg, | ||
| const strided_view_desc & | view, | ||
| const exprt & | count ) |
| exprt python_list::reduce_view_truth | ( | bool | is_any, |
| const nlohmann::json & | arg, | ||
| const strided_view_desc & | view ) |
| exprt python_list::register_strided_view | ( | const strided_view_desc & | source, |
| const exprt & | offset, | ||
| const std::vector< strided_axis > & | axes, | ||
| bool | readonly = false ) |
base + offset as a registered view with these axes for the assignment target (offset is a size_type element count).
| void python_list::reject_mixed_member_element_read | ( | const exprt & | array, |
| const nlohmann::json & | slice_node ) const |
Refuses an index other than a non-negative constant into a list attribute whose recorded elements have different types (#8666).
A list attribute such as self.tab has no symbol of its own, so its element types are recorded under the empty id.
An index other than a non-negative constant reads element 0's type, which misreads every element of another type (#8666).
| void python_list::reject_unresolved_element_read | ( | const exprt & | array, |
| const nlohmann::json & | slice_node ) const |
Refuses a read that no single recorded element type answers (#8472).
A list whose elements mix a list with another type is read at one element's type only when the index is a constant and every list element carries its own id, which the call-site seeding gives a position it resolved.
Any other read would pick one type for elements of several, so it is refused rather than misread (#8472).
| void python_list::require_stored_types | ( | expr2tc & | sizes_ok, |
| std::size_t | depth, | ||
| const exprt & | lhs_at, | ||
| const typet & | lhs_type, | ||
| const exprt & | rhs_at, | ||
| const typet & | rhs_type ) const |
Conjoins to sizes_ok that the slots lhs_at and rhs_at hold lhs_type and rhs_type, for compare()'s nested fast path.
Only a top-level scalar slot is exempt: any other slot was typed through a nested list the type map may name by a dead or rebound symbol (#8130).
| void python_list::reshape_registered_copy | ( | const std::string & | lhs_id, |
| const std::vector< std::size_t > & | new_shape ) |
Turn the store lhs = rhs into a replacement of the element record when the value cannot be written through the element's type.
lhs is the subscript target *(T *)item->value of the list subscript this handler was built for. When rhs is a tuple of another type than T (or T is a tuple and rhs is not), or T is a non-scalar a list copy may share, the pair is rewritten into *item = *list_at(tmp, 0), with tmp a list holding rhs, so the slot gets the new value, type_id and size. Otherwise both are left unchanged.
| std::optional< python_list::strided_axis > python_list::runtime_slice_axis | ( | const strided_axis & | source, |
| const nlohmann::json & | node, | ||
| exprt & | offset ) |
| exprt python_list::scalar_storage_pointer | ( | const exprt & | array, |
| const typet & | scalar_ptr_type ) const |
array's storage as a pointer to its scalar element type.
| void python_list::scale_split_axis_strides | ( | const nlohmann::json & | arg, |
| const strided_axis & | source, | ||
| std::vector< strided_axis > & | axes ) |
| python_list::list_eq_target python_list::select_list_eq | ( | const exprt & | l1, |
| const exprt & | l2, | ||
| const symbolt & | generic_func, | ||
| const std::vector< exprt > & | generic_trailing_args ) const |
Equality entry point for l1 == l2 and the arguments that follow the two list operands.
A tagged element has no single static width and cannot hold a nested list, so neither elem_size nor the depth stack applies (#7723).
| python_list::shallow_push_call python_list::select_list_extend | ( | const exprt & | src, |
| const exprt & | untagged_elem_size ) const |
| python_list::shallow_push_call python_list::select_shallow_push | ( | const exprt & | src, |
| const exprt & | untagged_last_arg ) const |
Shallow-push entry point for a copy of src.
A list of tagged scalars needs the bounded-copy variant, which reads its trailing argument as a float_type_id rather than as an element width (#7716).
| std::optional< python_list::strided_axis > python_list::slice_strided_axis | ( | const strided_axis & | source, |
| const nlohmann::json & | node, | ||
| exprt & | offset ) |
Whether storing a new_type value into an element read as old_type replaces the element rather than writing into its storage.
| bool python_list::strided_basic_view_declines | ( | const exprt & | array, |
| const std::vector< nlohmann::json > & | idx_nodes, | ||
| bool | allow_plain_array ) const |
| exprt python_list::strided_index_offset | ( | const strided_view_desc & | src, |
| const std::vector< nlohmann::json > & | indices ) |
| std::optional< python_list::strided_view_desc > python_list::symbolic_view_operand | ( | const nlohmann::json & | arg | ) |
The descriptor of the named view when its extents or strides are known only at run time; nullopt for anything else.
| typet python_list::tagged_elem_type_or | ( | const exprt & | array, |
| bool | constant_index, | ||
| const nlohmann::json & | list_node, | ||
| const typet & | fallback ) const |
The recorded element type when it is a tagged scalar and the index is not constant; otherwise the fallback (#7716 family).
The list's recorded element type when it is a tagged scalar and the index is not constant, else fallback unchanged.
Kept out of handle_index_access so the dispatch adds no decision point to it.
| std::vector< python_list::strided_axis > python_list::tracked_view_axes | ( | const std::string & | view_id | ) | const |
Axes of the pointer view registered under view_id.
| std::optional< exprt > python_list::try_build_diagonal_pointer_view | ( | const exprt & | array, |
| long long | k ) |
np.diagonal(a[, offset=k])/a.diagonal([k]): a read-only strided pointer view into a's own buffer (ADR-NP-003 etapa 2).
Public so numpy_call_expr.cpp's Call dispatch (where the offset/axis1/axis2 argument parsing lives) can build it directly. Declines (returns std::nullopt) for a non-symbol/non-numpy-tracked source or a source that isn't a fixed-shape 2-D array (including 3-D+). When current_lhs is unset (the type-inference pre-pass that runs before the real d symbol exists), returns a same-typed placeholder pointer instead of declining, so that pass can read a type and complete – the real, current_lhs-correct view is built on the unconditional second pass that follows for a Call RHS.
| array | Source 2-D array expression. |
| k | Literal diagonal offset (0 = main diagonal). |
| bool python_list::try_build_fill_diagonal_mutation | ( | const exprt & | array, |
| const nlohmann::json & | value_node ) |
np.fill_diagonal(a, value): mutates a's main diagonal in place via converter_.add_instruction, using the same offset/stride math as try_build_diagonal_pointer_view/build_trace_reduction with k=0.
value is either a scalar expression or a List literal whose length must equal the diagonal's exactly (throws ValueError otherwise, matching NumPy's own broadcasting rule for a 1-D val). Public for the same reason as try_build_diagonal_pointer_view. Declines (returns false) for a non-symbol/non-numpy-tracked source or a source that isn't a fixed-shape 2-D array.
| array | Source 2-D array expression. |
| value_node | Raw AST node for the value argument. |
| std::optional< exprt > python_list::try_build_flat_index_assignment_target | ( | const exprt & | array, |
| const nlohmann::json & | index_node ) |
a.flat[i] = x: builds a dereferenced-pointer lvalue into a's own buffer at flat index i (bounds-checked and negative-index-normalized the same way a registered pointer view's index is), for a fixed-shape 1-D or 2-D array – the same eligibility and offset/stride=1 math as try_build_ravel_pointer_view, but built inline for an assignment target that has no intermediate bare-name view symbol to register into numpy_pointer_view_info_.
Declines (returns std::nullopt) for a non-symbol/non-numpy-tracked source or a source that isn't fixed-shape 1-D/2-D (including 3-D+).
| array | Source 1-D or 2-D array expression. |
| index_node | Raw AST node for the flat index expression. |
| std::optional< exprt > python_list::try_build_numpy_param_slice_view | ( | const exprt & | array, |
| const typet & | resolved_array_type, | ||
| const nlohmann::json & | slice_node ) |
np.ravel(a)/a.ravel(): a writable, contiguous strided pointer view into a's own buffer (ADR-NP-003 etapa 2), for a fixed-shape 1-D or 2-D array.
Public for the same reason as try_build_diagonal_pointer_view. Declines (returns std::nullopt) for a non-symbol/non-numpy-tracked source, a source that isn't fixed-shape 1-D/2-D (including 3-D+), or an unassigned RHS (current_lhs unset) outside the discardable type-inference pre-pass – same current_lhs/in_rhs_type_probe_ handling as try_build_diagonal_pointer_view, for the same reason.
| array | Source 1-D or 2-D array expression. |
| std::optional< exprt > python_list::try_build_strided_basic_view | ( | const exprt & | array, |
| const std::vector< nlohmann::json > & | idx_nodes, | ||
| bool | allow_plain_array = false ) |
v = a[i, :, 1:3, ...] over a rank-3+ array or any N-D view, with literal or run-time indices and slice bounds: a view into the source's own storage (aliasing in both directions) when assigned to a bare name, otherwise an independent copy.
Declines for anything else.
| std::optional< exprt > python_list::try_build_strided_view_index | ( | const nlohmann::json & | element | ) |
b[i][j], b[i, j] or x = b[i] over a registered N-D strided view.
| std::optional< exprt > python_list::try_build_symbolic_view_list | ( | const nlohmann::json & | arg, |
| bool | nested ) |
A Python list of a run-time-extent view's elements (nested per axis when nested, flat otherwise).
| std::optional< exprt > python_list::try_copy_symbolic_view | ( | const nlohmann::json & | arg, |
| bool | flatten = false, | ||
| bool | alias_if_contiguous = false ) |
np.copy / np.array / .copy of a run-time-extent view.
| std::optional< exprt > python_list::try_reduce_symbolic_view | ( | const std::string & | function, |
| const nlohmann::json & | arg ) |
| std::optional< exprt > python_list::try_reshape_symbolic_view | ( | const nlohmann::json & | arg, |
| const std::vector< std::size_t > & | new_shape ) |
reshape of a run-time-extent view to constant new_shape: an alias when it is contiguous, a copy otherwise; ValueError if the sizes differ.
Same, for a list reached as an expression: a non-symbol operand names no list to look up, so it has no single width and yields 0.
| BigInt python_list::uniform_elem_size | ( | const std::string & | list_id | ) | const |
The element byte width every recorded element of list_id shares, or 0 when there is no single answer.
The list models apply one copy length to every element, so a width is only usable when all of them agree. Scalars and tuples have one, both being stored inline; a pointer-stored element (a nested list, a dict) and mixed widths yield 0, which keeps the model on its symbolic o->size path. Distinct from build_shallow_copy_call, which reads only the last type-map entry.
| std::optional< exprt > python_list::unnamed_nd_view_placeholder | ( | const strided_view_desc & | view, |
| bool | as_view, | ||
| bool | flat_result, | ||
| const char * | unnamed_error ) const |
| typet python_list::unrecorded_base_elem_type | ( | ) |
The element type a subscript's base declares when the type map has no record of the list: a name's annotation, or a called function's return annotation.
Empty when neither gives one.
| exprt python_list::view_element | ( | const strided_view_desc & | view, |
| const std::vector< exprt > & | index ) const |
Element lvalue of a view at a signed 64-bit multi-index.
| exprt python_list::view_element_count | ( | const nlohmann::json & | node, |
| const strided_view_desc & | view ) |
|
friend |
1.15.0