source: Deliverables/D3.1/C-semantics/Values.ma @ 478

Last change on this file since 478 was 478, checked in by campbell, 10 years ago

Prevent clashes between names in AST and other parts of the development.
(Noticed when trying a large example file.)

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