1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
module Thread = Thread_with_memory
module Choice = Symbolic_choice_with_memory
module Value = Symbolic_value
module Extern_func =
Extern.Func.Make (Value) (Choice) (Symbolic_memory_concretizing)
module Global = Symbolic_global
module Table = Symbolic_table
type thread = Thread.t
let select (c : Value.bool) ~(if_true : Value.t) ~(if_false : Value.t) :
Value.t Choice.t =
match (if_true, if_false) with
| I32 if_true, I32 if_false ->
Choice.return (Value.I32 (Value.Bool.select_expr c ~if_true ~if_false))
| I64 if_true, I64 if_false ->
Choice.return (Value.I64 (Value.Bool.select_expr c ~if_true ~if_false))
| F32 if_true, F32 if_false ->
Choice.return (Value.F32 (Value.Bool.select_expr c ~if_true ~if_false))
| F64 if_true, F64 if_false ->
Choice.return (Value.F64 (Value.Bool.select_expr c ~if_true ~if_false))
| Ref _, Ref _ ->
let open Choice in
let+ b = select c ~prio_true:Prio.Default ~prio_false:Prio.Default in
if b then if_true else if_false
| _, _ -> assert false
let get_pc = Thread.pc
module Elem = struct
type t = Link_env.elem
let get (elem : t) i : Value.ref_value =
match elem.value.(i) with Funcref f -> Funcref f | _ -> assert false
let size (elem : t) = Array.length elem.value
end
module Memory = struct
include Symbolic_memory_concretizing
let load_8_s m a = Choice.lift_mem @@ load_8_s m a
let load_8_u m a = Choice.lift_mem @@ load_8_u m a
let load_16_s m a = Choice.lift_mem @@ load_16_s m a
let load_16_u m a = Choice.lift_mem @@ load_16_u m a
let load_32 m a = Choice.lift_mem @@ load_32 m a
let load_64 m a = Choice.lift_mem @@ load_64 m a
let store_8 m ~addr v = Choice.lift_mem @@ store_8 m ~addr v
let store_16 m ~addr v = Choice.lift_mem @@ store_16 m ~addr v
let store_32 m ~addr v = Choice.lift_mem @@ store_32 m ~addr v
let store_64 m ~addr v = Choice.lift_mem @@ store_64 m ~addr v
let fill m ~pos ~len c = Choice.lift_mem @@ fill m ~pos ~len c
let blit m ~src ~dst ~len = Choice.lift_mem @@ blit m ~src ~dst ~len
end
module Data = struct
type t = Link_env.data
let value data = data.Link_env.value
let size data = String.length data.Link_env.value
end
module Env = struct
type t = Extern_func.extern_func Link_env.t
type t' = Env_id.t
let get_memory env id =
match Link_env.get_memory env id with
| Error e -> Choice.trap e
| Ok orig_mem ->
let f (t : thread) =
let memories = Thread.memories t in
Memory.get_memory (Link_env.id env) orig_mem memories id
in
Choice.with_thread f
let get_func = Link_env.get_func
let get_extern_func = Link_env.get_extern_func
let get_table (env : t) i : Table.t Choice.t =
match Link_env.get_table env i with
| Error e -> Choice.trap e
| Ok orig_table ->
let f (t : thread) =
let tables = Thread.tables t in
Symbolic_table.get_table (Link_env.id env) orig_table tables i
in
Choice.with_thread f
let get_elem env i = Link_env.get_elem env i
let get_data env n =
match Link_env.get_data env n with
| Error e -> Choice.trap e
| Ok orig_data -> Choice.return orig_data
let get_global (env : t) i : Global.t Choice.t =
match Link_env.get_global env i with
| Error e -> Choice.trap e
| Ok orig_global ->
let f (t : thread) =
let globals = Thread.globals t in
Symbolic_global.get_global (Link_env.id env) orig_global globals i
in
Choice.with_thread f
let drop_elem _ =
(* TODO *)
()
let drop_data = Link_env.drop_data
end