blob: 3a3942846ae994dff7f652e7ac1decf2eba5de64 (
plain)
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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
open Camlcoq
open Integers
open AST
let big_endian =
match Configuration.arch with
| "powerpc" -> true
| "arm" -> false
| _ -> assert false
let encode_float chunk f =
match chunk with
| Mint8unsigned | Mint8signed ->
[Byte.zero]
| Mint16unsigned | Mint16signed ->
[Byte.zero; Byte.zero]
| Mint32 ->
[Byte.zero; Byte.zero; Byte.zero; Byte.zero]
| Mfloat32 ->
let bits = Int32.bits_of_float f in
let byte n =
coqint_of_camlint
(Int32.logand (Int32.shift_right_logical bits n) 0xFFl) in
if big_endian then
[byte 24; byte 16; byte 8; byte 0]
else
[byte 0; byte 8; byte 16; byte 24]
| Mfloat64 ->
let bits = Int64.bits_of_float f in
let byte n =
coqint_of_camlint
(Int64.to_int32
(Int64.logand (Int64.shift_right_logical bits n) 0xFFL)) in
if big_endian then
[byte 56; byte 48; byte 40; byte 32; byte 24; byte 16; byte 8; byte 0]
else
[byte 0; byte 8; byte 16; byte 24; byte 32; byte 40; byte 48; byte 56]
let decode_float chunk bytes =
match chunk with
| Mfloat32 ->
let combine accu b =
Int32.logor (Int32.shift_left accu 8) (camlint_of_coqint b) in
Int32.float_of_bits
(List.fold_left combine 0l
(if big_endian then bytes else List.rev bytes))
| Mfloat64 ->
let combine accu b =
Int64.logor (Int64.shift_left accu 8)
(Int64.of_int32 (camlint_of_coqint b)) in
Int64.float_of_bits
(List.fold_left combine 0L
(if big_endian then bytes else List.rev bytes))
| _ ->
0.0 (* unspecified *)
|
