Tree_block (soteria-rust.Soteria_rust_lib.State.Tree_state.Tree

module Encoder : sig ... end

type rust_val = Sptr.t Rust_val.t

val pp_rust_val : 
  (Soteria_rust_lib.Typed.T.sint Typed.t,
    Soteria_rust_lib.Typed.T.sfloat Typed.t,
    Sptr.t)
    Rust_val.raw
    Fmt.t

module MemVal : sig ... end

module Expr : sig ... end

type nonrec sint = MemVal.S_bounded_int.t Sptr.DecayMapMonad.Value.t

type nonrec (!'a, !'sint) tree = {

node : 'a Soteria__Sym_states__Tree_block.node;
range : 'sint * 'sint;
children : (('a, 'sint) Soteria__Sym_states__Tree_block.tree * ('a, 'sint) Soteria__Sym_states__Tree_block.tree) option;

}

module Range : sig ... end

module Split_tree : sig ... end

A Split_tree is a simplified representation of a tree, that has no offset. It however indicates, on Nodes, at what offset the split occurs, relative to that node's start.

module Node : sig ... end

module Tree : sig ... end

type t = {

root : Tree.t;
bound : sint option;

}

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

val show : t -> Ppx_deriving_runtime.string

module SM : sig ... end

val is_empty : t -> bool

val pp_pretty : Stdlib.Format.formatter -> t -> unit

type syn =

| MemVal of {
1. offset : Expr.t;
2. len : Expr.t;
3. v : MemVal.syn;
}
| Bound of Expr.t

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

val show_syn : syn -> Ppx_deriving_runtime.string

val ins_outs : syn -> Expr.t list * Expr.t list

val lift_fixes : 
  offset:'a Sptr.DecayMapMonad.Value.t ->
  len:'b Sptr.DecayMapMonad.Value.t ->
  MemVal.syn list ->
  syn list

val lift_miss : 
  offset:'a Sptr.DecayMapMonad.Value.t ->
  len:'b Sptr.DecayMapMonad.Value.t ->
  ('c, 'd, MemVal.syn list) Sptr.DecayMapMonad.Result.t ->
  ('c, 'd, syn list) Sptr.DecayMapMonad.Result.t

val lift_miss_c : 
  offset:'a Sptr.DecayMapMonad.Value.t ->
  len:'b Sptr.DecayMapMonad.Value.t ->
  ('c, MemVal.syn list) Sptr.DecayMapMonad.Consumer.t ->
  ('c, syn list) Sptr.DecayMapMonad.Consumer.t

val of_opt : 
  ?mk_fixes:(unit -> 'a list Sptr.DecayMapMonad.t) ->
  'b option ->
  ('b, 'c, 'a) Sptr.DecayMapMonad.Result.t

val to_opt : t -> t option

val with_bound_check : 
  ?mk_fixes:(unit -> syn list list Sptr.DecayMapMonad.t) ->
  sint ->
  (Tree.t ->
    ('a * Tree.t, [> `OutOfBounds ] as 'b, syn list)
      Sptr.DecayMapMonad.Result.t) ->
  ('a, 'b, syn list) SM.Result.t

val assert_exclusively_owned : 
  t option ->
  (unit, 'a, syn list) Sptr.DecayMapMonad.Result.t

val get_raw_tree_owned : 
  MemVal.S_bounded_int.t Sptr.DecayMapMonad.Value.t ->
  MemVal.S_bounded_int.t Sptr.DecayMapMonad.Value.t ->
  ((MemVal.t, MemVal.S_bounded_int.t Sptr.DecayMapMonad.Value.t)
     Soteria__Sym_states__Tree_block.tree,
    [> `OutOfBounds ],
    syn list)
    SM.Result.t

val put_raw_tree : 
  MemVal.S_bounded_int.t Sptr.DecayMapMonad.Value.t ->
  Tree.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val to_syn : t -> syn list

val consume_bound : 
  Sptr.DecayMapMonad.Value.Expr.t ->
  t option ->
  (t option, 'a) Sptr.DecayMapMonad.Consumer.t

val produce_bound : 
  Expr.t ->
  t option ->
  t option Sptr.DecayMapMonad.Producer.t

val produce_mem_val : 
  Expr.t ->
  Expr.t ->
  MemVal.syn ->
  t option ->
  t option Sptr.DecayMapMonad.Producer.t

val consume_mem_val : 
  Expr.t ->
  Expr.t ->
  MemVal.syn ->
  t option ->
  (t option, syn list) Sptr.DecayMapMonad.Consumer.t

val consume : 
  syn ->
  t option ->
  (t option, syn list) Sptr.DecayMapMonad.Consumer.t

val produce : syn -> t option -> t option Sptr.DecayMapMonad.Producer.t

val lift_symex : 'a Sptr.DecayMapMonad.Symex.t -> 'a SM.t

val sint_to_int : 
  [< Soteria__Bv_values__Typed.T.any ] Soteria__Bv_values__Typed.t ->
  int Sptr.DecayMapMonad.t

val collect_leaves : 
  Tree.t ->
  ((rust_val
    * [> Soteria__Bv_values__Typed.T.sint ] Soteria__Bv_values__Typed.t)
     list,
    'a,
    'b)
    Sptr.DecayMapMonad.Result.t

val decode_mem_val : 
  ty:Charon.Types.ty ->
  Encoder.rust_val MemVal.value_raw ->
  Soteria_rust_lib__Sptr.DecayMap.t ->
  ((Encoder.rust_val,
     [> `InvalidLayout of Charon.Types.ty | `UninitializedMemoryAccess ],
     'a)
     Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Sptr.DecayMap.t)
    Rustsymex.t

val decode_lazy : 
  ty:Charon.Types.ty ->
  Tree.t ->
  Soteria_rust_lib__Sptr.DecayMap.t ->
  ((Encoder.rust_val, 'a, 'b) Soteria.Symex.Compo_res.t
   * Soteria_rust_lib__Sptr.DecayMap.t)
    Rustsymex.t

val decode_tree : 
  ty:Charon.Types.ty ->
  Tree.t ->
  (Encoder.rust_val,
    [> `InvalidLayout of Charon.Types.ty | `UninitializedMemoryAccess ],
    'a)
    Sptr.DecayMapMonad.Result.t

val uninit : (sint * sint) -> Tree_borrow.tb_state -> Tree.t

val zeros : (sint * sint) -> Tree_borrow.tb_state -> Tree.t

val mk_fix_typed : 
  'a Sptr.DecayMapMonad.Value.t ->
  Charon.Types.ty ->
  unit ->
  Soteria_rust_lib__Sptr.DecayMap.t ->
  (syn list list * Soteria_rust_lib__Sptr.DecayMap.t) Rustsymex.t

val mk_fix_any : 
  'a Sptr.DecayMapMonad.Value.t ->
  'b Sptr.DecayMapMonad.Value.t ->
  unit ->
  syn list list

val mk_fix_any_s : 
  'a Sptr.DecayMapMonad.Value.t ->
  'b Sptr.DecayMapMonad.Value.t ->
  unit ->
  syn list list Sptr.DecayMapMonad.t

val as_owned : 
  ?mk_fixes:
    (unit ->
      Soteria_rust_lib__Sptr.DecayMap.t ->
      ('a list * Soteria_rust_lib__Sptr.DecayMap.t) Rustsymex.t) ->
  ('b * 'c, 'd) tree ->
  (('b * 'c) -> ('e, 'f, 'a) Sptr.DecayMapMonad.Result.t) ->
  ('e, 'f, 'a) Sptr.DecayMapMonad.Result.t

val check_owned : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  [< Soteria_rust_lib.Typed.T.nonzero ] Typed.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val load : 
  ignore_borrow:bool ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Charon.Types.ty ->
  Tree_borrow.tag option ->
  Tree_borrow.t ->
  (Encoder.rust_val,
    [> `AliasingError
    | `InvalidLayout of Charon.Types.ty
    | `OutOfBounds
    | `UninitializedMemoryAccess ],
    syn list)
    Soteria.Symex.Compo_res.t
    SM.t

val store : 
  [ `NonZero | `Zero ] Typed.t ->
  rust_val ->
  Tree_borrow.tag option ->
  Tree_borrow.t ->
  (unit,
    [> `AliasingError | `InvalidLayout of Charon.Types.ty | `OutOfBounds ],
    syn list)
    SM.Result.t

val get_init_leaves : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  [< Soteria_rust_lib.Typed.T.nonzero ] Typed.t ->
  ((rust_val * Soteria_rust_lib.Typed.T.sint Typed.t) list,
    [> `OutOfBounds ],
    syn list)
    SM.Result.t

val uninit_range : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val zero_range : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val alloc : ?zeroed:bool -> sint -> t

val with_tb_access : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  (Tree_borrow.tb_state ->
    (Tree_borrow.tb_state, [> `OutOfBounds ] as 'a, syn list)
      Soteria.Symex.Compo_res.t
      Rustsymex.t) ->
  (unit, 'a, syn list) SM.Result.t

val protect : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Tree_borrow.tag ->
  Tree_borrow.t ->
  (unit, [> `AliasingError | `OutOfBounds ], syn list) SM.Result.t

val unprotect : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Tree_borrow.tag ->
  Tree_borrow.t ->
  (unit, [> `OutOfBounds ], syn list) SM.Result.t

val tb_access : 
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Soteria_rust_lib.Typed.T.sint Typed.t ->
  Tree_borrow.tag ->
  Tree_borrow.t ->
  (unit, [> `AliasingError | `OutOfBounds ], syn list) SM.Result.t