source: src/Clight/Csyntax.ma @ 1139

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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