source: src/common/FrontEndOps.ma @ 2044

Last change on this file since 2044 was 2032, checked in by sacerdot, 9 years ago

!! BEWARE: major commit !!

1) [affects everybody]

split for vectors renamed to vsplit to reduce ambiguity since split is
now also a function in the standard library.
Note: I have not been able to propagate the changes everywhere in
the front-end/back-end because some files do not compile

2) [affects everybody]

functions on Vectors copied both in the front and back-ends moved to
Vectors.ma

3) [affects only the back-end]

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