source: C-semantics/Csyntax.ma @ 250

Last change on this file since 250 was 250, checked in by campbell, 9 years ago

Begin separating soundness from executable semantics.

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