source: C-semantics/AST.ma @ 82

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

Separate out IOMonad from the rest of the executable semantics.
Start adding simulation results.

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