source: src/common/Values.ma @ 2530

Last change on this file since 2530 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

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