blob: 81688ca6135503a8920af3e80090ffb3fb6f7052 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
Require Import Coqlib.
Require Import Integers.
Require Import Values.
Require Import Floats.
Require Import Memory.
Require Import Lia.
Definition bits_of_float x :=
match x with
| Vfloat f => Vlong (Float.to_bits f)
| _ => Vundef
end.
Definition bits_of_single x :=
match x with
| Vsingle f => Vint (Float32.to_bits f)
| _ => Vundef
end.
Definition float_of_bits x :=
match x with
| Vlong f => Vfloat (Float.of_bits f)
| _ => Vundef
end.
Definition single_of_bits x :=
match x with
| Vint f => Vsingle (Float32.of_bits f)
| _ => Vundef
end.
Definition bitwise_select_long b vtrue vfalse :=
Int64.or (Int64.and (Int64.neg b) vtrue)
(Int64.and (Int64.sub b Int64.one) vfalse).
Lemma bitwise_select_long_true :
forall vtrue vfalse,
bitwise_select_long Int64.one vtrue vfalse = vtrue.
Proof.
intros. unfold bitwise_select_long. cbn.
change (Int64.neg Int64.one) with Int64.mone.
rewrite Int64.and_commut.
rewrite Int64.and_mone.
rewrite Int64.sub_idem.
rewrite Int64.and_commut.
rewrite Int64.and_zero.
apply Int64.or_zero.
Qed.
Lemma bitwise_select_long_false :
forall vtrue vfalse,
bitwise_select_long Int64.zero vtrue vfalse = vfalse.
Proof.
intros. unfold bitwise_select_long. cbn.
rewrite Int64.neg_zero.
rewrite Int64.and_commut.
rewrite Int64.and_zero.
rewrite Int64.sub_zero_r.
change (Int64.neg Int64.one) with Int64.mone.
rewrite Int64.and_commut.
rewrite Int64.and_mone.
rewrite Int64.or_commut.
apply Int64.or_zero.
Qed.
Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val :=
match vb with
| (Vint b) =>
if Int.eq b Int.one
then vtrue
else if Int.eq b Int.zero
then vfalse
else Vundef
| _ => Vundef
end.
Lemma normalize_select01:
forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong).
Proof.
unfold select01_long.
intros.
destruct x; cbn; trivial.
destruct (Int.eq i Int.one); trivial.
destruct (Int.eq i Int.zero); trivial.
Qed.
|
