Memdata.v

Require Import Coqlib.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.

(** * Properties of memory chunks *)

(** Memory reads and writes are performed by quantities called memory chunks,
  encoding the type, size and signedness of the chunk being addressed.
  The following functions extract the size information from a chunk. *)

Definition size_chunk (chunk: memory_chunk) : Z :=
  match chunk with
  | Mint8signed => 1
  | Mint8unsigned => 1
  | Mint16signed => 2
  | Mint16unsigned => 2
  | Mint32 => 4
  | Mfloat32 => 4
  | Mfloat64 => 8
  end.

Lemma size_chunk_pos:
  forall chunk, size_chunk chunk > 0.
Proof.
  intros. destruct chunk; simpl; omega.
Qed.

Definition size_chunk_nat (chunk: memory_chunk) : nat :=
  nat_of_Z(size_chunk chunk).

Lemma size_chunk_conv:
  forall chunk, size_chunk chunk = Z_of_nat (size_chunk_nat chunk).
Proof.
  intros. destruct chunk; reflexivity.
Qed.

Lemma size_chunk_nat_pos:
  forall chunk, exists n, size_chunk_nat chunk = S n.
Proof.
  intros. 
  generalize (size_chunk_pos chunk). rewrite size_chunk_conv. 
  destruct (size_chunk_nat chunk).
  simpl; intros; omegaContradiction.
  intros; exists n; auto.
Qed.

(** Memory reads and writes must respect alignment constraints:
  the byte offset of the location being addressed should be an exact
  multiple of the natural alignment for the chunk being addressed.
  This natural alignment is defined by the following 
  [align_chunk] function.  Some target architectures
  (e.g. the PowerPC) have no alignment constraints, which we could
  reflect by taking [align_chunk chunk = 1].  However, other architectures
  have stronger alignment requirements.  The following definition is
  appropriate for PowerPC and ARM. *)

Definition align_chunk (chunk: memory_chunk) : Z := 
  match chunk with
  | Mint8signed => 1
  | Mint8unsigned => 1
  | Mint16signed => 2
  | Mint16unsigned => 2
  | _ => 4
  end.

Lemma align_chunk_pos:
  forall chunk, align_chunk chunk > 0.
Proof.
  intro. destruct chunk; simpl; omega.
Qed.

Lemma align_size_chunk_divides:
  forall chunk, (align_chunk chunk | size_chunk chunk).
Proof.
  intros. destruct chunk; simpl; try apply Zdivide_refl. exists 2; auto. 
Qed.

Lemma align_chunk_compat:
  forall chunk1 chunk2,
  size_chunk chunk1 = size_chunk chunk2 -> align_chunk chunk1 = align_chunk chunk2.
Proof.
  intros chunk1 chunk2. 
  destruct chunk1; destruct chunk2; simpl; congruence.
Qed.

(** The type (integer/pointer or float) of a chunk. *)

Definition type_of_chunk (c: memory_chunk) : typ :=
  match c with
  | Mint8signed => Tint
  | Mint8unsigned => Tint
  | Mint16signed => Tint
  | Mint16unsigned => Tint
  | Mint32 => Tint
  | Mfloat32 => Tfloat
  | Mfloat64 => Tfloat
  end.

(** * Memory values *)

(** A ``memory value'' is a byte-sized quantity that describes the current
  content of a memory cell.  It can be either:
- a concrete 8-bit integer;
- a byte-sized fragment of an opaque pointer;
- the special constant [Undef] that represents uninitialized memory.
*)

(** Values stored in memory cells. *)

Inductive memval: Type :=
  | Undef: memval
  | Byte: byte -> memval
  | Pointer: block -> int -> nat -> memval.

(** * Encoding and decoding integers *)

(** We define functions to convert between integers and lists of bytes
  according to a given memory chunk. *)

Parameter big_endian: bool.

Definition rev_if_le (l: list byte) : list byte :=
  if big_endian then l else List.rev l.

Lemma rev_if_le_involutive:
  forall l, rev_if_le (rev_if_le l) = l.
Proof.
  intros; unfold rev_if_le; destruct big_endian. 
  auto.
  apply List.rev_involutive. 
Qed.

Lemma rev_if_le_length:
  forall l, length (rev_if_le l) = length l.
Proof.
  intros; unfold rev_if_le; destruct big_endian.
  auto.
  apply List.rev_length.
Qed.

Definition encode_int (c: memory_chunk) (x: int) : list byte :=
  let n := Int.unsigned x in
  rev_if_le (match c with
  | Mint8signed | Mint8unsigned =>
      Byte.repr n :: nil
  | Mint16signed | Mint16unsigned =>
      Byte.repr (n/256) :: Byte.repr n :: nil
  | Mint32 =>
      Byte.repr (n/16777216) :: Byte.repr (n/65536) :: Byte.repr (n/256) :: Byte.repr n :: nil
  | Mfloat32 =>
      Byte.zero :: Byte.zero :: Byte.zero :: Byte.zero :: nil
  | Mfloat64 =>
      Byte.zero :: Byte.zero :: Byte.zero :: Byte.zero ::
      Byte.zero :: Byte.zero :: Byte.zero :: Byte.zero :: nil
  end).

Definition decode_int (c: memory_chunk) (b: list byte) : int :=
  match c, rev_if_le b with
  | Mint8signed, b1 :: nil =>
      Int.sign_ext 8 (Int.repr (Byte.unsigned b1))
  | Mint8unsigned, b1 :: nil =>
      Int.repr (Byte.unsigned b1)
  | Mint16signed, b1 :: b2 :: nil =>
      Int.sign_ext 16 (Int.repr (Byte.unsigned b1 * 256 + Byte.unsigned b2))
  | Mint16unsigned, b1 :: b2 :: nil =>
      Int.repr (Byte.unsigned b1 * 256 + Byte.unsigned b2)
  | Mint32, b1 :: b2 :: b3 :: b4 :: nil =>
      Int.repr (Byte.unsigned b1 * 16777216 + Byte.unsigned b2 * 65536
                + Byte.unsigned b3 * 256 + Byte.unsigned b4)
  | _, _ => Int.zero
  end.

Lemma encode_int_length:
  forall chunk n, length(encode_int chunk n) = size_chunk_nat chunk.
Proof.
  intros. unfold encode_int. rewrite rev_if_le_length.
  destruct chunk; reflexivity.
Qed.

Lemma decode_encode_int8unsigned: forall n,
  decode_int Mint8unsigned (encode_int Mint8unsigned n) = Int.zero_ext 8 n.
Proof.
  intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive.
  simpl. auto.
Qed.

Lemma decode_encode_int8signed: forall n,
  decode_int Mint8signed (encode_int Mint8signed n) = Int.sign_ext 8 n.
Proof.
  intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive. simpl.
  change (Int.repr (Int.unsigned n mod Byte.modulus))
  with (Int.zero_ext 8 n).
  apply Int.sign_ext_zero_ext. compute; auto.
Qed.

Remark recombine_16:
  forall x,
  (x / 256) mod Byte.modulus * 256 + x mod Byte.modulus = x mod (two_p 16).