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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2026 OCamlPro *)
(* Written by the Owi programmers *)
open Syntax
module I = Abstract_interpreter_control_flow
let unsafe = false
type host_externref = int
let ty : host_externref Type.Id.t = Type.Id.make ()
let do_action env = function
| Wast.Invoke (module_name, func_name, args) -> begin
Log.info (fun m ->
m "invoke %a %s %a..."
(Fmt.option ~none:Fmt.nop Fmt.string)
module_name func_name Wast.pp_consts args );
let* f = Env.Abstract.get_exported_func ~env ~module_name ~func_name in
let ctx = Env.Abstract.get_context ~env in
let stack = List.rev_map (Abstract_value.of_script_const ctx ~ty) args in
try I.exec_vfunc_from_outside ~ctx ~stack ~env f
with exn ->
Fmt.error_msg "%a@\n%a" Fmt.exn exn Fmt.exn_backtrace
(exn, Printexc.get_raw_backtrace ())
end
| Get (module_name, global_name) ->
Log.info (fun m -> m "get...");
let+ _global =
Env.Abstract.get_exported_global ~env ~module_name ~global_name
in
(* (env, [ global ]) *)
assert false
let run_one ~no_exhaustion:_ (state : Env.Abstract.t Result.t) cmd =
let* env = state in
match cmd with
| Wast.Text_module (false, m) ->
Abstract_trace.record_wast_cmd Block_start cmd;
let* modul, env =
Compile.Wasm.Text.until_abstract_link env ~unsafe ~name:None m
in
let _state = I.modul ~env ~modul in
Abstract_trace.record_wast_cmd Block_end cmd;
(* TODO: set context in env? Or isn't it necessary as it's supposed to be mutable? *)
Ok env
| Quoted_module (false, modul) ->
Log.info (fun m -> m "*** quoted module");
Abstract_trace.record_wast_cmd Block_start cmd;
let* modul = Parse.Text.Inline_module.from_string modul in
let* modul, env =
Compile.Wasm.Text.until_abstract_link env ~unsafe ~name:None modul
in
let _state = I.modul ~env ~modul in
Abstract_trace.record_wast_cmd Block_end cmd;
Ok env
| Binary_module (false, id, modul) ->
Log.info (fun m -> m "*** binary module");
Abstract_trace.record_wast_cmd Block_start cmd;
let* modul = Parse.Binary.Module.from_string modul in
let modul = { modul with id } in
let* modul, env =
Compile.Wasm.Binary.until_abstract_link env ~unsafe ~name:None modul
in
let _state = I.modul ~env ~modul in
Abstract_trace.record_wast_cmd Block_end cmd;
Ok env
| Assert (Assert_malformed_binary (modul, expected)) ->
Log.info (fun m -> m "*** assert_malformed_binary");
let got = Parse.Binary.Module.from_string modul in
let res = Script_error.check_result ~expected ~got in
Abstract_trace.record_wast_cmd Step cmd;
let+ () = res in
env
| Assert (Assert_malformed_quote (modul, expected)) ->
Log.info (fun m -> m "*** assert_malformed_quote");
let got = Parse.Text.Module.from_string modul in
let+ () =
match got with
| Error got -> Script_error.check_error ~expected ~got
| Ok modul ->
let got = Compile.Wasm.Text.until_binary ~unsafe modul in
Script_error.check_result ~expected ~got
in
env
| Assert (Assert_invalid_binary (modul, expected)) ->
Log.info (fun m -> m "*** assert_invalid_binary");
let got = Parse.Binary.Module.from_string modul in
let+ () =
match got with
| Error got -> Script_error.check_error ~expected ~got
| Ok modul ->
begin match Binary_validate.modul modul with
| Error got -> Script_error.check_error ~expected ~got
| Ok () ->
let got = Env.Abstract.link_binary_module ~env ~name:None ~modul in
Script_error.check_result ~expected ~got
end
in
env
| Assert (Assert_invalid (modul, expected)) ->
Log.info (fun m -> m "*** assert_invalid");
let got =
Compile.Wasm.Text.until_abstract_link env ~unsafe ~name:None modul
in
let+ () = Script_error.check_result ~expected ~got in
env
| Assert (Assert_invalid_quote (modul, expected)) ->
Log.info (fun m -> m "*** assert_invalid_quote");
let got = Parse.Text.Script.from_string modul in
let+ () =
match got with
| Error got -> Script_error.check_error ~expected ~got
| Ok [ Text_module (false, modul) ] ->
let got = Compile.Wasm.Text.until_validate ~unsafe modul in
Script_error.check_result ~expected ~got
| _ -> assert false
in
env
| Assert (Assert_malformed (modul, expected)) ->
Log.info (fun m -> m "*** assert_malformed");
let got =
Compile.Wasm.Text.until_abstract_link ~unsafe ~name:None env modul
in
let+ () = Script_error.check_result ~expected ~got in
assert false
| Assert (Assert_return (action, res)) ->
Log.info (fun m -> m "*** assert_return");
Abstract_trace.record_wast_cmd Block_start cmd;
let* state = do_action env action in
let stack = List.rev state.stack in
let res =
if
List.compare_lengths res stack <> 0
|| not
@@ List.for_all2
(Abstract_value.equal_script_result
(Env.Abstract.get_context ~env)
~ty )
res stack
then begin
let ctx = Env.Abstract.get_context ~env in
Abstract_trace.record_wast_test_res
(Fail
{ expected = Fmt.to_to_string Wast.pp_results res
; got = Fmt.to_to_string (Abstract_stack.pp ctx) stack
} );
Log.err (fun m ->
m "got: %a@;expected: %a"
(Fmt.Dump.list (Abstract_value.pp_with_ctx ctx))
stack Wast.pp_results res );
Error `Bad_result
end
else (
Abstract_trace.record_wast_test_res Ok;
Ok env )
in
Abstract_trace.record_wast_cmd Block_end cmd;
res
| Assert assertion ->
Log.warn (fun m -> m "%a is not handled" Wast.pp_assertion assertion);
Ok env
| Register (name, modid) ->
Abstract_trace.record_wast_cmd Step cmd;
let+ env = Env.Abstract.register_module ~env ~name ~modid in
env
| Instance _ ->
Abstract_trace.record_wast_cmd Step cmd;
Log.err (fun m -> m "(module instance) is not handled");
assert false
| Text_module (true, _) | Binary_module (true, _, _) | Quoted_module (true, _)
->
Abstract_trace.record_wast_cmd Step cmd;
Ok env
| Action action ->
Abstract_trace.record_wast_cmd Block_start cmd;
let* _state = do_action env action in
Abstract_trace.record_wast_cmd Block_end cmd;
Ok env
let run ~no_exhaustion script =
let context = Abstract_domain.root_context () in
let env = Env.Abstract.empty ~context in
let* state =
Env.Abstract.link_extern_module ~env ~name:"spectest_extern"
Spectest.abstract_extern_m
in
let script = Spectest.m :: Register ("spectest", Some "spectest") :: script in
List.fold_left
(fun acc cmd -> run_one ~no_exhaustion acc cmd)
(Ok state) script
let exec ~(no_exhaustion : bool) (script : Wast.script) =
let res = run ~no_exhaustion script in
match res with Error e -> Error e | Ok _ -> Ok ()