source: src/Clight/Csyntax.ma @ 816

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

Clight to Cminor compilation, modulo switch statements, temporary
generation, 32 to 8 bit translation and miscellaneous bugs.

Also, remove (unused) signatures from function call statements in Cminor
and RTLabs; and separate comparison of integers and pointers in Clight
semantics.

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