source: C-semantics/AST.ma @ 153

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

Use appropriate memory chunks for 8051 pointers.

File size: 14.3 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  | Mint24 : memory_chunk
103  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
104  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
105  | Mfloat64 : memory_chunk.       (*r 64-bit double-precision float *)
106
107(* Memory spaces *)
108
109ninductive memory_space : Type ≝
110  | Any : memory_space
111  | Data : memory_space
112  | IData : memory_space
113  | XData : memory_space
114  | Code : memory_space.
115
116(* * Initialization data for global variables. *)
117
118ninductive init_data: Type[0] ≝
119  | Init_int8: int → init_data
120  | Init_int16: int → init_data
121  | Init_int32: int → init_data
122  | Init_float32: float → init_data
123  | Init_float64: float → init_data
124  | Init_space: Z → init_data
125  | Init_addrof: ident → int → init_data   (*r address of symbol + offset *)
126  | Init_pointer: list init_data → init_data.
127
128(* * Whole programs consist of:
129- a collection of function definitions (name and description);
130- the name of the ``main'' function that serves as entry point in the program;
131- a collection of global variable declarations, consisting of
132  a name, initialization data, and additional information.
133
134The type of function descriptions and that of additional information
135for variables vary among the various intermediate languages and are
136taken as parameters to the [program] type.  The other parts of whole
137programs are common to all languages. *)
138
139nrecord program (F,V: Type) : Type := {
140  prog_funct: list (ident × F);
141  prog_main: ident;
142  prog_vars: list (ident × (list init_data) × memory_space × V)
143}.
144
145ndefinition prog_funct_names ≝ λF,V: Type. λp: program F V.
146  map ?? (fst ident F) (prog_funct ?? p).
147
148ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
149  map ?? (λx: ident × (list init_data) × memory_space × V. fst ?? (fst ?? x)) (prog_vars ?? p).
150(*
151(** * Generic transformations over programs *)
152
153(** We now define a general iterator over programs that applies a given
154  code transformation function to all function descriptions and leaves
155  the other parts of the program unchanged. *)
156
157Section TRANSF_PROGRAM.
158
159Variable A B V: Type.
160Variable transf: A -> B.
161*)
162
163ndefinition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
164λA,B,transf,l.
165  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
166
167ndefinition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
168λA,B,V,transf,p.
169  mk_program B V
170    (transf_program ?? transf (prog_funct A V p))
171    (prog_main A V p)
172    (prog_vars A V p).
173
174nlemma transform_program_function:
175  ∀A,B,V,transf,p,i,tf.
176  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
177  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
178nnormalize; #A B V transf p i tf H; nelim (list_in_map_inv ????? H);
179#x; nelim x; #i' tf'; *; #e H; ndestruct; @tf'; /2/;
180nqed.
181
182(*
183End TRANSF_PROGRAM.
184
185(** The following is a variant of [transform_program] where the
186  code transformation function can fail and therefore returns an
187  option type. *)
188
189Open Local Scope error_monad_scope.
190Open Local Scope string_scope.
191
192Section MAP_PARTIAL.
193
194Variable A B C: Type.
195Variable prefix_errmsg: A -> errmsg.
196Variable f: B -> res C.
197
198Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
199  match l with
200  | nil => OK nil
201  | (a, b) :: rem =>
202      match f b with
203      | Error msg => Error (prefix_errmsg a ++ msg)%list
204      | OK c =>
205          do rem' <- map_partial rem;
206          OK ((a, c) :: rem')
207      end
208  end.
209
210Remark In_map_partial:
211  forall l l' a c,
212  map_partial l = OK l' ->
213  In (a, c) l' ->
214  exists b, In (a, b) l /\ f b = OK c.
215Proof.
216  induction l; simpl.
217  intros. inv H. elim H0.
218  intros until c. destruct a as [a1 b1].
219  caseEq (f b1); try congruence.
220  intro c1; intros. monadInv H0.
221  elim H1; intro. inv H0. exists b1; auto.
222  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
223Qed.
224
225Remark map_partial_forall2:
226  forall l l',
227  map_partial l = OK l' ->
228  list_forall2
229    (fun (a_b: A * B) (a_c: A * C) =>
230       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
231    l l'.
232Proof.
233  induction l; simpl.
234  intros. inv H. constructor.
235  intro l'. destruct a as [a b].
236  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
237  constructor. simpl. auto. auto.
238Qed.
239
240End MAP_PARTIAL.
241
242Remark map_partial_total:
243  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
244  map_partial prefix (fun b => OK (f b)) l =
245  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
246Proof.
247  induction l; simpl.
248  auto.
249  destruct a as [a1 b1]. rewrite IHl. reflexivity.
250Qed.
251
252Remark map_partial_identity:
253  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
254  map_partial prefix (fun b => OK b) l = OK l.
255Proof.
256  induction l; simpl.
257  auto.
258  destruct a as [a1 b1]. rewrite IHl. reflexivity.
259Qed.
260
261Section TRANSF_PARTIAL_PROGRAM.
262
263Variable A B V: Type.
264Variable transf_partial: A -> res B.
265
266Definition prefix_funct_name (id: ident) : errmsg :=
267  MSG "In function " :: CTX id :: MSG ": " :: nil.
268
269Definition transform_partial_program (p: program A V) : res (program B V) :=
270  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
271  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
272
273Lemma transform_partial_program_function:
274  forall p tp i tf,
275  transform_partial_program p = OK tp ->
276  In (i, tf) tp.(prog_funct) ->
277  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
278Proof.
279  intros. monadInv H. simpl in H0. 
280  eapply In_map_partial; eauto.
281Qed.
282
283Lemma transform_partial_program_main:
284  forall p tp,
285  transform_partial_program p = OK tp ->
286  tp.(prog_main) = p.(prog_main).
287Proof.
288  intros. monadInv H. reflexivity.
289Qed.
290
291Lemma transform_partial_program_vars:
292  forall p tp,
293  transform_partial_program p = OK tp ->
294  tp.(prog_vars) = p.(prog_vars).
295Proof.
296  intros. monadInv H. reflexivity.
297Qed.
298
299End TRANSF_PARTIAL_PROGRAM.
300
301(** The following is a variant of [transform_program_partial] where
302  both the program functions and the additional variable information
303  are transformed by functions that can fail. *)
304
305Section TRANSF_PARTIAL_PROGRAM2.
306
307Variable A B V W: Type.
308Variable transf_partial_function: A -> res B.
309Variable transf_partial_variable: V -> res W.
310
311Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
312  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
313
314Definition transform_partial_program2 (p: program A V) : res (program B W) :=
315  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
316  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
317  OK (mkprogram fl p.(prog_main) vl).
318
319Lemma transform_partial_program2_function:
320  forall p tp i tf,
321  transform_partial_program2 p = OK tp ->
322  In (i, tf) tp.(prog_funct) ->
323  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
324Proof.
325  intros. monadInv H. 
326  eapply In_map_partial; eauto.
327Qed.
328
329Lemma transform_partial_program2_variable:
330  forall p tp i tv,
331  transform_partial_program2 p = OK tp ->
332  In (i, tv) tp.(prog_vars) ->
333  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
334Proof.
335  intros. monadInv H.
336  eapply In_map_partial; eauto.
337Qed.
338
339Lemma transform_partial_program2_main:
340  forall p tp,
341  transform_partial_program2 p = OK tp ->
342  tp.(prog_main) = p.(prog_main).
343Proof.
344  intros. monadInv H. reflexivity.
345Qed.
346
347End TRANSF_PARTIAL_PROGRAM2.
348
349(** The following is a relational presentation of
350  [transform_program_partial2].  Given relations between function
351  definitions and between variable information, it defines a relation
352  between programs stating that the two programs have the same shape
353  (same global names, etc) and that identically-named function definitions
354  are variable information are related. *)
355
356Section MATCH_PROGRAM.
357
358Variable A B V W: Type.
359Variable match_fundef: A -> B -> Prop.
360Variable match_varinfo: V -> W -> Prop.
361
362Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
363  match x1, x2 with
364  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
365  end.
366
367Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
368  match x1, x2 with
369  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
370  end.
371
372Definition match_program (p1: program A V) (p2: program B W) : Prop :=
373  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
374  /\ p1.(prog_main) = p2.(prog_main)
375  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
376
377End MATCH_PROGRAM.
378
379Remark transform_partial_program2_match:
380  forall (A B V W: Type)
381         (transf_partial_function: A -> res B)
382         (transf_partial_variable: V -> res W)
383         (p: program A V) (tp: program B W),
384  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
385  match_program
386    (fun fd tfd => transf_partial_function fd = OK tfd)
387    (fun info tinfo => transf_partial_variable info = OK tinfo)
388    p tp.
389Proof.
390  intros. monadInv H. split.
391  apply list_forall2_imply with
392    (fun (ab: ident * A) (ac: ident * B) =>
393       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
394  eapply map_partial_forall2. eauto.
395  intros. destruct v1; destruct v2; simpl in *. auto.
396  split. auto.
397  apply list_forall2_imply with
398    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
399       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
400  eapply map_partial_forall2. eauto.
401  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
402Qed.
403*)
404(* * * External functions *)
405
406(* * For most languages, the functions composing the program are either
407  internal functions, defined within the language, or external functions
408  (a.k.a. system calls) that emit an event when applied.  We define
409  a type for such functions and some generic transformation functions. *)
410
411nrecord external_function : Type ≝ {
412  ef_id: ident;
413  ef_sig: signature
414}.
415
416ninductive fundef (F: Type): Type ≝
417  | Internal: F → fundef F
418  | External: external_function → fundef F.
419
420(* Implicit Arguments External [F]. *)
421(*
422Section TRANSF_FUNDEF.
423
424Variable A B: Type.
425Variable transf: A -> B.
426*)
427ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
428λA,B,transf,fd.
429  match fd with
430  [ Internal f ⇒ Internal ? (transf f)
431  | External ef ⇒ External ? ef
432  ].
433
434(*
435End TRANSF_FUNDEF.
436
437Section TRANSF_PARTIAL_FUNDEF.
438
439Variable A B: Type.
440Variable transf_partial: A -> res B.
441
442Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
443  match fd with
444  | Internal f => do f' <- transf_partial f; OK (Internal f')
445  | External ef => OK (External ef)
446  end.
447
448End TRANSF_PARTIAL_FUNDEF.
449*)
Note: See TracBrowser for help on using the repository browser.