Library memdata
The physical memory is modelled as a partial function mapping addresses
to abstract machine values. An address is a pair of memory blocks
and offsets. We use a positive number to represent the index number of
memory blocks, and offsets have the type of Z. 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 PtrByte(b,i,n), a special constan for the
NULL pointer, or the special constant UNDEF that represents uninitialized memory.
PtrByte(b,i,n) represents the n-th (0<= n <=3) byte for the 32-bit address
value (b,i). Our formalization for addresses and memory values are the
same as those in Compcert.
Memory blocks
Memory addresses
Definition of the values stored in each machine byte
It follows the similar definition used in CompCert.
Inductive memval : Set :=
| Undef : memval
| Byte : byte -> memval
| Pointer : block -> int32 -> nat -> memval
| MNull :memval.
Definition mvallist: Type := list memval.
Encoding and decoding integers
The following functions are used to convert
integers to the length-n byte list.
Open Local Scope Z_scope.
Fixpoint encode_int (n: nat) (x: Z) {struct n}: list byte :=
match n with
| O => nil
| S m => Byte.repr x :: encode_int m (x / 256)
end.
Fixpoint decode_int (l: list byte): Z :=
match l with
| nil => 0
| b :: l´ => Byte.unsigned b + decode_int l´ * 256
end.
Lemma encode_int_length:
forall sz x, length(encode_int sz x) = sz.
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.
Remark proj_inj_bytes:
forall bl, proj_bytes (inj_bytes bl) = Some bl.
Lemma inj_proj_bytes:
forall cl bl, proj_bytes cl = Some bl -> cl = inj_bytes bl.
Fixpoint inj_pointer (n: nat) (b: block) (ofs: int32) {struct n}: list memval :=
match n with
| O => nil
| S m => Pointer b ofs m :: inj_pointer m b ofs
end.
Fixpoint check_pointer (n: nat) (b: block) (ofs: int32) (vl: list memval)
{struct n} : bool :=
match n, vl with
| O, nil => true
| S m, Pointer b´ ofs´ m´ :: vl´ =>
peq b b´ && Int.eq_dec ofs ofs´ && beq_nat m m´ && check_pointer m b ofs vl´
| _, _ => false
end.
Definition addrval:=prod block int32.
Inductive val: Set :=
| Vundef: val
| Vnull : val
| Vint32 : int -> val
| Vptr : addrval -> val.
Definition proj_pointer (vl: list memval) : val :=
match vl with
| Pointer b ofs n :: vl´ =>
if check_pointer 4%nat b ofs vl then Vptr (b, ofs) else Vundef
| _ => Vundef
end.
Definition ident := Z.
We support 8 different types, including the type for NULL pointer,
the void type, the type of ``char'', the type of ``short'',
the type of ``int'', the type of ``pointers'', the type of ``array''
and the type of ``struct''. Following Clight, within a struct type,
the type "Tcom_ptr id" stands for a pointer type to the nearest
enclosing struct type named id.
Inductive type : Set :=
| Tnull
| Tvoid
| Tint8
| Tint16
| Tint32
| Tptr : type -> type
| Tcom_ptr : ident -> type
| Tarray : type -> nat -> type
| Tstruct : ident -> decllist -> type
with
decllist : Set:=
| dnil : decllist
| dcons : ident -> type -> decllist -> decllist.
Fixpoint typelen (t : type) : nat :=
match t with
| Tnull => 4 %nat
| Tvoid => 0 % nat
| Tint8 => 1 % nat
| Tint16 => 2 % nat
| Tint32 => 4 % nat
| Tptr _ => 4 % nat
| Tcom_ptr _ => 4 % nat
| Tarray t´ n => mult (typelen t´) n
| Tstruct _ dls => szstruct dls
end with szstruct (dls : decllist) {struct dls} : nat :=
match dls with
| dnil => O
| dcons _ t1 dls´ => plus (typelen t1) (szstruct dls´)
end.
Definition encode_val (t: type) (v: val) : list memval :=
match v, t with
| Vint32 n, Tint8 => inj_bytes (encode_int 1%nat (Int.unsigned n))
| Vint32 n, Tint16 => inj_bytes (encode_int 2%nat (Int.unsigned n))
| Vint32 n, Tint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
| Vptr (b, ofs), Tptr _ => inj_pointer 4%nat b (ofs)
| Vptr (b, ofs), Tcom_ptr _ => inj_pointer 4%nat b (ofs)
| Vnull, Tnull => list_repeat 4 MNull
| Vnull, Tptr _ => list_repeat 4 MNull
| Vnull, Tcom_ptr _ => list_repeat 4 MNull
| _, _ => list_repeat (typelen t) Undef
end.
Definition decode_val (t: type) (vl: list memval) : val :=
match proj_bytes vl with
| Some bl =>
match t with
| Tint8 => Vint32(Int.zero_ext 8 (Int.repr (decode_int bl)))
| Tint16 => Vint32(Int.zero_ext 16 (Int.repr (decode_int bl)))
| Tint32 => Vint32(Int.repr(decode_int bl))
| _ => Vundef
end
| None =>
match vl with
| MNull :: MNull ::MNull :: MNull :: nil=> match t with
| Tnull => Vnull
| Tptr _ => Vnull
| Tcom_ptr _ => Vnull
| _ => Vundef
end
| _ =>
match t with
| Tptr _ => proj_pointer vl
| Tcom_ptr _ => proj_pointer vl
| _ => Vundef
end
end
end.
Lemma encode_val_length:
forall t v, length(encode_val t v) = typelen t.