source: C-semantics/AST.ma @ 3

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

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

File size: 13.4 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(* * This file defines a number of data types and operations used in
17  the abstract syntax trees of many of the intermediate languages. *)
18
19include "datatypes/sums.ma".
20include "extralib.ma".
21include "Integers.ma".
22include "Floats.ma".
23
24(* * * Syntactic elements *)
25
26(* * Identifiers (names of local variables, of global symbols and functions,
27  etc) are represented by the type [positive] of positive integers. *)
28(*
29Definition ident := positive.
30
31Definition ident_eq := peq.
32*)
33(* TODO: define ident *)
34naxiom ident:Type[0].
35naxiom ident_eq: ∀x,y:ident. (x=y) + (x≠y).
36
37(* * The intermediate languages are weakly typed, using only two types:
38  [Tint] for integers and pointers, and [Tfloat] for floating-point
39  numbers. *)
40
41ninductive typ : Type ≝
42  | Tint : typ
43  | Tfloat : typ.
44
45ndefinition typesize : typ → Z ≝ λty.
46  match ty return λ_.Z with  [ Tint ⇒ 4 | Tfloat ⇒ 8 ].
47
48nlemma typesize_pos: ∀ty. typesize ty > 0.
49#ty; ncases ty; //; nqed.
50
51nlemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
52#t1;#t2;ncases t1;ncases t2;/2/; @2; napply nmk; #H; ndestruct; nqed.
53
54nlemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
55#t1;#t2;ncases t1;ncases t2;/2/;
56##[ ##1,2: #ty; @2; napply nmk; #H; ndestruct;
57##| #ty1;#ty2; nelim (typ_eq ty1 ty2); /2/; #neq; @2; napply nmk;
58    #H; ndestruct; /2/;
59##] nqed.
60
61(* * Additionally, function definitions and function calls are annotated
62  by function signatures indicating the number and types of arguments,
63  as well as the type of the returned value if any.  These signatures
64  are used in particular to determine appropriate calling conventions
65  for the function. *)
66
67nrecord signature : Type ≝ {
68  sig_args: list typ;
69  sig_res: option typ
70}.
71
72ndefinition proj_sig_res : signature → typ ≝ λs.
73  match sig_res s with
74  [ None ⇒ Tint
75  | Some t ⇒ t
76  ].
77
78(* * Memory accesses (load and store instructions) are annotated by
79  a ``memory chunk'' indicating the type, size and signedness of the
80  chunk of memory being accessed. *)
81
82ninductive memory_chunk : Type[0] ≝
83  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
84  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
85  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
86  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
87  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
88  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
89  | Mfloat64 : memory_chunk.       (*r 64-bit double-precision float *)
90
91(* * Initialization data for global variables. *)
92
93ninductive init_data: Type[0] ≝
94  | Init_int8: int → init_data
95  | Init_int16: int → init_data
96  | Init_int32: int → init_data
97  | Init_float32: float → init_data
98  | Init_float64: float → init_data
99  | Init_space: Z → init_data
100  | Init_addrof: ident → int → init_data   (*r address of symbol + offset *)
101  | Init_pointer: list init_data → init_data.
102
103(* * Whole programs consist of:
104- a collection of function definitions (name and description);
105- the name of the ``main'' function that serves as entry point in the program;
106- a collection of global variable declarations, consisting of
107  a name, initialization data, and additional information.
108
109The type of function descriptions and that of additional information
110for variables vary among the various intermediate languages and are
111taken as parameters to the [program] type.  The other parts of whole
112programs are common to all languages. *)
113
114nrecord program (F,V: Type) : Type := {
115  prog_funct: list (ident × F);
116  prog_main: ident;
117  prog_vars: list (ident × (list init_data) × V)
118}.
119
120ndefinition prog_funct_names ≝ λF,V: Type. λp: program F V.
121  map ?? (fst ident F) (prog_funct ?? p).
122
123ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
124  map ?? (λx: ident × (list init_data) × V. fst ?? (fst ?? x)) (prog_vars ?? p).
125(*
126(** * Generic transformations over programs *)
127
128(** We now define a general iterator over programs that applies a given
129  code transformation function to all function descriptions and leaves
130  the other parts of the program unchanged. *)
131
132Section TRANSF_PROGRAM.
133
134Variable A B V: Type.
135Variable transf: A -> B.
136
137Definition transf_program (l: list (ident * A)) : list (ident * B) :=
138  List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
139
140Definition transform_program (p: program A V) : program B V :=
141  mkprogram
142    (transf_program p.(prog_funct))
143    p.(prog_main)
144    p.(prog_vars).
145
146Lemma transform_program_function:
147  forall p i tf,
148  In (i, tf) (transform_program p).(prog_funct) ->
149  exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
150Proof.
151  simpl. unfold transf_program. intros.
152  exploit list_in_map_inv; eauto.
153  intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst.
154  exists f; split; auto.
155Qed.
156
157End TRANSF_PROGRAM.
158
159(** The following is a variant of [transform_program] where the
160  code transformation function can fail and therefore returns an
161  option type. *)
162
163Open Local Scope error_monad_scope.
164Open Local Scope string_scope.
165
166Section MAP_PARTIAL.
167
168Variable A B C: Type.
169Variable prefix_errmsg: A -> errmsg.
170Variable f: B -> res C.
171
172Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
173  match l with
174  | nil => OK nil
175  | (a, b) :: rem =>
176      match f b with
177      | Error msg => Error (prefix_errmsg a ++ msg)%list
178      | OK c =>
179          do rem' <- map_partial rem;
180          OK ((a, c) :: rem')
181      end
182  end.
183
184Remark In_map_partial:
185  forall l l' a c,
186  map_partial l = OK l' ->
187  In (a, c) l' ->
188  exists b, In (a, b) l /\ f b = OK c.
189Proof.
190  induction l; simpl.
191  intros. inv H. elim H0.
192  intros until c. destruct a as [a1 b1].
193  caseEq (f b1); try congruence.
194  intro c1; intros. monadInv H0.
195  elim H1; intro. inv H0. exists b1; auto.
196  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
197Qed.
198
199Remark map_partial_forall2:
200  forall l l',
201  map_partial l = OK l' ->
202  list_forall2
203    (fun (a_b: A * B) (a_c: A * C) =>
204       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
205    l l'.
206Proof.
207  induction l; simpl.
208  intros. inv H. constructor.
209  intro l'. destruct a as [a b].
210  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
211  constructor. simpl. auto. auto.
212Qed.
213
214End MAP_PARTIAL.
215
216Remark map_partial_total:
217  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
218  map_partial prefix (fun b => OK (f b)) l =
219  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
220Proof.
221  induction l; simpl.
222  auto.
223  destruct a as [a1 b1]. rewrite IHl. reflexivity.
224Qed.
225
226Remark map_partial_identity:
227  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
228  map_partial prefix (fun b => OK b) l = OK l.
229Proof.
230  induction l; simpl.
231  auto.
232  destruct a as [a1 b1]. rewrite IHl. reflexivity.
233Qed.
234
235Section TRANSF_PARTIAL_PROGRAM.
236
237Variable A B V: Type.
238Variable transf_partial: A -> res B.
239
240Definition prefix_funct_name (id: ident) : errmsg :=
241  MSG "In function " :: CTX id :: MSG ": " :: nil.
242
243Definition transform_partial_program (p: program A V) : res (program B V) :=
244  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
245  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
246
247Lemma transform_partial_program_function:
248  forall p tp i tf,
249  transform_partial_program p = OK tp ->
250  In (i, tf) tp.(prog_funct) ->
251  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
252Proof.
253  intros. monadInv H. simpl in H0. 
254  eapply In_map_partial; eauto.
255Qed.
256
257Lemma transform_partial_program_main:
258  forall p tp,
259  transform_partial_program p = OK tp ->
260  tp.(prog_main) = p.(prog_main).
261Proof.
262  intros. monadInv H. reflexivity.
263Qed.
264
265Lemma transform_partial_program_vars:
266  forall p tp,
267  transform_partial_program p = OK tp ->
268  tp.(prog_vars) = p.(prog_vars).
269Proof.
270  intros. monadInv H. reflexivity.
271Qed.
272
273End TRANSF_PARTIAL_PROGRAM.
274
275(** The following is a variant of [transform_program_partial] where
276  both the program functions and the additional variable information
277  are transformed by functions that can fail. *)
278
279Section TRANSF_PARTIAL_PROGRAM2.
280
281Variable A B V W: Type.
282Variable transf_partial_function: A -> res B.
283Variable transf_partial_variable: V -> res W.
284
285Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
286  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
287
288Definition transform_partial_program2 (p: program A V) : res (program B W) :=
289  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
290  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
291  OK (mkprogram fl p.(prog_main) vl).
292
293Lemma transform_partial_program2_function:
294  forall p tp i tf,
295  transform_partial_program2 p = OK tp ->
296  In (i, tf) tp.(prog_funct) ->
297  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
298Proof.
299  intros. monadInv H. 
300  eapply In_map_partial; eauto.
301Qed.
302
303Lemma transform_partial_program2_variable:
304  forall p tp i tv,
305  transform_partial_program2 p = OK tp ->
306  In (i, tv) tp.(prog_vars) ->
307  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
308Proof.
309  intros. monadInv H.
310  eapply In_map_partial; eauto.
311Qed.
312
313Lemma transform_partial_program2_main:
314  forall p tp,
315  transform_partial_program2 p = OK tp ->
316  tp.(prog_main) = p.(prog_main).
317Proof.
318  intros. monadInv H. reflexivity.
319Qed.
320
321End TRANSF_PARTIAL_PROGRAM2.
322
323(** The following is a relational presentation of
324  [transform_program_partial2].  Given relations between function
325  definitions and between variable information, it defines a relation
326  between programs stating that the two programs have the same shape
327  (same global names, etc) and that identically-named function definitions
328  are variable information are related. *)
329
330Section MATCH_PROGRAM.
331
332Variable A B V W: Type.
333Variable match_fundef: A -> B -> Prop.
334Variable match_varinfo: V -> W -> Prop.
335
336Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
337  match x1, x2 with
338  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
339  end.
340
341Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
342  match x1, x2 with
343  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
344  end.
345
346Definition match_program (p1: program A V) (p2: program B W) : Prop :=
347  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
348  /\ p1.(prog_main) = p2.(prog_main)
349  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
350
351End MATCH_PROGRAM.
352
353Remark transform_partial_program2_match:
354  forall (A B V W: Type)
355         (transf_partial_function: A -> res B)
356         (transf_partial_variable: V -> res W)
357         (p: program A V) (tp: program B W),
358  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
359  match_program
360    (fun fd tfd => transf_partial_function fd = OK tfd)
361    (fun info tinfo => transf_partial_variable info = OK tinfo)
362    p tp.
363Proof.
364  intros. monadInv H. split.
365  apply list_forall2_imply with
366    (fun (ab: ident * A) (ac: ident * B) =>
367       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
368  eapply map_partial_forall2. eauto.
369  intros. destruct v1; destruct v2; simpl in *. auto.
370  split. auto.
371  apply list_forall2_imply with
372    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
373       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
374  eapply map_partial_forall2. eauto.
375  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
376Qed.
377*)
378(* * * External functions *)
379
380(* * For most languages, the functions composing the program are either
381  internal functions, defined within the language, or external functions
382  (a.k.a. system calls) that emit an event when applied.  We define
383  a type for such functions and some generic transformation functions. *)
384
385nrecord external_function : Type ≝ {
386  ef_id: ident;
387  ef_sig: signature
388}.
389
390ninductive fundef (F: Type): Type ≝
391  | Internal: F → fundef F
392  | External: external_function → fundef F.
393
394(* Implicit Arguments External [F]. *)
395(*
396Section TRANSF_FUNDEF.
397
398Variable A B: Type.
399Variable transf: A -> B.
400
401Definition transf_fundef (fd: fundef A): fundef B :=
402  match fd with
403  | Internal f => Internal (transf f)
404  | External ef => External ef
405  end.
406
407End TRANSF_FUNDEF.
408
409Section TRANSF_PARTIAL_FUNDEF.
410
411Variable A B: Type.
412Variable transf_partial: A -> res B.
413
414Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
415  match fd with
416  | Internal f => do f' <- transf_partial f; OK (Internal f')
417  | External ef => OK (External ef)
418  end.
419
420End TRANSF_PARTIAL_FUNDEF.
421*)
Note: See TracBrowser for help on using the repository browser.