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

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

Make block type a little more abstract; remove knowledge about the old
representation for a pointer from the evaluation of lvalues.

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