source: src/Clight/Csyntax.ma @ 3178

Last change on this file since 3178 was 3178, checked in by campbell, 6 years ago

Some progress on Callstate steps in Clight to Cminor.
Note that some bogus alignment has been removed in Csyntax.

File size: 24.3 KB
RevLine 
[3]1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Abstract syntax for the Clight language *)
17
[474]18(*include "Integers.ma".*)
[747]19include "common/AST.ma".
[700]20include "utilities/Coqlib.ma".
21include "common/Errors.ma".
[720]22include "common/CostLabel.ma".
[3]23
24(* * * Abstract syntax *)
25
26(* * ** Types *)
27
28(* * The syntax of type expressions.  Some points to note:
29- Array types [Tarray n] carry the size [n] of the array.
30  Arrays with unknown sizes are represented by pointer types.
31- Function types [Tfunction targs tres] specify the number and types
32  of the function arguments (list [targs]), and the type of the
33  function result ([tres]).  Variadic functions and old-style unprototyped
34  functions are not supported.
35- In C, struct and union types are named and compared by name.
36  This enables the definition of recursive struct types such as
37<<
38  struct s1 { int n; struct * s1 next; };
39>>
40  Note that recursion within types must go through a pointer type.
41  For instance, the following is not allowed in C.
42<<
43  struct s2 { int n; struct s2 next; };
44>>
45  In Clight, struct and union types [Tstruct id fields] and
46  [Tunion id fields] are compared by structure: the [fields]
47  argument gives the names and types of the members.  The identifier
48  [id] is a local name which can be used in conjuction with the
[481]49  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr rg id]
[3]50  stands for a pointer type to the nearest enclosing [Tstruct]
[481]51  or [Tunion] type named [id] in memory region [rg].  For instance.
52  the structure [s1] defined above in C is expressed by
[3]53<<
54  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
[481]55               (Fcons "next" (Tcomp_ptr Any "id")
[3]56               Fnil))
57>>
58  Note that the incorrect structure [s2] above cannot be expressed at
59  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
60  structure or union, but not to the structure or union directly.
61*)
62
[487]63inductive type : Type[0] ≝
[3]64  | Tvoid: type                         (**r the [void] type *)
65  | Tint: intsize → signedness → type   (**r integer types *)
[2176]66  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
67  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
[3]68  | Tfunction: typelist → type → type   (**r function types *)
69  | Tstruct: ident → fieldlist → type   (**r struct types *)
70  | Tunion: ident → fieldlist → type    (**r union types *)
[2176]71  | Tcomp_ptr: (*region →*) ident → type    (**r pointer to named struct or union *)
[3]72
[487]73with typelist : Type[0] ≝
[3]74  | Tnil: typelist
75  | Tcons: type → typelist → typelist
76
[487]77with fieldlist : Type[0] ≝
[3]78  | Fnil: fieldlist
79  | Fcons: ident → type → fieldlist → fieldlist.
80
81(* XXX: no induction scheme! *)
[487]82let rec type_ind
[3]83  (P:type → Prop)
84  (vo:P Tvoid)
85  (it:∀i,s. P (Tint i s))
[2176]86  (pt:∀t. P t → P (Tpointer t))
87  (ar:∀t,n. P t → P (Tarray t n))
[3]88  (fn:∀tl,t. P t → P (Tfunction tl t))
89  (st:∀i,fl. P (Tstruct i fl))
90  (un:∀i,fl. P (Tunion i fl))
[2176]91  (cp:∀i. P (Tcomp_ptr i))
[3]92  (t:type) on t : P t ≝
93  match t return λt'.P t' with
94  [ Tvoid ⇒ vo
95  | Tint i s ⇒ it i s
[2468]96  | Tpointer t' ⇒ pt t' (type_ind P vo it pt ar fn st un cp t')
97  | Tarray t' n ⇒ ar t' n (type_ind P vo it pt ar fn st un cp t')
98  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it pt ar fn st un cp t')
[3]99  | Tstruct i fs ⇒ st i fs
100  | Tunion i fs ⇒ un i fs
[2176]101  | Tcomp_ptr i ⇒ cp i
[3]102  ].
103 
[487]104let rec fieldlist_ind
[3]105  (P:fieldlist → Prop)
106  (nl:P Fnil)
107  (cs:∀i,t,fs. P fs → P (Fcons i t fs))
108  (fs:fieldlist) on fs : P fs ≝
109  match fs with
110  [ Fnil ⇒ nl
111  | Fcons i t fs' ⇒ cs i t fs' (fieldlist_ind P nl cs fs')
112  ].
113
114(* * ** Expressions *)
115
116(* * Arithmetic and logical operators. *)
117
[487]118inductive unary_operation : Type[0] ≝
[3]119  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
120  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
121  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
122
[487]123inductive binary_operation : Type[0] ≝
[3]124  | Oadd : binary_operation             (**r addition (binary [+]) *)
125  | Osub : binary_operation             (**r subtraction (binary [-]) *)
126  | Omul : binary_operation             (**r multiplication (binary [*]) *)
127  | Odiv : binary_operation             (**r division ([/]) *)
128  | Omod : binary_operation             (**r remainder ([%]) *)
129  | Oand : binary_operation             (**r bitwise and ([&]) *)
130  | Oor : binary_operation              (**r bitwise or ([|]) *)
131  | Oxor : binary_operation             (**r bitwise xor ([^]) *)
132  | Oshl : binary_operation             (**r left shift ([<<]) *)
133  | Oshr : binary_operation             (**r right shift ([>>]) *)
134  | Oeq: binary_operation               (**r comparison ([==]) *)
135  | One: binary_operation               (**r comparison ([!=]) *)
136  | Olt: binary_operation               (**r comparison ([<]) *)
137  | Ogt: binary_operation               (**r comparison ([>]) *)
138  | Ole: binary_operation               (**r comparison ([<=]) *)
139  | Oge: binary_operation.              (**r comparison ([>=]) *)
140
141(* * Clight expressions are a large subset of those of C.
142  The main omissions are string literals and assignment operators
143  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
144  not an expression. 
145
146  All expressions are annotated with their types.  An expression
147  (type [expr]) is therefore a pair of a type and an expression
148  description (type [expr_descr]).
149*)
150
[487]151inductive expr : Type[0] ≝
[3]152  | Expr: expr_descr → type → expr
153
[487]154with expr_descr : Type[0] ≝
[961]155  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
[3]156  | Evar: ident → expr_descr           (**r variable *)
157  | Ederef: expr → expr_descr          (**r pointer dereference (unary [*]) *)
158  | Eaddrof: expr → expr_descr         (**r address-of operator ([&]) *)
159  | Eunop: unary_operation → expr → expr_descr  (**r unary operation *)
160  | Ebinop: binary_operation → expr → expr → expr_descr (**r binary operation *)
161  | Ecast: type → expr → expr_descr    (**r type cast ([(ty) e]) *)
162  | Econdition: expr → expr → expr → expr_descr (**r conditional ([e1 ? e2 : e3]) *)
163  | Eandbool: expr → expr → expr_descr (**r sequential and ([&&]) *)
164  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
165  | Esizeof: type → expr_descr         (**r size of a type *)
[175]166  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
167  | Ecost: costlabel → expr → expr_descr.
[3]168
[251]169
170
171
[3]172(* * Extract the type part of a type-annotated Clight expression. *)
173
[487]174definition typeof : expr → type ≝ λe.
[3]175  match e with [ Expr de te ⇒ te ].
176
177(* * ** Statements *)
178
179(* * Clight statements include all C statements.
180  Only structured forms of [switch] are supported; moreover,
181  the [default] case must occur last.  Blocks and block-scoped declarations
182  are not supported. *)
183
[487]184definition label ≝ ident.
[3]185
[487]186inductive statement : Type[0] ≝
[3]187  | Sskip : statement                   (**r do nothing *)
188  | Sassign : expr → expr → statement   (**r assignment [lvalue = rvalue] *)
189  | Scall: option expr → expr → list expr → statement (**r function call *)
190  | Ssequence : statement → statement → statement  (**r sequence *)
191  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
[2391]192  | Swhile : expr → statement → statement   (**r [while] loop *)
[3]193  | Sdowhile : expr → statement → statement (**r [do] loop *)
194  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
195  | Sbreak : statement                      (**r [break] statement *)
196  | Scontinue : statement                   (**r [continue] statement *)
197  | Sreturn : option expr → statement       (**r [return] statement *)
198  | Sswitch : expr → labeled_statements → statement  (**r [switch] statement *)
199  | Slabel : label → statement → statement
200  | Sgoto : label → statement
[175]201  | Scost : costlabel → statement → statement
[3]202
[487]203with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
[3]204  | LSdefault: statement → labeled_statements
[961]205  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
[3]206
[1920]207let rec labeled_statements_ind
208  (P:labeled_statements → Prop)
209  (LSd:∀s. P (LSdefault s))
210  (LSc:∀sz,i,s,tl. P tl → P (LScase sz i s tl))
211  ls on ls : P ls ≝
212match ls with
213[ LSdefault s ⇒ LSd s
214| LScase sz i s tl ⇒ LSc sz i s tl (labeled_statements_ind P LSd LSc tl)
215].
216
[487]217let rec statement_ind2
[24]218  (P:statement → Prop) (Q:labeled_statements → Prop)
219  (Ssk:P Sskip)
220  (Sas:∀e1,e2. P (Sassign e1 e2))
221  (Sca:∀eo,e,args. P (Scall eo e args))
222  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
223  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
[2391]224  (Swh:∀e,s. P s → P (Swhile e s))
[24]225  (Sdo:∀e,s. P s → P (Sdowhile e s))
226  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
227  (Sbr:P Sbreak)
228  (Sco:P Scontinue)
229  (Sre:∀eo. P (Sreturn eo))
230  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
231  (Sla:∀l,s. P s → P (Slabel l s))
232  (Sgo:∀l. P (Sgoto l))
[175]233  (Scs:∀l,s. P s → P (Scost l s))
[24]234  (LSd:∀s. P s → Q (LSdefault s))
[961]235  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
[24]236  (s:statement) on s : P s ≝
237match s with
238[ Sskip ⇒ Ssk
239| Sassign e1 e2 ⇒ Sas e1 e2
240| Scall eo e args ⇒ Sca eo e args
241| Ssequence s1 s2 ⇒ Ssq s1 s2
[175]242    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
243    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
[24]244| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
[175]245    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
246    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
[2391]247| Swhile e s ⇒ Swh e s
[175]248    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
[24]249| Sdowhile e s ⇒ Sdo e s
[175]250    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
[24]251| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
[175]252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
253    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
254    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
[24]255| Sbreak ⇒ Sbr
256| Scontinue ⇒ Sco
257| Sreturn eo ⇒ Sre eo
258| Sswitch e ls ⇒ Ssw e ls
[175]259    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
[24]260| Slabel l s ⇒ Sla l s
[175]261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
[24]262| Sgoto l ⇒ Sgo l
[175]263| Scost l s ⇒ Scs l s
264    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
[24]265]
266and labeled_statements_ind2
267  (P:statement → Prop) (Q:labeled_statements → Prop)
268  (Ssk:P Sskip)
269  (Sas:∀e1,e2. P (Sassign e1 e2))
270  (Sca:∀eo,e,args. P (Scall eo e args))
271  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
272  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
[2391]273  (Swh:∀e,s. P s → P (Swhile e s))
[24]274  (Sdo:∀e,s. P s → P (Sdowhile e s))
275  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
276  (Sbr:P Sbreak)
277  (Sco:P Scontinue)
278  (Sre:∀eo. P (Sreturn eo))
279  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
280  (Sla:∀l,s. P s → P (Slabel l s))
281  (Sgo:∀l. P (Sgoto l))
[175]282  (Scs:∀l,s. P s → P (Scost l s))
[24]283  (LSd:∀s. P s → Q (LSdefault s))
[961]284  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
[24]285  (ls:labeled_statements) on ls : Q ls ≝
286match ls with
287[ LSdefault s ⇒ LSd s
[175]288    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
[961]289| LScase sz i s t ⇒ LSc sz i s t
[175]290    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
291    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
[24]292].
293
[487]294definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
[175]295  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
[961]296  (λ_,_. I) (λ_,_,_,_,_,_.I).
[24]297
[3]298(* * ** Functions *)
299
300(* * A function definition is composed of its return type ([fn_return]),
301  the names and types of its parameters ([fn_params]), the names
302  and types of its local variables ([fn_vars]), and the body of the
303  function (a statement, [fn_body]). *)
304
[487]305record function : Type[0] ≝ {
[3]306  fn_return: type;
307  fn_params: list (ident × type);
308  fn_vars: list (ident × type);
309  fn_body: statement
310}.
311
[725]312(* * Functions can either be defined ([CL_Internal]) or declared as
313  external functions ([CL_External]).  Similar to the AST definition, but
314  with high level type information for external functions. *)
[3]315
[725]316inductive clight_fundef : Type[0] ≝
317  | CL_Internal: function → clight_fundef
318  | CL_External: ident → typelist → type → clight_fundef.
[3]319
320(* * ** Programs *)
321
322(* * A program is a collection of named functions, plus a collection
323  of named global variables, carrying their types and optional initialization
324  data.  See module [AST] for more details. *)
325
[1224]326definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).
[3]327
328(* * * Operations over types *)
329
330(* * The type of a function definition. *)
331
[487]332let rec type_of_params (params: list (ident × type)) : typelist ≝
[3]333  match params with
334  [ nil ⇒ Tnil
[1599]335  | cons h rem ⇒ let 〈id,ty〉 ≝ h in Tcons ty (type_of_params rem)
[3]336  ].
337
[487]338definition type_of_function : function → type ≝ λf.
[3]339  Tfunction (type_of_params (fn_params f)) (fn_return f).
340
[725]341definition type_of_fundef : clight_fundef → type ≝ λf.
[3]342  match f with
[725]343  [ CL_Internal fd ⇒ type_of_function fd
344  | CL_External id args res ⇒ Tfunction args res
[3]345  ].
346
347(* * Natural alignment of a type, in bytes. *)
[3178]348let rec alignof (t: type) : nat ≝ 1.
349(* these are old values for 32 bit machines
[744]350  match t with
[3]351  [ Tvoid ⇒ 1
[744]352  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
[2176]353  | Tpointer _ ⇒ 4
354  | Tarray t' n ⇒ alignof t'
[3]355  | Tfunction _ _ ⇒ 1
356  | Tstruct _ fld ⇒ alignof_fields fld
357  | Tunion _ fld ⇒ alignof_fields fld
[2176]358  | Tcomp_ptr _ ⇒ 4
[3]359  ]
360
[744]361and alignof_fields (f: fieldlist) : nat ≝
[3]362  match f with
363  [ Fnil ⇒ 1
[744]364  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
[3178]365  ].*)
[3]366
367(*
368Scheme type_ind2 := Induction for type Sort Prop
369  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
370*)
371
372(* XXX: automatic generation? *)
[487]373let rec type_ind2
[3]374  (P:type → Prop) (Q:fieldlist → Prop)
375  (vo:P Tvoid)
376  (it:∀i,s. P (Tint i s))
[2176]377  (pt:∀t. P t → P (Tpointer t))
378  (ar:∀t,n. P t → P (Tarray t n))
[3]379  (fn:∀tl,t. P t → P (Tfunction tl t))
380  (st:∀i,fl. Q fl → P (Tstruct i fl))
381  (un:∀i,fl. Q fl → P (Tunion i fl))
[2176]382  (cp:∀i. P (Tcomp_ptr i))
[3]383  (nl:Q Fnil)
384  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
385 (t:type) on t : P t ≝
386  match t return λt'.P t' with
387  [ Tvoid ⇒ vo
388  | Tint i s ⇒ it i s
[2468]389  | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it pt ar fn st un cp nl cs t')
390  | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it pt ar fn st un cp nl cs t')
391  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it pt ar fn st un cp nl cs t')
392  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs fs)
393  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs fs)
[2176]394  | Tcomp_ptr i ⇒ cp i
[3]395  ]
396and fieldlist_ind2
397  (P:type → Prop) (Q:fieldlist → Prop)
398  (vo:P Tvoid)
399  (it:∀i,s. P (Tint i s))
[2176]400  (pt:∀t. P t → P (Tpointer t))
401  (ar:∀t,n. P t → P (Tarray t n))
[3]402  (fn:∀tl,t. P t → P (Tfunction tl t))
403  (st:∀i,fl. Q fl → P (Tstruct i fl))
404  (un:∀i,fl. Q fl → P (Tunion i fl))
[2176]405  (cp:∀i. P (Tcomp_ptr i))
[3]406  (nl:Q Fnil)
407  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
408  (fs:fieldlist) on fs : Q fs ≝
409  match fs return λfs'.Q fs' with
410  [ Fnil ⇒ nl
[2468]411  | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it pt ar fn st un cp nl cs t)
412                        (fieldlist_ind2 P Q vo it pt ar fn st un cp nl cs f')
[3]413  ].
[3178]414(*
[487]415lemma alignof_fields_pos:
[3]416  ∀f. alignof_fields f > 0.
[487]417@fieldlist_ind //;
[744]418#i #t #fs' #IH @max_r @IH qed.
[3178]419*)
[487]420lemma alignof_pos:
[3]421  ∀t. alignof t > 0.
[3178]422#t elim t; normalize; //;(*
[744]423[ 1,2: #z cases z; /2/;
[487]424| 3,4: #i @alignof_fields_pos
[3178]425]*) qed.
[3]426
427(* * Size of a type, in bytes. *)
428
[744]429let rec sizeof (t: type) : nat ≝
430  match t with
[3]431  [ Tvoid ⇒ 1
[744]432  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
[2176]433  | Tpointer _ ⇒ size_pointer
434  | Tarray t' n ⇒ sizeof t' * max 1 n
[3]435  | Tfunction _ _ ⇒ 1
[744]436  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
437  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
[2176]438  | Tcomp_ptr _ ⇒ size_pointer
[3]439  ]
440
[744]441and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat ≝
[3]442  match fld with
443  [ Fnil ⇒ pos
444  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
445  ]
446
[744]447and sizeof_union (fld: fieldlist) : nat ≝
[3]448  match fld with
449  [ Fnil ⇒ 0
[744]450  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
[3]451  ].
[3178]452
[487]453lemma sizeof_pos:
[3]454  ∀t. sizeof t > 0.
[3178]455#t elim t //
456[ * //
457| #t' * [ /2/ | #n #H change with (0 < ?) whd in ⊢ (??%); change with (0*0) in ⊢ (?%?); @lt_times // ]
458| #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1
459  >commutative_plus cases (sizeof_struct ??) [2:#x] whd in ⊢ (?(?%?)?);
460  //
461| #i #fl whd in ⊢ (?%?); whd in match (alignof ?); <times_n_1
462  >commutative_plus cases (sizeof_union ?) [2:#x] whd in ⊢ (?(?%?)?);
463  //
464] qed.
[3]465
[3178]466(*
[3]467Lemma sizeof_struct_incr:
468  forall fld pos, pos <= sizeof_struct fld pos.
469Proof.
470  induction fld; intros; simpl. omega.
471  eapply Zle_trans. 2: apply IHfld.
472  apply Zle_trans with (align pos (alignof t)).
473  apply align_le. apply alignof_pos.
474  assert (sizeof t > 0) by apply sizeof_pos. omega.
475Qed.
476
477(** Byte offset for a field in a struct or union.
478  Field are laid out consecutively, and padding is inserted
479  to align each field to the natural alignment for its type. *)
480
481Open Local Scope string_scope.
482*)
[797]483
[744]484let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
485                              on fld : res nat ≝
[3]486  match fld with
[797]487  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
[3]488  | Fcons id' t fld' ⇒
489      match ident_eq id id' with
490      [ inl _ ⇒ OK ? (align pos (alignof t))
491      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
492      ]
493  ].
494
[487]495definition field_offset ≝ λid: ident. λfld: fieldlist.
[3]496  field_offset_rec id fld 0.
497
[487]498let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
[3]499  match fld with
[797]500  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
[3]501  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
502  ].
503
504(* * Some sanity checks about field offsets.  First, field offsets are
505  within the range of acceptable offsets. *)
506(*
507Remark field_offset_rec_in_range:
508  forall id ofs ty fld pos,
509  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
510  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
511Proof.
512  intros until ty. induction fld; simpl.
513  congruence.
514  destruct (ident_eq id i); intros.
515  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
516  exploit IHfld; eauto. intros [A B]. split; auto.
517  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
518  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
519Qed.
520
521Lemma field_offset_in_range:
522  forall id fld ofs ty,
523  field_offset id fld = OK ofs → field_type id fld = OK ty →
524  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
525Proof.
526  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
527Qed.
528
529(** Second, two distinct fields do not overlap *)
530
531Lemma field_offset_no_overlap:
532  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
533  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
534  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
535  id1 <> id2 →
536  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
537Proof.
538  intros until ty2. intros fld0 A B C D NEQ.
539  assert (forall fld pos,
540  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
541  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
542  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
543  induction fld; intro pos; simpl. congruence.
544  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
545  congruence.
546  subst i. intros. inv H; inv H0.
547  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
548  subst i. intros. inv H1; inv H2.
549  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
550  intros. eapply IHfld; eauto.
551
552  apply H with fld0 0; auto.
553Qed.
554
555(** Third, if a struct is a prefix of another, the offsets of fields
556  in common is the same. *)
557
558Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
559  match fld1 with
560  | Fnil ⇒ fld2
561  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
562  end.
563
564Lemma field_offset_prefix:
565  forall id ofs fld2 fld1,
566  field_offset id fld1 = OK ofs →
567  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
568Proof.
569  intros until fld2.
570  assert (forall fld1 pos,
571    field_offset_rec id fld1 pos = OK ofs ->
572    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
573  induction fld1; intros pos; simpl. congruence.
574  destruct (ident_eq id i); auto.
575  intros. unfold field_offset; auto.
576Qed.
577*)
578
579
580(* * Translating Clight types to Cminor types, function signatures,
581  and external functions. *)
582
[487]583definition typ_of_type : type → typ ≝ λt.
[3]584  match t with
[879]585  [ Tvoid ⇒ ASTint I32 Unsigned
586  | Tint sz sg ⇒ ASTint sz sg
[2176]587  | Tpointer _ ⇒ ASTptr
588  | Tarray _ _ ⇒ ASTptr
589  | Tfunction _ _ ⇒ ASTptr
590  | Tcomp_ptr _ ⇒ ASTptr
[879]591  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
[3]592  ].
593
[487]594definition opttyp_of_type : type → option typ ≝ λt.
[3]595  match t with
596  [ Tvoid ⇒ None ?
[879]597  | Tint sz sg ⇒ Some ? (ASTint sz sg)
[2176]598  | Tpointer _ ⇒ Some ? ASTptr
599  | Tarray _ _ ⇒ Some ? ASTptr
600  | Tfunction _ _ ⇒ Some ? ASTptr
601  | Tcomp_ptr _ ⇒ Some ? ASTptr
[879]602  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
[3]603  ].
604
[487]605let rec typlist_of_typelist (tl: typelist) : list typ ≝
[3]606  match tl with
607  [ Tnil ⇒ nil ?
608  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
609  ].
610
[1872]611
612(* * The [access_mode] function describes how a variable of the given
613type must be accessed:
614- [By_value ch]: access by value, i.e. by loading from the address
615  of the variable using the memory chunk [ch];
616- [By_reference]: access by reference, i.e. by just returning
617  the address of the variable;
618- [By_nothing]: no access is possible, e.g. for the [void] type.
619
620We currently do not support 64-bit integers and 128-bit floats, so these
621have an access mode of [By_nothing].
622*)
623
624inductive mode: typ → Type[0] ≝
625  | By_value: ∀t:typ. mode t
[2176]626  | By_reference: (*∀r:region.*) mode ASTptr
[1872]627  | By_nothing: ∀t. mode t.
628
629definition access_mode : ∀ty. mode (typ_of_type ty) ≝ λty.
630  match ty return λty. mode (typ_of_type ty) with
631  [ Tint i s ⇒ By_value (ASTint i s)
632  | Tvoid ⇒ By_nothing …
[2176]633  | Tpointer _ ⇒ By_value ASTptr
634  | Tarray _ _ ⇒ By_reference
635  | Tfunction _ _ ⇒ By_reference
[1872]636  | Tstruct _ fList ⇒ By_nothing …
637  | Tunion _ fList ⇒ By_nothing …
[2176]638  | Tcomp_ptr _ ⇒ By_value ASTptr
[1872]639  ].
640
[487]641definition signature_of_type : typelist → type → signature ≝ λargs. λres.
[3]642  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
643
[487]644definition external_function
[3]645    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
646  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.