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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2026 OCamlPro *)
(* Written by the Owi programmers *)
type context = unit
type boolean = Smtml.Typed.Bool.t
type i32 = Smtml.Typed.Bitv32.t
type i64 = Smtml.Typed.Bitv64.t
type f32 = Smtml.Typed.Float32.t
type f64 = Smtml.Typed.Float64.t
type v128 = Smtml.Typed.Bitv128.t
module Boolean = Symbolic_boolean
module I32 = Symbolic_i32
module F32 = Symbolic_f32
module I64 = Symbolic_i64
module F64 = Symbolic_f64
module V128 = Symbolic_v128
module Ref = Symbolic_ref
type t =
| I32 of Smtml.Typed.Bitv32.t
| I64 of Smtml.Typed.Bitv64.t
| F32 of Smtml.Typed.Float32.t
| F64 of Smtml.Typed.Float64.t
| V128 of Smtml.Typed.Bitv128.t
| Ref of t Ref.t
let pp fmt = function
| I32 i -> Smtml.Typed.Bitv32.pp fmt i
| I64 i -> Smtml.Typed.Bitv64.pp fmt i
| F32 f -> Smtml.Typed.Float32.pp fmt f
| F64 f -> Smtml.Typed.Float64.pp fmt f
| V128 e -> Smtml.Typed.Bitv128.pp fmt e
| Ref r -> Ref.pp fmt r
let of_script_const ~ty = function
| Wast.Const_I32 v -> (I32 (Symbolic_i32.of_int32 v) : t)
| Const_I64 v -> I64 (Symbolic_i64.of_int64 v)
| Const_F32 v -> F32 (Symbolic_f32.of_float32 v)
| Const_F64 v -> F64 (Symbolic_f64.of_float (Float64.to_float v))
| Const_V128 v -> V128 (Symbolic_v128.of_concrete v)
| Const_extern i -> Ref (Symbolic_ref.extern ty i)
(* TODO: not ideal, the following are a duplication of Concrete_ref.null
applying on Text.heap_type instead of Binary.heap_type. *)
| Const_null (Some (Func_ht | NoFunc_ht | TypeUse _)) -> Ref (Func None)
| Const_null (Some (Extern_ht | NoExtern_ht)) -> Ref (Extern None)
| Const_null (Some (Any_ht | None_ht | Struct_ht | Array_ht)) -> Ref NullRef
| Const_null (Some (Eq_ht | I31_ht)) -> Ref NullI31
| Const_null (Some (Exn_ht | NoExn_ht)) -> Ref NullExn
| _ -> assert false
let of_concrete () : Concrete_value.t -> t = function
| I32 v -> I32 (Symbolic_i32.of_int32 v)
| I64 v -> I64 (Symbolic_i64.of_int64 v)
| F32 v -> F32 (Symbolic_f32.of_float32 v)
| F64 v -> F64 (Symbolic_f64.of_float (Concrete_f64.to_float v))
| V128 v -> V128 (Symbolic_v128.of_concrete v)
| _ -> assert false
let equal_script_result =
let compare_f32 (script_result : Wast.result_f32) v =
match script_result with
| Concrete f ->
begin match
F32.eq (F32.of_float32 f) v |> Smtml.Typed.view
(*TODO:
|| String.equal (F32.to_string f) (F32.to_string v)*)
with
| Val True -> true
| Val False -> false
| _ -> assert false
end
| Nan_canon -> true
(* TODO: F32.is_pos_nan v || F32.is_neg_nan v *)
| Nan_arith -> true
(* TODO:
let pos_nan = F32.to_bits F32.pos_nan in
I32.eq (I32.logand (F32.to_bits v) pos_nan) pos_nan *)
in
let compare_f64 (script_result : Wast.result_f64) v =
match script_result with
| Concrete f ->
begin match
F64.eq (F64.of_float (Concrete_f64.to_float f)) v |> Smtml.Typed.view
(* TODO:
|| String.equal (F64.to_string f) (F64.to_string v) *)
with
| Val True -> true
| Val False -> false
| _ -> assert false
end
| Nan_canon -> true (* TODO: F64.is_pos_nan v || F64.is_neg_nan v *)
| Nan_arith -> true
(* TODO:
let pos_nan = F64.to_bits F64.pos_nan in
I64.eq (I64.logand (F64.to_bits v) pos_nan) pos_nan *)
in
let compare_v128 (script_result : Wast.result_v128) (const : V128.t) =
match script_result with
| Concrete v ->
begin match V128.eq (V128.of_concrete v) const |> Smtml.Typed.view with
| Val True -> true
| Val False -> false
| _ -> assert false
end
| F32x4 (a, b, c, d) ->
let a', b', c', d' = V128.to_i32x4 const in
let a', b', c', d' =
( F32.reinterpret_i32 a'
, F32.reinterpret_i32 b'
, F32.reinterpret_i32 c'
, F32.reinterpret_i32 d' )
in
compare_f32 a a' && compare_f32 b b' && compare_f32 c c'
&& compare_f32 d d'
| F64x2 (a, b) ->
let a', b' = V128.to_i64x2 const in
let a', b' = (F64.reinterpret_i64 a', F64.reinterpret_i64 b') in
compare_f64 a a' && compare_f64 b b'
in
fun ~ty script_result v ->
match (script_result, v) with
| Wast.Result_I32 n, I32 n' ->
begin match I32.eq (Symbolic_i32.of_int32 n) n' |> Smtml.Typed.view with
| Val True -> true
| Val False -> false
| _ -> assert false
end
| Result_I64 n, I64 n' ->
begin match I64.eq (Symbolic_i64.of_int64 n) n' |> Smtml.Typed.view with
| Val True -> true
| Val False -> false
| _ -> assert false
end
| Result_F32 script_result, F32 v -> compare_f32 script_result v
| Result_F64 script_result, F64 v -> compare_f64 script_result v
| Result_V128 script_result, V128 v -> compare_v128 script_result v
| Result_null None, Ref (NullRef | NullExn | Func None | Extern None) ->
true
| Result_null (Some (NoFunc_ht | Func_ht)), Ref (Func None) -> true
| Result_null (Some (Extern_ht | NoExtern_ht)), Ref (Extern None) -> true
| Result_null (Some (Exn_ht | NoExn_ht)), Ref NullExn -> true
| Result_null (Some (Any_ht | None_ht)), Ref NullRef -> true
| Result_extern n, Ref (Extern (Some ref)) ->
begin match Ref.Extern.cast ref ty with
| None -> false
| Some n' -> n = n'
end
| Result_func_ref, Ref (Func _) ->
(* TODO: FIX! This is probably unsound! *)
true
| ( ( Result_I32 _ | Result_I64 _ | Result_F32 _ | Result_F64 _
| Result_V128 _ | Result_null _ | Result_host _ )
, _ ) ->
false
| _, _ -> assert false