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

Last change on this file since 582 was 500, checked in by campbell, 10 years ago

Use dependent pointer type to ensure that the representation is always
compatible with the memory region used.
Add a couple of missing checks as a result...

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