src/concrete/concrete_f32.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

include Float32

type t = Float32.t

let demote_f64 x =
  if Float64.eq x x then Float32.of_float @@ Float64.to_float x
  else
    let nan64bits = Float64.to_bits x in
    let sign_field = Int64.(shift_left (shift_right_logical nan64bits 63) 31) in
    let significand_field =
      Int64.(shift_right_logical (shift_left nan64bits 12) 41)
    in
    let fields = Int64.logor sign_field significand_field in
    let nan32bits = Int32.logor 0x7fc0_0000l (Concrete_i32.wrap_i64 fields) in
    Float32.of_bits nan32bits

let convert_i32_s x = Float32.of_float (Int32.to_float x)

(*
 * Similar to convert_i64_u below, the high half of the i32 range are beyond
 * the range where f32 can represent odd numbers, though we do need to adjust
 * the least significant bit to round correctly.
 *)
let convert_i32_u x =
  Float32.of_float
    Int32.(
      if Int32.ge x zero then to_float x
      else to_float (logor (shift_right_logical x 1) (logand x 1l)) *. 2.0 )

(*
 * Values that are too large would get rounded when represented in f64,
 * but double rounding via i64->f64->f32 can produce inaccurate results.
 * Hence, for large values we shift right but make sure to accumulate the lost
 * bits in the least significant bit, such that rounding still is correct.
 *)
let convert_i64_s (x : int64) =
  Float32.of_float
    Int64.(
      if Int64.lt (abs x) 0x10_0000_0000_0000L then to_float x
      else
        let r = if Int64.eq (logand x 0xfffL) 0L then 0L else 1L in
        to_float (logor (shift_right x 12) r) *. 0x1p12 )

let convert_i64_u x =
  Float32.of_float
    Int64.(
      if Int64.lt_u x 0x10_0000_0000_0000L then to_float x
      else
        let r = if Int64.eq (logand x 0xfffL) 0L then 0L else 1L in
        to_float (logor (shift_right_logical x 12) r) *. 0x1p12 )

let reinterpret_i32 = Float32.of_bits

let of_concrete v = v