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

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

Fixpoint sizeOfStruct (s : Struct) : nat :=
  match s with
  | S_Nil => 0
  | S_Cons _ t s' => sizeOfStruct s' + sizeOfAType t

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
  | P_VoidPtr => Some 1

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)
      Some 0
      match (getStructOffset s' id) with
      | Some n => Some (n + sizeOfAType t)
      | None => None

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)
      Some t
      getStructType s' id

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.