source: C-semantics/AST.ma @ 9

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

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

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