source: src/Clight/Csyntax.ma @ 748

(* *********************************************************************)
(*                                                                     *)
(*              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 *)

(* * Clight types are similar to those of C.  They include numeric types,
  pointers, arrays, function types, and composite types (struct and 
  union).  Numeric types (integers and floats) fully specify the
  bit size of the type.  An integer type is a pair of a signed/unsigned
  flag and a bit size: 8, 16 or 32 bits. *)

inductive signedness : Type[0] ≝
  | Signed: signedness
  | Unsigned: signedness.

inductive intsize : Type[0] ≝
  | I8: intsize
  | I16: intsize
  | I32: intsize.

(* * Float types come in two sizes: 32 bits (single precision)
  and 64-bit (double precision). *)

inductive floatsize : Type[0] ≝
  | F32: floatsize
  | F64: floatsize.

(* * 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: int → 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: int → 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:∀i,s,t. P s → Q t → Q (LScase 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:∀i,s,t. P s → Q t → Q (LScase 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 i s t ⇒ LSc 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 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 ⇒ match h with [ pair id ty ⇒ 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.
*)
let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
                              on fld : res nat ≝
  match fld with
  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
  | 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 "Unknown field " :: CTX id :: nil*)
  | 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_ipip: classify_cmp_cases  (**r int|ptr|array , int|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_ipip)
    | _ ⇒ cmp_default ]
  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
  | Tpointer _ _ ⇒
    match ty2 with
    [ Tint _ _ ⇒ cmp_case_ipip
    | Tpointer _ _ ⇒ cmp_case_ipip
    | Tarray _ _ _ ⇒ cmp_case_ipip
    | _ ⇒ cmp_default ]
  | Tarray _ _ _ ⇒
    match ty2 with
    [ Tint _ _ ⇒ cmp_case_ipip
    | Tpointer _ _ ⇒ cmp_case_ipip
    | Tarray _ _ _ ⇒ cmp_case_ipip
    | _ ⇒ 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
  [ Tfloat _ ⇒ ASTfloat
  | _ ⇒ ASTint
  ].

definition opttyp_of_type : type → option typ ≝ λt.
  match t with
  [ Tvoid ⇒ None ?
  | Tfloat _ ⇒ Some ? ASTfloat
  | _ ⇒ Some ? ASTint
  ].

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).