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

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

First pass at moving regions to block type.

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