source: src/common/FrontEndOps.ma @ 1872

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

Make binary operations in Cminor/RTLabs properly typed.
A few extra bits and pieces that help:
Separate out Clight operation classification to its own file.
Use dependently typed classification to refine the types.
Fix bug in cast simplification.
Remove memory_chunk in favour of the low-level typ, as this now contains
exactly the right amount of information (unlike in CompCert?).
Make Cminor/RTLabs comparisons produce an 8-bit result (and cast if
necessary).

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