source: src/Clight/AST.ma @ 744

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

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

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