Syntax



The section gives the fragment of C used in our proof. Commands c_cmd consist of empty commands C_Skip, straight-line sequence of commands C_Seq, assignments C_Assign, free C_Free, and function calls C_Call. Functions calls declare local variables, but have no arguments or results. We also assume that there is a partial map funTable from function names to function definitions generated by the compiler. A function definition includes a frame which consists of local variables, and a sequence of commands.

Assignments update the memory pointed by left-hand-side c_lhs by right-hand-side c_rhs. The left-hand-side of an assignment is either a variable C_Var, a pointer dereference C_Deref, or the field of an anonymous struct C_StructPos, or the field of a named struct C_NamePos. The right-hand-side of an assignment can be an integer constant C_Cons, a left-hand-side C_Lhs, the address of a left-hand-side C_Ref, the result of an arithmetic operation C_Add, the result of a cast C_Cast, the size of a pointer type C_Size, or the result of malloc C_Alloc. We assume that the compiler generates some type information which is useful for the proofs. For example, we need to know the result type (pointer types) of the address-of and malloc.

Because the syntax only includes a simple function call that does not have inputs and return results, we explicitly define malloc as a right-hand-side C_Alloc, and free as a C_Free.

Inductive c_lhs : Set :=
  | C_Var : Var -> c_lhs
  | C_Deref : c_lhs -> c_lhs
  | C_StructPos : c_lhs -> c_ident -> c_lhs
  | C_NamePos : c_lhs -> c_ident -> c_lhs
  .

Inductive c_rhs : Set :=
  | C_Const : nat -> c_rhs
  | C_Lhs : c_lhs -> c_rhs
  | C_Ref : PType -> c_lhs -> c_rhs
  | C_Add : c_rhs -> c_rhs -> c_rhs
  | C_Cast : AType -> c_rhs -> c_rhs
  | C_Size : PType -> c_rhs
  | C_Alloc : PType -> c_rhs -> c_rhs
  .

Inductive c_cmd : Set :=
  | C_Skip : c_cmd
  | C_Seq : c_cmd -> c_cmd -> c_cmd
  | C_Assign : c_lhs -> c_rhs -> c_cmd
  | C_Free : c_lhs -> c_cmd
  | C_Call : c_ident -> c_cmd
  .

Parameter funTable : c_ident -> option (frame * c_cmd).

Our Coq proof defines a well-formedness predicate on syntax that picks out a subset of programs with these invariants.

Global, frame |-l c_lhs : AType defines a well-formed left-hand-side that ensures that each variable in a left-hand-side c_lhs has an atomic type AType assigned by global variables Global, or stack frames frame.

A global variable x is with type a if it is not defined in the local stack frame, globals maps x into a well-formed type a.
     fr(x) = None
     G(x) = (loc, a)
     |- a
    ----------------- :: WF_GVar
     G, fr |-l x: a
A local variable x is with type a if it is defined in the stack frame with a well formed type t.
     fr(x) = a
     |- a
    ----------------- :: WF_SVar
     G, fr |-l x: a
A pointer derefence *lhs is of type a if lhs is of type a*.
     G, fr |-l lhs: a*
     ---------------- :: WF_Deref
     G, fr |-l *lhs: a
A field of an anonymous struct, lhs->id is of type a' if lhs is a pointer to an anonymous struct s, and s maps id to the type a'.
     G, fr |-l lhs: s*
     getStructType(s, id) = a'
    --------------------------------- :: WF_StructPos
     G, fr |-l lhs->id: a'
A field of a named struct, lhs->id is of type a' if lhs is a pointer to a named struct n, typeTable maps n to an anonymous struct s, and s maps id to the type a'.
     G, fr |-l lhs: n*
     typeTable n = s
     getStructType(s, id) = a'
    --------------------------------- :: WF_NamePos
     G, fr |-l lhs->id: a'
Inductive wf_lhs : Global -> frame -> c_lhs -> AType -> Prop :=
  | WF_GVar : forall G f (v: Var) l t,
     f v = None ->
     lookUpGlobal G v = Some (l, t) ->
     wf_AType t ->
     wf_lhs G f (C_Var v) t
  | WF_SVar : forall G f (v: Var) t,
     f v = Some t ->
     wf_AType t ->
     wf_lhs G f (C_Var v) t
  | WF_Deref : forall G f lhs t,
     wf_lhs G f lhs (A_Pointer (P_AType t)) ->
     wf_lhs G f (C_Deref lhs) t
  | WF_StructPos : forall G f lhs id s t',
     wf_lhs G f lhs (A_Pointer (P_Struct s)) ->
     getStructType s id = Some t' ->
     wf_lhs G f (C_StructPos lhs id) t'
  | WF_NamePos : forall G f lhs id n s t',
     wf_lhs G f lhs (A_Pointer (P_Name n)) ->
     typeTable n = Some s ->
     getStructType s id = Some t' ->
     wf_lhs G f (C_NamePos lhs id) t'
  .

Global, frame |-r c_rhs : AType defines a well-formed right-hand-side that ensures that each variable in a right-hand-side c_rhs has an atomic type AType assigned by global variables Global, or stack frames frame.

First of all, integer constants are always of type int.
   ---------------- :: WF_Const
    G, fr |-r n: int
If this right-hand-side is derived from a left-hand-side, it is well-formed when the left-hand-side is well-formed.
    G, fr |-l lhs: a
    ------------ :: WF_Lhs
    G, fr |-r lhs: a
An address of a left-hand-side, &lhs is of type a* if a* is well-formed, and lhs is with type a.
    G, fr |-l lhs: a
    |- a*
    ----------------------- :: WF_Ref
    G, fr |-r (a* )&lhs: a*
We consider two kinds of additions: integer additions and pointer arithmetics.
    G, fr |-r rhs1: int
    G, fr |-r rhs2: int
    ------------------ :: WF_Add_Int_Int
    G, fr |-r rhs1+hsr2 : int

    G, fr |-r rhs1: a*
    G, fr |-r rhs2: int
    ------------------ :: WF_Add_Ptr_Int
    G, fr |-r rhs1+rhs2: a*
A cast, (a')rhs, is well-formed if both rhs and the type a' are well-formed.
    G, fr |-r rhs:  a
    |- a'
    ------------------ :: WF_Cast
    G, fr |-r (a')rhs: a'
The size of a well-formed pointer type is also a well-formed right-hand-side.
    |- p
    -------------------- :: WF_Size
    G |-r sizeof(p): int 
malloc must allocate memory with positive size, and return a well-formed pointer type. The size to allocate, rhs, is also well-formed.
    G |-r rhs: int
    |- p
    sizeOfPType p = Some size
    size > 0
    ----------------------------- :: WF_Alloc
    G |-r (p* )malloc(rhs) : p*
Inductive wf_rhs : Global -> frame -> c_rhs -> AType -> Prop :=
  | WF_Const : forall G f n,
     wf_rhs G f (C_Const n) A_Int
  | WF_Lhs : forall G f lhs t,
     wf_lhs G f lhs t ->
     wf_rhs G f (C_Lhs lhs) t
  | WF_Ref : forall G f lhs t,
     wf_lhs G f lhs t->
     wf_AType (A_Pointer (P_AType t)) ->
     wf_rhs G f (C_Ref (P_AType t)lhs) (A_Pointer (P_AType t))
  | WF_Add_Int_Int : forall G f rhs1 rhs2,
     wf_rhs G f rhs1 A_Int ->
     wf_rhs G f rhs2 A_Int ->
     wf_rhs G f (C_Add rhs1 rhs2) A_Int
  | WF_Add_Ptr_Int : forall G f rhs1 rhs2 p,
     wf_rhs G f rhs1 (A_Pointer p) ->
     wf_rhs G f rhs2 A_Int ->
     wf_AType (A_Pointer p) ->
     wf_rhs G f (C_Add rhs1 rhs2) (A_Pointer p)
  | WF_Cast : forall G f rhs t t',
     wf_rhs G f rhs t ->
     wf_AType t' ->
     wf_rhs G f (C_Cast t' rhs) t'
  | WF_Size : forall G f t,
     wf_PType t ->
     wf_rhs G f (C_Size t) A_Int
  | WF_Alloc : forall G f rhs p size,
    wf_rhs G f rhs A_Int ->
    wf_AType (A_Pointer p) ->
    sizeOfPType p = Some size ->
    size > 0 ->
    wf_rhs G f (C_Alloc p rhs) (A_Pointer p)
  .

Global, frame |-c c_cmd defines a well-formed command that ensures that each variable in a command c_cmd has an atomic type AType assigned by global variables Global, or stack frames frame.

Empty commands are trivially well-formed.
    ----------- :: Wf_Skip
    G, fr |-c skip
A sequence of commands is well-formed if each command is well-formed.
    G, fr |-c c1
    G, fr |-c c2
    ---------------- :: Wf_Seq
    G, fr |-c c1;c2
Given an assignment, we check if the left-hand-side and the right-hand-side are well-formed.
    G, fr |-l lhs: a
    G, fr |-r rhs: a'
    -------------------- :: WF_Assign
    G, fr |-c lhs = rhs
free must deallocate a well-formed left-hand-side with pointer types.
    G, fr |-l lhs : p*
    -------------------- :: WF_Free
    G, fr |-c free lhs 
To check a function call, we ensure that the function has been stored in funTable with a local frame fr' and commands c', then check if c' is well-formed w.r.t G and fr'.
    funTable f = (fr', c')
    G, fr' |-c c'
    ----------------------- :: WF_Call
    G, fr |-c f
Inductive wf_cmd : Global -> frame -> c_cmd -> Prop :=
  | WF_Skip : forall G f,
    wf_cmd G f (C_Skip)
  | WF_Seq : forall G f c1 c2,
    wf_cmd G f c1 ->
    wf_cmd G f c2 ->
    wf_cmd G f (C_Seq c1 c2)
  | WF_Assign : forall G f lhs rhs tl tr,
    wf_lhs G f lhs tl ->
    wf_rhs G f rhs tr ->
    wf_cmd G f (C_Assign lhs rhs)
  | WF_Free : forall G f lhs p,
    wf_lhs G f lhs (A_Pointer p) ->
    wf_cmd G f (C_Free lhs)
  | WF_Call : forall G n f f' c',
    funTable n = Some (f', c') ->
    wf_cmd G f' c' ->
    wf_cmd G f (C_Call n)
  .