source: src/common/Values.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 6 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

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