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

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

Tcomp_ptr should take the memory region and use that to calculate its size.

File size: 34.2 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Abstract syntax for the Clight language *)
17
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
34ninductive signedness : Type ≝
35  | Signed: signedness
36  | Unsigned: signedness.
37
38ninductive intsize : Type ≝
39  | I8: intsize
40  | I16: intsize
41  | I32: intsize.
42
43(* * Float types come in two sizes: 32 bits (single precision)
44  and 64-bit (double precision). *)
45
46ninductive floatsize : Type ≝
47  | F32: floatsize
48  | F64: floatsize.
49
50(* * The syntax of type expressions.  Some points to note:
51- Array types [Tarray n] carry the size [n] of the array.
52  Arrays with unknown sizes are represented by pointer types.
53- Function types [Tfunction targs tres] specify the number and types
54  of the function arguments (list [targs]), and the type of the
55  function result ([tres]).  Variadic functions and old-style unprototyped
56  functions are not supported.
57- In C, struct and union types are named and compared by name.
58  This enables the definition of recursive struct types such as
59<<
60  struct s1 { int n; struct * s1 next; };
61>>
62  Note that recursion within types must go through a pointer type.
63  For instance, the following is not allowed in C.
64<<
65  struct s2 { int n; struct s2 next; };
66>>
67  In Clight, struct and union types [Tstruct id fields] and
68  [Tunion id fields] are compared by structure: the [fields]
69  argument gives the names and types of the members.  The identifier
70  [id] is a local name which can be used in conjuction with the
71  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr 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
85ninductive type : Type ≝
86  | Tvoid: type                         (**r the [void] type *)
87  | Tint: intsize → signedness → type   (**r integer types *)
88  | Tfloat: floatsize → type            (**r floating-point types *)
89  | Tpointer: 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 ≝
97  | Tnil: typelist
98  | Tcons: type → typelist → typelist
99
100with fieldlist : Type ≝
101  | Fnil: fieldlist
102  | Fcons: ident → type → fieldlist → fieldlist.
103
104(* XXX: no induction scheme! *)
105nlet rec type_ind
106  (P:type → Prop)
107  (vo:P Tvoid)
108  (it:∀i,s. P (Tint i s))
109  (fl:∀f. P (Tfloat f))
110  (pt:∀s,t. P t → P (Tpointer s t))
111  (ar:∀s,t,n. P t → P (Tarray s t n))
112  (fn:∀tl,t. P t → P (Tfunction tl t))
113  (st:∀i,fl. P (Tstruct i fl))
114  (un:∀i,fl. P (Tunion i fl))
115  (cp:∀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 
129nlet rec fieldlist_ind
130  (P:fieldlist → Prop)
131  (nl:P Fnil)
132  (cs:∀i,t,fs. P fs → P (Fcons i t fs))
133  (fs:fieldlist) on fs : P fs ≝
134  match fs with
135  [ Fnil ⇒ nl
136  | Fcons i t fs' ⇒ cs i t fs' (fieldlist_ind P nl cs fs')
137  ].
138
139(* * ** Expressions *)
140
141(* * Arithmetic and logical operators. *)
142
143ninductive unary_operation : Type ≝
144  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
145  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
146  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
147
148ninductive binary_operation : Type ≝
149  | Oadd : binary_operation             (**r addition (binary [+]) *)
150  | Osub : binary_operation             (**r subtraction (binary [-]) *)
151  | Omul : binary_operation             (**r multiplication (binary [*]) *)
152  | Odiv : binary_operation             (**r division ([/]) *)
153  | Omod : binary_operation             (**r remainder ([%]) *)
154  | Oand : binary_operation             (**r bitwise and ([&]) *)
155  | Oor : binary_operation              (**r bitwise or ([|]) *)
156  | Oxor : binary_operation             (**r bitwise xor ([^]) *)
157  | Oshl : binary_operation             (**r left shift ([<<]) *)
158  | Oshr : binary_operation             (**r right shift ([>>]) *)
159  | Oeq: binary_operation               (**r comparison ([==]) *)
160  | One: binary_operation               (**r comparison ([!=]) *)
161  | Olt: binary_operation               (**r comparison ([<]) *)
162  | Ogt: binary_operation               (**r comparison ([>]) *)
163  | Ole: binary_operation               (**r comparison ([<=]) *)
164  | Oge: binary_operation.              (**r comparison ([>=]) *)
165
166(* * Clight expressions are a large subset of those of C.
167  The main omissions are string literals and assignment operators
168  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
169  not an expression. 
170
171  All expressions are annotated with their types.  An expression
172  (type [expr]) is therefore a pair of a type and an expression
173  description (type [expr_descr]).
174*)
175
176ninductive expr : Type ≝
177  | Expr: expr_descr → type → expr
178
179with expr_descr : Type ≝
180  | Econst_int: int → expr_descr       (**r integer literal *)
181  | Econst_float: float → expr_descr   (**r float literal *)
182  | Evar: ident → expr_descr           (**r variable *)
183  | Ederef: expr → expr_descr          (**r pointer dereference (unary [*]) *)
184  | Eaddrof: expr → expr_descr         (**r address-of operator ([&]) *)
185  | Eunop: unary_operation → expr → expr_descr  (**r unary operation *)
186  | Ebinop: binary_operation → expr → expr → expr_descr (**r binary operation *)
187  | Ecast: type → expr → expr_descr    (**r type cast ([(ty) e]) *)
188  | Econdition: expr → expr → expr → expr_descr (**r conditional ([e1 ? e2 : e3]) *)
189  | Eandbool: expr → expr → expr_descr (**r sequential and ([&&]) *)
190  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
191  | Esizeof: type → expr_descr         (**r size of a type *)
192  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
193  | Ecost: costlabel → expr → expr_descr.
194
195
196
197
198(* * Extract the type part of a type-annotated Clight expression. *)
199
200ndefinition 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
210ndefinition label ≝ ident.
211
212ninductive statement : Type ≝
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 ≝            (**r cases of a [switch] *)
230  | LSdefault: statement → labeled_statements
231  | LScase: int → statement → labeled_statements → labeled_statements.
232
233nlet 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
310ndefinition 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
321nrecord function : Type ≝ {
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
331ninductive fundef : Type ≝
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
341ndefinition clight_program : Type ≝ program fundef type.
342
343(* * * Operations over types *)
344
345(* * The type of a function definition. *)
346
347nlet rec type_of_params (params: list (ident × type)) : typelist ≝
348  match params with
349  [ nil ⇒ Tnil
350  | cons h rem ⇒ match h with [ mk_pair id ty ⇒ Tcons ty (type_of_params rem) ]
351  ].
352
353ndefinition type_of_function : function → type ≝ λf.
354  Tfunction (type_of_params (fn_params f)) (fn_return f).
355
356ndefinition 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 *)
364nlet 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? *)
389nlet 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
434nlemma alignof_fields_pos:
435  ∀f. alignof_fields f > 0.
436napply fieldlist_ind; //;
437#i;#t;#fs';#IH; nlapply (Zmax_r (alignof t) (alignof_fields fs'));
438napply Zlt_to_Zle_to_Zlt; //; nqed.
439
440nlemma alignof_pos:
441  ∀t. alignof t > 0.
442#t;nelim t; nnormalize; //;
443##[ ##1,2: #z; ncases z; //;
444##| ##3,4: #i;napply alignof_fields_pos
445##] nqed.
446
447(* * Size of a type, in bytes. *)
448
449ndefinition sizeof_pointer : region → Z ≝
450λsp. match sp with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
451
452nlet 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
477nlemma 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;ncases i;#s;//;
484##| #f;ncases f;//
485##| #t;#n;#H; nwhd 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*)
522nlet 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
533ndefinition field_offset ≝ λid: ident. λfld: fieldlist.
534  field_offset_rec id fld 0.
535
536nlet 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
628ninductive mode: Type ≝
629  | By_value: memory_chunk → mode
630  | By_reference: mode
631  | By_nothing: mode.
632
633ndefinition access_mode_pointer : region → mode ≝ λr.
634By_value (match r with
635[ Any   ⇒ Mint24
636| Data  ⇒ Mint8unsigned
637| IData ⇒ Mint8unsigned
638| PData ⇒ Mint8unsigned
639| XData ⇒ Mint16unsigned
640| Code ⇒ Mint16unsigned
641]).
642
643ndefinition access_mode : type → mode ≝ λty.
644  match ty with
645  [ Tint i s ⇒
646    match i with [ I8 ⇒
647      match s with [ Signed ⇒ By_value Mint8signed
648                   | Unsigned ⇒ By_value Mint8unsigned ]
649                 | I16 ⇒
650      match s with [ Signed ⇒ By_value Mint16signed
651                   | Unsigned ⇒ By_value Mint16unsigned ]
652                 | I32 ⇒ By_value Mint32 ]
653  | Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32
654                            | F64 ⇒ By_value Mfloat64 ]
655  | Tvoid ⇒ By_nothing
656  | Tpointer r _ ⇒ access_mode_pointer r
657  | Tarray _ _ _ ⇒ By_reference
658  | Tfunction _ _ ⇒ By_reference
659  | Tstruct _ fList ⇒ By_nothing
660  | Tunion _ fList ⇒ By_nothing
661  | Tcomp_ptr r _ ⇒ access_mode_pointer r
662  ].
663
664(* * Classification of arithmetic operations and comparisons.
665  The following [classify_] functions take as arguments the types
666  of the arguments of an operation.  They return enough information
667  to resolve overloading for this operator applications, such as
668  ``both arguments are floats'', or ``the first is a pointer
669  and the second is an integer''.  These functions are used to resolve
670  overloading both in the dynamic semantics (module [Csem]) and in the
671  compiler (module [Cshmgen]).
672*)
673
674ninductive classify_add_cases : Type ≝
675  | add_case_ii: classify_add_cases         (**r int , int *)
676  | add_case_ff: classify_add_cases         (**r float , float *)
677  | add_case_pi: type → classify_add_cases (**r ptr or array, int *)
678  | add_case_ip: type → classify_add_cases (**r int, ptr or array *)
679  | add_default: classify_add_cases.        (**r other *)
680
681ndefinition classify_add ≝ λty1: type. λty2: type.
682(*
683  match ty1, ty2 with
684  [ Tint _ _, Tint _ _ ⇒ add_case_ii
685  | Tfloat _, Tfloat _ ⇒ add_case_ff
686  | Tpointer ty, Tint _ _ ⇒ add_case_pi ty
687  | Tarray ty _, Tint _ _ ⇒ add_case_pi ty
688  | Tint _ _, Tpointer ty ⇒ add_case_ip ty
689  | Tint _ _, Tarray ty _ ⇒ add_case_ip ty
690  | _, _ ⇒ add_default
691  ].
692*)
693  match ty1 with
694  [ Tint _ _ ⇒
695    match ty2 with
696    [ Tint _ _ ⇒ add_case_ii
697    | Tpointer _ ty ⇒ add_case_ip ty
698    | Tarray _ ty _ ⇒ add_case_ip ty
699    | _ ⇒ add_default ]
700  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
701  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
702  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
703  | _ ⇒ add_default
704  ].
705
706ninductive classify_sub_cases : Type ≝
707  | sub_case_ii: classify_sub_cases          (**r int , int *)
708  | sub_case_ff: classify_sub_cases          (**r float , float *)
709  | sub_case_pi: type → classify_sub_cases  (**r ptr or array , int *)
710  | sub_case_pp: type → classify_sub_cases  (**r ptr or array , ptr or array *)
711  | sub_default: classify_sub_cases .        (**r other *)
712
713ndefinition classify_sub ≝ λty1: type. λty2: type.
714(*  match ty1, ty2 with
715  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
716  | Tfloat _ , Tfloat _ ⇒ sub_case_ff
717  | Tpointer ty , Tint _ _ ⇒ sub_case_pi ty
718  | Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty
719  | Tpointer ty , Tpointer _ ⇒ sub_case_pp ty
720  | Tpointer ty , Tarray _ _⇒ sub_case_pp ty
721  | Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty
722  | Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty
723  | _ ,_ ⇒ sub_default
724  end.
725*)
726  match ty1 with
727  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
728  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
729  | Tpointer _ ty ⇒
730    match ty2 with
731    [ Tint _ _ ⇒ sub_case_pi ty
732    | Tpointer _ _ ⇒ sub_case_pp ty
733    | Tarray _ _ _ ⇒ sub_case_pp ty
734    | _ ⇒ sub_default ]
735  | Tarray _ ty _ ⇒
736    match ty2 with
737    [ Tint _ _ ⇒ sub_case_pi ty
738    | Tpointer _ _ ⇒ sub_case_pp ty
739    | Tarray _ _ _ ⇒ sub_case_pp ty
740    | _ ⇒ sub_default ]
741  | _ ⇒ sub_default
742  ].
743
744ninductive classify_mul_cases : Type ≝
745  | mul_case_ii: classify_mul_cases (**r int , int *)
746  | mul_case_ff: classify_mul_cases (**r float , float *)
747  | mul_default: classify_mul_cases . (**r other *)
748
749ndefinition classify_mul ≝ λty1: type. λty2: type.
750  match ty1 with
751  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
752  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff | _ ⇒ mul_default ]
753  | _ ⇒ mul_default
754  ].
755(*
756  match ty1,ty2 with
757  | Tint _ _, Tint _ _ ⇒ mul_case_ii
758  | Tfloat _ , Tfloat _ ⇒ mul_case_ff
759  | _,_  ⇒ mul_default
760end.
761*)
762ninductive classify_div_cases : Type ≝
763  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
764  | div_case_ii: classify_div_cases    (**r int , int *)
765  | div_case_ff: classify_div_cases    (**r float , float *)
766  | div_default: classify_div_cases. (**r other *)
767
768ndefinition classify_32un_aux ≝ λT:Type.λi.λs.λr1:T.λr2:T.
769  match i with [ I32 ⇒
770    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
771  | _ ⇒ r2 ].
772
773ndefinition classify_div ≝ λty1: type. λty2: type.
774  match ty1 with
775  [ Tint i1 s1 ⇒
776    match ty2 with
777    [ Tint i2 s2 ⇒
778      classify_32un_aux ? i1 s1 div_case_I32unsi
779        (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii)
780    | _ ⇒ div_default ]
781  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff | _ ⇒ div_default ]
782  | _ ⇒ div_default
783  ].
784(*
785ndefinition classify_div ≝ λty1: type. λty2: type.
786  match ty1,ty2 with
787  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi
788  | Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi
789  | Tint _ _ , Tint _ _ ⇒ div_case_ii
790  | Tfloat _ , Tfloat _ ⇒ div_case_ff
791  | _ ,_ ⇒ div_default
792end.
793*)
794ninductive classify_mod_cases : Type ≝
795  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
796  | mod_case_ii: classify_mod_cases  (**r int , int *)
797  | mod_default: classify_mod_cases . (**r other *)
798
799ndefinition classify_mod ≝ λty1:type. λty2:type.
800  match ty1 with
801  [ Tint i1 s1 ⇒
802    match ty2 with
803    [ Tint i2 s2 ⇒
804      classify_32un_aux ? i1 s1 mod_case_I32unsi
805        (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii)
806    | _ ⇒ mod_default ]
807  | _ ⇒ mod_default
808  ].
809(*
810Definition classify_mod (ty1: type) (ty2: type) :=
811  match ty1,ty2 with
812  | Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi
813  | Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi
814  | Tint _ _ , Tint _ _ ⇒ mod_case_ii
815  | _ , _ ⇒ mod_default
816end .
817*)
818ninductive classify_shr_cases :Type ≝
819  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
820  | shr_case_ii :classify_shr_cases (**r int , int *)
821  | shr_default : classify_shr_cases . (**r other *)
822
823ndefinition classify_shr ≝ λty1: type. λty2: type.
824  match ty1 with
825  [ Tint i1 s1 ⇒
826    match ty2 with
827    [ Tint _ _ ⇒
828      classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii
829    | _ ⇒ shr_default ]
830  | _ ⇒ shr_default
831  ].
832
833(*
834Definition classify_shr (ty1: type) (ty2: type) :=
835  match ty1,ty2 with
836  | Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi
837  | Tint _ _ , Tint _ _ ⇒ shr_case_ii
838  | _ , _ ⇒ shr_default
839  end.
840*)
841ninductive classify_cmp_cases : Type ≝
842  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
843  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
844  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
845  | cmp_default: classify_cmp_cases . (**r other *)
846
847ndefinition classify_cmp ≝ λty1:type. λty2:type.
848  match ty1 with
849  [ Tint i1 s1 ⇒
850    match ty2 with
851    [ Tint i2 s2 ⇒
852      classify_32un_aux ? i1 s1 cmp_case_I32unsi
853        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
854    | _ ⇒ cmp_default ]
855  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
856  | Tpointer _ _ ⇒
857    match ty2 with
858    [ Tint _ _ ⇒ cmp_case_ipip
859    | Tpointer _ _ ⇒ cmp_case_ipip
860    | Tarray _ _ _ ⇒ cmp_case_ipip
861    | _ ⇒ cmp_default ]
862  | Tarray _ _ _ ⇒
863    match ty2 with
864    [ Tint _ _ ⇒ cmp_case_ipip
865    | Tpointer _ _ ⇒ cmp_case_ipip
866    | Tarray _ _ _ ⇒ cmp_case_ipip
867    | _ ⇒ cmp_default ]
868  | _ ⇒ cmp_default
869  ].
870
871(*
872Definition classify_cmp (ty1: type) (ty2: type) :=
873  match ty1,ty2 with
874  | Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi
875  | Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi
876  | Tint _ _ , Tint _ _ ⇒ cmp_case_ipip
877  | Tfloat _ , Tfloat _ ⇒ cmp_case_ff
878  | Tpointer _ , Tint _ _ ⇒ cmp_case_ipip
879  | Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip
880  | Tpointer _ , Tpointer _ ⇒ cmp_case_ipip
881  | Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip
882  | Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip
883  | Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip
884  | _ , _ ⇒ cmp_default
885  end.
886*)
887ninductive classify_fun_cases : Type ≝
888  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
889  | fun_default: classify_fun_cases . (**r other *)
890
891ndefinition classify_fun ≝ λty: type.
892  match ty with
893  [ Tfunction args res ⇒ fun_case_f args res
894  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
895                                    | _ ⇒ fun_default
896                                    ]
897  | _ ⇒ fun_default
898  ].
899
900(* * Translating Clight types to Cminor types, function signatures,
901  and external functions. *)
902
903ndefinition typ_of_type : type → typ ≝ λt.
904  match t with
905  [ Tfloat _ ⇒ ASTfloat
906  | _ ⇒ ASTint
907  ].
908
909ndefinition opttyp_of_type : type → option typ ≝ λt.
910  match t with
911  [ Tvoid ⇒ None ?
912  | Tfloat _ ⇒ Some ? ASTfloat
913  | _ ⇒ Some ? ASTint
914  ].
915
916nlet rec typlist_of_typelist (tl: typelist) : list typ ≝
917  match tl with
918  [ Tnil ⇒ nil ?
919  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
920  ].
921
922ndefinition signature_of_type : typelist → type → signature ≝ λargs. λres.
923  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
924
925ndefinition external_function
926    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
927  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.