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
198
199
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
module Expr = Smtml.Expr
module Choice = Symbolic_choice_with_memory
module Memory = Symbolic.Memory
(* The constraint is used here to make sure we don't forget to define one of the expected FFI functions, this whole file is further constrained such that if one function of M is unused in the FFI module below, an error will be displayed *)
module M : sig
include
Wasm_ffi_intf.S0
with type 'a t = 'a Choice.t
and type memory = Memory.t
and module Value = Symbolic_value
val symbol_i32_constant : Value.int32 -> Value.int32 t
end = struct
type 'a t = 'a Choice.t
type memory = Memory.t
module Value = Symbolic_value
let covered_labels = Hashtbl.create 16
let cov_lock = Mutex.create ()
let add_pc_wrapper e = Choice.add_pc e
let assume (i : Value.int32) : unit Choice.t =
add_pc_wrapper @@ Value.I32.to_bool i
let assert' (i : Value.int32) : unit Choice.t =
Choice.assertion @@ Value.I32.to_bool i
let symbol_invisible_bool () =
Choice.with_new_invisible_symbol (Ty_bitv 1) (fun sym ->
Expr.cvtop (Ty_bitv 32) (Zero_extend 31) (Expr.symbol sym) )
let symbol_bool () =
Choice.with_new_symbol (Ty_bitv 1) (fun sym ->
Expr.cvtop (Ty_bitv 32) (Zero_extend 31) (Expr.symbol sym) )
let symbol_i8 () =
Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
Expr.cvtop (Ty_bitv 32) (Zero_extend 24) (Expr.symbol sym) )
let symbol_char = symbol_i8
let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol
let symbol_i32_constant v =
let open Choice in
let* s = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol in
let eq = Value.I32.eq v s in
let+ () = Choice.add_pc eq in
s
let symbol_i64 () = Choice.with_new_symbol (Ty_bitv 64) Expr.symbol
let symbol_f32 () = Choice.with_new_symbol (Ty_fp 32) Expr.symbol
let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol
let symbol_range (lo : Value.int32) (hi : Value.int32) =
let open Choice in
let* x = symbol_i32 () in
let* () = add_pc_wrapper (Value.I32.le lo x) in
let+ () = add_pc_wrapper (Value.I32.gt hi x) in
x
let abort () : unit Choice.t = Choice.stop
let alloc m (base : Value.int32) (size : Value.int32) : Value.int32 Choice.t =
Choice.lift_mem @@ Memory.realloc m ~ptr:base ~size
let free m (ptr : Value.int32) : Value.int32 Choice.t =
Choice.lift_mem @@ Memory.free m ptr
let exit (_p : Value.int32) : unit Choice.t = abort ()
let in_replay_mode () = Choice.return @@ Smtml.Expr.value (Smtml.Value.Int 0)
let print_char (c : Value.int32) =
let open Choice in
let* c = select_i32 c in
Logs.app (fun m -> m "%c@?" (char_of_int (Int32.to_int c)));
return ()
let rec make_str m accu i =
let open Choice in
let* p = Memory.load_8_u m (Expr.value (Num (I32 i))) in
match Smtml.Expr.view p with
| Val (Num (I32 c)) ->
if Int32.gt c 255l || Int32.lt c 0l then trap `Invalid_character_in_memory
else
let ch = char_of_int (Int32.to_int c) in
if Char.equal ch '\x00' then return (List.rev accu |> Array.of_list)
else make_str m (ch :: accu) (Int32.add i (Int32.of_int 1))
| _ -> assert false
let cov_label_is_covered id =
let open Choice in
let* id = select_i32 id in
return @@ Value.const_i32
@@ Mutex.protect cov_lock (fun () ->
if Hashtbl.mem covered_labels id then 1l else 0l )
let cov_label_set m id ptr =
let open Choice in
let id = Smtml.Expr.simplify id in
let ptr = Smtml.Expr.simplify ptr in
match (Smtml.Expr.view id, Smtml.Expr.view ptr) with
| Val (Num (I32 id)), Val (Num (I32 ptr)) ->
Mutex.protect cov_lock (fun () ->
if Hashtbl.mem covered_labels id then abort ()
else
let* chars = make_str m [] ptr in
let str = String.init (Array.length chars) (Array.get chars) in
Hashtbl.add covered_labels id str;
let* () = add_label (Int32.to_int id, str) in
return () )
| _ ->
Logs.err (fun m ->
m "cov_label_set: invalid type id:%a ptr:%a" Smtml.Expr.pp id
Smtml.Expr.pp ptr );
assert false
end
type extern_func = Symbolic.Extern_func.extern_func
open M
let symbolic_extern_module =
let functions =
[ ( "i8_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i8) )
; ( "char_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_char)
)
; ( "i32_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_i32)
)
; ( "i32_symbol_constant"
, Symbolic.Extern_func.Extern_func
(Func (Arg (I32, Res), R1 I32), symbol_i32_constant) )
; ( "i64_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I64), symbol_i64)
)
; ( "f32_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 F32), symbol_f32)
)
; ( "f64_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
)
; ( "bool_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
)
; ( "invisible_bool_symbol"
, Symbolic.Extern_func.Extern_func
(Func (UArg Res, R1 I32), symbol_invisible_bool) )
; ( "range_symbol"
, Symbolic.Extern_func.Extern_func
(Func (Arg (I32, Arg (I32, Res)), R1 I32), symbol_range) )
; ( "assume"
, Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), assume) )
; ( "assert"
, Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), assert') )
; ( "in_replay_mode"
, Symbolic.Extern_func.Extern_func
(Func (UArg Res, R1 I32), in_replay_mode) )
; ( "print_char"
, Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), print_char)
)
; ( "cov_label_set"
, Symbolic.Extern_func.Extern_func
(Func (Mem (Arg (I32, Arg (I32, Res))), R0), cov_label_set) )
; ( "cov_label_is_covered"
, Symbolic.Extern_func.Extern_func
(Func (Arg (I32, Res), R1 I32), cov_label_is_covered) )
]
in
{ Link.functions }
let summaries_extern_module =
let functions =
[ ( "alloc"
, Symbolic.Extern_func.Extern_func
(Func (Mem (Arg (I32, Arg (I32, Res))), R1 I32), alloc) )
; ( "dealloc"
, Symbolic.Extern_func.Extern_func
(Func (Mem (Arg (I32, Res)), R1 I32), free) )
; ("abort", Symbolic.Extern_func.Extern_func (Func (UArg Res, R0), abort))
; ( "exit"
, Symbolic.Extern_func.Extern_func (Func (Arg (I32, Res), R0), exit) )
]
in
{ Link.functions }