source: C-semantics/Values.ma @ 82

Last change on this file since 82 was 14, checked in by campbell, 11 years ago

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File size: 27.3 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 "Coqlib.ma".
20include "AST.ma".
21include "Integers.ma".
22include "Floats.ma".
23
24include "Plogic/connectives.ma".
25
26ndefinition block ≝ Z.
27(*ndefinition eq_block ≝ zeq.*)
28
29(* * A value is either:
30- a machine integer;
31- a floating-point number;
32- a pointer: a pair of a memory address and an integer offset with respect
33  to this address;
34- the [Vundef] value denoting an arbitrary bit pattern, such as the
35  value of an uninitialized variable.
36*)
37
38ninductive val: Type[0] ≝
39  | Vundef: val
40  | Vint: int -> val
41  | Vfloat: float -> val
42  | Vptr: block -> int -> val.
43
44ndefinition Vzero: val ≝ Vint zero.
45ndefinition Vone: val ≝ Vint one.
46ndefinition Vmone: val ≝ Vint mone.
47
48ndefinition Vtrue: val ≝ Vint one.
49ndefinition Vfalse: val ≝ Vint zero.
50
51(*
52(** The module [Val] defines a number of arithmetic and logical operations
53  over type [val].  Most of these operations are straightforward extensions
54  of the corresponding integer or floating-point operations. *)
55
56Module Val.
57*)
58ndefinition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
59
60ndefinition has_type ≝ λv: val. λt: typ.
61  match v with
62  [ Vundef ⇒ True
63  | Vint _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
64  | Vfloat _ ⇒ match t with [ Tfloat ⇒ True | _ ⇒ False ]
65  | Vptr _ _ ⇒ match t with [ Tint ⇒ True | _ ⇒ False ]
66  | _ ⇒ False
67  ].
68
69nlet rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
70  match vl with
71  [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
72  | cons v1 vs ⇒ match tl with [ nil ⇒ False | cons t1 ts ⇒
73               has_type v1 t1 ∧ has_type_list vs ts ]
74  ].
75
76(* * Truth values.  Pointers and non-zero integers are treated as [True].
77  The integer 0 (also used to represent the null pointer) is [False].
78  [Vundef] and floats are neither true nor false. *)
79
80ndefinition is_true : val → Prop ≝ λv.
81  match v with
82  [ Vint n ⇒ n ≠ zero
83  | Vptr b ofs ⇒ True
84  | _ ⇒ False
85  ].
86
87ndefinition is_false : val → Prop ≝ λv.
88  match v with
89  [ Vint n ⇒ n = zero
90  | _ ⇒ False
91  ].
92
93ninductive bool_of_val: val → bool → Prop ≝
94  | bool_of_val_int_true:
95      ∀n. n ≠ zero → bool_of_val (Vint n) true
96  | bool_of_val_int_false:
97      bool_of_val (Vint zero) false
98  | bool_of_val_ptr:
99      ∀b,ofs. bool_of_val (Vptr b ofs) true.
100
101ndefinition neg : val → val ≝ λv.
102  match v with
103  [ Vint n ⇒ Vint (neg n)
104  | _ ⇒ Vundef
105  ].
106
107ndefinition negf : val → val ≝ λv.
108  match v with
109  [ Vfloat f ⇒ Vfloat (Fneg f)
110  | _ => Vundef
111  ].
112
113ndefinition absf : val → val ≝ λv.
114  match v with
115  [ Vfloat f ⇒ Vfloat (Fabs f)
116  | _ ⇒ Vundef
117  ].
118
119ndefinition intoffloat : val → val ≝ λv.
120  match v with
121  [ Vfloat f ⇒ Vint (intoffloat f)
122  | _ ⇒ Vundef
123  ].
124
125ndefinition intuoffloat : val → val ≝ λv.
126  match v with
127  [ Vfloat f ⇒ Vint (intuoffloat f)
128  | _ ⇒ Vundef
129  ].
130
131ndefinition floatofint : val → val ≝ λv.
132  match v with
133  [ Vint n ⇒ Vfloat (floatofint n)
134  | _ ⇒ Vundef
135  ].
136
137ndefinition floatofintu : val → val ≝ λv.
138  match v with
139  [ Vint n ⇒ Vfloat (floatofintu n)
140  | _ ⇒ Vundef
141  ].
142
143ndefinition notint : val → val ≝ λv.
144  match v with
145  [ Vint n ⇒ Vint (xor n mone)
146  | _ ⇒ Vundef
147  ].
148 
149(* FIXME: switch to alias, or rename, or … *)
150ndefinition int_eq : int → int → bool ≝ eq.
151ndefinition notbool : val → val ≝ λv.
152  match v with
153  [ Vint n ⇒ of_bool (int_eq n zero)
154  | Vptr b ofs ⇒ Vfalse
155  | _ ⇒ Vundef
156  ].
157
158ndefinition zero_ext ≝ λnbits: Z. λv: val.
159  match v with
160  [ Vint n ⇒ Vint (zero_ext nbits n)
161  | _ ⇒ Vundef
162  ].
163
164ndefinition sign_ext ≝ λnbits:Z. λv:val.
165  match v with
166  [ Vint i ⇒ Vint (sign_ext nbits i)
167  | _ ⇒ Vundef
168  ].
169
170ndefinition singleoffloat : val → val ≝ λv.
171  match v with
172  [ Vfloat f ⇒ Vfloat (singleoffloat f)
173  | _ ⇒ Vundef
174  ].
175
176ndefinition add ≝ λv1,v2: val.
177  match v1 with
178  [ Vint n1 ⇒ match v2 with
179    [ Vint n2 ⇒ Vint (add n1 n2)
180    | Vptr b2 ofs2 ⇒ Vptr b2 (add ofs2 n1)
181    | _ ⇒ Vundef ]
182  | Vptr b1 ofs1 ⇒ match v2 with
183    [ Vint n2 ⇒ Vptr b1 (add ofs1 n2)
184    | _ ⇒ Vundef ]
185  | _ ⇒ Vundef ].
186
187ndefinition sub ≝ λv1,v2: val.
188  match v1 with
189  [ Vint n1 ⇒ match v2 with
190    [ Vint n2 ⇒ Vint (sub n1 n2)
191    | _ ⇒ Vundef ]
192  | Vptr b1 ofs1 ⇒ match v2 with
193    [ Vint n2 ⇒ Vptr b1 (sub ofs1 n2)
194    | Vptr b2 ofs2 ⇒
195        if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
196    | _ ⇒ Vundef ]
197  | _ ⇒ Vundef ].
198
199ndefinition mul ≝ λv1, v2: val.
200  match v1 with
201  [ Vint n1 ⇒ match v2 with
202    [ Vint n2 ⇒ Vint (mul n1 n2)
203    | _ ⇒ Vundef ]
204  | _ ⇒ Vundef ].
205(*
206ndefinition divs ≝ λv1, v2: val.
207  match v1 with
208  [ Vint n1 ⇒ match v2 with
209    [ Vint n2 ⇒ Vint (divs n1 n2)
210    | _ ⇒ Vundef ]
211  | _ ⇒ Vundef ].
212
213Definition mods (v1 v2: val): val :=
214  match v1, v2 with
215  | Vint n1, Vint n2 =>
216      if Int.eq n2 Int.zero then Vundef else Vint(Int.mods n1 n2)
217  | _, _ => Vundef
218  end.
219
220Definition divu (v1 v2: val): val :=
221  match v1, v2 with
222  | Vint n1, Vint n2 =>
223      if Int.eq n2 Int.zero then Vundef else Vint(Int.divu n1 n2)
224  | _, _ => Vundef
225  end.
226
227Definition modu (v1 v2: val): val :=
228  match v1, v2 with
229  | Vint n1, Vint n2 =>
230      if Int.eq n2 Int.zero then Vundef else Vint(Int.modu n1 n2)
231  | _, _ => Vundef
232  end.
233*)
234ndefinition v_and ≝ λv1, v2: val.
235  match v1 with
236  [ Vint n1 ⇒ match v2 with
237    [ Vint n2 ⇒ Vint (i_and n1 n2)
238    | _ ⇒ Vundef ]
239  | _ ⇒ Vundef ].
240
241ndefinition or ≝ λv1, v2: val.
242  match v1 with
243  [ Vint n1 ⇒ match v2 with
244    [ Vint n2 ⇒ Vint (or n1 n2)
245    | _ ⇒ Vundef ]
246  | _ ⇒ Vundef ].
247
248ndefinition xor ≝ λv1, v2: val.
249  match v1 with
250  [ Vint n1 ⇒ match v2 with
251    [ Vint n2 ⇒ Vint (xor n1 n2)
252    | _ ⇒ Vundef ]
253  | _ ⇒ Vundef ].
254(*
255Definition shl (v1 v2: val): val :=
256  match v1, v2 with
257  | Vint n1, Vint n2 =>
258     if Int.ltu n2 Int.iwordsize
259     then Vint(Int.shl n1 n2)
260     else Vundef
261  | _, _ => Vundef
262  end.
263
264Definition shr (v1 v2: val): val :=
265  match v1, v2 with
266  | Vint n1, Vint n2 =>
267     if Int.ltu n2 Int.iwordsize
268     then Vint(Int.shr n1 n2)
269     else Vundef
270  | _, _ => Vundef
271  end.
272
273Definition shr_carry (v1 v2: val): val :=
274  match v1, v2 with
275  | Vint n1, Vint n2 =>
276     if Int.ltu n2 Int.iwordsize
277     then Vint(Int.shr_carry n1 n2)
278     else Vundef
279  | _, _ => Vundef
280  end.
281
282Definition shrx (v1 v2: val): val :=
283  match v1, v2 with
284  | Vint n1, Vint n2 =>
285     if Int.ltu n2 Int.iwordsize
286     then Vint(Int.shrx n1 n2)
287     else Vundef
288  | _, _ => Vundef
289  end.
290
291Definition shru (v1 v2: val): val :=
292  match v1, v2 with
293  | Vint n1, Vint n2 =>
294     if Int.ltu n2 Int.iwordsize
295     then Vint(Int.shru n1 n2)
296     else Vundef
297  | _, _ => Vundef
298  end.
299
300Definition rolm (v: val) (amount mask: int): val :=
301  match v with
302  | Vint n => Vint(Int.rolm n amount mask)
303  | _ => Vundef
304  end.
305
306Definition ror (v1 v2: val): val :=
307  match v1, v2 with
308  | Vint n1, Vint n2 =>
309     if Int.ltu n2 Int.iwordsize
310     then Vint(Int.ror n1 n2)
311     else Vundef
312  | _, _ => Vundef
313  end.
314*)
315ndefinition addf ≝ λv1,v2: val.
316  match v1 with
317  [ Vfloat f1 ⇒ match v2 with
318    [ Vfloat f2 ⇒ Vfloat (Fadd f1 f2)
319    | _ ⇒ Vundef ]
320  | _ ⇒ Vundef ].
321
322ndefinition subf ≝ λv1,v2: val.
323  match v1 with
324  [ Vfloat f1 ⇒ match v2 with
325    [ Vfloat f2 ⇒ Vfloat (Fsub f1 f2)
326    | _ ⇒ Vundef ]
327  | _ ⇒ Vundef ].
328
329ndefinition mulf ≝ λv1,v2: val.
330  match v1 with
331  [ Vfloat f1 ⇒ match v2 with
332    [ Vfloat f2 ⇒ Vfloat (Fmul f1 f2)
333    | _ ⇒ Vundef ]
334  | _ ⇒ Vundef ].
335
336ndefinition divf ≝ λv1,v2: val.
337  match v1 with
338  [ Vfloat f1 ⇒ match v2 with
339    [ Vfloat f2 ⇒ Vfloat (Fdiv f1 f2)
340    | _ ⇒ Vundef ]
341  | _ ⇒ Vundef ].
342
343ndefinition cmp_mismatch : comparison → val ≝ λc.
344  match c with
345  [ Ceq ⇒ Vfalse
346  | Cne ⇒ Vtrue
347  | _   ⇒ Vundef
348  ].
349
350ndefinition cmp ≝ λc: comparison. λv1,v2: val.
351  match v1 with
352  [ Vint n1 ⇒ match v2 with
353    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
354    | Vptr b2 ofs2 ⇒
355        if eq n1 zero then cmp_mismatch c else Vundef
356    | _ ⇒ Vundef ]
357  | Vptr b1 ofs1 ⇒ match v2 with
358    [ Vptr b2 ofs2 ⇒
359        if eqZb b1 b2
360        then of_bool (cmp c ofs1 ofs2)
361        else cmp_mismatch c
362    | Vint n2 ⇒
363        if eq n2 zero then cmp_mismatch c else Vundef
364    | _ ⇒ Vundef ]
365  | _ ⇒ Vundef ].
366
367ndefinition cmpu ≝ λc: comparison. λv1,v2: val.
368  match v1 with
369  [ Vint n1 ⇒ match v2 with
370    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
371    | Vptr b2 ofs2 ⇒
372        if eq n1 zero then cmp_mismatch c else Vundef
373    | _ ⇒ Vundef ]
374  | Vptr b1 ofs1 ⇒ match v2 with
375    [ Vptr b2 ofs2 ⇒
376        if eqZb b1 b2
377        then of_bool (cmpu c ofs1 ofs2)
378        else cmp_mismatch c
379    | Vint n2 ⇒
380        if eq n2 zero then cmp_mismatch c else Vundef
381    | _ ⇒ Vundef ]
382  | _ ⇒ Vundef ].
383
384ndefinition cmpf ≝ λc: comparison. λv1,v2: val.
385  match v1 with
386  [ Vfloat f1 ⇒ match v2 with
387    [ Vfloat f2 ⇒ of_bool (Fcmp c f1 f2)
388    | _ ⇒ Vundef ]
389  | _ ⇒ Vundef ].
390
391(* * [load_result] is used in the memory model (library [Mem])
392  to post-process the results of a memory read.  For instance,
393  consider storing the integer value [0xFFF] on 1 byte at a
394  given address, and reading it back.  If it is read back with
395  chunk [Mint8unsigned], zero-extension must be performed, resulting
396  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
397  is performed and [0xFFFFFFFF] is returned.   Type mismatches
398  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
399
400nlet rec load_result (chunk: memory_chunk) (v: val) ≝
401  match v with
402  [ Vint n ⇒
403    match chunk with
404    [ Mint8signed ⇒ Vint (sign_ext 8 n)
405    | Mint8unsigned ⇒ Vint (zero_ext 8 n)
406    | Mint16signed ⇒ Vint (sign_ext 16 n)
407    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
408    | Mint32 ⇒ Vint n
409    | _ ⇒ Vundef
410    ]
411  | Vptr b ofs ⇒
412    match chunk with
413    [ Mint32 ⇒ Vptr b ofs
414    | _ ⇒ Vundef
415    ]
416  | Vfloat f ⇒
417    match chunk with
418    [ Mfloat32 ⇒ Vfloat(singleoffloat f)
419    | Mfloat64 ⇒ Vfloat f
420    | _ ⇒ Vundef
421    ]
422  | _ ⇒ Vundef
423  ].
424
425(*
426(** Theorems on arithmetic operations. *)
427
428Theorem cast8unsigned_and:
429  forall x, zero_ext 8 x = and x (Vint(Int.repr 255)).
430Proof.
431  destruct x; simpl; auto. decEq.
432  change 255 with (two_p 8 - 1). apply Int.zero_ext_and. vm_compute; auto.
433Qed.
434
435Theorem cast16unsigned_and:
436  forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)).
437Proof.
438  destruct x; simpl; auto. decEq.
439  change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. vm_compute; auto.
440Qed.
441
442Theorem istrue_not_isfalse:
443  forall v, is_false v -> is_true (notbool v).
444Proof.
445  destruct v; simpl; try contradiction.
446  intros. subst i. simpl. discriminate.
447Qed.
448
449Theorem isfalse_not_istrue:
450  forall v, is_true v -> is_false (notbool v).
451Proof.
452  destruct v; simpl; try contradiction.
453  intros. generalize (Int.eq_spec i Int.zero).
454  case (Int.eq i Int.zero); intro.
455  contradiction. simpl. auto.
456  auto.
457Qed.
458
459Theorem bool_of_true_val:
460  forall v, is_true v -> bool_of_val v true.
461Proof.
462  intro. destruct v; simpl; intros; try contradiction.
463  constructor; auto. constructor.
464Qed.
465
466Theorem bool_of_true_val2:
467  forall v, bool_of_val v true -> is_true v.
468Proof.
469  intros. inversion H; simpl; auto.
470Qed.
471
472Theorem bool_of_true_val_inv:
473  forall v b, is_true v -> bool_of_val v b -> b = true.
474Proof.
475  intros. inversion H0; subst v b; simpl in H; auto.
476Qed.
477
478Theorem bool_of_false_val:
479  forall v, is_false v -> bool_of_val v false.
480Proof.
481  intro. destruct v; simpl; intros; try contradiction.
482  subst i;  constructor.
483Qed.
484
485Theorem bool_of_false_val2:
486  forall v, bool_of_val v false -> is_false v.
487Proof.
488  intros. inversion H; simpl; auto.
489Qed.
490
491Theorem bool_of_false_val_inv:
492  forall v b, is_false v -> bool_of_val v b -> b = false.
493Proof.
494  intros. inversion H0; subst v b; simpl in H.
495  congruence. auto. contradiction.
496Qed.
497
498Theorem notbool_negb_1:
499  forall b, of_bool (negb b) = notbool (of_bool b).
500Proof.
501  destruct b; reflexivity.
502Qed.
503
504Theorem notbool_negb_2:
505  forall b, of_bool b = notbool (of_bool (negb b)).
506Proof.
507  destruct b; reflexivity.
508Qed.
509
510Theorem notbool_idem2:
511  forall b, notbool(notbool(of_bool b)) = of_bool b.
512Proof.
513  destruct b; reflexivity.
514Qed.
515
516Theorem notbool_idem3:
517  forall x, notbool(notbool(notbool x)) = notbool x.
518Proof.
519  destruct x; simpl; auto.
520  case (Int.eq i Int.zero); reflexivity.
521Qed.
522
523Theorem add_commut: forall x y, add x y = add y x.
524Proof.
525  destruct x; destruct y; simpl; auto.
526  decEq. apply Int.add_commut.
527Qed.
528
529Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z).
530Proof.
531  destruct x; destruct y; destruct z; simpl; auto.
532  rewrite Int.add_assoc; auto.
533  rewrite Int.add_assoc; auto.
534  decEq. decEq. apply Int.add_commut.
535  decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc.
536  decEq. apply Int.add_commut.
537  decEq. rewrite Int.add_assoc. auto.
538Qed.
539
540Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
541Proof.
542  intros. rewrite (add_commut y z). rewrite <- add_assoc. apply add_commut.
543Qed.
544
545Theorem add_permut_4:
546  forall x y z t, add (add x y) (add z t) = add (add x z) (add y t).
547Proof.
548  intros. rewrite add_permut. rewrite add_assoc.
549  rewrite add_permut. symmetry. apply add_assoc.
550Qed.
551
552Theorem neg_zero: neg Vzero = Vzero.
553Proof.
554  reflexivity.
555Qed.
556
557Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y).
558Proof.
559  destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr.
560Qed.
561
562Theorem sub_zero_r: forall x, sub Vzero x = neg x.
563Proof.
564  destruct x; simpl; auto.
565Qed.
566
567Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)).
568Proof.
569  destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto.
570Qed.
571
572Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y).
573Proof.
574  intros. unfold sub, add.
575  destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto.
576Qed.
577
578Theorem sub_add_l:
579  forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i).
580Proof.
581  destruct v1; destruct v2; intros; simpl; auto.
582  rewrite Int.sub_add_l. auto.
583  rewrite Int.sub_add_l. auto.
584  case (zeq b b0); intro. rewrite Int.sub_add_l. auto. reflexivity.
585Qed.
586
587Theorem sub_add_r:
588  forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)).
589Proof.
590  destruct v1; destruct v2; intros; simpl; auto.
591  rewrite Int.sub_add_r. auto.
592  repeat rewrite Int.sub_add_opp. decEq.
593  repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
594  decEq. repeat rewrite Int.sub_add_opp.
595  rewrite Int.add_assoc. decEq. apply Int.neg_add_distr.
596  case (zeq b b0); intro. simpl. decEq.
597  repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq.
598  apply Int.neg_add_distr.
599  reflexivity.
600Qed.
601
602Theorem mul_commut: forall x y, mul x y = mul y x.
603Proof.
604  destruct x; destruct y; simpl; auto. decEq. apply Int.mul_commut.
605Qed.
606
607Theorem mul_assoc: forall x y z, mul (mul x y) z = mul x (mul y z).
608Proof.
609  destruct x; destruct y; destruct z; simpl; auto.
610  decEq. apply Int.mul_assoc.
611Qed.
612
613Theorem mul_add_distr_l:
614  forall x y z, mul (add x y) z = add (mul x z) (mul y z).
615Proof.
616  destruct x; destruct y; destruct z; simpl; auto.
617  decEq. apply Int.mul_add_distr_l.
618Qed.
619
620
621Theorem mul_add_distr_r:
622  forall x y z, mul x (add y z) = add (mul x y) (mul x z).
623Proof.
624  destruct x; destruct y; destruct z; simpl; auto.
625  decEq. apply Int.mul_add_distr_r.
626Qed.
627
628Theorem mul_pow2:
629  forall x n logn,
630  Int.is_power2 n = Some logn ->
631  mul x (Vint n) = shl x (Vint logn).
632Proof.
633  intros; destruct x; simpl; auto.
634  change 32 with (Z_of_nat Int.wordsize).
635  rewrite (Int.is_power2_range _ _ H). decEq. apply Int.mul_pow2. auto.
636Qed. 
637
638Theorem mods_divs:
639  forall x y, mods x y = sub x (mul (divs x y) y).
640Proof.
641  destruct x; destruct y; simpl; auto.
642  case (Int.eq i0 Int.zero); simpl. auto. decEq. apply Int.mods_divs.
643Qed.
644
645Theorem modu_divu:
646  forall x y, modu x y = sub x (mul (divu x y) y).
647Proof.
648  destruct x; destruct y; simpl; auto.
649  generalize (Int.eq_spec i0 Int.zero);
650  case (Int.eq i0 Int.zero); simpl. auto.
651  intro. decEq. apply Int.modu_divu. auto.
652Qed.
653
654Theorem divs_pow2:
655  forall x n logn,
656  Int.is_power2 n = Some logn ->
657  divs x (Vint n) = shrx x (Vint logn).
658Proof.
659  intros; destruct x; simpl; auto.
660  change 32 with (Z_of_nat Int.wordsize).
661  rewrite (Int.is_power2_range _ _ H).
662  generalize (Int.eq_spec n Int.zero);
663  case (Int.eq n Int.zero); intro.
664  subst n. compute in H. discriminate.
665  decEq. apply Int.divs_pow2. auto.
666Qed.
667
668Theorem divu_pow2:
669  forall x n logn,
670  Int.is_power2 n = Some logn ->
671  divu x (Vint n) = shru x (Vint logn).
672Proof.
673  intros; destruct x; simpl; auto.
674  change 32 with (Z_of_nat Int.wordsize).
675  rewrite (Int.is_power2_range _ _ H).
676  generalize (Int.eq_spec n Int.zero);
677  case (Int.eq n Int.zero); intro.
678  subst n. compute in H. discriminate.
679  decEq. apply Int.divu_pow2. auto.
680Qed.
681
682Theorem modu_pow2:
683  forall x n logn,
684  Int.is_power2 n = Some logn ->
685  modu x (Vint n) = and x (Vint (Int.sub n Int.one)).
686Proof.
687  intros; destruct x; simpl; auto.
688  generalize (Int.eq_spec n Int.zero);
689  case (Int.eq n Int.zero); intro.
690  subst n. compute in H. discriminate.
691  decEq. eapply Int.modu_and; eauto.
692Qed.
693
694Theorem and_commut: forall x y, and x y = and y x.
695Proof.
696  destruct x; destruct y; simpl; auto. decEq. apply Int.and_commut.
697Qed.
698
699Theorem and_assoc: forall x y z, and (and x y) z = and x (and y z).
700Proof.
701  destruct x; destruct y; destruct z; simpl; auto.
702  decEq. apply Int.and_assoc.
703Qed.
704
705Theorem or_commut: forall x y, or x y = or y x.
706Proof.
707  destruct x; destruct y; simpl; auto. decEq. apply Int.or_commut.
708Qed.
709
710Theorem or_assoc: forall x y z, or (or x y) z = or x (or y z).
711Proof.
712  destruct x; destruct y; destruct z; simpl; auto.
713  decEq. apply Int.or_assoc.
714Qed.
715
716Theorem xor_commut: forall x y, xor x y = xor y x.
717Proof.
718  destruct x; destruct y; simpl; auto. decEq. apply Int.xor_commut.
719Qed.
720
721Theorem xor_assoc: forall x y z, xor (xor x y) z = xor x (xor y z).
722Proof.
723  destruct x; destruct y; destruct z; simpl; auto.
724  decEq. apply Int.xor_assoc.
725Qed.
726
727Theorem shl_mul: forall x y, Val.mul x (Val.shl Vone y) = Val.shl x y.
728Proof.
729  destruct x; destruct y; simpl; auto.
730  case (Int.ltu i0 Int.iwordsize); auto.
731  decEq. symmetry. apply Int.shl_mul.
732Qed.
733
734Theorem shl_rolm:
735  forall x n,
736  Int.ltu n Int.iwordsize = true ->
737  shl x (Vint n) = rolm x n (Int.shl Int.mone n).
738Proof.
739  intros; destruct x; simpl; auto.
740  rewrite H. decEq. apply Int.shl_rolm. exact H.
741Qed.
742
743Theorem shru_rolm:
744  forall x n,
745  Int.ltu n Int.iwordsize = true ->
746  shru x (Vint n) = rolm x (Int.sub Int.iwordsize n) (Int.shru Int.mone n).
747Proof.
748  intros; destruct x; simpl; auto.
749  rewrite H. decEq. apply Int.shru_rolm. exact H.
750Qed.
751
752Theorem shrx_carry:
753  forall x y,
754  add (shr x y) (shr_carry x y) = shrx x y.
755Proof.
756  destruct x; destruct y; simpl; auto.
757  case (Int.ltu i0 Int.iwordsize); auto.
758  simpl. decEq. apply Int.shrx_carry.
759Qed.
760
761Theorem or_rolm:
762  forall x n m1 m2,
763  or (rolm x n m1) (rolm x n m2) = rolm x n (Int.or m1 m2).
764Proof.
765  intros; destruct x; simpl; auto.
766  decEq. apply Int.or_rolm.
767Qed.
768
769Theorem rolm_rolm:
770  forall x n1 m1 n2 m2,
771  rolm (rolm x n1 m1) n2 m2 =
772    rolm x (Int.modu (Int.add n1 n2) Int.iwordsize)
773           (Int.and (Int.rol m1 n2) m2).
774Proof.
775  intros; destruct x; simpl; auto.
776  decEq.
777  apply Int.rolm_rolm. apply int_wordsize_divides_modulus.
778Qed.
779
780Theorem rolm_zero:
781  forall x m,
782  rolm x Int.zero m = and x (Vint m).
783Proof.
784  intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero.
785Qed.
786
787Theorem addf_commut: forall x y, addf x y = addf y x.
788Proof.
789  destruct x; destruct y; simpl; auto. decEq. apply Float.addf_commut.
790Qed.
791
792Lemma negate_cmp_mismatch:
793  forall c,
794  cmp_mismatch (negate_comparison c) = notbool(cmp_mismatch c).
795Proof.
796  destruct c; reflexivity.
797Qed.
798
799Theorem negate_cmp:
800  forall c x y,
801  cmp (negate_comparison c) x y = notbool (cmp c x y).
802Proof.
803  destruct x; destruct y; simpl; auto.
804  rewrite Int.negate_cmp. apply notbool_negb_1.
805  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
806  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
807  case (zeq b b0); intro.
808  rewrite Int.negate_cmp. apply notbool_negb_1.
809  apply negate_cmp_mismatch.
810Qed.
811
812Theorem negate_cmpu:
813  forall c x y,
814  cmpu (negate_comparison c) x y = notbool (cmpu c x y).
815Proof.
816  destruct x; destruct y; simpl; auto.
817  rewrite Int.negate_cmpu. apply notbool_negb_1.
818  case (Int.eq i Int.zero). apply negate_cmp_mismatch. reflexivity.
819  case (Int.eq i0 Int.zero). apply negate_cmp_mismatch. reflexivity.
820  case (zeq b b0); intro.
821  rewrite Int.negate_cmpu. apply notbool_negb_1.
822  apply negate_cmp_mismatch.
823Qed.
824
825Lemma swap_cmp_mismatch:
826  forall c, cmp_mismatch (swap_comparison c) = cmp_mismatch c.
827Proof.
828  destruct c; reflexivity.
829Qed.
830 
831Theorem swap_cmp:
832  forall c x y,
833  cmp (swap_comparison c) x y = cmp c y x.
834Proof.
835  destruct x; destruct y; simpl; auto.
836  rewrite Int.swap_cmp. auto.
837  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
838  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
839  case (zeq b b0); intro.
840  subst b0. rewrite zeq_true. rewrite Int.swap_cmp. auto.
841  rewrite zeq_false. apply swap_cmp_mismatch. auto.
842Qed.
843
844Theorem swap_cmpu:
845  forall c x y,
846  cmpu (swap_comparison c) x y = cmpu c y x.
847Proof.
848  destruct x; destruct y; simpl; auto.
849  rewrite Int.swap_cmpu. auto.
850  case (Int.eq i Int.zero). apply swap_cmp_mismatch. auto.
851  case (Int.eq i0 Int.zero). apply swap_cmp_mismatch. auto.
852  case (zeq b b0); intro.
853  subst b0. rewrite zeq_true. rewrite Int.swap_cmpu. auto.
854  rewrite zeq_false. apply swap_cmp_mismatch. auto.
855Qed.
856
857Theorem negate_cmpf_eq:
858  forall v1 v2, notbool (cmpf Cne v1 v2) = cmpf Ceq v1 v2.
859Proof.
860  destruct v1; destruct v2; simpl; auto.
861  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1.
862  apply notbool_idem2.
863Qed.
864
865Theorem negate_cmpf_ne:
866  forall v1 v2, notbool (cmpf Ceq v1 v2) = cmpf Cne v1 v2.
867Proof.
868  destruct v1; destruct v2; simpl; auto.
869  rewrite Float.cmp_ne_eq. rewrite notbool_negb_1. auto.
870Qed.
871
872Lemma or_of_bool:
873  forall b1 b2, or (of_bool b1) (of_bool b2) = of_bool (b1 || b2).
874Proof.
875  destruct b1; destruct b2; reflexivity.
876Qed.
877
878Theorem cmpf_le:
879  forall v1 v2, cmpf Cle v1 v2 = or (cmpf Clt v1 v2) (cmpf Ceq v1 v2).
880Proof.
881  destruct v1; destruct v2; simpl; auto.
882  rewrite or_of_bool. decEq. apply Float.cmp_le_lt_eq.
883Qed.
884
885Theorem cmpf_ge:
886  forall v1 v2, cmpf Cge v1 v2 = or (cmpf Cgt v1 v2) (cmpf Ceq v1 v2).
887Proof.
888  destruct v1; destruct v2; simpl; auto.
889  rewrite or_of_bool. decEq. apply Float.cmp_ge_gt_eq.
890Qed.
891
892Definition is_bool (v: val) :=
893  v = Vundef \/ v = Vtrue \/ v = Vfalse.
894
895Lemma of_bool_is_bool:
896  forall b, is_bool (of_bool b).
897Proof.
898  destruct b; unfold is_bool; simpl; tauto.
899Qed.
900
901Lemma undef_is_bool: is_bool Vundef.
902Proof.
903  unfold is_bool; tauto.
904Qed.
905
906Lemma cmp_mismatch_is_bool:
907  forall c, is_bool (cmp_mismatch c).
908Proof.
909  destruct c; simpl; unfold is_bool; tauto.
910Qed.
911
912Lemma cmp_is_bool:
913  forall c v1 v2, is_bool (cmp c v1 v2).
914Proof.
915  destruct v1; destruct v2; simpl; try apply undef_is_bool.
916  apply of_bool_is_bool.
917  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
918  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
919  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
920Qed.
921
922Lemma cmpu_is_bool:
923  forall c v1 v2, is_bool (cmpu c v1 v2).
924Proof.
925  destruct v1; destruct v2; simpl; try apply undef_is_bool.
926  apply of_bool_is_bool.
927  case (Int.eq i Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
928  case (Int.eq i0 Int.zero). apply cmp_mismatch_is_bool. apply undef_is_bool.
929  case (zeq b b0); intro. apply of_bool_is_bool. apply cmp_mismatch_is_bool.
930Qed.
931
932Lemma cmpf_is_bool:
933  forall c v1 v2, is_bool (cmpf c v1 v2).
934Proof.
935  destruct v1; destruct v2; simpl;
936  apply undef_is_bool || apply of_bool_is_bool.
937Qed.
938
939Lemma notbool_is_bool:
940  forall v, is_bool (notbool v).
941Proof.
942  destruct v; simpl.
943  apply undef_is_bool. apply of_bool_is_bool.
944  apply undef_is_bool. unfold is_bool; tauto.
945Qed.
946
947Lemma notbool_xor:
948  forall v, is_bool v -> v = xor (notbool v) Vone.
949Proof.
950  intros. elim H; intro. 
951  subst v. reflexivity.
952  elim H0; intro; subst v; reflexivity.
953Qed.
954
955Lemma rolm_lt_zero:
956  forall v, rolm v Int.one Int.one = cmp Clt v (Vint Int.zero).
957Proof.
958  intros. destruct v; simpl; auto.
959  transitivity (Vint (Int.shru i (Int.repr (Z_of_nat Int.wordsize - 1)))).
960  decEq. symmetry. rewrite Int.shru_rolm. auto. auto.
961  rewrite Int.shru_lt_zero. destruct (Int.lt i Int.zero); auto.
962Qed.
963
964Lemma rolm_ge_zero:
965  forall v,
966  xor (rolm v Int.one Int.one) (Vint Int.one) = cmp Cge v (Vint Int.zero).
967Proof.
968  intros. rewrite rolm_lt_zero. destruct v; simpl; auto.
969  destruct (Int.lt i Int.zero); auto.
970Qed.
971*)
972(* * The ``is less defined'' relation between values.
973    A value is less defined than itself, and [Vundef] is
974    less defined than any value. *)
975
976ninductive Val_lessdef: val → val → Prop ≝
977  | lessdef_refl: ∀v. Val_lessdef v v
978  | lessdef_undef: ∀v. Val_lessdef Vundef v.
979
980ninductive lessdef_list: list val → list val → Prop ≝
981  | lessdef_list_nil:
982      lessdef_list (nil ?) (nil ?)
983  | lessdef_list_cons:
984      ∀v1,v2,vl1,vl2.
985      Val_lessdef v1 v2 → lessdef_list vl1 vl2 →
986      lessdef_list (v1 :: vl1) (v2 :: vl2).
987
988(*Hint Resolve lessdef_refl lessdef_undef lessdef_list_nil lessdef_list_cons.*)
989
990nlemma lessdef_list_inv:
991  ∀vl1,vl2. lessdef_list vl1 vl2 → vl1 = vl2 ∨ in_list ? Vundef vl1.
992#vl1; nelim vl1;
993##[ #vl2; #H; ninversion H; /2/; #h1;#h2;#t1;#t2;#H1;#H2;#H3;#Hbad; ndestruct
994##| #h;#t;#IH;#vl2;#H;
995    ninversion H;
996    ##[ #H'; ndestruct
997    ##| #h1;#h2;#t1;#t2;#H1;#H2;#H3;#e1;#e2; ndestruct;
998        nelim H1;
999        ##[ nelim (IH t2 H2);
1000            ##[ #e; ndestruct; /2/;
1001            ##| /3/ ##]
1002        ##| /3/ ##]
1003    ##]
1004##] nqed.
1005
1006nlemma load_result_lessdef:
1007  ∀chunk,v1,v2.
1008  Val_lessdef v1 v2 → Val_lessdef (load_result chunk v1) (load_result chunk v2).
1009#chunk;#v1;#v2;#H; ninversion H; //; #v e1 e2; ncases chunk; nwhd in ⊢ (?%?); //;
1010nqed.
1011
1012(*
1013Lemma zero_ext_lessdef:
1014  forall n v1 v2, lessdef v1 v2 -> lessdef (zero_ext n v1) (zero_ext n v2).
1015Proof.
1016  intros; inv H; simpl; auto.
1017Qed.
1018*)
1019nlemma sign_ext_lessdef:
1020  ∀n,v1,v2. Val_lessdef v1 v2 → Val_lessdef (sign_ext n v1) (sign_ext n v2).
1021#n;#v1;#v2;#H;ninversion H;//;#v;#e1;#e2;nrewrite < e1 in H; nrewrite > e2; //;
1022nqed.
1023(*
1024Lemma singleoffloat_lessdef:
1025  forall v1 v2, lessdef v1 v2 -> lessdef (singleoffloat v1) (singleoffloat v2).
1026Proof.
1027  intros; inv H; simpl; auto.
1028Qed.
1029
1030End Val.
1031*)
Note: See TracBrowser for help on using the repository browser.