source: C-semantics/AST.ma @ 211

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

pdata support

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