source: C-semantics/AST.ma @ 10

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

Add binary arithmetic libraries, use for integers and identifiers (but
we're not doing modular arithmetic yet.)
Add a dummy "tree" implementation to make environment lookups executable.
Fix if .. then .. else .. precedence.

File size: 13.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(* * 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
152Definition transf_program (l: list (ident * A)) : list (ident * B) :=
153  List.map (fun id_fn => (fst id_fn, transf (snd id_fn))) l.
154
155Definition transform_program (p: program A V) : program B V :=
156  mkprogram
157    (transf_program p.(prog_funct))
158    p.(prog_main)
159    p.(prog_vars).
160
161Lemma transform_program_function:
162  forall p i tf,
163  In (i, tf) (transform_program p).(prog_funct) ->
164  exists f, In (i, f) p.(prog_funct) /\ transf f = tf.
165Proof.
166  simpl. unfold transf_program. intros.
167  exploit list_in_map_inv; eauto.
168  intros [[i' f] [EQ IN]]. simpl in EQ. inversion EQ; subst.
169  exists f; split; auto.
170Qed.
171
172End TRANSF_PROGRAM.
173
174(** The following is a variant of [transform_program] where the
175  code transformation function can fail and therefore returns an
176  option type. *)
177
178Open Local Scope error_monad_scope.
179Open Local Scope string_scope.
180
181Section MAP_PARTIAL.
182
183Variable A B C: Type.
184Variable prefix_errmsg: A -> errmsg.
185Variable f: B -> res C.
186
187Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
188  match l with
189  | nil => OK nil
190  | (a, b) :: rem =>
191      match f b with
192      | Error msg => Error (prefix_errmsg a ++ msg)%list
193      | OK c =>
194          do rem' <- map_partial rem;
195          OK ((a, c) :: rem')
196      end
197  end.
198
199Remark In_map_partial:
200  forall l l' a c,
201  map_partial l = OK l' ->
202  In (a, c) l' ->
203  exists b, In (a, b) l /\ f b = OK c.
204Proof.
205  induction l; simpl.
206  intros. inv H. elim H0.
207  intros until c. destruct a as [a1 b1].
208  caseEq (f b1); try congruence.
209  intro c1; intros. monadInv H0.
210  elim H1; intro. inv H0. exists b1; auto.
211  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
212Qed.
213
214Remark map_partial_forall2:
215  forall l l',
216  map_partial l = OK l' ->
217  list_forall2
218    (fun (a_b: A * B) (a_c: A * C) =>
219       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
220    l l'.
221Proof.
222  induction l; simpl.
223  intros. inv H. constructor.
224  intro l'. destruct a as [a b].
225  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
226  constructor. simpl. auto. auto.
227Qed.
228
229End MAP_PARTIAL.
230
231Remark map_partial_total:
232  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
233  map_partial prefix (fun b => OK (f b)) l =
234  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
235Proof.
236  induction l; simpl.
237  auto.
238  destruct a as [a1 b1]. rewrite IHl. reflexivity.
239Qed.
240
241Remark map_partial_identity:
242  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
243  map_partial prefix (fun b => OK b) l = OK l.
244Proof.
245  induction l; simpl.
246  auto.
247  destruct a as [a1 b1]. rewrite IHl. reflexivity.
248Qed.
249
250Section TRANSF_PARTIAL_PROGRAM.
251
252Variable A B V: Type.
253Variable transf_partial: A -> res B.
254
255Definition prefix_funct_name (id: ident) : errmsg :=
256  MSG "In function " :: CTX id :: MSG ": " :: nil.
257
258Definition transform_partial_program (p: program A V) : res (program B V) :=
259  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
260  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
261
262Lemma transform_partial_program_function:
263  forall p tp i tf,
264  transform_partial_program p = OK tp ->
265  In (i, tf) tp.(prog_funct) ->
266  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
267Proof.
268  intros. monadInv H. simpl in H0. 
269  eapply In_map_partial; eauto.
270Qed.
271
272Lemma transform_partial_program_main:
273  forall p tp,
274  transform_partial_program p = OK tp ->
275  tp.(prog_main) = p.(prog_main).
276Proof.
277  intros. monadInv H. reflexivity.
278Qed.
279
280Lemma transform_partial_program_vars:
281  forall p tp,
282  transform_partial_program p = OK tp ->
283  tp.(prog_vars) = p.(prog_vars).
284Proof.
285  intros. monadInv H. reflexivity.
286Qed.
287
288End TRANSF_PARTIAL_PROGRAM.
289
290(** The following is a variant of [transform_program_partial] where
291  both the program functions and the additional variable information
292  are transformed by functions that can fail. *)
293
294Section TRANSF_PARTIAL_PROGRAM2.
295
296Variable A B V W: Type.
297Variable transf_partial_function: A -> res B.
298Variable transf_partial_variable: V -> res W.
299
300Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
301  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
302
303Definition transform_partial_program2 (p: program A V) : res (program B W) :=
304  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
305  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
306  OK (mkprogram fl p.(prog_main) vl).
307
308Lemma transform_partial_program2_function:
309  forall p tp i tf,
310  transform_partial_program2 p = OK tp ->
311  In (i, tf) tp.(prog_funct) ->
312  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
313Proof.
314  intros. monadInv H. 
315  eapply In_map_partial; eauto.
316Qed.
317
318Lemma transform_partial_program2_variable:
319  forall p tp i tv,
320  transform_partial_program2 p = OK tp ->
321  In (i, tv) tp.(prog_vars) ->
322  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
323Proof.
324  intros. monadInv H.
325  eapply In_map_partial; eauto.
326Qed.
327
328Lemma transform_partial_program2_main:
329  forall p tp,
330  transform_partial_program2 p = OK tp ->
331  tp.(prog_main) = p.(prog_main).
332Proof.
333  intros. monadInv H. reflexivity.
334Qed.
335
336End TRANSF_PARTIAL_PROGRAM2.
337
338(** The following is a relational presentation of
339  [transform_program_partial2].  Given relations between function
340  definitions and between variable information, it defines a relation
341  between programs stating that the two programs have the same shape
342  (same global names, etc) and that identically-named function definitions
343  are variable information are related. *)
344
345Section MATCH_PROGRAM.
346
347Variable A B V W: Type.
348Variable match_fundef: A -> B -> Prop.
349Variable match_varinfo: V -> W -> Prop.
350
351Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
352  match x1, x2 with
353  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
354  end.
355
356Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
357  match x1, x2 with
358  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
359  end.
360
361Definition match_program (p1: program A V) (p2: program B W) : Prop :=
362  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
363  /\ p1.(prog_main) = p2.(prog_main)
364  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
365
366End MATCH_PROGRAM.
367
368Remark transform_partial_program2_match:
369  forall (A B V W: Type)
370         (transf_partial_function: A -> res B)
371         (transf_partial_variable: V -> res W)
372         (p: program A V) (tp: program B W),
373  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
374  match_program
375    (fun fd tfd => transf_partial_function fd = OK tfd)
376    (fun info tinfo => transf_partial_variable info = OK tinfo)
377    p tp.
378Proof.
379  intros. monadInv H. split.
380  apply list_forall2_imply with
381    (fun (ab: ident * A) (ac: ident * B) =>
382       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
383  eapply map_partial_forall2. eauto.
384  intros. destruct v1; destruct v2; simpl in *. auto.
385  split. auto.
386  apply list_forall2_imply with
387    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
388       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
389  eapply map_partial_forall2. eauto.
390  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
391Qed.
392*)
393(* * * External functions *)
394
395(* * For most languages, the functions composing the program are either
396  internal functions, defined within the language, or external functions
397  (a.k.a. system calls) that emit an event when applied.  We define
398  a type for such functions and some generic transformation functions. *)
399
400nrecord external_function : Type ≝ {
401  ef_id: ident;
402  ef_sig: signature
403}.
404
405ninductive fundef (F: Type): Type ≝
406  | Internal: F → fundef F
407  | External: external_function → fundef F.
408
409(* Implicit Arguments External [F]. *)
410(*
411Section TRANSF_FUNDEF.
412
413Variable A B: Type.
414Variable transf: A -> B.
415
416Definition transf_fundef (fd: fundef A): fundef B :=
417  match fd with
418  | Internal f => Internal (transf f)
419  | External ef => External ef
420  end.
421
422End TRANSF_FUNDEF.
423
424Section TRANSF_PARTIAL_FUNDEF.
425
426Variable A B: Type.
427Variable transf_partial: A -> res B.
428
429Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
430  match fd with
431  | Internal f => do f' <- transf_partial f; OK (Internal f')
432  | External ef => OK (External ef)
433  end.
434
435End TRANSF_PARTIAL_FUNDEF.
436*)
Note: See TracBrowser for help on using the repository browser.