source: src/common/FrontEndOps.ma @ 2407

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

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