docs/api/python__list_8h_source.html

#pragma once


#include <irep2/irep2.h>

#include <nlohmann/json.hpp>

#include <python-frontend/type/element_type_registry.h>

#include <util/irep/type.h>

#include <util/irep/expr.h>

#include <util/irep/std_expr.h>

#include <util/symtab/symbol.h>

#include <functional>

#include <optional>

#include <set>

#include <utility>


class exprt;

class symbolt;

class python_converter;

class type_handler;

class codet;


struct list_elem_info

{

  symbolt *elem_type_sym;

  symbolt *elem_symbol;

  exprt elem_size;

  locationt location;

};


struct flat_array_shape_info

{

  typet elem_type;

  long long total_length;

};


class python_list

{

public:


  python_list(python_converter &converter, const nlohmann::json &list)

    : converter_(converter), list_value_(list)

  {

  }


  // @p from_right selects rsplit() semantics (split at the rightmost @p count

  // separators) over split() (the leftmost). Defaults to split().

  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);


  exprt get();


  exprt build_list_from_exprs(const std::vector<exprt> &elems);


  exprt build_symbolic_fill_list(

    const exprt &size,

    const exprt &fill_value,

    const typet &elem_type,

    const exprt *index_base = nullptr);


  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);


  exprt build_bool_mask_row_select(

    const exprt &array,

    const exprt &mask,

    const nlohmann::json &element);


  exprt build_bool_mask_row_select_symbolic(

    const exprt &array,

    const exprt &mask,

    const nlohmann::json &element);


  static bool is_bool_mask_rows_type(const typet &type);


  exprt index_bool_mask_rows(

    const exprt &array,

    const nlohmann::json &slice_node,

    const nlohmann::json &element);


  exprt build_column_select(

    const exprt &array,

    const nlohmann::json &col_index_node,

    const nlohmann::json &element);


  exprt build_strided_column_select(

    const exprt &array,

    const nlohmann::json &col_slice_node,

    const nlohmann::json &element);


  std::optional<exprt>

  try_build_diagonal_pointer_view(const exprt &array, long long k);


  std::optional<exprt> build_trace_reduction(const exprt &array, long long k);


  bool try_build_fill_diagonal_mutation(

    const exprt &array,

    const nlohmann::json &value_node);


  std::optional<exprt> try_build_ravel_pointer_view(const exprt &array);


  struct strided_axis

  {

    long long extent = 0;

    exprt extent_expr = nil_exprt();

    long long stride = 0;

    exprt stride_expr = nil_exprt();


    bool symbolic() const

    {

      return extent_expr.is_not_nil() || stride_expr.is_not_nil();

    }


  };


  struct strided_view_desc

  {

    exprt base;

    typet elem_type;

    std::vector<strided_axis> axes;

    bool readonly = false;

  };


  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;


  exprt register_strided_view(

    const strided_view_desc &source,

    const exprt &offset,

    const std::vector<strided_axis> &axes,

    bool readonly = false);


  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);


  static exprt axis_extent(const strided_axis &axis);

  static exprt axis_stride(const strided_axis &axis);


  std::optional<strided_view_desc>

  symbolic_view_operand(const nlohmann::json &arg);


  exprt view_element(

    const strided_view_desc &view,

    const std::vector<exprt> &index) const;


  void emit_counted_loop(

    const nlohmann::json &node,

    const exprt &extent,

    const std::function<void(const exprt &)> &body);


  void emit_view_loops(

    const nlohmann::json &node,

    const strided_view_desc &view,

    const std::function<void(const exprt &)> &leaf);


  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);

  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);


  enum class view_contiguity

  {

    contiguous,

    not_contiguous,

    unknown // depends on a run-time stride

  };


  static view_contiguity

  classify_view_contiguity(const strided_view_desc &view);


  std::optional<exprt> try_reshape_symbolic_view(

    const nlohmann::json &arg,

    const std::vector<std::size_t> &new_shape);


  std::optional<exprt> try_copy_symbolic_view(

    const nlohmann::json &arg,

    bool flatten = false,

    bool alias_if_contiguous = false);


  exprt emit_ll_temp(

    const nlohmann::json &node,

    const char *name,

    const exprt &value);


  std::optional<exprt> try_build_strided_basic_view(

    const exprt &array,

    const std::vector<nlohmann::json> &idx_nodes,

    bool allow_plain_array = false);


  std::optional<exprt>

  try_build_strided_view_index(const nlohmann::json &element);


  std::optional<flat_array_shape_info>

  flat_shape_info_of(const exprt &array) const;


  std::optional<exprt> build_contiguous_shaped_view(

    const exprt &array,

    const std::vector<std::size_t> &shape,

    std::size_t offset,

    bool readonly);


  exprt scalar_storage_pointer(const exprt &array, const typet &scalar_ptr_type)

    const;


  std::optional<exprt> try_build_flat_index_assignment_target(

    const exprt &array,

    const nlohmann::json &index_node);


  exprt build_mixed_slice_tuple_select(

    const exprt &array,

    const std::vector<nlohmann::json> &idx_nodes,

    const nlohmann::json &element);


  exprt build_fancy_index(

    const exprt &array,

    const std::vector<nlohmann::json> &indices,

    const nlohmann::json &element);


  void handle_slice_assignment(

    const exprt &list_expr,

    const nlohmann::json &slice_node,

    const nlohmann::json &value_node);


  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;

  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);


  bool has_shared_payload(const typet &type) const;


  exprt allocate_constructed_object(const exprt &lhs);


  void record_element_store(

    const nlohmann::json &subscript,

    const std::string &elem_id,

    const typet &elem_type);


  std::optional<expr2tc> fast_elem_equality(

    exprt lhs_val,

    exprt rhs_val,

    const typet &lhs_type,

    const typet &rhs_type) const;


  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;


  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);


  // Build: result = lhs + rhs   (concatenation)

  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);


  bool literal_still_describes_list(

    const exprt &source_list,

    size_t literal_elem_count);


  typet bare_list_param_elem_type(

    const nlohmann::json &param_node,

    const std::string &param_id,

    const typet &annotated,

    size_t index);


  bool mixes_list_and_other(const std::string &id) const;


  void reject_unresolved_element_read(

    const exprt &array,

    const nlohmann::json &slice_node) const;


  void reject_mixed_member_element_read(

    const exprt &array,

    const nlohmann::json &slice_node) const;


  exprt get_empty_set();


  exprt handle_comprehension(const nlohmann::json &element);


  exprt build_pop_list_call(

    const symbolt &list,

    const exprt &index,

    const nlohmann::json &element);


  void guard_pop_index(

    const symbolt &list,

    const exprt &index,

    const locationt &location);


  bool

  store_replaces_element(const typet &old_type, const typet &new_type) const;


  std::optional<exprt> build_element_replacement(

    const exprt &lhs,

    const exprt &rhs,

    const nlohmann::json &op);


  exprt extract_pyobject_value(

    const exprt &pyobject_expr,

    const typet &elem_type,

    bool mixed_numeric = false,

    bool string_safe = false);


  typet infer_literal_element_type(const nlohmann::json &list_literal);


  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);


  static exprt build_list_from_range(

    python_converter &converter,

    const nlohmann::json &range_args,

    const nlohmann::json &element,

    bool materialise_elements = true);


  static exprt build_list_from_tuple(

    python_converter &converter,

    const exprt &tuple_expr,

    const nlohmann::json &element);


  exprt

  build_copy_list_call(const symbolt &list, const nlohmann::json &element);


  exprt

  build_shallow_copy_call(const exprt &src_list, const nlohmann::json &element);


  exprt

  build_tuple_copy_call(const exprt &src_list, const nlohmann::json &element);


  void build_mark_tuple_call(const exprt &list);


  exprt build_is_tuple_call(const exprt &list);


  exprt build_remove_list_call(

    const symbolt &list,

    const nlohmann::json &op,

    const exprt &elem);


  exprt build_count_list_call(

    const symbolt &list,

    const nlohmann::json &op,

    const exprt &elem);


  exprt build_index_list_call(

    const symbolt &list,

    const nlohmann::json &op,

    const exprt &elem);


  exprt build_index_range_list_call(

    const symbolt &list,

    const nlohmann::json &op,

    const exprt &elem,

    const exprt &start,

    const exprt &end);


  exprt build_count_index_list_call(

    const symbolt &list,

    const nlohmann::json &op,

    const exprt &elem,

    const std::string &func_id);


  exprt build_set_membership_call(

    const symbolt &set,

    const nlohmann::json &op,

    const exprt &elem,

    const std::string &method_name);


  BigInt uniform_elem_size(const std::string &list_id) const;


  BigInt uniform_elem_size(const exprt &list) const;


  typet unrecorded_base_elem_type();


  typet attribute_elem_type(const exprt &array) const;


  const element_type_registry::entries *

  recorded_elem_types(const exprt &array) const;


  typet attribute_elem_type_or_any(const exprt &array) const;


  // True when the list's recorded element types include a tagged scalar, whose

  // payload width is per-element and symbolic (#7716).

  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;


  struct shallow_push_call

  {

    const symbolt *func;

    exprt last_arg;

  };


  shallow_push_call

  select_shallow_push(const exprt &src, const exprt &untagged_last_arg) const;


  shallow_push_call

  select_list_extend(const exprt &src, const exprt &untagged_elem_size) const;


  struct list_eq_target

  {

    const symbolt *func;

    std::vector<exprt> trailing_args;

  };


  list_eq_target select_list_eq(

    const exprt &l1,

    const exprt &l2,

    const symbolt &generic_func,

    const std::vector<exprt> &generic_trailing_args) const;


  void handle_list_var_unpacking(

    const nlohmann::json &ast_node,

    const nlohmann::json &target,

    const exprt &list_expr,

    codet &target_block);


private:

  exprt check_unpack_length(

    const exprt &list_expr,

    size_t fixed,

    bool starred,

    const locationt &loc,

    codet &target_block);


  typet unpack_elem_type(

    const std::string &list_id,

    size_t i,

    const typet &fallback) const;


  size_t

  recorded_index_from_end(const std::string &list_id, size_t from_end) const;


  void record_starred_elem_types(

    const std::string &list_id,

    const std::string &star_id,

    size_t before_star,

    size_t after_star,

    const typet &elem_type);


  void assign_unpack_target(

    const nlohmann::json &ast_node,

    const nlohmann::json &tgt_node,

    const std::string &list_id,

    size_t i,

    const exprt &val,

    codet &target_block);


  friend class python_dict_handler;


  // Evaluates value_node once and snapshots it into a fresh temporary, so a

  // multi-write caller (try_build_fill_diagonal_mutation) can reuse the

  // snapshot instead of re-embedding (and re-evaluating) the same expression

  // at each write site. Throws if the value isn't scalar-typed.

  exprt snapshot_scalar_value(const nlohmann::json &value_node);


  // Repeat the elements in `list_elems` `count` times at runtime (`count` may

  // be any integer expression: a constant, a symbol like `n`, or a compound

  // like `m + 1`). Each iteration pushes every element in order. Builds a

  // fresh list so a literal source's element is not reused (avoids off-by-one).

  exprt create_vla(

    const nlohmann::json &element,

    const exprt &count,

    const std::vector<exprt> &list_elems);


  exprt build_list_at_call(

    const exprt &list,

    const exprt &index,

    const nlohmann::json &element);


  exprt bind_list_element(const exprt &list_at_call);


  list_elem_info

  get_list_element_info(const nlohmann::json &op, const exprt &elem);


  void reject_items_view_vs_tuple_set(

    const exprt &lhs,

    const exprt &rhs,

    const exprt &converted_lhs,

    const exprt &converted_rhs);


  exprt as_object_reference(const nlohmann::json &op, const exprt &elem);


  list_elem_info

  get_tagged_element_info(const nlohmann::json &op, const exprt &elem);


  list_elem_info

  get_lookup_key_info(const nlohmann::json &op, const exprt &key);


  list_elem_info

  get_erased_key_info(const nlohmann::json &op, const exprt &key);


  // The type_id a tagged scalar carries when it holds a float, or 0 when the

  // caller opts out of the float path (dict values compare via void*).

  exprt tagged_float_type_id(bool enable_float_path) const;


  symbolt &create_list();


  exprt

  handle_range_slice(const exprt &array, const nlohmann::json &slice_node);


  // Propagate a dict view's element types onto its slice result. Split out to

  // keep handle_range_slice's own decision count from growing further.

  void

  copy_dict_view_elem_types(const exprt &array, const std::string &sliced_id);

  void copy_list_of_dict_view_elem_types(

    const exprt &array,

    const std::string &sliced_id);


  // Shared core of every ADR-NP-003 scalar pointer view producer; see

  // list_access.cpp for the full rationale, including when this declines.

  std::optional<exprt> build_scalar_pointer_view(

    const exprt &array,

    const typet &elem_type,

    long long offset,

    std::size_t length,

    long long stride,

    bool readonly);


  // ADR-NP-003 etapa 2, first slice: builds a pointer into the base

  // array's own storage for a 1-D, unit-stride, literal-bound slice

  // assigned directly to a bare name, instead of handle_range_slice()'s

  // usual independent copy. Split out to keep that already large

  // function's own decision count from growing further; see

  // list_access.cpp for the full rationale and the cases intentionally

  // left out of this first slice (returns std::nullopt for those, and the

  // caller falls through to the existing copy).

  std::optional<exprt> try_build_1d_pointer_view(

    const exprt &array,

    const typet &elem_type,

    long long step_val,

    bool needs_null_term,

    long long literal_start,

    long long static_slice_len);


  std::optional<exprt> try_build_row_pointer_view(

    const exprt &array,

    const nlohmann::json &slice_node);


  std::optional<exprt> try_build_nd_subarray_pointer_view(

    const exprt &array,

    const nlohmann::json &slice_node);


  std::optional<exprt> try_build_chained_subarray_pointer_view();


  std::optional<exprt> try_build_pointer_array_index(

    const exprt &array,

    const exprt &pos_expr,

    const nlohmann::json &slice_node);


  exprt build_numpy_array_index_access(

    const exprt &array,

    const exprt &pos_expr,

    const nlohmann::json &slice_node);


  std::optional<exprt> try_build_column_pointer_view(

    const exprt &array,

    const nlohmann::json &col_index_node);


  std::optional<exprt> try_build_numpy_view_subview(

    const exprt &array,

    const nlohmann::json &slice_node);


  std::optional<exprt> try_copy_numpy_pointer_view_slice(

    const exprt &array,

    const typet &elem_type,

    const nlohmann::json &slice_node,

    long long step_val,

    bool literal_step);


  void emit_slice_zero_step_raise(

    const nlohmann::json &slice_node,

    bool literal_zero_step);


  exprt normalize_and_scale_index(

    const exprt &index,

    long long length,

    long long stride,

    const nlohmann::json &slice_node);


  exprt normalize_and_scale_index(

    const exprt &index,

    const exprt &length,

    const exprt &stride,

    const nlohmann::json &slice_node);


  struct symbolic_slice_params

  {

    exprt offset;

    exprt stride;

    exprt length;

  };


  symbolic_slice_params emit_symbolic_slice_params(

    const nlohmann::json &slice_node,

    const exprt &extent);


  exprt build_symbolic_step_slice(

    const exprt &array,

    const nlohmann::json &slice_node);


  exprt guard_numpy_pointer_view_index(

    const exprt &array,

    const exprt &index,

    const nlohmann::json &slice_node);


  exprt guard_numpy_static_array_index(

    const exprt &array,

    const exprt &index,

    const nlohmann::json &slice_node);


  exprt

  handle_index_access(const exprt &array, const nlohmann::json &slice_node);

  exprt index_value(const exprt &index, const nlohmann::json &slice_node);


  // True when `array` is a 2-D+ numpy array parameter's decayed pointer

  // symbol (register_function_argument's row-pointer decay), i.e. one whose

  // pre-decay shape handle_index_access's own negative-index normalization

  // needs to consult in numpy_param_shapes_. Split out to keep that

  // function's own decision count down.

  bool is_numpy_param_negative_index_target(const exprt &array) const;


  // handle_index_access's own index/negative-index resolution: normalizes

  // pos_expr in place for a literal negative index (a[-1]) against the

  // right size source for `array`'s shape (a numpy parameter's pre-decay

  // shape, an array_typet's own size, or -- when neither applies -- deferred

  // to build_list_at_call's runtime normalization), or sets `index` alone

  // for a compile-time-only type lookup. A no-op for anything but a

  // UnaryOp(USub)/Constant slice. Split out of handle_index_access to keep

  // that function's own decision count down.

  void normalize_index_access_position(

    const exprt &array,

    const nlohmann::json &slice_node,

    const nlohmann::json &list_node,

    exprt &pos_expr,

    size_t &index) const;


  std::optional<exprt> resolve_nested_list_element(

    const exprt &array,

    const exprt &pos_expr,

    size_t index,

    typet &elem_type);


  exprt resolve_fixed_axis_index(

    const nlohmann::json &idx_node,

    const BigInt &axis_len,

    unsigned axis,

    const nlohmann::json &element);


  // Returns (registering if absent) the __python_str_slice symbol:

  //   char* __python_str_slice(const char*, long long, long long, long long)

  const symbolt &get_str_slice_sym();


  exprt remove_function_calls_recursive(exprt &e, const nlohmann::json &node);


  element_type_registry &elem_types();

  const element_type_registry &elem_types() const;


  void emit_list_copy(

    const exprt &src,

    const symbolt &dst,

    const nlohmann::json &element);


  static void set_list_symbolic_size(

    python_converter &converter,

    exprt &list_expr,

    const exprt &size_expr,

    const nlohmann::json &element);


  static exprt handle_symbolic_range(

    python_converter &converter,

    const nlohmann::json &range_args,

    const nlohmann::json &element,

    bool materialise_elements);


  static exprt build_concrete_range(

    python_converter &converter,

    const nlohmann::json &range_args,

    const nlohmann::json &element,

    const std::optional<long long> &arg0,

    const std::optional<long long> &arg1,

    const std::optional<long long> &arg2);


  python_converter &converter_;

  const nlohmann::json &list_value_;

};


BigInt
Definition bigint.hh:58

array
Definition toml.hpp:6607

codet
Definition std_code.h:8

element_type_registry
The single owner of per-instance element-type tracking for the Python frontend: "which types does thi...
Definition element_type_registry.h:49

element_type_registry::entries
std::vector< entry > entries
Definition element_type_registry.h:54

exprt
Definition expr.h:34

irep_idt
Definition irep_idt.h:12

locationt
Definition location.h:7

nil_exprt
Definition std_expr.h:1168

python_converter
Main converter for transforming Python AST into ESBMC's intermediate representation.
Definition python_converter.h:76

python_list::build_element_replacement
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...
Definition list_mutation.cpp:798

python_list::axis_stride
static exprt axis_stride(const strided_axis &axis)
Definition list_strided_consumers.cpp:25

python_list::build_insert_list_call
exprt build_insert_list_call(const symbolt &list, const exprt &index, const nlohmann::json &op, const exprt &elem)
Definition list_mutation.cpp:647

python_list::strided_basic_view_declines
bool strided_basic_view_declines(const exprt &array, const std::vector< nlohmann::json > &idx_nodes, bool allow_plain_array) const
Definition list_access.cpp:2264

python_list::unnamed_nd_view_placeholder
std::optional< exprt > unnamed_nd_view_placeholder(const strided_view_desc &view, bool as_view, bool flat_result, const char *unnamed_error) const
Definition list_strided_consumers.cpp:336

python_list::contains
exprt contains(const exprt &item, const exprt &list)
Definition list_query.cpp:769

python_list::handle_comprehension
exprt handle_comprehension(const nlohmann::json &element)
Convert generator expressions and list comprehensions to lists.
Definition list_comprehension.cpp:8

python_list::attribute_elem_type
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...
Definition list_access.cpp:4608

python_list::emit_view_accumulator
exprt emit_view_accumulator(const nlohmann::json &arg, const typet &type, const exprt &init)
Definition list_strided_consumers.cpp:129

python_list::emit_view_copy_buffer
exprt emit_view_copy_buffer(const nlohmann::json &arg, const strided_view_desc &view, const exprt &count)
Definition list_strided_consumers.cpp:373

python_list::handle_list_var_unpacking
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.
Definition list_comprehension.cpp:304

python_list::build_contiguous_shaped_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;...
Definition list_access.cpp:2531

python_list::guard_pop_index
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 ...
Definition list_mutation.cpp:1638

python_list::emit_counted_loop
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 lo...
Definition list_strided_consumers.cpp:69

python_list::build_mixed_slice_tuple_select
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 ax...
Definition list_access.cpp:1383

python_list::try_build_symbolic_view_list
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).
Definition list_strided_consumers.cpp:291

python_list::eq_float_type_id
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'...
Definition list_query.cpp:126

python_list::copy_strided_view
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.
Definition list_access.cpp:2184

python_list::build_fancy_index
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...
Definition list_access.cpp:1563

python_list::try_reduce_symbolic_view
std::optional< exprt > try_reduce_symbolic_view(const std::string &function, const nlohmann::json &arg)
Definition list_strided_consumers.cpp:255

python_list::get
exprt get()
Definition list_construction.cpp:152

python_list::tracked_view_axes
std::vector< strided_axis > tracked_view_axes(const std::string &view_id) const
Axes of the pointer view registered under view_id.
Definition list_access.cpp:2069

python_list::require_stored_types
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 nes...
Definition list_query.cpp:97

python_list::try_build_fill_diagonal_mutation
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,...
Definition list_access.cpp:2963

python_list::build_index_range_list_call
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 ...
Definition list_query.cpp:1081

python_list::build_pop_list_call
exprt build_pop_list_call(const symbolt &list, const exprt &index, const nlohmann::json &element)
Build a list pop operation.
Definition list_mutation.cpp:1672

python_list::is_runtime_numpy_slice
bool is_runtime_numpy_slice(const exprt &array, const typet &elem_type, const nlohmann::json &slice_node) const
Definition list_access.cpp:3410

python_list::select_shallow_push
shallow_push_call select_shallow_push(const exprt &src, const exprt &untagged_last_arg) const
Shallow-push entry point for a copy of src.
Definition list_mutation.cpp:1403

python_list::unrecorded_base_elem_type
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 an...
Definition list_access.cpp:4659

python_list::axis_extent
static exprt axis_extent(const strided_axis &axis)
Definition list_strided_consumers.cpp:19

python_list::build_list_from_exprs
exprt build_list_from_exprs(const std::vector< exprt > &elems)
Materialize a fresh list from already-evaluated element values.
Definition list_construction.cpp:237

python_list::literal_elems_for_variable_list
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.
Definition list_mutation.cpp:976

python_list::bare_list_param_elem_type
typet 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.
Definition list_access.cpp:4432

python_list::has_shared_payload
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 ...
Definition list_mutation.cpp:417

python_list::is_bool_mask_rows_type
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- ...
Definition list_access.cpp:514

python_list::index_bool_mask_rows
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): normal...
Definition list_access.cpp:642

python_list::alias_contiguous_ravel
std::optional< exprt > alias_contiguous_ravel(const nlohmann::json &arg, const strided_view_desc &view)
Definition list_strided_consumers.cpp:355

python_list::build_bool_mask_index
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 o...
Definition list_access.cpp:268

python_list::build_column_select
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,...
Definition list_access.cpp:1169

python_list::literal_still_describes_list
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.
Definition list_mutation.cpp:1018

python_list::build_list_from_tuple
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.
Definition list_construction.cpp:375

python_list::tagged_elem_type_or
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 fal...
Definition list_access.cpp:4679

python_list::list_repetition
exprt list_repetition(const nlohmann::json &left_node, const nlohmann::json &right_node, const exprt &lhs, const exprt &rhs)
Definition list_mutation.cpp:1032

python_list::emit_view_loops
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,...
Definition list_strided_consumers.cpp:100

python_list::runtime_slice_axis
std::optional< strided_axis > runtime_slice_axis(const strided_axis &source, const nlohmann::json &node, exprt &offset)
Definition list_access.cpp:2283

python_list::build_set_membership_call
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.
Definition list_set_ops.cpp:5

python_list::build_remove_list_call
exprt build_remove_list_call(const symbolt &list, const nlohmann::json &op, const exprt &elem)
Build a list remove operation (removes first matching element).
Definition list_mutation.cpp:1933

python_list::store_replaces_element
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 wr...
Definition list_mutation.cpp:762

python_list::flat_shape_info_of
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-...
Definition list_access.cpp:3019

python_list::try_build_ravel_pointer_view
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 et...
Definition list_access.cpp:3061

python_list::scale_split_axis_strides
void scale_split_axis_strides(const nlohmann::json &arg, const strided_axis &source, std::vector< strided_axis > &axes)
Definition list_strided_consumers.cpp:531

python_list::try_build_flat_index_assignment_target
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-check...
Definition list_access.cpp:3307

python_list::python_list
python_list(python_converter &converter, const nlohmann::json &list)
Definition python_list.h:38

python_list::record_element_store
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.
Definition list_mutation.cpp:397

python_list::reduce_view_truth
exprt reduce_view_truth(bool is_any, const nlohmann::json &arg, const strided_view_desc &view)
Definition list_strided_consumers.cpp:147

python_list::reduce_view_argextreme
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.
Definition list_strided_consumers.cpp:202

python_list::contiguous_view_desc
std::optional< strided_view_desc > contiguous_view_desc(const exprt &array, const typet &elem_type, const std::vector< std::size_t > &shape) const
Definition list_access.cpp:2046

python_list::allocate_constructed_object
exprt allocate_constructed_object(const exprt &lhs)
Allocates the instance a constructor stores to lhs and returns the pointer to pass as self.
Definition list_mutation.cpp:460

python_list::build_copy_list_call
exprt build_copy_list_call(const symbolt &list, const nlohmann::json &element)
Build a list copy operation.
Definition list_mutation.cpp:1753

python_list::select_list_extend
shallow_push_call select_list_extend(const exprt &src, const exprt &untagged_elem_size) const
Definition list_mutation.cpp:1393

python_list::build_trace_reduction
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 scala...
Definition list_access.cpp:2865

python_list::classify_view_contiguity
static view_contiguity classify_view_contiguity(const strided_view_desc &view)
Whether a view covers its storage densely in row-major order.
Definition list_strided_consumers.cpp:484

python_list::recorded_elem_types
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.
Definition list_access.cpp:4643

python_list::index
exprt index(const exprt &array, const nlohmann::json &slice_node)
Definition list_access.cpp:252

python_list::build_shallow_copy_call
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: sc...
Definition list_mutation.cpp:1826

python_list::reduce_view_extreme
exprt reduce_view_extreme(const std::string &function, const nlohmann::json &arg, const strided_view_desc &view, const exprt &count)
Definition list_strided_consumers.cpp:166

python_list::get_empty_set
exprt get_empty_set()
Create an empty set.

python_list::extract_pyobject_value
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.
Definition list_access.cpp:5586

python_list::has_tagged_elements
bool has_tagged_elements(const exprt &list) const
Definition list_mutation.cpp:1377

python_list::scalar_storage_pointer
exprt scalar_storage_pointer(const exprt &array, const typet &scalar_ptr_type) const
array's storage as a pointer to its scalar element type.
Definition list_access.cpp:3051

python_list::try_build_strided_basic_view
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 slic...
Definition list_access.cpp:2364

python_list::reject_unresolved_element_read
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).
Definition list_access.cpp:4475

python_list::index_strided_axis
bool index_strided_axis(const strided_axis &source, const nlohmann::json &node, exprt &offset)
Definition list_access.cpp:2336

python_list::strided_index_offset
exprt strided_index_offset(const strided_view_desc &src, const std::vector< nlohmann::json > &indices)
Definition list_access.cpp:2435

python_list::emit_ll_temp
exprt emit_ll_temp(const nlohmann::json &node, const char *name, const exprt &value)
Signed 64-bit temporary holding value, assigned once here.
Definition list_access.cpp:2022

python_list::handle_subscript_assign_none
void handle_subscript_assign_none(const exprt &list_expr, const nlohmann::json &slice_node)
Definition list_access.cpp:4329

python_list::try_reshape_symbolic_view
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,...
Definition list_strided_consumers.cpp:571

python_list::emit_reshape_size_guard
void emit_reshape_size_guard(const nlohmann::json &arg, const exprt &count, const std::vector< std::size_t > &new_shape)
Definition list_strided_consumers.cpp:507

python_list::try_build_diagonal_pointer_view
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...
Definition list_access.cpp:2816

python_list::build_bool_mask_row_select_symbolic
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 ...
Definition list_access.cpp:522

python_list::view_contiguity
view_contiguity
Definition python_list.h:429

python_list::view_contiguity::contiguous
@ contiguous
Definition python_list.h:430

python_list::view_contiguity::not_contiguous
@ not_contiguous
Definition python_list.h:431

python_list::view_contiguity::unknown
@ unknown
Definition python_list.h:432

python_list::fast_elem_equality
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,...
Definition list_query.cpp:56

python_list::owned_copy_axes
std::vector< strided_axis > owned_copy_axes(const nlohmann::json &arg, const strided_view_desc &view, bool flatten, const exprt &count)
Definition list_strided_consumers.cpp:408

python_list::view_element_count
exprt view_element_count(const nlohmann::json &node, const strided_view_desc &view)
Definition list_strided_consumers.cpp:119

python_list::build_concat_list_call
exprt build_concat_list_call(const exprt &lhs, const exprt &rhs, const nlohmann::json &element)
Definition list_mutation.cpp:947

python_list::symbolic_view_operand
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 ...
Definition list_strided_consumers.cpp:32

python_list::build_index_list_call
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.
Definition list_query.cpp:1015

python_list::build_min_max_for_mixed_numeric
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.
Definition list_query.cpp:904

python_list::build_tuple_copy_call
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).
Definition list_mutation.cpp:1798

python_list::build_bool_mask_row_select
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.
Definition list_access.cpp:368

python_list::retype_element_store
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 th...
Definition list_mutation.cpp:426

python_list::build_list_from_range
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.
Definition list_construction.cpp:313

python_list::build_extend_list_call
exprt build_extend_list_call(const symbolt &list, const nlohmann::json &op, const exprt &other_list)
Definition list_mutation.cpp:1421

python_list::build_split_list
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)
Definition list_string_ops.cpp:5

python_list::build_mark_tuple_call
void build_mark_tuple_call(const exprt &list)
Mark list as built by tuple(x) (#8777).
Definition list_mutation.cpp:1808

python_list::build_push_list_call
exprt build_push_list_call(const symbolt &list, const nlohmann::json &op, const exprt &elem, bool enable_float_path=true)
Definition list_mutation.cpp:520

python_list::build_is_tuple_call
exprt build_is_tuple_call(const exprt &list)
Whether list was built by tuple(x) (#8777).
Definition list_mutation.cpp:1818

python_list::build_strided_column_select
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 boun...
Definition list_access.cpp:1251

python_list::attribute_elem_type_or_any
typet attribute_elem_type_or_any(const exprt &array) const
The element type of array's attribute annotation, or Any without one.
Definition list_access.cpp:4653

python_list::slice_strided_axis
std::optional< strided_axis > slice_strided_axis(const strided_axis &source, const nlohmann::json &node, exprt &offset)
Definition list_access.cpp:2310

python_list::reshape_registered_copy
void reshape_registered_copy(const std::string &lhs_id, const std::vector< std::size_t > &new_shape)
Definition list_strided_consumers.cpp:553

python_list::reject_mixed_member_element_read
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 hav...
Definition list_access.cpp:4511

python_list::infer_literal_element_type
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...
Definition list_type_inference.cpp:291

python_list::view_element
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.
Definition list_strided_consumers.cpp:51

python_list::python_dict_handler
friend class python_dict_handler
Definition python_list.h:1027

python_list::mixes_list_and_other
bool mixes_list_and_other(const std::string &id) const
True when the recorded elements of id mix a list with another type.
Definition list_access.cpp:4458

python_list::compare
exprt compare(const exprt &l1, const exprt &l2, const std::string &op)
Definition list_query.cpp:155

python_list::describe_strided_view
std::optional< strided_view_desc > describe_strided_view(const exprt &array)
Definition list_access.cpp:2100

python_list::uniform_elem_size
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.
Definition list_mutation.cpp:1340

python_list::try_build_numpy_param_slice_view
std::optional< exprt > try_build_numpy_param_slice_view(const exprt &array, const typet &resolved_array_type, const nlohmann::json &slice_node)
Definition list_access.cpp:3390

python_list::build_count_list_call
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.
Definition list_query.cpp:1007

python_list::select_list_eq
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.
Definition list_query.cpp:37

python_list::build_symbolic_fill_list
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.
Definition list_construction.cpp:47

python_list::try_build_strided_view_index
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.
Definition list_access.cpp:2458

python_list::register_strided_view
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 e...
Definition list_access.cpp:2140

python_list::try_copy_symbolic_view
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.
Definition list_strided_consumers.cpp:444

python_list::build_count_index_list_call
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@__ES...
Definition list_query.cpp:974

python_list::handle_slice_assignment
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.
Definition list_access.cpp:4069

symbolt
Definition symbol.h:12

type_handler
Definition type_handler.h:113

typet
Definition type.h:9

value
Definition toml.hpp:1531

count
int count
Definition cuda.h:51

element_type_registry.h

irep2.h
Classes and definitions for non-stringy internal representation.

expr2tc
irep_container< expr2t > expr2tc
Definition irep2.h:431

create_list
static auto create_list(int size, T default_value)
Definition numpy_call_expr.cpp:4866

norm_order::l1
@ l1
Definition numpy_call_expr.cpp:2087

norm_order::l2
@ l2
Definition numpy_call_expr.cpp:2086

key
uint256_t key
Definition solidity_mapping.c:1

depth
unsigned stack_budget_guardt< Tag >::depth
Definition stack_budget.h:72

std_expr.h

flat_array_shape_info
Definition python_list.h:30

flat_array_shape_info::elem_type
typet elem_type
Definition python_list.h:31

flat_array_shape_info::total_length
long long total_length
Definition python_list.h:32

function
Definition module.h:12

list_elem_info
Definition python_list.h:22

list_elem_info::location
locationt location
Definition python_list.h:26

list_elem_info::elem_symbol
symbolt * elem_symbol
Definition python_list.h:24

list_elem_info::elem_size
exprt elem_size
Definition python_list.h:25

list_elem_info::elem_type_sym
symbolt * elem_type_sym
Definition python_list.h:23

python_list::list_eq_target
Definition python_list.h:958

python_list::list_eq_target::trailing_args
std::vector< exprt > trailing_args
Definition python_list.h:960

python_list::list_eq_target::func
const symbolt * func
Definition python_list.h:959

python_list::shallow_push_call
Definition python_list.h:942

python_list::shallow_push_call::func
const symbolt * func
Definition python_list.h:943

python_list::shallow_push_call::last_arg
exprt last_arg
Definition python_list.h:944

python_list::strided_axis
One axis of a strided view, in elements: its extent and stride are constants unless the matching expr...
Definition python_list.h:269

python_list::strided_axis::stride
long long stride
Definition python_list.h:272

python_list::strided_axis::extent_expr
exprt extent_expr
Definition python_list.h:271

python_list::strided_axis::extent
long long extent
Definition python_list.h:270

python_list::strided_axis::symbolic
bool symbolic() const
Definition python_list.h:275

python_list::strided_axis::stride_expr
exprt stride_expr
Definition python_list.h:273

python_list::strided_view_desc
A numpy array or view as a scalar base pointer plus its axes: the descriptor every N-D view is built ...
Definition python_list.h:284

python_list::strided_view_desc::elem_type
typet elem_type
Definition python_list.h:286

python_list::strided_view_desc::base
exprt base
Definition python_list.h:285

python_list::strided_view_desc::axes
std::vector< strided_axis > axes
Definition python_list.h:287

python_list::strided_view_desc::readonly
bool readonly
A view of a read-only view (broadcast_to, diagonal) is read-only.
Definition python_list.h:289

symbol.h

type.h

expr.h