source: src/Clight/Csyntax.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 6 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 25.4 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * Abstract syntax for the Clight language *)
17
18(*include "Integers.ma".*)
19include "common/AST.ma".
20include "utilities/Coqlib.ma".
21include "common/Errors.ma".
22include "common/CostLabel.ma".
23
24(* * * Abstract syntax *)
25
26(* * ** Types *)
27
28(* * The syntax of type expressions.  Some points to note:
29- Array types [Tarray n] carry the size [n] of the array.
30  Arrays with unknown sizes are represented by pointer types.
31- Function types [Tfunction targs tres] specify the number and types
32  of the function arguments (list [targs]), and the type of the
33  function result ([tres]).  Variadic functions and old-style unprototyped
34  functions are not supported.
35- In C, struct and union types are named and compared by name.
36  This enables the definition of recursive struct types such as
37<<
38  struct s1 { int n; struct * s1 next; };
39>>
40  Note that recursion within types must go through a pointer type.
41  For instance, the following is not allowed in C.
42<<
43  struct s2 { int n; struct s2 next; };
44>>
45  In Clight, struct and union types [Tstruct id fields] and
46  [Tunion id fields] are compared by structure: the [fields]
47  argument gives the names and types of the members.  The identifier
48  [id] is a local name which can be used in conjuction with the
49  [Tcomp_ptr] constructor to express recursive types.  [Tcomp_ptr rg id]
50  stands for a pointer type to the nearest enclosing [Tstruct]
51  or [Tunion] type named [id] in memory region [rg].  For instance.
52  the structure [s1] defined above in C is expressed by
53<<
54  Tstruct "s1" (Fcons "n" (Tint I32 Signed)
55               (Fcons "next" (Tcomp_ptr Any "id")
56               Fnil))
57>>
58  Note that the incorrect structure [s2] above cannot be expressed at
59  all, since [Tcomp_ptr] lets us refer to a pointer to an enclosing
60  structure or union, but not to the structure or union directly.
61*)
62
63inductive type : Type[0] ≝
64  | Tvoid: type                         (**r the [void] type *)
65  | Tint: intsize → signedness → type   (**r integer types *)
66  | Tfloat: floatsize → type            (**r floating-point types *)
67  | Tpointer: (*region →*) type → type      (**r pointer types ([*ty]) *)
68  | Tarray: (*region →*) type → nat → type  (**r array types ([ty[len]]) *)
69  | Tfunction: typelist → type → type   (**r function types *)
70  | Tstruct: ident → fieldlist → type   (**r struct types *)
71  | Tunion: ident → fieldlist → type    (**r union types *)
72  | Tcomp_ptr: (*region →*) ident → type    (**r pointer to named struct or union *)
73
74with typelist : Type[0] ≝
75  | Tnil: typelist
76  | Tcons: type → typelist → typelist
77
78with fieldlist : Type[0] ≝
79  | Fnil: fieldlist
80  | Fcons: ident → type → fieldlist → fieldlist.
81
82(* XXX: no induction scheme! *)
83let rec type_ind
84  (P:type → Prop)
85  (vo:P Tvoid)
86  (it:∀i,s. P (Tint i s))
87  (fl:∀f. P (Tfloat f))
88  (pt:∀t. P t → P (Tpointer t))
89  (ar:∀t,n. P t → P (Tarray t n))
90  (fn:∀tl,t. P t → P (Tfunction tl t))
91  (st:∀i,fl. P (Tstruct i fl))
92  (un:∀i,fl. P (Tunion i fl))
93  (cp:∀i. P (Tcomp_ptr i))
94  (t:type) on t : P t ≝
95  match t return λt'.P t' with
96  [ Tvoid ⇒ vo
97  | Tint i s ⇒ it i s
98  | Tfloat s ⇒ fl s
99  | Tpointer t' ⇒ pt t' (type_ind P vo it fl pt ar fn st un cp t')
100  | Tarray t' n ⇒ ar t' n (type_ind P vo it fl pt ar fn st un cp t')
101  | Tfunction tl t' ⇒ fn tl t' (type_ind P vo it fl pt ar fn st un cp t')
102  | Tstruct i fs ⇒ st i fs
103  | Tunion i fs ⇒ un i fs
104  | Tcomp_ptr i ⇒ cp i
105  ].
106 
107let rec fieldlist_ind
108  (P:fieldlist → Prop)
109  (nl:P Fnil)
110  (cs:∀i,t,fs. P fs → P (Fcons i t fs))
111  (fs:fieldlist) on fs : P fs ≝
112  match fs with
113  [ Fnil ⇒ nl
114  | Fcons i t fs' ⇒ cs i t fs' (fieldlist_ind P nl cs fs')
115  ].
116
117(* * ** Expressions *)
118
119(* * Arithmetic and logical operators. *)
120
121inductive unary_operation : Type[0] ≝
122  | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
123  | Onotint : unary_operation           (**r integer complement ([~] in C) *)
124  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
125
126inductive binary_operation : Type[0] ≝
127  | Oadd : binary_operation             (**r addition (binary [+]) *)
128  | Osub : binary_operation             (**r subtraction (binary [-]) *)
129  | Omul : binary_operation             (**r multiplication (binary [*]) *)
130  | Odiv : binary_operation             (**r division ([/]) *)
131  | Omod : binary_operation             (**r remainder ([%]) *)
132  | Oand : binary_operation             (**r bitwise and ([&]) *)
133  | Oor : binary_operation              (**r bitwise or ([|]) *)
134  | Oxor : binary_operation             (**r bitwise xor ([^]) *)
135  | Oshl : binary_operation             (**r left shift ([<<]) *)
136  | Oshr : binary_operation             (**r right shift ([>>]) *)
137  | Oeq: binary_operation               (**r comparison ([==]) *)
138  | One: binary_operation               (**r comparison ([!=]) *)
139  | Olt: binary_operation               (**r comparison ([<]) *)
140  | Ogt: binary_operation               (**r comparison ([>]) *)
141  | Ole: binary_operation               (**r comparison ([<=]) *)
142  | Oge: binary_operation.              (**r comparison ([>=]) *)
143
144(* * Clight expressions are a large subset of those of C.
145  The main omissions are string literals and assignment operators
146  ([=], [+=], [++], etc).  In Clight, assignment is a statement,
147  not an expression. 
148
149  All expressions are annotated with their types.  An expression
150  (type [expr]) is therefore a pair of a type and an expression
151  description (type [expr_descr]).
152*)
153
154inductive expr : Type[0] ≝
155  | Expr: expr_descr → type → expr
156
157with expr_descr : Type[0] ≝
158  | Econst_int: ∀sz:intsize. bvint sz → expr_descr       (**r integer literal *)
159  | Econst_float: float → expr_descr   (**r float literal *)
160  | Evar: ident → expr_descr           (**r variable *)
161  | Ederef: expr → expr_descr          (**r pointer dereference (unary [*]) *)
162  | Eaddrof: expr → expr_descr         (**r address-of operator ([&]) *)
163  | Eunop: unary_operation → expr → expr_descr  (**r unary operation *)
164  | Ebinop: binary_operation → expr → expr → expr_descr (**r binary operation *)
165  | Ecast: type → expr → expr_descr    (**r type cast ([(ty) e]) *)
166  | Econdition: expr → expr → expr → expr_descr (**r conditional ([e1 ? e2 : e3]) *)
167  | Eandbool: expr → expr → expr_descr (**r sequential and ([&&]) *)
168  | Eorbool: expr → expr → expr_descr  (**r sequential or ([||]) *)
169  | Esizeof: type → expr_descr         (**r size of a type *)
170  | Efield: expr → ident → expr_descr  (**r access to a member of a struct or union *)
171  | Ecost: costlabel → expr → expr_descr.
172
173
174
175
176(* * Extract the type part of a type-annotated Clight expression. *)
177
178definition typeof : expr → type ≝ λe.
179  match e with [ Expr de te ⇒ te ].
180
181(* * ** Statements *)
182
183(* * Clight statements include all C statements.
184  Only structured forms of [switch] are supported; moreover,
185  the [default] case must occur last.  Blocks and block-scoped declarations
186  are not supported. *)
187
188definition label ≝ ident.
189
190inductive statement : Type[0] ≝
191  | Sskip : statement                   (**r do nothing *)
192  | Sassign : expr → expr → statement   (**r assignment [lvalue = rvalue] *)
193  | Scall: option expr → expr → list expr → statement (**r function call *)
194  | Ssequence : statement → statement → statement  (**r sequence *)
195  | Sifthenelse : expr  → statement → statement → statement (**r conditional *)
196  | Swhile : expr → statement → statement   (**r [while] loop *)
197  | Sdowhile : expr → statement → statement (**r [do] loop *)
198  | Sfor: statement → expr → statement → statement → statement (**r [for] loop *)
199  | Sbreak : statement                      (**r [break] statement *)
200  | Scontinue : statement                   (**r [continue] statement *)
201  | Sreturn : option expr → statement       (**r [return] statement *)
202  | Sswitch : expr → labeled_statements → statement  (**r [switch] statement *)
203  | Slabel : label → statement → statement
204  | Sgoto : label → statement
205  | Scost : costlabel → statement → statement
206
207with labeled_statements : Type[0] ≝            (**r cases of a [switch] *)
208  | LSdefault: statement → labeled_statements
209  | LScase: ∀sz:intsize. bvint sz → statement → labeled_statements → labeled_statements.
210
211let rec labeled_statements_ind
212  (P:labeled_statements → Prop)
213  (LSd:∀s. P (LSdefault s))
214  (LSc:∀sz,i,s,tl. P tl → P (LScase sz i s tl))
215  ls on ls : P ls ≝
216match ls with
217[ LSdefault s ⇒ LSd s
218| LScase sz i s tl ⇒ LSc sz i s tl (labeled_statements_ind P LSd LSc tl)
219].
220
221let rec statement_ind2
222  (P:statement → Prop) (Q:labeled_statements → Prop)
223  (Ssk:P Sskip)
224  (Sas:∀e1,e2. P (Sassign e1 e2))
225  (Sca:∀eo,e,args. P (Scall eo e args))
226  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
227  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
228  (Swh:∀e,s. P s → P (Swhile e s))
229  (Sdo:∀e,s. P s → P (Sdowhile e s))
230  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
231  (Sbr:P Sbreak)
232  (Sco:P Scontinue)
233  (Sre:∀eo. P (Sreturn eo))
234  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
235  (Sla:∀l,s. P s → P (Slabel l s))
236  (Sgo:∀l. P (Sgoto l))
237  (Scs:∀l,s. P s → P (Scost l s))
238  (LSd:∀s. P s → Q (LSdefault s))
239  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
240  (s:statement) on s : P s ≝
241match s with
242[ Sskip ⇒ Ssk
243| Sassign e1 e2 ⇒ Sas e1 e2
244| Scall eo e args ⇒ Sca eo e args
245| Ssequence s1 s2 ⇒ Ssq s1 s2
246    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
247    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
248| Sifthenelse e s1 s2 ⇒ Sif e s1 s2
249    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
250    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
251| Swhile e s ⇒ Swh e s
252    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
253| Sdowhile e s ⇒ Sdo e s
254    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
255| Sfor s1 e s2 s3 ⇒ Sfo s1 e s2 s3
256    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s1)
257    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s2)
258    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s3)
259| Sbreak ⇒ Sbr
260| Scontinue ⇒ Sco
261| Sreturn eo ⇒ Sre eo
262| Sswitch e ls ⇒ Ssw e ls
263    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc ls)
264| Slabel l s ⇒ Sla l s
265    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
266| Sgoto l ⇒ Sgo l
267| Scost l s ⇒ Scs l s
268    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
269]
270and labeled_statements_ind2
271  (P:statement → Prop) (Q:labeled_statements → Prop)
272  (Ssk:P Sskip)
273  (Sas:∀e1,e2. P (Sassign e1 e2))
274  (Sca:∀eo,e,args. P (Scall eo e args))
275  (Ssq:∀s1,s2. P s1 → P s2 → P (Ssequence s1 s2))
276  (Sif:∀e,s1,s2. P s1 → P s2 → P (Sifthenelse e s1 s2))
277  (Swh:∀e,s. P s → P (Swhile e s))
278  (Sdo:∀e,s. P s → P (Sdowhile e s))
279  (Sfo:∀s1,e,s2,s3. P s1 → P s2 → P s3 → P (Sfor s1 e s2 s3))
280  (Sbr:P Sbreak)
281  (Sco:P Scontinue)
282  (Sre:∀eo. P (Sreturn eo))
283  (Ssw:∀e,ls. Q ls → P (Sswitch e ls))
284  (Sla:∀l,s. P s → P (Slabel l s))
285  (Sgo:∀l. P (Sgoto l))
286  (Scs:∀l,s. P s → P (Scost l s))
287  (LSd:∀s. P s → Q (LSdefault s))
288  (LSc:∀sz,i,s,t. P s → Q t → Q (LScase sz i s t))
289  (ls:labeled_statements) on ls : Q ls ≝
290match ls with
291[ LSdefault s ⇒ LSd s
292    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
293| LScase sz i s t ⇒ LSc sz i s t
294    (statement_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc s)
295    (labeled_statements_ind2 P Q Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs LSd LSc t)
296].
297
298definition statement_ind ≝ λP,Ssk,Sas,Sca,Ssq,Sif,Swh,Sdo,Sfo,Sbr,Sco,Sre,Ssw,Sla,Sgo,Scs.
299  statement_ind2 P (λ_.True) Ssk Sas Sca Ssq Sif Swh Sdo Sfo Sbr Sco Sre Ssw Sla Sgo Scs
300  (λ_,_. I) (λ_,_,_,_,_,_.I).
301
302(* * ** Functions *)
303
304(* * A function definition is composed of its return type ([fn_return]),
305  the names and types of its parameters ([fn_params]), the names
306  and types of its local variables ([fn_vars]), and the body of the
307  function (a statement, [fn_body]). *)
308
309record function : Type[0] ≝ {
310  fn_return: type;
311  fn_params: list (ident × type);
312  fn_vars: list (ident × type);
313  fn_body: statement
314}.
315
316(* * Functions can either be defined ([CL_Internal]) or declared as
317  external functions ([CL_External]).  Similar to the AST definition, but
318  with high level type information for external functions. *)
319
320inductive clight_fundef : Type[0] ≝
321  | CL_Internal: function → clight_fundef
322  | CL_External: ident → typelist → type → clight_fundef.
323
324(* * ** Programs *)
325
326(* * A program is a collection of named functions, plus a collection
327  of named global variables, carrying their types and optional initialization
328  data.  See module [AST] for more details. *)
329
330definition clight_program : Type[0] ≝ program (λ_.clight_fundef) (list init_data × type).
331
332(* * * Operations over types *)
333
334(* * The type of a function definition. *)
335
336let rec type_of_params (params: list (ident × type)) : typelist ≝
337  match params with
338  [ nil ⇒ Tnil
339  | cons h rem ⇒ let 〈id,ty〉 ≝ h in Tcons ty (type_of_params rem)
340  ].
341
342definition type_of_function : function → type ≝ λf.
343  Tfunction (type_of_params (fn_params f)) (fn_return f).
344
345definition type_of_fundef : clight_fundef → type ≝ λf.
346  match f with
347  [ CL_Internal fd ⇒ type_of_function fd
348  | CL_External id args res ⇒ Tfunction args res
349  ].
350
351(* * Natural alignment of a type, in bytes. *)
352let rec alignof (t: type) : nat ≝ (*1*)
353(* these are old values for 32 bit machines *)
354  match t with
355  [ Tvoid ⇒ 1
356  | Tint sz _ ⇒ match sz with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
357  | Tfloat sz ⇒ match sz with [ F32 ⇒ 4 | F64 ⇒ 8 ]
358  | Tpointer _ ⇒ 4
359  | Tarray t' n ⇒ alignof t'
360  | Tfunction _ _ ⇒ 1
361  | Tstruct _ fld ⇒ alignof_fields fld
362  | Tunion _ fld ⇒ alignof_fields fld
363  | Tcomp_ptr _ ⇒ 4
364  ]
365
366and alignof_fields (f: fieldlist) : nat ≝
367  match f with
368  [ Fnil ⇒ 1
369  | Fcons id t f' ⇒ max (alignof t) (alignof_fields f')
370  ].
371
372(*
373Scheme type_ind2 := Induction for type Sort Prop
374  with fieldlist_ind2 := Induction for fieldlist Sort Prop.
375*)
376
377(* XXX: automatic generation? *)
378let rec type_ind2
379  (P:type → Prop) (Q:fieldlist → Prop)
380  (vo:P Tvoid)
381  (it:∀i,s. P (Tint i s))
382  (fl:∀f. P (Tfloat f))
383  (pt:∀t. P t → P (Tpointer t))
384  (ar:∀t,n. P t → P (Tarray t n))
385  (fn:∀tl,t. P t → P (Tfunction tl t))
386  (st:∀i,fl. Q fl → P (Tstruct i fl))
387  (un:∀i,fl. Q fl → P (Tunion i fl))
388  (cp:∀i. P (Tcomp_ptr i))
389  (nl:Q Fnil)
390  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
391 (t:type) on t : P t ≝
392  match t return λt'.P t' with
393  [ Tvoid ⇒ vo
394  | Tint i s ⇒ it i s
395  | Tfloat s ⇒ fl s
396  | Tpointer t' ⇒ pt t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
397  | Tarray t' n ⇒ ar t' n (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
398  | Tfunction tl t' ⇒ fn tl t' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t')
399  | Tstruct i fs ⇒ st i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
400  | Tunion i fs ⇒ un i fs (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs fs)
401  | Tcomp_ptr i ⇒ cp i
402  ]
403and fieldlist_ind2
404  (P:type → Prop) (Q:fieldlist → Prop)
405  (vo:P Tvoid)
406  (it:∀i,s. P (Tint i s))
407  (fl:∀f. P (Tfloat f))
408  (pt:∀t. P t → P (Tpointer t))
409  (ar:∀t,n. P t → P (Tarray t n))
410  (fn:∀tl,t. P t → P (Tfunction tl t))
411  (st:∀i,fl. Q fl → P (Tstruct i fl))
412  (un:∀i,fl. Q fl → P (Tunion i fl))
413  (cp:∀i. P (Tcomp_ptr i))
414  (nl:Q Fnil)
415  (cs:∀i,t,f'. P t → Q f' → Q (Fcons i t f'))
416  (fs:fieldlist) on fs : Q fs ≝
417  match fs return λfs'.Q fs' with
418  [ Fnil ⇒ nl
419  | Fcons i t f' ⇒ cs i t f' (type_ind2 P Q vo it fl pt ar fn st un cp nl cs t)
420                        (fieldlist_ind2 P Q vo it fl pt ar fn st un cp nl cs f')
421  ].
422
423lemma alignof_fields_pos:
424  ∀f. alignof_fields f > 0.
425@fieldlist_ind //;
426#i #t #fs' #IH @max_r @IH qed.
427
428lemma alignof_pos:
429  ∀t. alignof t > 0.
430#t elim t; normalize; //;
431[ 1,2: #z cases z; /2/;
432| 3,4: #i @alignof_fields_pos
433] qed.
434
435(* * Size of a type, in bytes. *)
436
437let rec sizeof (t: type) : nat ≝
438  match t with
439  [ Tvoid ⇒ 1
440  | Tint i _ ⇒ match i with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
441  | Tfloat f ⇒ match f with [ F32 ⇒ 4 | F64 ⇒ 8 ]
442  | Tpointer _ ⇒ size_pointer
443  | Tarray t' n ⇒ sizeof t' * max 1 n
444  | Tfunction _ _ ⇒ 1
445  | Tstruct _ fld ⇒ align (max 1 (sizeof_struct fld 0)) (alignof t)
446  | Tunion _ fld ⇒ align (max 1 (sizeof_union fld)) (alignof t)
447  | Tcomp_ptr _ ⇒ size_pointer
448  ]
449
450and sizeof_struct (fld: fieldlist) (pos: nat) on fld : nat ≝
451  match fld with
452  [ Fnil ⇒ pos
453  | Fcons id t fld' ⇒ sizeof_struct fld' (align pos (alignof t) + sizeof t)
454  ]
455
456and sizeof_union (fld: fieldlist) : nat ≝
457  match fld with
458  [ Fnil ⇒ 0
459  | Fcons id t fld' ⇒ max (sizeof t) (sizeof_union fld')
460  ].
461(* TODO: needs some Z_times results
462lemma sizeof_pos:
463  ∀t. sizeof t > 0.
464#t0
465napply (type_ind2 (λt. sizeof t > 0)
466                  (λf. sizeof_union f ≥ 0 ∧ ∀pos:Z. pos ≥ 0 → sizeof_struct f pos ≥ 0));
467[ 1,4,6,9: //;
468| #i cases i;#s //;
469| #f cases f;//
470| #t #n #H whd in ⊢ (?%?);
471Proof.
472  intro t0.
473  apply (type_ind2 (fun t => sizeof t > 0)
474                   (fun f => sizeof_union f >= 0 /\ forall pos, pos >= 0 -> sizeof_struct f pos >= 0));
475  intros; simpl; auto; try omega.
476  destruct i; omega.
477  destruct f; omega.
478  apply Zmult_gt_0_compat. auto. generalize (Zmax1 1 z); omega.
479  destruct H.
480  generalize (align_le (Zmax 1 (sizeof_struct f 0)) (alignof_fields f) (alignof_fields_pos f)).
481  generalize (Zmax1 1 (sizeof_struct f 0)). omega.
482  generalize (align_le (Zmax 1 (sizeof_union f)) (alignof_fields f) (alignof_fields_pos f)).
483  generalize (Zmax1 1 (sizeof_union f)). omega.
484  split. omega. auto.
485  destruct H0. split; intros.
486  generalize (Zmax2 (sizeof t) (sizeof_union f)). omega.
487  apply H1.
488  generalize (align_le pos (alignof t) (alignof_pos t)). omega.
489Qed.
490
491Lemma sizeof_struct_incr:
492  forall fld pos, pos <= sizeof_struct fld pos.
493Proof.
494  induction fld; intros; simpl. omega.
495  eapply Zle_trans. 2: apply IHfld.
496  apply Zle_trans with (align pos (alignof t)).
497  apply align_le. apply alignof_pos.
498  assert (sizeof t > 0) by apply sizeof_pos. omega.
499Qed.
500
501(** Byte offset for a field in a struct or union.
502  Field are laid out consecutively, and padding is inserted
503  to align each field to the natural alignment for its type. *)
504
505Open Local Scope string_scope.
506*)
507axiom UnknownField : String.
508
509let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
510                              on fld : res nat ≝
511  match fld with
512  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
513  | Fcons id' t fld' ⇒
514      match ident_eq id id' with
515      [ inl _ ⇒ OK ? (align pos (alignof t))
516      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
517      ]
518  ].
519
520definition field_offset ≝ λid: ident. λfld: fieldlist.
521  field_offset_rec id fld 0.
522
523let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
524  match fld with
525  [ Fnil ⇒ Error ? [MSG UnknownField (*"Unknown field "*); CTX ? id]
526  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
527  ].
528
529(* * Some sanity checks about field offsets.  First, field offsets are
530  within the range of acceptable offsets. *)
531(*
532Remark field_offset_rec_in_range:
533  forall id ofs ty fld pos,
534  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
535  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
536Proof.
537  intros until ty. induction fld; simpl.
538  congruence.
539  destruct (ident_eq id i); intros.
540  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
541  exploit IHfld; eauto. intros [A B]. split; auto.
542  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
543  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
544Qed.
545
546Lemma field_offset_in_range:
547  forall id fld ofs ty,
548  field_offset id fld = OK ofs → field_type id fld = OK ty →
549  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
550Proof.
551  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
552Qed.
553
554(** Second, two distinct fields do not overlap *)
555
556Lemma field_offset_no_overlap:
557  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
558  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
559  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
560  id1 <> id2 →
561  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
562Proof.
563  intros until ty2. intros fld0 A B C D NEQ.
564  assert (forall fld pos,
565  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
566  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
567  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
568  induction fld; intro pos; simpl. congruence.
569  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
570  congruence.
571  subst i. intros. inv H; inv H0.
572  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
573  subst i. intros. inv H1; inv H2.
574  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
575  intros. eapply IHfld; eauto.
576
577  apply H with fld0 0; auto.
578Qed.
579
580(** Third, if a struct is a prefix of another, the offsets of fields
581  in common is the same. *)
582
583Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
584  match fld1 with
585  | Fnil ⇒ fld2
586  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
587  end.
588
589Lemma field_offset_prefix:
590  forall id ofs fld2 fld1,
591  field_offset id fld1 = OK ofs →
592  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
593Proof.
594  intros until fld2.
595  assert (forall fld1 pos,
596    field_offset_rec id fld1 pos = OK ofs ->
597    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
598  induction fld1; intros pos; simpl. congruence.
599  destruct (ident_eq id i); auto.
600  intros. unfold field_offset; auto.
601Qed.
602*)
603
604
605(* * Translating Clight types to Cminor types, function signatures,
606  and external functions. *)
607
608definition typ_of_type : type → typ ≝ λt.
609  match t with
610  [ Tvoid ⇒ ASTint I32 Unsigned
611  | Tint sz sg ⇒ ASTint sz sg
612  | Tfloat sz ⇒ ASTfloat sz
613  | Tpointer _ ⇒ ASTptr
614  | Tarray _ _ ⇒ ASTptr
615  | Tfunction _ _ ⇒ ASTptr
616  | Tcomp_ptr _ ⇒ ASTptr
617  | _ ⇒ ASTint I32 Unsigned (* structs and unions shouldn't be converted? *)
618  ].
619
620definition opttyp_of_type : type → option typ ≝ λt.
621  match t with
622  [ Tvoid ⇒ None ?
623  | Tint sz sg ⇒ Some ? (ASTint sz sg)
624  | Tfloat sz ⇒ Some ? (ASTfloat sz)
625  | Tpointer _ ⇒ Some ? ASTptr
626  | Tarray _ _ ⇒ Some ? ASTptr
627  | Tfunction _ _ ⇒ Some ? ASTptr
628  | Tcomp_ptr _ ⇒ Some ? ASTptr
629  | _ ⇒ None ? (* structs and unions shouldn't be converted? *)
630  ].
631
632let rec typlist_of_typelist (tl: typelist) : list typ ≝
633  match tl with
634  [ Tnil ⇒ nil ?
635  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
636  ].
637
638
639(* * The [access_mode] function describes how a variable of the given
640type must be accessed:
641- [By_value ch]: access by value, i.e. by loading from the address
642  of the variable using the memory chunk [ch];
643- [By_reference]: access by reference, i.e. by just returning
644  the address of the variable;
645- [By_nothing]: no access is possible, e.g. for the [void] type.
646
647We currently do not support 64-bit integers and 128-bit floats, so these
648have an access mode of [By_nothing].
649*)
650
651inductive mode: typ → Type[0] ≝
652  | By_value: ∀t:typ. mode t
653  | By_reference: (*∀r:region.*) mode ASTptr
654  | By_nothing: ∀t. mode t.
655
656definition access_mode : ∀ty. mode (typ_of_type ty) ≝ λty.
657  match ty return λty. mode (typ_of_type ty) with
658  [ Tint i s ⇒ By_value (ASTint i s)
659  | Tfloat sz ⇒ By_value (ASTfloat sz)
660  | Tvoid ⇒ By_nothing …
661  | Tpointer _ ⇒ By_value ASTptr
662  | Tarray _ _ ⇒ By_reference
663  | Tfunction _ _ ⇒ By_reference
664  | Tstruct _ fList ⇒ By_nothing …
665  | Tunion _ fList ⇒ By_nothing …
666  | Tcomp_ptr _ ⇒ By_value ASTptr
667  ].
668
669definition signature_of_type : typelist → type → signature ≝ λargs. λres.
670  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
671
672definition external_function
673    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
674  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.