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

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

Use pointer-specific "chunks" of memory for pointer loads and stores,
in particular getting rid of Mint24.

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