source: src/common/AST.ma @ 849

Last change on this file since 849 was 849, checked in by sacerdot, 9 years ago

...

File size: 19.7 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
181(*
182definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
183  map ?? (fst ident F) (prog_funct ?? p).
184
185definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
186  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
187
188(* * * Generic transformations over programs *)
189
190(* * We now define a general iterator over programs that applies a given
191  code transformation function to all function descriptions and leaves
192  the other parts of the program unchanged. *)
193(*
194Section TRANSF_PROGRAM.
195
196Variable A B V: Type.
197Variable transf: A -> B.
198*)
199
200definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
201λA,B,transf,l.
202  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
203
204definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
205λA,B,V,transf,p.
206  mk_program B V
207    (transf_program ?? transf (prog_funct A V p))
208    (prog_main A V p)
209    (prog_vars A V p).
210(*
211lemma transform_program_function:
212  ∀A,B,V,transf,p,i,tf.
213  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
214  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
215normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
216#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
217qed.
218*)
219(*
220End TRANSF_PROGRAM.
221
222(** The following is a variant of [transform_program] where the
223  code transformation function can fail and therefore returns an
224  option type. *)
225
226Open Local Scope error_monad_scope.
227Open Local Scope string_scope.
228
229Section MAP_PARTIAL.
230
231Variable A B C: Type.
232Variable prefix_errmsg: A -> errmsg.
233Variable f: B -> res C.
234*)
235definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
236                         list (A × B) → res (list (A × C)) ≝
237λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
238(*
239Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
240  match l with
241  | nil => OK nil
242  | (a, b) :: rem =>
243      match f b with
244      | Error msg => Error (prefix_errmsg a ++ msg)%list
245      | OK c =>
246          do rem' <- map_partial rem;
247          OK ((a, c) :: rem')
248      end
249  end.
250
251Remark In_map_partial:
252  forall l l' a c,
253  map_partial l = OK l' ->
254  In (a, c) l' ->
255  exists b, In (a, b) l /\ f b = OK c.
256Proof.
257  induction l; simpl.
258  intros. inv H. elim H0.
259  intros until c. destruct a as [a1 b1].
260  caseEq (f b1); try congruence.
261  intro c1; intros. monadInv H0.
262  elim H1; intro. inv H0. exists b1; auto.
263  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
264Qed.
265
266Remark map_partial_forall2:
267  forall l l',
268  map_partial l = OK l' ->
269  list_forall2
270    (fun (a_b: A * B) (a_c: A * C) =>
271       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
272    l l'.
273Proof.
274  induction l; simpl.
275  intros. inv H. constructor.
276  intro l'. destruct a as [a b].
277  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
278  constructor. simpl. auto. auto.
279Qed.
280
281End MAP_PARTIAL.
282
283Remark map_partial_total:
284  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
285  map_partial prefix (fun b => OK (f b)) l =
286  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
287Proof.
288  induction l; simpl.
289  auto.
290  destruct a as [a1 b1]. rewrite IHl. reflexivity.
291Qed.
292
293Remark map_partial_identity:
294  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
295  map_partial prefix (fun b => OK b) l = OK l.
296Proof.
297  induction l; simpl.
298  auto.
299  destruct a as [a1 b1]. rewrite IHl. reflexivity.
300Qed.
301
302Section TRANSF_PARTIAL_PROGRAM.
303
304Variable A B V: Type.
305Variable transf_partial: A -> res B.
306
307Definition prefix_funct_name (id: ident) : errmsg :=
308  MSG "In function " :: CTX id :: MSG ": " :: nil.
309*)
310definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
311λA,B,V,transf_partial,p.
312  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
313  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
314(*
315Lemma transform_partial_program_function:
316  forall p tp i tf,
317  transform_partial_program p = OK tp ->
318  In (i, tf) tp.(prog_funct) ->
319  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
320Proof.
321  intros. monadInv H. simpl in H0. 
322  eapply In_map_partial; eauto.
323Qed.
324
325Lemma transform_partial_program_main:
326  forall p tp,
327  transform_partial_program p = OK tp ->
328  tp.(prog_main) = p.(prog_main).
329Proof.
330  intros. monadInv H. reflexivity.
331Qed.
332
333Lemma transform_partial_program_vars:
334  forall p tp,
335  transform_partial_program p = OK tp ->
336  tp.(prog_vars) = p.(prog_vars).
337Proof.
338  intros. monadInv H. reflexivity.
339Qed.
340
341End TRANSF_PARTIAL_PROGRAM.
342
343(** The following is a variant of [transform_program_partial] where
344  both the program functions and the additional variable information
345  are transformed by functions that can fail. *)
346
347Section TRANSF_PARTIAL_PROGRAM2.
348
349Variable A B V W: Type.
350Variable transf_partial_function: A -> res B.
351Variable transf_partial_variable: V -> res W.
352
353Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
354  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
355*)
356definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
357                                        program A V → res (program B W) ≝
358λA,B,V,W, transf_partial_function, transf_partial_variable, p.
359  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
360  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
361  OK ? (mk_program … fl (prog_main ?? p) vl).
362(*
363Lemma transform_partial_program2_function:
364  forall p tp i tf,
365  transform_partial_program2 p = OK tp ->
366  In (i, tf) tp.(prog_funct) ->
367  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
368Proof.
369  intros. monadInv H. 
370  eapply In_map_partial; eauto.
371Qed.
372
373Lemma transform_partial_program2_variable:
374  forall p tp i tv,
375  transform_partial_program2 p = OK tp ->
376  In (i, tv) tp.(prog_vars) ->
377  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
378Proof.
379  intros. monadInv H.
380  eapply In_map_partial; eauto.
381Qed.
382
383Lemma transform_partial_program2_main:
384  forall p tp,
385  transform_partial_program2 p = OK tp ->
386  tp.(prog_main) = p.(prog_main).
387Proof.
388  intros. monadInv H. reflexivity.
389Qed.
390
391End TRANSF_PARTIAL_PROGRAM2.
392
393(** The following is a relational presentation of
394  [transform_program_partial2].  Given relations between function
395  definitions and between variable information, it defines a relation
396  between programs stating that the two programs have the same shape
397  (same global names, etc) and that identically-named function definitions
398  are variable information are related. *)
399
400Section MATCH_PROGRAM.
401
402Variable A B V W: Type.
403Variable match_fundef: A -> B -> Prop.
404Variable match_varinfo: V -> W -> Prop.
405
406Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
407  match x1, x2 with
408  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
409  end.
410
411Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
412  match x1, x2 with
413  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
414  end.
415
416Definition match_program (p1: program A V) (p2: program B W) : Prop :=
417  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
418  /\ p1.(prog_main) = p2.(prog_main)
419  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
420
421End MATCH_PROGRAM.
422
423Remark transform_partial_program2_match:
424  forall (A B V W: Type)
425         (transf_partial_function: A -> res B)
426         (transf_partial_variable: V -> res W)
427         (p: program A V) (tp: program B W),
428  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
429  match_program
430    (fun fd tfd => transf_partial_function fd = OK tfd)
431    (fun info tinfo => transf_partial_variable info = OK tinfo)
432    p tp.
433Proof.
434  intros. monadInv H. split.
435  apply list_forall2_imply with
436    (fun (ab: ident * A) (ac: ident * B) =>
437       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
438  eapply map_partial_forall2. eauto.
439  intros. destruct v1; destruct v2; simpl in *. auto.
440  split. auto.
441  apply list_forall2_imply with
442    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
443       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
444  eapply map_partial_forall2. eauto.
445  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
446Qed.
447*)
448(* * * External functions *)
449
450(* * For most languages, the functions composing the program are either
451  internal functions, defined within the language, or external functions
452  (a.k.a. system calls) that emit an event when applied.  We define
453  a type for such functions and some generic transformation functions. *)
454
455record external_function : Type[0] ≝ {
456  ef_id: ident;
457  ef_sig: signature
458}.
459
460definition ExternalFunction ≝ external_function.
461definition external_function_tag ≝ ef_id.
462definition external_function_sig ≝ ef_sig.
463
464inductive fundef (F: Type[0]): Type[0] ≝
465  | Internal: F → fundef F
466  | External: external_function → fundef F.
467
468(* Implicit Arguments External [F]. *)
469(*
470Section TRANSF_FUNDEF.
471
472Variable A B: Type.
473Variable transf: A -> B.
474*)
475definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
476λA,B,transf,fd.
477  match fd with
478  [ Internal f ⇒ Internal ? (transf f)
479  | External ef ⇒ External ? ef
480  ].
481
482(*
483End TRANSF_FUNDEF.
484
485Section TRANSF_PARTIAL_FUNDEF.
486
487Variable A B: Type.
488Variable transf_partial: A -> res B.
489*)
490
491definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
492λA,B,transf_partial,fd.
493  match fd with
494  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
495  | External ef ⇒ OK ? (External ? ef)
496  ].
497(*
498End TRANSF_PARTIAL_FUNDEF.
499*)
500*)
501
502
503
504(* Partially merged stuff derived from the prototype cerco compiler. *)
505
506definition bool_to_Prop ≝
507 λb. match b with [ true ⇒ True | false ⇒ False ].
508
509(* dpm: should go to standard library *)
510let rec member (i: ident) (eq_i: ident → ident → bool)
511               (g: list ident) on g: Prop ≝
512  match g with
513  [ nil ⇒ False
514  | cons hd tl ⇒
515      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
516  ].
517
518(* TODO: merge in comparison definitions from Integers.ma. *)
519inductive Compare: Type[0] ≝
520  Compare_Equal: Compare
521| Compare_NotEqual: Compare
522| Compare_Less: Compare
523| Compare_Greater: Compare
524| Compare_LessEqual: Compare
525| Compare_GreaterEqual: Compare.
526
527(* XXX unused definitions
528inductive Cast: Type[0] ≝
529  Cast_Int: Byte → Cast
530| Cast_AddrSymbol: Identifier → Cast
531| Cast_StackOffset: Immediate → Cast.
532
533inductive Data: Type[0] ≝
534  Data_Reserve: nat → Data
535| Data_Int8: Byte → Data
536| Data_Int16: Word → Data.
537
538inductive DataSize: Type[0] ≝
539  DataSize_Byte: DataSize
540| DataSize_HalfWord: DataSize
541| DataSize_Word: DataSize.
542*)
543
544definition Trace ≝ list Identifier.
545
546(* dpm: how are floats represented? *)
547inductive cast: Type[0] ≝
548  | cast_int: Byte → cast                    (* integer constant *)
549  | cast_float: Byte → cast                  (* float constant *)
550  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
551  | cast_stack_offset: Byte → cast.
552
553inductive op1: Type[0] ≝
554  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
555  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
556  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
557  | op_cast16_signed: op1    (**r 16-bit sign extension *)
558  | op_neg_int: op1          (**r integer opposite *)
559  | op_not_bool: op1         (**r boolean negation  *)
560  | op_not_int: op1          (**r bitwise complement  *)
561  | op_negf: op1             (**r float opposite *)
562  | op_absf: op1             (**r float absolute value *)
563  | op_single_of_float: op1  (**r float truncation *)
564  | op_int_of_float: op1     (**r signed integer to float *)
565  | op_intu_of_float: op1    (**r unsigned integer to float *)
566  | op_float_of_int: op1     (**r float to signed integer *)
567  | op_float_of_intu: op1    (**r float to unsigned integer *)
568  | op_id: op1               (**r identity *)
569  | op_ptr_of_int: op1       (**r int to pointer *)
570  | op_int_of_ptr: op1.      (**r pointer to int *)
571
572inductive op2: Type[0] ≝
573  | op_add: op2         (**r integer addition *)
574  | op_sub: op2         (**r integer subtraction *)
575  | op_mul: op2         (**r integer multiplication *)
576  | op_div: op2         (**r integer signed division *)
577  | op_divu: op2        (**r integer unsigned division *)
578  | op_mod: op2         (**r integer signed modulus *)
579  | op_modu: op2        (**r integer unsigned modulus *)
580  | op_and: op2         (**r bitwise ``and'' *)
581  | op_or: op2          (**r bitwise ``or'' *)
582  | op_xor: op2         (**r bitwise ``xor'' *)
583  | op_shl: op2         (**r left shift *)
584  | op_shr: op2         (**r right signed shift *)
585  | op_shru: op2        (**r right unsigned shift *)
586  | op_addf: op2        (**r float addition *)
587  | op_subf: op2        (**r float subtraction *)
588  | op_mulf: op2        (**r float multiplication *)
589  | op_divf: op2        (**r float division *)
590  | op_cmp: Compare → op2   (**r integer signed comparison *)
591  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
592  | op_cmpf: Compare → op2  (**r float comparison *)
593  | op_addp: op2        (**r addition for a pointer and an integer *)
594  | op_subp: op2        (**r substraction for a pointer and a integer *)
595  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracBrowser for help on using the repository browser.