source: Deliverables/D3.1/C-semantics/Csyntax.ma @ 535

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

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

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 "AST.ma".
20include "Coqlib.ma".
21include "Errors.ma".
22include "CostLabel.ma".
23
24(* * * Abstract syntax *)
25
26(* * ** Types *)
27
28(* * Clight types are similar to those of C.  They include numeric types,
29  pointers, arrays, function types, and composite types (struct and
30  union).  Numeric types (integers and floats) fully specify the
31  bit size of the type.  An integer type is a pair of a signed/unsigned
32  flag and a bit size: 8, 16 or 32 bits. *)
33
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 ([Internal]) or declared as
329  external functions ([External]). *)
330
331inductive fundef : Type[0] ≝
332  | Internal: function → fundef
333  | External: ident → typelist → type → fundef.
334
335(* * ** Programs *)
336
337(* * A program is a collection of named functions, plus a collection
338  of named global variables, carrying their types and optional initialization
339  data.  See module [AST] for more details. *)
340
341definition clight_program : Type[0] ≝ program fundef type.
342
343(* * * Operations over types *)
344
345(* * The type of a function definition. *)
346
347let rec type_of_params (params: list (ident × type)) : typelist ≝
348  match params with
349  [ nil ⇒ Tnil
350  | cons h rem ⇒ match h with [ pair id ty ⇒ Tcons ty (type_of_params rem) ]
351  ].
352
353definition type_of_function : function → type ≝ λf.
354  Tfunction (type_of_params (fn_params f)) (fn_return f).
355
356definition type_of_fundef : fundef → type ≝ λf.
357  match f with
358  [ Internal fd ⇒ type_of_function fd
359  | External id args res ⇒ Tfunction args res
360  ].
361
362(* * Natural alignment of a type, in bytes. *)
363(* FIXME: these are old values for 32 bit machines *)
364let rec alignof (t: type) : Z ≝
365  match t return λ_.Z (* XXX appears to infer nat otherwise *) with
366  [ Tvoid ⇒ 1
367  | Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
368  | Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
369  | Tpointer _ _ ⇒ 4
370  | Tarray _ t' n ⇒ alignof t'
371  | Tfunction _ _ ⇒ 1
372  | Tstruct _ fld ⇒ alignof_fields fld
373  | Tunion _ fld ⇒ alignof_fields fld
374  | Tcomp_ptr _ _ ⇒ 4
375  ]
376
377and alignof_fields (f: fieldlist) : Z ≝
378  match f with
379  [ Fnil ⇒ 1
380  | Fcons id t f' ⇒ Zmax (alignof t) (alignof_fields f')
381  ].
382
383(*
384Scheme type_ind2 := Induction for type Sort Prop
385  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
386*)
387
388(* XXX: automatic generation? *)
389let rec type_ind2
390  (P:type → Prop) (Q:fieldlist → Prop)
391  (vo:P Tvoid)
392  (it:∀i,s. P (Tint i s))
393  (fl:∀f. P (Tfloat f))
394  (pt:∀s,t. P t → P (Tpointer s t))
395  (ar:∀s,t,n. P t → P (Tarray s t n))
396  (fn:∀tl,t. P t → P (Tfunction tl t))
397  (st:∀i,fl. Q fl → P (Tstruct i fl))
398  (un:∀i,fl. Q fl → P (Tunion i fl))
399  (cp:∀r,i. P (Tcomp_ptr r i))
400  (nl:Q Fnil)
401  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
402 (t:type) on t : P t ≝
403  match t return λt'.P t' with
404  [ Tvoid ⇒ vo
405  | Tint i s ⇒ it i s
406  | Tfloat s ⇒ fl s
407  | Tpointer s t' ⇒ pt s t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
408  | Tarray s t' n ⇒ ar s t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
409  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
410  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
411  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
412  | Tcomp_ptr r i ⇒ cp r i
413  ]
414and fieldlist_ind2
415  (P:type → Prop) (Q:fieldlist → Prop)
416  (vo:P Tvoid)
417  (it:∀i,s. P (Tint i s))
418  (fl:∀f. P (Tfloat f))
419  (pt:∀s,t. P t → P (Tpointer s t))
420  (ar:∀s,t,n. P t → P (Tarray s t n))
421  (fn:∀tl,t. P t → P (Tfunction tl t))
422  (st:∀i,fl. Q fl → P (Tstruct i fl))
423  (un:∀i,fl. Q fl → P (Tunion i fl))
424  (cp:∀r,i. P (Tcomp_ptr r i))
425  (nl:Q Fnil)
426  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
427  (fs:fieldlist) on fs : Q fs ≝
428  match fs return λfs'.Q fs' with
429  [ Fnil ⇒ nl
430  | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t)
431                        (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs f')
432  ].
433
434lemma alignof_fields_pos:
435  ∀f. alignof_fields f > 0.
436@fieldlist_ind //;
437#i #t #fs' #IH lapply (Zmax_r (alignof t) (alignof_fields fs'));
438@Zlt_to_Zle_to_Zlt //; qed.
439
440lemma alignof_pos:
441  ∀t. alignof t > 0.
442#t elim t; normalize; //;
443[ 1,2: #z cases z; //;
444| 3,4: #i @alignof_fields_pos
445] qed.
446
447(* * Size of a type, in bytes. *)
448
449definition sizeof_pointer : region → Z ≝
450λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
451
452let rec sizeof (t: type) : Z ≝
453  match t return λ_.Z with
454  [ Tvoid ⇒ 1
455  | Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
456  | Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4 | F64 ⇒ 8 ]
457  | Tpointer r _ ⇒ sizeof_pointer r
458  | Tarray _ t' n ⇒ sizeof t' * Zmax 1 n
459  | Tfunction _ _ ⇒ 1
460  | Tstruct _ fld ⇒ align (Zmax 1 (sizeof_struct fld 0)) (alignof t)
461  | Tunion _ fld ⇒ align (Zmax 1 (sizeof_union fld)) (alignof t)
462  | Tcomp_ptr r _ ⇒ sizeof_pointer r
463  ]
464
465and sizeof_struct (fld: fieldlist) (pos: Z) on fld : Z ≝
466  match fld with
467  [ Fnil ⇒ pos
468  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
469  ]
470
471and sizeof_union (fld: fieldlist) : Z ≝
472  match fld with
473  [ Fnil ⇒ 0
474  | Fcons id t fld' ⇒ Zmax (sizeof t) (sizeof_union fld')
475  ].
476(* TODO: needs some Z_times results
477lemma sizeof_pos:
478  ∀t. sizeof t > 0.
479#t0
480napply (type_ind2 (λt. sizeof t > 0)
481                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
482[ 1,4,6,9: //;
483| #i cases i;#s //;
484| #f cases f;//
485| #t #n #H whd in ⊢ (?%?);
486Proof.
487  intro t0.
488  apply (type_ind2 (fun t => sizeof t > 0)
489                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
490  intros; simpl; auto; try omega.
491  destruct i; omega.
492  destruct f; omega.
493  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
494  destruct H.
495  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
496  generalize (Zmax1 1 (sizeof_struct f 0)). omega.
497  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
498  generalize (Zmax1 1 (sizeof_union f)). omega.
499  split. omega. auto.
500  destruct H0. split; intros.
501  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
502  apply H1.
503  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
504Qed.
505
506Lemma sizeof_struct_incr:
507  forall fld pos, pos <= sizeof_struct fld pos.
508Proof.
509  induction fld; intros; simpl. omega.
510  eapply Zle_trans. 2: apply IHfld.
511  apply Zle_trans with (align pos (alignof t)).
512  apply align_le. apply alignof_pos.
513  assert (sizeof t > 0) by apply sizeof_pos. omega.
514Qed.
515
516(** Byte offset for a field in a struct or union.
517  Field are laid out consecutively, and padding is inserted
518  to align each field to the natural alignment for its type. *)
519
520Open Local Scope string_scope.
521*)
522let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: Z)
523                              on fld : res Z ≝
524  match fld with
525  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
526  | Fcons id' t fld' ⇒
527      match ident_eq id id' with
528      [ inl _ ⇒ OK ? (align pos (alignof t))
529      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
530      ]
531  ].
532
533definition field_offset ≝ λid: ident. λfld: fieldlist.
534  field_offset_rec id fld 0.
535
536let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
537  match fld with
538  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
539  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
540  ].
541
542(* * Some sanity checks about field offsets.  First, field offsets are
543  within the range of acceptable offsets. *)
544(*
545Remark field_offset_rec_in_range:
546  forall id ofs ty fld pos,
547  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
548  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
549Proof.
550  intros until ty. induction fld; simpl.
551  congruence.
552  destruct (ident_eq id i); intros.
553  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
554  exploit IHfld; eauto. intros [A B]. split; auto.
555  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
556  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
557Qed.
558
559Lemma field_offset_in_range:
560  forall id fld ofs ty,
561  field_offset id fld = OK ofs → field_type id fld = OK ty →
562  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
563Proof.
564  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
565Qed.
566
567(** Second, two distinct fields do not overlap *)
568
569Lemma field_offset_no_overlap:
570  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
571  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
572  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
573  id1 <> id2 →
574  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
575Proof.
576  intros until ty2. intros fld0 A B C D NEQ.
577  assert (forall fld pos,
578  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
579  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
580  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
581  induction fld; intro pos; simpl. congruence.
582  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
583  congruence.
584  subst i. intros. inv H; inv H0.
585  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
586  subst i. intros. inv H1; inv H2.
587  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
588  intros. eapply IHfld; eauto.
589
590  apply H with fld0 0; auto.
591Qed.
592
593(** Third, if a struct is a prefix of another, the offsets of fields
594  in common is the same. *)
595
596Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
597  match fld1 with
598  | Fnil ⇒ fld2
599  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
600  end.
601
602Lemma field_offset_prefix:
603  forall id ofs fld2 fld1,
604  field_offset id fld1 = OK ofs →
605  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
606Proof.
607  intros until fld2.
608  assert (forall fld1 pos,
609    field_offset_rec id fld1 pos = OK ofs ->
610    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
611  induction fld1; intros pos; simpl. congruence.
612  destruct (ident_eq id i); auto.
613  intros. unfold field_offset; auto.
614Qed.
615*)
616(* * The [access_mode] function describes how a variable of the given
617type must be accessed:
618- [By_value ch]: access by value, i.e. by loading from the address
619  of the variable using the memory chunk [ch];
620- [By_reference]: access by reference, i.e. by just returning
621  the address of the variable;
622- [By_nothing]: no access is possible, e.g. for the [void] type.
623
624We currently do not support 64-bit integers and 128-bit floats, so these
625have an access mode of [By_nothing].
626*)
627
628inductive mode: Type[0] ≝
629  | By_value: memory_chunk → mode
630  | By_reference: region → mode
631  | By_nothing: mode.
632
633definition access_mode : type → mode ≝ λty.
634  match ty with
635  [ Tint i s ⇒
636    match i with [ I8 ⇒
637      match s with [ Signed ⇒ By_value Mint8signed
638                   | Unsigned ⇒ By_value Mint8unsigned ]
639                 | I16 ⇒
640      match s with [ Signed ⇒ By_value Mint16signed
641                   | Unsigned ⇒ By_value Mint16unsigned ]
642                 | I32 ⇒ By_value Mint32 ]
643  | Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32
644                            | F64 ⇒ By_value Mfloat64 ]
645  | Tvoid ⇒ By_nothing
646  | Tpointer r _ ⇒ By_value (Mpointer r)
647  | Tarray r _ _ ⇒ By_reference r
648  | Tfunction _ _ ⇒ By_reference Code
649  | Tstruct _ fList ⇒ By_nothing
650  | Tunion _ fList ⇒ By_nothing
651  | Tcomp_ptr r _ ⇒ By_value (Mpointer r)
652  ].
653
654(* * Classification of arithmetic operations and comparisons.
655  The following [classify_] functions take as arguments the types
656  of the arguments of an operation.  They return enough information
657  to resolve overloading for this operator applications, such as
658  ``both arguments are floats'', or ``the first is a pointer
659  and the second is an integer''.  These functions are used to resolve
660  overloading both in the dynamic semantics (module [Csem]) and in the
661  compiler (module [Cshmgen]).
662*)
663
664inductive classify_add_cases : Type[0] ≝
665  | add_case_ii: classify_add_cases         (**r int , int *)
666  | add_case_ff: classify_add_cases         (**r float , float *)
667  | add_case_pi: type → classify_add_cases (**r ptr or array, int *)
668  | add_case_ip: type → classify_add_cases (**r int, ptr or array *)
669  | add_default: classify_add_cases.        (**r other *)
670
671definition classify_add ≝ λty1: type. λty2: type.
672(*
673  match ty1, ty2 with
674  [ Tint _ _, Tint _ _ ⇒ add_case_ii
675  | Tfloat _, Tfloat _ ⇒ add_case_ff
676  | Tpointer ty, Tint _ _ ⇒ add_case_pi ty
677  | Tarray ty _, Tint _ _ ⇒ add_case_pi ty
678  | Tint _ _, Tpointer ty ⇒ add_case_ip ty
679  | Tint _ _, Tarray ty _ ⇒ add_case_ip ty
680  | _, _ ⇒ add_default
681  ].
682*)
683  match ty1 with
684  [ Tint _ _ ⇒
685    match ty2 with
686    [ Tint _ _ ⇒ add_case_ii
687    | Tpointer _ ty ⇒ add_case_ip ty
688    | Tarray _ ty _ ⇒ add_case_ip ty
689    | _ ⇒ add_default ]
690  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
691  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
692  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
693  | _ ⇒ add_default
694  ].
695
696inductive classify_sub_cases : Type[0] ≝
697  | sub_case_ii: classify_sub_cases          (**r int , int *)
698  | sub_case_ff: classify_sub_cases          (**r float , float *)
699  | sub_case_pi: type → classify_sub_cases  (**r ptr or array , int *)
700  | sub_case_pp: type → classify_sub_cases  (**r ptr or array , ptr or array *)
701  | sub_default: classify_sub_cases .        (**r other *)
702
703definition classify_sub ≝ λty1: type. λty2: type.
704(*  match ty1, ty2 with
705  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
706  | Tfloat _ , Tfloat _ ⇒ sub_case_ff
707  | Tpointer ty , Tint _ _ ⇒ sub_case_pi ty
708  | Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty
709  | Tpointer ty , Tpointer _ ⇒ sub_case_pp ty
710  | Tpointer ty , Tarray _ _⇒ sub_case_pp ty
711  | Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty
712  | Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty
713  | _ ,_ ⇒ sub_default
714  end.
715*)
716  match ty1 with
717  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
718  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
719  | Tpointer _ ty ⇒
720    match ty2 with
721    [ Tint _ _ ⇒ sub_case_pi ty
722    | Tpointer _ _ ⇒ sub_case_pp ty
723    | Tarray _ _ _ ⇒ sub_case_pp ty
724    | _ ⇒ sub_default ]
725  | Tarray _ ty _ ⇒
726    match ty2 with
727    [ Tint _ _ ⇒ sub_case_pi ty
728    | Tpointer _ _ ⇒ sub_case_pp ty
729    | Tarray _ _ _ ⇒ sub_case_pp ty
730    | _ ⇒ sub_default ]
731  | _ ⇒ sub_default
732  ].
733
734inductive classify_mul_cases : Type[0] ≝
735  | mul_case_ii: classify_mul_cases (**r int , int *)
736  | mul_case_ff: classify_mul_cases (**r float , float *)
737  | mul_default: classify_mul_cases . (**r other *)
738
739definition classify_mul ≝ λty1: type. λty2: type.
740  match ty1 with
741  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
742  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff | _ ⇒ mul_default ]
743  | _ ⇒ mul_default
744  ].
745(*
746  match ty1,ty2 with
747  | Tint _ _, Tint _ _ ⇒ mul_case_ii
748  | Tfloat _ , Tfloat _ ⇒ mul_case_ff
749  | _,_  ⇒ mul_default
750end.
751*)
752inductive classify_div_cases : Type[0] ≝
753  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
754  | div_case_ii: classify_div_cases    (**r int , int *)
755  | div_case_ff: classify_div_cases    (**r float , float *)
756  | div_default: classify_div_cases. (**r other *)
757
758definition classify_32un_aux ≝ λT:Type[0].λi.λs.λr1:T.λr2:T.
759  match i with [ I32 ⇒
760    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
761  | _ ⇒ r2 ].
762
763definition classify_div ≝ λty1: type. λty2: type.
764  match ty1 with
765  [ Tint i1 s1 ⇒
766    match ty2 with
767    [ Tint i2 s2 ⇒
768      classify_32un_aux ? i1 s1 div_case_I32unsi
769        (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii)
770    | _ ⇒ div_default ]
771  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff | _ ⇒ div_default ]
772  | _ ⇒ div_default
773  ].
774(*
775definition classify_div ≝ λty1: type. λty2: type.
776  match ty1,ty2 with
777  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi
778  | Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi
779  | Tint _ _ , Tint _ _ ⇒ div_case_ii
780  | Tfloat _ , Tfloat _ ⇒ div_case_ff
781  | _ ,_ ⇒ div_default
782end.
783*)
784inductive classify_mod_cases : Type[0] ≝
785  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
786  | mod_case_ii: classify_mod_cases  (**r int , int *)
787  | mod_default: classify_mod_cases . (**r other *)
788
789definition classify_mod ≝ λty1:type. λty2:type.
790  match ty1 with
791  [ Tint i1 s1 ⇒
792    match ty2 with
793    [ Tint i2 s2 ⇒
794      classify_32un_aux ? i1 s1 mod_case_I32unsi
795        (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii)
796    | _ ⇒ mod_default ]
797  | _ ⇒ mod_default
798  ].
799(*
800Definition classify_mod (ty1: type) (ty2: type) :=
801  match ty1,ty2 with
802  | Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi
803  | Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi
804  | Tint _ _ , Tint _ _ ⇒ mod_case_ii
805  | _ , _ ⇒ mod_default
806end .
807*)
808inductive classify_shr_cases :Type[0] ≝
809  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
810  | shr_case_ii :classify_shr_cases (**r int , int *)
811  | shr_default : classify_shr_cases . (**r other *)
812
813definition classify_shr ≝ λty1: type. λty2: type.
814  match ty1 with
815  [ Tint i1 s1 ⇒
816    match ty2 with
817    [ Tint _ _ ⇒
818      classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii
819    | _ ⇒ shr_default ]
820  | _ ⇒ shr_default
821  ].
822
823(*
824Definition classify_shr (ty1: type) (ty2: type) :=
825  match ty1,ty2 with
826  | Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi
827  | Tint _ _ , Tint _ _ ⇒ shr_case_ii
828  | _ , _ ⇒ shr_default
829  end.
830*)
831inductive classify_cmp_cases : Type[0] ≝
832  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
833  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
834  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
835  | cmp_default: classify_cmp_cases . (**r other *)
836
837definition classify_cmp ≝ λty1:type. λty2:type.
838  match ty1 with
839  [ Tint i1 s1 ⇒
840    match ty2 with
841    [ Tint i2 s2 ⇒
842      classify_32un_aux ? i1 s1 cmp_case_I32unsi
843        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
844    | _ ⇒ cmp_default ]
845  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
846  | Tpointer _ _ ⇒
847    match ty2 with
848    [ Tint _ _ ⇒ cmp_case_ipip
849    | Tpointer _ _ ⇒ cmp_case_ipip
850    | Tarray _ _ _ ⇒ cmp_case_ipip
851    | _ ⇒ cmp_default ]
852  | Tarray _ _ _ ⇒
853    match ty2 with
854    [ Tint _ _ ⇒ cmp_case_ipip
855    | Tpointer _ _ ⇒ cmp_case_ipip
856    | Tarray _ _ _ ⇒ cmp_case_ipip
857    | _ ⇒ cmp_default ]
858  | _ ⇒ cmp_default
859  ].
860
861(*
862Definition classify_cmp (ty1: type) (ty2: type) :=
863  match ty1,ty2 with
864  | Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi
865  | Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi
866  | Tint _ _ , Tint _ _ ⇒ cmp_case_ipip
867  | Tfloat _ , Tfloat _ ⇒ cmp_case_ff
868  | Tpointer _ , Tint _ _ ⇒ cmp_case_ipip
869  | Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip
870  | Tpointer _ , Tpointer _ ⇒ cmp_case_ipip
871  | Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip
872  | Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip
873  | Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip
874  | _ , _ ⇒ cmp_default
875  end.
876*)
877inductive classify_fun_cases : Type[0] ≝
878  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
879  | fun_default: classify_fun_cases . (**r other *)
880
881definition classify_fun ≝ λty: type.
882  match ty with
883  [ Tfunction args res ⇒ fun_case_f args res
884  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
885                                    | _ ⇒ fun_default
886                                    ]
887  | _ ⇒ fun_default
888  ].
889
890(* * Translating Clight types to Cminor types, function signatures,
891  and external functions. *)
892
893definition typ_of_type : type → typ ≝ λt.
894  match t with
895  [ Tfloat _ ⇒ ASTfloat
896  | _ ⇒ ASTint
897  ].
898
899definition opttyp_of_type : type → option typ ≝ λt.
900  match t with
901  [ Tvoid ⇒ None ?
902  | Tfloat _ ⇒ Some ? ASTfloat
903  | _ ⇒ Some ? ASTint
904  ].
905
906let rec typlist_of_typelist (tl: typelist) : list typ ≝
907  match tl with
908  [ Tnil ⇒ nil ?
909  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
910  ].
911
912definition signature_of_type : typelist → type → signature ≝ λargs. λres.
913  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
914
915definition external_function
916    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
917  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.