Make (soteria-rust.Soteria_rust

Parameters

module StateImpl : State.S

Signature

module StateM : sig ... end

module Core : sig ... end

module Std_funs : sig ... end

exception Unsupported of string * Charon.Meta.span_data

type 'a t = ('a, StateM.Sptr.t Store.t) StateM.t

type 'err fun_exec = StateM.rust_val list -> (StateM.rust_val, unit) StateM.t

type lazy_ptr =

| Store of Charon.Expressions.local_id
| Heap of StateM.full_ptr

val pp_lazy_ptr : 
  Ppx_deriving_runtime.Format.formatter ->
  lazy_ptr ->
  Ppx_deriving_runtime.unit

val show_lazy_ptr : lazy_ptr -> Ppx_deriving_runtime.string

val get_variable_ptr : 
  Store.Map.key ->
  (StateM.Sptr.t Rust_val.full_ptr, StateM.Sptr.t Store.t) StateM.t

val get_variable_lazy : 
  Store.Map.key ->
  (lazy_ptr, StateM.Sptr.t Store.t) StateM.t

val get_variable_lazy_and_ty : 
  Store.Map.key ->
  (lazy_ptr * Charon.Types.ty, StateM.Sptr.t Store.t) StateM.t

val load_lazy : lazy_ptr -> Charon.Types.ty -> StateM.rust_val t

val store_lazy : 
  lazy_ptr ->
  Charon.Types.ty ->
  StateM.Sptr.t Rust_val.t ->
  unit t

val uninit_lazy : lazy_ptr -> Charon.Types.ty -> unit t

val alloc_stack : 
  Charon.GAst.locals ->
  StateM.rust_val list ->
  ((StateM.full_ptr * Charon.Types.ty) list,
    StateM.Sptr.t Store.binding Store.Map.t)
    StateM.t

alloc_stack locals args Allocates stack space for the locals in locals, and initializes the arguments with args. Returns a list of protected pointers that need to be unprotected at the end of the function.

val dealloc_stack : 
  ?protected_address:StateM.Sptr.t ->
  (StateM.full_ptr * Charon.Types.ty) list ->
  (unit, StateM.Sptr.t Store.t) StateM.t

dealloc_stack ?protected_address store protected st Deallocates the locations in st used for the variables in store; if protected_address is provided, will not deallocate that location (this is used e.g. for globals, that return a &'static reference). Will also remove the protectors from the pointers protected that were given at the function's entry.

val resolve_fn_ptr : Charon.Types.fn_ptr -> Common.Fun_kind.t t

val resolve_constant : 
  Charon.Types.constant_expr ->
  ((Soteria_rust_lib.Typed.T.sint Soteria.Bv_values.Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    StateM.Sptr.t Store.t)
    StateM.t

val resolve_place : Charon.Expressions.place -> StateM.full_ptr t

Resolves a place to a pointer

val resolve_place_lazy : Charon.Expressions.place -> lazy_ptr t

val resolve_function : 
  in_tys:Charon.Types.ty list ->
  out_ty:Charon.Types.ty ->
  Charon.GAst.fn_operand ->
  ('a fun_exec * Charon.Types.ty Soteria.Soteria_std.List.t) t

Resolve a function operand, returning a callable symbolic function to execute it. It also returns the types expected of the function, which is needed to load the first argument of a dyn method call.

This function also handles validating the call; given the input types it will be called with and the output type expected, it will make sure these are the right types and in the right amount.

The arguments must be passed, as for calls on &dyn Trait types the first argument holds the VTable pointer.

val resolve_global : 
  Charon.Types.global_decl_ref ->
  (StateM.full_ptr, StateM.Sptr.t Store.t) StateM.t

Resolves a global into a *pointer* Rust value to where that global is

val eval_operand : 
  Charon.Expressions.operand ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    StateM.Sptr.t Store.t)
    StateM.t

val eval_operand_list : 
  Charon.Expressions.operand list ->
  ((Soteria_rust_lib.Typed.T.sint Soteria.Bv_values.Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw
     list,
    StateM.Sptr.t Store.t)
    StateM.t

val eval_rvalue : 
  Charon.Expressions.rvalue ->
  Charon.Types.ty ->
  ((Soteria_rust_lib.Typed.T.sint Typed.t,
     Soteria_rust_lib.Typed.T.sfloat Typed.t,
     StateM.Sptr.t)
     Rust_val.raw,
    StateM.Sptr.t Store.t)
    StateM.t

val exec_stmt : 
  Charon.UllbcAst.statement ->
  (unit, StateM.Sptr.t Store.t) StateM.t

val exec_block : 
  body:Charon.UllbcAst.expr_body ->
  Charon.UllbcAst.block ->
  (StateM.rust_val, StateM.Sptr.t Store.t) StateM.t

val exec_real_fun : 
  Charon.UllbcAst.fun_decl ->
  Charon.Types.generic_args ->
  'a fun_exec

val exec_fun : 
  args:StateM.rust_val list ->
  state:StateM.st ->
  Charon.UllbcAst.fun_decl ->
  (StateM.rust_val * StateM.st, Error.with_trace * StateM.st, StateM.syn list)
    Soteria.Symex.Compo_res.t
    Rustsymex.t