source: Deliverables/D3.1/C-semantics/AST.ma @ 467

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

Update some of the commented-out parts of Globalenvs for testing.

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