Layout (soteria-rust.Soteria_rust

module BV = Soteria_rust_lib.Typed.BV

include module type of struct include Layout_common end

module Tag_layout = Layout_common.Tag_layout

Layout of enum tags in memory. Note tags are distinct from discriminants: a discriminant is user specified and is what Rvalue.Discriminant returns, whereas a tag is specific to variant layouts, and may be of smaller size than the discriminant, or not be encoded at all if it is the untagged variant of a niche-optimised enum.

module Fields_shape = Layout_common.Fields_shape

We use a custom type for the member offsets for layouts; this allows us to use a more efficient representation for arrays T; N, that doesn't require N offsets.

type t = Layout_common.t = {

size : Soteria_rust_lib.Typed.T.sint Typed.t;
align : Soteria_rust_lib.Typed.T.nonzero Typed.t;
uninhabited : bool;
fields : Fields_shape.t;

}

val pp : 
  Ppx_deriving_runtime.Format.formatter ->
  t ->
  Ppx_deriving_runtime.unit

val show : t -> Ppx_deriving_runtime.string

val iter_vars : 
  t ->
  ((Soteria.Bv_values.Svalue.Var.t * 'a Typed.ty) -> unit) ->
  unit

module Session : sig ... end

val size_of_int_ty : Charon.Values.int_ty -> int

val size_of_uint_ty : Charon.Values.u_int_ty -> int

val size_of_literal_ty : Charon.Types.literal_type -> int

val is_signed : Charon.Types.literal_type -> bool

val align_of_literal_ty : Charon.Types.literal_type -> int

type meta_kind =

| LenKind
| VTableKind
| NoneKind

val dst_kind : Charon.Types.ty -> meta_kind

val dst_slice_ty : Charon.Types.ty -> Charon.Types.ty option

If this is a DST type with a slice tail, return the type of the slice's element.

val is_dst : Charon.Types.ty -> bool

If this is a dynamically sized type (requiring a fat pointer)

val size_to_fit : 
  size:[ `NonZero | `Zero ] Typed.t ->
  align:[< Soteria__Bv_values__Typed.T.nonzero ] Soteria__Bv_values__Typed.t ->
  [ `NonZero | `Zero ] Typed.t

val mk : 
  size:Soteria_rust_lib.Typed.T.sint Typed.t ->
  align:Soteria_rust_lib.Typed.T.nonzero Typed.t ->
  ?uninhabited:bool ->
  ?fields:Fields_shape.t ->
  unit ->
  t

val mk_concrete : 
  size:int ->
  align:int ->
  ?uninhabited:bool ->
  ?fields:Fields_shape.t ->
  unit ->
  t

val not_impl_layout : string -> Charon.Types.ty -> 'a Rustsymex.t

val layout_warning : string -> Charon.Types.ty -> unit

val layout_of : 
  Charon.Types.ty ->
  (t, [> `InvalidLayout of Charon.Types.ty ], 'f) Rustsymex.Result.t

val translate_layout : 
  Charon.Types.ty ->
  Charon.Types.layout ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((t, [> `InvalidLayout of Charon.Types.ty ], 'f) Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val compute_size : 
  Charon.Types.ty ->
  int option ->
  Soteria_rust_lib.Typed.T.sint Typed.t

val compute_align : 
  Charon.Types.ty ->
  int option ->
  Soteria_rust_lib.Typed.T.nonzero Typed.t

val compute_arbitrary_layout : 
  ?fst_size:Soteria_rust_lib.Typed.T.sint Typed.t ->
  ?fst_align:Soteria_rust_lib.Typed.T.nonzero Soteria.Bv_values.Typed.t ->
  ?variant:Charon.Types.VariantId.id ->
  Charon.Types.ty ->
  Charon.Types.ty list ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((t, [> `InvalidLayout of Charon.Types.ty ], 'f) Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val compute_enum_layout : 
  Charon.Types.ty ->
  Charon.Types.variant list ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((t, [> `InvalidLayout of Charon.Types.ty ], 'f) Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val compute_union_layout : 
  Charon.Types.ty ->
  Charon.Types.ty list ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((t, [> `InvalidLayout of Charon.Types.ty ], 'f) Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val resolve_trait_ty : 
  Charon.Types.trait_ref ->
  Charon.Types.trait_item_name ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((Charon.Types.ty, [> `InvalidLayout of Charon.Types.ty ], 'f)
     Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val normalise : 
  Charon.Types.ty ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  ((Charon.Types.ty, [> `InvalidLayout of Charon.Types.ty ], 'a)
     Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

Normalise a type, by substituting any generics with the current generic environment, and resolving the trait type if needed.

val size_of : 
  Charon.Types.ty ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  (([> Soteria_rust_lib.Typed.T.sint ] Typed.t,
     [> `InvalidLayout of Charon.Types.ty ],
     'a)
     Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val align_of : 
  Charon.Types.ty ->
  Soteria_rust_lib__Rustsymex.MonadState.t ->
  (([> Soteria_rust_lib.Typed.T.nonzero ] Typed.t,
     [> `InvalidLayout of Charon.Types.ty ],
     'a)
     Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Rustsymex.MonadState.t)
    Soteria__Symex.Make(Soteria.Bv_values.Bv_solver.Z3_solver).t

val min_value_z : Charon.Types.literal_type -> Soteria.Soteria_std.Z.t

val max_value_z : Charon.Types.literal_type -> Soteria.Soteria_std.Z.t

val is_unsafe_cell : Charon.Types.ty -> bool

val is_abi_compatible : 
  Charon.Types.ty ->
  Charon.Types.ty ->
  ([> Soteria__Bv_values__Typed.sbool ] Typed.t,
    [> `InvalidLayout of Charon.Types.ty ],
    'a)
    Rustsymex.Result.t

is_abi_compatible ty1 ty2 is true if a function expecting an argument of type ty1 can be called with an argument of type ty2.

The full specification is available at: https://doc.rust-lang.org/nightly/std/primitive.fn.html#abi-compatibility