source: Deliverables/D3.1/C-semantics/AST.ma @ 483

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

Use pointer-specific "chunks" of memory for pointer loads and stores,
in particular getting rid of Mint24.

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