source: src/common/Values.ma @ 2755

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