source: src/Clight/AST.ma @ 726

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

Change identifiers to Words in Clight and RTLabs semantics.

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