source: C-semantics/Csyntax.ma @ 156

Last change on this file since 156 was 156, checked in by campbell, 10 years ago

pdata support

File size: 33.8 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
18include "Integers.ma".
19include "AST.ma".
20include "Coqlib.ma".
21include "Errors.ma".
22
23(* * * Abstract syntax *)
24
25(* * ** Types *)
26
27(* * Clight types are similar to those of C.  They include numeric types,
28  pointers, arrays, function types, and composite types (struct and
29  union).  Numeric types (integers and floats) fully specify the
30  bit size of the type.  An integer type is a pair of a signed/unsigned
31  flag and a bit size: 8, 16 or 32 bits. *)
32
33ninductive signedness : Type ≝
34  | Signed: signedness
35  | Unsigned: signedness.
36
37ninductive intsize : Type ≝
38  | I8: intsize
39  | I16: intsize
40  | I32: intsize.
41
42(* * Float types come in two sizes: 32 bits (single precision)
43  and 64-bit (double precision). *)
44
45ninductive floatsize : Type ≝
46  | F32: floatsize
47  | F64: floatsize.
48
49(* * The syntax of type expressions.  Some points to note:
50- Array types [Tarray n] carry the size [n] of the array.
51  Arrays with unknown sizes are represented by pointer types.
52- Function types [Tfunction targs tres] specify the number and types
53  of the function arguments (list [targs]), and the type of the
54  function result ([tres]).  Variadic functions and old-style unprototyped
55  functions are not supported.
56- In C, struct and union types are named and compared by name.
57  This enables the definition of recursive struct types such as
58<<
59  struct s1 { int n; struct * s1 next; };
60>>
61  Note that recursion within types must go through a pointer type.
62  For instance, the following is not allowed in C.
63<<
64  struct s2 { int n; struct s2 next; };
65>>
66  In Clight, struct and union types [Tstruct id fields] and
67  [Tunion id fields] are compared by structure: the [fields]
68  argument gives the names and types of the members.  The identifier
69  [id] is a local name which can be used in conjuction with the
70  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr id]
71  stands for a pointer type to the nearest enclosing [Tstruct]
72  or [Tunion] type named [id].  For instance. the structure [s1]
73  defined above in C is expressed by
74<<
75  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
76               (Fcons "next" (Tcomp_ptr "id")
77               Fnil))
78>>
79  Note that the incorrect structure [s2] above cannot be expressed at
80  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
81  structure or union, but not to the structure or union directly.
82*)
83
84ninductive type : Type ≝
85  | Tvoid: type                         (**r the [void] type *)
86  | Tint: intsize → signedness → type   (**r integer types *)
87  | Tfloat: floatsize → type            (**r floating-point types *)
88  | Tpointer: memory_space → type → type   (**r pointer types ([*ty]) *)
89  | Tarray: memory_space → type → Z → type (**r array types ([ty[len]]) *)
90  | Tfunction: typelist → type → type   (**r function types *)
91  | Tstruct: ident → fieldlist → type   (**r struct types *)
92  | Tunion: ident → fieldlist → type    (**r union types *)
93  | Tcomp_ptr: ident → type             (**r pointer to named struct or union *)
94
95with typelist : Type ≝
96  | Tnil: typelist
97  | Tcons: type → typelist → typelist
98
99with fieldlist : Type ≝
100  | Fnil: fieldlist
101  | Fcons: ident → type → fieldlist → fieldlist.
102
103(* XXX: no induction scheme! *)
104nlet rec type_ind
105  (P:type → Prop)
106  (vo:P Tvoid)
107  (it:∀i,s. P (Tint i s))
108  (fl:∀f. P (Tfloat f))
109  (pt:∀s,t. P t → P (Tpointer s t))
110  (ar:∀s,t,n. P t → P (Tarray s t n))
111  (fn:∀tl,t. P t → P (Tfunction tl t))
112  (st:∀i,fl. P (Tstruct i fl))
113  (un:∀i,fl. P (Tunion i fl))
114  (cp:∀i. P (Tcomp_ptr i))
115  (t:type) on t : P t ≝
116  match t return λt'.P t' with
117  [ Tvoid ⇒ vo
118  | Tint i s ⇒ it i s
119  | Tfloat s ⇒ fl s
120  | Tpointer s t' ⇒ pt s t' (type_ind P vo it fl pt ar fn st un cp t')
121  | Tarray s t' n ⇒ ar s t' n (type_ind P vo it fl pt ar fn st un cp t')
122  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
123  | Tstruct i fs ⇒ st i fs
124  | Tunion i fs ⇒ un i fs
125  | Tcomp_ptr i ⇒ cp i
126  ].
127 
128nlet rec fieldlist_ind
129  (P:fieldlist → Prop)
130  (nl:P Fnil)
131  (cs:∀i,t,fs. P fs → P (Fcons i t fs))
132  (fs:fieldlist) on fs : P fs ≝
133  match fs with
134  [ Fnil ⇒ nl
135  | Fcons i t fs' ⇒ cs i t fs' (fieldlist_ind P nl cs fs')
136  ].
137
138(* * ** Expressions *)
139
140(* * Arithmetic and logical operators. *)
141
142ninductive unary_operation : Type ≝
143  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
144  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
145  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
146
147ninductive binary_operation : Type ≝
148  | Oadd : binary_operation             (**r addition (binary [+]) *)
149  | Osub : binary_operation             (**r subtraction (binary [-]) *)
150  | Omul : binary_operation             (**r multiplication (binary [*]) *)
151  | Odiv : binary_operation             (**r division ([/]) *)
152  | Omod : binary_operation             (**r remainder ([%]) *)
153  | Oand : binary_operation             (**r bitwise and ([&]) *)
154  | Oor : binary_operation              (**r bitwise or ([|]) *)
155  | Oxor : binary_operation             (**r bitwise xor ([^]) *)
156  | Oshl : binary_operation             (**r left shift ([<<]) *)
157  | Oshr : binary_operation             (**r right shift ([>>]) *)
158  | Oeq: binary_operation               (**r comparison ([==]) *)
159  | One: binary_operation               (**r comparison ([!=]) *)
160  | Olt: binary_operation               (**r comparison ([<]) *)
161  | Ogt: binary_operation               (**r comparison ([>]) *)
162  | Ole: binary_operation               (**r comparison ([<=]) *)
163  | Oge: binary_operation.              (**r comparison ([>=]) *)
164
165(* * Clight expressions are a large subset of those of C.
166  The main omissions are string literals and assignment operators
167  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
168  not an expression. 
169
170  All expressions are annotated with their types.  An expression
171  (type [expr]) is therefore a pair of a type and an expression
172  description (type [expr_descr]).
173*)
174
175ninductive expr : Type ≝
176  | Expr: expr_descr → type → expr
177
178with expr_descr : Type ≝
179  | Econst_int: int → expr_descr       (**r integer literal *)
180  | Econst_float: float → expr_descr   (**r float literal *)
181  | Evar: ident → expr_descr           (**r variable *)
182  | Ederef: expr → expr_descr          (**r pointer dereference (unary [*]) *)
183  | Eaddrof: expr → expr_descr         (**r address-of operator ([&]) *)
184  | Eunop: unary_operation → expr → expr_descr  (**r unary operation *)
185  | Ebinop: binary_operation → expr → expr → expr_descr (**r binary operation *)
186  | Ecast: type → expr → expr_descr    (**r type cast ([(ty) e]) *)
187  | Econdition: expr → expr → expr → expr_descr (**r conditional ([e1 ? e2 : e3]) *)
188  | Eandbool: expr → expr → expr_descr (**r sequential and ([&&]) *)
189  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
190  | Esizeof: type → expr_descr         (**r size of a type *)
191  | Efield: expr → ident → expr_descr. (**r access to a member of a struct or union *)
192
193(* * Extract the type part of a type-annotated Clight expression. *)
194
195ndefinition typeof : expr → type ≝ λe.
196  match e with [ Expr de te ⇒ te ].
197
198(* * ** Statements *)
199
200(* * Clight statements include all C statements.
201  Only structured forms of [switch] are supported; moreover,
202  the [default] case must occur last.  Blocks and block-scoped declarations
203  are not supported. *)
204
205ndefinition label ≝ ident.
206
207ninductive statement : Type ≝
208  | Sskip : statement                   (**r do nothing *)
209  | Sassign : expr → expr → statement   (**r assignment [lvalue = rvalue] *)
210  | Scall: option expr → expr → list expr → statement (**r function call *)
211  | Ssequence : statement → statement → statement  (**r sequence *)
212  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
213  | Swhile : expr → statement → statement   (**r [while] loop *)
214  | Sdowhile : expr → statement → statement (**r [do] loop *)
215  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
216  | Sbreak : statement                      (**r [break] statement *)
217  | Scontinue : statement                   (**r [continue] statement *)
218  | Sreturn : option expr → statement       (**r [return] statement *)
219  | Sswitch : expr → labeled_statements → statement  (**r [switch] statement *)
220  | Slabel : label → statement → statement
221  | Sgoto : label → statement
222
223with labeled_statements : Type ≝            (**r cases of a [switch] *)
224  | LSdefault: statement → labeled_statements
225  | LScase: int → statement → labeled_statements → labeled_statements.
226
227nlet rec statement_ind2
228  (P:statement → Prop) (Q:labeled_statements → Prop)
229  (Ssk:P Sskip)
230  (Sas:∀e1,e2. P (Sassign e1 e2))
231  (Sca:∀eo,e,args. P (Scall eo e args))
232  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
233  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
234  (Swh:∀e,s. P s → P (Swhile e s))
235  (Sdo:∀e,s. P s → P (Sdowhile e s))
236  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
237  (Sbr:P Sbreak)
238  (Sco:P Scontinue)
239  (Sre:∀eo. P (Sreturn eo))
240  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
241  (Sla:∀l,s. P s → P (Slabel l s))
242  (Sgo:∀l. P (Sgoto l))
243  (LSd:∀s. P s → Q (LSdefault s))
244  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
245  (s:statement) on s : P s ≝
246match s with
247[ Sskip ⇒ Ssk
248| Sassign e1 e2 ⇒ Sas e1 e2
249| Scall eo e args ⇒ Sca eo e args
250| Ssequence s1 s2 ⇒ Ssq s1 s2
251    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
253| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
254    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
255    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
256| Swhile e s ⇒ Swh e s
257    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
258| Sdowhile e s ⇒ Sdo e s
259    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
260| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
261    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s1)
262    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s2)
263    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s3)
264| Sbreak ⇒ Sbr
265| Scontinue ⇒ Sco
266| Sreturn eo ⇒ Sre eo
267| Sswitch e ls ⇒ Ssw e ls
268    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc ls)
269| Slabel l s ⇒ Sla l s
270    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
271| Sgoto l ⇒ Sgo l
272]
273and labeled_statements_ind2
274  (P:statement → Prop) (Q:labeled_statements → Prop)
275  (Ssk:P Sskip)
276  (Sas:∀e1,e2. P (Sassign e1 e2))
277  (Sca:∀eo,e,args. P (Scall eo e args))
278  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
279  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
280  (Swh:∀e,s. P s → P (Swhile e s))
281  (Sdo:∀e,s. P s → P (Sdowhile e s))
282  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
283  (Sbr:P Sbreak)
284  (Sco:P Scontinue)
285  (Sre:∀eo. P (Sreturn eo))
286  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
287  (Sla:∀l,s. P s → P (Slabel l s))
288  (Sgo:∀l. P (Sgoto l))
289  (LSd:∀s. P s → Q (LSdefault s))
290  (LSc:∀i,s,t. P s → Q t → Q (LScase i s t))
291  (ls:labeled_statements) on ls : Q ls ≝
292match ls with
293[ LSdefault s ⇒ LSd s
294    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
295| LScase i s t ⇒ LSc i s t
296    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc s)
297    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo LSd LSc t)
298].
299
300ndefinition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo.
301  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo
302  (λ_,_. I) (λ_,_,_,_,_.I).
303
304(* * ** Functions *)
305
306(* * A function definition is composed of its return type ([fn_return]),
307  the names and types of its parameters ([fn_params]), the names
308  and types of its local variables ([fn_vars]), and the body of the
309  function (a statement, [fn_body]). *)
310
311nrecord function : Type ≝ {
312  fn_return: type;
313  fn_params: list (ident × type);
314  fn_vars: list (ident × type);
315  fn_body: statement
316}.
317
318(* * Functions can either be defined ([Internal]) or declared as
319  external functions ([External]). *)
320
321ninductive fundef : Type ≝
322  | Internal: function → fundef
323  | External: ident → typelist → type → fundef.
324
325(* * ** Programs *)
326
327(* * A program is a collection of named functions, plus a collection
328  of named global variables, carrying their types and optional initialization
329  data.  See module [AST] for more details. *)
330
331ndefinition program : Type ≝ program fundef type.
332
333(* * * Operations over types *)
334
335(* * The type of a function definition. *)
336
337nlet rec type_of_params (params: list (ident × type)) : typelist ≝
338  match params with
339  [ nil ⇒ Tnil
340  | cons h rem ⇒ match h with [ mk_pair id ty ⇒ Tcons ty (type_of_params rem) ]
341  ].
342
343ndefinition type_of_function : function → type ≝ λf.
344  Tfunction (type_of_params (fn_params f)) (fn_return f).
345
346ndefinition type_of_fundef : fundef → type ≝ λf.
347  match f with
348  [ Internal fd ⇒ type_of_function fd
349  | External id args res ⇒ Tfunction args res
350  ].
351
352(* * Natural alignment of a type, in bytes. *)
353
354nlet rec alignof (t: type) : Z ≝
355  match t return λ_.Z (* XXX appears to infer nat otherwise *) with
356  [ Tvoid ⇒ 1
357  | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
358  | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
359  | Tpointer _ _ ⇒ 4
360  | Tarray _ t' n ⇒ alignof t'
361  | Tfunction _ _ ⇒ 1
362  | Tstruct _ fld ⇒ alignof_fields fld
363  | Tunion _ fld ⇒ alignof_fields fld
364  | Tcomp_ptr _ ⇒ 4
365  ]
366
367and alignof_fields (f: fieldlist) : Z ≝
368  match f with
369  [ Fnil ⇒ 1
370  | Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f')
371  ].
372
373(*
374Scheme type_ind2 := Induction for type Sort Prop
375  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
376*)
377
378(* XXX: automatic generation? *)
379nlet rec type_ind2
380  (P:type → Prop) (Q:fieldlist → Prop)
381  (vo:P Tvoid)
382  (it:∀i,s. P (Tint i s))
383  (fl:∀f. P (Tfloat f))
384  (pt:∀s,t. P t → P (Tpointer s t))
385  (ar:∀s,t,n. P t → P (Tarray s t n))
386  (fn:∀tl,t. P t → P (Tfunction tl t))
387  (st:∀i,fl. Q fl → P (Tstruct i fl))
388  (un:∀i,fl. Q fl → P (Tunion i fl))
389  (cp:∀i. P (Tcomp_ptr i))
390  (nl:Q Fnil)
391  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
392 (t:type) on t : P t ≝
393  match t return λt'.P t' with
394  [ Tvoid ⇒ vo
395  | Tint i s ⇒ it i s
396  | Tfloat s ⇒ fl s
397  | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
398  | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
399  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
400  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
401  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
402  | Tcomp_ptr i ⇒ cp i
403  ]
404and fieldlist_ind2
405  (P:type → Prop) (Q:fieldlist → Prop)
406  (vo:P Tvoid)
407  (it:∀i,s. P (Tint i s))
408  (fl:∀f. P (Tfloat f))
409  (pt:∀s,t. P t → P (Tpointer s t))
410  (ar:∀s,t,n. P t → P (Tarray s t n))
411  (fn:∀tl,t. P t → P (Tfunction tl t))
412  (st:∀i,fl. Q fl → P (Tstruct i fl))
413  (un:∀i,fl. Q fl → P (Tunion i fl))
414  (cp:∀i. P (Tcomp_ptr i))
415  (nl:Q Fnil)
416  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
417  (fs:fieldlist) on fs : Q fs ≝
418  match fs return λfs'.Q fs' with
419  [ Fnil ⇒ nl
420  | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t)
421                        (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs f')
422  ].
423
424nlemma alignof_fields_pos:
425  ∀f. alignof_fields f > 0.
426napply fieldlist_ind; //;
427#i;#t;#fs';#IH; nlapply (Zmax_r (alignof t) (alignof_fields fs'));
428napply Zlt_to_Zle_to_Zlt; //; nqed.
429
430nlemma alignof_pos:
431  ∀t. alignof t > 0.
432#t;nelim t; nnormalize; //;
433##[ ##1,2: #z; ncases z; //;
434##| ##3,4: #i;napply alignof_fields_pos
435##] nqed.
436
437(* * Size of a type, in bytes. *)
438
439ndefinition sizeof_pointer : memory_space → Z ≝
440λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
441
442nlet rec sizeof (t: type) : Z ≝
443  match t return λ_.Z with
444  [ Tvoid ⇒ 1
445  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
446  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
447  | Tpointer sp _ ⇒ sizeof_pointer sp
448  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
449  | Tfunction _ _ ⇒ 1
450  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
451  | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
452  | Tcomp_ptr _ ⇒ 4
453  ]
454
455and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z ≝
456  match fld with
457  [ Fnil ⇒ pos
458  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
459  ]
460
461and sizeof_union (fld: fieldlist) : Z ≝
462  match fld with
463  [ Fnil ⇒ 0
464  | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')
465  ].
466(* TODO: needs some Z_times results
467nlemma sizeof_pos:
468  ∀t. sizeof t > 0.
469#t0;
470napply (type_ind2 (λt. sizeof t > 0)
471                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
472##[ ##1,4,6,9: //;
473##| #i;ncases i;#s;//;
474##| #f;ncases f;//
475##| #t;#n;#H; nwhd in ⊢ (?%?);
476Proof.
477  intro t0.
478  apply (type_ind2 (fun t => sizeof t > 0)
479                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
480  intros; simpl; auto; try omega.
481  destruct i; omega.
482  destruct f; omega.
483  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
484  destruct H.
485  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
486  generalize (Zmax1 1 (sizeof_struct f 0)). omega.
487  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
488  generalize (Zmax1 1 (sizeof_union f)). omega.
489  split. omega. auto.
490  destruct H0. split; intros.
491  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
492  apply H1.
493  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
494Qed.
495
496Lemma sizeof_struct_incr:
497  forall fld pos, pos <= sizeof_struct fld pos.
498Proof.
499  induction fld; intros; simpl. omega.
500  eapply Zle_trans. 2: apply IHfld.
501  apply Zle_trans with (align pos (alignof t)).
502  apply align_le. apply alignof_pos.
503  assert (sizeof t > 0) by apply sizeof_pos. omega.
504Qed.
505
506(** Byte offset for a field in a struct or union.
507  Field are laid out consecutively, and padding is inserted
508  to align each field to the natural alignment for its type. *)
509
510Open Local Scope string_scope.
511*)
512nlet rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
513                              on fld : res Z ≝
514  match fld with
515  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
516  | Fcons id' t fld' ⇒
517      match ident_eq id id' with
518      [ inl _ ⇒ OK ? (align pos (alignof t))
519      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
520      ]
521  ].
522
523ndefinition field_offset ≝ λid: ident. λfld: fieldlist.
524  field_offset_rec id fld 0.
525
526nlet rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
527  match fld with
528  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
529  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
530  ].
531
532(* * Some sanity checks about field offsets.  First, field offsets are
533  within the range of acceptable offsets. *)
534(*
535Remark field_offset_rec_in_range:
536  forall id ofs ty fld pos,
537  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
538  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
539Proof.
540  intros until ty. induction fld; simpl.
541  congruence.
542  destruct (ident_eq id i); intros.
543  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
544  exploit IHfld; eauto. intros [A B]. split; auto.
545  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
546  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
547Qed.
548
549Lemma field_offset_in_range:
550  forall id fld ofs ty,
551  field_offset id fld = OK ofs → field_type id fld = OK ty →
552  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
553Proof.
554  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
555Qed.
556
557(** Second, two distinct fields do not overlap *)
558
559Lemma field_offset_no_overlap:
560  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
561  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
562  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
563  id1 <> id2 →
564  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
565Proof.
566  intros until ty2. intros fld0 A B C D NEQ.
567  assert (forall fld pos,
568  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
569  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
570  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
571  induction fld; intro pos; simpl. congruence.
572  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
573  congruence.
574  subst i. intros. inv H; inv H0.
575  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
576  subst i. intros. inv H1; inv H2.
577  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
578  intros. eapply IHfld; eauto.
579
580  apply H with fld0 0; auto.
581Qed.
582
583(** Third, if a struct is a prefix of another, the offsets of fields
584  in common is the same. *)
585
586Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
587  match fld1 with
588  | Fnil ⇒ fld2
589  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
590  end.
591
592Lemma field_offset_prefix:
593  forall id ofs fld2 fld1,
594  field_offset id fld1 = OK ofs →
595  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
596Proof.
597  intros until fld2.
598  assert (forall fld1 pos,
599    field_offset_rec id fld1 pos = OK ofs ->
600    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
601  induction fld1; intros pos; simpl. congruence.
602  destruct (ident_eq id i); auto.
603  intros. unfold field_offset; auto.
604Qed.
605*)
606(* * The [access_mode] function describes how a variable of the given
607type must be accessed:
608- [By_value ch]: access by value, i.e. by loading from the address
609  of the variable using the memory chunk [ch];
610- [By_reference]: access by reference, i.e. by just returning
611  the address of the variable;
612- [By_nothing]: no access is possible, e.g. for the [void] type.
613
614We currently do not support 64-bit integers and 128-bit floats, so these
615have an access mode of [By_nothing].
616*)
617
618ninductive mode: Type ≝
619  | By_value: memory_chunk → mode
620  | By_reference: mode
621  | By_nothing: mode.
622
623ndefinition access_mode : type → mode ≝ λty.
624  match ty with
625  [ Tint i s ⇒
626    match i with [ I8 ⇒
627      match s with [ Signed ⇒ By_value Mint8signed
628                   | Unsigned ⇒ By_value Mint8unsigned ]
629                 | I16 ⇒
630      match s with [ Signed ⇒ By_value Mint16signed
631                   | Unsigned ⇒ By_value Mint16unsigned ]
632                 | I32 ⇒ By_value Mint32 ]
633  | Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32
634                            | F64 ⇒ By_value Mfloat64 ]
635  | Tvoid ⇒ By_nothing
636  | Tpointer sp _ ⇒ By_value (match sp with [ Any ⇒ Mint24 | Data ⇒ Mint8unsigned | IData ⇒ Mint8unsigned | PData ⇒ Mint8unsigned | XData ⇒ Mint16unsigned | Code ⇒ Mint16unsigned ])
637  | Tarray _ _ _ ⇒ By_reference
638  | Tfunction _ _ ⇒ By_reference
639  | Tstruct _ fList ⇒ By_nothing
640  | Tunion _ fList ⇒ By_nothing
641  | Tcomp_ptr _ ⇒ By_value Mint32
642  ].
643
644(* * Classification of arithmetic operations and comparisons.
645  The following [classify_] functions take as arguments the types
646  of the arguments of an operation.  They return enough information
647  to resolve overloading for this operator applications, such as
648  ``both arguments are floats'', or ``the first is a pointer
649  and the second is an integer''.  These functions are used to resolve
650  overloading both in the dynamic semantics (module [Csem]) and in the
651  compiler (module [Cshmgen]).
652*)
653
654ninductive classify_add_cases : Type ≝
655  | add_case_ii: classify_add_cases         (**r int , int *)
656  | add_case_ff: classify_add_cases         (**r float , float *)
657  | add_case_pi: type → classify_add_cases (**r ptr or array, int *)
658  | add_case_ip: type → classify_add_cases (**r int, ptr or array *)
659  | add_default: classify_add_cases.        (**r other *)
660
661ndefinition classify_add ≝ λty1: type. λty2: type.
662(*
663  match ty1, ty2 with
664  [ Tint _ _, Tint _ _ ⇒ add_case_ii
665  | Tfloat _, Tfloat _ ⇒ add_case_ff
666  | Tpointer ty, Tint _ _ ⇒ add_case_pi ty
667  | Tarray ty _, Tint _ _ ⇒ add_case_pi ty
668  | Tint _ _, Tpointer ty ⇒ add_case_ip ty
669  | Tint _ _, Tarray ty _ ⇒ add_case_ip ty
670  | _, _ ⇒ add_default
671  ].
672*)
673  match ty1 with
674  [ Tint _ _ ⇒
675    match ty2 with
676    [ Tint _ _ ⇒ add_case_ii
677    | Tpointer _ ty ⇒ add_case_ip ty
678    | Tarray _ ty _ ⇒ add_case_ip ty
679    | _ ⇒ add_default ]
680  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
681  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
682  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
683  | _ ⇒ add_default
684  ].
685
686ninductive classify_sub_cases : Type ≝
687  | sub_case_ii: classify_sub_cases          (**r int , int *)
688  | sub_case_ff: classify_sub_cases          (**r float , float *)
689  | sub_case_pi: type → classify_sub_cases  (**r ptr or array , int *)
690  | sub_case_pp: type → classify_sub_cases  (**r ptr or array , ptr or array *)
691  | sub_default: classify_sub_cases .        (**r other *)
692
693ndefinition classify_sub ≝ λty1: type. λty2: type.
694(*  match ty1, ty2 with
695  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
696  | Tfloat _ , Tfloat _ ⇒ sub_case_ff
697  | Tpointer ty , Tint _ _ ⇒ sub_case_pi ty
698  | Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty
699  | Tpointer ty , Tpointer _ ⇒ sub_case_pp ty
700  | Tpointer ty , Tarray _ _⇒ sub_case_pp ty
701  | Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty
702  | Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty
703  | _ ,_ ⇒ sub_default
704  end.
705*)
706  match ty1 with
707  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
708  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
709  | Tpointer _ ty ⇒
710    match ty2 with
711    [ Tint _ _ ⇒ sub_case_pi ty
712    | Tpointer _ _ ⇒ sub_case_pp ty
713    | Tarray _ _ _ ⇒ sub_case_pp ty
714    | _ ⇒ sub_default ]
715  | Tarray _ ty _ ⇒
716    match ty2 with
717    [ Tint _ _ ⇒ sub_case_pi ty
718    | Tpointer _ _ ⇒ sub_case_pp ty
719    | Tarray _ _ _ ⇒ sub_case_pp ty
720    | _ ⇒ sub_default ]
721  | _ ⇒ sub_default
722  ].
723
724ninductive classify_mul_cases : Type ≝
725  | mul_case_ii: classify_mul_cases (**r int , int *)
726  | mul_case_ff: classify_mul_cases (**r float , float *)
727  | mul_default: classify_mul_cases . (**r other *)
728
729ndefinition classify_mul ≝ λty1: type. λty2: type.
730  match ty1 with
731  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
732  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff | _ ⇒ mul_default ]
733  | _ ⇒ mul_default
734  ].
735(*
736  match ty1,ty2 with
737  | Tint _ _, Tint _ _ ⇒ mul_case_ii
738  | Tfloat _ , Tfloat _ ⇒ mul_case_ff
739  | _,_  ⇒ mul_default
740end.
741*)
742ninductive classify_div_cases : Type ≝
743  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
744  | div_case_ii: classify_div_cases    (**r int , int *)
745  | div_case_ff: classify_div_cases    (**r float , float *)
746  | div_default: classify_div_cases. (**r other *)
747
748ndefinition classify_32un_aux ≝ λT:Type.λi.λs.λr1:T.λr2:T.
749  match i with [ I32 ⇒
750    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
751  | _ ⇒ r2 ].
752
753ndefinition classify_div ≝ λty1: type. λty2: type.
754  match ty1 with
755  [ Tint i1 s1 ⇒
756    match ty2 with
757    [ Tint i2 s2 ⇒
758      classify_32un_aux ? i1 s1 div_case_I32unsi
759        (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii)
760    | _ ⇒ div_default ]
761  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff | _ ⇒ div_default ]
762  | _ ⇒ div_default
763  ].
764(*
765ndefinition classify_div ≝ λty1: type. λty2: type.
766  match ty1,ty2 with
767  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi
768  | Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi
769  | Tint _ _ , Tint _ _ ⇒ div_case_ii
770  | Tfloat _ , Tfloat _ ⇒ div_case_ff
771  | _ ,_ ⇒ div_default
772end.
773*)
774ninductive classify_mod_cases : Type ≝
775  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
776  | mod_case_ii: classify_mod_cases  (**r int , int *)
777  | mod_default: classify_mod_cases . (**r other *)
778
779ndefinition classify_mod ≝ λty1:type. λty2:type.
780  match ty1 with
781  [ Tint i1 s1 ⇒
782    match ty2 with
783    [ Tint i2 s2 ⇒
784      classify_32un_aux ? i1 s1 mod_case_I32unsi
785        (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii)
786    | _ ⇒ mod_default ]
787  | _ ⇒ mod_default
788  ].
789(*
790Definition classify_mod (ty1: type) (ty2: type) :=
791  match ty1,ty2 with
792  | Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi
793  | Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi
794  | Tint _ _ , Tint _ _ ⇒ mod_case_ii
795  | _ , _ ⇒ mod_default
796end .
797*)
798ninductive classify_shr_cases :Type ≝
799  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
800  | shr_case_ii :classify_shr_cases (**r int , int *)
801  | shr_default : classify_shr_cases . (**r other *)
802
803ndefinition classify_shr ≝ λty1: type. λty2: type.
804  match ty1 with
805  [ Tint i1 s1 ⇒
806    match ty2 with
807    [ Tint _ _ ⇒
808      classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii
809    | _ ⇒ shr_default ]
810  | _ ⇒ shr_default
811  ].
812
813(*
814Definition classify_shr (ty1: type) (ty2: type) :=
815  match ty1,ty2 with
816  | Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi
817  | Tint _ _ , Tint _ _ ⇒ shr_case_ii
818  | _ , _ ⇒ shr_default
819  end.
820*)
821ninductive classify_cmp_cases : Type ≝
822  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
823  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
824  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
825  | cmp_default: classify_cmp_cases . (**r other *)
826
827ndefinition classify_cmp ≝ λty1:type. λty2:type.
828  match ty1 with
829  [ Tint i1 s1 ⇒
830    match ty2 with
831    [ Tint i2 s2 ⇒
832      classify_32un_aux ? i1 s1 cmp_case_I32unsi
833        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
834    | _ ⇒ cmp_default ]
835  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
836  | Tpointer _ _ ⇒
837    match ty2 with
838    [ Tint _ _ ⇒ cmp_case_ipip
839    | Tpointer _ _ ⇒ cmp_case_ipip
840    | Tarray _ _ _ ⇒ cmp_case_ipip
841    | _ ⇒ cmp_default ]
842  | Tarray _ _ _ ⇒
843    match ty2 with
844    [ Tint _ _ ⇒ cmp_case_ipip
845    | Tpointer _ _ ⇒ cmp_case_ipip
846    | Tarray _ _ _ ⇒ cmp_case_ipip
847    | _ ⇒ cmp_default ]
848  | _ ⇒ cmp_default
849  ].
850
851(*
852Definition classify_cmp (ty1: type) (ty2: type) :=
853  match ty1,ty2 with
854  | Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi
855  | Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi
856  | Tint _ _ , Tint _ _ ⇒ cmp_case_ipip
857  | Tfloat _ , Tfloat _ ⇒ cmp_case_ff
858  | Tpointer _ , Tint _ _ ⇒ cmp_case_ipip
859  | Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip
860  | Tpointer _ , Tpointer _ ⇒ cmp_case_ipip
861  | Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip
862  | Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip
863  | Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip
864  | _ , _ ⇒ cmp_default
865  end.
866*)
867ninductive classify_fun_cases : Type ≝
868  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
869  | fun_default: classify_fun_cases . (**r other *)
870
871ndefinition classify_fun ≝ λty: type.
872  match ty with
873  [ Tfunction args res ⇒ fun_case_f args res
874  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
875                                    | _ ⇒ fun_default
876                                    ]
877  | _ ⇒ fun_default
878  ].
879
880(* * Translating Clight types to Cminor types, function signatures,
881  and external functions. *)
882(* XXX: is this the best way to access these? *)
883alias id "ASTint" = "cic:/matita/c-semantics/AST/typ.con(0,1,0)".
884alias id "ASTfloat" = "cic:/matita/c-semantics/AST/typ.con(0,2,0)".
885
886ndefinition typ_of_type : type → typ ≝ λt.
887  match t with
888  [ Tfloat _ ⇒ ASTfloat
889  | _ ⇒ ASTint
890  ].
891
892ndefinition opttyp_of_type : type → option typ ≝ λt.
893  match t with
894  [ Tvoid ⇒ None ?
895  | Tfloat _ ⇒ Some ? ASTfloat
896  | _ ⇒ Some ? ASTint
897  ].
898
899nlet rec typlist_of_typelist (tl: typelist) : list typ ≝
900  match tl with
901  [ Tnil ⇒ nil ?
902  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
903  ].
904
905ndefinition signature_of_type : typelist → type → signature ≝ λargs. λres.
906  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
907
908ndefinition external_function
909    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
910  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.