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

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

Fix treatment of pointers in initialisation data, a little like later versions
of CompCert?. Remove obsolete Init_pointer.

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: region → ident → int → init_data.   (*r address of symbol + offset *)
150
151(* * Whole programs consist of:
152- a collection of function definitions (name and description);
153- the name of the ``main'' function that serves as entry point in the program;
154- a collection of global variable declarations, consisting of
155  a name, initialization data, and additional information.
156
157The type of function descriptions and that of additional information
158for variables vary among the various intermediate languages and are
159taken as parameters to the [program] type.  The other parts of whole
160programs are common to all languages. *)
161
162nrecord program (F,V: Type) : Type := {
163  prog_funct: list (ident × F);
164  prog_main: ident;
165  prog_vars: list (ident × (list init_data) × region × V)
166}.
167
168ndefinition prog_funct_names ≝ λF,V: Type. λp: program F V.
169  map ?? (fst ident F) (prog_funct ?? p).
170
171ndefinition prog_var_names ≝ λF,V: Type. λp: program F V.
172  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
173(*
174(** * Generic transformations over programs *)
175
176(** We now define a general iterator over programs that applies a given
177  code transformation function to all function descriptions and leaves
178  the other parts of the program unchanged. *)
179
180Section TRANSF_PROGRAM.
181
182Variable A B V: Type.
183Variable transf: A -> B.
184*)
185
186ndefinition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
187λA,B,transf,l.
188  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
189
190ndefinition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
191λA,B,V,transf,p.
192  mk_program B V
193    (transf_program ?? transf (prog_funct A V p))
194    (prog_main A V p)
195    (prog_vars A V p).
196
197nlemma transform_program_function:
198  ∀A,B,V,transf,p,i,tf.
199  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
200  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
201nnormalize; #A B V transf p i tf H; nelim (list_in_map_inv ????? H);
202#x; nelim x; #i' tf'; *; #e H; ndestruct; @tf'; /2/;
203nqed.
204
205(*
206End TRANSF_PROGRAM.
207
208(** The following is a variant of [transform_program] where the
209  code transformation function can fail and therefore returns an
210  option type. *)
211
212Open Local Scope error_monad_scope.
213Open Local Scope string_scope.
214
215Section MAP_PARTIAL.
216
217Variable A B C: Type.
218Variable prefix_errmsg: A -> errmsg.
219Variable f: B -> res C.
220
221Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
222  match l with
223  | nil => OK nil
224  | (a, b) :: rem =>
225      match f b with
226      | Error msg => Error (prefix_errmsg a ++ msg)%list
227      | OK c =>
228          do rem' <- map_partial rem;
229          OK ((a, c) :: rem')
230      end
231  end.
232
233Remark In_map_partial:
234  forall l l' a c,
235  map_partial l = OK l' ->
236  In (a, c) l' ->
237  exists b, In (a, b) l /\ f b = OK c.
238Proof.
239  induction l; simpl.
240  intros. inv H. elim H0.
241  intros until c. destruct a as [a1 b1].
242  caseEq (f b1); try congruence.
243  intro c1; intros. monadInv H0.
244  elim H1; intro. inv H0. exists b1; auto.
245  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
246Qed.
247
248Remark map_partial_forall2:
249  forall l l',
250  map_partial l = OK l' ->
251  list_forall2
252    (fun (a_b: A * B) (a_c: A * C) =>
253       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
254    l l'.
255Proof.
256  induction l; simpl.
257  intros. inv H. constructor.
258  intro l'. destruct a as [a b].
259  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
260  constructor. simpl. auto. auto.
261Qed.
262
263End MAP_PARTIAL.
264
265Remark map_partial_total:
266  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
267  map_partial prefix (fun b => OK (f b)) l =
268  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
269Proof.
270  induction l; simpl.
271  auto.
272  destruct a as [a1 b1]. rewrite IHl. reflexivity.
273Qed.
274
275Remark map_partial_identity:
276  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
277  map_partial prefix (fun b => OK b) l = OK l.
278Proof.
279  induction l; simpl.
280  auto.
281  destruct a as [a1 b1]. rewrite IHl. reflexivity.
282Qed.
283
284Section TRANSF_PARTIAL_PROGRAM.
285
286Variable A B V: Type.
287Variable transf_partial: A -> res B.
288
289Definition prefix_funct_name (id: ident) : errmsg :=
290  MSG "In function " :: CTX id :: MSG ": " :: nil.
291
292Definition transform_partial_program (p: program A V) : res (program B V) :=
293  do fl <- map_partial prefix_funct_name transf_partial p.(prog_funct);
294  OK (mkprogram fl p.(prog_main) p.(prog_vars)).
295
296Lemma transform_partial_program_function:
297  forall p tp i tf,
298  transform_partial_program p = OK tp ->
299  In (i, tf) tp.(prog_funct) ->
300  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
301Proof.
302  intros. monadInv H. simpl in H0. 
303  eapply In_map_partial; eauto.
304Qed.
305
306Lemma transform_partial_program_main:
307  forall p tp,
308  transform_partial_program p = OK tp ->
309  tp.(prog_main) = p.(prog_main).
310Proof.
311  intros. monadInv H. reflexivity.
312Qed.
313
314Lemma transform_partial_program_vars:
315  forall p tp,
316  transform_partial_program p = OK tp ->
317  tp.(prog_vars) = p.(prog_vars).
318Proof.
319  intros. monadInv H. reflexivity.
320Qed.
321
322End TRANSF_PARTIAL_PROGRAM.
323
324(** The following is a variant of [transform_program_partial] where
325  both the program functions and the additional variable information
326  are transformed by functions that can fail. *)
327
328Section TRANSF_PARTIAL_PROGRAM2.
329
330Variable A B V W: Type.
331Variable transf_partial_function: A -> res B.
332Variable transf_partial_variable: V -> res W.
333
334Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
335  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
336
337Definition transform_partial_program2 (p: program A V) : res (program B W) :=
338  do fl <- map_partial prefix_funct_name transf_partial_function p.(prog_funct);
339  do vl <- map_partial prefix_var_name transf_partial_variable p.(prog_vars);
340  OK (mkprogram fl p.(prog_main) vl).
341
342Lemma transform_partial_program2_function:
343  forall p tp i tf,
344  transform_partial_program2 p = OK tp ->
345  In (i, tf) tp.(prog_funct) ->
346  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
347Proof.
348  intros. monadInv H. 
349  eapply In_map_partial; eauto.
350Qed.
351
352Lemma transform_partial_program2_variable:
353  forall p tp i tv,
354  transform_partial_program2 p = OK tp ->
355  In (i, tv) tp.(prog_vars) ->
356  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
357Proof.
358  intros. monadInv H.
359  eapply In_map_partial; eauto.
360Qed.
361
362Lemma transform_partial_program2_main:
363  forall p tp,
364  transform_partial_program2 p = OK tp ->
365  tp.(prog_main) = p.(prog_main).
366Proof.
367  intros. monadInv H. reflexivity.
368Qed.
369
370End TRANSF_PARTIAL_PROGRAM2.
371
372(** The following is a relational presentation of
373  [transform_program_partial2].  Given relations between function
374  definitions and between variable information, it defines a relation
375  between programs stating that the two programs have the same shape
376  (same global names, etc) and that identically-named function definitions
377  are variable information are related. *)
378
379Section MATCH_PROGRAM.
380
381Variable A B V W: Type.
382Variable match_fundef: A -> B -> Prop.
383Variable match_varinfo: V -> W -> Prop.
384
385Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
386  match x1, x2 with
387  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
388  end.
389
390Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
391  match x1, x2 with
392  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
393  end.
394
395Definition match_program (p1: program A V) (p2: program B W) : Prop :=
396  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
397  /\ p1.(prog_main) = p2.(prog_main)
398  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
399
400End MATCH_PROGRAM.
401
402Remark transform_partial_program2_match:
403  forall (A B V W: Type)
404         (transf_partial_function: A -> res B)
405         (transf_partial_variable: V -> res W)
406         (p: program A V) (tp: program B W),
407  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
408  match_program
409    (fun fd tfd => transf_partial_function fd = OK tfd)
410    (fun info tinfo => transf_partial_variable info = OK tinfo)
411    p tp.
412Proof.
413  intros. monadInv H. split.
414  apply list_forall2_imply with
415    (fun (ab: ident * A) (ac: ident * B) =>
416       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
417  eapply map_partial_forall2. eauto.
418  intros. destruct v1; destruct v2; simpl in *. auto.
419  split. auto.
420  apply list_forall2_imply with
421    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
422       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
423  eapply map_partial_forall2. eauto.
424  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
425Qed.
426*)
427(* * * External functions *)
428
429(* * For most languages, the functions composing the program are either
430  internal functions, defined within the language, or external functions
431  (a.k.a. system calls) that emit an event when applied.  We define
432  a type for such functions and some generic transformation functions. *)
433
434nrecord external_function : Type ≝ {
435  ef_id: ident;
436  ef_sig: signature
437}.
438(*
439ninductive fundef (F: Type): Type ≝
440  | Internal: F → fundef F
441  | External: external_function → fundef F.
442
443(* Implicit Arguments External [F]. *)
444(*
445Section TRANSF_FUNDEF.
446
447Variable A B: Type.
448Variable transf: A -> B.
449*)
450ndefinition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
451λA,B,transf,fd.
452  match fd with
453  [ Internal f ⇒ Internal ? (transf f)
454  | External ef ⇒ External ? ef
455  ].
456*)
457(*
458End TRANSF_FUNDEF.
459
460Section TRANSF_PARTIAL_FUNDEF.
461
462Variable A B: Type.
463Variable transf_partial: A -> res B.
464
465Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
466  match fd with
467  | Internal f => do f' <- transf_partial f; OK (Internal f')
468  | External ef => OK (External ef)
469  end.
470
471End TRANSF_PARTIAL_FUNDEF.
472*)
Note: See TracBrowser for help on using the repository browser.