Sptr (soteria-rust.Soteria_rust_lib.Value

pointer type

include Sptr.D_abstr.S_with_syn

type t

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

val show : t -> Ppx_deriving_runtime.string

val fresh : unit -> t Sptr.DecayMapMonad.t

type syn

val pp_syn : 
  Ppx_deriving_runtime.Format.formatter ->
  syn ->
  Ppx_deriving_runtime.unit

val show_syn : syn -> Ppx_deriving_runtime.string

val to_syn : t -> syn

val subst : 
  (Sptr.DecayMapMonad.Value.Expr.t -> 'a Sptr.DecayMapMonad.Value.t) ->
  syn ->
  t

val learn_eq : syn -> t -> (unit, 'a) Sptr.DecayMapMonad.Consumer.t

val exprs_syn : syn -> Sptr.DecayMapMonad.Value.Expr.t list

include Sptr.D_abstr.Sem_eq with type t := t

val null_ptr : unit -> t

val null_ptr_of : [< Soteria_rust_lib.Typed.T.sint ] Typed.t -> t

val sem_eq : t -> t -> Soteria_rust_lib.Typed.T.sbool Typed.t

Pointer equality. This comparison is structural, i.e. it is aware of provenance.

In other words, given addr = decay ptr and ptr' = of_exposed addr, sem_eq ptr ptr' will be false, even though they would have the same address, as ptr has provenance and ptr' does not.

val is_at_null_loc : t -> Soteria_rust_lib.Typed.T.sbool Typed.t

If this pointer is at a null location, i.e. has no provenance

val is_same_loc : t -> t -> Soteria_rust_lib.Typed.T.sbool Typed.t

If these two pointers are at the same location (ie. same allocation)

val distance : 
  t ->
  t ->
  Soteria_rust_lib.Typed.T.sint Typed.t Sptr.DecayMapMonad.t

The distance, in bytes, between two pointers; if they point to different allocations, they are decayed and substracted.

val constraints : t -> Soteria_rust_lib.Typed.T.sbool Typed.t

The symbolic constraints needed for the pointer to be valid.

val nondet : Charon.Types.ty -> (t, [> Error.t ], 'a) Rustsymex.Result.t

Generates a nondeterministic pointer, that is valid for accesses to the given type. The location of the pointer is nondeterministic; it could point to any allocation.

val offset : 
  ?check:bool ->
  ?ty:Charon.Types.ty ->
  signed:bool ->
  t ->
  [< Soteria_rust_lib.Typed.T.sint ] Typed.t ->
  (t, [> Error.t ], 'a) Rustsymex.Result.t

offset ?check ?ty ~signed ptr off Offsets ptr by the size of ty * off, interpreting off as a signed integer. ty defaults to u8. May result in a dangling pointer error if the pointer goes over the allocation limit. This check can be disabled with ~check:false.

val project : 
  Charon.Types.ty ->
  Charon.Expressions.field_proj_kind ->
  Charon.Types.field_id ->
  t ->
  (t, [> Error.t ], 'a) Rustsymex.Result.t

Project a pointer to a field of the given type.

val decay : 
  t ->
  [> Soteria_rust_lib.Typed.T.sint ] Typed.t Sptr.DecayMapMonad.t

Decay a pointer into an integer value, losing provenance. This does not expose the address of the allocation; for that, use expose

val expose : 
  t ->
  [> Soteria_rust_lib.Typed.T.sint ] Typed.t Sptr.DecayMapMonad.t

Decay a pointer into an integer value, exposing the address of the allocation, allowing it to be retrieved with DecayMapS.from_exposed later.

val as_id : t -> [> Soteria_rust_lib.Typed.T.sint ] Typed.t

For Miri: the allocation ID of this location, as a u64

val is_aligned : 
  Soteria_rust_lib.Typed.T.nonzero Typed.t ->
  t ->
  [> Soteria_rust_lib.Typed.T.sbool ] Typed.t * Error.t

Returns a symbolic boolean to check whether this pointer has the given alignment, along with the error to raise otherwise.

val allocation_info : 
  t ->
  [> Soteria_rust_lib.Typed.T.sint ] Typed.t
  * [> Soteria_rust_lib.Typed.T.nonzero ] Typed.t

Get the allocation info for this pointer: its size and alignment