source: C-semantics/Csyntax.ma @ 3

Last change on this file since 3 was 3, checked in by campbell, 10 years ago

Import work-in-progress port of the CompCert? C semantics to matita.

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