source: src/common/AST.ma @ 789

Last change on this file since 789 was 764, checked in by campbell, 9 years ago

Start Cminor to RTLabs phase.

Includes some syntax for matching triples for convenience.

File size: 17.2 KB
RevLine 
[747]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(* *********************************************************************)
[491]15
[747]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".
[698]22include "ASM/BitVector.ma".
[747]23include "common/Identifiers.ma".
[491]24
[747]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. *)
[722]41definition Identifier ≝ Word.
[491]42
[747]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
[764]187(* * * Generic transformations over programs *)
188
189(* * We now define a general iterator over programs that applies a given
[747]190  code transformation function to all function descriptions and leaves
191  the other parts of the program unchanged. *)
[764]192(*
[747]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.
[764]233*)
234definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
235                         list (A × B) → res (list (A × C)) ≝
236λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
237(*
[747]238Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
239  match l with
240  | nil => OK nil
241  | (a, b) :: rem =>
242      match f b with
243      | Error msg => Error (prefix_errmsg a ++ msg)%list
244      | OK c =>
245          do rem' <- map_partial rem;
246          OK ((a, c) :: rem')
247      end
248  end.
249
250Remark In_map_partial:
251  forall l l' a c,
252  map_partial l = OK l' ->
253  In (a, c) l' ->
254  exists b, In (a, b) l /\ f b = OK c.
255Proof.
256  induction l; simpl.
257  intros. inv H. elim H0.
258  intros until c. destruct a as [a1 b1].
259  caseEq (f b1); try congruence.
260  intro c1; intros. monadInv H0.
261  elim H1; intro. inv H0. exists b1; auto.
262  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
263Qed.
264
265Remark map_partial_forall2:
266  forall l l',
267  map_partial l = OK l' ->
268  list_forall2
269    (fun (a_b: A * B) (a_c: A * C) =>
270       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
271    l l'.
272Proof.
273  induction l; simpl.
274  intros. inv H. constructor.
275  intro l'. destruct a as [a b].
276  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
277  constructor. simpl. auto. auto.
278Qed.
279
280End MAP_PARTIAL.
281
282Remark map_partial_total:
283  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
284  map_partial prefix (fun b => OK (f b)) l =
285  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
286Proof.
287  induction l; simpl.
288  auto.
289  destruct a as [a1 b1]. rewrite IHl. reflexivity.
290Qed.
291
292Remark map_partial_identity:
293  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
294  map_partial prefix (fun b => OK b) l = OK l.
295Proof.
296  induction l; simpl.
297  auto.
298  destruct a as [a1 b1]. rewrite IHl. reflexivity.
299Qed.
300
301Section TRANSF_PARTIAL_PROGRAM.
302
303Variable A B V: Type.
304Variable transf_partial: A -> res B.
305
306Definition prefix_funct_name (id: ident) : errmsg :=
307  MSG "In function " :: CTX id :: MSG ": " :: nil.
[764]308*)
309definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
310λA,B,V,transf_partial,p.
311  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
312  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
313(*
[747]314Lemma transform_partial_program_function:
315  forall p tp i tf,
316  transform_partial_program p = OK tp ->
317  In (i, tf) tp.(prog_funct) ->
318  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
319Proof.
320  intros. monadInv H. simpl in H0. 
321  eapply In_map_partial; eauto.
322Qed.
323
324Lemma transform_partial_program_main:
325  forall p tp,
326  transform_partial_program p = OK tp ->
327  tp.(prog_main) = p.(prog_main).
328Proof.
329  intros. monadInv H. reflexivity.
330Qed.
331
332Lemma transform_partial_program_vars:
333  forall p tp,
334  transform_partial_program p = OK tp ->
335  tp.(prog_vars) = p.(prog_vars).
336Proof.
337  intros. monadInv H. reflexivity.
338Qed.
339
340End TRANSF_PARTIAL_PROGRAM.
341
342(** The following is a variant of [transform_program_partial] where
343  both the program functions and the additional variable information
344  are transformed by functions that can fail. *)
345
346Section TRANSF_PARTIAL_PROGRAM2.
347
348Variable A B V W: Type.
349Variable transf_partial_function: A -> res B.
350Variable transf_partial_variable: V -> res W.
351
352Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
353  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
[764]354*)
355definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
356                                        program A V → res (program B W) ≝
357λA,B,V,W, transf_partial_function, transf_partial_variable, p.
358  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
359  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
360  OK ? (mk_program … fl (prog_main ?? p) vl).
361(*
[747]362Lemma transform_partial_program2_function:
363  forall p tp i tf,
364  transform_partial_program2 p = OK tp ->
365  In (i, tf) tp.(prog_funct) ->
366  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
367Proof.
368  intros. monadInv H. 
369  eapply In_map_partial; eauto.
370Qed.
371
372Lemma transform_partial_program2_variable:
373  forall p tp i tv,
374  transform_partial_program2 p = OK tp ->
375  In (i, tv) tp.(prog_vars) ->
376  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
377Proof.
378  intros. monadInv H.
379  eapply In_map_partial; eauto.
380Qed.
381
382Lemma transform_partial_program2_main:
383  forall p tp,
384  transform_partial_program2 p = OK tp ->
385  tp.(prog_main) = p.(prog_main).
386Proof.
387  intros. monadInv H. reflexivity.
388Qed.
389
390End TRANSF_PARTIAL_PROGRAM2.
391
392(** The following is a relational presentation of
393  [transform_program_partial2].  Given relations between function
394  definitions and between variable information, it defines a relation
395  between programs stating that the two programs have the same shape
396  (same global names, etc) and that identically-named function definitions
397  are variable information are related. *)
398
399Section MATCH_PROGRAM.
400
401Variable A B V W: Type.
402Variable match_fundef: A -> B -> Prop.
403Variable match_varinfo: V -> W -> Prop.
404
405Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
406  match x1, x2 with
407  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
408  end.
409
410Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
411  match x1, x2 with
412  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
413  end.
414
415Definition match_program (p1: program A V) (p2: program B W) : Prop :=
416  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
417  /\ p1.(prog_main) = p2.(prog_main)
418  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
419
420End MATCH_PROGRAM.
421
422Remark transform_partial_program2_match:
423  forall (A B V W: Type)
424         (transf_partial_function: A -> res B)
425         (transf_partial_variable: V -> res W)
426         (p: program A V) (tp: program B W),
427  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
428  match_program
429    (fun fd tfd => transf_partial_function fd = OK tfd)
430    (fun info tinfo => transf_partial_variable info = OK tinfo)
431    p tp.
432Proof.
433  intros. monadInv H. split.
434  apply list_forall2_imply with
435    (fun (ab: ident * A) (ac: ident * B) =>
436       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
437  eapply map_partial_forall2. eauto.
438  intros. destruct v1; destruct v2; simpl in *. auto.
439  split. auto.
440  apply list_forall2_imply with
441    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
442       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
443  eapply map_partial_forall2. eauto.
444  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
445Qed.
446*)
447(* * * External functions *)
448
449(* * For most languages, the functions composing the program are either
450  internal functions, defined within the language, or external functions
451  (a.k.a. system calls) that emit an event when applied.  We define
452  a type for such functions and some generic transformation functions. *)
453
454record external_function : Type[0] ≝ {
455  ef_id: ident;
456  ef_sig: signature
457}.
458
459definition ExternalFunction ≝ external_function.
460definition external_function_tag ≝ ef_id.
461definition external_function_sig ≝ ef_sig.
462
463inductive fundef (F: Type[0]): Type[0] ≝
464  | Internal: F → fundef F
465  | External: external_function → fundef F.
[764]466
[747]467(* Implicit Arguments External [F]. *)
468(*
469Section TRANSF_FUNDEF.
470
471Variable A B: Type.
472Variable transf: A -> B.
473*)
474definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
475λA,B,transf,fd.
476  match fd with
477  [ Internal f ⇒ Internal ? (transf f)
478  | External ef ⇒ External ? ef
479  ].
[764]480
[747]481(*
482End TRANSF_FUNDEF.
483
484Section TRANSF_PARTIAL_FUNDEF.
485
486Variable A B: Type.
487Variable transf_partial: A -> res B.
[764]488*)
[747]489
[764]490definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
491λA,B,transf_partial,fd.
[747]492  match fd with
[764]493  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
494  | External ef ⇒ OK ? (External ? ef)
495  ].
496(*
[747]497End TRANSF_PARTIAL_FUNDEF.
498*)
499
500
501
502(* Partially merged stuff derived from the prototype cerco compiler. *)
503
[714]504definition bool_to_Prop ≝
505 λb. match b with [ true ⇒ True | false ⇒ False ].
506
507(* dpm: should go to standard library *)
[757]508let rec member (i: ident) (eq_i: ident → ident → bool)
509               (g: list ident) on g: Prop ≝
[714]510  match g with
511  [ nil ⇒ False
512  | cons hd tl ⇒
513      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
514  ].
515
[747]516(* TODO: merge in comparison definitions from Integers.ma. *)
[491]517inductive Compare: Type[0] ≝
518  Compare_Equal: Compare
519| Compare_Less: Compare
520| Compare_Greater: Compare
521| Compare_LessEqual: Compare
522| Compare_GreaterEqual: Compare.
523
[747]524(* XXX unused definitions
[491]525inductive Cast: Type[0] ≝
526  Cast_Int: Byte → Cast
527| Cast_AddrSymbol: Identifier → Cast
528| Cast_StackOffset: Immediate → Cast.
529
530inductive Data: Type[0] ≝
531  Data_Reserve: nat → Data
532| Data_Int8: Byte → Data
533| Data_Int16: Word → Data.
534
535inductive DataSize: Type[0] ≝
536  DataSize_Byte: DataSize
537| DataSize_HalfWord: DataSize
538| DataSize_Word: DataSize.
539*)
540
[714]541definition Trace ≝ list Identifier.
Note: See TracBrowser for help on using the repository browser.