Module Memdata


In-memory representation of values.

Require Import Coqlib.
Require Archi.
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
  | Mint64 => 8
  | Mfloat32 => 4
  | Mfloat64 => 8
  | Many32 => 4
  | Many64 => 8
  end.

Lemma size_chunk_pos:
  forall chunk, size_chunk chunk > 0.
Proof.

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.

Lemma size_chunk_nat_pos:
  forall chunk, exists n, size_chunk_nat chunk = S n.
Proof.

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. PowerPC and x86) 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, ARM and x86.

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

Lemma align_chunk_pos:
  forall chunk, align_chunk chunk > 0.
Proof.

Lemma align_size_chunk_divides:
  forall chunk, (align_chunk chunk | size_chunk chunk).
Proof.

Lemma align_le_divides:
  forall chunk1 chunk2,
  align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2).
Proof.

Inductive quantity : Type := Q32 | Q64.

Definition quantity_eq (q1 q2: quantity) : {q1 = q2} + {q1 <> q2}.
Proof.
Global Opaque quantity_eq.

Definition size_quantity_nat (q: quantity) :=
  match q with Q32 => 4%nat | Q64 => 8%nat end.

Lemma size_quantity_nat_pos:
  forall q, exists n, size_quantity_nat q = S n.
Proof.

Memory values


A ``memory value'' is a byte-sized quantity that describes the current content of a memory cell. It can be either:

Values stored in memory cells.

Inductive memval: Type :=
  | Undef: memval
  | Byte: byte -> memval
  | Fragment: val -> quantity -> nat -> memval.

Encoding and decoding integers


We define functions to convert between integers and lists of bytes of a given length

Fixpoint bytes_of_int (n: nat) (x: Z) {struct n}: list byte :=
  match n with
  | O => nil
  | S m => Byte.repr x :: bytes_of_int m (x / 256)
  end.

Fixpoint int_of_bytes (l: list byte): Z :=
  match l with
  | nil => 0
  | b :: l' => Byte.unsigned b + int_of_bytes l' * 256
  end.

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

Definition encode_int (sz: nat) (x: Z) : list byte :=
  rev_if_be (bytes_of_int sz x).

Definition decode_int (b: list byte) : Z :=
  int_of_bytes (rev_if_be b).

Length properties

Lemma length_bytes_of_int:
  forall n x, length (bytes_of_int n x) = n.
Proof.

Lemma rev_if_be_length:
  forall l, length (rev_if_be l) = length l.
Proof.

Lemma encode_int_length:
  forall sz x, length(encode_int sz x) = sz.
Proof.

Decoding after encoding

Lemma int_of_bytes_of_int:
  forall n x,
  int_of_bytes (bytes_of_int n x) = x mod (two_p (Z_of_nat n * 8)).
Proof.

Lemma rev_if_be_involutive:
  forall l, rev_if_be (rev_if_be l) = l.
Proof.

Lemma decode_encode_int:
  forall n x, decode_int (encode_int n x) = x mod (two_p (Z_of_nat n * 8)).
Proof.

Lemma decode_encode_int_1:
  forall x, Int.repr (decode_int (encode_int 1 (Int.unsigned x))) = Int.zero_ext 8 x.
Proof.

Lemma decode_encode_int_2:
  forall x, Int.repr (decode_int (encode_int 2 (Int.unsigned x))) = Int.zero_ext 16 x.
Proof.

Lemma decode_encode_int_4:
  forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x.
Proof.

Lemma decode_encode_int_8:
  forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x.
Proof.

A length-n encoding depends only on the low 8*n bits of the integer.

Lemma bytes_of_int_mod:
  forall n x y,
  Int.eqmod (two_p (Z_of_nat n * 8)) x y ->
  bytes_of_int n x = bytes_of_int n y.
Proof.

Lemma encode_int_8_mod:
  forall x y,
  Int.eqmod (two_p 8) x y ->
  encode_int 1%nat x = encode_int 1%nat y.
Proof.

Lemma encode_int_16_mod:
  forall x y,
  Int.eqmod (two_p 16) x y ->
  encode_int 2%nat x = encode_int 2%nat y.
Proof.

Encoding and decoding values


Definition inj_bytes (bl: list byte) : list memval :=
  List.map Byte bl.

Fixpoint proj_bytes (vl: list memval) : option (list byte) :=
  match vl with
  | nil => Some nil
  | Byte b :: vl' =>
      match proj_bytes vl' with None => None | Some bl => Some(b :: bl) end
  | _ => None
  end.

Remark length_inj_bytes:
  forall bl, length (inj_bytes bl) = length bl.
Proof.

Remark proj_inj_bytes:
  forall bl, proj_bytes (inj_bytes bl) = Some bl.
Proof.

Lemma inj_proj_bytes:
  forall cl bl, proj_bytes cl = Some bl -> cl = inj_bytes bl.
Proof.

Fixpoint inj_value_rec (n: nat) (v: val) (q: quantity) {struct n}: list memval :=
  match n with
  | O => nil
  | S m => Fragment v q m :: inj_value_rec m v q
  end.

Definition inj_value (q: quantity) (v: val): list memval :=
  inj_value_rec (size_quantity_nat q) v q.

Fixpoint check_value (n: nat) (v: val) (q: quantity) (vl: list memval)
                       {struct n} : bool :=
  match n, vl with
  | O, nil => true
  | S m, Fragment v' q' m' :: vl' =>
      Val.eq v v' && quantity_eq q q' && beq_nat m m' && check_value m v q vl'
  | _, _ => false
  end.

Definition proj_value (q: quantity) (vl: list memval) : val :=
  match vl with
  | Fragment v q' n :: vl' =>
      if check_value (size_quantity_nat q) v q vl then v else Vundef
  | _ => Vundef
  end.

Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
  match v, chunk with
  | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n))
  | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
  | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
  | Vptr b ofs, Mint32 => inj_value Q32 v
  | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
  | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n)))
  | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n)))
  | _, Many32 => inj_value Q32 v
  | _, Many64 => inj_value Q64 v
  | _, _ => list_repeat (size_chunk_nat chunk) Undef
  end.

Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
  match proj_bytes vl with
  | Some bl =>
      match chunk with
      | Mint8signed => Vint(Int.sign_ext 8 (Int.repr (decode_int bl)))
      | Mint8unsigned => Vint(Int.zero_ext 8 (Int.repr (decode_int bl)))
      | Mint16signed => Vint(Int.sign_ext 16 (Int.repr (decode_int bl)))
      | Mint16unsigned => Vint(Int.zero_ext 16 (Int.repr (decode_int bl)))
      | Mint32 => Vint(Int.repr(decode_int bl))
      | Mint64 => Vlong(Int64.repr(decode_int bl))
      | Mfloat32 => Vsingle(Float32.of_bits (Int.repr (decode_int bl)))
      | Mfloat64 => Vfloat(Float.of_bits (Int64.repr (decode_int bl)))
      | Many32 => Vundef
      | Many64 => Vundef
      end
  | None =>
      match chunk with
      | Mint32 | Many32 => Val.load_result chunk (proj_value Q32 vl)
      | Many64 => Val.load_result chunk (proj_value Q64 vl)
      | _ => Vundef
      end
  end.

Lemma encode_val_length:
  forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk.
Proof.

Lemma check_inj_value:
  forall v q n, check_value n v q (inj_value_rec n v q) = true.
Proof.

Lemma proj_inj_value:
  forall q v, proj_value q (inj_value q v) = v.
Proof.

Remark in_inj_value:
  forall mv v q, In mv (inj_value q v) -> exists n, mv = Fragment v q n.
Proof.

Lemma proj_inj_value_mismatch:
  forall q1 q2 v, q1 <> q2 -> proj_value q1 (inj_value q2 v) = Vundef.
Proof.

Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : Prop :=
  match v1, chunk1, chunk2 with
  | Vundef, _, _ => v2 = Vundef
  | Vint n, Mint8signed, Mint8signed => v2 = Vint(Int.sign_ext 8 n)
  | Vint n, Mint8unsigned, Mint8signed => v2 = Vint(Int.sign_ext 8 n)
  | Vint n, Mint8signed, Mint8unsigned => v2 = Vint(Int.zero_ext 8 n)
  | Vint n, Mint8unsigned, Mint8unsigned => v2 = Vint(Int.zero_ext 8 n)
  | Vint n, Mint16signed, Mint16signed => v2 = Vint(Int.sign_ext 16 n)
  | Vint n, Mint16unsigned, Mint16signed => v2 = Vint(Int.sign_ext 16 n)
  | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
  | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
  | Vint n, Mint32, Mint32 => v2 = Vint n
  | Vint n, Many32, (Mint32 | Many32) => v2 = Vint n
  | Vint n, Mint32, Mfloat32 => v2 = Vsingle(Float32.of_bits n)
  | Vint n, Many64, Many64 => v2 = Vint n
  | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Many64), _ => v2 = Vundef
  | Vint n, _, _ => True (* nothing meaningful to say about v2 *)
  | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = Vptr b ofs
  | Vptr b ofs, Many64, Many64 => v2 = Vptr b ofs
  | Vptr b ofs, _, _ => v2 = Vundef
  | Vlong n, Mint64, Mint64 => v2 = Vlong n
  | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.of_bits n)
  | Vlong n, Many64, Many64 => v2 = Vlong n
  | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Many32), _ => v2 = Vundef
  | Vlong n, _, _ => True (* nothing meaningful to say about v2 *)
  | Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f
  | Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.to_bits f)
  | Vfloat f, Many64, Many64 => v2 = Vfloat f
  | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mint64|Many32), _ => v2 = Vundef
  | Vfloat f, _, _ => True
  | Vsingle f, Mfloat32, Mfloat32 => v2 = Vsingle f
  | Vsingle f, Mfloat32, Mint32 => v2 = Vint(Float32.to_bits f)
  | Vsingle f, Many32, Many32 => v2 = Vsingle f
  | Vsingle f, Many64, Many64 => v2 = Vsingle f
  | Vsingle f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64|Mfloat64|Many64), _ => v2 = Vundef
  | Vsingle f, _, _ => True
  end.

Remark decode_val_undef:
  forall bl chunk, decode_val chunk (Undef :: bl) = Vundef.
Proof.

Remark proj_bytes_inj_value:
  forall q v, proj_bytes (inj_value q v) = None.
Proof.

Lemma decode_encode_val_general:
  forall v chunk1 chunk2,
  decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)).
Proof.

Lemma decode_encode_val_similar:
  forall v1 chunk1 chunk2 v2,
  type_of_chunk chunk1 = type_of_chunk chunk2 ->
  size_chunk chunk1 = size_chunk chunk2 ->
  decode_encode_val v1 chunk1 chunk2 v2 ->
  v2 = Val.load_result chunk2 v1.
Proof.

Lemma decode_val_type:
  forall chunk cl,
  Val.has_type (decode_val chunk cl) (type_of_chunk chunk).
Proof.

Lemma encode_val_int8_signed_unsigned:
  forall v, encode_val Mint8signed v = encode_val Mint8unsigned v.
Proof.

Lemma encode_val_int16_signed_unsigned:
  forall v, encode_val Mint16signed v = encode_val Mint16unsigned v.
Proof.

Lemma encode_val_int8_zero_ext:
  forall n, encode_val Mint8unsigned (Vint (Int.zero_ext 8 n)) = encode_val Mint8unsigned (Vint n).
Proof.

Lemma encode_val_int8_sign_ext:
  forall n, encode_val Mint8signed (Vint (Int.sign_ext 8 n)) = encode_val Mint8signed (Vint n).
Proof.

Lemma encode_val_int16_zero_ext:
  forall n, encode_val Mint16unsigned (Vint (Int.zero_ext 16 n)) = encode_val Mint16unsigned (Vint n).
Proof.

Lemma encode_val_int16_sign_ext:
  forall n, encode_val Mint16signed (Vint (Int.sign_ext 16 n)) = encode_val Mint16signed (Vint n).
Proof.

Lemma decode_val_cast:
  forall chunk l,
  let v := decode_val chunk l in
  match chunk with
  | Mint8signed => v = Val.sign_ext 8 v
  | Mint8unsigned => v = Val.zero_ext 8 v
  | Mint16signed => v = Val.sign_ext 16 v
  | Mint16unsigned => v = Val.zero_ext 16 v
  | _ => True
  end.
Proof.

Pointers cannot be forged.

Definition quantity_chunk (chunk: memory_chunk) :=
  match chunk with
  | Mint64 | Mfloat64 | Many64 => Q64
  | _ => Q32
  end.

Inductive shape_encoding (chunk: memory_chunk) (v: val): list memval -> Prop :=
  | shape_encoding_f: forall q i mvl,
      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
      q = quantity_chunk chunk ->
      S i = size_quantity_nat q ->
      (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) ->
      shape_encoding chunk v (Fragment v q i :: mvl)
  | shape_encoding_b: forall b mvl,
      match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end ->
      (forall mv, In mv mvl -> exists b', mv = Byte b') ->
      shape_encoding chunk v (Byte b :: mvl)
  | shape_encoding_u: forall mvl,
      (forall mv, In mv mvl -> mv = Undef) ->
      shape_encoding chunk v (Undef :: mvl).

Lemma encode_val_shape: forall chunk v, shape_encoding chunk v (encode_val chunk v).
Proof.

Inductive shape_decoding (chunk: memory_chunk): list memval -> val -> Prop :=
  | shape_decoding_f: forall v q i mvl,
      (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) ->
      q = quantity_chunk chunk ->
      S i = size_quantity_nat q ->
      (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) ->
      shape_decoding chunk (Fragment v q i :: mvl) (Val.load_result chunk v)
  | shape_decoding_b: forall b mvl v,
      match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end ->
      (forall mv, In mv mvl -> exists b', mv = Byte b') ->
      shape_decoding chunk (Byte b :: mvl) v
  | shape_decoding_u: forall mvl,
      shape_decoding chunk mvl Vundef.

Lemma decode_val_shape: forall chunk mv1 mvl,
  shape_decoding chunk (mv1 :: mvl) (decode_val chunk (mv1 :: mvl)).
Proof.

Compatibility with memory injections


Relating two memory values according to a memory injection.

Inductive memval_inject (f: meminj): memval -> memval -> Prop :=
  | memval_inject_byte:
      forall n, memval_inject f (Byte n) (Byte n)
  | memval_inject_frag:
      forall v1 v2 q n,
      Val.inject f v1 v2 ->
      memval_inject f (Fragment v1 q n) (Fragment v2 q n)
  | memval_inject_undef:
      forall mv, memval_inject f Undef mv.

Lemma memval_inject_incr:
  forall f f' v1 v2, memval_inject f v1 v2 -> inject_incr f f' -> memval_inject f' v1 v2.
Proof.

decode_val, applied to lists of memory values that are pairwise related by memval_inject, returns values that are related by Val.inject.

Lemma proj_bytes_inject:
  forall f vl vl',
  list_forall2 (memval_inject f) vl vl' ->
  forall bl,
  proj_bytes vl = Some bl ->
  proj_bytes vl' = Some bl.
Proof.

Lemma check_value_inject:
  forall f vl vl',
  list_forall2 (memval_inject f) vl vl' ->
  forall v v' q n,
  check_value n v q vl = true ->
  Val.inject f v v' -> v <> Vundef ->
  check_value n v' q vl' = true.
Proof.

Lemma proj_value_inject:
  forall f q vl1 vl2,
  list_forall2 (memval_inject f) vl1 vl2 ->
  Val.inject f (proj_value q vl1) (proj_value q vl2).
Proof.

Lemma proj_bytes_not_inject:
  forall f vl vl',
  list_forall2 (memval_inject f) vl vl' ->
  proj_bytes vl = None -> proj_bytes vl' <> None -> In Undef vl.
Proof.

Lemma check_value_undef:
  forall n q v vl,
  In Undef vl -> check_value n v q vl = false.
Proof.

Lemma proj_value_undef:
  forall q vl, In Undef vl -> proj_value q vl = Vundef.
Proof.

Theorem decode_val_inject:
  forall f vl1 vl2 chunk,
  list_forall2 (memval_inject f) vl1 vl2 ->
  Val.inject f (decode_val chunk vl1) (decode_val chunk vl2).
Proof.

Symmetrically, encode_val, applied to values related by Val.inject, returns lists of memory values that are pairwise related by memval_inject.

Lemma inj_bytes_inject:
  forall f bl, list_forall2 (memval_inject f) (inj_bytes bl) (inj_bytes bl).
Proof.

Lemma repeat_Undef_inject_any:
  forall f vl,
  list_forall2 (memval_inject f) (list_repeat (length vl) Undef) vl.
Proof.

Lemma repeat_Undef_inject_encode_val:
  forall f chunk v,
  list_forall2 (memval_inject f) (list_repeat (size_chunk_nat chunk) Undef) (encode_val chunk v).
Proof.

Lemma repeat_Undef_inject_self:
  forall f n,
  list_forall2 (memval_inject f) (list_repeat n Undef) (list_repeat n Undef).
Proof.

Lemma inj_value_inject:
  forall f v1 v2 q, Val.inject f v1 v2 -> list_forall2 (memval_inject f) (inj_value q v1) (inj_value q v2).
Proof.

Theorem encode_val_inject:
  forall f v1 v2 chunk,
  Val.inject f v1 v2 ->
  list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2).
Proof.

Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id.

Lemma memval_lessdef_refl:
  forall mv, memval_lessdef mv mv.
Proof.

memval_inject and compositions

Lemma memval_inject_compose:
  forall f f' v1 v2 v3,
  memval_inject f v1 v2 -> memval_inject f' v2 v3 ->
  memval_inject (compose_meminj f f') v1 v3.
Proof.

Breaking 64-bit memory accesses into two 32-bit accesses


Lemma int_of_bytes_append:
  forall l2 l1,
  int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z_of_nat (length l1) * 8).
Proof.

Lemma int_of_bytes_range:
  forall l, 0 <= int_of_bytes l < two_p (Z_of_nat (length l) * 8).
Proof.

Lemma length_proj_bytes:
  forall l b, proj_bytes l = Some b -> length b = length l.
Proof.

Lemma proj_bytes_append:
  forall l2 l1,
  proj_bytes (l1 ++ l2) =
  match proj_bytes l1, proj_bytes l2 with
  | Some b1, Some b2 => Some (b1 ++ b2)
  | _, _ => None
  end.
Proof.

Lemma decode_val_int64:
  forall l1 l2,
  length l1 = 4%nat -> length l2 = 4%nat ->
  Val.lessdef
    (decode_val Mint64 (l1 ++ l2))
    (Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2))
                     (decode_val Mint32 (if Archi.big_endian then l2 else l1))).
Proof.

Lemma bytes_of_int_append:
  forall n2 x2 n1 x1,
  0 <= x1 < two_p (Z_of_nat n1 * 8) ->
  bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z_of_nat n1 * 8)) =
  bytes_of_int n1 x1 ++ bytes_of_int n2 x2.
Proof.

Lemma bytes_of_int64:
  forall i,
  bytes_of_int 8 (Int64.unsigned i) =
  bytes_of_int 4 (Int.unsigned (Int64.loword i)) ++ bytes_of_int 4 (Int.unsigned (Int64.hiword i)).
Proof.

Lemma encode_val_int64:
  forall v,
  encode_val Mint64 v =
     encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v)
  ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v).
Proof.