src/num.ml

 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

(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2024 formalsec *)
(* Written by the Smtml programmers *)

type t =
  | I8 of int
  | I32 of int32
  | I64 of int64
  | F32 of int32
  | F64 of int64

type printer =
  [ `Pretty
  | `Hexadecimal
  ]

let type_of (n : t) =
  match n with
  | I8 _ -> Ty.(Ty_bitv 8)
  | I32 _ -> Ty.(Ty_bitv 32)
  | I64 _ -> Ty.(Ty_bitv 64)
  | F32 _ -> Ty.(Ty_fp 32)
  | F64 _ -> Ty.(Ty_fp 64)

let compare n1 n2 =
  match (n1, n2) with
  | I8 i1, I8 i2 -> Int.compare i1 i2
  | I32 i1, I32 i2 -> Int32.compare i1 i2
  | I64 i1, I64 i2 -> Int64.compare i1 i2
  | F32 i1, F32 i2 ->
    Float.compare (Int32.float_of_bits i1) (Int32.float_of_bits i2)
  | F64 i1, F64 i2 ->
    Float.compare (Int64.float_of_bits i1) (Int64.float_of_bits i2)
  | I8 _, _ -> -1
  | I32 _, I8 _ -> 1
  | I32 _, _ -> -1
  | I64 _, (I8 _ | I32 _) -> 1
  | I64 _, _ -> -1
  | F32 _, (I8 _ | I32 _ | I64 _) -> 1
  | F32 _, F64 _ -> -1
  | F64 _, _ -> 1

let equal (n1 : t) (n2 : t) : bool = compare n1 n2 = 0

let num_of_bool (b : bool) : t = I32 (if b then 1l else 0l)

let pp_num fmt (n : t) =
  match n with
  | I8 i -> Fmt.pf fmt "(i8 %d)" i
  | I32 i -> Fmt.pf fmt "(i32 %ld)" i
  | I64 i -> Fmt.pf fmt "(i64 %Ld)" i
  | F32 f -> Fmt.pf fmt "(f32 %F)" (Int32.float_of_bits f)
  | F64 f -> Fmt.pf fmt "(f64 %F)" (Int64.float_of_bits f)

let pp_hex fmt (n : t) =
  match n with
  | I8 i -> Fmt.pf fmt "0x%02x" (i land 0xff)
  | I32 i -> Fmt.pf fmt "0x%08lx" i
  | I64 i -> Fmt.pf fmt "0x%016Lx" i
  | F32 f -> Fmt.pf fmt "(fp 0x%08lx)" f
  | F64 f -> Fmt.pf fmt "(fp 0x%016Lx)" f

let pp_no_type fmt = function
  | I8 i -> Fmt.pf fmt "%d" i
  | I32 i -> Fmt.pf fmt "%ld" i
  | I64 i -> Fmt.pf fmt "%Ld" i
  | F32 f -> Fmt.pf fmt "%F" (Int32.float_of_bits f)
  | F64 f -> Fmt.pf fmt "%F" (Int64.float_of_bits f)

let printer = ref pp_num

let set_default_printer = function
  | `Pretty -> printer := pp_num
  | `Hexadecimal -> printer := pp_hex

let pp fmt v = !printer fmt v

let to_string (n : t) : string = Fmt.str "%a" pp n

let of_string (cast : Ty.t) value =
  match cast with
  | Ty_bitv 8 -> (
    match int_of_string value with
    | None -> Error "invalid value, expected 8-bit bitv"
    | Some n -> Ok (I8 n) )
  | Ty_bitv 32 -> Ok (I32 (Int32.of_string value))
  | Ty_bitv 64 -> Ok (I64 (Int64.of_string value))
  | Ty_fp 32 -> (
    match float_of_string value with
    | None -> Error "invalid value, expected float"
    | Some n -> Ok (F32 (Int32.bits_of_float n)) )
  | Ty_fp 64 -> (
    match float_of_string value with
    | None -> Error "invalid value, expected float"
    | Some n -> Ok (F64 (Int64.bits_of_float n)) )
  | _ -> Error "invalid value, expected num"

let to_json (n : t) : Yojson.Basic.t = `String (to_string n)