source: src/Clight/Csyntax.ma @ 744

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

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate 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 "Clight/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*)
519let rec field_offset_rec (id: ident) (fld: fieldlist) (pos: nat)
520                              on fld : res nat ≝
521  match fld with
522  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
523  | Fcons id' t fld' ⇒
524      match ident_eq id id' with
525      [ inl _ ⇒ OK ? (align pos (alignof t))
526      | inr _ ⇒ field_offset_rec id fld' (align pos (alignof t) + sizeof t)
527      ]
528  ].
529
530definition field_offset ≝ λid: ident. λfld: fieldlist.
531  field_offset_rec id fld 0.
532
533let rec field_type (id: ident) (fld: fieldlist) on fld : res type :=
534  match fld with
535  [ Fnil ⇒ Error ? (*MSG "Unknown field " :: CTX id :: nil*)
536  | Fcons id' t fld' ⇒ match ident_eq id id' with [ inl _ ⇒ OK ? t | inr _ ⇒ field_type id fld']
537  ].
538
539(* * Some sanity checks about field offsets.  First, field offsets are
540  within the range of acceptable offsets. *)
541(*
542Remark field_offset_rec_in_range:
543  forall id ofs ty fld pos,
544  field_offset_rec id fld pos = OK ofs → field_type id fld = OK ty →
545  pos <= ofs /\ ofs + sizeof ty <= sizeof_struct fld pos.
546Proof.
547  intros until ty. induction fld; simpl.
548  congruence.
549  destruct (ident_eq id i); intros.
550  inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr.
551  exploit IHfld; eauto. intros [A B]. split; auto.
552  eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof t)).
553  apply align_le. apply alignof_pos. generalize (sizeof_pos t). omega.
554Qed.
555
556Lemma field_offset_in_range:
557  forall id fld ofs ty,
558  field_offset id fld = OK ofs → field_type id fld = OK ty →
559  0 <= ofs /\ ofs + sizeof ty <= sizeof_struct fld 0.
560Proof.
561  intros. eapply field_offset_rec_in_range. unfold field_offset in H; eauto. eauto.
562Qed.
563
564(** Second, two distinct fields do not overlap *)
565
566Lemma field_offset_no_overlap:
567  forall id1 ofs1 ty1 id2 ofs2 ty2 fld,
568  field_offset id1 fld = OK ofs1 → field_type id1 fld = OK ty1 →
569  field_offset id2 fld = OK ofs2 → field_type id2 fld = OK ty2 →
570  id1 <> id2 →
571  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1.
572Proof.
573  intros until ty2. intros fld0 A B C D NEQ.
574  assert (forall fld pos,
575  field_offset_rec id1 fld pos = OK ofs1 -> field_type id1 fld = OK ty1 ->
576  field_offset_rec id2 fld pos = OK ofs2 -> field_type id2 fld = OK ty2 ->
577  ofs1 + sizeof ty1 <= ofs2 \/ ofs2 + sizeof ty2 <= ofs1).
578  induction fld; intro pos; simpl. congruence.
579  destruct (ident_eq id1 i); destruct (ident_eq id2 i).
580  congruence.
581  subst i. intros. inv H; inv H0.
582  exploit field_offset_rec_in_range. eexact H1. eauto. tauto. 
583  subst i. intros. inv H1; inv H2.
584  exploit field_offset_rec_in_range. eexact H. eauto. tauto.
585  intros. eapply IHfld; eauto.
586
587  apply H with fld0 0; auto.
588Qed.
589
590(** Third, if a struct is a prefix of another, the offsets of fields
591  in common is the same. *)
592
593Fixpoint fieldlist_app (fld1 fld2: fieldlist) {struct fld1} : fieldlist :=
594  match fld1 with
595  | Fnil ⇒ fld2
596  | Fcons id ty fld ⇒ Fcons id ty (fieldlist_app fld fld2)
597  end.
598
599Lemma field_offset_prefix:
600  forall id ofs fld2 fld1,
601  field_offset id fld1 = OK ofs →
602  field_offset id (fieldlist_app fld1 fld2) = OK ofs.
603Proof.
604  intros until fld2.
605  assert (forall fld1 pos,
606    field_offset_rec id fld1 pos = OK ofs ->
607    field_offset_rec id (fieldlist_app fld1 fld2) pos = OK ofs).
608  induction fld1; intros pos; simpl. congruence.
609  destruct (ident_eq id i); auto.
610  intros. unfold field_offset; auto.
611Qed.
612*)
613(* * The [access_mode] function describes how a variable of the given
614type must be accessed:
615- [By_value ch]: access by value, i.e. by loading from the address
616  of the variable using the memory chunk [ch];
617- [By_reference]: access by reference, i.e. by just returning
618  the address of the variable;
619- [By_nothing]: no access is possible, e.g. for the [void] type.
620
621We currently do not support 64-bit integers and 128-bit floats, so these
622have an access mode of [By_nothing].
623*)
624
625inductive mode: Type[0] ≝
626  | By_value: memory_chunk → mode
627  | By_reference: region → mode
628  | By_nothing: mode.
629
630definition access_mode : type → mode ≝ λty.
631  match ty with
632  [ Tint i s ⇒
633    match i with [ I8 ⇒
634      match s with [ Signed ⇒ By_value Mint8signed
635                   | Unsigned ⇒ By_value Mint8unsigned ]
636                 | I16 ⇒
637      match s with [ Signed ⇒ By_value Mint16signed
638                   | Unsigned ⇒ By_value Mint16unsigned ]
639                 | I32 ⇒ By_value Mint32 ]
640  | Tfloat f ⇒ match f with [ F32 ⇒ By_value Mfloat32
641                            | F64 ⇒ By_value Mfloat64 ]
642  | Tvoid ⇒ By_nothing
643  | Tpointer r _ ⇒ By_value (Mpointer r)
644  | Tarray r _ _ ⇒ By_reference r
645  | Tfunction _ _ ⇒ By_reference Code
646  | Tstruct _ fList ⇒ By_nothing
647  | Tunion _ fList ⇒ By_nothing
648  | Tcomp_ptr r _ ⇒ By_value (Mpointer r)
649  ].
650
651(* * Classification of arithmetic operations and comparisons.
652  The following [classify_] functions take as arguments the types
653  of the arguments of an operation.  They return enough information
654  to resolve overloading for this operator applications, such as
655  ``both arguments are floats'', or ``the first is a pointer
656  and the second is an integer''.  These functions are used to resolve
657  overloading both in the dynamic semantics (module [Csem]) and in the
658  compiler (module [Cshmgen]).
659*)
660
661inductive classify_add_cases : Type[0] ≝
662  | add_case_ii: classify_add_cases         (**r int , int *)
663  | add_case_ff: classify_add_cases         (**r float , float *)
664  | add_case_pi: type → classify_add_cases (**r ptr or array, int *)
665  | add_case_ip: type → classify_add_cases (**r int, ptr or array *)
666  | add_default: classify_add_cases.        (**r other *)
667
668definition classify_add ≝ λty1: type. λty2: type.
669(*
670  match ty1, ty2 with
671  [ Tint _ _, Tint _ _ ⇒ add_case_ii
672  | Tfloat _, Tfloat _ ⇒ add_case_ff
673  | Tpointer ty, Tint _ _ ⇒ add_case_pi ty
674  | Tarray ty _, Tint _ _ ⇒ add_case_pi ty
675  | Tint _ _, Tpointer ty ⇒ add_case_ip ty
676  | Tint _ _, Tarray ty _ ⇒ add_case_ip ty
677  | _, _ ⇒ add_default
678  ].
679*)
680  match ty1 with
681  [ Tint _ _ ⇒
682    match ty2 with
683    [ Tint _ _ ⇒ add_case_ii
684    | Tpointer _ ty ⇒ add_case_ip ty
685    | Tarray _ ty _ ⇒ add_case_ip ty
686    | _ ⇒ add_default ]
687  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ add_case_ff | _ ⇒ add_default ]
688  | Tpointer _ ty ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
689  | Tarray _ ty _ ⇒ match ty2 with [Tint _ _ ⇒ add_case_pi ty | _ ⇒ add_default ]
690  | _ ⇒ add_default
691  ].
692
693inductive classify_sub_cases : Type[0] ≝
694  | sub_case_ii: classify_sub_cases          (**r int , int *)
695  | sub_case_ff: classify_sub_cases          (**r float , float *)
696  | sub_case_pi: type → classify_sub_cases  (**r ptr or array , int *)
697  | sub_case_pp: type → classify_sub_cases  (**r ptr or array , ptr or array *)
698  | sub_default: classify_sub_cases .        (**r other *)
699
700definition classify_sub ≝ λty1: type. λty2: type.
701(*  match ty1, ty2 with
702  | Tint _ _ , Tint _ _ ⇒ sub_case_ii
703  | Tfloat _ , Tfloat _ ⇒ sub_case_ff
704  | Tpointer ty , Tint _ _ ⇒ sub_case_pi ty
705  | Tarray ty _ , Tint _ _ ⇒ sub_case_pi ty
706  | Tpointer ty , Tpointer _ ⇒ sub_case_pp ty
707  | Tpointer ty , Tarray _ _⇒ sub_case_pp ty
708  | Tarray ty _ , Tpointer _ ⇒ sub_case_pp ty
709  | Tarray ty _ , Tarray _ _ ⇒ sub_case_pp ty
710  | _ ,_ ⇒ sub_default
711  end.
712*)
713  match ty1 with
714  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ sub_case_ii | _ ⇒ sub_default ]
715  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ sub_case_ff | _ ⇒ sub_default ]
716  | Tpointer _ ty ⇒
717    match ty2 with
718    [ Tint _ _ ⇒ sub_case_pi ty
719    | Tpointer _ _ ⇒ sub_case_pp ty
720    | Tarray _ _ _ ⇒ sub_case_pp ty
721    | _ ⇒ sub_default ]
722  | Tarray _ ty _ ⇒
723    match ty2 with
724    [ Tint _ _ ⇒ sub_case_pi ty
725    | Tpointer _ _ ⇒ sub_case_pp ty
726    | Tarray _ _ _ ⇒ sub_case_pp ty
727    | _ ⇒ sub_default ]
728  | _ ⇒ sub_default
729  ].
730
731inductive classify_mul_cases : Type[0] ≝
732  | mul_case_ii: classify_mul_cases (**r int , int *)
733  | mul_case_ff: classify_mul_cases (**r float , float *)
734  | mul_default: classify_mul_cases . (**r other *)
735
736definition classify_mul ≝ λty1: type. λty2: type.
737  match ty1 with
738  [ Tint _ _ ⇒ match ty2 with [ Tint _ _ ⇒ mul_case_ii | _ ⇒ mul_default ]
739  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ mul_case_ff | _ ⇒ mul_default ]
740  | _ ⇒ mul_default
741  ].
742(*
743  match ty1,ty2 with
744  | Tint _ _, Tint _ _ ⇒ mul_case_ii
745  | Tfloat _ , Tfloat _ ⇒ mul_case_ff
746  | _,_  ⇒ mul_default
747end.
748*)
749inductive classify_div_cases : Type[0] ≝
750  | div_case_I32unsi: classify_div_cases (**r unsigned int32 , int *)
751  | div_case_ii: classify_div_cases    (**r int , int *)
752  | div_case_ff: classify_div_cases    (**r float , float *)
753  | div_default: classify_div_cases. (**r other *)
754
755definition classify_32un_aux ≝ λT:Type[0].λi.λs.λr1:T.λr2:T.
756  match i with [ I32 ⇒
757    match s with [ Unsigned ⇒ r1 | _ ⇒ r2 ]
758  | _ ⇒ r2 ].
759
760definition classify_div ≝ λty1: type. λty2: type.
761  match ty1 with
762  [ Tint i1 s1 ⇒
763    match ty2 with
764    [ Tint i2 s2 ⇒
765      classify_32un_aux ? i1 s1 div_case_I32unsi
766        (classify_32un_aux ? i2 s2 div_case_I32unsi div_case_ii)
767    | _ ⇒ div_default ]
768  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ div_case_ff | _ ⇒ div_default ]
769  | _ ⇒ div_default
770  ].
771(*
772definition classify_div ≝ λty1: type. λty2: type.
773  match ty1,ty2 with
774  | Tint I32 Unsigned, Tint _ _ ⇒ div_case_I32unsi
775  | Tint _ _ , Tint I32 Unsigned ⇒ div_case_I32unsi
776  | Tint _ _ , Tint _ _ ⇒ div_case_ii
777  | Tfloat _ , Tfloat _ ⇒ div_case_ff
778  | _ ,_ ⇒ div_default
779end.
780*)
781inductive classify_mod_cases : Type[0] ≝
782  | mod_case_I32unsi: classify_mod_cases  (**r unsigned I32 , int *)
783  | mod_case_ii: classify_mod_cases  (**r int , int *)
784  | mod_default: classify_mod_cases . (**r other *)
785
786definition classify_mod ≝ λty1:type. λty2:type.
787  match ty1 with
788  [ Tint i1 s1 ⇒
789    match ty2 with
790    [ Tint i2 s2 ⇒
791      classify_32un_aux ? i1 s1 mod_case_I32unsi
792        (classify_32un_aux ? i2 s2 mod_case_I32unsi mod_case_ii)
793    | _ ⇒ mod_default ]
794  | _ ⇒ mod_default
795  ].
796(*
797Definition classify_mod (ty1: type) (ty2: type) :=
798  match ty1,ty2 with
799  | Tint I32 Unsigned , Tint _ _ ⇒ mod_case_I32unsi
800  | Tint _ _ , Tint I32 Unsigned ⇒ mod_case_I32unsi
801  | Tint _ _ , Tint _ _ ⇒ mod_case_ii
802  | _ , _ ⇒ mod_default
803end .
804*)
805inductive classify_shr_cases :Type[0] ≝
806  | shr_case_I32unsi:  classify_shr_cases (**r unsigned I32 , int *)
807  | shr_case_ii :classify_shr_cases (**r int , int *)
808  | shr_default : classify_shr_cases . (**r other *)
809
810definition classify_shr ≝ λty1: type. λty2: type.
811  match ty1 with
812  [ Tint i1 s1 ⇒
813    match ty2 with
814    [ Tint _ _ ⇒
815      classify_32un_aux ? i1 s1 shr_case_I32unsi shr_case_ii
816    | _ ⇒ shr_default ]
817  | _ ⇒ shr_default
818  ].
819
820(*
821Definition classify_shr (ty1: type) (ty2: type) :=
822  match ty1,ty2 with
823  | Tint I32 Unsigned , Tint _ _ ⇒ shr_case_I32unsi
824  | Tint _ _ , Tint _ _ ⇒ shr_case_ii
825  | _ , _ ⇒ shr_default
826  end.
827*)
828inductive classify_cmp_cases : Type[0] ≝
829  | cmp_case_I32unsi: classify_cmp_cases (**r unsigned I32 , int *)
830  | cmp_case_ipip: classify_cmp_cases  (**r int|ptr|array , int|ptr|array*)
831  | cmp_case_ff: classify_cmp_cases  (**r float , float *)
832  | cmp_default: classify_cmp_cases . (**r other *)
833
834definition classify_cmp ≝ λty1:type. λty2:type.
835  match ty1 with
836  [ Tint i1 s1 ⇒
837    match ty2 with
838    [ Tint i2 s2 ⇒
839      classify_32un_aux ? i1 s1 cmp_case_I32unsi
840        (classify_32un_aux ? i2 s2 cmp_case_I32unsi cmp_case_ipip)
841    | _ ⇒ cmp_default ]
842  | Tfloat _ ⇒ match ty2 with [ Tfloat _ ⇒ cmp_case_ff | _ ⇒ cmp_default ]
843  | Tpointer _ _ ⇒
844    match ty2 with
845    [ Tint _ _ ⇒ cmp_case_ipip
846    | Tpointer _ _ ⇒ cmp_case_ipip
847    | Tarray _ _ _ ⇒ cmp_case_ipip
848    | _ ⇒ cmp_default ]
849  | Tarray _ _ _ ⇒
850    match ty2 with
851    [ Tint _ _ ⇒ cmp_case_ipip
852    | Tpointer _ _ ⇒ cmp_case_ipip
853    | Tarray _ _ _ ⇒ cmp_case_ipip
854    | _ ⇒ cmp_default ]
855  | _ ⇒ cmp_default
856  ].
857
858(*
859Definition classify_cmp (ty1: type) (ty2: type) :=
860  match ty1,ty2 with
861  | Tint I32 Unsigned , Tint _ _ ⇒ cmp_case_I32unsi
862  | Tint _ _ , Tint I32 Unsigned ⇒ cmp_case_I32unsi
863  | Tint _ _ , Tint _ _ ⇒ cmp_case_ipip
864  | Tfloat _ , Tfloat _ ⇒ cmp_case_ff
865  | Tpointer _ , Tint _ _ ⇒ cmp_case_ipip
866  | Tarray _ _ , Tint _ _ ⇒ cmp_case_ipip
867  | Tpointer _ , Tpointer _ ⇒ cmp_case_ipip
868  | Tpointer _ , Tarray _ _ ⇒ cmp_case_ipip
869  | Tarray _ _ ,Tpointer _ ⇒ cmp_case_ipip
870  | Tarray _ _ ,Tarray _ _ ⇒ cmp_case_ipip
871  | _ , _ ⇒ cmp_default
872  end.
873*)
874inductive classify_fun_cases : Type[0] ≝
875  | fun_case_f: typelist → type → classify_fun_cases   (**r (pointer to) function *)
876  | fun_default: classify_fun_cases . (**r other *)
877
878definition classify_fun ≝ λty: type.
879  match ty with
880  [ Tfunction args res ⇒ fun_case_f args res
881  | Tpointer _ ty' ⇒ match ty' with [ Tfunction args res ⇒ fun_case_f args res
882                                    | _ ⇒ fun_default
883                                    ]
884  | _ ⇒ fun_default
885  ].
886
887(* * Translating Clight types to Cminor types, function signatures,
888  and external functions. *)
889
890definition typ_of_type : type → typ ≝ λt.
891  match t with
892  [ Tfloat _ ⇒ ASTfloat
893  | _ ⇒ ASTint
894  ].
895
896definition opttyp_of_type : type → option typ ≝ λt.
897  match t with
898  [ Tvoid ⇒ None ?
899  | Tfloat _ ⇒ Some ? ASTfloat
900  | _ ⇒ Some ? ASTint
901  ].
902
903let rec typlist_of_typelist (tl: typelist) : list typ ≝
904  match tl with
905  [ Tnil ⇒ nil ?
906  | Tcons hd tl ⇒ typ_of_type hd :: typlist_of_typelist tl
907  ].
908
909definition signature_of_type : typelist → type → signature ≝ λargs. λres.
910  mk_signature (typlist_of_typelist args) (opttyp_of_type res).
911
912definition external_function
913    : ident → typelist → type → external_function ≝ λid. λtargs. λtres.
914  mk_external_function id (signature_of_type targs tres).
Note: See TracBrowser for help on using the repository browser.