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

Last change on this file since 583 was 583, checked in by campbell, 9 years ago

Abstract pointer offsets a little, similar to the changes for the prototype
proposed in Bologna.

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