source: C-semantics/AST.ma @ 125

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

Unify memory space / pointer types.
Implement global variable initialisation and lookup.
Global variables get memory spaces, local variables could be anywhere (for now).

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