source: src/common/FrontEndOps.ma @ 2530

Last change on this file since 2530 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

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: //
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(*
170| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
171| #sz #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
172| #v #v' #H @(elim_val_typ … H) #f whd in ⊢ (??%? → ?); #E destruct %2
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) #f whd in ⊢ (??%? → ?); #E destruct %
175| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
176| #fsz #sz #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); #E destruct %2
177*)
178| #t'' #v #v' #H whd in ⊢ (??%? → ?); #E destruct @H
179| #sz #sg #v #v' #H @(elim_val_typ … H) #i whd in ⊢ (??%? → ?); cases (eq_bv ???)
180  whd in ⊢ (??%? → ?); #E destruct //
181| #sz #sg #v #v' #H @(elim_val_typ … H) %
182  [ whd in ⊢ (??%? → ?); #E destruct %
183  | #b #o whd in ⊢ (??%? → ?); #E destruct
184  ]
185] qed.
186 
187(* I think this is duplicated somewhere else *)
188definition eval_compare_mismatch : comparison → option val ≝
189λc. match c with [ Ceq ⇒ Some ? Vfalse | Cne ⇒ Some ? Vtrue | _ ⇒ None ? ].
190
191(* Individual operations, adapted from Values.  These differ in that they
192   implement the plain Cminor/RTLabs operations (e.g., with separate addition
193   for ints,floats and pointers) and use option rather than Vundef.  The ones
194   in Value are probably not needed. *)
195
196definition ev_add ≝ λv1,v2: val.
197  match v1 with
198  [ Vint sz1 n1 ⇒ match v2 with
199    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
200                    (λn1. Some ? (Vint ? (addition_n ? n1 n2)))
201                    (None ?)
202    | _ ⇒ None ? ]
203  | _ ⇒ None ? ].
204
205definition ev_sub ≝ λv1,v2: val.
206  match v1 with
207  [ Vint sz1 n1 ⇒ match v2 with
208    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
209                    (λn1. Some ? (Vint ? (subtraction ? n1 n2)))
210                    (None ?)
211    | _ ⇒ None ? ]
212  | _ ⇒ None ? ].
213
214(* NB: requires arguments to be presented pointer first. *)
215definition ev_addp ≝ λv1,v2: val.
216  match v1 with
217  [ Vptr ptr1 ⇒ match v2 with
218    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
219    | _ ⇒ None ? ]
220  | Vnull ⇒ match v2 with
221    [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ?
222    | _ ⇒ None ?
223    ]
224  | _ ⇒ None ? ].
225
226definition ev_subpi ≝ λv1,v2: val.
227  match v1 with
228  [ Vptr ptr1 ⇒ match v2 with
229    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
230    | _ ⇒ None ? ]
231  | Vnull ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? | _ ⇒ None ? ]
232  | _ ⇒ None ? ].
233
234definition ev_subpp ≝ λsz. λv1,v2: val.
235  match v1 with
236  [ Vptr ptr1 ⇒ match v2 with
237    [ Vptr ptr2 ⇒
238        if eq_block (pblock ptr1) (pblock ptr2)
239          then Some ? (Vint sz (sub_offset ? (poff ptr1) (poff ptr2)))
240          else None ?
241    | _ ⇒ None ? ]
242  | Vnull  ⇒ match v2 with [ Vnull  ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
243  | _ ⇒ None ? ].
244
245definition ev_mul ≝ λ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. Some ? (Vint ? (short_multiplication ? n1 n2)))
250                    (None ?)
251    | _ ⇒ None ? ]
252  | _ ⇒ None ? ].
253
254definition ev_divs ≝ λv1, v2: val.
255  match v1 with
256  [ Vint sz1 n1 ⇒ match v2 with
257    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
258                    (λn1. option_map ?? (Vint ?) (division_s ? n1 n2))
259                    (None ?)
260    | _ ⇒ None ? ]
261  | _ ⇒ None ? ].
262
263definition ev_mods ≝ λv1, v2: val.
264  match v1 with
265  [ Vint sz1 n1 ⇒ match v2 with
266    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
267                    (λn1. option_map ?? (Vint ?) (modulus_s ? n1 n2))
268                    (None ?)
269    | _ ⇒ None ?
270    ]
271  | _ ⇒ None ?
272  ].
273
274definition ev_divu ≝ λv1, v2: val.
275  match v1 with
276  [ Vint sz1 n1 ⇒ match v2 with
277    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
278                    (λn1. option_map ?? (Vint ?) (division_u ? n1 n2))
279                    (None ?)
280    | _ ⇒ None ?
281    ]
282  | _ ⇒ None ?
283  ].
284
285definition ev_modu ≝ λv1, v2: val.
286  match v1 with
287  [ Vint sz1 n1 ⇒ match v2 with
288    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
289                    (λn1. option_map ?? (Vint ?) (modulus_u ? n1 n2))
290                    (None ?)
291    | _ ⇒ None ?
292    ]
293  | _ ⇒ None ?
294  ].
295
296definition ev_and ≝ λ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 ? (conjunction_bv ? n1 n2)))
301                    (None ?)
302    | _ ⇒ None ? ]
303  | _ ⇒ None ? ].
304
305definition ev_or ≝ λv1, v2: val.
306  match v1 with
307  [ Vint sz1 n1 ⇒ match v2 with
308    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
309                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2)))
310                    (None ?)
311    | _ ⇒ None ? ]
312  | _ ⇒ None ? ].
313
314definition ev_xor ≝ λv1, v2: val.
315  match v1 with
316  [ Vint sz1 n1 ⇒ match v2 with
317    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
318                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2)))
319                    (None ?)
320    | _ ⇒ None ? ]
321  | _ ⇒ None ? ].
322
323definition ev_shl ≝ λv1, v2: val.
324  match v1 with
325  [ Vint sz1 n1 ⇒ match v2 with
326    [ Vint sz2 n2 ⇒
327       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
328       then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
329       else None ?
330    | _ ⇒ None ? ]
331  | _ ⇒ None ? ].
332
333definition ev_shr ≝ λv1, v2: val.
334  match v1 with
335  [ Vint sz1 n1 ⇒ match v2 with
336    [ Vint sz2 n2 ⇒
337       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
338       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
339       else None ?
340    | _ ⇒ None ? ]
341  | _ ⇒ None ? ].
342
343definition ev_shru ≝ λv1, v2: val.
344  match v1 with
345  [ Vint sz1 n1 ⇒ match v2 with
346    [ Vint sz2 n2 ⇒
347       if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
348       then Some ? (Vint sz1 (shift_right ?? (nat_of_bitvector … n2) n1 false))
349       else None ?
350    | _ ⇒ None ? ]
351  | _ ⇒ None ? ].
352
353(*
354definition ev_addf ≝ λv1,v2: val.
355  match v1 with
356  [ Vfloat f1 ⇒ match v2 with
357    [ Vfloat f2 ⇒ Some ? (Vfloat (Fadd f1 f2))
358    | _ ⇒ None ? ]
359  | _ ⇒ None ? ].
360
361definition ev_subf ≝ λv1,v2: val.
362  match v1 with
363  [ Vfloat f1 ⇒ match v2 with
364    [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
365    | _ ⇒ None ? ]
366  | _ ⇒ None ? ].
367
368definition ev_mulf ≝ λv1,v2: val.
369  match v1 with
370  [ Vfloat f1 ⇒ match v2 with
371    [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
372    | _ ⇒ None ? ]
373  | _ ⇒ None ? ].
374
375definition ev_divf ≝ λv1,v2: val.
376  match v1 with
377  [ Vfloat f1 ⇒ match v2 with
378    [ Vfloat f2 ⇒ Some ? (Vfloat (Fdiv f1 f2))
379    | _ ⇒ None ? ]
380  | _ ⇒ None ? ]. *)
381
382definition FEtrue : val ≝ Vint I8 (repr I8 1).
383definition FEfalse : val ≝ Vint I8 (repr I8 0).
384definition FE_of_bool : bool → val ≝
385λb. if b then FEtrue else FEfalse.
386
387definition ev_cmp_match : comparison → option val ≝ λc.
388  match c with
389  [ Ceq ⇒ Some ? FEtrue
390  | Cne ⇒ Some ? FEfalse
391  | _   ⇒ None ?
392  ].
393
394definition ev_cmp_mismatch : comparison → option val ≝ λc.
395  match c with
396  [ Ceq ⇒ Some ? FEfalse
397  | Cne ⇒ Some ? FEtrue
398  | _   ⇒ None ?
399  ].
400
401definition ev_cmp ≝ λc: comparison. λv1,v2: val.
402  match v1 with
403  [ Vint sz1 n1 ⇒ match v2 with
404    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
405                    (λn1. Some ? (FE_of_bool (cmp_int ? c n1 n2)))
406                    (None ?)
407    | _ ⇒ None ? ]
408  | _ ⇒ None ? ].
409
410definition ev_cmpp ≝ λm. λc: comparison. λv1,v2: val.
411  match v1 with
412  [ Vptr ptr1 ⇒ match v2 with
413    [ Vptr ptr2 ⇒
414        if valid_pointer m ptr1 ∧ valid_pointer m ptr2
415        then
416          if eq_block (pblock ptr1) (pblock ptr2)
417          then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
418          else ev_cmp_mismatch c
419        else None ?
420    | Vnull  ⇒ ev_cmp_mismatch c
421    | _ ⇒ None ? ]
422  | Vnull  ⇒ match v2 with
423    [ Vptr _ ⇒ ev_cmp_mismatch c
424    | Vnull  ⇒ ev_cmp_match c
425    | _ ⇒ None ?
426    ]
427  | _ ⇒ None ? ].
428
429(* TODO: check this, it isn't the cmpu used elsewhere *)
430definition ev_cmpu ≝ λc: comparison. λv1,v2: val.
431  match v1 with
432  [ Vint sz1 n1 ⇒ match v2 with
433    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
434                    (λn1. Some ? (FE_of_bool (cmpu_int ? c n1 n2)))
435                    (None ?)
436    | _ ⇒ None ? ]
437  | _ ⇒ None ? ].
438
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| 16,17: #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 (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.