source: src/Clight/Csyntax.ma @ 725

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

Do some light manual disambiguation to make Clight examples go through more
easily.

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