source: src/common/AST.ma @ 753

Last change on this file since 753 was 747, checked in by campbell, 9 years ago

Merge the two AST files together (although some definitions still need to be
harmonised).

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