source: src/Clight/Csyntax.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

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