(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(* * Abstract syntax for the Clight language *)

(*include "Integers.ma".*)
include "common/AST.ma".
include "utilities/Coqlib.ma".
include "common/Errors.ma".
include "common/CostLabel.ma".

(* * * Abstract syntax *)

(* * ** Types *)

(* * The syntax of type expressions.  Some points to note:
- Array types [Tarray n] carry the size [n] of the array.
  Arrays with unknown sizes are represented by pointer types.
- Function types [Tfunction targs tres] specify the number and types
  of the function arguments (list [targs]), and the type of the
  function result ([tres]).  Variadic functions and old-style unprototyped
  functions are not supported.
- In C, struct and union types are named and compared by name.
  This enables the definition of recursive struct types such as
<<
  struct s1 { int n; struct * s1 next; };
>>
  Note that recursion within types must go through a pointer type.
  For instance, the following is not allowed in C.
<<
  struct s2 { int n; struct s2 next; };
>>
  In Clight, struct and union types [Tstruct id fields] and
  [Tunion id fields] are compared by structure: the [fields]
  argument gives the names and types of the members.  The identifier
  [id] is a local name which can be used in conjuction with the
  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr rg id]
  stands for a pointer type to the nearest enclosing [Tstruct]
  or [Tunion] type named [id] in memory region [rg].  For instance.
  the structure [s1] defined above in C is expressed by
<<
  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
               (Fcons "next" (Tcomp_ptr Any "id")
               Fnil))
>>
  Note that the incorrect structure [s2] above cannot be expressed at
  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
  structure or union, but not to the structure or union directly.
*)

inductive type : Type[0] ≝
  | Tvoid: type                         (**r the [void] type *)
  | Tint: intsize → signedness → type   (**r integer types *)
  | Tfloat: floatsize → type            (**r floating-point types *)
  | Tpointer: region → type → type      (**r pointer types ([*ty]) *)
  | Tarray: region → type → nat → type  (**r array types ([ty[len]]) *)
  | Tfunction: typelist → type → type   (**r function types *)
  | Tstruct: ident → fieldlist → type   (**r struct types *)
  | Tunion: ident → fieldlist → type    (**r union types *)
  | Tcomp_ptr: region → ident → type    (**r pointer to named struct or union *)

with typelist : Type[0] ≝
  | Tnil: typelist
  | Tcons: type → typelist → typelist

with fieldlist : Type[0] ≝
  | Fnil: fieldlist
  | Fcons: ident → type → fieldlist → fieldlist.

(* XXX: no induction scheme! *)
let rec type_ind
  (P:type → Prop)
  (vo:P Tvoid)
  (it:∀i,s. P (Tint i s))
  (fl:∀f. P (Tfloat f))
  (pt:∀s,t. P t → P (Tpointer s t))
  (ar:∀s,t,n. P t → P (Tarray s t n))
  (fn:∀tl,t. P t → P (Tfunction tl t))
  (st:∀i,fl. P (Tstruct i fl))
  (un:∀i,fl. P (Tunion i fl))
  (cp:∀rg,i. P (Tcomp_ptr rg i))
  (t:type) on t : P t ≝
  match t return λt'.P t' with
  [ Tvoid ⇒ vo
  | Tint i s ⇒ it i s
  | Tfloat s ⇒ fl s
  | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
  | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
  | Tstruct i fs ⇒ st i fs
  | Tunion i fs ⇒ un i fs
  | Tcomp_ptr rg i ⇒ cp rg i
  ].
  
let rec fieldlist_ind
  (P:fieldlist → Prop)
  (nl:P Fnil)
  (cs:∀i,t,fs. P fs → P (Fcons i t fs))
  (fs:fieldlist) on fs : P fs ≝
  match fs with
  [ Fnil ⇒ nl
  | Fcons i t fs' ⇒ cs i t fs' (fieldlist_ind P nl cs fs')
  ].

(* * ** Expressions *)

(* * Arithmetic and logical operators. *)

inductive unary_operation : Type[0] ≝
  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
  | Oneg : unary_operation.             (**r opposite (unary [-]) *)

inductive binary_operation : Type[0] ≝
  | Oadd : binary_operation             (**r addition (binary [+]) *)
  | Osub : binary_operation             (**r subtraction (binary [-]) *)
  | Omul : binary_operation             (**r multiplication (binary [*]) *)
  | Odiv : binary_operation             (**r division ([/]) *)
  | Omod : binary_operation             (**r remainder ([%]) *)
  | Oand : binary_operation             (**r bitwise and ([&]) *)
  | Oor : binary_operation              (**r bitwise or ([|]) *)
  | Oxor : binary_operation             (**r bitwise xor ([^]) *)
  | Oshl : binary_operation             (**r left shift ([<<]) *)
  | Oshr : binary_operation             (**r right shift ([>>]) *)
  | Oeq: binary_operation               (**r comparison ([==]) *)
  | One: binary_operation               (**r comparison ([!=]) *)
  | Olt: binary_operation               (**r comparison ([<]) *)
  | Ogt: binary_operation               (**r comparison ([>]) *)
  | Ole: binary_operation               (**r comparison ([<=]) *)
  | Oge: binary_operation.              (**r comparison ([>=]) *)

(* * Clight expressions are a large subset of those of C.
  The main omissions are string literals and assignment operators
  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
  not an expression.  

  All expressions are annotated with their types.  An expression
  (type [expr]) is therefore a pair of a type and an expression
  description (type [expr_descr]).
*)

inductive expr : Type[0] ≝
  | Expr: expr_descr → type → expr

with expr_descr : Type[0] ≝
  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
  | Econst_float: float → expr_descr   (**r float literal *)
  | Evar: ident → expr_descr           (**r variable *)
  | Ederef: expr → expr_descr          (**r pointer dereference (unary [*]) *)
  | Eaddrof: expr → expr_descr         (**r address-of operator ([&]) *)
  | Eunop: unary_operation → expr → expr_descr  (**r unary operation *)
  | Ebinop: binary_operation → expr → expr → expr_descr (**r binary operation *)
  | Ecast: type → expr → expr_descr    (**r type cast ([(ty) e]) *)
  | Econdition: expr → expr → expr → expr_descr (**r conditional ([e1 ? e2 : e3]) *)
  | Eandbool: expr → expr → expr_descr (**r sequential and ([&&]) *)
  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
  | Esizeof: type → expr_descr         (**r size of a type *)
  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
  | Ecost: costlabel → expr → expr_descr.




(* * Extract the type part of a type-annotated Clight expression. *)

definition typeof : expr → type ≝ λe.
  match e with [ Expr de te ⇒ te ].

(* * ** Statements *)

(* * Clight statements include all C statements.
  Only structured forms of [switch] are supported; moreover,
  the [default] case must occur last.  Blocks and block-scoped declarations
  are not supported. *)

definition label ≝ ident.

inductive statement : Type[0] ≝
  | Sskip : statement                   (**r do nothing *)
  | Sassign : expr → expr → statement   (**r assignment [lvalue = rvalue] *)
  | Scall: option expr → expr → list expr → statement (**r function call *)
  | Ssequence : statement → statement → statement  (**r sequence *)
  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
  | Swhile : expr → statement → statement   (**r [while] loop *)
  | Sdowhile : expr → statement → statement (**r [do] loop *)
  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
  | Sbreak : statement                      (**r [break] statement *)
  | Scontinue : statement                   (**r [continue] statement *)
  | Sreturn : option expr → statement       (**r [return] statement *)
  | Sswitch : expr → labeled_statements → statement  (**r [switch] statement *)
  | Slabel : label → statement → statement
  | Sgoto : label → statement
  | Scost : costlabel → statement → statement

with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
  | LSdefault: statement → labeled_statements
  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.

let rec statement_ind2
  (P:statement → Prop) (Q:labeled_statements → Prop)
  (Ssk:P Sskip)
  (Sas:∀e1,e2. P (Sassign e1 e2))
  (Sca:∀eo,e,args. P (Scall eo e args))
  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
  (Swh:∀e,s. P s → P (Swhile e s))
  (Sdo:∀e,s. P s → P (Sdowhile e s))
  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
  (Sbr:P Sbreak)
  (Sco:P Scontinue)
  (Sre:∀eo. P (Sreturn eo))
  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
  (Sla:∀l,s. P s → P (Slabel l s))
  (Sgo:∀l. P (Sgoto l))
  (Scs:∀l,s. P s → P (Scost l s))
  (LSd:∀s. P s → Q (LSdefault s))
  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
  (s:statement) on s : P s ≝
match s with
[ Sskip ⇒ Ssk
| Sassign e1 e2 ⇒ Sas e1 e2
| Scall eo e args ⇒ Sca eo e args
| Ssequence s1 s2 ⇒ Ssq s1 s2
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
| Swhile e s ⇒ Swh e s
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| Sdowhile e s ⇒ Sdo e s
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
| Sbreak ⇒ Sbr
| Scontinue ⇒ Sco
| Sreturn eo ⇒ Sre eo
| Sswitch e ls ⇒ Ssw e ls
    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
| Slabel l s ⇒ Sla l s
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| Sgoto l ⇒ Sgo l
| Scost l s ⇒ Scs l s
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
]
and labeled_statements_ind2
  (P:statement → Prop) (Q:labeled_statements → Prop)
  (Ssk:P Sskip)
  (Sas:∀e1,e2. P (Sassign e1 e2))
  (Sca:∀eo,e,args. P (Scall eo e args))
  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
  (Swh:∀e,s. P s → P (Swhile e s))
  (Sdo:∀e,s. P s → P (Sdowhile e s))
  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
  (Sbr:P Sbreak)
  (Sco:P Scontinue)
  (Sre:∀eo. P (Sreturn eo))
  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
  (Sla:∀l,s. P s → P (Slabel l s))
  (Sgo:∀l. P (Sgoto l))
  (Scs:∀l,s. P s → P (Scost l s))
  (LSd:∀s. P s → Q (LSdefault s))
  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
  (ls:labeled_statements) on ls : Q ls ≝
match ls with
[ LSdefault s ⇒ LSd s
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
| LScase sz i s t ⇒ LSc sz i s t
    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
].

definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
  (λ_,_. I) (λ_,_,_,_,_,_.I).

(* * ** Functions *)

(* * A function definition is composed of its return type ([fn_return]),
  the names and types of its parameters ([fn_params]), the names
  and types of its local variables ([fn_vars]), and the body of the
  function (a statement, [fn_body]). *)

record function : Type[0] ≝ {
  fn_return: type;
  fn_params: list (ident × type);
  fn_vars: list (ident × type);
  fn_body: statement
}.

(* * Functions can either be defined ([CL_Internal]) or declared as
  external functions ([CL_External]).  Similar to the AST definition, but
  with high level type information for external functions. *)

inductive clight_fundef : Type[0] ≝
  | CL_Internal: function → clight_fundef
  | CL_External: ident → typelist → type → clight_fundef.

(* * ** Programs *)

(* * A program is a collection of named functions, plus a collection
  of named global variables, carrying their types and optional initialization 
  data.  See module [AST] for more details. *)

definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).

(* * * Operations over types *)

(* * The type of a function definition. *)

let rec type_of_params (params: list (ident × type)) : typelist ≝
  match params with
  [ nil ⇒ Tnil
  | cons h rem ⇒ let 〈id,ty〉 ≝ h in Tcons ty (type_of_params rem)
  ].

definition type_of_function : function → type ≝ λf.
  Tfunction (type_of_params (fn_params f)) (fn_return f).

definition type_of_fundef : clight_fundef → type ≝ λf.
  match f with
  [ CL_Internal fd ⇒ type_of_function fd
  | CL_External id args res ⇒ Tfunction args res
  ].

(* * Natural alignment of a type, in bytes. *)
(* FIXME: these are old values for 32 bit machines *)
let rec alignof (t: type) : nat ≝
  match t with
  [ Tvoid ⇒ 1
  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
  | Tpointer _ _ ⇒ 4
  | Tarray _ t' n ⇒ alignof t'
  | Tfunction _ _ ⇒ 1
  | Tstruct _ fld ⇒ alignof_fields fld
  | Tunion _ fld ⇒ alignof_fields fld
  | Tcomp_ptr _ _ ⇒ 4
  ]

and alignof_fields (f: fieldlist) : nat ≝
  match f with
  [ Fnil ⇒ 1
  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
  ].

(*
Scheme type_ind2 := Induction for type Sort Prop
  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
*)

(* XXX: automatic generation? *)
let rec type_ind2
  (P:type → Prop) (Q:fieldlist → Prop)
  (vo:P Tvoid)
  (it:∀i,s. P (Tint i s))
  (fl:∀f. P (Tfloat f))
  (pt:∀s,t. P t → P (Tpointer s t))
  (ar:∀s,t,n. P t → P (Tarray s t n))
  (fn:∀tl,t. P t → P (Tfunction tl t))
  (st:∀i,fl. Q fl → P (Tstruct i fl))
  (un:∀i,fl. Q fl → P (Tunion i fl))
  (cp:∀r,i. P (Tcomp_ptr r i))
  (nl:Q Fnil)
  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
 (t:type) on t : P t ≝
  match t return λt'.P t' with
  [ Tvoid ⇒ vo
  | Tint i s ⇒ it i s
  | Tfloat s ⇒ fl s
  | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
  | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
  | Tcomp_ptr r i ⇒ cp r i
  ]
and fieldlist_ind2
  (P:type → Prop) (Q:fieldlist → Prop)
  (vo:P Tvoid)
  (it:∀i,s. P (Tint i s))
  (fl:∀f. P (Tfloat f))
  (pt:∀s,t. P t → P (Tpointer s t))
  (ar:∀s,t,n. P t → P (Tarray s t n))
  (fn:∀tl,t. P t → P (Tfunction tl t))
  (st:∀i,fl. Q fl → P (Tstruct i fl))
  (un:∀i,fl. Q fl → P (Tunion i fl))
  (cp:∀r,i. P (Tcomp_ptr r i))
  (nl:Q Fnil)
  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
  (fs:fieldlist) on fs : Q fs ≝
  match fs return λfs'.Q fs' with
  [ Fnil ⇒ nl
  | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t)
                        (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs f')
  ].

lemma alignof_fields_pos:
  ∀f. alignof_fields f > 0.
@fieldlist_ind //;
#i #t #fs' #IH @max_r @IH qed. 

lemma alignof_pos:
  ∀t. alignof t > 0.
#t elim t; normalize; //;
[ 1,2: #z cases z; /2/;
| 3,4: #i @alignof_fields_pos
] qed.

(* * Size of a type, in bytes. *)

let rec sizeof (t: type) : nat ≝
  match t with
  [ Tvoid ⇒ 1
  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
  | Tpointer r _ ⇒ size_pointer r
  | Tarray _ t' n ⇒ sizeof t' * max 1 n
  | Tfunction _ _ ⇒ 1
  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
  | Tcomp_ptr r _ ⇒ size_pointer r
  ]

and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat ≝
  match fld with
  [ Fnil ⇒ pos
  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
  ]

and sizeof_union (fld: fieldlist) : nat ≝
  match fld with
  [ Fnil ⇒ 0
  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
  ].
(* TODO: needs some Z_times results
lemma sizeof_pos:
  ∀t. sizeof t > 0.
#t0
napply (type_ind2 (λt. sizeof t > 0)
                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
[ 1,4,6,9: //;
| #i cases i;#s //;
| #f cases f;//
| #t #n #H whd in ⊢ (?%?);
Proof.
  intro t0.
  apply (type_ind2 (fun t => sizeof t > 0)
                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
  intros; simpl; auto; try omega.
  destruct i; omega.
  destruct f; omega.
  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
  destruct H. 
  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)). 
  generalize (Zmax1 1 (sizeof_struct f 0)). omega. 
  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)). 
  generalize (Zmax1 1 (sizeof_union f)). omega. 
  split. omega. auto.
  destruct H0. split; intros.
  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
  apply H1. 
  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
Qed.

Lemma sizeof_struct_incr:
  forall fld pos, pos <= sizeof_struct fld pos.
Proof.
  induction fld; intros; simpl. omega. 
  eapply Zle_trans. 2: apply IHfld.
  apply Zle_trans with (align pos (alignof t)). 
  apply align_le. apply alignof_pos. 
  assert (sizeof t > 0) by apply sizeof_pos. omega.
Qed.

(** Byte offset for a field in a struct or union.
  Field are laid out consecutively, and padding is inserted
  to align each field to the natural alignment for its type. *)

Open Local Scope string_scope.
*)
axiom UnknownField : String.

let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
                              on fld : res nat ≝
  match fld with
  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
  | Fcons id' t fld' ⇒
      match ident_eq id id' with
      [ inl _ ⇒ OK ? (align pos (alignof t))
      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
      ]
  ].

definition field_offset ≝ λid: ident. λfld: fieldlist.
  field_offset_rec id fld 0.

let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
  match fld with
  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
  ].

(* * Some sanity checks about field offsets.  First, field offsets are 
  within the range of acceptable offsets. *)
(*
Remark field_offset_rec_in_range:
  forall id ofs ty fld pos,
  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
Proof.
  intros until ty. induction fld; simpl.
  congruence.
  destruct (ident_eq id i); intros.
  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
  exploit IHfld; eauto. intros [A B]. split; auto. 
  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega. 
Qed.

Lemma field_offset_in_range:
  forall id fld ofs ty,
  field_offset id fld = OK ofs → field_type id fld = OK ty →
  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
Proof.
  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
Qed.

(** Second, two distinct fields do not overlap *)

Lemma field_offset_no_overlap:
  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
  id1 <> id2 →
  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
Proof.
  intros until ty2. intros fld0 A B C D NEQ.
  assert (forall fld pos,
  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
  induction fld; intro pos; simpl. congruence.
  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
  congruence. 
  subst i. intros. inv H; inv H0.
  exploit field_offset_rec_in_range. eexact H1. eauto. tauto.  
  subst i. intros. inv H1; inv H2.
  exploit field_offset_rec_in_range. eexact H. eauto. tauto. 
  intros. eapply IHfld; eauto.

  apply H with fld0 0; auto.
Qed.

(** Third, if a struct is a prefix of another, the offsets of fields
  in common is the same. *)

Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
  match fld1 with
  | Fnil ⇒ fld2
  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
  end.

Lemma field_offset_prefix:
  forall id ofs fld2 fld1,
  field_offset id fld1 = OK ofs →
  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
Proof.
  intros until fld2.
  assert (forall fld1 pos, 
    field_offset_rec id fld1 pos = OK ofs ->
    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
  induction fld1; intros pos; simpl. congruence.
  destruct (ident_eq id i); auto.
  intros. unfold field_offset; auto. 
Qed.
*)
(* * The [access_mode] function describes how a variable of the given
type must be accessed:
- [By_value ch]: access by value, i.e. by loading from the address
  of the variable using the memory chunk [ch];
- [By_reference]: access by reference, i.e. by just returning
  the address of the variable;
- [By_nothing]: no access is possible, e.g. for the [void] type.

We currently do not support 64-bit integers and 128-bit floats, so these
have an access mode of [By_nothing].
*)

inductive mode: Type[0] ≝
  | By_value: memory_chunk → mode
  | By_reference: region → mode
  | By_nothing: mode.

definition access_mode : type → mode ≝ λty.
  match ty with
  [ Tint i s ⇒
    match i with [ I8 ⇒
      match s with [ Signed ⇒ By_value Mint8signed
                   | Unsigned ⇒ By_value Mint8unsigned ]
                 | I16 ⇒
      match s with [ Signed ⇒ By_value Mint16signed
                   | Unsigned ⇒ By_value Mint16unsigned ]
                 | I32 ⇒ By_value Mint32 ]
  | Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32
                            | F64 ⇒ By_value Mfloat64 ]
  | Tvoid ⇒ By_nothing
  | Tpointer r _ ⇒ By_value (Mpointer r)
  | Tarray r _ _ ⇒ By_reference r
  | Tfunction _ _ ⇒ By_reference Code
  | Tstruct _ fList ⇒ By_nothing
  | Tunion _ fList ⇒ By_nothing
  | Tcomp_ptr r _ ⇒ By_value (Mpointer r)
  ].

(* * Classification of arithmetic operations and comparisons.
  The following [classify_] functions take as arguments the types
  of the arguments of an operation.  They return enough information
  to resolve overloading for this operator applications, such as
  ``both arguments are floats'', or ``the first is a pointer
  and the second is an integer''.  These functions are used to resolve
  overloading both in the dynamic semantics (module [Csem]) and in the
  compiler (module [Cshmgen]).
*)

inductive classify_add_cases : Type[0] ≝
  | add_case_ii: classify_add_cases         (**r int , int *)
  | add_case_ff: classify_add_cases         (**r float , float *)
  | add_case_pi: type → classify_add_cases (**r ptr or array, int *)
  | add_case_ip: type → classify_add_cases (**r int, ptr or array *)
  | add_default: classify_add_cases.        (**r other *)

definition classify_add ≝ λty1: type. λty2: type.
(*
  match ty1, ty2 with
  [ Tint _ _, Tint _ _ ⇒ add_case_ii
  | Tfloat _, Tfloat _ ⇒ add_case_ff
  | Tpointer ty, Tint _ _ ⇒ add_case_pi ty
  | Tarray ty _, Tint _ _ ⇒ add_case_pi ty 
  | Tint _ _, Tpointer ty ⇒ add_case_ip ty
  | Tint _ _, Tarray ty _ ⇒ add_case_ip ty 
  | _, _ ⇒ add_default
  ].
*)
  match ty1 with
  [ Tint _ _ ⇒
    match ty2 with
    [ Tint _ _ ⇒ add_case_ii
    | Tpointer _ ty ⇒ add_case_ip ty
    | Tarray _ ty _ ⇒ add_case_ip ty
    | _ ⇒ add_default ]
  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
  | _ ⇒ add_default
  ].

inductive classify_sub_cases : Type[0] ≝
  | sub_case_ii: classify_sub_cases          (**r int , int *)
  | sub_case_ff: classify_sub_cases          (**r float , float *)
  | sub_case_pi: type → classify_sub_cases  (**r ptr or array , int *)
  | sub_case_pp: type → classify_sub_cases  (**r ptr or array , ptr or array *)
  | sub_default: classify_sub_cases .        (**r other *)

definition classify_sub ≝ λty1: type. λty2: type.
(*  match ty1, ty2 with
  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
  | Tfloat _ , Tfloat _ ⇒ sub_case_ff
  | Tpointer ty , Tint _ _ ⇒ sub_case_pi ty
  | Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty
  | Tpointer ty , Tpointer _ ⇒ sub_case_pp ty
  | Tpointer ty , Tarray _ _⇒ sub_case_pp ty
  | Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty
  | Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty 
  | _ ,_ ⇒ sub_default
  end.
*)
  match ty1 with
  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
  | Tpointer _ ty ⇒
    match ty2 with
    [ Tint _ _ ⇒ sub_case_pi ty
    | Tpointer _ _ ⇒ sub_case_pp ty
    | Tarray _ _ _ ⇒ sub_case_pp ty
    | _ ⇒ sub_default ]
  | Tarray _ ty _ ⇒
    match ty2 with
    [ Tint _ _ ⇒ sub_case_pi ty
    | Tpointer _ _ ⇒ sub_case_pp ty
    | Tarray _ _ _ ⇒ sub_case_pp ty
    | _ ⇒ sub_default ]
  | _ ⇒ sub_default
  ].

inductive classify_mul_cases : Type[0] ≝
  | mul_case_ii: classify_mul_cases (**r int , int *)
  | mul_case_ff: classify_mul_cases (**r float , float *)
  | mul_default: classify_mul_cases . (**r other *)

definition classify_mul ≝ λty1: type. λty2: type.
  match ty1 with
  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff | _ ⇒ mul_default ]
  | _ ⇒ mul_default
  ].
(*
  match ty1,ty2 with
  | Tint _ _, Tint _ _ ⇒ mul_case_ii
  | Tfloat _ , Tfloat _ ⇒ mul_case_ff
  | _,_  ⇒ mul_default
end.
*)
inductive classify_div_cases : Type[0] ≝
  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
  | div_case_ii: classify_div_cases    (**r int , int *) 
  | div_case_ff: classify_div_cases    (**r float , float *)
  | div_default: classify_div_cases. (**r other *)

definition classify_32un_aux ≝ λT:Type[0].λi.λs.λr1:T.λr2:T.
  match i with [ I32 ⇒
    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
  | _ ⇒ r2 ].

definition classify_div ≝ λty1: type. λty2: type.
  match ty1 with
  [ Tint i1 s1 ⇒
    match ty2 with
    [ Tint i2 s2 ⇒
      classify_32un_aux ? i1 s1 div_case_I32unsi
        (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii)
    | _ ⇒ div_default ]
  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff | _ ⇒ div_default ]
  | _ ⇒ div_default
  ].
(*
definition classify_div ≝ λty1: type. λty2: type.
  match ty1,ty2 with 
  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi 
  | Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi 
  | Tint _ _ , Tint _ _ ⇒ div_case_ii 
  | Tfloat _ , Tfloat _ ⇒ div_case_ff 
  | _ ,_ ⇒ div_default 
end.
*)
inductive classify_mod_cases : Type[0] ≝
  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
  | mod_case_ii: classify_mod_cases  (**r int , int *)
  | mod_default: classify_mod_cases . (**r other *)

definition classify_mod ≝ λty1:type. λty2:type.
  match ty1 with
  [ Tint i1 s1 ⇒
    match ty2 with
    [ Tint i2 s2 ⇒
      classify_32un_aux ? i1 s1 mod_case_I32unsi
        (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii)
    | _ ⇒ mod_default ]
  | _ ⇒ mod_default
  ].
(*
Definition classify_mod (ty1: type) (ty2: type) :=
  match ty1,ty2 with
  | Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi 
  | Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi 
  | Tint _ _ , Tint _ _ ⇒ mod_case_ii 
  | _ , _ ⇒ mod_default 
end .
*)
inductive classify_shr_cases :Type[0] ≝
  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
  | shr_case_ii :classify_shr_cases (**r int , int *)
  | shr_default : classify_shr_cases . (**r other *)

definition classify_shr ≝ λty1: type. λty2: type.
  match ty1 with
  [ Tint i1 s1 ⇒
    match ty2 with
    [ Tint _ _ ⇒
      classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii
    | _ ⇒ shr_default ]
  | _ ⇒ shr_default
  ].

(*
Definition classify_shr (ty1: type) (ty2: type) :=
  match ty1,ty2 with
  | Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi
  | Tint _ _ , Tint _ _ ⇒ shr_case_ii
  | _ , _ ⇒ shr_default 
  end.
*)
inductive classify_cmp_cases : Type[0] ≝
  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
  | cmp_case_ii: classify_cmp_cases  (**r int, int*)
  | cmp_case_pp: classify_cmp_cases  (**r ptr|array , ptr|array*)
  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
  | cmp_default: classify_cmp_cases . (**r other *)

definition classify_cmp ≝ λty1:type. λty2:type.
  match ty1 with
  [ Tint i1 s1 ⇒
    match ty2 with
    [ Tint i2 s2 ⇒
      classify_32un_aux ? i1 s1 cmp_case_I32unsi
        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ii)
    | _ ⇒ cmp_default ]
  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
  | Tpointer _ _ ⇒
    match ty2 with
    [ Tpointer _ _ ⇒ cmp_case_pp
    | Tarray _ _ _ ⇒ cmp_case_pp
    | _ ⇒ cmp_default ]
  | Tarray _ _ _ ⇒
    match ty2 with
    [ Tpointer _ _ ⇒ cmp_case_pp
    | Tarray _ _ _ ⇒ cmp_case_pp
    | _ ⇒ cmp_default ]
  | _ ⇒ cmp_default
  ].

(*
Definition classify_cmp (ty1: type) (ty2: type) :=
  match ty1,ty2 with 
  | Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi 
  | Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi 
  | Tint _ _ , Tint _ _ ⇒ cmp_case_ipip
  | Tfloat _ , Tfloat _ ⇒ cmp_case_ff
  | Tpointer _ , Tint _ _ ⇒ cmp_case_ipip
  | Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip
  | Tpointer _ , Tpointer _ ⇒ cmp_case_ipip
  | Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip
  | Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip
  | Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip
  | _ , _ ⇒ cmp_default
  end.
*)
inductive classify_fun_cases : Type[0] ≝
  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
  | fun_default: classify_fun_cases . (**r other *)

definition classify_fun ≝ λty: type.
  match ty with 
  [ Tfunction args res ⇒ fun_case_f args res
  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
                                    | _ ⇒ fun_default
                                    ]
  | _ ⇒ fun_default
  ].

(* * Translating Clight types to Cminor types, function signatures,
  and external functions. *)

definition typ_of_type : type → typ ≝ λt.
  match t with
  [ Tvoid ⇒ ASTint I32 Unsigned
  | Tint sz sg ⇒ ASTint sz sg
  | Tfloat sz ⇒ ASTfloat sz
  | Tpointer r _ ⇒ ASTptr r
  | Tarray r _ _ ⇒ ASTptr r
  | Tfunction _ _ ⇒ ASTptr Code
  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
  ].

definition opttyp_of_type : type → option typ ≝ λt.
  match t with
  [ Tvoid ⇒ None ?
  | Tint sz sg ⇒ Some ? (ASTint sz sg)
  | Tfloat sz ⇒ Some ? (ASTfloat sz)
  | Tpointer r _ ⇒ Some ? (ASTptr r)
  | Tarray r _ _ ⇒ Some ? (ASTptr r)
  | Tfunction _ _ ⇒ Some ? (ASTptr Code)
  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
  ].

let rec typlist_of_typelist (tl: typelist) : list typ ≝
  match tl with
  [ Tnil ⇒ nil ?
  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
  ].

definition signature_of_type : typelist → type → signature ≝ λargs. λres.
  mk_signature (typlist_of_typelist args) (opttyp_of_type res).

definition external_function
    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
  mk_external_function id (signature_of_type targs tres).