diff --git a/api/owi/Owi/Assigned/index.html b/api/owi/Owi/Assigned/index.html deleted file mode 100644 index c39c60305..000000000 --- a/api/owi/Owi/Assigned/index.html +++ /dev/null @@ -1,3 +0,0 @@ - -
Owi.Assigned
type t = {
id : string option;
typ : Types.binary Types.str_type Named.t;
global : (Text.global, Types.binary Types.global_type) Runtime.t Named.t;
table : (Types.binary Types.table, Types.binary Types.table_type) Runtime.t
- Named.t;
mem : (Types.mem, Types.limits) Runtime.t Named.t;
func : (Types.text Types.func, Types.text Types.block_type) Runtime.t Named.t;
elem : Text.elem Named.t;
data : Text.data Named.t;
exports : Grouped.opt_exports;
start : Types.text Types.indice option;
}
Owi.Binary
named exports of a module
type global = {
typ : Types.binary Types.global_type;
init : Types.binary Types.expr;
id : string option;
}
type elem_mode =
| Elem_passive
| Elem_active of int option * Types.binary Types.expr
| Elem_declarative
type elem = {
id : string option;
typ : Types.binary Types.ref_type;
init : Types.binary Types.expr list;
mode : elem_mode;
}
type modul = {
id : string option;
types : Types.binary Types.rec_type array;
global : (global, Types.binary Types.global_type) Runtime.t array;
table : (Types.binary Types.table, Types.binary Types.table_type) Runtime.t
- array;
mem : (Types.mem, Types.limits) Runtime.t array;
func : (Types.binary Types.func, Types.binary Types.block_type) Runtime.t array;
elem : elem array;
data : data array;
exports : exports;
start : int option;
}
val empty_modul : modul
Owi.Binary_encoder
val convert :
- Fpath.t ->
- unsafe:bool ->
- optimize:bool ->
- Text.modul ->
- (unit, Result.err) Prelude.result
Owi.Binary_parser
val from_string : string -> Binary.modul Result.t
val from_channel : Prelude.in_channel -> Binary.modul Result.t
val from_file : Fpath.t -> Binary.modul Result.t
Owi.Binary_to_text
val modul : Binary.modul -> Text.modul
Owi.Binary_types
val convert_val_type :
- tbl ->
- Types.text Types.val_type ->
- Types.binary Types.val_type Result.t
val convert_heap_type :
- tbl ->
- Types.text Types.heap_type ->
- Types.binary Types.heap_type Result.t
val convert_func_type :
- tbl ->
- Types.text Types.func_type ->
- Types.binary Types.func_type Result.t
val convert_ref_type :
- tbl ->
- Types.text Types.ref_type ->
- Types.binary Types.ref_type Result.t
val convert_param :
- tbl ->
- Types.text Types.param ->
- Types.binary Types.param Result.t
val convert_table_type :
- tbl ->
- Types.text Types.table_type ->
- Types.binary Types.table_type Result.t
val convert_str :
- tbl ->
- Types.text Types.str_type ->
- Types.binary Types.str_type Result.t
Owi.Binary_validate
Module to typecheck a simplified module.
val modul : Binary.modul -> unit Result.t
typecheck a given module
C_share_site.Sites
Owi.C_share_site
module Sites : sig ... end
Owi.Choice_intf
Base.V
Choice_intf.Base
module V : Func_intf.Value_types
val return : 'a -> 'a t
Complete.V
Choice_intf.Complete
val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
Owi.Cmd_c
val cmd :
- bool ->
- int ->
- Fpath.t option ->
- bool ->
- string ->
- int ->
- string ->
- Fpath.t list ->
- Fpath.t list ->
- bool ->
- bool ->
- bool ->
- bool ->
- bool ->
- bool ->
- Cmd_sym.fail_mode ->
- bool ->
- bool ->
- Smtml.Solver_dispatcher.solver_type ->
- unit Result.t
Owi.Cmd_conc
val cmd :
- bool ->
- bool ->
- bool ->
- bool ->
- int ->
- bool ->
- bool ->
- bool ->
- Cmd_sym.fail_mode ->
- Fpath.t ->
- Smtml.Solver_dispatcher.solver_type ->
- Fpath.t list ->
- unit Result.t
Owi.Cmd_fmt
val cmd : bool -> Fpath.t list -> unit Result.t
Owi.Cmd_opt
val cmd : bool -> bool -> Fpath.t list -> unit Result.t
Owi.Cmd_run
val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t
Owi.Cmd_script
val cmd : bool -> bool -> bool -> Fpath.t list -> bool -> unit Result.t
Owi.Cmd_sym
Owi.Cmd_utils
val write_testcase : dir:Fpath.t -> Smtml.Value.t list -> unit Result.t
val add_main_as_start :
- Binary.modul ->
- (Binary.modul, [> `Msg of string ]) Prelude.result
Owi.Cmd_validate
val cmd : bool -> Fpath.t list -> unit Result.t
Owi.Cmd_wasm2wat
val cmd : Fpath.t list -> bool -> unit Result.t
Owi.Cmd_wat2wasm
val cmd : bool -> bool -> bool -> bool -> Fpath.t list -> unit Result.t
Compile.Any
val until_binary_validate :
- unsafe:bool ->
- 'extern_func Kind.t ->
- Binary.modul Result.t
val until_optimize :
- unsafe:bool ->
- optimize:bool ->
- 'extern_func Kind.t ->
- Binary.modul Result.t
val until_link :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- 'extern_func Link.state ->
- 'extern_func Kind.t ->
- ('extern_func Link.module_to_run * 'extern_func Link.state) Result.t
compile a module with a given link state and produce a new link state and a runnable module
val until_interpret :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- Concrete_value.Func.extern_func Link.state ->
- Concrete_value.Func.extern_func Kind.t ->
- Concrete_value.Func.extern_func Link.state Result.t
compile and interpret a module with a given link state and produce a new link state
Compile.Binary
val until_binary_validate :
- unsafe:bool ->
- Binary.modul ->
- Binary.modul Result.t
val until_optimize :
- unsafe:bool ->
- optimize:bool ->
- Binary.modul ->
- Binary.modul Result.t
val until_link :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- 'f Link.state ->
- Binary.modul ->
- ('f Link.module_to_run * 'f Link.state) Result.t
compile a module with a given link state and produce a new link state and a runnable module
val until_interpret :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- Concrete_value.Func.extern_func Link.state ->
- Binary.modul ->
- Concrete_value.Func.extern_func Link.state Result.t
compile and interpret a module with a given link state and produce a new link state
Compile.File
val until_binary_validate : unsafe:bool -> Fpath.t -> Binary.modul Result.t
val until_optimize :
- unsafe:bool ->
- optimize:bool ->
- Fpath.t ->
- Binary.modul Result.t
val until_link :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- 'extern_func Link.state ->
- Fpath.t ->
- ('extern_func Link.module_to_run * 'extern_func Link.state) Result.t
compile a file with a given link state and produce a new link state and a runnable module
val until_interpret :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- Concrete_value.Func.extern_func Link.state ->
- Fpath.t ->
- Concrete_value.Func.extern_func Link.state Result.t
compile and interpret a file with a given link state and produce a new link state
Compile.Text
val until_text_validate : unsafe:bool -> Text.modul -> Text.modul Result.t
val until_binary : unsafe:bool -> Text.modul -> Binary.modul Result.t
val until_binary_validate : unsafe:bool -> Text.modul -> Binary.modul Result.t
val until_optimize :
- unsafe:bool ->
- optimize:bool ->
- Text.modul ->
- Binary.modul Result.t
val until_link :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- 'f Link.state ->
- Text.modul ->
- ('f Link.module_to_run * 'f Link.state) Result.t
compile a module with a given link state and produce a new link state and a runnable module
val until_interpret :
- unsafe:bool ->
- optimize:bool ->
- name:string option ->
- Concrete_value.Func.extern_func Link.state ->
- Text.modul ->
- Concrete_value.Func.extern_func Link.state Result.t
compile and interpret a module with a given link state and produce a new link state
Owi.Compile
Utility functions to compile a module until a given step.
module Any : sig ... end
module File : sig ... end
module Text : sig ... end
module Binary : sig ... end
P'.Choice
P'.Data
val value : t -> string
P'.Elem
P'.Env
val get_func : t -> int -> Func_intf.t
val get_extern_func : t -> Func_id.t -> Extern_func.extern_func
val drop_elem : Elem.t -> unit
val drop_data : Data.t -> unit
P'.Extern_func
type _ telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
P'.Global
val typ : t -> Types.binary Types.val_type
P'.Memory
val load_8_s : t -> Value.int32 -> Value.int32 Choice.t
val load_8_u : t -> Value.int32 -> Value.int32 Choice.t
val load_16_s : t -> Value.int32 -> Value.int32 Choice.t
val load_16_u : t -> Value.int32 -> Value.int32 Choice.t
val load_32 : t -> Value.int32 -> Value.int32 Choice.t
val load_64 : t -> Value.int32 -> Value.int64 Choice.t
val store_8 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_16 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_32 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_64 : t -> addr:Value.int32 -> Value.int64 -> unit Choice.t
val grow : t -> Value.int32 -> unit
val fill : t -> pos:Value.int32 -> len:Value.int32 -> char -> Value.vbool
val blit :
- t ->
- src:Value.int32 ->
- dst:Value.int32 ->
- len:Value.int32 ->
- Value.vbool
val blit_string :
- t ->
- string ->
- src:Value.int32 ->
- dst:Value.int32 ->
- len:Value.int32 ->
- Value.vbool
val size : t -> Value.int32
val size_in_pages : t -> Value.int32
val get_limit_max : t -> Value.int64 option
P'.Module_to_run
val to_run : t -> Types.binary Types.expr list
val modul : t -> Binary.modul
P'.Table
val get : t -> int -> Value.ref_value
val set : t -> int -> Value.ref_value -> unit
val size : t -> int
val typ : t -> Types.binary Types.ref_type
val max_size : t -> int option
val grow : t -> int32 -> Value.ref_value -> unit
val fill : t -> int32 -> int32 -> Value.ref_value -> unit
Value.Bool
Value.F32
Value.F64
Value.I32
Value.I64
Value.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
P'.Value
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
Concolic.P'
module Value : Value_intf.T
module Choice : Choice_intf.Base with module V := Value
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Global : sig ... end
module Table : sig ... end
module Memory : sig ... end
module Extern_func :
- Func_intf.T_Extern_func
- with type int32 := Value.int32
- and type int64 := Value.int64
- and type float32 := Value.float32
- and type float64 := Value.float64
- and type 'a m := 'a Choice.t
- and type memory := Memory.t
module Data : sig ... end
module Elem : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
P.Choice'
P.Data
type t = Link_env.data
val value : Link_env.data -> string
P.Elem
P.Env
type t = Extern_func.extern_func Link_env.t
type t' = Env_id.t
val get_memory : 'a Link_env.t -> int -> Memory.t Choice.t
val get_func : 'a Link_env.t -> int -> Func_intf.t
val get_extern_func : 'a Link_env.t -> Func_id.t -> 'b
val get_table : 'a Link_env.t -> Symbolic_table.ITbl.key -> Table.t Choice.t
val get_elem : 'a Link_env.t -> int -> Link_env.elem
val get_data : 'a Link_env.t -> int -> Link_env.data Choice.t
val get_global : 'a Link_env.t -> int -> Global.t Choice.t
val drop_data : Link_env.data -> unit
P.Extern_func
type !'b telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
P.Global
type t = (Concrete_global.t, Symbolic_global.t) Concolic_value.cs
val set_value : t -> Concolic_value.V.t -> unit
val typ : t -> Types.binary Types.val_type
P.Memory
type t = (Concrete_memory.t, Symbolic_memory.t) Concolic_value.cs
module C = Concrete_memory
module S = Symbolic_memory
val with_concrete :
- ('a, 'b) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- ('c -> Owi.Concrete.Value.int32 -> 'd) ->
- ('e -> Symbolic_value.int32 -> 'f) ->
- ('g, 'h) Concolic_value.cs Choice.t
val with_concrete_store :
- ('a, 'b) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- ('c -> addr:Owi.Concrete.Value.int32 -> 'd -> 'e) ->
- ('f -> addr:Symbolic_value.int32 -> 'g -> 'h) ->
- ('i, 'j) Concolic_value.cs ->
- 'k Choice.t
val load_8_s :
- (C.t, S.t) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- (int32, Symbolic_value.int32) Concolic_value.cs Choice.t
val load_8_u :
- (C.t, S.t) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- (int32, Symbolic_value.int32) Concolic_value.cs Choice.t
val load_16_s :
- (C.t, S.t) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- (int32, Symbolic_value.int32) Concolic_value.cs Choice.t
val load_16_u :
- (C.t, S.t) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- (int32, Symbolic_value.int32) Concolic_value.cs Choice.t
val load_32 :
- (C.t, S.t) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- (int32, Symbolic_value.int32) Concolic_value.cs Choice.t
val load_64 :
- (C.t, S.t) Concolic_value.cs ->
- Concolic_value.V.int32 ->
- (int64, Symbolic_value.int32) Concolic_value.cs Choice.t
val store_8 :
- (C.t, S.t) Concolic_value.cs ->
- addr:Concolic_value.V.int32 ->
- (int32, Smtml.Expr.t) Concolic_value.cs ->
- unit Choice.t
val store_16 :
- (C.t, S.t) Concolic_value.cs ->
- addr:Concolic_value.V.int32 ->
- (int32, Smtml.Expr.t) Concolic_value.cs ->
- unit Choice.t
val store_32 :
- (C.t, S.t) Concolic_value.cs ->
- addr:Concolic_value.V.int32 ->
- (int32, Smtml.Expr.t) Concolic_value.cs ->
- unit Choice.t
val store_64 :
- (C.t, S.t) Concolic_value.cs ->
- addr:Concolic_value.V.int32 ->
- (int64, Smtml.Expr.t) Concolic_value.cs ->
- unit Choice.t
val grow :
- (Concrete_memory.t, Symbolic_memory.t) Concolic_value.cs ->
- (int32, Smtml.Expr.t) Concolic_value.cs ->
- unit
val size :
- (Concrete_memory.t, Symbolic_memory.t) Concolic_value.cs ->
- (int32, Smtml.Expr.t) Concolic_value.cs
val size_in_pages :
- (Concrete_memory.t, Symbolic_memory.t) Concolic_value.cs ->
- (int32, Smtml.Expr.t) Concolic_value.cs
val blit_string :
- (Concrete_memory.t, Symbolic_memory.t) Concolic_value.cs ->
- string ->
- src:(int32, Smtml.Expr.t) Concolic_value.cs ->
- dst:(int32, Smtml.Expr.t) Concolic_value.cs ->
- len:(int32, Smtml.Expr.t) Concolic_value.cs ->
- (bool, Smtml.Expr.t) Concolic_value.cs
P.Module_to_run
P.Table
type t = (Concrete_table.t, Symbolic_table.t) Concolic_value.cs
val get :
- (Concrete_table.t, Symbolic_table.t) Concolic_value.cs ->
- int ->
- (Concrete_value.ref_value, Symbolic_value.ref_value) Owi__Concolic_value.cs
val set :
- (Concrete_table.t, Symbolic_table.t) Concolic_value.cs ->
- int ->
- (Concrete_value.ref_value, Symbolic_value.ref_value) Concolic_value.cs ->
- unit
val size : (Concrete_table.t, 'a) Concolic_value.cs -> int
val typ :
- (Concrete_table.t, 'a) Concolic_value.cs ->
- Types.binary Types.ref_type
val max_size : (Concrete_table.t, 'a) Concolic_value.cs -> int option
val grow :
- (Concrete_table.t, Symbolic_table.t) Concolic_value.cs ->
- Int32.t ->
- (Concrete_value.ref_value, Symbolic_value.ref_value) Concolic_value.cs ->
- unit
val fill :
- (Concrete_table.t, Symbolic_table.t) Concolic_value.cs ->
- Int32.t ->
- Int32.t ->
- (Concrete_value.ref_value, Symbolic_value.ref_value) Concolic_value.cs ->
- unit
val copy :
- t_src:(Concrete_table.t, Symbolic_table.t) Concolic_value.cs ->
- t_dst:(Concrete_table.t, Symbolic_table.t) Concolic_value.cs ->
- src:Int32.t ->
- dst:Int32.t ->
- len:Int32.t ->
- unit
Concolic.P
type thread = Concolic_choice.thread
module Value = Concolic_value.V
module Choice' : Choice_intf.Base with module V := Value
module Choice = Concolic_choice
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Global : sig ... end
module Table : sig ... end
module Memory : sig ... end
module Extern_func : sig ... end
module Data : sig ... end
module Elem : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
Owi.Concolic
module P : sig ... end
module P' : Interpret_intf.P
val convert_module_to_run :
- P.Extern_func.extern_func Link.module_to_run ->
- P.Module_to_run.t
val backup : P.Module_to_run.t -> P.Extern_func.extern_func Link_env.backup
val recover :
- P.Extern_func.extern_func Link_env.backup ->
- P.Module_to_run.t ->
- unit
Owi.Concolic_choice
type pc_elt =
| Select of Symbolic_value.vbool * bool
| Select_i32 of Symbolic_value.int32 * int32
| Assume of Symbolic_value.vbool
| Assert of Symbolic_value.vbool
type pc = pc_elt list
type assignments = (Smtml.Symbol.t * Concrete_value.t) list
val pp_pc_elt : Stdlib.Format.formatter -> pc_elt -> unit
val pp_pc : Stdlib.Format.formatter -> pc_elt list -> unit
val pp_assignments :
- no_values:bool ->
- Stdlib.Format.formatter ->
- (Smtml.Symbol.t * Concrete_value.t) list ->
- unit
val pc_elt_to_expr : pc_elt -> Symbolic_value.vbool option
val pc_to_exprs : pc_elt list -> Symbolic_value.vbool list
type thread = {
pc : pc;
symbols : int;
symbols_value : assignments;
preallocated_values : (Smtml.Symbol.t, Smtml.Value.t) Prelude.Hashtbl.t;
}
val init_thread :
- (Smtml.Symbol.t, Smtml.Value.t) Prelude.Hashtbl.t ->
- shared_thread_info ->
- thread
val return : 'a -> 'b t
val abort : unit t
val add_pc : Concolic_value.V.vbool -> unit t
val select : Concolic_value.V.vbool -> Owi.Concrete.Value.vbool t
val select_i32 : Concolic_value.V.int32 -> Owi.Concrete.Value.int32 t
val assume : Concolic_value.V.vbool -> unit t
val assertion : Concolic_value.V.vbool -> unit t
val with_new_symbol :
- Smtml.Ty.t ->
- (Smtml.Symbol.t -> Smtml.Value.t option -> Concrete_value.t * 'a) ->
- 'b t
val run :
- (Smtml.Symbol.t, Smtml.Value.t) Prelude.Hashtbl.t ->
- 'a t ->
- 'b run_result
val run' : 'a t -> 'b run_result
T_pair.Bool
T_pair.F32
include sig ... end
T_pair.F64
include sig ... end
T_pair.I32
include sig ... end
T_pair.I64
include sig ... end
MK_Fop.CT
MK_Fop.CIT
MK_Fop.ST
MK_Fop.SIT
MK_Fop.CFop
MK_Fop.SFop
T_pair.MK_Fop
MK_Iop.Const
MK_Iop.CT
MK_Iop.ST
MK_Iop.CIop
MK_Iop.SIop
T_pair.MK_Iop
T_pair.Ref
val equal_func_intf : Func_intf.t -> Func_intf.t -> bool
val get_func : (C.ref_value, S.ref_value) cs -> Func_intf.t Value_intf.get_ref
val get_externref :
- (C.ref_value, S.ref_value) cs ->
- 'a Prelude.Type.Id.t ->
- 'b Value_intf.get_ref
C.Bool
C.F32
C.F64
C.I32
C.I64
C.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
T_pair.C
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
S.Bool
S.F32
S.F64
S.I32
S.I64
S.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
T_pair.S
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
Concolic_value.T_pair
module C : Value_intf.T
module S : Value_intf.T
type ref_value = (C.ref_value, S.ref_value) cs
val pp_ref_value :
- Stdlib.Format.formatter ->
- (C.ref_value, S.ref_value) cs ->
- unit
val pair : 'a -> 'b -> ('c, 'd) cs
val f_pair_1_cst : ('a -> 'b) -> ('c -> 'd) -> 'e -> ('f, 'g) cs
val f_pair_2_cst :
- ('a -> 'b -> 'c) ->
- ('d -> 'e -> 'f) ->
- 'g ->
- 'h ->
- ('i, 'j) cs
val assert_ref_c : C.t -> C.ref_value
val assert_ref_s : S.t -> S.ref_value
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'b -> t
val ref_is_null : (C.ref_value, S.ref_value) cs -> (C.vbool, S.vbool) cs
val mk_pp :
- (Stdlib.Format.formatter -> 'a -> unit) ->
- (Stdlib.Format.formatter -> 'b -> unit) ->
- Stdlib.Format.formatter ->
- ('c, 'd) cs ->
- unit
val pp : Stdlib.Format.formatter -> t -> unit
module Ref : sig ... end
module Bool : sig ... end
module type CFop = sig ... end
module type SFop = sig ... end
module MK_Fop
- (CT : T)
- (CIT : T)
- (ST : T)
- (SIT : T)
- (CFop : CFop with type num := CT.t and type same_size_int := CIT.t)
- (SFop : SFop with type num := ST.t and type same_size_int := SIT.t) :
- Value_intf.Fop
- with type num := (CT.t, ST.t) cs
- and type vbool := vbool
- and type int32 := int32
- and type int64 := int64
- and type same_size_int := (CIT.t, SIT.t) cs
module type CIop = sig ... end
module type SIop = sig ... end
module MK_Iop
- (Const : T)
- (CT : T)
- (ST : T)
- (CIop : CIop with type num := CT.t and type const := Const.t)
- (SIop : SIop with type num := ST.t and type const := Const.t) :
- Value_intf.Iop
- with type num := (CT.t, ST.t) cs
- and type const := Const.t
- and type vbool := vbool
- and type float32 := float32
- and type float64 := float64
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
T_pair.CFop
include Value_intf.Fop
- with type num := num
- and type vbool := C.vbool
- and type int32 := C.int32
- and type int64 := C.int64
- and type same_size_int := same_size_int
val zero : num
val of_bits : same_size_int -> num
val to_bits : num -> same_size_int
T_pair.CIop
T_pair.SFop
include Value_intf.Fop
- with type num := num
- and type vbool := S.vbool
- and type int32 := S.int32
- and type int64 := S.int64
- and type same_size_int := same_size_int
val zero : num
val of_bits : same_size_int -> num
val to_bits : num -> same_size_int
T_pair.SIop
V'.Bool
V'.F32
V'.F64
V'.I32
V'.I64
V'.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
Concolic_value.V'
type vbool = (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
type int32 = (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
type int64 = (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
type float32 = (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
type float64 = (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
type ref_value = (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
V.Bool
val const : bool -> (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
val not :
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
val or_ :
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
val and_ :
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
val int32 :
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val pp :
- Stdlib.Format.formatter ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs ->
- unit
V.F32
val zero : (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val abs :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val neg :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val sqrt :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val ceil :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val floor :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val trunc :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val nearest :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val add :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val sub :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val mul :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val div :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val min :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val max :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val copy_sign :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val eq :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- vbool
val ne :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- vbool
val lt :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- vbool
val gt :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- vbool
val le :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- vbool
val ge :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- vbool
val convert_i32_s :
- int32 ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val convert_i32_u :
- int32 ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val convert_i64_s :
- int64 ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val convert_i64_u :
- int64 ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val of_bits :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val to_bits :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val demote_f64 :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val reinterpret_i32 :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
V.F64
val zero : (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val abs :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val neg :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val sqrt :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val ceil :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val floor :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val trunc :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val nearest :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val add :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val sub :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val mul :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val div :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val min :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val max :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val copy_sign :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val eq :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- vbool
val ne :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- vbool
val lt :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- vbool
val gt :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- vbool
val le :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- vbool
val ge :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- vbool
val convert_i32_s :
- int32 ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val convert_i32_u :
- int32 ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val convert_i64_s :
- int64 ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val convert_i64_u :
- int64 ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val of_bits :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val to_bits :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val promote_f32 :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val reinterpret_i64 :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
V.I32
val zero : (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val clz :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val ctz :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val popcnt :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val add :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val sub :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val mul :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val div :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val unsigned_div :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val rem :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val unsigned_rem :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val logand :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val logor :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val logxor :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val shl :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val shr_s :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val shr_u :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val rotl :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val rotr :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val eq_const :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- Int32.t ->
- vbool
val eq :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val ne :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val lt :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val gt :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val lt_u :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val gt_u :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val le :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val ge :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val le_u :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val ge_u :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- vbool
val trunc_f32_s :
- float32 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_f32_u :
- float32 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_f64_s :
- float64 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_f64_u :
- float64 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_sat_f32_s :
- float32 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_sat_f32_u :
- float32 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_sat_f64_s :
- float64 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val trunc_sat_f64_u :
- float64 ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val extend_s :
- int ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val to_bool :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
val reinterpret_f32 :
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val wrap_i64 :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
V.I64
val zero : (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val clz :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val ctz :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val popcnt :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val add :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val sub :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val mul :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val div :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val unsigned_div :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val rem :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val unsigned_rem :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val logand :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val logor :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val logxor :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val shl :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val shr_s :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val shr_u :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val rotl :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val rotr :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val eq_const :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- Int64.t ->
- vbool
val eq :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val ne :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val lt :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val gt :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val lt_u :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val gt_u :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val le :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val ge :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val le_u :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val ge_u :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- vbool
val trunc_f32_s :
- float32 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_f32_u :
- float32 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_f64_s :
- float64 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_f64_u :
- float64 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_sat_f32_s :
- float32 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_sat_f32_u :
- float32 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_sat_f64_s :
- float64 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val trunc_sat_f64_u :
- float64 ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val extend_s :
- int ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val of_int32 :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val to_int32 :
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val reinterpret_f64 :
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val extend_i32_s :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val extend_i32_u :
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
MK_Fop.CT
MK_Fop.CIT
MK_Fop.ST
MK_Fop.SIT
MK_Fop.CFop
val zero : CT.t
val eq : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val ne : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val lt : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val gt : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val le : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val ge : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val convert_i32_s : Owi.Concrete.Value.int32 -> CT.t
val convert_i32_u : Owi.Concrete.Value.int32 -> CT.t
val convert_i64_s : Owi.Concrete.Value.int64 -> CT.t
val convert_i64_u : Owi.Concrete.Value.int64 -> CT.t
MK_Fop.SFop
val zero : ST.t
val eq : ST.t -> ST.t -> Symbolic_value.vbool
val ne : ST.t -> ST.t -> Symbolic_value.vbool
val lt : ST.t -> ST.t -> Symbolic_value.vbool
val gt : ST.t -> ST.t -> Symbolic_value.vbool
val le : ST.t -> ST.t -> Symbolic_value.vbool
val ge : ST.t -> ST.t -> Symbolic_value.vbool
val convert_i32_s : Symbolic_value.int32 -> ST.t
val convert_i32_u : Symbolic_value.int32 -> ST.t
val convert_i64_s : Symbolic_value.int64 -> ST.t
val convert_i64_u : Symbolic_value.int64 -> ST.t
V.MK_Fop
MK_Iop.Const
MK_Iop.CT
MK_Iop.ST
MK_Iop.CIop
val zero : CT.t
val eq_const : CT.t -> Const.t -> Owi.Concrete.Value.vbool
val eq : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val ne : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val lt : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val gt : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val lt_u : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val gt_u : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val le : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val ge : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val le_u : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val ge_u : CT.t -> CT.t -> Owi.Concrete.Value.vbool
val trunc_f32_s : Owi.Concrete.Value.float32 -> CT.t
val trunc_f32_u : Owi.Concrete.Value.float32 -> CT.t
val trunc_f64_s : Owi.Concrete.Value.float64 -> CT.t
val trunc_f64_u : Owi.Concrete.Value.float64 -> CT.t
val trunc_sat_f32_s : Owi.Concrete.Value.float32 -> CT.t
val trunc_sat_f32_u : Owi.Concrete.Value.float32 -> CT.t
val trunc_sat_f64_s : Owi.Concrete.Value.float64 -> CT.t
val trunc_sat_f64_u : Owi.Concrete.Value.float64 -> CT.t
MK_Iop.SIop
val zero : ST.t
val eq_const : ST.t -> Const.t -> Symbolic_value.vbool
val eq : ST.t -> ST.t -> Symbolic_value.vbool
val ne : ST.t -> ST.t -> Symbolic_value.vbool
val lt : ST.t -> ST.t -> Symbolic_value.vbool
val gt : ST.t -> ST.t -> Symbolic_value.vbool
val lt_u : ST.t -> ST.t -> Symbolic_value.vbool
val gt_u : ST.t -> ST.t -> Symbolic_value.vbool
val le : ST.t -> ST.t -> Symbolic_value.vbool
val ge : ST.t -> ST.t -> Symbolic_value.vbool
val le_u : ST.t -> ST.t -> Symbolic_value.vbool
val ge_u : ST.t -> ST.t -> Symbolic_value.vbool
val trunc_f32_s : Symbolic_value.float32 -> ST.t
val trunc_f32_u : Symbolic_value.float32 -> ST.t
val trunc_f64_s : Symbolic_value.float64 -> ST.t
val trunc_f64_u : Symbolic_value.float64 -> ST.t
val trunc_sat_f32_s : Symbolic_value.float32 -> ST.t
val trunc_sat_f32_u : Symbolic_value.float32 -> ST.t
val trunc_sat_f64_s : Symbolic_value.float64 -> ST.t
val trunc_sat_f64_u : Symbolic_value.float64 -> ST.t
V.MK_Iop
V.Ref
val equal_func_intf : Func_intf.t -> Func_intf.t -> bool
val get_func :
- (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs ->
- Func_intf.t Value_intf.get_ref
val get_externref :
- (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs ->
- 'a Prelude.Type.Id.t ->
- 'b Value_intf.get_ref
Concolic_value.V
type vbool = (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
type int32 = (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val pp_int32 :
- Stdlib.Format.formatter ->
- (Owi.Concrete.Value.int32, Symbolic_value.int32) cs ->
- unit
type int64 = (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val pp_int64 :
- Stdlib.Format.formatter ->
- (Owi.Concrete.Value.int64, Symbolic_value.int64) cs ->
- unit
type float32 = (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val pp_float32 :
- Stdlib.Format.formatter ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs ->
- unit
type float64 = (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val pp_float64 :
- Stdlib.Format.formatter ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs ->
- unit
type ref_value = (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs
val pp_ref_value :
- Stdlib.Format.formatter ->
- (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs ->
- unit
val pair : 'a -> 'b -> ('c, 'd) cs
val value_pair : Owi.Concrete.Value.t -> Symbolic_value.t -> t
val concrete_value : t -> Owi.Concrete.Value.t
val symbolic_value : t -> Symbolic_value.t
val f_pair_1_cst : ('a -> 'b) -> ('c -> 'd) -> 'e -> ('f, 'g) cs
val f_pair_2_cst :
- ('a -> 'b -> 'c) ->
- ('d -> 'e -> 'f) ->
- 'g ->
- 'h ->
- ('i, 'j) cs
val const_i32 : Int32.t -> (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
val const_i64 : Int64.t -> (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
val const_f32 :
- Float32.t ->
- (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
val const_f64 :
- Float64.t ->
- (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
val assert_ref_c : Owi.Concrete.Value.t -> Owi.Concrete.Value.ref_value
val assert_ref_s : Symbolic_value.t -> Symbolic_value.ref_value
val ref_pair : Owi.Concrete.Value.t -> Symbolic_value.t -> t
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'b -> t
val ref_is_null :
- (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs ->
- (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
val mk_pp :
- (Stdlib.Format.formatter -> 'a -> unit) ->
- (Stdlib.Format.formatter -> 'b -> unit) ->
- Stdlib.Format.formatter ->
- ('c, 'd) cs ->
- unit
val pp : Stdlib.Format.formatter -> t -> unit
module Ref : sig ... end
module Bool : sig ... end
module type CFop = sig ... end
module type SFop = sig ... end
module type CIop = sig ... end
module type SIop = sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
V.CFop
val zero : num
val eq : num -> num -> Owi.Concrete.Value.vbool
val ne : num -> num -> Owi.Concrete.Value.vbool
val lt : num -> num -> Owi.Concrete.Value.vbool
val gt : num -> num -> Owi.Concrete.Value.vbool
val le : num -> num -> Owi.Concrete.Value.vbool
val ge : num -> num -> Owi.Concrete.Value.vbool
val convert_i32_s : Owi.Concrete.Value.int32 -> num
val convert_i32_u : Owi.Concrete.Value.int32 -> num
val convert_i64_s : Owi.Concrete.Value.int64 -> num
val convert_i64_u : Owi.Concrete.Value.int64 -> num
val of_bits : same_size_int -> num
val to_bits : num -> same_size_int
V.CIop
val zero : num
val eq_const : num -> const -> Owi.Concrete.Value.vbool
val eq : num -> num -> Owi.Concrete.Value.vbool
val ne : num -> num -> Owi.Concrete.Value.vbool
val lt : num -> num -> Owi.Concrete.Value.vbool
val gt : num -> num -> Owi.Concrete.Value.vbool
val lt_u : num -> num -> Owi.Concrete.Value.vbool
val gt_u : num -> num -> Owi.Concrete.Value.vbool
val le : num -> num -> Owi.Concrete.Value.vbool
val ge : num -> num -> Owi.Concrete.Value.vbool
val le_u : num -> num -> Owi.Concrete.Value.vbool
val ge_u : num -> num -> Owi.Concrete.Value.vbool
val trunc_f32_s : Owi.Concrete.Value.float32 -> num
val trunc_f32_u : Owi.Concrete.Value.float32 -> num
val trunc_f64_s : Owi.Concrete.Value.float64 -> num
val trunc_f64_u : Owi.Concrete.Value.float64 -> num
val trunc_sat_f32_s : Owi.Concrete.Value.float32 -> num
val trunc_sat_f32_u : Owi.Concrete.Value.float32 -> num
val trunc_sat_f64_s : Owi.Concrete.Value.float64 -> num
val trunc_sat_f64_u : Owi.Concrete.Value.float64 -> num
V.SFop
val zero : num
val eq : num -> num -> Symbolic_value.vbool
val ne : num -> num -> Symbolic_value.vbool
val lt : num -> num -> Symbolic_value.vbool
val gt : num -> num -> Symbolic_value.vbool
val le : num -> num -> Symbolic_value.vbool
val ge : num -> num -> Symbolic_value.vbool
val convert_i32_s : Symbolic_value.int32 -> num
val convert_i32_u : Symbolic_value.int32 -> num
val convert_i64_s : Symbolic_value.int64 -> num
val convert_i64_u : Symbolic_value.int64 -> num
val of_bits : same_size_int -> num
val to_bits : num -> same_size_int
V.SIop
val zero : num
val eq_const : num -> const -> Symbolic_value.vbool
val eq : num -> num -> Symbolic_value.vbool
val ne : num -> num -> Symbolic_value.vbool
val lt : num -> num -> Symbolic_value.vbool
val gt : num -> num -> Symbolic_value.vbool
val lt_u : num -> num -> Symbolic_value.vbool
val gt_u : num -> num -> Symbolic_value.vbool
val le : num -> num -> Symbolic_value.vbool
val ge : num -> num -> Symbolic_value.vbool
val le_u : num -> num -> Symbolic_value.vbool
val ge_u : num -> num -> Symbolic_value.vbool
val trunc_f32_s : Symbolic_value.float32 -> num
val trunc_f32_u : Symbolic_value.float32 -> num
val trunc_f64_s : Symbolic_value.float64 -> num
val trunc_f64_u : Symbolic_value.float64 -> num
val trunc_sat_f32_s : Symbolic_value.float32 -> num
val trunc_sat_f32_u : Symbolic_value.float32 -> num
val trunc_sat_f64_s : Symbolic_value.float64 -> num
val trunc_sat_f64_u : Symbolic_value.float64 -> num
Owi.Concolic_value
module type T = sig ... end
module T_pair (C : Value_intf.T) (S : Value_intf.T) : sig ... end
module V : sig ... end
module V' :
- Value_intf.T
- with type vbool = (Owi.Concrete.Value.vbool, Symbolic_value.vbool) cs
- and type int32 = (Owi.Concrete.Value.int32, Symbolic_value.int32) cs
- and type int64 = (Owi.Concrete.Value.int64, Symbolic_value.int64) cs
- and type float32 = (Owi.Concrete.Value.float32, Symbolic_value.float32) cs
- and type float64 = (Owi.Concrete.Value.float64, Symbolic_value.float64) cs
- and type ref_value =
- (Owi.Concrete.Value.ref_value, Symbolic_value.ref_value) cs
Concolic_value.T
Owi.Concolic_wasm_ffi
include Wasm_ffi_intf.S
- with type extern_func = Concolic.P.Extern_func.extern_func
type extern_func = Concolic.P.Extern_func.extern_func
val symbolic_extern_module : extern_func Link.extern_module
val summaries_extern_module : extern_func Link.extern_module
Concrete.Choice
Concrete.Data
val value : t -> string
Concrete.Elem
Concrete.Env
val get_func : t -> int -> Func_intf.t
val get_extern_func : t -> Func_id.t -> Extern_func.extern_func
val drop_elem : Elem.t -> unit
val drop_data : Data.t -> unit
Concrete.Extern_func
type _ telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
Concrete.Global
val typ : t -> Types.binary Types.val_type
Concrete.Memory
val load_8_s : t -> Value.int32 -> Value.int32 Choice.t
val load_8_u : t -> Value.int32 -> Value.int32 Choice.t
val load_16_s : t -> Value.int32 -> Value.int32 Choice.t
val load_16_u : t -> Value.int32 -> Value.int32 Choice.t
val load_32 : t -> Value.int32 -> Value.int32 Choice.t
val load_64 : t -> Value.int32 -> Value.int64 Choice.t
val store_8 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_16 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_32 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_64 : t -> addr:Value.int32 -> Value.int64 -> unit Choice.t
val grow : t -> Value.int32 -> unit
val fill : t -> pos:Value.int32 -> len:Value.int32 -> char -> Value.vbool
val blit :
- t ->
- src:Value.int32 ->
- dst:Value.int32 ->
- len:Value.int32 ->
- Value.vbool
val blit_string :
- t ->
- string ->
- src:Value.int32 ->
- dst:Value.int32 ->
- len:Value.int32 ->
- Value.vbool
val size : t -> Value.int32
val size_in_pages : t -> Value.int32
val get_limit_max : t -> Value.int64 option
Concrete.Module_to_run
Concrete.Table
val get : t -> int -> Value.ref_value
val set : t -> int -> Value.ref_value -> unit
val size : t -> int
val typ : t -> Types.binary Types.ref_type
val max_size : t -> int option
val grow : t -> int32 -> Value.ref_value -> unit
val fill : t -> int32 -> int32 -> Value.ref_value -> unit
Owi.Concrete
include Interpret_intf.P
- with type Env.t = Concrete_value.Func.extern_func Link_env.t
- and type Module_to_run.t =
- Concrete_value.Func.extern_func Link.module_to_run
- and type 'a Choice.t = 'a
- and module Value = V
module Value = V
module Choice : Choice_intf.Base with module V := Value with type 'a t = 'a
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Global : sig ... end
module Table : sig ... end
module Memory : sig ... end
module Extern_func :
- Func_intf.T_Extern_func
- with type int32 := Value.int32
- and type int64 := Value.int64
- and type float32 := Value.float32
- and type float64 := Value.float64
- and type 'a m := 'a Choice.t
- and type memory := Memory.t
module Data : sig ... end
module Elem : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
Owi.Concrete_choice
include Choice_intf.Base with type 'a t = 'a and module V := V
val return : 'a -> 'a t
val select : Owi.V.vbool -> bool t
val select_i32 : Owi.V.int32 -> Int32.t t
val run : 'a t -> 'a
Owi.Concrete_global
runtime global
type t = {
mutable value : Concrete_value.t;
label : string option;
mut : Types.mut;
typ : Types.binary Types.val_type;
}
val value : t -> Concrete_value.t
val set_value : t -> Concrete_value.t -> unit
val typ : t -> Types.binary Types.val_type
Owi.Concrete_memory
val get_limit_max : t -> int64 option
val get_limits : t -> Types.limits
val init : Types.limits -> t
val update_memory : t -> bytes -> unit
val load_8_s : t -> int32 -> int32
val load_8_u : t -> int32 -> int32
val load_16_s : t -> int32 -> int32
val load_16_u : t -> int32 -> int32
val load_32 : t -> int32 -> int32
val load_64 : t -> int32 -> int64
val store_8 : t -> addr:int32 -> int32 -> unit
val store_16 : t -> addr:int32 -> int32 -> unit
val store_32 : t -> addr:int32 -> int32 -> unit
val store_64 : t -> addr:int32 -> int64 -> unit
val grow : t -> int32 -> unit
val fill : t -> pos:int32 -> len:int32 -> char -> bool
val blit : t -> src:int32 -> dst:int32 -> len:int32 -> bool
val blit_string : t -> string -> src:int32 -> dst:int32 -> len:int32 -> bool
val size_in_pages : t -> int32
val size : t -> int32
Owi.Concrete_table
runtime table
type table = Concrete_value.ref_value array
type t = {
id : int;
label : string option;
limits : Types.limits;
typ : Types.binary Types.ref_type;
mutable data : table;
}
val get : t -> int -> Concrete_value.ref_value
val set : t -> int -> Concrete_value.ref_value -> unit
val size : t -> int
val typ : t -> Types.binary Types.ref_type
val init : ?label:string -> Types.binary Types.table_type -> t
val max_size : t -> int option
val grow : t -> int32 -> Concrete_value.ref_value -> unit
val fill : t -> int32 -> int32 -> Concrete_value.ref_value -> unit
Concrete_value.Func
include Func_intf.T_Extern_func
- with type int32 := Int32.t
- with type int64 := Int64.t
- with type float32 := Float32.t
- with type float64 := Float64.t
- with type 'a m := 'a
- with type memory := Concrete_memory.t
val extern_type : extern_func -> Types.binary Types.func_type
type nonrec t = Func_intf.t
val wasm : Types.binary Types.func -> Env_id.t -> t
Make_extern_func.V
Make_extern_func.M
Make_extern_func.Memory
Concrete_value.Make_extern_func
module V : Func_intf.Value_types
module M : Func_intf.Monad_type
module Memory : Func_intf.Memory_type
val extern_type : extern_func -> Types.binary Types.func_type
Owi.Concrete_value
Module to define externref values in OCaml. You should look in the `example` directory to understand how to use this before reading the code...
module Make_extern_func
- (V : Func_intf.Value_types)
- (M : Func_intf.Monad_type)
- (Memory : Func_intf.Memory_type) :
- Func_intf.T_Extern_func
- with type int32 := V.int32
- and type int64 := V.int64
- and type float32 := V.float32
- and type float64 := V.float64
- and type 'a m := 'a M.t
- and type memory := Memory.t
type ref_value =
| Externref of externref option
| Funcref of Func_intf.t option
| Arrayref of unit array option
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val cast_ref : externref -> 'a Prelude.Type.Id.t -> 'a option
val of_instr : Types.binary Types.instr -> t
val to_instr : t -> Types.binary Types.instr
val ref_null' : Types.binary Types.heap_type -> ref_value
val ref_null : Types.binary Types.heap_type -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
val ref_is_null : ref_value -> bool
val pp : Prelude.Fmt.formatter -> t -> unit
Convert.Float32
type t = Float32.t
Convert.Float64
type t = Float64.t
Convert.Int32
val wrap_i64 : int64 -> t
Convert.Int64
Owi.Convert
Various conversion functions between i32, i64, f32 and f64.
module Int32 : sig ... end
module Int64 : sig ... end
module Float32 : sig ... end
module Float64 : sig ... end
Owi.Env_id
val empty : 'a collection
val with_fresh_id :
- (t -> ('a * 'b) Result.t) ->
- 'a collection ->
- ('a collection * 'b) Result.t
val get : t -> 'a collection -> 'a
val map : ('a -> 'b) -> 'a collection -> 'b collection
Owi.Float32
Custom Float32 module for Wasm.
val neg_nan : t
val pos_nan : t
val is_neg_nan : t -> bool
val is_pos_nan : t -> bool
val zero : t
val of_string : string -> t
val to_hex_string : t -> string
val to_string : t -> string
val to_float : t -> Prelude.Float.t
val of_float : Prelude.Float.t -> t
val pp : Prelude.Fmt.formatter -> t -> unit
Owi.Float64
Custom Float64 module for Wasm.
val neg_nan : t
val pos_nan : t
val is_neg_nan : t -> bool
val is_pos_nan : t -> bool
val zero : t
val of_string : string -> t
val to_hex_string : t -> string
val to_string : t -> string
val to_float : t -> Prelude.Float.t
val of_float : Prelude.Float.t -> t
val pp : Prelude.Fmt.formatter -> t -> unit
Owi.Func_id
val empty : 'a collection
val add :
- 'a ->
- Types.binary Types.func_type ->
- 'a collection ->
- t * 'a collection
val get : t -> 'a collection -> 'a
val get_typ : t -> 'a collection -> Types.binary Types.func_type
Owi.Func_intf
module type Value_types = sig ... end
module type Monad_type = sig ... end
module type Memory_type = sig ... end
module type T_Extern_func = sig ... end
module type T = sig ... end
Func_intf.Memory_type
Func_intf.Monad_type
Func_intf.T
type nonrec t = t
val wasm : Types.binary Types.func -> Env_id.t -> t
Func_intf.T_Extern_func
Func_intf.Value_types
Owi.Grouped
type opt_exports = {
global : opt_export list;
mem : opt_export list;
table : opt_export list;
func : opt_export list;
}
type type_check = Types.text Types.indice * Types.text Types.func_type
type t = {
id : string option;
typ : Types.text Types.type_def list;
function_type : Types.text Types.func_type list;
type_checks : type_check list;
global : (Text.global, Types.binary Types.global_type) Runtime.t Indexed.t list;
table : (Types.binary Types.table, Types.binary Types.table_type) Runtime.t
- Indexed.t
- list;
mem : (Types.mem, Types.limits) Runtime.t Indexed.t list;
func : (Types.text Types.func, Types.text Types.block_type) Runtime.t Indexed.t
- list;
elem : Text.elem Indexed.t list;
data : Text.data Indexed.t list;
exports : opt_exports;
start : Types.text Types.indice option;
}
val of_symbolic : Text.modul -> t Result.t
Owi.Imported
Owi.Indexed
val get : 'a t -> 'a
val get_index : 'a t -> int
val return : int -> 'a -> 'a t
val get_at : int -> 'a t list -> 'a option
val has_index : int -> 'a t -> bool
Owi.Int32
Custom Int32 module for Wasm.
val min_int : t
val max_int : t
val zero : t
conversion
val bits_of_float : float -> t
val float_of_bits : t -> float
val of_float : float -> t
val to_float : t -> float
val of_string : string -> t
val of_int : int -> t
val to_int : t -> int
val of_int64 : int64 -> t
val to_int64 : t -> int64
val unsigned_to_int : t -> int option
unary operators
comparison operators
binary operators
Owi.Int64
Custom Int64 module for Wasm.
val min_int : t
val max_int : t
val zero : t
conversion
val bits_of_float : float -> t
val float_of_bits : t -> float
val of_float : float -> t
val to_float : t -> float
val of_string : string -> t
val of_int : int -> t
val to_int : t -> int
val of_int32 : int32 -> t
val to_int32 : t -> int32
unary operators
comparison operators
binary operators
Interpret.Concolic
val modul :
- Concolic.P.Env.t Env_id.collection ->
- Concolic.P.Module_to_run.t ->
- unit Result.t Owi.Concolic.P.Choice.t
Interpret.Concrete
val modul :
- Concrete.Env.t Env_id.collection ->
- Concrete.Module_to_run.t ->
- unit Result.t
val exec_vfunc_from_outside :
- locals:V.t list ->
- env:Link_env.t' ->
- envs:Concrete.Env.t Env_id.collection ->
- Func_intf.t ->
- V.t list Result.t
val exec_ibinop : V.t list -> Types.nn -> Types.ibinop -> V.t list
val exec_iunop : V.t list -> Types.nn -> Types.iunop -> V.t list
val exec_itestop : V.t list -> Types.nn -> Types.itestop -> V.t list
val exec_irelop : V.t list -> Types.nn -> Types.irelop -> V.t list
val exec_fbinop : V.t list -> Types.nn -> Types.fbinop -> V.t list
val exec_funop : V.t list -> Types.nn -> Types.funop -> V.t list
val exec_frelop : V.t list -> Types.nn -> Types.frelop -> V.t list
Interpret.SymbolicM
val modul :
- Symbolic.M.Env.t Env_id.collection ->
- Symbolic.M.Module_to_run.t ->
- unit Result.t Symbolic.M.Choice.t
Interpret.SymbolicP
val modul :
- Symbolic.P.Env.t Env_id.collection ->
- Symbolic.P.Module_to_run.t ->
- unit Result.t Symbolic.P.Choice.t
Owi.Interpret
module Concrete : sig ... end
module SymbolicP : sig ... end
module SymbolicM : sig ... end
module Concolic : sig ... end
Owi.Interpret_intf
P.Choice
P.Data
val value : t -> string
P.Elem
P.Env
val get_func : t -> int -> Func_intf.t
val get_extern_func : t -> Func_id.t -> Extern_func.extern_func
val drop_elem : Elem.t -> unit
val drop_data : Data.t -> unit
P.Extern_func
type _ telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
P.Global
val typ : t -> Types.binary Types.val_type
P.Memory
val load_8_s : t -> Value.int32 -> Value.int32 Choice.t
val load_8_u : t -> Value.int32 -> Value.int32 Choice.t
val load_16_s : t -> Value.int32 -> Value.int32 Choice.t
val load_16_u : t -> Value.int32 -> Value.int32 Choice.t
val load_32 : t -> Value.int32 -> Value.int32 Choice.t
val load_64 : t -> Value.int32 -> Value.int64 Choice.t
val store_8 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_16 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_32 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t
val store_64 : t -> addr:Value.int32 -> Value.int64 -> unit Choice.t
val grow : t -> Value.int32 -> unit
val fill : t -> pos:Value.int32 -> len:Value.int32 -> char -> Value.vbool
val blit :
- t ->
- src:Value.int32 ->
- dst:Value.int32 ->
- len:Value.int32 ->
- Value.vbool
val blit_string :
- t ->
- string ->
- src:Value.int32 ->
- dst:Value.int32 ->
- len:Value.int32 ->
- Value.vbool
val size : t -> Value.int32
val size_in_pages : t -> Value.int32
val get_limit_max : t -> Value.int64 option
P.Module_to_run
val to_run : t -> Types.binary Types.expr list
val modul : t -> Binary.modul
P.Table
val get : t -> int -> Value.ref_value
val set : t -> int -> Value.ref_value -> unit
val size : t -> int
val typ : t -> Types.binary Types.ref_type
val max_size : t -> int option
val grow : t -> int32 -> Value.ref_value -> unit
val fill : t -> int32 -> int32 -> Value.ref_value -> unit
Value.Bool
Value.F32
Value.F64
Value.I32
Value.I64
Value.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
P.Value
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
Interpret_intf.P
module Value : Value_intf.T
module Choice : Choice_intf.Base with module V := Value
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Global : sig ... end
module Table : sig ... end
module Memory : sig ... end
module Extern_func :
- Func_intf.T_Extern_func
- with type int32 := Value.int32
- and type int64 := Value.int64
- and type float32 := Value.float32
- and type float64 := Value.float64
- and type 'a m := 'a Choice.t
- and type memory := Memory.t
module Data : sig ... end
module Elem : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
S.State
Interpret_intf.S
val modul : env Env_id.collection -> module_to_run -> unit Result.t choice
interpret a module
module State : sig ... end
val exec_vfunc_from_outside :
- locals:value list ->
- env:Env_id.t ->
- envs:env Env_id.collection ->
- Func_intf.t ->
- value list Result.t choice
interpret a function with a given input stack and produce a new stack
val exec_iunop : State.stack -> Types.nn -> Types.iunop -> State.stack
val exec_funop : State.stack -> Types.nn -> Types.funop -> State.stack
val exec_ibinop : State.stack -> Types.nn -> Types.ibinop -> State.stack choice
val exec_fbinop : State.stack -> Types.nn -> Types.fbinop -> State.stack
val exec_itestop : State.stack -> Types.nn -> Types.itestop -> State.stack
val exec_irelop : State.stack -> Types.nn -> Types.irelop -> State.stack
val exec_frelop : State.stack -> Types.nn -> Types.frelop -> State.stack
val exec_itruncf :
- State.stack ->
- Types.nn ->
- Types.nn ->
- Types.sx ->
- State.stack
val exec_itruncsatf :
- State.stack ->
- Types.nn ->
- Types.nn ->
- Types.sx ->
- State.stack
val exec_fconverti :
- State.stack ->
- Types.nn ->
- Types.nn ->
- Types.sx ->
- State.stack
val exec_ireinterpretf : State.stack -> Types.nn -> Types.nn -> State.stack
val exec_freinterpreti : State.stack -> Types.nn -> Types.nn -> State.stack
Owi.Kind
type 'extern_func t =
| Wat of Text.modul
| Wast of Text.script
| Wasm of Binary.modul
| Ocaml of 'extern_func Link.extern_module
Owi.Link
Module to link a binary/extern module and producing a runnable module along with a link state.
runtime env
type 'f module_to_run = {
modul : Binary.modul;
env : 'f Link_env.t;
to_run : Types.binary Types.expr list;
}
runnable module
type func := Func_intf.t
type exports = {
globals : Concrete_global.t StringMap.t;
memories : Concrete_memory.t StringMap.t;
tables : Concrete_table.t StringMap.t;
functions : func StringMap.t;
defined_names : StringSet.t;
}
runtime exported items
type 'ext envs = 'ext Link_env.t Env_id.collection
type fenvs = Concrete_value.Func.extern_func Link_env.t Env_id.collection
type 'f state = {
by_name : exports StringMap.t;
by_id : (exports * Env_id.t) StringMap.t;
last : (exports * Env_id.t) option;
collection : 'f Func_id.collection;
envs : 'f envs;
}
link state
val empty_state : 'f state
the empty link state
val modul :
- 'f state ->
- name:string option ->
- Binary.modul ->
- ('f module_to_run * 'f state) Result.t
link a module with a given link state, producing a runnable module and a new link state
register a module inside a link state, producing a new link state
val extern_module' :
- 'f state ->
- name:string ->
- func_typ:('f -> Types.binary Types.func_type) ->
- 'f extern_module ->
- 'f state
register an extern module with a given link state, producing a new link state
val extern_module :
- Concrete_value.Func.extern_func state ->
- name:string ->
- Concrete_value.Func.extern_func extern_module ->
- Concrete_value.Func.extern_func state
type extern_func = Concrete_value.Func.extern_func Func_id.collection
Link_env.Build
val empty : t
val add_global : int -> Concrete_global.t -> t -> t
val add_memory : int -> Concrete_memory.t -> t -> t
val add_table : int -> Concrete_table.t -> t -> t
val get_const_global : t -> int -> Concrete_value.t Result.t
Owi.Link_env
type t' = Env_id.t
type func := Func_intf.t
val get_memory : _ t -> int -> Concrete_memory.t
val get_table : _ t -> int -> Concrete_table.t
val get_global : _ t -> int -> Concrete_global.t
val drop_elem : elem -> unit
val drop_data : data -> unit
module Build : sig ... end
type extern_funcs = Concrete_value.Func.extern_func Func_id.collection
val freeze : t' -> Build.t -> 'ext Func_id.collection -> 'ext t
module type T = sig ... end
module type P = sig ... end
Link_env.P
Link_env.T
val get_memory : t -> int -> Concrete_memory.t Result.t
val get_table : t -> int -> Concrete_table.t Result.t
val get_global : t -> int -> Concrete_global.t Result.t
val drop_elem : elem -> unit
val drop_data : data -> unit
val get_extern_func : t -> Func_id.t -> Concrete_value.Func.extern_func
val get_func_typ : t -> func -> Types.binary Types.func_type
val pp : Prelude.Fmt.formatter -> t -> unit
val freeze : Build.t -> extern_func Func_id.collection -> t
Owi.Log
Module to enable or disable the printing of debug logs.
Owi.Named
val empty : 'a t
val fold : (int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val to_array : 'a t -> 'a array
Owi.Optimize
Optimize module
val modul : Binary.modul -> Binary.modul
Binary.Module
val from_string : string -> Binary.modul Result.t
Parse a module from a string.
val from_channel : Prelude.in_channel -> Binary.modul Result.t
Parse a module from a channel.
val from_file : Fpath.t -> Binary.modul Result.t
Parse a module from a file.
Parse.Binary
module Module : sig ... end
Text.Inline_module
val from_string : string -> Text.modul Result.t
Parse an inline module from a string.
val from_channel : Prelude.in_channel -> Text.modul Result.t
Parse an inline module from a channel.
val from_file : Fpath.t -> Text.modul Result.t
Parse an inline module from a file.
Text.Module
val from_string : string -> Text.modul Result.t
Parse a module from a string.
val from_channel : Prelude.in_channel -> Text.modul Result.t
Parse a module from a channel.
val from_file : Fpath.t -> Text.modul Result.t
Parse a module from a file.
Text.Script
val from_string : string -> Text.script Result.t
Parse a script from a string.
val from_channel : Prelude.in_channel -> Text.script Result.t
Parse a script from a channel.
val from_file : Fpath.t -> Text.script Result.t
Parse a script from a file.
Parse.Text
Owi.Parse
Module providing functions to parse a wasm script from various kind of inputs.
Owi.Result
include module type of Prelude.Result
type err = [
| `Alignment_too_large
| `Assert_failure
| `Bad_result
| `Call_stack_exhausted
| `Constant_expression_required
| `Constant_out_of_range
| `Did_not_fail_but_expected of string
| `Duplicate_export_name
| `Duplicate_global of string
| `Duplicate_local of string
| `Duplicate_memory of string
| `Duplicate_table of string
| `Failed_with_but_expected of err * string
| `Found_bug of int
| `Global_is_immutable
| `Illegal_escape of string
| `Import_after_function
| `Import_after_global
| `Import_after_memory
| `Import_after_table
| `Incompatible_import_type
| `Inline_function_type
| `Invalid_result_arity
| `Lexer_unknown_operator of string
| `Malformed_utf8_encoding of string
| `Memory_size_too_large
| `Msg of string
| `Multiple_memories
| `Multiple_start_sections
| `No_error
| `Parse_fail of string
| `Size_minimum_greater_than_maximum
| `Start_function
| `Timeout
| `Trap of Trap.t
| `Type_mismatch of string
| `Unbound_last_module
| `Unbound_module of string
| `Unbound_name of string
| `Undeclared_function_reference
| `Unexpected_token of string
| `Unknown_data of Types.text Types.indice
| `Unknown_elem of Types.text Types.indice
| `Unknown_func of Types.text Types.indice
| `Unknown_global of Types.text Types.indice
| `Unknown_import of string * string
| `Unknown_label of Types.text Types.indice
| `Unknown_local of Types.text Types.indice
| `Unknown_memory of Types.text Types.indice
| `Unknown_module of string
| `Unknown_operator
| `Unknown_table of Types.text Types.indice
| `Unknown_type of Types.text Types.indice
| `Unsupported_file_extension of string
]
type 'a t = ('a, err) Prelude.Result.t
val err_to_string : err -> string
Owi.Rewrite
val modul : Assigned.t -> Binary.modul Result.t
Owi.Runtime
Owi.Script
Module to execute a full Wasm script.
val exec : no_exhaustion:bool -> optimize:bool -> Text.script -> unit Result.t
execute a Wasm script
Owi.Solver
val fresh : Smtml.Solver_dispatcher.solver_type -> unit -> t
val check : t -> Smtml.Expr.t list -> Smtml.Solver_intf.satisfiability
val model :
- t ->
- symbols:Smtml.Symbol.t list option ->
- pc:Smtml.Expr.t list ->
- Smtml.Model.t
Owi.Spectest
The `spectest` module, to run script from the official test suite.
type extern_module = Concrete_value.Func.extern_func Link.extern_module
val extern_m : extern_module
val m : Text.cmd
the spectest module
V.Bool
V.F32
V.F64
V.I32
V.I64
V.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
Make.V
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
Stack.Make
module V : Value_intf.T
type t = V.t list
val empty : t
val pp : Prelude.Fmt.formatter -> t -> unit
pop operations
val pop_as_ref : t -> V.ref_value * t
push operations
Owi.Stack
module type S = sig ... end
Stack.S
type t = value list
val empty : t
val pp : Prelude.Fmt.formatter -> t -> unit
pop operations
push operations
Owi.String_map
M.Choice
type 'a t = 'a Symbolic_choice_minimalist.t
val return : 'a -> 'a t
val select : Symbolic_value.vbool -> bool t
val select_i32 : Symbolic_value.int32 -> Int32.t t
type 'a run_result = 'a Symbolic_choice_minimalist.run_result
val assertion : Symbolic_value.vbool -> unit t
val with_thread : (Thread_with_memory.t -> 'b) -> 'b t
val thread : Thread_with_memory.t t
val add_pc : Symbolic_value.vbool -> unit t
val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
M.Data
type t = Link_env.data
val value : Link_env.data -> string
M.Elem
M.Env
type t = Extern_func.extern_func Link_env.t
type t' = Env_id.t
val get_memory : 'a Link_env.t -> int -> Memory.t Choice.t
val get_func : 'a Link_env.t -> int -> Func_intf.t
val get_extern_func : 'a Link_env.t -> Func_id.t -> 'a
val get_table : t -> Symbolic_table.ITbl.key -> Table.t Choice.t
val get_elem : 'a Link_env.t -> int -> Link_env.elem
val get_data : 'a Link_env.t -> int -> Link_env.data Choice.t
val drop_data : Link_env.data -> unit
M.Extern_func
type !'b telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
Memory.ITbl
type 'a t = 'a Symbolic_memory_concretizing.ITbl.t
type key = Symbolic_memory_concretizing.ITbl.key
M.Memory
type t = Symbolic_memory_concretizing.t
type collection = Symbolic_memory_concretizing.collection
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
M.Module_to_run
type t =
- MakeP(Symbolic_memory_concretizing)(Thread_with_memory)(Symbolic_choice_minimalist).Module_to_run.t =
- {
modul : Binary.modul;
env : Env.t;
to_run : Types.binary Types.expr list;
}
runnable module
val modul : t -> Binary.modul
val to_run : t -> Types.binary Types.expr list
Symbolic.M
module Value = Symbolic_value
module Choice : sig ... end
module Extern_func : sig ... end
module Global = Symbolic_global
module Table = Symbolic_table
type thread = Thread_with_memory.t
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Elem : sig ... end
module Memory : sig ... end
module Data : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
MakeP.Data
type t = Link_env.data
val value : Link_env.data -> string
MakeP.Elem
MakeP.Env
type t = Extern_func.extern_func Link_env.t
type t' = Env_id.t
val get_memory : 'a Link_env.t -> int -> Memory.t Choice.t
val get_func : 'a Link_env.t -> int -> Func_intf.t
val get_extern_func : 'a Link_env.t -> Func_id.t -> 'a
val get_table : t -> Symbolic_table.ITbl.key -> Table.t Choice.t
val get_elem : 'a Link_env.t -> int -> Link_env.elem
val get_data : 'a Link_env.t -> int -> Link_env.data Choice.t
val drop_data : Link_env.data -> unit
MakeP.Extern_func
type !'b telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
MakeP.Memory
include module type of struct include Memory end
type t = Memory.t
type collection = Memory.collection
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl = Memory.ITbl
val iter : (t ITbl.t -> unit) -> collection -> unit
val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
MakeP.Module_to_run
Memory.ITbl
MakeP.Memory
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val load_8_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_8_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_32 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_64 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val store_8 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_16 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_32 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_64 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
Thread.Memory
type collection = Memory.collection
val init : unit -> collection
val clone : collection -> collection
MakeP.Thread
module Memory : Thread_intf.M with type collection = Memory.collection
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
MakeP.Choice
include Choice_intf.Base with module V := Symbolic_value
val return : 'a -> 'a t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
val assertion : Owi.Symbolic_value.vbool -> unit t
val add_pc : Owi.Symbolic_value.vbool -> unit t
val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
Symbolic.MakeP
module Memory : Symbolic_memory_intf.S
module Thread : Thread.S with type Memory.collection = Memory.collection
module Choice :
- Choice_intf.Complete
- with module V := Symbolic_value
- and type thread := Thread.t
module Value = Symbolic_value
module Choice = Choice
module Extern_func : sig ... end
module Global = Symbolic_global
module Table = Symbolic_table
type thread = Thread.t
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Elem : sig ... end
module Memory : sig ... end
module Data : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
P.Choice
type 'a t = 'a Symbolic_choice_with_memory.t
val return : 'a -> 'a t
val select : Symbolic_value.vbool -> bool t
val select_i32 : Symbolic_value.int32 -> Int32.t t
type 'a run_result = 'a Symbolic_choice_with_memory.run_result
val assertion : Symbolic_value.vbool -> unit t
val with_thread : (Thread_with_memory.t -> 'b) -> 'b t
val thread : Thread_with_memory.t t
val add_pc : Symbolic_value.vbool -> unit t
val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
P.Data
type t = Link_env.data
val value : Link_env.data -> string
P.Elem
P.Env
type t = Extern_func.extern_func Link_env.t
type t' = Env_id.t
val get_memory : 'a Link_env.t -> int -> Memory.t Choice.t
val get_func : 'a Link_env.t -> int -> Func_intf.t
val get_extern_func : 'a Link_env.t -> Func_id.t -> 'a
val get_table : t -> Symbolic_table.ITbl.key -> Table.t Choice.t
val get_elem : 'a Link_env.t -> int -> Link_env.elem
val get_data : 'a Link_env.t -> int -> Link_env.data Choice.t
val drop_data : Link_env.data -> unit
P.Extern_func
type !'b telt =
| I32 : Value.int32 telt
| I64 : Value.int64 telt
| F32 : Value.float32 telt
| F64 : Value.float64 telt
| Externref : 'a Prelude.Type.Id.t -> 'a telt
val extern_type : extern_func -> Types.binary Types.func_type
Memory.ITbl
type 'a t = 'a Symbolic_memory_concretizing.ITbl.t
type key = Symbolic_memory_concretizing.ITbl.key
P.Memory
type t = Symbolic_memory_concretizing.t
type collection = Symbolic_memory_concretizing.collection
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32 Choice.t
P.Module_to_run
type t =
- MakeP(Symbolic_memory_concretizing)(Thread_with_memory)(Symbolic_choice_with_memory).Module_to_run.t =
- {
modul : Binary.modul;
env : Env.t;
to_run : Types.binary Types.expr list;
}
runnable module
val modul : t -> Binary.modul
val to_run : t -> Types.binary Types.expr list
Symbolic.P
module Value = Symbolic_value
module Choice : sig ... end
module Extern_func : sig ... end
module Global = Symbolic_global
module Table = Symbolic_table
type thread = Thread_with_memory.t
val select :
- Value.vbool ->
- if_true:Value.t ->
- if_false:Value.t ->
- Value.t Choice.t
module Elem : sig ... end
module Memory : sig ... end
module Data : sig ... end
module Env : sig ... end
module Module_to_run : sig ... end
Owi.Symbolic
module MakeP
- (Memory : Symbolic_memory_intf.S)
- (Thread : Thread.S with type Memory.collection = Memory.collection)
- (Choice :
- Choice_intf.Complete
- with module V := Symbolic_value
- and type thread := Thread.t) :
- sig ... end
module P : sig ... end
module M : sig ... end
val convert_module_to_run :
- P.Extern_func.extern_func Link.module_to_run ->
- P.Module_to_run.t
val convert_module_to_run_minimalist :
- M.Extern_func.extern_func Link.module_to_run ->
- M.Module_to_run.t
CoreImpl.State
Symbolic_choice.CoreImpl
module State : sig ... end
Thread.Memory
Make.Thread
module Memory : Thread_intf.M
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
Symbolic_choice.Make
type 'a t = ('a Symbolic_choice_intf.eval, Thread.t) CoreImpl.State.t
val return : 'a -> 'a t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
val assertion : Owi.Symbolic_value.vbool -> unit t
val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
val add_pc : Owi.Symbolic_value.vbool -> unit t
type 'a run_result = ('a Symbolic_choice_intf.eval * Thread.t) Prelude.Seq.t
val run :
- workers:int ->
- Smtml.Solver_dispatcher.solver_type ->
- 'a t ->
- Thread.t ->
- callback:(('a Symbolic_choice_intf.eval * Thread.t) -> unit) ->
- callback_init:(unit -> unit) ->
- callback_end:(unit -> unit) ->
- unit Prelude.Domain.t array
Owi.Symbolic_choice
module type S = Symbolic_choice_intf.S
module CoreImpl : sig ... end
module Make
- (Thread : Thread.S) :
- S
- with type 'a t = ('a Symbolic_choice_intf.eval, Thread.t) CoreImpl.State.t
- and type thread := Thread.t
- and module V := Symbolic_value
Owi.Symbolic_choice_intf
type 'a eval =
| EVal of 'a
| ETrap of Trap.t * Smtml.Model.t
| EAssert of Smtml.Expr.t * Smtml.Model.t
module type S = sig ... end
module type Intf = sig ... end
CoreImpl.State
Intf.CoreImpl
module State : sig ... end
Thread.Memory
Make.Thread
module Memory : Thread_intf.M
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
Intf.Make
type 'a t = ('a eval, Thread.t) CoreImpl.State.t
val return : 'a -> 'a t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
val assertion : Owi.Symbolic_value.vbool -> unit t
val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
val add_pc : Owi.Symbolic_value.vbool -> unit t
Symbolic_choice_intf.Intf
S.V
Symbolic_choice_intf.S
module V : Func_intf.Value_types
val return : 'a -> 'a t
val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
Owi.Symbolic_choice_minimalist
include Choice_intf.Complete
- with type thread := Thread_with_memory.t
- and type 'a run_result = ('a, err) Prelude.Result.t * Thread_with_memory.t
- and module V := Symbolic_value
include Choice_intf.Base with module V := Symbolic_value
val return : 'a -> 'a t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
type 'a run_result = ('a, err) Prelude.Result.t * Thread_with_memory.t
val assertion : Owi.Symbolic_value.vbool -> unit t
val with_thread : (Thread_with_memory.t -> 'b) -> 'b t
val thread : Thread_with_memory.t t
val add_pc : Owi.Symbolic_value.vbool -> unit t
val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
val run :
- workers:int ->
- Smtml.Solver_dispatcher.solver_type ->
- 'a t ->
- Thread_with_memory.t ->
- 'a run_result
Owi.Symbolic_choice_with_memory
include Symbolic_choice_intf.S
- with type 'a t =
- ('a Symbolic_choice_intf.eval, Thread_with_memory.t)
- Symbolic_choice.CoreImpl.State.t
- and type thread := Thread_with_memory.t
- and module V := Symbolic_value
type 'a t =
- ('a Symbolic_choice_intf.eval, Thread_with_memory.t)
- Symbolic_choice.CoreImpl.State.t
val return : 'a -> 'a t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
val assertion : Owi.Symbolic_value.vbool -> unit t
val with_thread : (Thread_with_memory.t -> 'a) -> 'a t
val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
val thread : Thread_with_memory.t t
val add_pc : Owi.Symbolic_value.vbool -> unit t
type 'a run_result =
- ('a Symbolic_choice_intf.eval * Thread_with_memory.t) Prelude.Seq.t
val run :
- workers:int ->
- Smtml.Solver_dispatcher.solver_type ->
- 'a t ->
- Thread_with_memory.t ->
- callback:(('a Symbolic_choice_intf.eval * Thread_with_memory.t) -> unit) ->
- callback_init:(unit -> unit) ->
- callback_end:(unit -> unit) ->
- unit Prelude.Domain.t array
val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t
Owi.Symbolic_choice_without_memory
include Symbolic_choice_intf.S
- with type 'a t =
- ('a Symbolic_choice_intf.eval, Thread_without_memory.t)
- Symbolic_choice.CoreImpl.State.t
- and type thread := Thread_without_memory.t
- and module V := Symbolic_value
type 'a t =
- ('a Symbolic_choice_intf.eval, Thread_without_memory.t)
- Symbolic_choice.CoreImpl.State.t
val return : 'a -> 'a t
val select : Owi.Symbolic_value.vbool -> bool t
val select_i32 : Owi.Symbolic_value.int32 -> Int32.t t
val assertion : Owi.Symbolic_value.vbool -> unit t
val with_thread : (Thread_without_memory.t -> 'a) -> 'a t
val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
val thread : Thread_without_memory.t t
val add_pc : Owi.Symbolic_value.vbool -> unit t
type 'a run_result =
- ('a Symbolic_choice_intf.eval * Thread_without_memory.t) Prelude.Seq.t
val run :
- workers:int ->
- Smtml.Solver_dispatcher.solver_type ->
- 'a t ->
- Thread_without_memory.t ->
- callback:(('a Symbolic_choice_intf.eval * Thread_without_memory.t) -> unit) ->
- callback_init:(unit -> unit) ->
- callback_end:(unit -> unit) ->
- unit Prelude.Domain.t array
Owi.Symbolic_global
val init : unit -> collection
val clone : collection -> collection
val get_global : Env_id.t -> Concrete_global.t -> collection -> int -> t
val typ : t -> Types.binary Types.val_type
val value : t -> Symbolic_value.t
val set_value : t -> Symbolic_value.t -> unit
Symbolic_memory.ITbl
Owi.Symbolic_memory
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val check_within_bounds :
- t ->
- Smtml.Expr.t ->
- (Smtml.Expr.t * Symbolic_value.int32, Trap.t) Prelude.result
val load_8_s : t -> Smtml.Expr.t -> Symbolic_value.int32
val load_8_u : t -> Smtml.Expr.t -> Symbolic_value.int32
val load_16_s : t -> Smtml.Expr.t -> Symbolic_value.int32
val load_16_u : t -> Smtml.Expr.t -> Symbolic_value.int32
val load_32 : t -> Smtml.Expr.t -> Symbolic_value.int32
val load_64 : t -> Smtml.Expr.t -> Symbolic_value.int32
val store_8 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
val store_16 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
val store_32 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
val store_64 : t -> addr:Smtml.Expr.t -> Smtml.Expr.t -> unit
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
Symbolic_memory_concretizing.ITbl
Owi.Symbolic_memory_concretizing
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val load_8_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_8_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_32 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_64 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val store_8 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_16 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_32 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_64 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
Owi.Symbolic_memory_intf
Make.ITbl
Make._
val address : Smtml.Expr.t -> address Symbolic_choice_without_memory.t
val make : unit -> t
val validate_address :
- t ->
- Smtml.Expr.t ->
- int ->
- (Smtml.Expr.t, Trap.t) Prelude.result Symbolic_choice_without_memory.t
validate_address m a range
verifies whether an operation starting at address a
is valid within the address range a
to a + range - 1
(inclusive).
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
Intf.Make
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val load_8_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_8_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_32 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_64 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val store_8 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_16 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_32 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_64 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
Symbolic_memory_intf.Intf
Symbolic_memory_intf.M
val address : Smtml.Expr.t -> address Symbolic_choice_without_memory.t
val make : unit -> t
val validate_address :
- t ->
- Smtml.Expr.t ->
- int ->
- (Smtml.Expr.t, Trap.t) Prelude.result Symbolic_choice_without_memory.t
validate_address m a range
verifies whether an operation starting at address a
is valid within the address range a
to a + range - 1
(inclusive).
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
S.ITbl
Symbolic_memory_intf.S
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val load_8_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_8_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_32 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_64 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val store_8 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_16 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_32 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_64 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
Make.ITbl
Make._
val address : Smtml.Expr.t -> address Symbolic_choice_without_memory.t
val make : unit -> t
val validate_address :
- t ->
- Smtml.Expr.t ->
- int ->
- (Smtml.Expr.t, Trap.t) Prelude.result Symbolic_choice_without_memory.t
validate_address m a range
verifies whether an operation starting at address a
is valid within the address range a
to a + range - 1
(inclusive).
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
Symbolic_memory_make.Make
val init : unit -> collection
val clone : collection -> collection
val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t
val realloc :
- t ->
- ptr:Smtml.Expr.t ->
- size:Smtml.Expr.t ->
- Smtml.Expr.t Symbolic_choice_without_memory.t
val free : t -> Smtml.Expr.t -> unit Symbolic_choice_without_memory.t
val load_8_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_8_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_s :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_16_u :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_32 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val load_64 :
- t ->
- Smtml.Expr.t ->
- Symbolic_value.int32 Symbolic_choice_without_memory.t
val store_8 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_16 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_32 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val store_64 :
- t ->
- addr:Smtml.Expr.t ->
- Smtml.Expr.t ->
- unit Symbolic_choice_without_memory.t
val grow : t -> Smtml.Expr.t -> unit
val fill : t -> pos:Smtml.Expr.t -> len:Smtml.Expr.t -> char -> Smtml.Expr.t
val blit :
- t ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val blit_string :
- t ->
- string ->
- src:Smtml.Expr.t ->
- dst:Smtml.Expr.t ->
- len:Smtml.Expr.t ->
- Smtml.Expr.t
val size : t -> Smtml.Expr.t
val size_in_pages : t -> Smtml.Expr.t
val get_limit_max : t -> Smtml.Expr.t option
module ITbl : sig ... end
val iter : (t ITbl.t -> unit) -> collection -> unit
Owi.Symbolic_memory_make
Symbolic_table.ITbl
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val length : 'a t -> int
val stats : 'a t -> Stdlib__Hashtbl.statistics
val to_seq_values : 'a t -> 'a Stdlib.Seq.t
Owi.Symbolic_table
module ITbl : sig ... end
type t = {
mutable data : Symbolic_value.ref_value array;
limits : Types.limits;
typ : Types.binary Types.ref_type;
}
val clone : collection -> t ITbl.t Owi.Env_id.Tbl.t
val convert_ref_values : Concrete_value.ref_value -> Symbolic_value.ref_value
val convert : Concrete_table.t -> t
val get_table :
- Owi.Env_id.Tbl.key ->
- Concrete_table.t ->
- collection ->
- ITbl.key ->
- t
val get : t -> int -> Symbolic_value.ref_value
val set : t -> int -> Symbolic_value.ref_value -> unit
val size : t -> int
val typ : t -> Types.binary Types.ref_type
val max_size : t -> int option
val grow : t -> Int32.t -> Symbolic_value.ref_value -> unit
val fill : t -> Int32.t -> Int32.t -> Symbolic_value.ref_value -> unit
Symbolic_value.Bool
Symbolic_value.F32
Symbolic_value.F64
Symbolic_value.I32
Symbolic_value.I64
Symbolic_value.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
Owi.Symbolic_value
include Value_intf.T
- with type ref_value := ref_value
- with type vbool = Smtml.Expr.t
- and type int32 = Smtml.Expr.t
- and type int64 = Smtml.Expr.t
- and type float32 = Smtml.Expr.t
- and type float64 = Smtml.Expr.t
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
module Bool : sig ... end
Owi.Symbolic_wasm_ffi
include Wasm_ffi_intf.S
- with type extern_func = Symbolic.P.Extern_func.extern_func
type extern_func = Symbolic.P.Extern_func.extern_func
val symbolic_extern_module : extern_func Link.extern_module
val summaries_extern_module : extern_func Link.extern_module
Owi.Synchronizer
val init :
- (unit -> 'get option) ->
- ('write -> Prelude.Condition.t -> unit) ->
- ('get, 'write) t
val get : ('get, 'write) t -> bool -> 'get option
val write : 'write -> ('get, 'write) t -> unit
val make_pledge : ('get, 'write) t -> unit
val end_pledge : ('get, 'write) t -> unit
val fail : ('get, 'write) t -> unit
val work_while : ('get -> ('write -> unit) -> unit) -> ('get, 'write) t -> unit
Owi.Syntax
Owi.Text
val symbolic : string -> < string_indices : Types.yes.. > Types.indice
val raw : int -> < .. > Types.indice
val bt_ind : < raw_bt : Types.yes.. > as 'a Types.indice -> 'a Types.block_type
val bt_raw :
- 'b as 'a Types.indice option ->
- ('a Types.param_type * 'a Types.result_type) ->
- 'a Types.block_type
val pp_global : Stdlib.Format.formatter -> global -> Prelude.Unit.t
type data_mode =
| Data_passive
| Data_active of Types.text Types.indice option * Types.text Types.expr
val pp_data_mode : Stdlib.Format.formatter -> data_mode -> Prelude.Unit.t
val pp_data : Stdlib.Format.formatter -> data -> Prelude.Unit.t
type elem_mode =
| Elem_passive
| Elem_active of Types.text Types.indice option * Types.text Types.expr
| Elem_declarative
val pp_elem_mode : Stdlib.Format.formatter -> elem_mode -> Prelude.Unit.t
type elem = {
id : string option;
typ : Types.text Types.ref_type;
init : Types.text Types.expr list;
mode : elem_mode;
}
val pp_elem_expr : Stdlib.Format.formatter -> 'a Types.expr -> Prelude.Unit.t
val pp_elem : Stdlib.Format.formatter -> elem -> Prelude.Unit.t
type module_field =
| MType of Types.text Types.rec_type
| MGlobal of global
| MTable of Types.text Types.table
| MMem of Types.mem
| MFunc of Types.text Types.func
| MElem of elem
| MData of data
| MStart of Types.text Types.indice
| MImport of Types.text Types.import
| MExport of Types.text Types.export
val pp_module_field : Stdlib.Format.formatter -> module_field -> Prelude.Unit.t
val pp_modul : Stdlib.Format.formatter -> modul -> unit
type action =
| Invoke of string option * string * Types.text Types.const list
| Get of string option * string
val pp_action : Stdlib.Format.formatter -> action -> unit
type result_const =
| Literal of Types.text Types.const
| Nan_canon of Types.nn
| Nan_arith of Types.nn
val pp_result_const : Stdlib.Format.formatter -> result_const -> unit
val pp_result : Stdlib.Format.formatter -> result -> unit
val pp_result_bis : Stdlib.Format.formatter -> result -> unit
val pp_results : Stdlib.Format.formatter -> result list -> unit
type assertion =
| Assert_return of action * result list
| Assert_trap of action * string
| Assert_trap_module of modul * string
| Assert_malformed of modul * string
| Assert_malformed_quote of string * string
| Assert_malformed_binary of string * string
| Assert_invalid of modul * string
| Assert_invalid_quote of string * string
| Assert_invalid_binary of string * string
| Assert_exhaustion of action * string
| Assert_unlinkable of modul * string
val pp_assertion : Stdlib.Format.formatter -> assertion -> unit
val pp_cmd : Stdlib.Format.formatter -> cmd -> unit
type script = cmd list
val pp_script : Stdlib.Format.formatter -> cmd list -> unit
Owi.Text_lexer
Module for Wasm lexing.
val token : Sedlexing.lexbuf -> Text_parser.token
tokenizer
val lexer :
- Sedlexing.lexbuf ->
- unit ->
- Text_parser.token * Prelude.Lexing.position * Prelude.Lexing.position
lexer
Text_parser.Incremental
val script :
- Prelude.Lexing.position ->
- Text.script MenhirInterpreter.checkpoint
val modul : Prelude.Lexing.position -> Text.modul MenhirInterpreter.checkpoint
val inline_module :
- Prelude.Lexing.position ->
- Text.modul MenhirInterpreter.checkpoint
Text_parser.MenhirInterpreter
include MenhirLib.IncrementalEngine.INCREMENTAL_ENGINE with type token = token
type token = token
val offer :
- 'a checkpoint ->
- (token
- * MenhirLib.IncrementalEngine.position
- * MenhirLib.IncrementalEngine.position) ->
- 'a checkpoint
val resume : ?strategy:strategy -> 'a checkpoint -> 'a checkpoint
type supplier =
- unit ->
- token
- * MenhirLib.IncrementalEngine.position
- * MenhirLib.IncrementalEngine.position
val loop : ?strategy:strategy -> supplier -> 'a checkpoint -> 'a
val loop_handle :
- ('a -> 'answer) ->
- ('a checkpoint -> 'answer) ->
- supplier ->
- 'a checkpoint ->
- 'answer
val loop_handle_undo :
- ('a -> 'answer) ->
- ('a checkpoint -> 'a checkpoint -> 'answer) ->
- supplier ->
- 'a checkpoint ->
- 'answer
val shifts : 'a checkpoint -> 'a env option
val acceptable :
- 'a checkpoint ->
- token ->
- MenhirLib.IncrementalEngine.position ->
- bool
val number : 'a lr1state -> int
val production_index : production -> int
val find_production : int -> production
type stack = element MenhirLib.General.stream
val current_state_number : 'a env -> int
val positions :
- 'a env ->
- MenhirLib.IncrementalEngine.position * MenhirLib.IncrementalEngine.position
val env_has_default_reduction : 'a env -> bool
val state_has_default_reduction : 'a lr1state -> bool
val force_reduction : production -> 'a env -> 'a env
val input_needed : 'a env -> 'a checkpoint
Owi.Text_parser
type token =
| UNREACHABLE
| TYPE
| THEN
| TABLE_SIZE
| TABLE_SET
| TABLE_INIT
| TABLE_GROW
| TABLE_GET
| TABLE_FILL
| TABLE_COPY
| TABLE
| SUB
| STRUCT_SET
| STRUCT_NEW_CANON_DEFAULT
| STRUCT_NEW_CANON
| STRUCT_GET_S
| STRUCT_GET
| STRUCTREF
| STRUCT
| START
| SELECT
| RPAR
| RETURN_CALL_REF
| RETURN_CALL_INDIRECT
| RETURN_CALL
| RETURN
| RESULT
| REGISTER
| REF_TEST
| REF_STRUCT
| REF_NULL
| REF_IS_NULL
| REF_I31
| REF_HOST
| REF_FUNC
| REF_EXTERN
| REF_EQ
| REF_CAST
| REF_AS_NON_NULL
| REF_ARRAY
| REF
| REC
| QUOTE
| PARAM
| OFFSET
| NUM of Prelude.String.t
| NULL_REF
| NULL_FUNC_REF
| NULL_EXTERN_REF
| NULL
| NOP
| NONE
| NOFUNC
| NOEXTERN
| NAN_CANON
| NAN_ARITH
| NAME of Prelude.String.t
| MUTABLE
| MODULE
| MEMORY_SIZE
| MEMORY_INIT
| MEMORY_GROW
| MEMORY_FILL
| MEMORY_COPY
| MEMORY
| LPAR
| LOOP
| LOCAL_TEE
| LOCAL_SET
| LOCAL_GET
| LOCAL
| ITEM
| INVOKE
| IMPORT
| IF
| ID of Prelude.String.t
| I8
| I64_XOR
| I64_TRUNC_SAT_F64_U
| I64_TRUNC_SAT_F64_S
| I64_TRUNC_SAT_F32_U
| I64_TRUNC_SAT_F32_S
| I64_TRUNC_F64_U
| I64_TRUNC_F64_S
| I64_TRUNC_F32_U
| I64_TRUNC_F32_S
| I64_SUB
| I64_STORE8
| I64_STORE32
| I64_STORE16
| I64_STORE
| I64_SHR_U
| I64_SHR_S
| I64_SHL
| I64_ROTR
| I64_ROTL
| I64_REM_U
| I64_REM_S
| I64_REINTERPRET_F64
| I64_REINTERPRET_F32
| I64_POPCNT
| I64_OR
| I64_NE
| I64_MUL
| I64_LT_U
| I64_LT_S
| I64_LOAD8_U
| I64_LOAD8_S
| I64_LOAD32_U
| I64_LOAD32_S
| I64_LOAD16_U
| I64_LOAD16_S
| I64_LOAD
| I64_LE_U
| I64_LE_S
| I64_GT_U
| I64_GT_S
| I64_GE_U
| I64_GE_S
| I64_EXTEND_I32_U
| I64_EXTEND_I32_S
| I64_EXTEND8_S
| I64_EXTEND32_S
| I64_EXTEND16_S
| I64_EQZ
| I64_EQ
| I64_DIV_U
| I64_DIV_S
| I64_CTZ
| I64_CONST
| I64_CLZ
| I64_AND
| I64_ADD
| I64
| I32_XOR
| I32_WRAP_I64
| I32_TRUNC_SAT_F64_U
| I32_TRUNC_SAT_F64_S
| I32_TRUNC_SAT_F32_U
| I32_TRUNC_SAT_F32_S
| I32_TRUNC_F64_U
| I32_TRUNC_F64_S
| I32_TRUNC_F32_U
| I32_TRUNC_F32_S
| I32_SUB
| I32_STORE8
| I32_STORE16
| I32_STORE
| I32_SHR_U
| I32_SHR_S
| I32_SHL
| I32_ROTR
| I32_ROTL
| I32_REM_U
| I32_REM_S
| I32_REINTERPRET_F64
| I32_REINTERPRET_F32
| I32_POPCNT
| I32_OR
| I32_NE
| I32_MUL
| I32_LT_U
| I32_LT_S
| I32_LOAD8_U
| I32_LOAD8_S
| I32_LOAD16_U
| I32_LOAD16_S
| I32_LOAD
| I32_LE_U
| I32_LE_S
| I32_GT_U
| I32_GT_S
| I32_GE_U
| I32_GE_S
| I32_EXTEND8_S
| I32_EXTEND16_S
| I32_EQZ
| I32_EQ
| I32_DIV_U
| I32_DIV_S
| I32_CTZ
| I32_CONST
| I32_CLZ
| I32_AND
| I32_ADD
| I32
| I31_REF
| I31_GET_U
| I31_GET_S
| I31
| I16
| GLOBAL_SET
| GLOBAL_GET
| GLOBAL
| GET
| FUNC_REF
| FUNC
| FINAL
| FIELD
| F64_TRUNC
| F64_SUB
| F64_STORE
| F64_SQRT
| F64_REINTERPRET_I64
| F64_REINTERPRET_I32
| F64_PROMOTE_F32
| F64_NEG
| F64_NEAREST
| F64_NE
| F64_MUL
| F64_MIN
| F64_MAX
| F64_LT
| F64_LOAD
| F64_LE
| F64_GT
| F64_GE
| F64_FLOOR
| F64_EQ
| F64_DIV
| F64_COPYSIGN
| F64_CONVERT_I64_U
| F64_CONVERT_I64_S
| F64_CONVERT_I32_U
| F64_CONVERT_I32_S
| F64_CONST
| F64_CEIL
| F64_ADD
| F64_ABS
| F64
| F32_TRUNC
| F32_SUB
| F32_STORE
| F32_SQRT
| F32_REINTERPRET_I64
| F32_REINTERPRET_I32
| F32_NEG
| F32_NEAREST
| F32_NE
| F32_MUL
| F32_MIN
| F32_MAX
| F32_LT
| F32_LOAD
| F32_LE
| F32_GT
| F32_GE
| F32_FLOOR
| F32_EQ
| F32_DIV
| F32_DEMOTE_F64
| F32_COPYSIGN
| F32_CONVERT_I64_U
| F32_CONVERT_I64_S
| F32_CONVERT_I32_U
| F32_CONVERT_I32_S
| F32_CONST
| F32_CEIL
| F32_ADD
| F32_ABS
| F32
| EXTERN_REF
| EXTERN_INTERNALIZE
| EXTERN_EXTERNALIZE
| EXTERN
| EXPORT
| EQ_REF
| EQUAL
| EQ
| EOF
| END
| ELSE
| ELEM_DROP
| ELEM
| DROP
| DECLARE
| DATA_DROP
| DATA
| CALL_REF
| CALL_INDIRECT
| CALL
| BR_TABLE
| BR_ON_NULL
| BR_ON_NON_NULL
| BR_ON_CAST_FAIL
| BR_ON_CAST
| BR_IF
| BR
| BLOCK
| BINARY
| ASSERT_UNLINKABLE
| ASSERT_TRAP
| ASSERT_RETURN
| ASSERT_MALFORMED
| ASSERT_INVALID
| ASSERT_EXHAUSTION
| ARRAY_SET
| ARRAY_REF
| ARRAY_NEW_CANON_FIXED
| ARRAY_NEW_CANON_ELEM
| ARRAY_NEW_CANON_DEFAULT
| ARRAY_NEW_CANON_DATA
| ARRAY_NEW_CANON
| ARRAY_LEN
| ARRAY_GET_U
| ARRAY_GET
| ARRAY
| ANY_REF
| ANY
| ALIGN
val script :
- (Prelude.Lexing.lexbuf -> token) ->
- Prelude.Lexing.lexbuf ->
- Text.script
val modul :
- (Prelude.Lexing.lexbuf -> token) ->
- Prelude.Lexing.lexbuf ->
- Text.modul
val inline_module :
- (Prelude.Lexing.lexbuf -> token) ->
- Prelude.Lexing.lexbuf ->
- Text.modul
module MenhirInterpreter : sig ... end
module Incremental : sig ... end
Owi.Text_validate
Initial check done on a module.
val modul : Text.modul -> Text.modul Result.t
check a module
Make.Memory
type collection = Symbolic_memory.collection
val init : unit -> collection
val clone : collection -> collection
Make.Symbolic_memory
Thread.Make
module Symbolic_memory : M
module Memory : Thread_intf.M with type collection = Symbolic_memory.collection
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
Owi.Thread
module type M = Thread_intf.M
module type S = Thread_intf.S
module Make
- (Symbolic_memory : M) :
- S with type Memory.collection = Symbolic_memory.collection
Owi.Thread_intf
Make.Memory
type collection = Symbolic_memory.collection
val init : unit -> collection
val clone : collection -> collection
Make.Symbolic_memory
Intf.Make
module Symbolic_memory : M
module Memory : M with type collection = Symbolic_memory.collection
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
Thread_intf.Intf
module type M = M
module type S = S
module Make
- (Symbolic_memory : M) :
- S with type Memory.collection = Symbolic_memory.collection
Thread_intf.M
S.Memory
Thread_intf.S
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
Thread_with_memory.Memory
type collection = Symbolic_memory_concretizing.collection
val init : unit -> collection
val clone : collection -> collection
Owi.Thread_with_memory
module Memory :
- Thread_intf.M with type collection = Symbolic_memory_concretizing.collection
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
val project : t -> Thread_without_memory.t * Memory.collection
val restore : Memory.collection -> Thread_without_memory.t -> t
Thread_without_memory.Memory
Owi.Thread_without_memory
module Memory : Thread_intf.M with type collection = bool
val init : unit -> t
val create :
- int ->
- Smtml.Symbol.t list ->
- Symbolic_value.vbool list ->
- Memory.collection ->
- Symbolic_table.collection ->
- Symbolic_global.collection ->
- int32 list ->
- t
val pc : t -> Symbolic_value.vbool list
val memories : t -> Memory.collection
val tables : t -> Symbolic_table.collection
val globals : t -> Symbolic_global.collection
val breadcrumbs : t -> int32 list
val symbols_set : t -> Smtml.Symbol.t list
val symbols : t -> int
val add_pc : t -> Symbolic_value.vbool -> t
Owi.Tracing
Owi.Trap
type t =
| Out_of_bounds_table_access
| Out_of_bounds_memory_access
| Undefined_element
| Uninitialized_element of int
| Integer_overflow
| Integer_divide_by_zero
| Element_type_error
| Unreachable
| Indirect_call_type_mismatch
| Extern_call_arg_type_mismatch
| Extern_call_null_arg
| Memory_leak_use_after_free
| Memory_heap_buffer_overflow
val to_string : t -> string
Owi.Types
type with_string_indices = < string_indices : yes >
type without_string_indices = < string_indices : no >
type with_ind_bt = < raw_bt : yes >
type without_ind_bt = < raw_bt : no >
type text = < with_string_indices ; with_ind_bt >
type binary = < without_string_indices ; without_ind_bt >
val pp_indice : Stdlib.Format.formatter -> 'kind indice -> unit
val pp_indice_opt : Stdlib.Format.formatter -> 'a indice option -> unit
val pp_indices : Stdlib.Format.formatter -> 'a indice list -> unit
val pp_num_type : Stdlib.Format.formatter -> num_type -> unit
val pp_nullable : Stdlib.Format.formatter -> nullable -> unit
val pp_packed_type : Stdlib.Format.formatter -> packed_type -> unit
val packed_type_eq : packed_type -> packed_type -> bool
val pp_mut : Stdlib.Format.formatter -> mut -> unit
val pp_nn : Stdlib.Format.formatter -> nn -> unit
val pp_sx : Stdlib.Format.formatter -> sx -> unit
val pp_iunop : Stdlib.Format.formatter -> iunop -> unit
val pp_funop : Stdlib.Format.formatter -> funop -> unit
val pp_ibinop : Stdlib.Format.formatter -> ibinop -> unit
val pp_fbinop : Stdlib.Format.formatter -> fbinop -> unit
val pp_itestop : Stdlib.Format.formatter -> itestop -> unit
val pp_irelop : Stdlib.Format.formatter -> irelop -> Prelude.Unit.t
val frelop : Stdlib.Format.formatter -> frelop -> Prelude.Unit.t
val pp_memarg : Stdlib.Format.formatter -> memarg -> unit
val pp_limits : Stdlib.Format.formatter -> limits -> unit
type nonrec mem = string option * limits
val pp_mem : Stdlib.Format.formatter -> (string option * limits) -> unit
val pp_final : Stdlib.Format.formatter -> final -> unit
Structure
Types
type 'a heap_type =
| Any_ht
| None_ht
| Eq_ht
| I31_ht
| Struct_ht
| Array_ht
| Func_ht
| No_func_ht
| Extern_ht
| No_extern_ht
| Def_ht of 'a indice
val pp_heap_type : Stdlib.Format.formatter -> 'a heap_type -> unit
val pp_heap_type_short : Stdlib.Format.formatter -> 'a heap_type -> unit
val pp_val_type : Stdlib.Format.formatter -> 'a val_type -> unit
type nonrec 'a param = string option * 'a val_type
val pp_param : Stdlib.Format.formatter -> (string option * 'a val_type) -> unit
type nonrec 'a param_type = 'a param list
val pp_param_type :
- Stdlib.Format.formatter ->
- (string option * 'a val_type) list ->
- unit
type nonrec 'a result_type = 'a val_type list
val pp_result_ : Stdlib.Format.formatter -> 'a val_type -> unit
val pp_result_type : Stdlib.Format.formatter -> 'a val_type list -> unit
type 'a block_type =
| Bt_ind : 'a indice -> < with_ind_bt.. > as 'a block_type
| Bt_raw : ('a indice option * ('a param_type * 'a result_type)) -> < .. > as 'a
- block_type
val pp_block_type : Stdlib.Format.formatter -> 'kind block_type -> unit
val pp_block_type_opt : Stdlib.Format.formatter -> 'a block_type option -> unit
type nonrec 'a func_type = 'a param_type * 'a result_type
type nonrec 'a extern_type =
| Func of string option * 'a func_type
| Table of string option * 'a table_type
| Mem of string option * limits
| Global of string option * 'a global_type
Instructions
type 'a instr =
| I32_const of Int32.t
| I64_const of Int64.t
| F32_const of Float32.t
| F64_const of Float64.t
| I_unop of nn * iunop
| F_unop of nn * funop
| I_binop of nn * ibinop
| F_binop of nn * fbinop
| I_testop of nn * itestop
| I_relop of nn * irelop
| F_relop of nn * frelop
| I_extend8_s of nn
| I_extend16_s of nn
| I64_extend32_s
| I32_wrap_i64
| I64_extend_i32 of sx
| I_trunc_f of nn * nn * sx
| I_trunc_sat_f of nn * nn * sx
| F32_demote_f64
| F64_promote_f32
| F_convert_i of nn * nn * sx
| I_reinterpret_f of nn * nn
| F_reinterpret_i of nn * nn
| Ref_null of 'a heap_type
| Ref_is_null
| Ref_i31
| Ref_func of 'a indice
| Ref_as_non_null
| Ref_cast of nullable * 'a heap_type
| Ref_test of nullable * 'a heap_type
| Ref_eq
| Drop
| Select of 'a val_type list option
| Local_get of 'a indice
| Local_set of 'a indice
| Local_tee of 'a indice
| Global_get of 'a indice
| Global_set of 'a indice
| Table_get of 'a indice
| Table_set of 'a indice
| Table_size of 'a indice
| Table_grow of 'a indice
| Table_fill of 'a indice
| Table_copy of 'a indice * 'a indice
| Table_init of 'a indice * 'a indice
| Elem_drop of 'a indice
| I_load of nn * memarg
| F_load of nn * memarg
| I_store of nn * memarg
| F_store of nn * memarg
| I_load8 of nn * sx * memarg
| I_load16 of nn * sx * memarg
| I64_load32 of sx * memarg
| I_store8 of nn * memarg
| I_store16 of nn * memarg
| I64_store32 of memarg
| Memory_size
| Memory_grow
| Memory_fill
| Memory_copy
| Memory_init of 'a indice
| Data_drop of 'a indice
| Nop
| Unreachable
| Block of string option * 'a block_type option * 'a expr
| Loop of string option * 'a block_type option * 'a expr
| If_else of string option * 'a block_type option * 'a expr * 'a expr
| Br of 'a indice
| Br_if of 'a indice
| Br_table of 'a indice array * 'a indice
| Br_on_cast of 'a indice * 'a ref_type * 'a ref_type
| Br_on_cast_fail of 'a indice * nullable * 'a heap_type
| Br_on_non_null of 'a indice
| Br_on_null of 'a indice
| Return
| Return_call of 'a indice
| Return_call_indirect of 'a indice * 'a block_type
| Return_call_ref of 'a block_type
| Call of 'a indice
| Call_indirect of 'a indice * 'a block_type
| Call_ref of 'a indice
| Array_get of 'a indice
| Array_get_u of 'a indice
| Array_len
| Array_new of 'a indice
| Array_new_data of 'a indice * 'a indice
| Array_new_default of 'a indice
| Array_new_elem of 'a indice * 'a indice
| Array_new_fixed of 'a indice * int
| Array_set of 'a indice
| I31_get_u
| I31_get_s
| Struct_get of 'a indice * 'a indice
| Struct_get_s of 'a indice * 'a indice
| Struct_new of 'a indice
| Struct_new_default of 'a indice
| Struct_set of 'a indice * 'a indice
| Extern_externalize
| Extern_internalize
and 'a expr = 'a instr list
val pp_instr : 'a instr Prelude.Fmt.t
val pp_expr : Stdlib.Format.formatter -> 'a expr -> Prelude.Unit.t
val pp_local : Stdlib.Format.formatter -> (string option * 'a val_type) -> unit
val pp_locals :
- Stdlib.Format.formatter ->
- (string option * 'a val_type) list ->
- unit
val pp_func : 'kind. Prelude.Fmt.formatter -> 'kind func -> unit
val pp_funcs : Stdlib.Format.formatter -> 'a func list -> unit
type 'a table = string option * 'a table_type
type 'a import_desc =
| Import_func of string option * 'a block_type
| Import_table of string option * 'a table_type
| Import_mem of string option * limits
| Import_global of string option * 'a global_type
val import_desc : Stdlib.Format.formatter -> 'a import_desc -> Prelude.Unit.t
type 'a import = {
modul : string;
The name of the module from which the import is done
*)name : string;
The name of the importee in its module of origin
*)desc : 'a import_desc;
If this import_desc first field is Some s, the importee is made available under name s, else it can only be used via its numerical index.
*)}
val pp_import : Stdlib.Format.formatter -> 'a import -> Prelude.Unit.t
val pp_export_desc : Stdlib.Format.formatter -> 'a export_desc -> unit
val pp_storage_type : Stdlib.Format.formatter -> 'a storage_type -> unit
val storage_type_eq : 'a storage_type -> 'b storage_type -> bool
type 'a field_type = mut * 'a storage_type
val pp_field_type : Stdlib.Format.formatter -> (mut * 'a storage_type) -> unit
val field_type_eq : (mut * 'a storage_type) -> (mut * 'b storage_type) -> bool
type 'a struct_field = string option * 'a field_type list
val pp_fields : Stdlib.Format.formatter -> (mut * 'a storage_type) list -> unit
val pp_struct_field :
- Stdlib.Format.formatter ->
- (string option * (mut * 'a storage_type) list) ->
- unit
val struct_field_eq :
- ('a * (mut * 'b storage_type) list) ->
- ('c * (mut * 'b storage_type) list) ->
- bool
type 'a struct_type = 'a struct_field list
val pp_struct_type :
- Stdlib.Format.formatter ->
- (string option * (mut * 'a storage_type) list) list ->
- unit
val struct_type_eq :
- ('a * (mut * 'b storage_type) list) list ->
- ('a * (mut * 'b storage_type) list) list ->
- bool
val pp_array_type : Stdlib.Format.formatter -> (mut * 'a storage_type) -> unit
type 'a str_type =
| Def_struct_t of 'a struct_type
| Def_array_t of 'a field_type
| Def_func_t of 'a func_type
val str_type : Stdlib.Format.formatter -> 'a str_type -> unit
type 'a type_def = string option * 'a sub_type
type 'a rec_type = 'a type_def list
val pp_start : Stdlib.Format.formatter -> 'a indice -> unit
val pp_const : Stdlib.Format.formatter -> 'a const -> unit
val pp_consts : Stdlib.Format.formatter -> 'a const list -> unit
V.Bool
V.F32
V.F64
V.I32
V.I64
V.Ref
val get_func : ref_value -> Func_intf.t Value_intf.get_ref
val get_externref : ref_value -> 'a Prelude.Type.Id.t -> 'a Value_intf.get_ref
Owi.V
include Value_intf.T
- with type vbool = Prelude.Bool.t
- and type int32 = Int32.t
- and type int64 = Int64.t
- and type float32 = Float32.t
- and type float64 = Float64.t
- and type ref_value = Concrete_value.ref_value
- and type t = Concrete_value.t
type int32 = Int32.t
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
type int64 = Int64.t
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
type float32 = Float32.t
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
type float64 = Float64.t
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
type ref_value = Concrete_value.ref_value
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
Owi.Value_intf
Value_intf.Fop
Value_intf.Iop
val zero : num
T.Bool
T.F32
T.F64
T.I32
T.I64
T.Ref
val get_func : ref_value -> Func_intf.t get_ref
Value_intf.T
val pp_int32 : Prelude.Fmt.formatter -> int32 -> unit
val pp_int64 : Prelude.Fmt.formatter -> int64 -> unit
val pp_float32 : Prelude.Fmt.formatter -> float32 -> unit
val pp_float64 : Prelude.Fmt.formatter -> float64 -> unit
val pp_ref_value : Prelude.Fmt.formatter -> ref_value -> unit
val pp : Prelude.Fmt.formatter -> t -> unit
val ref_null : Types.binary Types.heap_type -> t
val ref_func : Func_intf.t -> t
val ref_externref : 'a Prelude.Type.Id.t -> 'a -> t
module Ref : sig ... end
module Bool : sig ... end
module F32 : sig ... end
module F64 : sig ... end
module I32 : sig ... end
module I64 : sig ... end
Owi.Wasm_ffi_intf
Wasm_ffi_intf.S
val symbolic_extern_module : extern_func Link.extern_module
val summaries_extern_module : extern_func Link.extern_module
S0.Value
Wasm_ffi_intf.S0
module Value : sig ... end
val symbol_i8 : unit -> Value.int32 t
val symbol_char : unit -> Value.int32 t
val symbol_i32 : unit -> Value.int32 t
val symbol_i64 : unit -> Value.int64 t
val symbol_f32 : unit -> Value.float32 t
val symbol_f64 : unit -> Value.float64 t
val assume_i32 : Value.int32 -> unit t
val assume_positive_i32 : Value.int32 -> unit t
val assert_i32 : Value.int32 -> unit t
val abort : unit -> unit t
val alloc : memory -> Value.int32 -> Value.int32 -> Value.int32 t
val free : memory -> Value.int32 -> unit t
val exit : Value.int32 -> unit t
Owi.Wq
Synchronized FIFO queues
val make : unit -> 'a t
Create a new queue
val push : 'a -> 'a t -> unit
Add a new element to the queue
val pop : 'a t -> bool -> 'a option
Get an element from the queue. The boolean shall be true to atomically start a new pledge (cf make_pledge) while popping.
val make_pledge : 'a t -> unit
Make a new pledge, ie indicate that new elements may be pushed to the queue and that calls to pop should block waitting for them.
val end_pledge : 'a t -> unit
End one pledge.
val fail : 'a t -> unit
Mark the queue as failed: all threads trying to pop from it will get no element.
val read_as_seq : 'a t -> finalizer:(unit -> unit) -> 'a Prelude.Seq.t
Pop all elements from the queue in a lazy Seq.t,
val work_while : ('a -> ('a -> unit) -> unit) -> 'a t -> unit
Owi.Wutf8
Utility functions to work with utf8.
val check_utf8 : string -> unit Result.t
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
@@ -476,7 +506,7 @@ 100.00%
{ modul = import.modul; name = import.name; assigned_name; desc }
let empty_module id =
- { id
+ { id
; typ = []
; function_type = []
; type_checks = []
@@ -500,7 +530,7 @@ 100.00%
}
let init_curr () =
- { global = ref 0
+ { global = ref 0
; table = ref 0
; mem = ref 0
; func = ref 0
@@ -508,14 +538,14 @@ 100.00%
; data = ref 0
}
-let declare_func_type type_f (fields : t) =
- match type_f with
- | Bt_ind _ -> fields
- | Bt_raw (id, typ) ->
+let declare_func_type (fields : t) type_f =
+ match type_f with
+ | Bt_ind _ -> fields
+ | Bt_raw (id, typ) ->
let type_checks =
match id with
- | None -> fields.type_checks
- | Some id -> (id, typ) :: fields.type_checks
+ | None -> fields.type_checks
+ | Some id -> (id, typ) :: fields.type_checks
in
{ fields with function_type = typ :: fields.function_type; type_checks }
@@ -534,16 +564,31 @@ 100.00%
incr curr.mem;
{ fields with mem = Indexed.return index value :: fields.mem }
+let rec extract_block_types expr =
+ let aux instr =
+ match instr with
+ | Block (_str_opt, bt, expr1) | Loop (_str_opt, bt, expr1) ->
+ Option.to_list bt @ extract_block_types expr1
+ | If_else (_str_opt, bt, expr1, expr2) ->
+ Option.to_list bt @ extract_block_types expr1 @ extract_block_types expr2
+ | Return_call_indirect (_, bt) | Return_call_ref bt | Call_indirect (_, bt)
+ ->
+ [ bt ]
+ | _ -> []
+ in
+ List.concat_map aux expr
+
let add_func value (fields : t) (curr : curr) =
- let func_type =
+ let fields =
match value with
- | Runtime.Local func -> func.type_f
- | Imported func -> func.desc
+ | Runtime.Local func ->
+ let fields = declare_func_type fields func.type_f in
+ List.fold_left declare_func_type fields (extract_block_types func.body)
+ | Imported func -> declare_func_type fields func.desc
in
- let fields = declare_func_type func_type fields in
- let index = !(curr.func) in
+ let index = !(curr.func) in
incr curr.func;
- { fields with func = Indexed.return index value :: fields.func }
+ { fields with func = Indexed.return index value :: fields.func }
let add_elem value (fields : t) (curr : curr) =
let index = !(curr.elem) in
@@ -556,7 +601,7 @@ 100.00%
{ fields with data = Indexed.return index value :: fields.data }
let add_field curr (fields : t) = function
- | Text.MType typ ->
+ | Text.MType typ ->
let typ = typ @ fields.typ in
Ok { fields with typ }
| MGlobal global -> ok @@ add_global (Local global) fields curr
@@ -596,7 +641,7 @@ 100.00%
{ fields.exports with mem = { name; id } :: fields.exports.mem }
in
Ok { fields with exports }
- | MFunc func -> ok @@ add_func (Runtime.Local func) fields curr
+ | MFunc func -> ok @@ add_func (Runtime.Local func) fields curr
| MImport ({ desc = Import_func (a, type_f); _ } as import) ->
let imported : text block_type Imported.t = imp import (a, type_f) in
ok @@ add_func (Imported imported) fields curr
@@ -625,11 +670,11 @@ 100.00%
in
let data : Text.data = { id = data.id; init = data.init; mode } in
ok @@ add_data data fields curr
- | MStart start -> Ok { fields with start = Some start }
+ | MStart start -> Ok { fields with start = Some start }
let of_symbolic { Text.fields; id; _ } =
- Log.debug0 "grouping ...@\n";
- list_fold_left (add_field (init_curr ())) (empty_module id) fields
+ Log.debug0 "grouping ...@\n";
+ list_fold_left (add_field (init_curr ())) (empty_module id) fields
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
@@ -919,37 +877,57 @@ 88.62%
module StrType = struct
type t = binary str_type
- let compare (x : t) (y : t) = Types.compare_str_type x y
+ let compare (x : t) (y : t) = Types.compare_str_type x y
end
module TypeMap = Map.Make (StrType)
let typemap (types : binary str_type Named.t) =
- Named.fold
- (fun idx typ acc -> TypeMap.add typ (Raw idx) acc)
+ Named.fold
+ (fun idx typ acc -> TypeMap.add typ (Raw idx) acc)
types TypeMap.empty
-let find (named : 'a Named.t) : _ -> binary indice = function
- | Raw _i as indice -> indice
- | Text name -> (
+let find (named : 'a Named.t) : _ -> binary indice = function
+ | Raw _i as indice -> indice
+ | Text name -> (
match String_map.find_opt name named.named with
| None -> assert false
- | Some i -> Raw i )
+ | Some i -> Raw i )
let get error (named : 'a Named.t) indice : 'a Indexed.t Result.t =
- let (Raw i) = find named indice in
+ let (Raw i) = find named indice in
(* TODO change Named.t structure to make that sensible *)
- match List.nth_opt named.values i with None -> Error error | Some v -> Ok v
+ match List.nth_opt named.values i with None -> Error error | Some v -> Ok v
let find_global (modul : Assigned.t) id : binary indice = find modul.global id
let find_memory (modul : Assigned.t) id : binary indice = find modul.mem id
-let rewrite_expr (modul : Assigned.t) (locals : binary param list)
- (iexpr : text expr) : binary expr Result.t =
+let rewrite_block_type (typemap : binary indice TypeMap.t) (modul : Assigned.t)
+ (block_type : text block_type) : binary block_type Result.t =
+ match block_type with
+ | Bt_ind id -> begin
+ let+ v = get (`Unknown_type id) modul.typ id in
+ match Indexed.get v with
+ | Def_func_t t' ->
+ let idx = Indexed.get_index v in
+ Bt_raw (Some (Raw idx), t')
+ | _ -> assert false
+ end
+ | Bt_raw (_, func_type) ->
+ let+ t = Binary_types.convert_func_type None func_type in
+ let idx =
+ match TypeMap.find_opt (Def_func_t t) typemap with
+ | None -> assert false
+ | Some idx -> idx
+ in
+ Bt_raw (Some idx, t)
+
+let rewrite_expr (typemap : binary indice TypeMap.t) (modul : Assigned.t)
+ (locals : binary param list) (iexpr : text expr) : binary expr Result.t =
(* block_ids handling *)
- let block_id_to_raw (loop_count, block_ids) id =
- let* id =
+ let block_id_to_raw (loop_count, block_ids) id =
+ let* id =
match id with
| Text id -> begin
match
@@ -960,50 +938,27 @@ 88.62%
| None -> Error (`Unknown_label (Text id))
| Some id -> Ok id
end
- | Raw id -> Ok id
+ | Raw id -> Ok id
in
(* this is > and not >= because you can `br 0` without any block to target the function *)
- if id > List.length block_ids + loop_count then
+ if id > List.length block_ids + loop_count then
Error (`Unknown_label (Raw id))
- else Ok (Raw id)
+ else Ok (Raw id)
in
- let bt_some_to_raw : text block_type -> binary block_type Result.t = function
- | Bt_ind ind -> begin
- let+ v = get (`Unknown_type ind) modul.typ ind in
- match Indexed.get v with
- | Def_func_t t' ->
- let idx = Indexed.get_index v in
- Bt_raw (Some (Raw idx), t')
- | _ -> assert false
- end
- | Bt_raw (type_use, t) -> (
- let* t = Binary_types.convert_func_type None t in
- match type_use with
- | None -> Ok (Bt_raw (None, t))
- | Some ind ->
- (* we check that the explicit type match the type_use, we have to remove parameters names to do so *)
- let* t' =
- let+ v = get (`Unknown_type ind) modul.typ ind in
- match Indexed.get v with Def_func_t t' -> t' | _ -> assert false
- in
- let ok = Types.func_type_eq t t' in
- if not ok then Error `Inline_function_type else Ok (Bt_raw (None, t)) )
- in
-
- let bt_to_raw : text block_type option -> binary block_type option Result.t =
- function
+ (* block_types handling *)
+ let block_ty_opt_rewrite = function
+ | Some bt ->
+ let+ bt = rewrite_block_type typemap modul bt in
+ Some bt
| None -> Ok None
- | Some bt ->
- let+ raw = bt_some_to_raw bt in
- Some raw
in
let* locals, _after_last_assigned_local =
- list_fold_left
+ list_fold_left
(fun (locals, next_free_int) ((name, _type) : binary param) ->
- match name with
- | None -> Ok (locals, next_free_int + 1)
+ match name with
+ | None -> Ok (locals, next_free_int + 1)
| Some name ->
if String_map.mem name locals then Error (`Duplicate_local name)
else Ok (String_map.add name next_free_int locals, next_free_int + 1)
@@ -1011,75 +966,75 @@ 88.62%
(String_map.empty, 0) locals
in
- let find_local = function
- | Raw _i as id -> id
+ let find_local = function
+ | Raw _i as id -> id
| Text name -> (
match String_map.find_opt name locals with
| None -> assert false
| Some id -> Raw id )
in
- let find_table id = find modul.table id in
- let find_func id = find modul.func id in
+ let find_table id = find modul.table id in
+ let find_func id = find modul.func id in
let find_data id = find modul.data id in
let find_elem id = find modul.elem id in
let find_type id = find modul.typ id in
let rec body (loop_count, block_ids) : text instr -> binary instr Result.t =
- function
+ function
| Br_table (ids, id) ->
let block_id_to_raw = block_id_to_raw (loop_count, block_ids) in
let* ids = array_map block_id_to_raw ids in
let+ id = block_id_to_raw id in
Br_table (ids, id)
- | Br_if id ->
- let+ id = block_id_to_raw (loop_count, block_ids) id in
- Br_if id
+ | Br_if id ->
+ let+ id = block_id_to_raw (loop_count, block_ids) id in
+ Br_if id
| Br id ->
let+ id = block_id_to_raw (loop_count, block_ids) id in
Br id
- | Call id ->
+ | Call id ->
let id = find_func id in
- Ok (Call id)
+ Ok (Call id)
| Return_call id ->
let id = find_func id in
Ok (Return_call id)
| Local_set id ->
let id = find_local id in
Ok (Local_set id)
- | Local_get id ->
+ | Local_get id ->
let id = find_local id in
- Ok (Local_get id)
- | Local_tee id ->
+ Ok (Local_get id)
+ | Local_tee id ->
let id = find_local id in
- Ok (Local_tee id)
- | If_else (id, bt, e1, e2) ->
- let* bt = bt_to_raw bt in
+ Ok (Local_tee id)
+ | If_else (id, bt, e1, e2) ->
+ let* bt = block_ty_opt_rewrite bt in
let block_ids = id :: block_ids in
let* e1 = expr e1 (loop_count, block_ids) in
let+ e2 = expr e2 (loop_count, block_ids) in
If_else (id, bt, e1, e2)
- | Loop (id, bt, e) ->
- let* bt = bt_to_raw bt in
- let+ e = expr e (loop_count + 1, id :: block_ids) in
- Loop (id, bt, e)
- | Block (id, bt, e) ->
- let* bt = bt_to_raw bt in
- let+ e = expr e (loop_count, id :: block_ids) in
- Block (id, bt, e)
- | Call_indirect (tbl_i, bt) ->
+ | Loop (id, bt, e) ->
+ let* bt = block_ty_opt_rewrite bt in
+ let+ e = expr e (loop_count + 1, id :: block_ids) in
+ Loop (id, bt, e)
+ | Block (id, bt, e) ->
+ let* bt = block_ty_opt_rewrite bt in
+ let+ e = expr e (loop_count, id :: block_ids) in
+ Block (id, bt, e)
+ | Call_indirect (tbl_i, bt) ->
let tbl_i = find_table tbl_i in
- let+ bt = bt_some_to_raw bt in
+ let+ bt = rewrite_block_type typemap modul bt in
Call_indirect (tbl_i, bt)
- | Return_call_indirect (tbl_i, bt) ->
+ | Return_call_indirect (tbl_i, bt) ->
let tbl_i = find_table tbl_i in
- let+ bt = bt_some_to_raw bt in
+ let+ bt = rewrite_block_type typemap modul bt in
Return_call_indirect (tbl_i, bt)
| Call_ref t ->
let t = find_type t in
Ok (Call_ref t)
| Return_call_ref bt ->
- let+ bt = bt_some_to_raw bt in
+ let+ bt = rewrite_block_type typemap modul bt in
Return_call_ref bt
| Global_set id ->
let idx = find_global modul id in
@@ -1160,12 +1115,12 @@ 88.62%
| Ref_test (null, ht) ->
let+ ht = Binary_types.convert_heap_type None ht in
Ref_test (null, ht)
- | ( I_unop _ | I_binop _ | I_testop _ | I_relop _ | F_unop _ | F_relop _
+ | ( I_unop _ | I_binop _ | I_testop _ | I_relop _ | F_unop _ | F_relop _
| I32_wrap_i64 | F_reinterpret_i _ | I_reinterpret_f _ | I64_extend_i32 _
| I64_extend32_s | F32_demote_f64 | I_extend8_s _ | I_extend16_s _
| F64_promote_f32 | F_convert_i _ | I_trunc_f _ | I_trunc_sat_f _
- | Ref_is_null | F_binop _ | F32_const _ | F64_const _ | I32_const _
- | I64_const _ | Unreachable | Drop | Nop | Return | Ref_i31 | I31_get_s
+ | Ref_is_null | F_binop _ | F32_const _ | F64_const _ | I32_const _
+ | I64_const _ | Unreachable | Drop | Nop | Return | Ref_i31 | I31_get_s
| I31_get_u | Array_len | Ref_as_non_null | Extern_externalize
| Extern_internalize | Ref_eq | I_load8 _ | I_store8 _ | I_load16 _
| I_store16 _ | I64_load32 _ | I64_store32 _ | I_load _ | F_load _
@@ -1177,40 +1132,20 @@ 88.62%
| Struct_new _ | Br_on_non_null _ | Br_on_null _ ) as _i ->
assert false
and expr (e : text expr) (loop_count, block_ids) : binary expr Result.t =
- list_map (fun i -> body (loop_count, block_ids) i) e
+ list_map (fun i -> body (loop_count, block_ids) i) e
in
expr iexpr (0, [])
-let rewrite_block_type (typemap : binary indice TypeMap.t) (modul : Assigned.t)
- (block_type : text block_type) : binary block_type Result.t =
- match block_type with
- | Bt_ind id -> begin
- let+ v = get (`Unknown_type id) modul.typ id in
- match Indexed.get v with
- | Def_func_t t' ->
- let idx = Indexed.get_index v in
- Bt_raw (Some (Raw idx), t')
- | _ -> assert false
- end
- | Bt_raw (_, func_type) ->
- let+ t = Binary_types.convert_func_type None func_type in
- let idx =
- match TypeMap.find_opt (Def_func_t t) typemap with
- | None -> assert false
- | Some idx -> idx
- in
- Bt_raw (Some idx, t)
-
-let rewrite_global (modul : Assigned.t) (global : Text.global) :
- Binary.global Result.t =
- let* init = rewrite_expr modul [] global.init in
+let rewrite_global (typemap : binary indice TypeMap.t) (modul : Assigned.t)
+ (global : Text.global) : Binary.global Result.t =
+ let* init = rewrite_expr typemap modul [] global.init in
let mut, val_type = global.typ in
let+ val_type = Binary_types.convert_val_type None val_type in
let typ = (mut, val_type) in
{ Binary.id = global.id; init; typ }
-let rewrite_elem (modul : Assigned.t) (elem : Text.elem) : Binary.elem Result.t
- =
+let rewrite_elem (typemap : binary indice TypeMap.t) (modul : Assigned.t)
+ (elem : Text.elem) : Binary.elem Result.t =
let* (mode : Binary.elem_mode) =
match elem.mode with
| Elem_declarative -> Ok Binary.Elem_declarative
@@ -1218,29 +1153,29 @@ 88.62%
| Elem_active (None, _expr) -> assert false
| Elem_active (Some id, expr) ->
let (Raw indice) = find modul.table id in
- let+ expr = rewrite_expr modul [] expr in
+ let+ expr = rewrite_expr typemap modul [] expr in
Binary.Elem_active (Some indice, expr)
in
- let* init = list_map (rewrite_expr modul []) elem.init in
+ let* init = list_map (rewrite_expr typemap modul []) elem.init in
let+ typ = Binary_types.convert_ref_type None elem.typ in
{ Binary.init; mode; id = elem.id; typ }
-let rewrite_data (modul : Assigned.t) (data : Text.data) : Binary.data Result.t
- =
+let rewrite_data (typemap : binary indice TypeMap.t) (modul : Assigned.t)
+ (data : Text.data) : Binary.data Result.t =
let+ mode =
match data.mode with
| Data_passive -> Ok Binary.Data_passive
| Data_active (None, _expr) -> assert false
| Data_active (Some indice, expr) ->
let (Raw indice) = find_memory modul indice in
- let+ expr = rewrite_expr modul [] expr in
+ let+ expr = rewrite_expr typemap modul [] expr in
Binary.Data_active (indice, expr)
in
{ Binary.mode; id = data.id; init = data.init }
let rewrite_export named (exports : Grouped.opt_export list) :
Binary.export list =
- List.map
+ List.map
(fun { Grouped.name; id } ->
let (Raw id) = find named id in
{ Binary.name; id } )
@@ -1248,20 +1183,20 @@ 88.62%
let rewrite_exports (modul : Assigned.t) (exports : Grouped.opt_exports) :
Binary.exports =
- let global = rewrite_export modul.global exports.global in
- let mem = rewrite_export modul.mem exports.mem in
- let table = rewrite_export modul.table exports.table in
- let func = rewrite_export modul.func exports.func in
- { Binary.global; mem; table; func }
+ let global = rewrite_export modul.global exports.global in
+ let mem = rewrite_export modul.mem exports.mem in
+ let table = rewrite_export modul.table exports.table in
+ let func = rewrite_export modul.func exports.func in
+ { Binary.global; mem; table; func }
let rewrite_func (typemap : binary indice TypeMap.t) (modul : Assigned.t)
({ id; type_f; locals; body; _ } : text func) : binary func Result.t =
- let* (Bt_raw (_, (params, _)) as type_f) =
- rewrite_block_type typemap modul type_f
+ let* (Bt_raw (_, (params, _)) as type_f) =
+ rewrite_block_type typemap modul type_f
in
- let* locals = list_map (Binary_types.convert_param None) locals in
- let+ body = rewrite_expr modul (params @ locals) body in
- { body; type_f; id; locals }
+ let* locals = list_map (Binary_types.convert_param None) locals in
+ let+ body = rewrite_expr typemap modul (params @ locals) body in
+ { body; type_f; id; locals }
let rewrite_import (f : 'a -> 'b Result.t) (import : 'a Imported.t) :
'b Imported.t Result.t =
@@ -1269,69 +1204,71 @@ 88.62%
{ import with desc }
let rewrite_runtime f g r =
- match r with
- | Runtime.Local v ->
- let+ v = f v in
- Runtime.Local v
+ match r with
+ | Runtime.Local v ->
+ let+ v = f v in
+ Runtime.Local v
| Imported i ->
let+ i = g i in
Runtime.Imported i
let rewrite_named f named =
- let+ values =
- list_map
+ let+ values =
+ list_map
(fun ind ->
- let index = Indexed.get_index ind in
- let value = Indexed.get ind in
- let+ value = f value in
- Indexed.return index value )
+ let index = Indexed.get_index ind in
+ let value = Indexed.get ind in
+ let+ value = f value in
+ Indexed.return index value )
named.Named.values
in
- { named with Named.values }
+ { named with Named.values }
let rewrite_types (_modul : Assigned.t) (t : binary str_type) :
binary rec_type Result.t =
(* TODO: the input `t` should actually be a `binary rec_type` *)
- let t = [ (None, (Final, [], t)) ] in
+ let t = [ (None, (Final, [], t)) ] in
Ok t
let modul (modul : Assigned.t) : Binary.modul Result.t =
- Log.debug0 "rewriting ...@\n";
- let typemap = typemap modul.typ in
- let* global =
+ Log.debug0 "rewriting ...@\n";
+ let typemap = typemap modul.typ in
+ let* global =
let+ { Named.named; values } =
- rewrite_named (rewrite_runtime (rewrite_global modul) ok) modul.global
+ rewrite_named
+ (rewrite_runtime (rewrite_global typemap modul) ok)
+ modul.global
in
- let values = List.rev values in
- { Named.named; values }
+ let values = List.rev values in
+ { Named.named; values }
in
- let* elem = rewrite_named (rewrite_elem modul) modul.elem in
- let* data = rewrite_named (rewrite_data modul) modul.data in
- let exports = rewrite_exports modul modul.exports in
- let* func =
- let import = rewrite_import (rewrite_block_type typemap modul) in
- let runtime = rewrite_runtime (rewrite_func typemap modul) import in
- rewrite_named runtime modul.func
+ let* elem = rewrite_named (rewrite_elem typemap modul) modul.elem in
+ let* data = rewrite_named (rewrite_data typemap modul) modul.data in
+ let exports = rewrite_exports modul modul.exports in
+ let* func =
+ let import = rewrite_import (rewrite_block_type typemap modul) in
+ let runtime = rewrite_runtime (rewrite_func typemap modul) import in
+ rewrite_named runtime modul.func
in
- let+ types = rewrite_named (rewrite_types modul) modul.typ in
- let start =
+ let+ types = rewrite_named (rewrite_types modul) modul.typ in
+ let start =
match modul.start with
| None -> None
- | Some id ->
+ | Some id ->
let (Raw id) = find func id in
- Some id
+ Some id
in
let id = modul.id in
let mem = Named.to_array modul.mem in
- let table = Named.to_array modul.table in
- let types = Named.to_array types in
- let global = Named.to_array global in
- let elem = Named.to_array elem in
- let data = Named.to_array data in
- let func = Named.to_array func in
+ let table = Named.to_array modul.table in
+ let types = Named.to_array types in
+ let global = Named.to_array global in
+ let elem = Named.to_array elem in
+ let data = Named.to_array data in
+ let func = Named.to_array func in
- let modul : Binary.modul =
+ let modul : Binary.modul =
{ id; mem; table; types; global; elem; data; exports; func; start }
in
modul
diff --git a/coverage/src/utils/log.ml.html b/coverage/src/utils/log.ml.html
index dfab4c442..146a90246 100644
--- a/coverage/src/utils/log.ml.html
+++ b/coverage/src/utils/log.ml.html
@@ -86,18 +86,18 @@ 83.33%
let profiling_on = ref false
let debug0 t : unit =
- if !debug_on then begin
+ if !debug_on then begin
Fmt.epr t;
Fmt.flush Fmt.stderr ()
end
-let debug1 t a : unit = if !debug_on then Fmt.epr t a
+let debug1 t a : unit = if !debug_on then Fmt.epr t a
-let debug2 t a b : unit = if !debug_on then Fmt.epr t a b
+let debug2 t a b : unit = if !debug_on then Fmt.epr t a b
let debug5 t a b c d e : unit = if !debug_on then Fmt.epr t a b c d e
-let profile3 t a b c : unit = if !profiling_on then Fmt.epr t a b c
+let profile3 t a b c : unit = if !profiling_on then Fmt.epr t a b c
(* TODO: remove this *)
let err f = Fmt.failwith f
diff --git a/coverage/src/utils/syntax.ml.html b/coverage/src/utils/syntax.ml.html
index 1faf157be..89b0b868e 100644
--- a/coverage/src/utils/syntax.ml.html
+++ b/coverage/src/utils/syntax.ml.html
@@ -191,56 +191,56 @@ 100.00%
open Prelude.Result
-let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e
+let ( let* ) o f = match o with Ok v -> f v | Error _ as e -> e
-let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e
+let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e
-let ok v = Ok v
+let ok v = Ok v
let list_iter f l =
- let err = ref None in
+ let err = ref None in
try
List.iter
(fun v ->
- match f v with
- | Error _e as e ->
+ match f v with
+ | Error _e as e ->
err := Some e;
raise Exit
- | Ok () -> () )
+ | Ok () -> () )
l;
- Ok ()
- with Exit -> Option.get !err
+ Ok ()
+ with Exit -> Option.get !err
let list_map f l =
- let err = ref None in
+ let err = ref None in
try
- ok
- @@ List.map
+ ok
+ @@ List.map
(fun v ->
- match f v with
- | Error _e as e ->
+ match f v with
+ | Error _e as e ->
err := Some e;
raise Exit
- | Ok v -> v )
+ | Ok v -> v )
l
- with Exit -> Option.get !err
+ with Exit -> Option.get !err
let list_fold_left f acc l =
- List.fold_left
+ List.fold_left
(fun acc v ->
- let* acc in
- f acc v )
+ let* acc in
+ f acc v )
(Ok acc) l
let array_iter f a =
- let err = ref None in
+ let err = ref None in
try
- for i = 0 to Array.length a - 1 do
- match f (Array.unsafe_get a i) with
+ for i = 0 to Array.length a - 1 do
+ match f (Array.unsafe_get a i) with
| Error _e as e ->
err := Some e;
raise Exit
- | Ok () -> ()
+ | Ok () -> ()
done;
Ok ()
with Exit -> Option.get !err
@@ -259,10 +259,10 @@ 100.00%
with Exit -> Option.get !err
let array_fold_left f acc l =
- Array.fold_left
+ Array.fold_left
(fun acc v ->
- let* acc in
- f acc v )
+ let* acc in
+ f acc v )
(Ok acc) l