Types
The formal model is intended to represent programs after
they have already been compiled to a fairly low level intermediate
representation in which all code and data structures have been
flattened and all operations are expressed in terms of atomic data
types. Atomic types AType are integers or pointers to
pointer types PType, which include anonymous structure types Struct,
named structures and void in addition to atomic types. We
define an anonymous structure type Struct as a list of identifiers with
atomic types. We assume that we have a partial map typeTable from names to
anonymous structure types that represents typedef in the source code.
Here, c_ident ranges over C identifiers.
Definition c_ident := nat.
Inductive AType : Set :=
| A_Int: AType
| A_Pointer: PType -> AType
with Struct : Set :=
| S_Nil : Struct
| S_Cons : c_ident -> AType -> Struct -> Struct
with PType : Set :=
| P_AType : AType -> PType
| P_Struct : Struct -> PType
| P_Name : c_ident -> PType
| P_VoidPtr: PType.
Parameter typeTable : c_ident -> option Struct.
Definition isPtr (t: AType) : Prop :=
match t with
| A_Pointer _ => True
| _=> False
end.
Atomic types are always of size one, which is the minimial granularity in
our memory system. The size of an anonymous structure type is the number of
its fields. However, the size of a pointer type is a partial function, which
fails if typeTable doesn't know the name of a named structure.
Fixpoint sizeOfAType (t : AType) : nat :=
match t with
| A_Int => 1
| A_Pointer _ => 1
end.
Fixpoint sizeOfStruct (s : Struct) : nat :=
match s with
| S_Nil => 0
| S_Cons _ t s' => sizeOfStruct s' + sizeOfAType t
end.
Definition sizeOfPType (p : PType) : option nat :=
match p with
| P_AType t => Some (sizeOfAType t)
| P_Struct s => Some (sizeOfStruct s)
| P_Name n =>
match (typeTable n) with
| Some s => Some (sizeOfStruct s)
| None => None
end
| P_VoidPtr => Some 1
end.
Given an identifier, we can get its offset and atomic type if it is
a field of a structure.
Fixpoint getStructOffset (s : Struct) (id : c_ident) {struct s}: option nat :=
match s with
| S_Nil => None
| S_Cons i t s' =>
if (beq_nat i id)
then
Some 0
else
match (getStructOffset s' id) with
| Some n => Some (n + sizeOfAType t)
| None => None
end
end.
Fixpoint getStructType (s : Struct) (id : c_ident) {struct s}: option AType :=
match s with
| S_Nil => None
| S_Cons i t s' =>
if (beq_nat i id)
then
Some t
else
getStructType s' id
end.
The well-formedness |- a, |- s, and |-p for atomic types wf_Atype, anonymous structure types
wf_Struct, and pointer types wf_PType are defined mutually. Most of the
cases are straightward. At case wf_P_Name, a named structure is well-formed
if the name is stored in the table typeTable with a well-formed anonymous
structure type.
Inductive wf_AType : AType -> Prop :=
| wf_A_Int: wf_AType A_Int
| wf_A_TamePointer: forall p,
wf_PType p ->
wf_AType (A_Pointer p)
with wf_Struct : Struct -> Prop :=
| wf_S_Nil : wf_Struct S_Nil
| wf_S_Cons : forall id t s,
wf_AType t -> wf_Struct s -> wf_Struct (S_Cons id t s)
with wf_PType : PType -> Prop :=
| wf_P_AType : forall t,
wf_AType t ->
wf_PType (P_AType t)
| wf_P_Struct: forall s,
wf_Struct s -> wf_PType (P_Struct s)
| wf_P_Name: forall n s,
typeTable n = Some s ->
wf_Struct s ->
wf_PType (P_Name n)
| wf_P_VoidPtr: wf_PType P_VoidPtr.