source: src/Clight/AST.ma @ 725

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

Add an AST type (i.e., intermediate language type) for pointers.

File size: 15.0 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 "basics/types.ma".
20include "utilities/extralib.ma".
21include "common/Integers.ma".
22include "common/Floats.ma".
23include "utilities/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
30definition ident ≝ Pos.
31
32definition ident_eq : ∀x,y:ident. (x=y) + (x≠y).
33#x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);
34[ #H %2 /2/; | #H %1 //; | #H %2 /2/ ] qed.
35
36(* Memory spaces *)
37
38inductive region : Type[0] ≝
39  | Any : region
40  | Data : region
41  | IData : region
42  | PData : region
43  | XData : region
44  | Code : region.
45
46definition eq_region : region → region → bool ≝
47λr1,r2.
48  match r1 with
49  [ Any ⇒   match r2 with [ Any ⇒ true | _ ⇒ false ]
50  | Data ⇒  match r2 with [ Data ⇒ true | _ ⇒ false ]
51  | IData ⇒ match r2 with [ IData ⇒ true | _ ⇒ false ]
52  | PData ⇒ match r2 with [ PData ⇒ true | _ ⇒ false ]
53  | XData ⇒ match r2 with [ XData ⇒ true | _ ⇒ false ]
54  | Code ⇒  match r2 with [ Code ⇒ true | _ ⇒ false ]
55  ].
56
57lemma eq_region_elim : ∀P:bool → Type[0]. ∀r1,r2.
58  (r1 = r2 → P true) → (r1 ≠ r2 → P false) →
59  P (eq_region r1 r2).
60#P #r1 #r2 cases r1; cases r2; #Ptrue #Pfalse
61try ( @Ptrue // )
62@Pfalse % #E destruct;
63qed.
64
65definition eq_region_dec : ∀r1,r2:region. (r1=r2)+(r1≠r2).
66#r1 #r2 @(eq_region_elim ? r1 r2) /2/; qed.
67
68definition size_pointer : region → Z ≝
69λsp. match sp return λ_.Z with [ Data ⇒ 1 | IData ⇒ 1 | PData ⇒ 1 | XData ⇒ 2 | Code ⇒ 2 | Any ⇒ 3 ].
70
71(* * The intermediate languages are weakly typed, using only three types:
72  [ASTint] for integers, [ASTptr] for pointers, and [ASTfloat] for floating-point
73  numbers. *)
74
75inductive typ : Type[0] ≝
76  | ASTint : typ
77  | ASTptr : region → typ
78  | ASTfloat : typ.
79
80(* FIXME: ASTint size is not 1 for Clight32 *)
81definition typesize : typ → Z ≝ λty.
82  match ty return λ_.Z with  [ ASTint ⇒ 1 | ASTptr r ⇒ size_pointer r | ASTfloat ⇒ 8 ].
83
84lemma typesize_pos: ∀ty. typesize ty > 0.
85#ty cases ty [ 2: * ] // qed.
86
87lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
88#t1 #t2 cases t1 try *; cases t2 try *; /2/ %2 @nmk #H destruct; qed.
89
90lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
91#t1 #t2 cases t1 cases t2
92[ %1 @refl
93| 2,3: #ty %2 % #H destruct
94| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct /2/
95]
96qed.
97
98(* * Additionally, function definitions and function calls are annotated
99  by function signatures indicating the number and types of arguments,
100  as well as the type of the returned value if any.  These signatures
101  are used in particular to determine appropriate calling conventions
102  for the function. *)
103
104record signature : Type[0] ≝ {
105  sig_args: list typ;
106  sig_res: option typ
107}.
108
109definition proj_sig_res : signature → typ ≝ λs.
110  match sig_res s with
111  [ None ⇒ ASTint
112  | Some t ⇒ t
113  ].
114
115(* * Memory accesses (load and store instructions) are annotated by
116  a ``memory chunk'' indicating the type, size and signedness of the
117  chunk of memory being accessed. *)
118
119inductive memory_chunk : Type[0] ≝
120  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
121  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
122  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
123  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
124  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
125  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
126  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
127  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
128
129(* * Initialization data for global variables. *)
130
131inductive init_data: Type[0] ≝
132  | Init_int8: int → init_data
133  | Init_int16: int → init_data
134  | Init_int32: int → init_data
135  | Init_float32: float → init_data
136  | Init_float64: float → init_data
137  | Init_space: Z → init_data
138  | Init_null: region → init_data
139  | Init_addrof: region → ident → int → init_data.   (*r address of symbol + offset *)
140
141(* * Whole programs consist of:
142- a collection of function definitions (name and description);
143- the name of the ``main'' function that serves as entry point in the program;
144- a collection of global variable declarations, consisting of
145  a name, initialization data, and additional information.
146
147The type of function descriptions and that of additional information
148for variables vary among the various intermediate languages and are
149taken as parameters to the [program] type.  The other parts of whole
150programs are common to all languages. *)
151
152record program (F,V: Type[0]) : Type[0] := {
153  prog_funct: list (ident × F);
154  prog_main: ident;
155  prog_vars: list (ident × (list init_data) × region × V)
156}.
157
158definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
159  map ?? (fst ident F) (prog_funct ?? p).
160
161definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
162  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
163(*
164(** * Generic transformations over programs *)
165
166(** We now define a general iterator over programs that applies a given
167  code transformation function to all function descriptions and leaves
168  the other parts of the program unchanged. *)
169
170Section TRANSF_PROGRAM.
171
172Variable A B V: Type.
173Variable transf: A -> B.
174*)
175
176definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
177λA,B,transf,l.
178  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
179
180definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
181λA,B,V,transf,p.
182  mk_program B V
183    (transf_program ?? transf (prog_funct A V p))
184    (prog_main A V p)
185    (prog_vars A V p).
186(*
187lemma transform_program_function:
188  ∀A,B,V,transf,p,i,tf.
189  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
190  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
191normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
192#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
193qed.
194*)
195(*
196End TRANSF_PROGRAM.
197
198(** The following is a variant of [transform_program] where the
199  code transformation function can fail and therefore returns an
200  option type. *)
201
202Open Local Scope error_monad_scope.
203Open Local Scope string_scope.
204
205Section MAP_PARTIAL.
206
207Variable A B C: Type.
208Variable prefix_errmsg: A -> errmsg.
209Variable f: B -> res C.
210
211Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
212  match l with
213  | nil => OK nil
214  | (a, b) :: rem =>
215      match f b with
216      | Error msg => Error (prefix_errmsg a ++ msg)%list
217      | OK c =>
218          do rem' <- map_partial rem;
219          OK ((a, c) :: rem')
220      end
221  end.
222
223Remark In_map_partial:
224  forall l l' a c,
225  map_partial l = OK l' ->
226  In (a, c) l' ->
227  exists b, In (a, b) l /\ f b = OK c.
228Proof.
229  induction l; simpl.
230  intros. inv H. elim H0.
231  intros until c. destruct a as [a1 b1].
232  caseEq (f b1); try congruence.
233  intro c1; intros. monadInv H0.
234  elim H1; intro. inv H0. exists b1; auto.
235  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
236Qed.
237
238Remark map_partial_forall2:
239  forall l l',
240  map_partial l = OK l' ->
241  list_forall2
242    (fun (a_b: A * B) (a_c: A * C) =>
243       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
244    l l'.
245Proof.
246  induction l; simpl.
247  intros. inv H. constructor.
248  intro l'. destruct a as [a b].
249  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
250  constructor. simpl. auto. auto.
251Qed.
252
253End MAP_PARTIAL.
254
255Remark map_partial_total:
256  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
257  map_partial prefix (fun b => OK (f b)) l =
258  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
259Proof.
260  induction l; simpl.
261  auto.
262  destruct a as [a1 b1]. rewrite IHl. reflexivity.
263Qed.
264
265Remark map_partial_identity:
266  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
267  map_partial prefix (fun b => OK b) l = OK l.
268Proof.
269  induction l; simpl.
270  auto.
271  destruct a as [a1 b1]. rewrite IHl. reflexivity.
272Qed.
273
274Section TRANSF_PARTIAL_PROGRAM.
275
276Variable A B V: Type.
277Variable transf_partial: A -> res B.
278
279Definition prefix_funct_name (id: ident) : errmsg :=
280  MSG "In function " :: CTX id :: MSG ": " :: nil.
281
282Definition transform_partial_program (p: program A V) : res (program B V) :=
283  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
284  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
285
286Lemma transform_partial_program_function:
287  forall p tp i tf,
288  transform_partial_program p = OK tp ->
289  In (i, tf) tp.(prog_funct) ->
290  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
291Proof.
292  intros. monadInv H. simpl in H0. 
293  eapply In_map_partial; eauto.
294Qed.
295
296Lemma transform_partial_program_main:
297  forall p tp,
298  transform_partial_program p = OK tp ->
299  tp.(prog_main) = p.(prog_main).
300Proof.
301  intros. monadInv H. reflexivity.
302Qed.
303
304Lemma transform_partial_program_vars:
305  forall p tp,
306  transform_partial_program p = OK tp ->
307  tp.(prog_vars) = p.(prog_vars).
308Proof.
309  intros. monadInv H. reflexivity.
310Qed.
311
312End TRANSF_PARTIAL_PROGRAM.
313
314(** The following is a variant of [transform_program_partial] where
315  both the program functions and the additional variable information
316  are transformed by functions that can fail. *)
317
318Section TRANSF_PARTIAL_PROGRAM2.
319
320Variable A B V W: Type.
321Variable transf_partial_function: A -> res B.
322Variable transf_partial_variable: V -> res W.
323
324Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
325  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
326
327Definition transform_partial_program2 (p: program A V) : res (program B W) :=
328  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
329  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
330  OK (mkprogram fl p.(prog_main) vl).
331
332Lemma transform_partial_program2_function:
333  forall p tp i tf,
334  transform_partial_program2 p = OK tp ->
335  In (i, tf) tp.(prog_funct) ->
336  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
337Proof.
338  intros. monadInv H. 
339  eapply In_map_partial; eauto.
340Qed.
341
342Lemma transform_partial_program2_variable:
343  forall p tp i tv,
344  transform_partial_program2 p = OK tp ->
345  In (i, tv) tp.(prog_vars) ->
346  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
347Proof.
348  intros. monadInv H.
349  eapply In_map_partial; eauto.
350Qed.
351
352Lemma transform_partial_program2_main:
353  forall p tp,
354  transform_partial_program2 p = OK tp ->
355  tp.(prog_main) = p.(prog_main).
356Proof.
357  intros. monadInv H. reflexivity.
358Qed.
359
360End TRANSF_PARTIAL_PROGRAM2.
361
362(** The following is a relational presentation of
363  [transform_program_partial2].  Given relations between function
364  definitions and between variable information, it defines a relation
365  between programs stating that the two programs have the same shape
366  (same global names, etc) and that identically-named function definitions
367  are variable information are related. *)
368
369Section MATCH_PROGRAM.
370
371Variable A B V W: Type.
372Variable match_fundef: A -> B -> Prop.
373Variable match_varinfo: V -> W -> Prop.
374
375Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
376  match x1, x2 with
377  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
378  end.
379
380Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
381  match x1, x2 with
382  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
383  end.
384
385Definition match_program (p1: program A V) (p2: program B W) : Prop :=
386  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
387  /\ p1.(prog_main) = p2.(prog_main)
388  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
389
390End MATCH_PROGRAM.
391
392Remark transform_partial_program2_match:
393  forall (A B V W: Type)
394         (transf_partial_function: A -> res B)
395         (transf_partial_variable: V -> res W)
396         (p: program A V) (tp: program B W),
397  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
398  match_program
399    (fun fd tfd => transf_partial_function fd = OK tfd)
400    (fun info tinfo => transf_partial_variable info = OK tinfo)
401    p tp.
402Proof.
403  intros. monadInv H. split.
404  apply list_forall2_imply with
405    (fun (ab: ident * A) (ac: ident * B) =>
406       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
407  eapply map_partial_forall2. eauto.
408  intros. destruct v1; destruct v2; simpl in *. auto.
409  split. auto.
410  apply list_forall2_imply with
411    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
412       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
413  eapply map_partial_forall2. eauto.
414  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
415Qed.
416*)
417(* * * External functions *)
418
419(* * For most languages, the functions composing the program are either
420  internal functions, defined within the language, or external functions
421  (a.k.a. system calls) that emit an event when applied.  We define
422  a type for such functions and some generic transformation functions. *)
423
424record external_function : Type[0] ≝ {
425  ef_id: ident;
426  ef_sig: signature
427}.
428
429inductive fundef (F: Type[0]): Type[0] ≝
430  | Internal: F → fundef F
431  | External: external_function → fundef F.
432(*
433(* Implicit Arguments External [F]. *)
434(*
435Section TRANSF_FUNDEF.
436
437Variable A B: Type.
438Variable transf: A -> B.
439*)
440definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
441λA,B,transf,fd.
442  match fd with
443  [ Internal f ⇒ Internal ? (transf f)
444  | External ef ⇒ External ? ef
445  ].
446*)
447(*
448End TRANSF_FUNDEF.
449
450Section TRANSF_PARTIAL_FUNDEF.
451
452Variable A B: Type.
453Variable transf_partial: A -> res B.
454
455Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
456  match fd with
457  | Internal f => do f' <- transf_partial f; OK (Internal f')
458  | External ef => OK (External ef)
459  end.
460
461End TRANSF_PARTIAL_FUNDEF.
462*)
Note: See TracBrowser for help on using the repository browser.