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

Last change on this file since 535 was 500, checked in by campbell, 9 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.