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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2026 OCamlPro *)
(* Written by the Owi programmers *)
module Size = struct
let b32 = Units.In_bits.s32
let b64 = Units.In_bits.of_int 64
let equal s1 s2 = Units.In_bits.compare s1 s2 = 0
end
type boolean = Abstract_boolean.t
type i32 = Abstract_i32.t
type i64 = Abstract_i64.t
type f32 = Abstract_f32.t
type f64 = Abstract_f64.t
type v128 = Abstract_v128.t
module Boolean = Abstract_boolean
module I32 = Abstract_i32
module I64 = Abstract_i64
module F32 = Abstract_f32
module F64 = Abstract_f64
module V128 = Abstract_v128
module Ref = Abstract_ref
type t =
| I32 of i32
| I64 of i64
| F32 of f32
| F64 of f64
| V128 of v128
| Ref of Ref.t
let pp ppf = function
| I32 _b -> Fmt.pf ppf "i32 ..."
| I64 _b -> Fmt.pf ppf "i64 ..."
| _ -> .
let pp_with_ctx ctx ppf = function
| I32 b -> Fmt.pf ppf "i32 %a" (Abstract_i32.pp ctx) b
| I64 b -> Fmt.pf ppf "i64 %a" (Abstract_i64.pp ctx) b
| _ -> .
let equal v1 v2 =
match (v1, v2) with
| I32 v1, I32 v2 -> Abstract_i32.equal v1 v2
| I64 v1, I64 v2 -> Abstract_i64.equal v1 v2
| I32 _, I64 _ | I64 _, I32 _ -> false
| _ -> .
let to_binary = function
| I32 b -> Abstract_i32.to_binary b
| I64 b -> Abstract_i64.to_binary b
| _ -> .
let of_binary size x =
match Units.In_bits.to_int size with
| 32 -> I32 (I32.of_binary x)
| 64 -> I64 (I64.of_binary x)
| _ -> assert false
let of_boolean ctx size boolean =
let true_ = Abstract_boolean.true_ ctx in
let n = if Abstract_boolean.equal boolean true_ then 1 else 0 in
match Units.In_bits.to_int size with
| 32 -> I32 (Abstract_i32.of_int ctx n)
| 64 -> I64 (Abstract_i64.of_int ctx n)
| _ -> assert false
let size_of = function I32 _ -> Size.b32 | I64 _ -> Size.b64 | _ -> .
let to_boolean ctx x =
let size = Size.b32 in
let zero = Abstract_domain.Binary_Forward.biconst ~size Z.zero ctx in
Abstract_domain.Binary_Forward.beq ~size ctx (to_binary x) zero
let top size ctx = of_binary size @@ Abstract_domain.binary_empty ~size ctx