source: C-semantics/Csyntax.ma @ 125

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

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

File size: 33.5 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
439nlet rec sizeof (t: type) : Z ≝
440  match t return λ_.Z with
441  [ Tvoid ⇒ 1
442  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
443  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
444  | Tpointer _ _ ⇒ 4
445  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
446  | Tfunction _ _ ⇒ 1
447  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
448  | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
449  | Tcomp_ptr _ ⇒ 4
450  ]
451
452and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z ≝
453  match fld with
454  [ Fnil ⇒ pos
455  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
456  ]
457
458and sizeof_union (fld: fieldlist) : Z ≝
459  match fld with
460  [ Fnil ⇒ 0
461  | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')
462  ].
463(* TODO: needs some Z_times results
464nlemma sizeof_pos:
465  ∀t. sizeof t > 0.
466#t0;
467napply (type_ind2 (λt. sizeof t > 0)
468                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
469##[ ##1,4,6,9: //;
470##| #i;ncases i;#s;//;
471##| #f;ncases f;//
472##| #t;#n;#H; nwhd in ⊢ (?%?);
473Proof.
474  intro t0.
475  apply (type_ind2 (fun t => sizeof t > 0)
476                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
477  intros; simpl; auto; try omega.
478  destruct i; omega.
479  destruct f; omega.
480  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
481  destruct H.
482  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
483  generalize (Zmax1 1 (sizeof_struct f 0)). omega.
484  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
485  generalize (Zmax1 1 (sizeof_union f)). omega.
486  split. omega. auto.
487  destruct H0. split; intros.
488  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
489  apply H1.
490  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
491Qed.
492
493Lemma sizeof_struct_incr:
494  forall fld pos, pos <= sizeof_struct fld pos.
495Proof.
496  induction fld; intros; simpl. omega.
497  eapply Zle_trans. 2: apply IHfld.
498  apply Zle_trans with (align pos (alignof t)).
499  apply align_le. apply alignof_pos.
500  assert (sizeof t > 0) by apply sizeof_pos. omega.
501Qed.
502
503(** Byte offset for a field in a struct or union.
504  Field are laid out consecutively, and padding is inserted
505  to align each field to the natural alignment for its type. *)
506
507Open Local Scope string_scope.
508*)
509nlet rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
510                              on fld : res Z ≝
511  match fld with
512  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
513  | Fcons id' t fld' ⇒
514      match ident_eq id id' with
515      [ inl _ ⇒ OK ? (align pos (alignof t))
516      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
517      ]
518  ].
519
520ndefinition field_offset ≝ λid: ident. λfld: fieldlist.
521  field_offset_rec id fld 0.
522
523nlet rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
524  match fld with
525  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
526  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
527  ].
528
529(* * Some sanity checks about field offsets.  First, field offsets are
530  within the range of acceptable offsets. *)
531(*
532Remark field_offset_rec_in_range:
533  forall id ofs ty fld pos,
534  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
535  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
536Proof.
537  intros until ty. induction fld; simpl.
538  congruence.
539  destruct (ident_eq id i); intros.
540  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
541  exploit IHfld; eauto. intros [A B]. split; auto.
542  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
543  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
544Qed.
545
546Lemma field_offset_in_range:
547  forall id fld ofs ty,
548  field_offset id fld = OK ofs → field_type id fld = OK ty →
549  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
550Proof.
551  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
552Qed.
553
554(** Second, two distinct fields do not overlap *)
555
556Lemma field_offset_no_overlap:
557  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
558  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
559  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
560  id1 <> id2 →
561  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
562Proof.
563  intros until ty2. intros fld0 A B C D NEQ.
564  assert (forall fld pos,
565  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
566  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
567  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
568  induction fld; intro pos; simpl. congruence.
569  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
570  congruence.
571  subst i. intros. inv H; inv H0.
572  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
573  subst i. intros. inv H1; inv H2.
574  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
575  intros. eapply IHfld; eauto.
576
577  apply H with fld0 0; auto.
578Qed.
579
580(** Third, if a struct is a prefix of another, the offsets of fields
581  in common is the same. *)
582
583Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
584  match fld1 with
585  | Fnil ⇒ fld2
586  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
587  end.
588
589Lemma field_offset_prefix:
590  forall id ofs fld2 fld1,
591  field_offset id fld1 = OK ofs →
592  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
593Proof.
594  intros until fld2.
595  assert (forall fld1 pos,
596    field_offset_rec id fld1 pos = OK ofs ->
597    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
598  induction fld1; intros pos; simpl. congruence.
599  destruct (ident_eq id i); auto.
600  intros. unfold field_offset; auto.
601Qed.
602*)
603(* * The [access_mode] function describes how a variable of the given
604type must be accessed:
605- [By_value ch]: access by value, i.e. by loading from the address
606  of the variable using the memory chunk [ch];
607- [By_reference]: access by reference, i.e. by just returning
608  the address of the variable;
609- [By_nothing]: no access is possible, e.g. for the [void] type.
610
611We currently do not support 64-bit integers and 128-bit floats, so these
612have an access mode of [By_nothing].
613*)
614
615ninductive mode: Type ≝
616  | By_value: memory_chunk → mode
617  | By_reference: mode
618  | By_nothing: mode.
619
620ndefinition access_mode : type → mode ≝ λty.
621  match ty with
622  [ Tint i s ⇒
623    match i with [ I8 ⇒
624      match s with [ Signed ⇒ By_value Mint8signed
625                   | Unsigned ⇒ By_value Mint8unsigned ]
626                 | I16 ⇒
627      match s with [ Signed ⇒ By_value Mint16signed
628                   | Unsigned ⇒ By_value Mint16unsigned ]
629                 | I32 ⇒ By_value Mint32 ]
630  | Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32
631                            | F64 ⇒ By_value Mfloat64 ]
632  | Tvoid ⇒ By_nothing
633  | Tpointer _ _ ⇒ By_value Mint32
634  | Tarray _ _ _ ⇒ By_reference
635  | Tfunction _ _ ⇒ By_reference
636  | Tstruct _ fList ⇒ By_nothing
637  | Tunion _ fList ⇒ By_nothing
638  | Tcomp_ptr _ ⇒ By_value Mint32
639  ].
640
641(* * Classification of arithmetic operations and comparisons.
642  The following [classify_] functions take as arguments the types
643  of the arguments of an operation.  They return enough information
644  to resolve overloading for this operator applications, such as
645  ``both arguments are floats'', or ``the first is a pointer
646  and the second is an integer''.  These functions are used to resolve
647  overloading both in the dynamic semantics (module [Csem]) and in the
648  compiler (module [Cshmgen]).
649*)
650
651ninductive classify_add_cases : Type ≝
652  | add_case_ii: classify_add_cases         (**r int , int *)
653  | add_case_ff: classify_add_cases         (**r float , float *)
654  | add_case_pi: type → classify_add_cases (**r ptr or array, int *)
655  | add_case_ip: type → classify_add_cases (**r int, ptr or array *)
656  | add_default: classify_add_cases.        (**r other *)
657
658ndefinition classify_add ≝ λty1: type. λty2: type.
659(*
660  match ty1, ty2 with
661  [ Tint _ _, Tint _ _ ⇒ add_case_ii
662  | Tfloat _, Tfloat _ ⇒ add_case_ff
663  | Tpointer ty, Tint _ _ ⇒ add_case_pi ty
664  | Tarray ty _, Tint _ _ ⇒ add_case_pi ty
665  | Tint _ _, Tpointer ty ⇒ add_case_ip ty
666  | Tint _ _, Tarray ty _ ⇒ add_case_ip ty
667  | _, _ ⇒ add_default
668  ].
669*)
670  match ty1 with
671  [ Tint _ _ ⇒
672    match ty2 with
673    [ Tint _ _ ⇒ add_case_ii
674    | Tpointer _ ty ⇒ add_case_ip ty
675    | Tarray _ ty _ ⇒ add_case_ip ty
676    | _ ⇒ add_default ]
677  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
678  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
679  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
680  | _ ⇒ add_default
681  ].
682
683ninductive classify_sub_cases : Type ≝
684  | sub_case_ii: classify_sub_cases          (**r int , int *)
685  | sub_case_ff: classify_sub_cases          (**r float , float *)
686  | sub_case_pi: type → classify_sub_cases  (**r ptr or array , int *)
687  | sub_case_pp: type → classify_sub_cases  (**r ptr or array , ptr or array *)
688  | sub_default: classify_sub_cases .        (**r other *)
689
690ndefinition classify_sub ≝ λty1: type. λty2: type.
691(*  match ty1, ty2 with
692  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
693  | Tfloat _ , Tfloat _ ⇒ sub_case_ff
694  | Tpointer ty , Tint _ _ ⇒ sub_case_pi ty
695  | Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty
696  | Tpointer ty , Tpointer _ ⇒ sub_case_pp ty
697  | Tpointer ty , Tarray _ _⇒ sub_case_pp ty
698  | Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty
699  | Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty
700  | _ ,_ ⇒ sub_default
701  end.
702*)
703  match ty1 with
704  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
705  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
706  | Tpointer _ ty ⇒
707    match ty2 with
708    [ Tint _ _ ⇒ sub_case_pi ty
709    | Tpointer _ _ ⇒ sub_case_pp ty
710    | Tarray _ _ _ ⇒ sub_case_pp ty
711    | _ ⇒ sub_default ]
712  | Tarray _ ty _ ⇒
713    match ty2 with
714    [ Tint _ _ ⇒ sub_case_pi ty
715    | Tpointer _ _ ⇒ sub_case_pp ty
716    | Tarray _ _ _ ⇒ sub_case_pp ty
717    | _ ⇒ sub_default ]
718  | _ ⇒ sub_default
719  ].
720
721ninductive classify_mul_cases : Type ≝
722  | mul_case_ii: classify_mul_cases (**r int , int *)
723  | mul_case_ff: classify_mul_cases (**r float , float *)
724  | mul_default: classify_mul_cases . (**r other *)
725
726ndefinition classify_mul ≝ λty1: type. λty2: type.
727  match ty1 with
728  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
729  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff | _ ⇒ mul_default ]
730  | _ ⇒ mul_default
731  ].
732(*
733  match ty1,ty2 with
734  | Tint _ _, Tint _ _ ⇒ mul_case_ii
735  | Tfloat _ , Tfloat _ ⇒ mul_case_ff
736  | _,_  ⇒ mul_default
737end.
738*)
739ninductive classify_div_cases : Type ≝
740  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
741  | div_case_ii: classify_div_cases    (**r int , int *)
742  | div_case_ff: classify_div_cases    (**r float , float *)
743  | div_default: classify_div_cases. (**r other *)
744
745ndefinition classify_32un_aux ≝ λT:Type.λi.λs.λr1:T.λr2:T.
746  match i with [ I32 ⇒
747    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
748  | _ ⇒ r2 ].
749
750ndefinition classify_div ≝ λty1: type. λty2: type.
751  match ty1 with
752  [ Tint i1 s1 ⇒
753    match ty2 with
754    [ Tint i2 s2 ⇒
755      classify_32un_aux ? i1 s1 div_case_I32unsi
756        (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii)
757    | _ ⇒ div_default ]
758  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff | _ ⇒ div_default ]
759  | _ ⇒ div_default
760  ].
761(*
762ndefinition classify_div ≝ λty1: type. λty2: type.
763  match ty1,ty2 with
764  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi
765  | Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi
766  | Tint _ _ , Tint _ _ ⇒ div_case_ii
767  | Tfloat _ , Tfloat _ ⇒ div_case_ff
768  | _ ,_ ⇒ div_default
769end.
770*)
771ninductive classify_mod_cases : Type ≝
772  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
773  | mod_case_ii: classify_mod_cases  (**r int , int *)
774  | mod_default: classify_mod_cases . (**r other *)
775
776ndefinition classify_mod ≝ λty1:type. λty2:type.
777  match ty1 with
778  [ Tint i1 s1 ⇒
779    match ty2 with
780    [ Tint i2 s2 ⇒
781      classify_32un_aux ? i1 s1 mod_case_I32unsi
782        (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii)
783    | _ ⇒ mod_default ]
784  | _ ⇒ mod_default
785  ].
786(*
787Definition classify_mod (ty1: type) (ty2: type) :=
788  match ty1,ty2 with
789  | Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi
790  | Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi
791  | Tint _ _ , Tint _ _ ⇒ mod_case_ii
792  | _ , _ ⇒ mod_default
793end .
794*)
795ninductive classify_shr_cases :Type ≝
796  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
797  | shr_case_ii :classify_shr_cases (**r int , int *)
798  | shr_default : classify_shr_cases . (**r other *)
799
800ndefinition classify_shr ≝ λty1: type. λty2: type.
801  match ty1 with
802  [ Tint i1 s1 ⇒
803    match ty2 with
804    [ Tint _ _ ⇒
805      classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii
806    | _ ⇒ shr_default ]
807  | _ ⇒ shr_default
808  ].
809
810(*
811Definition classify_shr (ty1: type) (ty2: type) :=
812  match ty1,ty2 with
813  | Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi
814  | Tint _ _ , Tint _ _ ⇒ shr_case_ii
815  | _ , _ ⇒ shr_default
816  end.
817*)
818ninductive classify_cmp_cases : Type ≝
819  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
820  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
821  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
822  | cmp_default: classify_cmp_cases . (**r other *)
823
824ndefinition classify_cmp ≝ λty1:type. λty2:type.
825  match ty1 with
826  [ Tint i1 s1 ⇒
827    match ty2 with
828    [ Tint i2 s2 ⇒
829      classify_32un_aux ? i1 s1 cmp_case_I32unsi
830        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
831    | _ ⇒ cmp_default ]
832  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
833  | Tpointer _ _ ⇒
834    match ty2 with
835    [ Tint _ _ ⇒ cmp_case_ipip
836    | Tpointer _ _ ⇒ cmp_case_ipip
837    | Tarray _ _ _ ⇒ cmp_case_ipip
838    | _ ⇒ cmp_default ]
839  | Tarray _ _ _ ⇒
840    match ty2 with
841    [ Tint _ _ ⇒ cmp_case_ipip
842    | Tpointer _ _ ⇒ cmp_case_ipip
843    | Tarray _ _ _ ⇒ cmp_case_ipip
844    | _ ⇒ cmp_default ]
845  | _ ⇒ cmp_default
846  ].
847
848(*
849Definition classify_cmp (ty1: type) (ty2: type) :=
850  match ty1,ty2 with
851  | Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi
852  | Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi
853  | Tint _ _ , Tint _ _ ⇒ cmp_case_ipip
854  | Tfloat _ , Tfloat _ ⇒ cmp_case_ff
855  | Tpointer _ , Tint _ _ ⇒ cmp_case_ipip
856  | Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip
857  | Tpointer _ , Tpointer _ ⇒ cmp_case_ipip
858  | Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip
859  | Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip
860  | Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip
861  | _ , _ ⇒ cmp_default
862  end.
863*)
864ninductive classify_fun_cases : Type ≝
865  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
866  | fun_default: classify_fun_cases . (**r other *)
867
868ndefinition classify_fun ≝ λty: type.
869  match ty with
870  [ Tfunction args res ⇒ fun_case_f args res
871  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
872                                    | _ ⇒ fun_default
873                                    ]
874  | _ ⇒ fun_default
875  ].
876
877(* * Translating Clight types to Cminor types, function signatures,
878  and external functions. *)
879(* XXX: is this the best way to access these? *)
880alias id "ASTint" = "cic:/matita/c-semantics/AST/typ.con(0,1,0)".
881alias id "ASTfloat" = "cic:/matita/c-semantics/AST/typ.con(0,2,0)".
882
883ndefinition typ_of_type : type → typ ≝ λt.
884  match t with
885  [ Tfloat _ ⇒ ASTfloat
886  | _ ⇒ ASTint
887  ].
888
889ndefinition opttyp_of_type : type → option typ ≝ λt.
890  match t with
891  [ Tvoid ⇒ None ?
892  | Tfloat _ ⇒ Some ? ASTfloat
893  | _ ⇒ Some ? ASTint
894  ].
895
896nlet rec typlist_of_typelist (tl: typelist) : list typ ≝
897  match tl with
898  [ Tnil ⇒ nil ?
899  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
900  ].
901
902ndefinition signature_of_type : typelist → type → signature ≝ λargs. λres.
903  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
904
905ndefinition external_function
906    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
907  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.