source: C-semantics/Csyntax.ma @ 124

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

Initial work on Clight semantics with 8051 memory spaces.

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