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

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

Some commentary.

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