source: src/common/FrontEndOps.ma @ 2783

Last change on this file since 2783 was 2582, checked in by garnier, 7 years ago

Some progress on CL to CM.

File size: 22.9 KB
Line 
1(* Operations common to the Cminor and RTLabs front end stages. *)
2
3(* Adapted from CompCert's Cminor.ma: *)
4
5(* *********************************************************************)
6(*                                                                     *)
7(*              The Compcert verified compiler                         *)
8(*                                                                     *)
9(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
10(*                                                                     *)
11(*  Copyright Institut National de Recherche en Informatique et en     *)
12(*  Automatique.  All rights reserved.  This file is distributed       *)
13(*  under the terms of the GNU General Public License as published by  *)
14(*  the Free Software Foundation, either version 2 of the License, or  *)
15(*  (at your option) any later version.  This file is also distributed *)
16(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
17(*                                                                     *)
18(* *********************************************************************)
19
20include "common/Values.ma".
21include "common/FrontEndMem.ma".
22
23inductive constant : typ → Type[0] ≝
24  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
25(*  | Ofloatconst: ∀sz. float → constant (ASTfloat sz) *)
26  | Oaddrsymbol: ident → nat → constant ASTptr (**r address of the symbol plus the offset *)
27  | Oaddrstack: nat → constant ASTptr.         (**r stack pointer plus the given offset *)
28
29definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr ⇒ True | _ ⇒ False ].
30
31inductive unary_operation : typ → typ → Type[0] ≝
32  | Ocastint: ∀sz,sg,sz',sg'. unary_operation (ASTint sz sg) (ASTint sz' sg')  (**r integer casts *)
33  | Onegint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r integer opposite *)
34  | Onotbool: ∀t,sz,sg. boolsrc t → unary_operation t (ASTint sz sg)           (**r boolean negation  *)
35  | Onotint:  ∀sz,sg. unary_operation (ASTint sz sg) (ASTint sz sg)            (**r bitwise complement  *)
36(*| Onegf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float opposite *)
37(*| Oabsf: ∀sz. unary_operation (ASTfloat sz) (ASTfloat sz)*)                  (**r float absolute value *)
38(*| Osingleoffloat: unary_operation (ASTfloat F64) (ASTfloat F32)*)            (**r float truncation *)
39(*| Ointoffloat:  ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Signed)*) (**r signed integer to float *)
40(*| Ointuoffloat: ∀fsz,sz. unary_operation (ASTfloat fsz) (ASTint sz Unsigned)*) (**r unsigned integer to float *)
41(*| Ofloatofint:  ∀fsz,sz. unary_operation (ASTint sz Signed) (ASTfloat fsz)*)   (**r float to signed integer *)
42(*| Ofloatofintu: ∀fsz,sz. unary_operation (ASTint sz Unsigned) (ASTfloat fsz)*) (**r float to unsigned integer *)
43  | Oid: ∀t. unary_operation t t                                               (**r identity (used to move between registers *)
44  | Optrofint: ∀sz,sg. unary_operation (ASTint sz sg) ASTptr                   (**r int to pointer with given representation *)
45  | Ointofptr: ∀sz,sg. unary_operation ASTptr (ASTint sz sg).                  (**r pointer to int *)
46
47inductive binary_operation : typ → typ → typ → Type[0] ≝
48  | Oadd:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer addition *)
49  | Osub:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer subtraction *)
50  | Omul:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r integer multiplication *)
51  | Odiv:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed division *)
52  | Odivu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned division *)
53  | Omod:  ∀sz.    binary_operation (ASTint sz Signed)   (ASTint sz Signed)   (ASTint sz Signed)   (**r integer signed modulus *)
54  | Omodu: ∀sz.    binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint sz Unsigned) (**r integer unsigned modulus *)
55  | Oand:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``and'' *)
56  | Oor:   ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``or'' *)
57  | Oxor:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r bitwise ``xor'' *)
58  | Oshl:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r left shift *)
59  | Oshr:  ∀sz,sg. binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint sz sg)       (**r right signed shift *)
60  | Oshru: ∀sz,sg. binary_operation (ASTint sz Unsigned) (ASTint sz sg)       (ASTint sz sg)       (**r right unsigned shift *)
61(*  | Oaddf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float addition *)
62(*  | Osubf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float subtraction *)
63(*  | Omulf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float multiplication *)
64(*  | Odivf: ∀sz.    binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTfloat sz)*)        (**r float division *)
65  | Ocmp: ∀sz,sg,sg'. comparison -> binary_operation (ASTint sz sg)       (ASTint sz sg)       (ASTint I8 sg') (**r integer signed comparison *)
66  | Ocmpu: ∀sz,sg'.   comparison -> binary_operation (ASTint sz Unsigned) (ASTint sz Unsigned) (ASTint I8 sg') (**r integer unsigned comparison *)
67(*  | Ocmpf: ∀sz,sg'.   comparison -> binary_operation (ASTfloat sz)        (ASTfloat sz)        (ASTint I8 sg') *) (**r float comparison *)
68  | Oaddpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r add an integer to a pointer *)
69  | Oaddip: ∀sz.   binary_operation  (ASTint sz Signed)  ASTptr                ASTptr              (**r add an integer to a pointer *)
70  | Osubpi: ∀sz.   binary_operation  ASTptr              (ASTint sz Signed)    ASTptr              (**r subtract int from a pointers *)
71  | Osubpp: ∀sz.   binary_operation  ASTptr               ASTptr              (ASTint sz Unsigned)   (**r subtract two pointers *)
72  | Ocmpp: ∀sg'. comparison → binary_operation ASTptr     ASTptr              (ASTint I8 sg').  (**r compare pointers *)
73
74
75lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
76val_typ v t →
77match t with
78[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
79(*| ASTfloat sz ⇒ ∀f.P (Vfloat f) *)
80| ASTptr ⇒ P Vnull ∧ ∀b,o. P (Vptr (mk_pointer b o))
81] →
82P v.
83#v #t #P *
84[ 1: //
85| * //
86| #b #o * //
87] qed.
88
89(* * Evaluation of constants and operator applications.
90    [None] is returned when the computation is undefined, e.g.
91    if arguments are of the wrong types, or in case of an integer division
92    by zero. *)
93
94definition eval_constant : ∀t. (ident → option block) → block → constant t → option val ≝
95λt,find_symbol,sp,cst.
96  match cst with
97  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
98(*  | Ofloatconst sz n ⇒ Some ? (Vfloat n)*)
99  | Oaddrsymbol s ofs ⇒
100      match find_symbol s with
101      [ None ⇒ None ?
102      | Some b ⇒ (*match pointer_compat_dec b r with
103                 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
104                 | inr _ ⇒ None ?
105                 ]*) Some ? (Vptr (mk_pointer b (shift_offset ? zero_offset (repr I16 ofs))))
106      ]
107  | Oaddrstack ofs ⇒
108      Some ? (Vptr (mk_pointer sp (shift_offset ? zero_offset (repr I16 ofs))))
109  ]. (*cases sp // qed.*)
110
111lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
112  eval_constant t f sp c = Some ? v →
113  val_typ v t.
114#t #f #sp *
115[ #sz #sg #i #v #E normalize in E; destruct //
116(*| #sz #f #v #E normalize in E; destruct //*)
117| #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
118(*  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct *)
119  //
120| #n #v #E whd in E:(??%?); destruct //
121] qed.
122
123definition eval_unop : ∀t,t'. unary_operation t t' → val → option val ≝
124λt,t',op,arg.
125  match op with
126  [ Ocastint sz sg sz' sg' ⇒
127      match sg with
128      [ Unsigned ⇒ Some ? (zero_ext sz' arg)
129      |   Signed ⇒ Some ? (sign_ext sz' arg)
130      ]
131  | Onegint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (two_complement_negation ? n1)) | _ ⇒ None ? ]
132  | Onotbool t sz sg _ ⇒
133      match arg with
134      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
135      | Vptr _ ⇒ Some ? (Vint sz (zero ?))
136      | Vnull ⇒ Some ? (Vint sz (repr ? 1))
137      | _ ⇒ None ?
138      ]
139  | Onotint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vint sz1 (exclusive_disjunction_bv ? n1 (mone ?))) | _ ⇒ None ? ]
140(*  | Onegf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fneg f1)) | _ ⇒ None ? ]
141  | Oabsf _ ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vfloat (Fabs f1)) | _ ⇒ None ? ]
142  | Osingleoffloat ⇒ Some ? (singleoffloat arg)
143  | Ointoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intoffloat ? f1)) | _ ⇒ None ? ]
144  | Ointuoffloat _ sz ⇒ match arg with [ Vfloat f1 ⇒ Some ? (Vint sz (intuoffloat ? f1)) | _ ⇒ None ? ]
145  | Ofloatofint _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofint ? n1)) | _ ⇒ None ? ]
146  | Ofloatofintu _ _ ⇒ match arg with [ Vint sz1 n1 ⇒ Some ? (Vfloat (floatofintu ? n1)) | _ ⇒ None ? ] *)
147  | Oid t ⇒ Some ? arg (* XXX should we restricted the values allowed? *)
148  (* Only conversion of null pointers is specified. *)
149  | Optrofint sz sg ⇒ match arg with [ Vint sz1 n1 ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
150  | Ointofptr sz sg ⇒ match arg with [ Vnull ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
151  ].
152
153lemma eval_unop_typ_correct : ∀t,t',op,v,v'.
154  val_typ v t →
155  eval_unop t t' op v = Some ? v' →
156  val_typ v' t'.
157#t #t' #op elim op
158[ #sz #sg #sz' #sg' #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?);
159  cases sg whd in ⊢ (??%? → ?); #E' destruct %
160| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E' destruct %
161| #t'' #sz #sg cases t''
162  [ #sz' #sg' #H #v #v' #H1 @(elim_val_typ … H1) #i whd in ⊢ (??%? → ?); #E' destruct cases (eq_bv ???) whd in ⊢ (?%?); %
163  | #H #v #v' #H1 @(elim_val_typ … H1) whd %
164    [ whd in ⊢ (??%? → ?); #E' destruct; %
165    | #b #o whd in ⊢ (??%? → ?); #E' destruct %
166    ]
167(*  | #f * *)
168  ]
169| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %
170(*
171| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
172| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
173| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
174| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
175| #fsz #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %
176| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
177| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
178*)
179| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
180| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
181  whd in ⊢ (??%? → ?); #E destruct //
182| #sz #sg #v #v' #H @(elim_val_typ … H) %
183  [ whd in ⊢ (??%? → ?); #E destruct %
184  | #b #o whd in ⊢ (??%? → ?); #E destruct
185  ]
186] qed.
187 
188(* I think this is duplicated somewhere else *)
189definition eval_compare_mismatch : comparison → option val ≝
190λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
191
192(* Individual operations, adapted from Values.  These differ in that they
193   implement the plain Cminor/RTLabs operations (e.g., with separate addition
194   for ints,floats and pointers) and use option rather than Vundef.  The ones
195   in Value are probably not needed. *)
196
197definition ev_add ≝ λv1,v2: val.
198  match v1 with
199  [ Vint sz1 n1 ⇒ match v2 with
200    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
201                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
202                    (None ?)
203    | _ ⇒ None ? ]
204  | _ ⇒ None ? ].
205
206definition ev_sub ≝ λv1,v2: val.
207  match v1 with
208  [ Vint sz1 n1 ⇒ match v2 with
209    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
210                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
211                    (None ?)
212    | _ ⇒ None ? ]
213  | _ ⇒ None ? ].
214
215(* NB: requires arguments to be presented pointer first. *)
216definition ev_addpi ≝ λv1,v2: val.
217  match v1 with
218  [ Vptr ptr1 ⇒ match v2 with
219    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
220    | _ ⇒ None ? ]
221  | Vnull ⇒ match v2 with
222    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
223    | _ ⇒ None ?
224    ]
225  | _ ⇒ None ? ].
226
227definition ev_subpi ≝ λv1,v2: val.
228  match v1 with
229  [ Vptr ptr1 ⇒ match v2 with
230    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
231    | _ ⇒ None ? ]
232  | Vnull ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
233  | _ ⇒ None ? ].
234
235definition ev_subpp ≝ λsz. λv1,v2: val.
236  match v1 with
237  [ Vptr ptr1 ⇒ match v2 with
238    [ Vptr ptr2 ⇒
239        if eq_block (pblock ptr1) (pblock ptr2)
240          then Some ? (Vint sz (sub_offset ? (poff ptr1) (poff ptr2)))
241          else None ?
242    | _ ⇒ None ? ]
243  | Vnull  ⇒ match v2 with [ Vnull  ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
244  | _ ⇒ None ? ].
245
246definition ev_mul ≝ λv1, v2: val.
247  match v1 with
248  [ Vint sz1 n1 ⇒ match v2 with
249    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
250                    (λn1. Some ? (Vint ? (short_multiplication ? n1 n2)))
251                    (None ?)
252    | _ ⇒ None ? ]
253  | _ ⇒ None ? ].
254
255definition ev_divs ≝ λv1, v2: val.
256  match v1 with
257  [ Vint sz1 n1 ⇒ match v2 with
258    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
259                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
260                    (None ?)
261    | _ ⇒ None ? ]
262  | _ ⇒ None ? ].
263
264definition ev_mods ≝ λv1, v2: val.
265  match v1 with
266  [ Vint sz1 n1 ⇒ match v2 with
267    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
268                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
269                    (None ?)
270    | _ ⇒ None ?
271    ]
272  | _ ⇒ None ?
273  ].
274
275definition ev_divu ≝ λv1, v2: val.
276  match v1 with
277  [ Vint sz1 n1 ⇒ match v2 with
278    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
279                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
280                    (None ?)
281    | _ ⇒ None ?
282    ]
283  | _ ⇒ None ?
284  ].
285
286definition ev_modu ≝ λv1, v2: val.
287  match v1 with
288  [ Vint sz1 n1 ⇒ match v2 with
289    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
290                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
291                    (None ?)
292    | _ ⇒ None ?
293    ]
294  | _ ⇒ None ?
295  ].
296
297definition ev_and ≝ λv1, v2: val.
298  match v1 with
299  [ Vint sz1 n1 ⇒ match v2 with
300    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
301                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2)))
302                    (None ?)
303    | _ ⇒ None ? ]
304  | _ ⇒ None ? ].
305
306definition ev_or ≝ λv1, v2: val.
307  match v1 with
308  [ Vint sz1 n1 ⇒ match v2 with
309    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
310                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
311                    (None ?)
312    | _ ⇒ None ? ]
313  | _ ⇒ None ? ].
314
315definition ev_xor ≝ λv1, v2: val.
316  match v1 with
317  [ Vint sz1 n1 ⇒ match v2 with
318    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
319                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
320                    (None ?)
321    | _ ⇒ None ? ]
322  | _ ⇒ None ? ].
323
324definition ev_shl ≝ λv1, v2: val.
325  match v1 with
326  [ Vint sz1 n1 ⇒ match v2 with
327    [ Vint sz2 n2 ⇒
328       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
329       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
330       else None ?
331    | _ ⇒ None ? ]
332  | _ ⇒ None ? ].
333
334definition ev_shr ≝ λv1, v2: val.
335  match v1 with
336  [ Vint sz1 n1 ⇒ match v2 with
337    [ Vint sz2 n2 ⇒
338       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
339       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
340       else None ?
341    | _ ⇒ None ? ]
342  | _ ⇒ None ? ].
343
344definition ev_shru ≝ λv1, v2: val.
345  match v1 with
346  [ Vint sz1 n1 ⇒ match v2 with
347    [ Vint sz2 n2 ⇒
348       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
349       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
350       else None ?
351    | _ ⇒ None ? ]
352  | _ ⇒ None ? ].
353
354(*
355definition ev_addf ≝ λv1,v2: val.
356  match v1 with
357  [ Vfloat f1 ⇒ match v2 with
358    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
359    | _ ⇒ None ? ]
360  | _ ⇒ None ? ].
361
362definition ev_subf ≝ λv1,v2: val.
363  match v1 with
364  [ Vfloat f1 ⇒ match v2 with
365    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
366    | _ ⇒ None ? ]
367  | _ ⇒ None ? ].
368
369definition ev_mulf ≝ λv1,v2: val.
370  match v1 with
371  [ Vfloat f1 ⇒ match v2 with
372    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
373    | _ ⇒ None ? ]
374  | _ ⇒ None ? ].
375
376definition ev_divf ≝ λv1,v2: val.
377  match v1 with
378  [ Vfloat f1 ⇒ match v2 with
379    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
380    | _ ⇒ None ? ]
381  | _ ⇒ None ? ]. *)
382
383definition FEtrue : val ≝ Vint I8 (repr I8 1).
384definition FEfalse : val ≝ Vint I8 (repr I8 0).
385definition FE_of_bool : bool → val ≝
386λb. if b then FEtrue else FEfalse.
387
388definition ev_cmp_match : comparison → option val ≝ λc.
389  match c with
390  [ Ceq ⇒ Some ? FEtrue
391  | Cne ⇒ Some ? FEfalse
392  | _   ⇒ None ?
393  ].
394
395definition ev_cmp_mismatch : comparison → option val ≝ λc.
396  match c with
397  [ Ceq ⇒ Some ? FEfalse
398  | Cne ⇒ Some ? FEtrue
399  | _   ⇒ None ?
400  ].
401
402definition ev_cmp ≝ λc: comparison. λv1,v2: val.
403  match v1 with
404  [ Vint sz1 n1 ⇒ match v2 with
405    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
406                    (λn1. Some ? (FE_of_bool (cmp_int ? c n1 n2)))
407                    (None ?)
408    | _ ⇒ None ? ]
409  | _ ⇒ None ? ].
410
411definition ev_cmpp ≝ λm. λc: comparison. λv1,v2: val.
412  match v1 with
413  [ Vptr ptr1 ⇒ match v2 with
414    [ Vptr ptr2 ⇒
415        if valid_pointer m ptr1 ∧ valid_pointer m ptr2
416        then
417          if eq_block (pblock ptr1) (pblock ptr2)
418          then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
419          else ev_cmp_mismatch c
420        else None ?
421    | Vnull  ⇒ ev_cmp_mismatch c
422    | _ ⇒ None ? ]
423  | Vnull  ⇒ match v2 with
424    [ Vptr _ ⇒ ev_cmp_mismatch c
425    | Vnull  ⇒ ev_cmp_match c
426    | _ ⇒ None ?
427    ]
428  | _ ⇒ None ? ].
429
430(* TODO: check this, it isn't the cmpu used elsewhere *)
431definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
432  match v1 with
433  [ Vint sz1 n1 ⇒ match v2 with
434    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
435                    (λn1. Some ? (FE_of_bool (cmpu_int ? c n1 n2)))
436                    (None ?)
437    | _ ⇒ None ? ]
438  | _ ⇒ None ? ].
439
440(*
441definition ev_cmpf ≝ λc: comparison. λv1,v2: val.
442  match v1 with
443  [ Vfloat f1 ⇒ match v2 with
444    [ Vfloat f2 ⇒ Some ? (FE_of_bool (Fcmp c f1 f2))
445    | _ ⇒ None ? ]
446  | _ ⇒ None ? ]. *)
447
448definition eval_binop : mem → ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝
449λm,t1,t2,t',op.
450  match op with
451  [ Oadd _ _ ⇒ ev_add
452  | Osub _ _ ⇒ ev_sub
453  | Omul _ _ ⇒ ev_mul
454  | Odiv _ ⇒ ev_divs
455  | Odivu _ ⇒ ev_divu
456  | Omod _ ⇒ ev_mods
457  | Omodu _ ⇒ ev_modu
458  | Oand _ _ ⇒ ev_and
459  | Oor _ _ ⇒ ev_or
460  | Oxor _ _ ⇒ ev_xor
461  | Oshl _ _ ⇒ ev_shl
462  | Oshr _ _ ⇒ ev_shr
463  | Oshru _ _ ⇒ ev_shru
464(*  | Oaddf _ ⇒ ev_addf
465  | Osubf _ ⇒ ev_subf
466  | Omulf _ ⇒ ev_mulf
467  | Odivf _ ⇒ ev_divf *)
468  | Ocmp _ _ _ c ⇒ ev_cmp c
469  | Ocmpu _ _ c ⇒ ev_cmpu c
470(*  | Ocmpf _ _ c ⇒ ev_cmpf c *)
471  | Oaddpi _ ⇒ ev_addpi
472  | Oaddip _ ⇒ (λx,y. ev_addpi y x)
473  | Osubpi _ ⇒ ev_subpi
474  | Osubpp sz ⇒ ev_subpp sz
475  | Ocmpp _ c ⇒ ev_cmpp m c
476  ].
477
478lemma eval_binop_typ_correct : ∀m,t1,t2,t',op,v1,v2,v'.
479  val_typ v1 t1 → val_typ v2 t2 →
480  eval_binop m t1 t2 t' op v1 v2 = Some ? v' →
481  val_typ v' t'.
482#m #t1x #t2x #tx' *
483[ 1,2,3,8,9,10:
484  #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
485  whd in ⊢ (??%? → ?); >intsize_eq_elim_true #E destruct //
486| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
487  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_s ???) [ | #res ] #E whd in E:(??%?); destruct //
488| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
489  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (division_u ???) [ | #res ] #E whd in E:(??%?); destruct //
490| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
491  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_s ???) [ | #res ] #E whd in E:(??%?); destruct //
492| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
493  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (modulus_u ???) [ | #res ] #E whd in E:(??%?); destruct //
494(* shifts *)
495| 11,12,13: #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
496  whd in ⊢ (??%? → ?); cases (lt_u ???) whd in ⊢ (??%? → ?); #E destruct //
497(* floats *)
498(*| 14,15,16,17: #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
499  whd in ⊢ (??%? → ?); #E destruct // *)
500(* comparisons *)
501| #sz #sg #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
502  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmp_int ????) #E destruct //
503| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2
504  whd in ⊢ (??%? → ?); >intsize_eq_elim_true cases (cmpu_int ????) #E destruct //
505(*| #sz #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #f1 @(elim_val_typ … V2) #f2
506  whd in ⊢ (??%? → ?); cases (Fcmp ???) #E destruct // *)
507(* pointers *)
508| 16,18: #sz  #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2,4: #b #o ] @(elim_val_typ … V2) #i2
509  whd in ⊢ (??%? → ?); [ 3,4: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
510| 17: #sz  #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) % [ 2: #b #o ]
511  whd in ⊢ (??%? → ?); [ 2: cases (eq_bv ???) whd in ⊢ (??%? → ?); | ] #E destruct //
512| #sz #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ | #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
513  whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?); | ] #E destruct //
514| #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ]
515  whd in ⊢ (??%? → ?); [ cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //
516] qed.
517
518
Note: See TracBrowser for help on using the repository browser.