Merge of the newmem and newextcalls branches:

- Revised memory model with concrete representation of ints & floats,
  and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 68 insertions, 0 deletions

diff --git a/common/Memdataaux.ml b/common/Memdataaux.ml
new file mode 100644
index 0000000..3a39428
--- /dev/null
+++ b/common/Memdataaux.ml
@@ -0,0 +1,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 *)
+