source: src/common/AST.ma @ 961

Last change on this file since 961 was 961, checked in by campbell, 8 years ago

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 23.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 "common/Integers.ma".
21include "common/Floats.ma".
22include "ASM/Arithmetic.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(* We maintain some reasonable type information through the front end of the
81   compiler. *)
82
83inductive signedness : Type[0] ≝
84  | Signed: signedness
85  | Unsigned: signedness.
86
87inductive intsize : Type[0] ≝
88  | I8: intsize
89  | I16: intsize
90  | I32: intsize.
91
92(* * Float types come in two sizes: 32 bits (single precision)
93  and 64-bit (double precision). *)
94
95inductive floatsize : Type[0] ≝
96  | F32: floatsize
97  | F64: floatsize.
98
99inductive typ : Type[0] ≝
100  | ASTint : intsize → signedness → typ
101  | ASTptr : region → typ
102  | ASTfloat : floatsize → typ.
103
104(* XXX aliases *)
105definition SigType ≝ typ.
106definition SigType_Int ≝ ASTint I32 Unsigned.
107(*
108| SigType_Float: SigType
109*)
110definition SigType_Ptr ≝ ASTptr Any.
111
112(* Define these carefully so that we always know that the result is nonzero,
113   and can be used in dependent types of the form (S n).
114   (At the time of writing this is only used for bitsize_of_intsize.) *)
115
116definition size_intsize : intsize → nat ≝
117λsz. S match sz with [ I8 ⇒ 0 | I16 ⇒ 1 | I32 ⇒ 3].
118
119definition bitsize_of_intsize : intsize → nat ≝
120λsz. S match sz with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31].
121
122definition eq_intsize : intsize → intsize → bool ≝
123λsz1,sz2.
124  match sz1 with
125  [ I8  ⇒ match sz2 with [ I8  ⇒ true | _ ⇒ false ]
126  | I16 ⇒ match sz2 with [ I16 ⇒ true | _ ⇒ false ]
127  | I32 ⇒ match sz2 with [ I32 ⇒ true | _ ⇒ false ]
128  ].
129
130lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0].
131  (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2).
132* * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct
133qed.
134
135lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true.
136* @refl
137qed.
138
139lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false.
140* * * #NE try @refl @False_ind @NE @refl
141qed.
142
143(* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and
144   if it is returns [e1] where the type of [n] has its dependency on [sz1]
145   changed to [sz2], and if not returns [e2]. *)
146let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 :
147  P sz1 → (P sz2 → A) → A → A ≝
148match sz1 return λsz. P sz → (P sz2 → A) → A → A with
149[ I8  ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8  ⇒ λf,d. f x | _ ⇒ λf,d. d ]
150| I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
151| I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x | _ ⇒ λf,d. d ]
152].
153
154lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d.
155  intsize_eq_elim A sz sz P p f d = f p.
156#A * //
157qed.
158
159lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0].
160  (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d).
161#A * * #P #p #f #d #Q #Hne #Heq
162[ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??))
163| *: whd in ⊢ (?%) @Hne % #E destruct
164] qed.
165
166
167(* A type for the integers that appear in the semantics. *)
168definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz).
169
170definition repr : ∀sz:intsize. nat → bvint sz ≝
171λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x.
172
173
174definition size_floatsize : floatsize → nat ≝
175λsz. S match sz with [ F32 ⇒ 3 | F64 ⇒ 7 ].
176
177definition typesize : typ → nat ≝ λty.
178  match ty with
179  [ ASTint sz _ ⇒ size_intsize sz
180  | ASTptr r ⇒ size_pointer r
181  | ASTfloat sz ⇒ size_floatsize sz ].
182
183lemma typesize_pos: ∀ty. typesize ty > 0.
184* *; try * /2/ qed.
185
186lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
187* * * *; try *; try *; try (%1 @refl) %2 @nmk #H destruct qed.
188
189lemma opt_typ_eq: ∀t1,t2: option typ. (t1=t2) + (t1≠t2).
190#t1 #t2 cases t1 cases t2
191[ %1 @refl
192| 2,3: #ty %2 % #H destruct
193| #ty1 #ty2 elim (typ_eq ty1 ty2) #E [ %1 >E @refl | %2 % #E' destruct cases E /2/
194]
195qed.
196
197(* * Additionally, function definitions and function calls are annotated
198  by function signatures indicating the number and types of arguments,
199  as well as the type of the returned value if any.  These signatures
200  are used in particular to determine appropriate calling conventions
201  for the function. *)
202
203record signature : Type[0] ≝ {
204  sig_args: list typ;
205  sig_res: option typ
206}.
207
208(* XXX aliases *)
209definition Signature ≝ signature.
210definition signature_args ≝ sig_args.
211definition signature_return ≝ sig_res.
212
213definition proj_sig_res : signature → typ ≝ λs.
214  match sig_res s with
215  [ None ⇒ ASTint I32 Unsigned
216  | Some t ⇒ t
217  ].
218
219(* * Memory accesses (load and store instructions) are annotated by
220  a ``memory chunk'' indicating the type, size and signedness of the
221  chunk of memory being accessed. *)
222
223inductive memory_chunk : Type[0] ≝
224  | Mint8signed : memory_chunk     (*r 8-bit signed integer *)
225  | Mint8unsigned : memory_chunk   (*r 8-bit unsigned integer *)
226  | Mint16signed : memory_chunk    (*r 16-bit signed integer *)
227  | Mint16unsigned : memory_chunk  (*r 16-bit unsigned integer *)
228  | Mint32 : memory_chunk          (*r 32-bit integer, or pointer *)
229  | Mfloat32 : memory_chunk        (*r 32-bit single-precision float *)
230  | Mfloat64 : memory_chunk        (*r 64-bit double-precision float *)
231  | Mpointer : region → memory_chunk. (* pointer addressing given region *)
232
233definition typ_of_memory_chunk : memory_chunk → typ ≝
234λc. match c with
235[ Mint8signed ⇒ ASTint I8 Signed
236| Mint8unsigned ⇒ ASTint I8 Unsigned
237| Mint16signed ⇒ ASTint I16 Signed
238| Mint16unsigned ⇒ ASTint I16 Unsigned
239| Mint32 ⇒ ASTint I32 Unsigned (* XXX signed? *)
240| Mfloat32 ⇒ ASTfloat F32
241| Mfloat64 ⇒ ASTfloat F64
242| Mpointer r ⇒ ASTptr r
243].
244
245(* * Initialization data for global variables. *)
246
247inductive init_data: Type[0] ≝
248  | Init_int8: bvint I8 → init_data
249  | Init_int16: bvint I16 → init_data
250  | Init_int32: bvint I32 → init_data
251  | Init_float32: float → init_data
252  | Init_float64: float → init_data
253  | Init_space: nat → init_data
254  | Init_null: region → init_data
255  | Init_addrof: region → ident → nat → init_data.   (*r address of symbol + offset *)
256
257(* * Whole programs consist of:
258- a collection of function definitions (name and description);
259- the name of the ``main'' function that serves as entry point in the program;
260- a collection of global variable declarations, consisting of
261  a name, initialization data, and additional information.
262
263The type of function descriptions and that of additional information
264for variables vary among the various intermediate languages and are
265taken as parameters to the [program] type.  The other parts of whole
266programs are common to all languages. *)
267
268record program (F,V: Type[0]) : Type[0] := {
269  prog_funct: list (ident × F);
270  prog_main: ident;
271  prog_vars: list (ident × (list init_data) × region × V)
272}.
273
274
275definition prog_funct_names ≝ λF,V: Type[0]. λp: program F V.
276  map ?? (fst ident F) (prog_funct ?? p).
277
278definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
279  map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
280
281(* * * Generic transformations over programs *)
282
283(* * We now define a general iterator over programs that applies a given
284  code transformation function to all function descriptions and leaves
285  the other parts of the program unchanged. *)
286(*
287Section TRANSF_PROGRAM.
288
289Variable A B V: Type.
290Variable transf: A -> B.
291*)
292
293definition transf_program : ∀A,B. (A → B) → list (ident × A) → list (ident × B) ≝
294λA,B,transf,l.
295  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
296
297definition transform_program : ∀A,B,V. (A → B) → program A V → program B V ≝
298λA,B,V,transf,p.
299  mk_program B V
300    (transf_program ?? transf (prog_funct A V p))
301    (prog_main A V p)
302    (prog_vars A V p).
303(*
304lemma transform_program_function:
305  ∀A,B,V,transf,p,i,tf.
306  in_list ? 〈i, tf〉 (prog_funct ?? (transform_program A B V transf p)) →
307  ∃f. in_list ? 〈i, f〉 (prog_funct ?? p) ∧ transf f = tf.
308normalize; #A #B #V #transf #p #i #tf #H elim (list_in_map_inv ????? H);
309#x elim x; #i' #tf' *; #e #H destruct; %{tf'} /2/;
310qed.
311*)
312(*
313End TRANSF_PROGRAM.
314
315(** The following is a variant of [transform_program] where the
316  code transformation function can fail and therefore returns an
317  option type. *)
318
319Open Local Scope error_monad_scope.
320Open Local Scope string_scope.
321
322Section MAP_PARTIAL.
323
324Variable A B C: Type.
325Variable prefix_errmsg: A -> errmsg.
326Variable f: B -> res C.
327*)
328definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
329                         list (A × B) → res (list (A × C)) ≝
330λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).
331(*
332Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) :=
333  match l with
334  | nil => OK nil
335  | (a, b) :: rem =>
336      match f b with
337      | Error msg => Error (prefix_errmsg a ++ msg)%list
338      | OK c =>
339          do rem' <- map_partial rem;
340          OK ((a, c) :: rem')
341      end
342  end.
343
344Remark In_map_partial:
345  forall l l' a c,
346  map_partial l = OK l' ->
347  In (a, c) l' ->
348  exists b, In (a, b) l /\ f b = OK c.
349Proof.
350  induction l; simpl.
351  intros. inv H. elim H0.
352  intros until c. destruct a as [a1 b1].
353  caseEq (f b1); try congruence.
354  intro c1; intros. monadInv H0.
355  elim H1; intro. inv H0. exists b1; auto.
356  exploit IHl; eauto. intros [b [P Q]]. exists b; auto.
357Qed.
358
359Remark map_partial_forall2:
360  forall l l',
361  map_partial l = OK l' ->
362  list_forall2
363    (fun (a_b: A * B) (a_c: A * C) =>
364       fst a_b = fst a_c /\ f (snd a_b) = OK (snd a_c))
365    l l'.
366Proof.
367  induction l; simpl.
368  intros. inv H. constructor.
369  intro l'. destruct a as [a b].
370  caseEq (f b). 2: congruence. intro c; intros. monadInv H0. 
371  constructor. simpl. auto. auto.
372Qed.
373
374End MAP_PARTIAL.
375
376Remark map_partial_total:
377  forall (A B C: Type) (prefix: A -> errmsg) (f: B -> C) (l: list (A * B)),
378  map_partial prefix (fun b => OK (f b)) l =
379  OK (List.map (fun a_b => (fst a_b, f (snd a_b))) l).
380Proof.
381  induction l; simpl.
382  auto.
383  destruct a as [a1 b1]. rewrite IHl. reflexivity.
384Qed.
385
386Remark map_partial_identity:
387  forall (A B: Type) (prefix: A -> errmsg) (l: list (A * B)),
388  map_partial prefix (fun b => OK b) l = OK l.
389Proof.
390  induction l; simpl.
391  auto.
392  destruct a as [a1 b1]. rewrite IHl. reflexivity.
393Qed.
394
395Section TRANSF_PARTIAL_PROGRAM.
396
397Variable A B V: Type.
398Variable transf_partial: A -> res B.
399
400Definition prefix_funct_name (id: ident) : errmsg :=
401  MSG "In function " :: CTX id :: MSG ": " :: nil.
402*)
403definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝
404λA,B,V,transf_partial,p.
405  do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p);
406  OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)).
407(*
408Lemma transform_partial_program_function:
409  forall p tp i tf,
410  transform_partial_program p = OK tp ->
411  In (i, tf) tp.(prog_funct) ->
412  exists f, In (i, f) p.(prog_funct) /\ transf_partial f = OK tf.
413Proof.
414  intros. monadInv H. simpl in H0. 
415  eapply In_map_partial; eauto.
416Qed.
417
418Lemma transform_partial_program_main:
419  forall p tp,
420  transform_partial_program p = OK tp ->
421  tp.(prog_main) = p.(prog_main).
422Proof.
423  intros. monadInv H. reflexivity.
424Qed.
425
426Lemma transform_partial_program_vars:
427  forall p tp,
428  transform_partial_program p = OK tp ->
429  tp.(prog_vars) = p.(prog_vars).
430Proof.
431  intros. monadInv H. reflexivity.
432Qed.
433
434End TRANSF_PARTIAL_PROGRAM.
435
436(** The following is a variant of [transform_program_partial] where
437  both the program functions and the additional variable information
438  are transformed by functions that can fail. *)
439
440Section TRANSF_PARTIAL_PROGRAM2.
441
442Variable A B V W: Type.
443Variable transf_partial_function: A -> res B.
444Variable transf_partial_variable: V -> res W.
445
446Definition prefix_var_name (id_init: ident * list init_data) : errmsg :=
447  MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil.
448*)
449definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) →
450                                        program A V → res (program B W) ≝
451λA,B,V,W, transf_partial_function, transf_partial_variable, p.
452  do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p);
453  do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p);
454  OK ? (mk_program … fl (prog_main ?? p) vl).
455(*
456Lemma transform_partial_program2_function:
457  forall p tp i tf,
458  transform_partial_program2 p = OK tp ->
459  In (i, tf) tp.(prog_funct) ->
460  exists f, In (i, f) p.(prog_funct) /\ transf_partial_function f = OK tf.
461Proof.
462  intros. monadInv H. 
463  eapply In_map_partial; eauto.
464Qed.
465
466Lemma transform_partial_program2_variable:
467  forall p tp i tv,
468  transform_partial_program2 p = OK tp ->
469  In (i, tv) tp.(prog_vars) ->
470  exists v, In (i, v) p.(prog_vars) /\ transf_partial_variable v = OK tv.
471Proof.
472  intros. monadInv H.
473  eapply In_map_partial; eauto.
474Qed.
475
476Lemma transform_partial_program2_main:
477  forall p tp,
478  transform_partial_program2 p = OK tp ->
479  tp.(prog_main) = p.(prog_main).
480Proof.
481  intros. monadInv H. reflexivity.
482Qed.
483
484End TRANSF_PARTIAL_PROGRAM2.
485
486(** The following is a relational presentation of
487  [transform_program_partial2].  Given relations between function
488  definitions and between variable information, it defines a relation
489  between programs stating that the two programs have the same shape
490  (same global names, etc) and that identically-named function definitions
491  are variable information are related. *)
492
493Section MATCH_PROGRAM.
494
495Variable A B V W: Type.
496Variable match_fundef: A -> B -> Prop.
497Variable match_varinfo: V -> W -> Prop.
498
499Definition match_funct_entry (x1: ident * A) (x2: ident * B) :=
500  match x1, x2 with
501  | (id1, fn1), (id2, fn2) => id1 = id2 /\ match_fundef fn1 fn2
502  end.
503
504Definition match_var_entry (x1: ident * list init_data * V) (x2: ident * list init_data * W) :=
505  match x1, x2 with
506  | (id1, init1, info1), (id2, init2, info2) => id1 = id2 /\ init1 = init2 /\ match_varinfo info1 info2
507  end.
508
509Definition match_program (p1: program A V) (p2: program B W) : Prop :=
510  list_forall2 match_funct_entry p1.(prog_funct) p2.(prog_funct)
511  /\ p1.(prog_main) = p2.(prog_main)
512  /\ list_forall2 match_var_entry p1.(prog_vars) p2.(prog_vars).
513
514End MATCH_PROGRAM.
515
516Remark transform_partial_program2_match:
517  forall (A B V W: Type)
518         (transf_partial_function: A -> res B)
519         (transf_partial_variable: V -> res W)
520         (p: program A V) (tp: program B W),
521  transform_partial_program2 transf_partial_function transf_partial_variable p = OK tp ->
522  match_program
523    (fun fd tfd => transf_partial_function fd = OK tfd)
524    (fun info tinfo => transf_partial_variable info = OK tinfo)
525    p tp.
526Proof.
527  intros. monadInv H. split.
528  apply list_forall2_imply with
529    (fun (ab: ident * A) (ac: ident * B) =>
530       fst ab = fst ac /\ transf_partial_function (snd ab) = OK (snd ac)).
531  eapply map_partial_forall2. eauto.
532  intros. destruct v1; destruct v2; simpl in *. auto.
533  split. auto.
534  apply list_forall2_imply with
535    (fun (ab: ident * list init_data * V) (ac: ident * list init_data * W) =>
536       fst ab = fst ac /\ transf_partial_variable (snd ab) = OK (snd ac)).
537  eapply map_partial_forall2. eauto.
538  intros. destruct v1; destruct v2; simpl in *. destruct p0; destruct p1. intuition congruence.
539Qed.
540*)
541(* * * External functions *)
542
543(* * For most languages, the functions composing the program are either
544  internal functions, defined within the language, or external functions
545  (a.k.a. system calls) that emit an event when applied.  We define
546  a type for such functions and some generic transformation functions. *)
547
548record external_function : Type[0] ≝ {
549  ef_id: ident;
550  ef_sig: signature
551}.
552
553definition ExternalFunction ≝ external_function.
554definition external_function_tag ≝ ef_id.
555definition external_function_sig ≝ ef_sig.
556
557inductive fundef (F: Type[0]): Type[0] ≝
558  | Internal: F → fundef F
559  | External: external_function → fundef F.
560
561(* Implicit Arguments External [F]. *)
562(*
563Section TRANSF_FUNDEF.
564
565Variable A B: Type.
566Variable transf: A -> B.
567*)
568definition transf_fundef : ∀A,B. (A→B) → fundef A → fundef B ≝
569λA,B,transf,fd.
570  match fd with
571  [ Internal f ⇒ Internal ? (transf f)
572  | External ef ⇒ External ? ef
573  ].
574
575(*
576End TRANSF_FUNDEF.
577
578Section TRANSF_PARTIAL_FUNDEF.
579
580Variable A B: Type.
581Variable transf_partial: A -> res B.
582*)
583
584definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝
585λA,B,transf_partial,fd.
586  match fd with
587  [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f')
588  | External ef ⇒ OK ? (External ? ef)
589  ].
590(*
591End TRANSF_PARTIAL_FUNDEF.
592*)
593
594
595
596
597(* Partially merged stuff derived from the prototype cerco compiler. *)
598
599definition bool_to_Prop ≝
600 λb. match b with [ true ⇒ True | false ⇒ False ].
601
602(* dpm: should go to standard library *)
603let rec member (i: ident) (eq_i: ident → ident → bool)
604               (g: list ident) on g: Prop ≝
605  match g with
606  [ nil ⇒ False
607  | cons hd tl ⇒
608      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
609  ].
610
611(* TODO: merge in comparison definitions from Integers.ma. *)
612inductive Compare: Type[0] ≝
613  Compare_Equal: Compare
614| Compare_NotEqual: Compare
615| Compare_Less: Compare
616| Compare_Greater: Compare
617| Compare_LessEqual: Compare
618| Compare_GreaterEqual: Compare.
619
620(* XXX unused definitions
621inductive Cast: Type[0] ≝
622  Cast_Int: Byte → Cast
623| Cast_AddrSymbol: Identifier → Cast
624| Cast_StackOffset: Immediate → Cast.
625
626inductive Data: Type[0] ≝
627  Data_Reserve: nat → Data
628| Data_Int8: Byte → Data
629| Data_Int16: Word → Data.
630
631inductive DataSize: Type[0] ≝
632  DataSize_Byte: DataSize
633| DataSize_HalfWord: DataSize
634| DataSize_Word: DataSize.
635*)
636
637definition Trace ≝ list Identifier.
638
639(* dpm: how are floats represented? *)
640inductive cast: Type[0] ≝
641  | cast_int: Byte → cast                    (* integer constant *)
642  | cast_float: Byte → cast                  (* float constant *)
643  | cast_addr_symbol: ident → cast      (* address of a global symbol *)
644  | cast_stack_offset: Byte → cast.
645
646inductive op1: Type[0] ≝
647  | op_cast8_unsigned: op1   (**r 8-bit zero extension  *)
648  | op_cast8_signed: op1     (**r 8-bit sign extension  *)
649  | op_cast16_unsigned: op1  (**r 16-bit zero extension  *)
650  | op_cast16_signed: op1    (**r 16-bit sign extension *)
651  | op_neg_int: op1          (**r integer opposite *)
652  | op_not_bool: op1         (**r boolean negation  *)
653  | op_not_int: op1          (**r bitwise complement  *)
654  | op_negf: op1             (**r float opposite *)
655  | op_absf: op1             (**r float absolute value *)
656  | op_single_of_float: op1  (**r float truncation *)
657  | op_int_of_float: op1     (**r signed integer to float *)
658  | op_intu_of_float: op1    (**r unsigned integer to float *)
659  | op_float_of_int: op1     (**r float to signed integer *)
660  | op_float_of_intu: op1    (**r float to unsigned integer *)
661  | op_id: op1               (**r identity *)
662  | op_ptr_of_int: op1       (**r int to pointer *)
663  | op_int_of_ptr: op1.      (**r pointer to int *)
664
665inductive op2: Type[0] ≝
666  | op_add: op2         (**r integer addition *)
667  | op_sub: op2         (**r integer subtraction *)
668  | op_mul: op2         (**r integer multiplication *)
669  | op_div: op2         (**r integer signed division *)
670  | op_divu: op2        (**r integer unsigned division *)
671  | op_mod: op2         (**r integer signed modulus *)
672  | op_modu: op2        (**r integer unsigned modulus *)
673  | op_and: op2         (**r bitwise ``and'' *)
674  | op_or: op2          (**r bitwise ``or'' *)
675  | op_xor: op2         (**r bitwise ``xor'' *)
676  | op_shl: op2         (**r left shift *)
677  | op_shr: op2         (**r right signed shift *)
678  | op_shru: op2        (**r right unsigned shift *)
679  | op_addf: op2        (**r float addition *)
680  | op_subf: op2        (**r float subtraction *)
681  | op_mulf: op2        (**r float multiplication *)
682  | op_divf: op2        (**r float division *)
683  | op_cmp: Compare → op2   (**r integer signed comparison *)
684  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
685  | op_cmpf: Compare → op2  (**r float comparison *)
686  | op_addp: op2        (**r addition for a pointer and an integer *)
687  | op_subp: op2        (**r substraction for a pointer and a integer *)
688  | op_cmpp: Compare → op2. (**r pointer comparaison *)
Note: See TracBrowser for help on using the repository browser.