M (soteria-rust.Soteria_rust_lib.Builtins.Core.M)

Parameters

module StateM : State.StateM.S

Signature

val cmp : 
  signed:bool ->
  [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t ->
  [< Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] Typed.t, 'a, 'b) Rust_val.raw

val equality_check : 
  ([< `NonZero | `Ptr | `Zero ] as 'a) Typed.t ->
  'b Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] Soteria.Bv_values.Typed.t, 'c)
    StateM.t

val normalise_shift_r : 
  Charon.Expressions.binop ->
  'a Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint ] as 'b) Typed.t ->
  'b Typed.t

Rust allows shift operations on integers of differents sizes, which isn't possible in SMT-Lib, so we normalise the righthand side to match the left hand side.

val eval_lit_binop : 
  Charon.Expressions.binop ->
  Charon.Types.literal_type ->
  [< Soteria__Bv_values__Typed.T.sint ] Typed.t ->
  [ `NonZero | `Zero ] Typed.t ->
  ([> Soteria__Bv_values__Typed.T.sint_ovf ] Typed.t, 'e) StateM.t

Evaluates a binary operator of +,-,/,*,rem, and ensures the result is within the type's constraints, else errors

val eval_checked_lit_binop : 
  Charon.Expressions.binop ->
  Charon.Types.literal_type ->
  [< Soteria_rust_lib.Typed.T.any ] Typed.t ->
  [< Soteria_rust_lib.Typed.T.any ] Typed.t ->
  (([> Soteria__Bv_values__Typed.T.sint ] Soteria.Bv_values.Typed.t, 'a, 'b)
     Rust_val.raw,
    'c)
    StateM.t

Evaluates the checked operation, returning (wrapped value, overflowed).

val meta_as_int : 
  (Soteria_rust_lib.Typed.T.sint Typed.t, StateM.Sptr.t) Rust_val.meta_raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t option, 'a) StateM.t

val eval_meta_eq : 
  (Soteria_rust_lib.Typed.T.sint Typed.t, StateM.Sptr.t) Rust_val.meta_raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t, StateM.Sptr.t) Rust_val.meta_raw ->
  ([> Typed.sbool ] Typed.t, 'a) StateM.t

val eval_ptr_binop : 
  Charon.Expressions.binop ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    StateM.Sptr.t)
    Rust_val.raw ->
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    StateM.Sptr.t)
    Rust_val.raw ->
  ([> Soteria__Bv_values__Typed.T.sint ] Typed.t, 'a) StateM.t

val transmute : 
  from_ty:Charon.Types.ty ->
  to_ty:Charon.Types.ty ->
  StateM.rust_val ->
  (StateM.rust_val, 'a) StateM.t

val zero_valid : ty:Charon.Types.ty -> (bool, 'a) StateM.t