source: src/common/Values.ma @ 961

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

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File size: 37.0 KB
Line 
1(* *********************************************************************)
2(*                                                                     *)
3(*              The Compcert verified compiler                         *)
4(*                                                                     *)
5(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
6(*                                                                     *)
7(*  Copyright Institut National de Recherche en Informatique et en     *)
8(*  Automatique.  All rights reserved.  This file is distributed       *)
9(*  under the terms of the GNU General Public License as published by  *)
10(*  the Free Software Foundation, either version 2 of the License, or  *)
11(*  (at your option) any later version.  This file is also distributed *)
12(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
13(*                                                                     *)
14(* *********************************************************************)
15
16(* * This module defines the type of values that is used in the dynamic
17  semantics of all our intermediate languages. *)
18
19include "utilities/Coqlib.ma".
20include "common/AST.ma".
21include "common/Floats.ma".
22include "common/Errors.ma".
23
24include "ASM/BitVectorZ.ma".
25
26include "basics/logic.ma".
27
28include "utilities/extralib.ma".
29
30(* To define pointers we need a few details about the memory model.
31
32   There are several kinds of pointers, which differ in which regions of
33   memory they address and the pointer's representation.
34   
35   Pointers are given as kind, block, offset triples, where a block identifies
36   some memory in a given region with an arbitrary concrete address.  A proof
37   is also required that the representation is suitable for the region the
38   memory resides in.  Note that blocks cannot extend out of a region (in
39   particular, a pdata pointer can address any byte in a pdata block - we never
40   need to switch to a larger xdata pointer).
41 *)
42
43(* blocks - represented by the region the memory resides in and a unique id *)
44
45record block : Type[0] ≝
46{ block_region : region
47; block_id : Z
48}.
49
50definition eq_block ≝
51λb1,b2.
52  eq_region (block_region b1) (block_region b2) ∧
53  eqZb (block_id b1) (block_id b2)
54.
55
56lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
57  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
58  P (eq_block b1 b2).
59#P * #r1 #i1 * #r2 #i2 #H1 #H2
60whd in ⊢ (?%) @eq_region_elim #H3
61[ whd in ⊢ (?%) @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
62| @H2 % #E destruct elim H3 /2/
63] qed.
64
65lemma eq_block_b_b : ∀b. eq_block b b = true.
66* * #z whd in ⊢ (??%?) >eqZb_z_z @refl
67qed.
68
69(* Characterise the memory regions which the pointer representations can
70   address.
71
72   pointer_compat <block> <pointer representation> *)
73
74inductive pointer_compat : block → region → Prop ≝
75|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
76|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
77|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
78
79lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
80* * #id *;
81try ( %1 // )
82%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
83qed.
84
85definition is_pointer_compat : block → region → bool ≝
86λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
87
88(* Offsets into the block.  We allow integers like CompCert so that we have
89   the option of extending blocks backwards. *)
90
91record offset : Type[0] ≝ { offv : Z }.
92
93definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
94definition shift_offset : ∀n. offset → BitVector n → offset ≝
95  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
96(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
97definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
98  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
99definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
100  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
101definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
102  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
103definition sub_offset : ∀n. offset → offset → BitVector n ≝
104  λn,x,y. bitvector_of_Z ? (offv x - offv y).
105definition zero_offset ≝ mk_offset OZ.
106definition lt_offset : offset → offset → bool ≝
107  λx,y. Zltb (offv x) (offv y).
108
109(* * A value is either:
110- a machine integer;
111- a floating-point number;
112- a pointer: a triple giving the representation of the pointer (in terms of the
113             memory regions such a pointer could address), a memory address and
114             an integer offset with respect to this address;
115- a null pointer: the region denotes the representation (i.e., pointer size)
116- the [Vundef] value denoting an arbitrary bit pattern, such as the
117  value of an uninitialized variable.
118*)
119
120inductive val: Type[0] ≝
121  | Vundef: val
122  | Vint: ∀sz:intsize. bvint sz → val
123  | Vfloat: float → val
124  | Vnull: region → val
125  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
126
127definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
128definition Vone: intsize → val ≝ λsz. Vint sz (repr sz 1).
129definition mone ≝ λsz. bitvector_of_Z (bitsize_of_intsize sz) (neg one).
130definition Vmone: intsize → val ≝ λsz. Vint sz (mone ?).
131
132(* XXX 32bit booleans are Clight specific. *)
133definition Vtrue: val ≝ Vone I32.
134definition Vfalse: val ≝ Vzero I32.
135
136(* Values split into bytes.  Ideally we'd use some kind of sizeof for the
137   predicates here, but we don't (currently) have a single sizeof for Vundef.
138   We only split in stages of the compiler where all Vint values are byte sized.
139 *)
140
141definition ptr_may_be_single : region → bool ≝
142λr.match r with [ Data ⇒ true | IData ⇒ true | _ ⇒ false ].
143
144definition may_be_single : val → Prop ≝
145λv. match v with
146[ Vundef ⇒ True
147| Vint _ _ ⇒ True
148| Vfloat _ ⇒ False
149| Vnull r ⇒ ptr_may_be_single r = true
150| Vptr r _ _ _ ⇒ ptr_may_be_single r = true
151].
152
153definition may_be_split : val → Prop ≝
154λv.match v with
155[ Vint _ _ ⇒ False
156| Vnull r ⇒ ptr_may_be_single r = false
157| Vptr r _ _ _ ⇒ ptr_may_be_single r = false
158| _ ⇒ True
159].
160
161inductive split_val : Type[0] ≝
162| Single : ∀v:val. may_be_single v → split_val
163| High   : ∀v:val. may_be_split v → split_val
164| Low    : ∀v:val. may_be_split v → split_val.
165
166notation > "vbox('do' _ ← e; break e')" with precedence 40 for @{'bind ${e} (λ_.${e'})}.
167(*
168let rec assert_nat_eq (m,n:nat) : res (m = n) ≝
169match m return λx.res (x = n) with
170[ O ⇒ match n return λx. res (O = x) with [ O ⇒ OK ? (refl ??) | _ ⇒ Error ? ]
171| S m' ⇒ match n return λx.res (S m' = x) with [ O ⇒ Error ? | S n' ⇒
172  do E ← assert_nat_eq m' n';
173  match E return λx.λ_. res (S m' = S x) with [ refl ⇒ OK ? (refl ??) ] ]
174].
175
176definition res_eq_nat : ∀m,n:nat. ∀P:nat → Type[0]. P m → res (P n) ≝
177λm,n,P,p.
178  do E ← assert_nat_eq m n;
179  match E return λx.λ_. res (P x) with [ refl ⇒ OK ? p ].
180
181definition break : ∀n:nat. val → res (Vector split_val n) ≝
182λn,v. match v return λv'. (may_be_single v' → ?) → (may_be_split v' → ?) → ? with
183[ Vundef ⇒ λs.λt. res_eq_nat 1 n ? (s I)
184| Vint i ⇒ λs.λt. res_eq_nat 1 n ? (s I)
185| Vfloat f ⇒ λs.λt. res_eq_nat 2 n ? (t I)
186| Vnull r ⇒
187    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with
188    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
189    | false ⇒ λs.λt. ?
190    ]
191| Vptr r b p o ⇒
192    match ptr_may_be_single r return λx. (x = true → ?) → (x = false → ?) → ? with
193    [ true ⇒ λs.λt. res_eq_nat 1 n ? (s (refl ??))
194    | false ⇒ λs.λt. ?
195    ]
196] (λp. [[ Single v p ]]) (λp. [[ Low v p; High v p ]]).
197@(res_eq_nat 2 n ? (t (refl ??))) qed. (* XXX: I have no idea why this fails if you do it directly. *)
198
199definition val_eq : val → val → bool ≝
200λx,y.
201match x with
202[ Vundef ⇒ match y with [ Vundef ⇒ true | _ ⇒ false ]
203| Vint i ⇒ match y with [ Vint j ⇒ eq i j | _ ⇒ false ]
204| Vfloat f ⇒ match y with [ Vfloat f' ⇒ match eq_dec f f' with [ inl _ ⇒ true | _ ⇒ false ] | _ ⇒ false ]
205| Vnull r ⇒ match y with [ Vnull r' ⇒ eq_region r r' | _ ⇒ false ]
206| Vptr r b p o ⇒ match y with [ Vptr r' b' p' o' ⇒ eq_region r r' ∧ eq_block b b' ∧ eq_offset o o' | _ ⇒ false ]
207].
208
209definition merge : ∀n:nat. Vector split_val n → res val ≝
210λn,s. match s with
211[ VEmpty ⇒ Error ?
212| VCons _ h1 t1 ⇒
213  match t1 with
214  [ VEmpty ⇒ match h1 with [ Single v _ ⇒ OK ? v | _ ⇒ Error ? ]
215  | VCons _ h2 t2 ⇒
216    match t2 with
217    [ VEmpty ⇒ match h1 with [ Low v _ ⇒ match h2 with [ High v' _ ⇒ if val_eq v v' then OK ? v else Error ? | _ ⇒ Error ? ] | _ ⇒ Error ? ]
218    | VCons _ _ _ ⇒ Error ?
219    ]
220  ]
221].
222   
223*)
224(*
225(** The module [Val] defines a number of arithmetic and logical operations
226  over type [val].  Most of these operations are straightforward extensions
227  of the corresponding integer or floating-point operations. *)
228
229Module Val.
230*)
231definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
232(*
233definition has_type ≝ λv: val. λt: typ.
234  match v with
235  [ Vundef ⇒ True
236  | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
237  | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
238  | Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True | _ ⇒ False ]
239  | _ ⇒ False
240  ].
241
242let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
243  match vl with
244  [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
245  | cons v1 vs ⇒ match tl with [ nil ⇒ False | cons t1 ts ⇒
246               has_type v1 t1 ∧ has_type_list vs ts ]
247  ].
248*)
249(* * Truth values.  Pointers and non-zero integers are treated as [True].
250  The integer 0 (also used to represent the null pointer) is [False].
251  [Vundef] and floats are neither true nor false. *)
252
253definition is_true : val → Prop ≝ λv.
254  match v with
255  [ Vint _ n ⇒ n ≠ (zero ?)
256  | Vptr _ b _ ofs ⇒ True
257  | _ ⇒ False
258  ].
259
260definition is_false : val → Prop ≝ λv.
261  match v with
262  [ Vint _ n ⇒ n = (zero ?)
263  | Vnull _ ⇒ True
264  | _ ⇒ False
265  ].
266
267inductive bool_of_val: val → bool → Prop ≝
268  | bool_of_val_int_true:
269      ∀sz,n. n ≠ zero ? → bool_of_val (Vint sz n) true
270  | bool_of_val_int_false:
271      ∀sz. bool_of_val (Vzero sz) false
272  | bool_of_val_ptr:
273      ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
274  | bool_of_val_null:
275      ∀r. bool_of_val (Vnull r) true.
276
277axiom ValueNotABoolean : String.
278
279definition eval_bool_of_val : val → res bool ≝
280λv. match v with
281[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
282| Vnull _ ⇒ OK ? false
283| Vptr _ _ _ _ ⇒ OK ? true
284| _ ⇒ Error ? (msg ValueNotABoolean)
285].
286
287definition neg : val → val ≝ λv.
288  match v with
289  [ Vint sz n ⇒ Vint sz (two_complement_negation ? n)
290  | _ ⇒ Vundef
291  ].
292
293definition negf : val → val ≝ λv.
294  match v with
295  [ Vfloat f ⇒ Vfloat (Fneg f)
296  | _ => Vundef
297  ].
298
299definition absf : val → val ≝ λv.
300  match v with
301  [ Vfloat f ⇒ Vfloat (Fabs f)
302  | _ ⇒ Vundef
303  ].
304
305definition intoffloat : intsize → val → val ≝ λsz,v.
306  match v with
307  [ Vfloat f ⇒ Vint sz (intoffloat ? f)
308  | _ ⇒ Vundef
309  ].
310
311definition intuoffloat : intsize → val → val ≝ λsz,v.
312  match v with
313  [ Vfloat f ⇒ Vint sz (intuoffloat ? f)
314  | _ ⇒ Vundef
315  ].
316
317definition floatofint : val → val ≝ λv.
318  match v with
319  [ Vint sz n ⇒ Vfloat (floatofint ? n)
320  | _ ⇒ Vundef
321  ].
322
323definition floatofintu : val → val ≝ λv.
324  match v with
325  [ Vint sz n ⇒ Vfloat (floatofintu ? n)
326  | _ ⇒ Vundef
327  ].
328
329definition notint : val → val ≝ λv.
330  match v with
331  [ Vint sz n ⇒ Vint sz (exclusive_disjunction_bv ? n (mone ?))
332  | _ ⇒ Vundef
333  ].
334 
335definition notbool : val → val ≝ λv.
336  match v with
337  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
338  | Vptr _ b _ ofs ⇒ Vfalse
339  | Vnull _ ⇒ Vtrue
340  | _ ⇒ Vundef
341  ].
342
343definition zero_ext ≝ λrsz: intsize. λv: val.
344  match v with
345  [ Vint sz n ⇒ Vint rsz (zero_ext … n)
346  | _ ⇒ Vundef
347  ].
348
349definition sign_ext ≝ λrsz:intsize. λv:val.
350  match v with
351  [ Vint sz i ⇒ Vint rsz (sign_ext … i)
352  | _ ⇒ Vundef
353  ].
354
355definition singleoffloat : val → val ≝ λv.
356  match v with
357  [ Vfloat f ⇒ Vfloat (singleoffloat f)
358  | _ ⇒ Vundef
359  ].
360
361(* TODO: add zero to null? *)
362definition add ≝ λv1,v2: val.
363  match v1 with
364  [ Vint sz1 n1 ⇒ match v2 with
365    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
366                    (λn1. Vint sz2 (addition_n ? n1 n2))
367                    Vundef
368    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
369    | _ ⇒ Vundef ]
370  | Vptr r b1 p ofs1 ⇒ match v2 with
371    [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
372    | _ ⇒ Vundef ]
373  | _ ⇒ Vundef ].
374
375(* XXX Is I32 the best answer for ptr subtraction? *)
376
377definition sub ≝ λv1,v2: val.
378  match v1 with
379  [ Vint sz1 n1 ⇒ match v2 with
380    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
381                    (λn1. Vint sz2 (subtraction ? n1 n2))
382                    Vundef
383    | _ ⇒ Vundef ]
384  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
385    [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
386    | Vptr r2 b2 p2 ofs2 ⇒
387        if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
388    | _ ⇒ Vundef ]
389  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
390  | _ ⇒ Vundef ].
391
392definition mul ≝ λv1, v2: val.
393  match v1 with
394  [ Vint sz1 n1 ⇒ match v2 with
395    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
396                    (λn1. Vint sz2 (\snd (split … (multiplication ? n1 n2))))
397                    Vundef
398    | _ ⇒ Vundef ]
399  | _ ⇒ Vundef ].
400(*
401definition divs ≝ λv1, v2: val.
402  match v1 with
403  [ Vint n1 ⇒ match v2 with
404    [ Vint n2 ⇒ Vint (divs n1 n2)
405    | _ ⇒ Vundef ]
406  | _ ⇒ Vundef ].
407
408Definition mods (v1 v2: val): val :=
409  match v1, v2 with
410  | Vint n1, Vint n2 =>
411      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
412  | _, _ => Vundef
413  end.
414
415Definition divu (v1 v2: val): val :=
416  match v1, v2 with
417  | Vint n1, Vint n2 =>
418      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
419  | _, _ => Vundef
420  end.
421
422Definition modu (v1 v2: val): val :=
423  match v1, v2 with
424  | Vint n1, Vint n2 =>
425      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
426  | _, _ => Vundef
427  end.
428*)
429definition v_and ≝ λv1, v2: val.
430  match v1 with
431  [ Vint sz1 n1 ⇒ match v2 with
432    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
433                    (λn1. Vint ? (conjunction_bv ? n1 n2))
434                    Vundef
435    | _ ⇒ Vundef ]
436  | _ ⇒ Vundef ].
437
438definition or ≝ λv1, v2: val.
439  match v1 with
440  [ Vint sz1 n1 ⇒ match v2 with
441    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
442                    (λn1. Vint ? (inclusive_disjunction_bv ? n1 n2))
443                    Vundef
444    | _ ⇒ Vundef ]
445  | _ ⇒ Vundef ].
446
447definition xor ≝ λv1, v2: val.
448  match v1 with
449  [ Vint sz1 n1 ⇒ match v2 with
450    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
451                    (λn1. Vint ? (exclusive_disjunction_bv ? n1 n2))
452                    Vundef
453    | _ ⇒ Vundef ]
454  | _ ⇒ Vundef ].
455(*
456Definition shl (v1 v2: val): val :=
457  match v1, v2 with
458  | Vint n1, Vint n2 =>
459     if Int.ltu n2 Int.iwordsize
460     then Vint(Int.shl n1 n2)
461     else Vundef
462  | _, _ => Vundef
463  end.
464
465Definition shr (v1 v2: val): val :=
466  match v1, v2 with
467  | Vint n1, Vint n2 =>
468     if Int.ltu n2 Int.iwordsize
469     then Vint(Int.shr n1 n2)
470     else Vundef
471  | _, _ => Vundef
472  end.
473
474Definition shr_carry (v1 v2: val): val :=
475  match v1, v2 with
476  | Vint n1, Vint n2 =>
477     if Int.ltu n2 Int.iwordsize
478     then Vint(Int.shr_carry n1 n2)
479     else Vundef
480  | _, _ => Vundef
481  end.
482
483Definition shrx (v1 v2: val): val :=
484  match v1, v2 with
485  | Vint n1, Vint n2 =>
486     if Int.ltu n2 Int.iwordsize
487     then Vint(Int.shrx n1 n2)
488     else Vundef
489  | _, _ => Vundef
490  end.
491
492Definition shru (v1 v2: val): val :=
493  match v1, v2 with
494  | Vint n1, Vint n2 =>
495     if Int.ltu n2 Int.iwordsize
496     then Vint(Int.shru n1 n2)
497     else Vundef
498  | _, _ => Vundef
499  end.
500
501Definition rolm (v: val) (amount mask: int): val :=
502  match v with
503  | Vint n => Vint(Int.rolm n amount mask)
504  | _ => Vundef
505  end.
506
507Definition ror (v1 v2: val): val :=
508  match v1, v2 with
509  | Vint n1, Vint n2 =>
510     if Int.ltu n2 Int.iwordsize
511     then Vint(Int.ror n1 n2)
512     else Vundef
513  | _, _ => Vundef
514  end.
515*)
516definition addf ≝ λv1,v2: val.
517  match v1 with
518  [ Vfloat f1 ⇒ match v2 with
519    [ Vfloat f2 ⇒ Vfloat (Fadd f1 f2)
520    | _ ⇒ Vundef ]
521  | _ ⇒ Vundef ].
522
523definition subf ≝ λv1,v2: val.
524  match v1 with
525  [ Vfloat f1 ⇒ match v2 with
526    [ Vfloat f2 ⇒ Vfloat (Fsub f1 f2)
527    | _ ⇒ Vundef ]
528  | _ ⇒ Vundef ].
529
530definition mulf ≝ λv1,v2: val.
531  match v1 with
532  [ Vfloat f1 ⇒ match v2 with
533    [ Vfloat f2 ⇒ Vfloat (Fmul f1 f2)
534    | _ ⇒ Vundef ]
535  | _ ⇒ Vundef ].
536
537definition divf ≝ λv1,v2: val.
538  match v1 with
539  [ Vfloat f1 ⇒ match v2 with
540    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
541    | _ ⇒ Vundef ]
542  | _ ⇒ Vundef ].
543
544definition cmp_match : comparison → val ≝ λc.
545  match c with
546  [ Ceq ⇒ Vtrue
547  | Cne ⇒ Vfalse
548  | _   ⇒ Vundef
549  ].
550
551definition cmp_mismatch : comparison → val ≝ λc.
552  match c with
553  [ Ceq ⇒ Vfalse
554  | Cne ⇒ Vtrue
555  | _   ⇒ Vundef
556  ].
557
558definition cmp_offset ≝
559λc: comparison. λx,y:offset.
560  match c with
561  [ Ceq ⇒  eq_offset x y
562  | Cne ⇒ ¬eq_offset x y
563  | Clt ⇒  lt_offset x y
564  | Cle ⇒ ¬lt_offset y x
565  | Cgt ⇒  lt_offset y x
566  | Cge ⇒ ¬lt_offset x y
567  ].
568
569definition cmp_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
570λn,c,x,y.
571  match c with
572  [ Ceq ⇒ eq_bv ? x y
573  | Cne ⇒ notb (eq_bv ? x y)
574  | Clt ⇒ lt_s ? x y
575  | Cle ⇒ notb (lt_s ? y x)
576  | Cgt ⇒ lt_s ? y x
577  | Cge ⇒ notb (lt_s ? x y)
578  ].
579
580definition cmpu_int : ∀n. comparison → BitVector n → BitVector n → bool ≝
581λn,c,x,y.
582  match c with
583  [ Ceq ⇒ eq_bv ? x y
584  | Cne ⇒ notb (eq_bv ? x y)
585  | Clt ⇒ lt_u ? x y
586  | Cle ⇒ notb (lt_u ? y x)
587  | Cgt ⇒ lt_u ? y x
588  | Cge ⇒ notb (lt_u ? x y)
589  ].
590
591definition cmp ≝ λc: comparison. λv1,v2: val.
592  match v1 with
593  [ Vint sz1 n1 ⇒ match v2 with
594    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
595                    (λn1. of_bool (cmp_int ? c n1 n2))
596                    Vundef
597    | _ ⇒ Vundef ]
598  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
599    [ Vptr r2 b2 p2 ofs2 ⇒
600        if eq_block b1 b2
601        then of_bool (cmp_offset c ofs1 ofs2)
602        else cmp_mismatch c
603    | Vnull r2 ⇒ cmp_mismatch c
604    | _ ⇒ Vundef ]
605  | Vnull r1 ⇒ match v2 with
606    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
607    | Vnull r2 ⇒ cmp_match c
608    | _ ⇒ Vundef
609    ]
610  | _ ⇒ Vundef ].
611
612definition cmpu ≝ λc: comparison. λv1,v2: val.
613  match v1 with
614  [ Vint sz1 n1 ⇒ match v2 with
615    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
616                    (λn1. of_bool (cmpu_int ? c n1 n2))
617                    Vundef
618    | _ ⇒ Vundef ]
619  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
620    [ Vptr r2 b2 p2 ofs2 ⇒
621        if eq_block b1 b2
622        then of_bool (cmp_offset c ofs1 ofs2)
623        else cmp_mismatch c
624    | Vnull r2 ⇒ cmp_mismatch c
625    | _ ⇒ Vundef ]
626  | Vnull r1 ⇒ match v2 with
627    [ Vptr _ _ _ _ ⇒ cmp_mismatch c
628    | Vnull r2 ⇒ cmp_match c
629    | _ ⇒ Vundef
630    ]
631  | _ ⇒ Vundef ].
632
633definition cmpf ≝ λc: comparison. λsz:intsize. λv1,v2: val.
634  match v1 with
635  [ Vfloat f1 ⇒ match v2 with
636    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
637    | _ ⇒ Vundef ]
638  | _ ⇒ Vundef ].
639
640(* * [load_result] is used in the memory model (library [Mem])
641  to post-process the results of a memory read.  For instance,
642  consider storing the integer value [0xFFF] on 1 byte at a
643  given address, and reading it back.  If it is read back with
644  chunk [Mint8unsigned], zero-extension must be performed, resulting
645  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
646  is performed and [0xFFFFFFFF] is returned.   Type mismatches
647  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
648(* XXX update comment *)
649(* XXX is this even necessary now?
650       should we be able to extract bytes? *)
651
652let rec load_result (chunk: memory_chunk) (v: val) ≝
653  match v with
654  [ Vint sz n ⇒
655    match chunk with
656    [ Mint8signed ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
657    | Mint8unsigned ⇒ match sz with [ I8 ⇒ v | _ ⇒ Vundef ]
658    | Mint16signed ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
659    | Mint16unsigned ⇒ match sz with [ I16 ⇒ v | _ ⇒ Vundef ]
660    | Mint32 ⇒  match sz with [ I32 ⇒ v | _ ⇒ Vundef ]
661    | _ ⇒ Vundef
662    ]
663  | Vptr r b p ofs ⇒
664    match chunk with
665    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
666    | _ ⇒ Vundef
667    ]
668  | Vnull r ⇒
669    match chunk with
670    [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
671    | _ ⇒ Vundef
672    ]
673  | Vfloat f ⇒
674    match chunk with
675    [ Mfloat32 ⇒ Vfloat(singleoffloat f)
676    | Mfloat64 ⇒ Vfloat f
677    | _ ⇒ Vundef
678    ]
679  | _ ⇒ Vundef
680  ].
681
682(*
683(** Theorems on arithmetic operations. *)
684
685Theorem cast8unsigned_and:
686  forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
687Proof.
688  destruct x; simpl; auto. decEq.
689  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
690Qed.
691
692Theorem cast16unsigned_and:
693  forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
694Proof.
695  destruct x; simpl; auto. decEq.
696  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
697Qed.
698
699Theorem istrue_not_isfalse:
700  forall v, is_false v -> is_true (notbool v).
701Proof.
702  destruct v; simpl; try contradiction.
703  intros. subst i. simpl. discriminate.
704Qed.
705
706Theorem isfalse_not_istrue:
707  forall v, is_true v -> is_false (notbool v).
708Proof.
709  destruct v; simpl; try contradiction.
710  intros. generalize (Int.eq_spec i Int.zero).
711  case (Int.eq i Int.zero); intro.
712  contradiction. simpl. auto.
713  auto.
714Qed.
715
716Theorem bool_of_true_val:
717  forall v, is_true v -> bool_of_val v true.
718Proof.
719  intro. destruct v; simpl; intros; try contradiction.
720  constructor; auto. constructor.
721Qed.
722
723Theorem bool_of_true_val2:
724  forall v, bool_of_val v true -> is_true v.
725Proof.
726  intros. inversion H; simpl; auto.
727Qed.
728
729Theorem bool_of_true_val_inv:
730  forall v b, is_true v -> bool_of_val v b -> b = true.
731Proof.
732  intros. inversion H0; subst v b; simpl in H; auto.
733Qed.
734
735Theorem bool_of_false_val:
736  forall v, is_false v -> bool_of_val v false.
737Proof.
738  intro. destruct v; simpl; intros; try contradiction.
739  subst i;  constructor.
740Qed.
741
742Theorem bool_of_false_val2:
743  forall v, bool_of_val v false -> is_false v.
744Proof.
745  intros. inversion H; simpl; auto.
746Qed.
747
748Theorem bool_of_false_val_inv:
749  forall v b, is_false v -> bool_of_val v b -> b = false.
750Proof.
751  intros. inversion H0; subst v b; simpl in H.
752  congruence. auto. contradiction.
753Qed.
754
755Theorem notbool_negb_1:
756  forall b, of_bool (negb b) = notbool (of_bool b).
757Proof.
758  destruct b; reflexivity.
759Qed.
760
761Theorem notbool_negb_2:
762  forall b, of_bool b = notbool (of_bool (negb b)).
763Proof.
764  destruct b; reflexivity.
765Qed.
766
767Theorem notbool_idem2:
768  forall b, notbool(notbool(of_bool b)) = of_bool b.
769Proof.
770  destruct b; reflexivity.
771Qed.
772
773Theorem notbool_idem3:
774  forall x, notbool(notbool(notbool x)) = notbool x.
775Proof.
776  destruct x; simpl; auto.
777  case (Int.eq i Int.zero); reflexivity.
778Qed.
779
780Theorem add_commut: forall x y, add x y = add y x.
781Proof.
782  destruct x; destruct y; simpl; auto.
783  decEq. apply Int.add_commut.
784Qed.
785
786Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
787Proof.
788  destruct x; destruct y; destruct z; simpl; auto.
789  rewrite Int.add_assoc; auto.
790  rewrite Int.add_assoc; auto.
791  decEq. decEq. apply Int.add_commut.
792  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc.
793  decEq. apply Int.add_commut.
794  decEq. rewrite Int.add_assoc. auto.
795Qed.
796
797Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
798Proof.
799  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
800Qed.
801
802Theorem add_permut_4:
803  forall x y z t, add (add x y) (add z t) = add (add x z) (add y t).
804Proof.
805  intros. rewrite add_permut. rewrite add_assoc.
806  rewrite add_permut. symmetry. apply add_assoc.
807Qed.
808
809Theorem neg_zero: neg Vzero = Vzero.
810Proof.
811  reflexivity.
812Qed.
813
814Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
815Proof.
816  destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.
817Qed.
818
819Theorem sub_zero_r: forall x, sub Vzero x = neg x.
820Proof.
821  destruct x; simpl; auto.
822Qed.
823
824Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
825Proof.
826  destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
827Qed.
828
829Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
830Proof.
831  intros. unfold sub, add.
832  destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
833Qed.
834
835Theorem sub_add_l:
836  forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
837Proof.
838  destruct v1; destruct v2; intros; simpl; auto.
839  rewrite Int.sub_add_l. auto.
840  rewrite Int.sub_add_l. auto.
841  case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
842Qed.
843
844Theorem sub_add_r:
845  forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).
846Proof.
847  destruct v1; destruct v2; intros; simpl; auto.
848  rewrite Int.sub_add_r. auto.
849  repeat rewrite Int.sub_add_opp. decEq.
850  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
851  decEq. repeat rewrite Int.sub_add_opp.
852  rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
853  case (zeq b b0); intro. simpl. decEq.
854  repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
855  apply Int.neg_add_distr.
856  reflexivity.
857Qed.
858
859Theorem mul_commut: forall x y, mul x y = mul y x.
860Proof.
861  destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut.
862Qed.
863
864Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
865Proof.
866  destruct x; destruct y; destruct z; simpl; auto.
867  decEq. apply Int.mul_assoc.
868Qed.
869
870Theorem mul_add_distr_l:
871  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
872Proof.
873  destruct x; destruct y; destruct z; simpl; auto.
874  decEq. apply Int.mul_add_distr_l.
875Qed.
876
877
878Theorem mul_add_distr_r:
879  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
880Proof.
881  destruct x; destruct y; destruct z; simpl; auto.
882  decEq. apply Int.mul_add_distr_r.
883Qed.
884
885Theorem mul_pow2:
886  forall x n logn,
887  Int.is_power2 n = Some logn ->
888  mul x (Vint n) = shl x (Vint logn).
889Proof.
890  intros; destruct x; simpl; auto.
891  change 32 with (Z_of_nat Int.wordsize).
892  rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
893Qed. 
894
895Theorem mods_divs:
896  forall x y, mods x y = sub x (mul (divs x y) y).
897Proof.
898  destruct x; destruct y; simpl; auto.
899  case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs.
900Qed.
901
902Theorem modu_divu:
903  forall x y, modu x y = sub x (mul (divu x y) y).
904Proof.
905  destruct x; destruct y; simpl; auto.
906  generalize (Int.eq_spec i0 Int.zero);
907  case (Int.eq i0 Int.zero); simpl. auto.
908  intro. decEq. apply Int.modu_divu. auto.
909Qed.
910
911Theorem divs_pow2:
912  forall x n logn,
913  Int.is_power2 n = Some logn ->
914  divs x (Vint n) = shrx x (Vint logn).
915Proof.
916  intros; destruct x; simpl; auto.
917  change 32 with (Z_of_nat Int.wordsize).
918  rewrite (Int.is_power2_range _ _ H).
919  generalize (Int.eq_spec n Int.zero);
920  case (Int.eq n Int.zero); intro.
921  subst n. compute in H. discriminate.
922  decEq. apply Int.divs_pow2. auto.
923Qed.
924
925Theorem divu_pow2:
926  forall x n logn,
927  Int.is_power2 n = Some logn ->
928  divu x (Vint n) = shru x (Vint logn).
929Proof.
930  intros; destruct x; simpl; auto.
931  change 32 with (Z_of_nat Int.wordsize).
932  rewrite (Int.is_power2_range _ _ H).
933  generalize (Int.eq_spec n Int.zero);
934  case (Int.eq n Int.zero); intro.
935  subst n. compute in H. discriminate.
936  decEq. apply Int.divu_pow2. auto.
937Qed.
938
939Theorem modu_pow2:
940  forall x n logn,
941  Int.is_power2 n = Some logn ->
942  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).
943Proof.
944  intros; destruct x; simpl; auto.
945  generalize (Int.eq_spec n Int.zero);
946  case (Int.eq n Int.zero); intro.
947  subst n. compute in H. discriminate.
948  decEq. eapply Int.modu_and; eauto.
949Qed.
950
951Theorem and_commut: forall x y, and x y = and y x.
952Proof.
953  destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut.
954Qed.
955
956Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
957Proof.
958  destruct x; destruct y; destruct z; simpl; auto.
959  decEq. apply Int.and_assoc.
960Qed.
961
962Theorem or_commut: forall x y, or x y = or y x.
963Proof.
964  destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut.
965Qed.
966
967Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
968Proof.
969  destruct x; destruct y; destruct z; simpl; auto.
970  decEq. apply Int.or_assoc.
971Qed.
972
973Theorem xor_commut: forall x y, xor x y = xor y x.
974Proof.
975  destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut.
976Qed.
977
978Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
979Proof.
980  destruct x; destruct y; destruct z; simpl; auto.
981  decEq. apply Int.xor_assoc.
982Qed.
983
984Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
985Proof.
986  destruct x; destruct y; simpl; auto.
987  case (Int.ltu i0 Int.iwordsize); auto.
988  decEq. symmetry. apply Int.shl_mul.
989Qed.
990
991Theorem shl_rolm:
992  forall x n,
993  Int.ltu n Int.iwordsize = true ->
994  shl x (Vint n) = rolm x n (Int.shl Int.mone n).
995Proof.
996  intros; destruct x; simpl; auto.
997  rewrite H. decEq. apply Int.shl_rolm. exact H.
998Qed.
999
1000Theorem shru_rolm:
1001  forall x n,
1002  Int.ltu n Int.iwordsize = true ->
1003  shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).
1004Proof.
1005  intros; destruct x; simpl; auto.
1006  rewrite H. decEq. apply Int.shru_rolm. exact H.
1007Qed.
1008
1009Theorem shrx_carry:
1010  forall x y,
1011  add (shr x y) (shr_carry x y) = shrx x y.
1012Proof.
1013  destruct x; destruct y; simpl; auto.
1014  case (Int.ltu i0 Int.iwordsize); auto.
1015  simpl. decEq. apply Int.shrx_carry.
1016Qed.
1017
1018Theorem or_rolm:
1019  forall x n m1 m2,
1020  or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).
1021Proof.
1022  intros; destruct x; simpl; auto.
1023  decEq. apply Int.or_rolm.
1024Qed.
1025
1026Theorem rolm_rolm:
1027  forall x n1 m1 n2 m2,
1028  rolm (rolm x n1 m1) n2 m2 =
1029    rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
1030           (Int.and (Int.rol m1 n2) m2).
1031Proof.
1032  intros; destruct x; simpl; auto.
1033  decEq.
1034  apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
1035Qed.
1036
1037Theorem rolm_zero:
1038  forall x m,
1039  rolm x Int.zero m = and x (Vint m).
1040Proof.
1041  intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.
1042Qed.
1043
1044Theorem addf_commut: forall x y, addf x y = addf y x.
1045Proof.
1046  destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut.
1047Qed.
1048
1049Lemma negate_cmp_mismatch:
1050  forall c,
1051  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).
1052Proof.
1053  destruct c; reflexivity.
1054Qed.
1055
1056Theorem negate_cmp:
1057  forall c x y,
1058  cmp (negate_comparison c) x y = notbool (cmp c x y).
1059Proof.
1060  destruct x; destruct y; simpl; auto.
1061  rewrite Int.negate_cmp. apply notbool_negb_1.
1062  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
1063  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
1064  case (zeq b b0); intro.
1065  rewrite Int.negate_cmp. apply notbool_negb_1.
1066  apply negate_cmp_mismatch.
1067Qed.
1068
1069Theorem negate_cmpu:
1070  forall c x y,
1071  cmpu (negate_comparison c) x y = notbool (cmpu c x y).
1072Proof.
1073  destruct x; destruct y; simpl; auto.
1074  rewrite Int.negate_cmpu. apply notbool_negb_1.
1075  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
1076  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
1077  case (zeq b b0); intro.
1078  rewrite Int.negate_cmpu. apply notbool_negb_1.
1079  apply negate_cmp_mismatch.
1080Qed.
1081
1082Lemma swap_cmp_mismatch:
1083  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.
1084Proof.
1085  destruct c; reflexivity.
1086Qed.
1087 
1088Theorem swap_cmp:
1089  forall c x y,
1090  cmp (swap_comparison c) x y = cmp c y x.
1091Proof.
1092  destruct x; destruct y; simpl; auto.
1093  rewrite Int.swap_cmp. auto.
1094  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
1095  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
1096  case (zeq b b0); intro.
1097  subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto.
1098  rewrite zeq_false. apply swap_cmp_mismatch. auto.
1099Qed.
1100
1101Theorem swap_cmpu:
1102  forall c x y,
1103  cmpu (swap_comparison c) x y = cmpu c y x.
1104Proof.
1105  destruct x; destruct y; simpl; auto.
1106  rewrite Int.swap_cmpu. auto.
1107  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
1108  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
1109  case (zeq b b0); intro.
1110  subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto.
1111  rewrite zeq_false. apply swap_cmp_mismatch. auto.
1112Qed.
1113
1114Theorem negate_cmpf_eq:
1115  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
1116Proof.
1117  destruct v1; destruct v2; simpl; auto.
1118  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1.
1119  apply notbool_idem2.
1120Qed.
1121
1122Theorem negate_cmpf_ne:
1123  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
1124Proof.
1125  destruct v1; destruct v2; simpl; auto.
1126  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto.
1127Qed.
1128
1129Lemma or_of_bool:
1130  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
1131Proof.
1132  destruct b1; destruct b2; reflexivity.
1133Qed.
1134
1135Theorem cmpf_le:
1136  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
1137Proof.
1138  destruct v1; destruct v2; simpl; auto.
1139  rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq.
1140Qed.
1141
1142Theorem cmpf_ge:
1143  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
1144Proof.
1145  destruct v1; destruct v2; simpl; auto.
1146  rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq.
1147Qed.
1148
1149Definition is_bool (v: val) :=
1150  v = Vundef \/ v = Vtrue \/ v = Vfalse.
1151
1152Lemma of_bool_is_bool:
1153  forall b, is_bool (of_bool b).
1154Proof.
1155  destruct b; unfold is_bool; simpl; tauto.
1156Qed.
1157
1158Lemma undef_is_bool: is_bool Vundef.
1159Proof.
1160  unfold is_bool; tauto.
1161Qed.
1162
1163Lemma cmp_mismatch_is_bool:
1164  forall c, is_bool (cmp_mismatch c).
1165Proof.
1166  destruct c; simpl; unfold is_bool; tauto.
1167Qed.
1168
1169Lemma cmp_is_bool:
1170  forall c v1 v2, is_bool (cmp c v1 v2).
1171Proof.
1172  destruct v1; destruct v2; simpl; try apply undef_is_bool.
1173  apply of_bool_is_bool.
1174  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1175  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1176  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
1177Qed.
1178
1179Lemma cmpu_is_bool:
1180  forall c v1 v2, is_bool (cmpu c v1 v2).
1181Proof.
1182  destruct v1; destruct v2; simpl; try apply undef_is_bool.
1183  apply of_bool_is_bool.
1184  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1185  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
1186  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
1187Qed.
1188
1189Lemma cmpf_is_bool:
1190  forall c v1 v2, is_bool (cmpf c v1 v2).
1191Proof.
1192  destruct v1; destruct v2; simpl;
1193  apply undef_is_bool || apply of_bool_is_bool.
1194Qed.
1195
1196Lemma notbool_is_bool:
1197  forall v, is_bool (notbool v).
1198Proof.
1199  destruct v; simpl.
1200  apply undef_is_bool. apply of_bool_is_bool.
1201  apply undef_is_bool. unfold is_bool; tauto.
1202Qed.
1203
1204Lemma notbool_xor:
1205  forall v, is_bool v -> v = xor (notbool v) Vone.
1206Proof.
1207  intros. elim H; intro. 
1208  subst v. reflexivity.
1209  elim H0; intro; subst v; reflexivity.
1210Qed.
1211
1212Lemma rolm_lt_zero:
1213  forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
1214Proof.
1215  intros. destruct v; simpl; auto.
1216  transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
1217  decEq. symmetry. rewrite Int.shru_rolm. auto. auto.
1218  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.
1219Qed.
1220
1221Lemma rolm_ge_zero:
1222  forall v,
1223  xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
1224Proof.
1225  intros. rewrite rolm_lt_zero. destruct v; simpl; auto.
1226  destruct (Int.lt i Int.zero); auto.
1227Qed.
1228*)
1229(* * The ``is less defined'' relation between values.
1230    A value is less defined than itself, and [Vundef] is
1231    less defined than any value. *)
1232
1233inductive Val_lessdef: val → val → Prop ≝
1234  | lessdef_refl: ∀v. Val_lessdef v v
1235  | lessdef_undef: ∀v. Val_lessdef Vundef v.
1236
1237inductive lessdef_list: list val → list val → Prop ≝
1238  | lessdef_list_nil:
1239      lessdef_list (nil ?) (nil ?)
1240  | lessdef_list_cons:
1241      ∀v1,v2,vl1,vl2.
1242      Val_lessdef v1 v2 → lessdef_list vl1 vl2 →
1243      lessdef_list (v1 :: vl1) (v2 :: vl2).
1244
1245(*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*)
1246(*
1247lemma lessdef_list_inv:
1248  ∀vl1,vl2. lessdef_list vl1 vl2 → vl1 = vl2 ∨ in_list ? Vundef vl1.
1249#vl1 elim vl1;
1250[ #vl2 #H inversion H; /2/; #h1 #h2 #t1 #t2 #H1 #H2 #H3 #Hbad destruct
1251| #h #t #IH #vl2 #H
1252    inversion H;
1253    [ #H' destruct
1254    | #h1 #h2 #t1 #t2 #H1 #H2 #H3 #e1 #e2 destruct;
1255        elim H1;
1256        [ elim (IH t2 H2);
1257            [ #e destruct; /2/;
1258            | /3/ ]
1259        | /3/ ]
1260    ]
1261] qed.
1262*)
1263lemma load_result_lessdef:
1264  ∀chunk,v1,v2.
1265  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
1266#chunk #v1 #v2 #H inversion H; //; #v #e1 #e2 cases chunk
1267[ 8: #r ] whd in ⊢ (?%?); //;
1268qed.
1269
1270lemma zero_ext_lessdef:
1271  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (zero_ext n v1) (zero_ext n v2).
1272#n #v1 #v2 #H inversion H // #v #E1 #E2 destruct //
1273qed.
1274
1275lemma sign_ext_lessdef:
1276  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
1277#n #v1 #v2 #H inversion H // #v #e1 #e2 whd in ⊢ (?%?) //
1278qed.
1279(*
1280Lemma singleoffloat_lessdef:
1281  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).
1282Proof.
1283  intros; inv H; simpl; auto.
1284Qed.
1285
1286End Val.
1287*)
Note: See TracBrowser for help on using the repository browser.