source: src/Clight/Csyntax.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 6 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 24.9 KB
Line 
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
18(*include "Integers.ma".*)
19include "common/AST.ma".
20include "utilities/Coqlib.ma".
21include "common/Errors.ma".
22include "common/CostLabel.ma".
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
49  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr rg id]
50  stands for a pointer type to the nearest enclosing [Tstruct]
51  or [Tunion] type named [id] in memory region [rg].  For instance.
52  the structure [s1] defined above in C is expressed by
53<<
54  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
55               (Fcons "next" (Tcomp_ptr Any "id")
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
63inductive type : Type[0] ≝
64  | Tvoid: type                         (**r the [void] type *)
65  | Tint: intsize → signedness → type   (**r integer types *)
66  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
67  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
68  | Tfunction: typelist → type → type   (**r function types *)
69  | Tstruct: ident → fieldlist → type   (**r struct types *)
70  | Tunion: ident → fieldlist → type    (**r union types *)
71  | Tcomp_ptr: (*region →*) ident → type    (**r pointer to named struct or union *)
72
73with typelist : Type[0] ≝
74  | Tnil: typelist
75  | Tcons: type → typelist → typelist
76
77with fieldlist : Type[0] ≝
78  | Fnil: fieldlist
79  | Fcons: ident → type → fieldlist → fieldlist.
80
81(* XXX: no induction scheme! *)
82let rec type_ind
83  (P:type → Prop)
84  (vo:P Tvoid)
85  (it:∀i,s. P (Tint i s))
86  (pt:∀t. P t → P (Tpointer t))
87  (ar:∀t,n. P t → P (Tarray t n))
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))
91  (cp:∀i. P (Tcomp_ptr i))
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
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')
99  | Tstruct i fs ⇒ st i fs
100  | Tunion i fs ⇒ un i fs
101  | Tcomp_ptr i ⇒ cp i
102  ].
103 
104let rec fieldlist_ind
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
118inductive unary_operation : Type[0] ≝
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
123inductive binary_operation : Type[0] ≝
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
151inductive expr : Type[0] ≝
152  | Expr: expr_descr → type → expr
153
154with expr_descr : Type[0] ≝
155  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
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 *)
166  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
167  | Ecost: costlabel → expr → expr_descr.
168
169
170
171
172(* * Extract the type part of a type-annotated Clight expression. *)
173
174definition typeof : expr → type ≝ λe.
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
184definition label ≝ ident.
185
186inductive statement : Type[0] ≝
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 *)
192  | Swhile : expr → statement → statement   (**r [while] loop *)
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
201  | Scost : costlabel → statement → statement
202
203with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
204  | LSdefault: statement → labeled_statements
205  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
206
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
217let rec statement_ind2
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))
224  (Swh:∀e,s. P s → P (Swhile e s))
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))
233  (Scs:∀l,s. P s → P (Scost l s))
234  (LSd:∀s. P s → Q (LSdefault s))
235  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
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
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)
244| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
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)
247| Swhile e s ⇒ Swh e s
248    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
249| Sdowhile e s ⇒ Sdo e s
250    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
251| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
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)
255| Sbreak ⇒ Sbr
256| Scontinue ⇒ Sco
257| Sreturn eo ⇒ Sre eo
258| Sswitch e ls ⇒ Ssw e ls
259    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
260| Slabel l s ⇒ Sla l s
261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
262| Sgoto l ⇒ Sgo l
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)
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))
273  (Swh:∀e,s. P s → P (Swhile e s))
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))
282  (Scs:∀l,s. P s → P (Scost l s))
283  (LSd:∀s. P s → Q (LSdefault s))
284  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
285  (ls:labeled_statements) on ls : Q ls ≝
286match ls with
287[ LSdefault s ⇒ LSd s
288    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
289| LScase sz i s t ⇒ LSc sz i s t
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)
292].
293
294definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
295  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
296  (λ_,_. I) (λ_,_,_,_,_,_.I).
297
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
305record function : Type[0] ≝ {
306  fn_return: type;
307  fn_params: list (ident × type);
308  fn_vars: list (ident × type);
309  fn_body: statement
310}.
311
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. *)
315
316inductive clight_fundef : Type[0] ≝
317  | CL_Internal: function → clight_fundef
318  | CL_External: ident → typelist → type → clight_fundef.
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
326definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).
327
328(* * * Operations over types *)
329
330(* * The type of a function definition. *)
331
332let rec type_of_params (params: list (ident × type)) : typelist ≝
333  match params with
334  [ nil ⇒ Tnil
335  | cons h rem ⇒ let 〈id,ty〉 ≝ h in Tcons ty (type_of_params rem)
336  ].
337
338definition type_of_function : function → type ≝ λf.
339  Tfunction (type_of_params (fn_params f)) (fn_return f).
340
341definition type_of_fundef : clight_fundef → type ≝ λf.
342  match f with
343  [ CL_Internal fd ⇒ type_of_function fd
344  | CL_External id args res ⇒ Tfunction args res
345  ].
346
347(* * Natural alignment of a type, in bytes. *)
348let rec alignof (t: type) : nat ≝ (*1*)
349(* these are old values for 32 bit machines *)
350  match t with
351  [ Tvoid ⇒ 1
352  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
353  | Tpointer _ ⇒ 4
354  | Tarray t' n ⇒ alignof t'
355  | Tfunction _ _ ⇒ 1
356  | Tstruct _ fld ⇒ alignof_fields fld
357  | Tunion _ fld ⇒ alignof_fields fld
358  | Tcomp_ptr _ ⇒ 4
359  ]
360
361and alignof_fields (f: fieldlist) : nat ≝
362  match f with
363  [ Fnil ⇒ 1
364  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
365  ].
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? *)
373let rec type_ind2
374  (P:type → Prop) (Q:fieldlist → Prop)
375  (vo:P Tvoid)
376  (it:∀i,s. P (Tint i s))
377  (pt:∀t. P t → P (Tpointer t))
378  (ar:∀t,n. P t → P (Tarray t n))
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))
382  (cp:∀i. P (Tcomp_ptr i))
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
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)
394  | Tcomp_ptr i ⇒ cp i
395  ]
396and fieldlist_ind2
397  (P:type → Prop) (Q:fieldlist → Prop)
398  (vo:P Tvoid)
399  (it:∀i,s. P (Tint i s))
400  (pt:∀t. P t → P (Tpointer t))
401  (ar:∀t,n. P t → P (Tarray t n))
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))
405  (cp:∀i. P (Tcomp_ptr i))
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
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')
413  ].
414
415lemma alignof_fields_pos:
416  ∀f. alignof_fields f > 0.
417@fieldlist_ind //;
418#i #t #fs' #IH @max_r @IH qed.
419
420lemma alignof_pos:
421  ∀t. alignof t > 0.
422#t elim t; normalize; //;
423[ 1,2: #z cases z; /2/;
424| 3,4: #i @alignof_fields_pos
425] qed.
426
427(* * Size of a type, in bytes. *)
428
429let rec sizeof (t: type) : nat ≝
430  match t with
431  [ Tvoid ⇒ 1
432  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
433  | Tpointer _ ⇒ size_pointer
434  | Tarray t' n ⇒ sizeof t' * max 1 n
435  | Tfunction _ _ ⇒ 1
436  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
437  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
438  | Tcomp_ptr _ ⇒ size_pointer
439  ]
440
441and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat ≝
442  match fld with
443  [ Fnil ⇒ pos
444  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
445  ]
446
447and sizeof_union (fld: fieldlist) : nat ≝
448  match fld with
449  [ Fnil ⇒ 0
450  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
451  ].
452(* TODO: needs some Z_times results
453lemma sizeof_pos:
454  ∀t. sizeof t > 0.
455#t0
456napply (type_ind2 (λt. sizeof t > 0)
457                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
458[ 1,4,6,9: //;
459| #i cases i;#s //;
460| #f cases f;//
461| #t #n #H whd in ⊢ (?%?);
462Proof.
463  intro t0.
464  apply (type_ind2 (fun t => sizeof t > 0)
465                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
466  intros; simpl; auto; try omega.
467  destruct i; omega.
468  destruct f; omega.
469  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
470  destruct H.
471  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
472  generalize (Zmax1 1 (sizeof_struct f 0)). omega.
473  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
474  generalize (Zmax1 1 (sizeof_union f)). omega.
475  split. omega. auto.
476  destruct H0. split; intros.
477  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
478  apply H1.
479  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
480Qed.
481
482Lemma sizeof_struct_incr:
483  forall fld pos, pos <= sizeof_struct fld pos.
484Proof.
485  induction fld; intros; simpl. omega.
486  eapply Zle_trans. 2: apply IHfld.
487  apply Zle_trans with (align pos (alignof t)).
488  apply align_le. apply alignof_pos.
489  assert (sizeof t > 0) by apply sizeof_pos. omega.
490Qed.
491
492(** Byte offset for a field in a struct or union.
493  Field are laid out consecutively, and padding is inserted
494  to align each field to the natural alignment for its type. *)
495
496Open Local Scope string_scope.
497*)
498
499let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
500                              on fld : res nat ≝
501  match fld with
502  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
503  | Fcons id' t fld' ⇒
504      match ident_eq id id' with
505      [ inl _ ⇒ OK ? (align pos (alignof t))
506      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
507      ]
508  ].
509
510definition field_offset ≝ λid: ident. λfld: fieldlist.
511  field_offset_rec id fld 0.
512
513let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
514  match fld with
515  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
516  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
517  ].
518
519(* * Some sanity checks about field offsets.  First, field offsets are
520  within the range of acceptable offsets. *)
521(*
522Remark field_offset_rec_in_range:
523  forall id ofs ty fld pos,
524  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
525  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
526Proof.
527  intros until ty. induction fld; simpl.
528  congruence.
529  destruct (ident_eq id i); intros.
530  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
531  exploit IHfld; eauto. intros [A B]. split; auto.
532  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
533  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
534Qed.
535
536Lemma field_offset_in_range:
537  forall id fld ofs ty,
538  field_offset id fld = OK ofs → field_type id fld = OK ty →
539  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
540Proof.
541  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
542Qed.
543
544(** Second, two distinct fields do not overlap *)
545
546Lemma field_offset_no_overlap:
547  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
548  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
549  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
550  id1 <> id2 →
551  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
552Proof.
553  intros until ty2. intros fld0 A B C D NEQ.
554  assert (forall fld pos,
555  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
556  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
557  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
558  induction fld; intro pos; simpl. congruence.
559  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
560  congruence.
561  subst i. intros. inv H; inv H0.
562  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
563  subst i. intros. inv H1; inv H2.
564  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
565  intros. eapply IHfld; eauto.
566
567  apply H with fld0 0; auto.
568Qed.
569
570(** Third, if a struct is a prefix of another, the offsets of fields
571  in common is the same. *)
572
573Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
574  match fld1 with
575  | Fnil ⇒ fld2
576  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
577  end.
578
579Lemma field_offset_prefix:
580  forall id ofs fld2 fld1,
581  field_offset id fld1 = OK ofs →
582  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
583Proof.
584  intros until fld2.
585  assert (forall fld1 pos,
586    field_offset_rec id fld1 pos = OK ofs ->
587    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
588  induction fld1; intros pos; simpl. congruence.
589  destruct (ident_eq id i); auto.
590  intros. unfold field_offset; auto.
591Qed.
592*)
593
594
595(* * Translating Clight types to Cminor types, function signatures,
596  and external functions. *)
597
598definition typ_of_type : type → typ ≝ λt.
599  match t with
600  [ Tvoid ⇒ ASTint I32 Unsigned
601  | Tint sz sg ⇒ ASTint sz sg
602  | Tpointer _ ⇒ ASTptr
603  | Tarray _ _ ⇒ ASTptr
604  | Tfunction _ _ ⇒ ASTptr
605  | Tcomp_ptr _ ⇒ ASTptr
606  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
607  ].
608
609definition opttyp_of_type : type → option typ ≝ λt.
610  match t with
611  [ Tvoid ⇒ None ?
612  | Tint sz sg ⇒ Some ? (ASTint sz sg)
613  | Tpointer _ ⇒ Some ? ASTptr
614  | Tarray _ _ ⇒ Some ? ASTptr
615  | Tfunction _ _ ⇒ Some ? ASTptr
616  | Tcomp_ptr _ ⇒ Some ? ASTptr
617  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
618  ].
619
620let rec typlist_of_typelist (tl: typelist) : list typ ≝
621  match tl with
622  [ Tnil ⇒ nil ?
623  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
624  ].
625
626
627(* * The [access_mode] function describes how a variable of the given
628type must be accessed:
629- [By_value ch]: access by value, i.e. by loading from the address
630  of the variable using the memory chunk [ch];
631- [By_reference]: access by reference, i.e. by just returning
632  the address of the variable;
633- [By_nothing]: no access is possible, e.g. for the [void] type.
634
635We currently do not support 64-bit integers and 128-bit floats, so these
636have an access mode of [By_nothing].
637*)
638
639inductive mode: typ → Type[0] ≝
640  | By_value: ∀t:typ. mode t
641  | By_reference: (*∀r:region.*) mode ASTptr
642  | By_nothing: ∀t. mode t.
643
644definition access_mode : ∀ty. mode (typ_of_type ty) ≝ λty.
645  match ty return λty. mode (typ_of_type ty) with
646  [ Tint i s ⇒ By_value (ASTint i s)
647  | Tvoid ⇒ By_nothing …
648  | Tpointer _ ⇒ By_value ASTptr
649  | Tarray _ _ ⇒ By_reference
650  | Tfunction _ _ ⇒ By_reference
651  | Tstruct _ fList ⇒ By_nothing …
652  | Tunion _ fList ⇒ By_nothing …
653  | Tcomp_ptr _ ⇒ By_value ASTptr
654  ].
655
656definition signature_of_type : typelist → type → signature ≝ λargs. λres.
657  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
658
659definition external_function
660    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
661  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.