formalsec / smtml / 452

Committed 26 Dec 2025 11:33AM UTC coverage: 44.778% (-0.3%) from 45.031%

Build # 452

Build Type

push

github

Committed by

filipeom

Commit Message

Add Eval.pp_error_kind function

Run Details

0 of 1 new or added line in 1 file covered. (0.0%)

70 existing lines in 1 file now uncovered.

879 of 1963 relevant lines covered (44.78%)

7.37 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

77.13

/src/smtml/eval.ml

1	(* SPDX-License-Identifier: MIT *)
2	(* Copyright (C) 2023-2024 formalsec *)
3	(* Written by the Smtml programmers *)
4
5	(* Adapted from: *)
6	(* - https://github.com/WebAssembly/spec/blob/main/interpreter/exec/ixx.ml, *)
7	(* - https://github.com/WebAssembly/spec/blob/main/interpreter/exec/fxx.ml, and *)
8	(* - https://github.com/WebAssembly/spec/blob/main/interpreter/exec *)
9
UNCOV 10	type op_type =	×
11	[ `Unop of Ty.Unop.t	12✔
12	\| `Binop of Ty.Binop.t
13	\| `Relop of Ty.Relop.t
14	\| `Triop of Ty.Triop.t
15	\| `Cvtop of Ty.Cvtop.t
16	\| `Naryop of Ty.Naryop.t
17	]
18	[@@deriving show]
19
UNCOV 20	type type_error_info =	×
UNCOV 21	{ index : int	×
22	; value : Value.t
23	; ty : Ty.t
24	; op : op_type
UNCOV 25	; msg : string	×
26	}
NEW 27	[@@deriving show]	×
28
UNCOV 29	type error_kind =	×
UNCOV 30	[ `Divide_by_zero	×
31	\| `Conversion_to_integer
32	\| `Integer_overflow
33	\| `Index_out_of_bounds
34	\| `Invalid_format_conversion
UNCOV 35	\| `Unsupported_operator of op_type * Ty.t	×
36	\| `Unsupported_theory of Ty.t
37	\| `Type_error of type_error_info
38	]
39	[@@deriving show]
40
41	exception Eval_error of error_kind
42
43	exception Value of Ty.t
44
45	(* Exception helpers *)
46
47	let eval_error kind = raise (Eval_error kind)	13✔
48
49	let type_error n v ty op msg =
50	eval_error (`Type_error { index = n; value = v; ty; op; msg })	9✔
51
52	let err_str n op ty_expected ty_actual =
53	Fmt.str "Argument %d of %a expected type %a but got %a instead." n pp_op_type	6✔
54	op Ty.pp ty_expected Ty.pp ty_actual
55
56	let[@inline] of_arg f n v op =
57	try f v	649✔
58	with Value expected_ty ->	6✔
59	let actual_ty = Value.type_of v in
60	let msg = err_str n op expected_ty actual_ty in	6✔
61	type_error n v expected_ty op msg	6✔
62
63	(* Coercion helpers *)
64
65	let of_int n op v =
66	of_arg (function Int x -> x \| _ -> raise_notrace (Value Ty_int)) n v op	1✔
67
68	let[@inline] to_int x = Value.Int x	48✔
69
70	let of_real n op v =
71	of_arg (function Real x -> x \| _ -> raise_notrace (Value Ty_real)) n v op	1✔
72
73	let[@inline] to_real x = Value.Real x	37✔
74
75	let of_bool n op v =
76	of_arg	51✔
77	(function
78	\| True -> true \| False -> false \| _ -> raise_notrace (Value Ty_bool) )	1✔
79	n v op
80
81	let[@inline] to_bool x = if x then Value.True else False	12✔
82
83	let of_str n op v =
84	of_arg (function Str x -> x \| _ -> raise_notrace (Value Ty_str)) n v op	1✔
85
86	let[@inline] to_str x = Value.Str x	16✔
87
88	let of_list n op v =
89	of_arg (function List x -> x \| _ -> raise_notrace (Value Ty_list)) n v op	×
90
91	let of_bitv n op v =
92	of_arg	154✔
93	(function Bitv x -> x \| _ -> raise_notrace (Value (Ty_bitv 0)))	×
94	n v op
95
96	let int32_of_bitv n op v = of_bitv n op v \|> Bitvector.to_int32	8✔
97
98	let int64_of_bitv n op v = of_bitv n op v \|> Bitvector.to_int64	12✔
99
100	let[@inline] to_bitv x = Value.Bitv x	75✔
101
102	let[@inline] bitv_of_int32 x = to_bitv (Bitvector.of_int32 x)	14✔
103
104	let[@inline] bitv_of_int64 x = to_bitv (Bitvector.of_int64 x)	11✔
105
106	let of_fp32 i op v : int32 =
107	of_arg	92✔
108	(function Num (F32 f) -> f \| _ -> raise_notrace (Value (Ty_fp 32)))	1✔
109	i v op
110
111	let[@inline] to_fp32 (x : int32) = Value.Num (F32 x)	35✔
112
113	let[@inline] fp32_of_float (x : float) = to_fp32 (Int32.bits_of_float x)	15✔
114
115	let of_fp64 i op v : int64 =
116	of_arg	87✔
117	(function Num (F64 f) -> f \| _ -> raise_notrace (Value (Ty_fp 32)))	1✔
118	i v op
119
120	let[@inline] to_fp64 (x : int64) = Value.Num (F64 x)	32✔
121
122	let[@inline] fp64_of_float (x : float) = to_fp64 (Int64.bits_of_float x)	15✔
123
124	(* Operator evaluation *)
125
126	module Int = struct
127	let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
128	let f =	6✔
129	match op with
130	\| Neg -> Int.neg	3✔
131	\| Not -> Int.lognot	1✔
132	\| Abs -> Int.abs	2✔
133	\| _ -> eval_error (`Unsupported_operator (`Unop op, Ty_int))	×
134	in
135	to_int (f (of_int 1 (`Unop op) v))	5✔
136
137	let exp_by_squaring x n =
138	let rec exp_by_squaring2 y x n =	2✔
139	if n < 0 then exp_by_squaring2 y (1 / x) ~-n	×
140	else if n = 0 then y	2✔
141	else if n mod 2 = 0 then exp_by_squaring2 y (x * x) (n / 2)	1✔
142	else begin	3✔
143	assert (n mod 2 = 1);	3✔
144	exp_by_squaring2 (x * y) (x * x) ((n - 1) / 2)
145	end
146	in
147	exp_by_squaring2 1 x n
148
149	let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
150	let f =	31✔
151	match op with
152	\| Add -> Int.add	4✔
153	\| Sub -> Int.sub	2✔
154	\| Mul -> Int.mul	2✔
155	\| Div -> Int.div	3✔
156	\| Rem -> Int.rem	2✔
157	\| Pow -> exp_by_squaring	2✔
158	\| Min -> Int.min	2✔
159	\| Max -> Int.max	2✔
160	\| And -> Int.logand	2✔
161	\| Or -> Int.logor	2✔
162	\| Xor -> Int.logxor	2✔
163	\| Shl -> Int.shift_left	2✔
164	\| ShrL -> Int.shift_right_logical	1✔
165	\| ShrA -> Int.shift_right	3✔
166	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_int))	×
167	in
168	to_int (f (of_int 1 (`Binop op) v1) (of_int 2 (`Binop op) v2))	30✔
169
170	let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
171	let f =	8✔
172	match op with
173	\| Lt -> ( < )	2✔
174	\| Le -> ( <= )	2✔
175	\| Gt -> ( > )	2✔
176	\| Ge -> ( >= )	2✔
177	\| Eq -> Int.equal	×
178	\| Ne -> fun a b -> not (Int.equal a b)	×
179	\| _ -> eval_error (`Unsupported_operator (`Relop op, Ty_int))	×
180	in
181	f (of_int 1 (`Relop op) v1) (of_int 2 (`Relop op) v2)	8✔
182
183	let of_bool : Value.t -> int = function
184	\| True -> 1	2✔
185	\| False -> 0	1✔
186	\| _ -> assert false
187	[@@inline]
188
189	let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
190	match op with	5✔
191	\| OfBool -> to_int (of_bool v)	3✔
192	\| Reinterpret_float -> Int (Int.of_float (of_real 1 (`Cvtop op) v))	2✔
193	\| _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_int))	×
194	end
195
196	module Real = struct
197	let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
198	let v = of_real 1 (`Unop op) v in	19✔
199	match op with	18✔
200	\| Neg -> to_real @@ Float.neg v	2✔
201	\| Abs -> to_real @@ Float.abs v	2✔
202	\| Sqrt -> to_real @@ Float.sqrt v	2✔
203	\| Nearest -> to_real @@ Float.round v	3✔
204	\| Ceil -> to_real @@ Float.ceil v	2✔
205	\| Floor -> to_real @@ Float.floor v	2✔
206	\| Trunc -> to_real @@ Float.trunc v	2✔
207	\| Is_nan -> if Float.is_nan v then Value.True else Value.False	1✔
208	\| _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))	×
209
210	let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
211	let f =	16✔
212	match op with
213	\| Add -> Float.add	2✔
214	\| Sub -> Float.sub	2✔
215	\| Mul -> Float.mul	2✔
216	\| Div -> Float.div	3✔
217	\| Rem -> Float.rem	2✔
218	\| Min -> Float.min	2✔
219	\| Max -> Float.max	2✔
220	\| Pow -> Float.pow	1✔
221	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real))	×
222	in
223	to_real (f (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))	16✔
224
225	let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
226	let f =	12✔
227	match op with
228	\| Lt -> Float.Infix.( < )	2✔
229	\| Le -> Float.Infix.( <= )	2✔
230	\| Gt -> Float.Infix.( > )	2✔
231	\| Ge -> Float.Infix.( >= )	2✔
232	\| Eq -> Float.Infix.( = )	2✔
233	\| Ne -> Float.Infix.( <> )	2✔
234	\| _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real))	×
235	in
236	f (of_real 1 (`Relop op) v1) (of_real 2 (`Relop op) v2)	12✔
237
238	let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
239	let op' = `Cvtop op in	8✔
240	match op with
241	\| ToString -> Str (Float.to_string (of_real 1 op' v))	2✔
242	\| OfString -> begin	3✔
243	match float_of_string_opt (of_str 1 op' v) with	3✔
244	\| None -> eval_error `Invalid_format_conversion	1✔
245	\| Some v -> to_real v	2✔
246	end
247	\| Reinterpret_int -> to_real (float_of_int (of_int 1 op' v))	2✔
248	\| Reinterpret_float -> to_int (Float.to_int (of_real 1 op' v))	1✔
249	\| _ -> eval_error (`Unsupported_operator (op', Ty_real))	×
250	end
251
252	module Bool = struct
253	let unop (op : Ty.Unop.t) v =
254	let b = of_bool 1 (`Unop op) v in	3✔
255	match op with	2✔
256	\| Not -> to_bool (not b)	2✔
257	\| _ -> eval_error (`Unsupported_operator (`Unop op, Ty_bool))	×
258
259	let xor b1 b2 =
260	match (b1, b2) with	4✔
261	\| true, true -> false	1✔
262	\| true, false -> true	1✔
263	\| false, true -> true	1✔
264	\| false, false -> false	1✔
265
266	let binop (op : Ty.Binop.t) v1 v2 =
267	let f =	13✔
268	match op with
269	\| And -> ( && )	5✔
270	\| Or -> ( \|\| )	4✔
271	\| Xor -> xor	4✔
272	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_bool))	×
273	in
274	to_bool (f (of_bool 1 (`Binop op) v1) (of_bool 2 (`Binop op) v2))	13✔
275
276	let triop (op : Ty.Triop.t) c v1 v2 =
277	match op with	2✔
278	\| Ite -> ( match of_bool 1 (`Triop op) c with true -> v1 \| false -> v2 )	1✔
279	\| _ -> eval_error (`Unsupported_operator (`Triop op, Ty_bool))	×
280
281	let relop (op : Ty.Relop.t) v1 v2 =
282	match op with	9✔
283	\| Eq -> Value.equal v1 v2	4✔
284	\| Ne -> not (Value.equal v1 v2)	5✔
285	\| _ -> eval_error (`Unsupported_operator (`Relop op, Ty_bool))	×
286
287	let naryop (op : Ty.Naryop.t) vs =
288	let b =	6✔
289	match op with
290	\| Logand ->	3✔
291	List.fold_left ( && ) true	3✔
292	(List.mapi (fun i -> of_bool i (`Naryop op)) vs)	3✔
293	\| Logor ->	3✔
294	List.fold_left ( \|\| ) false	3✔
295	(List.mapi (fun i -> of_bool i (`Naryop op)) vs)	3✔
296	\| _ -> eval_error (`Unsupported_operator (`Naryop op, Ty_bool))	×
297	in
298	to_bool b
299	end
300
301	module Str = struct
302	let replace s t t' =
303	let len_s = String.length s in	2✔
304	let len_t = String.length t in	2✔
305	let rec loop i =	2✔
306	if i >= len_s then s	×
307	else if i + len_t > len_s then s	×
308	else if String.equal (String.sub s i len_t) t then	4✔
309	let s' = Fmt.str "%s%s" (String.sub s 0 i) t' in	2✔
310	let s'' = String.sub s (i + len_t) (len_s - i - len_t) in	2✔
311	Fmt.str "%s%s" s' s''	2✔
312	else loop (i + 1)	2✔
313	in
314	loop 0
315
316	let indexof s sub start =
317	let len_s = String.length s in	4✔
318	let len_sub = String.length sub in	4✔
319	let max_i = len_s - 1 in	4✔
320	let rec loop i =
321	if i > max_i then ~-1	×
322	else if i + len_sub > len_s then ~-1	×
323	else if String.equal sub (String.sub s i len_sub) then i	4✔
324	else loop (i + 1)	4✔
325	in
326	if start <= 0 then loop 0 else loop start	×
327
328	let contains s sub = if indexof s sub 0 < 0 then false else true	×
329
330	let unop (op : Ty.Unop.t) v =
331	let str = of_str 1 (`Unop op) v in	5✔
332	match op with	4✔
333	\| Length -> to_int (String.length str)	2✔
334	\| Trim -> to_str (String.trim str)	2✔
335	\| _ -> eval_error (`Unsupported_operator (`Unop op, Ty_str))	×
336
337	let binop (op : Ty.Binop.t) v1 v2 =
338	let op' = `Binop op in	9✔
339	let str = of_str 1 op' v1 in
340	match op with	9✔
341	\| At -> begin	3✔
342	let i = of_int 2 op' v2 in
343	try to_str (Fmt.str "%c" (String.get str i))	2✔
344	with Invalid_argument _ -> eval_error `Index_out_of_bounds	1✔
345	end
346	\| String_prefix ->	2✔
347	to_bool (String.starts_with ~prefix:str (of_str 2 op' v2))	2✔
348	\| String_suffix -> to_bool (String.ends_with ~suffix:str (of_str 2 op' v2))	2✔
349	\| String_contains -> to_bool (contains str (of_str 2 op' v2))	2✔
350	\| _ -> eval_error (`Unsupported_operator (op', Ty_str))	×
351
352	let triop (op : Ty.Triop.t) v1 v2 v3 =
353	let op' = `Triop op in	6✔
354	let str = of_str 1 op' v1 in
355	match op with	6✔
356	\| String_extract -> begin	2✔
357	let i = of_int 2 op' v2 in
358	let len = of_int 3 op' v3 in	2✔
359	try to_str (String.sub str i len)	2✔
360	with Invalid_argument _ -> eval_error `Index_out_of_bounds	×
361	end
362	\| String_replace ->	2✔
363	let t = of_str 2 op' v2 in
364	let t' = of_str 2 op' v3 in	2✔
365	to_str (replace str t t')	2✔
366	\| String_index ->	2✔
367	let t = of_str 2 op' v2 in
368	let i = of_int 3 op' v3 in	2✔
369	to_int (indexof str t i)	2✔
370	\| _ -> eval_error (`Unsupported_operator (`Triop op, Ty_str))	×
371
372	let relop (op : Ty.Relop.t) v1 v2 =
373	let f =	14✔
374	match op with
375	\| Lt -> ( < )	2✔
376	\| Le -> ( <= )	2✔
377	\| Gt -> ( > )	2✔
378	\| Ge -> ( >= )	2✔
379	\| Eq -> ( = )	3✔
380	\| Ne -> ( <> )	3✔
381	\| _ -> eval_error (`Unsupported_operator (`Relop op, Ty_str))	×
382	in
383	let f x y = f (String.compare x y) 0 in	14✔
384	f (of_str 1 (`Relop op) v1) (of_str 2 (`Relop op) v2)	14✔
385
386	let cvtop (op : Ty.Cvtop.t) v =
387	let op' = `Cvtop op in	12✔
388	match op with
389	\| String_to_code ->	2✔
390	let str = of_str 1 op' v in
391	to_int (Char.code str.[0])	2✔
392	\| String_from_code ->	2✔
393	let code = of_int 1 op' v in
394	to_str (String.make 1 (Char.chr code))	2✔
395	\| String_to_int -> begin	3✔
396	let s = of_str 1 op' v in
397	match int_of_string_opt s with	3✔
398	\| None -> eval_error `Invalid_format_conversion	1✔
399	\| Some x -> to_int x	2✔
400	end
401	\| String_from_int -> to_str (string_of_int (of_int 1 op' v))	2✔
402	\| String_to_float -> begin	3✔
403	let s = of_str 1 op' v in
404	match float_of_string_opt s with	3✔
405	\| None -> eval_error `Invalid_format_conversion	1✔
406	\| Some f -> to_real f	2✔
407	end
408	\| _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_str))	×
409
410	let naryop (op : Ty.Naryop.t) vs =
411	let op' = `Naryop op in	4✔
412	match op with
413	\| Concat -> to_str (String.concat "" (List.map (of_str 0 op') vs))	4✔
414	\| _ -> eval_error (`Unsupported_operator (`Naryop op, Ty_str))	×
415	end
416
417	module Lst = struct
418	let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
419	let lst = of_list 1 (`Unop op) v in	4✔
420	match op with	4✔
421	\| Head -> begin	1✔
422	(* FIXME: Exception handling *)
423	match lst with
424	\| hd :: _tl -> hd	1✔
425	\| [] -> assert false
426	end
427	\| Tail -> begin	1✔
428	(* FIXME: Exception handling *)
429	match lst with
430	\| _hd :: tl -> List tl	1✔
431	\| [] -> assert false
432	end
433	\| Length -> to_int (List.length lst)	1✔
434	\| Reverse -> List (List.rev lst)	1✔
435	\| _ -> eval_error (`Unsupported_operator (`Unop op, Ty_list))	×
436
437	let binop (op : Ty.Binop.t) v1 v2 =
438	let op' = `Binop op in	3✔
439	match op with
440	\| At ->	1✔
441	let lst = of_list 1 op' v1 in
442	let i = of_int 2 op' v2 in	1✔
443	(* TODO: change datastructure? *)
444	begin match List.nth_opt lst i with	1✔
445	\| None -> eval_error `Index_out_of_bounds	×
446	\| Some v -> v	1✔
447	end
448	\| List_cons -> List (v1 :: of_list 1 op' v2)	1✔
449	\| List_append -> List (of_list 1 op' v1 @ of_list 2 op' v2)	1✔
450	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_list))	×
451
452	let triop (op : Ty.Triop.t) (v1 : Value.t) (v2 : Value.t) (v3 : Value.t) :
453	Value.t =
454	let op' = `Triop op in	1✔
455	match op with
456	\| List_set ->	1✔
457	let lst = of_list 1 op' v1 in
458	let i = of_int 2 op' v2 in	1✔
459	let rec set i lst v acc =	1✔
460	match (i, lst) with	2✔
461	\| 0, _ :: tl -> List.rev_append acc (v :: tl)	1✔
462	\| i, hd :: tl -> set (i - 1) tl v (hd :: acc)	1✔
463	\| _, [] -> eval_error `Index_out_of_bounds	×
464	in
465	List (set i lst v3 [])	1✔
466	\| _ -> eval_error (`Unsupported_operator (`Triop op, Ty_list))	×
467
468	let naryop (op : Ty.Naryop.t) (vs : Value.t list) : Value.t =
469	let op' = `Naryop op in	×
470	match op with
471	\| Concat -> List (List.concat_map (of_list 0 op') vs)	×
472	\| _ -> eval_error (`Unsupported_operator (`Naryop op, Ty_list))	×
473	end
474
475	module I64 = struct
476	let cmp_u x op y = op Int64.(add x min_int) Int64.(add y min_int) [@@inline]	2✔
477
478	let lt_u x y = cmp_u x Int64.Infix.( < ) y [@@inline]	2✔
479	end
480
481	module Bitv = struct
482	let unop op bv =
483	let bv = of_bitv 1 (`Unop op) bv in	4✔
484	to_bitv	4✔
485	@@
486	match op with
487	\| Ty.Unop.Neg -> Bitvector.neg bv	2✔
488	\| Not -> Bitvector.lognot bv	2✔
489	\| Clz -> Bitvector.clz bv	×
490	\| Ctz -> Bitvector.ctz bv	×
491	\| Popcnt -> Bitvector.popcnt bv	×
492	\| _ ->	×
493	eval_error	×
494	(`Unsupported_operator (`Unop op, Ty_bitv (Bitvector.numbits bv)))	×
495
496	let binop op bv1 bv2 =
497	let bv1 = of_bitv 1 (`Binop op) bv1 in	38✔
498	let bv2 = of_bitv 2 (`Binop op) bv2 in	38✔
499	to_bitv	38✔
500	@@
501	match op with
502	\| Ty.Binop.Add -> Bitvector.add bv1 bv2	11✔
503	\| Sub -> Bitvector.sub bv1 bv2	4✔
504	\| Mul -> Bitvector.mul bv1 bv2	4✔
505	\| Div -> Bitvector.div bv1 bv2	2✔
506	\| DivU -> Bitvector.div_u bv1 bv2	×
507	\| Rem -> Bitvector.rem bv1 bv2	3✔
508	\| RemU -> Bitvector.rem_u bv1 bv2	×
509	\| And -> Bitvector.logand bv1 bv2	2✔
510	\| Or -> Bitvector.logor bv1 bv2	2✔
511	\| Xor -> Bitvector.logxor bv1 bv2	2✔
512	\| Shl -> Bitvector.shl bv1 bv2	2✔
513	\| ShrL -> Bitvector.lshr bv1 bv2	×
514	\| ShrA -> Bitvector.ashr bv1 bv2	2✔
515	\| Rotl -> Bitvector.rotate_left bv1 bv2	2✔
516	\| Rotr -> Bitvector.rotate_right bv1 bv2	2✔
517	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_bitv 0))	×
518
519	let relop op bv1 bv2 =
520	let bv1 = of_bitv 1 (`Relop op) bv1 in	23✔
521	let bv2 = of_bitv 2 (`Relop op) bv2 in	23✔
522	match op with	23✔
523	\| Ty.Relop.Lt -> Bitvector.lt bv1 bv2	3✔
524	\| LtU -> Bitvector.lt_u bv1 bv2	3✔
525	\| Le -> Bitvector.le bv1 bv2	3✔
526	\| LeU -> Bitvector.le_u bv1 bv2	3✔
527	\| Gt -> Bitvector.gt bv1 bv2	3✔
528	\| GtU -> Bitvector.gt_u bv1 bv2	2✔
529	\| Ge -> Bitvector.ge bv1 bv2	3✔
530	\| GeU -> Bitvector.ge_u bv1 bv2	2✔
531	\| Eq -> Bitvector.equal bv1 bv2	1✔
532	\| Ne -> not @@ Bitvector.equal bv1 bv2	×
533
534	let cvtop op bv =
UNCOV 535	let bv = of_bitv 1 (`Cvtop op) bv in	×
UNCOV 536	to_bitv	×
537	@@
538	match op with
UNCOV 539	\| Ty.Cvtop.Sign_extend m -> Bitvector.sign_extend m bv	×
UNCOV 540	\| Ty.Cvtop.Zero_extend m -> Bitvector.zero_extend m bv	×
UNCOV 541	\| _ ->	×
UNCOV 542	eval_error	×
UNCOV 543	(`Unsupported_operator (`Cvtop op, Ty_bitv (Bitvector.numbits bv)))	×
544	end
545
546	module F32 = struct
547	(* Stolen from Owi *)
548	let abs x = Int32.logand x Int32.max_int	6✔
549
550	let neg x = Int32.logxor x Int32.min_int	2✔
551
552	let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
553	let f = Int32.float_of_bits (of_fp32 1 (`Unop op) v) in	12✔
554	match op with	12✔
555	\| Neg -> to_fp32 @@ neg @@ of_fp32 1 (`Unop op) v	2✔
556	\| Abs -> to_fp32 @@ abs @@ of_fp32 1 (`Unop op) v	1✔
557	\| Sqrt -> fp32_of_float @@ Float.sqrt f	1✔
558	\| Nearest -> fp32_of_float @@ Float.round f	2✔
559	\| Ceil -> fp32_of_float @@ Float.ceil f	1✔
560	\| Floor -> fp32_of_float @@ Float.floor f	1✔
561	\| Trunc -> fp32_of_float @@ Float.trunc f	2✔
562	\| Is_nan -> if Float.is_nan f then Value.True else Value.False	1✔
UNCOV 563	\| _ -> eval_error (`Unsupported_operator (`Unop op, Ty_fp 32))	×
564
565	(* Stolen from Owi *)
566	let copy_sign x y = Int32.logor (abs x) (Int32.logand y Int32.min_int)	5✔
567
568	let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
569	let a = Int32.float_of_bits @@ of_fp32 1 (`Binop op) v1 in	13✔
570	let b = Int32.float_of_bits @@ of_fp32 1 (`Binop op) v2 in	13✔
571	match op with	13✔
572	\| Add -> fp32_of_float @@ Float.add a b	1✔
573	\| Sub -> fp32_of_float @@ Float.sub a b	1✔
574	\| Mul -> fp32_of_float @@ Float.mul a b	1✔
575	\| Div -> fp32_of_float @@ Float.div a b	2✔
576	\| Rem -> fp32_of_float @@ Float.rem a b	1✔
577	\| Min -> fp32_of_float @@ Float.min a b	1✔
578	\| Max -> fp32_of_float @@ Float.max a b	1✔
579	\| Copysign ->	5✔
580	let a = of_fp32 1 (`Binop op) v1 in
581	let b = of_fp32 1 (`Binop op) v2 in	5✔
582	to_fp32 (copy_sign a b)	5✔
583	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_fp 32))	×
584
585	let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
586	let f =	13✔
587	match op with
588	\| Eq -> Float.Infix.( = )	3✔
589	\| Ne -> Float.Infix.( <> )	2✔
590	\| Lt -> Float.Infix.( < )	2✔
591	\| Le -> Float.Infix.( <= )	2✔
592	\| Gt -> Float.Infix.( > )	2✔
593	\| Ge -> Float.Infix.( >= )	2✔
UNCOV 594	\| _ -> eval_error (`Unsupported_operator (`Relop op, Ty_fp 32))	×
595	in
596	let a = Int32.float_of_bits @@ of_fp32 1 (`Relop op) v1 in	13✔
597	let b = Int32.float_of_bits @@ of_fp32 2 (`Relop op) v2 in	13✔
598	f a b	13✔
599	end
600
601	module F64 = struct
602	(* Stolen from owi *)
603	let abs x = Int64.logand x Int64.max_int	6✔
604
605	let neg x = Int64.logxor x Int64.min_int	1✔
606
607	let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
608	let f = Int64.float_of_bits @@ of_fp64 1 (`Unop op) v in	11✔
609	match op with	11✔
610	\| Neg -> to_fp64 @@ neg @@ of_fp64 1 (`Unop op) v	1✔
611	\| Abs -> to_fp64 @@ abs @@ of_fp64 1 (`Unop op) v	1✔
612	\| Sqrt -> fp64_of_float @@ Float.sqrt f	1✔
613	\| Nearest -> fp64_of_float @@ Float.round f	2✔
614	\| Ceil -> fp64_of_float @@ Float.ceil f	1✔
615	\| Floor -> fp64_of_float @@ Float.floor f	1✔
616	\| Trunc -> fp64_of_float @@ Float.trunc f	2✔
617	\| Is_nan -> if Float.is_nan f then Value.True else Value.False	1✔
UNCOV 618	\| _ -> Fmt.failwith {\|unop: Unsupported f32 operator "%a"\|} Ty.Unop.pp op	×
619
620	let copy_sign x y = Int64.logor (abs x) (Int64.logand y Int64.min_int)	5✔
621
622	let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
623	let a = Int64.float_of_bits @@ of_fp64 1 (`Binop op) v1 in	13✔
624	let b = Int64.float_of_bits @@ of_fp64 2 (`Binop op) v2 in	13✔
625	match op with	13✔
626	\| Add -> fp64_of_float @@ Float.add a b	1✔
627	\| Sub -> fp64_of_float @@ Float.sub a b	1✔
628	\| Mul -> fp64_of_float @@ Float.mul a b	1✔
629	\| Div -> fp64_of_float @@ Float.div a b	2✔
630	\| Rem -> fp64_of_float @@ Float.rem a b	1✔
631	\| Min -> fp64_of_float @@ Float.min a b	1✔
632	\| Max -> fp64_of_float @@ Float.max a b	1✔
633	\| Copysign ->	5✔
634	let a = of_fp64 1 (`Binop op) v1 in
635	let b = of_fp64 2 (`Binop op) v2 in	5✔
636	to_fp64 @@ copy_sign a b	5✔
637	\| _ -> eval_error (`Unsupported_operator (`Binop op, Ty_fp 64))	×
638
639	let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
640	let f =	12✔
641	match op with
642	\| Eq -> Float.Infix.( = )	2✔
643	\| Ne -> Float.Infix.( <> )	2✔
644	\| Lt -> Float.Infix.( < )	2✔
645	\| Le -> Float.Infix.( <= )	2✔
646	\| Gt -> Float.Infix.( > )	2✔
647	\| Ge -> Float.Infix.( >= )	2✔
UNCOV 648	\| _ -> eval_error (`Unsupported_operator (`Relop op, Ty_fp 64))	×
649	in
650	let a = Int64.float_of_bits @@ of_fp64 1 (`Relop op) v1 in	12✔
651	let b = Int64.float_of_bits @@ of_fp64 2 (`Relop op) v2 in	12✔
652	f a b	12✔
653	end
654
655	module I32CvtOp = struct
656	let trunc_f32_s (x : int32) =
UNCOV 657	if Int32.Infix.(x <> x) then eval_error `Conversion_to_integer	×
658	else
659	let xf = Int32.float_of_bits x in	2✔
660	if	2✔
661	Float.Infix.(
UNCOV 662	xf >= -.Int32.(to_float min_int) \|\| xf < Int32.(to_float min_int) )	×
UNCOV 663	then eval_error `Integer_overflow	×
664	else Int32.of_float xf	2✔
665
666	let trunc_f32_u (x : int32) =
UNCOV 667	if Int32.Infix.(x <> x) then eval_error `Conversion_to_integer	×
668	else
669	let xf = Int32.float_of_bits x in	1✔
670	if Float.Infix.(xf >= -.Int32.(to_float min_int) *. 2.0 \|\| xf <= -1.0)	×
UNCOV 671	then eval_error `Integer_overflow	×
672	else Int32.of_float xf	1✔
673
674	let trunc_f64_s (x : int64) =
UNCOV 675	if Int64.Infix.(x <> x) then eval_error `Conversion_to_integer	×
676	else
677	let xf = Int64.float_of_bits x in	2✔
678	if	2✔
679	Float.Infix.(
UNCOV 680	xf >= -.Int64.(to_float min_int) \|\| xf < Int64.(to_float min_int) )	×
UNCOV 681	then eval_error `Integer_overflow	×
682	else Int32.of_float xf	2✔
683
684	let trunc_f64_u (x : int64) =
685	if Int64.Infix.(x <> x) then eval_error `Conversion_to_integer	×
686	else
687	let xf = Int64.float_of_bits x in	1✔
UNCOV 688	if Float.Infix.(xf >= -.Int64.(to_float min_int) *. 2.0 \|\| xf <= -1.0)	×
UNCOV 689	then eval_error `Integer_overflow	×
690	else Int32.of_float xf	1✔
691
692	let trunc_sat_f32_s x =
693	if Int32.Infix.(x <> x) then 0l	×
694	else
695	let xf = Int32.float_of_bits x in	1✔
UNCOV 696	if Float.Infix.(xf < Int32.(to_float min_int)) then Int32.min_int	×
UNCOV 697	else if Float.Infix.(xf >= -.Int32.(to_float min_int)) then Int32.max_int	×
698	else Int32.of_float xf	1✔
699
700	let trunc_sat_f32_u x =
701	if Int32.Infix.(x <> x) then 0l	×
702	else
703	let xf = Int32.float_of_bits x in	1✔
UNCOV 704	if Float.Infix.(xf <= -1.0) then 0l	×
UNCOV 705	else if Float.Infix.(xf >= -.Int32.(to_float min_int) *. 2.0) then -1l	×
706	else Int32.of_float xf	1✔
707
708	let trunc_sat_f64_s x =
709	if Int64.Infix.(x <> x) then 0l	×
710	else
711	let xf = Int64.float_of_bits x in	1✔
UNCOV 712	if Float.Infix.(xf < Int64.(to_float min_int)) then Int32.min_int	×
UNCOV 713	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then Int32.max_int	×
714	else Int32.of_float xf	1✔
715
716	let trunc_sat_f64_u x =
UNCOV 717	if Int64.Infix.(x <> x) then 0l	×
718	else
719	let xf = Int64.float_of_bits x in	1✔
UNCOV 720	if Float.Infix.(xf <= -1.0) then 0l	×
UNCOV 721	else if Float.Infix.(xf >= -.Int64.(to_float min_int) *. 2.0) then -1l	×
722	else Int32.of_float xf	1✔
723
724	let cvtop op v =
725	let op' = `Cvtop op in	17✔
726	match op with
727	\| Ty.Cvtop.WrapI64 -> bitv_of_int32 (Int64.to_int32 (int64_of_bitv 1 op' v))	2✔
728	\| TruncSF32 -> bitv_of_int32 (trunc_f32_s (of_fp32 1 op' v))	2✔
729	\| TruncUF32 -> bitv_of_int32 (trunc_f32_u (of_fp32 1 op' v))	1✔
730	\| TruncSF64 -> bitv_of_int32 (trunc_f64_s (of_fp64 1 op' v))	2✔
731	\| TruncUF64 -> bitv_of_int32 (trunc_f64_u (of_fp64 1 op' v))	1✔
732	\| Trunc_sat_f32_s -> bitv_of_int32 (trunc_sat_f32_s (of_fp32 1 op' v))	1✔
733	\| Trunc_sat_f32_u -> bitv_of_int32 (trunc_sat_f32_u (of_fp32 1 op' v))	1✔
734	\| Trunc_sat_f64_s -> bitv_of_int32 (trunc_sat_f64_s (of_fp64 1 op' v))	1✔
735	\| Trunc_sat_f64_u -> bitv_of_int32 (trunc_sat_f64_u (of_fp64 1 op' v))	1✔
736	\| Reinterpret_float -> bitv_of_int32 (of_fp32 1 op' v)	2✔
737	\| Sign_extend n -> to_bitv (Bitvector.sign_extend n (of_bitv 1 op' v))	2✔
738	\| Zero_extend n -> to_bitv (Bitvector.zero_extend n (of_bitv 1 op' v))	1✔
UNCOV 739	\| OfBool -> v (* v is already a number here *)	×
UNCOV 740	\| ToBool \| _ -> eval_error (`Unsupported_operator (op', Ty_bitv 32))	×
741	end
742
743	module I64CvtOp = struct
744	let extend_i32_u (x : int32) =
745	Int64.(logand (of_int32 x) 0x0000_0000_ffff_ffffL)	1✔
746
747	let trunc_f32_s (x : int32) =
UNCOV 748	if Int32.Infix.(x <> x) then eval_error `Conversion_to_integer	×
749	else
750	let xf = Int32.float_of_bits x in	2✔
751	if	2✔
752	Float.Infix.(
753	xf >= -.Int64.(to_float min_int) \|\| xf < Int64.(to_float min_int) )	×
UNCOV 754	then eval_error `Integer_overflow	×
755	else Int64.of_float xf	2✔
756
757	let trunc_f32_u (x : int32) =
UNCOV 758	if Int32.Infix.(x <> x) then eval_error `Conversion_to_integer	×
759	else
760	let xf = Int32.float_of_bits x in	1✔
UNCOV 761	if Float.Infix.(xf >= -.Int64.(to_float min_int) *. 2.0 \|\| xf <= -1.0)	×
762	then eval_error `Integer_overflow	×
763	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then	1✔
UNCOV 764	Int64.(logxor (of_float (xf -. 0x1p63)) min_int)	×
765	else Int64.of_float xf	1✔
766
767	let trunc_f64_s (x : int64) =
UNCOV 768	if Int64.Infix.(x <> x) then eval_error `Conversion_to_integer	×
769	else
770	let xf = Int64.float_of_bits x in	2✔
771	if	2✔
772	Float.Infix.(
773	xf >= -.Int64.(to_float min_int) \|\| xf < Int64.(to_float min_int) )	×
UNCOV 774	then eval_error `Integer_overflow	×
775	else Int64.of_float xf	2✔
776
777	let trunc_f64_u (x : int64) =
UNCOV 778	if Int64.Infix.(x <> x) then eval_error `Conversion_to_integer	×
779	else
780	let xf = Int64.float_of_bits x in	1✔
781	if Float.Infix.(xf >= -.Int64.(to_float min_int) *. 2.0 \|\| xf <= -1.0)	×
UNCOV 782	then eval_error `Integer_overflow	×
783	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then	1✔
UNCOV 784	Int64.(logxor (of_float (xf -. 0x1p63)) min_int)	×
785	else Int64.of_float xf	1✔
786
787	let trunc_sat_f32_s (x : int32) =
788	if Int32.Infix.(x <> x) then 0L	×
789	else
790	let xf = Int32.float_of_bits x in	1✔
791	if Float.Infix.(xf < Int64.(to_float min_int)) then Int64.min_int	×
UNCOV 792	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then Int64.max_int	×
793	else Int64.of_float xf	1✔
794
795	let trunc_sat_f32_u (x : int32) =
UNCOV 796	if Int32.Infix.(x <> x) then 0L	×
797	else
798	let xf = Int32.float_of_bits x in	1✔
799	if Float.Infix.(xf <= -1.0) then 0L	×
UNCOV 800	else if Float.Infix.(xf >= -.Int64.(to_float min_int) *. 2.0) then -1L	×
801	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then	1✔
UNCOV 802	Int64.(logxor (of_float (xf -. 0x1p63)) min_int)	×
803	else Int64.of_float xf	1✔
804
805	let trunc_sat_f64_s (x : int64) =
806	if Int64.Infix.(x <> x) then 0L	×
807	else
808	let xf = Int64.float_of_bits x in	1✔
809	if Float.Infix.(xf < Int64.(to_float min_int)) then Int64.min_int	×
UNCOV 810	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then Int64.max_int	×
811	else Int64.of_float xf	1✔
812
813	let trunc_sat_f64_u (x : int64) =
UNCOV 814	if Int64.Infix.(x <> x) then 0L	×
815	else
816	let xf = Int64.float_of_bits x in	1✔
UNCOV 817	if Float.Infix.(xf <= -1.0) then 0L	×
UNCOV 818	else if Float.Infix.(xf >= -.Int64.(to_float min_int) *. 2.0) then -1L	×
819	else if Float.Infix.(xf >= -.Int64.(to_float min_int)) then	1✔
UNCOV 820	Int64.(logxor (of_float (xf -. 0x1p63)) min_int)	×
821	else Int64.of_float xf	1✔
822
823	let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
824	let op' = `Cvtop op in	17✔
825	match op with
826	\| Sign_extend n -> to_bitv (Bitvector.sign_extend n (of_bitv 1 op' v))	3✔
827	\| Zero_extend n -> to_bitv (Bitvector.zero_extend n (of_bitv 1 op' v))	2✔
828	\| TruncSF32 -> bitv_of_int64 (trunc_f32_s (of_fp32 1 op' v))	2✔
829	\| TruncUF32 -> bitv_of_int64 (trunc_f32_u (of_fp32 1 op' v))	1✔
830	\| TruncSF64 -> bitv_of_int64 (trunc_f64_s (of_fp64 1 op' v))	2✔
831	\| TruncUF64 -> bitv_of_int64 (trunc_f64_u (of_fp64 1 op' v))	1✔
832	\| Trunc_sat_f32_s -> bitv_of_int64 (trunc_sat_f32_s (of_fp32 1 op' v))	1✔
833	\| Trunc_sat_f32_u -> bitv_of_int64 (trunc_sat_f32_u (of_fp32 1 op' v))	1✔
834	\| Trunc_sat_f64_s -> bitv_of_int64 (trunc_sat_f64_s (of_fp64 1 op' v))	1✔
835	\| Trunc_sat_f64_u -> bitv_of_int64 (trunc_sat_f64_u (of_fp64 1 op' v))	1✔
836	\| Reinterpret_float -> bitv_of_int64 (of_fp64 1 op' v)	1✔
837	\| WrapI64 -> type_error 1 v (Ty_bitv 64) op' "Cannot wrapI64 on an I64"	1✔
UNCOV 838	\| ToBool \| OfBool \| _ -> eval_error (`Unsupported_operator (op', Ty_bitv 64))	×
839	end
840
841	module F32CvtOp = struct
842	let demote_f64 x =
843	let xf = Int64.float_of_bits x in	2✔
844	if Float.Infix.(xf = xf) then Int32.bits_of_float xf	1✔
845	else
846	let nan64bits = x in	1✔
847	let sign_field =
848	Int64.(shift_left (shift_right_logical nan64bits 63) 31)	1✔
849	in
850	let significand_field =
851	Int64.(shift_right_logical (shift_left nan64bits 12) 41)	1✔
852	in
853	let fields = Int64.logor sign_field significand_field in
854	Int32.logor 0x7fc0_0000l (Int64.to_int32 fields)	1✔
855
856	let convert_i32_s x = Int32.bits_of_float (Int32.to_float x)	2✔
857
858	let convert_i32_u x =
859	Int32.bits_of_float	2✔
860	Int32.(
861	Int32.Infix.(
862	if x >= 0l then to_float x	1✔
863	else to_float (logor (shift_right_logical x 1) (logand x 1l)) *. 2.0 ) )	1✔
864
865	let convert_i64_s x =
866	Int32.bits_of_float	3✔
867	Int64.(
868	Int64.Infix.(
869	if abs x < 0x10_0000_0000_0000L then to_float x	2✔
870	else
UNCOV 871	let r = if logand x 0xfffL = 0L then 0L else 1L in	×
872	to_float (logor (shift_right x 12) r) *. 0x1p12 ) )	1✔
873
874	let convert_i64_u x =
875	Int32.bits_of_float	2✔
876	Int64.(
877	Int64.Infix.(
878	if I64.lt_u x 0x10_0000_0000_0000L then to_float x	1✔
879	else
UNCOV 880	let r = if logand x 0xfffL = 0L then 0L else 1L in	×
881	to_float (logor (shift_right_logical x 12) r) *. 0x1p12 ) )	1✔
882
883	let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
884	let op' = `Cvtop op in	13✔
885	match op with
886	\| DemoteF64 -> to_fp32 (demote_f64 (of_fp64 1 op' v))	2✔
887	\| ConvertSI32 -> to_fp32 (convert_i32_s (int32_of_bitv 1 op' v))	2✔
888	\| ConvertUI32 -> to_fp32 (convert_i32_u (int32_of_bitv 1 op' v))	2✔
889	\| ConvertSI64 -> to_fp32 (convert_i64_s (int64_of_bitv 1 op' v))	3✔
890	\| ConvertUI64 -> to_fp32 (convert_i64_u (int64_of_bitv 1 op' v))	2✔
891	\| Reinterpret_int -> to_fp32 (int32_of_bitv 1 op' v)	1✔
892	\| PromoteF32 -> type_error 1 v (Ty_fp 32) op' "F64 must promote F32"	1✔
UNCOV 893	\| ToString \| OfString \| _ ->	×
894	eval_error (`Unsupported_operator (op', Ty_fp 32))
895	end
896
897	module F64CvtOp = struct
898	let promote_f32 x =
899	let xf = Int32.float_of_bits x in	2✔
900	if Float.Infix.(xf = xf) then Int64.bits_of_float xf	1✔
901	else
902	let nan32bits = I64CvtOp.extend_i32_u x in	1✔
903	let sign_field =	1✔
904	Int64.(shift_left (shift_right_logical nan32bits 31) 63)	1✔
905	in
906	let significand_field =
907	Int64.(shift_right_logical (shift_left nan32bits 41) 12)	1✔
908	in
909	let fields = Int64.logor sign_field significand_field in
910	Int64.logor 0x7ff8_0000_0000_0000L fields	1✔
911
912	let convert_i32_s x = Int64.bits_of_float (Int32.to_float x)	2✔
913
914	(*
915	* Unlike the other convert_u functions, the high half of the i32 range is
916	* within the range where f32 can represent odd numbers, so we can't do the
917	* shift. Instead, we can use int64 signed arithmetic.
918	*)
919	let convert_i32_u x =
920	Int64.bits_of_float	1✔
921	Int64.(to_float (logand (of_int32 x) 0x0000_0000_ffff_ffffL))	1✔
922
923	let convert_i64_s x = Int64.bits_of_float (Int64.to_float x)	2✔
924
925	(*
926	* Values in the low half of the int64 range can be converted with a signed
927	* conversion. The high half is beyond the range where f64 can represent odd
928	* numbers, so we can shift the value right, adjust the least significant
929	* bit to round correctly, do a conversion, and then scale it back up.
930	*)
931	let convert_i64_u (x : int64) =
932	Int64.bits_of_float	2✔
933	Int64.(
934	Int64.Infix.(
935	if x >= 0L then to_float x	1✔
936	else to_float (logor (shift_right_logical x 1) (logand x 1L)) *. 2.0 ) )	1✔
937
938	let cvtop (op : Ty.Cvtop.t) v : Value.t =
939	let op' = `Cvtop op in	11✔
940	match op with
941	\| PromoteF32 -> to_fp64 (promote_f32 (of_fp32 1 op' v))	2✔
942	\| ConvertSI32 -> to_fp64 (convert_i32_s (int32_of_bitv 1 op' v))	2✔
943	\| ConvertUI32 -> to_fp64 (convert_i32_u (int32_of_bitv 1 op' v))	1✔
944	\| ConvertSI64 -> to_fp64 (convert_i64_s (int64_of_bitv 1 op' v))	2✔
945	\| ConvertUI64 -> to_fp64 (convert_i64_u (int64_of_bitv 1 op' v))	2✔
946	\| Reinterpret_int -> to_fp64 (int64_of_bitv 1 op' v)	1✔
947	\| DemoteF64 -> type_error 1 v (Ty_fp 64) op' "F32 must demote a F64"	1✔
UNCOV 948	\| ToString \| OfString \| _ ->	×
949	eval_error (`Unsupported_operator (op', Ty_fp 64))
950	end
951
952	(* Dispatch *)
953
954	let op int real bool str lst bv f32 f64 ty op =
955	match ty with	202✔
956	\| Ty.Ty_int -> int op	37✔
957	\| Ty_real -> real op	35✔
958	\| Ty_bool -> bool op	16✔
959	\| Ty_str -> str op	14✔
960	\| Ty_list -> lst op	7✔
961	\| Ty_bitv _ -> bv op	42✔
962	\| Ty_fp 32 -> f32 op	26✔
963	\| Ty_fp 64 -> f64 op	25✔
UNCOV 964	\| Ty_fp _ \| Ty_app \| Ty_unit \| Ty_none \| Ty_regexp \| Ty_roundingMode ->	×
965	eval_error (`Unsupported_theory ty)
966	[@@inline]
967
968	let unop =
969	op Int.unop Real.unop Bool.unop Str.unop Lst.unop Bitv.unop F32.unop F64.unop	7✔
970
971	let binop =
972	op Int.binop Real.binop Bool.binop Str.binop Lst.binop Bitv.binop F32.binop	7✔
973	F64.binop
974
975	let triop = function
976	\| Ty.Ty_bool -> Bool.triop	2✔
977	\| Ty_str -> Str.triop	6✔
978	\| Ty_list -> Lst.triop	1✔
UNCOV 979	\| ty -> eval_error (`Unsupported_theory ty)	×
980
981	let relop = function
982	\| Ty.Ty_int -> Int.relop	8✔
983	\| Ty_real -> Real.relop	12✔
984	\| Ty_bool -> Bool.relop	9✔
985	\| Ty_str -> Str.relop	14✔
986	\| Ty_bitv _ -> Bitv.relop	23✔
987	\| Ty_fp 32 -> F32.relop	13✔
988	\| Ty_fp 64 -> F64.relop	12✔
UNCOV 989	\| ty -> eval_error (`Unsupported_theory ty)	×
990
991	let cvtop = function
992	\| Ty.Ty_int -> Int.cvtop	5✔
993	\| Ty_real -> Real.cvtop	8✔
994	\| Ty_str -> Str.cvtop	12✔
995	\| Ty_bitv 32 -> I32CvtOp.cvtop	17✔
996	\| Ty_bitv 64 -> I64CvtOp.cvtop	17✔
997	(* Remaining fall into arbitrary-width bv cvtop operations *)
UNCOV 998	\| Ty_bitv _m -> Bitv.cvtop	×
999	\| Ty_fp 32 -> F32CvtOp.cvtop	13✔
1000	\| Ty_fp 64 -> F64CvtOp.cvtop	11✔
UNCOV 1001	\| ty -> eval_error (`Unsupported_theory ty)	×
1002
1003	let naryop = function
1004	\| Ty.Ty_bool -> Bool.naryop	6✔
1005	\| Ty_str -> Str.naryop	4✔
UNCOV 1006	\| Ty_list -> Lst.naryop	×
UNCOV 1007	\| ty -> eval_error (`Unsupported_theory ty)	×

formalsec / smtml / 452

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous